text:
module Compiler.ANF

import Compiler.LambdaLift

import Core.CompileExpr
import Core.Context
import Core.Core
import Core.TT

import Data.List
import Data.Vect

%default covering

-- Convert the lambda lifted form to ANF, with variable names made explicit.
-- i.e. turn intermediate expressions into let bindings. Every argument is
-- a variable as a result.

mutual
  public export
  data AVar : Type where
       ALocal : Int -> AVar
       ANull : AVar

  public export
  data ANF : Type where
    AV : FC -> AVar -> ANF
    AAppName : FC -> (lazy : Maybe LazyReason) -> Name -> List AVar -> ANF
    AUnderApp : FC -> Name -> (missing : Nat) -> (args : List AVar) -> ANF
    AApp : FC -> (lazy : Maybe LazyReason) -> (closure : AVar) -> (arg : AVar) -> ANF
    ALet : FC -> (var : Int) -> ANF -> ANF -> ANF
    ACon : FC -> Name -> ConInfo -> (tag : Maybe Int) -> List AVar -> ANF
    AOp : {0 arity : Nat} -> FC -> (lazy : Maybe LazyReason) -> PrimFn arity -> Vect arity AVar -> ANF
        -- ^ we explicitly bind arity here to silence the warning that it shadows
        --   existing functions called arity.
    AExtPrim : FC -> (lazy : Maybe LazyReason) -> Name -> List AVar -> ANF
    AConCase : FC -> AVar -> List AConAlt -> Maybe ANF -> ANF
    AConstCase : FC -> AVar -> List AConstAlt -> Maybe ANF -> ANF
    APrimVal : FC -> Constant -> ANF
    AErased : FC -> ANF
    ACrash : FC -> String -> ANF

  public export
  data AConAlt : Type where
       MkAConAlt : Name -> ConInfo -> (tag : Maybe Int) -> (args : List Int) ->
                   ANF -> AConAlt

  public export
  data AConstAlt : Type where
       MkAConstAlt : Constant -> ANF -> AConstAlt

public export
data ANFDef : Type where
     MkAFun : (args : List Int) -> ANF -> ANFDef
     MkACon : (tag : Maybe Int) -> (arity : Nat) -> (nt : Maybe Nat) -> ANFDef
     MkAForeign : (ccs : List String) -> (fargs : List CFType) ->
                  CFType -> ANFDef
     MkAError : ANF -> ANFDef

showLazy : Maybe LazyReason -> String
showLazy = maybe "" $ (" " ++) . show

mutual
  export
  Show AVar where
    show (ALocal i) = "v" ++ show i
    show ANull = "[__]"

  export
  Show ANF where
    show (AV _ v) = show v
    show (AAppName fc lazy n args)
        = show n ++ showLazy lazy ++ "(" ++ showSep ", " (map show args) ++ ")"
    show (AUnderApp fc n m args)
        = "<" ++ show n ++ " underapp " ++ show m ++ ">(" ++
          showSep ", " (map show args) ++ ")"
    show (AApp fc lazy c arg)
        = show c ++ showLazy lazy ++ " @ (" ++ show arg ++ ")"
    show (ALet fc x val sc)
        = "%let v" ++ show x ++ " = (" ++ show val ++ ") in (" ++ show sc ++ ")"
    show (ACon fc n _ t args)
        = "%con " ++ show n ++ "(" ++ showSep ", " (map show args) ++ ")"
    show (AOp fc lazy op args)
        = "%op " ++ show op ++ showLazy lazy ++ "(" ++ showSep ", " (toList (map show args)) ++ ")"
    show (AExtPrim fc lazy p args)
        = "%extprim " ++ show p ++ showLazy lazy ++ "(" ++ showSep ", " (map show args) ++ ")"
    show (AConCase fc sc alts def)
        = "%case " ++ show sc ++ " of { "
             ++ showSep "| " (map show alts) ++ " " ++ show def ++ " }"
    show (AConstCase fc sc alts def)
        = "%case " ++ show sc ++ " of { "
             ++ showSep "| " (map show alts) ++ " " ++ show def ++ " }"
    show (APrimVal _ x) = show x
    show (AErased _) = "___"
    show (ACrash _ x) = "%CRASH(" ++ show x ++ ")"

  export
  Show AConAlt where
    show (MkAConAlt n _ t args sc)
        = "%conalt " ++ show n ++
             "(" ++ showSep ", " (map showArg args) ++ ") => " ++ show sc
      where
        showArg : Int -> String
        showArg i = "v" ++ show i

  export
  Show AConstAlt where
    show (MkAConstAlt c sc)
        = "%constalt(" ++ show c ++ ") => " ++ show sc

export
Show ANFDef where
  show (MkAFun args exp) = show args ++ ": " ++ show exp
  show (MkACon tag arity nt)
      = "Constructor tag " ++ show tag ++ " arity " ++ show arity ++ " newtype by " ++ show nt
  show (MkAForeign ccs args ret)
      = "Foreign call " ++ show ccs ++ " " ++
        show args ++ " -> " ++ show ret
  show (MkAError exp) = "Error: " ++ show exp

data AVars : List Name -> Type where
     Nil : AVars []
     (::) : Int -> AVars xs -> AVars (x :: xs)

data Next : Type where

nextVar : {auto v : Ref Next Int} ->
          Core Int
nextVar
    = do i <- get Next
         put Next (i + 1)
         pure i

lookup : {idx : _} -> (0 p : IsVar x idx vs) -> AVars vs -> Int
lookup First (x :: xs) = x
lookup (Later p) (x :: xs) = lookup p xs

bindArgs : {auto v : Ref Next Int} ->
           List ANF -> Core (List (AVar, Maybe ANF))
bindArgs [] = pure []
bindArgs (AV fc var :: xs)
    = do xs' <- bindArgs xs
         pure $ (var, Nothing) :: xs'
bindArgs (AErased fc :: xs)
    = do xs' <- bindArgs xs
         pure $ (ANull, Nothing) :: xs'
bindArgs (x :: xs)
    = do i <- nextVar
         xs' <- bindArgs xs
         pure $ (ALocal i, Just x) :: xs'

letBind : {auto v : Ref Next Int} ->
          FC -> List ANF -> (List AVar -> ANF) -> Core ANF
letBind fc args f
    = do bargs <- bindArgs args
         pure $ doBind [] bargs
  where
    doBind : List AVar -> List (AVar, Maybe ANF) -> ANF
    doBind vs [] = f (reverse vs)
    doBind vs ((ALocal i, Just t) :: xs)
        = ALet fc i t (doBind (ALocal i :: vs) xs)
    doBind vs ((var, _) :: xs) = doBind (var :: vs) xs

mlet : {auto v : Ref Next Int} ->
       FC -> ANF -> (AVar -> ANF) -> Core ANF
mlet fc (AV _ var) sc = pure $ sc var
mlet fc val sc
    = do i <- nextVar
         pure $ ALet fc i val (sc (ALocal i))

mutual
  anfArgs : {vars : _} ->
            {auto v : Ref Next Int} ->
            FC -> AVars vars ->
            List (Lifted vars) -> (List AVar -> ANF) -> Core ANF
  anfArgs fc vs args f
      = do args' <- traverse (anf vs) args
           letBind fc args' f

  anf : {vars : _} ->
        {auto v : Ref Next Int} ->
        AVars vars -> Lifted vars -> Core ANF
  anf vs (LLocal fc p) = pure $ AV fc (ALocal (lookup p vs))
  anf vs (LAppName fc lazy n args)
      = anfArgs fc vs args (AAppName fc lazy n)
  anf vs (LUnderApp fc n m args)
      = anfArgs fc vs args (AUnderApp fc n m)
  anf vs (LApp fc lazy f a)
      = anfArgs fc vs [f, a] $
                \case
                  [fvar, avar] => AApp fc lazy fvar avar
                  _ => ACrash fc "Can't happen (AApp)"
  anf vs (LLet fc x val sc)
      = do i <- nextVar
           let vs' = i :: vs
           pure $ ALet fc i !(anf vs val) !(anf vs' sc)
  anf vs (LCon fc n ci t args)
      = anfArgs fc vs args (ACon fc n ci t)
  anf vs (LOp {arity} fc lazy op args)
      = do args' <- traverse (anf vs) (toList args)
           letBind fc args'
                (\args => case toVect arity args of
                               Nothing => ACrash fc "Can't happen (AOp)"
                               Just argsv => AOp fc lazy op argsv)
  anf vs (LExtPrim fc lazy p args)
      = anfArgs fc vs args (AExtPrim fc lazy p)
  anf vs (LConCase fc scr alts def)
      = do scr' <- anf vs scr
           alts' <- traverse (anfConAlt vs) alts
           def' <- traverseOpt (anf vs) def
           mlet fc scr' (\x => AConCase fc x alts' def')
  anf vs (LConstCase fc scr alts def)
      = do scr' <- anf vs scr
           alts' <- traverse (anfConstAlt vs) alts
           def' <- traverseOpt (anf vs) def
           mlet fc scr' (\x => AConstCase fc x alts' def')
  anf vs (LPrimVal fc c) = pure $ APrimVal fc c
  anf vs (LErased fc) = pure $ AErased fc
  anf vs (LCrash fc err) = pure $ ACrash fc err

  anfConAlt : {vars : _} ->
              {auto v : Ref Next Int} ->
              AVars vars -> LiftedConAlt vars -> Core AConAlt
  anfConAlt vs (MkLConAlt n ci t args sc)
      = do (is, vs') <- bindArgs args vs
           pure $ MkAConAlt n ci t is !(anf vs' sc)
    where
      bindArgs : (args : List Name) -> AVars vars' ->
                 Core (List Int, AVars (args ++ vars'))
      bindArgs [] vs = pure ([], vs)
      bindArgs (n :: ns) vs
          = do i <- nextVar
               (is, vs') <- bindArgs ns vs
               pure (i :: is, i :: vs')

  anfConstAlt : {vars : _} ->
                {auto v : Ref Next Int} ->
                AVars vars -> LiftedConstAlt vars -> Core AConstAlt
  anfConstAlt vs (MkLConstAlt c sc)
      = pure $ MkAConstAlt c !(anf vs sc)

export
toANF : LiftedDef -> Core ANFDef
toANF (MkLFun args scope sc)
    = do v <- newRef Next (the Int 0)
         (iargs, vsNil) <- bindArgs args []
         let vs : AVars args = rewrite sym (appendNilRightNeutral args) in
                                      vsNil
         (iargs', vs) <- bindArgs scope vs
         pure $ MkAFun (iargs ++ reverse iargs') !(anf vs sc)
  where
    bindArgs : {auto v : Ref Next Int} ->
               (args : List Name) -> AVars vars' ->
               Core (List Int, AVars (args ++ vars'))
    bindArgs [] vs = pure ([], vs)
    bindArgs (n :: ns) vs
        = do i <- nextVar
             (is, vs') <- bindArgs ns vs
             pure (i :: is, i :: vs')
toANF (MkLCon t a ns) = pure $ MkACon t a ns
toANF (MkLForeign ccs fargs t) = pure $ MkAForeign ccs fargs t
toANF (MkLError err)
    = do v <- newRef Next (the Int 0)
         pure $ MkAError !(anf [] err)


text:
module Network.Curl.Multi

-- The 'Multi Curl Interface'

{- The multi interface is the asynchronous brother in the family and offers
incremental getting of data and multiple transfers at once. -}

import Network.Curl.Types
import Network.Curl.Prim

-- multi-socket based api

ext: idr


text:
module Part2

import Day3.Part1

matchingIndices : List Char -> Nat -> Bool -> (String -> Bool)
matchingIndices lc n most = \s => ((index' n lc) == Just (strIndex s (toIntNat n))) == most

export
partial solve2 : List String -> List Char -> Nat -> Bool -> Maybe String
solve2 ls lc n most = if (length ls) == 1 then index' 0 ls else solve2 nls (solve nls) (n+1) most where
    nls : List String
    nls = (filter (matchingIndices lc n most) ls)


text:
-- HOF.idr
-- Higher order functions

twice : (a -> a) -> a -> a
twice f x = f (f x)

Shape : Type
rotate : Shape -> Shape

-- taken from Generic.idr:
double : Num ty => ty -> ty
double x = x + x

quadruple : Num a => a -> a
quadruple = twice double

turn_around : Shape -> Shape
turn_around = twice rotate

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module TTImp.Interactive.CaseSplit

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

import TTImp.Elab
import TTImp.Elab.Check
import TTImp.ProcessDef
import TTImp.ProcessDecls
import TTImp.TTImp
import TTImp.TTImp.Functor
import TTImp.Unelab
import TTImp.Utils

import Data.List
import Libraries.Data.NameMap

%default covering

-- The result of a request to case split is a list of string updates, i.e. edits
-- on the clause in the source file, which an interactive editor can deal with
-- however it sees fit. 'Valid' means that the result will type check,
-- 'Impossible' means that the result will be a valid 'impossible' case
public export
data ClauseUpdate : Type where
     Valid : RawImp -> List (Name, RawImp) -> ClauseUpdate
     Impossible : RawImp -> ClauseUpdate
     Invalid : ClauseUpdate

export
Show ClauseUpdate where
  show (Valid lhs updates) = "Valid: " ++ show lhs ++ "\n" ++ "Updates: " ++ show updates
  show (Impossible lhs) = "Impossible: " ++ show lhs
  show Invalid = "Invalid"

public export
data SplitError : Type where
     NoValidSplit : SplitError -- None of the splits either type check, or fail
                               -- in a way which is valid as an 'impossible' case
     CantSplitThis : Name -> String -> SplitError -- Request to split was not on a splittable variable
     CantFindLHS : SplitError -- Can't find any clause to split

export
Show SplitError where
  show NoValidSplit = "No valid case splits"
  show (CantSplitThis n r) = "Can't split on " ++ show n ++ " (" ++ r ++ ")"
  show CantFindLHS = "No clause to split here"

public export
data SplitResult : Type -> Type where
     SplitFail : SplitError -> SplitResult a
     OK : a -> SplitResult a

export
Show a => Show (SplitResult a) where
  show (SplitFail err) = "Split error: " ++ show err
  show (OK res) = "OK: " ++ show res

findTyName : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             Defs -> Env Term vars -> Name -> Term vars ->
             Core (Maybe Name)
findTyName defs env n (Bind _ x b@(PVar _ c p ty) sc)
      -- Take the first one, which is the most recently bound
    = if n == x
         then do tynf <- nf defs env ty
                 case tynf of
                      NTCon _ tyn _ _ _ => pure $ Just tyn
                      _ => pure Nothing
         else findTyName defs (b :: env) n sc
findTyName defs env n (Bind _ x b sc) = findTyName defs (b :: env) n sc
findTyName _ _ _ _ = pure Nothing

getDefining : Term vars -> Maybe Name
getDefining (Bind _ _ _ sc) = getDefining sc
getDefining tm
    = case getFn tm of
           Ref _ _ fn => Just fn
           _ => Nothing

-- For the name on the lhs, return the function name being defined, the
-- type name, and the possible constructors.
findCons : {auto c : Ref Ctxt Defs} ->
           Name -> Term [] -> Core (SplitResult (Name, Name, List Name))
findCons n lhs
    = case getDefining lhs of
           Nothing => pure (SplitFail
                            (CantSplitThis n "Can't find function name on LHS"))
           Just fn =>
              do defs <- get Ctxt
                 case !(findTyName defs [] n lhs) of
                      Nothing => pure (SplitFail (CantSplitThis n
                                         ("Can't find type of " ++ show n ++ " in LHS")))
                      Just tyn =>
                          do Just (TCon _ _ _ _ _ _ cons _) <-
                                      lookupDefExact tyn (gamma defs)
                                | res => pure (SplitFail
                                            (CantSplitThis n
                                               ("Not a type constructor " ++
                                                  show res)))
                             pure (OK (fn, !(toFullNames tyn),
                                           !(traverse toFullNames cons)))

findAllVars : Term vars -> List Name
findAllVars (Bind _ x (PVar _ _ _ _) sc)
    = x :: findAllVars sc
findAllVars (Bind _ x (Let _ _ _ _) sc)
    = x :: findAllVars sc
findAllVars (Bind _ x (PLet _ _ _ _) sc)
    = x :: findAllVars sc
findAllVars _ = []

unique : List String -> List String -> Int -> List Name -> String
unique [] supply suff usedns = unique supply supply (suff + 1) usedns
unique (str :: next) supply suff usedns
    = let var = mkVarN str suff in
          if UN (Basic var) `elem` usedns
             then unique next supply suff usedns
             else var
  where
    mkVarN : String -> Int -> String
    mkVarN x 0 = x
    mkVarN x i = x ++ show i

defaultNames : List String
defaultNames = ["x", "y", "z", "w", "v", "s", "t", "u"]

export
getArgName : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             Defs -> Name ->
             List Name -> -- explicitly bound names (possibly coming later),
                          -- so we don't invent a default
                          -- name that duplicates it
             List Name -> -- names bound so far
             NF vars -> Core String
getArgName defs x bound allvars ty
    = do defnames <- findNames ty
         pure $ getName x defnames allvars
  where
    lookupName : Name -> List (Name, a) -> Core (Maybe a)
    lookupName n [] = pure Nothing
    lookupName n ((n', t) :: ts)
        = if !(getFullName n) == !(getFullName n')
             then pure (Just t)
             else lookupName n ts

    notBound : String -> Bool
    notBound x = not $ UN (Basic x) `elem` bound

    findNames : NF vars -> Core (List String)
    findNames (NBind _ x (Pi _ _ _ _) _)
        = pure (filter notBound ["f", "g"])
    findNames (NTCon _ n _ _ _)
        = case !(lookupName n (NameMap.toList (namedirectives defs))) of
               Nothing => pure (filter notBound defaultNames)
               Just ns => pure (filter notBound ns)
    findNames ty = pure (filter notBound defaultNames)

    getName : Name -> List String -> List Name -> String
    getName (UN (Basic n)) defs used = unique (n :: defs) (n :: defs) 0 used
    getName _ defs used = unique defs defs 0 used

export
getArgNames : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              Defs -> List Name -> List Name -> Env Term vars -> NF vars ->
              Core (List String)
getArgNames defs bound allvars env (NBind fc x (Pi _ _ p ty) sc)
    = do ns <- case p of
                    Explicit => pure [!(getArgName defs x bound allvars !(evalClosure defs ty))]
                    _ => pure []
         sc' <- sc defs (toClosure defaultOpts env (Erased fc False))
         pure $ ns ++ !(getArgNames defs bound (map (UN . Basic) ns ++ allvars) env sc')
getArgNames defs bound allvars env val = pure []

export
explicitlyBound : Defs -> NF [] -> Core (List Name)
explicitlyBound defs (NBind fc x (Pi _ _ _ _) sc)
    = pure $ x :: !(explicitlyBound defs
                    !(sc defs (toClosure defaultOpts [] (Erased fc False))))
explicitlyBound defs _ = pure []

export
getEnvArgNames : {auto c : Ref Ctxt Defs} ->
                 Defs -> Nat -> NF [] -> Core (List String)
getEnvArgNames defs Z sc = getArgNames defs !(explicitlyBound defs sc) [] [] sc
getEnvArgNames defs (S k) (NBind fc n _ sc)
    = getEnvArgNames defs k !(sc defs (toClosure defaultOpts [] (Erased fc False)))
getEnvArgNames defs n ty = pure []

expandCon : {auto c : Ref Ctxt Defs} ->
            FC -> List Name -> Name -> Core RawImp
expandCon fc usedvars con
    = do defs <- get Ctxt
         Just ty <- lookupTyExact con (gamma defs)
              | Nothing => undefinedName fc con
         pure (apply (IVar fc con)
                (map (IBindVar fc)
                     !(getArgNames defs [] usedvars []
                                   !(nf defs [] ty))))

updateArg : {auto c : Ref Ctxt Defs} ->
            List Name -> -- all the variable names
            (var : Name) -> (con : Name) ->
            RawImp -> Core RawImp
updateArg allvars var con (IVar fc n)
    = if n `elem` allvars
         then if n == var
                 then expandCon fc (filter (/= n) allvars) con
                 else pure $ Implicit fc True
         else pure $ IVar fc n
updateArg allvars var con (IApp fc f a)
    = pure $ IApp fc !(updateArg allvars var con f)
                     !(updateArg allvars var con a)
updateArg allvars var con (IAutoApp fc f a)
    = pure $ IAutoApp fc !(updateArg allvars var con f)
                     !(updateArg allvars var con a)
updateArg allvars var con (INamedApp fc f n a)
    = pure $ INamedApp fc !(updateArg allvars var con f) n
                          !(updateArg allvars var con a)
updateArg allvars var con (IAs fc nameFC s n p)
    = updateArg allvars var con p
updateArg allvars var con tm = pure $ Implicit (getFC tm) True

data ArgType
    = Explicit FC RawImp
    | Auto     FC RawImp
    | Named    FC Name RawImp

update : {auto c : Ref Ctxt Defs} ->
         List Name -> -- all the variable names
         (var : Name) -> (con : Name) ->
         ArgType -> Core ArgType
update allvars var con (Explicit fc arg)
    = pure $ Explicit fc !(updateArg allvars var con arg)
update allvars var con (Auto fc arg)
    = pure $ Auto fc !(updateArg allvars var con arg)
update allvars var con (Named fc n arg)
    = pure $ Named fc n !(updateArg allvars var con arg)

getFnArgs : RawImp -> List ArgType -> (RawImp, List ArgType)
getFnArgs (IApp fc tm a) args
    = getFnArgs tm (Explicit fc a :: args)
getFnArgs (IAutoApp fc tm a) args
    = getFnArgs tm (Auto fc a :: args)
getFnArgs (INamedApp fc tm n a) args
    = getFnArgs tm (Named fc n a :: args)
getFnArgs tm args = (tm, args)

apply : RawImp -> List ArgType -> RawImp
apply f (Explicit fc a :: args) = apply (IApp fc f a) args
apply f (Auto fc a :: args) = apply (IAutoApp fc f a) args
apply f (Named fc n a :: args) = apply (INamedApp fc f n a) args
apply f [] = f

-- Return a new LHS to check, replacing 'var' with an application of 'con'
-- Also replace any variables with '_' to allow elaboration to
-- expand them
newLHS : {auto c : Ref Ctxt Defs} ->
         FC ->
         Nat -> -- previous environment length; leave these alone
         List Name -> -- all the variable names
         (var : Name) -> (con : Name) ->
         RawImp -> Core RawImp
newLHS fc envlen allvars var con tm
    = do let (f, args) = getFnArgs tm []
         let keep = map (const (Explicit fc (Implicit fc True)))
                        (take envlen args)
         let ups = drop envlen args
         ups' <- traverse (update allvars var con) ups
         pure $ apply f (keep ++ ups')

record Updates where
  constructor MkUpdates
  namemap : List (Name, Name)
  updates : List (Name, RawImp)

data UPD : Type where

recordUpdate : {auto u : Ref UPD Updates} ->
               FC -> Name -> RawImp -> Core ()
recordUpdate fc n tm
    = do u <- get UPD
         let nupdates = map (\x => (fst x, IVar fc (snd x))) (namemap u)
         put UPD (record { updates $= ((n, substNames [] nupdates tm) ::) } u)

findUpdates : {auto u : Ref UPD Updates} ->
              Defs -> RawImp -> RawImp -> Core ()
findUpdates defs (IVar fc n) (IVar _ n')
    = case !(lookupTyExact n' (gamma defs)) of
           Just _ => recordUpdate fc n (IVar fc n')
           Nothing =>
              do u <- get UPD
                 case lookup n' (namemap u) of
                      Nothing => put UPD (record { namemap $= ((n', n) ::) } u)
                      Just nm => put UPD (record { updates $= ((n, IVar fc nm) ::) } u)
findUpdates defs (IVar fc n) tm = recordUpdate fc n tm
findUpdates defs (IApp _ f a) (IApp _ f' a')
    = do findUpdates defs f f'
         findUpdates defs a a'
findUpdates defs (IAutoApp _ f a) (IAutoApp _ f' a')
    = do findUpdates defs f f'
         findUpdates defs a a'
findUpdates defs (IAutoApp _ f a) f'
    = findUpdates defs f f'
findUpdates defs f (IAutoApp _ f' a)
    = findUpdates defs f f'
findUpdates defs (INamedApp _ f _ a) (INamedApp _ f' _ a')
    = do findUpdates defs f f'
         findUpdates defs a a'
findUpdates defs (INamedApp _ f _ a) f' = findUpdates defs f f'
findUpdates defs f (INamedApp _ f' _ a) = findUpdates defs f f'
findUpdates defs (IAs _ _ _ _ f) f' = findUpdates defs f f'
findUpdates defs f (IAs _ _ _ _ f') = findUpdates defs f f'
findUpdates _ _ _ = pure ()

getUpdates : Defs -> RawImp -> RawImp -> Core (List (Name, RawImp))
getUpdates defs orig updated
    = do u <- newRef UPD (MkUpdates [] [])
         findUpdates defs orig updated
         pure (updates !(get UPD))

mkCase : {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         Int -> RawImp -> RawImp -> Core ClauseUpdate
mkCase {c} {u} fn orig lhs_raw
    = do m <- newRef MD (initMetadata $ Virtual Interactive)
         defs <- get Ctxt
         ust <- get UST
         catch
           (do
               -- Fixes Issue #74. The problem is that if the function is defined in a sub module,
               -- then the current namespace (accessed by calling getNS) differs from the function
               -- namespace, therefore it is not considered visible by TTImp.Elab.App.checkVisibleNS
               -- FIXME: Causes issue #1385
               setAllPublic True

               -- Use 'Rig0' since it might be a type level function, or it might
               -- be an erased name in a case block (which will be bound elsewhere
               -- once split and turned into a pattern)
               (lhs, _) <- elabTerm {c} {m} {u}
                                    fn (InLHS erased) [] (MkNested [])
                                    [] (IBindHere (getFC lhs_raw) PATTERN lhs_raw)
                                    Nothing
               -- Revert all public back to false
               setAllPublic False
               put Ctxt defs -- reset the context, we don't want any updates
               put UST ust
               lhs' <- map (map rawName) $ unelabNoSugar [] lhs

               log "interaction.casesplit" 3 $ "Original LHS: " ++ show orig
               log "interaction.casesplit" 3 $ "New LHS: " ++ show lhs'

               pure (Valid lhs' !(getUpdates defs orig lhs')))
           (\err =>
               do put Ctxt defs
                  put UST ust
                  case err of
                       WhenUnifying _ gam env l r err
                         => do let defs = record { gamma = gam } defs
                               if !(impossibleOK defs !(nf defs env l)
                                                      !(nf defs env r))
                                  then pure (Impossible lhs_raw)
                                  else pure Invalid
                       _ => pure Invalid)

substLets : {vars : _} ->
            Term vars -> Term vars
substLets (Bind _ n (Let _ c val ty) sc) = substLets (subst val sc)
substLets (Bind _ n (PLet _ c val ty) sc) = substLets (subst val sc)
substLets (Bind fc n b sc) = Bind fc n b (substLets sc)
substLets tm = tm

combine : List ClauseUpdate -> List ClauseUpdate ->
          SplitResult (List ClauseUpdate)
combine [] [] = SplitFail NoValidSplit
combine [] acc = OK (reverse acc)
combine (Invalid :: xs) acc = combine xs acc
combine (x :: xs) acc = combine xs (x :: acc)

export
getSplitsLHS : {auto m : Ref MD Metadata} ->
               {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               FC -> Nat -> ClosedTerm -> Name ->
               Core (SplitResult (List ClauseUpdate))
getSplitsLHS fc envlen lhs_in n
    = do let lhs = substLets lhs_in
         logTerm "interaction.casesplit" 3 "Splitting" lhs_in
         let usedns = findAllVars lhs_in

         defs <- get Ctxt

         OK (fn, tyn, cons) <- findCons n lhs
            | SplitFail err => pure (SplitFail err)

         rawlhs <- map (map rawName) $ unelabNoSugar [] lhs
         trycases <- traverse (\c => newLHS fc envlen usedns n c rawlhs) cons

         let Just idx = getNameID fn (gamma defs)
             | Nothing => undefinedName fc fn
         cases <- traverse (mkCase idx rawlhs) trycases
         log "interaction.casesplit" 3 $ "Found cases: " ++ show cases

         pure (combine cases [])

export
getSplits : {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            (NonEmptyFC -> ClosedTerm -> Bool) -> Name ->
            Core (SplitResult (List ClauseUpdate))
getSplits p n
    = do Just (loc, envlen, lhs_in) <- findLHSAt p
              | Nothing => pure (SplitFail CantFindLHS)
         getSplitsLHS (justFC loc) envlen lhs_in n


text:
module Channel

import Linear
import Data.IORef
import Data.List

import System.Concurrency.Raw

public export
data Actions : Type -> Type where
     Send : (a : Type) -> (a -> Actions b) -> Actions b
     Recv : (a : Type) -> (a -> Actions b) -> Actions b
     Close : Actions ()

public export
dual : Actions a -> Actions a
dual (Send x f) = Recv x (\val => dual (f val))
dual (Recv x f) = Send x (\val => dual (f val))
dual Close = Close

public export
data Protocol : Type -> Type where
     Request : (a : Type) -> Protocol a
     Respond : (a : Type) -> Protocol a
     Bind : Protocol a -> (a -> Protocol b) -> Protocol b
     Loop : Inf (Protocol a) -> Protocol a
     Done : Protocol ()

public export
(>>=) : Protocol a -> (a -> Protocol b) -> Protocol b
(>>=) = Bind

public export
ClientK : Protocol a -> (a -> Actions b) -> Actions b
ClientK (Request a) k = Send a k
ClientK (Respond a) k = Recv a k
ClientK (Bind act next) k = ClientK act (\res => ClientK (next res) k)
ClientK (Loop proto) k = ClientK proto k
ClientK Done k = k ()

public export
ServerK : Protocol a -> (a -> Actions b) -> Actions b
ServerK (Request a) k = Recv a k
ServerK (Respond a) k = Send a k
ServerK (Bind act next) k = ServerK act (\res => ServerK (next res) k)
ServerK (Loop proto) k = ServerK proto k
ServerK Done k = k ()

public export
AsClient : Protocol a -> Actions ()
AsClient proto = ClientK proto (\res => Close)

public export
AsServer : Protocol a -> Actions ()
AsServer proto = ServerK proto (\res => Close)

public export
data QueueEntry : Type where
     Entry : (1 val : any) -> QueueEntry

public export
record RawMsgQueue where
  constructor MkRawMsgQueue
  inputStack : List QueueEntry
  outputStack : List QueueEntry

newQueue : RawMsgQueue
newQueue = MkRawMsgQueue [] []

enqueue : (1 val : a) -> RawMsgQueue -> RawMsgQueue
enqueue item q = record { inputStack $= (Entry item ::) } q

dequeue : RawMsgQueue -> Maybe (RawMsgQueue, QueueEntry)
dequeue q
    = case outputStack q of
           [] => case reverse (inputStack q) of
                      [] => Nothing
                      (x :: xs) => Just (record { outputStack = xs, inputStack = [] } q, x)
           (x :: xs) => Just (record { outputStack = xs } q, x)

public export
data Channel : {p : Protocol b} -> Actions a -> Type where
     MkChannel : (lock : Mutex) ->
                 (cond_lock : Mutex) ->
                 (cond : Condition) ->
                 (myInbox : IORef RawMsgQueue) ->
                 (remoteInbox : IORef RawMsgQueue) -> Channel {p} actions

public export
Client : Protocol a -> Type
Client p = Channel {p} (AsClient p)

public export
Server : Protocol a -> Type
Server p = Channel {p} (AsServer p)

mkChannels : (p : Protocol a) -> One IO (Client p, Server p)
mkChannels p
    = do clientInbox <- lift $ newIORef newQueue
         serverInbox <- lift $ newIORef newQueue
         lock <- lift $ makeMutex
         cond_lock <- lift $ makeMutex
         cond <- lift $ makeCondition
         pure (MkChannel lock cond_lock cond clientInbox serverInbox,
               MkChannel lock cond_lock cond serverInbox clientInbox)

export
send : (1 chan : Channel {p} (Send ty next)) -> (1 val : ty) ->
       One IO (Channel {p} (next val))
send (MkChannel lock cond_lock cond local remote) val
    = do lift $ mutexAcquire lock
         q <- lift $ readIORef remote
         lift $ writeIORef remote (enqueue val q)
         lift $ mutexRelease lock

         lift $ mutexAcquire cond_lock
         lift $ conditionSignal cond
         lift $ mutexRelease cond_lock
         pure (MkChannel lock cond_lock cond local remote)

-- returns Nothing if the message isn't there
export
tryRecv : forall b, a .
          {0 ty : Type} ->
          {0 next : (ty -> Actions a)} ->
          {0 p : Protocol b} ->
          (1 chan : Channel {p} (Recv ty next)) ->
          One IO (Res (Maybe ty) (\r => case r of
                                             Nothing => Channel {p} (Recv ty next)
                                             Just val => Channel {p} (next val)))
tryRecv (MkChannel lock cond_lock cond local remote)
    = do lift $ mutexAcquire lock
         rq <- lift $ readIORef local
         case dequeue rq of
              Nothing =>
                  do lift $ mutexRelease lock
                     pure (Nothing # MkChannel lock cond_lock cond local remote)
              Just (rq', Entry {any} val) =>
                  do lift $ writeIORef local rq'
                     lift $ mutexRelease lock
                     pure (Just (believe_me {a=any} val) #
                           MkChannel lock cond_lock cond local remote)

-- blocks until the message is there
export
recv : (1 chan : Channel {p} (Recv ty next)) ->
       One IO (Res ty (\val => Channel {p} (next val)))
recv (MkChannel lock cond_lock cond local remote)
    = do lift $ mutexAcquire lock
         rq <- lift $ readIORef local
         case dequeue rq of
              Nothing => -- ... no message, so wait for condition and try again
                  do lift $ mutexRelease lock
                     lift $ mutexAcquire cond_lock
                     lift $ conditionWait cond cond_lock
                     lift $ mutexRelease cond_lock
                     recv (MkChannel lock cond_lock cond local remote)
              Just (rq', Entry {any} val) =>
                  do lift $ writeIORef local rq'
                     lift $ mutexRelease lock
                     pure (believe_me {a=any} val #
                           MkChannel lock cond_lock cond local remote)

export
timeoutRecv : forall b, a .
              {0 ty : Type} ->
              {0 next : (ty -> Actions a)} ->
              {0 p : Protocol b} ->
              (1 chan : Channel {p} (Recv ty next)) ->
              (timeout : Int) ->
              One IO (Res (Maybe ty) (\r => case r of
                                                 Nothing => Channel {p} (Recv ty next)
                                                 Just val => Channel {p} (next val)))
timeoutRecv (MkChannel lock cond_lock cond local remote) timeout
    = do lift $ mutexAcquire lock
         rq <- lift $ readIORef local
         case dequeue rq of
              Nothing => -- ... no message, so wait for condition and try again with tryRecv
                  do lift $ mutexRelease lock
                     lift $ mutexAcquire cond_lock
                     lift $ conditionWaitTimeout cond cond_lock timeout
                     lift $ mutexRelease cond_lock
                     res # chan <- tryRecv {ty} {next} (MkChannel lock cond_lock cond local remote)
                     case res of
                          Nothing => pure (Nothing # chan)
                          Just res => pure (Just res # chan)
              Just (rq', Entry {any} val) =>
                  do lift $ writeIORef local rq'
                     lift $ mutexRelease lock
                     pure (Just (believe_me {a=any} val) #
                           MkChannel lock cond_lock cond local remote)

export
close : (1 chan : Channel Close) -> Any IO ()
close (MkChannel _ _ _ _ _) = pure ()

export
fork : {p : _} -> ((1 chan : Server p) -> Any IO ()) ->
       One IO (Client p)
fork proc
    = do (cchan, MkChannel a b c d e) <- mkChannels p
        -- deconstruct and reconstruct is a hack to work around the fact that
        -- 'run' doesn't express the function is only used once in its type, because
        -- 'Monad' and 'Applicative' don't express linearity... ugh!
         lift $ fork (run (proc (MkChannel a b c d e)))
         pure cchan


text:
module Main

import Exercises.GettingStarted
-- import String.Extra

%access export

private
pluralize : String -> String -> Nat -> String
pluralize singular plural count =
  if count == 1
     then "1 " ++ singular
     else (show count) ++ " " ++ plural

private
showCounts : String -> String
showCounts str = let (wordCount, charCount) = counts str in
                     "\"" ++ str ++ "\" has " ++
                     pluralize "word" "words" wordCount ++ " in " ++
                     pluralize "character" "characters" charCount ++ ".\n"

||| A REPL that prompts for a string and prints its word and character counts.
partial
main : IO ()
main = repl "Enter a string: "
            showCounts

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
module CairoCode.Traversal.Defaults

import Core.Context
import CairoCode.Traversal.Composition
import CairoCode.CairoCode
import CairoCode.Traversal.Base
import Utils.Lens
import Data.SortedMap

%hide Prelude.toList

export
generalize : ((rets:List CairoReg) -> SortedMap LinearImplicit (a, CairoReg) -> (params:List a) -> b) -> (InstVisit a -> b)
generalize fn = generalized
    where generalized : InstVisit a -> b
          generalized (VisitFunction _ _ _ _) = fn [] empty []
          generalized (VisitForeignFunction _ _ _ _) = fn [] empty []
          generalized (VisitAssign res reg) = fn [res] empty [reg]
          generalized (VisitMkCon res _ args) = fn [res] empty args
          generalized (VisitMkClosure res _ _ args) = fn [res] empty args
          generalized (VisitApply res linImpls clo arg) = fn [res] linImpls [clo,arg]
          generalized (VisitMkConstant res _) = fn [res] empty []
          generalized (VisitCall res linImpls _ args) = fn res linImpls args
          generalized (VisitOp res linImpls _ args) = fn [res] linImpls args
          generalized (VisitExtprim res linImpls _ args) = fn res linImpls args
          generalized (VisitReturn res _) = fn [] empty res -- Todo: Shall we Map implicits and pass in? to LinearImplicit -> (CairoReg, Eliminated)
          generalized (VisitProject res src _) = fn [res] empty [src]
          generalized (VisitNull res) = fn [res] empty []
          generalized (VisitError res _) = fn [res] empty []
          generalized (VisitCase arg) = fn [] empty [arg]
          generalized _ = fn [] empty []

-- Executes fn and if defined (Just) returns the value, otherwise (Nothing) returns a list with the input value
export
instFallback : (InstVisit a -> Traversal s (Maybe (List (InstVisit a)))) -> (InstVisit a -> Traversal s (List (InstVisit a)))
instFallback fn = (\inst => map (fromMaybe [inst]) (fn inst))

-- A wrapper that does nothing for control instructions and forwards the rest
export
ignoreControl : (InstVisit a -> Traversal s (List (InstVisit a))) -> (InstVisit a -> Traversal s (List (InstVisit a)))
ignoreControl fn = forwardControls
    where forwardControls : InstVisit a -> Traversal s (List (InstVisit a))
          forwardControls inst@(VisitFunction _ _ _ _) = pure [inst]
          forwardControls inst@(VisitForeignFunction _ _ _ _) = pure [inst]
          forwardControls VisitEndFunction = pure [VisitEndFunction]
          forwardControls inst@(VisitCase _ ) = pure [inst]
          forwardControls inst@(VisitConBranch _) = pure [inst]
          forwardControls inst@(VisitConstBranch _) = pure [inst]
          forwardControls VisitBranchEnd = pure [VisitBranchEnd]
          forwardControls VisitCaseEnd = pure [VisitCaseEnd]
          forwardControls inst = fn inst

export
substituteInstVisitValue : (a -> Traversal s b) -> (InstVisit b -> Traversal s c) -> (InstVisit a -> Traversal s c)
substituteInstVisitValue subst fn = (\inst => (substitute inst) >>= fn)
    where substituteMany : List a -> Traversal s (List b)
          substituteMany Nil = pure $ Nil
          substituteMany (x::xs) = pure $ (!(subst x))::(!(substituteMany xs))
          substLinImpls : SortedMap LinearImplicit (a, CairoReg) -> Traversal s (SortedMap LinearImplicit (b, CairoReg))
          substLinImpls linImpls = map fromList (traverse (\(impl,(from,to)) => pure (impl,(!(subst from),to))) (toList linImpls))
          substRetImpls : SortedMap LinearImplicit a -> Traversal s (SortedMap LinearImplicit b)
          substRetImpls linImpls = map fromList (traverse (\(impl,from) => pure (impl,!(subst from))) (toList linImpls))
          substitute : (InstVisit a -> Traversal s (InstVisit b))
          substitute (VisitFunction name params linImpls rets) = pure $ VisitFunction name params linImpls rets
          substitute (VisitForeignFunction name inf args rets) = pure $ VisitForeignFunction name inf args rets
          substitute (VisitAssign res src) = pure $ VisitAssign res !(subst src)
          substitute (VisitMkCon res tag args) = pure $ VisitMkCon res tag !(substituteMany args)
          substitute (VisitMkClosure res name miss args) = pure $ VisitMkClosure res name miss !(substituteMany args)
          substitute (VisitApply res linImpls clo arg) = pure $ VisitApply res !(substLinImpls linImpls) !(subst clo) !(subst arg)
          substitute (VisitMkConstant res const) = pure $ VisitMkConstant res const
          substitute (VisitCall res linImpls name args) = pure $ VisitCall res !(substLinImpls linImpls) name !(substituteMany args)
          substitute (VisitOp res linImpls primFn args) = pure $ VisitOp res !(substLinImpls linImpls) primFn !(substituteMany args)
          substitute (VisitExtprim res linImpls name args) = pure $ VisitExtprim res !(substLinImpls linImpls) name !(substituteMany args)
          substitute (VisitCase reg) = pure $ VisitCase !(subst reg)
          substitute (VisitConBranch tag) = pure $ VisitConBranch tag
          substitute (VisitConstBranch const) = pure $ VisitConstBranch const
          substitute VisitBranchEnd = pure $ VisitBranchEnd
          substitute VisitCaseEnd = pure $ VisitCaseEnd
          substitute (VisitProject res val pos) = pure $ VisitProject res !(subst val) pos
          substitute (VisitReturn vals linImpls) = pure $ VisitReturn !(substituteMany vals) !(substRetImpls linImpls)
          substitute (VisitNull res) = pure $ VisitNull res
          substitute (VisitError res err) = pure $ VisitError res err
          substitute VisitEndFunction = pure $ VisitEndFunction

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Extra.Fin

import Data.Fin
import Data.Fin.Extra
import Data.Nat
import Data.Nat.Division
import Extra.Binary
import Extra.Nat

||| Turns a `Bits8` into its `Fin` representation
export
bits8ToFin : Bits8 -> Fin 256
bits8ToFin n = helper 0
  where
  helper : Bits8 -> Fin 256
  helper m = believe_me $ if m == n then FZ else FS (helper (m + 1))

||| Modulo a `Fin`
export
modFinNZ : Fin (S a) -> (b : Nat) -> Not (b = 0) -> Fin b
modFinNZ a b prf = let x = boundModNatNZ (finToNat a) b prf in natToFinLTE (modNatNZ (finToNat a) b prf) x

-- TODO: i have no idea how to prove this with the monotonic property of division or whatever its called by the true gameRZ of the community. For now i'm using natToFin, which is sacrilegious imo
||| Divide a `Fin`
export
divFinNZ : {a : Nat} -> Fin (S a) -> (b : Nat) -> (prf : Not (b = 0)) -> Fin (S (divNatNZ a b prf))
divFinNZ numer denom prf = case natToFin (divNatNZ (finToNat numer) denom prf) (S (divNatNZ a denom prf)) of
  Just x => x
  Nothing => last

||| Divide and modulo a `Fin`
export
divmodFinNZ : {a : Nat} -> Fin (S a) -> (b : Nat) -> (prf : Not (b = 0)) -> (Fin (S (divNatNZ a b prf)), Fin b)
divmodFinNZ a b prf = (divFinNZ a b prf, modFinNZ a b prf)


text:
module ArithExample

import Fix
import ALaCarte

%access public export

-- DSL for arithmetic expressions

data Val k = V Int
data Add k = A k k
data Mul k = M k k

Expr : Type
Expr = Fix (Sig [Val, Add, Mul])

Functor Val where
    map func (V x) = V x

Functor Add where
    map func (A x y) = A (func x) (func y)

Functor Mul where
    map func (M x y) = M (func x) (func y)

-- Smart constructors

val : {auto prf : Elem Val fs} -> Int -> Fix (Sig fs)
val x = inject (V x)

(+) : {auto prf : Elem Add fs} -> Fix (Sig fs) -> Fix (Sig fs) -> Fix (Sig fs)
x + y = inject (A x y)

(*) : {auto prf : Elem Mul fs} -> Fix (Sig fs) -> Fix (Sig fs) -> Fix (Sig fs)
x * y = inject (M x y)

-- Evaluation

Alg Val Int where
    alg (V x) = x

Alg Add Int where
    alg (A x y) = x + y

Alg Mul Int where
    alg (M x y) = x * y

calc : Expr -> Int
calc = eval

-- Pretty Printing

Alg Val String where
    alg (V x) = show x

Alg Add String where
    alg (A x y) = "(" ++ x ++ " + " ++ y ++ ")"

Alg Mul String where
    alg (M x y) = "(" ++ x ++ " * " ++ y ++ ")"

pretty : Expr -> String
pretty = eval

-- Examples

ex1 : Expr
ex1 = (val 1 + val 2) * val 3

runEx : Expr -> IO ()
runEx e = do
    putStrLn (pretty e)
    putStrLn (show (calc e))

max_stars_repo_name: BakerSmithA/alacarte-idris

max_issues_repo_name: BakerSmithA/alacarte-idris

max_forks_repo_name: BakerSmithA/alacarte-idris


text:
{-
55
-}
module Main

main : IO ()
main = printLn $ foldl (+) 0 [1..10]

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
test : Not (Nat = String)
test Refl impossible

test2 : Not (Char = String)
test2 Refl impossible

test3 : Not (Type = String)
test3 Refl impossible

test4 : Not (Type = Nat)
test4 Refl impossible

test5 : Not (List Nat = Type)
test5 Refl impossible

test6 : Not (Bits64 = Type)
test6 Refl impossible

test7 : Not ('a' = 'b')
test7 Refl impossible

-- The following ones are actually possible

test8 : Not (a = Type)
test8 Refl impossible

test9 : Not (a = 'a')
test9 Refl impossible

test10 : Not (a = Nat)
test10 Refl impossible

test11 : Not (3 = a)
test11 Refl impossible


text:
module Part2.Sec5_3_3_dpair
import Data.Vect

{-
Note, Idris figures out Vect size.
In Haskell "_" == "I do not care"
In Idris "_" == "You figure it out"
-}
||| Conversion between a list and dependent pair
||| Think about using strong dependent types in runtime calculations.
listToVect : List a -> (n ** Vect n a)
listToVect [] = (_ ** [])
listToVect (x :: xs) =
        let (_ ** vxs) = listToVect xs
        in (_ ** x :: vxs)

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
module Data.Sexp.Lexer

import Data.List
import Data.Maybe
import Data.String
import Libraries.Text.Lexer

%default covering

public export
data Token = LParen
           | RParen
           | Atom String
           | QuotedAtom String
           | Comment String

export
Show Token where
  show LParen = "LParen"
  show RParen = "RParen"
  show (Atom s) = "Atom \"" ++ s ++ "\""
  show (QuotedAtom s) = "QAtom \"" ++ s ++ "\""
  show (Comment s) = "; " ++ s ++ "\n"

export
Eq Token where
  LParen == LParen = True
  RParen == RParen = True
  _ == _ = False

comment : Lexer
comment = is ';' <+> many (pred (/= '\n')) <+> is '\n'

lparen : Lexer
lparen = is '(' <+> many space

rparen : Lexer
rparen = is ')' <+> many space

isAlphNum : Char -> Bool
isAlphNum c = (c >= 'a' && c <= 'z') || (c >= 'A' && c <= 'Z') || (c >= '0' && c <= '9')

ident : Lexer
ident = pred (\c => c /= '"' && c /= ' ' && c /= '(' && c /= ')' && c /= '\n' && c /= ';')

atom : Lexer
atom = some ident <+> many space

quotedAtom : Lexer
quotedAtom = stringLit <+> many space

removeQuotes : String -> String
removeQuotes s = assert_total $ reverse $ strTail $ reverse $ strTail s

escape : String -> Maybe String
escape s = map (fastPack . reverse) $ escape' (unpack s) [] where
  escape' : List Char -> List Char -> Maybe (List Char)
  escape' [] acc = Just acc
  escape' ('\\'::'{'::rest) acc =
    let (codepoint, rest) = span (/= '}') rest
        ch = cast $ cast {to=Int} (fastPack codepoint) in
        escape' (drop 1 rest) (ch::acc)
  escape' ('\\'::'\\'::rest) acc = escape' rest ('\\'::acc)
  escape' ('\\'::'a'::rest) acc = escape' rest ('\a'::acc)
  escape' ('\\'::'b'::rest) acc = escape' rest ('\b'::acc)
  escape' ('\\'::'f'::rest) acc = escape' rest ('\f'::acc)
  escape' ('\\'::'n'::rest) acc = escape' rest ('\n'::acc)
  escape' ('\\'::'r'::rest) acc = escape' rest ('\r'::acc)
  escape' ('\\'::'t'::rest) acc = escape' rest ('\t'::acc)
  escape' ('\\'::'v'::rest) acc = escape' rest ('\v'::acc)
  escape' ('\\'::'"'::rest) acc = escape' rest ('"'::acc)
  escape' ('\\'::'D'::'E'::'L'::rest) acc = escape' rest ('\DEL'::acc)
  escape' ('\\'::'E'::'S'::'C'::rest) acc = escape' rest ('\ESC'::acc)
  escape' ('\\'::'L'::'F'::rest) acc = escape' rest ('\LF'::acc)
  escape' ('\\'::'N'::'U'::'L'::rest) acc = escape' rest ('\NUL'::acc)
  escape' ('\\'::'S'::'O'::rest) acc = escape' rest ('\SO'::acc)
  escape' ('\\'::'S'::'Y'::'N'::rest) acc = escape' rest ('\SYN'::acc)
  escape' ('\\'::'U'::'S'::rest) acc = escape' rest ('\US'::acc)
  escape' ('\\'::xs) acc = case span isDigit xs of
           ([], rest) => escape' rest acc
           (ds, rest) => escape' rest (cast (cast {to=Int} (fastPack ds)) :: acc)
  escape' (c::rest) acc = escape' rest (c::acc)

tokenMap : TokenMap Token
tokenMap = [
  (lparen, \_ => LParen),
  (rparen, \_ => RParen),
  (atom, Atom . trim),
  (quotedAtom, QuotedAtom . (fromMaybe "<error>" . escape) . removeQuotes . trim)
  --(comment, Comment)
  ]

export
lexSexp : String -> Either (String) (List (WithBounds Token))
lexSexp s = let (toks, line, col, remainder) = lex tokenMap s in
                if remainder == "" then Right $ toks
                                   else Left $ "remaining: " ++ remainder

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Num

%default total

{-
  interface Num ty where
    (+) : ty -> ty -> ty
    (*) : ty -> ty -> ty
    fromInteger : Integer -> ty

  interface Num ty => Neg ty where
    negate : ty -> ty
    (-) : ty -> ty -> ty
    abs : ty -> ty

  interface Num ty => Integral ty  where
    div  : ty -> ty -> ty
    mod : ty -> ty -> ty

  interface Num ty => Fractional ty where
    (/) : ty -> ty -> ty
    recip : ty -> ty

    recip x = 1 / x
-}

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Main

import Data.List

large : (a: Type) -> a
-- integer larger than 64 bits
large Integer = 3518437212345678901234567890123
-- int close to 2ˆ63
-- we expect some operations will overflow
large Int = 3518437212345678901234567890

small : (a: Type) -> a
small Integer = 437
small Int = 377

numOps : (Num a) => List ( a -> a -> a )
numOps = [ (+), (*) ]

negOps : (Neg a) => List (a -> a -> a)
negOps = [ (-) ]

integralOps : (Integral a) => List (a -> a -> a)
integralOps = [ div, mod ]

binOps : (Num a, Neg a, Integral a) => List (a -> a -> a)
binOps = numOps ++ negOps ++ integralOps

main : IO ()
main = do
  putStrLn $ show (results Integer)
  putStrLn $ show (results Int)
  where
  results : (a:Type) -> (Num a, Neg a, Integral a) => List a
  results a = map (\ op => large a  `op` small a) binOps


text:
{-
'A'
'_'
'C'
True
False
True
True
False
True
-}
module Main

data D = A | B | C

adt : D -> IO Bool
adt A = pure True
adt C = pure True
adt _ = pure False

int : Int -> IO Bool
int 0          = pure True
int 2147483647 = pure True
int _          = pure False

char : Char -> IO Char
char 'C' = pure 'C'
char 'B' = pure 'B'
char 'A' = pure 'A'
char _   = pure '_'

printMap : (Traversable t, Show b) => (a -> IO b) -> t a -> IO ()
printMap f xs = for_ xs (\x => f x >>= printLn)

main : IO ()
main = do
  printMap char ['A', 'D', 'C']
  printMap int  [0, 1, 2147483647]
  printMap adt  [A, B, C]

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
> data Vect : Nat -> Type -> Type where
>      Nil : Vect Z a
>      (::) : a -> Vect k a -> Vect (S k) a

> %name Vect xs, ys, zs

> my_cong : forall f . (x : a) -> (y : a) -> x = y -> f x = f y

> my_curry : ((a, b) -> c) -> a -> b -> c

> my_uncurry : (a -> b -> c) -> (a, b) -> c

> append : Vect n a -> Vect m a -> Vect (n + m) a

> lappend : (1 xs : List a) -> (1 ys : List a) -> List a

> zipWith : (a -> b -> c) -> Vect n a -> Vect n b -> Vect n c

> data Env : Vect n Type -> Type where
>      ENil : Env []
>      ECons : a -> Env xs -> Env (a :: xs)

> %name Env es

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

> lookup : Elem ty vs -> Env vs -> ty

ext: lidr


text:
-- module Main

data N = Zero | Suc N

add : N -> N -> N
add Zero s = s
add (Suc a) b = add a (Suc b)

data Vec : (a : Type) -> N -> Type where
  Nil : Vec a Zero
  Cons : {n : N} -> a -> Vec a n -> Vec a (Suc n)

ccExp : {g : Type} -> {a : N} -> {b : N} -> Vec g a -> Vec g b -> Vec g (add a b)

ccImp : Vec g a -> Vec g b -> Vec g (add a b)

max_stars_repo_name: hjorthjort/IdrisToAgda

max_issues_repo_name: hjorthjort/IdrisToAgda

max_forks_repo_name: hjorthjort/IdrisToAgda


text:
module Induction

%default total

plusZeroReduces : (n : Nat) -> n + 0 = n
plusZeroReduces Z = refl
plusZeroReduces (S k) = let ind = plusZeroReduces k in ?plusZeroSucc

Induction.plusZeroSucc = proof
  intros
  rewrite ind
  trivial

minusDiag : (n : Nat) -> minus n n = Z
minusDiag Z = refl
minusDiag (S k) = let ih = minusDiag k in ?minusDiagNeutral

Induction.minusDiagNeutral = proof
  intros
  rewrite ih
  trivial

multZeroIsZero : (n : Nat) -> mult n Z = Z
multZeroIsZero Z = refl
multZeroIsZero (S k) = let ih = multZeroIsZero k in ?multSuccByZeroIsZero

Induction.multSuccByZeroIsZero = proof
  intros
  rewrite ih
  trivial

plusNSuccMRefl : (left : Nat) -> (right : Nat) -> S (left + right) = left + (S right)
plusNSuccMRefl Z right = refl
plusNSuccMRefl (S k) right = let ih = plusNSuccMRefl k right in ?plusSuccRefl

Induction.plusSuccRefl = proof
  intros
  rewrite ih
  trivial

plusCommutes : (left : Nat) -> (right : Nat) -> left + right = right + left
plusCommutes Z right = ?plusCommutesBaseCase
plusCommutes (S left) right = let ih = plusCommutes left right in ?plusCommutesSuccCase

Induction.plusCommutesBaseCase = proof
  intro
  rewrite sym (plusZeroReduces right)
  trivial

Induction.plusCommutesSuccCase = proof
  intros
  rewrite (plusNSuccMRefl right left)
  rewrite ih
  trivial

plusAssoc : (a : Nat) -> (b : Nat) -> (c : Nat) -> a + (b + c) = (a + b) + c
plusAssoc Z b c = ?plusAssocBaseCase
plusAssoc (S a) b c = let ih = plusAssoc a b c in ?plusAssocStepCase

Induction.plusAssocBaseCase = proof
  intros
  trivial

Induction.plusAssocStepCase = proof
  intros
  rewrite ih
  trivial

double : Nat -> Nat
double Z = Z
double (S k) = (S (S (double k)))

doublePlusRefl : (n : Nat) -> double n = n + n
doublePlusRefl Z = refl
doublePlusRefl (S n) = let ih = doublePlusRefl n in ?doublePlusStepCase

Induction.doublePlusStepCase = proof
  intros
  rewrite sym ih
  rewrite (plusNSuccMRefl n n)
  trivial

plusRearrange : (a:Nat) -> (b:Nat) -> (c:Nat) -> (d:Nat) -> (a + b) + (c + d) = (b + a) + (c + d)
plusRearrange a b c d = ?plusRearrangeBase

Induction.plusRearrangeBase = proof
  intros
  rewrite (plusCommutes a b)
  trivial

plusSwap : (a:Nat) -> (b:Nat) -> (c:Nat) -> a + (b + c) = b + (a + c)
plusSwap = ?plusSwapProof

Induction.plusSwapProof = proof
  intros
  rewrite sym (plusAssoc b a c)
  rewrite (plusCommutes b a)
  rewrite (plusCommutes a b)
  rewrite(plusAssoc a b c)
  trivial

max_stars_repo_name: joshvera/software-foundations-in-idris

max_issues_repo_name: joshvera/software-foundations-in-idris

max_forks_repo_name: joshvera/software-foundations-in-idris


text:
module Dualise

import Data.Vect
import ProcessLib
import Proto

%default total
%access public export

--TODO: think about if we need to make dualise not send on requests

resp: (pid: ProcPID (MkNiche cut_a cut_b)) ->
      (msg : Req (MkNiche (dual cut_b) (dual cut_a))) ->
      SubProc (MkNiche (dual cut_b) (dual cut_a))
              (ProcIF (MkNiche (dual cut_b) (dual cut_a)) msg)
resp pid (Conn (TopOutWire loc) pid' outw) = Request pid (Conn (BotOutWire (dualAddrUp   loc)) pid' outw)
resp pid (Conn (BotOutWire loc) pid' outw) = Request pid (Conn (TopOutWire (dualAddrDown loc)) pid' outw)
resp pid (Val  (TopInWire  loc) x)         = do --Action $ putStrLn "dual: got top, sending to bot"
                                                Request pid (Val  (BotInWire  (dualAddrDown loc)) x)
resp pid (Val  (BotInWire  loc) x)         = do --Action $ putStrLn "dual: got bot, sending to top"
                                                Request pid (Val  (TopInWire  (dualAddrUp   loc)) x)

loop: ProcPID (MkNiche cut_a cut_b) ->
      Process (ProcIF (MkNiche (dual cut_b) (dual cut_a))) () Ready Looping
loop pid = do --Action $ putStrLn "dual: starting normal loop"
              Just msg <- Respond $ resp pid | _ => do --Action $ putStrLn "dual: got nothing"
                                                       Loop (loop pid)
              Loop    $ loop pid

partial
dualise: Hom cut_a cut_b -> Hom (dual cut_b) (dual cut_a)
dualise proc = do Just pid <- Spawn proc
                  loop pid

max_stars_repo_name: jameshaydon/smproc

max_issues_repo_name: jameshaydon/smproc

max_forks_repo_name: jameshaydon/smproc


text:
module EquivFoldConstants

import Equiv
import Expr
import Logic
import Imp
import Maps

%access public export

%default total

fold_constants_aexp : (a : AExp) -> AExp
fold_constants_aexp (ANum k) = ANum k
fold_constants_aexp (AId x) = AId x
fold_constants_aexp (APlus a1 a2) =
  case (fold_constants_aexp a1, fold_constants_aexp a2) of
    (ANum n1, ANum n2) => ANum (n1 + n2)
    (e1, e2) => APlus e1 e2
fold_constants_aexp (AMinus a1 a2) =
  case (fold_constants_aexp a1, fold_constants_aexp a2) of
    (ANum n1, ANum n2) => ANum (minus n1 n2)
    (e1, e2) => AMinus e1 e2
fold_constants_aexp (AMult a1 a2) =
  case (fold_constants_aexp a1, fold_constants_aexp a2) of
    (ANum n1, ANum n2) => ANum (n1 * n2)
    (e1, e2) => AMult e1 e2

fold_aexp_example_1 : fold_constants_aexp ((1 + 2) * X) = 3 * X
fold_aexp_example_1 = Refl

fold_aexp_example_2 : fold_constants_aexp (X - (0 * 6 + Y))
                    = X - (0 + Y)
fold_aexp_example_2 = Refl

fold_constants_bexp : (b : BExp) -> BExp
fold_constants_bexp BTrue = BTrue
fold_constants_bexp BFalse = BFalse
fold_constants_bexp (BEq a1 a2) =
  case (fold_constants_aexp a1, fold_constants_aexp a2) of
    (ANum n1, ANum n2) => if n1 == n2 then BTrue else BFalse
    (e1, e2) => BEq e1 e2
fold_constants_bexp (BLe a1 a2) =
  case (fold_constants_aexp a1, fold_constants_aexp a2) of
    (ANum n1, ANum n2) => if lte n1 n2 then BTrue else BFalse
    (e1, e2) => BLe e1 e2
fold_constants_bexp (BNot b) =
  case fold_constants_bexp b of
    BTrue => BFalse
    BFalse => BTrue
    e => BNot e
fold_constants_bexp (BAnd b1 b2) =
  case (fold_constants_bexp b1, fold_constants_bexp b2) of
    (BTrue, e2) => e2
    (BFalse, _) => BFalse
    (e1, e2) => BAnd e1 e2

fold_bexp_example_1 : fold_constants_bexp (BTrue && (not (BFalse && BTrue)))
                    = BTrue
fold_bexp_example_1 = Refl

fold_bexp_example_2 : fold_constants_bexp ((X == Y) && (0 == 2 - (1 + 1)))
                    = (X == Y) && BTrue
fold_bexp_example_2 = Refl

fold_constants_com : (c : Com) -> Com
fold_constants_com CSkip = SKIP
fold_constants_com (CAss x e) = x ::= fold_constants_aexp e
fold_constants_com (CSeq c1 c2) = CSeq (fold_constants_com c1)
                                       (fold_constants_com c2)
fold_constants_com (CIf b ct cf) =
  case fold_constants_bexp b of
    BTrue => fold_constants_com ct
    BFalse => fold_constants_com cf
    e => CIf e (fold_constants_com ct) (fold_constants_com cf)
fold_constants_com (CIf1 b c) =
  case fold_constants_bexp b of
    BTrue => fold_constants_com c
    BFalse => SKIP
    e => CIf1 e (fold_constants_com c)
fold_constants_com (CWhile b c) =
  case fold_constants_bexp b of
    BTrue => CWhile BTrue SKIP
    BFalse => SKIP
    e => CWhile e (fold_constants_com c)
fold_constants_com (CFor init cond updt body) =
  case fold_constants_bexp cond of
    BTrue => CSeq (fold_constants_com init) (CWhile BTrue SKIP)
    BFalse => fold_constants_com init
    e => CFor (fold_constants_com init)
              e
              (fold_constants_com updt)
              (fold_constants_com body)
fold_constants_com (CRepeat c b) =
  case fold_constants_bexp b of
    BTrue => fold_constants_com c
    BFalse => CSeq (fold_constants_com c) (CWhile BTrue SKIP)
    e => CRepeat (fold_constants_com c) e

fold_com_example_1 :
  fold_constants_com
    (do X ::= 4 + 5
        Y ::= X - 3
        IFB X - Y == 2 + 4
            THEN SKIP
            ELSE Y ::= 0
        FI
        IFB 0 <= 4 - (2 + 1)
            THEN Y ::= 0
            ELSE SKIP
        FI
        WHILE (Y == 0) $
          X ::= X + 1)
  = (do X ::= 9
        Y ::= X - 3
        IFB X - Y == 6
            THEN SKIP
            ELSE Y ::= 0
        FI
        Y ::= 0
        WHILE (Y == 0) $
          X ::= X + 1)
fold_com_example_1 = Refl

fold_constants_aexp_sound : ATransSound EquivFoldConstants.fold_constants_aexp
fold_constants_aexp_sound (ANum _) _ = Refl
fold_constants_aexp_sound (AId _) _ = Refl
fold_constants_aexp_sound (APlus a1 a2) st
  with (fold_constants_aexp a1) proof a1prf
    fold_constants_aexp_sound (APlus a1 a2) st | ANum _
      with (fold_constants_aexp a2) proof a2prf
        fold_constants_aexp_sound (APlus a1 a2) st | ANum _ | ANum _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (APlus a1 a2) st | ANum _ | AId _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (APlus a1 a2) st | ANum _ | APlus _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (APlus a1 a2) st | ANum _ | AMinus _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (APlus a1 a2) st | ANum _ | AMult _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
    fold_constants_aexp_sound (APlus a1 a2) st | AId _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_aexp_sound (APlus a1 a2) st | APlus _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_aexp_sound (APlus a1 a2) st | AMinus _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_aexp_sound (APlus a1 a2) st | AMult _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
fold_constants_aexp_sound (AMinus a1 a2) st
  with (fold_constants_aexp a1) proof a1prf
    fold_constants_aexp_sound (AMinus a1 a2) st | ANum _
      with (fold_constants_aexp a2) proof a2prf
        fold_constants_aexp_sound (AMinus a1 a2) st | ANum _ | ANum _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (AMinus a1 a2) st | ANum _ | AId _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (AMinus a1 a2) st | ANum _ | APlus _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (AMinus a1 a2) st | ANum _ | AMinus _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (AMinus a1 a2) st | ANum _ | AMult _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
    fold_constants_aexp_sound (AMinus a1 a2) st | AId _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_aexp_sound (AMinus a1 a2) st | APlus _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_aexp_sound (AMinus a1 a2) st | AMinus _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_aexp_sound (AMinus a1 a2) st | AMult _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
fold_constants_aexp_sound (AMult a1 a2) st
  with (fold_constants_aexp a1) proof a1prf
    fold_constants_aexp_sound (AMult a1 a2) st | ANum _
      with (fold_constants_aexp a2) proof a2prf
        fold_constants_aexp_sound (AMult a1 a2) st | ANum _ | ANum _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (AMult a1 a2) st | ANum _ | AId _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (AMult a1 a2) st | ANum _ | APlus _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (AMult a1 a2) st | ANum _ | AMinus _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_aexp_sound (AMult a1 a2) st | ANum _ | AMult _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
    fold_constants_aexp_sound (AMult a1 a2) st | AId _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_aexp_sound (AMult a1 a2) st | APlus _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_aexp_sound (AMult a1 a2) st | AMinus _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_aexp_sound (AMult a1 a2) st | AMult _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl

fold_constants_bexp_sound : BTransSound EquivFoldConstants.fold_constants_bexp
fold_constants_bexp_sound BTrue _ = Refl
fold_constants_bexp_sound BFalse _ = Refl
fold_constants_bexp_sound (BEq a1 a2) st
  with (fold_constants_aexp a1) proof a1prf
    fold_constants_bexp_sound (BEq a1 a2) st | ANum k
      with (fold_constants_aexp a2) proof a2prf
        fold_constants_bexp_sound (BEq a1 a2) st | ANum k | ANum j
          with (k == j) proof eprf
            fold_constants_bexp_sound (BEq a1 a2) st | ANum k | ANum j | False =
              rewrite fold_constants_aexp_sound a1 st
              in rewrite sym a1prf
              in rewrite fold_constants_aexp_sound a2 st
              in rewrite sym a2prf
              in rewrite sym eprf
              in Refl
            fold_constants_bexp_sound (BEq a1 a2) st | ANum k | ANum j | True =
              rewrite fold_constants_aexp_sound a1 st
              in rewrite sym a1prf
              in rewrite fold_constants_aexp_sound a2 st
              in rewrite sym a2prf
              in rewrite sym eprf
              in Refl
        fold_constants_bexp_sound (BEq a1 a2) st | ANum _ | AId _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_bexp_sound (BEq a1 a2) st | ANum _ | APlus _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_bexp_sound (BEq a1 a2) st | ANum _ | AMinus _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_bexp_sound (BEq a1 a2) st | ANum _ | AMult _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
    fold_constants_bexp_sound (BEq a1 a2) st | AId _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_bexp_sound (BEq a1 a2) st | APlus _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_bexp_sound (BEq a1 a2) st | AMinus _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_bexp_sound (BEq a1 a2) st | AMult _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
fold_constants_bexp_sound (BLe a1 a2) st
  with (fold_constants_aexp a1) proof a1prf
    fold_constants_bexp_sound (BLe a1 a2) st | ANum k
      with (fold_constants_aexp a2) proof a2prf
        fold_constants_bexp_sound (BLe a1 a2) st | ANum k | ANum j
          with (lte k j) proof lte_prf
            fold_constants_bexp_sound (BLe a1 a2) st | ANum k | ANum j | False =
              rewrite fold_constants_aexp_sound a1 st
              in rewrite sym a1prf
              in rewrite fold_constants_aexp_sound a2 st
              in rewrite sym a2prf
              in rewrite lte_prf
              in Refl
            fold_constants_bexp_sound (BLe a1 a2) st | ANum k | ANum j | True =
              rewrite fold_constants_aexp_sound a1 st
              in rewrite sym a1prf
              in rewrite fold_constants_aexp_sound a2 st
              in rewrite sym a2prf
              in rewrite lte_prf
              in Refl
        fold_constants_bexp_sound (BLe a1 a2) st | ANum _ | AId _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_bexp_sound (BLe a1 a2) st | ANum _ | APlus _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_bexp_sound (BLe a1 a2) st | ANum _ | AMinus _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        fold_constants_bexp_sound (BLe a1 a2) st | ANum _ | AMult _ _ =
          rewrite fold_constants_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite fold_constants_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
    fold_constants_bexp_sound (BLe a1 a2) st | AId _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_bexp_sound (BLe a1 a2) st | APlus _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_bexp_sound (BLe a1 a2) st | AMinus _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
    fold_constants_bexp_sound (BLe a1 a2) st | AMult _ _ =
      rewrite fold_constants_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite fold_constants_aexp_sound a2 st
      in Refl
fold_constants_bexp_sound (BNot b) st
  with (fold_constants_bexp b) proof bprf
    fold_constants_bexp_sound (BNot b) st | BTrue =
      rewrite fold_constants_bexp_sound b st
      in rewrite sym bprf
      in Refl
    fold_constants_bexp_sound (BNot b) st | BFalse =
      rewrite fold_constants_bexp_sound b st
      in rewrite sym bprf
      in Refl
    fold_constants_bexp_sound (BNot b) st | BEq _ _ =
      rewrite fold_constants_bexp_sound b st
      in rewrite sym bprf
      in Refl
    fold_constants_bexp_sound (BNot b) st | BLe _ _ =
      rewrite fold_constants_bexp_sound b st
      in rewrite sym bprf
      in Refl
    fold_constants_bexp_sound (BNot b) st | BNot _ =
      rewrite fold_constants_bexp_sound b st
      in rewrite sym bprf
      in Refl
    fold_constants_bexp_sound (BNot b) st | BAnd _ _ =
      rewrite fold_constants_bexp_sound b st
      in rewrite sym bprf
      in Refl
fold_constants_bexp_sound (BAnd b1 b2) st
  with (fold_constants_bexp b1) proof b1prf
    fold_constants_bexp_sound (BAnd b1 b2) st | BTrue =
      rewrite fold_constants_bexp_sound b1 st
      in rewrite sym b1prf
      in fold_constants_bexp_sound b2 st
    fold_constants_bexp_sound (BAnd b1 b2) st | BFalse =
      rewrite fold_constants_bexp_sound b1 st
      in rewrite sym b1prf
      in Refl
    fold_constants_bexp_sound (BAnd b1 b2) st | BEq _ _ =
      rewrite fold_constants_bexp_sound b1 st
      in rewrite sym b1prf
      in rewrite fold_constants_bexp_sound b2 st
      in Refl
    fold_constants_bexp_sound (BAnd b1 b2) st | BLe _ _ =
      rewrite fold_constants_bexp_sound b1 st
      in rewrite sym b1prf
      in rewrite fold_constants_bexp_sound b2 st
      in Refl
    fold_constants_bexp_sound (BAnd b1 b2) st | BNot _ =
      rewrite fold_constants_bexp_sound b1 st
      in rewrite sym b1prf
      in rewrite fold_constants_bexp_sound b2 st
      in Refl
    fold_constants_bexp_sound (BAnd b1 b2) st | BAnd _ _ =
      rewrite fold_constants_bexp_sound b1 st
      in rewrite sym b1prf
      in rewrite fold_constants_bexp_sound b2 st
      in Refl

fold_constants_com_sound : CTransSound EquivFoldConstants.fold_constants_com
fold_constants_com_sound CSkip st st' = refl_cequiv {c=CSkip} st st'
fold_constants_com_sound (CAss x e) st st' =
  let c_equiv = cAss_congruence (fold_constants_aexp_sound e)
  in c_equiv st st'
fold_constants_com_sound (CSeq c1 c2) st st' =
  let c_equiv = cSeq_congruence (fold_constants_com_sound c1)
                                (fold_constants_com_sound c2)
  in c_equiv st st'
fold_constants_com_sound (CIf b ct cf) st st'
  with (fold_constants_bexp b) proof bprf
    fold_constants_com_sound (CIf b ct cf) st st' | BTrue =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
      in trans_cequiv (test_true b_equiv) (fold_constants_com_sound ct) st st'
    fold_constants_com_sound (CIf b ct cf) st st' | BFalse =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
      in trans_cequiv (test_false b_equiv) (fold_constants_com_sound cf) st st'
    fold_constants_com_sound (CIf b ct cf) st st' | BEq _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
          ct_equiv = fold_constants_com_sound ct
          cf_equiv = fold_constants_com_sound cf
          cif_equiv = cIf_congruence b_equiv ct_equiv cf_equiv
      in cif_equiv st st'
    fold_constants_com_sound (CIf b ct cf) st st' | BLe _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                            (sym bprf) (fold_constants_bexp_sound b st1)
          ct_equiv = fold_constants_com_sound ct
          cf_equiv = fold_constants_com_sound cf
          cif_equiv = cIf_congruence b_equiv ct_equiv cf_equiv
      in cif_equiv st st'
    fold_constants_com_sound (CIf b ct cf) st st' | BNot _ =
      let b_equiv = \st1 =>
            replace {P=\x => beval st1 b = beval st1 x}
                    (sym bprf) (fold_constants_bexp_sound b st1)
          ct_equiv = fold_constants_com_sound ct
          cf_equiv = fold_constants_com_sound cf
          cif_equiv = cIf_congruence b_equiv ct_equiv cf_equiv
      in cif_equiv st st'
    fold_constants_com_sound (CIf b ct cf) st st' | BAnd _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
          ct_equiv = fold_constants_com_sound ct
          cf_equiv = fold_constants_com_sound cf
          cif_equiv = cIf_congruence b_equiv ct_equiv cf_equiv
      in cif_equiv st st'
fold_constants_com_sound (CIf1 b c) st st'
  with (fold_constants_bexp b) proof bprf
    fold_constants_com_sound (CIf1 b c) st st' | BTrue =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
      in trans_cequiv (if1_true b_equiv) (fold_constants_com_sound c) st st'
    fold_constants_com_sound (CIf1 b c) st st' | BFalse =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
      in if1_false b_equiv st st'
    fold_constants_com_sound (CIf1 b c) st st' | BEq _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
          cif1_equiv = cIf1_congruence b_equiv (fold_constants_com_sound c)
      in cif1_equiv st st'
    fold_constants_com_sound (CIf1 b c) st st' | BLe _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
          cif1_equiv = cIf1_congruence b_equiv (fold_constants_com_sound c)
      in cif1_equiv st st'
    fold_constants_com_sound (CIf1 b c) st st' | BNot _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
          cif1_equiv = cIf1_congruence b_equiv (fold_constants_com_sound c)
      in cif1_equiv st st'
    fold_constants_com_sound (CIf1 b c) st st' | BAnd _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
          cif1_equiv = cIf1_congruence b_equiv (fold_constants_com_sound c)
      in cif1_equiv st st'
fold_constants_com_sound (CWhile b c) st st'
  with (fold_constants_bexp b) proof bprf
    fold_constants_cwhile_sound (CWhile b c) st st' | BTrue =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
      in while_true b_equiv st st'
    fold_constants_cwhile_sound (CWhile b c) st st' | BFalse =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
      in while_false b_equiv st st'
    fold_constants_cwhile_sound (CWhile b c) st st' | BEq _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
          c_equiv = fold_constants_com_sound c
          while_equiv = cWhile_congruence b_equiv c_equiv
      in while_equiv st st'
    fold_constants_cwhile_sound (CWhile b c) st st' | BLe _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
          c_equiv = fold_constants_com_sound c
          while_equiv = cWhile_congruence b_equiv c_equiv
      in while_equiv st st'
    fold_constants_cwhile_sound (CWhile b c) st st' | BNot _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
          c_equiv = fold_constants_com_sound c
          while_equiv = cWhile_congruence b_equiv c_equiv
      in while_equiv st st'
    fold_constants_cwhile_sound (CWhile b c) st st' | BAnd _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (fold_constants_bexp_sound b st1)
          c_equiv = fold_constants_com_sound c
          while_equiv = cWhile_congruence b_equiv c_equiv
      in while_equiv st st'
fold_constants_com_sound (CFor init cond updt body) st st'
  with (fold_constants_bexp cond) proof cond_prf
    fold_constants_com_sound (CFor init cond updt body) st st' | BTrue =
      let cond_equiv = \st1 => cong {f=beval st1} (sym cond_prf)
          while_equiv = trans_cequiv
                          (trans_cequiv
                             (cFor_congruence
                                {cond1=fold_constants_bexp cond} {cond2=BTrue}
                                refl_cequiv cond_equiv refl_cequiv refl_cequiv)
                             for_while_equiv)
                          (cSeq_congruence (fold_constants_com_sound init)
                                           (while_true btrue_is_true))
          equiv = trans_cequiv (cFor_congruence
                                  refl_cequiv
                                  (fold_constants_bexp_sound cond)
                                  refl_cequiv
                                  refl_cequiv)
                                while_equiv
      in equiv st st'
    fold_constants_com_sound (CFor init cond updt body) st st' | BFalse =
      let cond_equiv = \st1 => cong {f=beval st1} (sym cond_prf)
          while_equiv = trans_cequiv
                          (trans_cequiv
                             (cFor_congruence
                                {cond1=fold_constants_bexp cond} {cond2=BFalse}
                                refl_cequiv cond_equiv refl_cequiv refl_cequiv)
                             for_while_equiv)
                          (cSeq_congruence (fold_constants_com_sound init)
                                           (while_false bfalse_is_false))
          equiv = trans_cequiv (cFor_congruence
                                  refl_cequiv
                                  (fold_constants_bexp_sound cond)
                                  refl_cequiv
                                  refl_cequiv)
                               (trans_cequiv while_equiv skip_right)
      in equiv st st'
    fold_constants_com_sound (CFor init cond updt body) st st' | BEq _ _ =
      let cond_equiv = trans_bequiv (fold_constants_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cFor_congruence (fold_constants_com_sound init)
                                  cond_equiv
                                  (fold_constants_com_sound updt)
                                  (fold_constants_com_sound body)
      in equiv st st'
    fold_constants_com_sound (CFor init cond updt body) st st' | BLe _ _ =
      let cond_equiv = trans_bequiv (fold_constants_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cFor_congruence (fold_constants_com_sound init)
                                  cond_equiv
                                  (fold_constants_com_sound updt)
                                  (fold_constants_com_sound body)
      in equiv st st'
    fold_constants_com_sound (CFor init cond updt body) st st' | BNot _ =
      let cond_equiv = trans_bequiv (fold_constants_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cFor_congruence (fold_constants_com_sound init)
                                  cond_equiv
                                  (fold_constants_com_sound updt)
                                  (fold_constants_com_sound body)
      in equiv st st'
    fold_constants_com_sound (CFor init cond updt body) st st' | BAnd _ _ =
      let cond_equiv = trans_bequiv (fold_constants_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cFor_congruence (fold_constants_com_sound init)
                                  cond_equiv
                                  (fold_constants_com_sound updt)
                                  (fold_constants_com_sound body)
      in equiv st st'
fold_constants_com_sound (CRepeat body cond) st st'
  with (fold_constants_bexp cond) proof cond_prf
    fold_constants_com_sound (CRepeat body cond) st st' | BTrue =
      let cond_equiv = trans_bequiv
                         (fold_constants_bexp_sound cond)
                         (\st1 => cong {f=beval st1} (sym cond_prf))
          while_equiv = trans_cequiv
                          (cRepeat_congruence (fold_constants_com_sound body)
                                              cond_equiv)
                          (trans_cequiv
                             repeat_while_equiv
                             (cSeq_congruence
                                refl_cequiv
                                (while_false bnot_btrue_is_bfalse)))
          equiv = trans_cequiv while_equiv skip_right
      in equiv st st'
    fold_constants_com_sound (CRepeat body cond) st st' | BFalse =
      let cond_equiv = trans_bequiv
                         (fold_constants_bexp_sound cond)
                         (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = trans_cequiv
                    (cRepeat_congruence (fold_constants_com_sound body)
                                        cond_equiv)
                    (trans_cequiv
                       repeat_while_equiv
                       (cSeq_congruence
                          refl_cequiv
                          (while_true bnot_bfalse_is_btrue)))
      in equiv st st'
    fold_constants_com_sound (CRepeat body cond) st st' | BEq _ _ =
      let cond_equiv = trans_bequiv (fold_constants_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cRepeat_congruence (fold_constants_com_sound body) cond_equiv
      in equiv st st'
    fold_constants_com_sound (CRepeat body cond) st st' | BLe _ _ =
      let cond_equiv = trans_bequiv (fold_constants_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cRepeat_congruence (fold_constants_com_sound body) cond_equiv
      in equiv st st'
    fold_constants_com_sound (CRepeat body cond) st st' | BNot _ =
      let cond_equiv = trans_bequiv (fold_constants_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cRepeat_congruence (fold_constants_com_sound body) cond_equiv
      in equiv st st'
    fold_constants_com_sound (CRepeat body cond) st st' | BAnd _ _ =
      let cond_equiv = trans_bequiv (fold_constants_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cRepeat_congruence (fold_constants_com_sound body) cond_equiv
      in equiv st st'


text:
module Main

import ContriverText.Tests

main : IO ()
main = testMain {f=FFI_C}

max_stars_repo_name: rocketnia/contrivertext

max_issues_repo_name: rocketnia/contrivertext

max_forks_repo_name: rocketnia/contrivertext


text:
module Test.Main

import Test.Basics
import Hedgehog

main : IO ()
main = test [ Basics.props
            ]


text:
module Main

import Erlang

-- Wrapper functions around Erlang functions

validCharlists : List ErlTerm
validCharlists =
  erlUnsafeCall (List ErlTerm) "test_support" "get_valid_charlists" []

invalidCharlists : List ErlTerm
invalidCharlists =
  erlUnsafeCall (List ErlTerm) "test_support" "get_invalid_charlists" []

validIOLists : List ErlTerm
validIOLists =
  erlUnsafeCall (List ErlTerm) "test_support" "get_valid_io_lists" []

invalidIOLists : List ErlTerm
invalidIOLists =
  erlUnsafeCall (List ErlTerm) "test_support" "get_invalid_io_lists" []

-- Helper functions

ioDataToString : ErlTerm -> String
ioDataToString x =
  erlUnsafeCall String "unicode" "characters_to_binary" [x]

-- Tests

testCharlists : IO ()
testCharlists = do
  putStrLn "testCharlists"
  printLn (map (erlDecodeMay charlist) validCharlists)
  printLn (map (erlDecodeMay charlist) invalidCharlists)

testIOLists : IO ()
testIOLists = do
  putStrLn "testIOLists"
  printLn (map (map ioDataToString . erlDecodeMay ioData) validIOLists)
  printLn (map (map ioDataToString . erlDecodeMay ioData) invalidIOLists)

main : IO ()
main = do
  testCharlists
  testIOLists


text:
module Web.Html

import JS
import public Web.Internal.Types
import public Web.Raw.Html as Html

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

export
Callback BlobCallback (Maybe Blob -> JSIO ()) where
  callback f = toBlobCallback $ runJS . f . nullableToMaybe

export
Callback CustomElementConstructor (IO HTMLElement) where
  callback = toCustomElementConstructor . const

export
Callback EventHandlerNonNull (Event -> JSIO ()) where
  callback f = toEventHandlerNonNull (map (toFFI . MkAny) . runJS . f)

export
Callback FunctionStringCallback (String -> JSIO ()) where
  callback f = toFunctionStringCallback (runJS . f)

export
Callback OnBeforeUnloadEventHandlerNonNull (Event -> JSIO (Maybe String)) where
  callback f = toOnBeforeUnloadEventHandlerNonNull $ map maybeToNullable
                                                   . runJSWithDefault Nothing
                                                   . f
export
Callback OnErrorEventHandlerNonNull (  NS I [Event, String]
                                    -> Optional String
                                    -> Optional Bits32
                                    -> Optional Bits32
                                    -> Optional Any
                                    -> JSIO Any
                                    ) where
  callback f = toOnErrorEventHandlerNonNull $ \u,b,c,d,e =>
                 map toFFI $ runJSWithDefault (MkAny ()) $
                   do ns <- tryFromFFI "JS.Html.ErrorEventHandlerNonNull.callback" u
                      f ns (undeforToOptional b)
                           (undeforToOptional c)
                           (undeforToOptional d)
                           (MkAny <$> undeforToOptional e)

export
Callback FocusEventHandler (FocusEvent -> JSIO ()) where
  callback f = toFocusEventHandler (runJS . f)

export
Callback InputEventHandler (InputEvent -> JSIO ()) where
  callback f = toInputEventHandler (runJS . f)

export
Callback KeyboardEventHandler (KeyboardEvent -> JSIO ()) where
  callback f = toKeyboardEventHandler (runJS . f)

export
Callback MouseEventHandler (MouseEvent -> JSIO ()) where
  callback f = toMouseEventHandler (runJS . f)

export
Callback UIEventHandler (UIEvent -> JSIO ()) where
  callback f = toUIEventHandler (runJS . f)

export
Callback WheelEventHandler (WheelEvent -> JSIO ()) where
  callback f = toWheelEventHandler (runJS . f)


text:
module Arduino.Mega

import Arduino.Boards

public export
Mega2560 : Board
Mega2560 = BoardLabel "mega" $ Just "atmega2560"

-- Lossy function for simplicity having that we know that our numbers do not exceed 255.
lossyNatToBits8 : Nat -> Bits8
lossyNatToBits8 = fromInteger . toIntegerNat

public export
data DigitalPinCondition : Pin -> Type where
  DD : (n : Nat) -> {auto ev : n `LTE` 53} -> DigitalPinCondition $ D n
  AA : (n : Nat) -> {auto ev : n `LTE` 15} -> DigitalPinCondition $ A n

public export
HasDigitalPins Mega2560 where
  CanBeDigital = DigitalPinCondition
  lowLevelNumberForDigitalPin (D n) = lossyNatToBits8 n
  lowLevelNumberForDigitalPin (A n) = lossyNatToBits8 $ n + 54

public export
HasBuiltIn_LED Mega2560 where
  LED = D 13
  Builtin_LED_IsDigital = DD _

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
module Data.Validated

import Data.List1

import Decidable.Equality

%default total

||| `Validated` is like an `Either` but accumulates all errors with semigroup operation.
public export
data Validated e a = Valid a | Invalid e

--- Instances of standard interfaces ---

public export
(Eq e, Eq a) => Eq (Validated e a) where
  Valid x   == Valid y   = x == y
  Invalid e == Invalid f = e == f
  _ == _ = False

export
(Show e, Show a) => Show (Validated e a) where
  showPrec d $ Valid   x = showCon d "Valid" $ showArg x
  showPrec d $ Invalid e = showCon d "Invalid" $ showArg e

public export
Functor (Validated e) where
  map f $ Valid x   = Valid $ f x
  map _ $ Invalid e = Invalid e

public export
Bifunctor Validated where
  bimap _ s $ Valid x   = Valid   $ s x
  bimap f _ $ Invalid e = Invalid $ f e

public export
Bifoldable Validated where
  bifoldr _ g acc (Valid a)   = g a acc
  bifoldr f _ acc (Invalid e) = f e acc

  bifoldl _ g acc (Valid a)   = g acc a
  bifoldl f _ acc (Invalid e) = f acc e

  binull _ = False

public export
Bitraversable Validated where
  bitraverse _ g (Valid a)   = Valid <$> g a
  bitraverse f _ (Invalid e) = Invalid <$> f e

||| Applicative composition preserves invalidity sequentially accumulating all errors.
public export
Semigroup e => Applicative (Validated e) where
  pure = Valid

  Valid f    <*> Valid x    = Valid $ f x
  Invalid e1 <*> Invalid e2 = Invalid $ e1 <+> e2
  Invalid e  <*> Valid _    = Invalid e
  Valid _    <*> Invalid e  = Invalid e

-- There is no `Monad` implementation because it can't be coherent with the accumulating `Applicative` one.

||| Semigroup operation selects the leftmost valid value.
||| If both sides are invalid, errors are accumulated.
public export
Semigroup e => Semigroup (Validated e a) where
  l@(Valid _) <+> _           = l
  _           <+> r@(Valid _) = r
  Invalid e1  <+> Invalid e2  = Invalid $ e1 <+> e2

public export
Monoid e => Monoid (Validated e a) where
  neutral = Invalid neutral

||| Alternative composition preserves validity selecting the leftmost valid value.
||| If both sides are invalid, errors are accumulated.
public export
Monoid e => Alternative (Validated e) where
  empty = neutral
  l@(Valid _) <|> _           = l
  _           <|> r@(Valid _) = r
  Invalid e1  <|> Invalid e2  = Invalid $ e1 <+> e2

public export
Foldable (Validated e) where
  foldr op init $ Valid x   = x `op` init
  foldr _  init $ Invalid _ = init

  foldl op init $ Valid x   = init `op` x
  foldl _  init $ Invalid _ = init

  null $ Valid _   = False
  null $ Invalid _ = True

public export
Traversable (Validated e) where
  traverse f $ Valid x   = Valid <$> f x
  traverse _ $ Invalid e = pure $ Invalid e

public export
Semigroup e => Zippable (Validated e) where
  zipWith f (Valid l)   (Valid r)   = Valid $ f l r
  zipWith _ (Valid _)   (Invalid r) = Invalid r
  zipWith _ (Invalid l) (Valid _)   = Invalid l
  zipWith _ (Invalid l) (Invalid r) = Invalid $ l <+> r

  zipWith3 f (Valid x)   (Valid y)   (Valid z)   = Valid $ f x y z
  zipWith3 _ (Valid _)   (Valid _)   (Invalid z) = Invalid z
  zipWith3 _ (Valid _)   (Invalid y) (Valid _)   = Invalid y
  zipWith3 _ (Valid _)   (Invalid y) (Invalid z) = Invalid $ y <+> z
  zipWith3 _ (Invalid x) (Valid _)   (Valid _)   = Invalid x
  zipWith3 _ (Invalid x) (Valid _)   (Invalid z) = Invalid $ x <+> z
  zipWith3 _ (Invalid x) (Invalid y) (Valid _)   = Invalid $ x <+> y
  zipWith3 _ (Invalid x) (Invalid y) (Invalid z) = Invalid $ x <+> y <+> z

  unzipWith f (Valid x)   = let (a, b) = f x in (Valid a, Valid b)
  unzipWith _ (Invalid e) = (Invalid e, Invalid e)

  unzipWith3 f (Valid x)   = let (a, b, c) = f x in (Valid a, Valid b, Valid c)
  unzipWith3 _ (Invalid e) = (Invalid e, Invalid e, Invalid e)

public export
Uninhabited (Valid x = Invalid e) where
  uninhabited Refl impossible

public export
Uninhabited (Invalid e = Valid x) where
  uninhabited Refl impossible

public export
(DecEq e, DecEq a) => DecEq (Validated e a) where
  decEq (Valid x) (Invalid y) = No uninhabited
  decEq (Invalid x) (Valid y) = No uninhabited
  decEq (Valid x) (Valid y) with (decEq x y)
    decEq (Valid _) (Valid _) | Yes p = rewrite p in Yes Refl
    decEq (Valid _) (Valid _) | No up = No $ \case Refl => up Refl
  decEq (Invalid x) (Invalid y) with (decEq x y)
    decEq (Invalid _) (Invalid _) | Yes p = rewrite p in Yes Refl
    decEq (Invalid _) (Invalid _) | No up = No $ \case Refl => up Refl

--- Convenience representations ---

||| Special case of `Validated` with a `List` as an error accumulator.
public export %inline
ValidatedL : Type -> Type -> Type
ValidatedL = Validated . List1

public export %inline
oneInvalid : Applicative f => e -> Validated (f e) a
oneInvalid = Invalid . pure

--- Conversions to and from `Either` ---

public export %inline
fromEither : Either e a -> Validated e a
fromEither $ Right x = Valid x
fromEither $ Left  e = Invalid e

public export %inline
fromEitherL : Either e a -> ValidatedL e a
fromEitherL $ Right x = Valid x
fromEitherL $ Left  e = oneInvalid e

public export %inline
toEither : Validated e a -> Either e a
toEither $ Valid   x = Right x
toEither $ Invalid e = Left e

--- Conversions to and from `Maybe` ---

public export %inline
fromMaybe : Monoid e => Maybe a -> Validated e a
fromMaybe $ Just x  = Valid x
fromMaybe $ Nothing = empty

public export %inline
toMaybe : Validated e a -> Maybe a
toMaybe $ Valid x   = Just x
toMaybe $ Invalid _ = Nothing

--- Property of being valid ---

public export
data IsValid : Validated e a -> Type where
  ItIsValid : IsValid $ Valid x

export
Uninhabited (IsValid $ Invalid e) where
  uninhabited ItIsValid impossible

public export
isItValid : (v : Validated e a) -> Dec (IsValid v)
isItValid $ Valid _   = Yes ItIsValid
isItValid $ Invalid _ = No absurd