text:
module HTML.Types

-- TODO: FIX ACCESS
%access public export

data TypeTag =
      Address
    | Article
    | Aside
    | Footer
    | H1
    | H2
    | H3
    | H4
    | H5
    | H6
    | Header
    | Hgroup
    | Main
    | Nav
    | Section
    | Blockquote
    | Dd
    | Div
    | Dl
    | Dt
    | Figcaption
    | Figure
    | Hr
    | Li
    | Ol
    | P
    | Pre
    | Ul
    | A
    | Abbr
    | B
    | Bdi
    | Bdo
    | Br
    | Cite
    | Code
    | Data
    | Dfn
    | Em
    | I
    | Kbd
    | Mark
    | Q
    | Rb
    | Rp
    | Rt
    | Rtc
    | Ruby
    | S
    | Samp
    | Small
    | Span
    | Strong
    | Sub
    | Sup
    | Time
    | U
    | Var
    | Wbr
    | Area
    | Audio
    | Img
    | Map
    | Track
    | Video
    | Embed
    | Iframe
    | Object
    | Param
    | Picture
    | Source
    | Canvas
    | Noscript
    | Script
    | Del
    | Ins
    | Caption
    | Col
    | Colgroup
    | Table
    | Tbody
    | Td
    | Tfoot
    | Th
    | Thead
    | Tr
    | Button
    | Datalist
    | Fieldset
    | Form
    | Input
    | Label
    | Legend
    | Meter
    | Optgroup
    | Option
    | Output
    | Progress
    | Select
    | Textarea
    | Details
    | Dialog
    | Menu
    | Menuitem
    | Summary
    | Slot
    | Template
    {-
    | Math
    | Svg
    -}

Eq TypeTag where
    Address == Address = True
    Article == Article = True
    Aside == Aside = True
    Footer == Footer = True
    H1 == H1 = True
    H2 == H2 = True
    H3 == H3 = True
    H4 == H4 = True
    H5 == H5 = True
    H6 == H6 = True
    Header == Header = True
    Hgroup == Hgroup = True
    Main == Main = True
    Nav == Nav = True
    Section == Section = True
    Blockquote == Blockquote = True
    Dd == Dd = True
    Div == Div = True
    Dl == Dl = True
    Dt == Dt = True
    Figcaption == Figcaption = True
    Figure == Figure = True
    Hr == Hr = True
    Li == Li = True
    Ol == Ol = True
    P == P = True
    Pre == Pre = True
    Ul == Ul = True
    A == A = True
    Abbr == Abbr = True
    B == B = True
    Bdi == Bdi = True
    Bdo == Bdo = True
    Br == Br = True
    Cite == Cite = True
    Code == Code = True
    Data == Data = True
    Dfn == Dfn = True
    Em == Em = True
    I == I = True
    Kbd == Kbd = True
    Mark == Mark = True
    Q == Q = True
    Rb == Rb = True
    Rp == Rp = True
    Rt == Rt = True
    Rtc == Rtc = True
    Ruby == Ruby = True
    S == S = True
    Samp == Samp = True
    Small == Small = True
    Span == Span = True
    Strong == Strong = True
    Sub == Sub = True
    Sup == Sup = True
    Time == Time = True
    U == U = True
    Var == Var = True
    Wbr == Wbr = True
    Area == Area = True
    Audio == Audio = True
    Img == Img = True
    Map == Map = True
    Track == Track = True
    Video == Video = True
    Embed == Embed = True
    Iframe == Iframe = True
    Object == Object = True
    Param == Param = True
    Picture == Picture = True
    Source == Source = True
    Canvas == Canvas = True
    Noscript == Noscript = True
    Script == Script = True
    Del == Del = True
    Ins == Ins = True
    Caption == Caption = True
    Col == Col = True
    Colgroup == Colgroup = True
    Table == Table = True
    Tbody == Tbody = True
    Td == Td = True
    Tfoot == Tfoot = True
    Th == Th = True
    Thead == Thead = True
    Tr == Tr = True
    Button == Button = True
    Datalist == Datalist = True
    Fieldset == Fieldset = True
    Form == Form = True
    Input == Input = True
    Label == Label = True
    Legend == Legend = True
    Meter == Meter = True
    Optgroup == Optgroup = True
    Option == Option = True
    Output == Output = True
    Progress == Progress = True
    Select == Select = True
    Textarea == Textarea = True
    Details == Details = True
    Dialog == Dialog = True
    Menu == Menu = True
    Menuitem == Menuitem = True
    Summary == Summary = True
    Slot == Slot = True
    Template == Template = True
    _ == _ = False

Show TypeTag where
    show type = case type of
        Address => "address"
        Article => "article"
        Aside => "aside"
        Footer => "footer"
        H1 => "h1"
        H2 => "h2"
        H3 => "h3"
        H4 => "h4"
        H5 => "h5"
        H6 => "h6"
        Header => "header"
        Hgroup => "hgroup"
        Main => "main"
        Nav => "nav"
        Section => "section"
        Blockquote => "blockquote"
        Dd => "dd"
        Div => "div"
        Dl => "dl"
        Dt => "dt"
        Figcaption => "figcaption"
        Figure => "figure"
        Hr => "hr"
        Li => "li"
        Ol => "ol"
        P => "p"
        Pre => "pre"
        Ul => "ul"
        A => "a"
        Abbr => "abbr"
        B => "b"
        Bdi => "bdi"
        Bdo => "bdo"
        Br => "br"
        Cite => "cite"
        Code => "code"
        Data => "data"
        Dfn => "dfn"
        Em => "em"
        I => "i"
        Kbd => "kbd"
        Mark => "mark"
        Q => "q"
        Rb => "rb"
        Rp => "rp"
        Rt => "rt"
        Rtc => "rtc"
        Ruby => "ruby"
        S => "s"
        Samp => "samp"
        Small => "small"
        Span => "span"
        Strong => "strong"
        Sub => "sub"
        Sup => "sup"
        Time => "time"
        U => "u"
        Var => "var"
        Wbr => "wbr"
        Area => "area"
        Audio => "audio"
        Img => "img"
        Map => "map"
        Track => "track"
        Video => "video"
        Embed => "embed"
        Iframe => "iframe"
        Object => "object"
        Param => "param"
        Picture => "picture"
        Source => "source"
        Canvas => "canvas"
        Noscript => "noscript"
        Script => "script"
        Del => "del"
        Ins => "ins"
        Caption => "caption"
        Col => "col"
        Colgroup => "colgroup"
        Table => "table"
        Tbody => "tbody"
        Td => "td"
        Tfoot => "tfoot"
        Th => "th"
        Thead => "thead"
        Tr => "tr"
        Button => "button"
        Datalist => "datalist"
        Fieldset => "fieldset"
        Form => "form"
        Input => "input"
        Label => "label"
        Legend => "legend"
        Meter => "meter"
        Optgroup => "optgroup"
        Option => "option"
        Output => "output"
        Progress => "progress"
        Select => "select"
        Textarea => "textarea"
        Details => "details"
        Dialog => "dialog"
        Menu => "menu"
        Menuitem => "menuitem"
        Summary => "summary"
        Slot => "slot"
        Template => "template"

record Attr where
  constructor MkAttr
  name, value : String

Show Attr where
    show (MkAttr name value) = name ++ "=\"" ++ value ++ "\""

data TextNode = MkTextNode String

Show TextNode where
    show (MkTextNode s) = s

mutual
    record Element where
        constructor MkElement
        type : TypeTag
        omitTag : Bool
        attrs : List Attr
        children : List HTMLElement

    data HTMLElement = MkHTMLElement Element | MkHTMLTextNode TextNode

mutual
    showHTMLElement : HTMLElement -> String
    showHTMLElement (MkHTMLElement elem) = showElement elem
    showHTMLElement (MkHTMLTextNode text) = show text

    showElement : Element -> String
    showElement (MkElement type omitTag attrs children) =
        "<" ++ (show type) ++ (showAttrs attrs) ++ (if omitTag then "/" else "") ++ ">" ++
        (showChildren children) ++
        (if not omitTag then "</" ++ (show type) ++ ">" else "")
        where
            showAttrs : List Attr -> String
            showAttrs Nil = ""
            showAttrs attrs' = " " ++ (foldl (++) "" $ intersperse " " $ map show attrs')
            showChildren : List HTMLElement -> String
            showChildren children' = foldl (\acc, elem => acc ++ (showHTMLElement elem)) "" children'

Show HTMLElement where
    show = showHTMLElement

Show Element where
    show = showElement

max_stars_repo_name: ebenpack/pamperscript

max_issues_repo_name: ebenpack/pamperscript

max_forks_repo_name: ebenpack/pamperscript


text:
-- ------------------------------------------------------------- [ Process.idr ]
--
-- Implementation of the echo protocol for process communication.
--
-- --------------------------------------------------------------------- [ EOH ]
module Chargen

import Effects
import Effect.StdIO
import Effect.Default
import Effect.Msg

import System.Protocol

import RFC.CharGen
import Utils

-- ---------------------------------------------------------- [ Server Process ]

||| Implementation of the Echo Protocol from the Server's perspective.
|||
||| @client The PID of the client process.
covering
chargenServer : (str : Stream Char)
              -> Nat
              -> (client : PID)
              -> Process (chargen) 'Server ['Client := client] [STDIO] ()
chargenServer str pos client = do
    msg <- recvFrom 'Client
    case msg of
      Just m => do
        let pos' = mod (pos + 1) 92
        let str' = take 92 $ drop pos' str
        sendTo 'Client (pack str')
        rec (chargenServer str (pos + 1) client)

      Nothing => return ()

-- ---------------------------------------------------------- [ Client Process ]

||| Implementation of the Echo Protocol from the Client's perspective.
|||
||| @server The PID of the server process.
-- covering
chargenClient : (server : PID)
              -> Process (chargen) 'Client ['Server := server] [STDIO] ()
chargenClient server = do
    putStrLn "To stop enter 'q':"
    msg_raw <- getStr
    case processMsg (trim msg_raw) of
      Nothing => do
        sendTo 'Server Nothing
      Just m => do
        sendTo 'Server (Just m)
        putStrLn !(recvFrom 'Server)
        rec (chargenClient server)
  where
    processMsg : String -> Maybe String
    processMsg msg = case msg == "q" of
                       True => Nothing
                       False => Just msg

-- ------------------------------------------------------ [ Sample Innvocation ]

||| Sample Innvocation of the Echo protocols between the client and
||| server functions.
-- covering
doChargenProcess : IO ()
doChargenProcess = runConc [()] doEcho'
  where
    doEcho' : Process (chargen) 'Client [] [STDIO] ()
    doEcho' = do
       server <- spawn (chargenServer dummyTextStream 0) [()]
       setChan 'Server server
       chargenClient server
       dropChan 'Server

-- -------------------------------------------------------------------- [ Main ]
namespace Main
  main : IO ()
  main = doChargenProcess

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

ext: idr

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module Main

import Data.IOArray

x: IOArray 20
x = [2,3,4]

main : IO ()
main = do printLn $ "hi"


text:
module Syntax.Tokens

-- Just token definition

public export
data Tkn
  = TknId       String
  | TknNum      Int
  | TknStr      String
  | TknComment  String
  | TknLPar
  | TknRPar
  | TknRCurly
  | TknLCurly
  | TknRSquare
  | TknLSquare
  | TknWhitespace
  | TknLB

public export
Show Tkn where
  show (TknId dt)      = "ID: " ++ show dt
  show (TknNum dt)     = "INT: " ++ show dt
  show (TknStr dt)     = "STR: " ++ show dt
  show (TknComment dt) = "COMMENT: " ++ show dt
  show TknLPar         = "\"(\""
  show TknRPar         = "\")\""
  show TknLCurly       = "\"{\""
  show TknRCurly       = "\"}\""
  show TknLSquare      = "\"[\""
  show TknRSquare      = "\"]\""
  show TknWhitespace   = "WHITESPACE"
  show TknLB           = "LB"

public export
[real] Show Tkn where
  show (TknId dt)      = dt
  show (TknNum dt)     = show dt
  show (TknStr dt)     = dt
  show (TknComment dt) = dt
  show TknLPar         = "\"(\""
  show TknRPar         = "\")\""
  show TknLCurly       = "\"{\""
  show TknRCurly       = "\"}\""
  show TknLSquare      = "\"[\""
  show TknRSquare      = "\"]\""
  show TknWhitespace   = " "
  show TknLB           = "\\n"

public export
Eq Tkn where
  (==) (TknId a)  (TknId b)          = a == b
  (==) (TknNum a) (TknNum b)         = a == b
  (==) (TknStr a) (TknStr b)         = a == b
  (==) (TknComment a) (TknComment b) = a == b
  (==) TknLPar TknLPar             = True
  (==) TknRPar TknRPar             = True
  (==) TknRCurly TknRCurly         = True
  (==) TknLCurly TknLCurly         = True
  (==) TknRSquare TknRSquare       = True
  (==) TknLSquare TknLSquare       = True
  (==) TknWhitespace TknWhitespace = True
  (==) TknLB TknLB                 = True
  (==) _ _ = False

public export
tokenName : Tkn -> String
tokenName (TknId _)      = "identifier"
tokenName (TknNum _)     = "int"
tokenName (TknStr _)     = "string"
tokenName (TknComment _) = "comment"
tokenName TknLPar        = "left parenthesis"
tokenName TknRPar        = "right parenthesis"
tokenName TknLCurly      = "left curly bracket"
tokenName TknRCurly      = "right curly bracket"
tokenName TknLSquare     = "left square bracket"
tokenName TknRSquare     = "right square bracket"
tokenName TknWhitespace  = "whitespace"
tokenName TknLB          = "line break"

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
module Gadgil.Ass1

import Evens

-- name your module as above

data IsOdd : Nat -> Type where
  OneOdd : IsOdd 1
  SSOdd : (n: Nat) -> IsOdd n -> IsOdd (S (S n))

notOddZ : IsOdd Z -> Void
notOddZ OneOdd impossible
notOddZ (SSOdd _ _) impossible

notOdd2: IsOdd 2 -> Void
notOdd2 (SSOdd Z OneOdd) impossible
notOdd2 (SSOdd Z (SSOdd _ _)) impossible

evenS : (n: Nat) -> IsEven n -> IsOdd (S n)
evenS Z ZEven = OneOdd
evenS (S (S k)) (SSEven k x) = SSOdd (S k) (evenS k x)


text:
-- Testing that unbound implicits get lifted appropriately

-- Should all be at the top
comp : (b -> c) -> (a -> b) -> a -> c

-- Leave 'a' where it is
comp2 : (b -> c) -> {a : _} -> (a -> b) -> a -> c


text:
module Core.LinearCheck

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Normalise
import Core.Options
import Core.UnifyState
import Core.Value
import Core.TT

import Data.List

%default covering

-- List of variable usages - we'll count the contents of specific variables
-- when discharging binders, to ensure that linear names are only used once
data Usage : List Name -> Type where
     Nil : Usage vars
     (::) : Var vars -> Usage vars -> Usage vars

Show (Usage vars) where
  show xs = "[" ++ showAll xs ++ "]"
    where
      showAll : Usage vs -> String
      showAll [] = ""
      showAll [el] = show el
      showAll (x :: xs) = show x ++ ", " ++ show xs

doneScope : Usage (n :: vars) -> Usage vars
doneScope [] = []
doneScope (MkVar First :: xs) = doneScope xs
doneScope (MkVar (Later p) :: xs) = MkVar p :: doneScope xs

(++) : Usage ns -> Usage ns -> Usage ns
(++) [] ys = ys
(++) (x :: xs) ys = x :: xs ++ ys

count : Nat -> Usage ns -> Nat
count p [] = 0
count p (v :: xs)
    = if p == varIdx v then 1 + count p xs else count p xs

localPrf : {later : _} -> Var (later ++ n :: vars)
localPrf {later = []} = MkVar First
localPrf {n} {vars} {later = (x :: xs)}
    = let MkVar p = localPrf {n} {vars} {later = xs} in
          MkVar (Later p)

mutual
  updateHoleUsageArgs : {vars : _} ->
                        {auto c : Ref Ctxt Defs} ->
                        {auto u : Ref UST UState} ->
                        (useInHole : Bool) ->
                        Var vars -> List (Var vars) ->
                        List (Term vars) -> Core Bool
  updateHoleUsageArgs useInHole var zs [] = pure False
  updateHoleUsageArgs useInHole var zs (a :: as)
      = do h <- updateHoleUsage useInHole var zs a
           h' <- updateHoleUsageArgs useInHole var zs as
           pure (h || h')

  -- The assumption here is that hole types are abstracted over the entire
  -- environment, so that they have the appropriate number of function
  -- arguments and there are no lets
  updateHoleType : {vars : _} ->
                   {auto c : Ref Ctxt Defs} ->
                   {auto u : Ref UST UState} ->
                   (useInHole : Bool) ->
                   Var vars -> List (Var vars) ->
                   Term vs -> List (Term vars) ->
                   Core (Term vs)
  updateHoleType useInHole var zs (Bind bfc nm (Pi fc' c e ty) sc) (Local _ r v _ :: as)
      -- if the argument to the hole type is the variable of interest,
      -- and the variable should be used in the hole, set it to Rig1,
      -- otherwise set it to Rig0
      = if varIdx var == v
           then do scty <- updateHoleType False var zs sc as
                   let c' = if useInHole then c else erased
                   pure (Bind bfc nm (Pi fc' c' e ty) scty)
           else if elem v (map varIdx zs)
                then do scty <- updateHoleType useInHole var zs sc as
                        pure (Bind bfc nm (Pi fc' erased e ty) scty)
                else do scty <- updateHoleType useInHole var zs sc as
                        pure (Bind bfc nm (Pi fc' c e ty) scty)
  updateHoleType useInHole var zs (Bind bfc nm (Pi fc' c e ty) sc) (a :: as)
      = do ignore $ updateHoleUsage False var zs a
           scty <- updateHoleType useInHole var zs sc as
           pure (Bind bfc nm (Pi fc' c e ty) scty)
  updateHoleType useInHole var zs ty as
      = do ignore $ updateHoleUsageArgs False var zs as
           pure ty

  updateHoleUsagePats : {auto c : Ref Ctxt Defs} ->
                        {auto u : Ref UST UState} ->
                        (useInHole : Bool) ->
                        Var vars -> List (Term vars) ->
                        (vs ** (Env Term vs, Term vs, Term vs)) ->
                        Core Bool
  updateHoleUsagePats {vars} useInHole var args (vs ** (env, lhs, rhs))
      = do -- Find the argument which corresponds to var
           let argpos = findArg Z args
           log "quantity.hole" 10 $ "At positions " ++ show argpos
           -- Find what it's position is in env by looking at the lhs args
           let vars = mapMaybe (findLocal (getArgs lhs)) argpos
           hs <- traverse (\vsel => updateHoleUsage useInHole vsel [] rhs)
                          vars
           pure (any id hs)
    where
      findArg : Nat -> List (Term vars) -> List Nat
      findArg i [] = []
      findArg i (Local _ _ idx vel :: els)
          = if idx == varIdx var
               then i :: findArg (1 + i) els
               else findArg (1 + i) els
      findArg i (_ :: els) = findArg (1 + i) els

      findLocal : List (Term vs) -> Nat -> Maybe (Var vs)
      findLocal (Local _ _ _ p :: _) Z = Just (MkVar p)
      findLocal (As _ _ (Local _ _ _ p) _ :: _) Z = Just (MkVar p)
      findLocal (As _ _ _ (Local _ _ _ p) :: _) Z = Just (MkVar p)
      findLocal (_ :: els) (S k) = findLocal els k
      findLocal _ _ = Nothing

  updateHoleUsage : {vars : _} ->
                    {auto c : Ref Ctxt Defs} ->
                    {auto u : Ref UST UState} ->
                    (useInHole : Bool) ->
                    Var vars -> List (Var vars) ->
                    Term vars -> Core Bool
  updateHoleUsage useInHole (MkVar var) zs (Bind _ _ (Let _ _ val _) sc)
      = do h <- updateHoleUsage useInHole (MkVar var) zs val
           h' <- updateHoleUsage useInHole (MkVar (Later var)) (map weaken zs) sc
           pure (h || h')
  updateHoleUsage useInHole (MkVar var) zs (Bind _ n b sc)
      = updateHoleUsage useInHole (MkVar (Later var)) (map weaken zs) sc
  updateHoleUsage useInHole var zs (Meta fc n i args)
      = do defs <- get Ctxt
           Just gdef <- lookupCtxtExact (Resolved i) (gamma defs)
                | Nothing => updateHoleUsageArgs useInHole var zs args
           -- only update for holes with no definition yet
           case definition gdef of
                Hole _ _ =>
                   do let ty = type gdef
                      ty' <- updateHoleType useInHole var zs ty args
                      updateTy i ty'
                      logTerm "quantity.hole.update" 5 ("New type of " ++
                                 show (fullname gdef)) ty'
                      logTerm "quantity.hole.update" 5 ("Updated from " ++
                                 show (fullname gdef)) (type gdef)
                      pure True
                _ => updateHoleUsageArgs useInHole var zs args
  updateHoleUsage useInHole var zs (As _ _ a p)
      = do h <- updateHoleUsage useInHole var zs a
           h' <- updateHoleUsage useInHole var zs a
           pure (h || h')
  updateHoleUsage useInHole var zs (TDelayed _ _ t)
      = updateHoleUsage useInHole var zs t
  updateHoleUsage useInHole var zs (TDelay _ _ _ t)
      = updateHoleUsage useInHole var zs t
  updateHoleUsage useInHole var zs (TForce _ _ t)
      = updateHoleUsage useInHole var zs t
  updateHoleUsage useInHole var zs tm
      = case getFnArgs tm of
             (Ref _ _ fn, args) =>
                  -- no need to look inside 'fn' for holes since we did that
                  -- when working through lcheckDef recursively
                  updateHoleUsageArgs useInHole var zs args
             (f, []) => pure False
             (f, args) => updateHoleUsageArgs useInHole var zs (f :: args)

-- Linearity checking of an already checked term. This serves two purposes:
--  + Checking correct usage of linear bindings
--  + updating hole types to reflect usage counts correctly
-- Returns term, normalised type, and a list of used variables
mutual
  lcheck : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState } ->
           RigCount -> (erase : Bool) -> Env Term vars -> Term vars ->
           Core (Term vars, Glued vars, Usage vars)
  lcheck {vars} rig erase env (Local {name} fc x idx prf)
      = let b = getBinder prf env
            rigb = multiplicity b
            ty = binderType b in
            do when (not erase) $ rigSafe rigb rig
               pure (Local fc x idx prf, gnf env ty, used rig)
    where
      getName : {idx : _} -> (vs : List Name) -> (0 p : IsVar n idx vs) -> Name
      getName (x :: _) First = x
      getName (x :: xs) (Later p) = getName xs p

      rigSafe : RigCount -> RigCount -> Core ()
      rigSafe l r = when (l < r)
                         (throw (LinearMisuse fc (getName vars prf) l r))

      -- count the usage if we're in a linear context. If not, the usage doesn't
      -- matter
      used : RigCount -> Usage vars
      used r = if isLinear r then [MkVar prf] else []

  lcheck rig erase env (Ref fc nt fn)
      = do ty <- lcheckDef fc rig erase env fn
           pure (Ref fc nt fn, gnf env (embed ty), [])

  -- If the meta has a definition, and we're not in Rig0, expand it first
  -- and check the result.
  -- Otherwise, don't count variable usage in holes, so as far as linearity
  -- checking is concerned, update the type so that the binders
  -- are in Rig0
  lcheck {vars} rig erase env (Meta fc n idx args)
      = do defs <- get Ctxt
           Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)
                | _ => undefinedName fc n
           let expand = branchZero
                          (case type gdef of
                                Erased _ _ => True -- defined elsewhere, need to expand
                                _ => False)
                          (case definition gdef of
                                (PMDef _ _ _ _ _) => True
                                _ => False)
                          rig
           logC "quantity" 10 $ do
             def <- case definition gdef of
                         PMDef _ _ (STerm _ tm) _ _ =>
                              do tm' <- toFullNames tm
                                 pure (show tm')
                         _ => pure ""
             pure (show rig ++ ": " ++ show n ++ " " ++ show fc ++ "\n"
                     ++ show def)
           if expand
              then expandMeta rig erase env n idx (definition gdef) args
              else do let ty : ClosedTerm
                             = case definition gdef of
                                    Hole _ _ => unusedHoleArgs args (type gdef)
                                    _ => type gdef
                      nty <- nf defs env (embed ty)
                      lcheckMeta rig erase env fc n idx args [] nty
    where
      unusedHoleArgs : List a -> Term vs -> Term vs
      unusedHoleArgs (_ :: args) (Bind bfc n (Pi fc _ e ty) sc)
          = Bind bfc n (Pi fc erased e ty) (unusedHoleArgs args sc)
      unusedHoleArgs args (Bind bfc n (Let fc c e ty) sc)
          = Bind bfc n (Let fc c e ty) (unusedHoleArgs args sc)
      unusedHoleArgs _ ty = ty

  lcheck rig_in erase env (Bind fc nm b sc)
      = do (b', bt, usedb) <- handleUnify (lcheckBinder rig erase env b)
                                 (\err =>
                                     case err of
                                          LinearMisuse _ _ r _ =>
                                             lcheckBinder rig erase env
                                                (setMultiplicity b linear)
                                          _ => throw err)
           -- Anything linear can't be used in the scope of a lambda, if we're
           -- checking in general context
           let env' = if rig_in == top
                         then case b of
                              (Lam _ _ _ _) => eraseLinear env
                              _ => env
                         else env
           (sc', sct, usedsc) <- lcheck rig erase (b' :: env') sc
           defs <- get Ctxt

           let used_in = count 0 usedsc
           holeFound <- if not erase && isLinear (multiplicity b)
                           then updateHoleUsage (used_in == 0)
                                         (MkVar First)
                                         (map weaken (getZeroes env'))
                                         sc'
                           else pure False

           -- if there's a hole, assume it will contain the missing usage
           -- if there is none already
           let used = if isLinear ((multiplicity b) |*| rig) &&
                         holeFound && used_in == 0
                         then 1
                         else used_in

           when (not erase) $
               checkUsageOK used ((multiplicity b) |*| rig)
           defs <- get Ctxt
           discharge defs env fc nm b' bt sc' sct (usedb ++ doneScope usedsc)
    where
      rig : RigCount
      rig = case b of
                 Pi _ _ _ _ =>
                      if isErased rig_in
                         then erased
                         else top -- checking as if an inspectable run-time type
                 Let _ _ _ _ => rig_in
                 _ => if isErased rig_in
                         then erased
                         else linear

      getZeroes : {vs : _} -> Env Term vs -> List (Var vs)
      getZeroes [] = []
      getZeroes (b :: bs)
          = if isErased (multiplicity b)
               then MkVar First :: map weaken (getZeroes bs)
               else map weaken (getZeroes bs)

      eraseLinear : Env Term vs -> Env Term vs
      eraseLinear [] = []
      eraseLinear (b :: bs)
          = if isLinear (multiplicity b)
               then setMultiplicity b erased :: eraseLinear bs
               else b :: eraseLinear bs

      checkUsageOK : Nat -> RigCount -> Core ()
      checkUsageOK used r = when (isLinear r && used /= 1)
                                 (throw (LinearUsed fc used nm))

  lcheck rig erase env (App fc f a)
      = do (f', gfty, fused) <- lcheck rig erase env f
           defs <- get Ctxt
           fty <- getNF gfty
           case fty of
                NBind _ _ (Pi _ rigf _ ty) scdone =>
                     -- if the argument is borrowed, it's okay to use it in
                     -- unrestricted context, because we'll be out of the
                     -- application without spending it
                   do let checkRig = rigf |*| rig
                      (a', gaty, aused) <- lcheck checkRig erase env a
                      sc' <- scdone defs (toClosure defaultOpts env a')
                      let aerased = if erase && isErased rigf then Erased fc False else a'
                      -- Possibly remove this check, or make it a compiler
                      -- flag? It is a useful double check on the result of
                      -- elaboration, but there are pathological cases where
                      -- it makes the check very slow (id id id id ... id id etc
                      -- for example) and there may be similar realistic cases.
                      -- If elaboration is correct, this should never fail!
                      opts <- getSession
                      when (debugElabCheck opts) $ do
                        aty <- getNF gaty
                        when (not !(convert defs env aty !(evalClosure defs ty))) $
                           do ty' <- quote defs env ty
                              aty' <- quote defs env aty
                              throw (CantConvert fc (gamma defs) env ty' aty')
                      pure (App fc f' aerased,
                            glueBack defs env sc',
                            fused ++ aused)
                NApp _ (NRef _ n) _ =>
                      do Just _ <- lookupCtxtExact n (gamma defs)
                              | _ => undefinedName fc n
                         tfty <- getTerm gfty
                         throw (GenericMsg fc ("Linearity checking failed on " ++ show !(toFullNames f') ++
                              " (" ++ show !(toFullNames tfty) ++ " not a function type)"))

                _ => do tfty <- getTerm gfty
                        throw (GenericMsg fc ("Linearity checking failed on " ++ show !(toFullNames f') ++
                              " (" ++ show !(toFullNames tfty) ++ " not a function type)"))

  lcheck rig erase env (As fc s as pat)
      = do (as', _, _) <- lcheck rig erase env as
           (pat', pty, u) <- lcheck rig erase env pat
           pure (As fc s as' pat', pty, u)
  lcheck rig erase env (TDelayed fc r ty)
      = do (ty', _, u) <- lcheck rig erase env ty
           pure (TDelayed fc r ty', gType fc, u)
  lcheck rig erase env (TDelay fc r ty val)
      = do (ty', _, _) <- lcheck erased erase env ty
           (val', gty, u) <- lcheck rig erase env val
           ty <- getTerm gty
           pure (TDelay fc r ty' val', gnf env (TDelayed fc r ty), u)
  lcheck rig erase env (TForce fc r val)
      = do (val', gty, u) <- lcheck rig erase env val
           tynf <- getNF gty
           case tynf of
                NDelayed _ r narg
                    => do defs <- get Ctxt
                          pure (TForce fc r val', glueBack defs env narg, u)
                _ => throw (GenericMsg fc "Not a delayed type")
  lcheck rig erase env (PrimVal fc c)
      = pure (PrimVal fc c, gErased fc, [])
  lcheck rig erase env (Erased fc i)
      = pure (Erased fc i, gErased fc, [])
  lcheck rig erase env (TType fc)
      = pure (TType fc, gType fc, [])

  lcheckBinder : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 RigCount -> (erase : Bool) -> Env Term vars ->
                 Binder (Term vars) ->
                 Core (Binder (Term vars), Glued vars, Usage vars)
  lcheckBinder rig erase env (Lam fc c x ty)
      = do (tyv, tyt, _) <- lcheck erased erase env ty
           pure (Lam fc c x tyv, tyt, [])
  lcheckBinder rig erase env (Let fc rigc val ty)
      = do (tyv, tyt, _) <- lcheck erased erase env ty
           (valv, valt, vs) <- lcheck (rig |*| rigc) erase env val
           pure (Let fc rigc valv tyv, tyt, vs)
  lcheckBinder rig erase env (Pi fc c x ty)
      = do (tyv, tyt, _) <- lcheck (rig |*| c) erase env ty
           pure (Pi fc c x tyv, tyt, [])
  lcheckBinder rig erase env (PVar fc c p ty)
      = do (tyv, tyt, _) <- lcheck erased erase env ty
           pure (PVar fc c p tyv, tyt, [])
  lcheckBinder rig erase env (PLet fc rigc val ty)
      = do (tyv, tyt, _) <- lcheck erased erase env ty
           (valv, valt, vs) <- lcheck (rig |*| rigc) erase env val
           pure (PLet fc rigc valv tyv, tyt, vs)
  lcheckBinder rig erase env (PVTy fc c ty)
      = do (tyv, tyt, _) <- lcheck erased erase env ty
           pure (PVTy fc c tyv, tyt, [])

  discharge : {vars : _} ->
              Defs -> Env Term vars ->
              FC -> (nm : Name) -> Binder (Term vars) -> Glued vars ->
              Term (nm :: vars) -> Glued (nm :: vars) -> Usage vars ->
              Core (Term vars, Glued vars, Usage vars)
  discharge defs env fc nm (Lam fc' c x ty) gbindty scope gscopety used
       = do scty <- getTerm gscopety
            pure (Bind fc nm (Lam fc' c x ty) scope,
                  gnf env (Bind fc nm (Pi fc' c x ty) scty), used)
  discharge defs env fc nm (Let fc' c val ty) gbindty scope gscopety used
       = do scty <- getTerm gscopety
            pure (Bind fc nm (Let fc' c val ty) scope,
                  gnf env (Bind fc nm (Let fc' c val ty) scty), used)
  discharge defs env fc nm (Pi fc' c x ty) gbindty scope gscopety used
       = pure (Bind fc nm (Pi fc' c x ty) scope, gbindty, used)
  discharge defs env fc nm (PVar fc' c p ty) gbindty scope gscopety used
       = do scty <- getTerm gscopety
            pure (Bind fc nm (PVar fc' c p ty) scope,
                  gnf env (Bind fc nm (PVTy fc' c ty) scty), used)
  discharge defs env fc nm (PLet fc' c val ty) gbindty scope gscopety used
       = do scty <- getTerm gscopety
            pure (Bind fc nm (PLet fc' c val ty) scope,
                  gnf env (Bind fc nm (PLet fc' c val ty) scty), used)
  discharge defs env fc nm (PVTy fc' c ty) gbindty scope gscopety used
       = pure (Bind fc nm (PVTy fc' c ty) scope, gbindty, used)

  data ArgUsage
       = UseAny -- RigW so we don't care
       | Use0 -- argument position not used
       | Use1 -- argument position used exactly once
       | UseKeep -- keep as is
       | UseUnknown -- hole, so can't tell

  Show ArgUsage where
    show UseAny = "any"
    show Use0 = "0"
    show Use1 = "1"
    show UseKeep = "keep"
    show UseUnknown = "unknown"

  -- Check argument usage in case blocks. Returns a list of how each argument
  -- in the case block is used, to build the appropriate type for the outer
  -- block.
  getArgUsage : {auto c : Ref Ctxt Defs} ->
                {auto e : Ref UST UState} ->
                FC -> RigCount -> ClosedTerm ->
                List (vs ** (Env Term vs, Term vs, Term vs)) ->
                Core (List ArgUsage)
  getArgUsage topfc rig ty pats
      = do us <- traverse (getPUsage ty) pats
           pure (map snd !(combine us))
    where
      getCaseUsage : {vs : _} ->
                     Term ns -> Env Term vs -> List (Term vs) ->
                     Usage vs -> Term vs ->
                     Core (List (Name, ArgUsage))
      getCaseUsage ty env (As _ _ _ p :: args) used rhs
          = getCaseUsage ty env (p :: args) used rhs
      getCaseUsage (Bind _ n (Pi _ rig _ ty) sc) env (arg :: args) used rhs
          = if isLinear rig
               then case arg of
                         (Local _ _ idx p) =>
                           do rest <- getCaseUsage sc env args used rhs
                              let used_in = count idx used
                              holeFound <- updateHoleUsage (used_in == 0) (MkVar p) [] rhs
                              let ause
                                  = if holeFound && used_in == 0
                                            then UseUnknown
                                            else if used_in == 0
                                                    then Use0
                                                    else Use1
                              pure ((n, ause) :: rest)
                         _ => do elseCase
               else elseCase
          where
            elseCase : Core (List (Name, ArgUsage))
            elseCase = do rest <- getCaseUsage sc env args used rhs
                          pure $ if isErased rig
                             then ((n, Use0) :: rest)
                             else ((n, UseKeep) :: rest)
      getCaseUsage tm env args used rhs = pure []

      checkUsageOK : FC -> Nat -> Name -> Bool -> RigCount -> Core ()
      checkUsageOK fc used nm isloc rig
          = when (isLinear rig && ((isloc && used > 1) || (not isloc && used /= 1)))
                 (throw (LinearUsed fc used nm))

      -- Is the variable one of the lhs arguments; i.e. do we treat it as
      -- affine rather than linear
      isLocArg : Var vars -> List (Term vars) -> Bool
      isLocArg p [] = False
      isLocArg p (Local _ _ idx _ :: args)
          = idx == varIdx p || isLocArg p args
      isLocArg p (As _ _ tm pat :: args)
          = isLocArg p (tm :: pat :: args)
      isLocArg p (_ :: args) = isLocArg p args

      -- As checkEnvUsage in general, but it's okay for local variables to
      -- remain unused (since in that case, they must be used outside the
      -- case block)
      checkEnvUsage : {done, vars : _} ->
                      RigCount ->
                      Env Term vars -> Usage (done ++ vars) ->
                      List (Term (done ++ vars)) ->
                      Term (done ++ vars) -> Core ()
      checkEnvUsage rig [] usage args tm = pure ()
      checkEnvUsage rig {done} {vars = nm :: xs} (b :: env) usage args tm
          = do let pos = localPrf {later = done}
               let used_in = count (varIdx pos) usage

               holeFound <- if isLinear (multiplicity b)
                               then updateHoleUsage (used_in == 0) pos [] tm
                               else pure False
               let used = if isLinear ((multiplicity b) |*| rig) &&
                             holeFound && used_in == 0
                             then 1
                             else used_in
               checkUsageOK (getLoc (binderType b))
                            used nm (isLocArg pos args)
                                    ((multiplicity b) |*| rig)
               checkEnvUsage {done = done ++ [nm]} rig env
                     (rewrite sym (appendAssociative done [nm] xs) in usage)
                     (rewrite sym (appendAssociative done [nm] xs) in args)
                     (rewrite sym (appendAssociative done [nm] xs) in tm)

      getPUsage : ClosedTerm -> (vs ** (Env Term vs, Term vs, Term vs)) ->
                  Core (List (Name, ArgUsage))
      getPUsage ty (_ ** (penv, lhs, rhs))
          = do logEnv "quantity" 10 "Env" penv
               logTerm "quantity" 10 "LHS" lhs
               logTerm "quantity" 5 "Linear check in case RHS" rhs
               (rhs', _, used) <- lcheck rig False penv rhs
               log "quantity" 10 $ "Used: " ++ show used
               let args = getArgs lhs
               checkEnvUsage {done = []} rig penv used args rhs'
               ause <- getCaseUsage ty penv args used rhs
               log "quantity" 10 $ "Arg usage: " ++ show ause
               pure ause

      combineUsage : (Name, ArgUsage) -> (Name, ArgUsage) ->
                     Core (Name, ArgUsage)
      combineUsage (n, Use0) (_, Use1)
          = throw (GenericMsg topfc ("Inconsistent usage of " ++ show n ++ " in case branches"))
      combineUsage (n, Use1) (_, Use0)
          = throw (GenericMsg topfc ("Inconsistent usage of " ++ show n ++ " in case branches"))
      combineUsage (n, UseAny) _ = pure (n, UseAny)
      combineUsage _ (n, UseAny) = pure (n, UseAny)
      combineUsage (n, UseKeep) _ = pure (n, UseKeep)
      combineUsage _ (n, UseKeep) = pure (n, UseKeep)
      combineUsage (n, UseUnknown) _ = pure (n, UseUnknown)
      combineUsage _ (n, UseUnknown) = pure (n, UseUnknown)
      combineUsage x y = pure x

      combineUsages : List (Name, ArgUsage) -> List (Name, ArgUsage) ->
                      Core (List (Name, ArgUsage))
      combineUsages [] [] = pure []
      combineUsages (u :: us) (v :: vs)
          = do u' <- combineUsage u v
               us' <- combineUsages us vs
               pure (u' :: us')
      combineUsages _ _ = throw (InternalError "Argument usage lists inconsistent")

      combine : List (List (Name, ArgUsage)) ->
                Core (List (Name, ArgUsage))
      combine [] = pure []
      combine [x] = pure x
      combine (x :: xs)
          = do xs' <- combine xs
               combineUsages x xs'

  lcheckDef : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount -> (erase : Bool) -> Env Term vars -> Name ->
              Core ClosedTerm
  lcheckDef fc rig True env n
      = do defs <- get Ctxt
           Just def <- lookupCtxtExact n (gamma defs)
                | Nothing => undefinedName fc n
           pure (type def)
  lcheckDef fc rig False env n
      = do defs <- get Ctxt
           let Just idx = getNameID n (gamma defs)
                | Nothing => undefinedName fc n
           Just def <- lookupCtxtExact (Resolved idx) (gamma defs)
                | Nothing => undefinedName fc n
           rigSafe (multiplicity def) rig
           if linearChecked def
              then pure (type def)
              else case definition def of
                        PMDef _ _ _ _ pats =>
                            do u <- getArgUsage (getLoc (type def))
                                                rig (type def) pats
                               log "quantity" 5 $ "Overall arg usage " ++ show u
                               let ty' = updateUsage u (type def)
                               updateTy idx ty'
                               setLinearCheck idx True
                               logTerm "quantity" 5 ("New type of " ++
                                          show (fullname def)) ty'
                               logTerm "quantity" 5 ("Updated from " ++
                                          show (fullname def)) (type def)
                               pure ty'
                        _ => pure (type def)
    where
      updateUsage : List ArgUsage -> Term ns -> Term ns
      updateUsage (u :: us) (Bind bfc n (Pi fc c e ty) sc)
          = let sc' = updateUsage us sc
                c' = case u of
                          Use0 => erased
                          Use1 => linear -- ignore usage elsewhere, we checked here
                          UseUnknown => c -- don't know, assumed unchanged and update hole types
                          UseKeep => c -- matched here, so count usage elsewhere
                          UseAny => c in -- no constraint, so leave alone
                Bind bfc n (Pi fc c' e ty) sc'
      updateUsage _ ty = ty

      rigSafe : RigCount -> RigCount -> Core ()
      rigSafe a b = when (a < b)
                         (throw (LinearMisuse fc !(getFullName n) a b))

  expandMeta : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               RigCount -> (erase : Bool) -> Env Term vars ->
               Name -> Int -> Def -> List (Term vars) ->
               Core (Term vars, Glued vars, Usage vars)
  expandMeta rig erase env n idx (PMDef _ [] (STerm _ fn) _ _) args
      = do tm <- substMeta (embed fn) args []
           lcheck rig erase env tm
    where
      substMeta : {drop, vs : _} ->
                  Term (drop ++ vs) -> List (Term vs) -> SubstEnv drop vs ->
                  Core (Term vs)
      substMeta (Bind bfc n (Lam _ c e ty) sc) (a :: as) env
          = substMeta sc as (a :: env)
      substMeta (Bind bfc n (Let _ c val ty) sc) as env
          = substMeta (subst val sc) as env
      substMeta rhs [] env = pure (substs env rhs)
      substMeta rhs _ _ = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show fn))
  expandMeta rig erase env n idx def _
      = throw (InternalError ("Badly formed metavar solution " ++ show n ++ " " ++ show def))

  lcheckMeta : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               RigCount -> Bool -> Env Term vars ->
               FC -> Name -> Int ->
               (args : List (Term vars)) ->
               (checked : List (Term vars)) ->
               NF vars -> Core (Term vars, Glued vars, Usage vars)
  lcheckMeta rig erase env fc n idx
             (arg :: args) chk (NBind _ _ (Pi _ rigf _ ty) sc)
      = do let checkRig = rigf |*| rig
           (arg', gargTy, aused) <- lcheck checkRig erase env arg
           defs <- get Ctxt
           sc' <- sc defs (toClosure defaultOpts env arg')
           let aerased = if erase && isErased rigf then Erased fc False else arg'
           (tm, gty, u) <- lcheckMeta rig erase env fc n idx args
                                      (aerased :: chk) sc'
           pure (tm, gty, aused ++ u)
  lcheckMeta rig erase env fc n idx (arg :: args) chk nty
      = do defs <- get Ctxt
           empty <- clearDefs defs
           ty <- quote empty env nty
           throw (GenericMsg fc ("Linearity checking failed on metavar "
                      ++ show !(toFullNames n) ++ " (" ++ show !(toFullNames ty)
                      ++ " not a function type)"))
  lcheckMeta rig erase env fc n idx [] chk nty
      = do defs <- get Ctxt
           pure (Meta fc n idx (reverse chk), glueBack defs env nty, [])

checkEnvUsage : {vars, done : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                FC -> RigCount ->
                Env Term vars -> Usage (done ++ vars) ->
                Term (done ++ vars) ->
                Core ()
checkEnvUsage fc rig [] usage tm = pure ()
checkEnvUsage fc rig {done} {vars = nm :: xs} (b :: env) usage tm
    = do let pos = localPrf {later = done}
         let used_in = count (varIdx pos) usage

         holeFound <- if isLinear (multiplicity b)
                         then updateHoleUsage (used_in == 0) pos [] tm
                         else pure False
         let used = if isLinear ((multiplicity b) |*| rig) &&
                       holeFound && used_in == 0
                       then 1
                       else used_in
         checkUsageOK used ((multiplicity b) |*| rig)
         checkEnvUsage {done = done ++ [nm]} fc rig env
               (rewrite sym (appendAssociative done [nm] xs) in usage)
               (rewrite sym (appendAssociative done [nm] xs) in tm)
  where
    checkUsageOK : Nat -> RigCount -> Core ()
    checkUsageOK used r = when (isLinear r && used /= 1)
                               (throw (LinearUsed fc used nm))

-- Linearity check an elaborated term. If 'erase' is set, erase anything that's in
-- a Rig0 argument position (we can't do this until typechecking is complete, though,
-- since it might be used for unification/reasoning elsewhere, so we only do this for
-- definitions ready for compilation).
export
linearCheck : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount -> (erase : Bool) ->
              Env Term vars -> Term vars ->
              Core (Term vars)
linearCheck fc rig erase env tm
    = do logTerm "quantity" 5 "Linearity check on " tm
         logEnv "quantity" 5 "In env" env
         (tm', _, used) <- lcheck rig erase env tm
         log "quantity" 5 $ "Used: " ++ show used
         when (not erase) $ checkEnvUsage {done = []} fc rig env used tm'
         pure tm'


text:
module Test.Main

import Test.Array
import Test.JSON
import Test.Object
import Test.Util

main : IO ()
main = do Test.Array.test
          Test.Util.test
          Test.Object.test
          Test.JSON.test


text:
-- data MyNat = Z | S MyNat

-- Z
-- S Z
-- S (S Z)
-- S (S (S Z))

-- myPlus : MyNat -> MyNat -> MyNat
-- myPlus Z j = j
-- myPlus (S x) j = S (myPlus x j)

max_stars_repo_name: fthomas/tdd-talk

max_issues_repo_name: fthomas/tdd-talk

max_forks_repo_name: fthomas/tdd-talk


text:
%default total

||| View for traversing a list backwards
public export
data SnocList : List a -> Type where
     Empty : SnocList []
     Snoc : (x : a) -> (xs : List a) ->
            (rec : SnocList xs) -> SnocList (xs ++ [x])

empty : SnocList (x :: xs) -> a
empty Empty impossible

snoc : SnocList (x :: xs) -> a
snoc (Snoc _ _ _) impossible


text:
module Test

import Data.Vect
import Data.Fin

import Lightyear
import Lightyear.Char
import Lightyear.Strings
import Lightyear.Testing

%access export

listOf : Parser a -> Parser (List a)
listOf p = string "[" *!> (p `sepBy` string ",") <* string "]"

listOf' : Parser a -> Parser (List a)
listOf' p = brackets (commaSep p)

nat : Parser Nat
nat = integer

tests : IO ()
tests = runTests
  [ parseTestCmp "Test 1" nat          (==) "123"        123
  , parseTestCmp "Test 2" (listOf nat) (==) "[1,2,3,99]" [1,2,3,99]

  , parseTestCmpNot "Test 3" (listOf nat) "foo" "At 1:1:\n\tstring \"[\"\nAt 1:1:\n\tcharacter '['\nAt 1:1:\n\ta different token"

  -- should commit and fail
  , parseTestCmpNot "Test 4" (listOf nat <|> (string "[foo" *> pure List.Nil)) "[foo" "At 1:2:\n\tstring \"]\"\nAt 1:2:\n\tcharacter ']'\nAt 1:2:\n\ta different token"

  , parseTestCmp "Test 5" (listOf $ listOf nat)   (==) "[[1,2],[],[3,4,5]]" [[1, 2], [], [3, 4, 5]]
  , parseTestCmp "Test 6" (listOf' nat)           (==) "[1,2,3,99]"         [1, 2, 3, 99]
  , parseTestCmp "Test 6" (listOf' $ listOf' nat) (==) "[[1,2],[],[3,4,5]]" [[1, 2], [], [3, 4, 5]]

  -- should commit and fail
  , parseTestCmp "Test 7" (listOf' nat <|> (string "[foo" *> pure List.Nil)) (==) "[foo" []

  -- should NOT commit
  , parseTestCmp "Test 8" ((getPosition *> string "x") <|> string "y") (==) "y" "y"

  -- should not eat up the one "b"
  , parseTestCmp "Test 9" (ntimes 4 (requireFailure (string "bb") *> anyChar)) (==) "abcde" ['a','b','c','d']
  ]


text:
module Sub13Apply108x36

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(36x+12) --F[5,-2]->B[1,-2]--> 3(16x+5)
fb108x36To48x15 :
  (o:Nat) -> P (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                     (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                               (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))) 2
    -> P (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))) 2
fb108x36To48x15 o prf =
  let prf2 = lvDown (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                     (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                               (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))) 2
                    prf in
    let prf3 = fb108x36To48x15' o prf2 in lvDown (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))) 3 prf3

export
apply108x36 : P (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                     (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                               (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))) 2
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                        (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                  (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))),
         P m 2))
apply108x36 {o} col = let col2 = fb108x36To48x15 o col in ((S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))
                                                           ** (lte108x36 o, col2)) where
  lte108x36 : (o:Nat) -> LTE (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                  (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))
          (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                     (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                               (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))
  lte108x36 Z = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte108x36 (S o) = let lemma = lte108x36 o in

    rewrite (sym (plusSuccRightSucc o o)) in

    rewrite (sym (plusSuccRightSucc (plus o o)  (S (plus o o)))) in
    rewrite (sym (plusSuccRightSucc (plus o o)  (plus o o))) in

    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (S (plus (plus o o) (plus o o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (plus (plus o o) (plus o o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (plus (plus o o) (plus o o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (plus (plus o o) (plus o o)))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))) in

    rewrite (sym (plusSuccRightSucc (plus o o)  o)) in

    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (S (plus (plus o o) o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (plus (plus o o) o)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (plus (plus o o) o))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (S (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (plus (plus (plus o o) o) (plus (plus o o) o))))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))) in

      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
module Utils.ComplexAddon

import Data.Complex

%default total
%access public export

implementation (Fractional a, Neg a) => Fractional (Complex a) where
    (/) (a:+b) (c:+d) = let
                          real = (a*c+b*d)/(c*c+d*d)
                          imag = (b*c-a*d)/(c*c+d*d)
                        in
                          (real:+imag)

implementation (Cast a b) => Cast (Complex a) (Complex b) where
  cast (x :+ y) = (cast x :+ cast y)

max_stars_repo_name: GrandArchTemplar/QuantumProgramming

max_issues_repo_name: GrandArchTemplar/QuantumProgramming

max_forks_repo_name: GrandArchTemplar/QuantumProgramming


text:
module Main

import Effect.State

data Tree a = Leaf
            | Node (Tree a) a (Tree a)

flattenTree : Tree a -> List a
flattenTree Leaf = []
flattenTree (Node l x r) = flattenTree l ++ (x :: flattenTree r)

testTree : Tree String
testTree = Node (Node Leaf "One" (Node Leaf "Two" Leaf))
                "Three"
                (Node (Node Leaf "Four" Leaf) "Five" Leaf)

data Tag : Type where
data Leaves : Type where

label : Tree a -> { [Leaves ::: STATE Int, Tag ::: STATE Int] }
                  Eff m (Tree (Int, a))
label Leaf = do Leaves :- update (+1)
                return Leaf
label (Node l x r) = do l' <- label l
                        lbl <- Tag :- get
                        Tag :- put (lbl + 1)
                        r' <- label r
                        return (Node l' (lbl, x) r')

main : IO ()
main = do -- let ([Leaves := l, _], x)
          let x = runPureInit [default, Tag := 1] (label testTree)
          print (flattenTree x)

{-
label Leaf = return Leaf
label (Node l x r) = do l' <- label l
                        lbl <- get
                        put (lbl + 1)
                        r' <- label r
                        return (Node l' (lbl, x) r')
-}

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
data Access = LoggedOut | LoggedIn
data PwdCheck = Correct | Incorrect

data ShellCmd : (ty : Type) -> Access -> (ty -> Access) -> Type where
     Password : String -> ShellCmd PwdCheck LoggedOut
                                   (\res => case res of
                                                 Correct => LoggedIn
                                                 Incorrect => LoggedOut)
     Logout : ShellCmd () LoggedIn (const LoggedOut)
     GetSecret : ShellCmd String LoggedIn (const LoggedIn)

     PutStr : String -> ShellCmd () state (const state)

     Pure : (res : ty) -> ShellCmd ty (state_fn res) state_fn
     (>>=) : ShellCmd a state1 state2_fn ->
             ((res : a) -> ShellCmd b (state2_fn res) state3_fn) ->
             ShellCmd b state1 state3_fn

session : ShellCmd () LoggedOut (const LoggedOut)
session = do Correct <- Password "wurzel"
                | Incorrect => PutStr "Wrong password"
             msg <- GetSecret
             PutStr ("Secret code: " ++ show msg ++ "\n")
             Logout

{-
badSession : ShellCmd () LoggedOut (const LoggedOut)
badSession = do Password "wurzel"
                msg <- GetSecret
                PutStr ("Secret code: " ++ show msg ++ "\n")
                Logout

noLogout : ShellCmd () LoggedOut (const LoggedOut)
noLogout = do Correct <- Password "wurzel"
                 | Incorrect => PutStr "Wrong password"
              msg <- GetSecret
              PutStr ("Secret code: " ++ show msg ++ "\n")
-}

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
> import Data.So

> %default total

> data LTE : Double -> Double -> Type where
>   MkLTE : {x : Double} -> {y : Double} -> So (x <= y) -> LTE x y

> NonNegDouble : Type
> NonNegDouble = Subset Double (\ x => 0.0 `LTE` x)

> zero     : NonNegDouble
> one      : NonNegDouble
> toDouble : NonNegDouble -> Double
> toDouble = getWitness
> plus     : NonNegDouble -> NonNegDouble -> NonNegDouble
> mult     : NonNegDouble -> NonNegDouble -> NonNegDouble
> div      : NonNegDouble -> NonNegDouble -> NonNegDouble
> fromNat  : (n : Nat) -> NonNegDouble

> implementation [NumNonNegDouble] Num NonNegDouble where
>   (+) = plus
>   (*) = mult
>   fromInteger = fromNat . fromIntegerNat

> using implementation NumNonNegDouble
>   implementation [FractionalNonNegDouble] Fractional NonNegDouble where
>     (/) = div

> implementation [EqNonNegDouble] Eq NonNegDouble where
>   (==) x y = (toDouble x) == (toDouble y)

> using implementation EqNonNegDouble
>   implementation [OrdNonNegDouble] Ord NonNegDouble where
>     compare x y = compare (toDouble x) (toDouble y)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Replica.Other.String

import Data.List
import Data.String

%default total

export
separator : Nat -> String
separator = pack . flip replicate '-'

export
withOffset : Nat -> String -> String
withOffset k = (++) (pack $ replicate k ' ')

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module Data.Functor.Coproduct

import Data.Bifunctor
import Control.Comonad

%access public export

-- | `Coproduct f g` is the coproduct of two functors `f` and `g`
data Coproduct : (f : Type -> Type) -> (g : Type -> Type) -> (a : Type) -> Type where
  MkCoproduct : Either (f a) (g a) -> Coproduct f g a

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

-- | Left injection
left : f a -> Coproduct f g a
left fa = MkCoproduct (Left fa)

-- | Right injection
right : g a -> Coproduct f g a
right ga = MkCoproduct (Right ga)

-- | Eliminate a coproduct by providing eliminators for the left and
-- | right components
eliminate : (f a -> b) -> (g a -> b) -> Coproduct f g a -> b
eliminate f _ (MkCoproduct (Left a)) = f a
eliminate _ g (MkCoproduct (Right b)) = g b

-- | Change the underlying functors in a coproduct
bihoistCoproduct : (Functor f, Functor g, Functor h, Functor i) =>
                   ({a : Type} -> f a -> h a) ->
                   ({a : Type} -> g a -> i a) ->
                   ({a : Type} -> Coproduct f g a -> Coproduct h i a)
bihoistCoproduct natF natG (MkCoproduct e) = MkCoproduct (bimap natF natG e)

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

(Eq (f a), Eq (g a)) => Eq (Coproduct f g a) where
  (MkCoproduct fa) == (MkCoproduct ga) = fa == ga

(Ord (f a), Ord (g a)) => Ord (Coproduct f g a) where
  compare (MkCoproduct x) (MkCoproduct y) =
    assert_total $ case (x, y) of
      (Left fa, Left fa') => compare fa fa'
      (Left _, _)  => LT
      (_, Right _) => GT
      (Right ga, Right ga') => compare ga ga'

(Show (f a), Show (g a)) => Show (Coproduct f g a) where
  show (MkCoproduct x) = "Coproduct (" <+> show x <+> ")"

(Functor f, Functor g) => Functor (Coproduct f g) where
  map f (MkCoproduct e) = MkCoproduct (bimap (map f) (map f) e)

(Comonad f, Comonad g) => Comonad (Coproduct f g) where
  extract = eliminate extract extract

(Foldable f, Foldable g) => Foldable (Coproduct f g) where
  foldr f z = eliminate (foldr f z) (foldr f z)
  foldl f z = eliminate (foldl f z) (foldl f z)

(Traversable f, Traversable g) => Traversable (Coproduct f g) where
  traverse f = eliminate (map (MkCoproduct . Left)  . traverse f)
                         (map (MkCoproduct . Right) . traverse f)

max_stars_repo_name: Risto-Stevcev/idris-functors

max_issues_repo_name: Risto-Stevcev/idris-functors

max_forks_repo_name: Risto-Stevcev/idris-functors


text:
module WebAssembly.Validation.Modules.Tables

import WebAssembly.Structure
import WebAssembly.Validation.Conventions
import WebAssembly.Validation.Types

||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#tables)
|||
||| ```
||| ⊢ tabletype ok
||| --------------------------------
||| C ⊢ {type tabletype} : tabletype
||| ```
public export
data ValidTable : Context -> Table -> TableType -> Type where
  MkValidTable : (c : Context)
              -> (tabletype : TableType)
              -> ValidTableType tabletype
              -> ValidTable c (MkTable tableype) tabletype

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Web.Internal.WebidlPrim

import JS
import Web.Internal.Types

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

namespace DOMException

  export
  %foreign "browser:lambda:(a,b)=> new DOMException(a,b)"
  prim__new : UndefOr String -> UndefOr String -> PrimIO DOMException

  export
  %foreign "browser:lambda:x=>x.code"
  prim__code : DOMException -> PrimIO Bits16

  export
  %foreign "browser:lambda:x=>x.message"
  prim__message : DOMException -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.name"
  prim__name : DOMException -> PrimIO String

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

namespace Function

  export
  %foreign "browser:lambda:x=>(a)=>x(a)()"
  prim__toFunction : ( IO (Array AnyPtr) -> IO AnyPtr ) -> PrimIO Function

namespace VoidFunction

  export
  %foreign "browser:lambda:x=>()=>x()()"
  prim__toVoidFunction : (() -> IO ()) -> PrimIO VoidFunction


text:
module JS

import public Control.Monad.Either
import public Data.IOArray.Prims
import public Data.List.Elem
import public Data.Maybe
import public Data.SOP
import public Experimental.Prelude
import public JS.Any
import public JS.Attribute
import public JS.Array
import public JS.ByteString
import public JS.Boolean
import public JS.Buffer
import public JS.Callback
import public JS.Inheritance
import public JS.Marshall
import public JS.Nullable
import public JS.Number
import public JS.Object
import public JS.Promise
import public JS.Record
import public JS.Undefined
import public JS.Union
import public JS.Util
import public JS.VarArg


text:
data EqNat : (num1 : Nat) -> (Num2 : Nat) -> Type where
  Same : (num : Nat) -> EqNat num num

sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS j j (Same j) = Same (S j)

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just (Same 0)
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              (Just eq) => Just (sameS _ _ eq)

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

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case checkEqNat m len of
                                 Nothing => Nothing
                                 (Just (Same len)) => Just input

same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x ::xs = x :: ys
same_cons Refl = Refl

same_lists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
same_lists Refl Refl = Refl

data ThreeEq : (a : Nat) -> (b : Nat) -> (c : Nat) -> Type where
  ThreeSame : (num : Nat) -> ThreeEq num num num

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS Z Z Z (ThreeSame Z) = ThreeSame (S Z)
allSameS (S k) (S k) (S k) (ThreeSame (S k)) = ThreeSame (S (S k))

zeroNotSuc : (0 = S k) -> Void
zeroNotSuc Refl impossible

sucNotZero : (S k = 0) -> Void
sucNotZero Refl impossible

noRec : (contra : (k = j) -> Void) -> (S k = S j) -> Void
noRec contra Refl = contra Refl

decCheckEqNat : (num1 : Nat) -> (num2 : Nat) -> Dec (num1 = num2)
decCheckEqNat Z Z = Yes Refl
decCheckEqNat Z (S k) = No zeroNotSuc
decCheckEqNat (S k) Z = No sucNotZero
decCheckEqNat (S k) (S j) = case decCheckEqNat k j of
                                 (Yes prf) => Yes (cong prf)
                                 (No contra) => No (noRec contra)

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

headUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
    (contra : (x = y) -> Void) -> ((x::xs) = (y::ys)) -> Void
headUnequal contra Refl = contra Refl

tailUnequal : DecEq a => {xs : Vect n a} -> {ys : Vect n a} ->
    (contra : (xs = ys) -> Void) -> ((x::xs) = (y::ys)) -> Void
tailUnequal contra Refl = contra Refl

DecEq a => DecEq (Vect n a) where
  decEq [] [] = Yes Refl
  decEq (x :: xs) (y :: ys) = case decEq x y of
                                 (Yes Refl) => (case decEq xs ys of
                                                     (Yes Refl) => Yes Refl
                                                     (No contra) => No (tailUnequal contra))
                                 (No contra) => No (headUnequal contra)


text:
module Idrlisp.Code

import Control.Monad.State
import Idrlisp.Pattern

%default total

mutual
  public export
  data Inst a
    = Ldc a
    | Ldv String
    | Ldf Pattern (Code a)
    | Ldm Pattern (Code a)
    | Ldb String
    | Sel (Code a) (Code a)
    | App Nat
    | Leave
    | Pop
    | Def String
    | Set String

  export
  data Code a = MkCode (List (Inst a))

export
empty : Code a
empty = MkCode []

export
tailPosition : Code a -> Bool
tailPosition (MkCode [Leave]) = True
tailPosition (MkCode _) = False

export
singleton : Inst a -> Code a
singleton = MkCode . pure

export
next : Code a -> Maybe (Inst a, Code a)
next (MkCode []) = Nothing
next (MkCode (x :: xs)) = Just (x, MkCode xs)

export
(++) : Code a -> Code a -> Code a
(++) (MkCode x) (MkCode y) = MkCode (x ++ y)

mutual
  showCode : Show a => String -> Code a -> State Nat (String, String)
  showCode header (MkCode insts) = do
    id <- get
    modify succ
    let label = "[" ++ show id ++ " " ++ header ++ "]"
    (body, innerCodes) <- showInsts insts
    pure (label, label ++ "\n" ++ body ++ innerCodes)

  showInsts : Show a => List (Inst a) -> State Nat (String, String)
  showInsts [] = pure ("", "")
  showInsts (inst :: rest) = do
    (inst, innerCodes) <- showInst inst
    (body, innerCodes') <- showInsts rest
    pure ("  " ++ inst ++ "\n" ++ body, innerCodes ++ innerCodes')

  showInst : Show a => Inst a -> State Nat (String, String)
  showInst (Ldc value) = pure ("ldc " ++ show value, "")
  showInst (Ldv var) = pure ("ldv " ++ var, "")
  showInst (Ldf pat body) = do
    (label, innerCodes) <- showCode ("fun " ++ show pat) body
    pure ("ldf " ++ label, innerCodes)
  showInst (Ldm pat body) = do
    (label, innerCodes) <- showCode ("macro " ++ show pat) body
    pure ("ldm " ++ label, innerCodes)
  showInst (Ldb name) = pure ("ldb " ++ name, "")
  showInst (Sel thenc elsec) = do
    (thenl, innerCodes) <- showCode "then" thenc
    (elsel, innerCodes') <- showCode "else" elsec
    pure ("sel " ++ thenl ++ " " ++ elsel, innerCodes ++ innerCodes')
  showInst (App arity) = pure ("app " ++ show arity, "")
  showInst Leave = pure ("leave", "")
  showInst Pop = pure ("pop", "")
  showInst (Def name) = pure ("def " ++ name, "")
  showInst (Set name) = pure ("set " ++ name, "")

export
Show a => Show (Code a) where
  show code = evalState (snd <$> showCode "entry" code) 0

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
||| Definition and helper functions related to the LSP server implementation
||| configuration.
|||
||| (C) The Idris Community, 2021
module Server.Configuration

import Core.FC
import Data.SortedSet
import Language.LSP.CodeAction
import Language.LSP.Message.CodeAction
import Language.LSP.Message.Initialize
import Language.LSP.Message.Hover
import Language.LSP.Message.Location
import Language.LSP.Message.URI
import Libraries.Data.PosMap
import System.File

||| Label for the configuration reference.
public export
data LSPConf : Type where

||| Type for the LSP server configuration.
public export
record LSPConfiguration where
  constructor MkLSPConfiguration
  ||| File handle where to read LSP messages.
  inputHandle : File
  ||| File handle where to output LSP messages.
  outputHandle : File
  ||| File handle where to put log messages.
  logHandle : File
  ||| If the initialization protocol has succeded, it contains the client configuration.
  ||| @see https://microsoft.github.io/language-server-protocol/specifications/specification-3-16/#initialize
  initialized : Maybe InitializeParams
  ||| True if the client has completed the shutdown protocol.
  ||| @see https://microsoft.github.io/language-server-protocol/specifications/specification-3-16/#shutdown
  isShutdown : Bool
  ||| The currently loaded file, if any, and its version.
  openFile : Maybe (DocumentURI, Int)
  ||| Files with modification not saved. Command will fail on these files.
  dirtyFiles : SortedSet DocumentURI
  ||| Files with errors
  errorFiles : SortedSet DocumentURI
  ||| Semantic tokens have been sent
  semanticTokensSentFiles : SortedSet DocumentURI
  ||| Limit for multiple search results
  searchLimit : Nat
  ||| List of quickfixes to be send in addition to other code actions
  quickfixes : List CodeAction
  ||| Cached code actions by position
  cachedActions : PosMap (Range, IdrisAction, List CodeAction)
  ||| Cached hovers
  cachedHovers : PosMap (Range, Hover)
  ||| next id for requests to the server
  nextRequestId : Nat

||| Server default configuration. Uses standard input and standard output for input/output.
export
defaultConfig : LSPConfiguration
defaultConfig =
  MkLSPConfiguration
    { inputHandle       = stdin
    , outputHandle      = stdout
    , logHandle         = stderr
    , initialized       = Nothing
    , isShutdown        = False
    , openFile          = Nothing
    , dirtyFiles        = empty
    , errorFiles        = empty
    , semanticTokensSentFiles = empty
    , searchLimit       = 5
    , quickfixes        = []
    , cachedActions     = empty
    , cachedHovers      = empty
    , nextRequestId     = 0
    }


text:
module Part2.Sec3_2_3_gen
import Data.Vect

{-
implementation code generated 100% by idris
steps (based on Atom key bindings):
 * Add def with cursor on mapV (Ctr-Alt-a)
 * Case split xs (Ctr-Alt-c)
 * Search (Crl-Alt-s) for both holes
-}
mapV : (a -> b) -> Vect n a -> Vect n b
mapV f [] = []
mapV f (x :: xs) = f x :: mapV f xs

mapV2 : (a -> b) -> Vect n a -> Vect n b
mapV2 f [] = ?mapV2_rhs_1
mapV2 f (x :: xs) = ?mapV2_rhs_2

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
import Data.List
import Data.List.Views

{-
Note:
The | says that, in the recursive calls,
you want to bypass constructing the view,
because you already have appropriate views for lefts and rights.
-}

mergeSort : Ord a => List a -> List a
mergeSort input with (splitRec input)
  mergeSort [] | SplitRecNil = []
  mergeSort [x] | (SplitRecOne x) = [x]
  mergeSort (lefts ++ rights) | (SplitRecPair lefts rights lrec rrec)
            = merge (mergeSort lefts | lrec) (mergeSort rights | rrec)


text:
module Control.Cont.Exception

import Control.EffectAlgebra

import Control.Monad.Free

public export
data EitherC : Type -> (Type -> Type) -> Type -> Type where
  Throw : e -> EitherC e m a
  Catch : forall t. m t -> (e -> m t) -> (t -> m a) -> EitherC e m a

public export
Functor m => Functor (EitherC e m) where
  map f (Throw e) = Throw e
  map f (Catch p h k) = Catch p h (map f . k)

public export
HFunctor (EitherC e) where
  hmap t (Throw x) = Throw x
  hmap t (Catch p h k) = Catch (t p) (t . h) (t . k)

public export
Syntax (EitherC e) where
  emap f (Throw e) = Throw e
  emap f (Catch p h k) = Catch p h (f . k)

  weave f hdl (Throw x) = Throw x
  weave f hdl (Catch p h k) =
    Catch (hdl (map (const p) f))
          (\e => hdl (map (const (h e)) f))
          (hdl . map k)

public export
runEitherC : Syntax sig
      => Free (EitherC e :+: sig) a
      -> Free sig (Either e a)
runEitherC (Return x) = Return (Right x)
runEitherC (Op (Inl (Throw x))) = Return (Left x)
runEitherC (Op (Inl (Catch p h k))) = do
  r <- runEitherC p
  case r of
    Left e => do
      r <- runEitherC (h e)
      case r of
        Left e => Return (Left e)
        Right x => runEitherC (k x)
    Right x => runEitherC (k x)
runEitherC (Op (Inr op)) = Op (weave {s = Either e} (Right ()) hdl op) where
  hdl : Handler (Either e) (Free (EitherC e :+: sig)) (Free sig)
  hdl = either (Return . Left) runEitherC

public export
throw : (Inj (EitherC e) sig) => e -> Free sig a
throw err = inject {sub = EitherC e} (Throw err)

public export
catch : (p : Inj (EitherC e) sig) => Free sig a -> (e -> Free sig a) -> Free sig a
catch p h = inject {sub = EitherC e} (Catch p h Return)

public export
orThrow : Syntax sig => Inj (EitherC e) sig => Maybe a -> Free sig e -> Free sig a
orThrow Nothing e  = e >>= throw
orThrow (Just x) e = return x


text:
module Greeter.Backend

import Effects
import Effect.StdIO
import Effect.Default
import Effect.State
import Effect.Msg

import System.Protocol

import RFC.Greeter
import Greeter.Common

%access public

-- --------------------------------------------------------- [ Greeter Backend ]

private
obtainHelp : String
obtainHelp = unwords ["List 'o Commands\n" ++
                      "\t :greet <name>\n" ++
                      "\t :q\n" ++
                      "\t :cheat\n" ++
                      "\t :help,:?\n"]

private
constructGreeting : Int -> String
constructGreeting i = "Enter Command (" ++ func i ++ ", :? for help) :"
  where
    func : Int -> String
    func b = case b > 0 of
               True  => show i ++ " greetings remaining"
               False =>  "no more greetings"

mutual
  covering
  backendBody : PID -> GreeterBackend gBody ()
  backendBody proc = do
      setChan 'Alice proc
      sendTo 'Alice "Enter Command:"
      resp <- recvFrom 'Alice
      case resp of

        GreetMe str => do
          sendTo 'Alice ("Hello: " ++ str)
          dropChan 'Alice
          rec (backendBody proc)

        Help => do
          sendTo 'Alice obtainHelp
          dropChan 'Alice
          rec (backendBody proc)

        Quit => do
          dropChan 'Alice
          return ()

  covering
  backendBody' : PID -> GreeterBackend gBody ()
  backendBody' proc = do
      setChan 'Alice proc
      sendTo 'Alice (constructGreeting !get)

      case !(recvFrom 'Alice) of
        GreetMe str => do

          let resp = if !get > 0
                       then ("Hello: " ++ str)
                       else "Sorry ran out of greetings."
          update (\x => x - 1)
          sendTo 'Alice resp
          dropChan 'Alice
          rec (backendBody' proc)

        Help => do
          sendTo 'Alice obtainHelp
          dropChan 'Alice
          rec (backendBody proc)

        Quit => do
          dropChan 'Alice
          return ()

covering
greeterBackend : PID
               -> (PID -> GreeterBackend gBody ())
               -> GreeterBackend (greeter gBody) ()
greeterBackend proc body = do
    setChan 'Alice proc
    foo <- recvFrom 'Alice
    dropChan 'Alice
    (body proc)
    return ()

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