text:
module Language.LSP.CodeAction.RefineHole

import Core.Case.CaseTree
import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.String
import Idris.REPL.Common
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.CodeAction.Utils
import Language.LSP.Message
import Language.LSP.Message.Derive
import Language.Reflection
import Libraries.Data.NameMap
import Parser.Source
import Parser.Rule.Source
import Server.Configuration
import Server.Log
import Server.Utils
import TTImp.Interactive.ExprSearch
import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Utils

%language ElabReflection
%hide TT.Name

export
record RefineHoleWithHintsParams where
  constructor MkRefineHoleWithHintsParams
  codeAction : CodeActionParams
  hints : List String

%runElab deriveJSON defaultOpts `{RefineHoleWithHintsParams}

dropLams : Nat -> RawImp -> RawImp
dropLams Z tm = tm
dropLams (S k) (ILam _ _ _ _ _ sc) = dropLams k sc
dropLams _ tm = tm

dropLamsTm : {vars : _} -> Nat -> Env Term vars -> Term vars -> (vars' ** (Env Term vars', Term vars'))
dropLamsTm Z env tm = (_ ** (env, tm))
dropLamsTm (S k) env (Bind _ _ b sc) = dropLamsTm k (b :: env) sc
dropLamsTm _ env tm = (_ ** (env, tm))

isHole : Defs -> Name -> Core Bool
isHole defs n = do
  Just def <- lookupCtxtExact n defs.gamma
    | Nothing => pure False
  pure $ case def.definition of
    Hole _ _ => True
    _        => False

isRawHole : RawImp' nm -> Bool
isRawHole (ILam fc x y z argTy lamTy) = isRawHole lamTy
isRawHole (IHole fc x) = False
isRawHole _ = True

||| Checks if the name is visible in the namespace of the hole.
checkVisibleName : Ref Ctxt Defs => Name -> Name -> GlobalDef -> Core Bool
checkVisibleName hole name def = do
  (Just nameNS, _) <- displayName <$> toFullNames name
    | _ => pure False
  (Just holeNS, _) <- displayName <$> toFullNames hole
    | _ => pure False
  if nameNS == holeNS
     then pure True
     else pure $ !(isVisible nameNS) && def.visibility /= Private

||| Check if the name has the exact type and is not a hole
nameHasType : Ref LSPConf LSPConfiguration
           => Ref Ctxt Defs
           => Ref MD Metadata
           => Ref UST UState
           => Name -> Name -> ClosedTerm -> Core Bool
nameHasType hole name expected = do
  defs <- get Ctxt
  Just def <- lookupCtxtExact name defs.gamma
    | Nothing => pure False
  True <- checkVisibleName hole name def
    | False => pure False
  nt <- normaliseAll defs [] def.type
  ex <- normaliseAll defs [] expected
  equivTypes nt ex

findFirstN : Nat -> (a -> Core (Maybe b)) -> List a -> Core (List b)
findFirstN Z f xs = pure []
findFirstN (S k) f [] = pure []
findFirstN (S k) f (x :: xs) = case !(f x) of
  Nothing => findFirstN (S k) f xs
  Just y  => (y ::) <$> findFirstN k f xs

||| Keeps the name with same preffix as the hole, ignoring namespaces.
typeMatchingNames : Ref LSPConf LSPConfiguration
                 => Ref Ctxt Defs
                 => Ref MD Metadata
                 => Ref UST UState
                 => Name -> ClosedTerm -> Nat -> Core (List Name)
typeMatchingNames hole ty limit = do
  defs <- get Ctxt
  let holeUNR = userNameRoot hole
  let find = findFirstN limit $ \fun =>
        let funUNR = userNameRoot fun
         in if holeUNR /= funUNR && !(nameHasType hole fun ty)
               then pure $ Just fun
               else pure Nothing
  find $ keys $ namesResolvedAs defs.gamma

buildCodeAction : Name -> URI -> Range -> String -> CodeAction
buildCodeAction name uri range str =
  MkCodeAction
    { title       = "Refine hole on \{show $ dropAllNS name} as ~ \{strSubstr 0 50 str} ..."
    , kind        = Just RefactorRewrite
    , diagnostics = Just []
    , isPreferred = Just False
    , disabled    = Nothing
    , edit        = Just $ MkWorkspaceEdit
        { changes           = Just (singleton uri [MkTextEdit range str])
        , documentChanges   = Nothing
        , changeAnnotations = Nothing
        }
    , command     = Nothing
    , data_       = Nothing
    }

||| Tries to resolve a type like Nat, Maybe
||| It ignores the type parameters
resolveTypeName : Ref Ctxt Defs
               => Ref LSPConf LSPConfiguration
               => {vars : _}
               -> Term vars
               -> Core (Maybe Name)
resolveTypeName (Ref {name, _}) = Just <$> toFullNames name
resolveTypeName (Bind {scope, _}) = resolveTypeName scope -- ignores explicit/implicit parameters
resolveTypeName (App {fn, _}) = resolveTypeName fn        -- ignores type parameters
resolveTypeName other = logD RefineHole "resolveTypeName: \{show other}" >> pure Nothing

keepNonHoleNames : Ref Ctxt Defs => List Name -> Core (List Name)
keepNonHoleNames names = do
  defs <- get Ctxt
  filterM (map not . isHole defs) names

hasHints : List Name -> RawImp -> Bool
hasHints hs tm = not $ null $ intersect hs (findAllNames [] tm)

export
refineHoleKind : CodeActionKind
refineHoleKind = Other "refactor.rewrite.RefineHole"

isAllowed : CodeActionParams -> Bool
isAllowed params =
  maybe True (\filter => (refineHoleKind `elem` filter) || (RefactorRewrite `elem` filter)) params.context.only

refineHole' : Ref LSPConf LSPConfiguration
           => Ref MD Metadata
           => Ref Ctxt Defs
           => Ref UST UState
           => Ref Syn SyntaxInfo
           => Ref ROpts REPLOpts
           => CodeActionParams -> List Name -> Core (List CodeAction)
refineHole' params hints = do
  let True = isAllowed params
    | False => logI RefineHole "Skipped" >> pure []
  logI RefineHole "Checking for \{show params.textDocument.uri} at \{show params.range}"

  withSingleLine RefineHole params (pure []) $ \line => do
    fuel <- gets LSPConf searchLimit
    nameLocs <- gets MD nameLocMap
    let col = params.range.start.character
    let Just (loc@(_, nstart, nend), name) = findPointInTreeLoc (line, col) nameLocs
      | Nothing => logD RefineHole "No name found at \{show line}:\{show col}}" >> pure []
    logD RefineHole "Found name \{show name}"

    defs <- get Ctxt
    toBrack <- gets Syn (elemBy (\x, y => dropNS x == dropNS y) name . bracketholes)
    let showPTerm : IPTerm -> String = if toBrack then show . addBracket replFC else show
    let opts = MkSearchOpts True True Nothing 2 False False True False False Nothing
    names <- lookupCtxtName name defs.gamma
    solutions <-
      case names of
           [(n, nidx, def@(MkGlobalDef {definition = (Hole locs _), _}))] => do
             catch (do searchtms <- the (Core (List RawImp)) $ if null hints
                          then do matchingNames <- keepNonHoleNames =<< typeMatchingNames n def.type 1000
                                  similar <- keepNonHoleNames =<< maybe [] (map fst . snd) <$> getSimilarNames n
                                  fst <$> searchN fuel (exprSearchOpts opts replFC name (matchingNames ++ similar))
                          else do filtered <- filter (hasHints hints) <$> exprSearchOpts opts replFC name hints
                                  fst <$> searchN fuel filtered
                       let searchtms = filter isRawHole searchtms
                       traverse (map showPTerm . pterm . map defaultKindedName . dropLams locs) searchtms)
                   (\case Timeout _ => logI RefineHole "Timed out" >> pure []
                          err => logC RefineHole "Unexpected error while searching" >> throw err)
           [(n, nidx, def@(MkGlobalDef {definition = (PMDef pi [] (STerm _ tm) _ _), _}))] => case holeInfo pi of
             NotHole => logD RefineHole "\{show name} is not a metavariable" >> pure []
             SolvedHole locs => do
               (_ ** (env, tm')) <- dropLamsTm locs [] <$> normaliseHoles defs [] tm
               itm <- resugar env tm'
               pure [showPTerm itm]
           _ => logD RefineHole "\{show name} is not a metavariable" >> pure []

    let range = MkRange (uncurry MkPosition nstart) (uncurry MkPosition nend)
    let actions = buildCodeAction name params.textDocument.uri range <$> solutions
    pure actions

export
refineHole : Ref LSPConf LSPConfiguration
          => Ref MD Metadata
          => Ref Ctxt Defs
          => Ref UST UState
          => Ref Syn SyntaxInfo
          => Ref ROpts REPLOpts
          => CodeActionParams -> Core (List CodeAction)
refineHole params = refineHole' params []

export
refineHoleWithHints : Ref LSPConf LSPConfiguration
                   => Ref MD Metadata
                   => Ref Ctxt Defs
                   => Ref UST UState
                   => Ref Syn SyntaxInfo
                   => Ref ROpts REPLOpts
                   => RefineHoleWithHintsParams -> Core (List CodeAction)
refineHoleWithHints params = do
  defs <- get Ctxt
  hs <- for params.hints $ \str => do
    let Right (_, _, n) = runParser (Virtual Interactive) Nothing str name
      | _ => pure []
    ns <- lookupCtxtName n defs.gamma
    pure $ fst <$> ns
  refineHole' params.codeAction (concat hs)


text:
module Main

-- To solve a part for a day, import Day#.Part#
import Day3.Part1
import Day3.Part2
import Helpers.Helpers

main : IO ()
main = do
  list <- (parseFile "Day3/input.txt")
  printLn (solve list)
  printLn (solve2 list (solve list) 0 True)
  printLn (solve2 list (solve list) 0 False)

ext: idr


text:
module SQLite3.Bindings

import CUtils

libsqlite3 : String -> String
libsqlite3 x = "C:sqlite3_" <+> x <+> ",libsqlite3"

%foreign libsqlite3 "libversion"
sqlite3_libversion : PrimIO String

export data PrimHandle : Type where
export data PrimStmt : Type where

export %foreign libsqlite3 "errmsg"
sqlite3_errmsg : Ptr PrimHandle -> PrimIO String

export %foreign libsqlite3 "errcode"
sqlite3_errcode : Ptr PrimHandle -> PrimIO Int

export %foreign libsqlite3 "open"
sqlite3_open : (filename_utf8 : String) -> Ptr (Ptr PrimHandle) -> PrimIO Int

export %foreign libsqlite3 "close"
sqlite3_close : Ptr PrimHandle -> PrimIO Int

export %foreign libsqlite3 "prepare_v2"
sqlite3_prepare_v2 : Ptr PrimHandle -> (zsql : String) -> (zsql_max_len : Int) -> Ptr (Ptr PrimStmt) -> Ptr (Ptr String) -> PrimIO Int

export %foreign libsqlite3 "step"
sqlite3_step : Ptr PrimStmt -> PrimIO Int

export %foreign libsqlite3 "reset"
sqlite3_reset : Ptr PrimStmt -> PrimIO Int

export %foreign libsqlite3 "finalize"
sqlite3_finalize : Ptr PrimStmt -> PrimIO Int

export %foreign libsqlite3 "column_count"
sqlite3_column_count : Ptr PrimStmt -> PrimIO Int

export %foreign libsqlite3 "column_blob"
sqlite3_column_blob : Ptr PrimStmt -> (icol : Int) -> PrimIO AnyPtr

export %foreign libsqlite3 "column_text"
sqlite3_column_text : Ptr PrimStmt -> (icol : Int) -> PrimIO String

export %foreign libsqlite3 "column_double"
sqlite3_column_double : Ptr PrimStmt -> (icol : Int) -> PrimIO Double

||| sqlite3_column_int -> 32-bit INTEGER result
||| -- from: https://sqlite.org/c3ref/column_blob.html
||| tho the signature is `int sqlite3_column_int(sqlite3_stmt*, int iCol);`
export %foreign libsqlite3 "column_int"
sqlite3_column_int : Ptr PrimStmt -> (icol : Int) -> PrimIO Int32

export %foreign libsqlite3 "column_int64"
sqlite3_column_int64 : Ptr PrimStmt -> (icol : Int) -> PrimIO Int64

export %foreign libsqlite3 "column_bytes"
sqlite3_column_bytes : Ptr PrimStmt -> (icol : Int) -> PrimIO Int

export %foreign libsqlite3 "column_type"
sqlite3_column_type : Ptr PrimStmt -> (icol : Int) -> PrimIO Int


text:
module Test.Parser

import Text.WebIDL.Encoder
import Text.WebIDL.Parser
import Test.Generators

prp : Eq a => Show a => Encoder a -> Gen a -> IdlGrammar a -> Property
prp enc gen p = property $ do
                  v <- forAll gen
                  let str : String
                      str = enc v

                      len : Integer
                      len = natToInteger $ length str

                  classify "Length in (0000,10]"       (len <= 10)
                  classify "Length in (0010,50]"    (len > 10 && len <= 50)
                  classify "Length in (0050,100]"   (len > 50 && len <= 100)
                  classify "Length in (0100,500]"   (len > 100 && len <= 500)
                  classify "Length in (0500,1000]"  (len > 500 && len <= 1000)
                  classify "Length in (1000,10000]" (len > 1000 && len <= 10000)

                  footnote ("Encoded: " ++ str)

                  parseIdl p str === Right v

prop_other : Property
prop_other = prp other other other

prop_extAttributes : Property
prop_extAttributes = prp extAttribute (extAttribute 4) extAttribute

prop_primitiveType : Property
prop_primitiveType = prp primitive primitive primitive

prop_idlType : Property
prop_idlType = prp idlType (idlType 5) idlType

prop_const : Property
prop_const = prp const const const

prop_operation : Property
prop_operation = prp operation operation operation

prop_interfaceMember : Property
prop_interfaceMember = prp interfaceMember interfaceMember interfaceMember

prop_definition : Property
prop_definition = prp definition definition definition

prop_part : Property
prop_part = prp part part part

export
props : Group
props = MkGroup "Parser Properties"
          [ ("prop_other", prop_other)
          , ("prop_extAttributes", prop_extAttributes)
          , ("prop_primitiveType", prop_primitiveType)
          , ("prop_idlType", prop_idlType)
          , ("prop_const", prop_const)
          , ("prop_operation", prop_operation)
          , ("prop_interfaceMember", prop_interfaceMember)
          , ("prop_definition", prop_definition)
          , ("prop_part", prop_part)
          ]


text:
-- ReadVect.idr

-- Demonstrates reading of dependent types from stdin
-- e.g., reading Data.Vect of defined length

module ReadVect

import Data.Vect

||| Reads a Vect with given length
||| @len Length of Vect to be read
export
readVectLen : (len : Nat) -> IO (Vect len String)
readVectLen Z = pure []
readVectLen (S k) = do x <- getLine
                       xs <- readVectLen k
                       pure (x :: xs)

-- alternative implementation without DPairs

public export
data VectUnknown : Type -> Type where
  MkVect : (len : Nat) -> Vect len a -> VectUnknown a

||| Reads a Vect of unknown length
export
readVect2 : IO (VectUnknown String)
readVect2 = do x <- getLine
               if (x == "")
                 then pure (MkVect _ [])
                 else do MkVect _ xs <- readVect2
                         pure (MkVect _ (x :: xs))

||| Prints a vector of unknown length
export
printVect : Show a => VectUnknown a -> IO ()
printVect (MkVect len xs) =
  putStrLn (show xs ++ " (length: " ++ (show len) ++ ")\n")

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Lambda

%default total

data Ty = TyFunc Ty Ty | TyNat

data Context = Empty | Extend Context Ty

data Contains : Context -> Ty -> Type where
  Here : Contains (Extend g ty) ty
  There : (rest :  Contains g ty)
       -> Contains (Extend g not_ty) ty

data Term : Context -> Ty -> Type where
  Var : (idx : Contains g ty)
     -> Term g ty

  Func : (body : Term (Extend g tyA) tyB)
      -> Term g (TyFunc tyA tyB)

  App : (func : Term g (TyFunc tyA tyB))
     -> (var  : Term g tyA)
     -> Term g tyB

  Zero : Term g TyNat

  Next : (inner : Term g TyNat)
      -> Term g TyNat

  Case : (scrutinee : Term g TyNat)
      -> (zero : Term g tyA)
      -> (next : Term (Extend g TyNat) tyA)
      -> Term g tyA

  Plus : Term g TyNat
      -> Term g TyNat
      -> Term g TyNat

  Rec : (body : Term (Extend g tyA) tyA)
    -> Term g tyA

term : Term Empty
            (TyFunc TyNat -- (Var Here) -
                    (TyFunc TyNat -- (Var (There Here)) -
                            (TyFunc TyNat -- (Var (There (There Here))) -
                                    (TyFunc TyNat -- (Var (There (There (There Here)))) -
                                           (TyFunc TyNat -- (Var (There (There (There (There Here))))) -
                                                   (TyFunc TyNat -- (Var (There (There (There (There (There Here)))))) -
                                                           (TyFunc TyNat -- (Var (There (There (There (There (There (There Here)))))))
                                                                   TyNat
                                                                   )
                                                                   )
                                                                   )
                                                                   )
                                                                   )
                                                                   )
                                                                   )
term =
  Func
      (Func
           (Func
                (Func
                     (Func
                          (Func
                               (Func
                                    (Func (Plus (Var Here)
                                                (Plus (Var (There Here))
                                                      (Plus (Var (There (There Here)))
                                                            (Plus (Var (There (There (There Here))))
                                                                  (Plus (Var (There (There (There (There Here)))))
                                                                        (Plus  (Var (There (There (There (There (There Here))))))
                                                                               (Var (There (There (There (There (There (There Here)))))))
                                                                        )
                                                                  )
                                                            )
                                                      )
                                                 )
                                          )
                                    )
                               )
                          )
                     )
                )
            )
       )


text:
||| Convert binary string to an integer
module BinToDec

import Data.Nat.Exponentiation

data BinChar : Char -> Type where
  O : BinChar '0'
  I : BinChar '1'

data Every : (a -> Type) -> List a -> Type where
  Nil : {P : a -> Type} -> Every P []
  (::) : {P : a -> Type} -> P x -> Every P xs -> Every P (x :: xs)

fromBinChars : Every BinChar xs -> Nat -> Nat
fromBinChars [] _ = 0
fromBinChars (_ :: ys) Z = 1
fromBinChars (O :: ys) (S k) = fromBinChars ys k
fromBinChars (I :: ys) (S k) = lpow 2 k + fromBinChars ys k

b : (s : String) -> {auto p : Every BinChar (unpack s)} -> Nat
b {p} s = fromBinChars p (length s)

max_stars_repo_name: DejanMilicic/IdrisPlayground

max_issues_repo_name: DejanMilicic/IdrisPlayground

max_forks_repo_name: DejanMilicic/IdrisPlayground


text:
import Data.Vect

{-
vApp : Vect n (a -> b) -> Vect n a -> Vect n b
vApp []       []         = []
vApp (f :: fs) (a :: as) = f a :: vApp fs as
-}

total
vApp : {a:Type} -> {b:Type} -> {n:Nat} ->  Vect n (a -> b) -> Vect n a -> Vect n b
vApp  []       []         = []
vApp  (f :: fs) (e :: es) = f e :: vApp fs es

--vApp {a} {b} {n=S m} (f :: fs) (e :: es) = f e :: vApp fs es

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


text:
||| SExpParser stolen from Idris2 sources' `Idris.IDEMode.Parser`.
module Bautzen.REPL.SExpParser

import Bautzen.SExp

import Text.Parser
import Text.Lexer
import Text.Token
import Data.Strings
import Data.List

%hide Text.Lexer.Core.strTail

public export
data SExpKind = Ident
               | Literal
               | StrLit
               | Symbol
               | Comment
               | EndInput

Show a => Show (Token a) where
  show (Tok k t) = "Tok " ++ show k ++ "  " ++ t

Show SExpKind where
 show Ident = "Ident"
 show  Literal = "Literal"
 show  StrLit = "String"
 show  Symbol = "Symbol"
 show  Comment = "Comment"
 show  EndInput = "EOF"

TokenKind SExpKind where
  TokType Ident = String
  TokType Literal = Integer
  TokType StrLit = String
  TokType Symbol = String
  TokType Comment = ()
  TokType EndInput = ()

  tokValue Ident x = x
  tokValue StrLit x = x
  tokValue Literal x = cast x
  tokValue Symbol x = x
  tokValue Comment x = ()
  tokValue EndInput x = ()

public export
data ParseError = ParseFail String (Maybe (Int, Int)) (List (Token SExpKind))
                | LexFail (Int, Int, String)
                | LitFail (List Int)

export
Show ParseError where
  show (ParseFail err loc toks)
      = "Parse error: " ++ err ++ " (next tokens: "
            ++ show (take 10 toks) ++ ")"
  show (LexFail (c, l, str))
      = "Lex error at " ++ show (c, l) ++ " input: " ++ str
  show (LitFail l)
      = "Lit error(s) at " ++ show l

symbols : List String
symbols = ["(", ":", ")"]

ident : Lexer
ident = pred startIdent <+> many (pred validIdent)
  where
    startIdent : Char -> Bool
    startIdent '_' = True
    startIdent x = isAlpha x

    validIdent : Char -> Bool
    validIdent '_' = True
    validIdent '-' = True
    validIdent '\'' = True
    validIdent '?' = True
    validIdent '!' = True
    validIdent x = isAlphaNum x

ideTokens : TokenMap (Token SExpKind)
ideTokens =
  map (\x => (exact x, \s => Tok Symbol x)) symbols ++
    [ (digits, \x => Tok Literal x)
    , (stringLit, \x => Tok StrLit (stripQuotes x))
    , (ident, \x => Tok Ident x)
    , (space, \x => Tok Comment x)
    ]
  where
    stripQuotes : String -> String
    -- ASSUMPTION! Only total because we know we're getting quoted strings.
    stripQuotes = assert_total (strTail . reverse . strTail . reverse)

idelex : String -> Either (Int, Int, String) (List (TokenData (Token SExpKind)))
idelex str
    = case lex ideTokens str of
           -- Add the EndInput token so that we'll have a line and column
           -- number to read when storing spans in the file
           (tok, (l, c, "")) => Right (filter notComment tok ++
                                      [MkToken l c (Tok EndInput "")])
           (_, fail) => Left fail
    where
      notComment : TokenData (Token SExpKind) -> Bool
      notComment t = case tok t of
                          Tok Comment _ => False
                          _ => True

Rule : Type -> Type
Rule ty = Grammar (TokenData (Token SExpKind)) True ty

EmptyRule : Type -> Type
EmptyRule ty = Grammar (TokenData (Token SExpKind)) False ty

eoi : EmptyRule ()
eoi
    = do nextIs "Expected end of input" (isEOI . tok)
         pure ()
  where
    isEOI : Token SExpKind -> Bool
    isEOI (Tok EndInput _) = True
    isEOI _ = False

intLit : Rule Integer
intLit
    = terminal "Expected integer literal"
               (\x => case tok x of
                           Tok Literal i => Just (cast i)
                           _ => Nothing)

strLit : Rule String
strLit
    = terminal "Expected string literal"
               (\x => case tok x of
                           Tok StrLit s => Just s
                           _ => Nothing)

symbol : String -> Rule ()
symbol req
    = terminal ("Expected '" ++ req ++ "'")
               (\x => case tok x of
                           Tok Symbol s => if s == req
                                           then Just ()
                                           else Nothing
                           _ => Nothing)

exactIdent : String -> Rule ()
exactIdent req
    = terminal ("Expected " ++ req)
               (\x => case tok x of
                           Tok Ident s => if s == req
                                          then Just ()
                                          else Nothing
                           _ => Nothing)

identPart : Rule String
identPart
    = terminal "Expected name"
               (\x => case tok x of
                           Tok Ident str => Just str
                           _ => Nothing)

sexp : Rule SExp
sexp
    = do i <- fromInteger <$> intLit
         pure (SInt i)
  <|> do str <- strLit
         pure (SStr str)
  <|> do symbol ":"; x <- identPart
         pure (SSym x)
  <|> do symbol "("
         xs <- many sexp
         symbol ")"
         pure (SList xs)

ideParser : String -> Grammar (TokenData (Token SExpKind)) True ty -> Either String ty
ideParser str p
    = case idelex str of
           Left err => Left $ show $ LexFail err
           Right toks =>
              case parse p toks of
                   Left (Error err []) =>
                          Left $ show $ ParseFail err Nothing []
                   Left (Error err (t :: ts)) =>
                          Left $ show $ ParseFail err (Just (line t, col t))
                                                  (map tok (t :: ts))
                   Right (val, _) => Right val

export
parseSExp : String -> Either String SExp
parseSExp inp
    = ideParser inp (do c <- sexp; eoi; pure c)

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
||| Checks whether the input is a palindrome.
||| Case-insensitive and only returns True if the palindrome is more than len characters long.
||| @len the number of characters above which palindromes are checked.
||| @str the input string.
palindrome : (len : Nat) -> (str : String) -> Bool
palindrome len str = length lowercase > len && lowercase == reverse lowercase
    where
        lowercase : String
        lowercase = toLower str

||| Returns the number of words and characters in the input.
||| @str the input string.
counts : (str : String) -> (Nat, Nat)
counts str = (length (words str), length str)

||| Returns the 10 largest results in the list.
||| @list the input list.
top_ten : Ord a => (list : List a) -> (List a)
top_ten lst = take 10 (reverse (sort lst))

||| Returns the number of words in list longer than n.
||| @n the length limit.
||| @list the input list of strings.
over_length : (n : Nat) -> (list : List String) -> Nat
over_length n = length . filter (\str => length str > n)

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
module Utils.Handle

import Data.Vect
import Data.Nat
import Control.Monad.Error.Either
import Control.Linear.LIO

public export
ReadHack : (t_ok : Type) -> (t_read_failed : Type) -> Bool -> Type
ReadHack t_ok t_read_failed False = t_read_failed
ReadHack t_ok t_read_failed True = Res (List Bits8) (const t_ok)

public export
WriteHack : (t_ok : Type) -> (t_write_failed : Type) -> Bool -> Type
WriteHack t_ok t_write_failed False = t_write_failed
WriteHack t_ok t_write_failed True = t_ok

public export
record Handle (t_ok : Type) (t_closed : Type) (t_read_failed : Type) (t_write_failed : Type) where
  constructor MkHandle
  1 underlying : t_ok
  do_read : forall m. LinearIO m => (1 _ : t_ok) -> (len : Nat) -> L1 m $ Res Bool $ ReadHack t_ok t_read_failed
  do_write : forall m. LinearIO m => (1 _ : t_ok) -> List Bits8 -> L1 m $ Res Bool $ WriteHack t_ok t_write_failed
  do_close : forall m. LinearIO m => (1 _ : t_ok) -> L1 m t_closed

public export
close : LinearIO m => (1 _ : Handle t_ok t_closed t_read_failed t_write_failed) -> L1 m t_closed
close (MkHandle x do_read do_write do_close) = do_close x

public export
read : LinearIO m => (1 _ : Handle t_ok t_closed t_read_failed t_write_failed) -> (len : Nat) -> L1 m $ Res Bool $ \case
  False => t_read_failed
  True => Res (List Bits8) (\_ => Handle t_ok t_closed t_read_failed t_write_failed)
read (MkHandle x do_read do_write do_close) len = do
  (True # (output # x)) <- do_read x len
  | (False # x) => pure1 $ False # x
  pure1 $ True # (output # MkHandle x do_read do_write do_close)

public export
write : LinearIO m => (1 _ : Handle t_ok t_closed t_read_failed t_write_failed) -> (input : List Bits8) -> L1 m $ Res Bool $ \case
  False => t_write_failed
  True => Handle t_ok t_closed t_read_failed t_write_failed
write (MkHandle x do_read do_write do_close) input = do
  (True # x) <- do_write x input
  | (False # x) => pure1 $ False # x
  pure1 $ True # MkHandle x do_read do_write do_close

public export
Handle' : Type -> Type -> Type
Handle' t_ok t_closed = Handle t_ok t_closed (Res String $ const t_closed) (Res String $ const t_closed)


text:
module Chapter7

%default total

{-
  interface Functor f => Applicative (f : Type -> Type) where
    pure : a -> f a
    (<*>) : f (a -> b) -> f a -> f b

  interface Applicative m => Monad (m : Type -> Type) where
    (>>=) : m a -> (a -> m b) -> m b
    join : m (m a) = m a

  Monad Maybe where
    (>>=) Nothing next = Nothing
    (>>=) (Just x) next = next x

-}

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Test

import Data.Universe
import Control.Monad.Ref

-- Universe --------------------------------------------------------------------

data Basic
  = INT
  | STR

Uninhabited (INT = STR) where
  uninhabited Refl impossible

DecEq Basic where
  decEq INT INT = Yes Refl
  decEq STR STR = Yes Refl

  decEq INT STR = No absurd
  decEq STR INT = No (negEqSym absurd)

[basic] Universe Basic where
  typeOf INT = Int
  typeOf STR = String

  defaultOf INT = 0
  defaultOf STR = ""

-- Tests -----------------------------------------------------------------------

test0 : IO Int
test0 = do
  r <- newIORef 5
  writeIORef r 10
  x <- readIORef r
  pure x

test1 : MonadRef IORef IO => IO Int
test1 = do
  r <- ref (the Int 5)
  r := (the Int 10)
  x <- deref r
  pure x

test2 : MonadRef IORef IO => IO String
test2 = do
  r <- ref "Hello"
  r := !(deref r) ++ " World!"
  x <- deref r
  pure x

-- testRef : Ref @{Test.basic} Int
-- testRef = do
--   r <- ref (the Int 5)
--   r := (the Int 10)
--   x <- deref r
--   pure (x + 2)

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
> module SimpleProb.SimpleProb

> import NonNegRational.NonNegRational
> import NonNegRational.BasicProperties
> import Num.Refinements
> import List.Operations

> %default total
> %access public export
> %auto_implicits off

> |||
> data SimpleProb  :  Type -> Type where
>   MkSimpleProb   :  {A : Type} ->
>                     (aps : List (A, NonNegRational)) ->
>                     sumMapSnd aps = 1 ->
>                     SimpleProb A

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
parameters (x : Nat, y : Nat)
  add : Nat
  add = x + y


text:
%default total

nonproductive : Stream a -> (Stream a, ())
nonproductive (x :: xs) =
  case nonproductive xs of
    (xs, ()) => (xs, ())


text:
module Libraries.Text.Parser

import Data.Bool
import Data.List
import Data.Nat
import public Data.List1

import public Libraries.Text.Parser.Core
import public Libraries.Text.Quantity
import public Libraries.Text.Token

%default total

||| Parse a terminal based on a kind of token.
export
match : (Eq k, TokenKind k) =>
        (kind : k) ->
        Grammar state (Token k) True (TokType kind)
match k = terminal "Unrecognised input" $
    \t => if t.kind == k
             then Just $ tokValue k t.text
             else Nothing

||| Optionally parse a thing, with a default value if the grammar doesn't
||| match. May match the empty input.
export
option : {c : Bool} ->
         (def : a) -> (p : Grammar state tok c a) ->
         Grammar state tok False a
option {c = False} def p = p <|> pure def
option {c = True} def p = p <|> pure def

||| Optionally parse a thing.
||| To provide a default value, use `option` instead.
export
optional : {c : Bool} ->
           (p : Grammar state tok c a) ->
           Grammar state tok False (Maybe a)
optional p = option Nothing (map Just p)

||| Try to parse one thing or the other, producing a value that indicates
||| which option succeeded. If both would succeed, the left option
||| takes priority.
export
choose : {c1, c2 : Bool} ->
         (l : Grammar state tok c1 a) ->
         (r : Grammar state tok c2 b) ->
         Grammar state tok (c1 && c2) (Either a b)
choose l r = map Left l <|> map Right r

||| Produce a grammar by applying a function to each element of a container,
||| then try each resulting grammar until the first one succeeds. Fails if the
||| container is empty.
export
choiceMap : {c : Bool} ->
            (a -> Grammar state tok c b) ->
            Foldable t => t a ->
            Grammar state tok c b
choiceMap {c} f xs = foldr (\x, acc => rewrite sym (andSameNeutral c) in
                                               f x <|> acc)
                           (fail "No more options") xs

%hide Prelude.(>>=)

||| Try each grammar in a container until the first one succeeds.
||| Fails if the container is empty.
export
choice : Foldable t =>
         {c : Bool} ->
         t (Grammar state tok c a) ->
         Grammar state tok c a
choice = choiceMap id

mutual
  ||| Parse one or more things
  export
  some : Grammar state tok True a ->
         Grammar state tok True (List1 a)
  some p = pure (!p ::: !(many p))

  ||| Parse zero or more things (may match the empty input)
  export
  many : Grammar state tok True a ->
         Grammar state tok False (List a)
  many p = option [] (forget <$> some p)

mutual
  private
  count1 : (q : Quantity) ->
           (p : Grammar state tok True a) ->
           Grammar state tok True (List a)
  count1 q p = do x <- p
                  seq (count q p)
                      (\xs => pure (x :: xs))

  ||| Parse `p`, repeated as specified by `q`, returning the list of values.
  export
  count : (q : Quantity) ->
          (p : Grammar state tok True a) ->
          Grammar state tok (isSucc (min q)) (List a)
  count (Qty Z Nothing) p = many p
  count (Qty Z (Just Z)) _ = pure []
  count (Qty Z (Just (S max))) p = option [] $ count1 (atMost max) p
  count (Qty (S min) Nothing) p = count1 (atLeast min) p
  count (Qty (S min) (Just Z)) _ = fail "Quantity out of order"
  count (Qty (S min) (Just (S max))) p = count1 (between (S min) max) p

mutual
  ||| Parse one or more instances of `p` until `end` succeeds, returning the
  ||| list of values from `p`. Guaranteed to consume input.
  export
  someTill : {c : Bool} ->
             (end : Grammar state tok c e) ->
             (p : Grammar state tok True a) ->
             Grammar state tok True (List1 a)
  someTill {c} end p = do x <- p
                          seq (manyTill end p)
                              (\xs => pure (x ::: xs))

  ||| Parse zero or more instances of `p` until `end` succeeds, returning the
  ||| list of values from `p`. Guaranteed to consume input if `end` consumes.
  export
  manyTill : {c : Bool} ->
             (end : Grammar state tok c e) ->
             (p : Grammar state tok True a) ->
             Grammar state tok c (List a)
  manyTill {c} end p = rewrite sym (andTrueNeutral c) in
                               map (const []) end <|> (forget <$> someTill end p)

mutual
  ||| Parse one or more instance of `skip` until `p` is encountered,
  ||| returning its value.
  export
  afterSome : {c : Bool} ->
              (skip : Grammar state tok True s) ->
              (p : Grammar state tok c a) ->
              Grammar state tok True a
  afterSome skip p = do ignore $ skip
                        afterMany skip p

  ||| Parse zero or more instance of `skip` until `p` is encountered,
  ||| returning its value.
  export
  afterMany : {c : Bool} ->
              (skip : Grammar state tok True s) ->
              (p : Grammar state tok c a) ->
              Grammar state tok c a
  afterMany {c} skip p = rewrite sym (andTrueNeutral c) in
                                 p <|> afterSome skip p

||| Parse one or more things, each separated by another thing.
export
sepBy1 : {c : Bool} ->
         (sep : Grammar state tok True s) ->
         (p : Grammar state tok c a) ->
         Grammar state tok c (List1 a)
sepBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
                           [| p ::: many (sep *> p) |]

||| Parse zero or more things, each separated by another thing. May
||| match the empty input.
export
sepBy : {c : Bool} ->
        (sep : Grammar state tok True s) ->
        (p : Grammar state tok c a) ->
        Grammar state tok False (List a)
sepBy sep p = option [] $ forget <$> sepBy1 sep p

||| Parse one or more instances of `p` separated by and optionally terminated by
||| `sep`.
export
sepEndBy1 : {c : Bool} ->
            (sep : Grammar state tok True s) ->
            (p : Grammar state tok c a) ->
            Grammar state tok c (List1 a)
sepEndBy1 {c} sep p = rewrite sym (orFalseNeutral c) in
                              sepBy1 sep p <* optional sep

||| Parse zero or more instances of `p`, separated by and optionally terminated
||| by `sep`. Will not match a separator by itself.
export
sepEndBy : {c : Bool} ->
           (sep : Grammar state tok True s) ->
           (p : Grammar state tok c a) ->
           Grammar state tok False (List a)
sepEndBy sep p = option [] $ forget <$> sepEndBy1 sep p

||| Parse one or more instances of `p`, separated and terminated by `sep`.
export
endBy1 : {c : Bool} ->
         (sep : Grammar state tok True s) ->
         (p : Grammar state tok c a) ->
         Grammar state tok True (List1 a)
endBy1 {c} sep p = some $ rewrite sym (orTrueTrue c) in
                                  p <* sep

export
endBy : {c : Bool} ->
        (sep : Grammar state tok True s) ->
        (p : Grammar state tok c a) ->
        Grammar state tok False (List a)
endBy sep p = option [] $ forget <$> endBy1 sep p

||| Parse an instance of `p` that is between `left` and `right`.
export
between : {c : Bool} ->
          (left : Grammar state tok True l) ->
          (right : Grammar state tok True r) ->
          (p : Grammar state tok c a) ->
          Grammar state tok True a
between left right contents = left *> contents <* right

export
location : Grammar state token False (Int, Int)
location = startBounds <$> position

export
endLocation : Grammar state token False (Int, Int)
endLocation = endBounds <$> position

export
column : Grammar state token False Int
column = snd <$> location

public export
when : Bool -> Lazy (Grammar state token False ()) -> Grammar state token False ()
when True y = y
when False y = pure ()

public export
%inline
unless : Bool -> Lazy (Grammar state token False ()) -> Grammar state token False ()
unless = when . not


text:
module HTML.Elements

import HTML.Types

-- TODO: FIX ACCESS
%access public export

isFlowContent : HTMLElement -> Bool
isFlowContent (MkHTMLElement (MkElement A _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Abbr _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Address _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Article _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Aside _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Audio _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement B _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Bdo _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Bdi _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Blockquote _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Br _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Button _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Canvas _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Cite _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Code _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Data _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Datalist _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Del _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Details _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Dfn _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Div _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Dl _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Em _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Embed _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Fieldset _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Figure _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Footer _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Form _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement H1 _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement H2 _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement H3 _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement H4 _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement H5 _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement H6 _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Header _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Hgroup _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Hr _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement I _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Iframe _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Img _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Input _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Ins _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Kbd _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Label _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Main _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Map _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Mark _ _ _)) = True
-- isFlowContent (MkHTMLElement (MkElement Math _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Menu _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Meter _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Nav _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Noscript _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Object _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Ol _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Output _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement P _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Pre _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Progress _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Q _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Ruby _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement S _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Samp _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Script _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Section _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Select _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Small _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Span _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Strong _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Sub _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Sup _ _ _)) = True
-- isFlowContent (MkHTMLElement (MkElement Svg _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Table _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Template _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Textarea _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Time _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Ul _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Var _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Video _ _ _)) = True
isFlowContent (MkHTMLElement (MkElement Wbr _ _ _)) = True
isFlowContent (MkHTMLTextNode _) = True
isFlowContent _ = False

isSectioningContent : HTMLElement -> Bool
isSectioningContent (MkHTMLElement (MkElement Article _ _ _)) = True
isSectioningContent (MkHTMLElement (MkElement Aside _ _ _)) = True
isSectioningContent (MkHTMLElement (MkElement Nav _ _ _)) = True
isSectioningContent (MkHTMLElement (MkElement Section _ _ _)) = True
isSectioningContent _ = False

isLabelableContent : HTMLElement -> Bool
isLabelableContent (MkHTMLElement (MkElement Button _ _ _)) = True
isLabelableContent (MkHTMLElement (MkElement Input _ _ _)) = True
isLabelableContent (MkHTMLElement (MkElement Meter _ _ _)) = True
isLabelableContent (MkHTMLElement (MkElement Output _ _ _)) = True
isLabelableContent (MkHTMLElement (MkElement Progress _ _ _)) = True
isLabelableContent (MkHTMLElement (MkElement Select _ _ _)) = True
isLabelableContent (MkHTMLElement (MkElement Textarea _ _ _)) = True
isLabelableContent _ = False

isHTag : HTMLElement -> Bool
isHTag (MkHTMLElement (MkElement H1 _ _ _)) = True
isHTag (MkHTMLElement (MkElement H2 _ _ _)) = True
isHTag (MkHTMLElement (MkElement H3 _ _ _)) = True
isHTag (MkHTMLElement (MkElement H4 _ _ _)) = True
isHTag (MkHTMLElement (MkElement H5 _ _ _)) = True
isHTag (MkHTMLElement (MkElement H6 _ _ _)) = True
isHTag _ = False

isHeadingContent : HTMLElement -> Bool
isHeadingContent (MkHTMLElement (MkElement Hgroup _ _ _)) = True
isHeadingContent elem = isHTag elem

isPhrasingContent : HTMLElement -> Bool
isPhrasingContent (MkHTMLElement (MkElement Abbr _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Audio _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement B _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Bdo _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Br _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Button _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Canvas _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Cite _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Code _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Data _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Datalist _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Dfn _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Em _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Embed _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement I _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Iframe _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Img _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Input _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Kbd _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Label _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Mark _ _ _)) = True
-- isPhrasingContent (MkHTMLElement (MkElement Math _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Meter _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Noscript _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Object _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Output _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Progress _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Q _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Ruby _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Samp _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Script _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Select _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Small _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Span _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Strong _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Sub _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Sup _ _ _)) = True
-- isPhrasingContent (MkHTMLElement (MkElement Svg _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Textarea _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Time _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Var _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Video _ _ _)) = True
isPhrasingContent (MkHTMLElement (MkElement Wbr _ _ _)) = True
isPhrasingContent (MkHTMLTextNode _) = True
isPhrasingContent _ = False
{-
<a>, if it contains only phrasing content
<area>, if it is a descendant of a <map> element
<del>, if it contains only phrasing content
<ins>, if it contains only phrasing content
<link>, if the itemprop attribute is present
<map>, if it contains only phrasing content
<meta>, if the itemprop attribute is present
-}

isEmbeddedContent : HTMLElement -> Bool
isEmbeddedContent (MkHTMLElement (MkElement Audio _ _ _)) = True
isEmbeddedContent (MkHTMLElement (MkElement Canvas _ _ _)) = True
isEmbeddedContent (MkHTMLElement (MkElement Embed _ _ _)) = True
isEmbeddedContent (MkHTMLElement (MkElement Iframe _ _ _)) = True
isEmbeddedContent (MkHTMLElement (MkElement Img _ _ _)) = True
-- isEmbeddedContent (MkHTMLElement (MkElement Math _ _ _)) = True
isEmbeddedContent (MkHTMLElement (MkElement Object _ _ _)) = True
-- isEmbeddedContent (MkHTMLElement (MkElement Svg _ _ _)) = True
isEmbeddedContent (MkHTMLElement (MkElement Video _ _ _)) = True
isEmbeddedContent _ = False
{-
<audio>, if the controls attribute is present
<img>, if the usemap attribute is present
<input>, if the type attribute is not in the hidden state
<menu>, if the type attribute is in the toolbar state
<object>, if the usemap attribute is present
<video>, if the controls attribute is present
-}

isInteractiveContent : HTMLElement -> Bool
isInteractiveContent (MkHTMLElement (MkElement A _ _ _)) = True
isInteractiveContent (MkHTMLElement (MkElement Button _ _ _)) = True
isInteractiveContent (MkHTMLElement (MkElement Details _ _ _)) = True
isInteractiveContent (MkHTMLElement (MkElement Embed _ _ _)) = True
isInteractiveContent (MkHTMLElement (MkElement Iframe _ _ _)) = True
isInteractiveContent (MkHTMLElement (MkElement Label _ _ _)) = True
isInteractiveContent (MkHTMLElement (MkElement Select _ _ _)) = True
isInteractiveContent (MkHTMLElement (MkElement Textarea _ _ _)) = True
isInteractiveContent _ = False

isFormAssociatedContent : HTMLElement -> Bool
isFormAssociatedContent (MkHTMLElement (MkElement Button _ _ _)) = True
isFormAssociatedContent (MkHTMLElement (MkElement Fieldset _ _ _)) = True
isFormAssociatedContent (MkHTMLElement (MkElement Input _ _ _)) = True
isFormAssociatedContent (MkHTMLElement (MkElement Label _ _ _)) = True
isFormAssociatedContent (MkHTMLElement (MkElement Meter _ _ _)) = True
isFormAssociatedContent (MkHTMLElement (MkElement Object _ _ _)) = True
isFormAssociatedContent (MkHTMLElement (MkElement Output _ _ _)) = True
isFormAssociatedContent (MkHTMLElement (MkElement Progress _ _ _)) = True
isFormAssociatedContent (MkHTMLElement (MkElement Select _ _ _)) = True
isFormAssociatedContent (MkHTMLElement (MkElement Textarea _ _ _)) = True
isFormAssociatedContent _ = False

isTransparentContent : HTMLElement -> Bool
isTransparentContent (MkHTMLElement (MkElement Textarea _ _ _)) = True
isTransparentContent _ = False

isTextNode : HTMLElement -> Bool
isTextNode (MkHTMLTextNode _) = True
isTextNode _ = False

mkElement : TypeTag -> {default False omit : Bool} -> List Attr -> List HTMLElement -> HTMLElement
mkElement type {omit} attrs children = MkHTMLElement (MkElement type omit attrs children)

text : String -> HTMLElement
text s = MkHTMLTextNode (MkTextNode s)

validChildren : (HTMLElement -> Bool) -> List HTMLElement -> Bool
validChildren _ [] = True
validChildren pred (x :: xs) = pred x && validChildren pred xs

anyChildren : List HTMLElement -> Bool
anyChildren _ = True

isTag : TypeTag -> HTMLElement -> Bool
isTag t (MkHTMLElement (MkElement t' _ _ Nil)) = (t == t')
isTag _ _ = False

validDescendants : (HTMLElement -> Bool) -> List HTMLElement -> Bool
validDescendants _ Nil = True
validDescendants pred (x :: xs) = pred x && validDescendants pred xs &&
    case x of
        MkHTMLElement (MkElement _ _ _ Nil) => True
        MkHTMLElement (MkElement _ _ _ children) => validDescendants pred children
        _ => True

textChildren : List HTMLElement -> Bool
textChildren = validDescendants isTextNode

emptyChildren : List HTMLElement -> Bool
emptyChildren [] = True
emptyChildren _ = False

flowChildren : List HTMLElement -> Bool
flowChildren = validChildren isFlowContent

phrasingChildren : List HTMLElement -> Bool
phrasingChildren = validChildren isPhrasingContent

-- TODO: should isFlowContent recurse? or just no header/footer?
flowChildrenSansHeaderFooterDescendant : List HTMLElement -> Bool
flowChildrenSansHeaderFooterDescendant Nil = True
flowChildrenSansHeaderFooterDescendant (x :: xs) = validFlowContentSansHeaderFooter x && flowChildrenSansHeaderFooterDescendant xs
    where
        validFlowContentSansHeaderFooter (MkHTMLElement (MkElement Header _ _ _)) = False
        validFlowContentSansHeaderFooter (MkHTMLElement (MkElement Footer _ _ _)) = False
        validFlowContentSansHeaderFooter elem =
            isFlowContent elem &&
            case elem of
                MkHTMLElement (MkElement _ _ _ Nil) => True
                MkHTMLElement (MkElement _ _ _ children) => flowChildrenSansHeaderFooterDescendant children
                _ => True

{--
-- Elements
--}

validAddressChildren : List HTMLElement -> Bool
validAddressChildren Nil = True
validAddressChildren (x :: xs) = validAddressContent x && validAddressChildren xs
    where
        validAddressContent : HTMLElement -> Bool
        validAddressContent (MkHTMLElement (MkElement Header _ _ _)) = False
        validAddressContent (MkHTMLElement (MkElement Footer _ _ _)) = False
        validAddressContent (MkHTMLElement (MkElement Address _ _ _)) = False
        validAddressContent elem =
            not (isHeadingContent elem) &&
            not (isSectioningContent elem) &&
            case elem of
                MkHTMLElement (MkElement _ _ _ Nil) => True
                MkHTMLElement (MkElement _ _ _ children') => validAddressChildren children'
                _ => True

address_ :
    List Attr ->
    (children : List HTMLElement) ->
    HTMLElement
address_ attrs children = mkElement Address attrs children

address :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.validAddressChildren children) = True} ->
    HTMLElement
address attrs children = address_ attrs children

article :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
article attrs children = mkElement Article attrs children

aside :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
aside attrs children = mkElement Aside attrs children

footer :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildrenSansHeaderFooterDescendant children) = True} ->
    HTMLElement
footer attrs children = mkElement Footer attrs children

h1 :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
h1 attrs children = mkElement H1 attrs children

h2 :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
h2 attrs children = mkElement H2 attrs children

h3 :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
h3 attrs children = mkElement H3 attrs children

h4 :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
h4 attrs children = mkElement H4 attrs children

h5 :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
h5 attrs children = mkElement H5 attrs children

h6 :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
h6 attrs children = mkElement H6 attrs children

header :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildrenSansHeaderFooterDescendant children) = True} ->
    HTMLElement
header attrs children = mkElement Header attrs children

hgroupChildren : List HTMLElement -> Bool
hgroupChildren children = (not (emptyChildren children)) && (validChildren isHTag children)

hgroup :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : HTML.Elements.hgroupChildren children = True} ->
    HTMLElement
hgroup attrs children = mkElement Hgroup attrs children

main :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
main attrs children = mkElement Main attrs children

nav :
    List Attr ->
    (children : List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
nav attrs children = mkElement Nav attrs children

section :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
section attrs children = mkElement Section attrs children

blockquote :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
blockquote attrs children = mkElement Blockquote attrs children

dd :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
dd attrs children = mkElement Dd attrs children

div :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
div attrs children = mkElement Div attrs children

dlChildren : List HTMLElement -> Bool
dlChildren Nil = True
dlChildren children = dlDtChildren children || dlDivChildren children
    where
        -- TODO: DO THIS
        dlDtChildren : List HTMLElement -> Bool
        dlDtChildren _ = True -- Either: Zero or more groups each consisting of one or more <dt> elements followed by one or more <dd> elements, optionally intermixed with <script> and <template> elements.
        dlDivChildren : List HTMLElement -> Bool
        dlDivChildren _ = True -- Or: One or more <div> elements, optionally intermixed with <script> and <template> elements.

dl :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.dlChildren children) = True} ->
    HTMLElement
dl attrs children = mkElement Dl attrs children

dtChildren : List HTMLElement -> Bool
dtChildren Nil = True
dtChildren (x :: xs) = validDtContent x && dtChildren xs
    where
        validDtContent (MkHTMLElement (MkElement Header _ _ _)) = False
        validDtContent (MkHTMLElement (MkElement Footer _ _ _)) = False
        validDtContent elem =
            not (isSectioningContent elem) &&
            case elem of
                MkHTMLElement (MkElement _ _ _ Nil) => True
                MkHTMLElement (MkElement _ _ _ children) => flowChildrenSansHeaderFooterDescendant children
                _ => True

dt :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.dtChildren children) = True} ->
    HTMLElement
dt attrs children = mkElement Dt attrs children

figcaption :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
figcaption attrs children = mkElement Figcaption attrs children

figureChildren : List HTMLElement -> Bool
figureChildren Nil = True
figureChildren xs = figcaptionThenFlow xs || flowThenFigcaption xs || flowChildren xs
    where
        isFigCaption : HTMLElement -> Bool
        isFigCaption (MkHTMLElement (MkElement Figcaption _ _ _)) = True
        isFigCaption _ = False
        figcaptionThenFlow : List HTMLElement -> Bool
        figcaptionThenFlow [] = False
        figcaptionThenFlow (x::xs::Nil) = False
        figcaptionThenFlow (x::xs) = isFigCaption x && flowChildren xs
        flowThenFigcaption : List HTMLElement -> Bool
        flowThenFigcaption [] = False
        flowThenFigcaption (x::xs::Nil) = False
        flowThenFigcaption children@(_::_) = flowChildren (init children) && isFigCaption (last children)

figure :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.figureChildren children) = True} ->
    HTMLElement
figure attrs children = mkElement Figure attrs children

hr :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : HTML.Elements.emptyChildren children = True} ->
    HTMLElement
hr attrs children = mkElement Hr {omit = True} attrs children

li_ :
    List Attr ->
    (children: List HTMLElement) ->
    HTMLElement
li_ attrs children = mkElement Li attrs children

li :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
li attrs children = li_ attrs children

ol :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.validChildren (HTML.Elements.isTag Li) children) = True} ->
    HTMLElement
ol attrs children = mkElement Ol attrs children

p :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
p attrs children = mkElement P attrs children

pre :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
pre attrs children = mkElement Pre attrs children

ul_ :
    List Attr ->
    (children: List HTMLElement) ->
    HTMLElement
ul_ attrs children = mkElement Ul attrs children

ul :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.validChildren (HTML.Elements.isTag Li) children) = True} ->
    HTMLElement
ul attrs children = ul_ attrs children

aChildren : List HTMLElement -> Bool
aChildren Nil = True
aChildren (x :: xs) = aContent x && aChildren xs
    where
        aContent : HTMLElement -> Bool
        aContent elem =
            (isFlowContent elem && not (isInteractiveContent elem)) ||
            isPhrasingContent elem

a :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.aChildren children) = True} ->
    HTMLElement
a attrs children = mkElement A attrs children

abbr :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
abbr attrs children = mkElement Abbr attrs children

b :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
b attrs children = mkElement B attrs children

bdi :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
bdi attrs children = mkElement Bdi attrs children

bdo :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
bdo attrs children = mkElement Bdo attrs children

br :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.emptyChildren children) = True} ->
    HTMLElement
br attrs children = mkElement Br {omit = True} attrs children

cite :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
cite attrs children = mkElement Cite attrs children

code :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
code attrs children = mkElement Code attrs children

data_ :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
data_ attrs children = mkElement Data attrs children

dfnChildren : List HTMLElement -> Bool
dfnChildren Nil = True
dfnChildren xs = dfnChildren' xs && validDescendants (not . isDfn) xs
    where
        isDfn : HTMLElement -> Bool
        isDfn (MkHTMLElement (MkElement Dfn _ _ _)) = True
        isDfn _ = False
        dfnContent : HTMLElement -> Bool
        dfnContent elem = isPhrasingContent elem
        dfnChildren' : List HTMLElement -> Bool
        dfnChildren' Nil = True
        dfnChildren' (x :: xs) = (dfnContent x) && (dfnChildren' xs)

dfn :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.dfnChildren children) = True} ->
    HTMLElement
dfn attrs children = mkElement Dfn attrs children

em :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
em attrs children = mkElement Em attrs children

i :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
i attrs children = mkElement I attrs children

kbd :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
kbd attrs children = mkElement Kbd attrs children

mark :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
mark attrs children = mkElement Mark attrs children

q :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
q attrs children = mkElement Q attrs children

rb :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
rb attrs children = mkElement Rb attrs children

rp :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
rp attrs children = mkElement Rp attrs children

rt :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
rt attrs children = mkElement Rt attrs children

rtcChildren : List HTMLElement -> Bool
rtcChildren Nil = True
rtcChildren (x :: xs) = rtcContent x && rtcChildren xs
    where
        isRtc : HTMLElement -> Bool
        isRtc (MkHTMLElement (MkElement Rtc _ _ _)) = True
        isRtc _ = False
        rtcContent : HTMLElement -> Bool
        rtcContent elem = isPhrasingContent elem || isRtc elem

rtc :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.rtcChildren children) = True} ->
    HTMLElement
rtc attrs children = mkElement Rtc attrs children

ruby :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
ruby attrs children = mkElement Ruby attrs children

s :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
s attrs children = mkElement S attrs children

samp :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
samp attrs children = mkElement Samp attrs children

small :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
small attrs children = mkElement Small attrs children

span :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
span attrs children = mkElement Span attrs children

strong :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
strong attrs children = mkElement Strong attrs children

sub :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
sub attrs children = mkElement Sub attrs children

sup :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
sup attrs children = mkElement Sup attrs children

time :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
time attrs children = mkElement Time attrs children

u :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
u attrs children = mkElement U attrs children

var :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
var attrs children = mkElement Var attrs children

wbr :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.emptyChildren children) = True} ->
    HTMLElement
wbr attrs children = mkElement Wbr {omit = True} attrs children

area :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.emptyChildren children) = True} ->
    HTMLElement
area attrs children = mkElement Area {omit = True} attrs children

audioChildren : List HTMLElement -> Bool
-- TODO: FIX
audioChildren Nil = True
audioChildren (x :: xs) = True
-- If the element has a src attribute: zero or more <track> elements followed by transparent content that contains no <audio> or <video> media elements.
-- Else: zero or more <source> elements followed by zero or more <track> elements followed by transparent content that contains no <audio> or <video> media elements.

audio :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
audio attrs children = mkElement Audio attrs children

img :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.emptyChildren children) = True} ->
    HTMLElement
img attrs children = mkElement Img {omit = True} attrs children

map :
    List Attr ->
    (children: List HTMLElement) ->
    -- TODO: Any transparent element.
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
map attrs children = mkElement Map attrs children

track :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.emptyChildren children) = True} ->
    HTMLElement
track attrs children = mkElement Track {omit = True} attrs children

videoChildren : List HTMLElement -> Bool
-- TODO: FIX
videoChildren xs = True
-- If the element has a src attribute: zero or more <track> elements, followed by transparent content that contains no media elements–that is no <audio> or <video>
-- Else: zero or more <source> elements, followed by zero or more <track> elements, followed by transparent content that contains no media elements–that is no <audio> or <video>.

video :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
video attrs children = mkElement Video attrs children

embed :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.emptyChildren children) = True} ->
    HTMLElement
embed attrs children = mkElement Embed {omit = True} attrs children

iframeChildren : List HTMLElement -> Bool
-- TODO: FIX
iframeChildren xs = True
-- Fallback content, i.e. content that is normally not rendered, but that browsers not supporting the <iframe> element will render.

iframe :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
iframe attrs children = mkElement Iframe attrs children

objectChildren : List HTMLElement -> Bool
-- TODO: FIX
objectChildren xs = True
-- zero or more <param> elements, then transparent.

object :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
object attrs children = mkElement Object attrs children

param :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.emptyChildren children) = True} ->
    HTMLElement
param attrs children = mkElement Param {omit = True} attrs children

pictureChildren : List HTMLElement -> Bool
-- TODO: FIX
pictureChildren xs = True
-- Zero or more <source> elements, followed by one <img> element, optionally intermixed with script-supporting elements.

picture :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
picture attrs children = mkElement Picture attrs children

source :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.emptyChildren children) = True} ->
    HTMLElement
source attrs children = mkElement Source {omit = True} attrs children

canvasChildren : List HTMLElement -> Bool
-- TODO: FIX
canvasChildren xs = True
-- Transparent but with no interactive content descendants except for <a> elements, <button> elements, <input> elements whose type attribute is checkbox, radio, or button.

canvas :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
canvas attrs children = mkElement Canvas attrs children

noscriptChildren : List HTMLElement -> Bool
-- TODO: FIX
noscriptChildren xs = True
-- When scripting is disabled and when it is a descendant of the <head> element: in any order, zero or more <link> elements, zero or more <style> elements, and zero or more <meta> elements.
-- When scripting is disabled and when it isn't a descendant of the <head> element: any transparent content, but no <noscript> element must be among its descendants.
-- Otherwise: flow content or phrasing content.

noscript :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
noscript attrs children = mkElement Noscript attrs children

scriptChildren : List HTMLElement -> Bool
-- TODO: FIX
scriptChildren xs = True

script :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
-- TODO: OMIT?
script attrs children = mkElement Script attrs children

delChildren : List HTMLElement -> Bool
-- TODO: FIX
-- Transparent.
delChildren xs = True

del :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
del attrs children = mkElement Del attrs children

insChildren : List HTMLElement -> Bool
-- TODO: FIX
-- Transparent.
insChildren xs = True

ins :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
ins attrs children = mkElement Ins attrs children

caption :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
caption attrs children = mkElement Caption attrs children

col :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.emptyChildren children) = True} ->
    HTMLElement
col attrs children = mkElement Col {omit = True} attrs children

colgroupChildren : List HTMLElement -> Bool
-- TODO: FIX
colgroupChildren xs = True
-- If the span attribute is present: none, it is an empty element.
-- If the attribute is not present: zero or more <col> element

colgroup :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
colgroup attrs children = mkElement Colgroup attrs children

tableChildren : List HTMLElement -> Bool
-- TODO: FIX
tableChildren xs = True
-- In this order:
--      an optional <caption> element,
--      zero or more <colgroup> elements,
--      an optional <thead> element,
--      either one of the following:
--      zero or more <tbody> elements
--      one or more <tr> elements
--      an optional <tfoot> element

table :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
table attrs children = mkElement Table attrs children

tbodyChildren : List HTMLElement -> Bool
tbodyChildren Nil = True
tbodyChildren (x :: xs) = isTr x && tbodyChildren xs
    where
        isTr : HTMLElement -> Bool
        isTr (MkHTMLElement (MkElement Tr _ _ _)) = True
        isTr _ = False

tbody :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.tbodyChildren children) = True} ->
    HTMLElement
tbody attrs children = mkElement Tbody attrs children

td :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
td attrs children = mkElement Td attrs children

tfootChildren : List HTMLElement -> Bool
tfootChildren = tbodyChildren

tfoot :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.tfootChildren children) = True} ->
    HTMLElement
tfoot attrs children = mkElement Tfoot attrs children

thChildren : List HTMLElement -> Bool
-- TODO: FIX
thChildren xs = True
-- Flow content, but with no header, footer, sectioning content, or heading content descendants.
th :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
th attrs children = mkElement Th attrs children

theadChildren : List HTMLElement -> Bool
theadChildren = tbodyChildren

thead :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.theadChildren children) = True} ->
    HTMLElement
thead attrs children = mkElement Thead attrs children

trChildren : List HTMLElement -> Bool
-- TODO: FIX
trChildren xs = True
-- Zero or more <td> and/or <th> elements; script-supporting elements (<script> and <template>) are also allowed

tr :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
tr attrs children = mkElement Tr attrs children

buttonChildren : List HTMLElement -> Bool
buttonChildren Nil = True
buttonChildren (x :: xs) = isPhrasingContent x && not (isInteractiveContent x) && buttonChildren xs

button :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.buttonChildren children) = True} ->
    HTMLElement
button attrs children = mkElement Button attrs children

datalistChildren : List HTMLElement -> Bool
-- TODO: FIX
datalistChildren xs = True
-- Either phrasing content or zero or more <option> elements.

datalist :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
datalist attrs children = mkElement Datalist attrs children

fieldsetChildren : List HTMLElement -> Bool
-- TODO: FIX
fieldsetChildren xs = True
-- An optional <legend> element, followed by flow content.

fieldset :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
fieldset attrs children = mkElement Fieldset attrs children

validFormDescendant : HTMLElement -> Bool
validFormDescendant child = isFlowContent child && (not (isTag Form child))

formChildren : List HTMLElement -> Bool
formChildren = validDescendants validFormDescendant

form :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.formChildren children) = True} ->
    HTMLElement
form attrs children = mkElement Form attrs children

input :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.emptyChildren children) = True} ->
    HTMLElement
input attrs children = mkElement Input attrs children

validLabelDescendant : HTMLElement -> Bool
validLabelDescendant child = isPhrasingContent child && (not (isTag Label child))
-- TODO: FIX
-- No labelable elements other than the labeled control are allowed.

labelChildren : List HTMLElement -> Bool
labelChildren = validDescendants validLabelDescendant

label :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.labelChildren children) = True} ->
    HTMLElement
label attrs children = mkElement Label attrs children

legend :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
legend attrs children = mkElement Legend attrs children

validMeterDescendant : HTMLElement -> Bool
validMeterDescendant child = isPhrasingContent child && (not (isTag Meter child))

meterChildren : List HTMLElement -> Bool
meterChildren = validDescendants validMeterDescendant

meter :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.meterChildren children) = True} ->
    HTMLElement
meter attrs children = mkElement Meter attrs children

validOptgroupDescendant : HTMLElement -> Bool
validOptgroupDescendant = isTag Option

optgroupChildren : List HTMLElement -> Bool
optgroupChildren = validDescendants validOptgroupDescendant

optgroup :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.optgroupChildren children) = True} ->
    HTMLElement
optgroup attrs children = mkElement Optgroup attrs children

option :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.textChildren children) = True} ->
    HTMLElement
option attrs children = mkElement Option attrs children

output :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.phrasingChildren children) = True} ->
    HTMLElement
output attrs children = mkElement Output attrs children

progressChildren : List HTMLElement -> Bool
progressChildren = validDescendants validProgressDescendant
    where
        validProgressDescendant : HTMLElement -> Bool
        validProgressDescendant child = isPhrasingContent child && (not (isTag Progress child))

progress :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.progressChildren children) = True} ->
    HTMLElement
progress attrs children = mkElement Progress attrs children

selectChildren : List HTMLElement -> Bool
selectChildren = validChildren validSelectChildren
    where
        validSelectChildren : HTMLElement -> Bool
        validSelectChildren child = (isTag Option child) || (isTag Optgroup child)

select :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.selectChildren children) = True} ->
    HTMLElement
select attrs children = mkElement Select attrs children

textarea :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.textChildren children) = True} ->
    HTMLElement
textarea attrs children = mkElement Textarea attrs children

detailsChildren : List HTMLElement -> Bool
detailsChildren (x :: xs) = (isTag Summary x) && (validChildren isFlowContent xs)
detailsChildren _ = False

details :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.detailsChildren children) = True} ->
    HTMLElement
details attrs children = mkElement Details attrs children

dialog :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.flowChildren children) = True} ->
    HTMLElement
dialog attrs children = mkElement Dialog attrs children

-- menu :
--     List Attr ->
--     (children: List HTMLElement) ->
--     {auto prf : (HTML.Elements.flowChildren children) = True} ->
--     HTMLElement
-- menu attrs children = mkElement Menu attrs children
-- If the element is in the list menu state: flow content, or alternatively, zero or more occurrences of <li>, <script>, and <template>.
-- If the element is in the context menu state: zero or more occurrences, in any order, of <menu> (context menu state only), <menuitem {deprecated}>, <hr>, <script>, and <template>.
-- TODO: oof...
--

summaryChildren : List HTMLElement -> Bool
summaryChildren (x :: Nil) = isHeadingContent x
summaryChildren children = phrasingChildren children

summary :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.summaryChildren children) = True} ->
    HTMLElement
summary attrs children = mkElement Summary attrs children

template :
    List Attr ->
    (children: List HTMLElement) ->
    {auto prf : (HTML.Elements.anyChildren children) = True} ->
    HTMLElement
template attrs children = mkElement Template attrs children

max_stars_repo_name: ebenpack/pamperscript

max_issues_repo_name: ebenpack/pamperscript

max_forks_repo_name: ebenpack/pamperscript


text:
module Node.HTTP

import Coda.Node.Core

%access public export
%default total

record Server where
  constructor MkServer
  server : Ptr

data Port : Type where
  MkPort : (n : Int) -> { auto p : Dec ( n > 0 = True ) } -> Port

Handler : Type
Handler = Ptr -> Ptr -> JS_IO ()

wrapHandler : Handler -> Ptr -> JS_IO ()
wrapHandler handler ptr = do
  req <- prop { ty = Ptr } ptr "req"
  res <- prop { ty = Ptr } ptr "res"
  handler req res

partial
createServer : Handler -> JS_IO Server
createServer handler = do
  http <- require "http"
  server <- eval { ty = (Ptr -> String -> (JsFn (Ptr -> JS_IO())) -> JS_IO Ptr) }
                 "%0[%1]( (req, res) => %2({req, res}))"
                 http "createServer" (MkJsFn (wrapHandler handler))
  pure $ MkServer server

listen : Server -> Port -> JS_IO ()
listen (MkServer server) (MkPort number) = do
  startedPtr <- method { a = Int } { b = Ptr } server "listen" number
  log ("Started server on http://localhost:" ++ (show number))

max_stars_repo_name: ostera/idris-coda

max_issues_repo_name: ostera/idris-coda

max_forks_repo_name: ostera/idris-coda


text:
module Specdris.Data.SpecInfo

import Specdris.Data.ConsoleColor

%access export
%default total

||| Information/Specification about a certain module/data
||| and/or the description of its test cases.
public export
data SpecInfo : Type where
     Describe : (msg : String) -> SpecInfo
     It : (msg : String) -> SpecInfo

{- Evaluates the given `SpecInfo` by printing the formatted
   information to console.
 -}
evalInfo : SpecInfo -> (level : Nat) -> String
evalInfo (Describe msg) level = format msg White level
evalInfo (It msg)       level = format ("+ " ++ msg) White level

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
module Linear.MultiSolver

--To make sure that all imports work, load in idris as
--   idris Linear.MultiSolver.idr -p contrib

import ZZ
import Data.Matrix.Numeric
import Data.Fin
import BaseN
import Rationals

%access public export

{-
Representing a system of linear equations in matrix form as AX = B,
the solution for X is X = A^(-1)B
Unique solutions exist if |A| != 0.
If |A| == 0, the system can be either inconsistent (no sol.),
             or dependent (infinite sol.)
To Be Done:
- existence of solutions (depends on determinant)
- multiplication of matrices (Num interface defined)
- proof that solutions are correct
- etc.
-}

--Operations for (ZZ,ZZ) are defined, so that we can develop proofs
total
plusZZ : ZZPair -> ZZPair -> ZZPair
plusZZ x y = ((fst x)*(snd y) + (snd x)*(fst y), (snd x)*(snd y))

total
multZZ : ZZPair -> ZZPair -> ZZPair
multZZ x y = ((fst x)*(fst y), (snd x)*(snd y))

total
fromIntQ : Integer -> ZZPair
fromIntQ n = if n < 0
  then (NegS $ fromInteger ((-n) - 1), Pos 1)
  else (Pos $ fromInteger n, Pos 1)

--This allows arithmetic operations on ZZPair
implementation Num ZZPair where
  (+) = plusZZ
  (*) = multZZ
  fromInteger = fromIntQ

mutual
  implementation Neg ZZPair where
    negate (Pos Z, x)     = (Pos Z, x)
    negate (Pos (S n), x) = (NegS n, x)
    negate (NegS n, x)    = (Pos (S n), x)

    (-) = subZZ

  subZZ : ZZPair -> ZZPair -> ZZPair
  subZZ x y = plusZZ x (negate y)

--This can be used to check equality
(==) : ZZPair -> ZZPair -> Bool
(==) (a,b) (c,d) = (a*d) == (b*c)

--Minor for a term of a 1x1 Matrix (Not required, can be removed later)
total
minor1 : Fin 1 -> Fin 1 -> Matrix 1 1 ZZPair -> ZZPair
minor1 x y [[k]] = k

--Minor for a term of a 2x2 Matrix
total
minor2 : Fin 2 -> Fin 2 -> Matrix 2 2 ZZPair -> ZZPair
minor2 x y mat = indices 0 0 (subMatrix x y mat)

--Minor for a general matrix term (Indices are elements of Fin <size>)
minor : Fin (S n) -> Fin (S n) ->
  Matrix (S n) (S n) ZZPair -> ZZPair
minor {n} x y mat = case n of
                  Z => minor1 x y mat
                  (S Z) => minor2 x y mat
                  (S (S k)) => simplifyRational (det (subMatrix x y mat))

--Cofactor terms for a matrix (defined using the minor)
cofactor : Fin (S n) -> Fin (S n) ->
  Matrix (S n) (S n) ZZPair -> ZZPair
cofactor x y mat = case (modNat (finToNat x + finToNat y) 2) of
                        Z => minor x y mat
                        (S k) => (NegS 0, Pos 1) * (minor x y mat)

--To make calc simpler, I have defined the cofactor/determinant term, as
--this will be required for defining the inverse of a matrix
cofByDet : Fin (S n) -> Fin (S n) ->
  Matrix (S n) (S n) ZZPair -> ZZPair
cofByDet {n} x y mat = case n of
              Z => (snd (cofactor 0 0 mat), fst (cofactor 0 0 mat))
              (S k) => simplifyRational
                ((cofactor x y mat) * (snd (det mat), fst (det mat)))

--Auxillary functions for defining an empty matrix, which will be updated
--with values of the inverse

--Given n, give a vector of length n, with each element (0,1)
total
empRow : (n : Nat) -> Vect n ZZPair
empRow Z = []
empRow (S k) = [(Pos Z, Pos 1)] ++ (empRow k)

--Given m,n, give an empty mxn matrix with (0,1) filled for every term.
--This is the null matrix (in rationals, we defined 0 as (0,1))
total
empMat : (m : Nat) -> (n : Nat) -> Vect m (Vect n ZZPair)
empMat Z n = []
empMat (S k) n = [(empRow n)] ++ (empMat k n)

--Defining the cofactor matrix requires updating the null matrix
--with values of the cofactor.
--This requires inducting twice on the row and column, hence has
--been broken down into two separate functions.

--Given the reqRow, gives the row of cofactors for the original matrix
--for that index.
--iter is a variable used to induct on, and does not serve any
--real purpose
--"replaceAt index elem Vect" replaces an element of Vect at index by elem
--embn is from BaseN, and embeds an element of Fin n in Fin (S n)
cofRow : (size : Nat) -> (reqRow : Fin size) -> Matrix size size ZZPair ->
  (iter : Fin size) -> Vect size ZZPair
cofRow Z _ _ FZ impossible
cofRow Z _ _ (FS _) impossible

cofRow (S k) reqRow mat FZ =
                    replaceAt
                    0
                    (cofByDet reqRow 0 mat)
                    (empRow (S k))

cofRow (S k) reqRow mat (FS y) =
                    replaceAt
                    (FS y)
                    (cofByDet reqRow (FS y) mat)
                    (cofRow (S k) reqRow mat (embn k y))

--Now, we can construct the cofactor matrix from the formed cofactor rows.
--tofinNat is from BaseN, and converts an element of Nat to Fin.
cofMat : (size : Nat) -> Matrix size size ZZPair ->
  (iter : Fin size) -> Matrix size size ZZPair
cofMat Z _ FZ impossible
cofMat Z _ (FS _) impossible

cofMat (S k) mat FZ =
                    replaceAt
                    0
                    (cofRow (S k) 0 mat (tofinNat (k) (S k)))
                    (empMat (S k) (S k))

cofMat (S k) mat (FS y) =
                    replaceAt
                    (FS y)
                    (cofRow (S k) (FS y) mat (tofinNat (k) (S k)))
                    (cofMat (S k) mat (embn k y))

--Inverse of a matrix is the transpose of the cofactor matrix
invMat : Matrix n n ZZPair -> Matrix n n ZZPair
invMat {n} mat = case n of
             Z => []
             (S k) => transpose (cofMat (S k) mat (tofinNat (k) (S k)))

{-
Solving a system of n linear equations:
    a11*x1 + a12*x2 + ... + a1n*xn = b1
    .
    .
    an1*x1 + an2*x2 + ... + ann*xn = bn

-}

--Solves a system ax = b.
--The operation <> is matrix multiplication, defined in Matrix.Numeric
solve : (n : Nat) -> (a : Matrix n n ZZPair) -> (b : Matrix n 1 ZZPair) ->
  Matrix n 1 ZZPair
solve n a b = (invMat a) <> b


text:
%flag C "-I/usr/local/Cellar/glew/1.12.0/include -I/usr/local/Cellar/libpng/1.6.25/include/libpng16 "
%flag C "-L/usr/local/Cellar/glew/1.12.0/lib -L/usr/local/Cellar/libpng/1.6.25/lib -lGLEW -lpng16 "
%flag C "OpenGL -framework"

max_stars_repo_name: spearman/gl-idris

max_issues_repo_name: spearman/gl-idris

max_forks_repo_name: spearman/gl-idris


text:
module RecordInWhere2

fd : Int
fd = 5 where
  data X : Type where

gd : Int
gd = 5 where
  data X : Type where

fr : Int
fr = 5 where
  record X where

gr : Int
gr = 5 where
  record X where

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Test.Env

import Test.Assertions
import Idrlisp.Env

%default covering

export
test : IO ()
test = describe "Idrlisp.Env" $ do
  describe "single" $ do
    env <- Env.new Nothing
    Env.lookup "foo" env `shouldBe'` Left "foo"
    Env.set "foo" "value" env `shouldSatisfy'` isLeft
    Env.define "foo" "value" env
    Env.lookup "foo" env `shouldBe'` Right "value"
    Env.set "foo" "new-value" env `shouldSatisfy'` isRight
    Env.lookup "foo" env `shouldBe'` Right "new-value"
  describe "chained" $ do
    parent <- Env.new Nothing
    child <- Env.new (Just parent)
    Env.define "foo" "value" parent
    Env.lookup "foo" child `shouldBe'` Right "value"
    Env.set "foo" "new-value" child `shouldSatisfy'` isRight
    Env.lookup "foo" child `shouldBe'` Right "new-value"
    Env.lookup "foo" parent `shouldBe'` Right "new-value"
    Env.set "bar" "value" child `shouldSatisfy'` isLeft
    Env.define "bar" "value" child
    Env.lookup "bar" child `shouldBe'` Right "value"
    Env.lookup "bar" parent `shouldBe'` Left "bar"
    Env.set "bar" "new-value" child `shouldSatisfy'` isRight
    Env.lookup "bar" child `shouldBe'` Right "new-value"
    Env.lookup "bar" parent `shouldBe'` Left "bar"
    Env.define "foo" "shadowing" child
    Env.lookup "foo" child `shouldBe'` Right "shadowing"
    Env.lookup "foo" parent `shouldBe'` Right "new-value"
    Env.set "foo" "new-shadowing" child `shouldSatisfy'` isRight
    Env.lookup "foo" child `shouldBe'` Right "new-shadowing"
    Env.lookup "foo" parent `shouldBe'` Right "new-value"

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Main

import Data.Vect
import Prelude.Nat

Matrix :  Nat -> Nat -> Type -> Type
Matrix n m a = Vect n (Vect m a)

empties : Vect m (Vect 0 a)
empties {m = Z} = []
empties {m = (S k)} = [] :: empties

transpose_helper : (row : Vect m a) -> (row_trans : Vect m (Vect k a)) -> Vect m (Vect (S k) a)
transpose_helper [] [] = []
transpose_helper (x :: xs) (y :: ys) = (x :: y) :: transpose_helper xs ys

--transpose_vec: Vect n (Vect m a) -> Vect m (Vect n a)
transpose_vec: Matrix n m a -> Matrix m n a
transpose_vec [] = empties
transpose_vec (row :: rows) = let row_trans = transpose_vec rows in
  transpose_helper row row_trans

testMatrix : Matrix 3 4 Nat
testMatrix = ( 1 :: 2 :: 3 :: 4 :: Nil) :: ( 10 :: 20 :: 30 :: 40 :: Nil) :: ( 100 :: 200 :: 300 :: 400 :: Nil) :: Nil

transposed : Matrix 4 3 Nat
transposed = transpose_vec testMatrix

main : IO ()
main = putStrLn (show testMatrix ++ "\n--after transpose--\n" ++ show transposed)

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
{-
  An embeded DSL for prolog-style logic programming, based on the
  pure-prolog parser and interpreter originally written in Haskell

  Original author: Ken Friis Larsen      <kflarsen@diku.dk>
  Translated into Idris by Nathan Bedell <nbedell@tulane.edu>
-}

import Interp
import Ast

%access public export

p : Term
p = Comp "p" []

q : Term
q = Comp "q" []

x : Term
x = Comp "x" []

z : Term
z = Comp "z" []

r : Term -> Term
r x = Comp "r" [x]

n : Term -> Term
n x = Comp "n" [x]

X : Term
X = Var "X"

s : Term -> Term
s x = Comp "s" [x]

f : Term -> Term -> Term
f x y = Comp "f" [x, y]

program : Program
program = [ p .
          , q :- [p]
	  , (n z) .
	  , (n (s X)) :- [n X]
	  , (f z z) .
	  , (f z (s z)) .
	  , (f X X) .
	  ]

result : List Solution
result = nub $ bfs $ makeReportTree program [f z X]

-- Note: I should make this more type-safe.
getSolutions : List Solution -> List Term
getSolutions xs = concat $ map getSolution xs
  where getSolution (MkSolution x) = map snd x

f_val : Term -> List Term
f_val x = getSolutions $ nub $ bfs $ makeReportTree program [f x X]

nat : Term -> Bool
nat t = query /= []
  where query : List Solution
        query = ?- n t

-- This is a version of f_val that runs on our embedded prolog
-- system, but only allows values of type Nat.
f_val' : (x : Term) -> {auto p : True = nat x} -> List Term
f_val' x = getSolutions $ ?- f x X

-- An example. The following (should) compile.
-- However, the compiler doesn't like when I try to assert this total. It does strange things.
-- val : List Term
-- val = f_val' z

-- The following does not compile.
-- val' : List Term
-- val' = f_val' (s z)

max_stars_repo_name: Sintrastes/idr-pure-prolog

max_issues_repo_name: Sintrastes/idr-pure-prolog

max_forks_repo_name: Sintrastes/idr-pure-prolog