text:
> module NonNegRational.BasicOperations

> import NonNegRational.NonNegRational
> import Fraction.Fraction
> import Fraction.BasicOperations
> import Fraction.BasicProperties
> import Fraction.Normalize
> import Fraction.NormalizeProperties
> import Pairs.Operations
> import Sigma.Sigma

> %default total
> %access public export

> |||
> toFraction : NonNegRational -> Fraction
> toFraction = getWitness -- PairsOperations.Subset.getWitness
> -- %freeze toFraction

> |||
> fromFraction : Fraction -> NonNegRational
> fromFraction x = Element (normalize x) (normalNormalize x)
> %freeze fromFraction

> ||| The numerator of a non-negative rational
> num : NonNegRational -> Nat
> num = num . toFraction
> -- %freeze num

> ||| The denominator of a non-negative rational
> den : NonNegRational -> Nat
> den = den . toFraction
> -- %freeze den

> ||| Every natural number is a non-negative rational
> fromNat : (n : Nat) -> NonNegRational
> fromNat = fromFraction . fromNat
> -- %freeze fromNat

> ||| Addition of non-negative rational numbers
> plus : NonNegRational -> NonNegRational -> NonNegRational
> plus x y = fromFraction (toFraction x + toFraction y)
> -- %freeze plus

> ||| Multiplication of non-negative rational numbers
> mult : NonNegRational -> NonNegRational -> NonNegRational
> mult x y = fromFraction (toFraction x * toFraction y)
> -- %freeze mult


text:
import Control.Indexed
import Control.Monad.Indexed.State

data State = One | Two | Three

data Transition : Type -> State -> State -> Type where
  Pure : (x : a) -> Transition a s s
  First : Transition () One Two
  Second : Transition () Two Three
  Third : Transition () Three One
  Bind : Transition a x y -> (a -> Transition b y z) -> Transition b x z

IndexedFunctor State State Transition where
  map f (Pure x)   = Pure (f x)
  map f First      = Bind First  (Pure . f)
  map f Second     = Bind Second (Pure . f)
  map f Third      = Bind Third  (Pure . f)
  map f (Bind x g) = Bind x (\x' => map f (g x'))

[n1] IndexedApplicative State Transition where
  pure = Pure
  ap (Pure f) x = map f x
  ap (Bind y f) x =
    Bind y $ \y' =>
      Bind (f y') $ \f' =>
        Bind x (\x' => Pure (f' x'))

IndexedMonad State Transition using n1 where
  bind = Bind

data Meta = Description String

||| A Transition plus some metadata
TransitionPlus : Type -> State -> State -> Type
TransitionPlus = IndexedStateT Meta State State Transition

main : TransitionPlus () One One
main = do
  put $ Description "meta text"
  lift $ do
    First
    Second
  x <- get
  lift $ do
    Indexed.ignore $ Pure x
    Third

ext: idr

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
module Subst

-- This module constructs an expressively typed substitution
-- function 'subst' for substituting variables in the simply-typed
-- lambda calculus.
--
-- The key point is that the expressive type signature of the
-- function 'subst' can be read as the following theorem:
--
--    "Given a context 'ctx' and a variable with
--     de Bruijn index 'i'. Given further the terms
--       ts : Term [] s, and
--       tt : Term (insertAt i s ctx) t.
--     Then 'subst ts i tt' has type 't' in context 'ctx'."
--
-- Note that 'subst ts i tt' is typically written as "tt[ts/(Var i)]".
--
-- Note that the theorem that is expressed by the type signature
-- of 'subst' is usually referred to as
--
--    *** the substitution lemma ***
--
-- ans casually summarized as
--
--    *** substitution preserves type ***.
--

import FinCmp
import Term

%default total

-------------------------------------------------------------
-- Begin: WEAKENING, I.E. ADDING UNUSED VARIABLES TO CONTEXTS

-- Abbreviate the name of the function 'weakenN'
-- from 'Data.Fin' (for better readability):
wkN : (n : Nat) -> Fin m -> Fin (m + n)
wkN = Data.Fin.weakenN

-- Note that we only require weakening of a context 'ctx'
-- by appending another context on the right only.
weakeningPreservesType : {ctx : Context m} -> {ctx' : Context n} ->
                         {i : Fin m} ->
                         (index i ctx = t) ->
                         (index (wkN n i) (ctx ++ ctx') = t)
weakeningPreservesType {ctx = (_::_)}   {i = FZ}      eq = eq
weakeningPreservesType {ctx = (_:: xs)} {i = (FS i')} eq =
  weakeningPreservesType {i = i'} eq

weakenContext : {m : Nat} -> (ctx : Context m) ->
                {n : Nat} -> (ctx' : Context n) ->
                Term ctx t ->
                Term (ctx ++ ctx') t
weakenContext ctx {n = n} ctx' (TVar i {prf = p}) =
  TVar (wkN n i) {prf = weakeningPreservesType p}
--
weakenContext ctx ctx' (TAbs {s} e)       = TAbs (weakenContext (s::ctx) ctx' e)
weakenContext ctx ctx' (TApp e1 e2)       = TApp (weakenContext ctx ctx' e1)
                                                 (weakenContext ctx ctx' e2)
weakenContext ctx ctx' (TRec {t} e e0 e1) = TRec (weakenContext ctx ctx' e)
                                                 (weakenContext ctx ctx' e0)
                                                 (weakenContext (t::TyNat::ctx) ctx' e1)
weakenContext _   _    TZero              = TZero
weakenContext ctx ctx' (TSucc e)          = TSucc (weakenContext ctx ctx' e)
weakenContext ctx ctx' (TPred e)          = TPred (weakenContext ctx ctx' e)
weakenContext ctx ctx' (TIfz e1 e2 e3)    = TIfz (weakenContext ctx ctx' e1)
                                                 (weakenContext ctx ctx' e2)
                                                 (weakenContext ctx ctx' e3)

-- End: WEAKENING, I.E. ADDING UNUSED VARIABLES TO CONTEXTS
-----------------------------------------------------------

-----------------------------------------------------------------
-- Begin: TECHNICAL LEMMATA ABOUT INDEXING INTO MODIFIED CONTEXTS

-- Function 'lookupInserted' yields a proof of the following:
--
--     "Let ctx' = insertAt i s ctx, and let i = j.
--      If (index j ctx' = t), then t = s."
--
lookupInserted : {ctx : Context n} -> {s : Ty} -> {t : Ty} ->
                 {i : Fin (S n)} -> {j : Fin (S n)} ->
                 i = j ->
                 index j (insertAt i s ctx) = t ->
                 t = s
lookupInserted                {i = FZ}      {j = FZ}      _  prf = sym prf
lookupInserted {ctx} {s} {t}  {i = FZ}      {j = (FS j')} eq prf =
  sym $ replace {P = \k => index k (insertAt FZ s ctx) = t} (sym eq) prf
--
lookupInserted {ctx} {s} {t}  {i = (FS i')} {j = FZ}      eq prf =
  sym $ replace {P = \k => index FZ (insertAt k s ctx) = t} eq prf
--
lookupInserted {ctx = (_::_)} {i = (FS i')} {j = (FS j')} eq  prf =
  lookupInserted (FSinjective eq) prf

-- Function 'shiftDown' yields a proof of the following:
--
--     "Let ctx' = insertAt i s ctx, and let i < (j+1).
--      If (index (j+1) ctx' = t), then (index j ctx = t)."
--
shiftDown : {ctx : Context n} -> {s : Ty} ->
            {i : Fin (S n)} -> {j : Fin n} ->
            i :<: (FS j) ->
            index (FS j) (insertAt i s ctx) = t ->
            index j ctx = t
--
shiftDown {i = FZ}     {j = _}      _  prf = prf
shiftDown {i = (FS _)} {j = FZ}     lt prf =
  absurd $ finNotLtZ $ finLtPred lt
--
shiftDown {ctx = (_::xs)} {s} {i = (FS i')} {j = (FS j')} lt prf =
  shiftDown {ctx = xs} {s} {i = i'} {j = j'} (finLtPred lt) prf

-- Function 'indexZeroLemma' yields a proof of the following:
--
--     "Let ctx a non-empty context, and let ctx' = insertAt t (i+1) ctx.
--      Then, (index 0 ctx') = (index 0 ctx)."
--
indexZeroLemma : {ctx : Context (S n)} ->
                 (i : Fin (S n)) ->
                 index FZ (insertAt (FS i) t ctx) = index FZ ctx
--
indexZeroLemma {ctx = (_::_)} _ = Refl

-- Function 'pushLemma' yields a proof of the following:
--
--    "Let ctx be a context, and let (index i ctx = t).
--     Then, index (i+1) (s::ctx) = t."
--
pushLemma : (s : Ty) ->
            index i ctx = t ->
            index (FS i) (s::ctx) = t
pushLemma _ eq = eq

-- Function 'tightenBound' yields a proof of the following:
--
--     "Let ctx be a context, and let ctx' = insertAt i s ctx.
--      If (j < i) and (index j ctx' = t), then index j ctx = t."
--
-- The function 'tightenBound' returns a dependent pair.
--
-- The first component of the pair is 'j_', which represents
-- the same value as the function argument 'j' (as natural
-- numbers); but note that the bound on the ordinal 'j_' has
-- been tightened (by using the assumption "j < i"):
--   "j_ : Fin n"  while  "j : Fin (S n)".
--
-- The second component of the dependent pair is a proof of
--   "index j_ ctx = t".
--
tightenBound :  {n : Nat} -> {ctx : Context n} ->
                (j : Fin (S n)) -> {i : Fin (S n)} ->
                j :<: i ->
                index j (insertAt i s ctx) = t ->
                (j_ : Fin n ** (index j_ ctx = t))
--
tightenBound                 _       {i = FZ}      lt _  =
  absurd $ finNotLtZ lt
--
tightenBound {n = (S n')}    FZ      {i = (FS i')} _  eq =
  let izl = indexZeroLemma i'
      eq_ = trans (sym izl) eq
  in (FZ ** eq_)
--
tightenBound {ctx = (x::xs)} (FS j') {i = (FS i')} lt eq =
  let (j_ ** eq_) = tightenBound {ctx = xs} j' (finLtPred lt) eq
  in (FS j_ ** pushLemma x eq_)

-- End: TECHNICAL LEMMATA ABOUT INDEXING INTO MODIFIED CONTEXTS
---------------------------------------------------------------

-----------------------------------------------------------------------------
-- Begin: SUBSTITUTION PRESERVES TYPING OF EXPRESSIONS IN THE LAMBDA CALCULUS

subst_var : Term [] s ->        -- Term of type 's' is subtituted in.
            (i : Fin (S n)) ->  -- The i-th variable (Var i) is substituted for.
            (j : Fin (S n)) ->  -- Substitution takes place inside the term (Var j).
            index j (insertAt i s ctx) = t ->
            Term ctx t
--
-- An actual substitution occurs only if "i = j".
--
-- For "i /= j" no substitution occurs, but the proof 'prf'
-- in the returned expression 'TVar _ {prf}' has to be
-- adjusted to account for the fact that the context has
-- been shortened from (insertAt s i ctx) to 'ctx'.
subst_var {ctx} {s} ts i j prf = case finCmpDec i j of
  CmpEq eq => let ts' = weakenContext [] ctx ts
              in rewrite (lookupInserted eq prf) in ts'
  CmpLt lt => case j of
    FZ    => absurd $ finNotLtZ lt
    FS j' => TVar j' {prf = shiftDown lt prf}
  CmpGt gt => case i of
    FZ    => absurd $ finNotLtZ gt
    FS i' => let (j_ ** prf_) = tightenBound j gt prf
             in TVar j_ {prf = prf_}

export subst : Term [] s ->                  -- Term of type 's' is substituted in.
               (i : Fin (S n)) ->            -- The i-th varibale (Var i) is substituted for.
               Term (insertAt i s ctx) t ->  -- Substitution takes place inside this
                                             -- term of type 't'
               Term ctx t                    -- The resulting term is again of type 't'.
--
-- The hard part is substitution in expressions that
-- are variables, i.e. substitution in 'Var j'.
subst ts i (TVar j {prf}) = subst_var ts i j prf
--
-- Substitution in expressions that are not variables
-- is handled by recursing over (and substituting in)
-- subexpressions:
subst ts i (TAbs e)        = TAbs (subst ts (FS i) e)
subst ts i (TApp e1 e2)    = TApp (subst ts i e1) (subst ts i e2)
subst ts i (TRec e e0 e1)  = TRec (subst ts i e) (subst ts i e0) (subst ts (FS $ FS i) e1)
subst _  _ TZero           = TZero
subst ts i (TSucc e)       = TSucc (subst ts i e)
subst ts i (TPred e)       = TPred (subst ts i e)
subst ts i (TIfz e1 e2 e3) = TIfz (subst ts i e1) (subst ts i e2) (subst ts i e3)

-- End: SUBSTITUTION PRESERVES TYPING OF EXPRESSIONS IN THE LAMBDA CALCULUS
---------------------------------------------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Proofs.SemigroupTheory

import Specifications.Semigroup

%default total
%access export

abelianCongruence : isAbelian op -> x = y -> op x a = op a y
abelianCongruence {a} {x} abel given = abel x a === cong given

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Chez

public export
data SchemeVal = Op1

-- TODO: need lists and vector. Should fix representation of them first
public export
data SchemeTypes : Type -> Type where
    S_Int : SchemeTypes Int
    S_Nat : SchemeTypes Nat
    S_Integer : SchemeTypes Integer
    S_Real : SchemeTypes Double
    S_Bool : SchemeTypes Bool
    S_Unit : SchemeTypes ()
    S_Char : SchemeTypes Char
    S_String : SchemeTypes String

    S_Fun : SchemeTypes a -> SchemeTypes b -> SchemeTypes (a -> b)
    S_Opaque : SchemeTypes SchemeVal

public export
FFI_S : FFI
FFI_S = MkFFI SchemeTypes String String

public export
SIO : Type -> Type
SIO = IO' FFI_S

max_stars_repo_name: melted/idris-chez

max_issues_repo_name: melted/idris-chez

max_forks_repo_name: melted/idris-chez


text:
module TTImp.ProcessData

import Core.CompileExpr
import Core.Context
import Core.Context.Data
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Hash
import Core.Metadata
import Core.Normalise
import Core.UnifyState
import Core.Value

import TTImp.BindImplicits
import TTImp.Elab.Check
import TTImp.Elab.Utils
import TTImp.Elab
import TTImp.TTImp
import TTImp.Utils

import Data.DPair
import Data.List
import Libraries.Data.NameMap

%default covering

processDataOpt : {auto c : Ref Ctxt Defs} ->
                 FC -> Name -> DataOpt -> Core ()
processDataOpt fc n NoHints
    = pure ()
processDataOpt fc ndef (SearchBy dets)
    = setDetermining fc ndef dets
processDataOpt fc ndef UniqueSearch
    = setUniqueSearch fc ndef True
processDataOpt fc ndef External
    = setExternal fc ndef True
processDataOpt fc ndef NoNewtype
    = pure ()

checkRetType : {auto c : Ref Ctxt Defs} ->
               Env Term vars -> NF vars ->
               (NF vars -> Core ()) -> Core ()
checkRetType env (NBind fc x (Pi _ _ _ ty) sc) chk
    = do defs <- get Ctxt
         checkRetType env !(sc defs (toClosure defaultOpts env (Erased fc False))) chk
checkRetType env nf chk = chk nf

checkIsType : {auto c : Ref Ctxt Defs} ->
              FC -> Name -> Env Term vars -> NF vars -> Core ()
checkIsType loc n env nf
    = checkRetType env nf $
         \case
           NType _ => pure ()
           _ => throw $ BadTypeConType loc n

checkFamily : {auto c : Ref Ctxt Defs} ->
              FC -> Name -> Name -> Env Term vars -> NF vars -> Core ()
checkFamily loc cn tn env nf
    = checkRetType env nf $
         \case
           NType _ => throw $ BadDataConType loc cn tn
           NTCon _ n' _ _ _ =>
                 if tn == n'
                    then pure ()
                    else throw $ BadDataConType loc cn tn
           _ => throw $ BadDataConType loc cn tn

updateNS : Name -> Name -> RawImp -> RawImp
updateNS orig ns (IPi fc c p n ty sc) = IPi fc c p n ty (updateNS orig ns sc)
updateNS orig ns tm = updateNSApp tm
  where
    updateNSApp : RawImp -> RawImp
    updateNSApp (IVar fc n) -- data type type, must be defined in this namespace
        = if n == orig
             then IVar fc ns
             else IVar fc n
    updateNSApp (IApp fc f arg) = IApp fc (updateNSApp f) arg
    updateNSApp (IAutoApp fc f arg) = IAutoApp fc (updateNSApp f) arg
    updateNSApp (INamedApp fc f n arg) = INamedApp fc (updateNSApp f) n arg
    updateNSApp t = t

checkCon : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto m : Ref MD Metadata} ->
           {auto u : Ref UST UState} ->
           List ElabOpt -> NestedNames vars ->
           Env Term vars -> Visibility -> (orig : Name) -> (resolved : Name) ->
           ImpTy -> Core Constructor
checkCon {vars} opts nest env vis tn_in tn (MkImpTy fc _ cn_in ty_raw)
    = do cn <- inCurrentNS cn_in
         let ty_raw = updateNS tn_in tn ty_raw
         log "declare.data.constructor" 5 $ "Checking constructor type " ++ show cn ++ " : " ++ show ty_raw
         log "declare.data.constructor" 10 $ "Updated " ++ show (tn_in, tn)

         defs <- get Ctxt
         -- Check 'cn' is undefined
         Nothing <- lookupCtxtExact cn (gamma defs)
             | Just gdef => throw (AlreadyDefined fc cn)
         ty <-
             wrapErrorC opts (InCon fc cn) $
                   checkTerm !(resolveName cn) InType opts nest env
                              (IBindHere fc (PI erased) ty_raw)
                              (gType fc)

         -- Check 'ty' returns something in the right family
         checkFamily fc cn tn env !(nf defs env ty)
         let fullty = abstractEnvType fc env ty
         logTermNF "declare.data.constructor" 5 ("Constructor " ++ show cn) [] fullty

         traverse_ addToSave (keys (getMetas ty))
         addToSave cn
         log "declare.data.constructor" 10 $ "Saving from " ++ show cn ++ ": " ++ show (keys (getMetas ty))

         case vis of
              Public => do addHashWithNames cn
                           addHashWithNames fullty
              _ => pure ()
         pure (MkCon fc cn !(getArity defs [] fullty) fullty)

-- Get the indices of the constructor type (with non-constructor parts erased)
getIndexPats : {auto c : Ref Ctxt Defs} ->
               ClosedTerm -> Core (List (NF []))
getIndexPats tm
    = do defs <- get Ctxt
         tmnf <- nf defs [] tm
         ret <- getRetType defs tmnf
         getPats defs ret
  where
    getRetType : Defs -> NF [] -> Core (NF [])
    getRetType defs (NBind fc _ (Pi _ _ _ _) sc)
        = do sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
             getRetType defs sc'
    getRetType defs t = pure t

    getPats : Defs -> NF [] -> Core (List (NF []))
    getPats defs (NTCon fc _ _ _ args)
        = traverse (evalClosure defs . snd) args
    getPats defs _ = pure [] -- Can't happen if we defined the type successfully!

getDetags : {auto c : Ref Ctxt Defs} ->
            FC -> List ClosedTerm -> Core (Maybe (List Nat))
getDetags fc [] = pure (Just []) -- empty type, trivially detaggable
getDetags fc [t] = pure (Just []) -- one constructor, trivially detaggable
getDetags fc tys
   = do ps <- traverse getIndexPats tys
        case !(getDisjointPos 0 (transpose ps)) of
             [] => pure $ Nothing
             xs => pure $ Just xs
  where
    mutual
      disjointArgs : List (NF []) -> List (NF []) -> Core Bool
      disjointArgs [] _ = pure False
      disjointArgs _ [] = pure False
      disjointArgs (a :: args) (a' :: args')
          = if !(disjoint a a')
               then pure True
               else disjointArgs args args'

      disjoint : NF [] -> NF [] -> Core Bool
      disjoint (NDCon _ _ t _ args) (NDCon _ _ t' _ args')
          = if t /= t'
               then pure True
               else do defs <- get Ctxt
                       argsnf <- traverse (evalClosure defs . snd) args
                       args'nf <- traverse (evalClosure defs . snd) args'
                       disjointArgs argsnf args'nf
      disjoint (NTCon _ n _ _ args) (NDCon _ n' _ _ args')
          = if n /= n'
               then pure True
               else do defs <- get Ctxt
                       argsnf <- traverse (evalClosure defs . snd) args
                       args'nf <- traverse (evalClosure defs . snd) args'
                       disjointArgs argsnf args'nf
      disjoint (NPrimVal _ c) (NPrimVal _ c') = pure (c /= c')
      disjoint _ _ = pure False

    allDisjointWith : NF [] -> List (NF []) -> Core Bool
    allDisjointWith val [] = pure True
    allDisjointWith (NErased _ _) _ = pure False
    allDisjointWith val (nf :: nfs)
        = do ok <- disjoint val nf
             if ok then allDisjointWith val nfs
                   else pure False

    allDisjoint : List (NF []) -> Core Bool
    allDisjoint [] = pure True
    allDisjoint (NErased _ _ :: _) = pure False
    allDisjoint (nf :: nfs)
        = do ok <- allDisjoint nfs
             if ok then allDisjointWith nf nfs
                   else pure False

    -- Which argument positions have completely disjoint contructors
    getDisjointPos : Nat -> List (List (NF [])) -> Core (List Nat)
    getDisjointPos i [] = pure []
    getDisjointPos i (args :: argss)
        = do rest <- getDisjointPos (1 + i) argss
             if !(allDisjoint args)
                then pure (i :: rest)
                else pure rest

-- If exactly one argument is unerased, return its position
getRelevantArg : {auto c : Ref Ctxt Defs} ->
                 Defs -> Nat -> Maybe Nat -> Bool -> NF [] ->
                 Core (Maybe (Bool, Nat))
getRelevantArg defs i rel world (NBind fc _ (Pi _ rig _ val) sc)
    = branchZero (getRelevantArg defs (1 + i) rel world
                              !(sc defs (toClosure defaultOpts [] (Erased fc False))))
                 (case !(evalClosure defs val) of
                       -- %World is never inspected, so might as well be deleted from data types,
                       -- although it needs care when compiling to ensure that the function that
                       -- returns the IO/%World type isn't erased
                       (NPrimVal _ WorldType) =>
                           getRelevantArg defs (1 + i) rel False
                               !(sc defs (toClosure defaultOpts [] (Erased fc False)))
                       _ =>
                       -- if we haven't found a relevant argument yet, make
                       -- a note of this one and keep going. Otherwise, we
                       -- have more than one, so give up.
                           maybe (do sc' <- sc defs (toClosure defaultOpts [] (Erased fc False))
                                     getRelevantArg defs (1 + i) (Just i) False sc')
                                 (const (pure Nothing))
                                 rel)
                 rig
getRelevantArg defs i rel world tm
    = pure (maybe Nothing (\r => Just (world, r)) rel)

-- If there's one constructor with only one non-erased argument, flag it as
-- a newtype for optimisation
export
findNewtype : {auto c : Ref Ctxt Defs} ->
              List Constructor -> Core ()
findNewtype [con]
    = do defs <- get Ctxt
         Just arg <- getRelevantArg defs 0 Nothing True !(nf defs [] (type con))
              | Nothing => pure ()
         updateDef (name con) $
               \case
                 DCon t a _ => Just $ DCon t a $ Just arg
                 _ => Nothing
findNewtype _ = pure ()

hasArgs : Nat -> Term vs -> Bool
hasArgs (S k) (Bind _ _ (Pi _ c _ _) sc)
    = if isErased c
         then hasArgs (S k) sc
         else hasArgs k sc
hasArgs (S k) _ = False
hasArgs Z (Bind _ _ (Pi _ c _ _) sc)
    = if isErased c
         then hasArgs Z sc
         else False
hasArgs Z _ = True

-- get the first non-erased argument
firstArg : Term vs -> Maybe (Exists Term)
firstArg (Bind _ _ (Pi _ c _ val) sc)
    = if isErased c
         then firstArg sc
         else Just $ Evidence _ val
firstArg tm = Nothing

typeCon : Term vs -> Maybe Name
typeCon (Ref _ (TyCon _ _) n) = Just n
typeCon (App _ fn _) = typeCon fn
typeCon _ = Nothing

shaped : {auto c : Ref Ctxt Defs} ->
         (forall vs . Term vs -> Bool) ->
         List Constructor -> Core (Maybe Name)
shaped as [] = pure Nothing
shaped as (c :: cs)
    = do defs <- get Ctxt
         if as !(normalise defs [] (type c))
            then pure (Just (name c))
            else shaped as cs

-- Calculate whether the list of constructors gives a list-shaped type
-- If there's two constructors, one with no unerased arguments and one
-- with two unerased arguments, then it's listy.
-- If there's one constructor, with two unerased arugments, we can also
-- treat that as a cons cell, which will be cheaper for pairs.
-- Note they don't have to be recursive! It's just about whether we can
-- pair cheaply.
calcListy : {auto c : Ref Ctxt Defs} ->
            FC -> List Constructor -> Core Bool
calcListy fc cs@[_]
    = do Just cons <- shaped (hasArgs 2) cs
              | Nothing => pure False
         setFlag fc cons (ConType CONS)
         pure True
calcListy fc cs@[_, _]
    = do Just nil <- shaped (hasArgs 0) cs
              | Nothing => pure False
         Just cons <- shaped (hasArgs 2) cs
              | Nothing => pure False
         setFlag fc nil (ConType NIL)
         setFlag fc cons (ConType CONS)
         pure True
calcListy _ _ = pure False

-- It's option type shaped if there's two constructors, one of which has
-- zero arguments, and one of which has one.
calcMaybe : {auto c : Ref Ctxt Defs} ->
            FC -> List Constructor -> Core Bool
calcMaybe fc cs@[_, _]
    = do Just nothing <- shaped (hasArgs 0) cs
              | Nothing => pure False
         Just just <- shaped (hasArgs 1) cs
              | Nothing => pure False
         setFlag fc nothing (ConType NOTHING)
         setFlag fc just (ConType JUST)
         pure True
calcMaybe _ _ = pure False

calcEnum : {auto c : Ref Ctxt Defs} ->
           FC -> List Constructor -> Core Bool
calcEnum fc cs
    = if !(allM isNullary cs)
         then do traverse_ (\c => setFlag fc c (ConType ENUM)) (map name cs)
                 pure True
         else pure False
  where
    isNullary : Constructor -> Core Bool
    isNullary c
        = do defs <- get Ctxt
             pure $ hasArgs 0 !(normalise defs [] (type c))

calcRecord : {auto c : Ref Ctxt Defs} ->
             FC -> List Constructor -> Core Bool
calcRecord fc [c]
    = do setFlag fc (name c) (ConType RECORD)
         pure True
calcRecord _ _ = pure False

-- has two constructors
-- - ZERO: 0 args
-- - SUCC: 1 arg, of same type
calcNaty : {auto c : Ref Ctxt Defs} ->
           FC -> Name -> List Constructor -> Core Bool
calcNaty fc tyCon cs@[_, _]
    = do Just zero <- shaped (hasArgs 0) cs
              | Nothing => pure False
         Just succ <- shaped (hasArgs 1) cs
              | Nothing => pure False
         let Just succCon = find (\con => name con == succ) cs
              | Nothing => pure False
         let Just (Evidence _ succArgTy) = firstArg (type succCon)
              | Nothing => pure False
         let Just succArgCon = typeCon succArgTy
              | Nothing => pure False
         if succArgCon == tyCon
            then do setFlag fc zero (ConType ZERO)
                    setFlag fc succ (ConType SUCC)
                    pure True
            else pure False
calcNaty _ _ _ = pure False

calcConInfo : {auto c : Ref Ctxt Defs} ->
              FC -> Name -> List Constructor -> Core ()
calcConInfo fc type cons
   = do False <- calcNaty fc type cons
           | True => pure ()
        False <- calcListy fc cons
           | True => pure ()
        False <- calcMaybe fc cons
           | True => pure ()
        False <- calcEnum fc cons
           | True => pure ()
        False <- calcRecord fc cons
           | True => pure ()
        pure ()
     -- ... maybe more to come? The Bool just says when to stop looking

export
processData : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              List ElabOpt -> NestedNames vars ->
              Env Term vars -> FC -> Visibility ->
              ImpData -> Core ()
processData {vars} eopts nest env fc vis (MkImpLater dfc n_in ty_raw)
    = do n <- inCurrentNS n_in
         ty_raw <- bindTypeNames fc [] vars ty_raw

         defs <- get Ctxt
         -- Check 'n' is undefined
         Nothing <- lookupCtxtExact n (gamma defs)
             | Just gdef => throw (AlreadyDefined fc n)

         (ty, _) <-
             wrapErrorC eopts (InCon fc n) $
                    elabTerm !(resolveName n) InType eopts nest env
                              (IBindHere fc (PI erased) ty_raw)
                              (Just (gType dfc))
         let fullty = abstractEnvType dfc env ty
         logTermNF "declare.data" 5 ("data " ++ show n) [] fullty

         checkIsType fc n env !(nf defs env ty)
         arity <- getArity defs [] fullty

         -- Add the type constructor as a placeholder
         tidx <- addDef n (newDef fc n linear vars fullty vis
                          (TCon 0 arity [] [] defaultFlags [] [] Nothing))
         addMutData (Resolved tidx)
         defs <- get Ctxt
         traverse_ (\n => setMutWith fc n (mutData defs)) (mutData defs)

         traverse_ addToSave (keys (getMetas ty))
         addToSave n
         log "declare.data" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))

         case vis of
              Private => pure ()
              _ => do addHashWithNames n
                      addHashWithNames fullty

processData {vars} eopts nest env fc vis (MkImpData dfc n_in ty_raw opts cons_raw)
    = do n <- inCurrentNS n_in
         ty_raw <- bindTypeNames fc [] vars ty_raw

         log "declare.data" 1 $ "Processing " ++ show n
         defs <- get Ctxt
         (ty, _) <-
             wrapErrorC eopts (InCon fc n) $
                    elabTerm !(resolveName n) InType eopts nest env
                              (IBindHere fc (PI erased) ty_raw)
                              (Just (gType dfc))
         let fullty = abstractEnvType dfc env ty

         -- If n exists, check it's the same type as we have here, and is
         -- a data constructor.
         -- When looking up, note the data types which were undefined at the
         -- point of declaration.
         ndefm <- lookupCtxtExact n (gamma defs)
         mw <- case ndefm of
                  Nothing => pure []
                  Just ndef =>
                    case definition ndef of
                         TCon _ _ _ _ _ mw [] _ =>
                            do ok <- convert defs [] fullty (type ndef)
                               if ok then pure mw
                                     else do logTermNF "declare.data" 1 "Previous" [] (type ndef)
                                             logTermNF "declare.data" 1 "Now" [] fullty
                                             throw (AlreadyDefined fc n)
                         _ => throw (AlreadyDefined fc n)

         logTermNF "declare.data" 5 ("data " ++ show n) [] fullty

         checkIsType fc n env !(nf defs env ty)
         arity <- getArity defs [] fullty

         -- Add the type constructor as a placeholder while checking
         -- data constructors
         tidx <- addDef n (newDef fc n linear vars fullty vis
                          (TCon 0 arity [] [] defaultFlags [] [] Nothing))
         case vis of
              Private => pure ()
              _ => do addHashWithNames n
                      addHashWithNames fullty

         -- Constructors are private if the data type as a whole is
         -- export
         let cvis = if vis == Export then Private else vis
         cons <- traverse (checkCon eopts nest env cvis n_in (Resolved tidx)) cons_raw

         let ddef = MkData (MkCon dfc n arity fullty) cons
         ignore $ addData vars vis tidx ddef

         -- Flag data type as a newtype, if possible (See `findNewtype` for criteria).
         -- Skip optimisation if the data type has specified `noNewtype` in its
         -- options list.
         when (not (NoNewtype `elem` opts)) $
              findNewtype cons

         -- Type is defined mutually with every data type undefined at the
         -- point it was declared, and every data type undefined right now
         defs <- get Ctxt
         let mutWith = nub (mw ++ mutData defs)
         log "declare.data" 3 $ show n ++ " defined in a mutual block with " ++ show mw
         setMutWith fc (Resolved tidx) mw

         traverse_ (processDataOpt fc (Resolved tidx)) opts
         dropMutData (Resolved tidx)

         detags <- getDetags fc (map type cons)
         setDetags fc (Resolved tidx) detags

         traverse_ addToSave (keys (getMetas ty))
         addToSave n
         log "declare.data" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))

         let connames = map name cons
         unless (NoHints `elem` opts) $
              traverse_ (\x => addHintFor fc (Resolved tidx) x True False) connames

         calcConInfo fc (Resolved tidx) cons
         traverse_ updateErasable (Resolved tidx :: connames)


text:
module Data.Int.Algebra

import Control.Algebra

%access public export

--- ||| Return the smallest non-negative representative of the class of a modulo n.
leastPositiveResidue : (Integral ty, Ord ty) => (a : ty) -> (b : ty) -> ty
leastPositiveResidue a n = let r = a `mod` n in if r < 0 then r + n else r

data Zn : (n : Nat) -> Type where
  MkZn : Int -> Zn n

Semigroup (Zn n) where
  (MkZn x) <+> (MkZn y) = let z = x + y; i = fromNat n in
    MkZn $ if z < i then z else z - i

Monoid (Zn n) where
  neutral = MkZn 0

Group (Zn n) where
  inverse (MkZn x) = MkZn (fromNat n - x)

Eq (Zn n) where
  (MkZn x) == (MkZn y) = x == y

DecEq (Zn n) where
  decEq x y =
      case x == y of
        True => Yes primitiveEq
        False => No primitiveNotEq
    where
      primitiveEq : x = y
      primitiveEq = really_believe_me (Refl {x})
      primitiveNotEq : x = y -> Void
      primitiveNotEq prf = believe_me {b = Void} ()

Show (Zn n) where
  show (MkZn a) = show (leastPositiveResidue a (fromNat n))

max_stars_repo_name: yurrriq/gis

max_issues_repo_name: yurrriq/gis

max_forks_repo_name: yurrriq/gis


text:
module ServiceAttributes
%default total

-- attrType should represent the type of any service metadata that needs to be
-- tracked, (e.g. costs, quality, dependencies, etc).  It should implement
-- the Num interface to make Service composition a simple matter of combining
-- attributes with (+) and (*) operations.
data Service : (Num attrType) => (attrs : attrType) -> (t : Type) -> Type where
     -- Construct a basic service
     MkService : (Num attrType) => (a : attrType) ->  (f : t) -> Service a t
     -- Prove that a sequence of services creates a valid service.
     Sequence : (Num attrType) =>
              {a1 : attrType} -> {a2 : attrType} ->
              (Service a1 (t1 -> ti)) ->
              (Service a2 (ti -> t2)) ->
              (Service (a1 + a2) (t1 ->  t2))
    -- There might be a reason to write a third constructor representing
    -- branches in service composition, but for now we'll put that aside.

-- These are just here to help me wrap my head
-- around composing long types.
data Test1 : Type
data Test2 : Type
data Test3 : Type
data Test4 : Type

smallFun : Test1 -> Test2

medFun : Test2 -> Test3 -> Test4

endFun : Test4 -> Test1

smallService : Service 1.0 (Test1 -> Test2)

medService : Service 2.0 (Test2 -> Test3 -> Test4)

endService : Service 2.0 (Test4 -> Test1)

composedService : Service 3.0 (Test1 -> Test3 -> Test4)
composedService = Sequence smallService medService

longService : Service 5.0 ()

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
||| Utilities not (yet) available from idris2-dom
module Rhone.JS.Util

import Data.IORef
import Data.MSF
import JS

--------------------------------------------------------------------------------
--          Time
--------------------------------------------------------------------------------

%foreign "javascript:lambda:(w) => BigInt(new Date().getTime())"
prim__time : PrimIO Integer

||| Get the current time in milliseconds since 1970/01/01.
export
currentTime : HasIO io => io Integer
currentTime = primIO prim__time

--------------------------------------------------------------------------------
--          Timers
--------------------------------------------------------------------------------

||| ID used to identify and cancel a running timer.
public export
data IntervalID : Type where [external]

%foreign "browser:lambda:(n,h,w)=>setInterval(() => h(w),n)"
prim__setInterval : Bits32 -> IO () -> PrimIO IntervalID

%foreign "browser:lambda:(i,w)=>clearInterval(i)"
prim__clearInterval : IntervalID -> PrimIO ()

||| Sets a timer to repeatedly carry out the given IO action
||| after the given number of milliseconds.
|||
||| Returns an ID, which can be used with `clearInterval` to
||| cancel the timer.
export
setInterval : HasIO io => Bits32 -> JSIO () -> io (IntervalID)
setInterval millis run = primIO $ prim__setInterval millis (runJS run)

||| Cancel a running timer with the given ID.
export
clearInterval : HasIO io => IntervalID -> io ()
clearInterval id = primIO $ prim__clearInterval id

--------------------------------------------------------------------------------
--          Animations
--------------------------------------------------------------------------------

%foreign """
         browser:lambda:(h,w)=>{
            let previousTimeStamp;
            let stop = 0;

            function step(timestamp) {
              if (previousTimeStamp === undefined)
                previousTimeStamp = timestamp;
              const dtime = timestamp - previousTimeStamp;
              previousTimeStamp = timestamp;
              stop = h(dtime)(w);
              if (stop === 0) {
                window.requestAnimationFrame(step);
              }
            }

            window.requestAnimationFrame(step);
         }
         """
prim__animate : (Bits32 -> IO Bits32) -> PrimIO ()

||| Alias for a time delta in milliseconds
public export
DTime : Type
DTime = Bits32

||| Use `window.requestAnimationFrame` to repeatedly
||| animate the given function.
|||
||| The function takes the time delta (in milliseconds) since
||| the previous animation step as input.
|||
||| Returns a cleanup action, which can be run to
||| stop the running animation.
export
animate : HasIO io => (DTime -> JSIO ()) -> io (IO ())
animate run = do
  ref <- newIORef (the Bits32 0)
  primIO $ prim__animate (\dt => runJS (run dt) >> readIORef ref)
  pure (writeIORef ref 1)

export
showFPS : Bits32 -> String
showFPS n = #"FPS: \#{show n}"#

||| Averages the frames per second (FPS) of an animation
||| firing an event with the value every `n` steps.
export
fps : (n : Nat) -> MSF m DTime (Event Bits32)
fps n = mealy acc (n,0)
  where acc : DTime -> (Nat,DTime) -> NP I [(Nat,DTime),Event Bits32]
        acc dt (0,tot)   = [(n,0),Ev $ (1000 * cast (S n)) `div` (tot + dt)]
        acc dt (S k,tot) = [(k, tot + dt), NoEv]


text:
module JS.VarArg

-- TODO: How to handle vararg functions
export
data VarArg : Type -> Type where [external]


text:
import Data.Vect

same_cons : {xs : List a} -> {ys : List a} ->
            xs = ys -> x :: xs = x :: ys
same_cons prf = cong prf

same_lists : {xs : List a} -> {ys : List a} ->
             x = y -> xs = ys -> x :: xs = y :: ys
same_lists  Refl Refl = Refl

data ThreeEq : a -> b -> c -> Type where
  Trans : (x:a) -> ThreeEq x x x

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS z z z (Trans z) = Trans (S z)

myReverse : Vect n elem -> Vect n elem
myReverse [] = []
myReverse (x :: xs) = reverseProof (myReverse xs ++ [x]) where
                      reverseProof : Vect (len + 1) elem -> Vect (S len) elem
                      reverseProof {len} result = rewrite plusCommutative 1 len in result

append_rhs_2 : Vect (S (m + len)) elem -> Vect (plus m (S len)) elem
append_rhs_2 {m} {len} xs = rewrite sym (plusSuccRightSucc m len) in xs

append : Vect n elem -> Vect m elem -> Vect (m + n) elem
append {m} [] ys = rewrite plusZeroRightNeutral m in ys
append (x :: xs) ys = append_rhs_2 (x :: append xs ys)

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = let result = plusZeroRightNeutral m in
                        sym result
myPlusCommutes (S k) m = let result = plusSuccRightSucc k m
                             symresult = sym result
                         in
                                     ?usCommutes_rhs_2

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module VDOM

import VDOM.VDOM

max_stars_repo_name: ebenpack/pamperscript

max_issues_repo_name: ebenpack/pamperscript

max_forks_repo_name: ebenpack/pamperscript


text:
module Data.Date

import Data.List1
import Data.String

%default total

public export
record Date where
  constructor MkDate
  year, month, day : Nat

export
Show Date where
  show (MkDate year month day) = "\{show year}-\{pad month}-\{pad day}"
    where
      pad : Nat -> String
      pad k = if k < 10
                 then "0\{show k}"
                 else show k

export
Eq Date where
  (MkDate year month day) == (MkDate year' month' day') =
    year == year' && month == month' && day == day'

export
Ord Date where
  compare (MkDate year month day) (MkDate year' month' day') =
    compare [year, month, day] [year', month', day']

parsePositiveReversed : List Char -> Maybe Nat
parsePositiveReversed [] = Just 0
parsePositiveReversed (x :: xs) = [ n + 10 * !(parsePositiveReversed xs) | n <- parseNat x ]
  where
    parseNat : Char -> Maybe Nat
    parseNat '0' = Just 0
    parseNat '1' = Just 1
    parseNat '2' = Just 2
    parseNat '3' = Just 3
    parseNat '4' = Just 4
    parseNat '5' = Just 5
    parseNat '6' = Just 6
    parseNat '7' = Just 7
    parseNat '8' = Just 8
    parseNat '9' = Just 9
    parseNat _   = Nothing

export
parseDateString : String -> Maybe Date
parseDateString = guardSuccess . foldl go (Start ** ()) . unpack
  where
    data PrimaryPart = Year | Month

    data Part = Start
              | ||| Primary Part
                P PrimaryPart
              | ||| Separator (dash) following given primary part.
                S PrimaryPart
              | Day
              | Fail

    Partial : Part -> Type
    Partial Start     = ()
    Partial (P Year)  = List Char             -- partial year
    Partial (S Year)  = Nat                   -- full year
    Partial (P Month) = (Nat, List Char)      -- partial month
    Partial (S Month) = (Nat, Nat)            -- full month
    Partial Day       = (Nat, Nat, List Char) -- partial day
    Partial Fail      = ()

    -- if we are on day, parse it as a number and construct a
    -- Date or fail.
    guardSuccess : (part ** Partial part) -> Maybe Date
    guardSuccess (Day ** (y, m, cs)) = MkDate y m <$> parsePositiveReversed cs
    guardSuccess _ = Nothing

    go : (part ** Partial part) -> Char -> (part ** Partial part)
    go (Fail ** ()) c = (Fail ** ())

    -- kick things off with a digit
    go (Start ** ()) c = if isDigit c then (P Year ** [c]) else (Fail ** ())

    -- collect until you find a dash, then reverse and parse as number
    go ((P Year) ** cs) '-' = case parsePositiveReversed cs of
                                Nothing  => (Fail ** ())
                                (Just y) => (S Year ** y)
    go ((P Year) ** cs) c = (P Year ** c :: cs)

    -- kick things off with a digit
    go ((S Year) ** snd) c = if isDigit c then (P Month ** (snd, [c])) else (Fail ** ())

    -- collect until you find a dash, then reverse and parse as number
    go ((P Month) ** (y, cs)) '-' = case parsePositiveReversed cs of
                                         Nothing  => (Fail ** ())
                                         (Just m) => (S Month ** (y, m))
    go ((P Month) ** (y, cs)) c = (P Month ** (y, c :: cs))

    -- kick things off with a digit
    go ((S Month) ** (y, m)) c = if isDigit c then (Day ** (y, m, [c])) else (Fail ** ())

    -- collect until you are done
    go (Day ** (y, m, cs)) c = (Day ** (y, m, c :: cs))

export
parseDateTimeString : String -> Maybe Date
parseDateTimeString = parseDateString . head . split (== 'T')

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
-- %logging 2
test : List a -> Nat -> Nat
test xs n
    = case xs of
           [] => Z
           (y :: ys) => case n of
                             Z => Z
                             (S k) => calculate xs k
  where
    calculate : List a -> Nat -> Nat
%logging 0


text:
module CoinToss

import Data.Vect
import QStateT
import QuantumOp
import LinearTypes

||| A fair coin toss (as an IO effect) via quantum resources.
|||
||| first create a new qubit in state |0>
||| then apply a hadamard gate to it, thereby preparing state |+>
||| and finally measure the qubit and return this as the result
export
coin : QuantumOp t => IO Bool
coin = do
  [b] <- run (do
           q <- newQubit {t = t}
           q <- applyH q
           r <- measure [q]
           pure r
         )
  pure b

testCoin : IO Bool
testCoin = coin {t = SimulatedOp}

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module IdrisUnit

import Control.App
import Control.App.Console

data TestError : Type where
    NotEq : Show x => x -> x -> TestError

Show TestError where
    show (NotEq a b) = show a ++ " != " ++ show b

||| ```
||| spec : Spec es => App es ()
||| spec = describe "example" $ do
|||     context "arith" $ do
|||         it "1+1 = 2" $ do
|||             1+1 `shouldBe` 2
|||         it "1*1 = 1" $ do
|||             1*1 `shouldBe` 1
||| ```
public export
interface Spec es where
  describe : String -> App es () -> App es ()
  context : String -> App es () -> App es ()
  it : String -> App (TestError :: es) () -> App es ()

export
Console es => Spec es where
  describe text toRun = do
    putStrLn text
    toRun
  context text toRun = do
    putStrLn text
    toRun
  it text toRun = handle toRun
    (\_ => do
        putStrLn $ "test: " ++ text ++ " passed")
    (\err => do
        putStrLn $ "test: " ++ text
        printError err)
    where
        printError : Console es' => TestError -> App es' ()
        printError err = putStrLn $ "failed: " ++ show err

||| ```
||| a `shouldBe` b
||| ```
export
shouldBe : HasErr TestError es => Has [Show, Eq] x => x -> x -> App es ()
a `shouldBe` b = do
    if a == b
        then pure ()
        else throw $ NotEq a b

max_stars_repo_name: dannypsnl/idris-unit

max_issues_repo_name: dannypsnl/idris-unit

max_forks_repo_name: dannypsnl/idris-unit


text:
import Data.Vect

insert : Ord elem => (x : elem) -> (sorted : Vect k elem) -> Vect (S k) elem
insert x [] = [x]
insert x (y :: xs) = case x < y of
                        False => y :: insert x xs
                        True => x :: y :: xs

ins_sort : Ord elem => Vect n elem -> Vect n elem
ins_sort [] = []
ins_sort (x :: xs) = let sorted = ins_sort xs in
                      insert x sorted

-- *vec_sort> ins_sort ['C', 'A', 'Z']
-- ['A', 'C', 'Z'] : Vect 3 Char
-- *vec_sort> ins_sort [3,2,9,7,6,5,8]
-- [2, 3, 5, 6, 7, 8, 9] : Vect 7 Integer


text:
module Language.LSP.Message.ServerCapabilities

import Data.SortedMap
import Language.JSON
import Language.LSP.Message.CallHierarchy
import Language.LSP.Message.Cancel
import Language.LSP.Message.CodeAction
import Language.LSP.Message.CodeLens
import Language.LSP.Message.Command
import Language.LSP.Message.Completion
import Language.LSP.Message.Declaration
import Language.LSP.Message.Definition
import Language.LSP.Message.Derive
import Language.LSP.Message.Diagnostics
import Language.LSP.Message.DocumentColor
import Language.LSP.Message.DocumentFormatting
import Language.LSP.Message.DocumentHighlight
import Language.LSP.Message.DocumentLink
import Language.LSP.Message.DocumentSymbols
import Language.LSP.Message.FoldingRange
import Language.LSP.Message.Hover
import Language.LSP.Message.Implementation
import Language.LSP.Message.LinkedEditingRange
import Language.LSP.Message.Location
import Language.LSP.Message.Markup
import Language.LSP.Message.Method
import Language.LSP.Message.Moniker
import Language.LSP.Message.Progress
import Language.LSP.Message.References
import Language.LSP.Message.Registration
import Language.LSP.Message.RegularExpressions
import Language.LSP.Message.Rename
import Language.LSP.Message.SelectionRange
import Language.LSP.Message.SemanticTokens
import Language.LSP.Message.SignatureHelp
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Trace
import Language.LSP.Message.Utils
import Language.LSP.Message.Window
import Language.LSP.Message.Workspace
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record FileOperationsServerCapabilities where
  constructor MkFileOperationsServerCapabilities
  didCreate  : Maybe FileOperationRegistrationOptions
  willCreate : Maybe FileOperationRegistrationOptions
  didRename  : Maybe FileOperationRegistrationOptions
  willRename : Maybe FileOperationRegistrationOptions
  didDelete  : Maybe FileOperationRegistrationOptions
  willDelete : Maybe FileOperationRegistrationOptions
%runElab deriveJSON defaultOpts `{{FileOperationsServerCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record WorkspaceServerCapabilities where
  constructor MkWorkspaceServerCapabilities
  workspaceFolders : Maybe WorkspaceFoldersServerCapabilities
  fileOperations   : Maybe FileOperationsServerCapabilities
%runElab deriveJSON defaultOpts `{{WorkspaceServerCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record ServerCapabilities where
  constructor MkServerCapabilities
  textDocumentSync                 : Maybe (OneOf [TextDocumentSyncOptions, TextDocumentSyncKind])
  completionProvider               : Maybe CompletionOptions
  hoverProvider                    : Maybe (OneOf [Bool, HoverOptions])
  signatureHelpProvider            : Maybe SignatureHelpOptions
  declarationProvider              : Maybe (OneOf [Bool, DefinitionOptions])
  typeDefinitionProvider           : Maybe (OneOf [Bool, TypeDefinitionOptions, TypeDefinitionRegistrationOptions])
  implementationProvider           : Maybe (OneOf [Bool, ImplementationOptions, ImplementationRegistrationOptions])
  referencesProvider               : Maybe (OneOf [Bool, ReferenceOptions])
  documentHighlightProvider        : Maybe (OneOf [Bool, DocumentHighlightOptions])
  documentSymbolProvider           : Maybe (OneOf [Bool, DocumentSymbolOptions])
  codeActionProvider               : Maybe (OneOf [Bool, CodeActionOptions])
  codeLensProvider                 : Maybe CodeLensOptions
  documentLinkProvider             : Maybe DocumentLinkOptions
  colorProvider                    : Maybe (OneOf [Bool, DocumentColorOptions, DocumentColorRegistrationOptions])
  documentFormattingProvider       : Maybe (OneOf [Bool, DocumentFormattingOptions])
  documentRangeFormattingProvider  : Maybe (OneOf [Bool, DocumentRangeFormattingOptions])
  documentOnTypeFormattingProvider : Maybe DocumentOnTypeFormattingOptions
  renameProvider                   : Maybe (OneOf [Bool, RenameOptions])
  foldingRangeProvider             : Maybe (OneOf [Bool, FoldingRangeOptions, FoldingRangeRegistrationOptions])
  executeCommandProvider           : Maybe ExecuteCommandOptions
  selectionRangeProvider           : Maybe (OneOf [Bool, SelectionRangeOptions, SelectionRangeRegistrationOptions])
  linkedEditingRangeProvider       : Maybe (OneOf [Bool, LinkedEditingRangeOptions, LinkedEditingRangeRegistrationOptions])
  callHierarchyProvider            : Maybe (OneOf [Bool, CallHierarchyOptions, CallHierarchyRegistrationOptions])
  semanticTokensProvider           : Maybe (OneOf [SemanticTokensOptions, SemanticTokensRegistrationOptions])
  monikerProvider                  : Maybe (OneOf [Bool, MonikerOptions, MonikerRegistrationOptions])
  workspaceSymbolProvider          : Maybe (OneOf [Bool, WorkspaceSymbolOptions])
  workspace                        : Maybe WorkspaceServerCapabilities
  experimental                     : Maybe JSON
%runElab deriveJSON defaultOpts `{{ServerCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#initialize
public export
record ServerInfo where
  constructor MkServerInfo
  name    : String
  version : Maybe String
%runElab deriveJSON defaultOpts `{{ServerInfo}}


text:
-- ---------------------------------------------------------------- [ Main.idr ]
-- Module    : Main.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Serialiser and Parser and Evaluator for GLANG, quick and dirty.
module GRL.Lang.GLang.Main

import System

import Effects
import Effect.System
import Effect.StdIO
import Effect.State
import Effect.Exception
import Effect.File

import Data.AVL.Dict

import Lightyear
import Lightyear.Char
import Lightyear.Strings
import Lightyear.StringFile

import GRL.Lang.GLang

import GRL.Lang.GLang.Pretty
import GRL.Lang.Common.Error
import GRL.Lang.Common.Parser
import GRL.Lang.Common.Effs
import GRL.Lang.Common.Utils

import GRL.Eval

GLangE : Type -> Type
GLangE ty = Lang (GLang ELEM) ty

-- ------------------------------------------------------------------- [ Types ]

nodeTy : Parser GElemTy
nodeTy = (keyword "Goal" *> return GOALty)
     <|> (keyword "Soft" *> return SOFTty)
     <|> (keyword "Task" *> return TASKty)
     <|> (keyword "Res"  *> return RESty)
     <?> "Node Type"

intentTy : Parser GIntentTy
intentTy = (keyword "==>" *> return IMPACTSty)
       <|> (keyword "~~>" *> return AFFECTSty)
       <?> "Intent Type"

structTy : Parser GStructTy
structTy = (keyword "&=" *> return ANDty)
       <|> (keyword "|=" *> return IORty)
       <|> (keyword "X=" *> return XORty)
       <?> "Struct Type"

-- --------------------------------------------------------- [ Data Structures ]

node : Parser (GLangAST ELEM)
node = do
    n <- ident
    keyword "<-"
    ty <- nodeTy
    t <- quoted '"'
    sval <- opt $ keyword "is" *> sValue
    gComment
    pure (MkNode n ty t sval)
  <?> "Node"

intent : Parser (GLangAST INTENT)
intent = do
    x <- ident
    ty <- intentTy
    y <- ident
    keyword "|"
    cval <- cValue
    gComment
    pure (MkIntent ty cval x y)
  <?> "Intent"

struct : Parser (GLangAST STRUCT)
struct = do
    x <- ident
    ty <- structTy
    ys <- brackets $ commaSep1 ident
    gComment
    pure (MkStruct ty x ys)
  <?> "Struct"

-- ------------------------------------------------------- [ Model description ]

glang : Parser (ts ** DList GTy GLangAST ts)
glang = do
    gComment
    keyword "grl"
    keyword "model"
    gComment
    ns <- some node
    ss <- many struct
    is <- many intent

    let ns' = DList.fromList ns
    let ss' = DList.fromList ss
    let is' = DList.fromList is

    pure (_ ** (snd ns')
            ++ (snd ss')
            ++ (snd is'))
  <?> "GRL Model"

-- ----------------------------------------------------------- [ Strategy File ]

gstrategy : Parser $ List (String, SValue)
gstrategy = do
      gComment
      keyword "grl"
      keyword "strategy"
      gComment
      ss <- some pairing
      pure ss
    <?> "Strategy"
  where
    pairing : Parser (String, SValue)
    pairing = do
        i <- ident
        keyword "="
        sval <- sValue
        gComment
        pure (i,sval)

-- --------------------------------------------------------- [ Effectful Stuff ]

buildElem : GElemTy -> String -> GLangE (GLang ELEM)
buildElem GOALty t = pure $ mkGoal t
buildElem SOFTty t = pure $ mkSoft t
buildElem TASKty t = pure $ mkTask t
buildElem RESty  t = pure $ mkRes  t

buildElemSat : GElemTy -> String -> SValue -> GLangE (GLang ELEM)
buildElemSat GOALty t s = pure $ mkSatGoal t s
buildElemSat SOFTty t s = pure $ mkSatSoft t s
buildElemSat TASKty t s = pure $ mkSatTask t s
buildElemSat RESty  t s = pure $ mkSatRes  t s

insertE : GLangAST ty -> GModel -> GLangE GModel
insertE (MkNode i ty t Nothing) m = do
    g <- buildElem ty t
    update (\env => insert i g env)
    pure (insert g m)

insertE (MkNode i ty t (Just sval)) m = do
    g <- buildElemSat ty t sval
    update (\env => insert i g env)
    pure (insert g m)

insertE (MkIntent ty cval x y) m = do
    x' <- getElem x
    y' <- getElem y
    case ty of
      IMPACTSty => pure $ insert (x' ==> y' | cval) m
      AFFECTSty => pure $ insert (x' ~~> y' | cval) m

insertE (MkStruct ty x ys) m = do
    x' <- getElem x
    ys' <- mapE (\y => getElem y) ys
    case ty of
      ANDty => pure $ insert (x' &= ys') m
      XORty => pure $ insert (x' X= ys') m
      IORty => pure $ insert (x' |= ys') m

buildModel : DList GTy GLangAST ds -> GModel -> GLangE GModel
buildModel Nil     m = pure m
buildModel (d::ds) m = buildModel ds !(insertE d m)

buildStrategyE : List (String, SValue) -> GLangE Strategy
buildStrategyE is = do
    is' <- mapE (\x => doConv x) is
    pure $ buildStrategy is'
  where
    doConv : (String,SValue) -> GLangE (GLang ELEM, SValue)
    doConv (i,sval) = pure (!(getElem i), sval)

doEvaluateE : GModel
         -> Maybe String
         -> GLangE EvalResult
doEvaluateE m Nothing       = evaluateE m Nothing
doEvaluateE m (Just sfname) = do
    strat <- readLangFile gstrategy sfname
    strat' <- buildStrategyE strat
    evaluateE m (Just strat')

-- ------------------------------------------------------------------ [ Pretty ]

covering
eMain : GLangE ()
eMain = do
    as <- getArgs
    (mfname, sfname) <- processArgs as
    (_ ** ast) <- readLangFile glang mfname
    m <- buildModel ast emptyModel
    res <- doEvaluateE m sfname
    showRes prettyResult res
    putStrLn $ toString m

main : IO ()
main = do
  run eMain
  exit 0

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module OfficialCrashCourse.DTypes

-- Data Types
public export
data NatNum = Hero | Succ NatNum  -- natural numbers are either Zero or Successor of another natural number

public export
data PolyList a = Nil | (::) a (PolyList a)  -- a is a type variable, a polymorphic list is either nil or is a value of type a 'cons'-ed to a polymorphic list of the same type

max_stars_repo_name: umbrela-academy/idrusti

max_issues_repo_name: umbrela-academy/idrusti

max_forks_repo_name: umbrela-academy/idrusti


text:
module Lib

import Data.List

%default total

export
accMapAux : (a -> b) -> List a -> List b -> List b
accMapAux f [] acc = reverse acc
accMapAux f (x :: xs) acc = accMapAux f xs (f x :: acc)

public export
accMap : (a -> b) -> List a -> List b
accMap f xs = accMapAux f xs []


text:
module Codegen

import public Control.Monad.State
import Data.List
import Data.String

import Debug.Trace

ConstDef : Type
ConstDef = (String, String)

export
data CGBuffer : Type where
  MkCGBuf : Int -> List ConstDef -> List String -> List String -> CGBuffer

public export
Codegen : Type -> Type
Codegen = State CGBuffer

emptyCG : CGBuffer
emptyCG = MkCGBuf 0 [] [] []

export
appendCode : String -> Codegen ()
appendCode c = modify $ \(MkCGBuf i consts l e) => (MkCGBuf i consts (c::l) e)

export
getUnique : Codegen Int
getUnique = do
  (MkCGBuf i c l e) <- get
  put (MkCGBuf (i+1) c l e)
  pure i

export
addConstant : Int -> String -> Codegen String
addConstant i v = do
  ci <- getUnique
  let name = "@glob_" ++ show i ++ "_c" ++ show ci
  (MkCGBuf i c l e) <- get
  put (MkCGBuf i ((name, v)::c) l e)
  pure name

export
addError : String -> Codegen ()
addError msg = do
  appendCode ("; ERROR: " ++ msg)
  (MkCGBuf i c l e) <- get
  put $ trace ("add error: " ++ msg) (MkCGBuf i c l (msg::e))

export
addMetadata : Int -> String -> Codegen String
addMetadata i v = do
  u <- getUnique
  let mdId = u * 0x10000 + i
  let name = "!" ++ show mdId
  (MkCGBuf i c l e) <- get
  put (MkCGBuf i ((name, v)::c) l e)
  pure name

export
runCodegen : Codegen () -> String
runCodegen r = let (MkCGBuf _ cs ls errors) = fst $ runState emptyCG r in
                    fastAppend $ intersperse "\n" $ (map (\(n,v) => n ++ " = " ++ v) $ reverse cs) ++ reverse ls

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
import Data.Nat
import System

import Tensor

test_can_construct_scalar : Tensor [] Double
test_can_construct_scalar = const 0.0

test_can_construct_vector : Tensor [3] Double
test_can_construct_vector = const [0.0, 1.0, -2.0]

test_can_construct_matrix : Tensor [2, 3] Double
test_can_construct_matrix = const [[0.0, -1.0, -2.0], [3.0, 4.0, 5.0]]

test_can_construct_int_matrix : Tensor [2, 3] Int
test_can_construct_int_matrix = const [[0, -1, -2], [3, 4, 5]]

test_T : Tensor [2, 3] Double -> Tensor [3, 2] Double
test_T x = x.T

test_T_with_leading : Tensor [2, 3, 5] Double -> Tensor [2, 5, 3] Double
test_T_with_leading x = x.T

test_dimbroadcastable : List (a ** b ** DimBroadcastable a b)
test_dimbroadcastable = [
    (0 ** 0 ** Same),
    (1 ** 1 ** Same),
    (3 ** 3 ** Same),
    (1 ** 0 ** Stack),
    (1 ** 1 ** Stack),
    (1 ** 3 ** Stack),
    (0 ** 0 ** Zero),
    (1 ** 0 ** Zero),
    (3 ** 0 ** Zero)
]

test_broadcastable : List (
    fr ** tr ** from : Shape {rank=fr} ** to : Shape {rank=tr} ** Broadcastable from to
)
test_broadcastable = [
    (_ ** _ ** [] ** [] ** Same),
    (_ ** _ ** [3, 2, 5] ** [3, 2, 5] ** Same),
    (_ ** _ ** [] ** [3, 2, 5] ** Nest $ Nest $ Nest Same),
    (_ ** _ ** [3, 1, 5] ** [3, 7, 5] ** Match $ Match Same),
    (_ ** _ ** [3, 2, 5] ** [1, 3, 2, 5] ** Nest Same),
    (_ ** _ ** [3, 2, 5] ** [7, 3, 2, 5] ** Nest Same)
]

test_broadcastable_cannot_reduce_rank0 : Broadcastable [5] [] -> Void
test_broadcastable_cannot_reduce_rank0 _ impossible

test_broadcastable_cannot_reduce_rank1 : Broadcastable [3, 2, 5] [] -> Void
test_broadcastable_cannot_reduce_rank1 _ impossible

test_broadcastable_cannot_stack_dimension_gt_one : Broadcastable [3, 2] [3, 7] -> Void
test_broadcastable_cannot_stack_dimension_gt_one (Match Same) impossible
test_broadcastable_cannot_stack_dimension_gt_one (Nest Same) impossible

test_squeezable_can_noop : Squeezable [3, 2, 5] [3, 2, 5]
test_squeezable_can_noop = Same

test_squeezable_can_remove_ones : Squeezable [1, 3, 1, 1, 2, 5, 1] [3, 2, 5]
test_squeezable_can_remove_ones = Nest (Match (Nest (Nest (Match (Match (Nest Same))))))

test_squeezable_can_flatten_only_ones : Squeezable [1, 1] []
test_squeezable_can_flatten_only_ones = Nest (Nest Same)

test_squeezable_cannot_remove_non_ones : Squeezable [1, 2] [] -> Void
test_squeezable_cannot_remove_non_ones (Nest _) impossible

test_tensor_contraction11 : Tensor [4] Double -> Tensor [4] Double -> Tensor [] Double
test_tensor_contraction11 x y = x @@ y

test_tensor_contraction12 : Tensor [4] Double -> Tensor [4, 5] Double -> Tensor [5] Double
test_tensor_contraction12 x y = x @@ y

test_tensor_contraction21 : Tensor [3, 4] Double -> Tensor [4] Double -> Tensor [3] Double
test_tensor_contraction21 x y = x @@ y

test_tensor_contraction22 : Tensor [3, 4] Double -> Tensor [4, 5] Double -> Tensor [3, 5] Double
test_tensor_contraction22 x y = x @@ y

test_det : Tensor [3, 3] Double -> Tensor [] Double
test_det x = det x

test_det_with_leading : Tensor [2, 3, 3] Double -> Tensor [2] Double
test_det_with_leading x = det x

assert : Bool -> IO ()
assert x = if x then pure () else do
    putStrLn "Test failed"
    exitFailure

test_const_eval : IO ()
test_const_eval = do
    let x = [[True, False, False], [False, True, False]]
    x' <- eval $ const {shape=[_, _]} {dtype=Bool} x
    assert $ x' == x

    let x =  [[1, 15, 5], [-1, 7, 6]]
    x' <- eval $ const {shape=[_, _]} {dtype=Int} x
    assert $ x' == x

    x <- eval $ const {shape=[_, _]} {dtype=Double} [[-1.5], [1.3], [4.3]]
    assert $ abs (index 0 (index 0 x) - (-1.5)) < 0.000001
    assert $ abs (index 0 (index 1 x) - 1.3) < 0.000001
    assert $ abs (index 0 (index 2 x) - 4.3) < 0.000001

    x <- eval $ const {shape=[]} True
    assert x

    x <- eval $ const {shape=[]} {dtype=Int} 3
    assert $ x == 3

    x <- eval $ const {shape=[]} {dtype=Double} 3.4
    assert $ abs (x - 3.4) < 0.000001

test_toString : IO ()
test_toString = do
    str <- toString $ const {shape=[]} {dtype=Int} 1
    assert $ str == "constant, shape=[], metadata={:0}"

    let x = const {shape=[]} {dtype=Int} 1
        y = const {shape=[]} {dtype=Int} 2
    str <- toString (x + y)
    assert $ str ==
        """
        add, shape=[], metadata={:0}
          constant, shape=[], metadata={:0}
          constant, shape=[], metadata={:0}
        """

    str <- toString $ const {shape=[_]} {dtype=Double} [1.3, 2.0, -0.4]
    assert $ str == "constant, shape=[3], metadata={:0}"

test_broadcast : IO ()
test_broadcast = do
    let x = const {shape=[]} {dtype=Int} 7
    broadcasted <- eval $ broadcast {to=[]} x
    assert $ broadcasted == 7

    let x = const {shape=[]} {dtype=Int} 7
    broadcasted <- eval $ broadcast {to=[1]} x
    assert $ broadcasted == [7]

    let x = const {shape=[]} {dtype=Int} 7
    broadcasted <- eval $ broadcast {to=[2, 3]} x
    assert $ broadcasted == [[7, 7, 7], [7, 7, 7]]

    let x = const {shape=[]} {dtype=Int} 7
    broadcasted <- eval $ broadcast {to=[1, 1, 1]} x
    assert $ broadcasted == [[[7]]]

    let x = const {shape=[1]} {dtype=Int} [7]
    broadcasted <- eval $ broadcast {to=[0]} x
    assert $ broadcasted == []

    let x = const {shape=[1]} {dtype=Int} [7]
    broadcasted <- eval $ broadcast {to=[1]} x
    assert $ broadcasted == [7]

    let x = const {shape=[1]} {dtype=Int} [7]
    broadcasted <- eval $ broadcast {to=[3]} x
    assert $ broadcasted == [7, 7, 7]

    let x = const {shape=[1]} {dtype=Int} [7]
    broadcasted <- eval $ broadcast {to=[2, 3]} x
    assert $ broadcasted == [[7, 7, 7], [7, 7, 7]]

    let x = const {shape=[2]} {dtype=Int} [5, 7]
    broadcasted <- eval $ broadcast {to=[2, 0]} x
    assert $ broadcasted == [[], []]

    let x = const {shape=[2]} {dtype=Int} [5, 7]
    broadcasted <- eval $ broadcast {to=[3, 2]} x
    assert $ broadcasted == [[5, 7], [5, 7], [5, 7]]

    let x = const {shape=[2, 3]} {dtype=Int} [[2, 3, 5], [7, 11, 13]]
    broadcasted <- eval $ broadcast {to=[2, 3]} x
    assert $ broadcasted == [[2, 3, 5], [7, 11, 13]]

    let x = const {shape=[2, 3]} {dtype=Int} [[2, 3, 5], [7, 11, 13]]
    broadcasted <- eval $ broadcast {to=[2, 0]} x
    assert $ broadcasted == [[], []]

    let x = const {shape=[2, 3]} {dtype=Int} [[2, 3, 5], [7, 11, 13]]
    broadcasted <- eval $ broadcast {to=[0, 3]} x
    assert $ broadcasted == []

    let x = const {shape=[2, 3]} {dtype=Int} [[2, 3, 5], [7, 11, 13]]
    broadcasted <- eval $ broadcast {to=[2, 2, 3]} x
    assert $ broadcasted == [[[2, 3, 5], [7, 11, 13]], [[2, 3, 5], [7, 11, 13]]]

    let x = const {shape=[2, 1, 3]} {dtype=Int} [[[2, 3, 5]], [[7, 11, 13]]]
    broadcasted <- eval $ broadcast {to=[2, 2, 5, 3]} x
    assert $ broadcasted == [
        [
            [[2, 3, 5], [2, 3, 5], [2, 3, 5], [2, 3, 5], [2, 3, 5]],
            [[7, 11, 13], [7, 11, 13], [7, 11, 13], [7, 11, 13], [7, 11, 13]]
        ],
        [
            [[2, 3, 5], [2, 3, 5], [2, 3, 5], [2, 3, 5], [2, 3, 5]],
            [[7, 11, 13], [7, 11, 13], [7, 11, 13], [7, 11, 13], [7, 11, 13]]
        ]
    ]

test_elementwise_equality : IO ()
test_elementwise_equality = do
    let x = const {shape=[]} {dtype=Bool} True
    eq <- eval (x ==# x)
    assert eq

    let x = const {shape=[]} {dtype=Bool} True
        y = const {shape=[]} {dtype=Bool} False
    eq <- eval (x ==# y)
    assert (not eq)

    let x = const {shape=[_]} {dtype=Bool} [True, True, False]
        y = const {shape=[_]} {dtype=Bool} [False, True, False]
    eq <- eval (y ==# x)
    assert $ eq == [False, True, True]

    let x = const {shape=[]} {dtype=Int} 0
    eq <- eval (x ==# x)
    assert eq

    let x = const {shape=[]} {dtype=Int} 0
        y = const {shape=[]} {dtype=Int} 1
    eq <- eval (x ==# y)
    assert (not eq)

    let x = const {shape=[]} {dtype=Int} 0
        y = const {shape=[]} {dtype=Int} 1
    eq <- eval (y ==# x)
    assert (not eq)

    let x = const {shape=[]} {dtype=Int} 2
        y = const {shape=[]} {dtype=Int} (-3)
    eq <- eval (x ==# y)
    assert (not eq)

    let x = const {shape=[]} {dtype=Int} 2
        y = const {shape=[]} {dtype=Int} (-3)
    eq <- eval (y ==# x)
    assert (not eq)

    let x = const {shape=[_, _]} {dtype=Int} [[1, 15, 5], [-1, 7, 6]]
        y = const {shape=[_, _]} {dtype=Int} [[2, 15, 3], [2, 7, 6]]
    eq <- eval (y ==# x)
    assert $ eq == [[False, True, False], [False, True, True]]

    let x = const {shape=[]} {dtype=Double} 0.1
    eq <- eval (x ==# x)
    assert eq

    let x = const {shape=[]} {dtype=Double} 0.1
        y = const {shape=[]} {dtype=Double} 1.1
    eq <- eval (x ==# y)
    assert (not eq)

    let x = const {shape=[_, _]} {dtype=Double} [[1.1, 15.3, 5.2], [-1.6, 7.1, 6.0]]
        y = const {shape=[_, _]} {dtype=Double} [[2.2, 15.3, 3.4], [2.6, 7.1, 6.0]]
    eq <- eval (y ==# x)
    assert $ eq == [[False, True, False], [False, True, True]]

test_elementwise_inequality : IO ()
test_elementwise_inequality = do
    let x = const {shape=[]} {dtype=Bool} True
    neq <- eval (x /=# x)
    assert (not neq)

    let x = const {shape=[]} {dtype=Bool} True
        y = const {shape=[]} {dtype=Bool} False
    neq <- eval (x /=# y)
    assert neq

    let x = const {shape=[_]} {dtype=Bool} [True, True, False]
        y = const {shape=[_]} {dtype=Bool} [False, True, False]
    neq <- eval (y /=# x)
    assert $ neq == [True, False, False]

    let x = const {shape=[]} {dtype=Int} 0
    neq <- eval (x /=# x)
    assert (not neq)

    let x = const {shape=[]} {dtype=Int} 0
        y = const {shape=[]} {dtype=Int} 1
    neq <- eval (x /=# y)
    assert neq

    let x = const {shape=[]} {dtype=Int} 0
        y = const {shape=[]} {dtype=Int} 1
    neq <- eval (y /=# x)
    assert neq

    let x = const {shape=[]} {dtype=Int} 2
        y = const {shape=[]} {dtype=Int} (-3)
    neq <- eval (x /=# y)
    assert neq

    let x = const {shape=[]} {dtype=Int} 2
        y = const {shape=[]} {dtype=Int} (-3)
    neq <- eval (y /=# x)
    assert neq

    let x = const {shape=[_, _]} {dtype=Int} [[1, 15, 5], [-1, 7, 6]]
        y = const {shape=[_, _]} {dtype=Int} [[2, 15, 3], [2, 7, 6]]
    neq <- eval (y /=# x)
    assert $ neq == [[True, False, True], [True, False, False]]

    let x = const {shape=[]} {dtype=Double} 0.1
    neq <- eval (x /=# x)
    assert (not neq)

    let x = const {shape=[]} {dtype=Double} 0.1
        y = const {shape=[]} {dtype=Double} 1.1
    neq <- eval (x /=# y)
    assert neq

    let x = const {shape=[_, _]} {dtype=Double} [[1.1, 15.3, 5.2], [-1.6, 7.1, 6.0]]
        y = const {shape=[_, _]} {dtype=Double} [[2.2, 15.3, 3.4], [2.6, 7.1, 6.0]]
    neq <- eval (y /=# x)
    assert $ neq == [[True, False, True], [True, False, False]]

compareScalar : (Primitive dtype, Ord dtype) => (dtype, dtype) -> IO ()
compareScalar (x, y) = do
    let x' = const {shape=[]} {dtype=dtype} x
        y' = const {shape=[]} {dtype=dtype} y
    gt <- eval (y' ># x')
    lt <- eval (y' <# x')
    ge <- eval (y' >=# x')
    le <- eval (y' <=# x')
    assert $ gt == (y > x)
    assert $ lt == (y < x)
    assert $ ge == (y >= x)
    assert $ le == (y <= x)

test_comparison : IO ()
test_comparison = do
    let cases : List Int := [-3, -1, 0, 1, 3]
    traverse_ compareScalar [(x, y) | x <- cases, y <- cases]

    let cases : List Double := [-3.3, -1.1, -0.1, 0.0, 0.1, 1.1, 3.3]
    traverse_ compareScalar [(x, y) | x <- cases, y <- cases]

    let x = const {shape=[_, _]} {dtype=Int} [[1, 2, 3], [-1, -2, -3]]
        y = const {shape=[_, _]} {dtype=Int} [[1, 4, 2], [-2, -1, -3]]
    gt <- eval (y ># x)
    lt <- eval (y <# x)
    ge <- eval (y >=# x)
    le <- eval (y <=# x)
    assert (gt == [[False, True, False], [False, True, False]])
    assert (lt == [[False, False, True], [True, False, False]])
    assert (ge == [[True, True, False], [False, True, True]])
    assert (le == [[True, False, True], [True, False, True]])

    let x = const {shape=[_, _]} {dtype=Double} [[1.1, 2.2, 3.3], [-1.1, -2.2, -3.3]]
        y = const {shape=[_, _]} {dtype=Double} [[1.1, 4.4, 2.2], [-2.2, -1.1, -3.3]]
    gt <- eval (y ># x)
    lt <- eval (y <# x)
    ge <- eval (y >=# x)
    le <- eval (y <=# x)
    assert (gt == [[False, True, False], [False, True, False]])
    assert (lt == [[False, False, True], [True, False, False]])
    assert (ge == [[True, True, False], [False, True, True]])
    assert (le == [[True, False, True], [True, False, True]])

test_add : IO ()
test_add = do
    let x = const {shape=[_, _]} {dtype=Int} [[1, 15, 5], [-1, 7, 6]]
        y = const {shape=[_, _]} {dtype=Int} [[11, 5, 7], [-3, -4, 0]]
    sum <- eval (x + y)
    assert $ sum == [[12, 20, 12], [-4, 3, 6]]

    let x = const {shape=[_, _]} {dtype=Double} [[1.8], [1.3], [4.0]]
        y = const {shape=[_, _]} {dtype=Double} [[-3.3], [0.0], [0.3]]
    sum <- eval (x + y)
    assert $ abs (index 0 (index 0 sum) - (-1.5)) < 0.000001
    assert $ abs (index 0 (index 1 sum) - 1.3) < 0.000001
    assert $ abs (index 0 (index 2 sum) - 4.3) < 0.000001

    let x = const {shape=[]} {dtype=Int} 3
        y = const {shape=[]} {dtype=Int} (-7)
    sum <- eval (x + y)
    assert $ sum == -4

    let x = const {shape=[]} {dtype=Double} 3.4
        y = const {shape=[]} {dtype=Double} (-7.1)
    sum <- eval (x + y)
    assert $ abs (sum - (-3.7)) < 0.000001

test_elementwise_multiplication : IO ()
test_elementwise_multiplication = do
    let x = const {shape=[_, _]} {dtype=Int} [[1, 15, 5], [-1, 7, 6]]
        y = const {shape=[_, _]} {dtype=Int} [[11, 5, 7], [-3, -4, 0]]
    product <- eval (x *# y)
    assert $ product == [[11, 75, 35], [3, -28, 0]]

    let x = const {shape=[_, _]} {dtype=Double} [[1.8], [1.3], [4.0]]
        y = const {shape=[_, _]} {dtype=Double} [[-3.3], [0.0], [0.3]]
    product <- eval (x *# y)
    assert $ abs (index 0 (index 0 product) - (-1.8 * 3.3)) < 0.000001
    assert $ abs (index 0 (index 1 product) - 0.0) < 0.000001
    assert $ abs (index 0 (index 2 product) - 1.2) < 0.000001

    let x = const {shape=[]} {dtype=Int} 3
        y = const {shape=[]} {dtype=Int} (-7)
    product <- eval (x *# y)
    assert $ product == -21

    let x = const {shape=[]} {dtype=Double} 3.4
        y = const {shape=[]} {dtype=Double} (-7.1)
    product <- eval (x *# y)
    assert $ abs (product - (-3.4 * 7.1)) < 0.000001

test_constant_multiplication : IO ()
test_constant_multiplication = do
    let x = const {shape=[]} {dtype=Int} 2
        y = const {shape=[_, _]} {dtype=Int} [[11, 5, 7], [-3, -4, 0]]
    product <- eval (x * y)
    assert $ product == [[22, 10, 14], [-6, -8, 0]]

    let x = const {shape=[]} {dtype=Double} 2.3
        y = const {shape=[_, _]} {dtype=Double} [[-3.3], [0.0], [0.3]]
    product <- eval (x * y)
    assert $ abs (index 0 (index 0 product) - (-2.3 * 3.3)) < 0.000001
    assert $ abs (index 0 (index 1 product) - 0.0) < 0.000001
    assert $ abs (index 0 (index 2 product) - 0.69) < 0.000001

    let x = const {shape=[]} {dtype=Int} 3
        y = const {shape=[]} {dtype=Int} (-7)
    product <- eval (x * y)
    assert $ product == -21

    let x = const {shape=[]} {dtype=Double} 3.4
        y = const {shape=[]} {dtype=Double} (-7.1)
    product <- eval (x * y)
    assert $ abs (product - (-3.4 * 7.1)) < 0.000001

main : IO ()
main = do
    test_const_eval
    test_toString
    test_broadcast
    test_elementwise_equality
    test_elementwise_inequality
    test_comparison
    test_add
    test_elementwise_multiplication
    test_constant_multiplication
    putStrLn "Tests passed"

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module Web.Internal.DomTypes

import JS

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace ShadowRootMode

  public export
  data ShadowRootMode = Open | Closed

  public export
  Show ShadowRootMode where
    show Open = "open"
    show Closed = "closed"

  public export
  Eq ShadowRootMode where
    (==) = (==) `on` show

  public export
  Ord ShadowRootMode where
    compare = compare `on` show

  public export
  read : String -> Maybe ShadowRootMode
  read "open" = Just Open
  read "closed" = Just Closed
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (ShadowRootMode.read s)}
             -> ShadowRootMode
  fromString s = fromJust $ read s

  export
  ToFFI ShadowRootMode String where
    toFFI = show

  export
  FromFFI ShadowRootMode String where
    fromFFI = read

--------------------------------------------------------------------------------
--          Interfaces
--------------------------------------------------------------------------------

export data AbortController : Type where [external]

export
ToFFI AbortController AbortController where toFFI = id

export
FromFFI AbortController AbortController where fromFFI = Just

export
SafeCast AbortController where
  safeCast = unsafeCastOnPrototypeName "AbortController"

export data AbortSignal : Type where [external]

export
ToFFI AbortSignal AbortSignal where toFFI = id

export
FromFFI AbortSignal AbortSignal where fromFFI = Just

export
SafeCast AbortSignal where
  safeCast = unsafeCastOnPrototypeName "AbortSignal"

export data AbstractRange : Type where [external]

export
ToFFI AbstractRange AbstractRange where toFFI = id

export
FromFFI AbstractRange AbstractRange where fromFFI = Just

export
SafeCast AbstractRange where
  safeCast = unsafeCastOnPrototypeName "AbstractRange"

export data Attr : Type where [external]

export
ToFFI Attr Attr where toFFI = id

export
FromFFI Attr Attr where fromFFI = Just

export
SafeCast Attr where
  safeCast = unsafeCastOnPrototypeName "Attr"

export data CDATASection : Type where [external]

export
ToFFI CDATASection CDATASection where toFFI = id

export
FromFFI CDATASection CDATASection where fromFFI = Just

export
SafeCast CDATASection where
  safeCast = unsafeCastOnPrototypeName "CDATASection"

export data CharacterData : Type where [external]

export
ToFFI CharacterData CharacterData where toFFI = id

export
FromFFI CharacterData CharacterData where fromFFI = Just

export
SafeCast CharacterData where
  safeCast = unsafeCastOnPrototypeName "CharacterData"

export data Comment : Type where [external]

export
ToFFI Comment Comment where toFFI = id

export
FromFFI Comment Comment where fromFFI = Just

export
SafeCast Comment where
  safeCast = unsafeCastOnPrototypeName "Comment"

export data CustomEvent : Type where [external]

export
ToFFI CustomEvent CustomEvent where toFFI = id

export
FromFFI CustomEvent CustomEvent where fromFFI = Just

export
SafeCast CustomEvent where
  safeCast = unsafeCastOnPrototypeName "CustomEvent"

export data DOMImplementation : Type where [external]

export
ToFFI DOMImplementation DOMImplementation where toFFI = id

export
FromFFI DOMImplementation DOMImplementation where fromFFI = Just

export
SafeCast DOMImplementation where
  safeCast = unsafeCastOnPrototypeName "DOMImplementation"

export data DOMTokenList : Type where [external]

export
ToFFI DOMTokenList DOMTokenList where toFFI = id

export
FromFFI DOMTokenList DOMTokenList where fromFFI = Just

export
SafeCast DOMTokenList where
  safeCast = unsafeCastOnPrototypeName "DOMTokenList"

export data Document : Type where [external]

export
ToFFI Document Document where toFFI = id

export
FromFFI Document Document where fromFFI = Just

export
SafeCast Document where
  safeCast = unsafeCastOnPrototypeName "Document"

export data DocumentFragment : Type where [external]

export
ToFFI DocumentFragment DocumentFragment where toFFI = id

export
FromFFI DocumentFragment DocumentFragment where fromFFI = Just

export
SafeCast DocumentFragment where
  safeCast = unsafeCastOnPrototypeName "DocumentFragment"

export data DocumentType : Type where [external]

export
ToFFI DocumentType DocumentType where toFFI = id

export
FromFFI DocumentType DocumentType where fromFFI = Just

export
SafeCast DocumentType where
  safeCast = unsafeCastOnPrototypeName "DocumentType"

export data Element : Type where [external]

export
ToFFI Element Element where toFFI = id

export
FromFFI Element Element where fromFFI = Just

export
SafeCast Element where
  safeCast = unsafeCastOnPrototypeName "Element"

export data Event : Type where [external]

export
ToFFI Event Event where toFFI = id

export
FromFFI Event Event where fromFFI = Just

export
SafeCast Event where
  safeCast = unsafeCastOnPrototypeName "Event"

export data EventTarget : Type where [external]

export
ToFFI EventTarget EventTarget where toFFI = id

export
FromFFI EventTarget EventTarget where fromFFI = Just

export
SafeCast EventTarget where
  safeCast = unsafeCastOnPrototypeName "EventTarget"

export data HTMLCollection : Type where [external]

export
ToFFI HTMLCollection HTMLCollection where toFFI = id

export
FromFFI HTMLCollection HTMLCollection where fromFFI = Just

export
SafeCast HTMLCollection where
  safeCast = unsafeCastOnPrototypeName "HTMLCollection"

export data MutationObserver : Type where [external]

export
ToFFI MutationObserver MutationObserver where toFFI = id

export
FromFFI MutationObserver MutationObserver where fromFFI = Just

export
SafeCast MutationObserver where
  safeCast = unsafeCastOnPrototypeName "MutationObserver"

export data MutationRecord : Type where [external]

export
ToFFI MutationRecord MutationRecord where toFFI = id

export
FromFFI MutationRecord MutationRecord where fromFFI = Just

export
SafeCast MutationRecord where
  safeCast = unsafeCastOnPrototypeName "MutationRecord"

export data NamedNodeMap : Type where [external]

export
ToFFI NamedNodeMap NamedNodeMap where toFFI = id

export
FromFFI NamedNodeMap NamedNodeMap where fromFFI = Just

export
SafeCast NamedNodeMap where
  safeCast = unsafeCastOnPrototypeName "NamedNodeMap"

export data Node : Type where [external]

export
ToFFI Node Node where toFFI = id

export
FromFFI Node Node where fromFFI = Just

export
SafeCast Node where
  safeCast = unsafeCastOnPrototypeName "Node"

export data NodeIterator : Type where [external]

export
ToFFI NodeIterator NodeIterator where toFFI = id

export
FromFFI NodeIterator NodeIterator where fromFFI = Just

export
SafeCast NodeIterator where
  safeCast = unsafeCastOnPrototypeName "NodeIterator"

export data NodeList : Type where [external]

export
ToFFI NodeList NodeList where toFFI = id

export
FromFFI NodeList NodeList where fromFFI = Just

export
SafeCast NodeList where
  safeCast = unsafeCastOnPrototypeName "NodeList"

export data Performance : Type where [external]

export
ToFFI Performance Performance where toFFI = id

export
FromFFI Performance Performance where fromFFI = Just

export
SafeCast Performance where
  safeCast = unsafeCastOnPrototypeName "Performance"

export data ProcessingInstruction : Type where [external]

export
ToFFI ProcessingInstruction ProcessingInstruction where toFFI = id

export
FromFFI ProcessingInstruction ProcessingInstruction where fromFFI = Just

export
SafeCast ProcessingInstruction where
  safeCast = unsafeCastOnPrototypeName "ProcessingInstruction"

export data Range : Type where [external]

export
ToFFI Range Range where toFFI = id

export
FromFFI Range Range where fromFFI = Just

export
SafeCast Range where
  safeCast = unsafeCastOnPrototypeName "Range"

export data ShadowRoot : Type where [external]

export
ToFFI ShadowRoot ShadowRoot where toFFI = id

export
FromFFI ShadowRoot ShadowRoot where fromFFI = Just

export
SafeCast ShadowRoot where
  safeCast = unsafeCastOnPrototypeName "ShadowRoot"

export data StaticRange : Type where [external]

export
ToFFI StaticRange StaticRange where toFFI = id

export
FromFFI StaticRange StaticRange where fromFFI = Just

export
SafeCast StaticRange where
  safeCast = unsafeCastOnPrototypeName "StaticRange"

export data Text : Type where [external]

export
ToFFI Text Text where toFFI = id

export
FromFFI Text Text where fromFFI = Just

export
SafeCast Text where
  safeCast = unsafeCastOnPrototypeName "Text"

export data TreeWalker : Type where [external]

export
ToFFI TreeWalker TreeWalker where toFFI = id

export
FromFFI TreeWalker TreeWalker where fromFFI = Just

export
SafeCast TreeWalker where
  safeCast = unsafeCastOnPrototypeName "TreeWalker"

export data XMLDocument : Type where [external]

export
ToFFI XMLDocument XMLDocument where toFFI = id

export
FromFFI XMLDocument XMLDocument where fromFFI = Just

export
SafeCast XMLDocument where
  safeCast = unsafeCastOnPrototypeName "XMLDocument"

export data XMLSerializer : Type where [external]

export
ToFFI XMLSerializer XMLSerializer where toFFI = id

export
FromFFI XMLSerializer XMLSerializer where fromFFI = Just

export
SafeCast XMLSerializer where
  safeCast = unsafeCastOnPrototypeName "XMLSerializer"

export data XPathEvaluator : Type where [external]

export
ToFFI XPathEvaluator XPathEvaluator where toFFI = id

export
FromFFI XPathEvaluator XPathEvaluator where fromFFI = Just

export
SafeCast XPathEvaluator where
  safeCast = unsafeCastOnPrototypeName "XPathEvaluator"

export data XPathExpression : Type where [external]

export
ToFFI XPathExpression XPathExpression where toFFI = id

export
FromFFI XPathExpression XPathExpression where fromFFI = Just

export
SafeCast XPathExpression where
  safeCast = unsafeCastOnPrototypeName "XPathExpression"

export data XPathResult : Type where [external]

export
ToFFI XPathResult XPathResult where toFFI = id

export
FromFFI XPathResult XPathResult where fromFFI = Just

export
SafeCast XPathResult where
  safeCast = unsafeCastOnPrototypeName "XPathResult"

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

export data AddEventListenerOptions : Type where [external]

export
ToFFI AddEventListenerOptions AddEventListenerOptions where toFFI = id

export
FromFFI AddEventListenerOptions AddEventListenerOptions where fromFFI = Just

export data CustomEventInit : Type where [external]

export
ToFFI CustomEventInit CustomEventInit where toFFI = id

export
FromFFI CustomEventInit CustomEventInit where fromFFI = Just

export data ElementCreationOptions : Type where [external]

export
ToFFI ElementCreationOptions ElementCreationOptions where toFFI = id

export
FromFFI ElementCreationOptions ElementCreationOptions where fromFFI = Just

export data EventInit : Type where [external]

export
ToFFI EventInit EventInit where toFFI = id

export
FromFFI EventInit EventInit where fromFFI = Just

export data EventListenerOptions : Type where [external]

export
ToFFI EventListenerOptions EventListenerOptions where toFFI = id

export
FromFFI EventListenerOptions EventListenerOptions where fromFFI = Just

export data GetRootNodeOptions : Type where [external]

export
ToFFI GetRootNodeOptions GetRootNodeOptions where toFFI = id

export
FromFFI GetRootNodeOptions GetRootNodeOptions where fromFFI = Just

export data MutationObserverInit : Type where [external]

export
ToFFI MutationObserverInit MutationObserverInit where toFFI = id

export
FromFFI MutationObserverInit MutationObserverInit where fromFFI = Just

export data ShadowRootInit : Type where [external]

export
ToFFI ShadowRootInit ShadowRootInit where toFFI = id

export
FromFFI ShadowRootInit ShadowRootInit where fromFFI = Just

export data StaticRangeInit : Type where [external]

export
ToFFI StaticRangeInit StaticRangeInit where toFFI = id

export
FromFFI StaticRangeInit StaticRangeInit where fromFFI = Just

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

export data ChildNode : Type where [external]

export
ToFFI ChildNode ChildNode where toFFI = id

export
FromFFI ChildNode ChildNode where fromFFI = Just

export data DocumentOrShadowRoot : Type where [external]

export
ToFFI DocumentOrShadowRoot DocumentOrShadowRoot where toFFI = id

export
FromFFI DocumentOrShadowRoot DocumentOrShadowRoot where fromFFI = Just

export data InnerHTML : Type where [external]

export
ToFFI InnerHTML InnerHTML where toFFI = id

export
FromFFI InnerHTML InnerHTML where fromFFI = Just

export data NonDocumentTypeChildNode : Type where [external]

export
ToFFI NonDocumentTypeChildNode NonDocumentTypeChildNode where toFFI = id

export
FromFFI NonDocumentTypeChildNode NonDocumentTypeChildNode where fromFFI = Just

export data NonElementParentNode : Type where [external]

export
ToFFI NonElementParentNode NonElementParentNode where toFFI = id

export
FromFFI NonElementParentNode NonElementParentNode where fromFFI = Just

export data ParentNode : Type where [external]

export
ToFFI ParentNode ParentNode where toFFI = id

export
FromFFI ParentNode ParentNode where fromFFI = Just

export data Slottable : Type where [external]

export
ToFFI Slottable Slottable where toFFI = id

export
FromFFI Slottable Slottable where fromFFI = Just

export data XPathEvaluatorBase : Type where [external]

export
ToFFI XPathEvaluatorBase XPathEvaluatorBase where toFFI = id

export
FromFFI XPathEvaluatorBase XPathEvaluatorBase where fromFFI = Just

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

export data EventListener : Type where [external]

export
ToFFI EventListener EventListener where toFFI = id

export
FromFFI EventListener EventListener where fromFFI = Just

export data MutationCallback : Type where [external]

export
ToFFI MutationCallback MutationCallback where toFFI = id

export
FromFFI MutationCallback MutationCallback where fromFFI = Just

export data NodeFilter : Type where [external]

export
ToFFI NodeFilter NodeFilter where toFFI = id

export
FromFFI NodeFilter NodeFilter where fromFFI = Just

export data XPathNSResolver : Type where [external]

export
ToFFI XPathNSResolver XPathNSResolver where toFFI = id

export
FromFFI XPathNSResolver XPathNSResolver where fromFFI = Just


text:
module Toolkit.Decidable.Equality.Views

import Decidable.Equality

import Toolkit.Decidable.Informative

%default total

public export
data AllEqual : (a,b,c : ty) -> Type where
  AE : AllEqual a a a

public export
data Error = AB | AC

abNotEq : (a = b -> Void) -> AllEqual a b c -> Void
abNotEq f AE = f Refl

acNotEq : (a = c -> Void) -> AllEqual a b c -> Void
acNotEq f AE = f Refl

export
allEqual : DecEq type
        => (a,b,c : type)
                 -> DecInfo (Error) (AllEqual a b c)
allEqual a b c with (decEq a b)
  allEqual a a c | (Yes Refl) with (decEq a c)
    allEqual a a a | (Yes Refl) | (Yes Refl) = Yes AE
    allEqual a a c | (Yes Refl) | (No contra)
      = No (AC) (acNotEq contra)
  allEqual a b c | (No contra)
    = No (AB) (abNotEq contra)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
> module SequentialDecisionProblems.applications.FreezeOrIncrease

> import Data.Fin
> import Control.Isomorphism

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Sigma.Sigma

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

* Freeze / Increase options:

> data FreezeOrIncrease = Freeze | Increase

* |FreezeOrIncrease| is finite and non-empty:

> to : FreezeOrIncrease -> Fin 2
> to Freeze   =    FZ
> to Increase = FS FZ

> from : Fin 2 -> FreezeOrIncrease
> from             FZ   = Freeze
> from         (FS FZ)  = Increase
> from     (FS (FS  k)) = absurd k

> toFrom : (k : Fin 2) -> to (from k) = k
> toFrom             FZ   = Refl
> toFrom         (FS FZ)  = Refl
> toFrom     (FS (FS  k)) = absurd k

> fromTo : (a : FreezeOrIncrease) -> from (to a) = a
> fromTo Freeze   = Refl
> fromTo Increase = Refl

> |||
> finiteFreezeOrIncrease : Finite FreezeOrIncrease
> finiteFreezeOrIncrease = MkSigma 2 (MkIso to from toFrom fromTo)

> |||
> cardNotZFreezeOrIncrease : CardNotZ finiteFreezeOrIncrease
> cardNotZFreezeOrIncrease = cardNotZLemma finiteFreezeOrIncrease Freeze

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
identity : ty -> ty
identity x = x


text:
module Circuits.Common.Parser

import public Data.Nat
import public Text.Parser

import public Toolkit.Data.Location
import public Toolkit.Text.Lexer.Run
import public Toolkit.Text.Parser.Support
import public Toolkit.Text.Parser.Location
import public Toolkit.Text.Parser.Run

import public Toolkit.Data.Whole

import Circuits.Common.Lexer

import Circuits.Common

%default total

namespace Circuits
  public export
  Rule : Type -> Type
  Rule = Rule Unit Token

  public export
  RuleEmpty : Type -> Type
  RuleEmpty = RuleEmpty Unit Token

  export
  eoi : RuleEmpty Unit
  eoi = eoi isEOI
    where
      isEOI : Token -> Bool
      isEOI EndInput = True
      isEOI _ = False

namespace API

  export
  symbol : String -> Rule Unit
  symbol str
    = terminal ("Expected Symbol '" ++ str ++ "'")
               (\x => case x of
                             Symbol s => if s == str then Just MkUnit
                                                     else Nothing
                             _ => Nothing)

  export
  nat : Rule Nat
  nat = terminal "Expected nat literal"
               (\x => case x of
                           LitNat i => Just i
                           _ => Nothing)

  export
  keyword : String -> Rule Builtin.Unit
  keyword str
    = terminal ("Expected Keyword '" ++ str ++ "'")
                 (\x => case x of
                             Keyword s => if s == str then Just Builtin.MkUnit
                                                      else Nothing
                             _ => Nothing)

  export
  identifier : Rule String
  identifier
    = terminal "Expected Identifier"
               (\x => case x of
                                  ID str => Just str
                                  _ => Nothing)

  export
  name : Rule String
  name = identifier

  export
  ref : Rule Ref
  ref =
    do s <- Toolkit.location
       n <- name
       e <- Toolkit.location
       pure (MkRef (newFC s e) n)

  export
  gives : String -> a -> Rule a
  gives s ctor
    = do keyword s
         pure ctor

  export
  inserts : Rule a -> (a -> b) -> Rule b
  inserts value ctor
    = do v <- value
         pure (ctor v)

  export
  whole : Rule Whole
  whole =
      do n <- nat
         isWhole n
    where
      isWhole : Nat -> RuleEmpty Whole
      isWhole Z = fail "expected whole"
      isWhole (S n) = pure (W (S n) ItIsSucc)

  export
  sFooter : Location -> Rule FileContext
  sFooter s
    = do symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (newFC s e)

namespace Types

  mutual
    logic : Rule DType
    logic = gives "logic" LOGIC

    array : Rule DType
    array
        = do ty <- logic
             ns <- indices
             pure (arraytype ty ns)
      where
        mustBeZero : Nat -> Whole -> RuleEmpty Whole
        mustBeZero    Z  (W w prf) = pure (W (S w) ItIsSucc)
        mustBeZero (S n)    w      = fail "No ranges or big endian supported"

        index : Rule Whole
        index
          = do symbol "["
               n <- whole
               symbol ":"
               a <- nat
               symbol "]"
               mustBeZero a n

        indices : Rule (List1 Whole)
        indices = some index

        arraytype : DType -> List1 Whole -> DType
        arraytype ty (x:::xs) = foldl (\ty, n => BVECT n ty) ty (x::xs)

    export
    type : Rule DType
    type = array <|> logic

-- [ 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:
-- examples in "Type-Driven Development with Idris"
-- chapter 13, section 1, Door part

-- check that all functions are total
%default total

data DoorState = DoorClosed | DoorOpen

data DoorCmd : Type ->
               DoorState ->
               DoorState ->
               Type where
  Open :     DoorCmd ()       DoorClosed DoorOpen
  Close :    DoorCmd ()       DoorOpen   DoorClosed
  RingBell : DoorCmd ()       DoorClosed DoorClosed
  Pure :     ty -> DoorCmd ty state      state
  (>>=) :    DoorCmd a        state1     state2 ->
             (a -> DoorCmd b  state2     state3) ->
             DoorCmd b        state1     state3

doorProg : DoorCmd () DoorClosed DoorClosed
doorProg = do RingBell
              Open
              Close

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
-- --------------------------------------------------- [ {{ Project }}.Lib.idr ]
-- Module      : {{ Project }}.Lib
-- Description : {{ description }}
-- --------------------------------------------------------------------- [ EOH ]
module {{ Project }}.Lib

%access export

max_stars_repo_name: vmchale/project-init

max_issues_repo_name: vmchale/project-init

max_forks_repo_name: vmchale/project-init