text:
module Idris.Pretty

import Core.Metadata
import Data.List
import Data.Maybe
import Data.String
import Libraries.Control.ANSI.SGR

import Parser.Lexer.Source

import public Idris.Pretty.Render

import public Libraries.Text.PrettyPrint.Prettyprinter
import public Libraries.Text.PrettyPrint.Prettyprinter.Util

import Idris.REPL.Opts
import Idris.Syntax

%default covering

public export
data IdrisSyntax
  = Hole
  | TCon (Maybe Name) -- these may be primitive types
  | DCon (Maybe Name) -- these may be primitive constructors
  | Fun  Name
  | Bound
  | Keyword
  | Pragma

export
syntaxToDecoration : IdrisSyntax -> Maybe Decoration
syntaxToDecoration Hole     = Nothing
syntaxToDecoration (TCon{}) = pure Typ
syntaxToDecoration (DCon{}) = pure Data
syntaxToDecoration (Fun{})  = pure Function
syntaxToDecoration Bound    = pure Bound
syntaxToDecoration Keyword  = pure Keyword
syntaxToDecoration Pragma   = Nothing

export
kindAnn : KindedName -> Maybe IdrisSyntax
kindAnn (MkKindedName mcat fn nm) = do
    cat <- mcat
    pure $ case cat of
      Bound     => Bound
      Func      => Fun fn
      DataCon{} => DCon (Just fn)
      TyCon{}   => TCon (Just fn)

export
showCategory : (IdrisSyntax -> ann) -> GlobalDef -> Doc ann -> Doc ann
showCategory embed def = annotateM (embed <$> kindAnn (gDefKindedName def))

public export
data IdrisAnn
  = Warning
  | Error
  | ErrorDesc
  | FileCtxt
  | Code
  | Meta
  | Syntax IdrisSyntax

export
annToDecoration : IdrisAnn -> Maybe Decoration
annToDecoration (Syntax syn) = syntaxToDecoration syn
annToDecoration _ = Nothing

export
syntaxAnn : IdrisSyntax -> AnsiStyle
syntaxAnn Hole = color BrightGreen
syntaxAnn (TCon{}) = color BrightBlue
syntaxAnn (DCon{}) = color BrightRed
syntaxAnn (Fun{})  = color BrightGreen
syntaxAnn Bound    = italic
syntaxAnn Keyword  = color BrightWhite
syntaxAnn Pragma   = color BrightMagenta

export
colorAnn : IdrisAnn -> AnsiStyle
colorAnn Warning = color Yellow <+> bold
colorAnn Error = color BrightRed <+> bold
colorAnn ErrorDesc = bold
colorAnn FileCtxt = color BrightBlue
colorAnn Code = color Magenta
colorAnn Meta = color Green
colorAnn (Syntax syn) = syntaxAnn syn

export
warning : Doc IdrisAnn -> Doc IdrisAnn
warning = annotate Warning

export
error : Doc IdrisAnn -> Doc IdrisAnn
error = annotate Error

export
errorDesc : Doc IdrisAnn -> Doc IdrisAnn
errorDesc = annotate ErrorDesc

export
fileCtxt : Doc IdrisAnn -> Doc IdrisAnn
fileCtxt = annotate FileCtxt

export
keyword : Doc IdrisSyntax -> Doc IdrisSyntax
keyword = annotate Keyword

export
meta : Doc IdrisAnn -> Doc IdrisAnn
meta = annotate Meta

export
hole : Doc IdrisSyntax -> Doc IdrisSyntax
hole = annotate Hole

export
code : Doc IdrisAnn -> Doc IdrisAnn
code = annotate Code

let_ : Doc IdrisSyntax
let_ = keyword (pretty "let")

in_ : Doc IdrisSyntax
in_ = keyword (pretty "in")

case_ : Doc IdrisSyntax
case_ = keyword (pretty "case")

of_ : Doc IdrisSyntax
of_ = keyword (pretty "of")

do_ : Doc IdrisSyntax
do_ = keyword (pretty "do")

with_ : Doc IdrisSyntax
with_ = keyword (pretty "with")

record_ : Doc IdrisSyntax
record_ = keyword (pretty "record")

impossible_ : Doc IdrisSyntax
impossible_ = keyword (pretty "impossible")

auto_ : Doc IdrisSyntax
auto_ = keyword (pretty "auto")

default_ : Doc IdrisSyntax
default_ = keyword (pretty "default")

rewrite_ : Doc IdrisSyntax
rewrite_ = keyword (pretty "rewrite")

export
pragma : Doc IdrisSyntax -> Doc IdrisSyntax
pragma = annotate Pragma

export
prettyRig : RigCount -> Doc ann
prettyRig = elimSemi (pretty '0' <+> space)
                     (pretty '1' <+> space)
                     (const emptyDoc)

mutual
  prettyAlt : PClause' KindedName -> Doc IdrisSyntax
  prettyAlt (MkPatClause _ lhs rhs _) =
    space <+> pipe <++> prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs <+> semi
  prettyAlt (MkWithClause _ lhs wval prf flags cs) =
    space <+> pipe <++> angles (angles (reflow "with alts not possible")) <+> semi
  prettyAlt (MkImpossible _ lhs) =
    space <+> pipe <++> prettyTerm lhs <++> impossible_ <+> semi

  prettyCase : PClause' KindedName -> Doc IdrisSyntax
  prettyCase (MkPatClause _ lhs rhs _) =
    prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs
  prettyCase (MkWithClause _ lhs rhs prf flags _) =
    space <+> pipe <++> angles (angles (reflow "with alts not possible"))
  prettyCase (MkImpossible _ lhs) =
    prettyTerm lhs <++> impossible_

  prettyString : PStr' KindedName -> Doc IdrisSyntax
  prettyString (StrLiteral _ str) = pretty str
  prettyString (StrInterp _ tm) = prettyTerm tm

  prettyDo : PDo' KindedName -> Doc IdrisSyntax
  prettyDo (DoExp _ tm) = prettyTerm tm
  prettyDo (DoBind _ _ n tm) = pretty n <++> pretty "<-" <++> prettyTerm tm
  prettyDo (DoBindPat _ l tm alts) =
    prettyTerm l <++> pretty "<-" <++> prettyTerm tm <+> hang 4 (fillSep $ prettyAlt <$> alts)
  prettyDo (DoLet _ _ l rig _ tm) =
    let_ <++> prettyRig rig <+> pretty l <++> equals <++> prettyTerm tm
  prettyDo (DoLetPat _ l _ tm alts) =
    let_ <++> prettyTerm l <++> equals <++> prettyTerm tm <+> hang 4 (fillSep $ prettyAlt <$> alts)
  prettyDo (DoLetLocal _ ds) =
    let_ <++> braces (angles (angles (pretty "definitions")))
  prettyDo (DoRewrite _ rule) = rewrite_ <+> prettyTerm rule

  prettyUpdate : PFieldUpdate' KindedName -> Doc IdrisSyntax
  prettyUpdate (PSetField path v) =
    concatWith (surround dot) (pretty <$> path) <++> equals <++> prettyTerm v
  prettyUpdate (PSetFieldApp path v) =
    concatWith (surround dot) (pretty <$> path) <++> pretty '$' <+> equals <++> prettyTerm v

  prettyBinder : Name -> Doc IdrisSyntax
  prettyBinder = annotate Bound . pretty

  export
  prettyTerm : IPTerm -> Doc IdrisSyntax
  prettyTerm = go Open
    where
      startPrec : Prec
      startPrec = User 0
      appPrec : Prec
      appPrec = User 10
      leftAppPrec : Prec
      leftAppPrec = User 9
      prettyOp : OpStr' KindedName -> Doc IdrisSyntax
      prettyOp op@(MkKindedName _ _ nm) = if isOpName nm
        then annotateM (kindAnn op) $ pretty nm
        else Chara '`' <+> annotateM (kindAnn op) (pretty nm) <+> Chara '`'

      go : Prec -> IPTerm -> Doc IdrisSyntax
      go d (PRef _ nm) = annotateM (kindAnn nm) $ pretty nm.rawName
      go d (PPi _ rig Explicit Nothing arg ret) =
        parenthesise (d > startPrec) $ group $
          branchVal
            (go startPrec arg <++> "->" <++> go startPrec ret)
            (parens (prettyRig rig <+> "_" <++> colon <++> go startPrec arg)
                    <++> "->" <+> softline <+> go startPrec ret)
            rig
      go d (PPi _ rig Explicit (Just n) arg ret) =
        parenthesise (d > startPrec) $ group $
          parens (prettyRig rig <+> prettyBinder n
                 <++> colon <++> go startPrec arg)
                  <++> "->" <+> softline <+> go startPrec ret
      go d (PPi _ rig Implicit Nothing arg ret) =
        parenthesise (d > startPrec) $ group $
          braces (prettyRig rig <+> pretty '_'
                 <++> colon <++> go startPrec arg)
                 <++> "->" <+> softline <+> go startPrec ret
      go d (PPi _ rig Implicit (Just n) arg ret) =
        parenthesise (d > startPrec) $ group $
          braces (prettyRig rig <+> prettyBinder n
                 <++> colon <++> go startPrec arg)
                 <++> "->" <+> softline <+> go startPrec ret
      go d (PPi _ rig AutoImplicit Nothing arg ret) =
        parenthesise (d > startPrec) $ group $
          branchVal
            (go startPrec arg <++> "=>" <+> softline <+> go startPrec ret)
            (braces (auto_ <++> prettyRig rig <+> "_"
                    <++> colon <++> go startPrec arg)
                    <++> "->" <+> softline <+> go startPrec ret)
            rig
      go d (PPi _ rig AutoImplicit (Just n) arg ret) =
        parenthesise (d > startPrec) $ group $
          braces (auto_ <++> prettyRig rig <+> prettyBinder n
                 <++> colon <++> go startPrec arg)
                 <++> "->" <+> softline <+> go startPrec ret
      go d (PPi _ rig (DefImplicit t) Nothing arg ret) =
        parenthesise (d > startPrec) $ group $
          braces (default_ <++> go appPrec t <++> prettyRig rig <+> "_"
                 <++> colon <++> go startPrec arg)
                 <++> "->" <+> softline <+> go startPrec ret
      go d (PPi _ rig (DefImplicit t) (Just n) arg ret) =
        parenthesise (d > startPrec) $ group $
          braces (default_ <++> go appPrec t
                 <++> prettyRig rig <+> prettyBinder n
                 <++> colon <++> go startPrec arg)
                 <++> "->" <+> softline <+> go startPrec ret
      go d (PLam _ rig _ n ty sc) =
          let (ns, sc) = getLamNames [(rig, n, ty)] sc in
              parenthesise (d > startPrec) $ group $
                backslash <+> prettyBindings ns <++> "=>" <+> softline <+> go startPrec sc
        where
          getLamNames : List (RigCount, IPTerm, IPTerm) ->
                        IPTerm ->
                        (List (RigCount, IPTerm, IPTerm), IPTerm)
          getLamNames acc (PLam _ rig _ n ty sc) = getLamNames ((rig, n, ty) :: acc) sc
          getLamNames acc sc = (reverse acc, sc)

          prettyBindings : List (RigCount, IPTerm, IPTerm) -> Doc IdrisSyntax
          prettyBindings [] = neutral
          prettyBindings [(rig, n, (PImplicit _))] = prettyRig rig <+> go startPrec n
          prettyBindings [(rig, n, ty)] = prettyRig rig <+> go startPrec n <++> colon <++> go startPrec ty
          prettyBindings ((rig, n, (PImplicit _)) :: ns) = prettyRig rig <+> go startPrec n <+> comma <+> line <+> prettyBindings ns
          prettyBindings ((rig, n, ty) :: ns) = prettyRig rig <+> go startPrec n <++> colon <++> go startPrec ty <+> comma <+> line <+> prettyBindings ns
      go d (PLet _ rig n (PImplicit _) val sc alts) =
          -- Hide uninformative lets
          -- (Those that look like 'let x = x in ...')
          -- Makes printing the types of names bound in where clauses a lot
          -- more readable
          fromMaybe fullLet $ do
            nName   <- getPRefName n
            valName <- getPRefName val
            guard (show nName == show valName)
            pure continuation

         -- Hide lets that bind to underscore
         -- That is, 'let _ = x in ...'
         -- Those end up polluting the types of let bound variables in some
         -- occasions
          <|> do
            nName <- getPRefName n
            guard (isUnderscoreName nName)
            pure continuation

        where

          continuation : Doc IdrisSyntax
          continuation = go startPrec sc

          fullLet : Doc IdrisSyntax
          fullLet = parenthesise (d > startPrec) $ group $ align $
            let_ <++> (group $ align $ hang 2 $ prettyRig rig <+> go startPrec n <++> equals <+> line <+> go startPrec val) <+> line
              <+> in_ <++> (group $ align $ hang 2 $ continuation)

          getPRefName : IPTerm -> Maybe Name
          getPRefName (PRef _ n) = Just (rawName n)
          getPRefName _ = Nothing

      go d (PLet _ rig n ty val sc alts) =
        parenthesise (d > startPrec) $ group $ align $
          let_ <++> (group $ align $ hang 2 $ prettyRig rig <+> go startPrec n <++> colon <++> go startPrec ty <++> equals <+> line <+> go startPrec val) <+> hardline
            <+> hang 4 (fillSep (prettyAlt <$> alts)) <+> line <+> in_ <++> (group $ align $ hang 2 $ go startPrec sc)
      go d (PCase _ tm cs) =
        parenthesise (d > appPrec) $ align $ case_ <++> go startPrec tm <++> of_ <+> line <+>
          braces (vsep $ punctuate semi (prettyCase <$> cs))
      go d (PLocal _ ds sc) =
        parenthesise (d > startPrec) $ group $ align $
          let_ <++> braces (angles (angles "definitions")) <+> line <+> in_ <++> go startPrec sc
      go d (PUpdate _ fs) =
        parenthesise (d > appPrec) $ group $ record_ <++> braces (vsep $ punctuate comma (prettyUpdate <$> fs))
      go d (PApp _ f a) =
        let catchall : Lazy (Doc IdrisSyntax)
               := go leftAppPrec f <++> go appPrec a

        in parenthesise (d > appPrec) $ group $ case f of
          (PRef _ n) =>
            if isJust (isRF $ rawName n)
            then go leftAppPrec a <++> go appPrec f
            else catchall
          _ => catchall
      go d (PWithApp _ f a) = go d f <++> pipe <++> go d a
      go d (PDelayed _ LInf ty) = parenthesise (d > appPrec) $ "Inf" <++> go appPrec ty
      go d (PDelayed _ _ ty) = parenthesise (d > appPrec) $ "Lazy" <++> go appPrec ty
      go d (PDelay _ tm) = parenthesise (d > appPrec) $ "Delay" <++> go appPrec tm
      go d (PForce _ tm) = parenthesise (d > appPrec) $ "Force" <++> go appPrec tm
      go d (PAutoApp _ f a) =
        parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> "@" <+> braces (go startPrec a)
      go d (PNamedApp _ f n (PRef _ a)) =
        parenthesise (d > appPrec) $ group $
          if n == rawName a
             then go leftAppPrec f <++> braces (pretty n)
             else go leftAppPrec f <++> braces (pretty n <++> equals <++> pretty a.rawName)
      go d (PNamedApp _ f n a) =
        parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> braces (pretty n <++> equals <++> go d a)
      go d (PSearch _ _) = pragma "%search"
      go d (PQuote _ tm) = parenthesise (d > appPrec) $ "`" <+> parens (go startPrec tm)
      go d (PQuoteName _ n) = parenthesise (d > appPrec) $ "`" <+> braces (braces (pretty n))
      go d (PQuoteDecl _ tm) = parenthesise (d > appPrec) $ "`" <+> brackets (angles (angles (pretty "declaration")))
      go d (PUnquote _ tm) = parenthesise (d > appPrec) $ "~" <+> parens (go startPrec tm)
      go d (PRunElab _ tm) = parenthesise (d > appPrec) $ pragma "%runElab" <++> go startPrec tm
      go d (PPrimVal _ c) =
        let decor = if isPrimType c then TCon Nothing else DCon Nothing in
        annotate decor $ pretty c
      go d (PHole _ _ n) = hole (pretty (strCons '?' n))
      go d (PType _) = annotate (TCon Nothing) "Type"
      go d (PAs _ _ n p) = pretty n <+> "@" <+> go d p
      go d (PDotted _ p) = dot <+> go d p
      go d (PImplicit _) = "_"
      go d (PInfer _) = annotate Hole $ "?"
      go d (POp _ _ op x y) = parenthesise (d > appPrec) $ group $ go startPrec x <++> prettyOp op <++> go startPrec y
      go d (PPrefixOp _ _ op x) = parenthesise (d > appPrec) $ prettyOp op <+> go startPrec x
      go d (PSectionL _ _ op x) = parens (prettyOp op <++> go startPrec x)
      go d (PSectionR _ _ x op) = parens (go startPrec x <++> prettyOp op)
      go d (PEq fc l r) = parenthesise (d > appPrec) $ go startPrec l <++> equals <++> go startPrec r
      go d (PBracketed _ tm) = parens (go startPrec tm)
      go d (PString _ xs) = parenthesise (d > appPrec) $ hsep $ punctuate "++" (prettyString <$> xs)
      go d (PMultiline _ indent xs) = "multiline" <++> (parenthesise (d > appPrec) $ hsep $ punctuate "++" (prettyString <$> concat xs))
      go d (PDoBlock _ ns ds) = parenthesise (d > appPrec) $ group $ align $ hang 2 $ do_ <++> (vsep $ punctuate semi (prettyDo <$> ds))
      go d (PBang _ tm) = "!" <+> go d tm
      go d (PIdiom _ tm) = enclose (pretty "[|") (pretty "|]") (go startPrec tm)
      go d (PList _ _ xs) = brackets (group $ align $ vsep $ punctuate comma (go startPrec . snd <$> xs))
      go d (PSnocList _ _ xs) = brackets {ldelim = "[<"}
                                   (group $ align $ vsep $ punctuate comma (go startPrec . snd <$> xs))
      go d (PPair _ l r) = group $ parens (go startPrec l <+> comma <+> line <+> go startPrec r)
      go d (PDPair _ _ l (PImplicit _) r) = group $ parens (go startPrec l <++> pretty "**" <+> line <+> go startPrec r)
      go d (PDPair _ _ l ty r) = group $ parens (go startPrec l <++> colon <++> go startPrec ty <++> pretty "**" <+> line <+> go startPrec r)
      go d (PUnit _) = "()"
      go d (PIfThenElse _ x t e) =
        parenthesise (d > appPrec) $ group $ align $ hang 2 $ vsep
          [keyword "if" <++> go startPrec x, keyword "then" <++> go startPrec t, keyword "else" <++> go startPrec e]
      go d (PComprehension _ ret es) =
          group $ brackets (go startPrec (dePure ret) <++> pipe <++> vsep (punctuate comma (prettyDo . deGuard <$> es)))
        where
          dePure : IPTerm -> IPTerm
          dePure tm@(PApp _ (PRef _ n) arg)
            = if dropNS (rawName n) == UN (Basic "pure") then arg else tm
          dePure tm = tm

          deGuard : PDo' KindedName -> PDo' KindedName
          deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg))
            = if dropNS (rawName n) == UN (Basic "guard") then DoExp fc arg else tm
          deGuard tm = tm
      go d (PRewrite _ rule tm) =
        parenthesise (d > appPrec) $ group $ rewrite_ <++> go startPrec rule <+> line <+> in_ <++> go startPrec tm
      go d (PRange _ start Nothing end) =
        brackets (go startPrec start <++> pretty ".." <++> go startPrec end)
      go d (PRange _ start (Just next) end) =
        brackets (go startPrec start <+> comma <++> go startPrec next <++> pretty ".." <++> go startPrec end)
      go d (PRangeStream _ start Nothing) = brackets (go startPrec start <++> pretty "..")
      go d (PRangeStream _ start (Just next)) =
        brackets (go startPrec start <+> comma <++> go startPrec next <++> pretty "..")
      go d (PUnifyLog _ lvl tm) = go d tm
      go d (PPostfixApp fc rec fields) =
        parenthesise (d > appPrec) $ go startPrec rec <++> dot <+> concatWith (surround dot) (map pretty fields)
      go d (PPostfixAppPartial fc fields) =
        parens (dot <+> concatWith (surround dot) (map pretty fields))
      go d (PWithUnambigNames fc ns rhs) = parenthesise (d > appPrec) $ group $ with_ <++> pretty ns <+> line <+> go startPrec rhs

export
render : {auto o : Ref ROpts REPLOpts} -> Doc IdrisAnn -> Core String
render = render colorAnn

export
renderWithDecorations :
  {auto c : Ref Ctxt Defs} ->
  {auto o : Ref ROpts REPLOpts} ->
  (ann -> Maybe ann') ->
  Doc ann ->
  Core (String, List (Span ann'))
renderWithDecorations f doc =
  do (str, mspans) <- Render.renderWithSpans doc
     let spans = mapMaybe (traverse f) mspans
     pure (str, spans)


text:
> module SequentialDecisionProblems.DeterministicDefaults

> import Control.Monad.Identity

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.Utils

> import Identity.Operations
> import Identity.Properties

> %default total
> %auto_implicits off

In deterministic SDPs, |M = Identity|:

> SequentialDecisionProblems.CoreTheory.M =
>   Identity

Thus, |M| is a functor:

> SequentialDecisionProblems.CoreTheory.fmap =
>   Identity.Operations.fmap

, |M| is a monad:

> SequentialDecisionProblems.Utils.ret =
>   Identity.Operations.ret

> SequentialDecisionProblems.Utils.bind =
>   Identity.Operations.bind

Moreover, |M| is a container monad

> SequentialDecisionProblems.CoreTheory.Elem =
>   Identity.Operations.Elem

> SequentialDecisionProblems.CoreTheory.NotEmpty =
>   Identity.Operations.NonEmpty

> SequentialDecisionProblems.CoreTheory.All =
>   Identity.Operations.All

> SequentialDecisionProblems.CoreTheory.elemNotEmptySpec0 =
>   Identity.Properties.elemNonEmptySpec0

> SequentialDecisionProblems.CoreTheory.elemNotEmptySpec1 =
>   Identity.Properties.elemNonEmptySpec1

> SequentialDecisionProblems.CoreTheory.tagElem =
>   Identity.Operations.tagElem

> SequentialDecisionProblems.CoreTheory.allElemSpec0 =
>   Identity.Properties.containerMonadSpec3

and |All| and |NotEmpty| are finite and decidable:

> SequentialDecisionProblems.Utils.finiteAll =
>   Identity.Properties.finiteAll

> SequentialDecisionProblems.Utils.finiteNotEmpty =
>   Identity.Properties.finiteNonEmpty

> SequentialDecisionProblems.Utils.decidableAll =
>   Identity.Properties.decidableAll

> SequentialDecisionProblems.Utils.decidableNotEmpty =
>   Identity.Properties.decidableNonEmpty

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module B

import A

public export

--if you change the name of the function from BFromInteger to AInt here and in A.idr, as
--below, the problem disappears. Not sure the pattern here, but some names cause an issue
--and some do not
-- BFunc : AInt x => (a : x) -> Type
BFunc : BFromInteger x => (a : x) -> Type
BFunc a = (a = a)

ext: idr


text:
-- Computing the parameters

module Core.Context.Data

import Core.Context
import Core.Context.Log
import Core.Normalise

import Data.List
import Data.Maybe

%default covering

-- If a name appears more than once in an argument list, only the first is
-- considered a parameter
dropReps : List (Maybe (Term vars)) -> List (Maybe (Term vars))
dropReps [] = []
dropReps {vars} (Just (Local fc r x p) :: xs)
    = Just (Local fc r x p) :: assert_total (dropReps (map toNothing xs))
  where
    toNothing : Maybe (Term vars) -> Maybe (Term vars)
    toNothing tm@(Just (Local _ _ v' _))
        = if x == v' then Nothing else tm
    toNothing tm = tm
dropReps (x :: xs) = x :: dropReps xs

updateParams : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
               Maybe (List (Maybe (Term vars))) ->
                  -- arguments to the type constructor which could be
                  -- parameters
                  -- Nothing, as an argument, means this argument can't
                  -- be a parameter position
               List (Term vars) ->
                  -- arguments to an application
               Core (List (Maybe (Term vars)))
updateParams Nothing args = dropReps <$> traverse couldBeParam args
  where
    couldBeParam : Term vars -> Core (Maybe (Term vars))
    couldBeParam tm = pure $ case !(etaContract tm) of
      Local fc r v p => Just (Local fc r v p)
      _ => Nothing
updateParams (Just args) args' = pure $ dropReps $ zipWith mergeArg args args'
  where
    mergeArg : Maybe (Term vars) -> Term vars -> Maybe (Term vars)
    mergeArg (Just (Local fc r x p)) (Local _ _ y _)
        = if x == y then Just (Local fc r x p) else Nothing
    mergeArg _ _ = Nothing

getPs : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
        Maybe (List (Maybe (Term vars))) -> Name -> Term vars ->
        Core (Maybe (List (Maybe (Term vars))))
getPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
      = do scPs <- getPs (map (map (map weaken)) acc) tyn sc
           pure $ map (map shrink) scPs
  where
    shrink : Maybe (Term (x :: vars)) -> Maybe (Term vars)
    shrink Nothing = Nothing
    shrink (Just tm) = shrinkTerm tm (DropCons SubRefl)
getPs acc tyn tm
    = case getFnArgs tm of
           (Ref _ _ n, args) =>
              if n == tyn
                 then Just <$> updateParams acc args
                 else pure acc
           _ => pure acc

toPos : Maybe (List (Maybe a)) -> List Nat
toPos Nothing = []
toPos (Just ns) = justPos 0 ns
  where
    justPos : Nat -> List (Maybe a) -> List Nat
    justPos i [] = []
    justPos i (Just x :: xs) = i :: justPos (1 + i) xs
    justPos i (Nothing :: xs) = justPos (1 + i) xs

getConPs : {auto _ : Ref Ctxt Defs} -> {vars : _} ->
           Maybe (List (Maybe (Term vars))) -> Name -> Term vars ->
           Core (List Nat)
getConPs acc tyn (Bind _ x (Pi _ _ _ ty) sc)
    = do bacc <- getPs acc tyn ty
         getConPs (map (map (map weaken)) bacc) tyn sc
getConPs acc tyn (Bind _ x (Let _ _ v ty) sc)
    = getConPs acc tyn (subst v sc)
getConPs acc tyn tm = toPos <$> getPs acc tyn tm

paramPos : {auto _ : Ref Ctxt Defs} -> Name -> (dcons : List ClosedTerm) ->
           Core (Maybe (List Nat))
paramPos tyn [] = pure Nothing -- no constructor!
paramPos tyn dcons = do
  candidates <- traverse (getConPs Nothing tyn) dcons
  pure $ Just $ intersectAll candidates

export
addData : {auto c : Ref Ctxt Defs} ->
          List Name -> Visibility -> Int -> DataDef -> Core Int
addData vars vis tidx (MkData (MkCon dfc tyn arity tycon) datacons)
    = do defs <- get Ctxt
         tag <- getNextTypeTag
         let allPos = allDet arity
         -- In case there are no constructors, all the positions are parameter positions!
         let paramPositions = fromMaybe allPos !(paramPos (Resolved tidx) (map type datacons))
         log "declare.data.parameters" 20 $
            "Positions of parameters for datatype" ++ show tyn ++
            ": [" ++ showSep ", " (map show paramPositions) ++ "]"
         let tydef = newDef dfc tyn top vars tycon vis
                            (TCon tag arity
                                  paramPositions
                                  allPos
                                  defaultFlags [] (map name datacons) Nothing)
         (idx, gam') <- addCtxt tyn tydef (gamma defs)
         gam'' <- addDataConstructors 0 datacons gam'
         put Ctxt (record { gamma = gam'' } defs)
         pure idx
  where
    allDet : Nat -> List Nat
    allDet Z = []
    allDet (S k) = [0..k]

    conVisibility : Visibility -> Visibility
    conVisibility Export = Private
    conVisibility x = x

    addDataConstructors : (tag : Int) -> List Constructor ->
                          Context -> Core Context
    addDataConstructors tag [] gam = pure gam
    addDataConstructors tag (MkCon fc n a ty :: cs) gam
        = do let condef = newDef fc n top vars ty (conVisibility vis) (DCon tag a Nothing)
             (idx, gam') <- addCtxt n condef gam
             -- Check 'n' is undefined
             Nothing <- lookupCtxtExact n gam
                 | Just gdef => throw (AlreadyDefined fc n)
             addDataConstructors (tag + 1) cs gam'


text:
module Idris.Error

import Core.CaseTree
import Core.Core
import Core.Context
import Core.Env
import Core.Metadata
import Core.Options
import Core.Value

import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Idris.Pretty

import Parser.Source

import Data.List
import Data.List1
import Data.Maybe
import Data.Stream
import Data.String

import Libraries.Data.List.Extra
import Libraries.Data.List1 as Lib
import Libraries.Data.String.Extra
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Utils.String
import Libraries.Data.String.Extra

import System.File

%hide Data.String.lines
%hide Data.String.lines'
%hide Data.String.unlines
%hide Data.String.unlines'

%default covering

keyword : Doc IdrisAnn -> Doc IdrisAnn
keyword = annotate (Syntax Keyword)

-- | Add binding site information if the term is simply a machine-inserted name
pShowMN : {vars : _} -> Term vars -> Env t vars -> Doc IdrisAnn -> Doc IdrisAnn
pShowMN t env acc = case t of
  Local fc _ idx p => case dropAllNS (nameAt p) of
      MN _ _ => acc <++> parens ("implicitly bound at" <++> pretty (getBinderLoc p env))
      _ => acc
  _ => acc

pshow : {vars : _} ->
        {auto c : Ref Ctxt Defs} ->
        {auto s : Ref Syn SyntaxInfo} ->
        Env Term vars -> Term vars -> Core (Doc IdrisAnn)
pshow env tm
    = do defs <- get Ctxt
         ntm <- normaliseHoles defs env tm
         itm <- resugar env ntm
         pure (pShowMN ntm env $ reAnnotate Syntax $ prettyTerm itm)

pshowNoNorm : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Env Term vars -> Term vars -> Core (Doc IdrisAnn)
pshowNoNorm env tm
    = do defs <- get Ctxt
         itm <- resugar env tm
         pure (pShowMN tm env $ reAnnotate Syntax $ prettyTerm itm)

ploc : {auto o : Ref ROpts REPLOpts} ->
       FC -> Core (Doc IdrisAnn)
ploc fc = do
    let Just (fn, s, e) = isNonEmptyFC fc
        | Nothing => pure emptyDoc
    let (sr, sc) = mapHom (fromInteger . cast) s
    let (er, ec) = mapHom (fromInteger . cast) e
    let nsize = length $ show (er + 1)
    let head = annotate FileCtxt (pretty fc)
    source <- (forget . lines) <$> getCurrentElabSource
    if sr == er
       then do
         let emph = spaces (cast $ nsize + sc + 4) <+> annotate Error (pretty (Extra.replicate (ec `minus` sc) '^'))
         let firstr = er `minus` 4
         pure $ vsep ([emptyDoc, head] ++ (addLineNumbers nsize firstr (pretty <$> extractRange firstr er source)) ++ [emph]) <+> line
       else pure $ vsep (emptyDoc :: head :: addLineNumbers nsize sr (pretty <$> extractRange sr (Prelude.min er (sr + 5)) source)) <+> line
  where
    extractRange : Nat -> Nat -> List String -> List String
    extractRange s e xs = take ((e `minus` s) + 1) (drop s xs)
    pad : Nat -> String -> String
    pad size s = Extra.replicate (size `minus` length s) '0' ++ s
    addLineNumbers : Nat -> Nat -> List (Doc IdrisAnn) -> List (Doc IdrisAnn)
    addLineNumbers size st xs =
      snd $ foldl (\(i, s), l => (S i, snoc s (space <+> annotate FileCtxt (pretty (pad size $ show $ i + 1) <++> pipe) <++> l))) (st, []) xs

-- Assumes the two FCs are sorted
ploc2 : {auto o : Ref ROpts REPLOpts} ->
        FC -> FC -> Core (Doc IdrisAnn)
ploc2 fc1 fc2 =
    do let Just (fn1, s1, e1) = isNonEmptyFC fc1
           | Nothing => ploc fc2
       let Just (fn2, s2, e2) = isNonEmptyFC fc2
           | Nothing => ploc fc1
       let (sr1, sc1) = mapHom (fromInteger . cast) s1
       let (sr2, sc2) = mapHom (fromInteger . cast) s2
       let (er1, ec1) = mapHom (fromInteger . cast) e1
       let (er2, ec2) = mapHom (fromInteger . cast) e2
       if (er2 > the Nat (er1 + 5))
          then pure $ !(ploc (MkFC fn1 s1 e1)) <+> line <+> !(ploc (MkFC fn2 s2 e2))
          else do let nsize = length $ show (er2 + 1)
                  let head = annotate FileCtxt (pretty $ MkFC fn1 s1 e2)
                  let firstRow = annotate FileCtxt (spaces (cast $ nsize + 2) <+> pipe)
                  source <- (forget . lines) <$> getCurrentElabSource
                  case (sr1 == er1, sr2 == er2, sr1 == sr2) of
                       (True, True, True) => do
                         let line = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr1)
                         let emph = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty (Extra.replicate (ec1 `minus` sc1) '^'))
                                      <+> spaces (cast $ sc2 `minus` ec1) <+> error (pretty (Extra.replicate (ec2 `minus` sc2) '^'))
                         pure $ vsep [emptyDoc, head, firstRow, fileCtxt (space <+> pretty (sr1 + 1)) <++> align (vsep [line, emph]), emptyDoc]
                       (True, True, False) => do
                         let line1 = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr1)
                         let emph1 = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty (Extra.replicate (ec1 `minus` sc1) '^'))
                         let line2 = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr2)
                         let emph2 = fileCtxt pipe <++> spaces (cast sc2) <+> error (pretty (Extra.replicate (ec2 `minus` sc2) '^'))
                         let numbered = if (sr2 `minus` er1) == 1
                                           then []
                                           else addLineNumbers nsize (sr1 + 1) (pretty <$> extractRange (sr1 + 1) er1 source)
                         pure $ vsep $ [emptyDoc, head, firstRow, fileCtxt (space <+> pretty (sr1 + 1)) <++> align (vsep [line1, emph1])]
                            ++ numbered
                            ++ [fileCtxt (space <+> pretty (sr2 + 1)) <++> align (vsep [line2, emph2]), emptyDoc]
                       (True, False, _) => do
                         let line = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr1)
                         let emph = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty (Extra.replicate (ec1 `minus` sc1) '^'))
                         pure $ vsep $ [emptyDoc, head, firstRow, fileCtxt (space <+> pretty (sr1 + 1)) <++> align (vsep [line, emph])]
                            ++ addLineNumbers nsize (sr1 + 1) (pretty <$> extractRange (sr1 + 1) (Prelude.max er1 er2) source)
                            ++ [emptyDoc]
                       (False, True, True) => do
                         let line = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr1)
                         let emph = fileCtxt pipe <++> spaces (cast sc1) <+> error (pretty (Extra.replicate (ec1 `minus` sc1) '^'))
                         pure $ vsep $ [emptyDoc, head, firstRow, fileCtxt (space <+> pretty (sr1 + 1)) <++> align (vsep [line, emph])]
                            ++ addLineNumbers nsize (sr1 + 1) (pretty <$> extractRange (sr1 + 1) (Prelude.max er1 er2) source)
                            ++ [emptyDoc]
                       (False, True, False) => do
                         let top = addLineNumbers nsize (sr1 + 1) (pretty <$> extractRange (sr1 + 1) er1 source)
                         let line = fileCtxt pipe <++> maybe emptyDoc pretty (elemAt source sr1)
                         let emph = fileCtxt pipe <++> spaces (cast sc2) <+> error (pretty (Extra.replicate (ec2 `minus` sc2) '^'))
                         pure $ vsep $ [emptyDoc, head, firstRow] ++ top ++ [fileCtxt (space <+> pretty (sr2 + 1)) <++> align (vsep [line, emph]), emptyDoc]
                       (_, _, _) => pure $ vsep (emptyDoc :: head :: addLineNumbers nsize sr1 (pretty <$> extractRange sr1 er2 source)) <+> line
  where
    extractRange : Nat -> Nat -> List String -> List String
    extractRange s e xs = take ((e `minus` s) + 1) (drop s xs)
    pad : Nat -> String -> String
    pad size s = Extra.replicate (size `minus` length s) '0' ++ s
    addLineNumbers : Nat -> Nat -> List (Doc IdrisAnn) -> List (Doc IdrisAnn)
    addLineNumbers size st xs =
      snd $ foldl (\(i, s), l => (S i, snoc s (space <+> annotate FileCtxt (pretty (pad size $ show $ i + 1) <++> pipe) <++> l))) (st, []) xs

export
pwarning : {auto c : Ref Ctxt Defs} ->
           {auto s : Ref Syn SyntaxInfo} ->
           {auto o : Ref ROpts REPLOpts} ->
           Warning -> Core (Doc IdrisAnn)
pwarning (ParserWarning fc msg)
    = pure $ pretty msg <+> line <+> !(ploc fc)
pwarning (UnreachableClause fc env tm)
    = pure $ errorDesc (reflow "Unreachable clause:"
        <++> code !(pshow env tm))
        <+> line <+> !(ploc fc)
pwarning (ShadowingGlobalDefs _ ns)
    = pure $ vcat
    $ reflow "We are about to implicitly bind the following lowercase names."
   :: reflow "You may be unintentionally shadowing the associated global definitions:"
   :: map (\ (n, ns) => indent 2 $ hsep $ pretty n
                            :: reflow "is shadowing"
                            :: punctuate comma (map pretty (forget ns)))
          (forget ns)

pwarning (Deprecated s)
    = pure $ pretty "Deprecation warning:" <++> pretty s
pwarning (GenericWarn s)
    = pure $ pretty s

export
perror : {auto c : Ref Ctxt Defs} ->
         {auto s : Ref Syn SyntaxInfo} ->
         {auto o : Ref ROpts REPLOpts} ->
         Error -> Core (Doc IdrisAnn)
perror (Fatal err) = perror err
perror (CantConvert fc gam env l r)
    = do defs <- get Ctxt
         setCtxt gam
         let res = errorDesc (hsep [ reflow "Mismatch between" <+> colon
                  , code !(pshow env l)
                  , "and"
                  , code !(pshow env r) <+> dot
                  ]) <+> line <+> !(ploc fc)
         put Ctxt defs
         pure res
perror (CantSolveEq fc gam env l r)
    = do defs <- get Ctxt
         setCtxt gam
         let res = errorDesc (hsep [ reflow "Can't solve constraint between" <+> colon
                      , code !(pshow env l)
                      , "and"
                      , code !(pshow env r) <+> dot
                      ]) <+> line <+> !(ploc fc)
         put Ctxt defs
         pure res
perror (PatternVariableUnifies fc env n tm)
    = do let (min, max) = order fc (getLoc tm)
         pure $ errorDesc (hsep [ reflow "Pattern variable"
                  , code (prettyVar n)
                  , reflow "unifies with" <+> colon
                  , code !(pshow env tm) <+> dot
                  ]) <+> line <+> !(ploc2 min max) <+> line
                     <+> reflow "Suggestion: Use the same name for both pattern variables, since they unify."
  where
    prettyVar : Name -> Doc IdrisAnn
    prettyVar (PV n _) = prettyVar n
    prettyVar n = pretty n
    order : FC -> FC -> (FC, FC)
    order fc1 fc2 =
      let Just (_, sr1, sc1) = isNonEmptyFC fc1
           | Nothing => (EmptyFC, fc2)
          Just (_, sr2, sc2) = isNonEmptyFC fc2
           | Nothing => (fc1, EmptyFC)
      in if sr1 < sr2 then (fc1, fc2) else if sr1 == sr2 && sc1 < sc2 then (fc1, fc2) else (fc2, fc1)
perror (CyclicMeta fc env n tm)
    = pure $ errorDesc (reflow "Cycle detected in solution of metavariable" <++> meta (pretty !(prettyName n)) <++> equals
        <++> code !(pshow env tm)) <+> line <+> !(ploc fc)
perror (WhenUnifying _ gam env x y err)
    = do defs <- get Ctxt
         setCtxt gam
         let res = errorDesc (reflow "When unifying:" <+> line
                   <+> "    " <+> code !(pshow env x) <+> line <+> "and:" <+> line
                   <+> "    " <+> code !(pshow env y)) <+> line <+> !(perror err)
         put Ctxt defs
         pure res
perror (ValidCase fc env (Left tm))
    = pure $ errorDesc (code !(pshow env tm) <++> reflow "is not a valid impossible case.")
        <+> line <+> !(ploc fc)
perror (ValidCase _ env (Right err))
    = pure $ errorDesc (reflow "Impossible pattern gives an error" <+> colon) <+> line <+> !(perror err)
perror (UndefinedName fc x)
    = pure $ errorDesc (reflow "Undefined name" <++> code (pretty x) <+> dot) <++> line <+> !(ploc fc)
perror (InvisibleName fc n (Just ns))
    = pure $ errorDesc ("Name" <++> code (pretty n) <++> reflow "is inaccessible since"
        <++> code (pretty ns) <++> reflow "is not explicitly imported.")
        <+> line <+> !(ploc fc)
        <+> line <+> reflow "Suggestion: add an explicit" <++> keyword "export" <++> "or" <++> keyword ("public" <++> "export")
        <++> reflow "modifier. By default, all names are" <++> keyword "private" <++> reflow "in namespace blocks."
perror (InvisibleName fc x Nothing)
    = pure $ errorDesc ("Name" <++> code (pretty x) <++> reflow "is private.") <+> line <+> !(ploc fc)
        <+> line <+> reflow "Suggestion: add an explicit" <++> keyword "export" <++> "or" <++> keyword ("public" <++> "export")
        <++> reflow "modifier. By default, all names are" <++> keyword "private" <++> reflow "in namespace blocks."
perror (BadTypeConType fc n)
    = pure $ errorDesc (reflow "Return type of" <++> code (pretty n) <++> reflow "must be" <++> code "Type"
        <+> dot) <+> line <+> !(ploc fc)
perror (BadDataConType fc n fam)
    = pure $ errorDesc (reflow "Return type of" <++> code (pretty n) <++> reflow "must be in"
        <++> code (pretty !(toFullNames fam))) <++> line <+> !(ploc fc)
perror (NotCovering fc n IsCovering)
    = pure $ errorDesc (reflow "Internal error" <++> parens (reflow "Coverage of" <++> code (pretty n)))
perror (NotCovering fc n (MissingCases cs))
    = pure $ errorDesc (code (pretty !(prettyName n)) <++> reflow "is not covering.")
        <+> line <+> !(ploc fc) <+> line
        <+> reflow "Missing cases" <+> colon <+> line
        <+> indent 4 (vsep !(traverse (pshow []) cs)) <+> line
perror (NotCovering fc n (NonCoveringCall ns))
    = pure $ errorDesc (pretty !(prettyName n) <++> reflow "is not covering.")
        <+> line <+> !(ploc fc) <+> line
        <+> reflow "Calls non covering function" <+>
        case ns of
             [fn] => space <+> pretty fn
             _ => pretty 's' <+> colon <++> concatWith (surround (comma <+> space)) (pretty <$> ns)
perror (NotTotal fc n r)
    = pure $ errorDesc (code (pretty !(prettyName n)) <++> reflow "is not total," <++> pretty r)
        <+> line <+> !(ploc fc)
perror (LinearUsed fc count n)
    = pure $ errorDesc (reflow "There are" <++> pretty count <++> reflow "uses of linear name"
        <++> code (pretty (sugarName n)) <+> dot)
        <++> line <+> !(ploc fc)
        <+> line <+> reflow "Suggestion: linearly bounded variables must be used exactly once."
perror (LinearMisuse fc n exp ctx)
    = if isErased exp
         then pure $ errorDesc (code (pretty n) <++> reflow "is not accessible in this context.")
                <+> line <+> !(ploc fc)
         else pure $ errorDesc (reflow "Trying to use" <++> prettyRig exp <++> "name"
                <++> code (pretty (sugarName n)) <++> "in" <++> prettyRel ctx <++> "context.")
                <+> line <+> !(ploc fc)
  where
    prettyRig : RigCount -> Doc ann
    prettyRig = elimSemi "irrelevant"
                         "linear"
                         (const "unrestricted")

    prettyRel : RigCount -> Doc ann
    prettyRel = elimSemi "irrelevant"
                         "relevant"
                         (const "non-linear")
perror (BorrowPartial fc env tm arg)
    = pure $ errorDesc (code !(pshow env tm) <++> reflow "borrows argument" <++> code !(pshow env arg)
        <++> reflow "so must be fully applied.")
        <+> line <+> !(ploc fc)
perror (BorrowPartialType fc env tm)
    = pure $ errorDesc (code !(pshow env tm) <++>
        reflow "borrows, so must return a concrete type.") <+> line <+> !(ploc fc)
perror (AmbiguousName fc ns)
    = pure $ errorDesc (reflow "Ambiguous name" <++> code (pretty ns))
        <+> line <+> !(ploc fc)
perror (AmbiguousElab fc env ts)
    = do pp <- getPPrint
         setPPrint (record { fullNamespace = True } pp)
         let res = vsep [ errorDesc (reflow "Ambiguous elaboration. Possible results" <+> colon)
                        , indent 4 (vsep !(traverse (pshow env) ts))
                        ] <+> line <+> !(ploc fc)
         setPPrint pp
         pure res
perror (AmbiguousSearch fc env tgt ts)
    = pure $ vsep [ errorDesc (reflow "Multiple solutions found in search of" <+> colon)
                  , indent 4 !(pshowNoNorm env tgt)
                  , !(ploc fc)
                  , reflow "Possible correct results" <+> colon
                  , indent 4 (vsep !(traverse (pshowNoNorm env) ts))
                  ]
perror (AmbiguityTooDeep fc n ns)
    = pure $ errorDesc (reflow "Maximum ambiguity depth exceeded in" <++> code (pretty !(getFullName n))
        <+> colon) <+> line <+> concatWith (surround (pretty " --> ")) (pretty <$> !(traverse getFullName ns))
        <++> line <+> !(ploc fc)
        <+> line <+> reflow "Suggestion: the default ambiguity depth limit is 3, the" <++> code "%ambiguity_depth"
        <++> reflow "pragma can be used to extend this limit, but beware compilation times can be severely impacted."
perror (AllFailed ts)
    = case allUndefined ts of
           Just e => perror e
           _ => pure $ errorDesc (reflow "Sorry, I can't find any elaboration which works. All errors" <+> colon) <+> line
                  <+> vsep !(traverse pAlterror ts)
  where
    pAlterror : (Maybe Name, Error) -> Core (Doc IdrisAnn)
    pAlterror (Just n, err)
       = pure $ "If" <++> code (pretty !(aliasName !(getFullName n))) <+> colon <++> !(perror err)
    pAlterror (Nothing, err)
       = pure $ reflow "Possible error" <+> colon <+> line <+> indent 4 !(perror err)

    allUndefined : List (Maybe Name, Error) -> Maybe Error
    allUndefined [] = Nothing
    allUndefined [(_, err@(UndefinedName _ _))] = Just err
    allUndefined ((_, err@(UndefinedName _ _)) :: es) = allUndefined es
    allUndefined _ = Nothing
perror (RecordTypeNeeded fc _)
    = pure $ errorDesc (reflow "Can't infer type for this record update.") <+> line <+> !(ploc fc)
perror (NotRecordField fc fld Nothing)
    = pure $ errorDesc (code (pretty fld) <++> reflow "is not part of a record type.") <+> line <+> !(ploc fc)
perror (NotRecordField fc fld (Just ty))
    = pure $ errorDesc (reflow "Record type" <++> code (pretty !(getFullName ty)) <++> reflow "has no field"
        <++> code (pretty fld) <+> dot) <+> line <+> !(ploc fc)
perror (NotRecordType fc ty)
    = pure $ errorDesc (code (pretty !(getFullName ty)) <++> reflow "is not a record type.") <+> line <+> !(ploc fc)
perror (IncompatibleFieldUpdate fc flds)
    = pure $ reflow "Field update" <++> concatWith (surround (pretty "->")) (pretty <$> flds)
             <++> reflow "not compatible with other updates at" <+> colon <+> line <+> !(ploc fc)
perror (InvalidArgs fc env [n] tm)
    = pure $ errorDesc (code (pretty n) <++> reflow "is not a valid argument in" <++> !(pshow env tm)
        <+> dot) <+> line <+> !(ploc fc)
perror (InvalidArgs fc env ns tm)
    = pure $ errorDesc (concatWith (surround (comma <+> space)) (code . pretty <$> ns)
        <++> reflow "are not valid arguments in" <++> !(pshow env tm) <+> dot)
        <+> line <+> !(ploc fc)
perror (TryWithImplicits fc env imps)
    = pure $ errorDesc (reflow "Need to bind implicits"
        <++> concatWith (surround (comma <+> space)) !(traverse (tshow env) imps) <+> dot)
        <+> line <+> !(ploc fc)
  where
    tshow : {vars : _} ->
            Env Term vars -> (Name, Term vars) -> Core (Doc IdrisAnn)
    tshow env (n, ty) = pure $ pretty n <++> colon <++> code !(pshow env ty)
perror (BadUnboundImplicit fc env n ty)
    = pure $ errorDesc (reflow "Can't bind name" <++> code (pretty (nameRoot n)) <++> reflow "with type" <++> code !(pshow env ty)
        <+> colon) <+> line <+> !(ploc fc) <+> line <+> reflow "Suggestion: try an explicit bind."
perror (CantSolveGoal fc gam env g reason)
    = do defs <- get Ctxt
         setCtxt gam
         let (_ ** (env', g')) = dropEnv env g
         let res = errorDesc (reflow "Can't find an implementation for" <++> code !(pshow env' g')
                     <+> dot) <+> line <+> !(ploc fc)
         put Ctxt defs
         case reason of
              Nothing => pure res
              Just r => do rdesc <- perror r
                           pure (res <+> line <+>
                                 (reflow "Possible cause:" <++> rdesc))
  where
    -- For display, we don't want to see the full top level type; just the
    -- return type
    dropEnv : {vars : _} ->
              Env Term vars -> Term vars ->
              (ns ** (Env Term ns, Term ns))
    dropEnv env (Bind _ n b@(Pi _ _ _ _) sc) = dropEnv (b :: env) sc
    dropEnv env (Bind _ n b@(Let _ _ _ _) sc) = dropEnv (b :: env) sc
    dropEnv env tm = (_ ** (env, tm))

perror (DeterminingArg fc n i env g)
    = pure $ errorDesc (reflow "Can't find an implementation for" <++> code !(pshow env g) <+> line
        <+> reflow "since I can't infer a value for argument" <++> code (pretty n) <+> dot)
        <+> line <+> !(ploc fc)
perror (UnsolvedHoles hs)
    = pure $ errorDesc (reflow "Unsolved holes" <+> colon) <+> line <+> !(prettyHoles hs)
  where
    prettyHoles : List (FC, Name) -> Core (Doc IdrisAnn)
    prettyHoles [] = pure emptyDoc
    prettyHoles ((fc, n) :: hs)
        = pure $ meta (pretty n) <++> reflow "introduced at:" <++> !(ploc fc) <+> !(prettyHoles hs)
perror (CantInferArgType fc env n h ty)
    = pure $ errorDesc (reflow "Can't infer type for argument" <++> code (pretty n)) <+> line
        <+> "Got" <++> code !(pshow env ty) <++> reflow "with hole" <++> meta (pretty h) <+> dot
        <+> line <+> !(ploc fc)
perror (SolvedNamedHole fc env h tm)
    = pure $ errorDesc (reflow "Named hole" <++> meta (pretty h) <++> reflow "has been solved by unification.") <+> line
        <+> "Result" <+> colon <++> code !(pshow env tm)
        <+> line <+> !(ploc fc)
perror (VisibilityError fc vx x vy y)
    = pure $ errorDesc (keyword (pretty vx) <++> code (pretty (sugarName !(toFullNames x)))
        <++> reflow "cannot refer to" <++> keyword (pretty vy) <++> code (pretty (sugarName !(toFullNames y))))
        <+> line <+> !(ploc fc)
perror (NonLinearPattern fc n)
    = pure $ errorDesc (reflow "Non linear pattern" <++> code (pretty (sugarName n)) <+> dot) <+> line <+> !(ploc fc)
perror (BadPattern fc n)
    = pure $ errorDesc (reflow "Pattern not allowed here" <+> colon <++> code (pretty n) <+> dot) <+> line <+> !(ploc fc)
perror (NoDeclaration fc n)
    = pure $ errorDesc (reflow "No type declaration for" <++> code (pretty n) <+> dot) <+> line <+> !(ploc fc)
perror (AlreadyDefined fc n)
    = pure $ errorDesc (code (pretty n) <++> reflow "is already defined.") <+> line <+> !(ploc fc)
perror (NotFunctionType fc env tm)
    = pure $ errorDesc (code !(pshow env tm) <++> reflow "is not a function type.") <+> line <+> !(ploc fc)
perror (RewriteNoChange fc env rule ty)
    = pure $ errorDesc (reflow "Rewriting by" <++> code !(pshow env rule)
        <++> reflow "did not change type" <++> code !(pshow env ty) <+> dot)
        <+> line <+> !(ploc fc)
perror (NotRewriteRule fc env rule)
    = pure $ errorDesc (code !(pshow env rule) <++> reflow "is not a rewrite rule type.") <+> line <+> !(ploc fc)
perror (CaseCompile fc n DifferingArgNumbers)
    = pure $ errorDesc (reflow "Patterns for" <++> code (pretty !(prettyName n)) <++> reflow "have differing numbers of arguments.")
        <+> line <+> !(ploc fc)
perror (CaseCompile fc n DifferingTypes)
    = pure $ errorDesc (reflow "Patterns for" <++> code (pretty !(prettyName n)) <++> reflow "require matching on different types.")
        <+> line <+> !(ploc fc)
perror (CaseCompile fc n UnknownType)
    = pure $ errorDesc (reflow "Can't infer type to match in" <++> code (pretty !(prettyName n)) <+> dot)
        <+> line <+> !(ploc fc)
perror (CaseCompile fc n (NotFullyApplied cn))
    = pure $ errorDesc (pretty "Constructor" <++> code (pretty !(toFullNames cn)) <++> reflow "is not fully applied.")
         <+> line <+> !(ploc fc)
perror (CaseCompile fc n (MatchErased (_ ** (env, tm))))
    = pure $ errorDesc (reflow "Attempt to match on erased argument" <++> code !(pshow env tm) <++> pretty "in"
        <++> code (pretty !(prettyName n)) <+> dot) <+> line <+> !(ploc fc)
perror (BadDotPattern fc env reason x y)
    = pure $ errorDesc (reflow "Can't match on" <++> code !(pshow env x)
        <++> parens (pretty reason) <+> dot) <+> line <+> !(ploc fc)
perror (MatchTooSpecific fc env tm)
    = pure $ errorDesc (reflow "Can't match on" <++> code !(pshow env tm)
        <++> reflow "as it must have a polymorphic type.") <+> line <+> !(ploc fc)
perror (BadImplicit fc str)
    = pure $ errorDesc (reflow "Can't infer type for unbound implicit name" <++> code (pretty str) <+> dot)
        <+> line <+> !(ploc fc) <+> line <+> reflow "Suggestion: try making it a bound implicit."
perror (BadRunElab fc env script desc)
    = pure $ errorDesc (reflow "Bad elaborator script" <++> code !(pshow env script) <++> parens (pretty desc) <+> dot)
        <+> line <+> !(ploc fc)
perror (GenericMsg fc str) = pure $ pretty str <+> line <+> !(ploc fc)
perror (TTCError msg)
    = pure $ errorDesc (reflow "Error in TTC file" <+> colon <++> pretty (show msg))
        <++> parens (pretty "the most likely case is that the ./build directory in your current project contains files from a previous build of idris2 or the idris2 executable is from a different build than the installed .ttc files")
perror (FileErr fname err)
    = pure $ errorDesc (reflow "File error in" <++> pretty fname <++> colon) <++> pretty (show err)
perror (CantFindPackage fname)
    = pure $ errorDesc (reflow "Can't find package " <++> pretty fname)
perror (LitFail fc)
    = pure $ errorDesc (reflow "Can't parse literate.") <+> line <+> !(ploc fc)
perror (LexFail fc msg)
    = pure $ errorDesc (pretty msg) <+> line <+> !(ploc fc)
perror (ParseFail ((fc, msg) ::: Nil))
    = pure $ errorDesc (pretty msg) <+> line <+> !(ploc fc)
perror (ParseFail errs)
    = pure $ errorDesc (reflow "Couldn't parse any alternatives" <+> colon) <+> line <+> !listErrors
  where
    prettyErrors : Nat -> Nat -> List (FC, String) -> Core (Doc IdrisAnn)
    prettyErrors showCount _ []   = pure emptyDoc
    prettyErrors showCount 0 errs = pure $ meta (pretty "... (\{show $ length errs} others)")
    prettyErrors showCount (S k) ((fc, msg) :: hs)
        = do let idx = show $ showCount `minus` k
             pure $ warning (pretty "\{idx}: \{msg}") <+> line <+> !(ploc fc) <+> !(prettyErrors showCount k hs)

    listErrors : Core (Doc IdrisAnn)
    listErrors = do showCount <- logErrorCount . session . options <$> get Ctxt
                    prettyErrors showCount showCount . nub . reverse $ forget errs
perror (ModuleNotFound fc ns)
    = pure $ errorDesc ("Module" <++> annotate FileCtxt (pretty ns) <++> reflow "not found") <+> line <+> !(ploc fc)
perror (CyclicImports ns)
    = pure $ errorDesc (reflow "Module imports form a cycle" <+> colon) <++> concatWith (surround (pretty " -> ")) (pretty <$> ns)
perror ForceNeeded = pure $ errorDesc (reflow "Internal error when resolving implicit laziness")
perror (InternalError str) = pure $ errorDesc (reflow "INTERNAL ERROR" <+> colon) <++> pretty str
perror (UserError str) = pure $ errorDesc (pretty "Error" <+> colon) <++> pretty str
perror (NoForeignCC fc specs) = do
    let cgs = fst <$> availableCGs (options !(get Ctxt))
    let res = vsep [ errorDesc (reflow ("The given specifier '" ++ show specs ++ "' was not accepted by any backend. Available backends") <+> colon)
                   , indent 2 (concatWith (\ x, y => x <+> ", " <+> y) (map reflow cgs))
                   , reflow "Some backends have additional specifier rules, refer to their documentation."
                   ] <+> line <+> !(ploc fc)
    pure res
perror (BadMultiline fc str) = pure $ errorDesc (reflow "While processing multi-line string" <+> dot <++> pretty str <+> dot) <+> line <+> !(ploc fc)
perror (Timeout str) = pure $ errorDesc (reflow "Timeout in" <++> pretty str)

perror (InType fc n err)
    = pure $ hsep [ errorDesc (reflow "While processing type of" <++> code (pretty !(prettyName n))) <+> dot
                  , !(perror err)
                  ]
perror (InCon fc n err)
    = pure $ hsep [ errorDesc (reflow "While processing constructor" <++> code (pretty !(prettyName n))) <+> dot
                  , !(perror err)
                  ]
perror (InLHS fc n err)
    = pure $ hsep [ errorDesc (reflow "While processing left hand side of" <++> code (pretty !(prettyName n))) <+> dot
                  , !(perror err)
                  ]
perror (InRHS fc n err)
    = pure $ hsep [ errorDesc (reflow "While processing right hand side of" <++> code (pretty !(prettyName n))) <+> dot
                  , !(perror err)
                  ]

perror (MaybeMisspelling err ns) = pure $ !(perror err) <+> case ns of
  (n ::: []) => reflow "Did you mean:" <++> pretty n <+> "?"
  _ => let (xs, x) = Lib.unsnoc ns in
       reflow "Did you mean any of:"
       <++> concatWith (surround (comma <+> space)) (map pretty xs)
       <+> comma <++> reflow "or" <++> pretty x <+> "?"
perror (WarningAsError warn) = pwarning warn

prettyMaybeLoc : Maybe FC -> Doc IdrisAnn
prettyMaybeLoc Nothing = emptyDoc
prettyMaybeLoc (Just fc) = annotate FileCtxt (pretty fc) <+> colon

export
display : {auto c : Ref Ctxt Defs} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto o : Ref ROpts REPLOpts} ->
          Error -> Core (Doc IdrisAnn)
display err = do
  pure $ annotate Error (pretty "Error:") <++> !(perror err)

export
displayWarning : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 {auto o : Ref ROpts REPLOpts} ->
                 Warning -> Core (Doc IdrisAnn)
displayWarning w
    = pure $ annotate Warning (pretty "Warning:") <++> !(pwarning w)


text:
module YinYang

import Control.Monad.Trans
import src.ContT

data Rec : (r : Type) -> (m : Type -> Type) -> Type where
  RecK : (Rec r m -> ContT r m (Rec r m)) -> Rec r m

yin : ContT r IO (Rec r IO)
yin = do k <- callCC (\k => pure (RecK k))
         lift (putStrLn "")
         pure k

yang : ContT r IO (Rec r IO)
yang = do k <- callCC (\k => pure (RecK k))
          lift (putStr "*")
          pure k

yinyang : ContT r IO (Rec r IO)
yinyang = do (RecK k) <- yin
             k' <- yang
             k k'

test : IO ()
test = run (\_ => pure ()) yinyang

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Parser

import Lightyear
import Control.Monad.Identity
import Lexer as L
import Syntax

public export
Parser : Type -> Type
Parser = ParserT (List Lexeme) Identity

implementation Stream Lexeme (List Lexeme) where
  uncons []        = Nothing
  uncons (x :: xs) = Just (x, xs)

E : Type
E = Expression

chainl1 : Parser a -> Parser (a -> a -> a) -> Parser a
chainl1 p op = p >>= rest
  where rest a1 = (do f <- op
                      a2 <- p
                      rest (f a1 a2)) <|> pure a1

chainl : Parser a -> Parser (a -> a -> a) -> a -> Parser a
chainl p op a = (p `Parser.chainl1` op) <|> pure a

infixOp : L.Lexeme -> (E -> E -> E) -> Parser (E -> E -> E)
infixOp l ctor = do
  _ <- satisfy (== l)
  pure ctor

addOp : Parser (Expression -> Expression -> Expression)
addOp = infixOp L.Plus Plus <|> infixOp L.Minus Minus

mulOp : Parser (Expression -> Expression -> Expression)
mulOp = infixOp L.Times Times <|> infixOp L.Divide Divide

isNumeral : L.Lexeme -> Bool
isNumeral (L.Numeral n) = True
isNumeral _             = False

minus : Parser L.Lexeme
minus = satisfy (== L.Minus)

lparen : Parser L.Lexeme
lparen = satisfy (== L.LParen)

rparen : Parser L.Lexeme
rparen = satisfy (== L.RParen)

mutual
  expression : Parser Expression
  expression = term `Parser.chainl1` addOp

  term : Parser Expression
  term = factor `Parser.chainl1` mulOp

  numeral : Parser Expression
  numeral = do
    (L.Numeral n) <- satisfy isNumeral
    pure (Numeral n)

  negate : Parser Expression
  negate = do
    _ <- minus
    f <- factor
    pure $ Negate f

  subExp : Parser Expression
  subExp = do
    _ <- lparen
    expr <- expression
    _ <- rparen
    pure expr

  factor : Parser Expression
  factor = numeral
       <|> subExp
       <|> negate

export
toplevel : Parser Expression
toplevel = expression

max_stars_repo_name: steshaw/idris-calc

max_issues_repo_name: steshaw/idris-calc

max_forks_repo_name: steshaw/idris-calc


text:
module Compiler.Erlang.Codegen.ErlExprToAbstractFormat.Buffer

import Compiler.Erlang.IR.AbstractFormat
import Compiler.Erlang.Codegen.ErlExprToAbstractFormat.Internal
import Compiler.Erlang.Codegen.ErlExprToAbstractFormat.Binary

%default total

export
new : Line -> (size : Expr) -> Expr
new l size =
  AETuple l [Binary.empty l, size]

export
resize : Line -> (buf : Expr) -> (newSize : Expr) -> Expr
resize l buf newSize =
  let extendedBody =
        singleton $ AETuple l [AEVar l "Bin", AEVar l "NewSize"]
      shrinkedBinary = genFunCall l "binary" "part" [AEVar l "Bin", AELiteral (ALInteger l 0), AEVar l "NewSize"]
      shrinkedBody =
        singleton $ AETuple l [shrinkedBinary, AEVar l "NewSize"]
      funExpr = AEFun l 2
        ( MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "NewSize"]
            [MkGuardAlt (singleton $ AGOp l "=<" (AGFunCall l "byte_size" [AGVar l "Bin"]) (AGVar l "NewSize"))]
            extendedBody :::
          [ MkFunClause l
              [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "NewSize"]
              []
              shrinkedBody
          ]
        )
  in AEFunCall l funExpr [buf, newSize]

export
flatten : Line -> (buf : Expr) -> (maxbytes : Expr) -> Expr
flatten l buf maxbytes =
  let paddingSize = AEOp l "-" (AEVar l "MaxBytes") (genFunCall l "erlang" "byte_size" [AEVar l "Bin"])
      paddedBinaryValue = AEBitstring l
        [ MkBitSegment l (AEVar l "Bin")     ABSDefault ABBinary
        , MkBitSegment l (AEVar l "Padding") ABSDefault ABBinary
        ]
      extendedBody =
        ( AEMatch l (APVar l "Padding") (Binary.zeroPadded l paddingSize) :::
          [ AETuple l [paddedBinaryValue, AEVar l "BufSize"]
          ]
        )
      shrinkedBinary = genFunCall l "binary" "part" [AEVar l "Bin", AELiteral (ALInteger l 0), AEVar l "BufSize"]
      shrinkedBody =
        singleton $ AETuple l [shrinkedBinary, AEVar l "BufSize"]
      funExpr = AEFun l 2
        ( MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "MaxBytes"]
            [MkGuardAlt (singleton $ AGOp l "=<" (AGFunCall l "byte_size" [AGVar l "Bin"]) (AGVar l "MaxBytes"))]
            extendedBody :::
          [ MkFunClause l
              [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "MaxBytes"]
              []
              shrinkedBody
          ]
        )
  in AEFunCall l funExpr [buf, maxbytes]

-- Similar to the following Erlang code:
-- ```
-- buffer_set_byte(Bin, Loc, Value) when byte_size(Bin) =< Loc ->
--   Padding = binary:copy(<<0>>, Loc - byte_size(Bin)),
--   <<Bin/binary, Padding/binary, Value:8/integer>>;
-- buffer_set_byte(Bin, Loc, Value) ->
--   Padding = binary:copy(<<0>>, 1),
--   <<Start:Loc/binary, _:8/integer, End/binary>> = <<Bin/binary, Padding/binary>>,
--   <<Start/binary, Value:8/integer, End/binary>>.
-- ```
setGeneric : (targetTSL : TypeSpecifierList) -> (targetSize : Int) -> Line -> (buf : Expr) -> (loc : Expr) -> (value : Expr) -> Expr
setGeneric targetTSL targetSize l buf loc value =
  let binaryWithExtraPadding = AEBitstring l
        [ MkBitSegment l (AEVar l "Bin")     ABSDefault ABBinary
        , MkBitSegment l (AEVar l "Padding") ABSDefault ABBinary
        ]
      mutatedBinaryPattern = APBitstring l
        [ MkBitSegment l (ABPVar l "Start") (ABSVar l "Loc")                 ABBinary
        , MkBitSegment l (ABPUniversal l)   (ABSInteger l (cast targetSize)) targetTSL
        , MkBitSegment l (ABPVar l "End")   ABSDefault                       ABBinary
        ]
      mutatedBinaryValue = AEBitstring l
        [ MkBitSegment l (AEVar l "Start") ABSDefault                       ABBinary
        , MkBitSegment l (AEVar l "Value") (ABSInteger l (cast targetSize)) targetTSL
        , MkBitSegment l (AEVar l "End")   ABSDefault                       ABBinary
        ]
      targetSizeInBytes = AEOp l "div" (AELiteral (ALInteger l (cast targetSize))) (AELiteral (ALInteger l 8))
      mutatedBody =
        ( AEMatch l (APVar l "Padding") (Binary.zeroPadded l targetSizeInBytes) :::
          [ AEMatch l mutatedBinaryPattern binaryWithExtraPadding
          , AETuple l [mutatedBinaryValue, AEVar l "BufSize"]
          ]
        )
      paddingSize = AEOp l "-" (AEVar l "Loc") (genFunCall l "erlang" "byte_size" [AEVar l "Bin"])
      extendedBinaryValue =
        AEBitstring l
          [ MkBitSegment l (AEVar l "Bin")     ABSDefault ABBinary
          , MkBitSegment l (AEVar l "Padding") ABSDefault ABBinary
          , MkBitSegment l (AEVar l "Value")   (ABSInteger l (cast targetSize)) targetTSL
          ]
      extendedBody =
        ( AEMatch l (APVar l "Padding") (Binary.zeroPadded l paddingSize) :::
          [ AETuple l [extendedBinaryValue, AEVar l "BufSize"]
          ]
        )
      funExpr = AEFun l 3
        ( MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Value"]
            [MkGuardAlt (singleton $ AGOp l "=<" (AGFunCall l "byte_size" [AGVar l "Bin"]) (AGVar l "Loc"))]
            extendedBody :::
          [ MkFunClause l
              [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Value"]
              []
              mutatedBody
          ]
        )
  in AEFunCall l funExpr [buf, loc, value]

-- Similar to the following Erlang code:
-- ```
-- buffer_get_byte(Bin, Loc) when Loc + 1 =< byte_size(Bin) ->
--   <<_Start:Loc/binary, Value:8/integer, _End/binary>> = Bin,
--   Value.
-- buffer_get_byte(Bin, Loc) ->
--   0.
-- ```
getGeneric : (targetTSL : TypeSpecifierList) -> (targetSize : Int) -> (defaultValue : Expr) -> Line -> (buf : Expr) -> (loc : Expr) -> Expr
getGeneric targetTSL targetSize defaultValue l buf loc =
  let binaryPattern = APBitstring l
        [ MkBitSegment l (ABPUniversal l)   (ABSVar l "Loc")                 ABBinary
        , MkBitSegment l (ABPVar l "Value") (ABSInteger l (cast targetSize)) targetTSL
        , MkBitSegment l (ABPUniversal l)   ABSDefault                       ABBinary
        ]
      body =
        ( AEMatch l binaryPattern (AEVar l "Bin") :::
          [ AEVar l "Value"
          ]
        )
      targetSizeInBytes = AGOp l "div" (AGLiteral (ALInteger l (cast targetSize))) (AGLiteral (ALInteger l 8))
      funExpr = AEFun l 2
        ( MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc"]
            [MkGuardAlt (singleton $ AGOp l "=<" (AGOp l "+" (AGVar l "Loc") targetSizeInBytes) (AGFunCall l "byte_size" [AGVar l "Bin"]))]
            body :::
          [ MkFunClause l
              [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc"]
              []
              (singleton defaultValue)
          ]
        )
  in AEFunCall l funExpr [buf, loc]

export
setUnsignedInt : (size : Int) -> Line -> (buf : Expr) -> (loc : Expr) -> (value : Expr) -> Expr
setUnsignedInt = setGeneric (ABInteger {signedness=ABUnsigned, endianness=ABNative})

export
getUnsignedInt : (size : Int) -> Line -> (buf : Expr) -> (loc : Expr) -> Expr
getUnsignedInt size l = getGeneric (ABInteger {signedness=ABUnsigned, endianness=ABNative}) size (AELiteral (ALInteger l 0)) l

export
setSignedInt : (size : Int) -> Line -> (buf : Expr) -> (loc : Expr) -> (value : Expr) -> Expr
setSignedInt = setGeneric (ABInteger {signedness=ABSigned, endianness=ABNative})

export
getSignedInt : (size : Int) -> Line -> (buf : Expr) -> (loc : Expr) -> Expr
getSignedInt size l = getGeneric (ABInteger {signedness=ABSigned, endianness=ABNative}) size (AELiteral (ALInteger l 0)) l

export
setDouble : Line -> (buf : Expr) -> (loc : Expr) -> (value : Expr) -> Expr
setDouble = setGeneric (ABFloat {endianness=ABNative}) 64

export
getDouble : Line -> (buf : Expr) -> (loc : Expr) -> Expr
getDouble l = getGeneric (ABFloat {endianness=ABNative}) 64 (AELiteral (ALFloat l 0)) l

-- Similar to the following Erlang code:
-- ```
-- buffer_set_string(Bin, Loc, Value) when byte_size(Bin) =< Loc ->
--   Padding = binary:copy(<<0>>, Loc - byte_size(Bin)),
--   <<Bin/binary, Padding/binary, Value/binary>>;
-- buffer_set_string(Bin, Loc, Value) ->
--   Size = erlang:byte_size(Value),
--   Padding = binary:copy(<<0>>, Size),
--   <<Start:Loc/binary, _:Size/binary, End/binary>> = <<Bin/binary, Padding/binary>>,
--   <<Start/binary, Value/binary, End/binary>>.
-- ```
export
setString : Line -> (buf : Expr) -> (loc : Expr) -> (value : Expr) -> Expr
setString l buf loc value =
  let binaryWithExtraPadding = AEBitstring l
        [ MkBitSegment l (AEVar l "Bin")     ABSDefault ABBinary
        , MkBitSegment l (AEVar l "Padding") ABSDefault ABBinary
        ]
      mutatedBinaryPattern = APBitstring l
        [ MkBitSegment l (ABPVar l "Start") (ABSVar l "Loc")  ABBinary
        , MkBitSegment l (ABPUniversal l)   (ABSVar l "Size") ABBinary
        , MkBitSegment l (ABPVar l "End")   ABSDefault        ABBinary
        ]
      mutatedBinaryValue = AEBitstring l
        [ MkBitSegment l (AEVar l "Start") ABSDefault ABBinary
        , MkBitSegment l (AEVar l "Value") ABSDefault ABBinary
        , MkBitSegment l (AEVar l "End")   ABSDefault ABBinary
        ]
      mutatedBody =
        ( AEMatch l (APVar l "Size") (genFunCall l "erlang" "byte_size" [AEVar l "Value"]) :::
          [ AEMatch l (APVar l "Padding") (Binary.zeroPadded l (AEVar l "Size"))
          , AEMatch l mutatedBinaryPattern binaryWithExtraPadding
          , AETuple l [mutatedBinaryValue, AEVar l "BufSize"]
          ]
        )
      paddingSize = AEOp l "-" (AEVar l "Loc") (genFunCall l "erlang" "byte_size" [AEVar l "Bin"])
      extendedBinaryValue =
        AEBitstring l
          [ MkBitSegment l (AEVar l "Bin")     ABSDefault ABBinary
          , MkBitSegment l (AEVar l "Padding") ABSDefault ABBinary
          , MkBitSegment l (AEVar l "Value")   ABSDefault ABBinary
          ]
      extendedBody =
        ( AEMatch l (APVar l "Padding") (Binary.zeroPadded l paddingSize) :::
          [ AETuple l [extendedBinaryValue, AEVar l "BufSize"]
          ]
        )
      funExpr = AEFun l 3
        ( MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Value"]
            [MkGuardAlt (singleton $ AGOp l "=<" (AGFunCall l "byte_size" [AGVar l "Bin"]) (AGVar l "Loc"))]
            extendedBody :::
          [ MkFunClause l
              [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Value"]
              []
              mutatedBody
          ]
        )
  in AEFunCall l funExpr [buf, loc, value]

-- Similar to the following Erlang code:
-- ```
-- buffer_get_string(Bin, Loc, Len) when Loc + Len =< byte_size(Bin) ->
--   <<_Start:Loc/binary, Value:Len/binary, _End/binary>> = Bin,
--   Value.
-- buffer_get_string(Bin, Loc, Len) ->
--   binary:copy(<<0>>, Len).
-- ```
export
getString : Line -> (buf : Expr) -> (loc : Expr) -> (len : Expr) -> Expr
getString l buf loc len =
  let binaryPattern = APBitstring l
        [ MkBitSegment l (ABPUniversal l)   (ABSVar l "Loc") ABBinary
        , MkBitSegment l (ABPVar l "Value") (ABSVar l "Len") ABBinary
        , MkBitSegment l (ABPUniversal l)   ABSDefault       ABBinary
        ]
      body =
        ( AEMatch l binaryPattern (AEVar l "Bin") :::
          [ AEVar l "Value"
          ]
        )
      defaultBody =
        singleton $ Binary.zeroPadded l (AEVar l "Len")
      funExpr = AEFun l 3
        ( MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Len"]
            [MkGuardAlt (singleton $ AGOp l "=<" (AGOp l "+" (AGVar l "Loc") (AGVar l "Len")) (AGFunCall l "byte_size" [AGVar l "Bin"]))]
            body :::
          [ MkFunClause l
              [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Len"]
              []
              defaultBody
          ]
        )
  in AEFunCall l funExpr [buf, loc, len]


text:
module RecordUpdate

record Attributes where
  font : String
  size : Nat

bigMono : Attributes -> Attributes
bigMono = { font $= (++ "Mono")
          , size := 20
          }

smallMono : Attributes -> Attributes
smallMono = { size := 5 } . bigMono

-- Works for nested too
record Text where
  attributes : Attributes
  content : String

setArial10 : Text -> Text
setArial10 = { attributes->font := "Arial"
             , attributes.size := 10
             }


text:
module Foo

hi : IO String
hi = pure "Hi!"


text:
module Circuits.Idealised.AST

import Toolkit.Data.Location

import Ref
import Circuits.Idealised.Types

%default total

public export
data End = F | L

public export
data AST = Var Ref
         | Input FileContext Direction DType Ref AST
         | Wire FileContext DType Ref Ref AST
         | Seq AST AST
         | Mux FileContext AST AST AST AST
         | Dup FileContext AST AST AST
         | Not FileContext AST AST
         | Gate FileContext GateKind AST AST AST
         | Stop FileContext
         | IndexS FileContext AST AST
         | IndexE FileContext End AST AST AST
         | IndexP FileContext Nat AST AST AST AST
         | MergeS FileContext AST AST
         | MergeV FileContext AST AST AST

export
setSource : String -> AST -> AST
setSource new (Var x)
  = Var ({span $= setSource new} x)

setSource new (Input x y z w v)
  = (Input (setSource new x)
           y
           z
           (setSource new w)
           (setSource new v))

setSource new (Wire x y z w v)
  = (Wire (setSource new x)
          y
          (setSource new z)
          (setSource new w)
          (setSource new v))

setSource new (Seq x y)
  = Seq (setSource new x)
        (setSource new y)

setSource new (Mux x y z w v)
  = (Mux (setSource new x)
         (setSource new y)
         (setSource new z)
         (setSource new w)
         (setSource new v))

setSource new (Dup x y z w)
  = (Dup (setSource new x)
         (setSource new y)
         (setSource new z)
         (setSource new w))

setSource new (Not x y z)
  = (Not (setSource new x)
         (setSource new y)
         (setSource new z))

setSource new (Gate x y z w v)
  = (Gate (setSource new x)
          y
          (setSource new z)
          (setSource new w)
          (setSource new v))

setSource new (Stop x)
  = (Stop (setSource new x))

setSource new (IndexS x y z)
  = (IndexS (setSource new x)
            (setSource new y)
            (setSource new z))

setSource new (IndexE x y z w v)
  = (IndexE (setSource new x)
            y
            (setSource new z)
            (setSource new w)
            (setSource new v))

setSource new (IndexP x k y z w v)
  = (IndexP (setSource new x)
            k
            (setSource new y)
            (setSource new z)
            (setSource new w)
            (setSource new v))

setSource new (MergeS fc o i)
  = MergeS (setSource new fc)
           (setSource new o)
           (setSource new i)

setSource new (MergeV fc o a b)
  = MergeV (setSource new fc)
           (setSource new o)
           (setSource new a)
           (setSource new b)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Main

import Average
import Data.Vect

data Format = Number Format
  | Str Format
  | Lit String Format
  | End

PrintfType : Format -> Type
PrintfType (Number x) = (i: Int) -> PrintfType x
PrintfType (Str x) = (s: String) -> PrintfType x
PrintfType (Lit x y) = PrintfType y
PrintfType End = String

printfFmt : (fmt: Format) -> (acc: String) -> PrintfType fmt
printfFmt (Number x) acc = \i => printfFmt x (acc ++ show i)
printfFmt (Str x) acc = \s => printfFmt x (acc ++ s)
printfFmt (Lit x y) acc = printfFmt y (acc ++ x)
printfFmt End acc = acc

TupleVect : (n: Nat) -> Type -> Type
TupleVect Z _ = ()
TupleVect (S k) t = (Nat, TupleVect k t)

test: TupleVect 4 Nat
test = (1, 2, 3, 4, ())

-- C-c C-t - Type-check name
-- C-c C-s - Add clause (add definition)
-- C-c C-d - Documentation
-- C-c C-l - List holes
-- C-c C-a Seach expressions
-- case-split

showAve : (str1 : String) -> String
showAve str = (show "test")

data DataStore : Type where
  MkData : (size: Nat) -> (items: Vect size String) -> DataStore

size: DataStore -> Nat
size (MkData s i) = s

items: (store: DataStore) -> Vect (size store) String
items (MkData size items) = items

addToStore : DataStore -> String -> DataStore
addToStore (MkData size items) newitem = MkData _ (addToData items) where
  addToData : Vect old String -> Vect (S old) String
  addToData [] = [newitem]
  addToData (x :: xs) = x :: addToData xs

data Command = Add String
  | Get Integer
  | Quit

parseCommand : String -> String -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" val = case all isDigit (unpack val) of
  False => Nothing
  True => Just (Get (cast val))
parseCommand "quit" _ = Just Quit
parseCommand _ _ = Just Quit

parse : (input : String) -> Maybe Command
parse input = case (Prelude.Strings.span (/= ' ') input) of
  (cmd, args) => parseCommand cmd (ltrim args)

getEntry : (pos: Integer) -> (store: DataStore) -> Maybe (String, DataStore)
getEntry pos store = let store_items = items store in
  case integerToFin pos (size store) of
    Nothing => Just ("out of range\n", store)
    Just id => Just (index id store_items ++ "\n", store)

processCommand : Command -> DataStore -> Maybe (String, DataStore)
processCommand (Add x) ds = Just ("ID " ++ (show (size ds)) ++ "\n", addToStore ds x)
processCommand (Get x) ds = getEntry x ds
processCommand Quit _ = Nothing

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput ds s = case parse s of
  Nothing => Just ("Invalid command " ++ s ++ "\n", ds)
  Just command => processCommand command ds

main : IO ()
main = replWith (MkData _ []) "Command:  " processInput

allLengths: List String -> List Nat
allLengths [] = []
allLengths (x :: xs) = length x :: allLengths xs

xor : Bool -> Bool -> Bool
xor False y = y
xor True y = not y

isEven : Nat -> Bool
isEven Z = True
isEven (S k) = not (isEven k)

fourInts : Vect 4 Int
fourInts = [0, 1, 2, 3]

allLengthsV : Vect len String -> Vect len Nat
allLengthsV [] = []
allLengthsV (word :: words) = length words :: allLengthsV words

insert : Ord elem => (x: elem) -> (Vect len elem) -> (Vect (S len) elem)
insert x [] = [x]
insert x (y :: xs) = case  x < y of
                          False => y :: insert x xs
                          True => x :: y :: xs

--insert x (y :: xs) = if x < y then x :: y :: xs else y :: insert y xs

insSort : Ord elem => Vect n elem -> Vect n elem
insSort [] = []
insSort (x :: xs) = let xsSorted = insSort xs in
  insert x xsSorted

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

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

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

map2 : (a -> b) -> Vect len a -> Vect len b
map2 f [] = []
map2 f (x :: xs) = f x :: map2 f xs

createEmpties: Vect n (Vect 0 elem)
createEmpties = replicate _ []

transposeHelper: (x : Vect n elem) ->
                 (xsTrans : Vect n (Vect k elem)) ->
                 Vect n (Vect (S k) elem)
transposeHelper [] [] = []
transposeHelper (x :: xs) (y :: ys) = (x :: y) :: transposeHelper xs ys

transposeMat: Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) = let xsTrans = transposeMat xs in
  zipWith (::) x xsTrans

transposeV : Vect n elem -> Vect n (Vect 1 elem)
transposeV [] = []
transposeV (x :: xs) = [x] :: transposeV xs

addMatrix: Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = let added = addMatrix xs ys in
  (zipWith (+) x y) :: added

data Direction = North
  | East
  | South
  | West

tryIndex: Integer -> Vect n a -> Maybe a
tryIndex {n} i xs = case integerToFin i n of
  Nothing => Nothing
  Just idx => Just (index idx xs)

data PowerSource = Petrol | Pedal

data Vehicle : PowerSource -> Type where
  Bicycle: Vehicle Pedal
  Car: (fuel: Nat) -> Vehicle Petrol
  Bus: (fuel: Nat) -> Vehicle Petrol

wheels: Vehicle power -> Nat
wheels Bicycle = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4

refuel: Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200

--zip (+) x y :: ?hole1

--addMatrix [] = ?addMatrix_rhs_1
--addMatrix (x :: xs) = let xs_added = addMatrix xs in

-- StringOrInt : Bool -> Type
-- StringOrInt x = case x of
--   True => String
--   False => Int

-- getStringOrInt : (x : Bool) -> StringOrInt x
-- getStringOrInt x = case x of
--   True => ?xTrueType
--   False => ?yFalseType

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module Decidable.IntOrder

import Decidable.Order

%default total

public export
data LTE : Int -> Int -> Type where
  Compare : (a : Int) -> (b : Int) -> { auto prf : a <= b = True} -> LTE a b
  Reflexive : (a : Int) -> LTE a a
  Transitive : (a : Int) -> (b : Int) -> (c : Int) -> (ab : LTE a b) -> (bc : LTE b c) -> LTE a c
  Ordered : (a : Int) -> (b : Int) -> { auto contra : (a <= b = True) -> Void } -> LTE b a

export
implementation Preorder Int LTE where
  transitive = Transitive
  reflexive = Reflexive

export
implementation Poset Int LTE where
  antisymmetric x _ _ _ = really_believe_me $ Refl {x}

export
implementation Ordered Int LTE where
  order a b = case decEq (a <= b) True of
              Yes prf => Left $ Compare {prf} a b
              No contra => Right $ Ordered {contra} a b

max_stars_repo_name: jdevuyst/idris-data

max_issues_repo_name: jdevuyst/idris-data

max_forks_repo_name: jdevuyst/idris-data


text:
data Fin : Nat -> Type where
     FZ : Fin (S k)
     FS : Fin k -> Fin (S k)

interface Finite t where
  card   : Nat
  to     : t -> Fin card
  from   : Fin card -> t
  toFrom : (k : Fin card) -> to (from k) = k
  fromTo : (x : t) -> from (to x) = x

-- Checking dependent methods work, and that having names from the
-- methods shadowed in the interface head doesn't cause any issues

implementation Finite (Fin k) where
  card   = ?ncard
  to     = ?lala
  from   = ?lula
  toFrom = ?foo
  fromTo = ?bar

implementation Finite (Fin n) where
  card   = ?ncard1
  to     = ?lala1
  from   = ?lula1
  toFrom = ?foo1
  fromTo = ?bar1

implementation Finite (Fin t) where
  card   = ?ncard2
  to     = ?lala2
  from   = ?lula2
  toFrom = ?foo2
  fromTo = ?bar2


text:
import Drahko

foo : Promise String
foo = do
  let dot = "."
  let x = \y => do
    msgBox "appending"
    pure (y ++ dot)
  a <- x "Hello"
  b <- x "World"
  pure (a ++ "  ayy lmao  " ++ b)

main : Promise ()
main = do
  x <- foo
  msgBox x
  msgBox x

max_stars_repo_name: NickSeagull/idris-autohotkey

max_issues_repo_name: NickSeagull/idris-autohotkey

max_forks_repo_name: drahko/drahko


text:
module Language.LSP.Message.Trace

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

namespace Trace
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#traceValue
  public export
  data Trace = TraceOff | TraceMessages | TraceVerbose

export
ToJSON Trace where
  toJSON TraceOff      = JString "off"
  toJSON TraceMessages = JString "messages"
  toJSON TraceVerbose  = JString "verbose"

export
FromJSON Trace where
  fromJSON (JString "off")      = pure TraceOff
  fromJSON (JString "messages") = pure TraceMessages
  fromJSON (JString "verbose")  = pure TraceVerbose
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#setTrace
public export
record SetTraceParams where
  constructor MkSetTraceParams
  value : Trace
%runElab deriveJSON defaultOpts `{{SetTraceParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#logTrace
public export
record LogTraceParams where
  constructor MkLogTraceParams
  message : String
  verbose : Maybe String
%runElab deriveJSON defaultOpts `{{LogTraceParams}}


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

module API.Web.HTML.HTMLElement

import API.Web.HTML.HTMLCanvasElement
import API.Web.HTML.HTMLScriptElement
import IdrisScript

%access public export
%default total

||| The HTMLElement is the interface from which all the HTML elements'
||| interfaces inherit, and which must be used by elements that have no
||| additional requirements.
|||
||| The original specification can be found at
||| https://html.spec.whatwg.org/#htmlelement
data HTMLElement : Type where
  FromHTMLCanvasElement : HTMLCanvasElement    -> HTMLElement
  FromHTMLScriptElement     : HTMLScriptElement    -> HTMLElement
  New                   : (localName : String) -> (self : JSRef)-> HTMLElement

||| htmlElementFromPointer is a helper function for easily creating HTMLElements
||| from JavaScript references.
|||
||| @ ref A pointer to an HTMLElement.
htmlElementFromPointer : (ref : JSRef) -> JS_IO $ Maybe HTMLElement
htmlElementFromPointer ref = case !maybeLocalName of
    Nothing          => pure Nothing
    (Just localName) => case localName of
      "canvas" => case !(htmlCanvasElementFromPointer ref) of
        Nothing       => pure Nothing
        (Just canvas) => pure $ Just $ FromHTMLCanvasElement canvas
      "script" => case !(htmlScriptElementFromPointer ref) of
        Nothing       => pure Nothing
        (Just script) => pure $ Just $ FromHTMLScriptElement script
      _        => pure $ Just $ New localName ref
  where
    maybeLocalName : JS_IO $ Maybe String
    maybeLocalName = let
        getLocalName = jscall "%0.localName" (JSRef -> JS_IO JSRef) ref
      in
        case !(IdrisScript.pack !getLocalName) of
             (JSString ** str) => pure $ Just $ fromJS str
             _                 => pure Nothing

max_stars_repo_name: blau-io/idris-html

max_issues_repo_name: blau-io/idris-html

max_forks_repo_name: blau-io/idris-html


text:
module Bar

import Foo

main : IO ()
main = printLn "Bar"


text:
module Control.WellFounded

import Control.Relation
import Data.Nat
import Data.List

%default total

public export
data Accessible : (rel : a -> a -> Type) -> (x : a) -> Type where
  Access : (rec : (y : a) -> rel y x -> Accessible rel y) ->
           Accessible rel x

public export
interface WellFounded a rel where
  wellFounded : (x : a) -> Accessible rel x

export
accRec : {0 rel : (arg1 : a) -> (arg2 : a) -> Type} ->
         (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->
         (z : a) -> (0 acc : Accessible rel z) -> b
accRec step z (Access f) =
  step z $ \yarg, lt => accRec step yarg (f yarg lt)

export
accInd : {0 rel : a -> a -> Type} -> {0 P : a -> Type} ->
         (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
         (z : a) -> (0 acc : Accessible rel z) -> P z
accInd step z (Access f) =
  step z $ \y, lt => accInd step y (f y lt)

export
wfRec : (0 _ : WellFounded a rel) =>
        (step : (x : a) -> ((y : a) -> rel y x -> b) -> b) ->
        a -> b
wfRec step x = accRec step x (wellFounded {rel} x)

export
wfInd : (0 _ : WellFounded a rel) => {0 P : a -> Type} ->
        (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
        (myz : a) -> P myz
wfInd step myz = accInd step myz (wellFounded {rel} myz)

public export
interface Sized a where
  constructor MkSized
  total size : a -> Nat

public export
Smaller : Sized a => a -> a -> Type
Smaller = \x, y => size x `LT` size y

public export
SizeAccessible : Sized a => a -> Type
SizeAccessible = Accessible Smaller

export
sizeAccessible : Sized a => (x : a) -> SizeAccessible x
sizeAccessible x = Access (acc $ size x)
  where
    acc : (sizeX : Nat) -> (y : a) -> (size y `LT` sizeX) -> SizeAccessible y
    acc (S x') y (LTESucc yLEx')
        = Access $ \z, zLTy => acc x' z $ transitive {rel = LTE} zLTy yLEx'

export
sizeInd : Sized a => {0 P : a -> Type} ->
          (step : (x : a) -> ((y : a) -> Smaller y x -> P y) -> P x) ->
          (z : a) ->
          P z
sizeInd step z = accInd step z (sizeAccessible z)

export
sizeRec : Sized a =>
          (step : (x : a) -> ((y : a) -> Smaller y x -> b) -> b) ->
          (z : a) -> b
sizeRec step z = accRec step z (sizeAccessible z)

export
Sized Nat where
  size = id

export
WellFounded Nat LT where
  wellFounded = sizeAccessible

export
Sized (List a) where
  size = length

export
(Sized a, Sized b) => Sized (Pair a b) where
  size (x,y) = size x + size y


text:
infixl 7 <><

public export
(<><) : SnocList a -> List a -> SnocList a
sx <>< [] = sx
sx <>< (x :: xs) = (sx :< x) <>< xs


text:
import Data.Maybe
import Data.Nat

namespace SuperDog
  public export
  record SuperDog where
     constructor MkDog
     supername : String
     age : Int
     weight : Int

namespace OrdinaryDog
  public export
  record OrdinaryDog where
    constructor MkDog
    name : String
    age : Int
    weight : Int

record Other a where
  constructor MkOther
  {imp : String}
  fieldA : a
  fieldB : b

------ Using new application syntax as sugar for data instantiation (be it data/record/interface) -------

myDog : OrdinaryDog
myDog = MkDog { age = 4
              , weight = 12
              , name = "Sam" }

mySuperDog : SuperDog
mySuperDog = MkDog { age = 3
                   , weight = 10
                   , supername = "Super-Sam" }

other : ?
other = MkOther {fieldB = the Int 1, fieldA = "hi", imp = "Secret string"}

otherOk1 : Main.other.fieldB = (the Int 1)
otherOk1 = Refl

otherOk2 : Main.other.fieldA = "hi"
otherOk2 = Refl

otherOk3 : Main.other.imp = "Secret string"
otherOk3 = Refl

same : MkDog {age = 2, name = "Rex", weight = 10} = (the OrdinaryDog $ MkDog "Rex" 2 10)
same = Refl

namespace R1

  public export
  record R1 where
    constructor MkR
    field : a

namespace R2

  public export
  record R2 where
    constructor MkR
    {auto field : a}

r1 : R1 -- explicit fields access
r1 = MkR {field = "string"}

r2_shouldNotTypecheck1 : ?
r2_shouldNotTypecheck1 = MkR {field = the Nat 22} -- fail, impossible to disambiguate

interface Show a => (num : Num a) => MyIface a where -- Some interface with
  constructor MkIface
                                             -- constraints
  data MyData : a -> Type                    -- and a data declaration.
  someFunc : a -> a                          -- Constraints are now elaborated as auto implicits (as one would expect)
  giveBack : {x : a} -> MyData x -> a        -- (previously as explicit arguments of the interface
                                             -- constructor)

data MyDataImpl : a -> Type where            -- implementation of MyData
  MkMyData : (x : a) -> MyDataImpl x

-- implementation MyIface Int where
--    MyData = MyDataImpl
--    someFunc = id
--    giveBack (MkMyData x) = x

%hint
instanceMyIfaceInt : MyIface Integer -- this def, roughly speaking, is the 'same thing' as the above implementation
                                     -- Show Int, Num Int are auto implicits of MkIface
instanceMyIfaceInt = MkIface { MyData = MyDataImpl
                             , someFunc = id
                             , giveBack = \(MkMyData x) => x
                             , num = %search } -- auto implicit names are preserved

instanceOk : giveBack (MkMyData 22) = 22
instanceOk = Refl

interface Show' a where -- unlike Show, Show' reduces in types
   constructor MkShow'
   show' : a -> String

Show' String where
   show' = id

%hint
showMaybe' : Show' a => Show' (Maybe a)
showMaybe' = MkShow' { show' = fromMaybe "Nothing" . (("Just " ++ ) . show' <$>) }

showMaybe'Ok : show' (Just "nice") = "Just nice"
showMaybe'Ok = Refl

record AllFieldTypes a where
   constructor MkAllFieldTypes
   exp : a
   {imp : a}
   {auto aut : a}

testAllFieldTypesOk : MkAllFieldTypes { aut = "aut"
                                      , exp = "exp"
                                      , imp = "imp" }
                       = MkAllFieldTypes "exp" {imp = "imp"} @{"aut"}
testAllFieldTypesOk = Refl

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

------  The Update syntax --------

mapName : (String -> String) -> OrdinaryDog -> OrdinaryDog
mapName f = {name $= f}

setName : String -> OrdinaryDog -> OrdinaryDog
setName name' = {name := name'}

data Three : Type -> Type -> Type -> Type where
  MkThree : (x : a) -> (y : b) -> (z : c) -> Three a b c

mapSetMap : (a -> a') -> b' -> (c -> c') -> Three a b c -> Three a' b' c'
mapSetMap f y' g = {x $= f, y := y', z $= g}

setNameOld : String -> OrdinaryDog -> OrdinaryDog
setNameOld name' = {name := name'}

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

--------- Applications in presence of duplicate names ----------

-- Duplicate names are ok and treated sequentially
testDuplicateNames : {auto a : String} -> {auto a : String} -> String
testDuplicateNames @{a} @{a'} = show' a ++ ":" ++ show' a'

-- When binding arguments on LHS or listing arguments to
-- a function on RHS
-- unnamed arguments always take priority over named,
-- i.e they are bound/applied first,
-- regardless of their relative positions to named ones
testOrder1 : (a : String) -> (a : String) -> String
testOrder1 {a = a2} {-snd-} a1 {-fst-} = a1 ++ a2

testOrder1Ok : Main.testOrder1 "abc" "def" = "abcdef"
testOrder1Ok = Refl

-- unnamed explicit "1" is passed first, followed by named {a = "2"}
testAutoPriorityOk : Main.testOrder1 {a = "2"} "1" = "12"
testAutoPriorityOk = Refl

-- Two arguments with the same name can be successfully bound
-- if one of them is renamed in patterns.
-- As both arguments are requested by name
-- They are bound in the same order they are given
sameNamesOk : (a : String) -> (a : Nat) -> (String, Nat)
sameNamesOk {a {- = a-}, a = b} = (a, b)

-- All arguments are named and are of different `plicities`. Binds occur sequentially.
-- Arguments are renamed on LHS
eachArgType : (a : String) -> {a : String} -> {auto a : String} -> String
eachArgType {a = a1, a = a2, a = a3} = a1 ++ a2 ++ a3

eachArgTypeOk : eachArgType @{"3"} "1" {a = "2"} = "123"
eachArgTypeOk = Refl

-- Arguments with the same names are provided on RHS
-- which is ok, they are passed sequentially.
eachArgTypeOk2 : eachArgType {a = "1", a = "2", a = "3"} = "123"
eachArgTypeOk2 = Refl

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

--------- Bind-all-explicits pattern ----------

-- This pattern works like inexhaustible supply of
-- `_` (Match-any patterns).

-- Here to complete the definition we only
-- need to know the name of the OrdinaryDog.
-- We bind it with `{name, _}` also stating that
-- any extra explicits should be disregarded,
-- by inserting `_` into the braces.
onlyName : OrdinaryDog -> String
onlyName (MkDog {name, _ {-age, weight-} }) = name

dontCare : (x : String) -> (y : String) -> (z : String) -> String
dontCare {x, z, _} = x ++ z

dontCareOk : Main.dontCare "a" "b" "c" = "ac"
dontCareOk = Refl

-- If none of the explicit arguments are wanted
-- one `{}` can be used instead of writing an underscore for each.
dontCare2 : (x : Nat) -> Nat -> Nat -> Nat -> (y : Nat) -> x + y = y + x
dontCare2 {} = plusCommutative {}
-- dontCare2 _ _ _ _ _ = plusCommutative _ _

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

isNode : Tree a -> Bool
isNode (Node {}) = True
isNode _ = False

data IsNode : Tree a -> Type where
  Is : IsNode (Node {})

decIsNode : (x : Tree a) -> Dec (IsNode x)
decIsNode (Node {}) = Yes Is
decIsNode (Leaf {}) = No (\case Is impossible)
------------------------------------------------


text:
module Main

import Data.List
import Data.HVect
import Helper

allowedChars : List Char
allowedChars = ['a'..'z'] ++ ['0'..'9'] ++ ['-']

data ValidLiteral : List Char -> Type where
  One : { auto prf : Elem value Main.allowedChars } -> ValidLiteral [value]
  Multi : { auto prf : Elem value Main.allowedChars } -> ValidLiteral xs -> ValidLiteral (value :: xs)

data LiteralRoute : String -> Type where
  Literal : (lit:String) ->
            -- RULE 1
            { auto prf : ValidLiteral (unpack lit) } ->
            LiteralRoute lit

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

data Base = MkBase

maxLevel : Nat
maxLevel = 3

infixl 9 /
data Route :  List Type -> Type where
  Root : Route [Base]
  (/) : Route parent ->
        child ->
        -- RULE 2
        { auto prf : LTE (length (child :: parent) ) Main.maxLevel } ->
        Route (child :: parent)

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

data HttpMethod = HttpGet | HttpPost

HttpHandler : Type
HttpHandler = String -> String

handler : HttpHandler
handler = id

RouteHandler : (route:List Type) -> Type
RouteHandler r = (HttpMethod, Route r, HttpHandler)

GET : Route r -> HttpHandler -> RouteHandler r
GET route handler = (HttpGet, route, handler)

sampleRoute : Test RouteHandler
sampleRoute = Check $ GET (Root / Literal "sports") handler

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

--validConfiguration : Test RoutesConfiguration
--validConfiguration = Check $ Routes
--            ( GET  Root handler ) &
--            ( GET (Root / Literal "sports") handler) &
--            ( GET (Root / Literal "sports" / Literal "football") handler ) -- must compile

--invalidConfiguration : Test RoutesConfiguration
--invalidConfiguration = Check $ Routes
--            ( GET  Root handler ) &
--            ( GET (Root / Literal "sports" / Literal "football") handler ) -- must not compile

max_stars_repo_name: janschultecom/typelevel-seo

max_issues_repo_name: janschultecom/typelevel-seo

max_forks_repo_name: janschultecom/typelevel-seo


text:
module Data.Time.Clock.Internal.POSIX

import Data.Time.Clock.Internal.POSIXTime

import Data.Fixed
import Data.Time.Calendar.Days
import Data.Time.Clock.Internal.POSIXTime
import Data.Time.Clock.Internal.UTCTime
import Data.Time.Clock.System

posixSecondsToUTCTime :: POSIXTime -> UTCTime
posixSecondsToUTCTime i = let
(d, t) = divMod' i posixDayLength
in UTCTime (addDays d systemEpochDay) (realToFrac t)

utcTimeToPOSIXSeconds :: UTCTime -> POSIXTime
utcTimeToPOSIXSeconds (UTCTime d t) =
(fromInteger (diffDays d systemEpochDay) * posixDayLength) + min posixDayLength (realToFrac t)

systemToPOSIXTime :: SystemTime -> POSIXTime
systemToPOSIXTime (MkSystemTime s ns) = (fromIntegral s) + (fromIntegral ns) * 1E-9

-- | Get the current POSIX time from the system clock.
getPOSIXTime :: IO POSIXTime
getPOSIXTime = fmap systemToPOSIXTime getSystemTime

-- | Get the current 'UTCTime' from the system clock.
getCurrentTime :: IO UTCTime
getCurrentTime = systemToUTCTime `fmap` getSystemTime

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Control.Comonad.Trans

import Control.Comonad

%default total

public export
interface ComonadTrans (0 t : (Type -> Type) -> Type -> Type) where
  lower : Comonad w => t w a -> w a


text:
import Data.Vect

tryIndex : Integer -> Vect n a -> Maybe a
tryIndex {n} i xs = case integerToFin i n of
                         Nothing => Nothing
                         (Just idx) => Just (index idx xs)

vectTake : (num : Fin (S n)) -> Vect n a -> Vect (finToNat num) a
vectTake FZ _ = []
vectTake (FS y) (x :: xs) = x :: vectTake y xs