text:
{-#  OPTIONS --type-in-type #-}
module TooManyArgs

import IdrisPrelude

myFun : (a : Type) -> a -> a -> a
myFun a x y = x

myApp : Nat
myApp = myFun _ Zero Zero Zero Zero

max_stars_repo_name: JoeyEremondi/lambda-pi-constraint

max_issues_repo_name: JoeyEremondi/lambda-pi-constraint

max_forks_repo_name: JoeyEremondi/lambda-pi-constraint


text:
module Text.Parser.Core

import public Control.Delayed
import Data.List

||| Description of a language's grammar. The `tok` parameter is the type
||| of tokens, and the `consumes` flag is True if the language is guaranteed
||| to be non-empty - that is, successfully parsing the language is guaranteed
||| to consume some input.
public export
data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
     Empty : (val : ty) -> Grammar tok False ty
     Terminal : String -> (tok -> Maybe a) -> Grammar tok True a
     NextIs : String -> (tok -> Bool) -> Grammar tok False tok
     EOF : Grammar tok False ()

     Fail : Bool -> String -> Grammar tok c ty
     Commit : Grammar tok False ()
     MustWork : Grammar tok c a -> Grammar tok c a

     SeqEat : {c2 : _} -> Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
              Grammar tok True b
     SeqEmpty : {c1, c2 : _} -> Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
                Grammar tok (c1 || c2) b
     Alt : {c1, c2 : _} -> Grammar tok c1 ty -> Grammar tok c2 ty ->
           Grammar tok (c1 && c2) ty

||| Sequence two grammars. If either consumes some input, the sequence is
||| guaranteed to consume some input. If the first one consumes input, the
||| second is allowed to be recursive (because it means some input has been
||| consumed and therefore the input is smaller)
public export %inline %tcinline
(>>=) : {c1, c2 : Bool} ->
        Grammar tok c1 a ->
        inf c1 (a -> Grammar tok c2 b) ->
        Grammar tok (c1 || c2) b
(>>=) {c1 = False} = SeqEmpty
(>>=) {c1 = True} = SeqEat

||| Sequence two grammars. If either consumes some input, the sequence is
||| guaranteed to consume input. This is an explicitly non-infinite version
||| of `>>=`.
export
seq : {c1, c2 : _} -> Grammar tok c1 a ->
      (a -> Grammar tok c2 b) ->
      Grammar tok (c1 || c2) b
seq = SeqEmpty

||| Sequence a grammar followed by the grammar it returns.
export
join : {c1, c2 : Bool} ->
       Grammar tok c1 (Grammar tok c2 a) ->
       Grammar tok (c1 || c2) a
join {c1 = False} p = SeqEmpty p id
join {c1 = True} p = SeqEat p id

||| Give two alternative grammars. If both consume, the combination is
||| guaranteed to consume.
export
(<|>) : {c1, c2 : _} ->
        Grammar tok c1 ty ->
        Grammar tok c2 ty ->
        Grammar tok (c1 && c2) ty
(<|>) = Alt

||| Allows the result of a grammar to be mapped to a different value.
export
{c : _} -> Functor (Grammar tok c) where
  map f (Empty val)  = Empty (f val)
  map f (Fail fatal msg) = Fail fatal msg
  map f (MustWork g) = MustWork (map f g)
  map f (Terminal msg g) = Terminal msg (\t => map f (g t))
  map f (Alt x y)    = Alt (map f x) (map f y)
  map f (SeqEat act next)
      = SeqEat act (\val => map f (next val))
  map f (SeqEmpty act next)
      = SeqEmpty act (\val => map f (next val))
  -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
  -- so a sequence must be used.
  map {c = False} f p = SeqEmpty p (Empty . f)

||| Sequence a grammar with value type `a -> b` and a grammar
||| with value type `a`. If both succeed, apply the function
||| from the first grammar to the value from the second grammar.
||| Guaranteed to consume if either grammar consumes.
export
(<*>) : {c1, c2 : _} ->
        Grammar tok c1 (a -> b) ->
        Inf (Grammar tok c2 a) ->
        Grammar tok (c1 || c2) b
(<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)
(<*>) {c1 = True } x y = SeqEmpty x (\f => map f (Force y))

||| Sequence two grammars. If both succeed, use the value of the first one.
||| Guaranteed to consume if either grammar consumes.
export
(<*) : {c1, c2 : _} ->
       Grammar tok c1 a ->
       Inf (Grammar tok c2 b) ->
       Grammar tok (c1 || c2) a
(<*) x y = map const x <*> y

||| Sequence two grammars. If both succeed, use the value of the second one.
||| Guaranteed to consume if either grammar consumes.
export
(*>) : {c1, c2 : _} ->
       Grammar tok c1 a ->
       Inf (Grammar tok c2 b) ->
       Grammar tok (c1 || c2) b
(*>) x y = map (const id) x <*> y

||| Produce a grammar that can parse a different type of token by providing a
||| function converting the new token type into the original one.
export
mapToken : (a -> b) -> Grammar b c ty -> Grammar a c ty
mapToken f (Empty val) = Empty val
mapToken f (Terminal msg g) = Terminal msg (g . f)
mapToken f (NextIs msg g) = SeqEmpty (NextIs msg (g . f)) (Empty . f)
mapToken f EOF = EOF
mapToken f (Fail fatal msg) = Fail fatal msg
mapToken f (MustWork g) = MustWork (mapToken f g)
mapToken f Commit = Commit
mapToken f (SeqEat act next) = SeqEat (mapToken f act) (\x => mapToken f (next x))
mapToken f (SeqEmpty act next) = SeqEmpty (mapToken f act) (\x => mapToken f (next x))
mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)

||| Always succeed with the given value.
export
pure : (val : ty) -> Grammar tok False ty
pure = Empty

||| Check whether the next token satisfies a predicate
export
nextIs : String -> (tok -> Bool) -> Grammar tok False tok
nextIs = NextIs

||| Look at the next token in the input
export
peek : Grammar tok False tok
peek = nextIs "Unrecognised token" (const True)

||| Succeeds if running the predicate on the next token returns Just x,
||| returning x. Otherwise fails.
export
terminal : String -> (tok -> Maybe a) -> Grammar tok True a
terminal = Terminal

||| Always fail with a message
export
fail : String -> Grammar tok c ty
fail = Fail False

export
fatalError : String -> Grammar tok c ty
fatalError = Fail True

||| Succeed if the input is empty
export
eof : Grammar tok False ()
eof = EOF

||| Commit to an alternative; if the current branch of an alternative
||| fails to parse, no more branches will be tried
export
commit : Grammar tok False ()
commit = Commit

||| If the parser fails, treat it as a fatal error
export
mustWork : Grammar tok c ty -> Grammar tok c ty
mustWork = MustWork

data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
     Failure : {xs : List tok} ->
               (committed : Bool) -> (fatal : Bool) ->
               (err : String) -> (rest : List tok) -> ParseResult xs c ty
     EmptyRes : (committed : Bool) ->
                (val : ty) -> (more : List tok) -> ParseResult more False ty
     NonEmptyRes : {xs : List tok} ->
                   (committed : Bool) ->
                   (val : ty) -> (more : List tok) ->
                   ParseResult (x :: xs ++ more) c ty

-- Take the result of an alternative branch, reset the commit flag to
-- the commit flag from the outer alternative, and weaken the 'consumes'
-- flag to take both alternatives into account
weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
            (com' : Bool) ->
						ParseResult xs c ty -> ParseResult xs (whatever && c) ty
weakenRes com' (Failure com fatal msg ts) = Failure com' fatal msg ts
weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
weakenRes com' (NonEmptyRes {xs} com val more) = NonEmptyRes {xs} com' val more

doParse : (commit : Bool) ->
          (act : Grammar tok c ty) ->
          (xs : List tok) ->
          ParseResult xs c ty
-- doParse com xs act with (sizeAccessible xs)
doParse com (Empty val) xs = EmptyRes com val xs
doParse com (Fail fatal str) [] = Failure com fatal str []
doParse com (Fail fatal str) (x :: xs) = Failure com fatal str (x :: xs)
doParse com Commit xs = EmptyRes True () xs
doParse com (MustWork g) xs =
  let p' = doParse com g xs in
      case p' of
           Failure com' _ msg ts => Failure com' True msg ts
           res => res
doParse com (Terminal err f) [] = Failure com False "End of input" []
doParse com (Terminal err f) (x :: xs)
      = maybe
           (Failure com False err (x :: xs))
           (\a => NonEmptyRes com {xs=[]} a xs)
           (f x)
doParse com EOF [] = EmptyRes com () []
doParse com EOF (x :: xs)
      = Failure com False "Expected end of input" (x :: xs)
doParse com (NextIs err f) [] = Failure com False "End of input" []
doParse com (NextIs err f) (x :: xs)
      = if f x
           then EmptyRes com x (x :: xs)
           else Failure com False err (x :: xs)
doParse com (Alt {c1} {c2} x y) xs
    = let p' = doParse False x xs in
          case p' of
               Failure com' fatal msg ts
                  => if com' || fatal
                            -- If the alternative had committed, don't try the
                            -- other branch (and reset commit flag)
                       then Failure com fatal msg ts
                       else weakenRes {whatever = c1} com (doParse False y xs)
  -- Successfully parsed the first option, so use the outer commit flag
               EmptyRes _ val xs => EmptyRes com val xs
               NonEmptyRes {xs=xs'} _ val more => NonEmptyRes {xs=xs'} com val more
doParse com (SeqEmpty {c1} {c2} act next) xs
    = let p' = assert_total (doParse {c = c1} com act xs) in
              case p' of
               Failure com fatal msg ts => Failure com fatal msg ts
               EmptyRes com val xs =>
                     case assert_total (doParse com (next val) xs) of
                          Failure com' fatal msg ts => Failure com' fatal msg ts
                          EmptyRes com' val xs => EmptyRes com' val xs
                          NonEmptyRes {xs=xs'} com' val more =>
                                           NonEmptyRes {xs=xs'} com' val more
               NonEmptyRes {x} {xs=ys} com val more =>
                     case (assert_total (doParse com (next val) more)) of
                          Failure com' fatal msg ts => Failure com' fatal msg ts
                          EmptyRes com' val _ => NonEmptyRes {xs=ys} com' val more
                          NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
                               rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
                                       NonEmptyRes {xs = ys ++ (x1 :: xs1)} com' val more'
doParse com (SeqEat act next) xs with (doParse com act xs)
  doParse com (SeqEat act next) xs | Failure com' fatal msg ts
       = Failure com' fatal msg ts
  doParse com (SeqEat act next) (x :: (ys ++ more)) | (NonEmptyRes {xs=ys} com' val more)
       = let p' = assert_total (doParse com' (next val) more) in
             case p' of
              Failure com' fatal msg ts => Failure com' fatal msg ts
              EmptyRes com' val _ => NonEmptyRes {xs=ys} com' val more
              NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
                   rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
                           NonEmptyRes {xs = ys ++ (x1 :: xs1)} com' val more'
-- This next line is not strictly necessary, but it stops the coverage
-- checker taking a really long time and eating lots of memory...
-- doParse _ _ _ = Failure True True "Help the coverage checker!" []

public export
data ParseError tok = Error String (List tok)

||| Parse a list of tokens according to the given grammar. If successful,
||| returns a pair of the parse result and the unparsed tokens (the remaining
||| input).
export
parse : {c : _} -> (act : Grammar tok c ty) -> (xs : List tok) ->
        Either (ParseError tok) (ty, List tok)
parse act xs
    = case doParse False act xs of
           Failure _ _ msg ts => Left (Error msg ts)
           EmptyRes _ val rest => pure (val, rest)
           NonEmptyRes _ val rest => pure (val, rest)

ext: idr


text:
module Main
import Foo

main : IO ()
main = printLn "Hello World"

prf : (x : Nat) -> foo x === 1+x
prf x = Refl


text:
module Language.Elab.Syntax

import Language.Reflection

import Data.Strings -- strM

-- Get rid of all the instances here when we've gotten far enough along, these
-- are not things to leave laying around

private
z : (Int,Int)
z = (0,0)

export
namedFC : String -> FC
namedFC s = MkFC s z z

export
iVar : Name -> TTImp
iVar = IVar EmptyFC

export
iVar' : String -> Name -> TTImp
iVar' s = IVar (namedFC s)

export
iBindVar : String -> TTImp
iBindVar = IBindVar EmptyFC

export
iBindVar' : String -> String -> TTImp
iBindVar' s = IBindVar (namedFC s)

-- export
infixl 6 `iApp`
export
iApp : TTImp -> TTImp -> TTImp
iApp = IApp EmptyFC

export
iApp' : String -> TTImp -> TTImp -> TTImp
iApp' s = IApp (namedFC s)

export
iNamedApp : TTImp -> Name -> TTImp -> TTImp
iNamedApp = INamedApp EmptyFC

export
iAutoApp : TTImp -> TTImp -> TTImp
iAutoApp = IAutoApp EmptyFC

export
implicit' : TTImp
implicit' = Implicit EmptyFC True

export
implicit'' : TTImp
implicit'' = Implicit EmptyFC False

export
patClause : (lhs : TTImp) -> (rhs : TTImp) -> Clause
patClause = PatClause EmptyFC

export
patClause' : String -> (lhs : TTImp) -> (rhs : TTImp) -> Clause
patClause' s = PatClause (namedFC s)

export
iClaim : Count -> Visibility -> List FnOpt -> ITy -> Decl
iClaim = IClaim EmptyFC

export
iClaim' : String -> Count -> Visibility -> List FnOpt -> ITy -> Decl
iClaim' s = IClaim (namedFC s)

export
mkTy : (n : Name) -> (ty : TTImp) -> ITy
mkTy = MkTy EmptyFC EmptyFC

export
mkTy' : String -> (n : Name) -> (ty : TTImp) -> ITy
mkTy' s = MkTy EmptyFC (namedFC s)

export
iPi : Count -> PiInfo TTImp -> Maybe Name ->
      (argTy : TTImp) -> (retTy : TTImp) -> TTImp
iPi = IPi EmptyFC

export
iPi' : String -> Count -> PiInfo TTImp -> Maybe Name ->
      (argTy : TTImp) -> (retTy : TTImp) -> TTImp
iPi' s = IPi (namedFC s)

export
iLam : Count -> PiInfo TTImp -> Maybe Name ->
      (argTy : TTImp) -> (lamTy : TTImp) -> TTImp
iLam = ILam EmptyFC

export
iLet : Count -> Name -> (nTy : TTImp) -> (nVal : TTImp)
    -> (scope : TTImp) -> TTImp
iLet = ILet EmptyFC EmptyFC

export
iCase : TTImp -> (ty : TTImp)
     -> List Clause -> TTImp
iCase = ICase EmptyFC

export
iDef : Name -> List Clause -> Decl
iDef = IDef EmptyFC

export
iAs : Name -> TTImp -> TTImp
iAs = IAs EmptyFC EmptyFC UseLeft

export
iPrimVal : (c : Constant) -> TTImp
iPrimVal = IPrimVal EmptyFC

export
iPrimVal' : String -> (c : Constant) -> TTImp
iPrimVal' s = IPrimVal (namedFC s)

-- test this, possibly using InCurrentNS, it's unclear whether the name results
-- list will return useful info or how namespaces affect it.
-- Fetch fully qualified name and ttinfo.
-- TODO intersperse instead of concatmap
-- TODO This currently seems to detect names in other modules that arne't
-- actually exported, so I need to also check the visibility of the names this
-- finds.
export
lookupName : Name -> Elab (Name, TTImp)
lookupName n = do
  [(name,imp)] <- getType n
    | xs => fail $ show n ++
      case xs of
        [] => " is not in scope."
        xs => " is not uniquely in scope, these conflicting names exist: " ++
          concatMap (show . fst) xs
  pure (name,imp)

-- `[ ] returns a list, assert that it only returned one declaration where it
-- was used
export
singleDecl : String -> List Decl -> Elab Decl
singleDecl fun dec = do [dec] <- pure dec
                          | _ => fail $ "code error in " ++ fun
                        pure dec

export
getExplicitArgs : Name -> Elab (List Name)
getExplicitArgs n = do (_,tyimp) <- lookupName n
                       getEArgs tyimp
  where
    getEArgs : TTImp -> Elab (List Name)
    getEArgs (IPi _ _ ExplicitArg _ _ retTy)
      = [| genSym "arg" :: getEArgs retTy |]
    getEArgs (IPi _ _ _ _ _ retTy) = getEArgs retTy -- skip implicit args
    getEArgs _ = pure []

export
readableGenSym : String -> Elab Name
readableGenSym s = do MN n i <- genSym s
                        | _ => fail "readableGenSym failure"
                      pure (UN (n ++ show i))

export
mapName : (String -> String) -> Name -> Name
mapName f (UN n) = UN (f n)
mapName f (MN n i) = (MN (f n) i)
mapName f (NS ns n) = (NS ns (mapName f n))
mapName f (DN n realn) = (DN (f n) realn)
mapName f (RF n) = RF (f n)

export
extractNameStr : Name -> String
extractNameStr (UN x) = x
extractNameStr (MN x y) = x
extractNameStr (NS xs x) = extractNameStr x
extractNameStr (DN x _) = x
extractNameStr (RF x) = x

isOpChar : Char -> Bool
isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~")

export
isOpName : Name -> Bool
isOpName n = any isOpChar (unpack (extractNameStr n))

export
extractNameNo : Name -> Int
extractNameNo (MN _ i) = i
extractNameNo _ = 0

-- Change/remove this later, we really don't want to export it and we currently
-- do due to the nature of needing to make things public for elaboration
export
implementation Eq Name where
  (==) (UN x) (UN y) = x == y
  (==) (MN x z) (MN y w) = z == w && x == y
  (==) (NS (MkNS xs) x) (NS (MkNS ys) y) = xs == ys && x == y
  (==) _ _ = False

export
isExplicitPi : PiInfo t -> Bool
isExplicitPi ExplicitArg = True
isExplicitPi _ = False

export
isImplicitPi : PiInfo t -> Bool
isImplicitPi ImplicitArg = True
isImplicitPi _ = False

export
isAutoImplicitPi : PiInfo t -> Bool
isAutoImplicitPi AutoImplicit = True
isAutoImplicitPi _ = False

export
logDecls : String -> Nat -> String -> List Decl -> Elab ()
logDecls ty n s d = logTerm ty n s $ ILocal EmptyFC d `( () )

-- Turn a name into a string, add parens to an operator-like string
export
showName : Name -> Elab String
showName n = let s = extractNameStr n
             in  case strM s of
                   StrNil => fail "showName: empty name"
                   StrCons x xs => pure $
                     if isAlpha x then s else "(" ++ s ++ ")"

export
bindNameVar : Name -> TTImp
bindNameVar = iBindVar . extractNameStr

-- bindNameVar = iBindVar  . show

-----------------------------
-- Predicates
-- Replace these with something better down the road, even just Eq?
-----------------------------

export
Show Count where
  show M0 = "M0"
  show M1 = "M1"
  show MW = "MW"

export
Show (PiInfo tt) where
  show ImplicitArg = "ImplicitArg"
  show ExplicitArg = "ExplicitArg"
  show AutoImplicit = "AutoImplicit"
  show (DefImplicit _) = "DefImplicit _"

-- Don't do this yourself, use Selectors :>
export
isUse0 : Count -> Bool
isUse0 M0 = True
isUse0 _ = False

export
isUse1 : Count -> Bool
isUse1 M1 = True
isUse1 _ = False

export
isUseW : Count -> Bool
isUseW MW = True
isUseW _ = False

export
isType : TTImp -> Bool
isType (IType _) = True
isType _ = False

-- e.g. %runElab printInterfaceCon `{{Eq}}
export
printInterfaceCon : Name -> Elab ()
printInterfaceCon n = do
  (qname,_) <- lookupName n
  let nstr = extractNameStr n
  [NS _ (DN _ icon)] <- getCons qname
    | _ => fail $ "showObject: error during " ++ nstr ++ " constructor lookup"
  (_, objimp) <- lookupName icon
  logTerm "printInterfaceCon" 1 (nstr ++ ": ") objimp

alterTT : (TTImp -> Maybe TTImp) -> TTImp -> TTImp
alterTT f tt = maybe tt id (f tt)

Eq FC where
  (MkFC x1 y1 z1) == (MkFC x2 y2 z2) = x1 == x2 && y1 == y2 && z1 == z2
  EmptyFC == EmptyFC = True
  _ == _ = False

-- bleh, but if I can polish Eq enough to add the deriving to the compiler this can go away.
Eq TTImp where
  (IVar x1 y1) == (IVar x2 y2) = x1 == x2 && y1 == y2
  (IPi x1 y1 z1 w1 argTy1 retTy1) == (IPi x2 y2 z2 w2 argTy2 retTy2) = ?holeEq_2
  (ILam x1 y1 z1 w1 argTy1 lamTy1) == (ILam x2 y2 z2 w2 argTy2 lamTy2) = ?holeEq_3
  (ILet a1 x1 y1 z1 nTy1 nVal1 scope1) == (ILet a2 x2 y2 z2 nTy2 nVal2 scope2) = ?holeEq_4
  (ICase x1 y1 ty1 xs1) == (ICase x2 y2 ty2 xs2) = ?holeEq_5
  (ILocal x1 xs1 y1) == (ILocal x2 xs2 y2) = ?holeEq_6
  (IUpdate x1 xs1 y1) == (IUpdate x2 xs2 y2) = ?holeEq_7
  (IApp x1 y1 z1) == (IApp x2 y2 z2) = x1 == x2 && y1 == y2 && z1 == z2
  (INamedApp x1 y1 z1 w1) == (INamedApp x2 y2 z2 w2) = x1 == x2 && y1 == y2 && z1 == z2 && w1 == w2
  (IAutoApp x1 y1 w1) == (IAutoApp x2 y2 w2) = x1 == x2 && y1 == y2 && w1 == w2
  (IWithApp x1 y1 z1) == (IWithApp x2 y2 z2) = x1 == x2 && y1 == y2 && z1 == z2
  (ISearch x1 depth1) == (ISearch x2 depth2) = x1 == x2 && depth1 == depth2
  (IAlternative x1 y1 xs1) == (IAlternative x2 y2 xs2) = ?holeEq_12
  (IRewrite x1 y1 z1) == (IRewrite x2 y2 z2) = ?holeEq_13
  (IBindHere x1 y1 z1) == (IBindHere x2 y2 z2) = ?holeEq_14
  (IBindVar x1 y1) == (IBindVar x2 y2) = ?holeEq_15
  (IAs a1 x1 y1 z1 w1) == (IAs a2 x2 y2 z2 w2) = ?holeEq_16
  (IMustUnify x1 y1 z1) == (IMustUnify x2 y2 z2) = ?holeEq_17
  (IDelayed x1 y1 z1) == (IDelayed x2 y2 z2) = ?holeEq_18
  (IDelay x1 y1) == (IDelay x2 y2) = ?holeEq_19
  (IForce x1 y1) == (IForce x2 y2) = ?holeEq_20
  (IQuote x1 y1) == (IQuote x2 y2) = ?holeEq_21
  (IQuoteName x1 y1) == (IQuoteName x2 y2) = ?holeEq_22
  (IQuoteDecl x1 y1) == (IQuoteDecl x2 y2) = ?holeEq_23
  (IUnquote x1 y1) == (IUnquote x2 y2) = ?holeEq_24
  (IPrimVal x1 c1) == (IPrimVal x2 c2) = ?holeEq_25
  (IType x1) == (IType x2) = ?holeEq_26
  (IHole x1 y1) == (IHole x2 y2) = ?holeEq_27
  (Implicit x1 bindIfUnsolved1) == (Implicit x2 bindIfUnsolved2) = ?holeEq_28
  (IWithUnambigNames x1 xs1 y1) == (IWithUnambigNames x2 xs2 y2) = ?holeEq_29
  _ == _ = False

-- ||| target for mapping an exact given TTImp
-- target : TTImp -> (TTImp -> TTImp) -> TTImp -> TTImp


text:
module Compiler.ES.ImperativeAst

import Compiler.CompileExpr
import public Core.TT
import public Data.Vect
import public Data.List

mutual
  public export
  data ImperativeExp = IEVar Name
                     | IELambda (List Name) ImperativeStatement
                     | IEApp ImperativeExp (List ImperativeExp)
                     | IEConstant Constant
                     | IEPrimFn (PrimFn arity) (Vect arity ImperativeExp)
                     | IEPrimFnExt Name (List ImperativeExp)
                     | IEConstructorHead ImperativeExp
                     | IEConstructorTag (Either Int String)
                     | IEConstructorArg Int ImperativeExp
                     | IEConstructor (Either Int String) (List ImperativeExp)
                     | IEDelay ImperativeExp
                     | IEForce ImperativeExp
                     | IENull

  public export
  data ImperativeStatement = DoNothing
                           | SeqStatement ImperativeStatement ImperativeStatement
                           | FunDecl FC Name (List Name) ImperativeStatement
                           | ForeignDecl FC Name (List String) (List CFType) CFType
                           | ReturnStatement ImperativeExp
                           | SwitchStatement ImperativeExp (List (ImperativeExp, ImperativeStatement)) (Maybe ImperativeStatement)
                           | LetDecl Name (Maybe ImperativeExp)
                           | ConstDecl Name ImperativeExp
                           | MutateStatement Name ImperativeExp
                           | ErrorStatement String
                           | EvalExpStatement ImperativeExp
                           | CommentStatement String
                           | ForEverLoop ImperativeStatement

public export
Semigroup ImperativeStatement where
  DoNothing <+> y = y
  x <+> DoNothing = x
  x <+> y = SeqStatement x y

public export
Monoid ImperativeStatement where
  neutral = DoNothing

mutual
  export
  Show ImperativeExp where
    show (IEVar n) =  "(IEVar " ++ show n ++ ")"
    show (IELambda args b) = "(IELambda " ++ show args ++ " " ++ show b ++ ")"
    show (IEApp f args) = "(IEApp " ++ show f ++ " " ++ show args ++ ")"
    show (IEConstant c) =  "(IEConstant " ++ show c ++ ")"
    show (IEPrimFn f args) = "(IEPrimFn " ++ show f ++ " " ++ show args ++ ")"
    show (IEPrimFnExt f args) = "(IEPrimFnExt " ++ show f ++ " " ++ show args ++ ")"
    show (IEConstructorHead c) =  "(IEConstructorHead " ++ show c ++ ")"
    show (IEConstructorTag t) =  "(IEConstructorTag " ++ show t ++ ")"
    show (IEConstructorArg i c) = "(IEConstructorArg " ++ show i ++ " " ++ show c ++ ")"
    show (IEConstructor i args) = "(IEConstructor " ++ show i ++ " " ++ show args ++ ")"
    show (IEDelay x) =  "(IEDelay " ++ show x ++ ")"
    show (IEForce x) =  "(IEForce " ++ show x ++ ")"
    show IENull = "IENull"

  export
  Show ImperativeStatement where
    show DoNothing = "DoNothing"
    show (SeqStatement x y) = show x ++ ";" ++ show y
    show (FunDecl fc n args b) = "\n\n" ++ "(FunDecl (" ++ show fc ++ ") " ++ show n ++ " " ++ show args ++ " " ++ show b ++ ")"
    show (ForeignDecl fc n path args ret) = "(ForeignDecl " ++ show n ++ " " ++ show path ++")"
    show (ReturnStatement x) = "(ReturnStatement " ++ show x ++ ")"
    show (SwitchStatement e alts d) = "(SwitchStatement " ++ show e ++ " " ++ show alts ++ " " ++ show d ++ ")"
    show (LetDecl n v) = "(LetDecl " ++ show n ++ " " ++ show v ++ ")"
    show (ConstDecl n v) = "(ConstDecl " ++ show n ++ " " ++ show v ++ ")"
    show (MutateStatement n v) = "(MutateStatement " ++ show n ++ " " ++ show v ++ ")"
    show (ErrorStatement s) = "(ErrorStatement " ++ s ++ ")"
    show (EvalExpStatement x) =  "(EvalExpStatement " ++ show x ++ ")"
    show (CommentStatement x) = "(CommentStatement " ++ show x ++ ")"
    show (ForEverLoop x) = "(ForEverLoop " ++ show x ++ ")"

mutual
  public export
  replaceNamesExp : List (Name, ImperativeExp) -> ImperativeExp -> ImperativeExp
  replaceNamesExp reps (IEVar n) =
    case lookup n reps of
      Nothing => IEVar n
      Just e => e
  replaceNamesExp reps (IELambda args body) =
    IELambda args $ replaceNamesExpS reps body
  replaceNamesExp reps (IEApp f args) =
    IEApp (replaceNamesExp reps f) (replaceNamesExp reps <$> args)
  replaceNamesExp reps (IEConstant c) =
    IEConstant c
  replaceNamesExp reps (IEPrimFn f args) =
    IEPrimFn f (replaceNamesExp reps <$> args)
  replaceNamesExp reps (IEPrimFnExt f args) =
    IEPrimFnExt f (replaceNamesExp reps <$> args)
  replaceNamesExp reps (IEConstructorHead e) =
    IEConstructorHead $ replaceNamesExp reps e
  replaceNamesExp reps (IEConstructorTag i) =
    IEConstructorTag i
  replaceNamesExp reps (IEConstructorArg i e) =
    IEConstructorArg i (replaceNamesExp reps e)
  replaceNamesExp reps (IEConstructor t args) =
    IEConstructor t (replaceNamesExp reps <$> args)
  replaceNamesExp reps (IEDelay e) =
    IEDelay $ replaceNamesExp reps e
  replaceNamesExp reps (IEForce e) =
    IEForce $ replaceNamesExp reps e
  replaceNamesExp reps IENull =
    IENull

  public export
  replaceNamesExpS : List (Name, ImperativeExp) -> ImperativeStatement -> ImperativeStatement
  replaceNamesExpS reps DoNothing =
    DoNothing
  replaceNamesExpS reps (SeqStatement x y) =
    SeqStatement (replaceNamesExpS reps x) (replaceNamesExpS reps y)
  replaceNamesExpS reps (FunDecl fc n args body) =
    FunDecl fc n args $ replaceNamesExpS reps body
  replaceNamesExpS reps decl@(ForeignDecl fc n path args ret) =
    decl
  replaceNamesExpS reps (ReturnStatement e) =
    ReturnStatement $ replaceNamesExp reps e
  replaceNamesExpS reps (SwitchStatement s alts def) =
    let s_    = replaceNamesExp reps s
        alts_ = (\(e,b) => (replaceNamesExp reps e, replaceNamesExpS reps b)) <$> alts
        def_  = replaceNamesExpS reps <$> def
    in SwitchStatement s_ alts_ def_
  replaceNamesExpS reps (LetDecl n v) =
    LetDecl n $ replaceNamesExp reps <$> v
  replaceNamesExpS reps (ConstDecl n v) =
    ConstDecl n $ replaceNamesExp reps v
  replaceNamesExpS reps (MutateStatement n v) =
    MutateStatement n $ replaceNamesExp reps v
  replaceNamesExpS reps (ErrorStatement s) =
    ErrorStatement s
  replaceNamesExpS reps (EvalExpStatement x) =
    EvalExpStatement $ replaceNamesExp reps x
  replaceNamesExpS reps (CommentStatement x) =
    CommentStatement x
  replaceNamesExpS reps (ForEverLoop x) =
    ForEverLoop $ replaceNamesExpS reps x


text:
module States

import Effects
import Effect.State
import Control.Monad.Identity

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

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

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

labelFrom : (i : Int) -> Tree a -> Tree (Int, a)
labelFrom i x = runPure (do put i; label x)

-- *state> labelFrom 1 t1
-- Node (Node Leaf (1, "One") (Node Leaf (2, "Two") Leaf))
--      (3, "Three")
--      (Node (Node Leaf (4, "Four") Leaf) (5, "Five") Leaf) : Tree (Int, String)


text:
module System.Random.Node

import Data.List

%default total

%foreign "node:lambda:() => Math.random()"
prim__rnd : PrimIO Double

||| Generate a random number between 0 and 1.
export
rnd : HasIO io => io Double
rnd = primIO $ prim__rnd

export
rndSelect : HasIO io => (elems : List a) -> (0 _ : NonEmpty elems) => io a
rndSelect elems =
  do randomDouble <- rnd
     let randomNat : Nat = cast . floor $ randomDouble * cast (length elems)
     pure $
       case inBounds randomNat elems of
            (No _)  => head elems
            (Yes _) => index randomNat elems

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
import Data.Vect

Position : Type
Position = (Double, Double)

Polygon : Nat -> Type
Polygon n = Vect n Position

tri : Polygon 3
tri = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]


text:
module TTImp.ProcessRecord

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.UnifyState
import Core.Value

import TTImp.BindImplicits
import TTImp.Elab
import TTImp.Elab.Check
import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Unelab
import TTImp.Utils

import Data.List

%default covering

mkDataTy : FC -> List (Name, RigCount, PiInfo RawImp, RawImp) -> RawImp
mkDataTy fc [] = IType fc
mkDataTy fc ((n, c, p, ty) :: ps)
    = IPi fc c p (Just n) ty (mkDataTy fc ps)

-- Projections are only visible if the record is public export
projVis : Visibility -> Visibility
projVis Public = Public
projVis _ = Private

elabRecord : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             List ElabOpt -> FC -> Env Term vars ->
             NestedNames vars -> Maybe String ->
             Visibility -> Name ->
             (params : List (Name, RigCount, PiInfo RawImp, RawImp)) ->
             (conName : Name) ->
             List IField ->
             Core ()
elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
    = do conName <- inCurrentNS conName_in
         elabAsData conName
         defs <- get Ctxt
         Just conty <- lookupTyExact conName (gamma defs)
             | Nothing => throw (InternalError ("Adding " ++ show tn ++ "failed"))

         -- Go into new namespace, if there is one, for getters
         case newns of
              Nothing => elabGetters conName 0 [] [] conty
              Just ns =>
                   do let cns = currentNS defs
                      let nns = nestedNS defs
                      extendNS (mkNamespace ns)
                      newns <- getNS
                      elabGetters conName 0 [] [] conty
                      defs <- get Ctxt
                      -- Record that the current namespace is allowed to look
                      -- at private names in the nested namespace
                      put Ctxt (record { currentNS = cns,
                                         nestedNS = newns :: nns } defs)
  where
    paramTelescope : List (FC, Maybe Name, RigCount, PiInfo RawImp, RawImp)
    paramTelescope = map jname params
      where
        jname : (Name, RigCount, PiInfo RawImp, RawImp)
             -> (FC, Maybe Name, RigCount, PiInfo RawImp, RawImp)
        -- Record type parameters are implicit in the constructor
        -- and projections
        jname (n, _, _, t) = (EmptyFC, Just n, erased, Implicit, t)

    fname : IField -> Name
    fname (MkIField fc c p n ty) = n

    farg : IField ->
           (FC, Maybe Name, RigCount, PiInfo RawImp, RawImp)
    farg (MkIField fc c p n ty) = (virtualiseFC fc, Just n, c, p, ty)

    mkTy : List (FC, Maybe Name, RigCount, PiInfo RawImp, RawImp) ->
           RawImp -> RawImp
    mkTy [] ret = ret
    mkTy ((fc, n, c, imp, argty) :: args) ret
        = IPi fc c imp n argty (mkTy args ret)

    recTy : RawImp
    recTy = apply (IVar (virtualiseFC fc) tn) (map (\(n, c, p, tm) => (n, IVar EmptyFC n, p)) params)
      where
        ||| Apply argument to list of explicit or implicit named arguments
        apply : RawImp -> List (Name, RawImp, PiInfo RawImp) -> RawImp
        apply f [] = f
        apply f ((n, arg, Explicit) :: xs) = apply (IApp         (getFC f) f          arg) xs
        apply f ((n, arg, _       ) :: xs) = apply (INamedApp (getFC f) f n arg) xs

    elabAsData : Name -> Core ()
    elabAsData cname
        = do let fc = virtualiseFC fc
             let conty = mkTy paramTelescope $
                         mkTy (map farg fields) recTy
             let con = MkImpTy EmptyFC EmptyFC cname !(bindTypeNames fc [] (map fst params ++
                                           map fname fields ++ vars) conty)
             let dt = MkImpData fc tn !(bindTypeNames fc [] (map fst params ++
                                           map fname fields ++ vars)
                                         (mkDataTy fc params)) [] [con]
             log "declare.record" 5 $ "Record data type " ++ show dt
             processDecl [] nest env (IData fc vis dt)

    countExp : Term vs -> Nat
    countExp (Bind _ _ (Pi _ _ Explicit _) sc) = S (countExp sc)
    countExp (Bind _ _ (Pi _ _ _ _) sc) = countExp sc
    countExp _ = 0

    -- Generate getters from the elaborated record constructor type
    --
    -- WARNING: if you alter the names of the getters,
    --          you probably will have to adjust TTImp.TTImp.definedInBlock.
    --
    elabGetters : {vs : _} ->
                  Name ->
                  (done : Nat) -> -- number of explicit fields processed
                  List (Name, RawImp) -> -- names to update in types
                    -- (for dependent records, where a field's type may depend
                    -- on an earlier projection)
                  Env Term vs -> Term vs ->
                  Core ()
    elabGetters con done upds tyenv (Bind bfc n b@(Pi _ rc imp ty_chk) sc)
        = let rig = if isErased rc then erased else top
              isVis = projVis vis
          in if (n `elem` map fst params) || (n `elem` vars)
             then elabGetters con
                              (if imp == Explicit && not (n `elem` vars)
                                  then S done else done)
                              upds (b :: tyenv) sc
             else
                do let fldNameStr = nameRoot n
                   rfNameNS <- inCurrentNS (UN $ Field fldNameStr)
                   unNameNS <- inCurrentNS (UN $ Basic fldNameStr)

                   let nestDrop
                          = map (\ (n, (_, ns, _)) => (n, length ns))
                                (names nest)
                   nestDrop <- traverse (\ (n, ns) => pure (!(toFullNames n), ns)) nestDrop
                   ty <- unelabNest nestDrop tyenv ty_chk
                   let ty' = substNames vars upds $ map rawName ty
                   log "declare.record.field" 5 $ "Field type: " ++ show ty'
                   let rname = MN "rec" 0

                   -- Claim the projection type
                   projTy <- bindTypeNames fc []
                                 (map fst params ++ map fname fields ++ vars) $
                                    mkTy paramTelescope $
                                      IPi bfc top Explicit (Just rname) recTy ty'

                   let mkProjClaim = \ nm =>
                          let ty = MkImpTy EmptyFC EmptyFC nm projTy
                          in IClaim bfc rig isVis [Inline] ty

                   log "declare.record.projection" 5 $
                      "Projection " ++ show rfNameNS ++ " : " ++ show projTy
                   processDecl [] nest env (mkProjClaim rfNameNS)

                   -- Define the LHS and RHS
                   let lhs_exp
                          = apply (IVar bfc con)
                                    (replicate done (Implicit bfc True) ++
                                       (if imp == Explicit
                                           then [IBindVar EmptyFC fldNameStr]
                                           else []) ++
                                    (replicate (countExp sc) (Implicit bfc True)))
                   let lhs = IApp bfc (IVar bfc rfNameNS)
                                (if imp == Explicit
                                    then lhs_exp
                                    else INamedApp bfc lhs_exp (UN $ Basic fldNameStr)
                                             (IBindVar bfc fldNameStr))
                   let rhs = IVar EmptyFC (UN $ Basic fldNameStr)
                   log "declare.record.projection" 5 $ "Projection " ++ show lhs ++ " = " ++ show rhs
                   processDecl [] nest env
                       (IDef bfc rfNameNS [PatClause bfc lhs rhs])

                   -- Make prefix projection aliases if requested
                   when !isPrefixRecordProjections $ do  -- beware: `!` is NOT boolean `not`!
                     -- Claim the type.
                     -- we just reuse `projTy` defined above
                     log "declare.record.projection.prefix" 5 $
                       "Prefix projection " ++ show unNameNS ++ " : " ++ show projTy
                     processDecl [] nest env (mkProjClaim unNameNS)

                     -- Define the LHS and RHS
                     let lhs = IVar bfc unNameNS
                     let rhs = IVar bfc rfNameNS
                     log "declare.record.projection.prefix" 5 $
                       "Prefix projection " ++ show lhs ++ " = " ++ show rhs
                     processDecl [] nest env
                         (IDef bfc unNameNS [PatClause bfc lhs rhs])

                   -- Move on to the next getter.
                   --
                   -- In upds, we use unNameNS (as opposed to rfNameNS or both)
                   -- because the field types will probably mention the UN versions of the projections.
                   let upds' = (n, IApp bfc (IVar bfc unNameNS) (IVar bfc rname)) :: upds
                   elabGetters con
                               (if imp == Explicit
                                   then S done else done)
                               upds' (b :: tyenv) sc

    elabGetters con done upds _ _ = pure ()

export
processRecord : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto m : Ref MD Metadata} ->
                {auto u : Ref UST UState} ->
                List ElabOpt -> NestedNames vars ->
                Env Term vars -> Maybe String ->
                Visibility -> ImpRecord -> Core ()
processRecord eopts nest env newns vis (MkImpRecord fc n ps cons fs)
    = elabRecord eopts fc env nest newns vis n ps cons fs


text:
module Core.Transform

import Core.Context
import Core.Env
import Core.Normalise
import Core.TT

import Data.NameMap

%default total

unload : List (FC, Term vars) -> Term vars -> Term vars
unload [] fn = fn
unload ((fc, arg) :: args) fn = unload args (App fc fn arg)

-- List of matches on LHS
data MatchVars : List Name -> List Name -> Type where
     None : MatchVars lhsvars vs
     Match : (idx : Nat) -> (0 p : IsVar n idx lhsvars) -> Term vs ->
             MatchVars lhsvars vs -> MatchVars lhsvars vs

lookupMatch : (idx : Nat) -> (0 p : IsVar n idx lhsvars) -> MatchVars lhsvars vs ->
              Maybe (Term vs)
lookupMatch idx p None = Nothing
lookupMatch idx p (Match v _ val rest)
    = if idx == v
         then Just val
         else lookupMatch idx p rest

addMatch : (idx : Nat) -> (0 p : IsVar n idx lhsvars) -> Term vs ->
           MatchVars lhsvars vs -> Maybe (MatchVars lhsvars vs)
addMatch idx p val ms
    = case lookupMatch idx p ms of
           Nothing => Just (Match idx p val ms)
           Just val' => if eqTerm val val'
                           then Just ms
                           else Nothing

-- LHS of a rule must be a function application, so there's not much work
-- to do here!
match : MatchVars vars vs ->
        Term vars -> Term vs -> Maybe (MatchVars vars vs)
match ms (Local _ _ idx p) val
    = addMatch idx p val ms
match ms (App _ f a) (App _ f' a')
    = do ms' <- match ms f f'
         match ms' a a'
match ms x y
    = if eqTerm x y
         then Just ms
         else Nothing

covering
tryReplace : MatchVars vars vs -> Term vars -> Maybe (Term vs)
tryReplace ms (Local _ _ idx p) = lookupMatch idx p ms
tryReplace ms (Ref fc nt n) = pure (Ref fc nt n)
tryReplace ms (Meta fc n i as)
    = do as' <- traverse (tryReplace ms) as
         pure (Meta fc n i as')
tryReplace ms (Bind fc x b sc)
    = Nothing -- TODO: can't do this yet... need to be able to weaken ms
              -- Rules are unlikely to have binders usually but we should
              -- still support it eventually
tryReplace ms (App fc f a)
    = do f' <- tryReplace ms f
         a' <- tryReplace ms a
         pure (App fc f' a')
tryReplace ms (As fc s a p)
    = do a' <- tryReplace ms a
         p' <- tryReplace ms p
         pure (As fc s a' p')
tryReplace ms (TDelayed fc r tm)
    = do tm' <- tryReplace ms tm
         pure (TDelayed fc r tm')
tryReplace ms (TDelay fc r ty tm)
    = do ty' <- tryReplace ms ty
         tm' <- tryReplace ms tm
         pure (TDelay fc r ty' tm')
tryReplace ms (TForce fc r tm)
    = do tm' <- tryReplace ms tm
         pure (TForce fc r tm')
tryReplace ms (PrimVal fc c) = pure (PrimVal fc c)
tryReplace ms (Erased fc i) = pure (Erased fc i)
tryReplace ms (TType fc) = pure (TType fc)

covering
tryApply : Transform -> Term vs -> Maybe (Term vs)
tryApply trans@(MkTransform {vars} n _ lhs rhs) tm
   = case match None lhs tm of
          Just ms => tryReplace ms rhs
          Nothing =>
            case tm of
                 App fc f a =>
                     do f' <- tryApply trans f
                        Just (App fc f' a)
                 _ => Nothing

apply : List Transform -> Term vars -> (Bool, Term vars)
apply [] tm = (False, tm)
apply (t :: ts) tm
    = case tryApply t tm of
           Nothing => apply ts tm
           Just res => (True, res)

data Upd : Type where

covering
trans : {auto c : Ref Ctxt Defs} ->
        {auto u : Ref Upd Bool} ->
        Env Term vars -> List (FC, Term vars) -> Term vars ->
        Core (Term vars)
trans env stk (Ref fc Func fn)
    = do defs <- get Ctxt
         case lookup fn (transforms defs) of
              Nothing => pure (unload stk (Ref fc Func fn))
              Just ts => do let fullapp = unload stk (Ref fc Func fn)
                            let (u, tm') = apply ts fullapp
                            upd <- get Upd
                            put Upd (upd || u)
                            pure tm'
trans env stk (Meta fc n i args)
    = do args' <- traverse (trans env []) args
         pure $ unload stk (Meta fc n i args')
trans env stk (Bind fc x b sc)
    = do b' <- traverse (trans env []) b
         sc' <- trans (b' :: env) [] sc
         pure $ unload stk (Bind fc x b' sc')
trans env stk (App fc fn arg)
    = do arg' <- trans env [] arg
         trans env ((fc, arg') :: stk) fn
trans env stk (TDelayed fc r tm)
    = do tm' <- trans env [] tm
         pure $ unload stk (TDelayed fc r tm')
trans env stk (TDelay fc r ty tm)
    = do ty' <- trans env [] ty
         tm' <- trans env [] tm
         pure $ unload stk (TDelay fc r ty' tm')
trans env stk (TForce fc r tm)
    = do tm' <- trans env [] tm
         pure $ unload stk (TForce fc r tm')
trans env stk tm = pure $ unload stk tm

covering
transLoop : {auto c : Ref Ctxt Defs} ->
            Nat -> Env Term vars -> Term vars -> Core (Term vars)
transLoop Z env tm = pure tm
transLoop (S k) env tm
    = do u <- newRef Upd False
         tm' <- trans env [] tm
         upd <- get Upd
         if upd -- If there was a transform applied, go around again until
                -- we hit the threshold
            then transLoop k env tm'
            else pure tm'

export
covering
applyTransforms : {auto c : Ref Ctxt Defs} ->
                  Env Term vars -> Term vars -> Core (Term vars)
applyTransforms env tm = transLoop 5 env tm


text:
module WebAssembly.Validation.Types

import public WebAssembly.Validation.Types.Limits
import public WebAssembly.Validation.Types.BlockTypes
import public WebAssembly.Validation.Types.FunctionTypes
import public WebAssembly.Validation.Types.TableTypes
import public WebAssembly.Validation.Types.MemoryTypes
import public WebAssembly.Validation.Types.GlobalTypes
import public WebAssembly.Validation.Types.ExternalTypes

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
parameters (n : Nat)
    data X : Type -> Type where
         A : t -> X t
         B : t -> X t

    Eq t => Eq (X t) where
      A x == A y = x == y
      B x == B y = x == y
      _ == _ = False

    test : Char -> Char -> Bool
    test x y = A x == A y

mkEq : (approx : Bool) -> Eq Nat
mkEq True = withinOne
  where
    [withinOne] Eq Nat where
      Z == Z = True
      Z == S Z = True
      S Z == Z = True
      S x == S y = x == y
      _ == _ = False
mkEq False = %search


text:
module Inigo.Template

import Data.List1
import Data.SnocList
import Data.String
import Debug.Trace

public export
record Pos where
    constructor MkPos
    line : Int
    col : Int

Show Pos where
    show pos = "\{show pos.line}:\{show pos.col}"

initPos : Pos
initPos = MkPos 1 1

nextChar : Pos -> Pos
nextChar = record { col $= (+ 1) }

nextLine : Pos -> Pos
nextLine = record { line $= (+ 1), col = 1 }

advance : Char -> Pos -> Pos
advance '\n' = nextLine
advance _ = nextChar

data TempVar
    = Package
    | Namespace
    | File String

data TempPart : Type where
    Var : TempVar -> TempPart
    Text : String -> TempPart

data TempState : Type where
    InText : SnocList Char -> TempState
    InVar : SnocList Char -> TempState
    Escape : TempState

initState : TempState
initState = InText [<]

unknownVar : Either String a
unknownVar = Left "Unknown variable"

parseVar : List Char -> Maybe TempVar
parseVar ['P', 'a', 'c', 'k', 'a', 'g', 'e'] = Just Package
parseVar ['N', 'a', 'm', 'e', 's', 'p', 'a', 'c', 'e'] = Just Namespace
parseVar ('f' :: 'i' :: 'l' :: 'e' :: ' ' :: file) = Just $ File $ fastPack file
parseVar _ = Nothing

makeText : SnocList TempPart -> SnocList Char -> SnocList TempPart
makeText acc [<] = acc
makeText acc xs = acc :< Text (fastPack $ xs <>> [])

cleanStart : List TempPart -> List TempPart
cleanStart (Text t :: xs) = if "\n" `isPrefixOf` t
    then Text (assert_total $ strSubstr 1 (cast (length t) - 1) t) :: xs
    else Text t :: xs
cleanStart xs = xs

cleanEnd : SnocList TempPart -> SnocList TempPart
cleanEnd (xs :< Text t) = if "\n" `isSuffixOf` t
    then xs :< Text (assert_total $ strSubstr 0 (cast (length t) - 1) t)
    else xs :< Text t
cleanEnd xs = xs

parse :
    TempState -> -- state
    List Char -> -- input
    SnocList TempPart -> -- accumulator
    Pos -> -- position
    Either (Pos, String) (SnocList TempPart)
parse (InText xs) [] acc pos = Right $ makeText acc xs
parse (InText xs) ('\\' :: ys) acc pos = parse Escape ys (makeText acc xs) (nextChar pos)
parse (InText xs) (x :: ys) acc pos = parse (InText $ xs :< x) ys acc (advance x pos)

parse (InVar xs) [] acc pos = Left (pos, "Missing closing brace")
parse (InVar xs) ('}' :: ys) acc pos =
    let xs' = xs <>> []
     in case parseVar xs' of
        Nothing => Left (pos, "Unknown variable: \{fastPack xs'}")
        Just var@(File _) => parse initState ys (cleanEnd acc :< Var var) (nextChar pos)
        Just var => parse initState ys (acc :< Var var) (nextChar pos)
parse (InVar xs) (x :: ys) acc pos = parse (InVar $ xs :< x) ys acc (advance x pos)

parse Escape [] acc pos = Left (pos, "Trailing escape character")
parse Escape ('\\' :: xs) acc pos = parse initState xs (acc :< Text "\\") (nextChar pos)
parse Escape ('{' :: xs) acc pos = parse (InVar [<]) xs acc (nextChar pos)
parse Escape (x :: xs) acc pos = Left (pos, "Unknown escape character: \{show x}")

seperateFiles :
    SnocList TempPart -> -- input
    List TempPart -> -- accumulator for the file
    List (String, List TempPart) -> -- accumulator for the entire template
    Either String (List (String, List TempPart))
seperateFiles [<] _ acc = Right acc
seperateFiles (sx :< Var (File fp)) file acc = seperateFiles sx [] ((fp, cleanStart file) :: acc)
seperateFiles (sx :< x) xs ys = seperateFiles sx (x :: xs) ys

parameters (ns, pkg : String)

    renderVar : TempVar -> Either String String
    renderVar Package = Right pkg
    renderVar Namespace = Right ns
    renderVar (File x) = Left "Internal Error: Unexpected \\{file ...}"

    renderTemplate :
        List TempPart -> -- template
        SnocList String -> -- accumulator
        Either String (SnocList String)
    renderTemplate [] acc = Right acc
    renderTemplate (Var x :: xs) acc = case renderVar x of
        Left err => Left err
        Right v => renderTemplate xs (acc :< v)
    renderTemplate (Text x :: xs) acc = renderTemplate xs (acc :< x)

    render :
        List (String, List TempPart) ->
        List (String, String) ->
        Either String (List (String, String))
    render [] acc = Right acc
    render ((fp, temp) :: ts) acc = case renderTemplate temp [<] of
        Left err => Left err
        Right res => render ts $ (fp, fastConcat $ res <>> []) :: acc

    export
    runTemplate :
        String -> -- filepath
        String -> -- input
        Either String (List (String, String))
    runTemplate fp inp0 = do
        let Right inp1 = parse initState (fastUnpack inp0)  [<] initPos
            | Left (pos, err) => Left $ "Parse error in \{fp}, at \{show pos}: \{err}"
        let Right inp2 = seperateFiles inp1 [] []
            | Left err => Left $ "Parse error in \{fp}: \{err}"
        render inp2 []

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Circuits.NetList.Linear.Usage.DataType

import Decidable.Equality

import Data.Nat
import Data.List.Elem
import Data.List.Quantifiers

import Data.Vect
import Data.Vect.AtIndex
import Data.Vect.Quantifiers

import Data.String

import Toolkit.Data.Whole
import Toolkit.Data.DList
import Toolkit.Data.DList.Elem

--import Toolkit.Data.Vect.Leanings
import Toolkit.Data.Vect.Extra
import Toolkit.Data.DVect

import Circuits.Common

import Circuits.NetList.Types

%default total

public export
data Usage : DType -> Type where
  Logic : (u : Usage) -> Usage LOGIC

  Array : (us : Vect            (S n)           (Usage type))
             -> Usage (BVECT (W (S n) ItIsSucc)        type)

mutual
  namespace Free
    public export
    data IsFree : (type : DType) -> (u : Usage type) -> Type
      where
        FreeL : IsFree LOGIC (Logic FREE)
        FreeA : (prf : All (IsFree type) os)
                    -> IsFree (BVECT (W (S n) ItIsSucc) type) (Array os)

    Uninhabited (IsFree LOGIC (Logic USED)) where
      uninhabited FreeL impossible

  namespace Used
    public export
    data IsUsed : (type : DType) -> (u : Usage type) -> Type
      where
        UsedL : IsUsed LOGIC (Logic USED)
        UsedA : (prf : All (IsUsed type) os)
                    -> IsUsed (BVECT (W (S n) ItIsSucc) type) (Array os)

    Uninhabited (IsUsed LOGIC (Logic FREE)) where
      uninhabited UsedL impossible

  namespace Part
    public export
    data IsPart : (type : DType) -> (u : Usage type) -> Type
      where
        PartA : (notF : Any (IsFree type) os )
             -> (notU : Any (IsUsed type) os )
                     -> IsPart (BVECT (W (S n) ItIsSucc) type) (Array os)

    Uninhabited (IsPart LOGIC (Logic u)) where
      uninhabited PartA impossible

mutual

  namespace Free
    notFree : (All (IsFree type) us -> Void)
            -> IsFree (BVECT (W (S n) ItIsSucc) type) (Array us)
            -> Void
    notFree f (FreeA prf) = f prf

    export
    isFree : {type : DType}
          -> (u    : Usage type)
                  -> Dec (IsFree type u)
    isFree (Logic USED)
      = No absurd
    isFree (Logic FREE)
      = Yes FreeL

    isFree (Array us) with (all isFree us)
      isFree (Array us) | (Yes prf)
         = Yes (FreeA prf)
      isFree (Array us) | (No contra)
        = No (notFree contra)

  namespace Used
    notUsed : (All (IsUsed type) us -> Void)
           -> IsUsed (BVECT (W (S n) ItIsSucc) type) (Array us)
           -> Void
    notUsed f (UsedA prf) = f prf

    export
    isUsed : {type : DType}
          -> (u    : Usage type)
                  -> Dec (IsUsed type u)
    isUsed (Logic FREE)
      = No absurd
    isUsed (Logic USED)
      = Yes UsedL

    isUsed (Array us) with (all isUsed us)
      isUsed (Array us) | (Yes prf)
         = Yes (UsedA prf)
      isUsed (Array us) | (No contra)
        = No (notUsed contra)

  namespace Part

    export
    isPart : {type : DType}
          -> (u    : Usage type)
                  -> Dec (IsPart type u)
    isPart (Logic u)
      = No absurd

    isPart (Array us) with (any isFree us)
      isPart (Array us) | (Yes prfF) with (any isUsed us)
        isPart (Array us) | (Yes prfF) | (Yes prfU)
          = Yes (PartA prfF prfU)
        isPart (Array us) | (Yes prfF) | (No contra)
          = No (\(PartA fs us) => contra us)

      isPart (Array us) | (No contra)
        = No (\(PartA fs us) => contra fs)

public export
data IsFreeAt : (idx : Fin n) -> (type : DType) -> (u : Usage type) -> Type
  where
    FreeAt : {idx : Fin m}
          -> {us  : Vect (S n) (Usage type)}
          -> (prf : AtIndexI (Usage type) (IsFree type) m (S n) idx us)
                 -> IsFreeAt idx (BVECT (W (S n) ItIsSucc) type) (Array us)

Uninhabited (IsFreeAt idx LOGIC u) where
  uninhabited (FreeAt prf) impossible

notFreeAtIndex : (AtIndexI (Usage type) (IsFree type) m (S n) idx us -> Void)
              -> IsFreeAt idx (BVECT (W (S n) ItIsSucc) type) (Array us) -> Void
notFreeAtIndex f (FreeAt prf) = f  prf

export
isFreeAt : {type : DType}
        -> {n   : Nat}
        -> (idx : Fin n)
        -> (u   : Usage type)
               -> Dec (IsFreeAt idx type u)

isFreeAt {n = n} idx (Logic u)
  = No absurd

isFreeAt {n = n} idx (Array us) with (atIndexI isFree idx us)
  isFreeAt {n = (S n)} idx (Array us) | (Yes prf)
    = Yes (FreeAt prf)

  isFreeAt {n = n} idx (Array us) | (No contra)
    = No (notFreeAtIndex contra)

public export
data IsUsedAt : (idx : Fin n) -> (type : DType) -> (u : Usage type) -> Type
  where
    UsedAt : {idx : Fin m}
          -> (prf : AtIndexI (Usage type) (IsUsed type) m (S n) idx us)
                 -> IsUsedAt idx (BVECT (W (S n) ItIsSucc) type) (Array us)

Uninhabited (IsUsedAt idx LOGIC u) where
  uninhabited (UsedAt prf) impossible

notUsedAtIndex : (AtIndexI (Usage type) (IsUsed type) m (S n) idx us -> Void)
               -> IsUsedAt idx (BVECT (W (S n) ItIsSucc) type) (Array us) -> Void
notUsedAtIndex f (UsedAt prf) = f prf

export
isUsedAt : {type : DType}
        -> {n   : Nat}
        -> (idx : Fin n)
        -> (u   : Usage type)
               -> Dec (IsUsedAt idx type u)

isUsedAt {n = n} idx (Logic u)
  = No absurd

isUsedAt {n = n} idx (Array us) with (atIndexI isUsed idx us)
  isUsedAt {n = (S n)} idx (Array us) | (Yes prf)
    = Yes (UsedAt prf)

  isUsedAt {n = n} idx (Array us) | (No contra)
    = No (notUsedAtIndex contra)

mutual

  export
  init : (type : DType) -> DPair (Usage type) (IsFree type)
  init LOGIC
    = MkDPair (Logic FREE) FreeL

  init (BVECT (W (S n) ItIsSucc) type) with (init type)
    init (BVECT (W (S n) ItIsSucc) type) | (MkDPair u prf) with (init (S n) u prf)
      init (BVECT (W (S n) ItIsSucc) type) | (MkDPair u prf) | (MkDPair os pU)
        = MkDPair (Array os) (FreeA pU)

  namespace Vect
    export
    init : (n   : Nat)
        -> (u   : Usage type)
        -> (prf : IsFree type u)
               -> DPair (Vect n (Usage type)) (All (IsFree type))
    init Z _ _ = MkDPair [] []
    init (S k) u prf with (init k u prf)
      init (S k) u prf | (MkDPair fst snd)
        = MkDPair (u :: fst) (prf :: snd)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Main

forLoop : List a -> (a -> IO ()) -> IO ()
forLoop [] f = pure ()
forLoop (x :: xs) f = do f x
                         forLoop xs f

syntax for {x} "in" [xs] ":" [body] = forLoop xs (\x => body)

main : IO ()
main = do putStrLn "Counting:"
          for x in [1..10]:
              putStrLn $ "Number " ++ show x
          putStrLn "Done!"

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module Libraries.Data.Fin

import public Data.Fin

%default total

-- TODO: Remove this, once Data.Fin.strengthen from base is available
--       to the compiler

export
strengthen : {n : _} -> Fin (S n) -> Maybe (Fin n)
strengthen {n = S _} FZ = Just FZ
strengthen {n = S _} (FS p) with (Libraries.Data.Fin.strengthen p)
  strengthen (FS _) | Nothing = Nothing
  strengthen (FS _) | Just q  = Just $ FS q
strengthen _ = Nothing


text:
module Sing

%default total

data Fing : Type -> Type where
  StringFing : String -> Fing String
  BoolFing : Bool -> Fing Bool

stringFing : Fing String -> String
stringFing (StringFing s) = s

boolFing : Fing Bool -> Bool
boolFing (BoolFing b) = b


text:
module Test

public export
data Test : (f : a -> Type) -> Type where
  Check : { F : x -> Type } -> { t : x } -> ( value : F t) -> Test F

max_stars_repo_name: janschultecom/typelevel-seo

max_issues_repo_name: janschultecom/typelevel-seo

max_forks_repo_name: janschultecom/typelevel-seo


text:
module Circuits

-- Based on http://okmij.org/ftp/tagless-final/course2/

interface Sym where
  Repr : Type

  lit : Bool -> Repr
  neg : Repr -> Repr
  (&&) : Repr -> Repr -> Repr
  (||) : Repr -> Repr -> Repr

[boolSym] Sym where
  Repr = Bool

  lit x = x
  neg x = not x
  (&&) x y = x && y
  (||) x y = x || y

[strSym] Sym where
  Repr = String

  lit x = if x then "tt" else "ff"
  neg x = "~" ++ x
  (&&) x y = "(" ++ x ++ " && " ++ y ++ ")"
  (||) x y = "(" ++ x ++ " || " ++ y ++ ")"

namespace Ex
  interface NAND where
    Repr : Type

    lit : Bool -> Repr
    nand : Repr -> Repr -> Repr

[boolNAND] NAND where
  Repr = Bool

  lit x = x
  nand x y =  not (x && y)

[strNAND] NAND where
  Repr = String

  lit x = if x then "tt" else "ff"
  nand x y =  "(" ++ x ++ " ^^ " ++ y ++ ")"

[nandSym] NAND => Sym where
  Repr = Ex.Repr

  lit x = Ex.lit x
  neg x = nand x x
  (&&) x y = neg (nand x y)
  (||) x y = nand (neg x) (neg y)

ex : Sym => Repr
ex = lit True && (neg (lit False))

test : Bool
test = ex @{nandSym @{boolNAND}}

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Holes

int : Int
int = ?a

nat : Nat
nat = ?b

equal : cast Holes.int === Holes.nat
equal = ?c


text:
module TrieOfTrees

import FiniteMap

%default total
%access private

public export
data Tree a = E | T a (Tree a) (Tree a)

export
data Trie : (Type -> Type) -> Type -> Type -> Type where
  MkTrie : Maybe a -> mk (Trie mk ks (Trie mk ks a)) -> Trie mk ks a

export
FiniteMap m k => FiniteMap (Trie (m k)) (Tree k) where
  empty = assert_total $ MkTrie Nothing empty

  lookup E t = assert_total $ case t of
    MkTrie v m => v
  lookup (T k a b) t = assert_total $ case t of
    MkTrie v m => do
      m' <- lookup k m
      m'' <- lookup a m'
      lookup b m''

  bind E x t = assert_total $ case t of
    MkTrie v m => MkTrie (Just x) m
  bind (T k a b) x t = assert_total $ case t of
    MkTrie v m => let tt  = fromMaybe empty $ lookup k m
                      t   = fromMaybe empty $ lookup a tt
                      t'  = bind b x t
                      tt' = bind a t' tt
                  in MkTrie v (bind k tt' m)


text:
module Dart.FFI

import public Dart.FFI.Constructors
import public Dart.FFI.Enums
import public Dart.FFI.Upcast


text:
module Data.StringTrie

import Data.These
import Data.StringMap

%default total

-- prefix tree specialised to use `String`s as keys

public export
record StringTrie a where
  constructor MkStringTrie
  node : These a (StringMap (StringTrie a))

public export
Show a => Show (StringTrie a) where
  show (MkStringTrie node) = assert_total $ show node

public export
Functor StringTrie where
  map f (MkStringTrie node) = MkStringTrie $ assert_total $ bimap f (map (map f)) node

public export
empty : StringTrie a
empty = MkStringTrie $ That empty

public export
singleton : List String -> a -> StringTrie a
singleton []      v = MkStringTrie $ This v
singleton (k::ks) v = MkStringTrie $ That $ singleton k (singleton ks v)

-- insert using supplied function to resolve clashes
public export
insertWith : List String -> (Maybe a -> a) -> StringTrie a -> StringTrie a
insertWith []      f (MkStringTrie nd) =
  MkStringTrie $ these (This . f . Just) (Both (f Nothing)) (Both . f . Just) nd
insertWith (k::ks) f (MkStringTrie nd) =
  MkStringTrie $ these (\x => Both x (singleton k end)) (That . rec) (\x => Both x . rec) nd
  where
  end : StringTrie a
  end = singleton ks (f Nothing)
  rec : StringMap (StringTrie a) -> StringMap (StringTrie a)
  rec sm = maybe (insert k end sm) (\tm => insert k (insertWith ks f tm) sm) (lookup k sm)

public export
insert : List String -> a -> StringTrie a -> StringTrie a
insert ks v = insertWith ks (const v)

-- fold the trie in a depth-first fashion performing monadic actions on values, then keys
-- note that for `Both` the action on node values will be performed first because of `bitraverse` implementation
public export
foldWithKeysM : (Monad m, Monoid b) => (List String -> m b) -> (List String -> a -> m b) -> StringTrie a -> m b
foldWithKeysM {a} {m} {b} fk fv = go []
  where
  go : List String -> StringTrie a -> m b
  go ks (MkStringTrie nd) =
    bifold <$> bitraverse
                (fv ks)
                (\sm => foldlM
                          (\x, (k, vs) => do let ks' = ks++[k]
                                             y <- assert_total $ go ks' vs
                                             z <- fk ks'
                                             pure $ x <+> y <+> z)
                          neutral
                          (toList sm))
                nd


text:
module Libraries.Data.List1

import Data.List1

%default total

-- TODO: Remove this, once Data.List1.unsnoc from base is available
--       to the compiler

export
unsnoc : (xs : List1 a) -> (List a, a)
unsnoc (x ::: xs) = go x xs where

  go : (x : a) -> (xs : List a) -> (List a, a)
  go x [] = ([], x)
  go x (y :: ys) = let (ini,lst) = go y ys
                   in (x :: ini, lst)


text:
module Data.Prim.String

import public Data.DPair
import public Data.Prim.Ord

%default total

unsafeRefl : a === b
unsafeRefl = believe_me (Refl {x = a})

--------------------------------------------------------------------------------
--          (<)
--------------------------------------------------------------------------------

||| Witness that `m < n === True`.
export
data (<) : (m,n : String) -> Type where
  LT : {0 m,n : String} -> (0 prf : (m < n) === True) -> m < n

||| Contructor for `(<)`.
|||
||| This can only be used in an erased context.
export %hint
0 mkLT : (0 prf : (m < n) === True) -> m < n
mkLT = LT

||| Extractor for `(<)`.
|||
||| This can only be used in an erased context.
export
0 runLT : m < n -> (m < n) === True
runLT (LT prf) = prf

||| We don't trust values of type `(<)` too much,
||| so we use this when creating magical results.
export
strictLT : (0 p : m < n) -> Lazy c -> c
strictLT (LT prf) x = x

--------------------------------------------------------------------------------
--          Aliases
--------------------------------------------------------------------------------

||| Flipped version of `(<)`.
public export
0 (>) : (m,n : String) -> Type
m > n = n < m

||| `m <= n` mean that either `m < n` or `m === n` holds.
public export
0 (<=) : (m,n : String) -> Type
m <= n = Either (m < n) (m === n)

||| Flipped version of `(<=)`.
public export
0 (>=) : (m,n : String) -> Type
m >= n = n <= m

||| `m /= n` mean that either `m < n` or `m > n` holds.
public export
0 (/=) : (m,n : String) -> Type
m /= n = Either (m < n) (m > n)

--------------------------------------------------------------------------------
--          Order
--------------------------------------------------------------------------------

0 ltNotEQ : m < n -> Not (m === n)
ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")

0 ltNotGT : m < n -> Not (n < m)
ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")

0 eqNotLT : m === n -> Not (m < n)
eqNotLT = flip ltNotEQ

export
comp : (m,n : String) -> Trichotomy (<) m n
comp m n = case prim__lt_String m n of
  0 => case prim__eq_String m n of
    0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
    x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)

export
Total String (<) where
  trichotomy   = comp
  transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl

--------------------------------------------------------------------------------
--          Bounds and Well-Foundedness
--------------------------------------------------------------------------------

||| Lower bound of `String`
public export
MinString : String
MinString = ""

||| `m >= MinString` for all `m` of type `String`.
export
0 GTE_MinString : (m : String) -> m >= MinString
GTE_MinString m = case comp MinString m of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total $ idris_crash #"IMPOSSIBLE: String smaller than """#

||| Not value of type `String` is less than `MinString`.
export
0 Not_LT_MinString : m < MinString -> Void
Not_LT_MinString = GTE_not_LT (GTE_MinString m)


text:
-- Exercises_4_1.idr
--
-- Exercises for generic types

import Tree
import Shape
import Picture

||| Converts given List to a binary Tree
listToTree : Ord elem => List elem -> Tree elem
listToTree [] = Empty
listToTree (x :: xs) = insert x (listToTree xs)

||| Converts given Tree to an ordered List
treeToList : Tree a -> List a
treeToList Empty = []
treeToList (Node left x right) = let leftList = treeToList left
                                     rightList = treeToList right in
                                     leftList ++ [x] ++ rightList

-- Integer arithmetic
-- ==================

||| Data type for arithmetic expression(s)
data Expr = ||| Int value
            Val Int
          | ||| Arithmetic addition of two expressions
            Add Expr Expr
          | ||| Arithmetic substraction of two expressions
            Sub Expr Expr
          | ||| Arithmetic multiplication of two expressions
            Mult Expr Expr

||| Evaluates given arithmentic expression
evaluate : Expr -> Int
evaluate (Val x) = x
evaluate (Add x y) = (evaluate x) + (evaluate y)
evaluate (Sub x y) = (evaluate x) - (evaluate y)
evaluate (Mult x y) = (evaluate x) * (evaluate y)

-- Maybe comparator
-- ================
maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing Nothing = Nothing
maxMaybe Nothing (Just y) = Just y
maxMaybe (Just x) Nothing = Just x
maxMaybe (Just x) (Just y) = case compare x y of
                                  LT => Just y
                                  EQ => Just x
                                  GT => Just x

-- Biggest triangle of picture
-- ===========================
biggestTriangle : Picture -> Maybe Double
biggestTriangle (Primitive triangle@(Triangle _ _)) = Just (area triangle)
biggestTriangle (Primitive _) = Nothing
biggestTriangle (Combine pic pic1) = maxMaybe (biggestTriangle pic) (biggestTriangle pic1)
biggestTriangle (Rotate x pic) = biggestTriangle pic
biggestTriangle (Translate x y pic) = biggestTriangle pic

testPic1 : Picture
testPic1 = Combine (Primitive (Triangle 2 3))
                   (Primitive (Triangle 2 4))
testPic2 : Picture
testPic2 = Combine (Primitive (Rectangle 1 3))
                   (Primitive (Circle 4))

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Pred

import Data.Vect

maryInVector : Elem "Prat" ["Peter", "Paul", "Prat"]
maryInVector = There $ There Here

export
removeElem : (value : a) ->
             (xs : Vect (S n) a) ->
             (prf : Elem value xs) ->
             Vect n a
removeElem value (value :: ys) Here = ys
removeElem {n = Z} value (y :: []) (There later) = absurd later
removeElem {n = (S k)} value (y :: ys) (There later) = y :: removeElem value ys later

-- absurd : Uninhabited t => t -> a

removeElem_auto : (value : a) ->
             (xs : Vect (S n) a) ->
             {auto prf : Elem value xs} ->
             Vect n a
removeElem_auto value xs {prf} = removeElem value xs prf

-- data Elem : a -> Vect k a -> Type where
--      Here : Elem x (x :: xs)
--      There : (later : Elem x xs) -> Elem x (y :: xs)

not_in_nil : Elem value [] -> Void
not_in_nil Here impossible
not_in_nil (There _) impossible

not_in_tail : (notThere : Elem value xs -> Void) ->
              (notHere : (value = x) -> Void) ->
              Elem value (x :: xs) -> Void
not_in_tail notThere notHere Here = notHere Refl
not_in_tail notThere notHere (There later) = notThere later

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = No not_in_nil
isElem value (x :: xs) = case decEq value x of
                              Yes Refl => Yes Here
                              No notHere => case Pred.isElem value xs of
                                                 Yes prf => Yes (There prf)
                                                 No notThere => No (not_in_tail notThere notHere)


text:
module Minecraft.Base.PreClassic.Dirt.Item

import public Minecraft.Base.PreClassic.Dirt
import public Minecraft.Core.Item.Export
import public Minecraft.Core.Item.Put.Export
import public Minecraft.Data.Type.Vtbl

%default total

namespace Export
  public export %hint dirtItem : Item Dirt.Item
  public export %hint putDirt  : Put  Dirt.Item
  public export %hint dirtVtbl : Vtbl Dirt.Item

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
data Matter = Solid | Liquid | Gas

Eq Matter where
  (==) Solid Solid = True
  (==) Liquid Liquid = True
  (==) Gas Gas = True
  (==) _ _ = False

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

Eq elem => Eq (Tree elem) where
  (==) Empty Empty = True
  (==) (Node x y z) (Node w s t) = x == w && y == s && z == t
  (==) _ _ = False

record Album where
  constructor MkAlbum
  artist : String
  name : String
  year : Integer

Eq Album where
  (==) (MkAlbum artist name year) (MkAlbum artist' name' year') =
          artist == artist' && name == name' && year == year'

Ord Album where
  compare (MkAlbum artist name year) (MkAlbum artist' name' year') =
    case compare artist artist' of
         EQ => (case compare year year' of
                     EQ => compare name name
                     different => different)
         different => different

data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

Eq Shape where
  (==) (Triangle x y) (Triangle z w) = x == z && y == w
  (==) (Rectangle x y) (Rectangle z w) = x == z && y == w
  (==) (Circle x) (Circle y) = x == y
  (==) _ _ = False

area : Shape -> Double
area (Triangle x y) = x * y / 2
area (Rectangle x y) = x * y
area (Circle x) = x * pi * pi

Ord Shape where
  compare shape1 shape2  = compare (area shape1) (area shape2)

testShapes : List Shape
testShapes = [Circle 3, Triangle 3 9, Rectangle 2 6, Circle 4, Rectangle 2 7]

data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

eval : (Abs num, Neg num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x)  = abs (eval x)

Num ty => Num (Expr ty) where
  (+) = Add
  (*) = Mul
  fromInteger = Val . fromInteger

Num ty => Neg (Expr ty) where
  negate x = 0 - x
  (-) = Sub

Abs ty => Abs (Expr ty) where
  abs = Abs

parens : String -> String
parens s = "(" ++ s ++ ")"

Show ty => Show (Expr ty) where
  show (Val x) = show x
  show (Add x y) = parens $ show x ++ " + " ++ show y
  show (Sub x y) = parens $ show x ++ " - " ++ show y
  show (Mul x y) = parens $ show x ++ " * " ++ show y
  show (Div x y) = parens $ show x ++ " / " ++ show y
  show (Abs x) = "|" ++ show x ++ "|"

(Eq ty, Abs ty, Neg ty, Integral ty) => Eq (Expr ty) where
  (==) expr1 expr2 = (eval expr1) == (eval expr2)

(Abs num, Neg num, Integral num) => Cast (Expr num) num where
  cast e = eval e

Functor Tree where
  map f Empty = Empty
  map f (Node left val right) = Node (map f left) (f val) (map f right)

foldLength : List String -> Nat
foldLength = sum . map length
-- foldLength xs = foldl (\n, str => n + length str) 0 xs

Foldable Tree where
  foldr f initialVal Empty = initialVal
  foldr f initialVal (Node left val right) = f val $ foldr f (foldr f initialVal left) right

Functor Expr where
  map f (Val x) = Val (f x)
  map f (Add x y) = Add (map f x) (map f y)
  map f (Sub x y) = Sub (map f x) (map f y)
  map f (Mul x y) = Mul (map f x) (map f y)
  map f (Div x y) = Div (map f x) (map f y)
  map f (Abs x) = Abs (map f x)

data Vect : Nat -> Type -> Type where
  Nil : Vect 0 a
  (::) : a -> Vect n a -> Vect (S n) a

Eq a => Eq (Vect n a) where
  [] == [] = True
  (x :: xs) == (y :: ys) = x == y && xs == ys

Foldable (Vect n) where
  foldr f initialVal [] = initialVal
  foldr f initialVal (x :: y) = f x (foldr f initialVal y)


text:
module Main
import Lib
import Prelude.List as lst
import Data.List

dataset : List String
dataset = [ "The future king is the prince",
--           "Daughter is the princess.",
--           "Son is the prince.",
--           "Only a man can be a king",
--           "Only a woman can be a queen",
--           "The princess will be a queen",
--           "Queen and king rule the realm",
--           "The prince is a strong man",
--           "The princess is a beautiful woman",
--           "The royal family is the king and queen and their children",
--           "Prince is only a boy now",
           "A boy will be a man"]

index : String -> List (String, Nat) ->  Nat
index x dict = (\(Just i) => i ) $ lookup x dict

get_indices : List String -> List (String,Nat) -> List Nat
get_indices vocabs dict = foldr (\x, acc => (index x  dict)::acc) [] vocabs

zeros : List String -> List (String, Nat) -> List Double
zeros vocabs dict = replicate ( lst.length $ get_indices vocabs dict ) 0

cleaned : List String
cleaned = rawToCleaned dataset

paired : List (String, String)
paired = makeWordPairs cleaned

dict : List (String,Nat)
dict = createDictionary cleaned

input : List String
input = xss paired

target : List String
target = yss paired

zs : List Double
zs = zeros cleaned dict

ran_wht : List Double
ran_wht = replicate (length $ get_indices input dict) 0.06

xss_index : List Nat
xss_index = get_indices input dict

yss_index : List Nat
yss_index = get_indices target dict

weights : List (List Double)
weights = matrix_gen ran_wht zs

en_inputs : List (List Double)
en_inputs = oneHotEncoder xss_index zs

en_targets : List  (List Double)
en_targets = oneHotEncoder yss_index zs

bias : Double
bias = 0.3

-- TODO insertAt inserts extra zeros
main : IO ()
main = let classifier = model weights en_inputs en_targets 0.001 0.9 0.999 0.00000001 2
       in print $ classifier

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Main

import Js.Dom
import public Js.ASync
import Control.ST
import Js.HtmlStyle
import Data.AVL.Set

data Input
  = Tick
  | KeyDown String
  | KeyUp String

record Model where
  constructor MkModel
  scroll : List String
  n : Int
  keymap : Set String
  hero : (Double, Double)

emptyModel : Model
emptyModel =
  MkModel
    ["ola"]
    0
    Data.AVL.Set.empty
    (320,240)

add_scroll : String -> Model -> Model
add_scroll s model =
  let
    lines = scroll model
  in
  set_scroll (s :: lines) model

record Circle where
  constructor MkCircle
  center_x : Double
  center_y : Double
  radius : Double
  color : String

Gui : Dom m => Type
Gui {m} = DomRef {m} () (const Model) (const Input) ()

interface Drawable a where
  draw : a -> Html Input

implementation Drawable Circle where
  draw c =
    div
      [ style
          [ position (Fixed (center_x c) (center_y c))
          , width (2.0 * (radius c))
          , height (2.0 * (radius c))
          , backgroundColor (color c)
          ]
      ] []

drawables : Model -> List (Html Input)
drawables model =
  let
    (hx,hy) = hero model
  in
  [ draw (MkCircle hx hy 5.0 "red") ]

vw : () -> Model -> Html Input
vw () inp =
  div
    [ style
        [ position (Fixed 0 0)
        , width 640
        , height 480
        ]
    , onkeydown (\k => KeyDown (key k))
    , onkeyup (\k => KeyUp (key k))
    , tabindex 0
    ]
    ([ div [] (map (\t => div [] [text t]) (scroll inp))
     ] ++ (drawables inp)
    )

handleKeys : Model -> Model
handleKeys model =
  let
    (hx,hy) = hero model
    km = keymap model
  in
  if Data.AVL.Set.contains "a" km then
    set_hero (hx - 3, hy) model
  else if Data.AVL.Set.contains "s" km then
    set_hero (hx, hy + 3) model
  else if Data.AVL.Set.contains "d" km then
    set_hero (hx + 3, hy) model
  else if Data.AVL.Set.contains "w" km then
    set_hero (hx, hy - 3) model
  else
    model

handleInput : Dom m => (d: Var) -> (s: Var) -> Input -> ST m () [s:::State Model, d:::Gui {m}]
handleInput d s x =
  case x of
    KeyDown k =>
      do
        inp <- read s
        let km = keymap inp
        write s (add_scroll ("down " ++ k) (set_keymap (Data.AVL.Set.insert k km) inp))

    KeyUp k =>
      do
        inp <- read s
        let km = keymap inp
        let turnoff = Data.AVL.Set.fromList [ k ]
        write s (add_scroll ("up " ++ k) (set_keymap (Data.AVL.Set.difference km turnoff) inp))

    Tick =>
      do
        inp <- read s
        write s (handleKeys (set_n ((n inp) + 1) inp))
        call $ schedule d 30 Tick
        call $ domPut d inp

pageLoop : Dom m => (d: Var) -> (s:Var) -> ST m () [s:::State Model, d:::Gui {m}]
pageLoop d s =
  do
    x <- call $ getInput d

    handleInput d s x

    pageLoop d s

pageStart : Dom m => (d: Var) -> (s:Var) -> ST m () [s:::State Model, d:::Gui {m}]
pageStart d s =
  do
    call $ schedule d 30 Tick
    pageLoop d s

page : Dom m => ST m () []
page =
  do
    let model = emptyModel
    dom <- initBody [] vw () model
    txt <- new model
    pageStart dom txt
    delete txt
    clearDom dom

main : JS_IO ()
main = setASync_ $ run page

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: rbarreiro/idrisjs

max_forks_repo_name: rbarreiro/idrisjs


text:
module Idris.Doc.HTML

import Core.Context
import Core.Core
import Core.Directory

import Data.String

import Parser.Lexer.Source

import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Render.HTML
import Libraries.Text.PrettyPrint.Prettyprinter.SimpleDocTree

import Idris.Doc.String
import Idris.Package.Types
import Idris.Pretty
import Idris.Version

%default covering

getNS : Name -> String
getNS (NS ns _) = show ns
getNS _ = ""

hasNS : Name -> Bool
hasNS (NS _ _) = True
hasNS _ = False

tryCanonicalName : {auto c : Ref Ctxt Defs} ->
                FC -> Name -> Core (Maybe Name)
tryCanonicalName fc n with (hasNS n)
  tryCanonicalName fc n | True
      = do defs <- get Ctxt
           case !(lookupCtxtName n (gamma defs)) of
                [(n, _, _)] => pure $ Just n
                _ => pure Nothing
  tryCanonicalName fc n | False = pure Nothing

packageInternal : {auto c : Ref Ctxt Defs} ->
                  Name -> Core Bool
packageInternal (NS ns _) =
  do let mi = nsAsModuleIdent ns
     catch ((const True) <$> nsToSource emptyFC mi) (\_ => pure False)
packageInternal _ = pure False

addLink : {auto c : Ref Ctxt Defs} ->
          Maybe Name -> String -> Core String
addLink Nothing rest = pure rest
addLink (Just n) rest = do
  Just cName <- tryCanonicalName emptyFC n
    | Nothing => pure $ "" <+> rest <+> ""
  True <- packageInternal cName
    | False => pure $ fastConcat
                    [ ""
                    , rest
                    , ""
                    ]
  pure $ fastConcat
       [ ""
       , rest
       , ""
       ]

renderHtml : {auto c : Ref Ctxt Defs} ->
             SimpleDocTree IdrisDocAnn ->
             Core String
renderHtml STEmpty = pure neutral
renderHtml (STChar ' ') = pure " "
renderHtml (STChar c) = pure $ cast c
renderHtml (STText _ text) = pure $ htmlEscape text
renderHtml (STLine _) = pure "
"
renderHtml (STAnn Declarations rest)
  = pure $ "
" <+> !(renderHtml rest) <+> "
"
renderHtml (STAnn (Decl n) rest) = pure $ "
" <+> !(renderHtml rest) <+> "
"
renderHtml (STAnn DocStringBody rest)
  = pure $ "
" <+> !(renderHtml rest) <+> "
"
renderHtml (STAnn UserDocString rest)
  = pure $ "
" <+> !(renderHtml rest) <+> "
"
renderHtml (STAnn (Syntax (DCon mn)) rest) = do
  dcon <- renderHtml rest
  addLink mn $ "" <+> dcon <+> ""
renderHtml (STAnn (Syntax (TCon mn)) rest) = do
  tcon <- renderHtml rest
  addLink mn $ "" <+> tcon <+> ""
renderHtml (STAnn (Syntax (Fun n)) rest) = do
  fun <- renderHtml rest
  addLink (Just n) $ "" <+> fun <+> ""
renderHtml (STAnn Header rest) = do
  resthtml <- renderHtml rest
  pure $ "" <+> resthtml <+> ""
renderHtml (STAnn ann rest) = do
  resthtml <- renderHtml rest
  pure $ "" ++ resthtml ++ ""
renderHtml (STConcat docs) = pure $ fastConcat !(traverse renderHtml docs)

removeNewlinesFromDeclarations : SimpleDocTree IdrisDocAnn -> SimpleDocTree IdrisDocAnn
removeNewlinesFromDeclarations = go False
  where
    go : Bool -> SimpleDocTree IdrisDocAnn -> SimpleDocTree IdrisDocAnn
    go False l@(STLine i) = l
    go True l@(STLine i) = STEmpty
    go ignoring (STConcat docs) = STConcat $ map (go ignoring) docs
    go _ (STAnn Declarations rest) = STAnn Declarations $ go True rest
    go _ (STAnn ann rest) = STAnn ann $ go False rest
    go _ doc = doc

docDocToHtml : {auto c : Ref Ctxt Defs} ->
               Doc IdrisDocAnn ->
               Core String
docDocToHtml doc =
  let dt = SimpleDocTree.fromStream $ layoutUnbounded doc in
      renderHtml $ removeNewlinesFromDeclarations dt

htmlPreamble : String -> String -> String -> String
htmlPreamble title root class =
  let title       = htmlEscape title in
  let cssID       = "preferredStyle" in
  let cssSelectID = "selectPreferredStyle" in
  let cssDefault  = "default" in
  let cssLocalKey = "stylefile" in
  """
  <!DOCTYPE html>

    <meta charset="utf-8">
    <title>\{title}</title>
    <link rel="stylesheet" type="text/css" id="\{cssID}" href="\{root}\{cssDefault}.css">

    Idris2Doc : \{title}
    Index

    <select id="\{cssSelectID}">
      \{String.unlines $ flip map cssFiles $ \ css =>
         #"<option value="\#{css.filename}">\#{css.stylename}</option>"#
      }
    </select>

  """

htmlFooter : String
htmlFooter = "
Produced by Idris 2 version " ++ (showVersion True version) ++ ""

export
renderDocIndex : PkgDesc -> String
renderDocIndex pkg = fastConcat $
  [ htmlPreamble (name pkg) "" "index"
  , "
Package ", name pkg, " - Namespaces
"
  , "
"] ++
  (map moduleLink $ modules pkg) ++
  [ "
"
  , htmlFooter
  ]
    where
      moduleLink : (ModuleIdent, String) -> String
      moduleLink (mod, filename) =
         "
" ++ (show mod) ++ "
"

preserveLayout : String -> String
preserveLayout d = "
" ++ d ++ "
"

export
renderModuleDoc : {auto c : Ref Ctxt Defs} ->
                  ModuleIdent ->
                  Maybe String ->
                  Doc IdrisDocAnn ->
                  Core String
renderModuleDoc mod modDoc allModuleDocs =
  let mdoc = maybe "" (preserveLayout . htmlEscape) modDoc
  in pure $ fastConcat
  [ htmlPreamble (show mod) "../" "namespace"
  , "
"
  , "
", show mod, "
"
  , mdoc
  , "
"
  , !(docDocToHtml allModuleDocs)
  , htmlFooter
  ]


text:
module Mrk.Languages

%default total
%access public export

data Language
  = English
%name Language lang

Show Language where
  show x = case x of
                English => "en"

Eq Language where
  (==) x y = show x == show y

max_stars_repo_name: camelpunch/mrk

max_issues_repo_name: camelpunch/mrk

max_forks_repo_name: camelpunch/mrk


text:
module Sub11LTE36t21

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total

-- 6(6t+3)+3 --B[1,-2]--> 6t+3
export
lte36t21 : (k : Nat) -> LTE (S k) (S (S (S (plus (plus (plus k k) (plus k k)) (plus k k)))))
lte36t21 Z     = (lteSuccRight . LTESucc) LTEZero
lte36t21 (S k) =
  let lemma = lte36t21 k in
  rewrite (sym (plusSuccRightSucc k k)) in
  rewrite (sym (plusSuccRightSucc (plus k k) (S (plus k k)))) in
  rewrite (sym (plusSuccRightSucc (plus k k) (plus k k))) in
  rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (S (plus k k)))) in
  rewrite (sym (plusSuccRightSucc (plus (plus k k) (plus k k)) (plus k k))) in
    (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc) lemma


text:
module Lexer

import Lightyear
import Lightyear.Char
import Lightyear.Strings

public export
data Lexeme
  = INT Integer
  | TINT
  | TBOOL
  | TRUE
  | FALSE
  | FUN
  | IS
  | IF
  | THEN
  | ELSE
  | LET
  | SEMICOLON2
  | EQUAL
  | LESS
  | TARROW
  | COLON
  | LPAREN
  | RPAREN
  | PLUS
  | MINUS
  | TIMES
  | VAR String

-- XXX: deriving Eq?
export
implementation Eq Lexeme where
  (INT i1) == (INT i2) = i1 == i2
  TINT == TINT = True
  TBOOL == TBOOL = True
  TRUE == TRUE = True
  FALSE == FALSE = True
  FUN == FUN = True
  IS == IS = True
  IF == IF = True
  THEN == THEN = True
  ELSE == ELSE = True
  LET == LET = True
  SEMICOLON2 == SEMICOLON2 = True
  EQUAL == EQUAL = True
  LESS == LESS = True
  TARROW == TARROW = True
  COLON == COLON = True
  LPAREN == LPAREN = True
  RPAREN == RPAREN = True
  PLUS == PLUS = True
  MINUS == MINUS = True
  TIMES == TIMES = True
  (VAR nm1) == (VAR nm2) = nm1 == nm2
  _ == _ = False

-- XXX: deriving Show?
export
implementation Show Lexeme where
  show _ = "<lexeme>"

getInteger : List (Fin 10) -> Integer
getInteger = foldl (\a => \b => 10 * a + cast b) 0

int : Parser Lexeme
int = do
  digits <- some digit
  pure $ INT (getInteger digits)

kw : String -> Lexeme
kw "int" = TINT
kw "bool" = TBOOL
kw "true" = TRUE
kw "false" = FALSE
kw "fun" = FUN
kw "is" = IS
kw "if" = IF
kw "then" = THEN
kw "else" = ELSE
kw "let" = LET
kw nm = VAR nm

varKw : Parser Lexeme
varKw = do
  nm <- some letter
  pure $ kw (pack nm)

tok : Parser Lexeme
tok = int
  <|> varKw
  <|> (string ";;" *> pure SEMICOLON2)
  <|> (string "=" *> pure EQUAL)
  <|> (string "<" *> pure LESS)
  <|> (string "->" *> pure TARROW)
  <|> (string ":" *> pure COLON)
  <|> (string "(" *> pure LPAREN)
  <|> (string ")" *> pure RPAREN)
  <|> (string "+" *> pure PLUS)
  <|> (string "-" *> pure MINUS)
  <|> (string "×" *> pure TIMES)
  <|> (string "*" *> pure TIMES)

export
lexer : Parser (List Lexeme)
lexer = spaces *> (many (tok <* spaces))

max_stars_repo_name: steshaw/idris-miniml

max_issues_repo_name: steshaw/idris-miniml

max_forks_repo_name: steshaw/idris-miniml


text:
module Toolkit.Data.List.Filter

import Toolkit.Data.DList
import Toolkit.Data.List.Interleaving

%default total

public export
data Filter : (holdsFor : type -> Type)
           -> (input : List type)
           -> Type
  where
    MkFilter : {thrown : List type}
            -> (kept : List type)
            -> (prfOrdering : Interleaving kept thrown input)
            -> (prfKept     : DList type holdsFor kept)
            -> (prfThrown   : DList type (Not . holdsFor) thrown)
            -> Filter holdsFor input

export
filter : (test   : (value : type) -> Dec (holds value))
      -> (input  : List type)
      -> Filter holds input
filter test [] = MkFilter [] Empty [] []
filter test (x :: xs) with (filter test xs)
  filter test (x :: xs) | (MkFilter kept prfOrdering prfKept prfThrown) with (test x)
    filter test (x :: xs) | (MkFilter kept prfOrdering prfKept prfThrown) | (Yes prf)
      = MkFilter (x::kept) (Left x prfOrdering) (prf :: prfKept) prfThrown
    filter test (x :: xs) | (MkFilter kept prfOrdering prfKept prfThrown) | (No contra)
      = MkFilter kept (Right x prfOrdering) prfKept (contra :: prfThrown)

export
extract : Filter p xs
       -> (ks ** DList type p ks)
extract (MkFilter kept prfOrdering prfKept prfThrown)
  = (kept ** prfKept)

-- [ EOF ]


text:
module ElemType

data Vect : Nat -> (ty : Type) -> Type where
     Nil : Vect Z ty
     (::) : ty -> Vect n ty -> Vect (S n) ty

data Elem : a -> Vect k a -> Type where
     Here : Elem x (x :: xs)
     There : (later : Elem x xs) -> Elem x (y :: xs)

notInNil : Elem value [] -> Void
notInNil Here impossible
notInNil (There _) impossible

notInTail : (notHere : (value = x) -> Void) -> (notThere : Elem value y -> Void) -> Elem value (x :: y) -> Void
notInTail notHere notThere Here = notHere Refl
notInTail notHere notThere (There later) = notThere later

isElem : DecEq a => (value : a) -> (xs : Vect n a) -> Dec (Elem value xs)
isElem value [] = No notInNil
isElem value (x :: y) = case decEq value x of
                             (Yes Refl) => Yes Here
                             (No notHere) => case isElem value y of
                                                 (Yes prf) => Yes (There prf)
                                                 (No notThere) => No (notInTail notHere notThere)

-- Exercise 9.1 # 1
data LElem : a -> List a -> Type where
     LHere : LElem x (x :: xs)
     LThere : (later : LElem x xs) -> LElem x (y :: xs)

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

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

isNotLast : (contra : Last xs value -> Void) -> (notFinalprf : (xs = []) -> Void) -> Last (x :: xs) value -> Void
isNotLast contra notFinalprf LastOne = notFinalprf Refl
isNotLast contra notFinalprf (LastCons prf) = contra prf

isLastLemma : (eqValPrf : x = value) -> (finalValPrf : xs = []) -> Last (x :: xs) value
isLastLemma Refl Refl = LastOne

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] value = No isLastNil
isLast (x :: xs) value = case decEq xs [] of
                              (Yes finalValPrf) => case decEq x value of
                                                (Yes eqValPrf) => Yes (isLastLemma eqValPrf finalValPrf)
                                                -- Or:
                                                -- (Yes eqValPrf) => Yes (rewrite eqValPrf in rewrite finalValPrf in LastOne)
                                                (No contra) => ?adfasfasd_3
                              (No notFinalprf) => case isLast xs value of
                                            (Yes prf) => Yes (LastCons prf)
                                            (No contra) => No (isNotLast contra notFinalprf)


text:
module Control.Optics.Getter

import public Control.Optics.Types

export
view : Getting a s a -> s -> a
view l = runConst . applyMor (l (Mor MkConst))

infixl 8 ^.
export
(^.) : s -> Getting a s a -> a
s ^. l = view l s

export
to : (Profunctor p, Contravariant f) => (s -> a) -> Simple (Optic p f) s a
to k = dimap k (contramap k)


text:
module WordLength

import Data.Vect

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

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

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

suc : Nat
suc = S 5


text:
module Specifications.Group

import public Specifications.Monoid

%default total
%access public export

infixl 8 #

||| specification
isInverseL : Binop s -> s -> (s -> s) -> Type
isInverseL (#) e inv = (x : _) -> inv x # x = e

||| specification
isInverseR : Binop s -> s -> (s -> s) -> Type
isInverseR (#) e inv = (x : _) -> x # inv x = e

||| composed specification
data GroupSpec : Binop s -> s -> (s -> s) -> Type where
  MkGroup : MonoidSpec op e -> isInverseL op e inv -> isInverseR op e inv ->
    GroupSpec op e inv

||| forget
monoid : GroupSpec op e _ -> MonoidSpec op e
monoid (MkGroup m _ _) = m

||| forget
inverseL : GroupSpec op e inv -> isInverseL op e inv
inverseL (MkGroup _ l _) = l

||| forget
inverseR : GroupSpec op e inv -> isInverseR op e inv
inverseR (MkGroup _ _ r) = r

||| composed specification
data AbelianGroupSpec : Binop s -> s -> (s -> s) -> Type where
  MkAbelianGroup : GroupSpec op e inv -> isAbelian op ->
    AbelianGroupSpec op e inv

||| forget
group : AbelianGroupSpec op e inv -> GroupSpec op e inv
group (MkAbelianGroup g _) = g

||| forget
abelian : AbelianGroupSpec op _ _ -> isAbelian op
abelian (MkAbelianGroup _ a) = a

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
import Language.Reflection
import DerivingEq

%language ElabReflection

-- This tree doesn't work

data TreeTwo a = BranchTwo (TreeTwo a) a (TreeTwo a)
               | Leaf

Eq a => Eq (TreeTwo a) where
  (==) = %runElab genEq `{ TreeTwo }


text:
-- --------------------------------------------------------- [ Categorical.idr ]

module Data.ML.Categorical

import public Data.ML.Util

%access export

catToNum : (Num n, Cast Bool n, Ord a) => List a -> List (List n)
catToNum xs = [ cast . (== cat) <$> xs | cat <- unique xs ]

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

max_stars_repo_name: yurrriq/real-world-machine-learning

max_issues_repo_name: yurrriq/real-world-machine-learning

max_forks_repo_name: yurrriq/real-world-machine-learning


text:
module Main

-- https://github.com/idris-lang/Idris-dev/issues/2844
main_2844 : IO ()
main_2844 =
  let
    f =
      the
        ((String,String) -> String -> (String, Maybe String ))
        (\(_,s),y => (s, Just s))
  in
    case snd $ f ("tst","tst2") "cenas" of
      Just z => putStr z

-- https://github.com/idris-lang/Idris-dev/issues/2493
main_2493 : IO ()
main_2493 = printLn $ doThing [1,2,3] [("as",1),("asasasas",4)]
  where
    doThing : List Nat -> List (v,Nat) -> List v
    doThing is g = foldr (\(v,i),res => if elem i is then v::res else res) List.Nil g

main : IO ()
main = main_2844 *> main_2493


text:
module Rapid.Driver

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

import Compiler.Common
import Compiler.VMCode
import Core.Directory
import Core.CompileExpr
import Core.Name
import Libraries.Utils.Path

import Compiler.GenLLVMIR
import Compiler.PrepareCode

export
writeIR : (functions : List (Name, VMDef)) -> (foreigns : List (Name, NamedDef)) ->
          (support : String) -> (outfile : String) -> (debug : Bool) -> IO ()
writeIR functions foreigns support outfile debug = do
  let foreignCode = map (compileForeign debug) (enumerate foreigns)
  let nameMap = getNameMap $ map snd functions
  let indexedFuncs = enumerate functions
  let fcount = length indexedFuncs
  ignore $ fPutStrLn stderr $ "functions to compile: " ++ show (length indexedFuncs)
  (Right outFile) <- openFile outfile WriteTruncate
  | Left err => putStrLn $ "error opening output file: " ++ show err
  ignore $ fPutStr outFile support
  ignore $ fPutStr outFile closureHelper
  ignore $ fPutStr outFile $ fastAppend foreignCode

  for_ indexedFuncs (\c => do
    -- This dummy IO forces the `getVMIR` calls to wait until it's "their turn",
    -- otherwise we get huge memory spikes.
    ignore $ fPutStr stderr ""
    let i = 1 + fst c
    when (i `mod` 100 == 0) $ ignore $ fPutStrLn stderr ("compile fun " ++ show i ++ "/" ++ (show fcount) ++ ": " ++ safeName (fst (snd c)))
    let funcIr = getVMIR debug nameMap c
    fPutStr outFile funcIr
    )
  closeFile outFile

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid