text:
module Circuits.Idealised.Parser

import Data.Nat
import Data.List1

import Text.Lexer
import Text.Parser

import Toolkit.Data.Whole
import Toolkit.Data.Location
import Toolkit.Text.Lexer.Run
import Toolkit.Text.Parser.Support
import Toolkit.Text.Parser.Location
import Toolkit.Text.Parser.Run

import Ref

import Circuits.Idealised.Types
import Circuits.Idealised.AST
import Circuits.Idealised.Lexer

%default total

namespace Idealised
  public export
  Rule : Type -> Type
  Rule = Rule Unit Token

  public export
  RuleEmpty : Type -> Type
  RuleEmpty = RuleEmpty Unit Token

  export
  eoi : RuleEmpty Unit
  eoi = eoi isEOI
    where
      isEOI : Token -> Bool
      isEOI EndInput = True
      isEOI _ = False

namespace API
  export
  symbol : String -> Rule Unit
  symbol str
    = terminal ("Expected Symbol '" ++ str ++ "'")
               (\x => case x of
                             Symbol s => if s == str then Just MkUnit
                                                     else Nothing
                             _ => Nothing)

  export
  nat : Rule Nat
  nat = terminal "Expected nat literal"
               (\x => case x of
                           LitNat i => Just i
                           _ => Nothing)

  export
  keyword : String -> Rule Builtin.Unit
  keyword str
    = terminal ("Expected Keyword '" ++ str ++ "'")
                 (\x => case x of
                             Keyword s => if s == str then Just Builtin.MkUnit
                                                      else Nothing
                             _ => Nothing)

  export
  identifier : Rule String
  identifier
    = terminal "Expected Identifier"
               (\x => case x of
                                  ID str => Just str
                                  _ => Nothing)

  export
  name : Rule String
  name = identifier

  export
  ref : Rule Ref
  ref =
    do s <- Toolkit.location
       n <- name
       e <- Toolkit.location
       pure (MkRef (newFC s e) n)

  export
  gives : String -> a -> Rule a
  gives s ctor
    = do keyword s
         pure ctor

  export
  inserts : Rule a -> (a -> b) -> Rule b
  inserts value ctor
    = do v <- value
         pure (ctor v)

  export
  whole : Rule Whole
  whole =
      do n <- nat
         isWhole n
    where
      isWhole : Nat -> RuleEmpty Whole
      isWhole Z = fail "expected whole"
      isWhole (S n) = pure (W (S n) ItIsSucc)

  export
  sFooter : Location -> Rule FileContext
  sFooter s
    = do symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (newFC s e)

namespace Direction
  export
  direction : Rule Direction
  direction = gives "input" INPUT <|> gives "output" OUTPUT

namespace Types

  mutual
    logic : Rule DType
    logic = gives "logic" LOGIC

    array : Rule DType
    array
        = do ty <- logic
             ns <- indices
             pure (arraytype ty ns)
      where
        index : Rule Whole
        index
          = do symbol "["
               n <- whole
               symbol "]"
               pure n

        indices : Rule (List1 Whole)
        indices = some index

        arraytype : DType -> List1 Whole -> DType
        arraytype ty (x:::xs) = foldl (\ty, n => BVECT n ty) ty (x::xs)

    export
    type : Rule DType
    type = array <|> logic

namespace Kinds

  export
  gateKind : Rule GateKind
  gateKind =  gives "nand" ANDN
          <|> gives "and"  AND
          <|> gives "xor"  XOR
          <|> gives "xnor" XORN
          <|> gives "ior"  IOR
          <|> gives "nior" IORN
          <|> gives "join" JOIN

namespace Terms

  portDecl : Rule (Location, Ref, Direction, DType)
  portDecl
    = do s <- Toolkit.location
         d <- direction
         t <- type
         r <- ref
         pure (s,r,d,t)

  portList : Rule (List1 (Location,Ref, Direction, DType))
  portList
    = do symbol "("
         ps <- sepBy1 (symbol ",") portDecl
         symbol ")"
         symbol ";"
         pure ps

  data Body = WDecl  FileContext DType Ref Ref
            | GInst  FileContext GateKind Ref Ref Ref
            | DInst  FileContext Ref Ref Ref
            | NInst  FileContext Ref Ref
            | MInst  FileContext Ref Ref Ref Ref
            | ISInst FileContext Ref Ref
            | IEInst FileContext End Ref Ref Ref
            | IPInst FileContext Nat Ref Ref Ref Ref

            | ESInst FileContext Ref Ref
            | Merge  FileContext Ref Ref Ref

  gateNot : Rule Body
  gateNot
    = do s <- Toolkit.location
         keyword "not"
         symbol "("
         o <- ref
         symbol ","
         i <- ref
         fc <- sFooter s
         pure (NInst fc o i)

  gateBin : Rule Body
  gateBin
    = do s <- Toolkit.location
         k <- gateKind
         symbol "("
         o <- ref
         symbol ","
         a <- ref
         symbol ","
         b <- ref
         fc <- sFooter s
         e <- Toolkit.location
         pure (GInst fc k o a b)

  gateCopy : Rule Body
  gateCopy
    = do s <- Toolkit.location
         keyword "copy"
         symbol "("
         o <- ref
         symbol ","
         a <- ref
         symbol ","
         b <- ref
         fc <- sFooter s
         pure (DInst fc o a b)

  gateMux : Rule Body
  gateMux
    = do s <- Toolkit.location
         keyword "mux"
         symbol "("
         o <- ref
         symbol ","
         c <- ref
         symbol ","
         a <- ref
         symbol ","
         b <- ref
         fc <- sFooter s
         pure (MInst fc o c a b)

  gateMerge : Rule Body
  gateMerge
    = do s <- Toolkit.location
         keyword "merge"
         symbol "("
         o <- ref
         symbol ","
         a <- ref
         symbol ","
         b <- ref
         fc <- sFooter s
         pure (Merge fc o a b)

  gateSplit : Rule Body
  gateSplit
      = singletonI <|> singletonE <|> edge <|> split
    where

      singletonE : Rule Body
      singletonE
        = do s <- Toolkit.location
             keyword "extract"
             symbol "("
             o <- ref
             symbol ","
             i <- ref
             fc <- sFooter s
             pure (ISInst fc o i)

      singletonI : Rule Body
      singletonI
        = do s <- Toolkit.location
             keyword "insert"
             symbol "("
             o <- ref
             symbol ","
             i <- ref
             fc <- sFooter s
             pure (ESInst fc o i)

      kind : Rule End
      kind = gives "first" F <|> gives "last" L

      edge : Rule Body
      edge
        = do s <- Toolkit.location
             k <- kind
             symbol "("
             a <- ref
             symbol ","
             b <- ref
             symbol ","
             i <- ref
             fc <- sFooter s
             pure (IEInst fc k a b i)

      split : Rule Body
      split
        = do s <- Toolkit.location
             keyword "index"
             symbol "["
             n <- nat
             symbol "]"
             symbol "("
             a <- ref
             symbol ","
             b <- ref
             symbol ","
             x <- ref
             symbol ","
             y <- ref
             fc <- sFooter s
             pure (IPInst fc n a b x y)

  wireDecl : Rule Body
  wireDecl
      = do s <- Toolkit.location
           keyword "wire"
           t <- type
           keyword "as"
           symbol "("
           a <- ref
           symbol ","
           b <- ref
           symbol ")"
           symbol ";"
           e <- Toolkit.location
           pure (WDecl (newFC s e) t a b)

  expr : Rule Body
  expr =  wireDecl
      <|> gateNot
      <|> gateBin
      <|> gateCopy
      <|> gateSplit
      <|> gateMux
      <|> gateSplit
      <|> gateMerge

  foldBody : Location
          -> List Body
          -> AST
  foldBody l Nil
        = Stop (newFC l l)
  foldBody l (head :: tail)
        = foldr doFold (Stop (newFC l l)) (head :: tail)
    where
      doFold : Body -> AST -> AST
      doFold (WDecl x y z w) accum
        = Wire x y z w accum

      doFold (MInst v x y z w) accum
        = Seq (Mux v (Var x) (Var y) (Var z) (Var w))
              accum

      doFold (GInst x k y z w) accum
        = Seq (Gate x k (Var y) (Var z) (Var w))
              accum

      doFold (DInst x y z w) accum
        = Seq (Dup x (Var y) (Var z) (Var w))
              accum

      doFold (NInst x y z) accum
        = Seq (Not x (Var y) (Var z))
              accum

      doFold (ISInst x y z) accum
        = Seq (IndexS x (Var y) (Var z))
              accum

      doFold (IEInst v w x y z) accum
        = Seq (IndexE v w (Var x) (Var y) (Var z))
              accum

      doFold (IPInst u v w x y z) accum
        = Seq (IndexP u v (Var w) (Var x) (Var y) (Var z))
              accum

      doFold (ESInst fc o i) accum
        = Seq (MergeS fc (Var o) (Var i))
              accum

      doFold (Merge fc o a b) accum
        = Seq (MergeV fc (Var o) (Var a) (Var b))
              accum

  foldPorts : Location
           -> List1 (Location,Ref, Direction, DType)
           -> AST
           -> AST
  foldPorts e (x:::xs) y
    = foldr (\(s,r,d,t), body => Input (newFC s e) d t r body) y (x::xs)

  export
  design : Rule AST
  design
    = do keyword "module"
         n <- ref
         ps <- portList
         b <- many expr
         e <- Toolkit.location
         keyword "endmodule"
         symbol ";"
         pure (foldPorts e ps (foldBody e b))

namespace Idealised

  export
  fromFile : (fname : String)
                   -> IO (Either (ParseError Token) AST)
  fromFile fname
    = case !(parseFile Idealised.Lexer design fname) of
        Left err  => pure (Left err)
        Right ast => pure (Right (setSource fname ast))
-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module CairoCode.Traversal.Base

import CairoCode.CairoCode
import Core.Context
import Data.SortedSet
import Data.SortedMap
import Utils.Lens

export
data TraversalRes : Type -> Type -> Type  where
  MkTraversalRes : s -> a -> TraversalRes s a

export
data Traversal : Type -> Type -> Type where
  MkTraversal : (s -> TraversalRes s a) -> Traversal s a

export
runTraversal : Traversal s a -> s -> TraversalRes s a
runTraversal (MkTraversal f) = f

getState : TraversalRes s a -> s
getState (MkTraversalRes s a) = s

getValue : TraversalRes s a -> a
getValue (MkTraversalRes s a) = a

export
readState : Traversal s s
readState = MkTraversal (\s => MkTraversalRes s s)

export
writeState : s -> Traversal s ()
writeState sv = MkTraversal (\_ => MkTraversalRes sv ())

export
updateState : (s -> s) -> Traversal s ()
updateState fn = MkTraversal (\s => MkTraversalRes (fn s) ())

-- Note: is only here because needs access to MkTraversal & MkTraversalRes & runTraversal
export
composeState : Lens os is -> Traversal is a -> Traversal os a
composeState lens it = MkTraversal (\osv => let MkTraversalRes is av = runTraversal it (lens.get osv) in MkTraversalRes (lens.set osv is) av)

public export
Functor (Traversal s) where
 map fn (MkTraversal ma) = MkTraversal
    (\s => let MkTraversalRes s' a = ma s in MkTraversalRes s' (fn a))

public export
Applicative (Traversal s) where
    pure a = MkTraversal (\s => MkTraversalRes s a)
    (<*>) (MkTraversal mf) (MkTraversal ma) = MkTraversal
        (\s => let MkTraversalRes s' f = mf s in
        let MkTraversalRes s'' a = ma s' in MkTraversalRes s'' (f a))

public export
Monad (Traversal s) where
    (MkTraversal ma) >>= f = MkTraversal
        (\s => let MkTraversalRes s' a = ma s in runTraversal (f a) s')

public export
data InstVisit : Type -> Type where
      VisitFunction : Name -> (params: List CairoReg) -> (implicits: SortedMap LinearImplicit CairoReg) -> (rets: List String) -> InstVisit a
      VisitForeignFunction : Name -> (info : ForeignInfo) -> (args:Nat) -> (rets:Nat) -> InstVisit a
      VisitAssign : (res:CairoReg) -> a -> InstVisit a
      VisitMkCon : (res:CairoReg) -> Maybe Int -> (args : List a) -> InstVisit a
      VisitMkClosure: (res:CairoReg) -> Name -> (missing : Nat) -> (args : List a) -> InstVisit a
      VisitApply : (res:CairoReg) -> (implicits: SortedMap LinearImplicit (a, CairoReg)) -> (f : a) -> (arg : a) -> InstVisit a
      VisitMkConstant : (res:CairoReg) -> CairoConst -> InstVisit a
      VisitCall : List CairoReg -> (implicits: SortedMap LinearImplicit (a, CairoReg)) -> Name -> (args : List a) -> InstVisit a
      VisitOp : (res:CairoReg) -> (implicits: SortedMap LinearImplicit (a, CairoReg)) -> CairoPrimFn -> List a -> InstVisit a
      VisitExtprim : List CairoReg -> (implicits: SortedMap LinearImplicit (a, CairoReg)) -> Name -> List a -> InstVisit a
      VisitCase : a -> InstVisit a
      VisitConBranch : Maybe Int -> InstVisit a
      VisitConstBranch : Maybe CairoConst -> InstVisit a
      VisitBranchEnd : InstVisit a
      VisitCaseEnd : InstVisit a
      VisitProject : (res:CairoReg) -> (value : a) -> (pos : Nat) -> InstVisit a
      VisitReturn : List a -> SortedMap LinearImplicit a -> InstVisit a
      VisitNull : (res:CairoReg) -> InstVisit a
      VisitError : (res:CairoReg) -> String -> InstVisit a
      VisitEndFunction : InstVisit a

export
Show a => Show (InstVisit a) where
   show (VisitFunction _ _ _ _) = "VisitFunction"
   show (VisitForeignFunction _ _ _ _) = "VisitForeignFunction"
   show (VisitAssign _ _ ) = "VisitAssign"
   show (VisitMkCon _ _ _ ) = "VisitMkCon"
   show (VisitMkClosure _ _ _ _) = "VisitMkClosure"
   show (VisitApply _ _ _ _) = "VisitApply"
   show (VisitMkConstant _ _ ) = "VisitMkConstant"
   show (VisitCall _ _ _ _) = "VisitCall"
   show (VisitOp _ _ _ _) = "VisitOp"
   show (VisitExtprim _ _ _ _) = "VisitExtprim"
   show (VisitCase _) = "VisitCase"
   show (VisitConBranch _ ) = "VisitConBranch"
   show (VisitConstBranch _ ) = "VisitConstBranch"
   show VisitBranchEnd = "VisitBranchEnd"
   show VisitCaseEnd = "VisitCaseEnd"
   show (VisitProject _ _ _) = "VisitProject"
   show (VisitReturn _ _ ) = "VisitReturn"
   show (VisitNull _ ) = "VisitNull"
   show (VisitError _ _ ) = "VisitError"
   show VisitEndFunction = "VisitEndFunction"

mutual
    export
    fromCairoInst : CairoInst -> List (InstVisit CairoReg)
    fromCairoInst (ASSIGN res src) = [VisitAssign res src]
    fromCairoInst (MKCON res tag args) = [VisitMkCon res tag args]
    fromCairoInst (MKCLOSURE res name missing args) = [VisitMkClosure res name missing args]
    fromCairoInst (APPLY res implicits f a) = [VisitApply res implicits f a]
    fromCairoInst (MKCONSTANT res const) = [VisitMkConstant res const]
    fromCairoInst (CALL res implicits name args) = [VisitCall res implicits name args]
    fromCairoInst (OP res implicits fn args) = [VisitOp res implicits fn args]
    fromCairoInst (EXTPRIM res implicits name args) = [VisitExtprim res implicits name args]
    fromCairoInst (CASE reg alts def) = (VisitCase reg)::(
        (alts >>= (\(t,b) => fromBlock (VisitConBranch (Just t)) b (VisitBranchEnd))) ++
        (fromMaybe [] (map (\b => fromBlock (VisitConBranch Nothing) b (VisitBranchEnd)) def)) ++
        [VisitCaseEnd])
    fromCairoInst (CONSTCASE reg alts def) =  (VisitCase reg)::(
        (alts >>= (\(c,b) => fromBlock (VisitConstBranch (Just c)) b (VisitBranchEnd))) ++
        (fromMaybe [] (map (\b => fromBlock (VisitConstBranch Nothing) b (VisitBranchEnd)) def)) ++
        [VisitCaseEnd])
    fromCairoInst (PROJECT res value pos) = [VisitProject res value pos]
    fromCairoInst (RETURN res implicits) = [VisitReturn res implicits]
    fromCairoInst (NULL res) = [VisitNull res]
    fromCairoInst (ERROR res err) = [VisitError res err]

    fromBlock : InstVisit CairoReg -> List CairoInst -> InstVisit CairoReg -> List (InstVisit CairoReg)
    fromBlock start body end = start::(foldr (\inst,acc => (fromCairoInst inst) ++ acc) [end] body)

export
fromCairoInsts : List CairoInst -> List (InstVisit CairoReg)
fromCairoInsts insts = foldr (\inst,acc => (fromCairoInst inst) ++ acc) [] insts

export
fromCairoDef : (Name, CairoDef) -> List (InstVisit CairoReg)
fromCairoDef (name, FunDef params implicits rets body) = fromBlock (VisitFunction name params implicits rets) body VisitEndFunction
fromCairoDef (name, ForeignDef info args ret) = [VisitForeignFunction name info args ret, VisitEndFunction]

caseInlineOptim : CairoInst -> List CairoInst
caseInlineOptim (CASE reg [] Nothing) = []
caseInlineOptim (CASE reg [alt] Nothing) = snd alt
caseInlineOptim (CASE reg Nil (Just def)) = def
caseInlineOptim inst@(CASE reg alts Nothing) = if all (\(i,b) => isNil b) alts then [] else [inst]
caseInlineOptim inst@(CASE reg alts (Just [])) = if all (\(i,b) => isNil b) alts then [] else [inst]
caseInlineOptim (CONSTCASE reg [] Nothing) = []
caseInlineOptim (CONSTCASE reg [alt] Nothing) = snd alt
caseInlineOptim (CONSTCASE reg Nil (Just def)) = def
caseInlineOptim inst@(CONSTCASE reg alts Nothing) = if all (\(c,b) => isNil b) alts then [] else [inst]
caseInlineOptim inst@(CONSTCASE reg alts (Just [])) = if all (\(c,b) => isNil b) alts then [] else [inst]
caseInlineOptim other = [other]

extractDefaultBranch : List a -> Maybe a
extractDefaultBranch Nil = Nothing
extractDefaultBranch (b::Nil) = Just b
extractDefaultBranch _ = assert_total $ idris_crash "More than one default branch found"

mutual
    toCairoCase : CairoReg -> List (InstVisit CairoReg) -> (CairoInst, List (InstVisit CairoReg))
    toCairoCase reg ((VisitConBranch t)::xs) = buildRes $ processNextBranch t (toCairoInsts xs Nil)
        where processNextBranch : Maybe Int -> (List CairoInst, List (InstVisit CairoReg)) -> (List (Maybe Int, List CairoInst), List (InstVisit CairoReg))
              processNextBranch t (body, VisitCaseEnd::xs) = ([(t,body)],xs)
              processNextBranch t (body, (VisitConBranch nt)::xs) = let (res,rem) = processNextBranch nt (toCairoInsts xs Nil) in ((t,body)::res,rem)
              processNextBranch _ _ = assert_total $ idris_crash "Illegal Const Visitor Pattern"
              buildRes : (List (Maybe Int, List CairoInst), List (InstVisit CairoReg)) -> (CairoInst, List (InstVisit CairoReg))
              buildRes (branches, rem) = (CASE reg alts def, rem)
                where alts : List (Int, List CairoInst)
                      alts = branches >>=  (\(t,b) => fromMaybe [] (map (\rt => [(rt,b)]) t))
                      def : Maybe (List CairoInst)
                      def = extractDefaultBranch (map (\(_,b) => b) (filter (\(t,_) => isNothing t) branches))

    toCairoCase reg ((VisitConstBranch c)::xs) = buildRes $ processNextBranch c (toCairoInsts xs Nil)
        where processNextBranch : Maybe CairoConst -> (List CairoInst, List (InstVisit CairoReg)) -> (List (Maybe CairoConst, List CairoInst), List (InstVisit CairoReg))
              processNextBranch c (body, VisitCaseEnd::xs) = ([(c,body)],xs)
              processNextBranch c (body, (VisitConstBranch nc)::xs) = let (res,rem) = processNextBranch nc (toCairoInsts xs Nil) in ((c,body)::res,rem)
              processNextBranch _ _ = assert_total $ idris_crash "Illegal ConCase Visitor Pattern"
              buildRes : (List (Maybe CairoConst, List CairoInst), List (InstVisit CairoReg)) -> (CairoInst, List (InstVisit CairoReg))
              buildRes (branches, rem) = (CONSTCASE reg alts def, rem)
                where alts : List (CairoConst, List CairoInst)
                      alts = branches >>=  (\(c,b) => fromMaybe [] (map (\rc => [(rc,b)]) c))
                      def : Maybe (List CairoInst)
                      def = extractDefaultBranch (map (\(_,b) => b) (filter (\(c,_) => isNothing c ) branches))

    toCairoCase _ _ = assert_total $ idris_crash "Illegal ConstCase Visitor Pattern"

    -- tail recursive over accumulator
    toCairoInsts : List (InstVisit CairoReg) -> List CairoInst -> (List CairoInst, List (InstVisit CairoReg))
    toCairoInsts (VisitBranchEnd::xs) acc = (reverse acc, xs)
    toCairoInsts (VisitEndFunction::Nil) acc = (reverse acc, Nil)
    toCairoInsts ((VisitAssign res src)::xs) acc = toCairoInsts xs ((ASSIGN res src)::acc)
    toCairoInsts ((VisitMkCon res tag args)::xs) acc = toCairoInsts xs ((MKCON res tag args)::acc)
    toCairoInsts ((VisitMkClosure res name missing args)::xs) acc = toCairoInsts xs ((MKCLOSURE res name missing args)::acc)
    toCairoInsts ((VisitApply res implicits f a)::xs) acc = toCairoInsts xs ((APPLY res implicits f a)::acc)
    toCairoInsts ((VisitMkConstant res const)::xs) acc = toCairoInsts xs ((MKCONSTANT res const)::acc)
    toCairoInsts ((VisitCall res implicits name args)::xs) acc = toCairoInsts xs ((CALL res implicits name args)::acc)
    toCairoInsts ((VisitOp res implicits fn args)::xs) acc = toCairoInsts xs ((OP res implicits fn args)::acc)
    toCairoInsts ((VisitExtprim res implicits name args)::xs) acc = toCairoInsts xs ((EXTPRIM res implicits name args)::acc)
    toCairoInsts ((VisitCase reg)::(VisitCaseEnd)::xs) acc = toCairoInsts xs acc
    toCairoInsts ((VisitCase reg)::xs) acc = let (cI, rem) = toCairoCase reg xs in toCairoInsts rem ((reverse $ caseInlineOptim cI) ++ acc)
    toCairoInsts ((VisitProject res value pos)::xs) acc = toCairoInsts xs ((PROJECT res value pos)::acc)
    toCairoInsts ((VisitReturn res implicits)::xs) acc = toCairoInsts xs ((RETURN res implicits)::acc)
    toCairoInsts ((VisitNull res)::xs) acc = toCairoInsts xs ((NULL res)::acc)
    toCairoInsts ((VisitError res err)::xs) acc = toCairoInsts xs ((ERROR res err)::acc)
    toCairoInsts _ _ = assert_total $ idris_crash "Illegal Visitor Pattern"

export
toCairoDef : List (InstVisit CairoReg) -> (Name, CairoDef)
toCairoDef ((VisitFunction name params implicits rets)::xs) = (name, FunDef params implicits rets (extractResult (toCairoInsts xs [])))
  where extractResult : (List CairoInst, List (InstVisit CairoReg)) -> List CairoInst
        extractResult (is, Nil) = is
        extractResult _ = assert_total $ idris_crash "Not fully parsed"
toCairoDef ((VisitForeignFunction name info args ret)::VisitEndFunction::Nil) = (name, ForeignDef info args ret)
toCairoDef _ = assert_total $ idris_crash "Visitor Pattern must start with a function declaration"

export
visitCairoDef : (InstVisit CairoReg -> Traversal s ()) -> (Name, CairoDef) -> Traversal s ()
visitCairoDef fn def = foldlM (\_,iv => fn iv) () (fromCairoDef def)

export
visitCairoDefs : (InstVisit CairoReg -> Traversal s ()) -> List (Name, CairoDef) -> Traversal s ()
visitCairoDefs fn defs = foldlM (\_,def => visitCairoDef fn def) () defs

export
runVisitCairoDef : (InstVisit CairoReg -> Traversal s (), s) -> (Name, CairoDef) -> s
runVisitCairoDef (fn, init) def = getState $ runTraversal (visitCairoDef fn def) init

export
runVisitCairoDefs : (InstVisit CairoReg -> Traversal s (), s) -> List (Name, CairoDef) -> s
runVisitCairoDefs (fn, init) defs = getState $ runTraversal (visitCairoDefs fn defs) init

export
visitConcatCairoDef : Monoid m => (InstVisit CairoReg -> Traversal s m) -> (Name, CairoDef) -> Traversal s m
visitConcatCairoDef fn def = foldlM (\acc,iv => map (acc <+>) (fn iv)) neutral (fromCairoDef def)

export
visitConcatCairoDefs : Monoid m => (InstVisit CairoReg -> Traversal s m) -> List (Name, CairoDef) -> Traversal s m
visitConcatCairoDefs fn defs  = foldlM (\acc,def => map (acc <+>) (visitConcatCairoDef fn def)) neutral defs

export
runVisitConcatCairoDef : Monoid m => (InstVisit CairoReg -> Traversal s m, s) -> (Name, CairoDef) -> (s, m)
runVisitConcatCairoDef (fn, init) def = let res = runTraversal (visitConcatCairoDef fn def) init in (getState res, getValue res)

export
runVisitConcatCairoDefs : Monoid m => (InstVisit CairoReg -> Traversal s m, s) -> List (Name, CairoDef) -> (s, m)
runVisitConcatCairoDefs (fn, init) defs = let res = runTraversal (visitConcatCairoDefs fn defs) init in (getState res, getValue res)

export
runVisitTransformCairoDef : (InstVisit CairoReg -> Traversal s (List (InstVisit CairoReg)), s) -> (Name, CairoDef) -> (s, (Name, CairoDef))
runVisitTransformCairoDef (fn, init) def = let res = runTraversal (visitConcatCairoDef fn def) init in (getState res, toCairoDef $ getValue res)

export
runVisitTransformCairoDefs : (InstVisit CairoReg -> Traversal s (List (InstVisit CairoReg)), s) -> List (Name, CairoDef) -> (s, List (Name, CairoDef))
runVisitTransformCairoDefs (fn, init) defs = foldl (\(s,acc),def => let (ns,res) = runVisitTransformCairoDef (fn,s) def in (ns, acc ++ [res])) (init,[]) defs

export
lift : (InstVisit a -> b) -> (InstVisit a -> Traversal s b)
lift fn = (\inst => pure $ fn inst)

-- This is the standard and just here for completness
-- use-examples: runVisitCairoDef (rawTraversal myTraverser myInitialState) def
--               runVisitConcatCairoDef (rawTraversal myTraverser myInitialState)  def
--               runVisitTransformCairoDef (traversal myTransformer myInitialState) def

export
rawTraversal : (InstVisit CairoReg -> Traversal s a) -> s -> (InstVisit CairoReg -> Traversal s a, s)
rawTraversal fn s = (fn, s)

-- This is the standard case with a monoidic state
-- use-examples: runVisitCairoDef (traversal myTraverser) def
--               runVisitConcatCairoDef (traversal myTraverser) def
--               runVisitTransformCairoDef (traversal myTransformer) def
export
traversal : Monoid s => (InstVisit CairoReg -> Traversal s a) -> (InstVisit CairoReg -> Traversal s a, s)
traversal fn = (fn, neutral)

-- This is the statelessTraversal and just here for completness
-- use-examples: runVisitCairoDef (pureTraversal myTraverser) def
--               runVisitConcatCairoDef (pureTraversal myTraverser)  def
--               runVisitTransformCairoDef (pureTraversal myTransformer) def

export
pureTraversal : (InstVisit a -> b) -> (InstVisit a -> Traversal () b, ())
pureTraversal fn = (lift fn, ())

-- Helper to work with lenses (L is for lense)
export
readStateL : Lens w p -> Traversal w p
readStateL lens = map lens.get readState

export
updateStateL : Lens w p -> (p -> p) -> Traversal w ()
updateStateL lens fn = updateState (\wv => lens.update wv fn)

export
writeStateL : Lens w p -> p -> Traversal w ()
writeStateL lens pv = updateStateL lens (\_ => pv)

stateCompL : Lens w p -> (p -> (p,r)) -> Traversal w r
stateCompL lens fn = do
    sv <- readStateL lens
    let (nsv, res) = fn sv
    _ <- writeStateL lens nsv
    pure res

ext: idr

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module TwoRepeats

import Data.Stream

%default total

public export
repeat : a -> Stream a
repeat x = xs where
  xs : Stream a
  xs = x :: xs

public export
repeat' : a -> Stream a
repeat' x = x :: repeat' x

repeatsTheSame : (x : a) -> TwoRepeats.repeat x = repeat' x
repeatsTheSame x = ?repeatsTheSame_rhs -- Refl here hangs the typechecker.

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
import Shape_abs

area : Shape -> Double
area s with (shapeView s)
  area (triangle base height) | STriangle = (base * height) / 2
  area (rectangle width height) | SRectangle = width * height
  area (circle radius) | SCircle = 2 * pi * radius * radius

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Libraries.Data.NameMap.Traversable

import Core.Core
import Core.Name
import Libraries.Data.NameMap

treeTraverse : (Name -> a -> Core b) -> Tree h a -> Core (Tree h b)
treeTraverse f (Leaf k v) = Leaf k <$> f k v
treeTraverse f (Branch2 l k r) =
    (\l', r' => Branch2 l' k r')
    <$> treeTraverse f l
    <*> treeTraverse f r
treeTraverse f (Branch3 l k1 m k2 r) =
    (\l', m', r' => Branch3 l' k1 m' k2 r')
    <$> treeTraverse f l
    <*> treeTraverse f m
    <*> treeTraverse f r

export
traverseNameMap : (Name -> a -> Core b) -> NameMap a -> Core (NameMap b)
traverseNameMap f Empty = pure Empty
traverseNameMap f (M h t) = M h <$> treeTraverse f t


text:
||| Predicates for reasoning about elements of a list, based on their
||| index.
|||
||| Module    : AtIndex.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
module Toolkit.Data.List.AtIndex

import Decidable.Equality
import Toolkit.Decidable.Informative

%default total

public export
data AtIndex : (x   :      type)
            -> (xs  : List type)
            -> (idx : Nat)
                   -> Type
  where
    Here : AtIndex x (x::xs) Z
    There : (later : AtIndex x     rest     idx)
                  -> AtIndex x (y::rest) (S idx)

namespace Check

  namespace IsAtIndex
    public export
    data Error = EmptyList
               | SupposedToBeHere
               | SupposedToBeLater
               | Later Error

  listIsEmpty : AtIndex x [] 0 -> Void
  listIsEmpty Here impossible
  listIsEmpty (There later) impossible

  supposedToBeHere : (x = y -> Void) -> AtIndex x (y :: xs) 0 -> Void
  supposedToBeHere f Here = f Refl

  supposedToBeLater : AtIndex x [] (S k) -> Void
  supposedToBeLater Here impossible
  supposedToBeLater (There later) impossible

  isNotLater : (AtIndex x xs k -> Void) -> AtIndex x (y :: xs) (S k) -> Void
  isNotLater f (There later) = f later

  export
  isAtIndex : DecEq type
           => (idx : Nat)
           -> (x   : type)
           -> (xs  : List type)
                  -> DecInfo Error (AtIndex x xs idx)
  isAtIndex Z x []
    = No EmptyList (listIsEmpty)

  isAtIndex Z x (y :: xs) with (decEq x y)
    isAtIndex Z x (x :: xs) | (Yes Refl)
      = Yes Here
    isAtIndex Z x (y :: xs) | (No contra)
      = No SupposedToBeHere (supposedToBeHere contra)

  isAtIndex (S k) x []
    = No SupposedToBeLater (supposedToBeLater)

  isAtIndex (S k) x (_ :: xs) with (isAtIndex k x xs)
    isAtIndex (S k) x (_ :: xs) | (Yes prf)
      = Yes (There prf)
    isAtIndex (S k) x (_ :: xs) | (No msg contra)
      = No (Later msg) (isNotLater contra)

namespace Find

  namespace HasIndex
    public export
    data Error = IsEmpty
               | Later HasIndex.Error

  isEmpty : DPair Nat (AtIndex x []) -> Void
  isEmpty (MkDPair _ Here) impossible

  isNotElem : {x,y : type}
           -> (DPair Nat (AtIndex x xs) -> Void)
           -> (x = y -> Void)
           -> DPair Nat (AtIndex x (y :: xs))
           -> Void
  isNotElem {x} {y} f g (MkDPair fst snd) with (snd)
    isNotElem {x = x} {y = x} f g (MkDPair 0 snd) | Here
      = g Refl
    isNotElem {x = x} {y = y} f g (MkDPair (S idx) snd) | (There later)
      = f (MkDPair idx later)

  export
  hasIndex : DecEq type
          => (x : type)
          -> (xs : List type)
                -> DecInfo HasIndex.Error
                           (DPair Nat (AtIndex x xs))
  hasIndex x []
    = No IsEmpty (isEmpty)
  hasIndex x (y :: xs) with (decEq x y)
    hasIndex x (x :: xs) | (Yes Refl)
      = Yes (MkDPair Z Here)

    hasIndex x (y :: xs) | (No contra) with (hasIndex x xs)
      hasIndex x (y :: xs) | (No contra) | (Yes (MkDPair idx prf))
        = Yes (MkDPair (S idx) (There prf))

      hasIndex x (y :: xs) | (No contra) | (No msg f)
        = No (Later msg) (isNotElem f contra)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
||| An implementation of `Data.Heap` based on left-skewed binary trees.
|||
||| This implementation is an adaptation of Okasaki's `LeftistHeap`
||| found on pp.18-20 of his book, and of this
||| [Agda](http://ics.p.lodz.pl/~stolarek/_media/pl:research:dep-typed-wbl-heaps.pdf)
||| implementation that looked reasonably easy to port.
|||
||| Note that contrary to the paper, we don't index our `LeftistBinTree` with a
||| `Priority` because this would require to _tighten_ the constraint to bounded
||| types: We must have a _lowest_ bound when we construct a singleton tree.
module Data.Heap.LeftistHeap

import public Data.Heap

import Decidable.Order
import Data.Nat
import public Data.Nat.Order

%default covering

-- namespace RawTree

--   ||| A implementation of a leftist binary tree which is not `Nat`-indexed
--   data LeftistBinTree : (a : Type) -> Type where
--     Empty : LeftistBinTree a
--     Node : (elem : a) -> (rank : Int) -> (left : LeftistBinTree a) -> (right : LeftistBinTree a)
--          -> LeftistBinTree a

--   rank : LeftistBinTree a -> Int
--   rank Empty = 0
--   rank (Node _ rank _ _) = rank

--   makeNode : (elem : a) -> LeftistBinTree a -> LeftistBinTree a -> LeftistBinTree a
--   makeNode elem left right =
--     if rank left < rank right
--     then Node elem (rank left + rank right) right left
--     else Node elem (rank left + rank right) left right

--   mergeTree : (Ord a) => (left : LeftistBinTree a) -> (right : LeftistBinTree a) -> LeftistBinTree a
--   mergeTree Empty right = right
--   mergeTree left  Empty = left
--   mergeTree l@(Node elem rank left right) r@(Node elem' rank' left' right') =
--     if (elem < elem')
--     then  makeNode elem left (mergeTree right r)
--     else  makeNode elem' left' (mergeTree l right')

--   findMin : LeftistBinTree a -> Maybe a
--   findMin Empty           = Nothing
--   findMin (Node elem _ _ _) = Just elem

--   popMin : (Ord a) => LeftistBinTree a -> (LeftistBinTree a, Maybe a)
--   popMin Empty  = (Empty, Nothing)
--   popMin (Node elem _ left right) = (mergeTree left right, Just elem)

--   insert : (Ord a) => a -> LeftistBinTree a -> LeftistBinTree a
--   insert x Empty = Node x 1 Empty Empty
--   insert x node  = mergeTree (Node x 1 Empty Empty) node

||| A `LeftistBinTree` is a binary tree decorated with `rank` informations.
|||
||| This is a `Nat`-indexed data structure that forms the basis for a proper
||| heap respecting the `Heap` interface.
||| @rank the rank of the tree, eg. the number of elements it contains
||| @a The type of elements stored in the tree
data LeftistBinTree : (rank : Nat) -> (a : Type) -> Type where

  ||| The empty tree
  Empty : LeftistBinTree Z a

  ||| An element in the `Tree`
  |||
  ||| A `Node` in the tree is built in such a way that it respects the _leftist_
  ||| property: The rank of the `left` node is greater than or equal to the rank
  ||| of the `right` node. Furthermore it must respect the _priority_ property
  ||| which implies that `elem` is lower than equal to elements in `left`  and
  ||| `right` sub-trees.
  |||
  ||| @elem the element contained in the node
  ||| @left the left branch of the tree with rank `k`
  ||| @right the right branch of the tree with rank `n`
  ||| @prfLeftist a proof that the rank of `left` is greater than or equal to the
  ||| the rank of `right`
  Node : {k, n : Nat}
       -> (elem : a)
       -> (left : LeftistBinTree k a) -> (right : LeftistBinTree n a)
       -> { auto prfLeftist : LTE n k }
       -> LeftistBinTree (S (k + n)) a

makeNode : {r, q : Nat} -> (elem : a) -> LeftistBinTree r a -> LeftistBinTree q a -> LeftistBinTree (S (r + q)) a
makeNode elem x y with (order r q {to=LTE})
  makeNode elem x y | (Left z) = rewrite plusCommutative r q in Node elem y x
  makeNode elem x y | (Right z) = Node elem x y

||| Merge 2 `LeftistBinTree`s while preserving properties.
|||
||| @left first tree to merge
||| @right second tree to merge
mergeTree : (Ord a) => {r, q: Nat} -> (left : LeftistBinTree r a) -> (right : LeftistBinTree q a) -> LeftistBinTree (r + q) a
mergeTree Empty right = right
mergeTree left  Empty {r} = rewrite plusZeroRightNeutral r in left
mergeTree (Node elem left right {k} {n}) (Node elem' left' right' {k=k1} {n=n1}) with (elem < elem')
  mergeTree (Node elem left right {k} {n}) (Node elem' left' right' {k=k1} {n=n1}) | True =
    rewrite sym (plusAssociative k n (S (k1 + n1))) in
    makeNode elem left (mergeTree right (Node elem' left' right'))
  mergeTree (Node elem left right {k} {n}) (Node elem' left' right' {k=k1} {n=n1}) | False =
    rewrite sym (plusSuccRightSucc (k + n) (k1 + n1)) in
    rewrite plusCommutative (plus k n) (plus k1 n1) in
    rewrite plusSuccRightSucc (k1 + n1) (k + n) in
    rewrite sym (plusAssociative k1 n1 (S (k + n))) in
    rewrite plusCommutative n1 (S (plus k n)) in
    makeNode elem' left' (mergeTree (Node elem left right) right')

findMin : LeftistBinTree r a -> Maybe a
findMin Empty           = Nothing
findMin (Node elem _ _) = Just elem

popMin : (Ord a) => LeftistBinTree (S r) a -> (LeftistBinTree r a, a)
popMin Empty impossible
popMin (Node elem left right) = (mergeTree left right, elem)

insert : (Ord a) => a -> {r : Nat} -> LeftistBinTree r a -> LeftistBinTree (S r) a
insert x Empty = Node x Empty Empty
insert x node  = mergeTree (Node x Empty Empty) node

||| a `BinaryHeap` is a heap backed by a `LeftistBinTree`
public export
data BinaryHeap : Type -> Type where

  ||| Wrapper around a dependent product of a `rank` and a tree of the
  ||| given rank.
  |||
  ||| This allows us to "hide" the indexed nature of the binary tree and to
  ||| provide a proper implementation of `Heap` interface.
  |||
  BinHeap : ( n : Nat ** LeftistBinTree n a) -> BinaryHeap a

EmptyHeap : BinaryHeap a
EmptyHeap = BinHeap (Z ** Empty)

-- implementation of Heap
public export
Heap BinaryHeap where

  empty = EmptyHeap

  isEmpty (BinHeap (Z ** _)) = True
  isEmpty (BinHeap _) = False

  push elem (BinHeap (n ** tree)) = BinHeap (S n ** insert elem tree)

  peek (BinHeap (n ** tree)) = findMin tree

  pop (BinHeap (Z ** Empty))  = (EmptyHeap, Nothing)
  pop (BinHeap (S n ** tree)) = let (tree', x) = popMin tree
                                in (BinHeap (n ** tree'), Just x)

  merge (BinHeap (n ** left)) (BinHeap (m ** right)) =
    BinHeap (n + m ** mergeTree left right)

  stats = const Nothing

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
> module Rel.TotalPreorderOperations

> import Rel.TotalPreorder

> %default total

> %access public export

> {-
> ||| R
> R : {A : Type} -> {R : A -> A -> Type} -> TotalPreorder R -> (A -> A -> Type)
> R (MkTotalPreorder R _ _ _) = R
> -}

> ||| reflexive
> reflexive : {A : Type} -> {R : A -> A -> Type} ->
>             TotalPreorder R ->
>             (x : A) -> R x x
> reflexive (MkTotalPreorder _ reflexive _ _) = reflexive

> ||| transitive
> transitive : {A : Type} -> {R : A -> A -> Type} ->
>              TotalPreorder R ->
>              (x : A) -> (y : A) -> (z : A) -> R x y -> R y z -> R x z
> transitive (MkTotalPreorder _ _ transitive _) = transitive

> ||| totalPre
> totalPre : {A : Type} -> {R : A -> A -> Type} ->
>            TotalPreorder R ->
>            (x : A) -> (y : A) -> Either (R x y) (R y x)
> totalPre (MkTotalPreorder _ _ _ totalPre) = totalPre

> |||
> extendRight : {A, B : Type} ->
>               (A -> A -> Type) -> ((A, B) -> (A, B) -> Type)
> extendRight R = \ x => \ y => R (fst x) (fst y)

> ||| |extendRight| preserves total preorders
> extendRightLemma : {A, B : Type} -> {R : A -> A -> Type} ->
>                    TotalPreorder R -> TotalPreorder (extendRight {A} {B} R)
> extendRightLemma {A} {B} {R} (MkTotalPreorder R reflexiveR transitiveR totalR) =
>   MkTotalPreorder S reflexiveS transitiveS totalS where
>     S           : (A, B) -> (A, B) -> Type
>     S           = extendRight R
>     reflexiveS  : (x : (A, B)) -> S x x
>     reflexiveS  = \ x => reflexiveR (fst x)
>     transitiveS : (x : (A, B)) -> (y : (A, B)) -> (z : (A, B)) -> S x y -> S y z -> S x z
>     transitiveS = \ x => \ y => \ z => \ xRy => \ yRz => transitiveR (fst x) (fst y) (fst z) xRy yRz
>     totalS      : (x : (A, B)) -> (y : (A, B)) -> Either (S x y) (S y x)
>     totalS      = \ x => \ y => totalR (fst x) (fst y)

> |||
> extendLeft : {A, B : Type} ->
>              (B -> B -> Type) -> ((A, B) -> (A, B) -> Type)
> extendLeft R = \ x => \ y => R (snd x) (snd y)

> ||| |extendRight| preserves total preorders
> extendLeftLemma : {A, B : Type} -> {R : B -> B -> Type} ->
>                   TotalPreorder R -> TotalPreorder (extendLeft {A} {B} R)
> extendLeftLemma {A} {B} {R} (MkTotalPreorder R reflexiveR transitiveR totalR) =
>   MkTotalPreorder S reflexiveS transitiveS totalS where
>     S           : (A, B) -> (A, B) -> Type
>     S           = extendLeft R
>     reflexiveS  : (x : (A, B)) -> S x x
>     reflexiveS  = \ x => reflexiveR (snd x)
>     transitiveS : (x : (A, B)) -> (y : (A, B)) -> (z : (A, B)) -> S x y -> S y z -> S x z
>     transitiveS = \ x => \ y => \ z => \ xRy => \ yRz => transitiveR (snd x) (snd y) (snd z) xRy yRz
>     totalS      : (x : (A, B)) -> (y : (A, B)) -> Either (S x y) (S y x)
>     totalS      = \ x => \ y => totalR (snd x) (snd y)

> {-

> ||| R
> R : {A : Type} -> TotalPreorder A -> (A -> A -> Type)
> R (MkTotalPreorder R _ _ _) = R

> ||| reflexive
> reflexive : {A : Type} ->
>             (tp : TotalPreorder A) ->
>             (x : A) -> (R tp) x x
> reflexive (MkTotalPreorder _ reflexive _ _) = reflexive

> ||| transitive
> transitive : {A : Type} ->
>              (tp : TotalPreorder A) ->
>              (x : A) -> (y : A) -> (z : A) -> (R tp) x y -> (R tp) y z -> (R tp) x z
> transitive (MkTotalPreorder _ _ transitive _) = transitive

> ||| totalPre
> totalPre : {A : Type} ->
>          (tp : TotalPreorder A) ->
>          (x : A) -> (y : A) -> Either ((R tp) x y) ((R tp) y x)
> totalPre (MkTotalPreorder _ _ _ totalPre) = totalPre

> ||| Total preorders on |A| induce total preorders on |(A, B)|
> fromTotalPreorder1 : {A, B : Type} -> TotalPreorder A -> TotalPreorder (A, B)
> fromTotalPreorder1 (MkTotalPreorder R reflexive transitive totalPre) =
>   MkTotalPreorder (\ x => \ y => R (fst x) (fst y))
>              (\ x => reflexive (fst x))
>              (\ x => \ y => \ z => \ xRy => \ yRz => transitive (fst x) (fst y) (fst z) xRy yRz)
>              (\ x => \ y => totalPre (fst x) (fst y))

> from2 : {A, B : Type} -> (B -> B -> Type) -> (A, B) -> (A, B) -> Type
> from2 R x y = R (snd x) (snd y)

> ||| Total preorders on |B| induce total preorders on |(A, B)|
> fromTotalPreorder2 : {A, B : Type} -> TotalPreorder B -> TotalPreorder (A, B)
> fromTotalPreorder2 to =
>   MkTotalPreorder (from2 (R to))
>                   (\ x => reflexive to (snd x))
>                   (\ x => \ y => \ z => \ xRy => \ yRz => transitive to (snd x) (snd y) (snd z) xRy yRz)
>                   (\ x => \ y => totalPre to (snd x) (snd y))

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)

%name Tree tree, tree1

insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node left val right) = case compare x val of
                                      LT => Node (insert x left) val right
                                      EQ => orig
                                      GT => Node left val (insert x right)


text:
module Text.WebIDL.Types

import public Data.List1
import public Data.SOP
import public Text.WebIDL.Types.Argument
import public Text.WebIDL.Types.Attribute
import public Text.WebIDL.Types.Definition
import public Text.WebIDL.Types.Err
import public Text.WebIDL.Types.Identifier
import public Text.WebIDL.Types.Member
import public Text.WebIDL.Types.Numbers
import public Text.WebIDL.Types.StringLit
import public Text.WebIDL.Types.Symbol
import public Text.WebIDL.Types.Token
import public Text.WebIDL.Types.Type


text:
import Data.Vect

{- 1 -}

readToBlank : IO (List String)
readToBlank = do x <- getLine
                 case x of
                      "" => pure []
                      _ => do rest <- readToBlank
                              pure (x :: rest)

{- 2 -}

readAndSave : IO ()
readAndSave = do lines <- readToBlank
                 putStr "Filename: "
                 f <- getLine
                 Right () <- writeFile f (unlines lines)
                     | Left err => putStrLn (show err)
                 pure ()

{- 3 -}

readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do Right h <- openFile filename Read
                               | Left err => pure (_ ** [])
                           Right contents <- readContents h
                               | Left err => pure (_ ** [])
                           closeFile h
                           pure contents
    where readContents : File -> IO (Either FileError (n ** Vect n String))
          readContents h = do eof <- fEOF h
                              if eof then pure (Right (_ ** [])) else do
                                 Right str <- fGetLine h
                                    | Left err => pure (Left err)
                                 Right (_ ** rest) <- readContents h
                                    | Left err => pure (Left err)
                                 pure (Right (_ ** str :: rest))

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module BioCore.Strand

import Data.List
import Data.Strings

%default total

--Strand--

public export
data Strand = Plus
            | Minus

public export
Eq Strand where
  (==) Plus Plus   = True
  (==) Minus Minus = True
  (==) _     _     = False
  (/=) x     y     = not (x == y)

----------

max_stars_repo_name: Matthew-Mosior/biocore-idris

max_issues_repo_name: Matthew-Mosior/biocore-idris

max_forks_repo_name: Matthew-Mosior/biocore-idris


text:
-- ---------------------------------------------------------------- [ Date.idr ]
-- Module  : Data.Date
-- Description : Simple data types and helper functions to represent dates.
--
-- License : This code is distributed under the MIT license. See the
--           file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Data.Date

%access public export

-- -------------------------------------------------------------- [ Data Types ]

||| A day of the week.
data Day = Monday
         | Tuesday
         | Wednesday
         | Thursday
         | Friday
         | Saturday
         | Sunday

%name Day day, day1, day2

||| A month of the year.
data Month = January
           | February
           | March
           | April
           | May
           | June
           | July
           | August
           | September
           | October
           | November
           | December

%name Month month, month1, month2

-- ------------------------------------------------------ [ Eq Implementations ]

Eq Day where
  Monday    == Monday    = True
  Tuesday   == Tuesday   = True
  Wednesday == Wednesday = True
  Thursday  == Thursday  = True
  Friday    == Friday    = True
  Saturday  == Saturday  = True
  Sunday    == Sunday    = True
  _         == _         = False

Eq Month where
  January   == January   = True
  February  == February  = True
  March     == March     = True
  April     == April     = True
  May       == May       = True
  June      == June      = True
  July      == July      = True
  August    == August    = True
  September == September = True
  October   == October   = True
  November  == November  = True
  December  == December  = True
  _         == _         = False

-- ---------------------------------------------------- [ Show Implementations ]

Show Day where
  show Monday    = "Monday"
  show Tuesday   = "Tuesday"
  show Wednesday = "Wednesday"
  show Thursday  = "Thursday"
  show Friday    = "Friday"
  show Saturday  = "Saturday"
  show Sunday    = "Sunday"

Show Month where
  show January   = "January"
  show February  = "February"
  show March     = "March"
  show April     = "April"
  show May       = "May"
  show June      = "June"
  show July      = "July"
  show August    = "August"
  show September = "September"
  show October   = "October"
  show November  = "November"
  show December  = "December"

-- -------------------------------------------------------- [ Helper Functions ]

namespace Days
  ||| Convert a string to a day, if possible, otherwise return `Nothing`.
  ||| @ str A string representing a day.
  fromString : (str : String) -> Maybe Day
  fromString "Monday"    = Just Monday
  fromString "Tuesday"   = Just Tuesday
  fromString "Wednesday" = Just Wednesday
  fromString "Thursday"  = Just Thursday
  fromString "Friday"    = Just Friday
  fromString "Saturday"  = Just Saturday
  fromString "Sunday"    = Just Sunday
  fromString _           = Nothing

namespace Months
  ||| Convert a string to a month, if possible, otherwise return `Nothing`.
  ||| @ str A string representing a month.
  fromString : (str : String) -> Maybe Month
  fromString "January"   = Just January
  fromString "February"  = Just February
  fromString "March"     = Just March
  fromString "April"     = Just April
  fromString "May"       = Just May
  fromString "June"      = Just June
  fromString "July"      = Just July
  fromString "August"    = Just August
  fromString "September" = Just September
  fromString "October"   = Just October
  fromString "November"  = Just November
  fromString "December"  = Just December
  fromString _           = Nothing

-- -------------------------------------------------------------------- [ Date ]

||| A date consists of a day, month, date and year.
record Date where
    ||| Make a date.
    constructor MkDate
    ||| A day.
    DDay  : Day
    ||| A month.
    DMon  : Month
    ||| A date.
    DDate : Integer -- Fin 32
    ||| A year.
    DYear : Integer
    -- TODO: data Time where ...

implementation Show Date where
    show (MkDate day month date year) =
        concat $ List.intersperse ", " [ show day
                                       , show month ++ " " ++ show date
                                       , show year ]

implementation Eq Date where
    (MkDate dayA monthA dateA yearA) == (MkDate dayB monthB dateB yearB) =
        dayA   == dayB   &&
        monthA == monthB &&
        dateA  == dateB  &&
        yearA  == yearB

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

max_stars_repo_name: yurrriq/my-clippings

max_issues_repo_name: yurrriq/my-clippings

max_forks_repo_name: yurrriq/my-clippings


text:
-- --------------------------------------------------------------- [ Model.idr ]
-- Module      : UML.Sequence.Model
-- Description : A model for sequence diagrams.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Sequence.Model

import UML.Code.Model

%access public

data ElemTy = MODEL | STEP | SEND | LOOP | SWITCH | CHOICE

data OkElem : ElemTy -> Type where
  OkSend : OkElem SEND
  OkLoop : OkElem LOOP
  OkSwitch  : OkElem SWITCH

data SequenceModel : ElemTy -> Type where
  ||| Construct a step.
  |||
  ||| @from The sending entity.
  ||| @to The receiving entity.
  ||| @ms The messages being sent.
  Send : (from : String)
       -> (to : String)
       -> (ms : List (String, String)) -> SequenceModel SEND
  Choice : (condition : String)
         -> (List (SequenceModel SEND))
         -> SequenceModel CHOICE
  Loop : (condition : String)
       -> (List (SequenceModel SEND))
       -> SequenceModel LOOP
  Opt  : SequenceModel CHOICE
       -> SequenceModel CHOICE
       -> SequenceModel SWITCH
  Alt  : List (SequenceModel CHOICE) -> SequenceModel SWITCH
  Nil  : SequenceModel STEP
  (::) : (SequenceModel a)
       -> {auto prf : OkElem a}
       -> SequenceModel STEP
       -> SequenceModel STEP
  MkSeqModel : List DType -> SequenceModel STEP -> SequenceModel MODEL

mkStep : List (SequenceModel a) -> {auto prf : OkElem a} -> SequenceModel STEP
mkStep Nil       = Model.Nil
mkStep (x :: xs) = Model.(::) x (mkStep xs)
-- ---------------------------------------------------------------------- [ Eq ]

instance Eq ElemTy where
  (==) MODEL  MODEL  = True
  (==) STEP   STEP   = True
  (==) SEND   SEND   = True
  (==) LOOP   LOOP   = True
  (==) SWITCH SWITCH = True
  (==) CHOICE CHOICE = True
  (==) _      _      = False

mutual

  %assert_total
  eqSeqModel : (SequenceModel a) -> (SequenceModel b) -> Bool
  eqSeqModel (Send af at as)  (Send bf bt bs)  = af == bf && at == bt && as == bs
  eqSeqModel (Choice a as)    (Choice b bs)    = a == b && as == bs
  eqSeqModel (Loop a as)      (Loop b bs)      = a == b && as == bs
  eqSeqModel (Opt ax ay)      (Opt bx by)      = ax == bx && ay == by
  eqSeqModel (Alt as)         (Alt bs)         = as == bs
  eqSeqModel Nil              Nil              = True
  eqSeqModel (x::xs)          (y::ys)          = eqSeqModel x y && eqSeqModel xs ys
  eqSeqModel (MkSeqModel x a) (MkSeqModel y b) = a == b && x == y
  eqSeqModel _                _                = False

  instance Eq (SequenceModel x) where
    (==) = eqSeqModel

-- -------------------------------------------------------------------- [ Show ]

instance Show ElemTy where
  show MODEL  = "MODEL"
  show STEP   = "STEP"
  show SEND   = "SEND"
  show LOOP   = "LOOP"
  show SWITCH = "SWITCH"
  show CHOICE = "CHOICE"

instance Show (SequenceModel x) where
  show (Send a b ms) = unwords ["[", a, "->", b, ":", show ms, "]\n"]
  show (Choice d ss) = unwords ["[Choice ", show d, "[", show ss, "]", "]\n"]
  show (Loop d ss)   = unwords ["[Loop ", show d, "[", show ss, "]", "]\n"]
  show (Opt x y)     = unwords ["[Opt ", show x, show y, "]\n"]
  show (Alt as)      = unwords ["[Alt ", show as, " ]\n"]
  show Nil           = ""
  show (x::xs)       = unwords ["[Steps ", showXS (x::xs), "]\n"]
    where
      showXS : SequenceModel STEP -> String
      showXS (x::xs) = show x ++ "," ++ showXS xs
  show (MkSeqModel ds m) = unwords ["[Seq ", show ds, show m, "]\n"]

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

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module GRIN.GrinState

import Data.List
import Data.SortedMap
import Data.SortedSet as Set

import GRIN.AST
import GRIN.Error
import GRIN.Analysis.MaxVar

public export
0 CallGraph : Type -> Type
CallGraph name = SortedMap name (SortedSet name)

public export
record GrinState name where
    constructor MkGrinState
    prog : Prog name
    calls : Maybe (CallGraph name)
    calledBy : Maybe (CallGraph name)
    toInline : SortedMap name (Def name) -- should have all fetch ids removed
    errors : List Error
    varMap : SortedMap Var Var
    nextVar : Var

export
getErrors : GrinState name -> List Error
getErrors = reverse . errors

export
newGrinState : Ord name => Prog name -> GrinState name
newGrinState prog = MkGrinState
    { prog
    , calls = Nothing
    , calledBy = Nothing
    , toInline = empty
    , errors = []
    , varMap = empty
    , nextVar = incVar $ maxVar prog
    }

public export
data AnalysisTag
    = CallsGraph
    | CalledByGraph
    | CallGraphs


text:
module Debug.Trace

import Prelude
import PrimIO

export
trace : (msg : String) -> (result : a) -> a
trace x val = unsafePerformIO (do putStrLn x; pure val)


text:
module Protocol.IDE.Result

import Protocol.SExp

import Protocol.IDE.Holes
import Protocol.IDE.FileContext

import Data.Maybe

%default total

public export
data OptionType = BOOL | STRING | ATOM

public export
(.sem) : OptionType -> Type
BOOL   .sem = Bool
STRING .sem = String
ATOM   .sem = String

%unbound_implicits off
public export
record REPLOption where
  constructor MkOption
  name : String
  type : OptionType
  val  : type.sem
%unbound_implicits on

sexpOptionVal : {type : OptionType} -> type.sem -> SExp
sexpOptionVal {type = BOOL  } = toSExp
sexpOptionVal {type = STRING} = toSExp
sexpOptionVal {type = ATOM  } = toSExp

export
SExpable REPLOption where
  toSExp opt@(MkOption {}) = SExpList
    [ SymbolAtom opt.name
    , sexpOptionVal opt.val
    ]

export
FromSExpable REPLOption where
  fromSExp (SExpList
    [ SymbolAtom name
    , val
    ]) = do
    let Nothing = fromSExp val
      | Just val => Just $ MkOption {name, type = BOOL, val}
    let Nothing = fromSExp val
      | Just val => Just $ MkOption {name, type = STRING, val}
    val <- fromSExp val
    Just $ MkOption {name, type = ATOM, val}
  fromSExp _ = Nothing

public export
record MetaVarLemma where
  constructor MkMetaVarLemma
  application, lemma : String

export
SExpable MetaVarLemma where
  toSExp mvl =  SExpList [ SymbolAtom "metavariable-lemma"
             , SExpList [ SymbolAtom "replace-metavariable", StringAtom mvl.application ]
             , SExpList [ SymbolAtom "definition-type", StringAtom mvl.lemma ]
             ]

export
FromSExpable MetaVarLemma where
  fromSExp (SExpList [ SymbolAtom "metavariable-lemma"
             , SExpList [ SymbolAtom "replace-metavariable", StringAtom application ]
             , SExpList [ SymbolAtom "definition-type", StringAtom lemma ]
             ]) = Just $ MkMetaVarLemma {application, lemma}
  fromSExp _ = Nothing

public export
record IdrisVersion where
  constructor MkIdrisVersion
  major, minor, patch : Nat
  tag : Maybe String

export
SExpable IdrisVersion where
  toSExp version = SExpList
    [ SExpList (map toSExp [version.major, version.minor, version.patch])
    , SExpList [StringAtom $ fromMaybe "" version.tag]
    ]

export
FromSExpable IdrisVersion where
  fromSExp (SExpList
    [ SExpList [majorSExp, minorSExp, patchSExp]
    , SExpList [StringAtom tagSExp]
    ]) = do pure $ MkIdrisVersion
              { major = !(fromSExp majorSExp)
              , minor = !(fromSExp minorSExp)
              , patch = !(fromSExp patchSExp)
              , tag = case tagSExp of
                  "" => Nothing
                  str => Just str}
  fromSExp _ = Nothing

public export
data Result =
    AString String
  | AUnit
  | AVersion IdrisVersion
  | AMetaVarLemma MetaVarLemma
  | ANameLocList (List (String, FileContext))
  | AHoleList (List HoleData)
  | ANameList (List String)
  | AnOptionList (List REPLOption)

export
SExpable Result where
  toSExp (AString s) = toSExp s
  toSExp (AUnit    ) = toSExp (the (List Int) [])
  toSExp (AVersion version) = toSExp version
  toSExp (AMetaVarLemma mvl) = toSExp mvl
  toSExp (ANameLocList fcs) = toSExp fcs
  toSExp (AHoleList holes) = toSExp holes
  toSExp (ANameList names) = SExpList (map SymbolAtom names)
  toSExp (AnOptionList opts) = toSExp opts

-- This code is not efficient. Usually the client knows what kind of
-- result to expect based on the request it issued.
export
FromSExpable Result where
  fromSExp (SExpList []) = Just AUnit -- resolve ambiguity somewhat arbitrarily...
  fromSExp sexp = do
  let Nothing = fromSExp sexp
    | Just str => pure $ AString str
  let Nothing = fromSExp sexp
    | Just version => pure $ AVersion version
  let Nothing = fromSExp sexp
    | Just mvl => pure $ AMetaVarLemma mvl
  let Nothing = fromSExp sexp
    | Just nll => pure $ ANameLocList nll
  let Nothing = fromSExp sexp
    | Just hl => pure $ AHoleList hl
  let Nothing = fromSExp sexp
    | Just nl => pure $ ANameList nl
  let Nothing = fromSExp sexp
    | Just optl => pure $ AnOptionList optl
  Nothing


text:
module Language.LSP.Message.Registration

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

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_registerCapability
public export
record Registration where
  constructor MkRegistration
  id              : String
  method          : String
  registerOptions : Maybe JSON
%runElab deriveJSON defaultOpts `{{Registration}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_registerCapability
public export
record RegistrationParams where
  constructor MkRegistrationParams
  registrations : List Registration
%runElab deriveJSON defaultOpts `{{RegistrationParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_unregisterCapability
public export
record Unregistration where
  constructor MkUnregistration
  id     : String
  method : String
%runElab deriveJSON defaultOpts `{{Unregistration}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#client_unregisterCapability
public export
record UnregistrationParams where
  constructor MkUnregistrationParams
  -- NOTE: not my typo, but see the specification link in the record documentation
  unregisterations : List Unregistration
%runElab deriveJSON defaultOpts `{{UnregistrationParams}}


text:
module Sub06Apply36x9

import ProofColDivSeqBase
import ProofColDivSeqPostulate
import ProofColDivSeqPostuProof

%default total
-- %language ElabReflection

-- 3(12x+3) --E[2,-4]--> 3x
export
apply36x9 : (Not . P) (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l))))))
  -> (m : Nat ** (LTE (S m) (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l)))))), (Not . P) m))
apply36x9 {l} col = (l ** (lte36x9 l, e36x9To3x l col)) where
  lte36x9 : (l:Nat) -> LTE (S l) (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l))))))
  lte36x9 Z = (lteSuccRight . lteSuccRight . LTESucc) LTEZero
  lte36x9 (S l) = let lemma = lte36x9 l in
    rewrite (sym (plusSuccRightSucc l l)) in
    rewrite (sym (plusSuccRightSucc (plus l l) (S (plus l l)))) in
    rewrite (sym (plusSuccRightSucc (plus l l) (plus l l))) in
    rewrite (sym (plusSuccRightSucc (plus (plus l l) (plus l l))  (S (S (S (plus (plus l l) (plus l l))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus l l) (plus l l))  (S (S (plus (plus l l) (plus l l)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus l l) (plus l l))  (S (plus (plus l l) (plus l l))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus l l) (plus l l))  (plus (plus l l) (plus l l)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))  (S (S (S (plus (plus l l) (plus l l))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))  (S (S (plus (plus l l) (plus l l)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))  (S (plus (plus l l) (plus l l))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))  (plus (plus l l) (plus l l)))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc) lemma


text:
||| Properties of Data.Vect.map
module Data.Vect.Properties.Map

import Data.Vect.Properties.Tabulate
import Data.Vect.Properties.Index
import Data.Vect.Properties.Foldr

import Data.Vect
import Data.Vect.Elem
import Data.Fin
import Data.Vect.Extra

import Syntax.PreorderReasoning

||| `map` functoriality: identity preservation
export
mapId : (xs : Vect n a) -> map Prelude.id xs = xs
mapId xs = vectorExtensionality _ _ $ \i => indexNaturality _ _ _

||| `mapWtihPos f` represents post-composition the tabulated function `f`
export
indexMapWithPos : (f : Fin n -> a -> b) -> (xs : Vect n a) -> (i : Fin n)
  -> index i (mapWithPos f xs) = f i (index i xs)
indexMapWithPos f (x :: _ )  FZ    = Refl
indexMapWithPos f (_ :: xs) (FS i) = indexMapWithPos _ _ _

||| `tabulate : (Fin n ->) -> Vect n` is a natural transformation
export
mapTabulate : (f : a -> b) -> (g : Fin n -> a)
  -> tabulate (f . g) = map f (tabulate g)
mapTabulate f g = irrelevantEq $
  vectorExtensionality _ _ $ \i => Calc $
  |~ index i (tabulate (f . g))
  ~~ f (g i)                      ...(indexTabulate _ _)
  ~~ f (index i $ tabulate g)     ...(cong f (sym $ indexTabulate _ _))
  ~~ index i (map f $ tabulate g) ...(sym $ indexNaturality _ _ _)

||| Tabulating with the constant function is replication
export
tabulateConstantly : (x : a) -> Fin.tabulate {len} (const x) === replicate len  x
tabulateConstantly x = irrelevantEq $
  vectorExtensionality _ _ $ \i => Calc $
  |~ index i (Fin.tabulate (const x))
  ~~ x ...(indexTabulate _ _)
  ~~ index i (replicate _ x) ...(sym $ indexReplicate _ _)

||| It's enough that two functions agree on the elements of a vector for the maps to agree
export
mapRestrictedExtensional : (f, g : a -> b) -> (xs : Vect n a)
  -> (prf : (i : Fin n) -> f (index i xs) = g (index i xs))
  -> map f xs = map g xs
mapRestrictedExtensional f g xs prf = vectorExtensionality _ _ $ \i => Calc $
  |~ index i (map f xs)
  ~~ f (index i xs)     ...(      indexNaturality _ _ _)
  ~~ g (index i xs)     ...(prf _)
  ~~ index i (map g xs) ...(sym $ indexNaturality _ _ _)

||| function extensionality is a congruence wrt map
export
mapExtensional : (f, g : a -> b)
  -> (prf : (x : a) -> f x = g x)
  -> (xs : Vect n a)
  -> map f xs = map g xs
mapExtensional f g prf xs = mapRestrictedExtensional f g xs (\i => prf (index i xs))

||| map-fusion property for vectors up to function extensionality
export
mapFusion : (f : b -> c) -> (g : a -> b) -> (xs : Vect n a)
  -> map f (map g xs) = map (f . g) xs
mapFusion f g    []     = Refl
mapFusion f g (x :: xs) = cong (f $ g x ::) $ mapFusion f g xs

||| function extensionality is a congruence wrt mapWithElem
export
mapWithElemExtensional : (xs : Vect n a) -> (f, g :  (x : a) -> (0 _ : x `Elem` xs) -> b)
  -> ((x : a) -> (0 pos : x `Elem` xs) -> f x pos = g x pos)
  -> mapWithElem xs f = mapWithElem xs g
mapWithElemExtensional    []     f g prf = Refl
mapWithElemExtensional (x :: xs) f g prf
  = cong2 (::) (prf x Here)
               (mapWithElemExtensional xs _ _ (\x,pos => prf x (There pos)))


text:
module Main

main : IO ()
main = putStrLn "Hello from Lazy Idris!"

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

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

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


text:
module Idris.Doc.String

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.TT
import Core.TT.Traversals

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

import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Elab.Prim

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

import Libraries.Data.ANameMap
import Libraries.Data.NameMap
import Libraries.Data.SortedSet
import Libraries.Data.SortedMap
import Libraries.Data.StringMap as S
import Libraries.Data.String.Extra

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

import Parser.Lexer.Source

import public Idris.Doc.Annotations
import Idris.Doc.Keywords

%default covering

-- Add a doc string for a module name
export
addModDocString : {auto s : Ref Syn SyntaxInfo} ->
                  ModuleIdent -> String ->
                  Core ()
addModDocString mi doc
    = do syn <- get Syn
         put Syn ({ saveMod $= (mi ::)
                  , modDocstrings $= insert mi doc } syn)

-- Add a doc string for a name in the current namespace
export
addDocString : {auto c : Ref Ctxt Defs} ->
               {auto s : Ref Syn SyntaxInfo} ->
               Name -> String ->
               Core ()
addDocString n_in doc
    = do n <- inCurrentNS n_in
         log "doc.record" 50 $
           "Adding doc for " ++ show n_in ++ " (aka " ++ show n ++ " in current NS)"
         syn <- get Syn
         put Syn ({ defDocstrings $= addName n doc,
                    saveDocstrings $= insert n () } syn)

-- Add a doc string for a name, in an extended namespace (e.g. for
-- record getters)
export
addDocStringNS : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 Namespace -> Name -> String ->
                 Core ()
addDocStringNS ns n_in doc
    = do n <- inCurrentNS n_in
         let n' = case n of
                       NS old root => NS (old <.> ns) root
                       root => NS ns root
         syn <- get Syn
         put Syn ({ defDocstrings $= addName n' doc,
                    saveDocstrings $= insert n' () } syn)

prettyTerm : IPTerm -> Doc IdrisDocAnn
prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm

prettyName : Name -> Doc IdrisDocAnn
prettyName n =
  case userNameRoot n of
    -- shouldn't happen: we only show UN anyways...
    Nothing => pretty (nameRoot n)
    Just un => if isOpUserName un then parens (pretty un) else pretty un

prettyKindedName : Maybe String -> Doc IdrisDocAnn -> Doc IdrisDocAnn
prettyKindedName Nothing   nm = nm
prettyKindedName (Just kw) nm
  = annotate (Syntax Keyword) (pretty kw) <++> nm

||| Look up implementations
getImplDocs : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              (keep : Term [] -> Core Bool) ->
              Core (List (Doc IdrisDocAnn))
getImplDocs keep
    = do defs <- get Ctxt
         docss <- for (concat $ values $ typeHints defs) $ \ (impl, _) =>
           do Just def <- lookupCtxtExact impl (gamma defs)
                | _ => pure []
              -- Only keep things that look like implementations.
              -- i.e. get rid of data constructors
              let Just Func = defNameType (definition def)
                | _ => pure []
              -- Check that the type mentions the name of interest
              ty <- toFullNames !(normaliseHoles defs [] (type def))
              True <- keep ty
                | False => pure []
              ty <- resugar [] ty
              pure [annotate (Decl impl) $ prettyTerm ty]
         pure $ case concat docss of
           [] => []
           [doc] => [header "Hint" <++> annotate Declarations doc]
           docs  => [vcat [header "Hints"
                    , annotate Declarations $
                        vcat $ map (indent 2) docs]]

||| Look up implementations corresponding to the named type
getHintsForType : {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
                  Name -> Core (List (Doc IdrisDocAnn))
getHintsForType nty
    = do log "doc.data" 10 $ "Looking at \{show nty}"
         getImplDocs $ \ ty =>
           do let nms = allGlobals ty
              log "doc.data" 10 $ String.unlines
                [ "Candidate: " ++ show ty
                , "Containing names: " ++ show nms
                ]
              pure $ isJust (lookup nty nms)

||| Look up implementations corresponding to the primitive type
getHintsForPrimitive : {auto c : Ref Ctxt Defs} ->
                       {auto s : Ref Syn SyntaxInfo} ->
                       Constant -> Core (List (Doc IdrisDocAnn))
getHintsForPrimitive c
    = do log "doc.data" 10 $ "Looking at \{show c}"
         getImplDocs $ \ ty =>
           do let nms = allConstants ty
              log "doc.data" 10 $ String.unlines
                [ "Candidate: " ++ show ty
                , "Containing constants: " ++ show nms
                ]
              pure $ contains c nms

export
getDocsForPrimitive : {auto c : Ref Ctxt Defs} ->
                      {auto s : Ref Syn SyntaxInfo} ->
                      Constant -> Core (Doc IdrisDocAnn)
getDocsForPrimitive constant = do
    let (_, type) = checkPrim EmptyFC constant
    let typeString = prettyTerm (PPrimVal EmptyFC constant)
                     <++> colon
                     <++> prettyTerm !(resugar [] type)
    hintsDoc <- getHintsForPrimitive constant
    pure $ vcat $ typeString
               :: indent 2 (primDoc constant)
               :: hintsDoc

  where
  primDoc : Constant -> Doc IdrisDocAnn
  primDoc (I i) = "Primitive signed int value (backend-dependent precision)"
  primDoc (I8 i) = "Primitive signed 8 bits value"
  primDoc (I16 i) = "Primitive signed 16 bits value"
  primDoc (I32 i) = "Primitive signed 32 bits value"
  primDoc (I64 i) = "Primitive signed 64 bits value"
  primDoc (BI i) = "Primitive unsigned int value (backend-dependent precision)"
  primDoc (B8 i) = "Primitive unsigned 8 bits value"
  primDoc (B16 i) = "Primitive unsigned 16 bits value"
  primDoc (B32 i) = "Primitive unsigned 32 bits value"
  primDoc (B64 i) = "Primitive unsigned 64 bits value"
  primDoc (Str s) = "Primitive string value"
  primDoc (Ch c) = "Primitive character value"
  primDoc (Db d) = "Primitive double value"
  primDoc WorldVal = "Primitive token for IO actions"

  primDoc IntType = "Primitive type of bounded signed integers (backend dependent size)"
  primDoc Int8Type = "Primitive type of 8 bits signed integers"
  primDoc Int16Type = "Primitive type of 16 bits signed integers"
  primDoc Int32Type = "Primitive type of 32 bits signed integers"
  primDoc Int64Type = "Primitive type of 64 bits signed integers"
  primDoc IntegerType = "Primitive type of unbounded signed integers"
  primDoc Bits8Type = "Primitive type of 8 bits unsigned integers"
  primDoc Bits16Type = "Primitive type of 16 bits unsigned integers"
  primDoc Bits32Type = "Primitive type of 32 bits unsigned integers"
  primDoc Bits64Type = "Primitive type of 64 bits unsigned integers"
  primDoc StringType = "Primitive type of strings"
  primDoc CharType = "Primitive type of characters"
  primDoc DoubleType = "Primitive type of double-precision floating-points"
  primDoc WorldType = "Primitive type of tokens for IO actions"

public export
data Config : Type where
  ||| Configuration of the printer for a name
  ||| @ showType    Do we show the type?
  ||| @ longNames   Do we print qualified names?
  ||| @ dropFirst   Do we drop the first argument in the type?
  ||| @ getTotality Do we print the totality status of the function?
  MkConfig : {default True  showType    : Bool} ->
             {default True  longNames   : Bool} ->
             {default False dropFirst   : Bool} ->
             {default True  getTotality : Bool} ->
             Config

||| Printer configuration for interface methods
||| * longNames turned off for interface methods because the namespace is
|||             already spelt out for the interface itself
||| * dropFirst turned on for interface methods because the first argument
|||             is always the interface constraint
||| * totality  turned off for interface methods because the methods themselves
|||             are just projections out of a record and so are total
export
methodsConfig : Config
methodsConfig
  = MkConfig {showType = True}
             {longNames = False}
             {dropFirst = True}
             {getTotality = False}

export
shortNamesConfig : Config
shortNamesConfig
  = MkConfig {showType = True}
             {longNames = False}
             {dropFirst = False}
             {getTotality = True}

export
justUserDoc : Config
justUserDoc
  = MkConfig {showType = False}
             {longNames = False}
             {dropFirst = True}
             {getTotality = False}

export
getDocsForName : {auto o : Ref ROpts REPLOpts} ->
                 {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 FC -> Name -> Config -> Core (Doc IdrisDocAnn)
getDocsForName fc n config
    = do syn <- get Syn
         defs <- get Ctxt
         let extra = case nameRoot n of
                       "-" => [NS numNS (UN $ Basic "negate")]
                       _ => []
         resolved <- lookupCtxtName n (gamma defs)
         let all@(_ :: _) = extra ++ map fst resolved
             | _ => undefinedName fc n
         let ns@(_ :: _) = concatMap (\n => lookupName n (defDocstrings syn)) all
             | [] => pure emptyDoc
         docs <- traverse (showDoc config) ns
         pure $ vcat docs
  where

    showDoc : Config -> (Name, String) -> Core (Doc IdrisDocAnn)

    -- Avoid generating too much whitespace by not returning a single empty line
    reflowDoc : String -> List (Doc IdrisDocAnn)
    reflowDoc "" = []
    reflowDoc str = map (indent 2 . reflow) (forget $ Extra.lines str)

    showTotal : Name -> Totality -> Doc IdrisDocAnn
    showTotal n tot
        = case isTerminating tot of
               Unchecked => ""
               _ => header "Totality" <++> pretty tot

    getDConDoc : Name -> Core (Doc IdrisDocAnn)
    getDConDoc con
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact con (gamma defs)
                  -- should never happen, since we know that the DCon exists:
                  | Nothing => pure Empty
             syn <- get Syn
             ty <- resugar [] =<< normaliseHoles defs [] (type def)
             let conWithTypeDoc = annotate (Decl con) (hsep [dCon con (prettyName con), colon, prettyTerm ty])
             case lookupName con (defDocstrings syn) of
               [(n, "")] => pure conWithTypeDoc
               [(n, str)] => pure $ vcat
                    [ conWithTypeDoc
                    , annotate DocStringBody
                    $ annotate UserDocString
                    $ vcat $ reflowDoc str
                    ]
               _ => pure conWithTypeDoc

    ||| The name corresponds to an implementation, typeset its type accordingly
    getImplDoc : Name -> Core (List (Doc IdrisDocAnn))
    getImplDoc n
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure []
             ty <- resugar [] =<< normaliseHoles defs [] (type def)
             pure [annotate (Decl n) $ prettyTerm ty]

    getMethDoc : Method -> Core (List (Doc IdrisDocAnn))
    getMethDoc meth
        = do syn <- get Syn
             let [nstr] = lookupName meth.name (defDocstrings syn)
                  | _ => pure []
             pure <$> showDoc methodsConfig nstr

    getInfixDoc : Name -> Core (List (Doc IdrisDocAnn))
    getInfixDoc n
        = do let Just (Basic n) = userNameRoot n
                    | _ => pure []
             let Just (fixity, assoc) = S.lookup n (infixes !(get Syn))
                    | Nothing => pure []
             pure $ pure $ hsep
                  [ pretty (show fixity)
                  , "operator,"
                  , "level"
                  , pretty (show assoc)
                  ]

    getPrefixDoc : Name -> Core (List (Doc IdrisDocAnn))
    getPrefixDoc n
        = do let Just (Basic n) = userNameRoot n
                    | _ => pure []
             let Just assoc = S.lookup n (prefixes !(get Syn))
                    | Nothing => pure []
             pure $ ["prefix operator, level" <++> pretty (show assoc)]

    getFixityDoc : Name -> Core (List (Doc IdrisDocAnn))
    getFixityDoc n =
      pure $ case toList !(getInfixDoc n) ++ toList !(getPrefixDoc n) of
        []  => []
        [f] => [header "Fixity Declaration" <++> f]
        fs  => [header "Fixity Declarations" <+> Line <+>
                 indent 2 (vcat fs)]

    getIFaceDoc : (Name, IFaceInfo) -> Core (Doc IdrisDocAnn)
    getIFaceDoc (n, iface)
        = do let params =
                case params iface of
                     [] => []
                     ps => [hsep (header "Parameters" :: punctuate comma (map (pretty . show) ps))]
             let constraints =
                case !(traverse (pterm . map defaultKindedName) (parents iface)) of
                     [] => []
                     ps => [hsep (header "Constraints" :: punctuate comma (map (pretty . show) ps))]
             let icon = case dropNS (iconstructor iface) of
                          DN _ _ => [] -- machine inserted
                          nm => [hsep [header "Constructor", dCon nm (prettyName nm)]]
             mdocs <- traverse getMethDoc (methods iface)
             let meths = case concat mdocs of
                           [] => []
                           docs => [vcat [header "Methods", annotate Declarations $ vcat $ map (indent 2) docs]]
             sd <- getSearchData fc False n
             idocs <- case hintGroups sd of
                           [] => pure (the (List (List (Doc IdrisDocAnn))) [])
                           ((_, tophs) :: _) => traverse getImplDoc tophs
             let insts = case concat idocs of
                           [] => []
                           [doc] => [header "Implementation" <++> annotate Declarations doc]
                           docs => [vcat [header "Implementations"
                                   , annotate Declarations $ vcat $ map (indent 2) docs]]
             pure (vcat (params ++ constraints ++ icon ++ meths ++ insts))

    getFieldDoc : Name -> Core (Doc IdrisDocAnn)
    getFieldDoc nm
      = do syn <- get Syn
           defs <- get Ctxt
           Just def <- lookupCtxtExact nm (gamma defs)
                -- should never happen, since we know that the DCon exists:
                | Nothing => pure Empty
           ty <- resugar [] =<< normaliseHoles defs [] (type def)
           let prettyName = prettyName nm
           let projDecl = annotate (Decl nm) $ hsep [ fun nm prettyName, colon, prettyTerm ty ]
           case lookupName nm (defDocstrings syn) of
                [(_, "")] => pure projDecl
                [(_, str)] =>
                  pure $ vcat [ projDecl
                              , annotate DocStringBody
                              $ annotate UserDocString
                              $ vcat $ reflowDoc str
                              ]
                _ => pure projDecl

    getFieldsDoc : Name -> Core (Maybe (Doc IdrisDocAnn))
    getFieldsDoc recName
      = do let (Just ns, n) = displayName recName
               | _ => pure Nothing
           let recNS = ns <.> mkNamespace n
           defs <- get Ctxt
           let fields = getFieldNames (gamma defs) recNS
           syn <- get Syn
           case fields of
             [] => pure Nothing
             [proj] => pure $ Just $ header "Projection" <++> annotate Declarations !(getFieldDoc proj)
             projs => pure $ Just $ vcat
                           [ header "Projections"
                           , annotate Declarations $ vcat $
                               map (indent 2) $ !(traverse getFieldDoc projs)
                           ]

    getExtra : Name -> GlobalDef -> Core (Maybe String, List (Doc IdrisDocAnn))
    getExtra n d = do
      do syn <- get Syn
         let [] = lookupName n (ifaces syn)
             | [ifacedata] => (Just "interface",) . pure <$> getIFaceDoc ifacedata
             | _ => pure (Nothing, []) -- shouldn't happen, we've resolved ambiguity by now
         case definition d of
           PMDef _ _ _ _ _ => pure (Nothing, [showTotal n (totality d)])
           TCon _ _ _ _ _ _ cons _ =>
             do let tot = [showTotal n (totality d)]
                cdocs <- traverse (getDConDoc <=< toFullNames) cons
                cdoc <- case cdocs of
                  [] => pure (Just "data", [])
                  [doc] =>
                    let cdoc = header "Constructor" <++> annotate Declarations doc in
                    case !(getFieldsDoc n) of
                      Nothing => pure (Just "data", [cdoc])
                      Just fs => pure (Just "record", cdoc :: [fs])
                  docs => pure (Just "data"
                               , [vcat [header "Constructors"
                                       , annotate Declarations $
                                           vcat $ map (indent 2) docs]])
                idoc <- getHintsForType n
                pure (map (\ cons => tot ++ cons ++ idoc) cdoc)
           _ => pure (Nothing, [])

    showDoc (MkConfig {showType, longNames, dropFirst, getTotality}) (n, str)
        = do defs <- get Ctxt
             Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => undefinedName fc n
             -- First get the extra stuff because this also tells us whether a
             -- definition is `data`, `record`, or `interface`.
             (typ, extra) <- ifThenElse getTotality
                               (getExtra n def)
                               (pure (Nothing, []))

             -- Then form the type declaration
             ty <- resugar [] =<< normaliseHoles defs [] (type def)
             -- when printing e.g. interface methods there is no point in
             -- repeating the interface's name
             let ty = ifThenElse (not dropFirst) ty $ case ty of
                        PPi _ _ AutoImplicit _ _ sc => sc
                        _ => ty
             nm <- aliasName n
             -- when printing e.g. interface methods there is no point in
             -- repeating the namespace the interface lives in
             let cat = showCategory Syntax def
             let nm = prettyKindedName typ $ cat
                    $ ifThenElse longNames (pretty (show nm)) (prettyName nm)
             let deprecated = if Deprecate `elem` def.flags
                                 then annotate Deprecation "=DEPRECATED=" <+> line else emptyDoc
             let docDecl = deprecated <+> annotate (Decl n) (hsep [nm, colon, prettyTerm ty])

             -- Finally add the user-provided docstring
             let docText = let docs = reflowDoc str in
                           annotate UserDocString (vcat docs)
                           <$ guard (not $ null docs)
             fixes <- getFixityDoc n
             let docBody =
                  let docs = maybe id (::) docText
                           $ map (indent 2) (extra ++ fixes)
                  in annotate DocStringBody
                     (concatWith (\l, r => l <+> hardline <+> r) docs)
                     <$ guard (not (null docs))
             let maybeDocDecl = [docDecl | showType]
             pure . vcat . catMaybes $ maybeDocDecl :: (map Just $ docBody)

export
getDocsForPTerm : {auto o : Ref ROpts REPLOpts} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
                  PTerm -> Core (Doc IdrisDocAnn)
getDocsForPTerm (PRef fc name) = getDocsForName fc name MkConfig
getDocsForPTerm (PPrimVal _ c) = getDocsForPrimitive c
getDocsForPTerm (PType _) = pure $ vcat
  [ "Type : Type"
  , indent 2 "The type of all types is Type. The type of Type is Type."
  ]
getDocsForPTerm (PString _ _) = pure $ vcat
  [ "String Literal"
  , indent 2 "Desugars to a fromString call"
  ]
getDocsForPTerm (PList _ _ _) = pure $ vcat
  [ "List Literal"
  , indent 2 "Desugars to (::) and Nil"
  ]
getDocsForPTerm (PSnocList _ _ _) = pure $ vcat
  [ "SnocList Literal"
  , indent 2 "Desugars to (:<) and Lin"
  ]
getDocsForPTerm (PPair _ _ _) = pure $ vcat
  [ "Pair Literal"
  , indent 2 "Desugars to MkPair or Pair"
  ]
getDocsForPTerm (PDPair _ _ _ _ _) = pure $ vcat
  [ "Dependant Pair Literal"
  , indent 2 "Desugars to MkDPair or DPair"
  ]
getDocsForPTerm (PUnit _) = pure $ vcat
  [ "Unit Literal"
  , indent 2 "Desugars to MkUnit or Unit"
  ]
getDocsForPTerm pterm = pure $
  "Docs not implemented for" <++> pretty (show pterm) <++> "yet"

export
getDocs : {auto o : Ref ROpts REPLOpts} ->
          {auto c : Ref Ctxt Defs} ->
          {auto s : Ref Syn SyntaxInfo} ->
          DocDirective -> Core (Doc IdrisDocAnn)
getDocs (APTerm ptm) = getDocsForPTerm ptm
getDocs (Symbol k) = pure $ getDocsForSymbol k
getDocs (Keyword k) = pure $ getDocsForKeyword k

summarise : {auto c : Ref Ctxt Defs} ->
            {auto s : Ref Syn SyntaxInfo} ->
            Name -> Core (Doc IdrisDocAnn)
summarise n -- n is fully qualified
    = do syn <- get Syn
         defs <- get Ctxt
         Just def <- lookupCtxtExact n (gamma defs)
             | _ => pure ""
         ty <- normaliseHoles defs [] (type def)
         pure $ showCategory Syntax def (prettyName n)
              <++> colon <++> hang 0 (prettyTerm !(resugar [] ty))

-- Display all the exported names in the given namespace
export
getContents : {auto o : Ref ROpts REPLOpts} ->
              {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Namespace -> Core (Doc IdrisDocAnn)
getContents ns
   = -- Get all the names, filter by any that match the given namespace
     -- and are visible, then display with their type
     do defs <- get Ctxt
        ns <- allNames (gamma defs)
        let allNs = filter inNS ns
        allNs <- filterM (visible defs) allNs
        vsep <$> traverse summarise (sort allNs)
  where
    visible : Defs -> Name -> Core Bool
    visible defs n
        = do Just def <- lookupCtxtExact n (gamma defs)
                  | Nothing => pure False
             pure (visibility def /= Private)

    inNS : Name -> Bool
    inNS (NS xns (UN _)) = ns `isParentOf` xns
    inNS _ = False


text:
module Idris.REPL.Common

import Core.Context.Log
import Core.Directory
import Core.Env
import Core.InitPrimitives
import Core.Metadata
import Core.Primitives
import Core.TT
import Core.Unify
import Core.UnifyState

import Idris.Doc.String
import Idris.Error
import Idris.IDEMode.Commands
import Idris.IDEMode.Holes
import Idris.Pretty
import public Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Idris.Version

import Libraries.Data.ANameMap
import Libraries.Text.PrettyPrint.Prettyprinter

import Data.List
import Data.String
import System.File

%default covering

||| Output informational messages, unless suppressed by a flag.
||| This function should only be called with informational
||| messages, an unhandled error is an example of what should
||| *not* end up here.
export
iputStrLn : {auto c : Ref Ctxt Defs} ->
            {auto o : Ref ROpts REPLOpts} ->
            Doc IdrisAnn -> Core ()
iputStrLn msg
    = do opts <- get ROpts
         case idemode opts of
              REPL InfoLvl  => coreLift $ putStrLn !(render msg)
              -- output silenced
              REPL _ => pure ()
              IDEMode i _ f =>
                send f (SExpList [SymbolAtom "write-string",
                                 toSExp !(renderWithoutColor msg), toSExp i])

||| Sampled against `VerbosityLvl`.
public export
data MsgStatus = MsgStatusNone | MsgStatusError | MsgStatusInfo

doPrint : MsgStatus -> VerbosityLvl -> Bool
doPrint MsgStatusNone  InfoLvl  = True
doPrint MsgStatusNone  ErrorLvl = True
doPrint MsgStatusNone  NoneLvl  = True
doPrint MsgStatusError InfoLvl  = True
doPrint MsgStatusError ErrorLvl = True
doPrint MsgStatusError NoneLvl  = False
doPrint MsgStatusInfo  InfoLvl  = True
doPrint MsgStatusInfo  ErrorLvl = False
doPrint MsgStatusInfo  NoneLvl  = False

printWithStatus : {auto o : Ref ROpts REPLOpts} ->
                  (Doc ann -> Core String) ->
                  (Doc ann -> MsgStatus -> Core ())
printWithStatus render msg status
  = do opts <- get ROpts
       case idemode opts of
         REPL verbosityLvl =>
           case doPrint status verbosityLvl of
             True   => coreLift $ putStrLn !(render msg)
             False  => pure ()
         IDEMode {} => pure () -- this function should never be called in IDE Mode

||| Print REPL result.
export
printResult : {auto o : Ref ROpts REPLOpts} ->
              Doc IdrisAnn -> Core ()
printResult x = printWithStatus render x MsgStatusNone
 --                                      ^^^^^^^^^^^^^
 -- "results" are printed no matter the verbosity level

||| Print REPL result.
export
printDocResult : {auto o : Ref ROpts REPLOpts} ->
                 Doc IdrisDocAnn -> Core ()
printDocResult x = printWithStatus (render styleAnn) x MsgStatusNone
 --                                                    ^^^^^^^^^^^^^
 -- "results" are printed no matter the verbosity level

-- Return that a protocol request failed somehow
export
printError : {auto o : Ref ROpts REPLOpts} ->
             Doc IdrisAnn -> Core ()
printError msg = printWithStatus render msg MsgStatusError

DocCreator : Type -> Type
DocCreator a = a -> Core (Doc IdrisAnn)

export
emitProblem : {auto c : Ref Ctxt Defs} ->
            {auto o : Ref ROpts REPLOpts} ->
            {auto s : Ref Syn SyntaxInfo} ->
            a -> (DocCreator a) -> (DocCreator a) -> (a -> Maybe FC) -> MsgStatus -> Core ()
emitProblem a replDocCreator idemodeDocCreator getFC status
    = do opts <- get ROpts
         case idemode opts of
              REPL _ =>
                  do msg <- replDocCreator a
                     printWithStatus render msg status
              IDEMode i _ f =>
                  do msg <- idemodeDocCreator a
                     -- TODO: Display a better message when the error doesn't contain a location
                     case map toNonEmptyFC (getFC a) of
                          Nothing => iputStrLn msg
                          Just (origin, startPos, endPos) => do
                            fname <- case origin of
                              PhysicalIdrSrc ident => do
                                -- recover the file name relative to the working directory.
                                -- (This is what idris2-mode expects)
                                let fc = MkFC (PhysicalIdrSrc ident) startPos endPos
                                catch (nsToSource fc ident) (const $ pure "(File-Not-Found)")
                              PhysicalPkgSrc fname =>
                                pure fname
                              Virtual Interactive =>
                                pure "(Interactive)"
                            send f (SExpList [SymbolAtom "warning",
                                   SExpList [toSExp {a = String} fname,
                                            toSExp (addOne startPos),
                                              toSExp (addOne endPos),
                                              toSExp !(renderWithoutColor msg),
                                              -- highlighting; currently blank
                                              SExpList []],
                                    toSExp i])
  where
    addOne : (Int, Int) -> (Int, Int)
    addOne (l, c) = (l + 1, c + 1)

-- Display an error message from checking a source file
export
emitError : {auto c : Ref Ctxt Defs} ->
            {auto o : Ref ROpts REPLOpts} ->
            {auto s : Ref Syn SyntaxInfo} ->
            Error -> Core ()
emitError e = emitProblem e display perror getErrorLoc MsgStatusError

export
emitWarning : {auto c : Ref Ctxt Defs} ->
              {auto o : Ref ROpts REPLOpts} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Warning -> Core ()
emitWarning w = emitProblem w displayWarning pwarning getWarningLoc MsgStatusInfo

export
emitWarnings : {auto c : Ref Ctxt Defs} ->
               {auto o : Ref ROpts REPLOpts} ->
               {auto s : Ref Syn SyntaxInfo} ->
               Core (List Error)
emitWarnings
    = do defs <- get Ctxt
         let ws = reverse (warnings defs)
         session <- getSession
         if (session.warningsAsErrors)
           then let errs = WarningAsError <$> ws in
                errs <$ traverse_ emitError errs
           else [] <$ traverse_ emitWarning ws

export
emitWarningsAndErrors : {auto c : Ref Ctxt Defs} ->
                        {auto o : Ref ROpts REPLOpts} ->
                        {auto s : Ref Syn SyntaxInfo} ->
                        List Error -> Core (List Error)
emitWarningsAndErrors errs = do
  ws <- emitWarnings
  traverse_ emitError errs
  pure ws

getFCLine : FC -> Maybe Int
getFCLine = map startLine . isNonEmptyFC

export
updateErrorLine : {auto o : Ref ROpts REPLOpts} ->
                  List Error -> Core ()
updateErrorLine []
    = do opts <- get ROpts
         put ROpts (record { errorLine = Nothing } opts)
updateErrorLine (e :: _)
    = do opts <- get ROpts
         put ROpts (record { errorLine = (getErrorLoc e) >>= getFCLine } opts)

export
resetContext : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto m : Ref MD Metadata} ->
               (origin : OriginDesc) ->
               Core ()
resetContext origin
    = do defs <- get Ctxt
         put Ctxt (record { options = clearNames (options defs) } !initDefs)
         addPrimitives
         put UST initUState
         put Syn initSyntax
         put MD (initMetadata origin)

public export
data EditResult : Type where
  DisplayEdit : Doc IdrisAnn -> EditResult
  EditError : Doc IdrisAnn -> EditResult
  MadeLemma : Maybe String -> Name -> IPTerm -> String -> EditResult
  MadeWith : Maybe String -> List String -> EditResult
  MadeCase : Maybe String -> List String -> EditResult

public export
data MissedResult : Type where
  CasesMissing : Name -> List String  -> MissedResult
  CallsNonCovering : Name -> List Name -> MissedResult
  AllCasesCovered : Name -> MissedResult

public export
data REPLResult : Type where
  Done : REPLResult
  REPLError : Doc IdrisAnn -> REPLResult
  Executed : PTerm -> REPLResult
  RequestedHelp : REPLResult
  Evaluated : IPTerm -> Maybe IPTerm -> REPLResult
  Printed : Doc IdrisAnn -> REPLResult
  PrintedDoc : Doc IdrisDocAnn -> REPLResult
  TermChecked : IPTerm -> IPTerm -> REPLResult
  FileLoaded : String -> REPLResult
  ModuleLoaded : String -> REPLResult
  ErrorLoadingModule : String -> Error -> REPLResult
  ErrorLoadingFile : String -> FileError -> REPLResult
  ErrorsBuildingFile : String -> List Error -> REPLResult
  NoFileLoaded : REPLResult
  CurrentDirectory : String -> REPLResult
  CompilationFailed: REPLResult
  Compiled : String -> REPLResult
  ProofFound : IPTerm -> REPLResult
  Missed : List MissedResult -> REPLResult
  CheckedTotal : List (Name, Totality) -> REPLResult
  FoundHoles : List HoleData -> REPLResult
  OptionsSet : List REPLOpt -> REPLResult
  LogLevelSet : Maybe LogLevel -> REPLResult
  ConsoleWidthSet : Maybe Nat -> REPLResult
  ColorSet : Bool -> REPLResult
  VersionIs : Version -> REPLResult
  DefDeclared : REPLResult
  Exited : REPLResult
  Edited : EditResult -> REPLResult

prettyTerm : IPTerm -> Doc IdrisDocAnn
prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm

export
docsOrSignature : {auto o : Ref ROpts REPLOpts} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto s : Ref Syn SyntaxInfo} ->
                  FC -> Name -> Core (Doc IdrisDocAnn)
docsOrSignature fc n
    = do syn  <- get Syn
         defs <- get Ctxt
         all@(_ :: _) <- lookupCtxtName n (gamma defs)
             | _ => undefinedName fc n
         let ns@(_ :: _) = concatMap (\n => lookupName n (defDocstrings syn))
                                     (map fst all)
             | [] => typeSummary defs
         getDocsForName fc n MkConfig
  where
    typeSummary : Defs -> Core (Doc IdrisDocAnn)
    typeSummary defs = do Just def <- lookupCtxtExact n (gamma defs)
                            | Nothing => pure ""
                          ty <- resugar [] !(normaliseHoles defs [] (type def))
                          pure $ pretty n <++> ":" <++> prettyTerm ty

export
equivTypes : {auto c : Ref Ctxt Defs} ->
             (ty1 : ClosedTerm) ->
             (ty2 : ClosedTerm) ->
             Core Bool
equivTypes ty1 ty2 =
  do let False = isErased ty1
          | _ => pure False
     logTerm "typesearch.equiv" 10 "Candidate: " ty1
     defs <- get Ctxt
     True <- pure (!(getArity defs [] ty1) == !(getArity defs [] ty2))
       | False => pure False
     _ <- newRef UST initUState
     b <- catch
           (do res <- unify inTerm EmptyFC [] ty1 ty2
               case res of
                 (MkUnifyResult [] _ [] NoLazy) => pure True
                 _ => pure False)
           (\err => pure False)
     when b $ logTerm "typesearch.equiv" 20 "Accepted: " ty1
     pure b