text:
import IdrisJvm.IO
import IdrisJvm.System
import IdrisJvm.JvmImport
import Java.Lang
import Java.Util
import Java.Util.Function
import Data.Vect
import Mmhelloworld.IdrisSpringBoot.Boot
import Mmhelloworld.IdrisSpringBoot.Web.Bind.Annotation
import Mmhelloworld.IdrisSpringBoot.Context.Annotation
import Mmhelloworld.IdrisSpringBoot.Boot.Autoconfigure
import Mmhelloworld.IdrisSpringBoot.Context

%access public export

namespace BeanDefinitionCustomizer
    BeanDefinitionCustomizer : Type
    BeanDefinitionCustomizer = javaInterface "org/springframework/beans/factory/config/BeanDefinitionCustomizer"

namespace GenericApplicationContext
  GenericApplicationContext : Type
  GenericApplicationContext = javaClass "org/springframework/context/support/GenericApplicationContext"

  registerBean : GenericApplicationContext -> JClass -> Supplier -> JVM_Array BeanDefinitionCustomizer -> JVM_IO ()
  registerBean = invokeInstance "registerBean" (GenericApplicationContext -> JClass -> Supplier -> JVM_Array BeanDefinitionCustomizer -> JVM_IO ())

Inherits ConfigurableApplicationContext GenericApplicationContext where {}

namespace ApplicationContextInitializer
  ApplicationContextInitializer : Type
  ApplicationContextInitializer = javaInterface "org/springframework/context/ApplicationContextInitializer"

  %inline
  jlambda : (ConfigurableApplicationContext -> JVM_IO ()) -> ApplicationContextInitializer
  jlambda f = javalambda "initialize" (ConfigurableApplicationContext -> JVM_IO ()) g
    where
      g : ConfigurableApplicationContext -> ()
      g context = believe_me $ unsafePerformIO (f context)

namespace ApplicationArguments
    ApplicationArguments : Type
    ApplicationArguments = javaInterface "org/springframework/boot/ApplicationArguments"

namespace SpringApplicationBuilder
  SpringApplicationBuilder : Type
  SpringApplicationBuilder = javaClass "org/springframework/boot/builder/SpringApplicationBuilder"

  new : JVM_Array JClass -> JVM_IO SpringApplicationBuilder
  new = FFI.new (JVM_Array JClass -> JVM_IO SpringApplicationBuilder)

  initializers : SpringApplicationBuilder -> JVM_Array ApplicationContextInitializer -> JVM_IO SpringApplicationBuilder
  initializers = invokeInstance "initializers" (SpringApplicationBuilder -> JVM_Array ApplicationContextInitializer -> JVM_IO SpringApplicationBuilder)

  run : SpringApplicationBuilder -> StringArray -> JVM_IO ConfigurableApplicationContext
  run = invokeInstance "run" (SpringApplicationBuilder -> StringArray -> JVM_IO ConfigurableApplicationContext)

namespace ApplicationRunner
  ApplicationRunner : Type
  ApplicationRunner = javaInterface "org/springframework/boot/ApplicationRunner"

  clazz : JClass
  clazz = classLit "org/springframework/boot/ApplicationRunner"

  %inline
  jlambda : (ApplicationArguments -> JVM_IO ()) -> ApplicationRunner
  jlambda f = javalambda "run" (ApplicationArguments -> JVM_IO ()) g
    where
      g : ApplicationArguments -> ()
      g args = believe_me $ unsafePerformIO (f args)

namespace Publisher
    PublisherClass : JVM_NativeTy
    PublisherClass = Interface "org/reactivestreams/Publisher"

    Publisher : Type
    Publisher = javaInterface "org/reactivestreams/Publisher"

namespace Mono
    MonoClass : JVM_NativeTy
    MonoClass = Class "reactor/core/publisher/Mono"

    Mono : Type
    Mono = javaClass "reactor/core/publisher/Mono"

    just : a -> JVM_IO Mono
    just d = invokeStatic MonoClass "just" (Object -> JVM_IO Mono) $ believe_me d

MonoClass inherits PublisherClass

namespace ServerRequest
    ServerRequest : Type
    ServerRequest = javaInterface "org/springframework/web/reactive/function/server/ServerRequest"

namespace HandlerFunction
    HandlerFunction : Type
    HandlerFunction = javaInterface "org/springframework/web/reactive/function/server/HandlerFunction"

    %inline
    jlambda : (ServerRequest -> JVM_IO Mono) -> HandlerFunction
    jlambda f = javalambda "handle" (ServerRequest -> JVM_IO Mono) g
       where
         g : ServerRequest -> Mono
         g request = unsafePerformIO (f request)

namespace RequestPredicate
    RequestPredicate : Type
    RequestPredicate = javaInterface "org/springframework/web/reactive/function/server/RequestPredicate"

namespace RequestPredicates
    RequestPredicatesClass : JVM_NativeTy
    RequestPredicatesClass = Class "org/springframework/web/reactive/function/server/RequestPredicates"

    get : String -> JVM_IO RequestPredicate
    get = invokeStatic RequestPredicatesClass "GET" (String -> JVM_IO RequestPredicate)

namespace RouterFunction
    RouterFunctionClass : JVM_NativeTy
    RouterFunctionClass = Class "org/springframework/web/reactive/function/server/RouterFunction"

    RouterFunction : Type
    RouterFunction = javaInterface "org/springframework/web/reactive/function/server/RouterFunction"

    clazz : JClass
    clazz = classLit "org/springframework/web/reactive/function/server/RouterFunction"

namespace RouterFunctions
    RouterFunctionsClass : JVM_NativeTy
    RouterFunctionsClass = Class "org/springframework/web/reactive/function/server/RouterFunctions"

    route : RequestPredicate -> HandlerFunction -> JVM_IO RouterFunction
    route = invokeStatic RouterFunctionsClass "route" (RequestPredicate -> HandlerFunction -> JVM_IO RouterFunction)

namespace ServerResponse
    namespace BodyBuilder
        BodyBuilderClass : JVM_NativeTy
        BodyBuilderClass = Class "org/springframework/web/reactive/function/server/ServerResponse$BodyBuilder"

        BodyBuilder : Type
        BodyBuilder = javaInterface "org/springframework/web/reactive/function/server/ServerResponse$BodyBuilder"

        body : BodyBuilder -> Publisher -> JClass -> JVM_IO Mono
        body = invokeInstance "body" (BodyBuilder -> Publisher -> JClass -> JVM_IO Mono)

    ServerResponseClass : JVM_NativeTy
    ServerResponseClass = Interface "org/springframework/web/reactive/function/server/ServerResponse"

    ok : JVM_IO BodyBuilder
    ok = invokeStatic ServerResponseClass "ok" (JVM_IO BodyBuilder)

classWith : String
classWith = ""

ok : String -> JVM_IO Mono
ok str = body !ServerResponse.ok !(just str) (classLit "java/lang/String")

Bean : Type
Bean = ConfigurableApplicationContext -> JVM_IO ()

runner : (ApplicationArguments -> JVM_IO ()) -> Bean
runner f context = do
  let genericContext = the GenericApplicationContext (believe_me context)
  let beanSupplier = Supplier.jlambda $ pure (ApplicationRunner.jlambda f)
  noCustomizers <- newArray BeanDefinitionCustomizer 0
  registerBean genericContext ApplicationRunner.clazz beanSupplier noCustomizers

route : RequestPredicate -> (ServerRequest -> JVM_IO Mono) -> Bean
route requestPredicate f context = do
  let genericContext = the GenericApplicationContext (believe_me context)
  let beanSupplier = Supplier.jlambda $ RouterFunctions.route requestPredicate $ HandlerFunction.jlambda f
  noCustomizers <- newArray BeanDefinitionCustomizer 0
  registerBean genericContext RouterFunction.clazz beanSupplier noCustomizers

get : String -> (ServerRequest -> JVM_IO Mono) -> Bean
get pattern f context = do
  requestPredicate <- RequestPredicates.get pattern
  route requestPredicate f context

registerBeans : List Bean -> ConfigurableApplicationContext -> JVM_IO ()
registerBeans [] context = pure ()
registerBeans (bean :: beans) context = do
  bean context
  registerBeans beans context

runSpring : JClass -> List Bean -> StringArray -> JVM_IO ()
runSpring clazz beans args = do
  sources <- listToArray [clazz]
  appBuilder <- SpringApplicationBuilder.new sources
  let initializer = ApplicationContextInitializer.jlambda (registerBeans beans)
  _ <- initializers appBuilder !(listToArray [initializer])
  SpringApplicationBuilder.run appBuilder args
  pure ()

max_stars_repo_name: mmhelloworld/idris-spring-boot-example

max_issues_repo_name: mmhelloworld/idris-spring-boot-example

max_forks_repo_name: mmhelloworld/idris-spring-boot-example


text:
module Data.AVL.Core.API

import public Data.Tree
import public Data.AVL.Core

%default total
%access export

namespace AVL
  ||| Find a value in the tree.
  lookup : (Ord k) => k -> AVLTree h k v -> Maybe v
  lookup key (Element t _) = lookup' key t
    where
      lookup' : (Ord k) => k -> Tree k v -> Maybe v
      lookup' key Empty = Nothing
      lookup' key (Node key' value' l r) with (compare key key')
        lookup' key (Node key' value' l r) | LT = lookup' key l
        lookup' key (Node key' value' l r) | EQ = Just value'
        lookup' key (Node key' value' l r) | GT = lookup' key r

  ||| Update an element in the tree.
  update : (Ord k) => k
                   -> (v -> v)
                   -> AVLTree h k v
                   -> AVLTree h k v
  update key f t@(Element Empty inv) = t
  update key f (Element (Node key' value' l r) inv) with (compare key key')
      update key f (Element (Node key' value' l r) (AVLNode invl invr b)) | LT with (assert_total $ update key f (Element l invl)) -- Totality checker again
        update key f (Element (Node key' value' l r) (AVLNode invl invr b)) | LT | (Element l' invl')
                                                             = Element (Node key' value' l' r) (AVLNode invl' invr b)
      update key f (Element (Node key' value' l r) (AVLNode invl invr b)) | EQ
                                                             = Element (Node key' (f value') l r) (AVLNode invl invr b)
      update key f (Element (Node key' value' l r) (AVLNode invl invr b)) | GT with (assert_total $ update key f (Element r invr))
        update key f (Element (Node key' value' l r) (AVLNode invl invr b)) | GT | (Element r' invr')
                                                             = Element (Node key' value' l r') (AVLNode invl invr' b)

  ||| Perform a right fold over the tree.
  foldr : (step : k -> v -> p -> p)
       -> (init : p)
       -> AVLTree n k v
       -> p
  foldr step init (Element t _) = foldr' step init t
    where
      foldr' : (k -> v -> p -> p) -> p -> Tree k v -> p
      foldr' step' init' Empty = init'
      foldr' step' init' (Node key val l r) = foldr' step' (step' key val (foldr' step' init' r)) l

  ||| Construct a AVL Tree from an association list.
  fromList : (Ord k) => List (k, v)
                     -> (n : Nat ** AVLTree n k v)
  fromList [] = (0 ** Element Empty AVLEmpty)
  fromList ((k, v) :: xs) with (doInsert k v (snd (fromList xs)))
    fromList ((k, v) :: xs) | (Same x) = (_ ** x)
    fromList ((k, v) :: xs) | (Grew x) = (_ ** x)

  ||| Flatten the tree to an association list.
  toList : AVLTree n k v -> List (k, v)
  toList = foldr (\k,v,xs => (k, v) :: xs) []

  ||| Is the tree empty?
  isEmpty : AVLTree h k v -> Bool
  isEmpty (Element t _) = isEmpty' t
    where
      isEmpty' : Tree k v -> Bool
      isEmpty' Empty          = True
      isEmpty' (Node _ _ _ _) = False

  ||| Calculate the size of the tree.
  size : AVLTree h k v -> Nat
  size = foldr (\_,_=> S) 0

  ||| Return a list of keys in the tree.
  keys : AVLTree h k v -> List k
  keys = map fst . toList

  ||| Return a list of the values in the key.
  values : AVLTree h k v -> List v
  values = map snd . toList

  ||| Check if the provided check holds for all elements in the tree.
  all : (pred : k -> v -> Bool) ->  AVLTree h k v -> Bool
  all pred = foldr (\k,v,pred' => pred' && pred k v) True

  ||| Check if the provided check holds for at least one element in the tree.
  any : (pred : k -> v -> Bool) ->  AVLTree h k v -> Bool
  any pred = foldr (\k,v,pred' => pred' || pred k v) False

  ||| Does the given key exist in the tree?
  hasKey : (o : Ord k) => k -> AVLTree h k v -> Bool
  hasKey key = any (\key',value' => key == key')

  ||| Does the given value exist in the tree?
  hasValue : (Eq v) => v -> AVLTree h k v -> Bool
  hasValue value = any (\key',value' => value == value')

  ||| Find the first key that satisfies the provided predicate.
  findKey : (pred : v -> Bool) -> AVLTree h k v -> Maybe k
  findKey pred = foldr (\k,v,p => if pred v then Just k else p) Nothing

  ||| Find the key that is associated with provided value.
  findKeyOf : (Eq v) => v -> AVLTree h k v -> Maybe k
  findKeyOf value = findKey (== value)

  -- --------------------------------------------------------- [ Implementations ]

private
eqTree : (Eq k, Eq v) => Tree k v -> Tree k v -> Bool
eqTree Empty              Empty              = True
eqTree (Node xk xv xl xr) (Node yk yv yl yr) =
      xk == yk  &&
      xv == yv  &&
      eqTree xl yl &&
      eqTree xr yr
eqTree _ _                                   = False

(Eq k, Eq v) => Eq (Tree k v) where
  (==) = eqTree

(Eq k, Eq v) => Eq (AVLTree h k v) where
  (==) (Element t _) (Element t' _) = t == t'

(Show k, Show v) => Show (Tree k v) where
  show Empty          = ""
  show (Node k v l r) = unwords
      [
        "{"
      , show l
      , "(", show k, ":", show v, "),"
      , show r
      , "}"
      ]

(Show k, Show v) => Show (AVLTree h k v) where
  show (Element t _) = show t

ext: idr


text:
module Compiler.Erlang.Codegen.ErlExprToAbstractFormat.Buffer

import Compiler.Erlang.IR.AbstractFormat

%default total

genFunCall : Line -> String -> String -> List Expr -> Expr
genFunCall l modName fnName args =
  AEFunCall l (AERemoteRef l (AELiteral (ALAtom l modName)) (AELiteral (ALAtom l fnName))) args

emptyBinary : Line -> Expr
emptyBinary l = AEBitstring l []

zeroBinary : Line -> Expr
zeroBinary l = AEBitstring l [MkBitSegment l (AELiteral (ALInteger l 0)) ABSDefault (MkTSL Nothing Nothing Nothing Nothing)]

zeroPaddedBinary : Line -> (size : Expr) -> Expr
zeroPaddedBinary l size =
  genFunCall l "binary" "copy" [zeroBinary l, size]

export
binaryConcat : Line -> Expr -> Expr -> Expr
binaryConcat l bin1 bin2 =
  let binaryValue =
        AEBitstring l
          [ MkBitSegment l (AEVar l "Bin1") ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
          , MkBitSegment l (AEVar l "Bin2") ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
          ]
      funExpr = AEFun l 2
        [ MkFunClause l
            [ APVar l "Bin1"
            , APVar l "Bin2"
            ]
            []
            [ binaryValue
            ]
        ]
  in AEFunCall l funExpr [bin1, bin2]

export
bufferNew : Line -> (size : Expr) -> Expr
bufferNew l size =
  AETuple l [emptyBinary l, size]

export
bufferResize : Line -> (buf : Expr) -> (newSize : Expr) -> Expr
bufferResize l buf newSize =
  let extendedBody =
        [ AETuple l [AEVar l "Bin", AEVar l "NewSize"]
        ]
      shrinkedBinary = genFunCall l "binary" "part" [AEVar l "Bin", AELiteral (ALInteger l 0), AEVar l "NewSize"]
      shrinkedBody =
        [ AETuple l [shrinkedBinary, AEVar l "NewSize"]
        ]
      funExpr = AEFun l 2
        [ MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "NewSize"]
            [MkGuardAlt [AGOp l "=<" (AGFunCall l "byte_size" [AGVar l "Bin"]) (AGVar l "NewSize")]]
            extendedBody
        , MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "NewSize"]
            []
            shrinkedBody
        ]
  in AEFunCall l funExpr [buf, newSize]

export
bufferFlatten : Line -> (buf : Expr) -> (maxbytes : Expr) -> Expr
bufferFlatten l buf maxbytes =
  let paddingSize = AEOp l "-" (AEVar l "MaxBytes") (genFunCall l "erlang" "byte_size" [AEVar l "Bin"])
      paddedBinaryValue = AEBitstring l
        [ MkBitSegment l (AEVar l "Bin")     ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (AEVar l "Padding") ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        ]
      extendedBody =
        [ AEMatch l (APVar l "Padding") (zeroPaddedBinary l paddingSize)
        , AETuple l [paddedBinaryValue, AEVar l "BufSize"]
        ]
      shrinkedBinary = genFunCall l "binary" "part" [AEVar l "Bin", AELiteral (ALInteger l 0), AEVar l "BufSize"]
      shrinkedBody =
        [ AETuple l [shrinkedBinary, AEVar l "BufSize"]
        ]
      funExpr = AEFun l 2
        [ MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "MaxBytes"]
            [MkGuardAlt [AGOp l "=<" (AGFunCall l "byte_size" [AGVar l "Bin"]) (AGVar l "MaxBytes")]]
            extendedBody
        , MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "MaxBytes"]
            []
            shrinkedBody
        ]
  in AEFunCall l funExpr [buf, maxbytes]

-- Similar to the following Erlang code:
-- ```
-- buffer_set_byte(Bin, Loc, Value) when byte_size(Bin) =< Loc ->
--   Padding = binary:copy(<<0>>, Loc - byte_size(Bin)),
--   <<Bin/binary, Padding/binary, Value:8/integer>>;
-- buffer_set_byte(Bin, Loc, Value) ->
--   Padding = binary:copy(<<0>>, 1),
--   <<Start:Loc/binary, _:8/integer, End/binary>> = <<Bin/binary, Padding/binary>>,
--   <<Start/binary, Value:8/integer, End/binary>>.
-- ```
bufferSetGeneric : (targetTSL : TypeSpecifierList) -> (targetSize : Int) -> Line -> (buf : Expr) -> (loc : Expr) -> (value : Expr) -> Expr
bufferSetGeneric targetTSL targetSize l buf loc value =
  let binaryWithExtraPadding = AEBitstring l
        [ MkBitSegment l (AEVar l "Bin")     ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (AEVar l "Padding") ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        ]
      mutatedBinaryPattern = APBitstring l
        [ MkBitSegment l (ABPVar l "Start") (ABSVar l "Loc")                 (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (ABPUniversal l)   (ABSInteger l (cast targetSize)) targetTSL
        , MkBitSegment l (ABPVar l "End")   ABSDefault                       (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        ]
      mutatedBinaryValue = AEBitstring l
        [ MkBitSegment l (AEVar l "Start") ABSDefault                       (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (AEVar l "Value") (ABSInteger l (cast targetSize)) targetTSL
        , MkBitSegment l (AEVar l "End")   ABSDefault                       (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        ]
      targetSizeInBytes = AEOp l "div" (AELiteral (ALInteger l (cast targetSize))) (AELiteral (ALInteger l 8))
      mutatedBody =
        [ AEMatch l (APVar l "Padding") (zeroPaddedBinary l targetSizeInBytes)
        , AEMatch l mutatedBinaryPattern binaryWithExtraPadding
        , AETuple l [mutatedBinaryValue, AEVar l "BufSize"]
        ]
      paddingSize = AEOp l "-" (AEVar l "Loc") (genFunCall l "erlang" "byte_size" [AEVar l "Bin"])
      extendedBinaryValue =
        AEBitstring l
          [ MkBitSegment l (AEVar l "Bin")     ABSDefault                       (MkTSL Nothing Nothing (Just ABBinary) Nothing)
          , MkBitSegment l (AEVar l "Padding") ABSDefault                       (MkTSL Nothing Nothing (Just ABBinary) Nothing)
          , MkBitSegment l (AEVar l "Value")   (ABSInteger l (cast targetSize)) targetTSL
          ]
      extendedBody =
        [ AEMatch l (APVar l "Padding") (zeroPaddedBinary l paddingSize)
        , AETuple l [extendedBinaryValue, AEVar l "BufSize"]
        ]
      funExpr = AEFun l 3
        [ MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Value"]
            [MkGuardAlt [AGOp l "=<" (AGFunCall l "byte_size" [AGVar l "Bin"]) (AGVar l "Loc")]]
            extendedBody
        , MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Value"]
            []
            mutatedBody
        ]
  in AEFunCall l funExpr [buf, loc, value]

-- Similar to the following Erlang code:
-- ```
-- buffer_get_byte(Bin, Loc) when Loc + 1 =< byte_size(Bin) ->
--   <<_Start:Loc/binary, Value:8/integer, _End/binary>> = Bin,
--   Value.
-- buffer_get_byte(Bin, Loc) ->
--   0.
-- ```
bufferGetGeneric : (targetTSL : TypeSpecifierList) -> (targetSize : Int) -> (defaultValue : Expr) -> Line -> (buf : Expr) -> (loc : Expr) -> Expr
bufferGetGeneric targetTSL targetSize defaultValue l buf loc =
  let binaryPattern = APBitstring l
        [ MkBitSegment l (ABPUniversal l)   (ABSVar l "Loc")                 (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (ABPVar l "Value") (ABSInteger l (cast targetSize)) targetTSL
        , MkBitSegment l (ABPUniversal l)   ABSDefault                       (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        ]
      body =
        [ AEMatch l binaryPattern (AEVar l "Bin")
        , AEVar l "Value"
        ]
      targetSizeInBytes = AGOp l "div" (AGLiteral (ALInteger l (cast targetSize))) (AGLiteral (ALInteger l 8))
      funExpr = AEFun l 2
        [ MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc"]
            [MkGuardAlt [AGOp l "=<" (AGOp l "+" (AGVar l "Loc") targetSizeInBytes) (AGFunCall l "byte_size" [AGVar l "Bin"])]]
            body
        , MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc"]
            []
            [defaultValue]
        ]
  in AEFunCall l funExpr [buf, loc]

export
bufferSetUnsignedInt : (size : Int) -> Line -> (buf : Expr) -> (loc : Expr) -> (value : Expr) -> Expr
bufferSetUnsignedInt = bufferSetGeneric (MkTSL (Just ABUnsigned) (Just ABNative) (Just ABInteger) Nothing)

export
bufferGetUnsignedInt : (size : Int) -> Line -> (buf : Expr) -> (loc : Expr) -> Expr
bufferGetUnsignedInt size l = bufferGetGeneric (MkTSL (Just ABUnsigned) (Just ABNative) (Just ABInteger) Nothing) size (AELiteral (ALInteger l 0)) l

export
bufferSetSignedInt : (size : Int) -> Line -> (buf : Expr) -> (loc : Expr) -> (value : Expr) -> Expr
bufferSetSignedInt = bufferSetGeneric (MkTSL (Just ABSigned) (Just ABNative) (Just ABInteger) Nothing)

export
bufferGetSignedInt : (size : Int) -> Line -> (buf : Expr) -> (loc : Expr) -> Expr
bufferGetSignedInt size l = bufferGetGeneric (MkTSL (Just ABSigned) (Just ABNative) (Just ABInteger) Nothing) size (AELiteral (ALInteger l 0)) l

export
bufferSetDouble : Line -> (buf : Expr) -> (loc : Expr) -> (value : Expr) -> Expr
bufferSetDouble = bufferSetGeneric (MkTSL Nothing (Just ABNative) (Just ABFloat) Nothing) 64

export
bufferGetDouble : Line -> (buf : Expr) -> (loc : Expr) -> Expr
bufferGetDouble l = bufferGetGeneric (MkTSL Nothing (Just ABNative) (Just ABFloat) Nothing) 64 (AELiteral (ALFloat l 0)) l

-- Similar to the following Erlang code:
-- ```
-- buffer_set_string(Bin, Loc, Value) when byte_size(Bin) =< Loc ->
--   Padding = binary:copy(<<0>>, Loc - byte_size(Bin)),
--   <<Bin/binary, Padding/binary, Value/binary>>;
-- buffer_set_string(Bin, Loc, Value) ->
--   Size = erlang:byte_size(Value),
--   Padding = binary:copy(<<0>>, Size),
--   <<Start:Loc/binary, _:Size/binary, End/binary>> = <<Bin/binary, Padding/binary>>,
--   <<Start/binary, Value/binary, End/binary>>.
-- ```
export
bufferSetString : Line -> (buf : Expr) -> (loc : Expr) -> (value : Expr) -> Expr
bufferSetString l buf loc value =
  let binaryWithExtraPadding = AEBitstring l
        [ MkBitSegment l (AEVar l "Bin")     ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (AEVar l "Padding") ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        ]
      mutatedBinaryPattern = APBitstring l
        [ MkBitSegment l (ABPVar l "Start") (ABSVar l "Loc")  (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (ABPUniversal l)   (ABSVar l "Size") (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (ABPVar l "End")   ABSDefault        (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        ]
      mutatedBinaryValue = AEBitstring l
        [ MkBitSegment l (AEVar l "Start") ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (AEVar l "Value") ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (AEVar l "End")   ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        ]
      mutatedBody =
        [ AEMatch l (APVar l "Size") (genFunCall l "erlang" "byte_size" [AEVar l "Value"])
        , AEMatch l (APVar l "Padding") (zeroPaddedBinary l (AEVar l "Size"))
        , AEMatch l mutatedBinaryPattern binaryWithExtraPadding
        , AETuple l [mutatedBinaryValue, AEVar l "BufSize"]
        ]
      paddingSize = AEOp l "-" (AEVar l "Loc") (genFunCall l "erlang" "byte_size" [AEVar l "Bin"])
      extendedBinaryValue =
        AEBitstring l
          [ MkBitSegment l (AEVar l "Bin")     ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
          , MkBitSegment l (AEVar l "Padding") ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
          , MkBitSegment l (AEVar l "Value")   ABSDefault (MkTSL Nothing Nothing (Just ABBinary) Nothing)
          ]
      extendedBody =
        [ AEMatch l (APVar l "Padding") (zeroPaddedBinary l paddingSize)
        , AETuple l [extendedBinaryValue, AEVar l "BufSize"]
        ]
      funExpr = AEFun l 3
        [ MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Value"]
            [MkGuardAlt [AGOp l "=<" (AGFunCall l "byte_size" [AGVar l "Bin"]) (AGVar l "Loc")]]
            extendedBody
        , MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Value"]
            []
            mutatedBody
        ]
  in AEFunCall l funExpr [buf, loc, value]

-- Similar to the following Erlang code:
-- ```
-- buffer_get_string(Bin, Loc, Len) when Loc + Len =< byte_size(Bin) ->
--   <<_Start:Loc/binary, Value:Len/binary, _End/binary>> = Bin,
--   Value.
-- buffer_get_string(Bin, Loc, Len) ->
--   binary:copy(<<0>>, Len).
-- ```
export
bufferGetString : Line -> (buf : Expr) -> (loc : Expr) -> (len : Expr) -> Expr
bufferGetString l buf loc len =
  let binaryPattern = APBitstring l
        [ MkBitSegment l (ABPUniversal l)   (ABSVar l "Loc") (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (ABPVar l "Value") (ABSVar l "Len") (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        , MkBitSegment l (ABPUniversal l)   ABSDefault       (MkTSL Nothing Nothing (Just ABBinary) Nothing)
        ]
      body =
        [ AEMatch l binaryPattern (AEVar l "Bin")
        , AEVar l "Value"
        ]
      defaultBody =
        [ zeroPaddedBinary l (AEVar l "Len")
        ]
      funExpr = AEFun l 3
        [ MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Len"]
            [MkGuardAlt [AGOp l "=<" (AGOp l "+" (AGVar l "Loc") (AGVar l "Len")) (AGFunCall l "byte_size" [AGVar l "Bin"])]]
            body
        , MkFunClause l
            [APTuple l [APVar l "Bin", APVar l "BufSize"], APVar l "Loc", APVar l "Len"]
            []
            defaultBody
        ]
  in AEFunCall l funExpr [buf, loc, len]


text:
module Typing.Equate

import Typing.Common
import Typing.Util

-- 8YYYY _YYY_ 0   0  o8o  YY8YY Y8Y _YYY_ 8o  0
-- 8___  0 _ 8 0   0 8   8   0    0  0   0 8Yo 8
-- 8"""  0 "%8 0   0 8YYY8   0    0  0   0 8 Yo8
-- 8oooo "oooo "ooo" 0   0   0   o8o "ooo" 0   8

infix 4 ~~
public export
data Equation = (~~) Term Term

-- _YYY_  oYYo  oYYo 0   0 8YYYo oYYYo
-- 0   0 0   " 0   " 0   0 8___P %___
-- 0   0 0   , 0   , 0   0 8""Yo `"""p
-- "ooo"  YooY  YooY "ooo" 0   0 YoooY

export
occurs : MetaVar -> Term -> Bool
occurs x (Meta y)         = x == y
occurs _ (Var _)          = False
occurs _ (DottedVar _ _)  = False
occurs _ (AbsoluteDottedVar _ _)
                          = False
occurs x (Ann m t)        = occurs x m || occurs x t
occurs _ Star             = False
occurs x (Pi _ a sc)      = occurs x a || occurs x (descope (Var . Name) sc)
occurs x (Lam _ sc)       = occurs x (descope (Var . Name) sc)
occurs x (App _ f a)      = occurs x f || occurs x a
occurs x (Con _ as)       = any (occurs x . snd) as
occurs x (Case as mot cs) = any (occurs x) as || occursCaseMotive mot || any occursClause cs
where
	occursCaseMotive : CaseMotive -> Bool
	occursClause : Clause -> Bool
	occursPattern : Pattern -> Bool

	occursCaseMotive (CaseMotiveNil m) = occurs x m
	occursCaseMotive (CaseMotiveCons a sc)
		= occurs x a || occursCaseMotive (descope (Var . Name) sc)

	occursClause (NewClause psc sc) = any occursPattern (descope Name psc) || occurs x (descope (Var . Name) sc)

	occursPattern (VarPat _) = False
	occursPattern (ConPat _ xs) = any (occursPattern . snd) xs
	occursPattern (AssertionPat m) = occurs x m
	occursPattern MakeMeta = False
occurs x (RecordType tele)  = occursTelescope tele
where
	occursTelescope : Telescope -> Bool
	occursTelescope TelescopeNil = False
	occursTelescope (TelescopeCons t sc) = occurs x t || occursTelescope (descope (Var . Name) sc)
occurs x (RecordCon fields) = any (occurs x . snd) fields
occurs x (Project m _)    = occurs x m

export
evalWithSubs : Substitution -> Equation -> TypeChecker Equation
evalWithSubs subs (l ~~ r) = do
	l' <- evaluate (instantiateMetas subs l)
	r' <- evaluate (instantiateMetas subs r)
	pure (l' ~~ r')

--  oYYo _YYY_ 8_   _8 8YYYo  o8o  8YYYo 8YYYY  oYYo  o8o  oYYYo 8YYYY 8_   _8 _YYY_ YY8YY Y8Y 0   0 8YYYY
-- 0   " 0   0 8"o_o"8 8___P 8   8 8___P 8___  0   " 8   8 %___  8___  8"o_o"8 0   0   0    0  0   0 8___
-- 0   , 0   0 0  8  0 8"""  8YYY8 8""Yo 8"""  0   , 8YYY8 `"""p 8"""  0  8  0 0   0   0    0  "o o" 8"""
--  YooY "ooo" 0     0 0     0   0 0   0 8oooo  YooY 0   0 YoooY 8oooo 0     0 "ooo"   0   o8o  "8"  8oooo

export
compareCaseMotive : CaseMotive -> CaseMotive -> TypeChecker (List Equation)
compareCaseMotive (CaseMotiveNil a1) (CaseMotiveNil a2) = pure [(a1 ~~ a2)]
compareCaseMotive (CaseMotiveCons a1 sc1) (CaseMotiveCons a2 sc2) = do
	i <- newName {s=TCState}
	case (head' (names sc1), head' (names sc2)) of
		(Just h1, Just h2) => do
			reqs <- compareCaseMotive
				(instantiate sc1 [Var (Generated h1 i)])
				(instantiate sc2 [Var (Generated h2 i)])
			pure ((a1 ~~ a2) :: reqs)
		_ => throw "Should not happen"
compareCaseMotive mot mot' = throw $ "Motives not equal: " ++ show mot ++ " and " ++ show mot'

--  oYYo _YYY_ 8_   _8 8YYYo  o8o  8YYYo 8YYYY     oYYo 0     o8o  0   0 oYYYo 8YYYY
-- 0   " 0   0 8"o_o"8 8___P 8   8 8___P 8___     0   " 0    8   8 0   0 %___  8___
-- 0   , 0   0 0  8  0 8"""  8YYY8 8""Yo 8"""     0   , 0    8YYY8 0   0 `"""p 8"""
--  YooY "ooo" 0     0 0     0   0 0   0 8oooo     YooY 8ooo 0   0 "ooo" YoooY 8oooo

export
compareClauses : List Clause -> List Clause -> TypeChecker (List Equation)
export
comparePattern : Pattern -> Pattern -> TypeChecker (List Equation)
export
comparePatterns : List (Plict,Pattern) -> List (Plict,Pattern) -> TypeChecker (List Equation)

compareClauses [] [] = pure []
compareClauses (NewClause psc1 sc1::cs1) (NewClause psc2 sc2::cs2) = do
	unless (length (names psc1) == length (names psc2))
		$ throw "Patterns bind different numbers of arguments."
	is <- replicateM (length (names psc1)) $ newName
	let xs1 = zipWith Generated (names psc1) is
	let xs1' = map Var (removeByDummies (names psc1) xs1)
	let xs2 = zipWith Generated (names psc2) is
	let xs2' = map Var (removeByDummies (names psc2) xs2)
	reqss <- zipWithM comparePattern (instantiate psc1 xs1) (instantiate psc2 xs2)
	reqs' <- compareClauses cs1 cs2
	pure ((instantiate sc1 xs1' ~~ instantiate sc2 xs2') :: concat reqss ++ reqs')
compareClauses _ _ = throw $ "Mismatching number of clauses."

comparePattern (VarPat x) (VarPat x') = do
	unless (x == x')
		$ throw $ "Variable patters not equal: " ++ show x ++ " and " ++ show x'
	pure []
comparePattern (ConPat c ps) (ConPat c' ps') with (c == c')
	| True  = comparePatterns ps ps'
	| False = throw $ "Mismatching constructors " ++ show c ++ " and " ++ show c'
comparePattern _ _ = throw "Patterns not equal."

comparePatterns [] [] = pure []
comparePatterns ((plic1,p1)::ps1) ((plic2,p2)::ps2) = do
	unless (plic1 == plic2)
		$ throw "Mismatched plicities when trying to unify constructor sequences."
	eqs <- comparePattern p1 p2
	eqs' <- comparePatterns ps1 ps2
	pure $ eqs ++ eqs'
comparePatterns _ _ = throw "Patterns not equal."

--  oYYo _YYY_ 8_   _8 8YYYo  o8o  8YYYo 8YYYY YY8YY 8YYYY 0    8YYYY oYYYo  oYYo _YYY_ 8YYYo 8YYYY
-- 0   " 0   0 8"o_o"8 8___P 8   8 8___P 8___    0   8___  0    8___  %___  0   " 0   0 8___P 8___
-- 0   , 0   0 0  8  0 8"""  8YYY8 8""Yo 8"""    0   8"""  0    8"""  `"""p 0   , 0   0 8"""  8"""
--  YooY "ooo" 0     0 0     0   0 0   0 8oooo   0   8oooo 8ooo 8oooo YoooY  YooY "ooo" 0     8oooo

export
compareTelescope : Telescope -> Telescope -> TypeChecker (List Equation)
compareTelescope TelescopeNil TelescopeNil = pure []
compareTelescope (TelescopeCons t1 sc1) (TelescopeCons t2 sc2) = do
	unless (names sc1 == names sc2)
		$ throw $ "Mismatching record field names: " ++ unwords (names sc1) ++ " and " ++ unwords (names sc2)
	eqs' <- compareTelescope (descope (Var . Name) sc1) (descope (Var . Name) sc2)
	pure ((t1 ~~ t2) :: eqs')
compareTelescope _ _ = throw "Mismatched number of record fields."

--  oYYo _YYY_ 8_   _8 8YYYo  o8o  8YYYo 8YYYY 8YYYY Y8Y 8YYYY 0    8888_ oYYYo
-- 0   " 0   0 8"o_o"8 8___P 8   8 8___P 8___  8___   0  8___  0    0   0 %___
-- 0   , 0   0 0  8  0 8"""  8YYY8 8""Yo 8"""  8"""   0  8"""  0    0   0 `"""p
--  YooY "ooo" 0     0 0     0   0 0   0 8oooo 0     o8o 8oooo 8ooo 8oooY YoooY

export
compareFields : List (String,Term) -> List (String,Term) -> TypeChecker (List Equation)
compareFields [] [] = pure []
compareFields (_ :: _) [] = throw "Mismatching number of record fields."
compareFields [] (_ :: _) = throw "Mismatching number of record fields."
compareFields ((x,m)::xms) xms' = case extract (\(x',_) => x == x') xms' of
	Nothing      => throw "Mismatching record field names."
	Just ((_,m'),xms'') => do
		eqs' <- compareFields xms xms''
		pure ((m ~~ m') :: eqs')

-- 8YYYY _YYY_ 0   0  o8o  YY8YY 8YYYY
-- 8___  0 _ 8 0   0 8   8   0   8___
-- 8"""  0 "%8 0   0 8YYY8   0   8"""
-- 8oooo "oooo "ooo" 0   0   0   8oooo

export
equate : List Equation -> Substitution -> TypeChecker ()
equate eqs0 subs = go eqs0
where
	go : List Equation -> TypeChecker ()

	go [] = pure ()

	go ((Meta x ~~ Meta y) :: eqs) with (x == y)
		| True = go eqs
		| False = do
			eqs' <- traverse (evalWithSubs subs) eqs
			go eqs'

	go ((Meta x ~~ t2) :: eqs) = do
		unless (not (occurs x t2))
			$ throw $ "Cannot unify because " ++ show (Meta x)
				++ " occurs in " ++ show t2
		eqs' <- traverse (evalWithSubs subs) eqs
		go eqs'

	go ((t1 ~~ Meta y) :: eqs) = do
		unless (not (occurs y t1))
			$ throw $ "Cannot unify because " ++ show (Meta y)
				++ " occurs in " ++ show t1
		eqs' <- traverse (evalWithSubs subs) eqs
		go eqs'

	go ((Var x ~~ Var y) :: eqs) = do
		unless (x == y)
			$ throw $ "Cannot unify variables " ++ show (Var x)
				++ " and " ++ show (Var y)
		go eqs

	go ((DottedVar m1 x1 ~~ DottedVar m2 x2) :: eqs) = do
		unless (m1 == m2 && x1 == x2)
			$ throw $ "Cannot unify symbols " ++ show (DottedVar m1 x1)
				++ " and " ++ show (DottedVar m2 x2)
		go eqs

	go ((AbsoluteDottedVar m1 x1 ~~ AbsoluteDottedVar m2 x2) :: eqs) = do
		unless (m1 == m2 && x1 == x2)
			$ throw $ "Cannot unify symbols " ++ show (AbsoluteDottedVar m1 x1)
				++ " and " ++ show (AbsoluteDottedVar m2 x2)
		go eqs

	go ((Ann m1 t1 ~~ Ann m2 t2) :: eqs) = go ((m1 ~~ m2) :: (t1 ~~ t2) :: eqs)

	go ((Star ~~ Star) :: eqs) = go eqs

	go ((Pi plic1 a1 sc1 ~~ Pi plic2 a2 sc2) :: eqs) = do
		unless (plic1 == plic2)
			$ throw $ "Mismatched plicities when trying to unify "
						++ show (Pi plic1 a1 sc1) ++ " with "
						++ show (Pi plic2 a2 sc2)
		i <- newName
		case (head' (names sc1), head' (names sc2)) of
			(Just h1, Just h2) => do
				let b1 = instantiate sc1 [Var (Generated h1 i)]
				let b2 = instantiate sc2 [Var (Generated h2 i)]
				go ((a1 ~~ a2) :: (b1 ~~ b2) :: eqs)
			_ => throw "should not happen"

	go ((Lam plic1 sc1 ~~ Lam plic2 sc2) :: eqs) = do
		unless (plic1 == plic2)
			$ throw $ "Mismatched plicities when trying to unify "
						++ show (Lam plic1 sc1) ++ " with "
						++ show (Lam plic2 sc2)
		i <- newName
		case (head' (names sc1), head' (names sc2)) of
			(Just h1, Just h2) => do
				let b1 = instantiate sc1 [Var (Generated h1 i)]
				let b2 = instantiate sc2 [Var (Generated h2 i)]
				go ((b1 ~~ b2) :: eqs)
			_ => throw "should not happen"

	go ((App plic1 f1 a1 ~~ App plic2 f2 a2) :: eqs) = do
		unless (plic1 == plic2)
			$ throw $ "Mismatched plicities when trying to unify "
						++ show (App plic1 f1 a1) ++ " with "
						++ show (App plic2 f2 a2)
		go ((f1 ~~ f2) :: (a1 ~~ a2) :: eqs)

	go ((Con c1 as1 ~~ Con c2 as2) :: eqs) = do
		unless (c1 == c2) $ throw $ "Mismatching constructors " ++ show c1 ++ " and " ++ show c2
		unless (length as1 == length as2) $ throw $ "Mismatching number of arguments in "
			++ show (Con c1 as1) ++ " and "
			++ show (Con c2 as2)
		eqs' <- zipConArgs as1 as2
		go (eqs' ++ eqs)
	where
		zipConArgs : List (Plict, Term) -> List (Plict, Term) -> TypeChecker (List Equation)
		zipConArgs [] [] = pure []
		zipConArgs ((plic1',a1')::as1') ((plic2',a2')::as2') = if plic1' == plic2'
				then do
					eqs' <- zipConArgs as1' as2'
					pure $ (a1' ~~ a2') :: eqs'
				else
					throw "Mismatching plicity."
		zipConArgs _ _ = throw "Mismatching number of arguments."

	go ((Case as1 mot1 cs1 ~~ Case as2 mot2 cs2) :: eqs) = do
		unless(length as1 == length as2)
			$ throw $ "Mismatching number of case arguments in "
						++ show (Case as1 mot1 cs1) ++ " and "
						++ show (Case as2 mot2 cs2)
		unless (length cs1 == length cs2)
			$ throw $ "Mismatching number of clauses in "
						++ show (Case as1 mot1 cs1) ++ " and "
						++ show (Case as2 mot2 cs2)
		let argEqs = zipWith (~~) as1 as2
		motEqs <- compareCaseMotive mot1 mot2
		clauseEqs <- compareClauses cs1 cs2
		go (argEqs ++ motEqs ++ clauseEqs ++ eqs)

	go ((RecordType tele1 ~~ RecordType tele2) :: eqs) = do
		eqs' <- compareTelescope tele1 tele2
		go (eqs' ++ eqs)

	go ((RecordCon fields1 ~~ RecordCon fields2) :: eqs) = do
		eqs' <- compareFields fields1 fields2
		go (eqs' ++ eqs)

	go ((Project m1 x1 ~~ Project m2 x2) :: eqs) = do
		unless (x1 == x2) $ throw $ "Field names not equal: " ++ x1 ++ " and " ++ x2
		go ((m1 ~~ m2) :: eqs)

	go ((m ~~ m') :: _) = throw $ "Terms not equal: " ++ show m ++ " and " ++ show m'

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
module Data.Linear.Vector

import public Data.Fin
import Data.IOArray.Prims

%default total

unsafePrimIO : PrimIO a -> a
unsafePrimIO = unsafePerformIO . primIO

export
data Vector : Nat -> Type -> Type where
  UnsafeFromPrimArray : ArrayData a -> Vector n a

export
newVector : {n : Nat} -> a -> Vector n a
newVector x = UnsafeFromPrimArray . unsafePrimIO $ prim__newArray (cast n) x

export
readVector : Vector n a -> Fin n -> a
readVector (UnsafeFromPrimArray xs) i = unsafePrimIO $ prim__arrayGet xs (cast (finToNat i))

public export
interface LVector (f : Nat -> Type -> Type) where
  withVector : {n : Nat} -> a -> (1 _ : ((1 _ : f n a) -> b)) -> b
  read : (1 _ : f n a) -> Fin n -> Res a (const (f n a))
  write : (1 _ : f n a) -> Fin n -> a -> f n a
  modify : (1 _ : f n a) -> Fin n -> (a -> a) -> f n a

export
LVector Vector where
  withVector x f =
    let xs := unsafePrimIO $ prim__newArray (cast n) x
     in f $ UnsafeFromPrimArray xs

  read (UnsafeFromPrimArray xs) i =
    unsafePrimIO (prim__arrayGet xs (cast (finToNat i))) # UnsafeFromPrimArray xs

  write (UnsafeFromPrimArray xs) i x =
    unsafePrimIO $ prim__arraySet xs (cast (finToNat i)) x
        `prim__io_bind` const (prim__io_pure (UnsafeFromPrimArray xs))

  modify (UnsafeFromPrimArray xs) i f =
    let i' := cast (finToNat i)
     in unsafePrimIO $ (prim__arrayGet xs i'
            `prim__io_bind` prim__arraySet xs i' . f)
            `prim__io_bind` const (prim__io_pure (UnsafeFromPrimArray xs))


text:
module Text.WebIDL.Codegen.Members

import Data.List
import Text.WebIDL.Codegen.Args
import Text.WebIDL.Codegen.Rules
import Text.WebIDL.Codegen.Types
import Text.WebIDL.Codegen.Util
import Text.WebIDL.Types

--------------------------------------------------------------------------------
--          Subtyping
--------------------------------------------------------------------------------

export
jsType : Identifier -> Supertypes -> String
jsType n (MkSupertypes parents ms) =
  let mixins = sortedNubOn id ms

   in show $ vsep [ ""
                  , "public export"
                  , "JSType" <++> pretty' n.value <++> "where"
                  , "  parents = " <++>
                      prettyList (map (pretty . value) parents)
                  , ""
                  , "  mixins = " <++>
                      prettyList (map (pretty . value) mixins)
                  ]

--------------------------------------------------------------------------------
--          Constants
--------------------------------------------------------------------------------

export
constants : List CGConst -> List String
constants = map (show . const) . sortBy (comparing name)
  where const : CGConst -> Doc ()
        const (MkConst t n v) =
          indent 2 $ vsep [ ""
                          , "public export"
                          , pretty n.value <++> ":" <++> constTpe t
                          , pretty n.value <++> "=" <++> pretty v
                          ]

--------------------------------------------------------------------------------
--          Callback Conversion
--------------------------------------------------------------------------------

export
primCallback : CGCallback -> String
primCallback (MkCallback n _ t as) =
  callbackFFI n (primMarshallCallback n) (callbackFFI $ length as) as t

export
callback : CGCallback -> String
callback (MkCallback n _ t as) =
  callbackAPI n (marshallCallback n) (primMarshallCallback n) as t

--------------------------------------------------------------------------------
--          Attribute
--------------------------------------------------------------------------------

attrImpl:  (msg : Doc())
        -> (set : Doc())
        -> (get : Doc())
        -> (app : Doc())
        -> (arg : CGArg)
        -> (Doc (), Doc())
attrImpl msg s g a (Mandatory _ (Simple $ MaybeNull x)) =
  ( "Attribute False Maybe" <++> ret App (Simple $ NotNull x)
  , "fromNullablePrim" <++> align (sep [msg,s,g,a])
  )

attrImpl msg s g a (Mandatory _ (Union $ MaybeNull x)) =
  ( "Attribute False Maybe" <++> ret App (Union $ NotNull x)
  , "fromNullablePrim" <++> align (sep [msg,s,g,a])
  )

attrImpl msg s g a (Mandatory _ t) =
  ( "Attribute True I" <++> ret App t
  , "fromPrim" <++> align (sep [msg,s,g,a])
  )

attrImpl msg s g a (VarArg _ t) =
  ( "Attribute True I" <++> prettyCon App "VarArg" [ffi App t]
  , "fromPrim" <++> align (sep [msg,s,g,a])
  )

attrImpl msg s g a (Optional _ t d) =
   case deflt (safeCast t) App t d of
      Nothing  =>
        ( "Attribute False Optional" <++> ret App t
        , "fromUndefOrPrimNoDefault" <++> align (sep [msg,s,g,a])
        )
      Just x =>
        ( "Attribute True Optional" <++> ret App t
        , "fromUndefOrPrim" <++> align (sep [msg,s,g,x,a])
        )

attrRW :  Nat
       -> AttributeName
       -> Kind
       -> CGArg
       -> ReturnType
       -> String
attrRW k n o t rt =
  let implName   = attrGetter k n
      primGet    = pretty' $ primAttrGetter k n
      primSet    = pretty' $ primAttrSetter k n
      msg        = pretty' $ namespacedIdent o (fromString $ "get" ++ n.value)
      po         = pretty' $ kindToString o
      up         = if isParent o
                      then "(v :> " <+> po <+> ")"
                      else "v"

      (tpe,impl) = attrImpl msg primGet primSet up t
      funTpe     = if isParent o
                      then typeDeclWithImplicits
                           implName
                           tpe
                           ["(0 _ : JSType t)"]
                           ["{auto 0 _ : Elem" <++> po <++> "(Types t)}","t"]
                      else typeDecl implName tpe [po]

   in show . indent 2 $ vsep [ ""
                             , "export"
                             , funTpe
                             , hsep [pretty' implName,"v =",impl]
                             ]

--------------------------------------------------------------------------------
--          Functions
--------------------------------------------------------------------------------

obj : Kind -> CGArg
obj k = Mandatory (MkArgName "obj") (fromKind k)

function : (Nat,CGFunction) -> String
function (k,Getter o i t) = fun o (getter k) (primGetter k) [obj o, i] t

function (k,Setter o i v) =
  fun o (setter k) (primSetter k) [obj o, i, v] Undefined

function (k,Regular n o as t) = fun o (op k n) (primOp k n) (obj o :: as) t

function (k,Static n o as t) = fun o (op k n) (primOp k n) as t

function (k,Attribute n o t rt) = attrRW k n o t rt

function (k,AttributeGet n o t) =
  fun o (attrGetter k n) (primAttrGetter k n) [obj o] t

function (k,StaticAttributeSet n o t) =
  fun o (attrSetter k n) (primAttrSetter k n) [t] Undefined

function (k,StaticAttributeGet n o t) =
  fun o (attrGetter k n) (primAttrGetter k n) [] t

function (k,DictConstructor o as) =
  fun o (constr k) (primConstr k) as (fromKind o)

function (k,Constructor o as) =
  fun o (constr k) (primConstr k) as (fromKind o)

hasVarArg : Args -> Bool
hasVarArg (VarArg _ _ :: []) = True
hasVarArg []                 = False
hasVarArg (_ :: xs)          = hasVarArg xs

prim : (Nat,CGFunction) -> String
prim (k,Getter o i t) = funFFI (primGetter k) getterFFI [obj o, i] t
prim (k,Setter o i v) = funFFI (primSetter k) setterFFI [obj o, i, v] Undefined
prim (k,Regular n o args t) =
  let as = obj o :: args
   in if hasVarArg args
         then funFFI (primOp k n) (funFFIVarArg n $ length args) as t
         else funFFI (primOp k n) (funFFI n $ length args) as t

prim (k,Static n o as t) =
  if hasVarArg as
     then funFFI (primOp k n) (staticFunFFIVarArg o n $ length as) as t
     else funFFI (primOp k n) (staticFunFFI o n $ length as) as t

prim (k,Attribute n o t rt) =
  fastUnlines
    [ funFFI (primAttrGetter k n) (attrGetFFI n) [obj o] rt
    , ""
    , funFFI (primAttrSetter k n) (attrSetFFI n) [obj o, t] Undefined
    ]

prim (k,AttributeGet n o t) =
  funFFI (primAttrGetter k n) (attrGetFFI n) [obj o] t

prim (k,StaticAttributeSet n o t) =
  funFFI (primAttrSetter k n) (staticAttrSetFFI o n) [t] Undefined

prim (k,StaticAttributeGet n o t) =
  funFFI (primAttrGetter k n) (staticAttrGetFFI o n) [] t

prim (k,DictConstructor o as) =
  funFFI (primConstr k) (dictConFFI $ map argName as) as (fromKind o)

prim (k,Constructor o as)  =
  if hasVarArg as
     then funFFI (primConstr k) (conFFIVarArg o $ length as) as (fromKind o)
     else funFFI (primConstr k) (conFFI o $ length as) as (fromKind o)

-- Tags functions with an index if several function of the
-- same priority (same kind of function and same name) exist,
-- as these would lead to overloading issues.
tagFunctions : List CGFunction -> List (Nat,CGFunction)
tagFunctions = go 0
  where go : Nat -> List CGFunction -> List (Nat,CGFunction)
        go _ []        = []
        go k (x :: []) = [(k,x)]
        go k (x :: t@(y :: ys)) =
          if priority x == priority y
             then (k,x) :: go (S k) t
             else (k,x) :: go 0 t

export
functions : List CGFunction -> List String
functions = map function . tagFunctions . sortBy (comparing priority)

export
primFunctions : List CGFunction -> List String
primFunctions = map prim . tagFunctions . sortBy (comparing priority)


text:
module Data.List1

import public Data.Zippable

%default total

infixr 7 :::

||| Non-empty lists.
public export
record List1 a where
  constructor (:::)
  head : a
  tail : List a

%name List1 xs, ys, zs

------------------------------------------------------------------------
-- Basic functions

public export
fromList : List a -> Maybe (List1 a)
fromList [] = Nothing
fromList (x :: xs) = Just (x ::: xs)

public export
singleton : (x : a) -> List1 a
singleton a = a ::: []

||| Forget that a list is non-empty.
public export
forget : List1 a -> List a
forget (x ::: xs) = x :: xs

export
last : List1 a -> a
last (x ::: xs) = loop x xs where
  loop : a -> List a -> a
  loop x [] = x
  loop _ (x :: xs) = loop x xs

export
init : List1 a -> List a
init (x ::: xs) = loop x xs where
  loop : a -> List a -> List a
  loop x [] = []
  loop x (y :: xs) = x :: loop y xs

export
foldr1By : (func : a -> b -> b) -> (map : a -> b) -> (l : List1 a) -> b
foldr1By f map (x ::: xs) = loop x xs where
  loop : a -> List a -> b
  loop x [] = map x
  loop x (y :: xs) = f x (loop y xs)

export
foldl1By : (func : b -> a -> b) -> (map : a -> b) -> (l : List1 a) -> b
foldl1By f map (x ::: xs) = foldl f (map x) xs

export
foldr1 : (func : a -> a -> a) -> (l : List1 a) -> a
foldr1 f = foldr1By f id

export
foldl1 : (func : a -> a -> a) -> (l : List1 a) -> a
foldl1 f = foldl1By f id

------------------------------------------------------------------------
-- Append

export
appendl : (xs : List1 a) -> (ys : List a) -> List1 a
appendl (x ::: xs) ys = x ::: xs ++ ys

export
(++) : (xs, ys : List1 a) -> List1 a
(++) xs ys = appendl xs (forget ys)

export
lappend : (xs : List a) -> (ys : List1 a) -> List1 a
lappend [] ys = ys
lappend (x :: xs) ys = (x ::: xs) ++ ys

------------------------------------------------------------------------
-- Cons/Snoc

public export
cons : (x : a) -> (xs : List1 a) -> List1 a
cons x xs = x ::: forget xs

export
snoc : (xs : List1 a) -> (x : a) -> List1 a
snoc xs x = xs ++ (singleton x)

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

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

------------------------------------------------------------------------
-- Reverse

public export
reverseOnto : (acc : List1 a) -> (xs : List a) -> List1 a
reverseOnto acc [] = acc
reverseOnto acc (x :: xs) = reverseOnto (x ::: forget acc) xs

public export
reverse : (xs : List1 a) -> List1 a
reverse (x ::: xs) = reverseOnto (singleton x) xs

------------------------------------------------------------------------
-- Instances

export
Semigroup (List1 a) where
  (<+>) = (++)

public export
Functor List1 where
  map f (x ::: xs) = f x ::: map f xs

public export
Applicative List1 where
  pure x = singleton x
  f ::: fs <*> xs = appendl (map f xs) (fs <*> forget xs)

export
Monad List1 where
  (x ::: xs) >>= f = appendl (f x) (xs >>= forget . f)

export
Foldable List1 where
  foldr c n (x ::: xs) = c x (foldr c n xs)
  foldl f z (x ::: xs) = foldl f (f z x) xs
  null _ = False
  toList = forget
  foldMap f (x ::: xs) = f x <+> foldMap f xs

export
Traversable List1 where
  traverse f (x ::: xs) = [| f x ::: traverse f xs |]

export
Show a => Show (List1 a) where
  show = show . forget

export
Eq a => Eq (List1 a) where
  (x ::: xs) == (y ::: ys) = x == y && xs == ys

export
Ord a => Ord (List1 a) where
  compare xs ys = compare (forget xs) (forget ys)

------------------------------------------------------------------------
-- Properties

export
consInjective : (x ::: xs) === (y ::: ys) -> (x === y, xs === ys)
consInjective Refl = (Refl, Refl)

------------------------------------------------------------------------
-- Zippable

public export
Zippable List1 where
  zipWith f (x ::: xs) (y ::: ys) = f x y ::: zipWith' xs ys
  where
      zipWith' : List a -> List b -> List c
      zipWith' [] _ = []
      zipWith' _ [] = []
      zipWith' (x :: xs) (y :: ys) = f x y :: zipWith' xs ys

  zipWith3 f (x ::: xs) (y ::: ys) (z ::: zs) = f x y z ::: zipWith3' xs ys zs
    where
      zipWith3' : List a -> List b -> List c -> List d
      zipWith3' [] _ _ = []
      zipWith3' _ [] _ = []
      zipWith3' _ _ [] = []
      zipWith3' (x :: xs) (y :: ys) (z :: zs) = f x y z :: zipWith3' xs ys zs

  unzipWith f (x ::: xs) = let (b, c) = f x
                               (bs, cs) = unzipWith' xs in
                               (b ::: bs, c ::: cs)
    where
      unzipWith' : List a -> (List b, List c)
      unzipWith' [] = ([], [])
      unzipWith' (x :: xs) = let (b, c) = f x
                                 (bs, cs) = unzipWith' xs in
                                 (b :: bs, c :: cs)

  unzipWith3 f (x ::: xs) = let (b, c, d) = f x
                                (bs, cs, ds) = unzipWith3' xs in
                                (b ::: bs, c ::: cs, d ::: ds)
    where
      unzipWith3' : List a -> (List b, List c, List d)
      unzipWith3' [] = ([], [], [])
      unzipWith3' (x :: xs) = let (b, c, d) = f x
                                  (bs, cs, ds) = unzipWith3' xs in
                                  (b :: bs, c :: cs, d :: ds)

export
Uninhabited a => Uninhabited (List1 a) where
  uninhabited (hd ::: _) = uninhabited hd


text:
import Data.Primitives.Views

data Face = Head | Tail

getFace : Int -> Face
getFace x with (divides x 2)
  getFace ((2 * div) + rem) | (DivBy prf)
    = case rem of
           0 => Head
           other => Tail

coinFlips : (count : Nat) -> Stream Int -> List Face
coinFlips Z xs = []
coinFlips (S k) (x :: xs) = getFace x :: coinFlips k xs

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
||| Contains:
|||
||| 1. Tail recursive versions of the list processing functions from
|||    Data.List.
|||
||| 2. Extensional equality proofs that these variants are
|||    (extensionally) equivalent to their non-tail-recursive
|||    counterparts.
|||
||| Note:
|||
||| 1. Written in one sitting, feel free to refactor
|||
||| 2. The proofs below also work on non-publicly exported
|||    definitions.  This could be due to a bug, and will need to be
|||    moved elsewhere if it's fixed.
module Data.List.TailRec

import Syntax.PreorderReasoning
import Syntax.WithProof

import Data.List
import Data.List1
import Data.Vect
import Data.Nat

total
lengthAcc : List a -> Nat -> Nat
lengthAcc [] acc = acc
lengthAcc (_::xs) acc = lengthAcc xs $ S acc

export total
length : List a -> Nat
length xs = lengthAcc xs Z

total
lengthAccSucc : (xs : List a) -> (n : Nat) -> lengthAcc xs (S n) = S (lengthAcc xs n)
lengthAccSucc [] _ = Refl
lengthAccSucc (_::xs) n = rewrite lengthAccSucc xs (S n) in cong S Refl

export total
length_ext : (xs : List a) -> List.length xs = Data.List.TailRec.length xs
length_ext [] = Refl
length_ext (_::xs) = rewrite length_ext xs in sym $ lengthAccSucc xs Z

take_aux : Nat -> List a -> List a -> List a
take_aux Z     xs        acc = reverseOnto [] acc
take_aux (S n) []        acc = reverseOnto [] acc
take_aux (S n) (x :: xs) acc = take_aux n xs (x :: acc)

export
take : Nat -> List a -> List a
take n xs = take_aux n xs []

export
take_ext :
  (n : Nat) -> (xs : List a) ->
     Data.List.take n xs = Data.List.TailRec.take n xs
take_ext n xs = Calc $
  |~ Data.List.take n xs
  ~~ reverse [] ++ (Data.List.take n xs)  ...( Refl )
  ~~ reverseOnto (Data.List.take n xs) [] ...( sym (revOnto (Data.List.take n xs) []) )
  ~~ take_aux n xs []                     ...( sym (lemma n xs []) )
  where
    lemma : (n : Nat) -> (xs, acc : List a) ->
            take_aux n xs acc =  reverseOnto (Data.List.take n xs) acc
    lemma Z     xs      acc = Refl
    lemma (S n) []      acc = Refl
    lemma (S n) (x::xs) acc = lemma n xs (x :: acc)

span_aux : (a -> Bool) -> List a -> List a -> (List a, List a)
span_aux p []      acc = (reverseOnto [] acc, [])
span_aux p (x::xs) acc =
  if p x then
    Data.List.TailRec.span_aux p xs (x :: acc)
  else
    (reverseOnto [] acc, x::xs)

export
span : (a -> Bool) -> List a -> (List a, List a)
span p xs = span_aux p xs []

coe : (f : (i : a) -> Type) -> i = i' -> f i -> f i'
coe f Refl x = x

span_aux_ext : (p : a -> Bool) -> (xs, acc : List a) ->
  (reverseOnto (fst $ Data.List.span p xs) acc, snd $ Data.List.span p xs)
  =
  span_aux p xs acc
span_aux_ext p []      acc = Refl
-- This is disgusting. Please teach me a better way.
span_aux_ext p (x::xs) acc with (@@(p x), @@(Data.List.span p xs))
 span_aux_ext p (x::xs) acc | ((True ** px_tru), ((pre, rest)**dl_pf)) =
   rewrite px_tru in
   rewrite dl_pf in
   let u = span_aux_ext p xs (x::acc) in
   coe (\u => (reverseOnto (x :: fst u) acc, snd u) =
               Data.List.TailRec.span_aux p xs (x :: acc)) dl_pf u
 span_aux_ext p (x::xs) acc | ((False**px_fls), ((pre,rest)**dl_pf)) =
   rewrite px_fls in
   Refl

export
span_ext : (p : a -> Bool) -> (xs : List a) ->
  Data.List.span p xs = Data.List.TailRec.span p xs
span_ext p xs with (@@(Data.List.span p xs))
  span_ext p xs |  ((pre, rest) ** pf) =
    rewrite pf in
    let u = span_aux_ext p xs [] in
    coe (\u => (fst u, snd u) = span_aux p xs []) pf u

export
break : (a -> Bool) -> List a -> (List a, List a)
break p xs = Data.List.TailRec.span (not . p) xs

export
break_ext : (p : a -> Bool) -> (xs : List a) ->
  Data.List.break p xs = Data.List.TailRec.break p xs
break_ext p xs = span_ext (not . p) xs

splitOnto : List (List a) -> (a -> Bool) -> List a -> List1 (List a)
splitOnto acc p xs =
  case Data.List.break p xs of
    (chunk, []       ) => reverseOnto [chunk] acc
    (chunk, (c::rest)) => splitOnto (chunk::acc) p rest

export
split : (a -> Bool) -> List a -> List1 (List a)
split p xs = splitOnto [] p xs

splitOnto_ext : (acc : List (List a)) -> (p : a -> Bool) -> (xs : List a) ->
              reverseOnto (Data.List.split p xs) acc
              = Data.List.TailRec.splitOnto acc p xs
splitOnto_ext  acc p xs with (@@(Data.List.break p xs))
 splitOnto_ext acc p xs | ((chunk,  []    )**pf) =
   rewrite pf in
   Refl
 splitOnto_ext acc p xs | ((chunk, c::rest)**pf) =
   rewrite pf in
   rewrite splitOnto_ext (chunk::acc) p rest in
   Refl

export
split_ext : (p : a -> Bool) -> (xs : List a) ->
  Data.List.split p xs = Data.List.TailRec.split p xs
split_ext p xs = splitOnto_ext [] p xs

splitAtOnto : List a -> (n : Nat) -> (xs : List a) -> (List a, List a)
splitAtOnto acc Z     xs      = (reverseOnto [] acc, xs)
splitAtOnto acc (S n) []      = (reverseOnto [] acc, [])
splitAtOnto acc (S n) (x::xs) = splitAtOnto (x::acc) n xs

export
splitAt : (n : Nat) -> (xs : List a) -> (List a, List a)
splitAt n xs = splitAtOnto [] n xs

splitAtOnto_ext : (acc : List a) -> (n : Nat) -> (xs : List a) ->
  (reverseOnto (fst $ Data.List.splitAt n xs) acc, snd $ Data.List.splitAt n xs)
  = splitAtOnto acc n xs
splitAtOnto_ext  acc Z     xs      = Refl
splitAtOnto_ext  acc (S n) []      = Refl
splitAtOnto_ext  acc (S n) (x::xs) with (@@(Data.List.splitAt n xs))
 splitAtOnto_ext acc (S n) (x::xs) | ((tk, dr)**pf) =
   rewrite pf in
   let u = splitAtOnto_ext (x::acc) n xs in
   coe (\u => (reverseOnto (x :: fst u) acc, snd u) =
                      splitAtOnto (x :: acc) n xs) pf u

export
splitAt_ext : (n : Nat) -> (xs : List a) ->
  Data.List.splitAt n xs =
  Data.List.TailRec.splitAt n xs
splitAt_ext  n xs with (@@(Data.List.splitAt n xs))
 splitAt_ext n xs | ((tk, dr)**pf) =
   rewrite pf in
   rewrite sym $ splitAtOnto_ext [] n xs in
   rewrite pf in
   Refl

partitionOnto : List a -> List a -> (a -> Bool) -> List a -> (List a, List a)
partitionOnto lfts rgts p []      = (reverseOnto [] lfts, reverseOnto [] rgts)
partitionOnto lfts rgts p (x::xs) =
  if p x then
    partitionOnto (x :: lfts)     rgts  p xs
  else
    partitionOnto       lfts  (x::rgts) p xs

export
partition : (a -> Bool) -> List a -> (List a, List a)
partition p xs = partitionOnto [] [] p xs

partitionOnto_ext : (lfts, rgts : List a) -> (p : a -> Bool) -> (xs : List a) ->
  (reverseOnto (fst $ Data.List.partition p xs) lfts
  ,reverseOnto (snd $ Data.List.partition p xs) rgts)
  = Data.List.TailRec.partitionOnto lfts rgts p xs
partitionOnto_ext  lfts rgts p [] = Refl
partitionOnto_ext  lfts rgts p (x::xs) with (@@(p x), @@(Data.List.partition p xs))
 partitionOnto_ext lfts rgts p (x::xs) | ((True **px_tru), ((dl_l, dl_r)**dl_pf))
   = rewrite px_tru in
     rewrite dl_pf  in
     rewrite px_tru in
     let u = partitionOnto_ext (x :: lfts) rgts p xs in
     coe (\u => (reverseOnto (x :: fst u) lfts
                ,reverseOnto (     snd u) rgts)
                = partitionOnto (x :: lfts) rgts p xs) dl_pf u

 partitionOnto_ext lfts rgts p (x::xs) | ((False**px_fls), ((dl_l, dl_r)**dl_pf))
   = rewrite px_fls in
     rewrite dl_pf  in
     rewrite px_fls in
     let u = partitionOnto_ext lfts (x :: rgts) p xs in
     coe (\u => (reverseOnto (     fst u) lfts
                ,reverseOnto (x :: snd u) rgts)
                = partitionOnto lfts (x::rgts) p xs) dl_pf u

mergeReplicate_aux : a -> List a -> List a -> List a
mergeReplicate_aux sep []      acc = reverseOnto [] acc
mergeReplicate_aux sep (x::xs) acc = mergeReplicate_aux sep xs (x :: sep :: acc)

mergeReplicate_ext : (sep : a) -> (xs : List a) -> (acc : List a) ->
                   mergeReplicate_aux sep xs acc =
                   reverseOnto (mergeReplicate sep xs) acc
mergeReplicate_ext sep []      acc = Refl
mergeReplicate_ext sep (x::xs) acc = Calc $
  |~ mergeReplicate_aux sep xs (x :: sep :: acc)
  ~~ reverseOnto (sep :: x :: mergeReplicate sep xs) acc
                              ...( mergeReplicate_ext sep xs (x :: sep :: acc) )

export
intersperse : a -> List a -> List a
intersperse sep []      = []
intersperse sep (y::ys) = y :: mergeReplicate_aux sep ys []

export
intersperse_ext : (sep : a) -> (xs : List a) ->
              Data.List.intersperse sep xs =
              Data.List.TailRec.intersperse sep xs
intersperse_ext sep [] = Refl
intersperse_ext sep (y::ys) = cong (y::) (sym $ mergeReplicate_ext sep ys [])

mapMaybeOnto : List b -> (a -> Maybe b) -> List a -> List b
mapMaybeOnto acc f [] = reverseOnto [] acc
mapMaybeOnto acc f (x::xs) =
  case f x of
    Nothing => mapMaybeOnto acc f xs
    Just  y => mapMaybeOnto (y :: acc) f xs

export
mapMaybe : (a -> Maybe b) -> List a -> List b
mapMaybe f xs = mapMaybeOnto [] f xs

mapMaybeOnto_ext : (acc : List b) -> (f : a -> Maybe b) -> (xs : List a) ->
  reverseOnto (Data.List.mapMaybe f xs) acc
  =
  mapMaybeOnto acc f xs
mapMaybeOnto_ext  acc f []                = Refl
mapMaybeOnto_ext  acc f (x::xs) with (f x)
 mapMaybeOnto_ext acc f (x::xs) | Nothing = mapMaybeOnto_ext acc f xs
 mapMaybeOnto_ext acc f (x::xs) | Just  y = mapMaybeOnto_ext (y :: acc) f xs

export
mapMaybe_ext : (f : a -> Maybe b) -> (xs : List a) ->
  Data.List.mapMaybe f xs = Data.List.TailRec.mapMaybe f xs
mapMaybe_ext f xs = mapMaybeOnto_ext [] f xs

export
sorted : Ord a => List a -> Bool
sorted [ ] = True
sorted [x] = True
sorted  (x :: xs@(y :: ys)) = case (x <= y) of
                                False => False
                                True  => Data.List.TailRec.sorted xs

export
sorted_ext : Ord a => (xs : List a) ->
  Data.List.sorted xs = Data.List.TailRec.sorted xs
sorted_ext []  = Refl
sorted_ext [x] = Refl
sorted_ext  (x :: y :: ys) with (x <= y)
 sorted_ext (x :: y :: ys) | False = Refl
 sorted_ext (x :: y :: ys) | True  = sorted_ext (y::ys)

mergeByOnto : List a -> (a -> a -> Ordering) -> List a -> List a -> List a
mergeByOnto acc order []           right         = reverseOnto right acc
mergeByOnto acc order left         []            = reverseOnto left  acc
mergeByOnto acc order left@(x::xs) right@(y::ys) =
  -- We need the variant annotations (bug #300)
  case order x y of
    LT => mergeByOnto (x :: acc) order (assert_smaller left xs)   right
    _  => mergeByOnto (y :: acc) order left                       (assert_smaller right ys)

mergeByOnto_ext : (acc : List a)
               -> (order : a -> a -> Ordering)
               -> (left, right : List a)
               -> reverseOnto (mergeBy order left right) acc
                  = mergeByOnto acc order left right
mergeByOnto_ext acc order []           right         = Refl
mergeByOnto_ext  acc order left        []            with( left)
 mergeByOnto_ext acc order _           []            | []     = Refl
 mergeByOnto_ext acc order _           []            | (_::_) = Refl
mergeByOnto_ext acc order left@(x::xs) right@(y::ys) with (order x y)
 mergeByOnto_ext acc order left@(x::xs) right@(y::ys) | LT =
                           mergeByOnto_ext (x :: acc) order xs (y::ys)
 -- We need to exhaust the two other cases explicitly to convince the
 -- typecheker. See #140
 mergeByOnto_ext acc order left@(x::xs) right@(y::ys) | EQ =
                           mergeByOnto_ext (y :: acc) order (x::xs) ys
 mergeByOnto_ext acc order left@(x::xs) right@(y::ys) | GT =
                           mergeByOnto_ext (y :: acc) order (x::xs) ys

export
mergeBy : (a -> a -> Ordering) -> List a -> List a -> List a
mergeBy order left right = mergeByOnto [] order left right

export
mergeBy_ext : (order : a -> a -> Ordering) -> (left, right : List a) ->
  Data.List.mergeBy order left right =
  Data.List.TailRec.mergeBy order left right
mergeBy_ext order left right = mergeByOnto_ext [] order left right

export
merge : Ord a => List a -> List a -> List a
merge = Data.List.TailRec.mergeBy compare

export
merge_ext : Ord a => (left, right : List a) ->
  Data.List.merge left right = Data.List.TailRec.merge left right
merge_ext left right = mergeBy_ext compare left right

-- Not quite finished due to a bug.

sortBy_splitRec : List a -> List a -> (List a -> List a) -> (List a, List a)
sortBy_splitRec (_::_::xs) (y::ys) zs = sortBy_splitRec xs ys (zs . ((::) y))
sortBy_splitRec _          ys      zs = (zs [], ys)

sortBy_split : List a -> (List a, List a)
sortBy_split xs = sortBy_splitRec xs xs id

export
sortBy : (cmp : a -> a -> Ordering) -> (xs : List a) -> List a
sortBy cmp []  = []
sortBy cmp [x] = [x]
sortBy cmp zs = let (xs, ys) = sortBy_split zs in
    Data.List.TailRec.mergeBy cmp
          (Data.List.TailRec.sortBy cmp (assert_smaller zs xs))
          (Data.List.TailRec.sortBy cmp (assert_smaller zs ys))

 {- Can't really finish this proof because Data.List doesn't export the definition of sortBy. -}
 {-
export
sortBy_ext : (cmp : a -> a -> Ordering) -> (xs : List a) ->
  Data.List.sortBy cmp xs = Data.List.TailRec.sortBy cmp xs
sortBy_ext  cmp []  = Refl
sortBy_ext  cmp [x] = Refl
sortBy_ext  cmp zs'@(z::zs) =
  Calc $
  |~ Data.List.sortBy cmp (z::zs)
  ~~ (let (xs, ys) = sortBy_split zs' in
     Data.List.mergeBy cmp
     (Data.List.sortBy cmp xs)
     (Data.List.sortBy cmp ys))
      ...( ?help0 )
  ~~
  let (xs, ys) = sortBy_split (z::zs) in
  Data.List.TailRec.mergeBy cmp
    (Data.List.TailRec.sortBy cmp xs)
    (Data.List.TailRec.sortBy cmp ys)
    ...( ?help1 )
-}


text:
module Test.Bits16

import Data.Prim.Bits16
import Data.SOP
import Hedgehog
import Test.RingLaws

allBits16 : Gen Bits16
allBits16 = bits16 (linear 0 0xffff)

gt0 : Gen Bits16
gt0 = bits16 (linear 1 MaxBits16)

gt1 : Gen Bits16
gt1 = bits16 (linear 2 MaxBits16)

prop_ltMax : Property
prop_ltMax = property $ do
  b8 <- forAll allBits16
  (b8 <= MaxBits16) === True

prop_ltMin : Property
prop_ltMin = property $ do
  b8 <- forAll allBits16
  (b8 >= MinBits16) === True

prop_comp : Property
prop_comp = property $ do
  [m,n] <- forAll $ np [allBits16, allBits16]
  toOrdering (comp m n) === compare m n

prop_mod : Property
prop_mod = property $ do
  [n,d] <- forAll $ np [allBits16, gt0]
  compare (n `mod` d) d === LT

prop_div : Property
prop_div = property $ do
  [n,d] <- forAll $ np [gt0, gt1]
  compare (n `div` d) n === LT

prop_divMod : Property
prop_divMod = property $ do
  [n,d] <- forAll $ np [allBits16, gt0]
  let x = n `div` d
      r = n `mod` d
  n === x * d + r

export
props : Group
props = MkGroup "Bits16" $
  [ ("prop_ltMax",  prop_ltMax)
  , ("prop_ltMin",  prop_ltMin)
  , ("prop_comp",   prop_comp)
  , ("prop_mod",    prop_mod)
  , ("prop_div",    prop_div)
  , ("prop_divMod", prop_divMod)
  ] ++ ringProps allBits16


text:
> module NonNegDouble.MeasureProperties

> import Syntax.PreorderReasoning

> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import NonNegDouble.Measures
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import NonNegDouble.Predicates
> import NonNegDouble.LTEProperties
> import List.Properties

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

* Properties of |average|:

> %freeze monotoneSum

> using implementation NumNonNegDouble
>   using implementation FractionalNonNegDouble
>     ||| |average| is monotone
>     monotoneAverage : {A : Type} ->
>                       (f : A -> NonNegDouble) -> (g : A -> NonNegDouble) ->
>                       (p : (a : A) -> f a `LTE` g a) ->
>                       (as : List A) ->
>                       average (map f as) `LTE` average (map g as)
>     monotoneAverage f g p as = monotoneMultLTE {a = sum (map f as)}
>                                                {b = sum (map g as)}
>                                                {c = one / fromNat (length (map f as))}
>                                                {d = one / fromNat (length (map g as))}
>                                                s1 s3 where
>       s1 : sum (map f as) `LTE` sum (map g as)
>       s1 = monotoneSum f g p as
>       s2 : one / fromNat (length (map f as)) `LTE` one / fromNat (length (map f as))
>       s2 = reflexiveLTE (one / fromNat (length (map f as)))
>       s3 : one / fromNat (length (map f as)) `LTE` one / fromNat (length (map g as))
>       s3 = replace {P = \ X => one / fromNat (length (map f as)) `LTE` one / fromNat X} (lengthLemma as f g) s2

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Control.Algebra.Laws

import Control.Algebra

%default total

-- Monoids

||| Inverses are unique.
public export
uniqueInverse : MonoidV ty => (x, y, z : ty) ->
  y <+> x = neutral {ty} -> x <+> z = neutral {ty} -> y = z
uniqueInverse x y z p q =
  rewrite sym $ monoidNeutralIsNeutralL y in
    rewrite sym q in
      rewrite semigroupOpIsAssociative y x z in
  rewrite p in
    rewrite monoidNeutralIsNeutralR z in
      Refl

-- Groups

||| Only identity is self-squaring.
public export
selfSquareId : Group ty => (x : ty) ->
  x <+> x = x -> x = neutral {ty}
selfSquareId x p =
  rewrite sym $ monoidNeutralIsNeutralR x in
    rewrite sym $ groupInverseIsInverseR x in
  rewrite sym $ semigroupOpIsAssociative (inverse x) x x in
    rewrite p in
      Refl

||| Inverse elements commute.
public export
inverseCommute : Group ty => (x, y : ty) ->
  y <+> x = neutral {ty} -> x <+> y = neutral {ty}
inverseCommute x y p = selfSquareId (x <+> y) prop where
  prop : (x <+> y) <+> (x <+> y) = x <+> y
  prop =
    rewrite sym $ semigroupOpIsAssociative x y (x <+> y) in
      rewrite semigroupOpIsAssociative y x y in
    rewrite p in
      rewrite monoidNeutralIsNeutralR y in
        Refl

||| Every element has a right inverse.
public export
groupInverseIsInverseL : Group ty => (x : ty) ->
  x <+> inverse x = neutral {ty}
groupInverseIsInverseL x =
  inverseCommute x (inverse x) (groupInverseIsInverseR x)

||| -(-x) = x
public export
inverseSquaredIsIdentity : Group ty => (x : ty) ->
  inverse (inverse x) = x
inverseSquaredIsIdentity {ty} x =
  uniqueInverse
    (inverse x)
    (inverse $ inverse x)
    x
    (groupInverseIsInverseR $ inverse x)
    (groupInverseIsInverseR x)

||| If every square in a group is identity, the group is commutative.
public export
squareIdCommutative : Group ty => (x, y : ty) ->
  ((a : ty) -> a <+> a = neutral {ty}) ->
  x <+> y = y <+> x
squareIdCommutative x y p =
  uniqueInverse (x <+> y) (x <+> y) (y <+> x) (p (x <+> y)) prop where
    prop : (x <+> y) <+> (y <+> x) = neutral {ty}
    prop =
      rewrite sym $ semigroupOpIsAssociative x y (y <+> x) in
        rewrite semigroupOpIsAssociative y y x in
      rewrite p y in
        rewrite monoidNeutralIsNeutralR x in
          p x

||| -0 = 0
public export
inverseNeutralIsNeutral : Group ty =>
  inverse (neutral {ty}) = neutral {ty}
inverseNeutralIsNeutral {ty} =
  rewrite sym $ cong inverse (groupInverseIsInverseL (neutral {ty})) in
    rewrite monoidNeutralIsNeutralR $ inverse (neutral {ty}) in
      inverseSquaredIsIdentity (neutral {ty})

-- ||| -(x + y) = -y + -x
-- public export
-- inverseOfSum : Group ty => (l, r : ty) ->
--   inverse (l <+> r) = inverse r <+> inverse l
-- inverseOfSum {ty} l r =
--   -- expand
--   rewrite sym $ monoidNeutralIsNeutralR $ inverse $ l <+> r in
--     rewrite sym $ groupInverseIsInverseR r in
--       rewrite sym $ monoidNeutralIsNeutralL $ inverse r in
--         rewrite sym $ groupInverseIsInverseR l in
--   -- shuffle
--   rewrite semigroupOpIsAssociative (inverse r) (inverse l) l in
--     rewrite sym $ semigroupOpIsAssociative (inverse r <+> inverse l) l r in
--       rewrite sym $ semigroupOpIsAssociative (inverse r <+> inverse l) (l <+> r) (inverse $ l <+> r) in
--   -- contract
--   rewrite sym $ monoidNeutralIsNeutralL $ inverse l in
--     rewrite groupInverseIsInverseL $ l <+> r in
--       rewrite sym $ semigroupOpIsAssociative (inverse r <+> (inverse l <+> neutral)) l (inverse l <+> neutral) in
--         rewrite semigroupOpIsAssociative l (inverse l) neutral in
--           rewrite groupInverseIsInverseL l in
--             rewrite monoidNeutralIsNeutralL $ the ty neutral in
--               Refl

||| y = z if x + y = x + z
public export
cancelLeft : Group ty => (x, y, z : ty) ->
  x <+> y = x <+> z -> y = z
cancelLeft x y z p =
  rewrite sym $ monoidNeutralIsNeutralR y in
    rewrite sym $ groupInverseIsInverseR x in
      rewrite sym $ semigroupOpIsAssociative (inverse x) x y in
        rewrite p in
      rewrite semigroupOpIsAssociative (inverse x) x z in
    rewrite groupInverseIsInverseR x in
  monoidNeutralIsNeutralR z

||| y = z if y + x = z + x.
public export
cancelRight : Group ty => (x, y, z : ty) ->
  y <+> x = z <+> x -> y = z
cancelRight x y z p =
  rewrite sym $ monoidNeutralIsNeutralL y in
    rewrite sym $ groupInverseIsInverseL x in
      rewrite semigroupOpIsAssociative y x (inverse x) in
        rewrite p in
      rewrite sym $ semigroupOpIsAssociative z x (inverse x) in
    rewrite groupInverseIsInverseL x in
  monoidNeutralIsNeutralL z

||| ab = 0 -> a = b^-1
public export
neutralProductInverseR : Group ty => (a, b : ty) ->
  a <+> b = neutral {ty} -> a = inverse b
neutralProductInverseR a b prf =
  cancelRight  b a (inverse b) $
    trans prf $ sym $ groupInverseIsInverseR b

||| ab = 0 -> a^-1 = b
public export
neutralProductInverseL : Group ty => (a, b : ty) ->
  a <+> b = neutral {ty} -> inverse a = b
neutralProductInverseL a b prf =
  cancelLeft a (inverse a) b $
    trans (groupInverseIsInverseL a) $ sym prf

||| For any a and b, ax = b and ya = b have solutions.
public export
latinSquareProperty : Group ty => (a, b : ty) ->
  ((x : ty ** a <+> x = b),
    (y : ty ** y <+> a = b))
latinSquareProperty a b =
  ((((inverse a) <+> b) **
    rewrite semigroupOpIsAssociative a (inverse a) b in
      rewrite groupInverseIsInverseL a in
        monoidNeutralIsNeutralR b),
  (b <+> (inverse a) **
    rewrite sym $ semigroupOpIsAssociative b (inverse a) a in
      rewrite groupInverseIsInverseR a in
        monoidNeutralIsNeutralL b))

||| For any a, b, x, the solution to ax = b is unique.
public export
uniqueSolutionR : Group ty => (a, b, x, y : ty) ->
  a <+> x = b -> a <+> y = b -> x = y
uniqueSolutionR a b x y p q = cancelLeft a x y $ trans p (sym q)

||| For any a, b, y, the solution to ya = b is unique.
public export
uniqueSolutionL : Group t => (a, b, x, y : t) ->
  x <+> a = b -> y <+> a = b -> x = y
uniqueSolutionL a b x y p q = cancelRight a x y $ trans p (sym q)

-- ||| -(x + y) = -x + -y
-- public export
-- inverseDistributesOverGroupOp : AbelianGroup ty => (l, r : ty) ->
--   inverse (l <+> r) = inverse l <+> inverse r
-- inverseDistributesOverGroupOp l r =
--   rewrite groupOpIsCommutative (inverse l) (inverse r) in
--     inverseOfSum l r

||| Homomorphism preserves neutral.
public export
homoNeutral : GroupHomomorphism a b =>
  to (neutral {ty=a}) = neutral {ty=b}
homoNeutral =
  selfSquareId (to neutral) $
    trans (sym $ toGroup neutral neutral) $
      cong to $ monoidNeutralIsNeutralL neutral

||| Homomorphism preserves inverses.
public export
homoInverse : GroupHomomorphism a b => (x : a) ->
  the b (to $ inverse x) = the b (inverse $ to x)
homoInverse x =
  cancelRight (to x) (to $ inverse x) (inverse $ to x) $
    trans (sym $ toGroup (inverse x) x) $
      trans (cong to $ groupInverseIsInverseR x) $
        trans homoNeutral $
          sym $ groupInverseIsInverseR (to x)

-- Rings

||| 0x = x
public export
multNeutralAbsorbingL : Ring ty => (r : ty) ->
  neutral {ty} <.> r = neutral {ty}
multNeutralAbsorbingL {ty} r =
  rewrite sym $ monoidNeutralIsNeutralR $ neutral <.> r in
    rewrite sym $ groupInverseIsInverseR $ neutral <.> r in
  rewrite sym $ semigroupOpIsAssociative (inverse $ neutral <.> r) (neutral <.> r) (((inverse $ neutral <.> r) <+> (neutral <.> r)) <.> r) in
    rewrite groupInverseIsInverseR $ neutral <.> r in
  rewrite sym $ ringOpIsDistributiveR neutral neutral r in
    rewrite monoidNeutralIsNeutralR $ the ty neutral in
  groupInverseIsInverseR $ neutral <.> r

||| x0 = 0
public export
multNeutralAbsorbingR : Ring ty => (l : ty) ->
  l <.> neutral {ty} = neutral {ty}
multNeutralAbsorbingR {ty} l =
  rewrite sym $ monoidNeutralIsNeutralL $ l <.> neutral in
    rewrite sym $ groupInverseIsInverseL $ l <.> neutral in
  rewrite semigroupOpIsAssociative (l <.> ((l <.> neutral) <+> (inverse $ l <.> neutral))) (l <.> neutral) (inverse $ l <.> neutral) in
    rewrite groupInverseIsInverseL $ l <.> neutral in
  rewrite sym $ ringOpIsDistributiveL l neutral neutral in
    rewrite monoidNeutralIsNeutralL $ the ty neutral in
  groupInverseIsInverseL $ l <.> neutral

||| (-x)y = -(xy)
public export
multInverseInversesL : Ring ty => (l, r : ty) ->
  inverse l <.> r = inverse (l <.> r)
multInverseInversesL l r =
  rewrite sym $ monoidNeutralIsNeutralR $ inverse l <.> r in
    rewrite sym $ groupInverseIsInverseR $ l <.> r in
      rewrite sym $ semigroupOpIsAssociative (inverse $ l <.> r) (l <.> r) (inverse l <.> r) in
  rewrite sym $ ringOpIsDistributiveR l (inverse l) r in
    rewrite groupInverseIsInverseL l in
  rewrite multNeutralAbsorbingL r in
    monoidNeutralIsNeutralL $ inverse $ l <.> r

||| x(-y) = -(xy)
public export
multInverseInversesR : Ring ty => (l, r : ty) ->
  l <.> inverse r = inverse (l <.> r)
multInverseInversesR l r =
  rewrite sym $ monoidNeutralIsNeutralL $ l <.> (inverse r) in
    rewrite sym $ groupInverseIsInverseL (l <.> r) in
      rewrite semigroupOpIsAssociative (l <.> (inverse r)) (l <.> r) (inverse $ l <.> r) in
  rewrite sym $ ringOpIsDistributiveL l (inverse r) r in
    rewrite groupInverseIsInverseR r in
  rewrite multNeutralAbsorbingR l in
    monoidNeutralIsNeutralR $ inverse $ l <.> r

||| (-x)(-y) = xy
public export
multNegativeByNegativeIsPositive : Ring ty => (l, r : ty) ->
  inverse l <.> inverse r = l <.> r
multNegativeByNegativeIsPositive l r =
    rewrite multInverseInversesR (inverse l) r in
    rewrite sym $ multInverseInversesL (inverse l) r in
    rewrite inverseSquaredIsIdentity l in
    Refl

||| (-1)x = -x
public export
inverseOfUnityR : RingWithUnity ty => (x : ty) ->
  inverse (unity {ty}) <.> x = inverse x
inverseOfUnityR x =
  rewrite multInverseInversesL unity x in
    rewrite unityIsRingIdR x in
      Refl

||| x(-1) = -x
public export
inverseOfUnityL : RingWithUnity ty => (x : ty) ->
  x <.> inverse (unity {ty}) = inverse x
inverseOfUnityL x =
  rewrite multInverseInversesR x unity in
    rewrite unityIsRingIdL x in
      Refl


text:
module VectHelp

import Data.Vect

%default total

||| If an element is in a concat of two vectors, then it's in one or the other.
export
elemConcat: {x: a} -> (xs: Vect m a) -> (ys: Vect n a) -> Elem x (xs ++ ys) -> Either (Elem x xs) (Elem x ys)
elemConcat {x} []        (x :: xs) Here          = Right Here
elemConcat {x} []        (y :: xs) (There later) = Right (There later)
elemConcat {x} (x :: xs) ys        Here          = Left Here
elemConcat {x} (y :: xs) ys        (There later) = case elemConcat xs ys later of
  Left l  => Left $ There l
  Right r => Right r

shift : {x : a} -> {xs : Vect len a} ->
        (y : a ** Elem y xs) -> (y : a ** Elem y (x :: xs))
shift (x ** pf) = (x ** There pf)

||| Returns all the proofs that elements of a vector are in that vector.
export
allElems: (xs: Vect n a) -> Vect n (x: a ** Elem x xs)
allElems []        = []
allElems (x :: xs) =
    let es = allElems xs
    in (x ** Here) :: (map shift es)

max_stars_repo_name: jameshaydon/smproc

max_issues_repo_name: jameshaydon/smproc

max_forks_repo_name: jameshaydon/smproc


text:
||| Example Queries over AList implemented graphs.
|||
||| TODO make query higher-order.
module Data.Graph.AList.Query

import Effects
import Effect.State
import Effect.StdIO

import Data.Graph.AList

import Data.Queue
import Data.Stack

%access public

-- --------------------------------------------------------------------- [ BFS ]
||| The effects used in a BFS.
BfsEffs : List EFFECT
BfsEffs = [ 'next ::: STATE (Queue Node),
            'seen ::: STATE (List Node),
            STDIO]

||| Traverse the given graph using a BFS, printing the visited nodes
||| in order of visit.
private
doTraceBFS : (Ord n, Show n) => Graph n e -> Eff () BfsEffs
doTraceBFS g = do
   q <- 'next :- get
   case popQ q of
     Nothing         => pure () -- Stop if all nodes have been traversed.
     Just (curr, q') => do
       'next :- put q'
       -- Do the thing we do at the nodes.
       putStrLn $ show curr

       -- Move on
       let es = getSuccs curr g
       doMoves es

       -- Repeat
       doTraceBFS g
  where
    doMove : Node -> Eff () BfsEffs
    doMove n = do
      visited <- 'seen :- get
      case elem n visited of
        True => pure ()
        False => do
          'seen :- update (\xs => [n] ++ xs)
          'next :- update (\xs => pushQ n xs)

    doMoves : Maybe (List Node) -> Eff () BfsEffs
    doMoves Nothing = pure ()
    doMoves (Just Nil) = pure ()
    doMoves (Just (e::es)) = do
       doMove e
       doMoves (Just es)

||| Traverse the given graph using a BFS, printing the visited nodes
||| in order of visit.
traceBfsIO : (Ord v, Show v) => Node -> Graph v e -> IO ()
traceBfsIO n g = runInit ['next := initQ n, 'seen := List.Nil, ()] $ doTraceBFS g

-- --------------------------------------------------------------------- [ DFS ]
||| The Effects used in a DFS.
DfsEffs : List EFFECT
DfsEffs = [ 'next ::: STATE (Stack Node),
            'seen ::: STATE (List Node),
            STDIO]

||| Traverse the given graph using a DFS, printing the visited nodes
||| in order of visit.
doTraceDFS : (Ord n, Show n) => Graph n e -> Eff () DfsEffs
doTraceDFS g = do
    s <- 'next :- get
    case popS s of
      Nothing         => pure ()
      Just (curr, s') => do
        'next :- put s'
        visited <- 'seen :- get
        case elem curr visited of
          True  => pure ()
          False => do
            putStrLn $ show curr
            let es = getSuccs curr g
            'seen :- update (\xs => [curr] ++ xs)
            'next :- update (\xs => pushSThings (fromMaybe Nil es) s)
            doTraceDFS g

||| Traverse the given graph using a DFS, printing the visited nodes
||| in order of visit.
traceDfsIO : (Ord v, Show v) => Node -> Graph v e -> IO ()
traceDfsIO n g = runInit ['next := initS n, 'seen := List.Nil, ()] $ doTraceDFS g
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module Test.TestOrdinalDate

import Data.Fin

import Test.TestUtil
import Data.Time.Calendar.OrdinalDate
import Data.Time.Calendar.Days
import Data.Time.Calendar.Gregorian

export
test_toOrdinalDate: IO ()
test_toOrdinalDate = do
  let result = toOrdinalDate (MkModifiedJulianDay 59053)
  assertEq "test_toOrdinalDate" result (2020, 205) (show result)

export
test_fromOrdinalDate: IO ()
test_fromOrdinalDate = do
  let result = fromOrdinalDate 2020 205
  assertEq "test_toOrdinalDate" result (MkModifiedJulianDay 59053) (show result)

export
test_fromOrdinalDateWithJust: IO ()
test_fromOrdinalDateWithJust = do
  let result = fromOrdinalDateValid 2020 205
  assertEq "test_fromOrdinalDateWithJust_1" result (Just (MkModifiedJulianDay 59053)) (show result)
  let result = fromOrdinalDateValid 2020 366
  assertEq "test_fromOrdinalDataWithJust_2" result (Just (MkModifiedJulianDay 59214)) (show result)

export
test_fromOrdinalDateWithNothing: IO ()
test_fromOrdinalDateWithNothing = do
  let result = fromOrdinalDateValid 2020 368
  assertEq "test_toOrdinalDateWithNothing" result Nothing (show result)

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
> module Functor.Predicates

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

* Naturality

> ||| What it means for a transformation to be natural
> Natural : {F, G : Type -> Type} ->
>           (Functor F) => (Functor G) =>
>           (t : {A : Type} -> F A -> G A) ->
>           Type
>
> Natural {F} {G} t = {A, B : Type} ->
>                     (f : A -> B) ->
>                     (x : F A) ->
>                     t (map f x) = map f  (t x)

> {-
> ||| What it means for a transformation to be natural
> Natural : {F, G : Type -> Type} ->
>           (Functor F) => (Functor G) =>
>           (t : (A : Type) -> F A -> G A) ->
>           Type
>
> Natural {F} {G} t = {A, B : Type} ->
>                     (f : A -> B) ->
>                     (x : F A) ->
>                     t B (map f x) = map f (t A x)
> -}

* Monotonicity

> ||| What it means for a measure to be monotone
> Monotone : {B, C : Type} -> {F : Type -> Type} -> (Functor F) =>
>            (LTE_B : B -> B -> Type) ->
>            (LTE_C : C -> C -> Type) ->
>            (measure : F B -> C) ->
>            Type
>
> Monotone {B} {C} {F} LTE_B LTE_C measure =
>   {A : Type} ->
>   (f : A -> B) ->
>   (g : A -> B) ->
>   (p : (a : A) -> f a `LTE_B` g a) ->
>   (x : F A) ->
>   measure (map f x) `LTE_C` measure (map g x)

> {-

> ---}


text:
module Resimp

-- IO operations which read a resource
data Reader : Type -> Type where
    MkReader : IO a -> Reader a

getReader : Reader a -> IO a
getReader (MkReader x) = x

ior : IO a -> Reader a
ior = MkReader

-- IO operations which update a resource
data Updater : Type -> Type where
    MkUpdater : IO a -> Updater a

getUpdater : Updater a -> IO a
getUpdater (MkUpdater x) = x

iou : IO a -> Updater a
iou = MkUpdater

-- IO operations which create a resource
data Creator : Type -> Type where
    MkCreator : IO a -> Creator a

getCreator : Creator a -> IO a
getCreator (MkCreator x) = x

ioc : IO a -> Creator a
ioc = MkCreator

infixr 5 :->

using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

  data Ty = R Type
          | Val Type
          | Choice Type Type
          | (:->) Type Ty

  interpTy : Ty -> Type
  interpTy (R t) = IO t
  interpTy (Val t) = t
  interpTy (Choice x y) = Either x y
  interpTy (a :-> b) = a -> interpTy b

  data HasType : Vect n Ty -> Fin n -> Ty -> Type where
       stop : HasType (a :: gam) fZ a
       pop  : HasType gam i b -> HasType (a :: gam) (fS i) b

  data Env : Vect n Ty -> Type where
       Nil : Env Nil
       (::) : interpTy a -> Env gam -> Env (a :: gam)

  envLookup : HasType gam i a -> Env gam -> interpTy a
  envLookup stop    (x :: xs) = x
  envLookup (pop k) (x :: xs) = envLookup k xs

  update : (gam : Vect n Ty) -> HasType gam i b -> Ty -> Vect n Ty
  update (x :: xs) stop    y = y :: xs
  update (x :: xs) (pop k) y = x :: update xs k y
  update Nil       stop    _ impossible

  total
  envUpdate : (p:HasType gam i a) -> (val:interpTy b) ->
              Env gam -> Env (update gam p b)
  envUpdate stop    val (x :: xs) = val :: xs
  envUpdate (pop k) val (x :: xs) = x :: envUpdate k val xs
  envUpdate stop    _   Nil impossible

  total
  envUpdateVal : (p:HasType gam i a) -> (val:b) ->
              Env gam -> Env (update gam p (Val b))
  envUpdateVal stop    val (x :: xs) = val :: xs
  envUpdateVal (pop k) val (x :: xs) = x :: envUpdateVal k val xs
  envUpdateVal stop    _   Nil impossible

  envTail : Env (a :: gam) -> Env gam
  envTail (x :: xs) = xs

  data Args  : Vect n Ty -> List Type -> Type where
       ANil  : Args gam []
       ACons : HasType gam i a ->
               Args gam as -> Args gam (interpTy a :: as)

  funTy : List Type -> Ty -> Ty
  funTy list.Nil t = t
  funTy (a :: as) t = a :-> funTy as t

  data Res : Vect n Ty -> Vect n Ty -> Ty -> Type where

{-- Resource creation and usage. 'Let' creates a resource - the type
    at the end means that the resource must have been consumed by the time
    it goes out of scope, where "consumed" simply means that it has been
    replaced with a value of type '()'. --}

       Let    : Creator (interpTy a) ->
                Res (a :: gam) (Val () :: gam') (R t) ->
                Res gam gam' (R t)
       Update : (a -> Updater b) -> (p:HasType gam i (Val a)) ->
                Res gam (update gam p (Val b)) (R ())
       Use    : (a -> Reader b) -> HasType gam i (Val a) ->
                Res gam gam (R b)

{-- Control structures --}

       Lift   : IO a -> Res gam gam (R a)
       Check  : (p:HasType gam i (Choice (interpTy a) (interpTy b))) ->
                (failure:Res (update gam p a) (update gam p c) t) ->
                (success:Res (update gam p b) (update gam p c) t) ->
                Res gam (update gam p c) t
       While  : Res gam gam (R Bool) ->
                Res gam gam (R ()) -> Res gam gam (R ())
       Return : a -> Res gam gam (R a)
       (>>=)  : Res gam gam'  (R a) -> (a -> Res gam' gam'' (R t)) ->
                Res gam gam'' (R t)

  ioret : a -> IO a
  ioret = return

  iolift : IO a -> Res gam gam (R a)
  iolift = Lift

  interp : Env gam -> (e : Res gam gam' t) ->
           (Env gam' -> interpTy t -> IO u) -> IO u

  interp env (Let val scope) k
     = do x <- getCreator val
          interp (x :: env) scope
                   (\env', scope' => k (envTail env') scope')
  interp env (Update method x) k
      = do x' <- getUpdater (method (envLookup x env))
           k (envUpdateVal x x' env) (return ())
  interp env (Use method x) k
      = do x' <- getReader (method (envLookup x env))
           k env (return x')
  interp env (Lift io) k
     = k env io
  interp env (Check x left right) k =
     either (\a => interp (envUpdate x a env) left k)
            (\b => interp (envUpdate x b env) right k)
            (envLookup x env)
  interp env (While test body) k
     = interp env test
          (\env', result =>
             do r <- result
                if (not r)
                   then (k env' (return ()))
                   else (interp env' body
                        (\env'', body' =>
                           do v <- body' -- make sure it's evalled
                              interp env'' (While test body) k )))
  interp env (Return v) k = k env (return v)
  interp env (v >>= f) k
     = interp env v (\env', v' => do n <- v'
                                     interp env' (f n) k)

--   run : {static} Res [] [] (R t) -> IO t
--   run prog = interp [] prog (\env, res => res)

syntax run [prog] = interp [] prog (\env, res => res)

dsl res
   variable = id
   let = Let
   index_first = stop
   index_next = pop

syntax RES [x] = {gam:Vect n Ty} -> Res gam gam (R x)

max_stars_repo_name: silky/idris-demos

max_issues_repo_name: silky/idris-demos

max_forks_repo_name: silky/idris-demos


text:
module Main

main : IO ()
main = repl "> " reverse

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Text.PrettyPrint.Prettyprinter.Symbols

import Text.PrettyPrint.Prettyprinter.Doc

%default total

export
squote : Doc ann
squote = pretty '\''

export
dquote : Doc ann
dquote = pretty '"'

export
lparen : Doc ann
lparen = pretty '('

export
rparen : Doc ann
rparen = pretty ')'

export
langle : Doc ann
langle = pretty '<'

export
rangle : Doc ann
rangle = pretty '>'

export
lbracket : Doc ann
lbracket = pretty '['

export
rbracket : Doc ann
rbracket = pretty ']'

export
lbrace : Doc ann
lbrace = pretty '{'

export
rbrace : Doc ann
rbrace = pretty '}'

export
semi : Doc ann
semi = pretty ';'

export
colon : Doc ann
colon = pretty ':'

export
comma : Doc ann
comma = pretty ','

export
space : Doc ann
space = pretty ' '

export
dot : Doc ann
dot = pretty '.'

export
slash : Doc ann
slash = pretty '/'

export
backslash : Doc ann
backslash = pretty '\\'

export
equals : Doc ann
equals = pretty '='

export
pipe : Doc ann
pipe = pretty '|'

export
squotes : Doc ann -> Doc ann
squotes = enclose squote squote

export
dquotes : Doc ann -> Doc ann
dquotes = enclose dquote dquote

export
parens : Doc ann -> Doc ann
parens = enclose lparen rparen

export
angles : Doc ann -> Doc ann
angles = enclose langle rangle

export
brackets : Doc ann -> Doc ann
brackets = enclose lbracket rbracket

export
braces : Doc ann -> Doc ann
braces = enclose lbrace rbrace