text:
-- ----------------------------------------------------------------- [ DOM.idr ]
-- Module      : XML.DOM
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
--
--
-- --------------------------------------------------------------------- [ EOH ]
module XML.DOM

import public Data.DList
import public Data.PList
import public Commons.Text.Display

%access export
%default total

public export
data NodeTy = DOCUMENT | ELEMENT | TEXT | CDATA | INSTRUCTION | COMMENT | QNAME | INFO | IDENT | DOCTYPE

Eq NodeTy where
  (==) DOCUMENT    DOCUMENT    = True
  (==) ELEMENT     ELEMENT     = True
  (==) TEXT        TEXT        = True
  (==) CDATA       CDATA       = True
  (==) INSTRUCTION INSTRUCTION = True
  (==) COMMENT     COMMENT     = True
  (==) QNAME       QNAME       = True
  (==) INFO        INFO        = True
  (==) IDENT       IDENT       = True
  (==) DOCTYPE     DOCTYPE     = True
  (==) _ _ = False

public export
data ValidNode : NodeTy -> Type where
  ValidElem  : ValidNode ELEMENT
  ValidCData : ValidNode CDATA
  ValidText  : ValidNode TEXT
  ValidDoc   : ValidNode COMMENT
  ValidInstr : ValidNode INSTRUCTION

data Document : NodeTy -> Type where
  MkDocument : (info         : Document INFO)
            -> (doctype      : Maybe $ Document DOCTYPE)
            -> (instructions : List (Document INSTRUCTION))
            -> (comment      : Maybe (Document COMMENT))
            -> (root         : Document ELEMENT)
            -> Document DOCUMENT

  XMLInfo : (version : String)
         -> (encoding : String)
         -> (standalone : Bool)
         -> Document INFO

  DocType : (name : String)
         -> (ident : Maybe $ Document IDENT)
         -> Document DOCTYPE

  SystemID : (ident : String) -> Document IDENT
  PublicID : (ident : String) -> (ident_sys : String) -> Document IDENT

  QName : (name : String)
       -> (nspace : Maybe String)
       -> (nprefix : Maybe String)
       -> Document QNAME

  Element : (qName      : Document QNAME)
         -> (attributes : List (Document QNAME, String))
         -> (children   : PList NodeTy Document ValidNode ts prfs)
         -> Document ELEMENT

  Comment : (comment : String) -> Document COMMENT

  Text : (text : String) -> Document TEXT

  CData : (cdata : String) -> Document CDATA

  Instruction : (name : String)
             -> (attributes : List (String, String))
             -> Document INSTRUCTION

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

private
maybeEq : (Document a -> Document b -> Bool)
       -> Maybe (Document a)
       -> Maybe (Document b)
       -> Bool
maybeEq _ Nothing  Nothing  = True
maybeEq f (Just x) (Just y) = f x y
maybeEq _ _        _        = False

partial
eqDoc : Document a -> Document b -> Bool
eqDoc (MkDocument iA dA inA cA rA) (MkDocument iB dB inB cB rB) =
         eqDoc iA iB
      && maybeEq eqDoc dA dB
      && (and (zipWith (\x, y => eqDoc x y) inA inB))
      && maybeEq eqDoc cA cB
      && eqDoc rA rB

eqDoc (XMLInfo vA eA sA) (XMLInfo vB eB sB) = vA == vB && eA == eB && sA == sB

eqDoc (DocType nA iA) (DocType nB iB) = nA == nB && maybeEq eqDoc iA iB

eqDoc (SystemID x) (SystemID y) = x == y

eqDoc (PublicID x xloc) (PublicID y yloc) = x == y && xloc == yloc

eqDoc (QName x xs _) (QName y ys _) = x == y && xs == ys

eqDoc (Element nA aA cA) (Element nB aB cB) =
        eqDoc nA nB
     && (and (zipWith (\(a,b), (x,y) => eqDoc a x && b == y) aA aB))
     && eqPList eqDoc cA cB

eqDoc (Comment a) (Comment b) = a == b

eqDoc (Text a) (Text b) = a == b
eqDoc (CData a) (CData b) = a == b
eqDoc (Instruction at ad) (Instruction bt bd) = at == bt && ad == ad
eqDoc _ _ = False

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

partial
Show (Document a) where
  show (MkDocument info doctype instructions comment root) =
      unwords ["[MkDocument"
              , show info
              , show doctype
              , show instructions
              , show comment
              , show root
              ,"]"
              ]
  show (XMLInfo version encoding standalone) =
      unwords ["[XMLInfo"
              , show version
              , show encoding
              , show standalone
              , "]"
              ]
  show (DocType name ident) =
      unwords ["[DocType"
              , show name
              , show ident
              , "]"
              ]
  show (SystemID ident) = unwords ["SystemID", show ident]

  show (PublicID ident loc) = unwords ["PublicID", show ident, show loc]

  show (QName name nspace nprefix) =
      unwords ["[QName"
              , show name
              , show nspace
              , show nprefix
              , "]"
              ]

  show (Element qName attributes children) =
       unwords ["[Element "
               , show qName
               , show attributes
               , showPList show children
               , "]"
               ]

  show (Comment comment) = unwords ["[Comment ", show comment, "]"]
  show (Text text) = unwords ["[Text", show text, "]"]
  show (CData cdata) = unwords ["[CData", show cdata, "]"]

  show (Instruction name attributes) =
       unwords ["[Instruction"
               , show name
               , show attributes
               ,"]"
               ]

partial
displayDoc : Document a -> String
displayDoc (MkDocument info doctype instructions comment root) =
    unwords ["[MkDocument"
            , displayDoc info
            , maybe "" displayDoc doctype
            , unwords $ Functor.map displayDoc instructions
            , maybe "" displayDoc comment
            , displayDoc root
            ,"]"
            ]
displayDoc (XMLInfo version encoding standalone) =
    unwords ["<?xml"
            , concat ["version=", show version]
            , concat ["encoding=", show encoding]
--            , concat ["standalone=", show standalone
            , "?>"
            ]
displayDoc (DocType name ident) =
    unwords ["<!DOCTYPE"
            , name
            , maybe "" displayDoc ident
            , ">"
            ]
displayDoc (SystemID ident) = ident

displayDoc (PublicID ident loc) = unwords [display ident, display loc]

displayDoc (QName name nspace nprefix) =
    concat [maybe "" display nspace
           , if isJust nspace then ":" else ""
           , display name
           ]

displayDoc (Element qName attributes Nil) =
         concat [ "<"
                , displayDoc qName
                , unwords $ Functor.map (\(k,v) => concat [displayDoc k, "=", show v]) attributes
                , "/>"
                ]

displayDoc (Element qName attributes children) =
         concat ["[Element "
                , "<", displayDoc qName, ">"
                , unwords $ Functor.map (\(k,v) => concat [displayDoc k, "=", show v]) attributes
                , concat $ map displayDoc children
                ,"</", displayDoc qName, ">"
                ]

displayDoc (Comment comment) = unwords ["<!--", comment, "-->"]
displayDoc (Text text) = text
displayDoc (CData cdata) = unwords ["<![CData[", cdata, "]]>"]

displayDoc (Instruction name attributes) =
     unwords ["<?"
             , name
             , show attributes
             ,"?>"
             ]

Display (Document a) where
  display d = assert_total $ displayDoc d -- nasty hack
-- -------------------------------------------------------------------- [ Misc ]

getDocElemTy : {a : NodeTy} -> Document a -> NodeTy
getDocElemTy {a} _ = a

public export
NodeList : (types : List NodeTy)
        -> (prfs  : DList NodeTy ValidNode types)
        -> Type
NodeList = PList NodeTy Document ValidNode
-- --------------------------------------------------------------------- [ API ]

setRoot : Document ELEMENT -> Document DOCUMENT -> Document DOCUMENT
setRoot newe (MkDocument info dtype ins doc e) = MkDocument info dtype ins doc newe

getRoot : Document DOCUMENT -> Document ELEMENT
getRoot (MkDocument info doctype instructions comment root) = root

mkXMLInfo : String -> String -> Bool -> Document INFO
mkXMLInfo = XMLInfo

defaultXMLInfo : Document INFO
defaultXMLInfo = mkXMLInfo "1.2" "UTF-8" True

emptyNodeList : PList NodeTy Document ValidNode Nil Nil
emptyNodeList = Nil

mkSystemID : String -> Document IDENT
mkSystemID = SystemID

mkPublicID : String -> String -> Document IDENT
mkPublicID = PublicID

-- [ DocTypes ]

mkDocType : String -> Maybe (Document IDENT) -> Document DOCTYPE
mkDocType = DocType

-- ------------------------------------------------------------- [ DOM Objects ]

-- ------------------------------------------------------------------ [ QNames ]

mkQName : String -> Maybe String -> Maybe String -> Document QNAME
mkQName = QName

namespace Simple

    ||| Create a local name
    mkQName : String -> Document QNAME
    mkQName n = QName n Nothing Nothing

||| Create a qualified name with a name space
|||
||| @n The name
||| @ns   The name space.
mkQNameNS : (n : String) -> (ns : String) -> Document QNAME
mkQNameNS n ns = QName n (Just ns) Nothing

||| Create a tag with a name and a prefix
|||
||| @n The name
||| @pre The prefix
mkQNamePrefix : (n : String) -> (pre : String) -> Document QNAME
mkQNamePrefix n pre = QName n Nothing (Just pre)

||| Create a tag with namespace and prefix.
|||
||| @n The name
||| @pre The prefix.
||| @ns The namespace
mkQNameNSPrefix : (n : String) -> (pre : String) -> (ns : String) -> Document QNAME
mkQNameNSPrefix n pre ns = QName n (Just ns) (Just pre)

||| Create a prefixed qualified name, intended for use with
||| attributes.
mkAttrNamePrefix : String -> String -> Document QNAME
mkAttrNamePrefix n pre = QName n Nothing (Just pre)

setNameSpace : Maybe String -> Document QNAME -> Document QNAME
setNameSpace s (QName n _ pre) = QName n s pre

-- ---------------------------------------------------------------- [ Elements ]

||| Create a element with a local qualified name.
mkSimpleElement : String -> Document ELEMENT
mkSimpleElement name = Element tag Nil Nil
  where
   tag : Document QNAME
   tag = mkQName name

||| Create a element with a Namespace.
|||
||| @n The name
||| @ns The namespace
mkElementNS : (n : String) -> (ns : String) -> Document ELEMENT
mkElementNS n ns = Element tag Nil Nil
  where
    tag = mkQNameNS n ns

||| Create an element with a prefix
|||
||| @n The name
||| @pre The prefix.
mkElementPrefix : (n : String) -> (pre : String) -> Document ELEMENT
mkElementPrefix n p = Element (mkQNamePrefix n p) Nil Nil

||| Create an element with a namespace and a prefix
|||
||| @n The name
||| @pre The prefix.
||| @ns The namespace
mkElementNSPrefix : (n : String)
                 -> (pre : String)
                 -> (ns : String)
                 -> Document ELEMENT
mkElementNSPrefix n pre ns = Element (mkQNameNSPrefix n pre ns) Nil Nil

||| Create a key value pair
mkAttribute : String -> String -> (Document QNAME, String)
mkAttribute k v = (mkQName k, v)

mkAttributePrefix : String -> String -> String -> (Document QNAME, String)
mkAttributePrefix k p v = (mkQNamePrefix k p, v)

||| Creates a Document with an empty root node
mkEmptyDocument : Document QNAME -> Maybe (Document DOCTYPE) -> Document DOCUMENT
mkEmptyDocument n dtd =
  MkDocument defaultXMLInfo
             dtd
             Nil
             Nothing
             (Element n Nil emptyNodeList)

mkSimpleDocument : Document ELEMENT -> Document DOCUMENT
mkSimpleDocument root = MkDocument (defaultXMLInfo) Nothing Nil Nothing root

mkDocument : (info         : Document INFO)
          -> (doctype      : Maybe $ Document DOCTYPE)
          -> (instructions : List (Document INSTRUCTION))
          -> (comment      : Maybe (Document COMMENT))
          -> (root         : Document ELEMENT)
          -> Document DOCUMENT
mkDocument = MkDocument

-- ----------------------------------------------------------- [ Node Creation ]

||| Create an XML Comment
mkComment : String -> Document COMMENT
mkComment = Comment

mkCData : String -> Document CDATA
mkCData = CData

mkText : String -> Document TEXT
mkText = Text

mkInstruction : String -> List (String, String) -> Document INSTRUCTION
mkInstruction = Instruction

mkEmptyElement : Document QNAME -> List (Document QNAME, String) -> Document ELEMENT
mkEmptyElement n as = Element n as Nil

mkElement : Document QNAME -> List (Document QNAME, String) -> NodeList ts prfs -> Document ELEMENT
mkElement = Element

-- -------------------------------------------------------------- [ Attributes ]

getAttrName : (Document QNAME, String) -> String
getAttrName (QName n ns prefix', v) = n

getAttrPrefix : (Document QNAME, String) -> Maybe String
getAttrPrefix (QName n ns prefix', v) = prefix'

getAttrValue : (Document QNAME, String) -> String
getAttrValue (k,v) = v

-- --------------------------------------------------------------- [ Accessors ]

||| Get the attributes of the node
getAttributes : (node : Document a )
             -> {auto prf : ValidNode a}
             -> List (Document QNAME, String)
getAttributes (Element x xs y) {prf=ValidElem} = xs
getAttributes node {prf} = Nil

||| Does node have attributes
hasAttributes : Document a
             -> {auto prf : ValidNode a}
             -> Bool
hasAttributes n {prf} = isCons (getAttributes n {prf=prf})

||| Get the children
getNodes : Document a
        -> {auto prf : ValidNode a}
        -> (ts ** prfs ** NodeList ts prfs)
getNodes (Element x xs ys) {prf=ValidElem} = (_ ** _ ** ys)
getNodes x {prf}                           = ([] ** [] ** [])

||| Does element have child nodes
hasNodes : Document a
        -> {auto prf : ValidNode a}
        -> Bool
hasNodes n = let (ts ** prfs ** nodes) = getNodes n
              in isCons nodes

||| Get node name
||| http://docs.oracle.com/javase/7/docs/api/org/w3c/dom/Node.html
getNodeName : Document a
           -> {auto prf : ValidNode a}
           -> String
getNodeName (Element (QName name nspace nprefix) xs y)   {prf = ValidElem}  = name
getNodeName (CData x)          {prf = ValidCData} = "#cdata-section"
getNodeName (Text x)           {prf = ValidText}  = "#text"
getNodeName (Comment x)        {prf = ValidDoc}   = "#comment"
getNodeName (Instruction x xs) {prf = ValidInstr} = x

||| Return the element's value
getNodeValue : Document a
            -> {auto prf : ValidNode a}
            -> Maybe String
getNodeValue x {prf = ValidElem} = Nothing
getNodeValue (CData x) {prf = ValidCData} = Just x
getNodeValue (Text x) {prf = ValidText} = Just x
getNodeValue (Comment x) {prf = ValidDoc} = Just x
getNodeValue (Instruction x xs) {prf = ValidInstr} =
  Just $ unwords $ Functor.map show xs

getTag : Document ELEMENT -> Document QNAME
getTag (Element n _ _) = n

||| Get tag name
getTagName : Document ELEMENT -> String
getTagName (Element (QName name nspace nprefix) _ _) = name

||| Return an element's prefix
getTagPrefix : Document ELEMENT -> Maybe String
getTagPrefix (Element (QName name nspace nprefix) _ _) = nprefix

||| Return an element's namespace
getTagNS : Document ELEMENT -> Maybe String
getTagNS (Element (QName name nspace nprefix) _ _ ) = nspace

||| Get value for a given attribute
getAttribute : String -> Document ELEMENT -> Maybe String
getAttribute key (Element x xs y) =
    lookupBy cmpQName (mkQName key) xs
  where
    cmpQName (QName a _ _) (QName b _ _) = a == b

||| Remove first occurance of attribute.
removeAttribute : String -> Document ELEMENT -> Document ELEMENT
removeAttribute key (Element n as ns) = Element n attrs' ns
  where
    cmpQNameKVPair : (Document QNAME, String)
                  -> (Document QNAME, String)
                  -> Bool
    cmpQNameKVPair (QName a _ _, b) (QName x _ _, y) = a == x

    attrs' : List (Document QNAME, String)
    attrs' = deleteBy cmpQNameKVPair
                      (mkQName key, "")
                      (as)

||| Set first occurance of atttribute to new value.
setAttribute : (key : String)
            -> (value : String)
            -> Document ELEMENT
            -> Document ELEMENT
setAttribute k v e@(Element n as ns) = Element n (newAS e) ns
  where
    newAS : Document ELEMENT -> List (Document QNAME, String)
    newAS e = mkAttribute k v :: getAttributes (removeAttribute k e)

-- ------------------------------------------------------------- [ Element Ops ]

ContainsChild : (child : Document a)
             -> (node  : NodeList ts prfs)
             -> (prfI : Elem a ts)
             -> (prfP : DElem NodeTy ValidNode prf prfs prfI)
             -> Type
ContainsChild c n prfI prfP {a} {prf} =
  Elem NodeTy Document ValidNode a c prf n prfI prfP

data HasElem : (elem : Document a)
            -> (prf : ValidNode a)
            -> (node : Document ELEMENT)
            -> Type
  where
    HasElemProof : (prf : ContainsChild elem children prfI prfP)
                -> HasElem elem vnode (Element n as children)

infixl 2 <++> -- Append Child
infixl 2 <--> -- Remove Child
infixl 2 <=>  -- Add Text Node
infixl 2 <+=> -- Create and add text node

private
appendToNode : Document a
            -> Document ELEMENT
            -> (prf : ValidNode a)
            -> Document ELEMENT
appendToNode c (Element n as ns) prf = Element n as (add c ns)

private
removeFromNodeList : (elem : Document a)
                  -> (nodes : NodeList ts prfs)
                  -> {auto idx  : Elem a ts}
                  -> {auto vprf : DElem NodeTy ValidNode prf prfs idx}
                  -> NodeList (dropElem ts idx) (dropElem prfs vprf)
removeFromNodeList elem nodes {idx} {vprf} = delete' elem nodes idx vprf

private
removeFromNode : (elem : Document a)
              -> (node : Document ELEMENT)
              -> (vnode : ValidNode a)
              -> (prf : HasElem elem vnode node)
              -> Document ELEMENT
removeFromNode c (Element n as ns {ts = ts}) vnode (HasElemProof prf) =
   Element n as (dropElem ns prf)

||| Set Value
addText : String -> Document ELEMENT -> Document ELEMENT
addText s e = appendToNode (Text s) e ValidText

--  -------------------------------------------------------------------- [ Ops ]

||| Append
(<++>) : Document ELEMENT
       -> Document a
       -> {auto prf : ValidNode a}
       -> Document ELEMENT
(<++>) p c {prf} = appendToNode c p prf

||| Remove
(<-->) : (node : Document ELEMENT)
      -> (elem : Document a)
      -> {auto prfV : ValidNode a}
      -> {auto prfN : HasElem elem prfV node}
      -> Document ELEMENT
(<-->) p c {prfV} {prfN} = removeFromNode c p prfV prfN

||| Add text value
(<=>) : Document ELEMENT -> String -> Document ELEMENT
(<=>) e s = e <++> (Text s)

||| Create and add text value
(<+=>) : String -> String -> Document ELEMENT
(<+=>) n v = (mkSimpleElement n) <=> v

-- ------------------------------------------------------------ [ Node Queries ]

namespace NodeList
  ||| getElements
  getElements : NodeList ts prfs
             -> List $ Document ELEMENT
  getElements [] = []
  getElements ((::) elem {prf = ValidElem} rest) = elem :: getElements rest
  getElements ((::) elem {prf} rest) = getElements rest

  getText : NodeList ts prfs
         -> List $ Document TEXT
  getText [] = []
  getText ((::) elem {prf = ValidText} rest) = elem :: getText rest
  getText ((::) elem {prf} rest) = getText rest

  getComments : NodeList ts prfs
             -> List $ Document COMMENT
  getComments Nil = Nil
  getComments ((::) elem {prf = ValidDoc} rest) = elem :: getComments rest
  getComments ((::) elem {prf} rest)            = getComments rest

  getCData : NodeList ts prfs -> List $ Document CDATA
  getCData Nil = Nil
  getCData ((::) elem {prf = ValidCData} rest) = elem :: getCData rest
  getCData ((::) elem {prf} rest)              = getCData rest

getElements : Document ELEMENT -> List $ Document ELEMENT
getElements (Element _ _ ns) = getElements ns

getText : Document ELEMENT -> List $ Document TEXT
getText (Element _ _ ns) = getText ns

getComments : Document ELEMENT -> List $ Document COMMENT
getComments (Element _ _ ns) = getComments ns

getCData : Document ELEMENT -> List $ Document CDATA
getCData (Element _ _ ns) = getCData ns

-- --------------------------------------------------------- [ Element Queries ]

public export
data CanQuery : NodeTy -> Type where
  QueryDoc  : CanQuery DOCUMENT
  QueryElem : CanQuery ELEMENT

||| Get the immediate child elements
getChildElements : Document a -> {auto prf : CanQuery a} -> List $ Document ELEMENT
getChildElements (Element _ _ ns) {prf=QueryElem} = getElements ns
getChildElements (MkDocument x y xs z (Element _ _ ns)) {prf=QueryDoc}  = getElements ns

private
doTest : (eqFunc : Document QNAME -> Document QNAME -> Bool)
      -> (name   : Document QNAME)
      -> (node   : Document ELEMENT)
      -> Maybe (Document ELEMENT)
doTest eqFunc name node@(Element n attrs children) =
  if eqFunc name n
    then Just node
    else Nothing

private partial
getAllElements : (node : Document ELEMENT)
              -> List $ Document ELEMENT
getAllElements node@(Element x as Nil) = node :: Nil
getAllElements node@(Element x as xs)  = node :: concatMap getAllElements (getElements xs)

private
getElementsBy' : (func : Document ELEMENT -> Bool)
              -> (node : Document a)
              -> (prf  : CanQuery a)
              -> List (Document ELEMENT)
getElementsBy' func (MkDocument x y xs z w) QueryDoc = filter func (assert_total $ getAllElements w)
getElementsBy' func node QueryElem = filter func (assert_total $ getAllElements node)

getElementsBy : (func : Document ELEMENT -> Bool)
             -> (node : Document a)
             -> {auto prf : CanQuery a}
             -> List (Document ELEMENT)
getElementsBy func node {prf} = getElementsBy' func node prf

||| Get all Elements with a given QName
getElementsByQName : Document QNAME
                  -> Document a
                  -> {auto prf : CanQuery a}
                  -> List $ Document ELEMENT
getElementsByQName (QName x ns p) node = getElementsBy (\(Element (QName y _ _) as xs) => x == y) node
-- change tp ==

||| Get all Elements with a given name. This ignores prefixes and namespaces.
getElementsByName : String
                 -> Document a
                 -> {auto prf : CanQuery a}
                 -> List $ Document ELEMENT
getElementsByName naam e = getElementsBy (\(Element (QName x _ _) _ _) => naam == x) e

||| Get All Child Elements with a given QName.
getChildElementsByQName : Document QNAME
                       -> Document a
                       -> {auto prf : CanQuery a}
                       -> List $ Document ELEMENT
getChildElementsByQName (QName y _ _) node {prf} =
  filter (\(Element (QName x _ _) _ _) => x == y) (getChildElements node) -- change to ==

||| Get All Child Elements with a local name
getChildElementsByName : String
                      -> Document a
                      -> {auto prf : CanQuery a}
                      -> List $ Document ELEMENT
getChildElementsByName name node {prf} =
  filter (\(Element (QName x _ _) _ _) => x == name) (getChildElements node)

||| Get All child elements regardless of name.
getAllChildren : Document a
              -> {auto prf : CanQuery a}
              -> List $ Document ELEMENT
getAllChildren (MkDocument x y xs z w) {prf = QueryDoc} = assert_total $ getAllElements w
getAllChildren node {prf = QueryElem} = assert_total $ getAllElements node

-- ----------------------------------------------------------------- [ Aliases ]

public export
XMLDoc : Type
XMLDoc = Document DOCUMENT

public export
XMLElem : Type
XMLElem = Document ELEMENT

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

max_stars_repo_name: jfdm/idris-xml

max_issues_repo_name: jfdm/idris-xml

max_forks_repo_name: jfdm/idris-xml


text:
module Python.Prim

import Python
import Python.Telescope
import Python.Fields
import Python.Functions

%access public export
%default total

||| The actual state of iteration.
Iterator : Type -> Signature
Iterator a f = case f of
  "next" => [] ~~> a
  _ => Object f

||| Something that can produce an iterator.
Iterable : Type -> Signature
Iterable a f = case f of
  "__iter__" => [] ~~> Obj (Iterator a)
  _ => Object f

||| Python string as object.
PyString : Signature
PyString f = case f of
  "join" => [Obj $ Iterable String] ~~> String
  _ => Iterable Char f

||| Python list as object.
PyList : Type -> Signature
PyList a = Iterable a  -- nothing else yet

||| Primitives promotable to objects.
data PythonPrim : Type -> Signature -> Type where
  PPString : PythonPrim String PyString

namespace Builtins
  Builtins : Signature
  Builtins f = case f of
    "list" => fun $
      forall a : Type .
        pi xs : (List a) .
          Return $ Obj (PyList a)

    _ => Module f

  builtins : Obj Builtins
  builtins = getGlobal "__builtins__"

pyList : List a -> Obj $ PyList a
pyList {a=a} xs = unsafePerformIO (builtins /. "list" $. [Erase a, xs])

||| Promote a primitive to an object. Note that this is a no-oop,
||| all primitives already are objects in Python.
obj : (x : a) -> {auto pf : PythonPrim a sig} -> Obj sig
obj x = believe_me x

||| Get the next value from an iterator.
next : Obj (Iterator a) -> PIO (Maybe a)
next {a = a} it = do
  OK x <- try (it /. "next" $. [])
    | Except StopIteration e => pure Nothing
    | Except _ e => raise e
  pure $ Just x

||| A left-fold over an iterable object, implemented in Idris.
||| This is not very efficient (TCO does not kick in here)
||| but it's a demonstration we can do it easily.
|||
||| See also `foreach`, which is a native Python for-loop.
partial
iterate : (o : Obj sig)
  -> (st : b)
  -> (f : b -> a -> PIO b)
  -> {auto pf : sig "__iter__" = [] ~~> Obj (Iterator a)}
  -> PIO b
iterate iterable st f = do
    iterator <- iterable /. "__iter__" $. []
    iter iterator st f
  where
    partial
    iter : Obj (Iterator a) -> (st : b) -> (f : b -> a -> PIO b) -> PIO b
    iter it st f = do
      Just x <- next it | Nothing => pure st
      st' <- f st x
      iter it st' f

||| A left-fold over an iterable object, implemented as a for-loop in Python.
|||
||| @ o The iterable object.
||| @ st Initial state.
||| @ f  PIO action called for every element, transforms the state.
partial
foreach :
  (o : Obj sig)
  -> (st : b)
  -> (f : b -> a -> PIO b)
  -> {auto pf : sig "__iter__" = [] ~~> Obj (Iterator a)}
  -> PIO b
foreach {a=a} {b=b} {sig=sig} iterable st f = do
  iterator <- iterable /. "__iter__" $. []
  unRaw <$>
    foreign FFI_Py "_idris_foreach"
      (Obj sig -> Raw b -> Raw (b -> a -> PIO b) -> PIO (Raw b))
      iterable
      (MkRaw st)
      (MkRaw f)

||| Collect all elements of an iterator into a list.
partial
collect : (it : Obj sig) -> {auto pf : sig "__iter__" = [] ~~> Obj (Iterator a)} -> PIO (List a)
collect it = reverse <$> foreach it List.Nil (\xs, x => pure (x :: xs))

ext: idr

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
module Main

import Average

showAverage : String -> String
showAverage str = "The average word length is " ++
                  show (average str) ++ "\n"

main : IO ()
main = repl "Enter a string: "
            showAverage


text:
module Baseline

%include C "baseline_idris.h"
%lib     C "editline"
%link    C "baseline_idris.o"

readline : String -> IO String
readline = foreign FFI_C "bl_readline" (String -> IO String)

||| Run the readline prompt and save input to history.
export
baseline : (prompt : String) -> IO (Maybe String)
baseline prompt = do
  text <- readline prompt
  null <- nullStr text
  pure (toMaybe (not null) text)

||| Add an entry to tab completion dictionary.
export
addDictEntry : (entry : String) -> IO ()
addDictEntry = foreign FFI_C "bl_add_dict_entry" (String -> IO ())

||| Add multiple entries to tab completion dictionary.
export
addDictEntries : Foldable t => (entries : t String) -> IO ()
addDictEntries es = for_ es addDictEntry

||| Recover saved history from file.
export
readHistory : (filename : String) -> IO ()
readHistory = foreign FFI_C "bl_read_history" (String -> IO ())

||| Save history to file.
export
writeHistory : (filename : String) -> IO ()
writeHistory = foreign FFI_C "bl_write_history" (String -> IO ())

max_stars_repo_name: laserpants/baseline-idris

max_issues_repo_name: laserpants/baseline-idris

max_forks_repo_name: laserpants/baseline-idris


text:
---
pandoc-minted:
  language: idris
---

= No Time for a Taxicab

[Link](https://adventofcode.com/2016/day/1)

Santa's sleigh uses a very high-precision clock to guide its movements, and the
clock's oscillator is regulated by stars. Unfortunately, the stars have been
stolen... by the Easter Bunny. To save Christmas, Santa needs you to retrieve
all **fifty stars** by December 25th.

Collect stars by solving puzzles. Two puzzles will be made available on each day
in the advent calendar; the second puzzle is unlocked when you complete the
first. Each puzzle grants **one star**. Good luck!

You're airdropped near *Easter Bunny Headquarters* in a city somewhere. "Near",
unfortunately, is as close as you can get - the instructions on the Easter Bunny
Recruiting Document the Elves intercepted start here, and nobody had time to
work them out further.

The Document indicates that you should start at the given coordinates (where you
just landed) and face North. Then, follow the provided sequence: either turn
left (`L`) or right (`R`) 90 degrees, then walk forward the given number of
blocks, ending at a new intersection.

There's no time to follow such ridiculous instructions on foot, though, so you
take a moment and work out the destination. Given that you can only walk on the
[street grid of the city](https://en.wikipedia.org/wiki/Taxicab_geometry), how
far is the shortest path to the destination?

For example:

- Following `R2, L3` leaves you `2` blocks East and `3` blocks North, or `5`
  blocks away.
- `R2, R2, R2` leaves you `2` blocks due South of your starting position, which
  is `2` blocks away.
- `R5, L5, R5, R3` leaves you `12` blocks away.

\newpage

== Module Declaration and Imports

> ||| Day 1: No Time for a Taxicab
> module Data.Advent.Day01

Import the [generic `Day`
structure](https://github.com/yurrriq/advent-of-idris/blob/master/src/Data/Advent/Day.idr),
inspired by [Steve Purcell Haskell
solution](https://github.com/purcell/adventofcode2016).

> import public Data.Advent.Day

For no compelling reason, I like to use
[arrows](https://www.haskell.org/arrows/), so import the requisite modules.

> import Control.Arrow
> import Control.Category
> import Data.Morphisms
> import Data.SortedSet

For parsing, use [Lightyear](https://github.com/ziman/lightyear).

> import public Lightyear
> import public Lightyear.Char
> import public Lightyear.Strings

== Data Types

Ensure both the type and data constructors are
[exported](http://docs.idris-lang.org/en/latest/tutorial/modules.html#meaning-for-data-types)
for all the following data types.

> %access public export

We'll need to keep track of which cardinal direction we're facing, so define a
data type `Heading` to model that. A heading is `N`orth, `E`ast, `S`outh or `W`est.

> ||| A cardinal heading.
> data Heading = ||| North
>                N
>              | ||| East
>                E
>              | ||| South
>                S
>              | ||| West
>                W

As per the [puzzle description](no-time-for-a-taxicab), the instructions will
tell us to go `L`eft or `R`ight, so model `Direction`s accordingly.

> ||| A direction to walk in, left or right.
> data Direction = ||| Left
>                  L
>                | ||| Right
>                  R

\newpage

For convenience in the REPL, implement the `Show`
[interface](http://docs.idris-lang.org/en/latest/tutorial/interfaces.html) for
`Direction`.

> implementation Show Direction where
>     show L = "Left"
>     show R = "Right"

An `Instruction`, e.g. `R2`, is comprised of a `Direction` and a number of
blocks to walk in that direction.

As such, define an `Instruction` as a record containing a `Direction` and a
number of `Blocks`.

> Blocks : Type
> Blocks = Integer
>
> ||| A direction and a number of blocks.
> record Instruction where
>     constructor MkIns
>     iDir    : Direction
>     iBlocks : Blocks

A `Position` is a record containing x and y coordinates in the [street
grid](https://en.wikipedia.org/wiki/Taxicab_geometry).

> ||| A pair of coordinates on the street grid.
> record Position where
>     constructor MkPos
>     posX, posY : Blocks
>
> implementation Eq Position where
>     (MkPos x1 y1) == (MkPos x2 y2) = x1 == x2 && y1 == y2
>
> implementation Ord Position where
>     compare (MkPos x1 y1) (MkPos x2 y2) with (compare x1 x2)
>       | EQ = compare y1 y2
>       | o  = o

== Parsers

Ensure the type constructors of the following parsers are
[exported](http://docs.idris-lang.org/en/latest/tutorial/modules.html#meaning-for-data-types).

> %access export

A `Direction` is represented in the input by a single character, `'L'` or `'R'`.

> direction : Parser Direction
> direction = (char 'L' *> pure L) <|>|
>             (char 'R' *> pure R) <?>
>             "a direction"

\newpage

An `Instruction` is represented as a `Direction` followed immediately by an
integer.

> ||| Parse an instruction, i.e. a direction and
> ||| a number of blocks to walk in that direction.
> partial instruction : Parser Instruction
> instruction = [| MkIns direction integer |] <?> "an instruction"

The instructions are given as a comma-separated list.

> ||| Parse a comma-separated list of `Instruction`s.
> partial instructions : Parser (List Instruction)
> instructions = commaSep instruction <* spaces <?>
>                "a comma-separated list of instructions"

== Logic

> ||| Return the new heading after turning right.
> ||| @ initial the initial heading
> turnRight : (initial : Heading) -> Heading
> turnRight N = E
> turnRight E = S
> turnRight S = W
> turnRight W = N
>
> ||| Return the new heading after turning left.
> ||| @ initial the initial heading
> turnLeft : (initial : Heading) -> Heading
> turnLeft N = W
> turnLeft E = N
> turnLeft S = E
> turnLeft W = S
>
> ||| Return the new heading after turning in a given direction.
> turn : Heading -> Direction -> Heading
> turn h L = turnLeft  h
> turn h R = turnRight h
>
> ||| Return the new position after moving one block with a given heading.
> move : Heading -> (Position -> Position)
> move N = record { posY $= (+ 1) }
> move E = record { posX $= (+ 1) }
> move S = record { posY $= (flip (-) 1) }
> move W = record { posX $= (flip (-) 1) }

> ||| Compute the shortest distance from the initial position and a given one.
> shortestDistance : Position -> Blocks
> shortestDistance (MkPos x y) = abs x + abs y

\newpage

> ||| Return the list of intermediate positions visited
> ||| when following a given list of instructions.
> followInstructions : List Instruction -> List Position
> followInstructions is =
>     let directions = drop 1 $ scanl turn N (iDir <$> is)
>         distances  = iBlocks <$> is
>         moves      = concatMap expand (zip directions distances) in
>         scanl (flip move) (MkPos 0 0) moves
>   where
>     expand : (Heading, Blocks) -> List Heading
>     expand (h, n) = replicate (cast n) h

== Part One

\begin{quote}
  \textit{How many blocks away} is Easter Bunny HQ?
\end{quote}

To compute the answer to Part One, `262`, follow the instructions, get the last
position and compute the shortest distance from the initial position.

> partOne : List Instruction -> Maybe Blocks
> partOne = map shortestDistance . last' . followInstructions

== Part Two

Then, you notice the instructions continue on the back of the Recruiting
Document. Easter Bunny HQ is actually at the first location you visit twice.

For example, if your instructions are `R8, R4, R4, R8`, the first location you
visit twice is `4` blocks away, due East.

\begin{quote}
  How many blocks away is the \textit{first location you visit twice}?
\end{quote}

First, define a function `firstDuplicate` to find the first location visited
twice in a list of positions. Instead of specializing for `List Position`,
generalize the solution to `Ord a => List a`.

> ||| Return `Just` the first duplicate in a given list.
> ||| If there are none, return `Nothing`.
> firstDuplicate : Ord a => List a -> Maybe a
> firstDuplicate = go empty
>   where
>     go : SortedSet a -> List a -> Maybe a
>     go _ []         = Nothing
>     go seen (x::xs) =
>         if contains x seen
>            then Just x
>            else go (insert x seen) xs

> partTwo : List Instruction -> Maybe Blocks
> partTwo = map shortestDistance . firstDuplicate . followInstructions

\newpage

== Main

Run the solutions for Day 1.

> namespace Main
>
>     partial main : IO ()
>     main = runDay $ MkDay 1 instructions
>            (pure . maybe "Failed!" show . partOne)
>            (pure . maybe "Failed!" show . partTwo)

$\qed$

\newpage

ext: lidr

max_stars_repo_name: yurrriq/advent-of-code


text:
module Issue758

-- introduce linear bind and linear pure
interface LMonad m where
  pure : (1 _ : a) -> m a
  (>>=) : (1 _ : m a) -> (1 _ : (1 _ : a) -> m b) -> m b

(>>) : LMonad m => (1 _ : m ()) -> (1 _ : m a) -> m a
ma >> mb = ma >>= \ () => mb

fail : LMonad m => (1 _ : m ((1 _ : a) -> b)) -> (1 _ : a) -> m b
fail ma a = do f <- ma
               ?what_is_f
               pure (f a)


text:
module LightClick.IR.ModuleCentric

import Data.String
import Data.Vect

import Toolkit.Data.DList
import Toolkit.Data.DVect

import Language.SystemVerilog.Gates

import LightClick.Types
import LightClick.Values

%default total

public export
data TyIR = PORT
          | UNIT
          | MODULE
          | CONN
          | DATA
          | CHAN
          | GATE

export
Show TyIR where
  show PORT   = "MTyPORT"
  show UNIT   = "MTyUNIT"
  show MODULE = "MTyMODULE"
  show CONN   = "MTyCONN"
  show DATA   = "MTyDATA"
  show CHAN   = "MTyCHAN"
  show GATE   = "MTyGATE"

public export
data ModuleIR : TyIR -> Type where
  MRef : (name : String) -> (type : TyIR) -> ModuleIR type
  MLet : {term : TyIR} -> (name : String)
      -> (beThis : ModuleIR (term))
      -> (inThis : ModuleIR (expr)) -> ModuleIR (expr)

  MSeq : {a,b : TyIR} -> (doThis   : ModuleIR a)
      -> (thenThis : ModuleIR b) -> ModuleIR b

  MEnd  : ModuleIR UNIT

  MPort : (label : String)
       -> (dir   : Direction)
       -> (type  : ModuleIR DATA) -> ModuleIR PORT

  MModule : {n : Nat} -> Vect (S n) (ModuleIR PORT) -> ModuleIR MODULE

  MDataLogic : ModuleIR DATA
  MDataArray : ModuleIR DATA -> Nat -> ModuleIR DATA
  MDataStruct : {n : Nat} -> Vect (S n) (Pair String (ModuleIR DATA)) -> ModuleIR DATA
  MDataUnion  : {n : Nat} -> Vect (S n) (Pair String (ModuleIR DATA)) -> ModuleIR DATA

  MChan : ModuleIR DATA -> ModuleIR CHAN

  MIDX : (label : String)
      -> ModuleIR MODULE
      -> ModuleIR PORT
      -> ModuleIR PORT

  MConn : {n : Nat}
       -> (cname  : ModuleIR CHAN)
       -> (input  : ModuleIR PORT)
       -> (output : Vect (S n) $ ModuleIR PORT)
       -> ModuleIR CONN

  MNot : ModuleIR CHAN
      -> ModuleIR CHAN
      -> ModuleIR GATE

  MGate : {n : Nat}
       -> TyGateComb
       -> ModuleIR CHAN
       -> Vect (S (S n)) (ModuleIR CHAN)
       -> ModuleIR GATE

  MConnG : ModuleIR CHAN
        -> ModuleIR PORT
        -> ModuleIR CONN

-- go from value (with proof of normal form) to moduleIR
public export
interp : TyValue -> TyIR
interp (PORT x) = PORT
interp UNIT = UNIT
interp (MODULE xs) = MODULE
interp CONN = CONN
interp DATA = DATA
interp CHAN = CHAN
interp GATE = GATE

covering
convert : Value type -> ModuleIR (interp type)
convert (VRef name type) = MRef name (interp type)
convert (VLet name beThis inThis) = MLet name (convert beThis) (convert inThis)
convert (VSeq this thenThis) = MSeq (convert this) (convert thenThis)
convert VEnd = MEnd

convert (VPort label dir type) = MPort label dir (convert type)
convert (VModule x) = MModule $ mapToVect (\p => (convert p)) x

convert VDataLogic = MDataLogic
convert (VDataArray x k) = MDataArray (convert x) k
convert (VDataStruct xs) = MDataStruct $ map (\(l,p) => (l,convert p)) xs
convert (VDataUnion xs) = MDataUnion $ map (\(l,p) => (l,convert p)) xs

convert (VChan x) = MChan (convert x)
convert (VIDX name x y) = MIDX name (convert x) (convert y)

convert (VConnD x y z) = MConn (convert x) (convert y) [convert z]
convert (VConnFO x y z) = MConn (convert x) (convert y) (mapToVect (\p => convert p) z)
convert (VNot o i) = MNot (convert o) (convert i)
convert (VGate ty o ins) = MGate ty (convert o) (map convert ins)
convert (VConnG c idx) = MConnG (convert c) (convert idx)

covering
export
runConvert : Value type -> ModuleIR (interp type)
runConvert = convert

covering
showM : ModuleIR type -> String
showM (MRef name type) =
  "(MRef " <+> show name <+> ")"

showM (MLet x y z) =
   "(MLet "
     <+> show x <+> " "
     <+> showM y <+> " "
     <+> showM z
     <+> ")"

showM (MSeq x y) =
    "(MSeq "
      <+> showM x <+> " "
      <+> showM y
      <+> ")"
showM MEnd = "(MEnd)"

showM (MPort x y z) =
    "(MPort "
      <+> show x <+> " "
      <+> show y <+> " "
      <+> showM z <+> " "
      <+> ")"

showM (MModule x) =
    "(MModule "
      <+> show (map showM x)
      <+> ")"

showM MDataLogic = "(MTyLogic)"

showM (MDataArray x k) =
  "(MTyArray "
    <+> showM x <+> " "
    <+> show k
    <+> ")"

showM (MDataStruct {n} xs) = "(MTyStruct " <+> show ps <+> ")"
  where
    covering
    ps : Vect (S n) String
    ps = map (\(l,c) => "(" <+> show l <+> " " <+> showM c <+> ")") xs

showM (MDataUnion {n} xs) = "(TyUnion " <+> show ps <+> ")"
  where
    covering
    ps : Vect (S n) String
    ps = map (\(l,c) => "(" <+> show l <+> " " <+> showM c <+> ")") xs

showM (MChan x) = "(MChan " <+> showM x <+> ")"

showM (MIDX x y z) =
    "(MIndex "
       <+> show x <+> " "
       <+> showM y <+> " "
       <+> showM z
       <+> ")"

showM (MConn x y ps) =
    "(MDConn "
      <+> showM x <+> " "
      <+> showM y <+> " "
      <+> show (map showM ps)
      <+> ")"

showM (MNot o i)
  = unwords ["(MNot", showM o, showM i, ")"]

showM (MGate ty o ins)
    = unwords ["(MGate", show ty, showM o, ins', ")"]

  where
    covering
    ins' : String
    ins' = unwords $ toList $ map (\c => "(" <+> showM c <+> ")") ins

showM (MConnG c idx)
  = unwords ["(MConnG", showM c, showM idx, ")"]

export
Show (ModuleIR type) where
  show = assert_total showM -- TODO

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
import Data.Vect

test1 : Vect 4 Int
test1 = [1, 2, 3, 4]

test2: Vect (2 + 2) Int
test2 = test1

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


text:
foo : Nat -> Nat
foo x = ?foo_rhs

bar : Nat -> Nat
bar x = plus x ?bar_rhs

-- Rest of file


text:
module Libraries.Text.PrettyPrint.Prettyprinter.Doc

import Data.List
import public Data.List1
import Data.Maybe
import Data.SnocList
import Data.String
import public Libraries.Data.String.Extra

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

%default total

export
textSpaces : Int -> String
textSpaces n = Extra.replicate (integerToNat $ cast n) ' '

||| Maximum number of characters that fit in one line.
public export
data PageWidth : Type where
  ||| The `Int` is the number of characters, including whitespace, that fit in a line.
  ||| The `Double` is the ribbon, the fraction of the toal page width that can be printed on.
  AvailablePerLine : Int -> Double -> PageWidth
  ||| The layouters should not introduce line breaks.
  Unbounded : PageWidth

data FlattenResult : Type -> Type where
  Flattened : a -> FlattenResult a
  AlreadyFlat : FlattenResult a
  NeverFlat : FlattenResult a

Functor FlattenResult where
  map f (Flattened a) = Flattened (f a)
  map _ AlreadyFlat = AlreadyFlat
  map _ NeverFlat = NeverFlat

||| Fusion depth parameter.
public export
data FusionDepth : Type where
  ||| Do not dive deep into nested documents.
  Shallow : FusionDepth
  ||| Recurse into all parts of the `Doc`. May impact performace.
  Deep : FusionDepth

||| This data type represents pretty documents that have
||| been annotated with an arbitrary data type `ann`.
public export
data Doc : Type -> Type where
  Empty : Doc ann
  Chara : (c : Char) -> Doc ann                         -- Invariant: not '\n'
  Text : (len : Int) -> (text : String) -> Doc ann      -- Invariant: at least two characters long and no '\n'
  Line : Doc ann
  FlatAlt : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann
  Cat : Doc ann -> Doc ann -> Doc ann
  Nest : (i : Int) -> Doc ann -> Doc ann
  Union : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann   -- Invariant: the first line of the first document should be
                                                        -- longer than the first lines of the second one
  Column : (Int -> Doc ann) -> Doc ann
  WithPageWidth : (PageWidth -> Doc ann) -> Doc ann
  Nesting : (Int -> Doc ann) -> Doc ann
  Annotated : ann -> Doc ann -> Doc ann

export
Semigroup (Doc ann) where
  (<+>) = Cat

export
Monoid (Doc ann) where
  neutral = Empty

||| Layout a document depending on which column it starts at.
export
column : (Int -> Doc ann) -> Doc ann
column = Column

||| Lays out a document with the current nesting level increased by `i`.
export
nest : Int -> Doc ann -> Doc ann
nest 0 x = x
nest i x = Nest i x

||| Layout a document depending on the current nesting level.
export
nesting : (Int -> Doc ann) -> Doc ann
nesting = Nesting

||| Lays out a document, and makes the column width of it available to a function.
export
width : Doc ann -> (Int -> Doc ann) -> Doc ann
width doc f = column (\colStart => doc <+> column (\colEnd => f (colEnd - colStart)))

||| Layout a document depending on the page width, if one has been specified.
export
pageWidth : (PageWidth -> Doc ann) -> Doc ann
pageWidth = WithPageWidth

||| Lays out a document with the nesting level set to the current column.
export
align : Doc ann -> Doc ann
align d = column (\k => nesting (\i => nest (k - i) d))

||| Lays out a document with a nesting level set to the current column plus `i`.
||| Negative values are allowed, and decrease the nesting level accordingly.
export
hang : Int -> Doc ann -> Doc ann
hang i d = align (nest i d)

||| Insert a number of spaces.
export
spaces : Int -> Doc ann
spaces n = if n <= 0
              then Empty
              else if n == 1
                      then Chara ' '
                      else Text n (textSpaces n)

||| Indents a document with `i` spaces, starting from the current cursor position.
export
indent : Int -> Doc ann -> Doc ann
indent i d = hang i (spaces i <+> d)

||| Lays out a document. It then appends spaces until the width is equal to `i`.
||| If the width is already larger, nothing is appended.
export
fill : Int -> Doc ann -> Doc ann
fill n doc = width doc (\w => spaces $ n - w)

infixr 6 <++>
||| Concatenates two documents with a space in between.
export
(<++>) : Doc ann -> Doc ann -> Doc ann
x <++> y = x <+> Chara ' ' <+> y

||| The empty document behaves like `pretty ""`, so it has a height of 1.
export
emptyDoc : Doc ann
emptyDoc = Empty

||| Behaves like `space` if the resulting output fits the page, otherwise like `line`.
export
softline : Doc ann
softline = Union (Chara ' ') Line

||| Like `softline`, but behaves like `neutral` if the resulting output does not fit
||| on the page.
export
softline' : Doc ann
softline' = Union neutral Line

||| A line break, even when grouped.
export
hardline : Doc ann
hardline = Line

flatten : Doc ann -> Doc ann
flatten Empty = Empty
flatten (Chara x) = Chara x
flatten (Text len x) = Text len x
flatten Line = Empty
flatten (FlatAlt _ y) = flatten y
flatten (Cat x y) = Cat (flatten x) (flatten y)
flatten (Nest i x) = Nest i (flatten x)
flatten (Union x _) = flatten x
flatten (Column f) = Column (\x => flatten $ f x)
flatten (WithPageWidth f) = WithPageWidth (\x => flatten $ f x)
flatten (Nesting f) = Nesting (\x => flatten $ f x)
flatten (Annotated ann x) = Annotated ann (flatten x)

changesUponFlattening : Doc ann -> FlattenResult (Doc ann)
changesUponFlattening Empty = AlreadyFlat
changesUponFlattening (Chara x) = AlreadyFlat
changesUponFlattening (Text x y) = AlreadyFlat
changesUponFlattening Line = NeverFlat
changesUponFlattening (FlatAlt _ y) = Flattened (flatten y)
changesUponFlattening (Cat x y) = case (changesUponFlattening x, changesUponFlattening y) of
  (NeverFlat, _) => NeverFlat
  (_, NeverFlat) => NeverFlat
  (Flattened x', Flattened y') => Flattened (Cat x' y')
  (Flattened x', AlreadyFlat) => Flattened (Cat x' y)
  (AlreadyFlat , Flattened y') => Flattened (Cat x y')
  (AlreadyFlat , AlreadyFlat) => AlreadyFlat
changesUponFlattening (Nest i x) = map (Nest i) (changesUponFlattening x)
changesUponFlattening (Union x _) = Flattened x
changesUponFlattening (Column f) = Flattened (Column (flatten . f))
changesUponFlattening (WithPageWidth f) = Flattened (WithPageWidth (flatten . f))
changesUponFlattening (Nesting f) = Flattened (Nesting (flatten . f))
changesUponFlattening (Annotated ann x) = map (Annotated ann) (changesUponFlattening x)

||| Tries laying out a document into a single line by removing the contained
||| line breaks; if this does not fit the page, or has an `hardline`, the document
||| is laid out without changes.
export
group : Doc ann -> Doc ann
group (Union x y) = Union x y
group (FlatAlt x y) = case changesUponFlattening y of
  Flattened y' => Union y' x
  AlreadyFlat => Union y x
  NeverFlat => x
group x = case changesUponFlattening x of
  Flattened x' => Union x' x
  AlreadyFlat => x
  NeverFlat => x

||| By default renders the first document, When grouped renders the second, with
||| the first as fallback when there is not enough space.
export
flatAlt : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann
flatAlt = FlatAlt

||| Advances to the next line and indents to the current nesting level.
export
line : Doc ann
line = FlatAlt Line (Chara ' ')

||| Like `line`, but behaves like `neutral` if the line break is undone by `group`.
export
line' : Doc ann
line' = FlatAlt Line Empty

||| First lays out the document. It then appends spaces until the width is equal to `i`.
||| If the width is already larger than `i`, the nesting level is decreased by `i`
||| and a line is appended.
export
fillBreak : Int -> Doc ann -> Doc ann
fillBreak f x  = width x (\w => if w > f
                                   then nest f line'
                                   else spaces $ f - w)

||| Concatenate all documents element-wise with a binary function.
export
concatWith : (Doc ann -> Doc ann -> Doc ann) -> List (Doc ann) -> Doc ann
concatWith f [] = neutral
concatWith f (x :: xs) = foldl f x xs

||| Concatenates all documents horizontally with `(<++>)`.
export
hsep : List (Doc ann) -> Doc ann
hsep = concatWith (<++>)

||| Concatenates all documents above each other. If a `group` undoes the line breaks,
||| the documents are separated with a space instead.
export
vsep : List (Doc ann) -> Doc ann
vsep = concatWith (\x, y => x <+> line <+> y)

||| Concatenates the documents horizontally with `(<++>)` as long as it fits the page,
||| then inserts a line and continues.
export
fillSep : List (Doc ann) -> Doc ann
fillSep = concatWith (\x, y => x <+> softline <+> y)

||| Tries laying out the documents separated with spaces and if this does not fit,
||| separates them with newlines.
export
sep : List (Doc ann) -> Doc ann
sep = group . vsep

||| Concatenates all documents horizontally with `(<+>)`.
export
hcat : List (Doc ann) -> Doc ann
hcat = concatWith (<+>)

||| Vertically concatenates the documents. If it is grouped, the line breaks are removed.
export
vcat : List (Doc ann) -> Doc ann
vcat = concatWith (\x, y => x <+> line' <+> y)

||| Concatenates documents horizontally with `(<+>)` as log as it fits the page, then
||| inserts a line and continues.
export
fillCat : List (Doc ann) -> Doc ann
fillCat = concatWith (\x, y => x <+> softline' <+> y)

||| Tries laying out the documents separated with nothing, and if it does not fit the page,
||| separates them with newlines.
export
cat : List (Doc ann) -> Doc ann
cat = group . vcat

||| Appends `p` to all but the last document.
export
punctuate : Doc ann -> List (Doc ann) -> List (Doc ann)
punctuate _ [] = []
punctuate _ [d] = [d]
punctuate p (d :: ds) = (d <+> p) :: punctuate p ds

export
plural : (Num amount, Eq amount) => doc -> doc -> amount -> doc
plural one multiple n = if n == 1 then one else multiple

||| Encloses the document between two other documents using `(<+>)`.
export
enclose : Doc ann -> Doc ann -> Doc ann -> Doc ann
enclose l r x = l <+> x <+> r

||| Reordering of `encloses`.
||| Example: concatWith (surround (pretty ".")) [pretty "Text", pretty "PrettyPrint", pretty "Doc"]
|||          Text.PrettyPrint.Doc
export
surround : Doc ann -> Doc ann -> Doc ann -> Doc ann
surround x l r = l <+> x <+> r

||| Concatenates the documents separated by `s` and encloses the resulting document by `l` and `r`.
export
encloseSep : Doc ann -> Doc ann -> Doc ann -> List (Doc ann) -> Doc ann
encloseSep l r s []  = l <+> r
encloseSep l r s [d] = l <+> d <+> r
encloseSep l r s ds  = cat (zipWith (<+>) (l :: replicate (length ds `minus` 1) s) ds) <+> r

unsafeTextWithoutNewLines : String -> Doc ann
unsafeTextWithoutNewLines str = case strM str of
  StrNil => Empty
  StrCons c cs => if cs == ""
                     then Chara c
                     else Text (cast $ length str) str

||| Adds an annotation to a document.
export
annotate : ann -> Doc ann -> Doc ann
annotate = Annotated

||| Changes the annotations of a document. Individual annotations can be removed,
||| changed, or replaced by multiple ones.
export
alterAnnotations : (ann -> List ann') -> Doc ann -> Doc ann'
alterAnnotations re Empty = Empty
alterAnnotations re (Chara c) = Chara c
alterAnnotations re (Text l t) = Text l t
alterAnnotations re Line = Line
alterAnnotations re (FlatAlt x y) = FlatAlt (alterAnnotations re x) (alterAnnotations re y)
alterAnnotations re (Cat x y) = Cat (alterAnnotations re x) (alterAnnotations re y)
alterAnnotations re (Nest i x) = Nest i (alterAnnotations re x)
alterAnnotations re (Union x y) = Union (alterAnnotations re x) (alterAnnotations re y)
alterAnnotations re (Column f) = Column (\x => alterAnnotations re $ f x)
alterAnnotations re (WithPageWidth f) = WithPageWidth (\x => alterAnnotations re $ f x)
alterAnnotations re (Nesting f) = Nesting (\x => alterAnnotations re $ f x)
alterAnnotations re (Annotated ann x) = foldr Annotated (alterAnnotations re x) (re ann)

||| Removes all annotations.
export
unAnnotate : Doc ann -> Doc xxx
unAnnotate = alterAnnotations (const [])

||| Changes the annotations of a document.
export
reAnnotate : (ann -> ann') -> Doc ann -> Doc ann'
reAnnotate re = alterAnnotations (pure . re)

||| Alter the document's annotations.
export
Functor Doc where
  map = reAnnotate

||| Overloaded converison to `Doc`.
public export
interface Pretty a where
  pretty : a -> Doc ann
  pretty x = prettyPrec Open x

  prettyPrec : Prec -> a -> Doc ann
  prettyPrec _ x = pretty x

export
Pretty String where
  pretty str = let str' = if "\n" `isSuffixOf` str then dropLast 1 str else str in
                   vsep $ map unsafeTextWithoutNewLines $ forget $ lines str'

public export
FromString (Doc ann) where
  fromString = pretty

||| Variant of `encloseSep` with braces and comma as separator.
export
list : List (Doc ann) -> Doc ann
list = group . encloseSep (flatAlt (pretty "[ ") (pretty "["))
                          (flatAlt (pretty " ]") (pretty "]"))
                          (pretty ", ")

||| Variant of `encloseSep` with parentheses and comma as separator.
export
tupled : List (Doc ann) -> Doc ann
tupled = group . encloseSep (flatAlt (pretty "( ") (pretty "("))
                            (flatAlt (pretty " )") (pretty ")"))
                            (pretty ", ")

export
Pretty a => Pretty (List a) where
  pretty = align . list . map pretty

export
Pretty a => Pretty (List1 a) where
  pretty = pretty . forget

export
[prettyListMaybe] Pretty a => Pretty (List (Maybe a)) where
  pretty = pretty . catMaybes
    where catMaybes : List (Maybe a) -> List a
          catMaybes [] = []
          catMaybes (Nothing :: xs) = catMaybes xs
          catMaybes ((Just x) :: xs) = x :: catMaybes xs

export
Pretty () where
  pretty _ = pretty "()"

export
Pretty Bool where
  pretty True = pretty "True"
  pretty False = pretty "False"

export
Pretty Char where
  pretty '\n' = line
  pretty c = Chara c

export Pretty Nat where pretty = unsafeTextWithoutNewLines . show
export Pretty Int where pretty = unsafeTextWithoutNewLines . show
export Pretty Integer where pretty = unsafeTextWithoutNewLines . show
export Pretty Double where pretty = unsafeTextWithoutNewLines . show
export Pretty Bits8 where pretty = unsafeTextWithoutNewLines . show
export Pretty Bits16 where pretty = unsafeTextWithoutNewLines . show
export Pretty Bits32 where pretty = unsafeTextWithoutNewLines . show
export Pretty Bits64 where pretty = unsafeTextWithoutNewLines . show

export
(Pretty a, Pretty b) => Pretty (a, b) where
  pretty (x, y) = tupled [pretty x, pretty y]

export
Pretty a => Pretty (Maybe a) where
  pretty = maybe neutral pretty

||| Combines text nodes so they can be rendered more efficiently.
export
fuse : FusionDepth -> Doc ann -> Doc ann
fuse depth (Cat Empty x) = fuse depth x
fuse depth (Cat x Empty) = fuse depth x
fuse depth (Cat (Chara c1) (Chara c2)) = Text 2 (strCons c1 (strCons c2 ""))
fuse depth (Cat (Text lt t) (Chara c)) = Text (lt + 1) (t ++ singleton c)
fuse depth (Cat (Chara c) (Text lt t)) = Text (lt + 1) (strCons c t)
fuse depth (Cat (Text l1 t1) (Text l2 t2)) = Text (l1 + l2) (t1 ++ t2)
fuse depth (Cat (Chara x) (Cat (Chara y) z)) =
  let sub = Text 2 (strCons x (strCons y "")) in
      fuse depth $ assert_smaller (Cat (Chara x) (Cat (Chara y) z)) (Cat sub z)
fuse depth (Cat (Text lx x) (Cat (Chara y) z)) =
  let sub = Text (lx + 1) (x ++ singleton y) in
      fuse depth $ assert_smaller (Cat (Text lx x) (Cat (Chara y) z)) (Cat sub z)
fuse depth (Cat (Chara x) (Cat (Text ly y) z)) =
  let sub = Text (ly + 1) (strCons x y) in
      fuse depth $ assert_smaller (Cat (Chara x) (Cat (Text ly y) z)) (Cat sub z)
fuse depth (Cat (Text lx x) (Cat (Text ly y) z)) =
  let sub = Text (lx + ly) (x ++ y) in
      fuse depth $ assert_smaller (Cat (Text lx x) (Cat (Text ly y) z)) (Cat sub z)
fuse depth (Cat (Cat x (Chara y)) z) =
  let sub = fuse depth (Cat (Chara y) z) in
      assert_total $ fuse depth (Cat x sub)
fuse depth (Cat (Cat x (Text ly y)) z) =
  let sub = fuse depth (Cat (Text ly y) z) in
      assert_total $ fuse depth (Cat x sub)
fuse depth (Cat x y) = Cat (fuse depth x) (fuse depth y)
fuse depth (Nest i (Nest j x)) = fuse depth $ assert_smaller (Nest i (Nest j x)) (Nest (i + j) x)
fuse depth (Nest _ Empty) = Empty
fuse depth (Nest _ (Text lx x)) = Text lx x
fuse depth (Nest _ (Chara x)) = Chara x
fuse depth (Nest 0 x) = fuse depth x
fuse depth (Nest i x) = Nest i (fuse depth x)
fuse depth (Annotated ann x) = Annotated ann (fuse depth x)
fuse depth (FlatAlt x y) = FlatAlt (fuse depth x) (fuse depth y)
fuse depth (Union x y) = Union (fuse depth x) (fuse depth y)
fuse Shallow (Column f) = Column f
fuse depth (Column f) = Column (\x => fuse depth $ f x)
fuse Shallow (WithPageWidth f) = WithPageWidth f
fuse depth (WithPageWidth f) = WithPageWidth (\x => fuse depth $ f x)
fuse Shallow (Nesting f) = Nesting f
fuse depth (Nesting f) = Nesting (\x => fuse depth $ f x)
fuse depth x = x

||| This data type represents laid out documents and is used by the display functions.
public export
data SimpleDocStream : Type -> Type where
  SEmpty : SimpleDocStream ann
  SChar : (c : Char) -> (rest : Lazy (SimpleDocStream ann)) -> SimpleDocStream ann
  SText : (len : Int) -> (text : String) -> (rest : Lazy (SimpleDocStream ann)) -> SimpleDocStream ann
  SLine : (i : Int) -> (rest : SimpleDocStream ann) -> SimpleDocStream ann
  SAnnPush : ann -> (rest : SimpleDocStream ann) -> SimpleDocStream ann
  SAnnPop : (rest : SimpleDocStream ann) -> SimpleDocStream ann

internalError : SimpleDocStream ann
internalError = let msg = "<internal pretty printing error>" in
                    SText (cast $ length msg) msg SEmpty

data AnnotationRemoval = Remove | DontRemove

||| Changes the annotation of a document to a different annotation or none.
export
alterAnnotationsS : (ann -> Maybe ann') -> SimpleDocStream ann -> SimpleDocStream ann'
alterAnnotationsS re = fromMaybe internalError . go []
  where
    go : List AnnotationRemoval -> SimpleDocStream ann -> Maybe (SimpleDocStream ann')
    go stack SEmpty = pure SEmpty
    go stack (SChar c rest) = SChar c . delay <$> go stack rest
    go stack (SText l t rest) = SText l t . delay <$> go stack rest
    go stack (SLine l rest) = SLine l <$> go stack rest
    go stack (SAnnPush ann rest) = case re ann of
      Nothing => go (Remove :: stack) rest
      Just ann' => SAnnPush ann' <$> go (DontRemove :: stack) rest
    go stack (SAnnPop rest) = case stack of
      [] => Nothing
      DontRemove :: stack' => SAnnPop <$> go stack' rest
      Remove :: stack' => go stack' rest

||| Removes all annotations.
export
unAnnotateS : SimpleDocStream ann -> SimpleDocStream xxx
unAnnotateS SEmpty = SEmpty
unAnnotateS (SChar c rest) = SChar c (unAnnotateS rest)
unAnnotateS (SText l t rest) = SText l t (unAnnotateS rest)
unAnnotateS (SLine l rest) = SLine l (unAnnotateS rest)
unAnnotateS (SAnnPush ann rest) = unAnnotateS rest
unAnnotateS (SAnnPop rest) = unAnnotateS rest

||| Changes the annotation of a document.
export
reAnnotateS : (ann -> ann') -> SimpleDocStream ann -> SimpleDocStream ann'
reAnnotateS re SEmpty = SEmpty
reAnnotateS re (SChar c rest) = SChar c (reAnnotateS re rest)
reAnnotateS re (SText l t rest) = SText l t (reAnnotateS re rest)
reAnnotateS re (SLine l rest) = SLine l (reAnnotateS re rest)
reAnnotateS re (SAnnPush ann rest) = SAnnPush (re ann) (reAnnotateS re rest)
reAnnotateS re (SAnnPop rest) = SAnnPop (reAnnotateS re rest)

export
Functor SimpleDocStream where
  map = reAnnotateS

||| Collects all annotations from a document.
export
collectAnnotations : Monoid m => (ann -> m) -> SimpleDocStream ann -> m
collectAnnotations f SEmpty = neutral
collectAnnotations f (SChar c rest) = collectAnnotations f rest
collectAnnotations f (SText l t rest) = collectAnnotations f rest
collectAnnotations f (SLine l rest) = collectAnnotations f rest
collectAnnotations f (SAnnPush ann rest) = f ann <+> collectAnnotations f rest
collectAnnotations f (SAnnPop rest) = collectAnnotations f rest

||| Transform a document based on its annotations.
export
traverse : Applicative f => (ann -> f ann') -> SimpleDocStream ann -> f (SimpleDocStream ann')
traverse f SEmpty = pure SEmpty
traverse f (SChar c rest) = SChar c . delay <$> traverse f rest
traverse f (SText l t rest) = SText l t . delay <$> traverse f rest
traverse f (SLine l rest) = SLine l <$> traverse f rest
traverse f (SAnnPush ann rest) = SAnnPush <$> f ann <*> traverse f rest
traverse f (SAnnPop rest) = SAnnPop <$> traverse f rest

data WhitespaceStrippingState = AnnotationLevel Int | RecordedWithespace (List Int) Int

dropWhileEnd : (a -> Bool) -> List a -> List a
dropWhileEnd p = foldr (\x, xs => if p x && isNil xs then [] else x :: xs) []

||| Removes all trailing space characters.
export
removeTrailingWhitespace : SimpleDocStream ann -> SimpleDocStream ann
removeTrailingWhitespace = fromMaybe internalError . go (RecordedWithespace [] 0)
  where
    prependEmptyLines : List Int -> SimpleDocStream ann -> SimpleDocStream ann
    prependEmptyLines is sds0 = foldr (\_, sds => SLine 0 sds) sds0 is

    commitWhitespace : List Int -> Int -> SimpleDocStream ann -> SimpleDocStream ann
    commitWhitespace [] 0 sds = sds
    commitWhitespace [] 1 sds = SChar ' ' sds
    commitWhitespace [] n sds = SText n (textSpaces n) sds
    commitWhitespace (i :: is) n sds = prependEmptyLines is (SLine (i + n) sds)

    go : WhitespaceStrippingState -> SimpleDocStream ann -> Maybe (SimpleDocStream ann)
    go (AnnotationLevel _) SEmpty = pure SEmpty
    go l@(AnnotationLevel _) (SChar c rest) = SChar c . delay <$> go l rest
    go l@(AnnotationLevel _) (SText lt text rest) = SText lt text . delay <$> go l rest
    go l@(AnnotationLevel _) (SLine i rest) = SLine i <$> go l rest
    go (AnnotationLevel l) (SAnnPush ann rest) = SAnnPush ann <$> go (AnnotationLevel (l + 1)) rest
    go (AnnotationLevel l) (SAnnPop rest) =
      if l > 1
         then SAnnPop <$> go (AnnotationLevel (l - 1)) rest
         else SAnnPop <$> go (RecordedWithespace [] 0) rest
    go (RecordedWithespace _ _) SEmpty = pure SEmpty
    go (RecordedWithespace lines spaces) (SChar ' ' rest) = go (RecordedWithespace lines (spaces + 1)) rest
    go (RecordedWithespace lines spaces) (SChar c rest) =
      do rest' <- go (RecordedWithespace [] 0) rest
         pure $ commitWhitespace lines spaces (SChar c rest')
    go (RecordedWithespace lines spaces) (SText l text rest) =
      let stripped = pack $ dropWhileEnd (== ' ') $ unpack text
          strippedLength = cast $ length stripped
          trailingLength = l - strippedLength in
          if strippedLength == 0
             then go (RecordedWithespace lines (spaces + l)) rest
             else do rest' <- go (RecordedWithespace [] trailingLength) rest
                     pure $ commitWhitespace lines spaces (SText strippedLength stripped rest')
    go (RecordedWithespace lines spaces) (SLine i rest) = go (RecordedWithespace (i :: lines) 0) rest
    go (RecordedWithespace lines spaces) (SAnnPush ann rest) =
      do rest' <- go (AnnotationLevel 1) rest
         pure $ commitWhitespace lines spaces (SAnnPush ann rest')
    go (RecordedWithespace lines spaces) (SAnnPop _) = Nothing

public export
FittingPredicate : Type -> Type
FittingPredicate ann = Int -> Int -> Maybe Int -> SimpleDocStream ann -> Bool

data LayoutPipeline ann = Nil | Cons Int (Doc ann) (LayoutPipeline ann) | UndoAnn (LayoutPipeline ann)

export
defaultPageWidth : PageWidth
defaultPageWidth = AvailablePerLine 80 1

round : Double -> Int
round x = if x > 0
             then if x - floor x < 0.5 then cast $ floor x else cast $ ceiling x
             else if ceiling x - x < 0.5 then cast $ ceiling x else cast $ floor x

||| The remaining width on the current line.
remainingWidth : Int -> Double -> Int -> Int -> Int
remainingWidth lineLength ribbonFraction lineIndent currentColumn =
  let columnsLeftInLine = lineLength - currentColumn
      ribbonWidth = (max 0 . min lineLength . round) (cast lineLength * ribbonFraction)
      columnsLeftInRibbon = lineIndent + ribbonWidth - currentColumn in
      min columnsLeftInLine columnsLeftInRibbon

public export
record LayoutOptions where
  constructor MkLayoutOptions
  layoutPageWidth : PageWidth

export
defaultLayoutOptions : LayoutOptions
defaultLayoutOptions = MkLayoutOptions defaultPageWidth

||| The Wadler/Leijen layout algorithm.
export
layoutWadlerLeijen : FittingPredicate ann -> PageWidth -> Doc ann -> SimpleDocStream ann
layoutWadlerLeijen fits pageWidth_ doc = best 0 0 (Cons 0 doc Nil)
  where
    initialIndentation : SimpleDocStream ann -> Maybe Int
    initialIndentation (SLine i _) = Just i
    initialIndentation (SAnnPush _ s) = initialIndentation s
    initialIndentation (SAnnPop s) = initialIndentation s
    initialIndentation _ = Nothing

    selectNicer : Int -> Int -> SimpleDocStream ann -> Lazy (SimpleDocStream ann) -> SimpleDocStream ann
    selectNicer lineIndent currentColumn x y =
      if fits lineIndent currentColumn (initialIndentation y) x then x else y

    best : Int -> Int -> LayoutPipeline ann -> SimpleDocStream ann
    best _ _ Nil = SEmpty
    best nl cc (UndoAnn ds) = SAnnPop (best nl cc ds)
    best nl cc (Cons i Empty ds) = best nl cc ds
    best nl cc (Cons i (Chara c) ds) = SChar c (best nl (cc + 1) ds)
    best nl cc (Cons i (Text l t) ds) = SText l t (best nl (cc + l) ds)
    best nl cc (Cons i Line ds) = let x = best i i ds
                                      i' = case x of
                                                SEmpty => 0
                                                SLine _ _ => 0
                                                _ => i in
                                      SLine i' x
    best nl cc c@(Cons i (FlatAlt x y) ds) = best nl cc $ assert_smaller c (Cons i x ds)
    best nl cc (Cons i (Cat x y) ds) = assert_total $ best nl cc (Cons i x (Cons i y ds))
    best nl cc c@(Cons i (Nest j x) ds) = best nl cc $ assert_smaller c (Cons (i + j) x ds)
    best nl cc c@(Cons i (Union x y) ds) = let x' = best nl cc $ assert_smaller c (Cons i x ds)
                                               y' = delay $ best nl cc $ assert_smaller c (Cons i y ds) in
                                               selectNicer nl cc x' y'
    best nl cc c@(Cons i (Column f) ds) = best nl cc $ assert_smaller c (Cons i (f cc) ds)
    best nl cc c@(Cons i (WithPageWidth f) ds) = best nl cc $ assert_smaller c (Cons i (f pageWidth_) ds)
    best nl cc c@(Cons i (Nesting f) ds) = best nl cc $ assert_smaller c (Cons i (f i) ds)
    best nl cc c@(Cons i (Annotated ann x) ds) = SAnnPush ann $ best nl cc $ assert_smaller c (Cons i x (UndoAnn ds))

||| Layout a document with unbounded page width.
export
layoutUnbounded : Doc ann -> SimpleDocStream ann
layoutUnbounded = layoutWadlerLeijen (\_, _, _, sdoc => True) Unbounded

fits : Int -> SimpleDocStream ann -> Bool
fits w s = if w < 0 then False
  else case s of
            SEmpty => True
            SChar _ x => fits (w - 1) x
            SText l _ x => fits (w - l) x
            SLine i x => True
            SAnnPush _ x => fits w x
            SAnnPop x => fits w x

||| The default layout algorithm.
export
layoutPretty : LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutPretty (MkLayoutOptions pageWidth_@(AvailablePerLine lineLength ribbonFraction)) =
    layoutWadlerLeijen (\lineIndent, currentColumn, _, sdoc =>
      fits (remainingWidth lineLength ribbonFraction lineIndent currentColumn) sdoc) pageWidth_
layoutPretty (MkLayoutOptions Unbounded) = layoutUnbounded

||| Layout algorithm with more lookahead than layoutPretty.
export
layoutSmart : LayoutOptions -> Doc ann -> SimpleDocStream ann
layoutSmart (MkLayoutOptions pageWidth_@(AvailablePerLine lineLength ribbonFraction)) =
    layoutWadlerLeijen fits pageWidth_
  where
    fits : Int -> Int -> Maybe Int -> SimpleDocStream ann -> Bool
    fits lineIndent currentColumn initialIndentY sdoc = go availableWidth sdoc
      where
        availableWidth : Int
        availableWidth = remainingWidth lineLength ribbonFraction lineIndent currentColumn

        minNestingLevel : Int
        minNestingLevel = case initialIndentY of
                               Just i => min i currentColumn
                               Nothing => currentColumn

        go : Int -> SimpleDocStream ann -> Bool
        go w s = if w < 0
          then False
          else case s of
                    SEmpty => True
                    SChar _ x => go (w - 1) $ assert_smaller s x
                    SText l _ x => go (w - l) $ assert_smaller s x
                    SLine i x => if minNestingLevel < i
                                    then go (lineLength - i) $ assert_smaller s x
                                    else True
                    SAnnPush _ x => go w x
                    SAnnPop x => go w x
layoutSmart (MkLayoutOptions Unbounded) = layoutUnbounded

||| Lays out the document without adding any indentation. This layouter is very fast.
export
layoutCompact : Doc ann -> SimpleDocStream ann
layoutCompact doc = scan 0 [doc]
  where
    scan : Int -> List (Doc ann) -> SimpleDocStream ann
    scan _ [] = SEmpty
    scan col (Empty :: ds) = scan col ds
    scan col ((Chara c) :: ds) = SChar c (scan (col + 1) ds)
    scan col ((Text l t) :: ds) = SText l t (scan (col + l) ds)
    scan col s@((FlatAlt x _) :: ds) = scan col $ assert_smaller s (x :: ds)
    scan col (Line :: ds) = SLine 0 (scan 0 ds)
    scan col s@((Cat x y) :: ds) = scan col $ assert_smaller s (x :: y :: ds)
    scan col s@((Nest _ x) :: ds) = scan col $ assert_smaller s (x :: ds)
    scan col s@((Union _ y) :: ds) = scan col $ assert_smaller s (y :: ds)
    scan col s@((Column f) :: ds) = scan col $ assert_smaller s (f col :: ds)
    scan col s@((WithPageWidth f) :: ds) = scan col $ assert_smaller s (f Unbounded :: ds)
    scan col s@((Nesting f) :: ds) = scan col $ assert_smaller s (f 0 :: ds)
    scan col s@((Annotated _ x) :: ds) = scan col $ assert_smaller s (x :: ds)

------------------------------------------------------------------------
-- Turn the document into a string
------------------------------------------------------------------------

export
renderShow : SimpleDocStream ann -> (String -> String)
renderShow SEmpty = id
renderShow (SChar c x) = (strCons c) . renderShow x
renderShow (SText _ t x) = (t ++) . renderShow x
renderShow (SLine i x) = ((strCons '\n' $ textSpaces i) ++) . renderShow x
renderShow (SAnnPush _ x) = renderShow x
renderShow (SAnnPop x) = renderShow x

export
Show (Doc ann) where
  show doc = renderShow (layoutPretty defaultLayoutOptions doc) ""

------------------------------------------------------------------------
-- Turn the document into a string, and a list of annotation spans
------------------------------------------------------------------------

public export
record Span (a : Type) where
  constructor MkSpan
  start    : Nat
  length   : Nat
  property : a

export
Functor Span where
  map f = { property $= f }

export
Foldable Span where
  foldr c n span = c span.property n

export
Traversable Span where
  traverse f (MkSpan start width prop)
    = MkSpan start width <$> f prop

export
Show a => Show (Span a) where
  show (MkSpan start width prop)
    = concat {t = List} [ "[", show start, "-", show width, "]"
                        , show prop
                        ]

export
displaySpans : SimpleDocStream a -> (String, List (Span a))
displaySpans p =
  let (bits, anns) = go Z [<] [<] [] p in
  (concat bits, anns)

  where

    go : (index : Nat) ->
         (doc   : SnocList String) ->
         (spans : SnocList (Span a)) ->
         (ann : List (Nat, a)) -> -- starting index, < current
         SimpleDocStream a ->
         (List String, List (Span a))
    go index doc spans ann SEmpty = (doc <>> [], spans <>> [])
    go index doc spans ann (SChar c rest)
      = go (S index) (doc :< cast c) spans ann rest
    go index doc spans ann (SText len text rest)
      = go (integerToNat (cast len) + index) (doc :< text) spans ann rest
    go index doc spans ann (SLine i rest)
      = let text = strCons '\n' (textSpaces i) in
        go (S (integerToNat $ cast i) + index) (doc :< text) spans ann rest
    go index doc spans ann (SAnnPush a rest)
      = go index doc spans ((index, a) :: ann) rest
    go index doc spans ((start, a) :: ann) (SAnnPop rest)
      = let span = MkSpan start (minus index start) a in
        go index doc (spans :< span) ann rest
    go index doc spans [] (SAnnPop rest)
      = go index doc spans [] rest


text:
module Html

import Js.VirtualDom
import Js.Utils

%include JavaScript "js/html.js"

public export
Html : Type -> Type
Html a = Node 'Html a

export
interface HtmlAllAttribute (o : Type) where

public export
HtmlAttribute : Type -> Type
HtmlAttribute a = Attribute 'HtmlAttribute a

public export
InputAttribute : Type -> Type
InputAttribute a = Attribute 'InputAttribute a

public export
KeyEvtAttribute : Type -> Type
KeyEvtAttribute a = Attribute 'KeyEvtAttribute a

export
implementation HtmlAllAttribute 'HtmlAttribute where

export
implementation HtmlAllAttribute 'InputAttribute where

export
implementation HtmlAllAttribute 'KeyEvtAttribute where

-------- Nodes --------

export
div : List (HtmlAttribute a) -> List (Html a) -> Html a
div = node "div"

export
span : List (HtmlAttribute a) -> List (Html a) -> Html a
span = node "span"

export
emptySpan : Html a
emptySpan = span [] []

export
input : List (InputAttribute a) -> Html a
input attrs = node "input" attrs []

export
form : List (HtmlAttribute a) -> a -> List (Html a) -> Html a
form attrs val childs =
  node
  "form"
  (eventListenerAttributePreventDefault "submit" (\_ => pure val) :: attrs)
  childs

export
button : List (HtmlAttribute a) -> String -> Html a
button attrs txt = node "button" attrs [text txt]

export
img : List (HtmlAttribute a) -> String -> Html a
img attrs url =
  node
    "img"
    (stringAttribute "src" url :: attrs)
    []

-------- Attributes --------

export
value : String -> Attribute 'InputAttribute a
value v = propertyAttribute "value" v

export
cssClass : HtmlAllAttribute o => String -> Attribute o a
cssClass s = stringAttribute "class" s

export
tabindex : HtmlAllAttribute o => Int -> Attribute o a
tabindex idx = stringAttribute "tabindex" (show idx)

-------- Events --------

export
onclick : HtmlAllAttribute o => a -> Attribute o a
onclick x = eventListenerAttribute "click" (\_ => pure x)

export
onchange : (String -> a) -> Attribute 'InputAttribute a
onchange convert =
  eventListenerAttribute
  "change"
  (\x => convert <$> jscall "%0.target.value" (Ptr -> JS_IO String) x)

export
onlongpress : HtmlAllAttribute o => a -> Attribute o a
onlongpress x = customEventListenerAttribute "longpress" (jscall "$JSLIB$html.addLongPressEventListener(%0)" (Ptr -> JS_IO ())) (\_ => pure x)

export
onshortpress : HtmlAllAttribute o => a -> Attribute o a
onshortpress x = customEventListenerAttribute "shortpress" (jscall "$JSLIB$html.addShortPressEventListener(%0)" (Ptr -> JS_IO ())) (\_ => pure x)

public export
record KeyEvent where
  constructor MkKeyEvent
  altKey : Bool
  char : String
  code : String
  ctrlKey : Bool
  isComposing : Bool
  key : String
  keyCode : Int
  locale : String
  location : Int
  metaKey : Bool
  repeat : Bool
  shiftKey : Bool

keyRecordOfEvent : Ptr -> JS_IO KeyEvent
keyRecordOfEvent x =
  do
    altKey <- jscall "%0.altKey" (Ptr -> JS_IO Int) x
    char <- jscall "%0.char" (Ptr -> JS_IO String) x
    code <- jscall "%0.code" (Ptr -> JS_IO String) x
    ctrlKey <- jscall "%0.ctrlKey" (Ptr -> JS_IO Int) x
    isComposing <- jscall "%0.isComposing" (Ptr -> JS_IO Int) x
    key <- jscall "%0.key" (Ptr -> JS_IO String) x
    keyCode <- jscall "%0.keyCode" (Ptr -> JS_IO Int) x
    locale <- jscall "%0.locale" (Ptr -> JS_IO String) x
    location <- jscall "%0.location" (Ptr -> JS_IO Int) x
    metaKey <- jscall "%0.metaKey" (Ptr -> JS_IO Int) x
    repeat <- jscall "%0.repeat" (Ptr -> JS_IO Int) x
    shiftKey <- jscall "%0.shiftKey" (Ptr -> JS_IO Int) x
    pure (MkKeyEvent (altKey /= 0) char code (ctrlKey /= 0) (isComposing /= 0) key keyCode locale location (metaKey /= 0) (repeat /= 0) (shiftKey /= 0))

export
onkeydown : HtmlAllAttribute o => (KeyEvent -> a) -> Attribute o a
onkeydown convert =
  eventListenerAttribute "keydown"
  (\x =>
    do
      evt <- keyRecordOfEvent x
      pure (convert evt)
  )

export
onkeyup : HtmlAllAttribute o => (KeyEvent -> a) -> Attribute o a
onkeyup convert =
  eventListenerAttribute "keyup"
  (\x =>
    do
      evt <- keyRecordOfEvent x
      pure (convert evt)
  )

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: rbarreiro/idrisjs

max_forks_repo_name: rbarreiro/idrisjs


text:
||| Instances of algebraic classes (group, ring, etc) for numeric data types,
||| and Complex number types.
module Control.Algebra.NumericInstances

import Control.Algebra
import Control.Algebra.VectorSpace
import Data.Complex
import Data.ZZ

instance Semigroup Integer where
  (<+>) = (+)

instance Monoid Integer where
  neutral = 0

instance Group Integer where
  inverse = (* -1)

instance AbelianGroup Integer

instance Ring Integer where
  (<.>) = (*)

instance RingWithUnity Integer where
  unity = 1

instance Semigroup Int where
  (<+>) = (+)

instance Monoid Int where
  neutral = 0

instance Group Int where
  inverse = (* -1)

instance AbelianGroup Int

instance Ring Int where
  (<.>) = (*)

instance RingWithUnity Int where
  unity = 1

instance Semigroup Float where
  (<+>) = (+)

instance Monoid Float where
  neutral = 0

instance Group Float where
  inverse = (* -1)

instance AbelianGroup Float

instance Ring Float where
  (<.>) = (*)

instance RingWithUnity Float where
  unity = 1

instance Field Float where
  inverseM f _ = 1 / f

instance Semigroup Nat where
  (<+>) = (+)

instance Monoid Nat where
  neutral = 0

instance Semigroup ZZ where
  (<+>) = (+)

instance Monoid ZZ where
  neutral = 0

instance Group ZZ where
  inverse = (* -1)

instance AbelianGroup ZZ

instance Ring ZZ where
  (<.>) = (*)

instance RingWithUnity ZZ where
  unity = 1

instance Semigroup a => Semigroup (Complex a) where
  (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)

instance Monoid a => Monoid (Complex a) where
  neutral = (neutral :+ neutral)

instance Group a => Group (Complex a) where
  inverse (r :+ i) = (inverse r :+ inverse i)

instance Ring a => AbelianGroup (Complex a) where {}

instance Ring a => Ring (Complex a) where
  (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)

instance RingWithUnity a => RingWithUnity (Complex a) where
  unity = (unity :+ neutral)

instance RingWithUnity a => Module a (Complex a) where
  (<#>) x = map (x <.>)

instance RingWithUnity a => InnerProductSpace a (Complex a) where
  (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z

max_stars_repo_name: BlackBrane/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
import Stuff

data IsSuc : Nat -> Type where
     Yes : IsSuc (S x)

pred : (x : Nat) -> IsSuc x -> Nat
pred (S x) Yes = x

test1 : Nat -> Nat
test1 x = let y = S (S x) in
              case x of
                   res => pred y ?foo

-- Propagating let binding's computational behaviour through case is
-- not supported, sorry!
{-
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

test2 : Nat -> Nat -> Nat
test2 x@(S Z) y
    = case y of
           res =>
               let fn : Vect (S Z) Nat -> Nat
                   fn ys = ?bar
               in pred x Yes
-}


text:
module ex

-- ex 9.1.6

-- List version of Elem dependent type
data Elem : a -> List a -> Type where
     Here : Elem x (x::xs)
     There : (later : Elem x xs) -> Elem x (y::xs)

data Last : List a -> a -> Type where
     LastOne : Last [value] value
     LastCons : (prf : Last xs value) -> Last (x :: xs) value

notInNil : Last [] value -> Void
notInNil LastOne impossible
notInNil (LastCons _) impossible

single : (contra : (x = value) -> Void) -> Last [x] value -> Void
single contra LastOne = contra Refl
single _ (LastCons LastOne) impossible
single _ (LastCons (LastCons _)) impossible

noGood : (contra : Last (y :: ys) value -> Void) -> Last (x :: (y :: ys)) value -> Void
noGood contra (LastCons prf) = contra prf

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No notInNil
isLast (x :: []) value = case decEq x value of
                              (Yes Refl) => Yes LastOne
                              (No contra) => No (single contra)
isLast (x :: (y :: ys)) value = case isLast (y :: ys) value of
                                     (Yes prf) => Yes (LastCons prf)
                                     (No contra) => No (noGood contra)


text:
||| Spec: https://webassembly.github.io/spec/core/valid/types.html#table-types
module WebAssembly.Validation.Types.TableTypes

import WebAssembly.Structure
import WebAssembly.Validation.Types.Limits

public export
MAX_LIMIT_TABLE : Nat
MAX_LIMIT_TABLE = power 2 4  -- set to (power 2 32) for original WebAssembly behvaiour WARNING: type-checking then takes like forever

-------------------------------------------------------------------------------
-- Validation Rules
-------------------------------------------------------------------------------

public export
data ValidTableType : TableType -> Type where
  MkValidTableType : (limits : Limits)
                  -> (elementType : ElemType)
                  -> (limits_valid: ValidLimits limits MAX_LIMIT_TABLE)
                  -> ValidTableType (limits, elementType)

-------------------------------------------------------------------------------
-- Lemmas about table-type validation
-------------------------------------------------------------------------------

total invalid_limit : (contra : ValidLimits limits MAX_LIMIT_TABLE -> Void) -> ValidTableType (limits, elemType) -> Void
invalid_limit contra (MkValidTableType limits elemType limits_valid) = contra limits_valid

-------------------------------------------------------------------------------
-- Decidablity of Validation
-------------------------------------------------------------------------------

total public export
isTableTypeValid : (tableType : TableType) -> Dec (ValidTableType tableType)
isTableTypeValid (limits, elemType) = case (isLimitsValid limits MAX_LIMIT_TABLE) of
  No contra => No (invalid_limit contra)
  Yes prof  => Yes (MkValidTableType limits elemType prof)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
import System
import System.Info

main : IO ()
main = do
  Just expectedOs <- getEnv "EXPECTED_OS"
    | Nothing => do
      putStrLn "EXPECTED_OS unset"
      exitFailure
  case os == expectedOs of
    True => putStrLn "correct"
    False => do
      putStrLn ("os=" ++ os ++ " expected=" ++ expectedOs)
      exitFailure


text:
data N = Z | Suc N

one : N
one = Suc Z

max_stars_repo_name: hjorthjort/IdrisToAgda

max_issues_repo_name: hjorthjort/IdrisToAgda

max_forks_repo_name: hjorthjort/IdrisToAgda


text:
module Replica.Option.Parse

import Replica.Other.Validation
import Replica.Other.Decorated
import Replica.Option.Global

import Control.Monad.Identity
import Control.Monad.RWS
import Data.Either
import Data.List
import Data.List1
import Data.String
import System
import System.File
import System.Path

import Language.JSON

validateReplicaDir : JSON -> Validation (List String) String
validateReplicaDir (JString x) = Valid x
validateReplicaDir x = Error ["Replica dir must be a string, found: \{show x}"]

validateGoldenDir : JSON -> Validation (List String) String
validateGoldenDir (JString x) = Valid x
validateGoldenDir x = Error ["Goldendir must be a string, found: \{show x}"]

validateColour : JSON -> Validation (List String) Bool
validateColour (JBoolean x) = Valid x
validateColour x = Error ["Colour must be a boolean, found: \{show x}"]

validateAscii : JSON -> Validation (List String) Bool
validateAscii (JBoolean x) = Valid x
validateAscii x = Error ["Ascii must be a boolean, found: \{show x}"]

invalidLogLevel : Validation (List String) a
invalidLogLevel = Error ["LogLevel must be either none, debug, info, warning, or critical"]

validateLogLevel : JSON -> Validation (List String) (Maybe LogLevel)
validateLogLevel (JString x) = maybe invalidLogLevel Valid $ readLogLevel x
validateLogLevel x = invalidLogLevel

validateDiff : JSON -> Validation (List String) DiffCommand
validateDiff (JString x) = Valid $ readDiffCommand x
validateDiff x = Error ["Diff should be a string"]

validateFile : JSON -> Validation (List String) String
validateFile (JString x) = Valid x
validateFile x = Error ["File should be a string"]

export
record ConfigValue where
  constructor CfgValue
  primary : String
  secondaries : List String
  parser : String -> Maybe JSON

(.keys) : ConfigValue -> List1 String
(.keys) x = x.primary ::: x.secondaries

export
checkKey : ConfigValue -> String -> Maybe String
checkKey x y = guard (y `elem` forget x.keys) $> x.primary

export
getKey : ConfigValue -> (String, a) -> Maybe a
getKey x (k, v) = guard (k `elem` forget x.keys) $> v

export
jsonFor: ConfigValue -> (String, String) -> Maybe (String, JSON)
jsonFor x kv = getKey x kv >>= map (MkPair x.primary) . x.parser

replicaDirValues : ConfigValue
replicaDirValues = CfgValue "replicaDir" ["replica-dir", "rDir"]
  (Just . JString)

goldenDirValues : ConfigValue
goldenDirValues = CfgValue "goldenDir" ["golden-dir", "gDir"]
  (Just . JString)

colourValues : ConfigValue
colourValues = CfgValue "colour" ["color"]
  (\x => case toLower x of
              "true" => Just $ JBoolean True
              "false" => Just $ JBoolean False
              _ => Nothing)

asciiValues : ConfigValue
asciiValues = CfgValue "ascii" []
  (\x => case toLower x of
              "true" => Just $ JBoolean True
              "false" => Just $ JBoolean False
              _ => Nothing)

logValues : ConfigValue
logValues = CfgValue "logLevel" ["log-level", "log"]
  (\x => readLogLevel x $> JString x)

diffValues : ConfigValue
diffValues = CfgValue "diff" []
  (Just . JString)

testFileValues : ConfigValue
testFileValues= CfgValue "testFile" ["jsonFile", "test"]
  (Just . JString)

export
configValues : List ConfigValue
configValues =
  [ replicaDirValues
  , goldenDirValues
  , colourValues
  , asciiValues
  , logValues
  , diffValues
  , testFileValues]

jsonConfig : JSON -> Default Global'
jsonConfig (JObject xs) = MkGlobal
  (foldMap (getKey replicaDirValues) xs >>= toMaybe . validateReplicaDir)
  (foldMap (getKey goldenDirValues) xs >>= map Just . toMaybe . validateGoldenDir)
  (foldMap (getKey colourValues) xs >>= toMaybe . validateColour)
  (foldMap (getKey asciiValues) xs >>= toMaybe . validateAscii)
  (foldMap (getKey logValues) xs >>= toMaybe . validateLogLevel)
  (foldMap (getKey diffValues) xs >>= toMaybe . validateDiff)
  (foldMap (getKey testFileValues) xs >>= toMaybe . map pure . validateFile)
jsonConfig json = neutral

export
configPath : IO (List String)
configPath = do
  Just global <- map (</> ".replica.json") <$> getEnv "HOME"
    | Nothing => pure [".replica.json"]
  pure [global </> ".replica.json", ".replica.json"]

export
givenConfig : IO (Default Global')
givenConfig = do
  path <- configPath
  xs <- catMaybes . map JSON.parse . rights <$> traverse readFile path
  pure $ concatMap jsonConfig xs

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A command line argument parser
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Options.Applicative.Builder

import public Text.PrettyPrint.WL
import        Options.Applicative.Types
import        Control.Monad.Trans
import        Control.Lens

%default total
%access public export

optRdr : Lens' (Option x a) (OptReader x a)
optRdr (Mor f) = Mor $ \(Opt props rdr) => Opt props <$> f rdr

optProps : Lens' (Option x a) (OptProperties)
optProps (Mor f) = Mor $ \(Opt props rdr) => flip Opt rdr <$> f props

interface HasMeta d where
  meta : {f : Type -> Type} -> Functor f => LensLike' f d String

HasMeta (OptReader OptionParams a) where
  meta (Mor f) = Mor $ \(OptionReader n p m) => OptionReader n p <$> f m

HasMeta (OptReader ArgParams a) where
  meta (Mor f) = Mor $ \(ArgReader p m) => ArgReader p <$> f m

HasMeta (OptReader CmdParams a) where
  meta (Mor f) = Mor $ \(CmdReader ps m) => CmdReader ps <$> f m

HasMeta (OptReader x a) => HasMeta (Option x a) where
  meta = optRdr . meta

interface HasName d where
  names : {f : Type -> Type} -> Functor f => LensLike' f d (List OptName)

HasName (OptReader OptionParams a) where
  names (Mor f) = Mor $ \(OptionReader n p m) => (\n' => OptionReader n' p m) <$> f n

HasName (OptReader FlagParams a) where
  names (Mor f) = Mor $ \(FlagReader n d) => flip FlagReader d <$> f n

HasName (OptReader x a) => HasName (Option x a) where
  names = optRdr . names

short : HasName d => Char -> d -> d
short c = over names (\ns => ShortName c :: ns)

long : HasName d => String -> d -> d
long c = over names (\ns => LongName c :: ns)

interface HasSubCommands d a where
  cmds : {f : Type -> Type} -> Functor f => LensLike' f d (List (String, (Parser a)))

HasSubCommands (OptReader CmdParams a) a where
  cmds (Mor f) = Mor $ \(CmdReader ps m) => flip CmdReader m <$> f ps

HasSubCommands (Option CmdParams a) a where
  cmds = optRdr . cmds

cmd : HasSubCommands d a => String -> Parser a -> d -> d
cmd n p = over cmds (\ns => (n,p) :: ns)

interface HasHelp d where
  help : {f : Type -> Type} -> Functor f => LensLike' f d Doc

HasHelp OptProperties where
  help (Mor f) = Mor $ \(MkOptProperties vis hdoc) => MkOptProperties vis <$> f hdoc

HasHelp (Option x a) where
  help = optProps . help

interface HasVisibility d where
  visibility : {f : Type -> Type} -> Functor f => LensLike' f d Visibility

HasVisibility OptProperties where
  visibility (Mor f) = Mor $ \(MkOptProperties vis hdoc) => flip MkOptProperties hdoc <$> f vis

HasVisibility (Option x a) where
  visibility = optProps . visibility

hide : HasVisibility d => d -> d
hide = visibility .~ Hidden

internal : HasVisibility d => d -> d
internal = visibility .~ Internal

interface HasValue (d : Type -> Type) where
  value : {a, b : Type} -> {f : Type -> Type} -> Functor f => LensLike f (d a) (d b) a b

HasValue (OptReader FlagParams) where
  value (Mor f) = Mor $ \(FlagReader n d) => FlagReader n <$> f d

HasValue (Option FlagParams) where
  value (Mor f) = Mor $ \(Opt props (FlagReader n d)) => (Opt props . FlagReader n) <$> f d

defProps : OptProperties
defProps = MkOptProperties Visible empty

option : (String -> Either ParseError a) -> (Option OptionParams a -> Option OptionParams a) -> Parser a
option rdr f = OptP $ f $ Opt defProps (OptionReader [] rdr "OPT")

strOption : (Option OptionParams String -> Option OptionParams String) -> Parser String
strOption = option Right

arg : (String -> Either ParseError a) -> (Option ArgParams a -> Option ArgParams a) -> Parser a
arg rdr f = OptP $ f $ Opt defProps (ArgReader rdr "ARG")

strArg : (Option ArgParams String -> Option ArgParams String) -> Parser String
strArg = arg Right

flag' : a -> (Option FlagParams a -> Option FlagParams a) -> Parser a
flag' d f = OptP $ f $ Opt defProps (FlagReader [] d)

flag : (Option FlagParams Bool -> Option FlagParams a) -> Parser a
flag f = OptP $ f $ Opt defProps (FlagReader [] True)

subparser : (Option CmdParams a -> Option CmdParams a) -> Parser a
subparser f = OptP $ f $ Opt defProps (CmdReader [] "COMMAND")

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

max_stars_repo_name: statebox/optparse-idris

max_issues_repo_name: statebox/optparse-idris

max_forks_repo_name: statebox/optparse-idris