text:
module Core.AutoSearch

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Normalise
import Core.TT
import Core.Unify
import Core.Value

import Data.Bool.Extra
import Data.Either
import Data.List
import Data.Maybe

%default covering

SearchEnv : List Name -> Type
SearchEnv vars = List (NF vars, Closure vars)

searchType : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             FC -> RigCount ->
             (defaults : Bool) -> (trying : List (Term vars)) ->
             (depth : Nat) ->
             (defining : Name) ->
             (checkDets : Bool) -> (topTy : ClosedTerm) ->
             Env Term vars -> (target : Term vars) -> Core (Term vars)

public export
record ArgInfo (vars : List Name) where
  constructor MkArgInfo
  holeID : Int
  argRig : RigCount
  plicit : PiInfo (NF vars)
  metaApp : Term vars
  argType : Term vars

export
mkArgs : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         FC -> RigCount ->
         Env Term vars -> NF vars ->
         Core (List (ArgInfo vars), NF vars)
mkArgs fc rigc env (NBind nfc x (Pi fc' c p ty) sc)
    = do defs <- get Ctxt
         empty <- clearDefs defs
         nm <- genName "sa"
         argTy <- quote empty env ty
         let argRig = rigMult rigc c
         (idx, arg) <- newMeta fc' argRig env nm argTy
                               (Hole (length env) (holeInit False)) False
         setInvertible fc (Resolved idx)
         (rest, restTy) <- mkArgs fc rigc env
                              !(sc defs (toClosure defaultOpts env arg))
         pure (MkArgInfo idx argRig p arg argTy :: rest, restTy)
mkArgs fc rigc env ty = pure ([], ty)

export
impLast : List (ArgInfo vars) -> List (ArgInfo vars)
impLast xs = filter (not . impl) xs ++ filter impl xs
  where
      impl : ArgInfo vs -> Bool
      impl inf
          = case plicit inf of
                 Explicit => False
                 _ => True

searchIfHole : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               FC ->
               (defaults : Bool) -> List (Term vars) ->
               (ispair : Bool) -> (depth : Nat) ->
               (defining : Name) -> (topTy : ClosedTerm) -> Env Term vars ->
               (arg : ArgInfo vars) ->
               Core ()
searchIfHole fc defaults trying ispair Z def top env arg
    = throw (CantSolveGoal fc [] top) -- possibly should say depth limit hit?
searchIfHole fc defaults trying ispair (S depth) def top env arg
    = do let hole = holeID arg
         let rig = argRig arg

         defs <- get Ctxt
         Just gdef <- lookupCtxtExact (Resolved hole) (gamma defs)
              | Nothing => throw (CantSolveGoal fc [] top)
         let Hole _ _ = definition gdef
              | _ => pure () -- already solved
         top' <- if ispair
                    then normaliseScope defs [] (type gdef)
                    else pure top

         argdef <- searchType fc rig defaults trying depth def False top' env
                              !(normaliseScope defs env (argType arg))
         logTermNF "auto" 5 "Solved arg" env argdef
         logTermNF "auto" 5 "Arg meta" env (metaApp arg)
         ok <- solveIfUndefined env (metaApp arg) argdef
         if ok
            then pure ()
            else do vs <- unify inTerm fc env (metaApp arg) argdef
                    let [] = constraints vs
                        | _ => throw (CantSolveGoal fc [] top)
                    pure ()

successful : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             List (Core (Term vars)) ->
             Core (List (Either Error (Term vars, Defs, UState)))
successful [] = pure []
successful (elab :: elabs)
    = do ust <- get UST
         defs <- branch
         catch (do -- Run the elaborator
                   res <- elab
                   -- Record post-elaborator state
                   ust' <- get UST
                   defs' <- get Ctxt
                   -- Reset to previous state and try the rest
                   put UST ust
                   put Ctxt defs
                   elabs' <- successful elabs
                   -- Record success, and the state we ended at
                   pure (Right (res, defs', ust') :: elabs'))
               (\err => do put UST ust
                           put Ctxt defs
                           elabs' <- successful elabs
                           pure (Left err :: elabs'))

anyOne : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         FC -> Env Term vars -> (topTy : ClosedTerm) ->
         List (Core (Term vars)) ->
         Core (Term vars)
anyOne fc env top [] = throw (CantSolveGoal fc [] top)
anyOne fc env top [elab]
    = catch elab
         (\err => case err of
                       CantSolveGoal _ _ _ => throw err
                       _ => throw (CantSolveGoal fc [] top))
anyOne fc env top (elab :: elabs)
    = tryUnify elab (anyOne fc env top elabs)

exactlyOne : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             FC -> Env Term vars -> (topTy : ClosedTerm) -> (target : NF vars) ->
             List (Core (Term vars)) ->
             Core (Term vars)
exactlyOne fc env top target [elab]
    = catch elab
         (\err => case err of
                       CantSolveGoal _ _ _ => throw err
                       _ => throw (CantSolveGoal fc [] top))
exactlyOne {vars} fc env top target all
    = do elabs <- successful all
         case rights elabs of
              [(res, defs, ust)] =>
                    do put UST ust
                       put Ctxt defs
                       commit
                       pure res
              [] => throw (CantSolveGoal fc [] top)
              rs => throw (AmbiguousSearch fc env !(quote !(get Ctxt) env target)
                             !(traverse normRes rs))
  where
    normRes : (Term vars, Defs, UState) -> Core (Term vars)
    normRes (tm, defs, _) = normaliseHoles defs env tm

-- We can only resolve things which are at any multiplicity. Expression
-- search happens before linearity checking and we can't guarantee that just
-- because something is apparently available now, it will be available by the
-- time we get to linearity checking.
-- It's also fine to use anything if we're working at multiplicity 0
getAllEnv : FC -> RigCount ->
            SizeOf done ->
            Env Term vars ->
            List (Term (done ++ vars), Term (done ++ vars))
getAllEnv fc rigc p [] = []
getAllEnv {vars = v :: vs} {done} fc rigc p (b :: env)
   = let rest = getAllEnv fc rigc (sucR p) env in
         if multiplicity b == top || isErased rigc
            then let MkVar var = weakenVar p (MkVar First) in
                     (Local (binderLoc b) Nothing _ var,
                       rewrite appendAssociative done [v] vs in
                          weakenNs (sucR p) (binderType b)) ::
                               rewrite appendAssociative done [v] vs in rest
            else rewrite appendAssociative done [v] vs in rest

-- A local is usable if it contains no holes in a determining argument position
usableLocal : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              FC -> (defaults : Bool) ->
              Env Term vars -> (locTy : NF vars) -> Core Bool
-- pattern variables count as concrete things!
usableLocal loc defaults env (NApp fc (NMeta (PV _ _) _ _) args)
    = pure True
usableLocal loc defaults env (NApp fc (NMeta _ _ _) args)
    = pure False
usableLocal {vars} loc defaults env (NTCon _ n _ _ args)
    = do sd <- getSearchData loc (not defaults) n
         usableLocalArg 0 (detArgs sd) args
  -- usable if none of the determining arguments of the local's type are
  -- holes
  where
    usableLocalArg : Nat -> List Nat -> List (Closure vars) -> Core Bool
    usableLocalArg i dets [] = pure True
    usableLocalArg i dets (c :: cs)
        = if i `elem` dets
             then do defs <- get Ctxt
                     u <- usableLocal loc defaults env !(evalClosure defs c)
                     if u
                        then usableLocalArg (1 + i) dets cs
                        else pure False
             else usableLocalArg (1 + i) dets cs
usableLocal loc defaults env (NDCon _ n _ _ args)
    = do defs <- get Ctxt
         us <- traverse (usableLocal loc defaults env)
                        !(traverse (evalClosure defs) args)
         pure (allTrue us)
usableLocal loc defaults env (NApp _ (NLocal _ _ _) args)
    = do defs <- get Ctxt
         us <- traverse (usableLocal loc defaults env)
                        !(traverse (evalClosure defs) args)
         pure (allTrue us)
usableLocal loc defaults env (NBind fc x (Pi _ _ _ _) sc)
    = do defs <- get Ctxt
         usableLocal loc defaults env
                !(sc defs (toClosure defaultOpts env (Erased fc False)))
usableLocal loc defaults env (NErased _ _) = pure False
usableLocal loc _ _ _ = pure True

searchLocalWith : {vars : _} ->
                  {auto c : Ref Ctxt Defs} ->
                  {auto u : Ref UST UState} ->
                  FC -> RigCount ->
                  (defaults : Bool) -> List (Term vars) ->
                  (depth : Nat) ->
                  (defining : Name) -> (topTy : ClosedTerm) ->
                  Env Term vars -> (Term vars, Term vars) ->
                  (target : NF vars) -> Core (Term vars)
searchLocalWith {vars} fc rigc defaults trying depth def top env (prf, ty) target
    = do defs <- get Ctxt
         nty <- nf defs env ty
         findPos defs prf id nty target
  where
    ambig : Error -> Bool
    ambig (AmbiguousSearch _ _ _ _) = True
    ambig _ = False

    clearEnvType : {idx : Nat} -> (0 p : IsVar name idx vs) ->
                   FC -> Env Term vs -> Env Term vs
    clearEnvType First fc (b :: env)
        = Lam (binderLoc b) (multiplicity b) Explicit (Erased fc False) :: env
    clearEnvType (Later p) fc (b :: env) = b :: clearEnvType p fc env

    clearEnv : Term vars -> Env Term vars -> Env Term vars
    clearEnv (Local fc _ idx p) env
        = clearEnvType p fc env
    clearEnv _ env = env

    findDirect : Defs -> Term vars ->
                 (Term vars -> Term vars) ->
                 NF vars ->  -- local's type
                 (target : NF vars) ->
                 Core (Term vars)
    findDirect defs p f ty target
        = do (args, appTy) <- mkArgs fc rigc env ty
             logNF "auto" 10 "Trying" env ty
             logNF "auto" 10 "For target" env target
             ures <- unify inTerm fc env target appTy
             let [] = constraints ures
                 | _ => throw (CantSolveGoal fc [] top)
             -- We can only use the local if its type is not an unsolved hole
             if !(usableLocal fc defaults env ty)
                then do
                   let candidate = apply fc (f prf) (map metaApp args)
                   logTermNF "auto" 10 "Local var candidate " env candidate
                   -- Clear the local from the environment to avoid getting
                   -- into a loop repeatedly applying it
                   let env' = clearEnv prf env
                   -- Work right to left, because later arguments may solve
                   -- earlier ones by unification
                   traverse (searchIfHole fc defaults trying False depth def top env')
                            (impLast args)
                   pure candidate
                else do logNF "auto" 10 "Can't use " env ty
                        throw (CantSolveGoal fc [] top)

    findPos : Defs -> Term vars ->
              (Term vars -> Term vars) ->
              NF vars ->  -- local's type
              (target : NF vars) ->
              Core (Term vars)
    findPos defs p f nty@(NTCon pfc pn _ _ [xty, yty]) target
        = handleUnify (findDirect defs prf f nty target) (\e =>
           if ambig e then throw e else
             do fname <- maybe (throw (CantSolveGoal fc [] top))
                               pure
                               !fstName
                sname <- maybe (throw (CantSolveGoal fc [] top))
                               pure
                               !sndName
                if !(isPairType pn)
                   then do empty <- clearDefs defs
                           xtytm <- quote empty env xty
                           ytytm <- quote empty env yty
                           exactlyOne fc env top target
                            [(do xtynf <- evalClosure defs xty
                                 findPos defs p
                                     (\arg => apply fc (Ref fc Func fname)
                                                        [xtytm,
                                                         ytytm,
                                                         f arg])
                                     xtynf target),
                             (do ytynf <- evalClosure defs yty
                                 findPos defs p
                                     (\arg => apply fc (Ref fc Func sname)
                                                        [xtytm,
                                                         ytytm,
                                                         f arg])
                                     ytynf target)]
                   else throw (CantSolveGoal fc [] top))
    findPos defs p f nty target
        = findDirect defs p f nty target

searchLocal : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount ->
              (defaults : Bool) -> List (Term vars) ->
              (depth : Nat) ->
              (defining : Name) -> (topTy : ClosedTerm) ->
              Env Term vars ->
              (target : NF vars) -> Core (Term vars)
searchLocal fc rig defaults trying depth def top env target
    = let elabs = map (\t => searchLocalWith fc rig defaults trying depth def
                                             top env t target)
                      (getAllEnv fc rig zero env) in
          exactlyOne fc env top target elabs

isPairNF : {auto c : Ref Ctxt Defs} ->
           Env Term vars -> NF vars -> Defs -> Core Bool
isPairNF env (NTCon _ n _ _ _) defs
    = isPairType n
isPairNF env (NBind fc b (Pi _ _ _ _) sc) defs
    = isPairNF env !(sc defs (toClosure defaultOpts env (Erased fc False))) defs
isPairNF _ _ _ = pure False

searchName : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             FC -> RigCount ->
             (defaults : Bool) -> List (Term vars) ->
             (depth : Nat) ->
             (defining : Name) -> (topTy : ClosedTerm) ->
             Env Term vars -> (target : NF vars) ->
             (Name, GlobalDef) ->
             Core (Term vars)
searchName fc rigc defaults trying depth def top env target (n, ndef)
    = do defs <- get Ctxt
         when (not (visibleInAny (!getNS :: !getNestedNS)
                                 (fullname ndef) (visibility ndef))) $
            throw (CantSolveGoal fc [] top)
         when (BlockedHint `elem` flags ndef) $
            throw (CantSolveGoal fc [] top)

         let ty = type ndef
         let namety : NameType
                 = case definition ndef of
                        DCon tag arity _ => DataCon tag arity
                        TCon tag arity _ _ _ _ _ _ => TyCon tag arity
                        _ => Func
         nty <- nf defs env (embed ty)
         logNF "auto" 10 ("Searching Name " ++ show n) env nty
         (args, appTy) <- mkArgs fc rigc env nty
         ures <- unify inTerm fc env target appTy
         let [] = constraints ures
             | _ => throw (CantSolveGoal fc [] top)
         ispair <- isPairNF env nty defs
         let candidate = apply fc (Ref fc namety n) (map metaApp args)
         logTermNF "auto" 10 "Candidate " env candidate
         -- Work right to left, because later arguments may solve earlier
         -- dependencies by unification
         traverse (searchIfHole fc defaults trying ispair depth def top env)
                  (impLast args)
         pure candidate

searchNames : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount ->
              (defaults : Bool) -> List (Term vars) ->
              (depth : Nat) ->
              (defining : Name) -> (topTy : ClosedTerm) ->
              Env Term vars -> Bool -> List Name ->
              (target : NF vars) -> Core (Term vars)
searchNames fc rigc defaults trying depth defining topty env ambig [] target
    = throw (CantSolveGoal fc [] topty)
searchNames fc rigc defaults trying depth defining topty env ambig (n :: ns) target
    = do defs <- get Ctxt
         visnsm <- traverse (visible (gamma defs) (currentNS defs :: nestedNS defs)) (n :: ns)
         let visns = mapMaybe id visnsm
         let elabs = map (searchName fc rigc defaults trying depth defining topty env target) visns
         if ambig
            then anyOne fc env topty elabs
            else exactlyOne fc env topty target elabs
  where
    visible : Context ->
              List Namespace -> Name -> Core (Maybe (Name, GlobalDef))
    visible gam nspace n
        = do Just def <- lookupCtxtExact n gam
                  | Nothing => pure Nothing
             if visibleInAny nspace n (visibility def)
                then pure $ Just (n, def)
                else pure $ Nothing

concreteDets : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               FC -> Bool ->
               Env Term vars -> (top : ClosedTerm) ->
               (pos : Nat) -> (dets : List Nat) ->
               (args : List (Closure vars)) ->
               Core ()
concreteDets fc defaults env top pos dets [] = pure ()
concreteDets {vars} fc defaults env top pos dets (arg :: args)
    = if not (pos `elem` dets)
         then concreteDets fc defaults env top (1 + pos) dets args
         else do defs <- get Ctxt
                 argnf <- evalClosure defs arg
                 concrete defs argnf True
                 concreteDets fc defaults env top (1 + pos) dets args
  where
    drop : Nat -> List Nat -> List t -> List t
    drop i ns [] = []
    drop i ns (x :: xs)
        = if i `elem` ns
             then x :: drop (1+i) ns xs
             else drop (1+i) ns xs

    concrete : Defs -> NF vars -> (atTop : Bool) -> Core ()
    concrete defs (NBind nfc x b sc) atTop
        = do scnf <- sc defs (toClosure defaultOpts env (Erased nfc False))
             concrete defs scnf False
    concrete defs (NTCon nfc n t a args) atTop
        = do sd <- getSearchData nfc False n
             let args' = drop 0 (detArgs sd) args
             traverse (\ parg => do argnf <- evalClosure defs parg
                                    concrete defs argnf False) args'
             pure ()
    concrete defs (NDCon nfc n t a args) atTop
        = do traverse (\ parg => do argnf <- evalClosure defs parg
                                    concrete defs argnf False) args
             pure ()
    concrete defs (NApp _ (NMeta n i _) _) True
        = do Just (Hole _ b) <- lookupDefExact n (gamma defs)
                  | _ => throw (DeterminingArg fc n i [] top)
             when (not (implbind b)) $
                  throw (DeterminingArg fc n i [] top)
             pure ()
    concrete defs (NApp _ (NMeta n i _) _) False
        = do Just (Hole _ b) <- lookupDefExact n (gamma defs)
                  | def => throw (CantSolveGoal fc [] top)
             when (not (implbind b)) $
                  throw (CantSolveGoal fc [] top)
             pure ()
    concrete defs tm atTop = pure ()

checkConcreteDets : {vars : _} ->
                    {auto c : Ref Ctxt Defs} ->
                    {auto u : Ref UST UState} ->
                    FC -> Bool ->
                    Env Term vars -> (top : ClosedTerm) ->
                    NF vars ->
                    Core ()
checkConcreteDets fc defaults env top (NTCon tfc tyn t a args)
    = do defs <- get Ctxt
         if !(isPairType tyn)
            then case args of
                      [aty, bty] =>
                          do anf <- evalClosure defs aty
                             bnf <- evalClosure defs bty
                             checkConcreteDets fc defaults env top anf
                             checkConcreteDets fc defaults env top bnf
                      _ => do sd <- getSearchData fc defaults tyn
                              concreteDets fc defaults env top 0 (detArgs sd) args
            else
              do sd <- getSearchData fc defaults tyn
                 log "auto" 10 $ "Determining arguments for " ++ show !(toFullNames tyn)
                              ++ " " ++ show (detArgs sd)
                 concreteDets fc defaults env top 0 (detArgs sd) args
checkConcreteDets fc defaults env top _
    = pure ()

abandonIfCycle : {vars : _} ->
                 {auto c : Ref Ctxt Defs} ->
                 Env Term vars -> Term vars -> List (Term vars) ->
                 Core ()
abandonIfCycle env tm [] = pure ()
abandonIfCycle env tm (ty :: tys)
    = do defs <- get Ctxt
         if !(convert defs env tm ty)
            then throw (InternalError "Cycle in search")
            else abandonIfCycle env tm tys

-- Declared at the top
searchType fc rigc defaults trying depth def checkdets top env (Bind nfc x b@(Pi fc' c p ty) sc)
    = pure (Bind nfc x (Lam fc' c p ty)
             !(searchType fc rigc defaults [] depth def checkdets top
                          (b :: env) sc))
searchType fc rigc defaults trying depth def checkdets top env (Bind nfc x b@(Let fc' c val ty) sc)
    = pure (Bind nfc x b
             !(searchType fc rigc defaults [] depth def checkdets top
                          (b :: env) sc))
searchType {vars} fc rigc defaults trying depth def checkdets top env target
    = do defs <- get Ctxt
         abandonIfCycle env target trying
         let trying' = target :: trying
         nty <- nf defs env target
         case nty of
              NTCon tfc tyn t a args =>
                  if a == length args
                     then do logNF "auto" 10 "Next target" env nty
                             sd <- getSearchData fc defaults tyn
                             -- Check determining arguments are okay for 'args'
                             when checkdets $
                                 checkConcreteDets fc defaults env top
                                                   (NTCon tfc tyn t a args)
                             if defaults && checkdets
                                then tryGroups Nothing nty (hintGroups sd)
                                else handleUnify
                                       (searchLocal fc rigc defaults trying' depth def top env nty)
                                       (\e => if ambig e
                                                 then throw e
                                                 else tryGroups Nothing nty (hintGroups sd))
                     else throw (CantSolveGoal fc [] top)
              _ => do logNF "auto" 10 "Next target: " env nty
                      searchLocal fc rigc defaults trying' depth def top env nty
  where
    ambig : Error -> Bool
    ambig (AmbiguousSearch _ _ _ _) = True
    ambig _ = False

    -- Take the earliest error message (that's when we look inside pairs,
    -- typically, and it's best to be more precise)
    tryGroups : Maybe Error ->
                NF vars -> List (Bool, List Name) -> Core (Term vars)
    tryGroups (Just err) nty [] = throw err
    tryGroups Nothing nty [] = throw (CantSolveGoal fc [] top)
    tryGroups merr nty ((ambigok, g) :: gs)
        = handleUnify
             (do logC "auto" 5
                        (do gn <- traverse getFullName g
                            pure ("Search: Trying " ++ show (length gn) ++
                                           " names " ++ show gn))
                 logNF "auto" 5 "For target" env nty
                 searchNames fc rigc defaults (target :: trying) depth def top env ambigok g nty)
             (\err => if ambig err then throw err
                         else tryGroups (Just $ fromMaybe err merr) nty gs)

-- Declared in Core.Unify as:
-- search : {vars : _} -
--          {auto c : Ref Ctxt Defs} ->
--          {auto u : Ref UST UState} ->
--          FC -> RigCount ->
--          (defaults : Bool) -> (depth : Nat) ->
--          (defining : Name) -> (topTy : Term vars) -> Env Term vars ->
--          Core (Term vars)
Core.Unify.search fc rigc defaults depth def top env
    = do defs <- get Ctxt
         logTermNF "auto" 3 "Initial target: " env top
         log "auto" 3 $ "Running search with defaults " ++ show defaults
         tm <- searchType fc rigc defaults [] depth def
                          True (abstractEnvType fc env top) env
                          top
         logTermNF "auto" 3 "Result" env tm
         defs <- get Ctxt
         pure tm


text:
module Libraries.Data.IMaybe

%default total

public export
data IMaybe : Bool -> Type -> Type where
  Nothing : IMaybe False a
  Just : a -> IMaybe True a

export
Functor (IMaybe b) where
  map f Nothing = Nothing
  map f (Just x) = Just (f x)

export
fromJust : IMaybe True a -> a
fromJust (Just x) = x

ext: idr


text:
||| Stuff that goes wrong.
|||
||| Module    : Error.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
module Circuits.Idealised.Error

import Toolkit.Text.Parser.Run
import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Graph.EdgeBounded.HasExactDegree.All
import Toolkit.Data.Whole
import Toolkit.Data.Location
import Toolkit.Data.DList

import Toolkit.Data.List.AtIndex
import Toolkit.DeBruijn.Context.Item
import Toolkit.DeBruijn.Context
import Toolkit.DeBruijn.Renaming

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

%default total

namespace Check

  namespace FreeVar
    public export
    data LookupFail = NotFound String
                    | IsUsed String

  public export
  data FailingEdgeCase = InvalidSplit Nat Nat Nat Nat
                       | InvalidEdge  Nat Nat Nat

  public export
  data Error = Mismatch Ty Ty
             | ElemFail String (Exists.Error ())
             | PortExpected Direction
             | VectorExpected
             | VectorTooShort
             | VectorSizeMismatch Whole Whole Whole
             | LinearityError (Context (Ty,Usage) types)
             | Err FileContext Check.Error
             | NotEdgeCase FailingEdgeCase
             | MismatchGate DType DType

namespace Idealised

  public export
  data Error = TyCheck Check.Error
             | Parse   String (ParseError Token)
             | Sound   (Graph String) (HasExactDegree.Error String)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
import Data.List.Views

total
merge_sort : Ord a => List a -> List a
merge_sort xs with (splitRec xs)
  merge_sort [] | SplitRecNil = []
  merge_sort [x] | SplitRecOne = [x]
  merge_sort (lefts ++ rights) | (SplitRecPair lrec rrec)
    = merge (merge_sort lefts | lrec) (merge_sort rights | rrec)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Control.Permutation.Proofs

import Control.Permutation.Mod

%access export
%default total

||| Proof that (n + 1)! >= n!
private
factorialIncr : (n : Nat) -> LTE (factorial n) (factorial (S n))
factorialIncr Z = lteRefl
factorialIncr n = lteAddRight (factorial n)

||| Proof that n! >= 1
export
factorialLTE : (n : Nat) -> LTE 1 (factorial n)
factorialLTE Z = lteRefl
factorialLTE (S k) = lteTransitive (factorialLTE k) (factorialIncr k)

max_stars_repo_name: marcosh/permutations

max_issues_repo_name: marcosh/permutations

max_forks_repo_name: marcosh/permutations


text:
> module SequentialDecisionProblems.StochasticDefaults

> -- import Data.List
> -- import Data.List.Quantifiers

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.Utils

> import SimpleProb.SimpleProb
> import SimpleProb.MonadicOperations
> import SimpleProb.MonadicProperties
> -- import List.Operations
> -- import List.Properties

> %default total
> %auto_implicits off

In stochastic SDPs, |M = SimpleProb|:

> SequentialDecisionProblems.CoreTheory.M =
>   SimpleProb

Thus, |M| is a functor:

> SequentialDecisionProblems.CoreTheory.fmap =
>   SimpleProb.MonadicOperations.fmap

, |M| is a monad:

> SequentialDecisionProblems.Utils.ret =
>   SimpleProb.MonadicOperations.ret

> SequentialDecisionProblems.Utils.bind =
>   SimpleProb.MonadicOperations.bind

Moreover, |M| is a container monad

> SequentialDecisionProblems.CoreTheory.Elem =
>   SimpleProb.MonadicOperations.Elem

> SequentialDecisionProblems.CoreTheory.NotEmpty =
>   SimpleProb.MonadicOperations.NonEmpty

> SequentialDecisionProblems.CoreTheory.All =
>   SimpleProb.MonadicOperations.All

> SequentialDecisionProblems.CoreTheory.elemNotEmptySpec0 =
>   SimpleProb.MonadicProperties.elemNonEmptySpec0

> SequentialDecisionProblems.CoreTheory.elemNotEmptySpec1 =
>   SimpleProb.MonadicProperties.elemNonEmptySpec1

> SequentialDecisionProblems.CoreTheory.tagElem =
>   SimpleProb.MonadicOperations.tagElem

> SequentialDecisionProblems.CoreTheory.allElemSpec0 =
>   SimpleProb.MonadicProperties.containerMonadSpec3

and |All| and |NotEmpty| are finite and decidable:

> SequentialDecisionProblems.Utils.finiteAll =
>   SimpleProb.MonadicProperties.finiteAll

> SequentialDecisionProblems.Utils.finiteNotEmpty =
>   SimpleProb.MonadicProperties.finiteNonEmpty

> SequentialDecisionProblems.Utils.decidableAll =
>   SimpleProb.MonadicProperties.decidableAll

> SequentialDecisionProblems.Utils.decidableNotEmpty =
>   SimpleProb.MonadicProperties.decidableNonEmpty

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Commons.Data.Location

%default total
%access public export

record Location where
  constructor MkLoc
  source : Maybe String
  line   : Nat
  col    : Nat

record FileContext where
  constructor MkFC
  source : Maybe String
  start  : Location
  end    : Location

export
newFC : Maybe String -> Location -> Location -> FileContext
newFC n s e = MkFC n (record {source = n} s) (record {source = n} e)

namespace FromCoords
  export
  newLoc : Maybe String -> (Nat, Nat) -> Location
  newLoc n (l,c) = MkLoc n l c

  export
  newFC : Maybe String -> (Nat, Nat) -> (Nat, Nat) -> FileContext
  newFC n s e = newFC n (newLoc n s) (newLoc n e)

namespace Anon

  export
  newLoc : (Nat, Nat) -> Location
  newLoc (l,c) = MkLoc Nothing l c

  export
  newFC : Location -> Location -> FileContext
  newFC s e = newFC Nothing s e

export
emptyFC : FileContext
emptyFC = newFC Nothing (0,0) (0,0)

Show Location where
  show (MkLoc Nothing  l c) = with List concat [show l, ":", show c]
  show (MkLoc (Just n) l c) = with List concat [n, ":", show l, ":", show c]

Show FileContext where
  show (MkFC Nothing (MkLoc _ l scol) (MkLoc _ _ ecol)) = with List concat ["global:", show l, ":", show scol, "-", show ecol, ":"]
  show (MkFC (Just x) (MkLoc _ l scol) (MkLoc _ _ ecol)) = with List concat [x, ":", show l, ":", show scol, "-", show ecol, ":"]

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Control.Monad.State

import public Control.Monad.Identity -- left here for compatibility
import public Control.Monad.Trans -- left here for compatibility
import public Control.Monad.State.Interface as Control.Monad.State
import public Control.Monad.State.State as Control.Monad.State


text:
module Replica

import Data.List
import Data.Strings

import System
import System.Directory
import System.File
import System.Info

import Replica.TestConfig
import Replica.RunEnv

%default total

public export
data TestResult
  = Success
  | Failure (Maybe String) String
  | NewGolden String

public export
data TestError
  = CantLocateDir String
  | CantReadOutput FileError
  | CantParseTest (ParsingError BuildError)
  | CantReadExpected FileError
  | CantWriteNewGolden
  | CommandFailed Int

expectedVsGiven : Maybe String -> String -> IO ()
expectedVsGiven exp out = do
  case exp of
       Nothing => putStrLn "Expected: Nothing Found"
       Just str => do
         putStrLn "Expected:"
         putStrLn str
  putStrLn "Given:"
  putStrLn out

covering export
displayResult : Either TestError TestResult -> IO ()
displayResult (Left (CantLocateDir x)) = putStrLn $ "ERROR: Cannot find test directory"
displayResult (Left (CantReadOutput x)) = putStrLn $ "ERROR: Cannot read test output"
displayResult (Left (CantReadExpected x)) = putStrLn $ "ERROR: Cannot read expected output"
displayResult (Left (CantParseTest x)) = putStrLn $ "ERROR: Parsing failed: " ++ displayParsingError (const "something is missing") x
displayResult (Left CantWriteNewGolden) = putStrLn $ "ERROR: Cannot write file 'expected'"
displayResult (Left (CommandFailed x)) = putStrLn $ "ERROR: Cannot run command - Exit code: " ++ show x
displayResult (Right Success) = putStrLn "ok"
displayResult (Right (NewGolden str)) = putStrLn "new golden value" *> putStrLn str
displayResult (Right (Failure expected given)) = do
  putStrLn "FAILURE"
  expectedVsGiven expected given

displayPath : Path -> String
displayPath (MkDPair path snd) = foldr1 (\x, y => x <+> "." <+> y) path

covering export
displayTestResult : String -> Either TestError TestResult -> IO ()
displayTestResult testPath result = do
  putStr $ testPath ++ ": "
  displayResult result

-- on Windows, we just ignore backslashes and slashes when comparing,
-- similarity up to that is good enough. Leave errors that depend
-- on the confusion of slashes and backslashes to unix machines.
covering
normalize : String -> String
normalize str =
    if isWindows
      then pack $ filter (\ch => ch /= '/' && ch /= '\\') (unpack str)
      else str

commandLine : TestConfig -> String
commandLine (MkTestConfig exec path params inputFile outputFile)
 = exec ++ " " ++ params ++ (maybe "" (" < " ++) inputFile) ++ " > " ++ outputFile

covering
handleFailure : Maybe String -> String -> IO (Either TestError TestResult)
handleFailure exp out = do
  expectedVsGiven exp out
  putStrLn $ "Do you want to " ++ maybe "set" (const "replace") exp ++ " the golden value? [N/y]"
  if !readAnswer
     then do
       Right _ <- writeFile "expected" out
         | Left err => pure $ Left $ CantWriteNewGolden
       putStrLn "New golden value saved"
       pure $ Right $ NewGolden out
     else do
       putStrLn "Resuming..."
       pure $ Right $ Failure exp out
  where
    covering
    readAnswer : IO Bool
    readAnswer = do
      answer <- getLine
      case answer of
           ""  => pure False
           "n" => pure False
           "N" => pure False
           "y" => pure True
           "Y" => pure True
           _ => putStrLn "I didn't understand your answer. [N/y]" *> readAnswer

covering
testExecution : (interactive : Bool) -> TestConfig -> IO (Either TestError TestResult)
testExecution interactive opts = do
  removeFile opts.outputFile
  0 <- system $ commandLine opts
    | n => pure $ Left $ CommandFailed 0
  Right out <- readFile opts.outputFile
    | Left err => pure $ Left $ CantReadOutput err
  Right exp <- readFile "expected"
    | Left err => if interactive
                  then handleFailure Nothing out
                  else pure $ Left $ CantReadExpected err
  let result = normalize exp == normalize out
  if result
    then pure $ Right Success
    else if interactive
           then handleFailure (Just exp) out
           else pure $ Right $ Failure (Just exp) out

asPath : DPair (List String) NonEmpty -> String
asPath (MkDPair path snd) = foldr1 (\x,y => x <+> "/" <+> y) path

covering export
runTest : RunEnv -> IO (Either TestError TestResult)
runTest env = do
  Just cdir <- currentDir
    | Nothing => pure $ Left $ CantLocateDir "Can't resolve currentDir"
  True <- changeDir env.path
    | False => pure $ Left $ CantLocateDir $ "Can't locate " ++ show env.path
  Right cfg <- parseTestConfig "test.repl"
    | Left err => pure $ Left $ CantParseTest err
  result <- testExecution env.interactive cfg
  changeDir cdir
  pure $ result

max_stars_repo_name: xvw/REPLica

max_issues_repo_name: xvw/REPLica

max_forks_repo_name: xvw/REPLica


text:
-- --------------------------------------------------------------- [ Tests.idr ]
-- Module    : Tests.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Sif.DSL.Test

import Test.Parsing

import Lightyear
import Lightyear.Char
import Lightyear.Strings

import Sif.Types
import Sif.AbsSyntax
import Sif.DSL.Parser.Problem
import Sif.DSL.Parser.Solution

export
runTests : IO ()
runTests = do
  putStrLn $ heading "Complete File Tests"
  canParse (Just "Problem")
           problem
           """sif problem

> Given two entities Alice and Bob, how can Bob give a message to
> Alice such that only the intended recipient, Alice, can be guaranteed
> to access the message.

infosec <- Problem "Information Secrecy"

> Core principle that ensures that the data is kept confidential.
>
> This functional requirement represents the core principle behind
> data confidentiality, the data should be kept confidential. The
> attacker may obtain knowledge about the sender/recipient, means and
> times of transport but the information contained inside should not be
> accessible.

dataConf <- Functional "Data Confidentiality"

> The data should be viewable only by the intended recipient.
>
> A related functional requirement is that the recipient of the
> message should be the only entity capable of accessing the data
> contained within the message.

recipConf <- Functional "Recipient Confidentiality"

> This performance requirement represents the notion that not all data
> needs equivalent levels of protection.  Data only needs to be
> protected for the lifetime that the confidentiality needs to be
> guaranteed.

multiSecLevels <- Performance "Suitable Security Level"

> This usability requirement represents the idea that the actual act
> of securing data should not hinder upon the usage of any proposed
> mechanism. A user of the solution must not be inconvenienced by its
> use.

mechPerf <- Performance "Suitable performance"

> A secondary usability requirement targets the level of knowledge
> that an end-user of the solution must possess to use the solution.
> The user should need minimal knowledge of the underlying system.

understandable <- Usability "Comprehensible by Non-Experts"

> The resulting solution should have minimal impact on the workflow of
> the user.

minDisrupt <- Usability "Minimal Workflow Disruption"

> The implementation should be implemented securely.

secureImpl <- Reliability "Secure Implementation"
"""

  canParse (Just "Solution Complete")
           solution
           """sif solution

Description "Information Secrecy is about keeping data confidential. Public key encryption provides a mathematically guaranteed mechanism that allows data to be obfuscated such that only the recipient can reconstitute the messages original meaning."

> Public key crypto schemes are an application of asymmetric
> cryptography in which the public/private key pair is used for
> encryption/decryption respectively. Asymmetric crypto schemes
> consist of three algorithms.
> \
> + keygen :: Given a security parameter generates a public private key pair.
> + encrypt :: Given a public key and a message, encrypts the message under the given public key.
> + decrypt :: Given a private key and a ciphertext, =decrypt= returns a readable plaintext if the private key was paired with the ciphertexts encryption key.
Solution "Public Key Cryptography" solves infosec in std {

  > The underlying mathematical algorithm that provides the asymmetric cipher used.
  Property "Maths Algorithm" {

    > There will be a formal proof of the operations working.
    Advantage "Formal Guarantee" is Satisfied {
      Affects { Helps dataConf, Helps recipConf }
    }

	> The maths algorithm is generally computationally expensive on large data.
    Disadvantage "Computationally Expensive" is WeakSatis {
      Affects { Hurts mechPerf, Hurts minDisrupt }
    }
  }

  > The implementation in Code
  Property "Implementation in Code" {

    > There is possibility that the implementation of the algorithm is insecure/poor.
	Trait "Implementation InSecure" is WeakSatis {
	  Affects {
	    SomeNeg recipConf, SomeNeg dataConf, Unknown minDisrupt, SomeNeg secureImpl
	  }
	}

	> Some implementations really make it hard to understand things
	Trait "Implementation obfuscates understanding" is WeakDen {
	  Affects { Hurts understandable, Hurts minDisrupt }
    }
  }

  > There are two keys in use.
  Property "Key Pairs" {

    > Reduces problems with Key Security
    Advantage "PublicEnc/PrivateDec Keys" is Satisfied {
       Affects { Makes recipConf by "Only recipient has key to unlock the message" }
    }

	> A means of key distribution is required to ensure that public key ownership can be attested.
	Trait "Key Distribution" is Satisfied {
       Affects {
         SomeNeg recipConf by "Keys are distributed insecurely.",
		 SomeNeg minDisrupt by "Incorrect Distribution."
       }
    }

	> This solution requires the management of keys. That is, for each recipient the sender has to obtain a encryption key.
    Trait "Key Management" is Satisfied {
	   Affects {
	     SomeNeg dataConf by "Possibly sending data encrypted under the wrong key."
	   }
	}
  }

  > Different algorithm's will have different security parameters, and may allow different key lengths.
  Property "Variable Security Parameters" {

    > Many algorithms have variable security levels. Data can been secured at various levels.
    Advantage "Greater Security" is Satisfied {
	    Affects { Helps multiSecLevels }
	}

   > Common parameters are required to be selected and agreed upon.
   Trait "Parameter Selection" is Satisfied {
        Affects {
		    SomeNeg multiSecLevels by "insecure parameters being selected."
		  , SomeNeg secureImpl     by "insecure paremeters being selected."
		}
   }

   > Some parameters though secure might occur a greater processing cost.
   Disadvantage "Parameter Computation" is Satisfied {
       Affects { Hurts mechPerf, Hurts minDisrupt }
   }
  }
}
"""

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
data Things : Type where
     MkThings : a -> a -> Things

namespace X
  public export
  data Test = A | B

namespace Y
  public export
  data TestType = Test | Baz

test1 : Things
test1 = MkThings Baz Test

test2 : Things
test2 = MkThings Int Test

test3 : Integer -> Things
test3 x = MkThings Test Baz

test4 : Things
test4 = MkThings Test Int


text:
module Parity

data Parity : Nat -> Type where
   even : Parity (n + n)
   odd  : Parity (S (n + n))

parity : (n:Nat) -> Parity n
parity Z     = even {n=Z}
parity (S Z) = odd {n=Z}
parity (S (S k)) with (parity k)
    parity (S (S (j + j)))     | even ?= even {n=S j}
    parity (S (S (S (j + j)))) | odd  ?= odd {n=S j}

parity_lemma_2 = proof {
    intro;
    intro;
    rewrite sym (plusSuccRightSucc j j);
    trivial;
}

parity_lemma_1 = proof {
    intro j;
    intro;
    rewrite sym (plusSuccRightSucc j j);
    trivial;
}

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
import Data.Vect

--data Option t = Some t | None
data Option : (t:Type) -> Type where
  Some : (value:t) -> Option t
  None : Option t

add : Int -> Int -> Int
add x y = x + y

StringOrNat : Nat -> Type
StringOrNat Z = String
StringOrNat (S K) = Nat

divide : (x:Nat) -> (y:Nat) -> StringOrNat y
divide x Z = "Divisor was 0"
divide x y @ (S k) = div x y

max_stars_repo_name: janschultecom/typelevel-seo

max_issues_repo_name: janschultecom/typelevel-seo

max_forks_repo_name: janschultecom/typelevel-seo


text:
module Main
import Package.IpkgAst
import Package.IkanAssets
import System

ikanSettingsDir : String
ikanSettingsDir = "~/.idris-ikan"

echo : String -> IO ()
echo = putStrLn

echo0 : String -> IO ()
echo0 = putStr

rawcmd : String -> IO ()
rawcmd c = do system c ; pure ()

ikanInit : IO ()
ikanInit = do
  r<-createDir ikanSettingsDir
  case r of
         (Left l)=>  echo "error ikanInit"
         (Right x)=>  pure ()

cmds : List (String,String,IO ())
cmds = [("np","create new template project ",do
  echo "project name ?"
  fn<-getLine
  r<-createDir fn
  case r of
         (Left l)=>  echo "error !"
         (Right x)=>  do
           writeFile (fn++"/"++ fn++".ipkg") (ipkgPackage fn)
           writeFile (fn++"/.gitignore") (IkanAssets.flGitignore)
           echo $ "ok,project created : "++ fn
           echo "create main.idr? n for not "
           x<-getLine
           if (x=="n") then pure () else do writeFile (fn++"/Main.idr") IkanAssets.flMain;pure ()
           ) ,
         ("iinit","initialize ikan package manager(write files to "++ikanSettingsDir++")",do
           r<-dirOpen ikanSettingsDir
           case r of
                (Left l)=> ikanInit
                (Right r)=> echo "dir ok!"
         ),
         ("clr","clean this project,delete all .ibc file",do
         rawcmd "rm **/*.ibc"
         echo "ok,project cleaned"
         --rawcmd "idris clean ipkg"
         ),
         ("nf","new file/module",
         do
           echo0 "new file/module name:"
           s<-getLine
           writeFile (s++".idr") $ concat ["module ",s," \n"]
           pure ()
           )
         ]

showHelp : IO ()
showHelp = do
  let lns=map (\(c,desc,_) => concat [" ",c," : ",desc," \n"]) cmds
  echo $ "showing help : "
  putStrLn $ "avail commands : \n" ++ (foldl1 (\x,y=>x++y) lns)

listDirs : String->IO ()
listDirs s = do
  d<-dirOpen s
  case d of
    Left l => echo "failed dirOpen "
    (Right d1)=> do
      echo $ "dirOpen "++s ++" ok !"
      nextdir<-dirEntry d1
      case nextdir of
        (Left l)=> do print l; echo "dirEntry failed"
        (Right r)=> do
          echo $ "dir dirEntry " ++ s ++ " ok!"
          listDirs r

main : IO ()
main = do
--  let
  echo "welcome to ikan , a idris package manager in idris ! "
--  listDirs "src"
  args<-getArgs
  case args of
       (_ :: x :: xs) => doAct x
       y => do
         showHelp
         echo0 "input cmd:"
         ln<-getLine
         doAct ln

  pure ()
where
    doAct : String->IO ()
    doAct = (\x => let act = find (\cmd=> let (nm,_,_)=cmd in nm==x) cmds
                    in (case act of
                            Nothing=> do echo "cmd not found"
                                         showHelp
                            Just (_, _,io)=> io))

max_stars_repo_name: renpillay/ikan

max_issues_repo_name: renpillay/ikan

max_forks_repo_name: renpillay/ikan


text:
module Libraries.Utils.Term

import System.FFI

%default total

libterm : String -> String
libterm s = "C:" ++ s ++ ", libidris2_support, idris_term.h"

%foreign libterm "idris2_setupTerm"
         "jvm:setup,io/github/mmhelloworld/idrisjvm/runtime/Terminal"
prim__setupTerm : PrimIO ()

%foreign libterm "idris2_getTermCols"
         "jvm:getColumns,io/github/mmhelloworld/idrisjvm/runtime/Terminal"
prim__getTermCols : PrimIO Int

%foreign libterm "idris2_getTermLines"
         "jvm:getRows,io/github/mmhelloworld/idrisjvm/runtime/Terminal"
prim__getTermLines : PrimIO Int

export
setupTerm : IO ()
setupTerm = primIO prim__setupTerm

export
getTermCols : IO Int
getTermCols = primIO prim__getTermCols

export
getTermLines : IO Int
getTermLines = primIO prim__getTermLines


text:
-- --------------------------------------------------------------- [ PList.idr ]
-- Module    : PList.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A `list` construct to create lists with with values that satisfy
||| some predicate..
|||
||| The list quantifier `All` in idris is an external proof for a list
||| with type `List a`.  `PList` is a proof-carrying data structure
||| that only allows for lists to be constructed if they satisfy the
||| predicate.
module Data.PList

import public Data.List
import public Data.DList

%access export
%default total

public export
data PList : (aTy    : Type)
          -> (elemTy : aTy -> Type)
          -> (predTy : aTy -> Type)
          -> (as     : List aTy)
          -> (prf    : DList aTy predTy as)
          -> Type
  where
    ||| Create an empty List
    Nil  : PList aTy elemTy predTy Nil Nil

    ||| Cons
    |||
    ||| @elem The element to add and proof that the element's type satisfies a certain predicate.
    ||| @rest The list for `elem` to be added to.
    (::) : (elem : elemTy x)
        -> {prf : predTy x}
        -> (rest : PList aTy elemTy predTy xs prfs)
        -> PList aTy elemTy predTy (x :: xs) (prf :: prfs)

(++) : PList aTy eTy pTy as pAs
    -> PList aTy eTy pTy bs pBs
    -> PList aTy eTy pTy (as ++ bs) (pAs ++ pBs)
(++) [] ys = ys
(++) (elem :: rest) ys = elem :: rest ++ ys

empty : PList aTy eTy pTy Nil Nil
empty = Nil

add  : (elem : elemTy x)
    -> {auto prf : predTy x}
    -> (rest : PList aTy elemTy predTy xs prfs)
    -> PList aTy elemTy predTy (x :: xs) (prf :: prfs)
add x {prf} rest = x :: rest

-- -------------------------------------------------------------- [ Form Tests ]
isNil : PList aTy eTy p as prfs -> Bool
isNil [] = True
isNil (elem :: rest) = False

isCons : PList aTy eTy p as prfs -> Bool
isCons l = isNil l == False

-- ------------------------------------------------------------------ [ Length ]

length : PList aTy eTy p as prfs -> Nat
length Nil     = Z
length (x::xs) = (S Z) + length xs

Sized (PList aTy eTy pTy as prfs) where
  size = length

eqPList : ({a,b : aTy} -> elemTy a -> elemTy b -> Bool)
       -> PList aTy elemTy predTy as aPrfs
       -> PList aTy elemTy predTy bs bPrfs
       -> Bool
eqPList _ Nil     Nil     = True
eqPList p (x::xs) (y::ys) =
  if p x y
    then eqPList p xs ys
    else False
eqPList _ _       _       = False

-- ---------------------------------------------- [ List-Based Transformations ]

toDList : PList aTy eTy p as prfs -> DList aTy eTy as
toDList Nil     = Nil
toDList (elem::xs) = elem :: toDList xs

toList : PList aTy eTy pTy as prfs -> List (a : aTy ** prf : pTy a ** eTy a)
toList [] = []
toList ((::) elem {x} {prf} rest) = (x ** prf ** elem) :: toList rest

fromDList : (xs   : DList aTy eTy as)
         -> (prfs : DList aTy pTy as)
         -> PList aTy eTy pTy as prfs
fromDList [] [] = []
fromDList (elem :: rest) (prf :: prfs) = elem :: fromDList rest prfs

fromList : (prf : predTy a)
        -> (xs  : List $ elemTy a)
        -> PList aTy elemTy predTy (replicate (length xs) a)
                                   (replicate (length xs) prf)
fromList prf [] = []
fromList prf (x :: xs) = x :: fromList prf xs

-- ---------------------------------------------------------------- [ Indexing ]

public export
data NonEmpty : (xs : PList aTy eTy pTy as prfs) -> Type where
  IsNonEmpty : PList.NonEmpty (x::rest)

Uninhabited (PList.NonEmpty []) where
  uninhabited IsNonEmpty impossible

nonEmpty : (xs : PList aTy eTy pTy as prfs) -> Dec (NonEmpty xs)
nonEmpty [] = No absurd
nonEmpty (elem :: rest) = Yes IsNonEmpty

public export
data InBounds : (idx : Nat)
             -> (xs : PList aTy eTy pTy as prfs)
             -> Type
  where
    InFirst : PList.InBounds Z (x::rest)
    InLater : (later : PList.InBounds idx rest)
           -> PList.InBounds (S idx) (x::rest)

Uninhabited (PList.InBounds idx []) where
  uninhabited InFirst impossible
  uninhabited (InLater _) impossible

inBounds : (idx : Nat)
        -> (xs  : PList aTy eTy pTy as prfs)
        -> Dec (InBounds idx xs)
inBounds idx Nil = No uninhabited
inBounds Z (elem :: rest) = Yes InFirst
inBounds (S k) (elem :: rest) with (inBounds k rest)
  inBounds (S k) (elem :: rest) | (Yes prf) = Yes $ InLater prf
  inBounds (S k) (elem :: rest) | (No contra) =
      No (\p => case p of
                   InLater y => contra y)

index : (idx : Nat)
     -> (xs : PList aTy eTy pTy as prfs)
     -> {auto ok   : InBounds idx xs}
     -> {auto ok'  : InBounds idx as}
     -> {auto ok'' : InBounds idx prfs}
     -> eTy (index idx as)
index Z (y :: rest) {ok = InFirst} = y
index (S k) (y :: rest) {ok = (InLater later)} {ok' = (InLater later')} {ok'' = (InLater later'')} = PList.index k rest

head : (xs : PList aTy eTy pTy (a::as) prfs)
    -> {auto ok   : NonEmpty xs}
    -> {auto ok'  : NonEmpty (a::as)}
    -> {auto ok'' : NonEmpty prfs}
    -> eTy a
head (elem :: rest) = elem

tail : (xs : PList aTy eTy pTy (a::as) (p::prfs))
    -> {auto ok   : NonEmpty xs}
    -> {auto ok'  : NonEmpty (a::as)}
    -> {auto ok'' : NonEmpty (p::prfs)}
    -> PList aTy eTy pTy as prfs
tail (elem :: rest) = rest

last : (xs : PList aTy eTy pTy as prfs)
    -> {auto ok   : NonEmpty xs}
    -> {auto ok'  : NonEmpty as}
    -> {auto ok'' : NonEmpty prfs}
    -> eTy (last as)
last [] {ok = IsNonEmpty} impossible
last (elem :: []) {ok = ok} {ok' = ok'} {ok'' = ok''} = elem
last (elem :: ((::) {prf} y rest)) {ok = ok} {ok' = ok'} {ok'' = ok''} = last $ (::) y rest {prf=prf}

init : (xs : PList aTy eTy pTy as prfs)
    -> {auto ok   : NonEmpty xs}
    -> {auto ok'  : NonEmpty as}
    -> {auto ok'' : NonEmpty prfs}
    -> PList aTy eTy pTy (init as) (init {ok=ok''} prfs)
init (y :: []) {ok = IsNonEmpty} {ok' = IsNonEmpty} {ok'' = IsNonEmpty} = []
init (y :: ((::) {prf} elem rest)) {ok = IsNonEmpty} {ok' = IsNonEmpty} {ok'' = IsNonEmpty} = y :: init (elem :: rest)

public export
data Elem : (aTy    : Type)
         -> (elemTy : aTy -> Type)
         -> (predTy : aTy -> Type)
         -> (a : aTy)
         -> (x : elemTy a)
         -> (prf : predTy a)
         -> (xs   : PList aTy elemTy predTy as prfs)
         -> (prfA : Elem a as)
         -> (prfP : DElem aTy predTy prf prfs prfA)
         -> Type
  where
    Hier  : PList.Elem aTy eTy pTy a x p (x::xs) Here Hier
    Er    : (rest : PList.Elem aTy eTy pTy a x p xs prfA prfP)
         -> PList.Elem aTy eTy pTy a x p (x'::xs) (There prfA) (DList.Er prfP)

Uninhabited (PList.Elem aTy eTy pTy a x prf Nil prfA prfP) where
  uninhabited Hier impossible
  uninhabited (Er _) impossible

dropElem : (as   : PList iTy elemTy predTy is prfs)
        -> (idxP : Elem iTy elemTy predTy i e prf as prfA prfP)
        -> PList iTy elemTy predTy (dropElem is prfA) (dropElem prfs prfP)
dropElem (e :: x) Hier = x
dropElem (x :: z) (Er rest) = x :: dropElem z rest

delete' : (x  : elemTy i)
       -> (xs : PList iTy elemTy predTy is prfs)
       -> (idxVal : Elem i is)
       -> (idxPrf : DElem iTy predTy prf prfs idxVal)
       -> PList iTy elemTy predTy (dropElem is idxVal) (dropElem prfs idxPrf)
delete' x (elem :: rest) Here Hier = rest
delete' x (elem :: rest) (There later) (Er komst) = elem :: delete' x rest later komst

delete : (x  : elemTy i)
      -> (xs : PList iTy elemTy predTy is prfs)
      -> {auto idxVal : Elem i is}
      -> {auto idxPrf : DElem iTy predTy prf prfs idxVal}
      -> PList iTy elemTy predTy (dropElem is idxVal) (dropElem prfs idxPrf)
delete x xs {idxVal} {idxPrf} = delete' x xs idxVal idxPrf

-- --------------------------------------------------------- [ Bob The Builder ]

-- TODO append
-- TODO replicate

-- ---------------------------------------------------------------- [ SubLists ]

take : (n : Nat)
    -> (xs : PList aTy elemTy predTy as prfs)
    -> PList aTy elemTy predTy (take n as) (take n prfs)
take Z     xs             = Nil
take (S k) []             = Nil
take (S k) (elem :: rest) = elem :: take k rest

-- TODO takeWhile

-- TODO drop
drop : (n : Nat)
    -> (xs : PList aTy elemTy predTy as prfs)
    -> PList aTy elemTy predTy (drop n as) (drop n prfs)
drop Z     rest           = rest
drop (S k) []             = Nil
drop (S k) (elem :: rest) = drop k rest

-- TODO dropWhile

-- ---------------------------------------------------------------- [ Equality ]
-- TODO eqPList

-- ------------------------------------------------------------------- [ Order ]
-- TODO cmpPList

-- ----------------------------------------------------------------- [ Folding ]
-- TODO foldr and foldl
foldr : ({a : aTy} -> elemTy a -> p -> p)
     -> p
     -> PList aTy elemTy predTy as prfs
     -> p
foldr f init Nil     = init
foldr f init (x::xs) = f x (PList.foldr f init xs)

foldl : ({a : aTy} -> p -> elemTy a -> p)
      -> p
      -> PList aTy elemTy predTy as prfs
      -> p
foldl f init Nil = init
foldl f init (x::xs) = PList.foldl f (f init x) xs

-- ----------------------------------------------------------------- [ Functor ]

map : ({a : aTy} -> elemTy a -> b)
   -> PList aTy elemTy predTy as prf
   -> List b
map f Nil     = List.Nil
map f (x::xs) = with List f x :: map f xs

mapMaybe : ({a : aTy} -> elemTy a -> Maybe b)
         -> PList aTy elemTy predTy as prfs
         -> List b
mapMaybe f Nil     = Nil
mapMaybe f (x::xs) =
  case f x of
    Nothing => mapMaybe f xs
    Just y  => y :: mapMaybe f xs

concatMap : Monoid m
         => (func : {a : aTy} -> elemTy a -> m)
         -> (xs : PList aTy elemTy predTy as prfs)
         -> m
concatMap f = foldr (\e, res => f e <+> res) neutral

-- -------------------------------------------------------- [ Membership Tests ]
-- TODO make deceq tests
-- TODO any
-- TODO all
-- TODO elemBy
-- TODO elem
-- TODO hasAnyBy
-- TODO hasAny

-- --------------------------------------------------------------- [ Searching ]

-- TODO find

-- ------------------------------------------------------------- [ Conversions ]
-- TODO

-- ----------------------------------------------------------------- [ Filters ]
-- TODO

-- ------------------------------------------------------------ [ Partitioning ]
-- TODO

-- ----------------------------------------------------------------- [ Zipping ]
-- TODO

-- -------------------------------------------------------------- [ Predicates ]
-- TODO

-- ----------------------------------------------------------------- [ Sorting ]
-- TODO

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

private
doPListShow : ({a : aTy} -> elemTy a -> String)
           -> PList aTy elemTy predTy as prfs
           -> List String
doPListShow _  Nil     = Nil
doPListShow f  (x::xs) = (f x) :: doPListShow f xs

showPList : (showFunc : {a : aTy} -> elemTy a -> String)
         -> (l : PList aTy elemTy predTy as prfs)
         -> String
showPList f xs = "[" ++ unwords (intersperse "," (doPListShow f xs)) ++ "]"

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
-- BSTree.idr
--
-- Demonstates generic data types

module BSTree

||| A binary tree
public export
data BSTree : Type -> Type where
  Empty : Ord elem => BSTree elem
  Node : Ord elem => (left : BSTree elem) -> (val : elem) ->
                     (right : BSTree elem) -> BSTree elem

%name BSTree tree, tree1

||| Inserts a new element into a binary search tree
export
insert : elem -> BSTree elem -> BSTree elem
insert x Empty = Node Empty x Empty
insert x (Node left val right) = case compare x val of
                                      LT => Node (insert x left) val right
                                      EQ => Node left val right
                                      GT => Node left val (insert x right)

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Data.OneOf

import public Data.List.Elem
import public Data.HList

%default total

public export
data OneOf : List Type -> Type where
  Here : x -> OneOf (x :: xs)
  There : OneOf xs -> OneOf (x :: xs)

public export
make : Elem a as => a -> OneOf as
make x @{Here} = Here x
make x @{There _} = There (make x)

public export
TypeAt : (as : List Type) -> OneOf as -> Type
TypeAt (x :: _) (Here _) = x
TypeAt (_ :: xs) (There x) = TypeAt xs x

public export
Eliminators : (as : List Type) -> (r : Type) -> Type
Eliminators xs r = HList (map (\x => x -> r) xs)

public export
get : (o : OneOf as) -> TypeAt as o
get (Here x) = x
get (There x) = get x

public export
match : OneOf as -> Eliminators as r -> r
match (Here x) (f :: _) = f x
match (There x) (_ :: fs) = match x fs

public export
extend : OneOf as -> OneOf (as ++ bs)
extend (Here x) = Here x
extend (There x) = There (extend x)


text:
module TypedContainers.Util.Filter

import Data.List

%default total

public export
0 filterCommutative' :
  {f : a -> Bool} -> {g : a -> Bool} -> (xxs : List a) -> (yys : List a)
  -> (yys = filter f (filter g xxs)) -> (yys = filter g (filter f xxs))
filterCommutative' [] yys p = p
filterCommutative' (x :: xs) yys p =
  case the (DPair Bool (g x ===)) $ MkDPair (g x) Refl of
    MkDPair True p0 => case the (DPair Bool (f x ===)) $ MkDPair (f x) Refl of
      MkDPair True p1 =>
        let p2 : (filter f (x :: filter g xs) = filter f (filter g (x :: xs))) = rewrite p0 in Refl in
        let p3 : (x :: filter f (filter g xs) = filter f (x :: filter g xs)) = rewrite p1 in Refl in
        let p3 : (x :: filter f (filter g xs) = filter f (filter g (x :: xs))) = trans p3 p2 in
        case yys of
          [] impossible
          y :: ys =>
            let (Refl) : (y :: ys = x :: filter f (filter g xs)) = trans p (sym p3) in
            let p4 = filterCommutative' {f, g} xs ys Refl in
            rewrite p1 in rewrite p0 in cong (x ::) p4
      MkDPair False p1 =>
        let p2 : (filter f (x :: filter g xs) = filter f (filter g (x :: xs))) = rewrite p0 in Refl in
        let p3 : (filter f (filter g xs) = filter f (x :: filter g xs)) = rewrite p1 in Refl in
        let p3 : (filter f (filter g xs) = filter f (filter g (x :: xs))) = trans p3 p2 in
        case yys of
          [] impossible
          y :: ys =>
            let p4 : (y :: ys = filter f (filter g xs)) = trans p (sym p3) in
            let p5 = filterCommutative' {f, g} xs (y :: ys) p4 in
            rewrite p1 in p5
    MkDPair False p0 =>
      let p2 : (filter f (filter g (x :: xs)) = filter f (filter g xs)) = rewrite p0 in Refl in
      let p3 : (yys = filter f (filter g xs)) = trans p p2 in
      let p4 = filterCommutative' {f, g} xs yys p3 in
      case the (DPair Bool (f x ===)) $ MkDPair (f x) Refl of
        MkDPair True p5 => rewrite p5 in rewrite p0 in p4
        MkDPair False p5 => rewrite p5 in p4

public export
0 filterCommutative : (filter f (filter g l) = filter g (filter f l))
filterCommutative = filterCommutative' {f, g} l (filter f (filter g l)) Refl

0 filterImplication' :
  {f : a -> Bool} -> {g : a -> Bool}
  -> ((x : a) -> (g x = True) -> (f x = True)) -> (xxs : List a) -> (yys : List a)
  -> (yys = filter f (filter g xxs)) -> (yys = filter g xxs)
filterImplication' p0 [] yys p1 = p1
filterImplication' p0 (x :: xs) yys p1 =
  case the (DPair Bool (g x ===)) $ MkDPair (g x) Refl of
    MkDPair True p2 =>
      let p3 : (filter f (filter g (x :: xs)) = filter f (x :: filter g xs)) = rewrite p2 in Refl in
      let p4 : (filter f (x :: filter g xs) = x :: filter f (filter g xs)) = rewrite (p0 x p2) in Refl in
      let p5 : (yys = x :: filter f (filter g xs)) = trans (trans p1 p3) p4 in
      let p6 : (filter f (filter g xs) = filter g xs) = filterImplication' {f, g} p0 xs (filter f (filter g xs)) Refl in
      let p7 : (yys = x :: filter g xs) = replace {p = \p => yys === x :: p} p6 p5 in
      rewrite p2 in p7
    MkDPair False p2 =>
      let p3 : (filter f (filter g (x :: xs)) = filter f (filter g xs)) = rewrite p2 in Refl in
      let p5 : (yys = filter f (filter g xs)) = trans p1 p3 in
      let p6 : (filter f (filter g xs) = filter g xs) = filterImplication' {f, g} p0 xs (filter f (filter g xs)) Refl in
      let p7 : (yys = filter g xs) = replace {p = (yys ===)} p6 p5 in
      rewrite p2 in p7

public export
0 filterImplication : ((x : a) -> (g x = True) -> (f x = True)) -> (filter f (filter g l) = filter g l)
filterImplication p = filterImplication' {f, g} p l (filter f (filter g l)) Refl

0 filterExtensionality' : {f : a -> Bool} -> {g : a -> Bool} -> {p : (x : a) -> f x = g x} -> (l : List a) -> (filter f l = filter g l)
filterExtensionality' [] = Refl
filterExtensionality' (x :: xs) =
  let rec = filterExtensionality' {f, g, p} xs in
  case MkDPair (f x) Refl {p = (f x ===)} of
    MkDPair True p0 =>
      let p1 : (g x = True) = rewrite sym $ p x in p0 in
      rewrite p1 in
      rewrite p0 in
      rewrite rec in
      Refl
    MkDPair False p0 =>
      let p1 : (g x = False) = rewrite sym $ p x in p0 in
      rewrite p1 in
      rewrite p0 in
      rewrite rec in
      Refl

public export
0 filterExtensionality : ((x : a) -> f x = g x) -> (filter f l = filter g l)
filterExtensionality p = filterExtensionality' {p} l

max_stars_repo_name: L-as/idris-rbtree

max_issues_repo_name: L-as/idris-rbtree

max_forks_repo_name: L-as/idris-rbtree


text:
-- ----------------------------------------------------------------- [ Day.idr ]
-- Module      : Data.Advent.Day
-- Description : Common structure for all puzzles, inspired by
--               Steve Purcell's Haskell solution.
-- Copyright   : Copyright (c) 2016, Eric Bailey
-- License     : MIT
-- Link        : https://github.com/purcell/adventofcode2016
-- --------------------------------------------------------------------- [ EOH ]
||| Common Structure for All Puzzles
module Data.Advent.Day

import Debug.Error

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

%default partial

%access public export

record Day (i : Type) where
    constructor MkDay
    dayNum     : Nat
    dayParser  : Parser i
    dayPartOne : i -> IO String
    dayPartTwo : i -> IO String

%access export

loadDay : Day i -> IO i
loadDay d = either error pure $
            either (Left . show) (parse (dayParser d <* eof))
            !(readFile $ "input/day" ++ zeroPad (dayNum d) ++ ".txt")
  where
    zeroPad : Nat -> String
    zeroPad n = if n < 10 then strCons '0' (show n) else show n

runDay : Day i -> IO ()
runDay d = do args <- getArgs
              input <- loadDay d
              when (isNil args || ("one" `elem` args)) $
                   do putStr $ banner "One"
                      putStrLn !(dayPartOne d input)
              when (isNil args || ("two" `elem` args)) $
                   do putStr $ banner "Two"
                      putStrLn !(dayPartTwo d input)
  where
    banner : String -> String
    banner part = "Day " ++ show (dayNum d) ++ ": Part " ++ part ++ " ==> "

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

max_stars_repo_name: yurrriq/advent-of-code


text:
module Libraries.Control.ANSI

import public Libraries.Control.ANSI.CSI
import public Libraries.Control.ANSI.SGR

%default total

public export
record DecoratedString where
  constructor MkDString
  sgr : List SGR
  str : String

export
Show DecoratedString where
  show dstr = escapeSGR dstr.sgr ++ dstr.str ++ escapeSGR [Reset]

export
colored : Color -> String -> DecoratedString
colored c = MkDString [SetForeground c]

export
background : Color -> String -> DecoratedString
background c = MkDString [SetBackground c]

export
bolden : String -> DecoratedString
bolden = MkDString [SetStyle Bold]

export
italicize : String -> DecoratedString
italicize = MkDString [SetStyle Italic]

export
underline : String -> DecoratedString
underline = MkDString [SetStyle SingleUnderline]


text:
module Main

import System.Info

main : IO ()
main = do
  putStrLn codegen
  putStrLn os

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


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

import Lightyear
import Lightyear.Char
import Lightyear.Strings

import Sif.Types
import Sif.DSL.Parser.Utils
import Sif.DSL.Parser.Common

export
context : Parser $ Pair String SifDomain
context = do
    keyword "sif"
    string "context"
    endOfLine
    spaces
    keyword "Context"
    t <- title
    keyword "as"
    i <- ident
    spaces
    d <- opt desc
    pure $ (i, MkDomain t d)
  <?> "Problem Specification"

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


text:
module Control.Effect.Reader

import Control.EffectAlgebra

import Control.Monad.Reader

||| Reader effect.
public export
data ReaderE : Type -> (Type -> Type) -> Type -> Type where
  Ask : ReaderE r m r

export
Functor (\r => ReaderE r m r) where
  map _ Ask = Ask

||| Read the value within a monadic context that supports it.
public export
ask : Inj (ReaderE r) sig => Algebra sig m => m r
ask = send Ask

namespace Algebra
  ||| Apply the reader effect of the signature to the underlying monad,
  ||| resulting in the ReaderT transformer.
  public export
  [Reader] (al : Algebra sig m) => Algebra (ReaderE s :+: sig) (ReaderT s m) where
    alg ctx hdl (Inl Ask) = MkReaderT $ \s => pure (s <$ ctx)
    alg ctx hdl (Inr x) = MkReaderT $ \r => alg ctx (runReaderT r . hdl) x

  %hint public export
  HintReader : (al : Algebra sig m) => Algebra (ReaderE s :+: sig) (ReaderT s m)
  HintReader = Reader


text:
module Flutter.FFI

import Dart.Core
import Dart.FFI.Elab

%language ElabReflection

%runElab importDart [
  package "package:flutter/foundation.dart" [
    class' "Key" [
    ],
    class' "Listenable" [
    ],
    enum "TargetPlatform" [
      "android",
      "fuchsia",
      "iOS",
      "linux",
      "macOS",
      "windows"
    ]
  ],
  package "package:flutter/rendering.dart" [
    enum "MainAxisSize" [
      "max",
      "min"
    ]
  ],
  package "package:flutter/painting.dart" [
    class' "Alignment" [
      extends "AlignmentGeometry",
      static $ final "Alignment" "centerLeft",
      static $ final "Alignment" "centerRight"
    ],
    class' "AlignmentGeometry" [
    ],
    enum "BoxFit" [
      "contain", "cover", "fill", "fitHeight", "fitWidth", "none", "scaleDown"
    ],
    class' "EdgeInsets" [
      extends "EdgeInsetsGeometry",
      const $ new "all" [
        "value" :: "double"
      ]
    ],
    class' "EdgeInsetsGeometry" [
    ],
    class' "ShapeBorder" [
    ],
    class' "TextStyle" [
      final "TextAlign" "textAlign",
      new "" [
        "color" :? "Color",
        -- "decoration" :? "TextDecoration",
        "decorationColor" :? "Color",
        -- "decorationStyle" :? "TextDecorationStyle",
        "decorationThickness" :? "double",
        -- "fontWeight" :? "FontWeight",
        -- "fontStyle" :? "FontStyle",
        -- "textBaseline" :? "TextBaseline",
        "fontFamily" :? "String",
        "fontFamilyFallback" :? "Dart.Core.List" :<> "String",
        "fontSize" :? "double",
        "letterSpacing" :? "double",
        "wordSpacing" :? "double",
        "height" :? "double"
      ]
    ]
  ],
  package "package:flutter/material.dart" [
    class' "AppBar" [
      extends "Widget",
      new "" [
        "title" :? "Widget"
      ]
    ],
    class' "ButtonStyle" [
      const $ new "" [
        "backgroundColor" :? "MaterialStateProperty" :<> "Color",
        "foregroundColor" :? "MaterialStateProperty" :<> "Color",
        "textStyle" :? "MaterialStateProperty" :<> "TextStyle",
        "overlayColor" :? "MaterialStateProperty" :<> "Color",
        "shadowColor" :? "MaterialStateProperty" :<> "Color"
      ]
    ],
    class' "Card" [
      extends "Widget",
      const $ new "" [
        "key" :? "Key",
        "color" :? "Color",
        "shadowColor" :? "Color",
        "elevation" :? "double",
        "shape" :? "ShapeBorder",
        "borderOnForeground" :? "bool",
        "margin" :? "EdgeInsetsGeometry",
        "clipBehavior" :? "Clip",
        "child" :? "Widget",
        "semanticContainer" :? "bool"
      ]
    ],
    class' "CircularProgressIndicator" [
      extends "Widget",
      const $ new "" [
        "key" :? "Key"
      ]
    ],
    class' "Colors" [
      static $ final "MaterialColor" "black",
      static $ final "MaterialColor" "blue",
      static $ final "MaterialColor" "brown",
      static $ final "MaterialColor" "cyan",
      static $ final "MaterialColor" "green",
      static $ final "MaterialColor" "grey",
      static $ final "MaterialColor" "orange",
      static $ final "MaterialColor" "purple",
      static $ final "MaterialColor" "red",
      static $ final "MaterialColor" "transparent",
      static $ final "MaterialColor" "white",
      static $ final "MaterialColor" "yellow"
    ],
    class' "FloatingActionButton" [
      extends "Widget",
      const $ new "" [
        "onPressed" :? "IO" :<> "()",
        "tooltip" :? "String",
        "child" :? "Widget"
      ]
    ],
    class' "Icons" [
      static $ final "IconData" "add",
      static $ final "IconData" "add_circle_outline",
      static $ final "IconData" "remove",
      static $ final "IconData" "remove_circle_outline",
      static $ final "IconData" "play_arrow",
      static $ final "IconData" "stop",
      static $ final "IconData" "stop_circle",
      static $ final "IconData" "stop_circle_outlined",
      static $ final "IconData" "stop_circle_rounded",
      static $ final "IconData" "stop_circle_sharp",
      static $ final "IconData" "stop_outlined",
      static $ final "IconData" "stop_rounded"
    ],
    class' "IconButton" [
      extends "Widget",
      const $ new "" [
        "onPressed" :? "IO" :<> "()",
        "tooltip" :? "String",
        "icon" :? "Widget",
        "alignment" :? "AlignmentGeometry"
      ]
    ],
    class' "InputBorder" [
      static $ final "InputBorder" "none"
    ],
    class' "InputDecoration" [
      const $ new "" [
        "labelText" :? "String",
        "hintText" :? "String",
        "hintStyle" :? "TextStyle",
        "border" :? "InputBorder"
      ]
    ],
    class' "LinearProgressIndicator" [
      extends "Widget",
      const $ new "" [
        "key" :? "Key",
        "value" :? "double",
        "backgroundColor" :? "Color",
        "minHeight" :? "double",
        "semanticsLabel" :? "String",
        "semanticsValue" :? "String",
        "valueColor" :? "Animation" :<> "Color"
      ]
    ],
    class' "MaterialApp" [
      extends "Widget",
      const $ new "" [
        "title" :? "String",
        "home" :? "Widget",
        "theme" :? "ThemeData",
        "routes" :? "Dart.Core.Map" :<> "String" :<> "WidgetBuilder",
        "navigatorObservers" :? "Dart.Core.List" :<> "NavigatorObserver"
      ]
    ],
    class' "MaterialColor" [
      extends "Color",
      final "int" "alpha",
      final "int" "blue",
      final "int" "green",
      final "int" "red",
      final "double" "opacity",
      final "Color" "shade50",
      final "Color" "shade100",
      final "Color" "shade200",
      final "Color" "shade300",
      final "Color" "shade400",
      final "Color" "shade500",
      final "Color" "shade600",
      final "Color" "shade700",
      final "Color" "shade800",
      final "Color" "shade900"
    ],
    enum "MaterialState" [
      "disabled",
      "dragged",
      "error",
      "focused",
      "hovered",
      "pressed",
      "selected"
    ],
    generic ["a"] $ class' "MaterialStateProperty" [
      generic ["a"] $ static $
        io ("MaterialStateProperty" :<> "a") "resolveWith" [
          "resolver" :: "Dart.Core.Set" :<> "MaterialState" :-> "IO" :<> "a"
        ],
      generic ["a"] $ static $
        fun ("MaterialStateProperty" :<> "a") "all" [
          "value" :: "a"
        ]
    ],
    class' "CupertinoPageTransitionsBuilder" [
      extends "PageTransitionsBuilder",
      const $ new "" []
    ],
    class' "PageTransitionsBuilder" [
    ],
    class' "PageTransitionsTheme" [
      const $ new "" [
        "builders" :? "Dart.Core.Map" :<> "TargetPlatform" :<> "PageTransitionsBuilder"
      ]
    ],
    class' "Scaffold" [
      extends "Widget",
      const $ new "" [
        "appBar" :? "Widget",
        "body" :? "Widget",
        "floatingActionButton" :? "Widget",
        "backgroundColor" :? "Color"
      ]
    ],
    class' "Slider" [
      extends "Widget",
      const $ new "" [
        "value" :? "Double",
        "onChanged" :? "Double" :-> "IO" :<> "()",
        "onChangeStart" :? "Double" :-> "IO" :<> "()",
        "onChangeEnd" :? "Double" :-> "IO" :<> "()",
        "min" :? "Double",
        "max" :? "Double",
        "divisions" :? "int",
        "label" :? "String"
      ]
    ],
    class' "TextButton" [
      extends "Widget",
      const $ new "" [
        "onPressed" :? "IO" :<> "()",
        "style" :? "ButtonStyle",
        "child" :? "Widget"
      ],
      static $ fun "ButtonStyle" "styleFrom" [
        "primary" :? "Color",
        "backgroundColor" :? "Color"
      ]
    ],
    class' "TextField" [
      extends "Widget",
      new "" [
        "key" :? "Key",
        "controller" :? "TextEditingController",
        "decoration" :? "InputDecoration",
        "keyboardType" :? "TextInputType",
        "inputFormatters" :? "Dart.Core.List" :<> "TextInputFormatter",
        "textAlign" :? "TextAlign",
        "style" :? "TextStyle"
      ]
    ],
    class' "TextFormField" [
      extends "FormField",
      extends "Widget",
      new "" [
        "key" :? "Key",
        "controller" :? "TextEditingController",
        "initialValue" :? "String",
        "decoration" :? "InputDecoration"
      ]
    ],
    class' "TextTheme" [
      final "TextStyle" "subtitle1",
      final "TextStyle" "subtitle2",
      final "TextStyle" "headline1",
      final "TextStyle" "headline2",
      final "TextStyle" "headline3",
      final "TextStyle" "headline4"
    ],
    class' "Theme" [
      static $ io "ThemeData" "of" ["context" :: "BuildContext"]
    ],
    class' "ThemeData" [
      new "" [
        "primarySwatch" :? "MaterialColor",
        "visualDensity" :? "VisualDensity",
        "pageTransitionsTheme" :? "PageTransitionsTheme"
      ],
      final "TextTheme" "textTheme"
    ],
    class' "VisualDensity" [
      static $ final "VisualDensity" "adaptivePlatformDensity"
    ]
  ],
  package "package:flutter/widgets.dart" [
    class' "Align" [
      const $ new "" [
        "key" :? "Key",
        "alignment" :? "AlignmentGeometry",
        "widthFactor" :? "double",
        "heightFactor" :? "double",
        "child" :? "Widget"
      ]
    ],
    class' "AnimatedBuilder" [
      extends "Widget",
      const $ new "" [
        "key" :? "Key",
        "animation" :? "Listenable",
        "builder" :? "BuildContext" :-> "Nullable" :<> "Widget" :-> "IO" :<> "Widget",
        "child" :? "Widget"
      ]
    ],
    enum "AutovalidateMode" [
      "always",
      "disabled",
      "onUserInteraction"
    ],
    class' "BuildContext" [
    ],
    class' "Center" [
      extends "Widget",
      const $ new "" [
        "child" :? "Widget"
      ]
    ],
    class' "Column" [
      extends "Widget",
      new "" [
        "children" :? "Dart.Core.List" :<> "Widget",
        "mainAxisAlignment" :? "MainAxisAlignment",
        "mainAxisSize" :? "MainAxisSize"
      ]
    ],
    class' "CustomPaint" [
      extends "Widget",
      const $ new "" [
        "key" :? "Key",
        "child" :? "Widget",
        "painter" :? "CustomPainter",
        "foregroundPainter" :? "CustomPainter",
        "size" :? "Size",
        "isComplex" :? "bool",
        "willChange" :? "bool"
      ]
    ],
    class' "CustomPainter" [
    ],
    class' "Expanded" [
      extends "Widget",
      const $ new "" [
        "child" :? "Widget"
      ]
    ],
    class' "FittedBox" [
      extends "Widget",
      const $ new "" [
        "key" :? "Key",
        "child" :? "Widget",
        "fit" :? "BoxFit",
        "alignment" :? "AlignmentGeometry",
        "clipBehavior" :? "Clip"
      ]
    ],
    class' "Form" [
      extends "Widget",
      const $ new "" [
        "child" :? "Widget",
        "onChanged" :? "IO" :<> "()",
        "autovalidateMode" :? "AutovalidateMode"
      ]
    ],
    class' "FormField" [
    ],
    class' "GestureDetector" [
      extends "Widget",
      new "" [
        "key" :? "Key",
        "child" :? "Widget",
        "onTapDown" :? "TapDownDetails" :-> "IO" :<> "()",
        "onTapUp" :? "TapUpDetails" :-> "IO" :<> "()",
        "onTap" :? "IO" :<> "()",
        "onTapCancel" :? "IO" :<> "()",
        "onSecondaryTap" :? "IO" :<> "()",
        "onSecondaryTapCancel" :? "IO" :<> "()",
        "onDoubleTap" :? "IO" :<> "()",
        "onDoubleTapCancel" :? "IO" :<> "()",
        "onSecondaryTapDown" :? "TapDownDetails" :-> "IO" :<> "()",
        "onSecondaryTapUp" :? "TapUpDetails" :-> "IO" :<> "()",
        "onLongPress" :? "IO" :<> "()",
        "onLongPressStart" :? "LongPressStartDetails" :-> "IO" :<> "()",
        "onLongPressMoveUpdate" :? "LongPressMoveUpdateDetails" :-> "IO" :<> "()",
        "onLongPressEnd" :? "LongPressEndDetails" :-> "IO" :<> "()"
      ]
    ],
    class' "Icon" [
      extends "Widget",
      const $ new "" [
        "icon" :: "IconData",
        "key" :? "Key"
      ]
    ],
    class' "IconData" [
    ],
    enum "MainAxisAlignment" [
      "start", "end", "center", "spaceBetween", "spaceAround", "spaceEvenly"
    ],
    class' "Navigator" [
      static $ io "NavigatorState" "of" [
        "context" :: "BuildContext",
        "rootNavigator" :? "bool"
      ],
      static $ io "void" "popUntil" [
        "context" :: "BuildContext",
        "predicate" :: "RoutePredicate"
      ]
    ],
    class' "NavigatorObserver" [
    ],
    class' "NavigatorState" [
      io "void" "pushNamed" [
        "routeName" :: "String",
        "arguments" :? "Object"
      ]
    ],
    class' "Route" [
    ],
    class' "RoutePredicate" [
    ],
    class' "ModalRoute" [
      static $ fun "RoutePredicate" "withName" [
        "name" :: "String"
      ]
    ],
    class' "Row" [
      extends "Widget",
      new "" [
        "children" :? "Dart.Core.List" :<> "Widget",
        "mainAxisAlignment" :? "MainAxisAlignment"
      ]
    ],
    class' "Padding" [
      extends "Widget",
      const $ new "" [
        "key" :? "Key",
        "padding" :? "EdgeInsetsGeometry",
        "child" :? "Widget"
      ]
    ],
    class' "SizedBox" [
      extends "Widget",
      const $ new "" [
        "key" :? "Key",
        "width" :? "double",
        "height" :? "double",
        "child" :? "Widget"
      ]
    ],
    class' "Text" [
      extends "Widget",
      const $ new "" [
        "text" :: "String",
        "textScaleFactor" :? "Double",
        "style" :? "TextStyle",
        "textAlign" :? "TextAlign"
      ]
    ],
    class' "TextEditingController" [
      new "" [
        "text" :? "String"
      ],
      var "TextEditingValue" "value"
    ],
    class' "Widget" [
    ],
    class' "WidgetBuilder" [
    ],
    class' "TransitionBuilder" [
    ]
  ],
  package "dart:ui" [
    enum "AppLifecycleState" [
      "detached",
      "inactive",
      "paused",
      "resumed"
    ],
    class' "Canvas" [
      io "void" "drawPath" [
        "path" :: "Path",
        "paint" :: "Paint"
      ]
    ],
    enum "Clip" [
      "antiAlias", "antiAliasWithSaveLayer", "hardEdge", "none"
    ],
    class' "Color" [
      const $ new "" [
        "value" :: "int"
      ],
      fun "Color" "withOpacity" [
        "opacity" :: "double"
      ]
    ],
    class' "Offset" [
      const $ new "" ["dx" :: "Double", "dy" :: "Double"],
      final "Double" "dx",
      final "Double" "dy"
    ],
    class' "Paint" [
      new "" [],
      var "PaintingStyle" "style",
      var "Double" "strokeWidth"
    ],
    enum "PaintingStyle" [
      "stroke"
    ],
    class' "Path" [
      new "" [],
      io "void" "moveTo" ["x" :: "Double", "y" :: "Double"],
      io "void" "lineTo" ["x" :: "Double", "y" :: "Double"]
    ],
    class' "Size" [
      final "Double" "width",
      final "Double" "height"
    ],
    enum "TextAlign" [
      "left",
      "right",
      "center",
      "start",
      "end",
      "justify"
    ],
    class' "Velocity" [
      final "Offset" "pixelsPerSecond"
    ]
  ],
  package "package:flutter/gestures.dart" [
    class' "LongPressEndDetails" [
      final "Offset" "globalPosition",
      final "Offset" "localPosition"
    ],
    class' "LongPressMoveUpdateDetails" [
      final "Offset" "localOffsetFromOrigin",
      final "Offset" "localPosition"
    ],
    class' "LongPressStartDetails" [
      final "Offset" "globalPosition",
      final "Offset" "localPosition"
    ],
    class' "TapDownDetails" [
      final "Offset" "globalPosition",
      final "Offset" "localPosition"
    ],
    class' "TapUpDetails" [
      final "Offset" "globalPosition",
      final "Offset" "localPosition"
    ]
  ],
  package "package:flutter/services.dart" [
    class' "FilteringTextInputFormatter" [
      static $ final "TextInputFormatter" "digitsOnly"
    ],
    class' "TextEditingValue" [
      final "String" "text"
    ],
    class' "TextInputFormatter" [
    ],
    class' "TextInputType" [
      static $ final "TextInputType" "datetime",
      static $ final "TextInputType" "emailAddress",
      static $ final "TextInputType" "multiline",
      static $ final "TextInputType" "name",
      static $ final "TextInputType" "number",
      static $ final "TextInputType" "phone",
      static $ final "TextInputType" "streetAddress",
      static $ final "TextInputType" "text",
      static $ final "TextInputType" "url",
      static $ final "TextInputType" "visiblePassword"
    ]
  ],
  package "package:flutter/scheduler.dart" [
    class' "TickerProvider" [
    ]
  ],
  package "package:flutter/animation.dart" [
    enum "AnimationBehavior" [
      "normal",
      "preserve"
    ],
    class' "AnimationController" [
      extends ("Animation" :<> "double"),
      extends "Listenable",
      new "" [
        "value" :? "double",
        "duration" :? "Duration",
        "reverseDuration" :? "Duration",
        "debugLabel" :? "String",
        "lowerBound" :? "double",
        "upperBound" :? "double",
        "animationBehavior" :? "AnimationBehavior",
        "vsync" :? "TickerProvider"
      ],
      io "void" "animateTo" ["value" :: "double"],
      generic ["u"] $
        io ("Animation" :<> "u") "drive" [
          "animatable" :: "Animatable" :<> "u"
        ],
      io "void" "dispose" []
    ],
    generic ["a"] $
      class' "Animatable" [
      ],
    generic ["a"] $
      class' "Animation" [
        getter "a" "value"
      ],
    class' "ColorTween" [
      extends ("Animatable" :<> "Color"),
      extends "Listenable",
      new "" [
        "begin" :? "Color",
        "end" :? "Color"
      ]
    ],
    class' "Curve" [
    ],
    class' "Curves" [
      static $ final "Curve" "bounceIn",
      static $ final "Curve" "bounceInOut",
      static $ final "Curve" "bounceOut",
      static $ final "Curve" "decelerate",
      static $ final "Curve" "ease",
      static $ final "Curve" "easeIn",
      static $ final "Curve" "easeInBack",
      static $ final "Curve" "easeInCirc",
      static $ final "Curve" "easeInCubic",
      static $ final "Curve" "easeInExpo",
      static $ final "Curve" "easeInOut",
      static $ final "Curve" "easeInOutBack",
      static $ final "Curve" "easeInOutCirc",
      static $ final "Curve" "easeInOutCubic",
      static $ final "Curve" "easeInOutCubicEmphasized",
      static $ final "Curve" "easeInOutExpo",
      static $ final "Curve" "easeInOutQuad",
      static $ final "Curve" "easeInOutQuart",
      static $ final "Curve" "easeInOutQuint",
      static $ final "Curve" "easeInOutSine",
      static $ final "Curve" "easeInQuad",
      static $ final "Curve" "easeInQuart",
      static $ final "Curve" "easeInQuint",
      static $ final "Curve" "easeInSine",
      static $ final "Curve" "easeInToLinear",
      static $ final "Curve" "easeOut",
      static $ final "Curve" "easeOutBack",
      static $ final "Curve" "easeOutCirc",
      static $ final "Curve" "easeOutCubic",
      static $ final "Curve" "easeOutExpo",
      static $ final "Curve" "easeOutQuad",
      static $ final "Curve" "easeOutQuart",
      static $ final "Curve" "easeOutQuint",
      static $ final "Curve" "easeOutSine",
      static $ final "Curve" "elasticIn",
      static $ final "Curve" "elasticInOut",
      static $ final "Curve" "elasticOut",
      static $ final "Curve" "fastLinearToSlowEaseIn",
      static $ final "Curve" "fastOutSlowIn",
      static $ final "Curve" "linear",
      static $ final "Curve" "linearToEaseOut",
      static $ final "Curve" "slowMiddle"
    ],
    class' "CurveTween" [
      extends ("Animatable" :<> "double"),
      extends "Listenable",
      new "" [
        "curve" :? "Curve"
      ]
    ],
    generic ["a"] $
      class' "TweenSequence" [
        -- extends ("Animatable" :<> "a"),
        extends "Listenable",
        new "" [
          "items" :: "Dart.Core.List" :<> ("TweenSequenceItem" :<> "a")
        ]
      ],
    generic ["a"] $
      class' "TweenSequenceItem" [
        const $ new "" [
          "tween" :? "Animatable" :<> "a",
          "weight" :? "double"
        ]
      ]
  ]
]

-- TODO: fix `extends` for generic types
public export
IsAssignableFrom (Animatable a) (TweenSequence a) where


text:
StringOrInt : (x : Bool) -> Type
StringOrInt False = String
StringOrInt True = Int

valToString : (isInt : Bool) -> StringOrInt isInt -> String
valToString False str = trim str
valToString True n = cast n

valToString' : (isInt : Bool) -> (case isInt of
                                       False => String
                                       True => Int) -> String
valToString' False x = trim x
valToString' True x = cast x


text:
||| System clock time.
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Time.Clock.System

import Data.Fixed

import Data.Time.Calendar.Types
import Data.Time.Calendar.Days
import Data.Time.Clock.Internal.UTCTime
import Data.Time.Clock.AbsoluteTime
import Data.Time.Clock.DiffTime
import Data.Time.LocalTime.TimeOfDay
import Data.Time.LocalTime.TimeZone

import System.Clock as CLK
import System.Info

%default total

-- ---------------------------------------------------------------------------

public export
data SystemTime : Type where [external]

%foreign "scheme,chez:current-time"
         "javascript:lambda:() => new Date()"
         "RefC:clockTimeUTC"
prim__systime_get : PrimIO SystemTime

export getSystemTime : HasIO io => io SystemTime
getSystemTime = primIO $ prim__systime_get

%foreign "scheme,chez:time-second"
         "javascript:lambda:(x) => (x.getTime() / 1000)"
         "RefC:clockSecond"
systemSeconds : SystemTime -> Int

%foreign "scheme,chez:time-nanosecond"
         "javascript:lambda:(x) => ((x.getTime() % 1000)* 1000000)"
         "RefC:clockNanosecond"
systemNanoseconds : SystemTime -> Int

%foreign "scheme,chez:(lambda (s ns) (make-time 'time-utc ns s))"
         "javascript:lambda:(s, ns) => new Date(s * 1000 + (ns / 1000000))"
toSystemTime : Int -> Int -> SystemTime

public export
Show SystemTime where
  show x = "#" ++ show (systemSeconds x) ++ "s+"
           ++ show (systemNanoseconds x) ++ "ns"

||| Map leap-second values to the start of the following second.
||| The resulting 'systemNanoseconds' will always be in the range 0 to 1E9-1.
export truncateSystemTimeLeapSecond : SystemTime -> SystemTime
truncateSystemTimeLeapSecond t =
  if systemNanoseconds t >= 1000000000
     then toSystemTime (systemSeconds t + 1) 0
     else t

||| The day of the epoch of 'SystemTime', 1970-01-01
export systemEpochDay : Day
systemEpochDay = ModifiedJulianDay 40587

export systemEpochAbsolute : AbsoluteTime
systemEpochAbsolute = taiNominalDayStart systemEpochDay

||| Convert 'SystemTime' to 'UTCTime', matching zero 'SystemTime' to midnight of 'systemEpochDay' UTC.
export systemToUTCTime : SystemTime -> UTCTime
systemToUTCTime t = let
  days = cast $ systemSeconds t `div` 86400
  day = addDays days systemEpochDay
  --
  timeseconds = systemSeconds t `mod` 86400
  timeNanoseconds = cast timeseconds * 1000000000 + cast (systemNanoseconds t)
  timePicoseconds = cast timeNanoseconds * 1000
  in MkUTCTime day $ picosecondsToDiffTime timePicoseconds

export getCurrentTime : HasIO io => io UTCTime
getCurrentTime = [| systemToUTCTime getSystemTime |]

||| Convert 'UTCTime' to 'SystemTime', matching zero 'SystemTime' to midnight of 'systemEpochDay' UTC.
export utcToSystemTime : UTCTime -> SystemTime
utcToSystemTime (MkUTCTime day time) = let
    days = diffDays day systemEpochDay
    timeNanoseconds = diffTimeToPicoseconds time `div` 1000
    (timeSeconds, nanoseconds) =
        if timeNanoseconds >= 86400000000000
            then (86399, timeNanoseconds - 86399000000000)
            else (timeNanoseconds `div` 1000000000, timeNanoseconds `mod` 1000000000)
    seconds = days * 86400 + timeSeconds
    in toSystemTime (cast seconds) $ cast nanoseconds

||| Convert 'SystemTime' to 'AbsoluteTime', matching zero 'SystemTime' to midnight of 'systemEpochDay' TAI.
export systemToTAITime : SystemTime -> AbsoluteTime
systemToTAITime t = let
    s = cast $ systemSeconds t
    ns = systemNanoseconds t
    diff = secondsToDiffTime (fromInteger s) + picosecondsToDiffTime (cast ns * 1000)
    in addAbsoluteTime diff systemEpochAbsolute

-- ---------------------------------------------------------------------------

public export data SystemLocalTime : Type where [external]

%foreign "scheme,chez:current-date"
         "javascript:lambda:() => new Date()"
export prim__getSystemLocalTime : PrimIO SystemLocalTime

export getSystemLocalTime : HasIO io => io SystemLocalTime
getSystemLocalTime = primIO prim__getSystemLocalTime

%foreign "scheme,chez:date-year"
         "javascript:lambda:(x) => x.getFullYear()"
prim__systemLocalTimeYear : SystemLocalTime -> Int

export systemLocalTimeYear : SystemLocalTime -> Integer
systemLocalTimeYear = cast . prim__systemLocalTimeYear

%foreign "scheme,chez:date-month"
         "javascript:lambda:(x) => x.getMonth()"
export systemLocalTimeMonth : SystemLocalTime -> Int

%foreign "scheme,chez:date-day"
         "javascript:lambda:(x) => x.getDate()"
export systemLocalTimeDay : SystemLocalTime -> Int

%foreign "scheme,chez:date-hour"
         "javascript:lambda:(x) => x.getHours()"
export systemLocalTimeHour : SystemLocalTime -> Int

%foreign "scheme,chez:date-minute"
         "javascript:lambda:(x) => x.getMinutes()"
export systemLocalTimeMinute : SystemLocalTime -> Int

%foreign "scheme,chez:date-second"
         "javascript:lambda:(x) => x.getSeconds()"
export systemLocalTimeSecond : SystemLocalTime -> Int

%foreign "scheme,chez:date-nanosecond"
         "javascript:lambda:(x) => (x.getMilliseconds() * 1000000)"
export systemLocalTimeNanosecond : SystemLocalTime -> Int

%foreign "scheme,chez:date-zone-offset"
         "javascript:lambda:(x) => x.getTimezoneOffset()"
export systemLocalTimeOffset : SystemLocalTime -> Int

%foreign "scheme,chez:(lambda (x) \"\")"
         "javascript:lambda:(x) => ''"
export systemLocalTimeZoneName : SystemLocalTime -> String

%foreign "scheme,chez:(lambda (x) #f)"
         "javascript:lambda:(x) => false"
export systemLocalTimeIsSummerTime : SystemLocalTime -> Bool

export systemLocalDate : SystemLocalTime -> (Year, MonthOfYear, DayOfMonth)
systemLocalDate t = let
  y = systemLocalTimeYear t
  m = systemLocalTimeMonth t
  d = systemLocalTimeDay t
  in (cast y, m, d)

export systemLocalTimeOfDay : SystemLocalTime -> TimeOfDay
systemLocalTimeOfDay t = let
  h = systemLocalTimeHour t
  m = systemLocalTimeMinute t
  s = systemLocalTimeSecond t
  ns = systemLocalTimeNanosecond t
  in MkTimeOfDay h m (cast s + MkFixed (cast $ ns * 1000))

export systemLocalTimeZone : SystemLocalTime -> TimeZone
systemLocalTimeZone t = let
  m = negate $ systemLocalTimeOffset t `div` 60
  in MkTimeZone m (systemLocalTimeIsSummerTime t) (systemLocalTimeZoneName t)

export getCurrentTimeZone : IO TimeZone
getCurrentTimeZone = getSystemLocalTime >>= pure . systemLocalTimeZone

public export
Show SystemLocalTime where
  show x = let
    (y, m, d) = systemLocalDate x
    td = systemLocalTimeOfDay x
    tz = systemLocalTimeZone x
    in show y ++ "-" ++ show m ++ "-" ++ show d ++ " "
       ++ show td ++ " " ++ show tz

-- vim: tw=80 sw=2 expandtab :


text:
module EditorMode

%default total

public export
data EditorMode = Insert | Normal | Quit

max_stars_repo_name: PeterHajdu/peti

max_issues_repo_name: PeterHajdu/peti

max_forks_repo_name: PeterHajdu/peti