text:
import Prelude.Nat

-- Not in axiom list, but covered in class
-- (ab)^k = a^k * b^k
postulate powerDistributesRightMult : (a : Nat) -> (b : Nat) -> (k : Nat) -> power (a * b) k = (power a k) * (power b k)

-- a | b
Divides : (a : Nat) -> (b : Nat) -> Type
Divides a b = DPair Nat (\n => b = n * a)

-- a = b & x = y -> a + x = b + y
additionEquality : {a : Nat} -> {b : Nat} -> a = n -> b = m -> a + b = n + m
additionEquality pa pb =
  rewrite pa in
  rewrite pb in
  Refl

-- a | b & a | c -> a | (b + c)
theorem1_1 : {a : Nat} -> {b : Nat} -> {c : Nat} -> Divides a b -> Divides a c -> Divides a (b + c)
theorem1_1 {a} {b} {c} (bFactor ** bProof) (cFactor ** cProof) =
  let result = additionEquality bProof cProof in
  let proofOfDist = multDistributesOverPlusLeft bFactor cFactor a in
  ((bFactor + cFactor) ** (rewrite proofOfDist in result))

-- a | b & b | c -> a | c
theorem1_2 : {a : Nat} -> {b : Nat} -> {c : Nat} -> Divides a b -> Divides b c -> Divides a c
theorem1_2 {a} {b} {c} (bFactor ** bProof) (cFactor ** cProof) =
  rewrite cProof in
  rewrite bProof in
  ((cFactor * bFactor) ** multAssociative cFactor bFactor a)

-- a | b -> a^k | b^k
theorem1_4 : {a : Nat} -> {b : Nat} -> {k : Nat} -> Divides a b -> Divides (power a k) (power b k)
theorem1_4 {a} {k} (bFactor ** bProof) =
  rewrite bProof in
  ((power bFactor k) ** powerDistributesRightMult bFactor a k)


text:
module Choice

--- Axiom of choice in type theory

ext: idr


text:
data State : (stateType : Type) -> Type -> Type where
  Get : State stateType stateType
  Put : stateType -> State stateType ()
  Pure : ty -> State stateType ty
  Bind : State stateType a -> (a -> State stateType b) -> State stateType b

get : State stateType stateType
get = Get

put : stateType -> State stateType ()
put = Put

pure : ty -> State stateType ty
pure = Pure

(>>=) : State stateType a -> (a -> State stateType b) -> State stateType b
(>>=) = Bind

runState : State stateType a -> (st: stateType) -> (a, stateType)
runState Get             st = (st, st)
runState (Put newState)  _  = ((), newState)
runState (Pure x)        st = (x, st)
runState (Bind cmd prog) st =
  let
    (val, nextState) = runState cmd st
  in
    runState (prog val) nextState

implementation Functor (State stateType) where
  map func stA = Bind stA (\valA => Pure (func valA))

implementation Applicative (State stateType) where
  pure  x   = Pure x
  (<*>) x y = Bind x (\func => map func y)

implementation Monad (State stateType) where
  (>>=) = Bind

addIfPositive : Integer -> State Integer Bool
addIfPositive x =
  let
    isPositive = x > 0
  in
    do when isPositive (
        do current <- get
           put (current + x)
       )
       pure isPositive

addPositives : List Integer -> State Integer Nat
addPositives xs = do added <- traverse addIfPositive xs
                     pure (length (filter id added))

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

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty) "Fred" (Node Empty "Sheila" Empty)) "Alice" (Node Empty "Bob" (Node Empty "Eve" Empty))

labelTreeWith2 : Tree a -> State (Stream label) (Tree (label, a))
labelTreeWith2 Empty                  = pure Empty
labelTreeWith2 (Node left elem right) =
  do
    lbldLeft <- labelTreeWith2 left
    (this :: rest) <- get
    put rest
    lbldRight <- labelTreeWith2 right
    pure (Node lbldLeft (this, elem) lbldRight)

flatten : Tree a -> List a
flatten Empty = []
flatten (Node left val right) = flatten left ++ (val :: flatten right)

deepFirst : Tree elem -> Tree (Int, elem)
deepFirst tree = fst (runState (labelTreeWith2 tree) [1..])

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Mb

import public Language.Reflection.Pretty
import public Language.Reflection.Syntax
import public Language.Reflection.Types
import Data.Vect

%language ElabReflection

export
maybeInfo : TypeInfo
maybeInfo = getInfo "Maybe"

data T : Type -> Type where
  TU : T Unit
  TI : T Int
  Ta : T a

tParamInfo : ParamTypeInfo
--tParamInfo = getParamInfo "T"

data P : Nat -> Type where
  PZ : P Z
  PS : (x : Nat) -> P (S x)
  P3 : (y : Nat) -> P (S y)

data Q : Nat -> Type where
  QZ : Q Z
  QS : (x : Nat) -> Q (S x)
  Q3 : (xs : List Nat) -> Q (S $ length xs)

data R : Nat -> Type where
  RZ  : R Z
  RS  : (x : Nat) -> R (S x)
  RSS : (y : Nat) -> R (S (S y))

pParamInfo : ParamTypeInfo
--pParamInfo = getParamInfo "P"

qParamInfo : ParamTypeInfo
--qParamInfo = getParamInfo "Q"

rParamInfo : ParamTypeInfo
--rParamInfo = getParamInfo "R"

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module fn_to_vect

import Data.Vect
import Data.Fin

%access public export
%default total
-- module to convert a function to a vectot and a vector to a
-- function

||| Converts a vector to the corresponding function
vect_to_fn : (n : Nat) -> (ty : Type)-> (Vect n ty) ->
             (k : Fin n) -> ty
vect_to_fn n ty v k = index k v

||| Converts a function to the reversed vector
fn_to_vect : (n : Nat) -> (ty : Type) -> ((k : Fin n) -> ty) ->
             (Vect n ty)
fn_to_vect Z ty fn = []
fn_to_vect (S k) ty fn = (fn FZ) ::
      (fn_to_vect k ty smaller) where
          smaller : ((l : Fin k) -> ty)
          smaller l = fn (FS l)
--
-- ||| Converts a function to the corresponding vector
-- fn_to_vect : (n : Nat) -> (ty : Type) -> ((k : Fin n) -> ty) ->
--              (Vect n ty)
-- fn_to_vect n ty fn = fn_to_vect_rev n ty fn
--   -- reverse (fn_to_vect_rev n ty fn)

||| Definition of Matrices using vectors
Mat_Vect : (n : Nat) -> (m : Nat) -> (ty : Type) -> Type
Mat_Vect n m ty = Vect n (Vect m ty)

||| Definition of Matrices using functions
Mat_fn : (n : Nat) -> (m : Nat) -> (ty : Type) -> Type
Mat_fn n m ty = (i : Fin n) -> (j : Fin m) -> ty

||| From a matrix to its corresponding function
Mat_Vect_to_fn : (n : Nat) -> (m : Nat) -> (ty : Type) ->
                 (Mat_Vect n m ty) -> (Mat_fn n m ty)

Mat_Vect_to_fn n m ty vec i j = index j (index i vec)

||| From a function to the corresponding vector
Mat_fn_to_Vect : (n : Nat) -> (m : Nat) -> (ty : Type) ->
                     (Mat_fn n m ty) -> (Mat_Vect n m ty)

Mat_fn_to_Vect Z m ty fn = []
Mat_fn_to_Vect (S n) m ty fn = (v_top :: v_down) where
  fn_top : ( Fin m ) -> ty
  fn_top j = fn FZ j
  v_top : Vect m ty
  v_top = fn_to_vect m ty fn_top
  fn_down : Mat_fn n m ty
  fn_down i j = fn (FS i) j
  v_down : Mat_Vect n m ty
  v_down = Mat_fn_to_Vect n m ty fn_down

Diag_Mat_fn : (n : Nat) -> (ty : Type) ->
              (zero : ty) -> (elem : ty) ->
              (Mat_fn n n ty)
Diag_Mat_fn n ty zero elem i j = case (decEq i j) of
      Yes prf => elem
      No cont => zero

Diag_Mat_Vect : (n : Nat) -> (ty : Type) ->
                (zero : ty) -> (elem : ty) ->
                (Mat_Vect n n ty)
Diag_Mat_Vect n ty zero elem =
      Mat_fn_to_Vect n n ty (Diag_Mat_fn n ty zero elem)

Id_Mat_Nat : (n : Nat) -> Mat_Vect n n Nat
Id_Mat_Nat n = Diag_Mat_Vect n Nat Z (S Z)


text:
%default total

partial
foo : Nat -> Nat
foo Z = Z

partial
bar : Nat -> Nat
bar n with (0)
 bar n | k = foo n


text:
-- check peek doesn't remove things

import System.Concurrency.Queue

main : IO ()
main = do q <- makeQueue {a=Nat}
          let val = 3
          enqueue q val
          (Just theVal) <- peek q
            | Nothing => putStrLn "ERROR: Value disappeared from queue."
          (Just theVal') <- peek q
            | Nothing => putStrLn "ERROR: Peek removed the item."
          if (val == theVal) && (val == theVal')
             then putStrLn "Success!"
             else putStrLn "ERROR: Value changed between calls to peek."


text:
module Mmhelloworld.IdrisSpringBoot.Boot.Autoconfigure

import IdrisJvm.IO

%access public export

term syntax "<@SpringBootApplication>" [attrs] = <@> "org/springframework/boot/autoconfigure/SpringBootApplication" attrs

max_stars_repo_name: mmhelloworld/idris-spring-boot

max_issues_repo_name: mmhelloworld/idris-spring-boot

max_forks_repo_name: mmhelloworld/idris-spring-boot


text:
module Idris.Elab.Interface

import Core.Binary
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Name
import Core.Env
import Core.Metadata
import Core.TT
import Core.Unify
import Core.Value

import Idris.Resugar
import Idris.Syntax

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

import Libraries.Data.ANameMap
import Libraries.Data.List.Extra
import Data.List
import Data.Maybe

%default covering

------------------------------------------------------------------------
-- Signature

record Signature where
  constructor MkSignature
  location : FC
  count    : RigCount
  flags    : List FnOpt
  name     : Name
  nameLoc  : FC
  isData   : Bool
  type     : RawImp

-- Give implicit Pi bindings explicit names, if they don't have one already,
-- because we need them to be consistent everywhere we refer to them
namePis : Int -> RawImp -> RawImp
namePis i (IPi fc r AutoImplicit Nothing ty sc)
    = IPi fc r AutoImplicit (Just (MN "i_con" i)) ty (namePis (i + 1) sc)
namePis i (IPi fc r Implicit Nothing ty sc)
    = IPi fc r Implicit (Just (MN "i_imp" i)) ty (namePis (i + 1) sc)
namePis i (IPi fc r p n ty sc)
    = IPi fc r p n ty (namePis i sc)
namePis i (IBindHere fc m ty) = IBindHere fc m (namePis i ty)
namePis i ty = ty

getSig : ImpDecl -> Maybe Signature
getSig (IClaim _ c _ opts (MkImpTy fc nameFC n ty))
    = Just $ MkSignature { location = fc
                         , count    = c
                         , flags    = opts
                         , name     = n
                         , nameLoc  = nameFC
                         , isData   = False
                         , type     = namePis 0 ty
                         }
getSig (IData _ _ (MkImpLater fc n ty))
    = Just $ MkSignature { location = fc
                         , count    = erased
                         , flags    = [Invertible]
                         , name     = n
                         , nameLoc  = emptyFC
                         , isData   = True
                         , type     = namePis 0 ty
                         }
getSig _ = Nothing

------------------------------------------------------------------------
-- Declaration

record Declaration where
  constructor MkDeclaration
  name   : Name
  count  : RigCount
  flags  : List FnOpt
  isData : Bool
  type   : RawImp

sigToDecl : Signature -> Declaration
sigToDecl sig = MkDeclaration
  { name = sig.name
  , count = sig.count
  , flags = sig.flags
  , isData = sig.isData
  , type = sig.type
  }

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

-- TODO: Check all the parts of the body are legal
-- TODO: Deal with default superclass implementations

mkDataTy : FC -> List (Name, (RigCount, RawImp)) -> RawImp
mkDataTy fc [] = IType fc
mkDataTy fc ((n, (_, ty)) :: ps)
    = IPi fc top Explicit (Just n) ty (mkDataTy fc ps)

mkIfaceData : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              FC -> Visibility -> Env Term vars ->
              List (Maybe Name, RigCount, RawImp) ->
              Name -> Name -> List (Name, (RigCount, RawImp)) ->
              List Name -> List (Name, RigCount, RawImp) -> Core ImpDecl
mkIfaceData {vars} ifc vis env constraints n conName ps dets meths
    = let opts = if isNil dets
                    then [NoHints, UniqueSearch]
                    else [NoHints, UniqueSearch, SearchBy dets]
          pNames = map fst ps
          retty = apply (IVar vfc n) (map (IVar EmptyFC) pNames)
          conty = mkTy Implicit (map jname ps) $
                  mkTy AutoImplicit (map bhere constraints) (mkTy Explicit (map bname meths) retty)
          con = MkImpTy EmptyFC EmptyFC conName !(bindTypeNames ifc [] (pNames ++ map fst meths ++ vars) conty) in
          pure $ IData vfc vis (MkImpData vfc n
                                  !(bindTypeNames ifc [] (pNames ++ map fst meths ++ vars)
                                                  (mkDataTy vfc ps))
                                  opts [con])
  where

    vfc : FC
    vfc = virtualiseFC ifc

    jname : (Name, (RigCount, RawImp)) -> (Maybe Name, RigCount, RawImp)
    jname (n, rig, t) = (Just n, rig, t)

    bname : (Name, RigCount, RawImp) -> (Maybe Name, RigCount, RawImp)
    bname (n, c, t) = (Just n, c, IBindHere (getFC t) (PI erased) t)

    bhere : (Maybe Name, RigCount, RawImp) -> (Maybe Name, RigCount, RawImp)
    bhere (n, c, t) = (n, c, IBindHere (getFC t) (PI erased) t)

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

-- Get the implicit arguments for a method declaration or constraint hint
-- to allow us to build the data declaration
getMethDecl : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              Env Term vars -> NestedNames vars ->
              (params : List (Name, (RigCount, RawImp))) ->
              (mnames : List Name) ->
              (RigCount, nm, RawImp) ->
              Core (nm, RigCount, RawImp)
getMethDecl {vars} env nest params mnames (c, nm, ty)
    = do let paramNames = map fst params
         ty_imp <- bindTypeNames EmptyFC [] (paramNames ++ mnames ++ vars) ty
         pure (nm, c, stripParams paramNames ty_imp)
  where
    -- We don't want the parameters to explicitly appear in the method
    -- type in the record for the interface (they are parameters of the
    -- interface type), so remove it here
    stripParams : List Name -> RawImp -> RawImp
    stripParams ps (IPi fc r p mn arg ret)
        = if (maybe False (\n => n `elem` ps) mn)
             then stripParams ps ret
             else IPi fc r p mn arg (stripParams ps ret)
    stripParams ps ty = ty

-- bind the auto implicit for the interface - put it first, as it may be needed
-- in other method variables, including implicit variables
bindIFace : FC -> RawImp -> RawImp -> RawImp
bindIFace fc ity sc = IPi fc top AutoImplicit (Just (UN $ Basic "__con")) ity sc

-- Get the top level function for implementing a method
getMethToplevel : {vars : _} ->
                  {auto c : Ref Ctxt Defs} ->
                  Env Term vars -> Visibility ->
                  Name -> Name ->
                  (constraints : List (Maybe Name)) ->
                  (allmeths : List Name) ->
                  (params : List (Name, (RigCount, RawImp))) ->
                  Signature ->
                  Core (List ImpDecl)
getMethToplevel {vars} env vis iname cname constraints allmeths params sig
    = do let paramNames = map fst params
         let ity = apply (IVar vfc iname) (map (IVar EmptyFC) paramNames)
         -- Make the constraint application explicit for any method names
         -- which appear in other method types
         let ty_constr =
             substNames vars (map applyCon allmeths) sig.type
         ty_imp <- bindTypeNames EmptyFC [] vars (bindPs params $ bindIFace vfc ity ty_constr)
         cn <- inCurrentNS sig.name
         let tydecl = IClaim vfc sig.count vis (if sig.isData then [Inline, Invertible]
                                            else [Inline])
                                      (MkImpTy vfc sig.nameLoc cn ty_imp)
         let conapp = apply (IVar vfc cname)
                            (map (IBindVar EmptyFC) (map bindName allmeths))
         let argns = getExplicitArgs 0 sig.type
         -- eta expand the RHS so that we put implicits in the right place
         let fnclause = PatClause vfc (INamedApp vfc (IVar sig.location cn)
                                                   (UN $ Basic "__con")
                                                   conapp)
                                  (mkLam argns
                                    (apply (IVar EmptyFC (methName sig.name))
                                           (map (IVar EmptyFC) argns)))
         let fndef = IDef vfc cn [fnclause]
         pure [tydecl, fndef]
  where
    vfc : FC
    vfc = virtualiseFC sig.location

    -- Bind the type parameters given explicitly - there might be information
    -- in there that we can't infer after all
    bindPs : List (Name, (RigCount, RawImp)) -> RawImp -> RawImp
    bindPs [] ty = ty
    bindPs ((n, rig, pty) :: ps) ty
        = IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)

    applyCon : Name -> (Name, RawImp)
    applyCon n = let name = UN (Basic "__con") in
                 (n, INamedApp vfc (IVar vfc n) name (IVar vfc name))

    getExplicitArgs : Int -> RawImp -> List Name
    getExplicitArgs i (IPi _ _ Explicit n _ sc)
        = MN "arg" i :: getExplicitArgs (i + 1) sc
    getExplicitArgs i (IPi _ _ _ n _ sc) = getExplicitArgs i sc
    getExplicitArgs i tm = []

    mkLam : List Name -> RawImp -> RawImp
    mkLam [] tm = tm
    mkLam (x :: xs) tm
       = ILam EmptyFC top Explicit (Just x) (Implicit vfc False) (mkLam xs tm)

    bindName : Name -> String
    bindName (UN n) = "__bind_" ++ displayUserName n
    bindName (NS _ n) = bindName n
    bindName n = show n

    methName : Name -> Name
    methName n = UN (Basic $ bindName n)

-- Get the function for chasing a constraint. This is one of the
-- arguments to the record, appearing before the method arguments.
getConstraintHint : {vars : _} ->
                    {auto c : Ref Ctxt Defs} ->
                    FC -> Env Term vars -> Visibility ->
                    Name -> Name ->
                    (constraints : List Name) ->
                    (allmeths : List Name) ->
                    (params : List Name) ->
                    (Name, RawImp) -> Core (Name, List ImpDecl)
getConstraintHint {vars} fc env vis iname cname constraints meths params (cn, con)
    = do let ity = apply (IVar fc iname) (map (IVar fc) params)
         let fty = IPi fc top Explicit Nothing ity con
         ty_imp <- bindTypeNames fc [] (meths ++ vars) fty
         let hintname = DN ("Constraint " ++ show con)
                          (UN (Basic $ "__" ++ show iname ++ "_" ++ show con))

         let tydecl = IClaim fc top vis [Inline, Hint False]
                          (MkImpTy EmptyFC EmptyFC hintname ty_imp)

         let conapp = apply (impsBind (IVar fc cname) (map bindName constraints))
                              (map (const (Implicit fc True)) meths)

         let fnclause = PatClause fc (IApp fc (IVar fc hintname) conapp)
                                  (IVar fc (constName cn))
         let fndef = IDef fc hintname [fnclause]
         pure (hintname, [tydecl, fndef])
  where
    bindName : Name -> String
    bindName (UN n) = "__bind_" ++ displayUserName n
    bindName (NS _ n) = bindName n
    bindName n = show n

    constName : Name -> Name
    constName n = UN (Basic $ bindName n)

    impsBind : RawImp -> List String -> RawImp
    impsBind fn [] = fn
    impsBind fn (n :: ns)
        = impsBind (IAutoApp fc fn (IBindVar fc n)) ns

getDefault : ImpDecl -> Maybe (FC, List FnOpt, Name, List ImpClause)
getDefault (IDef fc n cs) = Just (fc, [], n, cs)
getDefault _ = Nothing

mkCon : FC -> Name -> Name
mkCon loc (NS ns (UN n))
   = let str = displayUserName n in
     NS ns (DN (str ++ " at " ++ show loc) (UN $ Basic ("__mk" ++ str)))
mkCon loc n
   = let str = show n in
     DN (str ++ " at " ++ show loc) (UN $ Basic ("__mk" ++  str))

updateIfaceSyn : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 Name -> Name -> List Name -> List Name -> List RawImp ->
                 List Declaration -> List (Name, List ImpClause) ->
                 Core ()
updateIfaceSyn iname cn impps ps cs ms ds
    = do syn <- get Syn
         ms' <- traverse totMeth ms
         let info = MkIFaceInfo cn impps ps cs ms' ds
         put Syn (record { ifaces $= addName iname info,
                           saveIFaces $= (iname :: ) } syn)
 where
    findSetTotal : List FnOpt -> Maybe TotalReq
    findSetTotal [] = Nothing
    findSetTotal (Totality t :: _) = Just t
    findSetTotal (_ :: xs) = findSetTotal xs

    totMeth : Declaration -> Core Method
    totMeth decl
        = do let treq = findSetTotal decl.flags
             pure $ MkMethod { name = decl.name
                             , count = decl.count
                             , totalReq = treq
                             , type = decl.type
                             }

-- Read the implicitly added parameters from an interface type, so that we
-- know to substitute an implicit in when defining the implementation
getImplParams : Term vars -> List Name
getImplParams (Bind _ n (Pi _ _ Implicit _) sc)
    = n :: getImplParams sc
getImplParams _ = []

export
elabInterface : {vars : _} ->
                {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                {auto s : Ref Syn SyntaxInfo} ->
                {auto m : Ref MD Metadata} ->
                FC -> Visibility ->
                Env Term vars -> NestedNames vars ->
                (constraints : List (Maybe Name, RawImp)) ->
                Name ->
                (params : List (Name, (RigCount, RawImp))) ->
                (dets : List Name) ->
                (conName : Maybe Name) ->
                List ImpDecl ->
                Core ()
elabInterface {vars} ifc vis env nest constraints iname params dets mcon body
    = do fullIName <- getFullName iname
         ns_iname <- inCurrentNS fullIName
         let conName_in = maybe (mkCon vfc fullIName) id mcon
         -- Machine generated names need to be qualified when looking them up
         conName <- inCurrentNS conName_in
         let meth_sigs = mapMaybe getSig body
         let meth_decls = map sigToDecl meth_sigs
         let meth_names = map name meth_decls
         let defaults = mapMaybe getDefault body

         elabAsData conName meth_names meth_sigs
         elabConstraintHints conName meth_names
         elabMethods conName meth_names meth_sigs
         ds <- traverse (elabDefault meth_decls) defaults

         ns_meths <- traverse (\mt => do n <- inCurrentNS mt.name
                                         pure (record { name = n } mt)) meth_decls
         defs <- get Ctxt
         Just ty <- lookupTyExact ns_iname (gamma defs)
              | Nothing => undefinedName ifc iname
         let implParams = getImplParams ty

         updateIfaceSyn ns_iname conName
                        implParams paramNames (map snd constraints)
                        ns_meths ds
  where
    vfc : FC
    vfc = virtualiseFC ifc

    paramNames : List Name
    paramNames = map fst params

    nameCons : Int -> List (Maybe Name, RawImp) -> List (Name, RawImp)
    nameCons i [] = []
    nameCons i ((_, ty) :: rest)
        = (UN (Basic $ "__con" ++ show i), ty) :: nameCons (i + 1) rest

    -- Elaborate the data declaration part of the interface
    elabAsData : (conName : Name) -> List Name ->
                 List Signature ->
                 Core ()
    elabAsData conName meth_names meth_sigs
        = do -- set up the implicit arguments correctly in the method
             -- signatures and constraint hints
             meths <- traverse (\ meth => getMethDecl env nest params meth_names
                                          (meth.count, meth.name, meth.type))
                                meth_sigs
             log "elab.interface" 5 $ "Method declarations: " ++ show meths

             consts <- traverse (getMethDecl env nest params meth_names . (top,)) constraints
             log "elab.interface" 5 $ "Constraints: " ++ show consts

             dt <- mkIfaceData vfc vis env consts iname conName params
                                  dets meths
             log "elab.interface" 10 $ "Methods: " ++ show meths
             log "elab.interface" 5 $ "Making interface data type " ++ show dt
             ignore $ processDecls nest env [dt]

    elabMethods : (conName : Name) -> List Name ->
                  List Signature ->
                  Core ()
    elabMethods conName meth_names meth_sigs
        = do -- Methods have same visibility as data declaration
             fnsm <- traverse (getMethToplevel env vis iname conName
                                               (map fst constraints)
                                               meth_names
                                               params) meth_sigs
             let fns = concat fnsm
             log "elab.interface" 5 $ "Top level methods: " ++ show fns
             traverse_ (processDecl [] nest env) fns
             traverse_ (\n => do mn <- inCurrentNS n
                                 setFlag vfc mn Inline
                                 setFlag vfc mn TCInline
                                 setFlag vfc mn Overloadable) meth_names

    -- Check that a default definition is correct. We just discard it here once
    -- we know it's okay, since we'll need to re-elaborate it for each
    -- instance, to specialise it
    elabDefault : List Declaration ->
                  (FC, List FnOpt, Name, List ImpClause) ->
                  Core (Name, List ImpClause)
    elabDefault tydecls (dfc, opts, n, cs)
        = do -- orig <- branch

             let dn_in = MN ("Default implementation of " ++ show n) 0
             dn <- inCurrentNS dn_in

             (rig, dty) <-
                       case findBy (\ d => d <$ guard (n == d.name)) tydecls of
                          Just d => pure (d.count, d.type)
                          Nothing => throw (GenericMsg dfc ("No method named " ++ show n ++ " in interface " ++ show iname))

             let ity = apply (IVar vdfc iname) (map (IVar vdfc) paramNames)

             -- Substitute the method names with their top level function
             -- name, so they don't get implicitly bound in the name
             methNameMap <- traverse (\d =>
                                do let n = d.name
                                   cn <- inCurrentNS n
                                   pure (n, applyParams (IVar vdfc cn) paramNames))
                               tydecls
             let dty = bindPs params      -- bind parameters
                     $ bindIFace vdfc ity -- bind interface (?!)
                     $ substNames vars methNameMap dty

             dty_imp <- bindTypeNames dfc [] (map name tydecls ++ vars) dty
             log "elab.interface.default" 5 $ "Default method " ++ show dn ++ " : " ++ show dty_imp

             let dtydecl = IClaim vdfc rig vis [] (MkImpTy EmptyFC EmptyFC dn dty_imp)

             processDecl [] nest env dtydecl

             cs' <- traverse (changeName dn) cs
             log "elab.interface.default" 5 $ "Default method body " ++ show cs'

             processDecl [] nest env (IDef vdfc dn cs')
             -- Reset the original context, we don't need to keep the definition
             -- Actually we do for the metadata and name map!
--              put Ctxt orig
             pure (n, cs)
      where
        vdfc : FC
        vdfc = virtualiseFC dfc

        -- Bind the type parameters given explicitly - there might be information
        -- in there that we can't infer after all
        bindPs : List (Name, (RigCount, RawImp)) -> RawImp -> RawImp
        bindPs [] ty = ty
        bindPs ((n, (rig, pty)) :: ps) ty
          = IPi (getFC pty) rig Implicit (Just n) pty (bindPs ps ty)

        applyParams : RawImp -> List Name -> RawImp
        applyParams tm [] = tm
        applyParams tm (UN (Basic n) :: ns)
            = applyParams (INamedApp vdfc tm (UN (Basic n)) (IBindVar vdfc n)) ns
        applyParams tm (_ :: ns) = applyParams tm ns

        changeNameTerm : Name -> RawImp -> Core RawImp
        changeNameTerm dn (IVar fc n')
            = do if n /= n' then pure (IVar fc n') else do
                 log "ide-mode.highlight" 7 $
                   "elabDefault is trying to add Function: " ++ show n ++ " (" ++ show fc ++")"
                 whenJust (isConcreteFC fc) $ \nfc => do
                   log "ide-mode.highlight" 7 $ "elabDefault is adding Function: " ++ show n
                   addSemanticDecorations [(nfc, Function, Just n)]
                 pure (IVar fc dn)
        changeNameTerm dn (IApp fc f arg)
            = IApp fc <$> changeNameTerm dn f <*> pure arg
        changeNameTerm dn (IAutoApp fc f arg)
            = IAutoApp fc <$> changeNameTerm dn f <*> pure arg
        changeNameTerm dn (INamedApp fc f x arg)
            = INamedApp fc <$> changeNameTerm dn f <*> pure x <*> pure arg
        changeNameTerm dn tm = pure tm

        changeName : Name -> ImpClause -> Core ImpClause
        changeName dn (PatClause fc lhs rhs)
            = PatClause fc <$> changeNameTerm dn lhs <*> pure rhs
        changeName dn (WithClause fc lhs wval prf flags cs)
            = WithClause fc
                 <$> changeNameTerm dn lhs
                 <*> pure wval
                 <*> pure prf
                 <*> pure flags
                 <*> traverse (changeName dn) cs
        changeName dn (ImpossibleClause fc lhs)
            = ImpossibleClause fc <$> changeNameTerm dn lhs

    elabConstraintHints : (conName : Name) -> List Name ->
                          Core ()
    elabConstraintHints conName meth_names
        = do let nconstraints = nameCons 0 constraints
             chints <- traverse (getConstraintHint vfc env vis iname conName
                                                 (map fst nconstraints)
                                                 meth_names
                                                 paramNames) nconstraints
             log "elab.interface" 5 $ "Constraint hints from " ++ show constraints ++ ": " ++ show chints
             traverse_ (processDecl [] nest env) (concatMap snd chints)
             traverse_ (\n => do mn <- inCurrentNS n
                                 setFlag vfc mn TCInline) (map fst chints)


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

import Decidable.Equality

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

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

import Data.String

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

import Toolkit.Data.Vect.Extra
import Toolkit.Data.DVect

import Circuits.Common

import Circuits.NetList.Types

import Circuits.NetList.Linear.Usage.DataType
import Circuits.NetList.Linear.Usage.DataType.Use.Full
import Circuits.NetList.Linear.Usage.DataType.Use.Partial

import Circuits.NetList.Linear.Usage.TermType
import Circuits.NetList.Linear.Usage.TermType.Use.Port
import Circuits.NetList.Linear.Usage.TermType.Use.Channel

import Circuits.NetList.Linear.Usage.Item

%default total

|||
|||
||| Construction of this will during type-checking...
public export
data IsFreePort : (item : Item)
               -> (ctxt : List Item)
                       -> Type
  where
    FreePortHere : (prf : IsFree        (TyPort (flow,dtype)) u)
                       -> IsFreePort (I (TyPort (flow,dtype)) u)
                                     (I (TyPort (flow,dtype)) u :: rest)

    FreePortThere : (later : IsFreePort (I (TyPort (flow,dtype)) u)              rest)
                          -> IsFreePort (I (TyPort (flow,dtype)) u) (not_item :: rest)

public export
data UsePort : (old : List Item)
            -> (prf : IsFreePort (I (TyPort (flow,dtype)) u) old)
            -> (new : List Item)
                   -> Type
  where
    UsePortHere : (use : Use        (TyPort (flow,dtype)) f                        pf  u pu)
                      -> UsePort (I (TyPort (flow,dtype)) f :: rest) (FreePortHere pf)
                                 (I (TyPort (flow,dtype)) u :: rest)

    UsePortThere : (later : UsePort          old                 rest           new)
                         -> UsePort (item :: old) (FreePortThere rest) (item :: new)

export
usePort : (old : List Item)
       -> (prf : IsFreePort (I (TyPort (flow,dtype)) u) old)
              -> DPair (List Item) (UsePort old prf)
usePort (I (TyPort (flow, dtype)) u :: rest) (FreePortHere prf) with (use prf)
  usePort (I (TyPort (flow, dtype)) u :: rest) (FreePortHere prf) | (R used prfU x)
    = MkDPair (I (TyPort (flow, dtype)) used :: rest) (UsePortHere x)

usePort (not_item :: rest) (FreePortThere later) with (usePort rest later)
  usePort (not_item :: rest) (FreePortThere later) | (MkDPair fst snd)
    = (not_item :: fst ** UsePortThere snd)

|||
|||
||| Construction of this will during type-checking...
public export
data IsFreeChannel : (how  : Project dir)
                  -> (item : Item)
                  -> (ctxt : List Item)
                          -> Type
  where
    FreeChannelHere : (prf : CanProject    how    (TyChan type) u)
                          -> IsFreeChannel how (I (TyChan type) u)
                                               (I (TyChan type) u  :: rest)

    FreeChannelThere : (later : IsFreeChannel how (I (TyChan type) u)              rest)
                             -> IsFreeChannel how (I (TyChan type) u) (not_item :: rest)

public export
data ProjectChannel : (how : Project dir)
                   -> (old : List Item)
                   -> (prf : IsFreeChannel how (I (TyChan dtype) u) old)
                   -> (new : List Item)
                          -> Type
  where
    ProjectHere : (use : Use            how    (TyChan type) o                           prf  n)
                      -> ProjectChannel how (I (TyChan type) o :: rest) (FreeChannelHere prf)
                                            (I (TyChan type) n :: rest)

    ProjectThere : (later : ProjectChannel how          old                    rest           new)
                         -> ProjectChannel how (item :: old) (FreeChannelThere rest) (item :: new)

export
projectChannel : (how : Project dir)
              -> (old : List Item)
              -> (prf : IsFreeChannel how (I (TyChan type) u) old)
                     -> DPair (List Item) (ProjectChannel how old prf)
projectChannel how (I (TyChan type) u :: rest) (FreeChannelHere prf) with (use prf)
  projectChannel how (I (TyChan type) u :: rest) (FreeChannelHere prf) | (R new x)
    = MkDPair (I (TyChan type) new :: rest) (ProjectHere x)

projectChannel how (not_item :: rest) (FreeChannelThere later) with (projectChannel how rest later)
  projectChannel how (not_item :: rest) (FreeChannelThere later) | (MkDPair fst snd)
    = MkDPair (not_item :: fst) (ProjectThere snd)

|||
|||
||| Construction of this will during type-checking...
public export
data CanIndexPort : (idx  : Fin n)
                 -> (item : Item)
                 -> (ctxt : List Item)
                         -> Type
  where
    CanIndexHere : (prf : IsFreeAt     idx    (TyPort (flow,dtype)) u)
                       -> CanIndexPort idx (I (TyPort (flow,dtype)) u)
                                           (I (TyPort (flow,dtype)) u  :: rest)

    CanIndexThere : (later : CanIndexPort idx (I (TyPort (flow,dtype)) u)              rest)
                          -> CanIndexPort idx (I (TyPort (flow,dtype)) u) (not_item :: rest)

public export
data IndexPort : (idx : Fin n)
              -> (old : List Item)
              -> (prf : CanIndexPort idx (I (TyPort (flow,dtype)) u) old)
              -> (new : List Item)
                     -> Type

  where
    IndexHere : (use : Use       idx    (TyPort (flow,type)) o                        prf  n pU)
                    -> IndexPort idx (I (TyPort (flow,type)) o :: rest) (CanIndexHere prf)
                                     (I (TyPort (flow,type)) n :: rest)

    IndexThere : (later : IndexPort idx          old                 rest           new)
                       -> IndexPort idx (item :: old) (CanIndexThere rest) (item :: new)

indexPort : (idx : Fin n)
         -> (old : List Item)
         -> (prf : CanIndexPort idx (I (TyPort (flow,dtype)) u) old)
                -> DPair (List Item) (IndexPort idx old prf)

indexPort idx (I (TyPort (flow, dtype)) u :: rest) (CanIndexHere prf) with (use idx prf)
  indexPort idx (I (TyPort (flow, dtype)) u :: rest) (CanIndexHere prf) | (R used prfU holds)
    = MkDPair (I (TyPort (flow, dtype)) used :: rest) (IndexHere holds)

indexPort idx (not_item :: rest) (CanIndexThere later) with (indexPort idx rest later)
  indexPort idx (not_item :: rest) (CanIndexThere later) | (MkDPair fst snd)
    = MkDPair (not_item :: fst) (IndexThere snd)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
{- Support code -}

data Shape = ||| A triangle, with its base length and height
             Triangle Double Double
           | ||| A rectangle, with its length and height
              Rectangle Double Double
           | ||| A circle, with its radius
             Circle Double

area : Shape -> Double
area (Triangle base height) = 0.5 * base * height
area (Rectangle length height) = length * height
area (Circle radius) = pi * radius * radius

data Picture = Primitive Shape
             | Combine Picture Picture
             | Rotate Double Picture
             | Translate Double Double Picture

testPic1 : Picture
testPic1 = Combine (Primitive (Triangle 2 3))
                   (Primitive (Triangle 2 4))

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

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

%name Tree tree, tree1

insert : Ord elem => elem -> Tree elem -> Tree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node left val right)
    = case compare x val of
           LT => Node (insert x left) val right
           EQ => orig
           GT => Node left val (insert x right)

{- Answers -}

{- 1 -}

listToTree : Ord a => List a -> Tree a
listToTree [] = Empty
listToTree (x :: xs) = insert x (listToTree xs)

{- 2 -}

treeToList : Tree a -> List a
treeToList Empty = []
treeToList (Node left val right) = treeToList left ++ val :: treeToList right

{- 3 -}

data Expr = Val Int
          | Add Expr Expr
          | Sub Expr Expr
          | Mult Expr Expr

{- 4 -}

evaluate : Expr -> Int
evaluate (Val x) = x
evaluate (Add x y) = evaluate x + evaluate y
evaluate (Sub x y) = evaluate x - evaluate y
evaluate (Mult x y) = evaluate x * evaluate y

{- 5 -}

maxMaybe : Ord a => Maybe a -> Maybe a -> Maybe a
maxMaybe Nothing Nothing = Nothing
maxMaybe Nothing (Just x) = Just x
maxMaybe (Just x) Nothing = Just x
maxMaybe (Just x) (Just y) = Just (max x y)

{- 6 -}

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

max_stars_repo_name: PiotrJander/TypeDD-Samples

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
> module Main

> import Syntax.PreorderReasoning
> import Data.List
> import Effects
> import Effect.Exception
> import Effect.StdIO

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

* 1. An amazingly versatile functional

They start from the offset with |bigotimes|, the function to be
discussed in the paper

> bigotimes : {X, R : Type} -> List ((X -> R) -> X) -> (List X -> R) -> List X
> bigotimes  Nil      p = Nil
> bigotimes (e :: es) p = x0 :: bigotimes es (p . (x0 ::)) where
>   x0 = e (\ x => p (x :: bigotimes es (p . (x ::))))

, introduce the notion of selection function

> Selection : Type -> Type -> Type
> Selection X R = (X -> R) -> X

and of a "binary operation that combines two selection functions" in
terms of which |bigotimes| can be implemented recursively. In the rest
of the section they relate |bigotimes| with sequential games (apparently
deterministic, with finite or infinite number of steps and alternating
players), with the Tychonoff theorem and with the Double-Negation Shift
(DNS). Then they present an outline of the paper.

* 2. Selection functions

They start by introducing shortcuts for (flipped) selection functions

> J : Type -> Type -> Type
> J R X = (X -> R) -> X

and generalized quantifiers

> K : Type -> Type -> Type
> K R X = (X -> R) -> R

Here, |R| represents generalized truth values. The text suggests that
selection functions of type |J R X| and quantifiers of type |K R X| take
as arguments functions of type |X -> R| that represent properties of
values of type |X|, see the "Terminology" table.

As a matter of fact, however, these functions are not dependently
typed. I think that the arguments of selection functions and quantifiers
are in fact decision procedured associated for a decidable property of
interest. Thus, for instance, for |X = Nat| and |R = Bool|, one could
have

> P : Nat -> Type
> P i = LTE i 42

and

> dP : Nat -> Bool
> dP i = if i <= 42 then True else False

Anyway, the authors go on by remarking that, with the |J| operator, the
type of |bigotimes| can be rewritten as

< bigotimes : {X, R : Type} -> List (J R X) -> J R (List X)

They then introduce

> overline : {X, R : Type} -> J R X -> K R X
> overline e = \ p => p (e p)

and start discussing selection functions for sets in a subsection.

** 2.1 Selection functions for sets

Escardo-Oliva start by stating that "A selection function for a set S
finds an element of S for which a given predicate holds". They require
selection functions for sets to be total and point out that "if there is
no element of S satisfying the predicate, we select an arbitrary element
of S". Thus, selection functions for sets are only defined for non-empty
sets

> find : {X : Type} -> (xs : List X) -> NonEmpty xs -> J Bool X -- J Bool xs
> find      Nil  _ p impossible
> find (x :: xs) _ p with (nonEmpty xs)
>   | (Yes prf) = if p x then x else find xs prf p
>   | ( No prf) = x

> forsome : {X : Type} -> (xs : List X) -> NonEmpty xs -> K Bool X
> forsome xs ne = overline (find xs ne)

> forevery : {X : Type} -> (xs : List X) -> NonEmpty xs -> K Bool X
> forevery xs ne p = not (forsome xs ne (not . p))

At this point, Escardo-Oliva point out that their definition of the
existential quantifier is the same as in Hilbert’s ε-calculus:

  ∃x p(x) ⇐⇒ p(ε(p)).

This looks like a claim about |find|:

> findLemma1 : {X : Type} ->
>              (xs : List X) -> (ne : NonEmpty xs) -> (p : X -> Bool) ->
>              (x ** p x = True) -> p (find xs ne p) = True

> findLemma2 : {X : Type} ->
>              (xs : List X) -> (ne : NonEmpty xs) -> (p : X -> Bool) ->
>              p (find xs ne p) = True -> (x ** p x = True)

The second lemma holds trivially

> findLemma2 {X} xs ne p prf = (find xs ne p ** prf)

and it should not be difficult to show that the first one holds as well
using the implementation of |find|:

> findLemma2 {X}      Nil  _ p prf impossible
> findLemma2 {X} (x :: xs) _ p prf = ?lala

Further, they state that a selection function ε for a set S has to
satisfy:

1. ε(p) ∈ S, whether or not there actually is some x ∈ S such that p(x)
   holds.

2. If p(x) holds for some x ∈ S, then it holds for x = ε(p).

With the helper function

> typeOf : {X : Type} -> X -> Type
> typeOf {X} _ = X

the first condition boils down to

> SpecJ1 : {X, R : Type} -> (eps : J R X) -> (p : X -> R) -> typeOf (eps p) = X

which trivially holds

> SpecJ1 eps p = Refl

In the second condition it is not completely clear what it means for
p(x) to "hold". If we restrict ourselves to the case in which |R =
Bool|, I think that the condition could be written as

< SpecJ2 : {X : Type} -> (eps : J Bool X) -> (p : X -> Bool) -> (x : X) -> p x = True -> p (eps p) = True

Here we have translated "p(x) holds" with |p x = True|. If the arguments
of selection functions and quantifiers were truly propositions, we would
again know how to formalize condition 2

< SpecJ2 : {X : Type} -> (eps : J Type X) -> (p : X -> Type) -> (x : X) -> p x -> p (eps p)

** 2.2 Selection functions for quantifiers

Hilbert's condition

  ϕ p = p (ε p)

is used to express what it means for a selection function to be
compatible with a quantifier:

> infixl 9 <>

> (<>) : {X, R : Type} -> (eps : J R X) -> (phi : K R X) -> Type
> (<>) {X} {R} eps phi = (p : X -> R) -> phi p = p (eps p)

This trivially implies

> overlineLemma : {X, R : Type} -> (eps : J R X) -> eps <> overline eps
> overlineLemma eps = \ p => Refl

Then they give examples of selection functions that are compatible with
given quantifiers. One for the universal quantifier

< forevery : {X : Type} -> (xs : List X) -> NonEmpty xs -> K Bool X
< forevery xs ne p = not (forsome xs ne (not . p))

is |findnot|:

> findnot : {X : Type} -> (xs : List X) -> NonEmpty xs -> J Bool X
> findnot      Nil  _ p impossible
> findnot (x :: xs) _ p with (nonEmpty xs)
>   | (Yes prf) = if p x then find xs prf p else x
>   | ( No prf) = x

they argue. They first notice that

> findnotLemma : {X : Type} ->
>                (xs : List X) -> (ne : NonEmpty xs) ->
>                (p : X -> Bool) -> findnot xs ne p = find xs ne (not . p)

and

> foreveryFindnotLemma : {X : Type} ->
>                        (xs : List X) -> (ne : NonEmpty xs) ->
>                        (p : X -> Bool) ->
>                        forevery xs ne p = overline (findnot xs ne) p

from which they conclude

> findnotForeveryLemma : {X : Type} ->
>                        (xs : List X) -> (ne : NonEmpty xs) ->
>                        findnot xs ne <> forevery xs ne
> findnotForeveryLemma xs ne p = ( forevery xs ne p )
>                              ={ foreveryFindnotLemma xs ne p }=
>                                ( overline (findnot xs ne) p )
>                              ={ overlineLemma (findnot xs ne) p }=
>                                ( p (findnot xs ne p) )
>                              QED

Further examples of selection functions are given for "predicates" that
return numbers rather than Boolean values:

> {-

> argsup : {X : Type} -> (xs : List X) -> (ne : NonEmpty xs) -> J Int X
> argsup      Nil  _ p impossible
> argsup (x :: xs) _ p with (nonEmpty xs)
>   | (Yes prf) = if p x < p x' then x' else x
>       where x' = argsup xs prf p
>   | ( No prf) = x

> arginf : {X : Type} -> (xs : List X) -> (ne : NonEmpty xs) -> J Int X
> arginf xs ne p = argsup xs ne (\ x => - p x)

>-}

-- > partial
-- > argsup : {X : Type} -> List X -> J Int X  --  here Int is just {-1, 0, 1}
-- > -- argsup [] p  =  undefined
-- > argsup {X} (x :: xs) p  =  f xs x (p x)
-- >   where
-- >   f : List X -> X -> Int -> X
-- >   f xs' a 1  =  a
-- >   f [] a r  =  a
-- >   f xs'       a  0    =  g xs'
-- >     where
-- >     g []  =  a
-- >     g (a :: as)  = if  p a  ==  1  then  a else g as
-- >   f (x' :: xs') a r  =  f xs' x' (p x') -- at this point, r = -1

-- > {- original implementation (non-optimised) -}
-- > partial
-- > argsup : {X : Type} -> (xs : List X) -> J Int X
-- > argsup (x :: xs) p with (nonEmpty xs)
-- >   | (Yes prf) = if p x < p x' then x' else x
-- >       where x' = argsup xs p
-- >   | ( No prf) = x

> partial
> argsup : {X : Type} -> (xs : List X) -> J Int X
> argsup (x :: Nil) p = x
> argsup (x :: x' :: xs) p = if p x < p x' then argsup (x' :: xs) p else argsup (x :: xs) p

-- > findnot xs prf p  =  find xs prf (not . p)

> partial
> arginf : {X : Type} -> (xs : List X) -> J Int X
> arginf xs p = argsup xs (\ x => - p x)

* 3 Products of selection functions

** 3.1 Binary product

> opairJ : {X, Y, R : Type} -> J R X -> J R Y -> J R (X,Y)
> opairJ epsx epsy p = (a, b) where
>   a = epsx (\ x => overline epsy (\ y => p (x, y)))
>   b = epsy (\ y => p (a, y))

> opairK : {X, Y, R : Type} -> K R X -> K R Y -> K R (X,Y)
> opairK phix phiy p = phix (\ x => phiy (\ y => p (x, y)))

It is easy to see that |opairJ| implements two backwards induction steps
followed by a forward computation of "optimal" controls:

> opairJ' : {X, Y, R : Type} -> J R X -> J R Y -> J R (X,Y)
> opairJ' {X} {Y} epsx epsy p = (x, y) where
>   piy  :  X -> Y
>   piy  =  \ x => epsy (\ y => p (x, y))
>   pix  :  Unit -> X
>   pix  =  \ u => epsx (\ x => p (x, piy x))
>   x    :  X
>   x    =  pix ()
>   y    :  Y
>   y    =  piy x

In this context, the set of states at decision steps one and two are
|Unit| and |X|, respectively. The controls are |X| in the first step and
|Y| in the second step.

In order to compute the result of |opairJ' epsx epsy p|, we first
compute |piy|. This is an optimal policy for the second (last) step in
the sense that for every |x : X|, |piy x| is a "best" control, that is

< p (x, piy x) = overline epsy (curry p x)

< p (x, piy x)
<
<   { Def. |piy| }
<
< p (x, epsy (\ y => p (x, y)))
<
<   { Def. |curry| }
<
< (curry p) x (epsy (\ y => curry p x y))
<
<   { Abstraction }
<
< (curry p) x (epsy (curry p x))
<
<   { |overline e q = q (e q)| with |q = (curry p) x| and |e = epsy| }
<
< overline epsy (curry p x)

Then, we compute |pix|. This is an optimal extension of |piy| in the
sense that for every |u : Unit|, |pix u| is a "best" control *under the
assumption that the next decision is taken with |piy|*, that is

< p (pix u, piy (pix u)) = overline epsx (\ x => p (x, (piy x)))

< p (pix u, piy (pix u))
<
<   { Def. |pix| }
<
< p (epsx (\ x => p (x, piy x)), piy (epsx (\ x => p (x, piy x))))
<
<   { Let |g = \ x => p (x, piy x)| }
<
< p (epsx g, piy (epsx g))
<
<   { Def. |g| }
<
< g (epsx g)
<
<   { Def. |overline| }
<
< overline epsx g
<
<   { Def. |g| }
<
< overline epsx (\ x => p (x, piy x))

Finally, we compute |x| by applying the policy |pix| to |()| and then
|y| by applying |piy| to |x|. It remains to show that |opairJ' epsx epsy
p = opairJ eosx epsy p| for all |epsx : J R X|, |epsy : J R Y| and |p :
(X, Y) -> R|:

< opairJ' epsx epsy p
<
<   { Def. |opairJ'| }
<
< (x, y)
<
<   { Def. |x| and |y| in |opairJ'| }
<
< (pix (), piy (pix ()))
<
<   { Def. |pix ()| in |opairJ'| }
<
< (epsx (\ x => p (x, piy x)), piy (epsx (\ x => p (x, piy x))))
<
<   { Def. |piy| in |opairJ'| }
<
< (epsx (\ x => p (x, epsy (\ y => p (x, y)))), piy (epsx (\ x => p (x, epsy (\ y => p (x, y))))))
<
<   { Let |q x = \ y => p (x, y)| }
<
< (epsx (\ x => (q x) (epsy (q x))), piy (epsx (\ x => (q x) (epsy (qx)))))
<
<   { Def. |overline e p = p (e p)| with |p = q x| and |e = epsy| }
<
< (epsx (\ x => overline epsy (q x)), piy (epsx (\ x => overline epsy (q x))))
<
<   { Def. |q x| }
<
< (epsx (\ x => overline epsy (\ y => p (x, y))), piy (epsx (\ x => overline epsy (\ y => p (x, y)))))
<
<   { Def. |a| in |opairJ| }
<
< (a, piy a)
<
<   { Def. |piy| in |opairJ'| }
<
< (a, epsy (\ y => p (a, y)))
<
<   { Def. |b| in |opairJ| }
<
< (a, b)
<
<   { Def. |opairJ| }
<
< opairJ epsx epsy p

** 3.2 Iterated product

Define the product of a "sequence of sets |X 0|, |X 1|, ..., |X n|,
...". First we need a tail function for families of types:

> Tail : (Nat -> Type) -> (Nat -> Type)
> Tail X = \ n => X (S n)

Then we can define the product as a list

> data Prod : (Nat -> Type) -> Type where
>   Nil   :  {X : Nat -> Type} -> Prod X
>   (::)  :  {X : Nat -> Type} -> (x : X Z) -> Prod (Tail X) -> Prod X

We cannot implement the iterated product in terms of |opairJ| because
the types of the arguments have to be in the relation implied by
|Prod|. We need a more specific helper:

> oprodJ : {X : Nat -> Type} -> {R : Type} ->
>          J R (X Z) -> J R (Prod (Tail X)) -> J R (Prod X)
> oprodJ e ep p = a :: as where
>   a  = e (\ x => overline ep (\ xs => p (x :: xs)))
>   as = ep (\ xs => p (a :: xs))

With |oprodJ| implementing the iterated product is easy:

> bigoprodJ : {X : Nat -> Type} -> {R : Type} ->
>             Prod ((J R) . X) -> J R (Prod X)
> bigoprodJ      Nil  = \ p => Nil
> bigoprodJ (e :: es) = oprodJ e (bigoprodJ es)

We can do othe same with vectors instead of lists

< data Prod : Nat -> (Nat -> Type) -> Type where
<   Nil   :               {X : Nat -> Type} -> Prod Z X
<   (::)  :  {n : Nat} -> {X : Nat -> Type} -> (x : X Z) -> Prod n (Tail X) -> Prod (S n) X

< oprodJ : {X : Nat -> Type} -> {R : Type} -> {n : Nat} ->
<          J R (X Z) -> J R (Prod n (Tail X)) -> J R (Prod (S n) X)
< oprodJ e ep p = a :: as where
<   a  = e (\ x => overline ep (\ xs => p (x :: xs)))
<   as = ep (\ xs => p (a :: xs))

< bigoprodJ : {X : Nat -> Type} -> {R : Type} -> {n : Nat} ->
<             Prod n ((J R) . X) -> J R (Prod n X)
< bigoprodJ      Nil  = \ p => Nil
< bigoprodJ (e :: es) = oprodJ e (bigoprodJ es)

Because they do not have dependent types, they implement |bigoprodJ| in
Haskell for the special case of a constant family of types:

> otimesJ : {X : Type} -> {R : Type} ->
>           J R X -> J R (List X) -> J R (List X)
> otimesJ e ep p = a :: as where
>   a  = e (\ x => overline ep (\ xs => p (x :: xs)))
>   as = ep (\ xs => p (a :: xs))

> bigotimesJ : {X, R : Type} -> List (J R X) -> J R (List X)
> bigotimesJ      Nil  = \ p => Nil
> bigotimesJ (e :: es) = otimesJ e (bigotimesJ es)

* 4. Playing games

** 4.2 History dependent games

-- > hotimesJ : {X : Type} -> {R : Type} ->
-- >           J R X -> (X -> J R (List X)) -> J R (List X)
-- > hotimesJ e f p = a :: as where
-- >   a  = e (\ x => overline (f x) (\ xs => p (x :: xs)))
-- >   as = (f a) (\ xs => p (a :: xs))

> hotimesJ : {X : Type} -> {R : Type} ->
>           J R X -> (X -> J R (List X)) -> J R (List X)
> hotimesJ e0 e1 p = a0 :: a1
>   where
>   a0 = e0 (\ x0 => overline (e1 x0) (\ x1 => p (x0 :: x1)))
>   a1 = e1 a0 (\ x1 => p (a0 :: x1))

> bighotimesJ : {X, R : Type} -> List (List X -> J R X) -> J R (List X)
> bighotimesJ [] = \p => []
> bighotimesJ (e :: es)  =  (e []) `hotimesJ` (\x => bighotimesJ [\ xs => d (x :: xs) | d <- es])

** 4.3 Implementation of games and optimal strategies

-- > data Game : Type -> Type -> Type where
-- >   MkGame : {Move, Outcome : Type} ->
-- >            (p : List Move -> Outcome) ->
-- >            (es : List (List Move -> J Outcome Move)) ->
-- >            Game Move Outcome

-- > pred : {Move, Outcome : Type} -> Game Move Outcome -> (List Move -> Outcome)
-- > pred (MkGame p _) = p

-- > epss : {Move, Outcome : Type} -> Game Move Outcome -> List (List Move -> J Outcome Move)
-- > epss (MkGame _ es) = es

> {-
> optimalStrategy : {Move, Outcome : Type} -> Game Move Outcome -> List Move -> Move
> optimalStrategy {Move} {Outcome} g ms = head (optimalPlay g') where
>   g' : Game Move Outcome
>   g' = MkGame p' es' where
>     p'   :  List Move -> Outcome
>     p'   =  \ ms' => (pred g) (ms ++ ms')
>     es'  :  List (List Move -> J Outcome Move)
>     es'  =  drop (length ms) (epss g)
> -}

** 4.5 Tic-Tac-Toe

> data Player =  X | O

> Outcome : Type
> Outcome = Int

> Move : Type
> Move = Int

> Board : Type
> Board = (List Move, List Move)

> someContained : {X : Type} -> Ord X =>
>                 List (List X) -> List X -> Bool

> wins : List Move -> Bool
> wins = someContained [[0,1,2],[3,4,5],[6,7,8],
>                       [0,3,6],[1,4,7],[2,5,8],
>                       [0,4,8],[2,4,6]]

> value : Board -> Outcome
> value (xs, os) = if wins xs
>                  then 1
>                  else if wins os
>                       then -1
>                       else 0

> insert : {X : Type} -> Ord X => X -> List X -> List X

> outcome : Player -> List Move -> Board -> Board
> outcome _      Nil     board = board
> outcome X (m :: ms) (xs, os) = if wins os
>                                then (xs, os)
>                                else outcome O ms (insert m xs, os)
> outcome O (m :: ms) (xs, os) = if wins xs
>                                then (xs, os)
>                                else outcome X ms (xs, insert m os)

> setMinus : {X : Type} -> Ord X =>
>            List X -> List X -> List X

-- > partial
-- > es : List (List Move -> J Outcome Move)
-- > es = take 3 all where
-- >   partial
-- >   eX  :  List Move -> J Outcome Move
-- >   eX  =  \ h => argsup (setMinus [0..8] h)
-- >   partial
-- >   eO  :  List Move -> J Outcome Move
-- >   eO  =  \ h => arginf (setMinus [0..8] h)
-- >   partial
-- >   all :  List (List Move -> J Outcome Move)
-- >   all =  [eX, eO, eX, eO, eX, eO, eX, eO, eX, eO]

-- > partial
-- > ticTacToe : Game Move Outcome
-- > ticTacToe = MkGame p es

> partial
> epsilons : List (List Move -> J Outcome Move)
> epsilons = take 3 all where
>   partial
>   eX  :  List Move -> J Outcome Move
>   eX  =  \ h => argsup (setMinus [0..8] h)
>   partial
>   eO  :  List Move -> J Outcome Move
>   eO  =  \ h => arginf (setMinus [0..8] h)
>   partial
>   all :  List (List Move -> J Outcome Move)
>   all =  [eX, eO, eX, eO, eX, eO, eX, eO, eX, eO]

> p : List Move -> Outcome
> p ms = value (outcome X ms (Nil, Nil))

> partial
> optimalPlay : List Move
> optimalPlay = bighotimesJ epsilons p

> partial
> optimalOutcome : Outcome
> optimalOutcome = p optimalPlay

> partial
> main : IO ()
> main =
>   do putStr ("An optimal play for Tic-Tac-Toe is "
>              ++
>              show optimalPlay ++ "\n"
>              ++
>              "and the optimal outcome is "
>              ++
>              show optimalOutcome ++ "\n"
>              )

** 4.7 Appendix

> contained : {X : Type} -> Ord X => List X -> List X -> Bool
> contained       []        ys  = True
> contained       xs        []  = False
> contained (x :: xs) (y :: ys) = if x == y
>                                 then contained xs ys
>                                 else if x >= y
>                                      then contained (x :: xs) ys
>                                      else False

> someContained         []  ys  = False
> someContained        xss  []  = False
> someContained (xs :: xss) ys = contained xs ys || someContained xss ys

> insert x [] = [x]
> insert x (y :: ys) = if x == y
>                      then (y :: ys)
>                      else if x < y
>                           then x :: (y :: ys)
>                           else y :: (insert x ys)

> delete : {X : Type} -> Ord X => X -> List X -> List X
> delete x [] = []
> delete x (y :: ys) = if x == y
>                      then ys
>                      else if x < y
>                           then y :: ys
>                           else y :: Main.delete x ys

> setMinus xs       []  = xs
> setMinus xs (y :: ys) = setMinus (Main.delete y xs) ys

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module GameMessage
import GameState
import IdrisNet.PacketLang
import IdrisNet.UDP.UDPClient
import Effect.StdIO

-- Data structure communicated between aux thread and master thread,
-- signifying some update.
data GameMessage = UpdateRemotePaddle Bool Bool Int Int -- Up pressed, down pressed, x, y
                 | UpdateRemoteBallPos PongBall

ballUpdate : PacketLang
ballUpdate = with PacketLang do
  x <- bits 32
  y <- bits 32
  xv_neg <- bool
  x_vel <- bits 32
  yv_neg <- bool
  y_vel <- bits 32
  bool -- Stuck to paddle?
  bool -- Last hit left

paddleUpdate : PacketLang
paddleUpdate = with PacketLang do
  bool
  bool
  bits 32 -- X
  bits 32 -- Y

statusUpdate : PacketLang
statusUpdate = with PacketLang do
  is_ball <- bool -- True if ball update, false if paddle
  p_if is_ball then ballUpdate else paddleUpdate

mkMessage : (mkTy statusUpdate) -> GameMessage
mkMessage (True ## x ## y ## xv_neg ## xv ## yv_neg ## yv ## stuck ## left) =
    UpdateRemoteBallPos $ MkPongBall (val x, val y) xv' yv' stuck left
  where xv' = if xv_neg then ((val xv) * (-1)) else (val xv)
        yv' = if yv_neg then ((val yv) * (-1)) else (val yv)

mkMessage (False ## up ## down ## x ## y) = UpdateRemotePaddle up down (val x) (val y)

sendBallUpdate : { [STATE GameState, STDIO, UDPCLIENT] } Eff Bool
sendBallUpdate = do
    st <- get
    let sa = pongRemoteAddr st
    let p = pongRemotePort st
    case m_pckt (pongBall st) of
      Just pckt => do IdrisNet.UDP.UDPClient.udpWritePacket sa p statusUpdate pckt
                      return True
      Nothing => return False
  where m_pckt : PongBall -> (Maybe (mkTy statusUpdate))
        m_pckt pb = with Monad do
                       let ((x, y), xv, yv) =
                         (pongBallPos pb, pongBallXVel pb, pongBallYVel pb)
                       b_x <- mkBounded 32 x
                       b_y <- mkBounded 32 y
                       let neg_xv = xv < 0
                       b_xv <- mkBounded 32 (abs xv)
                       let neg_yv = yv < 0
                       b_yv <- mkBounded 32 (abs yv)
                       return (True ## b_x ## b_y ## neg_xv ## b_xv ##
                               neg_yv ## b_yv ## (pongBallStuck pb) ## (pongBallHitLeft pb))

sendPaddleUpdate : { [STATE GameState, UDPCLIENT] } Eff Bool
sendPaddleUpdate = do
    st <- get
    let sa = pongRemoteAddr st
    let p = pongRemotePort st
    let up_pressed = pongIsUpPressed st
    let down_pressed = pongIsDownPressed st
    case m_pckt up_pressed down_pressed !getLocalPaddlePos of
      Just pckt => do IdrisNet.UDP.UDPClient.udpWritePacket sa p statusUpdate pckt
                      return True
      Nothing => return False
  where m_pckt : Bool -> Bool -> (Int, Int) -> (Maybe (mkTy statusUpdate))
        m_pckt up_pressed down_pressed (x, y) = with Monad do
          b_x <- mkBounded 32 x
          b_y <- mkBounded 32 y
          return (False ## up_pressed ## down_pressed ## b_x ## b_y)


text:
%default total

data S = T | F

Eq S where

main : IO ()
main = printLn $ T == T

%default covering


text:
module Data.List.AtIndex

import Data.DPair
import Data.List.HasLength
import Data.Nat
import Decidable.Equality

%default total

||| @AtIndex witnesses the fact that a natural number encodes a membership proof.
||| It is meant to be used as a runtime-irrelevant gadget to guarantee that the
||| natural number is indeed a valid index.
public export
data AtIndex : a -> List a -> Nat -> Type where
  Z : AtIndex a (a :: as) Z
  S : AtIndex a as n -> AtIndex a (b :: as) (S n)

||| Inversion principle for Z constructor
export
inverseZ : AtIndex x (y :: xs) Z -> x === y
inverseZ Z = Refl

||| inversion principle for S constructor
export
inverseS : AtIndex x (y :: xs) (S n) -> AtIndex x xs n
inverseS (S p) = p

||| An empty list cannot possibly have members
export
Uninhabited (AtIndex a [] n) where
  uninhabited Z impossible
  uninhabited (S _) impossible

||| For a given list and a given index, there is only one possible value
||| stored at that index in that list
export
atIndexUnique : AtIndex a as n -> AtIndex b as n -> a === b
atIndexUnique Z Z = Refl
atIndexUnique (S p) (S q) = atIndexUnique p q

||| Provided that equality is decidable, we can look for the first occurence
||| of a value inside of a list
public export
find : DecEq a => (x : a) -> (xs : List a) -> Dec (Subset Nat (AtIndex x xs))
find x [] = No (\ p => void (absurd (snd p)))
find x (y :: xs) with (decEq x y)
  find x (x :: xs) | Yes Refl = Yes (Element Z Z)
  find x (y :: xs) | No neqxy = case find x xs of
      Yes (Element n prf) => Yes (Element (S n) (S prf))
      No notInxs => No $ \case
        (Element Z p) => void (neqxy (inverseZ p))
        (Element (S n) prf) => absurd (notInxs (Element n (inverseS prf)))

||| If the equality is not decidable, we may instead rely on interface resolution
public export
interface Member (0 t : a) (0 ts : List a) where
  isMember' : Subset Nat (AtIndex t ts)

public export
isMember : (0 t : a) -> (0 ts : List a) -> Member t ts =>
              Subset Nat (AtIndex t ts)
isMember t ts @{p} = isMember' @{p}

public export
Member t (t :: ts) where
  isMember' = Element 0 Z

public export
Member t ts => Member t (u :: ts) where
  isMember' = let (Element n prf) = isMember t ts in
              Element (S n) (S prf)

||| Given an index, we can decide whether there is a value corresponding to it
public export
lookup : (n : Nat) -> (xs : List a) -> Dec (Subset a (\ x => AtIndex x xs n))
lookup n [] = No (\ p => void (absurd (snd p)))
lookup Z (x :: xs) = Yes (Element x Z)
lookup (S n) (x :: xs) = case lookup n xs of
  Yes (Element x p) => Yes (Element x (S p))
  No notInxs => No (\ (Element x p) => void (notInxs (Element x (inverseS p))))

||| An AtIndex proof implies that n is less than the length of the list indexed into
public export
inRange : (n : Nat) -> (xs : List a) -> (0 _ : AtIndex x xs n) -> LTE n (length xs)
inRange n [] p = void (absurd p)
inRange Z (x :: xs) p = LTEZero
inRange (S n) (x :: xs) p = LTESucc (inRange n xs (inverseS p))

|||
export
weakenR : AtIndex x xs n -> AtIndex x (xs ++ ys) n
weakenR Z = Z
weakenR (S p) = S (weakenR p)

export
weakenL : (p : Subset Nat (HasLength ws)) -> AtIndex x xs n -> AtIndex x (ws ++ xs) (fst p + n)
weakenL m p = case view m of
  Z     => p
  (S m) => S (weakenL m p)

export
strengthenL : (p : Subset Nat (HasLength xs)) ->
              lt n (fst p) === True ->
              AtIndex x (xs ++ ys) n -> AtIndex x xs n
strengthenL m lt idx = case view m of
  S m => case idx of
    Z => Z
    S idx => S (strengthenL m lt idx)

export
strengthenR : (p : Subset Nat (HasLength ws)) ->
              lte (fst p) n === True ->
              AtIndex x (ws ++ xs) n -> AtIndex x xs (minus n (fst p))
strengthenR m lt idx = case view m of
  Z => rewrite minusZeroRight n in idx
  S m => case idx of S idx => strengthenR m lt idx


text:
module Web.Internal.IndexedDBPrim

import JS
import Web.Internal.Types

%default total

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

namespace IDBCursor

  export
  %foreign "browser:lambda:x=>x.direction"
  prim__direction : IDBCursor -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.key"
  prim__key : IDBCursor -> PrimIO AnyPtr

  export
  %foreign "browser:lambda:x=>x.primaryKey"
  prim__primaryKey : IDBCursor -> PrimIO AnyPtr

  export
  %foreign "browser:lambda:x=>x.request"
  prim__request : IDBCursor -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:x=>x.source"
  prim__source : IDBCursor -> PrimIO (Union2 IDBObjectStore IDBIndex)

  export
  %foreign "browser:lambda:(x,a)=>x.advance(a)"
  prim__advance : IDBCursor -> Bits32 -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.continue(a)"
  prim__continue : IDBCursor -> UndefOr AnyPtr -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.continuePrimaryKey(a,b)"
  prim__continuePrimaryKey : IDBCursor -> AnyPtr -> AnyPtr -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.delete()"
  prim__delete : IDBCursor -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a)=>x.update(a)"
  prim__update : IDBCursor -> AnyPtr -> PrimIO IDBRequest

namespace IDBCursorWithValue

  export
  %foreign "browser:lambda:x=>x.value"
  prim__value : IDBCursorWithValue -> PrimIO AnyPtr

namespace IDBDatabase

  export
  %foreign "browser:lambda:x=>x.name"
  prim__name : IDBDatabase -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.objectStoreNames"
  prim__objectStoreNames : IDBDatabase -> PrimIO DOMStringList

  export
  %foreign "browser:lambda:x=>x.onabort"
  prim__onabort : IDBDatabase -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onabort = v}"
  prim__setOnabort : IDBDatabase -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onclose"
  prim__onclose : IDBDatabase -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onclose = v}"
  prim__setOnclose : IDBDatabase -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onerror"
  prim__onerror : IDBDatabase -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onerror = v}"
  prim__setOnerror : IDBDatabase -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onversionchange"
  prim__onversionchange : IDBDatabase -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onversionchange = v}"
  prim__setOnversionchange :  IDBDatabase
                           -> Nullable EventHandlerNonNull
                           -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.version"
  prim__version : IDBDatabase -> PrimIO JSBits64

  export
  %foreign "browser:lambda:x=>x.close()"
  prim__close : IDBDatabase -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.createObjectStore(a,b)"
  prim__createObjectStore :  IDBDatabase
                          -> String
                          -> UndefOr IDBObjectStoreParameters
                          -> PrimIO IDBObjectStore

  export
  %foreign "browser:lambda:(x,a)=>x.deleteObjectStore(a)"
  prim__deleteObjectStore : IDBDatabase -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.transaction(a,b,c)"
  prim__transaction :  IDBDatabase
                    -> Union2 String (Array String)
                    -> UndefOr String
                    -> UndefOr IDBTransactionOptions
                    -> PrimIO IDBTransaction

namespace IDBFactory

  export
  %foreign "browser:lambda:(x,a,b)=>x.cmp(a,b)"
  prim__cmp : IDBFactory -> AnyPtr -> AnyPtr -> PrimIO Int16

  export
  %foreign "browser:lambda:x=>x.databases()"
  prim__databases : IDBFactory -> PrimIO (Promise (Array IDBDatabaseInfo))

  export
  %foreign "browser:lambda:(x,a)=>x.deleteDatabase(a)"
  prim__deleteDatabase : IDBFactory -> String -> PrimIO IDBOpenDBRequest

  export
  %foreign "browser:lambda:(x,a,b)=>x.open(a,b)"
  prim__open :  IDBFactory
             -> String
             -> UndefOr JSBits64
             -> PrimIO IDBOpenDBRequest

namespace IDBIndex

  export
  %foreign "browser:lambda:x=>x.keyPath"
  prim__keyPath : IDBIndex -> PrimIO AnyPtr

  export
  %foreign "browser:lambda:x=>x.multiEntry"
  prim__multiEntry : IDBIndex -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.name"
  prim__name : IDBIndex -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.name = v}"
  prim__setName : IDBIndex -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.objectStore"
  prim__objectStore : IDBIndex -> PrimIO IDBObjectStore

  export
  %foreign "browser:lambda:x=>x.unique"
  prim__unique : IDBIndex -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,a)=>x.count(a)"
  prim__count : IDBIndex -> UndefOr AnyPtr -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a,b)=>x.getAll(a,b)"
  prim__getAll :  IDBIndex
               -> UndefOr AnyPtr
               -> UndefOr Bits32
               -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a,b)=>x.getAllKeys(a,b)"
  prim__getAllKeys :  IDBIndex
                   -> UndefOr AnyPtr
                   -> UndefOr Bits32
                   -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a)=>x.get(a)"
  prim__get : IDBIndex -> AnyPtr -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a)=>x.getKey(a)"
  prim__getKey : IDBIndex -> AnyPtr -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a,b)=>x.openCursor(a,b)"
  prim__openCursor :  IDBIndex
                   -> UndefOr AnyPtr
                   -> UndefOr String
                   -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a,b)=>x.openKeyCursor(a,b)"
  prim__openKeyCursor :  IDBIndex
                      -> UndefOr AnyPtr
                      -> UndefOr String
                      -> PrimIO IDBRequest

namespace IDBKeyRange

  export
  %foreign "browser:lambda:(a,b,c,d)=>IDBKeyRange.bound(a,b,c,d)"
  prim__bound :  AnyPtr
              -> AnyPtr
              -> UndefOr Boolean
              -> UndefOr Boolean
              -> PrimIO IDBKeyRange

  export
  %foreign "browser:lambda:(a,b)=>IDBKeyRange.lowerBound(a,b)"
  prim__lowerBound : AnyPtr -> UndefOr Boolean -> PrimIO IDBKeyRange

  export
  %foreign "browser:lambda:(a)=>IDBKeyRange.only(a)"
  prim__only : AnyPtr -> PrimIO IDBKeyRange

  export
  %foreign "browser:lambda:(a,b)=>IDBKeyRange.upperBound(a,b)"
  prim__upperBound : AnyPtr -> UndefOr Boolean -> PrimIO IDBKeyRange

  export
  %foreign "browser:lambda:x=>x.lower"
  prim__lower : IDBKeyRange -> PrimIO AnyPtr

  export
  %foreign "browser:lambda:x=>x.lowerOpen"
  prim__lowerOpen : IDBKeyRange -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.upper"
  prim__upper : IDBKeyRange -> PrimIO AnyPtr

  export
  %foreign "browser:lambda:x=>x.upperOpen"
  prim__upperOpen : IDBKeyRange -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,a)=>x.includes(a)"
  prim__includes : IDBKeyRange -> AnyPtr -> PrimIO Boolean

namespace IDBObjectStore

  export
  %foreign "browser:lambda:x=>x.autoIncrement"
  prim__autoIncrement : IDBObjectStore -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.indexNames"
  prim__indexNames : IDBObjectStore -> PrimIO DOMStringList

  export
  %foreign "browser:lambda:x=>x.keyPath"
  prim__keyPath : IDBObjectStore -> PrimIO AnyPtr

  export
  %foreign "browser:lambda:x=>x.name"
  prim__name : IDBObjectStore -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.name = v}"
  prim__setName : IDBObjectStore -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.transaction"
  prim__transaction : IDBObjectStore -> PrimIO IDBTransaction

  export
  %foreign "browser:lambda:(x,a,b)=>x.add(a,b)"
  prim__add : IDBObjectStore -> AnyPtr -> UndefOr AnyPtr -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:x=>x.clear()"
  prim__clear : IDBObjectStore -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a)=>x.count(a)"
  prim__count : IDBObjectStore -> UndefOr AnyPtr -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.createIndex(a,b,c)"
  prim__createIndex :  IDBObjectStore
                    -> String
                    -> Union2 String (Array String)
                    -> UndefOr IDBIndexParameters
                    -> PrimIO IDBIndex

  export
  %foreign "browser:lambda:(x,a)=>x.delete(a)"
  prim__delete : IDBObjectStore -> AnyPtr -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a)=>x.deleteIndex(a)"
  prim__deleteIndex : IDBObjectStore -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.getAll(a,b)"
  prim__getAll :  IDBObjectStore
               -> UndefOr AnyPtr
               -> UndefOr Bits32
               -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a,b)=>x.getAllKeys(a,b)"
  prim__getAllKeys :  IDBObjectStore
                   -> UndefOr AnyPtr
                   -> UndefOr Bits32
                   -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a)=>x.get(a)"
  prim__get : IDBObjectStore -> AnyPtr -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a)=>x.getKey(a)"
  prim__getKey : IDBObjectStore -> AnyPtr -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a)=>x.index(a)"
  prim__index : IDBObjectStore -> String -> PrimIO IDBIndex

  export
  %foreign "browser:lambda:(x,a,b)=>x.openCursor(a,b)"
  prim__openCursor :  IDBObjectStore
                   -> UndefOr AnyPtr
                   -> UndefOr String
                   -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a,b)=>x.openKeyCursor(a,b)"
  prim__openKeyCursor :  IDBObjectStore
                      -> UndefOr AnyPtr
                      -> UndefOr String
                      -> PrimIO IDBRequest

  export
  %foreign "browser:lambda:(x,a,b)=>x.put(a,b)"
  prim__put : IDBObjectStore -> AnyPtr -> UndefOr AnyPtr -> PrimIO IDBRequest

namespace IDBOpenDBRequest

  export
  %foreign "browser:lambda:x=>x.onblocked"
  prim__onblocked : IDBOpenDBRequest -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onblocked = v}"
  prim__setOnblocked :  IDBOpenDBRequest
                     -> Nullable EventHandlerNonNull
                     -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onupgradeneeded"
  prim__onupgradeneeded :  IDBOpenDBRequest
                        -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onupgradeneeded = v}"
  prim__setOnupgradeneeded :  IDBOpenDBRequest
                           -> Nullable EventHandlerNonNull
                           -> PrimIO ()

namespace IDBRequest

  export
  %foreign "browser:lambda:x=>x.error"
  prim__error : IDBRequest -> PrimIO (Nullable DOMException)

  export
  %foreign "browser:lambda:x=>x.onerror"
  prim__onerror : IDBRequest -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onerror = v}"
  prim__setOnerror : IDBRequest -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onsuccess"
  prim__onsuccess : IDBRequest -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onsuccess = v}"
  prim__setOnsuccess : IDBRequest -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.readyState"
  prim__readyState : IDBRequest -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.result"
  prim__result : IDBRequest -> PrimIO AnyPtr

  export
  %foreign "browser:lambda:x=>x.source"
  prim__source :  IDBRequest
               -> PrimIO (Nullable (Union3 IDBObjectStore IDBIndex IDBCursor))

  export
  %foreign "browser:lambda:x=>x.transaction"
  prim__transaction : IDBRequest -> PrimIO (Nullable IDBTransaction)

namespace IDBTransaction

  export
  %foreign "browser:lambda:x=>x.db"
  prim__db : IDBTransaction -> PrimIO IDBDatabase

  export
  %foreign "browser:lambda:x=>x.durability"
  prim__durability : IDBTransaction -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.error"
  prim__error : IDBTransaction -> PrimIO (Nullable DOMException)

  export
  %foreign "browser:lambda:x=>x.mode"
  prim__mode : IDBTransaction -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.objectStoreNames"
  prim__objectStoreNames : IDBTransaction -> PrimIO DOMStringList

  export
  %foreign "browser:lambda:x=>x.onabort"
  prim__onabort : IDBTransaction -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onabort = v}"
  prim__setOnabort : IDBTransaction -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.oncomplete"
  prim__oncomplete : IDBTransaction -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.oncomplete = v}"
  prim__setOncomplete :  IDBTransaction
                      -> Nullable EventHandlerNonNull
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onerror"
  prim__onerror : IDBTransaction -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onerror = v}"
  prim__setOnerror : IDBTransaction -> Nullable EventHandlerNonNull -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.abort()"
  prim__abort : IDBTransaction -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.commit()"
  prim__commit : IDBTransaction -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.objectStore(a)"
  prim__objectStore : IDBTransaction -> String -> PrimIO IDBObjectStore

namespace IDBVersionChangeEvent

  export
  %foreign "browser:lambda:(a,b)=> new IDBVersionChangeEvent(a,b)"
  prim__new :  String
            -> UndefOr IDBVersionChangeEventInit
            -> PrimIO IDBVersionChangeEvent

  export
  %foreign "browser:lambda:x=>x.newVersion"
  prim__newVersion : IDBVersionChangeEvent -> PrimIO (Nullable JSBits64)

  export
  %foreign "browser:lambda:x=>x.oldVersion"
  prim__oldVersion : IDBVersionChangeEvent -> PrimIO JSBits64

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

namespace IDBDatabaseInfo

  export
  %foreign "browser:lambda:(a,b)=> ({name: a,version: b})"
  prim__new : UndefOr String -> UndefOr JSBits64 -> PrimIO IDBDatabaseInfo

  export
  %foreign "browser:lambda:x=>x.name"
  prim__name : IDBDatabaseInfo -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.name = v}"
  prim__setName : IDBDatabaseInfo -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.version"
  prim__version : IDBDatabaseInfo -> PrimIO (UndefOr JSBits64)

  export
  %foreign "browser:lambda:(x,v)=>{x.version = v}"
  prim__setVersion : IDBDatabaseInfo -> UndefOr JSBits64 -> PrimIO ()

namespace IDBIndexParameters

  export
  %foreign "browser:lambda:(a,b)=> ({unique: a,multiEntry: b})"
  prim__new : UndefOr Boolean -> UndefOr Boolean -> PrimIO IDBIndexParameters

  export
  %foreign "browser:lambda:x=>x.multiEntry"
  prim__multiEntry : IDBIndexParameters -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.multiEntry = v}"
  prim__setMultiEntry : IDBIndexParameters -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.unique"
  prim__unique : IDBIndexParameters -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.unique = v}"
  prim__setUnique : IDBIndexParameters -> UndefOr Boolean -> PrimIO ()

namespace IDBObjectStoreParameters

  export
  %foreign "browser:lambda:(a,b)=> ({keyPath: a,autoIncrement: b})"
  prim__new :  UndefOr (Nullable (Union2 String (Array String)))
            -> UndefOr Boolean
            -> PrimIO IDBObjectStoreParameters

  export
  %foreign "browser:lambda:x=>x.autoIncrement"
  prim__autoIncrement : IDBObjectStoreParameters -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.autoIncrement = v}"
  prim__setAutoIncrement :  IDBObjectStoreParameters
                         -> UndefOr Boolean
                         -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.keyPath"
  prim__keyPath :  IDBObjectStoreParameters
                -> PrimIO (UndefOr (Nullable (Union2 String (Array String))))

  export
  %foreign "browser:lambda:(x,v)=>{x.keyPath = v}"
  prim__setKeyPath :  IDBObjectStoreParameters
                   -> UndefOr (Nullable (Union2 String (Array String)))
                   -> PrimIO ()

namespace IDBTransactionOptions

  export
  %foreign "browser:lambda:(a)=> ({durability: a})"
  prim__new : UndefOr String -> PrimIO IDBTransactionOptions

  export
  %foreign "browser:lambda:x=>x.durability"
  prim__durability : IDBTransactionOptions -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.durability = v}"
  prim__setDurability : IDBTransactionOptions -> UndefOr String -> PrimIO ()

namespace IDBVersionChangeEventInit

  export
  %foreign "browser:lambda:(a,b)=> ({oldVersion: a,newVersion: b})"
  prim__new :  UndefOr JSBits64
            -> UndefOr (Nullable JSBits64)
            -> PrimIO IDBVersionChangeEventInit

  export
  %foreign "browser:lambda:x=>x.newVersion"
  prim__newVersion :  IDBVersionChangeEventInit
                   -> PrimIO (UndefOr (Nullable JSBits64))

  export
  %foreign "browser:lambda:(x,v)=>{x.newVersion = v}"
  prim__setNewVersion :  IDBVersionChangeEventInit
                      -> UndefOr (Nullable JSBits64)
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.oldVersion"
  prim__oldVersion : IDBVersionChangeEventInit -> PrimIO (UndefOr JSBits64)

  export
  %foreign "browser:lambda:(x,v)=>{x.oldVersion = v}"
  prim__setOldVersion :  IDBVersionChangeEventInit
                      -> UndefOr JSBits64
                      -> PrimIO ()


text:
module DataTypes

import Ratio
import Data.Complex
import Control.ST.Exception
import Control.ST
import Environment
import ParserCombinator

%access public export

data Arity =
    Min Int
  | MinMax Int Int

mutual
    PrimitiveLispFunc : Type
    PrimitiveLispFunc = List LispVal -> ThrowsError LispVal

    ThrowsError : Type -> Type
    ThrowsError = Either LispError

    codata LispVal =
        LispVector Int (List LispVal) -- TODO: Array?
      | LispAtom String
      | LispList (List LispVal)
      | LispDottedList (List LispVal) LispVal
      | LispInteger Integer
      | LispFloat Double
      | LispComplex (Complex Double)
      | LispRational Rational
      | LispString String
      | LispCharacter Char
      | LispBool Bool
      | LispPrimitiveFunc String PrimitiveLispFunc
      | LispFunc String (List String) (Maybe String) (List LispVal) (EnvRef LispVal)
      | LispVoid

    data LispError = NumArgs Arity Integer (List LispVal)
        | TypeMismatch String LispVal
        | BadSpecialForm String LispVal
        | NotFunction String String
        | UnboundVar String String
        | LispParseError String Pos
        | Default String

mutual
  listEq : List LispVal -> List LispVal -> Bool
  listEq [] [] = True
  listEq (x::xs) (y::ys) = if x == y then listEq xs ys else False
  listEq _ _ = False

  Eq LispVal where
    (LispVector n a) == (LispVector m b) = if n == m then False else listEq a b
    (LispAtom a) == (LispAtom b) = a == b
    (LispList a) == (LispList b) = listEq a b
    (LispDottedList xs v1) == (LispDottedList ys v2) = if v1 == v2 then False else listEq xs ys
    (LispInteger n) == (LispInteger m) = n == m
    (LispFloat n) == (LispFloat m) = n == m
    (LispComplex n) == (LispComplex m) = n == m
    (LispRational n) == (LispRational m) = n == m
    (LispString a) == (LispString b) = a == b
    (LispCharacter a) == (LispCharacter b) = a == b
    (LispBool a) == (LispBool b) = a == b
    LispVoid == LispVoid = True
    -- LispPrimitiveFunc String PrimitiveLispFunc
    -- LispFunc String (List String) (Maybe String) (List LispVal) (EnvRef LispVal)
    x == y = False

interface (Exception m LispError, ConsoleIO m, Envir LispVal m) =>
          Context (m : Type -> Type) where

(Exception m LispError, ConsoleIO m, Envir LispVal m) => Context m where

mutual
    unwordsList : List LispVal -> String
    unwordsList = unwords . map showVal

    showVal : LispVal -> String
    showVal (LispString contents) = "\"" ++ contents ++ "\""
    showVal (LispAtom name') = name'
    showVal (LispInteger contents) = show contents
    showVal (LispFloat contents) = show contents
    showVal (LispComplex c) = show c
    showVal (LispRational (n .% d)) = show n++ "/" ++ show d
    showVal (LispBool True) = "#t"
    showVal (LispBool False) = "#f"
    showVal (LispList contents) = "(" ++ unwordsList contents ++ ")"
    showVal (LispVector n contents) = "#(" ++ unwordsList contents ++ ")"
    showVal (LispDottedList h t) = "(" ++ unwordsList h ++ " . " ++ showVal t ++ ")"
    showVal (LispFunc name _ _ _ _) = "#<procedure:" ++ name ++ ">"
    showVal LispVoid = ""
    showVal _ = ""

Show LispVal where
    show = showVal

showError : LispError -> String
showError (Default message) = message
showError (UnboundVar message varname) = message ++ ": " ++ varname
showError (BadSpecialForm message form) = message ++ ": " ++ (show form)
showError (NotFunction message func) = message ++ ": " ++ (show func)
showError (NumArgs expected found args) =
  let error' =
        case expected of
          Min min' =>
            "arity mismatch;\nthe expected number of arguments does not match the given number" ++
            "\nexpected: at least " ++ show min' ++ "\ngiven: " ++ show found
          MinMax min' max' =>
            "arity mismatch;\nthe expected number of arguments does not match the given number" ++
            "\nexpected: " ++
            (if min' == max'
               then show min'
               else "between " ++ show min' ++ " and " ++ show max') ++
            "\ngiven: " ++ show found
      argsError =
        case args of
          [] => ""
          a => "\narguments:\n" ++ unwordsList a
  in error' ++ argsError
showError (LispParseError parseErr pos) = "Parse error " ++ show pos
showError (TypeMismatch expected found) =
  "Invalid type: expected " ++ expected ++ ", found " ++ (show found)

Show LispError where
    show = showError

max_stars_repo_name: ebenpack/lidrisp

max_issues_repo_name: ebenpack/lidrisp

max_forks_repo_name: ebenpack/lidrisp


text:
module Main

import IdrisJvm.IO
import Java.Lang
import Java.Util
import Data.Vect

numTest : (Num a, Show a) => a -> a -> JVM_IO ()
numTest a b = do
  putStrLn $ show a ++ " + " ++ show b ++ " = " ++ show (a + b)
  putStrLn $ show a ++ " * " ++ show b ++ " = " ++ show (a * b)

integralTest : (Integral a, Show a) => a -> a -> JVM_IO ()
integralTest a b = do
  putStrLn $ show a ++ " div " ++ show b ++ " = " ++ show (a `div` b)
  -- putStrLn $ show a ++ " mod " ++ show b ++ " = " ++ show (a `mod` b) -- not working due to a defect in Idris portable codegen

fractionalTest : (Fractional a, Show a) => a -> a -> JVM_IO ()
fractionalTest a b = do
  putStrLn $ show a ++ " / " ++ show b ++ " = " ++ show (a / b)
  putStrLn $ "recip " ++ show a ++ " = " ++ show (recip a)
  putStrLn $ "recip " ++ show b ++ " = " ++ show (recip b)

showOrdering : Ordering -> String
showOrdering EQ = "EQ"
showOrdering LT = "LT"
showOrdering GT = "GT"

ordTest : (Ord a, Show a) => a -> a -> JVM_IO ()
ordTest a b = putStrLn $ "compare " ++ show a ++ " " ++ show b ++ " = " ++ showOrdering (compare a b)

int1 : Int
int1 = 2147483647

int2 : Int
int2 = -2147483648

int3 : Int
int3 = 4

integer1 : Integer
integer1 = 100000000000000009

integer2 : Integer
integer2 = 200000000000000008

bits8_1: Bits8
bits8_1 = 255

bits8_2: Bits8
bits8_2 = 255

bits16_1: Bits16
bits16_1 = 4097

bits16_2: Bits16
bits16_2 = 512

bits32_1: Bits32
bits32_1 = 8388608

bits32_2: Bits32
bits32_2 = 524288

bits64_1: Bits64
bits64_1 = 9223372036854775807

bits64_2: Bits64
bits64_2 = 281474976710656

double1 : Double
double1 = 24.234234

double2 : Double
double2 = 75676.23232

printHeader : String -> JVM_IO ()
printHeader header = do
  putStrLn ""
  putStrLn header
  putStrLn $ concat $ List.replicate (length header) "="

pythag : Int -> List (Int, Int, Int)
pythag max = [(x, y, z) | z <- [1..max], y <- [1..z], x <- [1..y],
                          x * x + y * y == z * z]

compareMaybe : (a, Maybe Int, b) -> (a, Maybe Int, b) -> Ordering
compareMaybe (_, Just c1, _) (_, Just c2, _) = compare c1 c2
compareMaybe (_, Just _, _) (_, Nothing, _)  = LT
compareMaybe (_, Nothing, _) (_, Just _, _)  = GT
compareMaybe _ _                             = EQ

maybeTest1 : Maybe String -> JVM_IO ()
maybeTest1 s = putStrLn (maybe "nothing" id s)

maybeTest2 : Maybe String -> JVM_IO ()
maybeTest2 Nothing = putStrLn "nothing"
maybeTest2 _       = putStrLn "just"

maybeTest3 : Maybe String -> JVM_IO ()
maybeTest3 (Just _) = putStrLn "just"
maybeTest3 _        = putStrLn "nothing"

main : JVM_IO ()
main = do
  print "Hello "
  putStrLn "world!"
  printHeader "numTest on Int"
  numTest int1 int2

  printHeader "numTest on Integer"
  numTest integer1 integer2

  printHeader "numTest on Bits8"
  numTest bits8_1 bits8_2

  printHeader "numTest on Bits16"
  numTest bits16_1 bits16_2

  printHeader "numTest on Bits32"
  numTest bits32_1 bits32_2

  printHeader "numTest on Bits64"
  numTest bits64_1 bits64_2

  printHeader "numTest on Double"
  numTest double1 double2

  printHeader "integralTest on Int"
  integralTest int1 int2

  printHeader "integralTest on Integer"
  integralTest integer1 integer2

  printHeader "integralTest on Bits8"
  integralTest bits8_1 bits8_2

  printHeader "integralTest on Bits16"
  integralTest bits16_1 bits16_2

  printHeader "integralTest on Bits32"
  integralTest bits32_1 bits32_2

  printHeader "integralTest on Bits64"
  integralTest bits64_1 bits64_2

  printHeader "fractionalTest on Double"
  fractionalTest double1 double2

  printHeader "ordTest on Int"
  ordTest int1 int2

  printHeader "ordTest on Integer"
  ordTest integer1 integer2

  printHeader "ordTest on Bits8"
  ordTest bits8_1 bits8_2

  printHeader "ordTest on Bits16"
  ordTest bits16_1 bits16_2

  printHeader "ordTest on Bits32"
  ordTest bits32_1 bits32_2

  printHeader "ordTest on Bits64"
  ordTest bits64_1 bits64_2

  printHeader "ordTest on Double"
  ordTest double1 double2

  putStrLn ""
  printLn $ pythag 50

  -- Array tests start
  printLn !(arrayToVect !(vectToArray ['d', 'c', 'a']))
  printLn !(arrayToVect !(vectToArray $ the (Vect _ Int) $ [3, 4, 5]))
  printLn !(arrayToVect !(vectToArray (the (Vect _ Bits8) [2, 4, 6, 5, 3])))
  printLn !(arrayToVect !(vectToArray (the (Vect _ Bits16) [5, 3])))
  printLn !(arrayToVect !(vectToArray (the (Vect _ Bits32) [2, 5, 3])))
  printLn !(arrayToVect !(vectToArray (the (Vect _ Bits64) [2, 4, 6, 5])))
  printLn !(arrayToVect !(vectToArray [Float 0.5, Float 2.0, Float 4.5]))
  printLn !(arrayToVect !(vectToArray [1.3, 1.5, 1.9, 2.5]))
  printLn !(arrayToVect !(vectToArray ["hello", "world", "!"]))

  marr <- newMultiArray (Int -> Int -> Int -> Int -> JVM_IO (JVM_Array (JVM_Array (JVM_Array (JVM_Array String))))) 3 2 2 4
  setArray (JVM_Array (JVM_Array (JVM_Array (JVM_Array String))) -> Int -> Int -> Int -> Int -> String -> JVM_IO ()) marr 0 0 0 3 "foo"
  printLn !(Arrays.deepToString marr)
  printLn !(getArray (JVM_Array (JVM_Array (JVM_Array (JVM_Array String))) -> Int -> Int -> Int -> Int -> JVM_IO String) marr 0 0 0 3)
  printLn !(arrayLength !(getArray (JVM_Array (JVM_Array (JVM_Array (JVM_Array String))) -> Int -> Int -> JVM_IO (JVM_Array (JVM_Array String))) marr 0 0))
  printLn !(arrayLength marr)

  vectArr2d <- vectToArray2d (the (Vect _ (Vect _ Int)) [[3, 33], [4, 44], [5, 55]])
  printLn !(Arrays.deepToString vectArr2d)
  -- Array tests end

  -- Maybe tests
  maybeTest1 (if Strings.length "foo" == 0 then Nothing else Just "foo")
  maybeTest2 (if Strings.length "" == 0 then Nothing else Just "foobar")
  maybeTest3 (if Strings.length "bar" == 0 then Nothing else Just "bar")
  printLn $ sortBy compareMaybe $ [("", Just 10, ""), ("", Just 23, ""), ("", Nothing, ""), ("", Just 15, "")]


text:
module Markdown.Parser

import Markdown.Lexer
import Markdown.Data
import Text.Parser
import Text.Token
import Data.List
import Data.List1

import public Markdown.Tokens

-- Note: this is currently infinitely recursive
-- %default total

mutual
  private
  markdown : Grammar _ MarkdownToken False Markdown
  markdown =
    do
      els <- many (
              (map Just header)
          <|> (map Just paragraph)
          <|> (map (const Nothing) $ newLine)
        )
      pure $ Doc (mapMaybe id els)

  private
  inline : Grammar _ MarkdownToken True Inline
  inline =
    (
          text
      <|> pre
      <|> codeBlock
      <|> bold
      <|> italics
      <|> image
      <|> link
      <|> html
      <|> parts
    )

  -- TODO: Handle other incomplete parts
  parts : Grammar _ MarkdownToken True Inline
  parts =
    map (const $ Text "!") (match ImageSym)

  wrapInline : MarkdownTokenKind -> (List Inline -> a) -> Grammar _ MarkdownToken True a
  wrapInline sym tok =
    do
      ignore $ match sym
      contents <- some inline
      ignore $ match sym
      pure $ tok (forget contents)

  private
  header : Grammar _ MarkdownToken True Block
  header =
    do
      level <- match HeadingSym
      commit -- TODO: Should we commit here?
      contents <- many inline
      blockTerminal
      pure $ Header level contents

  blockTerminal : Grammar _ MarkdownToken False ()
  blockTerminal =
    (map (const ()) $ (some newLine)) <|>
    eof

  private
  newLine : Grammar _ MarkdownToken True ()
  newLine =
    map (const ()) (match NewLine)

  private
  paragraph : Grammar _ MarkdownToken True Block
  paragraph =
    do
      contents <- some inline
      blockTerminal
      pure $ Paragraph (forget contents)

  private
  text : Grammar _ MarkdownToken True Inline
  text =
    map Text (match MdText)

  private
  pre : Grammar _ MarkdownToken True Inline
  pre =
    map Pre (match MdPre)

  private
  codeBlock : Grammar _ MarkdownToken True Inline
  codeBlock =
    map (uncurry CodeBlock) (match MdCodeBlock)

  private
  bold : Grammar _ MarkdownToken True Inline
  bold =
    wrapInline BoldSym Bold

  private
  italics : Grammar _ MarkdownToken True Inline
  italics =
    wrapInline ItalicsSym Italics

  private
  image : Grammar _ MarkdownToken True Inline
  image =
    do
      match ImageSym
      r <- match MdLink
      buildImage r

  private
  buildImage : (String, String) -> Grammar _ MarkdownToken False Inline
  buildImage (alt, src) =
    pure $ Image alt src

  private
  link : Grammar _ MarkdownToken True Inline
  link =
    map (\(href, desc) => Link href desc) (match MdLink)

  private
  html : Grammar _ MarkdownToken True Inline
  html =
    do
      openTag <- match HtmlOpenTag
      contents <- many inline
      closer openTag -- TODO: Is this inefficient?
      pure $ Html openTag contents

  private
  closer : String -> Grammar _ MarkdownToken True ()
  closer tag =
    do
      closeTag <- match HtmlCloseTag
      checkTag closeTag tag

  private
  checkTag : String -> String -> Grammar _ MarkdownToken False ()
  checkTag x y =
    if x == y
      then pure ()
      else fail "tag mismatch"

export
parseMarkdown : List (WithBounds MarkdownToken) -> Maybe Markdown
parseMarkdown toks = case parse markdown toks of
                      Right (j, []) => Just j
                      _ => Nothing

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo