text:
||| The content of this module is based on the
||| tutorial post about [refined primitives](../../Doc/Primitives.md).
module Language.Reflection.Refined

import public Language.Reflection.Refined.Util
import public Language.Reflection.Derive

%default total

--------------------------------------------------------------------------------
--          Elab Scripts
--------------------------------------------------------------------------------

||| Creates an `Eq` implementation for the given datatype
||| by using the given accessor function.
|||
||| This is hardly useful on its own but convenient when
||| combined with other interface implementors.
|||
||| In some occasions it is useful to have one or several
||| phantom types for the refined type. Therefore, the exact
||| type should be given as a `TTImp`.
|||
||| ```idris example
||| record AtomicNr a where
|||   constructor MkAtomicNr
|||   value : Int
|||   0 inBounds : So (1 <= value && value <= 118)
|||
||| %runElab refinedEq "AtomicNr" `(AtomicNr a) `{{value}}
||| ```
export
refinedEq : (dataType : String) -> (dt : TTImp) -> (accessor : Name) -> Elab ()
refinedEq dt t accessor =
  let eqFun   = UN $ Basic $ "implEq"   ++ dt
      acc     = var accessor

   in declare
        [ interfaceHint Public eqFun `(Eq ~(t))
        , def eqFun [patClause (var eqFun) `(mkEq ((==) `on` ~(acc)))]
        ]

||| Creates an `Ord` implementation for the given datatype
||| by using the given accessor function.
|||
||| This is hardly useful on its own but convenient when
||| combined with other interface implementors.
|||
||| ```idris example
||| record AtomicNr a where
|||   constructor MkAtomicNr
|||   value : Int
|||   0 inBounds : So (1 <= value && value <= 118)
|||
||| %runElab refinedOrd "AtomicNr" `(AtomicNr a) `{{value}}
||| ```
export
refinedOrd : (dataType : String) -> (dt : TTImp) -> (accessor : Name) -> Elab ()
refinedOrd dt t accessor =
  let ordFun  = UN $ Basic $ "implOrd"  ++ dt
      acc     = var accessor

   in declare
        [ interfaceHint Public ordFun `(Ord ~(t))
        , def ordFun [patClause (var ordFun) `(mkOrd (compare `on` ~(acc)))]
        ]

||| Creates a `Show` implementation for the given datatype
||| by using the given accessor function.
|||
||| This is hardly useful on its own but convenient when
||| combined with other interface implementors.
|||
||| ```idris example
||| record AtomicNr a where
|||   constructor MkAtomicNr
|||   value : Int
|||   0 inBounds : So (1 <= value && value <= 118)
|||
||| %runElab refinedShow "AtomicNr" `(AtomicNr a) `{{value}}
||| ```
export
refinedShow : (dataType : String) -> (dt : TTImp) -> (accessor : Name) -> Elab ()
refinedShow dt t accessor =
  let showFun = UN $ Basic $ "implShow" ++ dt
      acc     = var accessor

   in declare
        [ interfaceHint Public showFun `(Show ~(t))
        , def showFun [patClause (var showFun)
                       `(mkShowPrec (\p => showPrec p . ~(acc)))]
        ]

||| Convenience function combining `refinedEq`, `refinedOrd`,
||| and `refinedShow`.
export
refinedEqOrdShow :  (dataType : String)
                 -> (dt : TTImp)
                 -> (accessor : Name)
                 -> Elab ()
refinedEqOrdShow dt t acc = do refinedEq dt t acc
                               refinedOrd dt t acc
                               refinedShow dt t acc

||| This creates `Eq`, `Ord`, and `Show` implementations as
||| well as conversion functions for a refined integral number.
|||
||| Conversion functions are called `refine` and `fromInteger`
||| and are put in their own namespace, named after the
||| data type's name.
|||
||| ```idris example
||| record AtomicNr a where
|||   constructor MkAtomicNr
|||   value : Int
|||   0 inBounds : So (1 <= value && value <= 118)
|||
||| %runElab refinedIntegral "AtomicNr"
|||                          `(AtomicNr a)
|||                          `{{MkAtomicNr}}
|||                          `{{value}}
|||                          `(Int)
||| ```
|||
||| The above will result in the following declarations being generated:
|||
||| ```idris example
||| Eq AtomicNr where
|||   (==) = (==) `on` value
|||
||| Ord AtomicNr where
|||   compare = compare `on` value
|||
||| Show AtomicNr where
|||   showPrec p = showPrec p . value
|||
||| namespace AtomicNr
|||   refine : Int -> Maybe AtomicNr
|||   refine = refineSo MkAtomicNr
|||
|||   fromInteger :  (v : Integer)
|||               -> {auto 0 _: IsJust (refine $ fromInteger v)}
|||               -> AtomicNr
|||   fromInteger v = fromJust (refine $ fromInteger v)
||| ```
export
refinedIntegral :  (dataType : String)
                -> (dt       : TTImp)
                -> (con      : Name)
                -> (accessor : Name)
                -> (tpe      : TTImp)
                -> Elab ()
refinedIntegral dt t con acc tpe =
  let ns   = MkNS [dt]

      -- this has to be namespaced
      -- to avoid disambiguities when being used
      -- in fromInteger
      refineNS = var $ NS ns (UN $ Basic "refine")

   in refinedEqOrdShow dt t acc >>
      declare
        [ INamespace EmptyFC ns
          `[ public export
             refine : ~(tpe) -> Maybe ~(t)
             refine = refineSo ~(var con)

             public export
             fromInteger :  (n : Integer)
                         -> {auto 0 _: IsJust (~(refineNS) $ fromInteger n)}
                         -> ~(t)
             fromInteger n = fromJust (refine $ fromInteger n)
           ]
        ]

export
refinedIntegralDflt : (dataType : String) -> (tpe : TTImp) -> Elab ()
refinedIntegralDflt dt tpe =
  refinedIntegral dt (varStr dt) (UN $ Basic $ "Mk" ++ dt) `{value} tpe

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
|||
||| ```idris example
||| record AtomicNr where
|||   constructor MkAtomicNr
|||   value : Int
|||   0 inBounds : So (1 <= value && value <= 118)
|||
||| %runElab refinedInt "AtomicNr"
||| ```
export
refinedInt : (dataType : String) -> Elab ()
refinedInt dt = refinedIntegralDflt dt `(Int)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export
refinedBits8 : (dataType : String) -> Elab ()
refinedBits8 dt = refinedIntegralDflt dt `(Bits8)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export
refinedBits16 : (dataType : String) -> Elab ()
refinedBits16 dt = refinedIntegralDflt dt `(Bits16)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export
refinedBits32 : (dataType : String) -> Elab ()
refinedBits32 dt = refinedIntegralDflt dt `(Bits32)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export
refinedBits64 : (dataType : String) -> Elab ()
refinedBits64 dt = refinedIntegralDflt dt `(Bits64)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export
refinedInt8 : (dataType : String) -> Elab ()
refinedInt8 dt = refinedIntegralDflt dt `(Int8)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export
refinedInt16 : (dataType : String) -> Elab ()
refinedInt16 dt = refinedIntegralDflt dt `(Int16)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export
refinedInt32 : (dataType : String) -> Elab ()
refinedInt32 dt = refinedIntegralDflt dt `(Int32)

||| Specialized version of `refinedIntegral` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export
refinedInt64 : (dataType : String) -> Elab ()
refinedInt64 dt = refinedIntegralDflt dt `(Int64)

||| This creates `Eq`, `Ord`, and `Show` implementations as
||| well as conversion functions for a refined floating point
||| number.
|||
||| Conversion functions are called `refine` and `fromDouble`
||| and are put in their own namespace, named after the
||| data type's name.
|||
||| ```idris example
||| record Abundance a where
|||   constructor MkAbundance
|||   value : Double
|||   0 inBounds : So (0 < value && value <= 1)
|||
||| %runElab refinedFloating "Abundance" `(Abundance a) `{{MkAbundance}} `{{value}}
||| ```
|||
||| The above will result in the following declarations being generated:
|||
||| ```idris example
||| Eq Abundance where
|||   (==) = (==) `on` value
|||
||| Ord Abundance where
|||   compare = compare `on` value
|||
||| Show Abundance where
|||   showPrec p = showPrec p . value
|||
||| namespace Abundance
|||   refine : Double -> Maybe Abundance
|||   refine = refineSo MkAbundance
|||
|||   fromDouble :  (v : Double)
|||              -> {auto 0 _: IsJust (refine v)}
|||              -> Abundance
|||   fromDouble v = fromJust (refine v)
||| ```
export
refinedFloating :  (dataType : String)
                -> (dt       : TTImp)
                -> (con      : Name)
                -> (accessor : Name)
                -> Elab ()
refinedFloating dt t con acc =
  let ns   = MkNS [dt]

      -- this has to be namespaced
      -- to avoid disambiguities when being used
      -- in fromInteger
      refineNS = var $ NS ns (UN $ Basic "refine")

   in refinedEqOrdShow dt t acc >>
      declare
        [ INamespace EmptyFC ns
          `[ public export
             refine : Double -> Maybe ~(t)
             refine = refineSo ~(var con)

             public export
             fromDouble :  (n : Double)
                        -> {auto 0 _: IsJust (~(refineNS) n)}
                        -> ~(t)
             fromDouble n = fromJust (refine n)
           ]
        ]

||| Convenience version of `refinedFloating` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export
refinedDouble : (dataType : String) -> Elab ()
refinedDouble dt = refinedFloating dt (varStr dt) (UN $ Basic $ "Mk" ++ dt) `{value}

||| This creates `Eq`, `Ord`, and `Show` implementations as
||| well as conversion functions for a refined string value.
|||
||| Conversion functions are called `refine` and `fromString`
||| and are put in their own namespace, named after the
||| data type's name.
|||
||| ```idris example
||| record Html a where
|||   constructor MkHtml
|||   value : String
|||   0 inBounds : So (isValidHtml value)
|||
||| %runElab refinedText "Html" `(Html a) `{{MkHtml}} `{{value}}
||| ```
|||
||| The above will result in the following declarations being generated:
|||
||| ```idris example
||| Eq Html where
|||   (==) = (==) `on` value
|||
||| Ord Html where
|||   compare = compare `on` value
|||
||| Show Html where
|||   showPrec p = showPrec p . value
|||
||| namespace Html
|||   refine : String -> Maybe Html
|||   refine = refineSo MkHtml
|||
|||   fromString :  (v : String)
|||              -> {auto 0 _: IsJust (refine v)}
|||              -> Html
|||   fromString v = fromJust (refine v)
||| ```
export
refinedText :  (dataType : String)
            -> (dt       : TTImp)
            -> (con      : Name)
            -> (accessor : Name)
            -> Elab ()
refinedText dt t con acc =
  let ns   = MkNS [dt]

      -- this has to be namespaced
      -- to avoid disambiguities when being used
      -- in fromInteger
      refineNS = var $ NS ns (UN $ Basic "refine")

   in refinedEqOrdShow dt t acc >>
      declare
        [ INamespace EmptyFC ns
          `[ public export
             refine : String -> Maybe ~(t)
             refine = refineSo ~(var con)

             public export
             fromString :  (n : String)
                        -> {auto 0 _: IsJust (~(refineNS) n)}
                        -> ~(t)
             fromString n = fromJust (refine n)
           ]
        ]

||| Convenience version of `refinedText` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Int is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export
refinedString : (dataType : String) -> Elab ()
refinedString dt = refinedText dt (varStr dt) (UN $ Basic $ "Mk" ++ dt) `{value}

||| This creates `Eq`, `Ord`, and `Show` implementations as
||| well as conversion functions for a refined charater.
|||
||| Conversion functions are called `refine` and `fromChar`
||| and are put in their own namespace, named after the
||| data type's name.
|||
||| ```idris example
||| record Digit a where
|||   constructor MkDigit
|||   value : Char
|||   0 inBounds : So (isDigit value)
|||
||| %runElab refinedText "Digit" `(Digit a) `{{MkDigit}} `{{value}}
||| ```
|||
||| The above will result in the following declarations being generated:
|||
||| ```idris example
||| Eq Digit where
|||   (==) = (==) `on` value
|||
||| Ord Digit where
|||   compare = compare `on` value
|||
||| Show Digit where
|||   showPrec p = showPrec p . value
|||
||| namespace Digit
|||   refine : Char -> Maybe Digit
|||   refine = refineSo MkDigit
|||
|||   fromChar :  (v : Char)
|||            -> {auto 0 _: IsJust (refine v)}
|||            -> Digit
|||   fromChar v = fromJust (refine v)
||| ```
export
refinedCharacter :  (dataType : String)
                 -> (dt       : TTImp)
                 -> (con      : Name)
                 -> (accessor : Name)
                 -> Elab ()
refinedCharacter dt t con acc =
  let ns   = MkNS [dt]

      -- this has to be namespaced
      -- to avoid disambiguities when being used
      -- in fromInteger
      refineNS = var $ NS ns (UN $ Basic "refine")

   in refinedEqOrdShow dt t acc >>
      declare
        [ INamespace EmptyFC ns
          `[ public export
             refine : Char -> Maybe ~(t)
             refine = refineSo ~(var con)

             public export
             fromChar :  (n : Char)
                      -> {auto 0 _: IsJust (~(refineNS) n)}
                      -> ~(t)
             fromChar n = fromJust (refine n)
           ]
        ]

||| Convenience version of `refinedCharacter` for data types,
||| which adhere to the following conventions:
|||
|||  * If a data type's name is `Foo` its constructor is named `MkFoo`.
|||  * The field accessor of the wrapped Char is named `value`.
|||  * The proof of validity consists of a single zero quantity `So`.
export
refinedChar : (dataType : String) -> Elab ()
refinedChar dt = refinedCharacter dt (varStr dt) (UN $ Basic $ "Mk" ++ dt) `{value}


text:
module Data.Time.Clock.Internal.SystemTime
    -- ( SystemTime(..)
    -- , getSystemTime
    -- , getTime_resolution
    -- , getTAISystemTime
    -- ) where

--import Data.Bits32

--import Data.Data
--import Control.DeepSeq
--import Data.Int (Int64)
import Data.Time.Clock.Internal.DiffTime
--import Data.Word
--#include "HsTimeConfig.h"

import Internal.CTimespec
import Data.Time.Clock.Internal.Fixed

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

-- | 'SystemTime' is time returned by system clock functions.
-- Its semantics depends on the clock function, but the epoch is typically the beginning of 1970.
-- Note that 'systemNanoseconds' of 1E9 to 2E9-1 can be used to represent leap seconds.
public export
record SystemTime where
  constructor MkSystemTime
  systemSeconds: Integer
  systemNanoseconds: Integer

-- | Get the system time, epoch start of 1970 UTC, leap-seconds ignored.
-- 'getSystemTime' is typically much faster than 'getCurrentTime'.
export
getSystemTime: IO SystemTime
getSystemTime = do
  (MkCTimeSpec x y) <- clock_gettime
  pure $ MkSystemTime x y

-- | The resolution of 'getSystemTime', 'getCurrentTime', 'getPOSIXTime'
-- | TODO: Fix this.
--getTime_resolution: DiffTime
-- getTime_resolution = 100E-9 -- 100ns

timespecToSystemTime: CTimeSpec -> SystemTime
timespecToSystemTime (MkCTimeSpec s ns) = (MkSystemTime s ns)

-- TODO: Currently nano second resolution does not work
timespecToDiffTime: CTimeSpec -> DiffTime
timespecToDiffTime (MkCTimeSpec s ns) = MkDiffTime (MkFixed (s)) -- + (ns  * 1E-9)))

--clockGetSystemTime :: ClockID -> IO SystemTime
--clockGetSystemTime clock = fmap timespecToSystemTime $ clockGetTime clock

--getSystemTime = clockGetSystemTime clock_REALTIME

--getTime_resolution = timespecToDiffTime realtimeRes

-- Use gettimeofday
-- getTime_resolution = 1E-6 -- microsecond

ext: idr

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module TyTTP.Core.Error

public export
interface Error e where
  message : e -> String

export
Error String where
  message = id

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Main

import IdrisScript
import IdrisScript.Objects

main : JS_IO ()
main = do
  obj <- empty

  setProperty "foo" (toJS {from=Int}{to=JSNumber} 666)  obj
  setProperty "bar" (toJS {from=Int}{to=JSNumber} 1337) obj

  keys <- keys obj

  log keys
  log obj

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module Main

import Go

%include Go "strings"
upper : String -> String
upper s = unsafePerformIO $
  gocall (Function "strings.ToUpper") (String -> GIO String) s

trim : String -> String -> String
trim s cutset = unsafePerformIO $
  gocall (Function "strings.Trim") (String -> String -> GIO String) s cutset

main : GIO ()
main = do
  putStrLn' $ upper "foo"
  putStrLn' $ trim "foobar" "fr"

max_stars_repo_name: Trundle/idris-go

max_issues_repo_name: Trundle/idris-go

max_forks_repo_name: Trundle/idris-go


text:
module Multiplicities

import Data.Vect

append : Vect n a -> Vect m a -> Vect (n + m) a
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

{-
  Idris is based on QTT, which uses Linear Logic. As such, Idris supports three levels of "multiplicities":
    - 0 meaning that the value is erased at runtime (this applies to implicits as well)
    - 1 meaning that the value is consumed exactly once at runtime, and
    - no multiplicity annotation, meaning unrestrained multiplicity.
-}

-- identical to the definition above, just explicit
appendExplicit : { 0 n : Nat } -> { 0 m : Nat } -> Vect n a -> Vect m a -> Vect (n + m) a
appendExplicit [] ys = ys
appendExplicit (x :: xs) ys = x :: appendExplicit xs ys

-- linearity

-- this is not possible
--duplicate : (1 _ : a) -> (a, a)
--duplicate x = (x, x)

data Lin : Type -> Type where
  MkLin : (1 _ : a) -> Lin a

getLin : (1 _ : Lin a) -> a
getLin (MkLin x) = x

data Unr : Type -> Type where
  MkUnr : a -> Unr a

getUnr : Unr a -> a
getUnr (MkUnr x) = x

-- erasure

vlen :  { n : _ } -> Vect n a -> Nat
vlen xs = n

sumLengths : { m, n : _ } -> Vect m a -> Vect n a -> Nat
sumLengths xs ys = m + n

-- it is an error to try pattern matching on an erased argument (i.e., an argument with multiplicity 0), unless
-- that argument's value can be uniquely inferred from another argument

-- so this does not work
--badNot : (0 x : Bool) -> Bool
--badNot False = True
--badNot True = False

-- but this works since the dependent argument (SBool x) allows us to uniquely infer a value for the first argument

data SBool : Bool -> Type where
  SFalse: SBool False
  STrue : SBool True

sNot : (0 x : Bool) -> SBool x -> Bool
sNot False SFalse = True
sNot True STrue = False
sNot False STrue impossible
sNot True SFalse impossible

-- pattern matching on types

showType : Type -> String
showType Int = "Int"
showType (List a) = "List of " ++ showType a
showType (Vect _ a) = "Vect of " ++ showType a
showType (Nat -> a) = "Function from Nat to " ++ showType (a Z)
showType _ = "something else"

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Core.UnifyState

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.FC
import Core.Normalise
import Core.Options
import Core.TT
import Core.TTC
import Core.Value
import Libraries.Utils.Binary

import Libraries.Data.IntMap
import Data.List
import Libraries.Data.NameMap
import Libraries.Data.StringMap

%default covering

public export
data Constraint : Type where
     -- An unsolved constraint, noting two terms which need to be convertible
     -- in a particular environment
     MkConstraint : {vars : _} ->
                    FC ->
                    (withLazy : Bool) ->
                    (env : Env Term vars) ->
                    (x : NF vars) -> (y : NF vars) ->
                    Constraint
     -- An unsolved sequence of constraints, arising from arguments in an
     -- application where solving later constraints relies on solving earlier
     -- ones
     MkSeqConstraint : {vars : _} ->
                       FC ->
                       (env : Env Term vars) ->
                       (xs : List (NF vars)) ->
                       (ys : List (NF vars)) ->
                       Constraint
     -- A resolved constraint
     Resolved : Constraint

-- a constraint on the LHS arising from checking an argument in a position
-- where we expect a polymorphic type. If, in the end, the expected type is
-- polymorphic but the argument is concrete, then the pattern match is too
-- specific
public export
data PolyConstraint : Type where
     MkPolyConstraint : {vars : _} ->
                        FC -> Env Term vars ->
                        (arg : Term vars) ->
                        (expty : NF vars) ->
                        (argty : NF vars) -> PolyConstraint

-- Explanation for why an elaborator has been delayed. It's helpful to know
-- the reason for a delay (I wish airlines and train companies knew this)
-- because it means we can choose to run only a subset (e.g. it's sometimes
-- useful to just retry the case blocks) and because we can run them in the
-- order that prioritises the best error messages.
public export
data DelayReason
      = CaseBlock
      | Ambiguity
      | RecordUpdate
      | Rewrite
      | LazyDelay

public export
Eq DelayReason where
  CaseBlock == CaseBlock = True
  Ambiguity == Ambiguity = True
  RecordUpdate == RecordUpdate = True
  Rewrite == Rewrite = True
  LazyDelay == LazyDelay = True
  _ == _ = False

public export
Ord DelayReason where
  compare x y = compare (tag x) (tag y)
    where
      -- The ordering here is chosen to give the most likely useful error
      -- messages first. For example, often the real reason for a strange error
      -- is because there's an ambiguity that can't be resolved.
      tag : DelayReason -> Int
      tag CaseBlock = 1 -- we can often proceed even if there's still some
                        -- ambiguity
      tag Ambiguity = 2
      tag LazyDelay = 3
      tag RecordUpdate = 4
      tag Rewrite = 5

public export
record UState where
  constructor MkUState
  holes : IntMap (FC, Name) -- All metavariables with no definition yet.
                            -- 'Int' is the 'Resolved' name
  guesses : IntMap (FC, Name) -- Names which will be defined when constraints solved
                              -- (also includes auto implicit searches)
  currentHoles : IntMap (FC, Name) -- Holes introduced this elaboration session
  delayedHoles : IntMap (FC, Name) -- Holes left unsolved after an elaboration,
                                   -- so we need to check again at the end whether
                                   -- they have been solved later. Doesn't include
                                   -- user defined hole names, which don't need
                                   -- to have been solved
  constraints : IntMap Constraint -- map for finding constraints by ID
  noSolve : IntMap () -- Names not to solve
                      -- If we're checking an LHS, then checking an argument can't
                      -- solve its own type, or we might end up with something
                      -- less polymorphic than it should be
  polyConstraints : List PolyConstraint -- constraints which need to be solved
                      -- successfully to check an LHS is polymorphic enough
  dotConstraints : List (Name, DotReason, Constraint) -- dot pattern constraints
  nextName : Int
  nextConstraint : Int
  delayedElab : List (DelayReason, Int, NameMap (), Core ClosedTerm)
                -- Elaborators which we need to try again later, because
                -- we didn't have enough type information to elaborate
                -- successfully yet.
                -- The 'Int' is the resolved name.
                -- NameMap () is the set of local hints at the point of delay
  logging : Bool

export
initUState : UState
initUState = MkUState
  { holes = empty
  , guesses = empty
  , currentHoles = empty
  , delayedHoles = empty
  , constraints = empty
  , noSolve = empty
  , polyConstraints = []
  , dotConstraints = []
  , nextName = 0
  , nextConstraint = 0
  , delayedElab = []
  , logging = False
  }

export
data UST : Type where

export
resetNextVar : {auto u : Ref UST UState} ->
               Core ()
resetNextVar
    = do ust <- get UST
         put UST (record { nextName = 0 } ust)

-- Generate a global name based on the given root, in the current namespace
export
genName : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          String -> Core Name
genName str
    = do ust <- get UST
         put UST (record { nextName $= (+1) } ust)
         n <- inCurrentNS (MN str (nextName ust))
         pure n

-- Generate a global name based on the given name, in the current namespace
export
genMVName : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            Name -> Core Name
genMVName (UN str) = genName (displayUserName str)
genMVName (MN str _) = genName str
genMVName n
    = do ust <- get UST
         put UST (record { nextName $= (+1) } ust)
         mn <- inCurrentNS (MN (show n) (nextName ust))
         pure mn

-- Generate a unique variable name based on the given root
export
genVarName : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             String -> Core Name
genVarName str
    = do ust <- get UST
         put UST (record { nextName $= (+1) } ust)
         pure (MN str (nextName ust))

-- Again, for case names
export
genCaseName : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              String -> Core Name
genCaseName root
    = do ust <- get UST
         put UST (record { nextName $= (+1) } ust)
         inCurrentNS (CaseBlock root (nextName ust))

export
genWithName : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              String -> Core Name
genWithName root
    = do ust <- get UST
         put UST (record { nextName $= (+1) } ust)
         inCurrentNS (WithBlock root (nextName ust))

addHoleName : {auto u : Ref UST UState} ->
              FC -> Name -> Int -> Core ()
addHoleName fc n i
    = do ust <- get UST
         put UST (record { holes $= insert i (fc, n),
                           currentHoles $= insert i (fc, n) } ust)

addGuessName : {auto u : Ref UST UState} ->
               FC -> Name -> Int -> Core ()
addGuessName fc n i
    = do ust <- get UST
         put UST (record { guesses $= insert i (fc, n)  } ust)

export
removeHole : {auto u : Ref UST UState} ->
             Int -> Core ()
removeHole n
    = do ust <- get UST
         put UST (record { holes $= delete n,
                           currentHoles $= delete n,
                           delayedHoles $= delete n } ust)

export
removeHoleName : {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 Name -> Core ()
removeHoleName n
    = do defs <- get Ctxt
         let Just i = getNameID n (gamma defs)
             | Nothing => pure ()
         removeHole i

export
addNoSolve : {auto u : Ref UST UState} ->
             Int -> Core ()
addNoSolve i
    = do ust <- get UST
         put UST (record { noSolve $= insert i () } ust)

export
removeNoSolve : {auto u : Ref UST UState} ->
                Int -> Core ()
removeNoSolve i
    = do ust <- get UST
         put UST (record { noSolve $= delete i } ust)

export
saveHoles : {auto u : Ref UST UState} ->
            Core (IntMap (FC, Name))
saveHoles
    = do ust <- get UST
         put UST (record { currentHoles = empty } ust)
         pure (currentHoles ust)

export
restoreHoles : {auto u : Ref UST UState} ->
               IntMap (FC, Name) -> Core ()
restoreHoles hs
    = do ust <- get UST
         put UST (record { currentHoles = hs } ust)

export
removeGuess : {auto u : Ref UST UState} ->
              Int -> Core ()
removeGuess n
    = do ust <- get UST
         put UST (record { guesses $= delete n } ust)

-- Get all of the hole data
export
getHoles : {auto u : Ref UST UState} ->
           Core (IntMap (FC, Name))
getHoles
    = do ust <- get UST
         pure (holes ust)

-- Get all of the guess data
export
getGuesses : {auto u : Ref UST UState} ->
           Core (IntMap (FC, Name))
getGuesses
    = do ust <- get UST
         pure (guesses ust)

-- Get the hole data for holes in the current elaboration session
-- (i.e. since the last 'saveHoles')
export
getCurrentHoles : {auto u : Ref UST UState} ->
                  Core (IntMap (FC, Name))
getCurrentHoles
    = do ust <- get UST
         pure (currentHoles ust)

export
isHole : {auto u : Ref UST UState} ->
         Int -> Core Bool
isHole i
    = do ust <- get UST
         pure (maybe False (const True) (lookup i (holes ust)))

export
isCurrentHole : {auto u : Ref UST UState} ->
                Int -> Core Bool
isCurrentHole i
    = do ust <- get UST
         pure (maybe False (const True) (lookup i (currentHoles ust)))

export
setConstraint : {auto u : Ref UST UState} ->
                Int -> Constraint -> Core ()
setConstraint cid c
    = do ust <- get UST
         put UST (record { constraints $= insert cid c } ust)

export
deleteConstraint : {auto u : Ref UST UState} ->
                Int -> Core ()
deleteConstraint cid
    = do ust <- get UST
         put UST (record { constraints $= delete cid } ust)

export
addConstraint : {auto u : Ref UST UState} ->
                {auto c : Ref Ctxt Defs} ->
                Constraint -> Core Int
addConstraint constr
    = do ust <- get UST
         let cid = nextConstraint ust
         put UST (record { constraints $= insert cid constr,
                           nextConstraint = cid+1 } ust)
         pure cid

export
addDot : {vars : _} ->
         {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         FC -> Env Term vars -> Name -> Term vars -> DotReason -> Term vars ->
         Core ()
addDot fc env dotarg x reason y
    = do ust <- get UST
         defs <- get Ctxt
         xnf <- nf defs env x
         ynf <- nf defs env y
         put UST (record { dotConstraints $=
                             ((dotarg, reason, MkConstraint fc False env xnf ynf) ::)
                         } ust)

export
addPolyConstraint : {vars : _} ->
                    {auto u : Ref UST UState} ->
                    FC -> Env Term vars -> Term vars -> NF vars -> NF vars ->
                    Core ()
addPolyConstraint fc env arg x@(NApp _ (NMeta _ _ _) _) y
    = do ust <- get UST
         put UST (record { polyConstraints $= ((MkPolyConstraint fc env arg x y) ::) } ust)
addPolyConstraint fc env arg x y
    = pure ()

mkConstantAppArgs : {vars : _} ->
                    Bool -> FC -> Env Term vars ->
                    (wkns : List Name) ->
                    List (Term (wkns ++ (vars ++ done)))
mkConstantAppArgs lets fc [] wkns = []
mkConstantAppArgs {done} {vars = x :: xs} lets fc (b :: env) wkns
    = let rec = mkConstantAppArgs {done} lets fc env (wkns ++ [x]) in
          if lets || not (isLet b)
             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
                  rewrite (appendAssociative wkns [x] (xs ++ done)) in rec
             else rewrite (appendAssociative wkns [x] (xs ++ done)) in rec

mkConstantAppArgsSub : {vars : _} ->
                       Bool -> FC -> Env Term vars ->
                       SubVars smaller vars ->
                       (wkns : List Name) ->
                       List (Term (wkns ++ (vars ++ done)))
mkConstantAppArgsSub lets fc [] p wkns = []
mkConstantAppArgsSub {done} {vars = x :: xs}
                        lets fc (b :: env) SubRefl wkns
    = rewrite appendAssociative wkns [x] (xs ++ done) in
              mkConstantAppArgs lets fc env (wkns ++ [x])
mkConstantAppArgsSub {done} {vars = x :: xs}
                        lets fc (b :: env) (DropCons p) wkns
    = rewrite appendAssociative wkns [x] (xs ++ done) in
              mkConstantAppArgsSub lets fc env p (wkns ++ [x])
mkConstantAppArgsSub {done} {vars = x :: xs}
                        lets fc (b :: env) (KeepCons p) wkns
    = let rec = mkConstantAppArgsSub {done} lets fc env p (wkns ++ [x]) in
          if lets || not (isLet b)
             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
                  rewrite appendAssociative wkns [x] (xs ++ done) in rec
             else rewrite appendAssociative wkns [x] (xs ++ done) in rec

mkConstantAppArgsOthers : {vars : _} ->
                          Bool -> FC -> Env Term vars ->
                          SubVars smaller vars ->
                          (wkns : List Name) ->
                          List (Term (wkns ++ (vars ++ done)))
mkConstantAppArgsOthers lets fc [] p wkns = []
mkConstantAppArgsOthers {done} {vars = x :: xs}
                        lets fc (b :: env) SubRefl wkns
    = rewrite appendAssociative wkns [x] (xs ++ done) in
              mkConstantAppArgsOthers lets fc env SubRefl (wkns ++ [x])
mkConstantAppArgsOthers {done} {vars = x :: xs}
                        lets fc (b :: env) (KeepCons p) wkns
    = rewrite appendAssociative wkns [x] (xs ++ done) in
              mkConstantAppArgsOthers lets fc env p (wkns ++ [x])
mkConstantAppArgsOthers {done} {vars = x :: xs}
                        lets fc (b :: env) (DropCons p) wkns
    = let rec = mkConstantAppArgsOthers {done} lets fc env p (wkns ++ [x]) in
          if lets || not (isLet b)
             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
                  rewrite appendAssociative wkns [x] (xs ++ done) in rec
             else rewrite appendAssociative wkns [x] (xs ++ done) in rec

export
applyTo : {vars : _} ->
          FC -> Term vars -> Env Term vars -> Term vars
applyTo fc tm env
  = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

export
applyToFull : {vars : _} ->
              FC -> Term vars -> Env Term vars -> Term vars
applyToFull fc tm env
  = let args = reverse (mkConstantAppArgs {done = []} True fc env []) in
        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

export
applyToSub : {vars : _} ->
             FC -> Term vars -> Env Term vars ->
             SubVars smaller vars -> Term vars
applyToSub fc tm env sub
  = let args = reverse (mkConstantAppArgsSub {done = []} True fc env sub []) in
        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

export
applyToOthers : {vars : _} ->
                FC -> Term vars -> Env Term vars ->
                SubVars smaller vars -> Term vars
applyToOthers fc tm env sub
  = let args = reverse (mkConstantAppArgsOthers {done = []} True fc env sub []) in
        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

-- Create a new metavariable with the given name and return type,
-- and return a term which is the metavariable applied to the environment
-- (and which has the given type)
-- Flag whether cycles are allowed in the result, and whether to abstract
-- over lets
export
newMetaLets : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount ->
              Env Term vars -> Name -> Term vars -> Def ->
              Bool -> Bool ->
              Core (Int, Term vars)
newMetaLets {vars} fc rig env n ty def nocyc lets
    = do let hty = if lets then abstractFullEnvType fc env ty
                           else abstractEnvType fc env ty
         let hole = record { noCycles = nocyc }
                           (newDef fc n rig [] hty Public def)
         log "unify.meta" 5 $ "Adding new meta " ++ show (n, fc, rig)
         logTerm "unify.meta" 10 ("New meta type " ++ show n) hty
         defs <- get Ctxt
         idx <- addDef n hole
         addHoleName fc n idx
         pure (idx, Meta fc n idx envArgs)
  where
    envArgs : List (Term vars)
    envArgs = let args = reverse (mkConstantAppArgs {done = []} lets fc env []) in
                  rewrite sym (appendNilRightNeutral vars) in args

export
newMeta : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          FC -> RigCount ->
          Env Term vars -> Name -> Term vars -> Def ->
          Bool ->
          Core (Int, Term vars)
newMeta fc r env n ty def cyc = newMetaLets fc r env n ty def cyc False

mkConstant : {vars : _} ->
             FC -> Env Term vars -> Term vars -> ClosedTerm
mkConstant fc [] tm = tm
-- mkConstant {vars = x :: _} fc (Let c val ty :: env) tm
--     = mkConstant fc env (Bind fc x (Let c val ty) tm)
mkConstant {vars = x :: _} fc (b :: env) tm
    = let ty = binderType b in
          mkConstant fc env (Bind fc x (Lam fc (multiplicity b) Explicit ty) tm)

-- Given a term and a type, add a new guarded constant to the global context
-- by applying the term to the current environment
-- Return the replacement term (the name applied to the environment)
export
newConstant : {vars : _} ->
              {auto u : Ref UST UState} ->
              {auto c : Ref Ctxt Defs} ->
              FC -> RigCount -> Env Term vars ->
              (tm : Term vars) -> (ty : Term vars) ->
              (constrs : List Int) ->
              Core (Term vars)
newConstant {vars} fc rig env tm ty constrs
    = do let def = mkConstant fc env tm
         let defty = abstractFullEnvType fc env ty
         cn <- genName "postpone"
         let guess = newDef fc cn rig [] defty Public
                            (Guess def (length env) constrs)
         log "unify.constant" 5 $ "Adding new constant " ++ show (cn, fc, rig)
         logTerm "unify.constant" 10 ("New constant type " ++ show cn) defty
         idx <- addDef cn guess
         addGuessName fc cn idx
         pure (Meta fc cn idx envArgs)
  where
    envArgs : List (Term vars)
    envArgs = let args = reverse (mkConstantAppArgs {done = []} True fc env []) in
                  rewrite sym (appendNilRightNeutral vars) in args

-- Create a new search with the given name and return type,
-- and return a term which is the name applied to the environment
-- (and which has the given type)
export
newSearch : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            FC -> RigCount -> Nat -> Name ->
            Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
newSearch {vars} fc rig depth def env n ty
    = do let hty = abstractEnvType fc env ty
         let hole = newDef fc n rig [] hty Public (BySearch rig depth def)
         log "unify.search" 10 $ "Adding new search " ++ show fc ++ " " ++ show n
         logTermNF "unify.search" 10 "New search type" [] hty
         idx <- addDef n hole
         addGuessName fc n idx
         pure (idx, Meta fc n idx envArgs)
  where
    envArgs : List (Term vars)
    envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
                  rewrite sym (appendNilRightNeutral vars) in args

-- Add a hole which stands for a delayed elaborator
export
newDelayed : {vars : _} ->
             {auto u : Ref UST UState} ->
             {auto c : Ref Ctxt Defs} ->
             FC -> RigCount ->
             Env Term vars -> Name ->
             (ty : Term vars) -> Core (Int, Term vars)
newDelayed {vars} fc rig env n ty
    = do let hty = abstractEnvType fc env ty
         let hole = newDef fc n rig [] hty Public Delayed
         idx <- addDef n hole
         log "unify.delay" 10 $ "Added delayed elaborator " ++ show (n, idx)
         addHoleName fc n idx
         pure (idx, Meta fc n idx envArgs)
  where
    envArgs : List (Term vars)
    envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
                  rewrite sym (appendNilRightNeutral vars) in args

export
tryErrorUnify : {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                Core a -> Core (Either Error a)
tryErrorUnify elab
    = do ust <- get UST
         defs <- branch
         catch (do res <- elab
                   commit
                   pure (Right res))
               (\err => do put UST ust
                           defs' <- get Ctxt
                           put Ctxt (record { timings = timings defs' } defs)
                           pure (Left err))

export
tryUnify : {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           Core a -> Core a -> Core a
tryUnify elab1 elab2
    = do Right ok <- tryErrorUnify elab1
               | Left err => elab2
         pure ok

export
handleUnify : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              Core a -> (Error -> Core a) -> Core a
handleUnify elab1 elab2
    = do Right ok <- tryErrorUnify elab1
               | Left err => elab2 err
         pure ok

-- Note that the given hole name arises from a type declaration, so needs
-- to be resolved later
export
addDelayedHoleName : {auto u : Ref UST UState} ->
                     (Int, (FC, Name)) -> Core ()
addDelayedHoleName (idx, h)
    = do ust <- get UST
         put UST (record { delayedHoles $= insert idx h } ust)

export
checkDelayedHoles : {auto u : Ref UST UState} ->
                    {auto c : Ref Ctxt Defs} ->
                    Core (Maybe Error)
checkDelayedHoles
    = do ust <- get UST
         let hs = toList (delayedHoles ust)
         if (not (isNil hs))
            then do pure (Just (UnsolvedHoles (map snd hs)))
            else pure Nothing

-- A hole is 'valid' - i.e. okay to leave unsolved for later - as long as it's
-- not guarded by a unification problem (in which case, report that the unification
-- problem is unsolved) and it doesn't depend on an implicit pattern variable
-- (in which case, perhaps suggest binding it explicitly)
checkValidHole : {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 Int -> (Int, (FC, Name)) -> Core ()
checkValidHole base (idx, (fc, n))
  = when (idx >= base) $
      do defs <- get Ctxt
         ust <- get UST
         Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)
              | Nothing => pure ()
         case definition gdef of
              BySearch _ _ _ =>
                  do defs <- get Ctxt
                     Just ty <- lookupTyExact n (gamma defs)
                          | Nothing => pure ()
                     throw (CantSolveGoal fc (gamma defs) [] ty Nothing)
              Guess tm envb (con :: _) =>
                  do ust <- get UST
                     let Just c = lookup con (constraints ust)
                          | Nothing => pure ()
                     case c of
                          MkConstraint fc l env x y =>
                             do put UST (record { guesses = empty } ust)
                                empty <- clearDefs defs
                                xnf <- quote empty env x
                                ynf <- quote empty env y
                                throw (CantSolveEq fc (gamma defs) env xnf ynf)
                          MkSeqConstraint fc env (x :: _) (y :: _) =>
                             do put UST (record { guesses = empty } ust)
                                empty <- clearDefs defs
                                xnf <- quote empty env x
                                ynf <- quote empty env y
                                throw (CantSolveEq fc (gamma defs) env xnf ynf)
                          _ => pure ()
              _ => traverse_ checkRef !(traverse getFullName
                                        ((keys (getRefs (Resolved (-1)) (type gdef)))))
  where
    checkRef : Name -> Core ()
    checkRef (PV n f)
        = throw (GenericMsg fc
                   ("Hole cannot depend on an unbound implicit " ++ show n))
    checkRef _ = pure ()

-- Bool flag says whether it's an error for there to have been holes left
-- in the last session. Usually we can leave them to the end, but it's not
-- valid for there to be holes remaining when checking a LHS.
-- Also throw an error if there are unresolved guarded constants or
-- unsolved searches
export
checkUserHolesAfter : {auto u : Ref UST UState} ->
                      {auto c : Ref Ctxt Defs} ->
                      Int -> Bool -> Core ()
checkUserHolesAfter base now
    = do gs_map <- getGuesses
         let gs = toList gs_map
         log "unify.unsolved" 10 $ "Unsolved guesses " ++ show gs
         traverse_ (checkValidHole base) gs
         hs_map <- getCurrentHoles
         let hs = toList hs_map
         let hs' = if any isUserName (map (snd . snd) hs)
                      then [] else hs
         when (now && not (isNil hs')) $
              throw (UnsolvedHoles (map snd (nubBy nameEq hs)))
         -- Note the hole names, to ensure they are resolved
         -- by the end of elaborating the current source file
         traverse_ addDelayedHoleName hs'
  where
    nameEq : (a, b, Name) -> (a, b, Name) -> Bool
    nameEq (_, _, x) (_, _, y) = x == y

export
checkUserHoles : {auto u : Ref UST UState} ->
                 {auto c : Ref Ctxt Defs} ->
                 Bool -> Core ()
checkUserHoles = checkUserHolesAfter 0

export
checkNoGuards : {auto u : Ref UST UState} ->
                {auto c : Ref Ctxt Defs} ->
                Core ()
checkNoGuards = checkUserHoles False

export
dumpHole : {auto u : Ref UST UState} ->
           {auto c : Ref Ctxt Defs} ->
           (s : String) ->
           {auto 0 _ : KnownTopic s} ->
           Nat -> (hole : Int) -> Core ()
dumpHole str n hole
    = do ust <- get UST
         defs <- get Ctxt
         sopts <- getSession
         defs <- get Ctxt
         case !(lookupCtxtExact (Resolved hole) (gamma defs)) of
          Nothing => pure ()
          Just gdef => case (definition gdef, type gdef) of
             (Guess tm envb constraints, ty) =>
                  do logString str n $
                       "!" ++ show !(getFullName (Resolved hole)) ++ " : "
                           ++ show !(toFullNames !(normaliseHoles defs [] ty))
                       ++ "\n\t  = "
                           ++ show !(normaliseHoles defs [] tm)
                           ++ "\n\twhen"
                     traverse_ dumpConstraint constraints
             (Hole _ p, ty) =>
                  logString str n $
                    "?" ++ show (fullname gdef) ++ " : "
                        ++ show !(normaliseHoles defs [] ty)
                        ++ if implbind p then " (ImplBind)" else ""
                        ++ if invertible gdef then " (Invertible)" else ""
             (BySearch _ _ _, ty) =>
                  logString str n $
                     "Search " ++ show hole ++ " : " ++
                     show !(toFullNames !(normaliseHoles defs [] ty))
             (PMDef _ args t _ _, ty) =>
                  log str 4 $
                     "Solved: " ++ show hole ++ " : " ++
                     show !(normalise defs [] ty) ++
                     " = " ++ show !(normalise defs [] (Ref emptyFC Func (Resolved hole)))
             (ImpBind, ty) =>
                  log str 4 $
                      "Bound: " ++ show hole ++ " : " ++
                      show !(normalise defs [] ty)
             (Delayed, ty) =>
                  log str 4 $
                     "Delayed elaborator : " ++
                     show !(normalise defs [] ty)
             _ => pure ()
  where
    dumpConstraint : Int -> Core ()
    dumpConstraint cid
        = do ust <- get UST
             defs <- get Ctxt
             case lookup cid (constraints ust) of
                  Nothing => pure ()
                  Just Resolved => logString str n "\tResolved"
                  Just (MkConstraint _ lazy env x y) =>
                    do logString str n $
                         "\t  " ++ show !(toFullNames !(quote defs env x))
                                ++ " =?= " ++ show !(toFullNames !(quote defs env y))
                       empty <- clearDefs defs
                       log str 5 $
                         "\t    from " ++ show !(toFullNames !(quote empty env x))
                            ++ " =?= " ++ show !(toFullNames !(quote empty env y))
                            ++ if lazy then "\n\t(lazy allowed)" else ""
                  Just (MkSeqConstraint _ _ xs ys) =>
                       logString str n $ "\t\t" ++ show xs ++ " =?= " ++ show ys

export
dumpConstraints : {auto u : Ref UST UState} ->
                  {auto c : Ref Ctxt Defs} ->
                  (topics : String) ->
                  {auto 0 _ : KnownTopic topics} ->
                  (verbosity : Nat) ->
                  (all : Bool) ->
                  Core ()
dumpConstraints str n all
    = do ust <- get UST
         defs <- get Ctxt
         sopts <- getSession
         when !(logging str n) $ do
           let hs = toList (guesses ust) ++
                    toList (if all then holes ust else currentHoles ust)
           unless (isNil hs) $
             do logString str n "--- CONSTRAINTS AND HOLES ---"
                traverse_ (dumpHole str n) (map fst hs)


text:
module Main
import Effects
import IdrisNet.TCP.TCPClient
import IdrisNet.TCP.TCPCommon
import Effect.StdIO
import Network.Socket

clientLoop : ByteLength ->
               { [TCPCLIENT (ClientConnected), STDIO] ==>
                 [TCPCLIENT (), STDIO]}
               Eff ()
clientLoop len = do
  input <- getStr
  if (input == "bye!\n") then tcpClose
  else do
    OperationSuccess _ <- tcpSend input
      | RecoverableError err => do putStr ("Error sending: " ++ (show err))
                                   tcpClose
      | FatalError err => do putStr ("Error sending: " ++ (show err))
                             tcpFinalise
      | ConnectionClosed => return ()
    OperationSuccess (str, len') <- tcpRecv len
      | RecoverableError err => do putStr ("Error receiving: " ++ (show err))
                                   tcpClose
      | FatalError err => do putStr ("Error receiving: " ++ (show err))
                             tcpFinalise
      | ConnectionClosed => return ()
    putStr ("Received: " ++ str ++ "\n")
    clientLoop len

echoClient : SocketAddress ->
             Port ->
             { [TCPCLIENT (), STDIO] ==>
               [TCPCLIENT (), STDIO]} Eff ()
echoClient sa port = do
  OperationSuccess _ <- tcpConnect sa port
    | RecoverableError _ => echoClient sa port
    | ConnectionClosed => putStr "Unable to connect: connection closed. \n"
    | FatalError err => putStr ("Unable to connect: fatal error " ++ (show err))
  putStr "Connected!\n"
  clientLoop 1024

main : IO ()
main = run (echoClient (IPv4Addr 127 0 0 1) 1234)


text:
-- Printf.idr
-- A C-style printf function, demonstarting
-- variable function arguments

module Printf

export
data Format = Num Format
            | Chr Format
            | Dbl Format
            | Str Format
            | Lit String Format
            | End

%name Format fmt

export
PrintfType : Format -> Type
PrintfType (Num fmt) = (i : Int) -> PrintfType fmt
PrintfType (Chr fmt) = (c : Char) -> PrintfType fmt
PrintfType (Dbl fmt) = (f : Double) -> PrintfType fmt
PrintfType (Str fmt) = (str : String) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String

||| Generates a string from the given format spec
export
printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Num fmt) acc = \i => printfFmt fmt (acc ++ (show i))
printfFmt (Chr fmt) acc = \c => printfFmt fmt (acc ++ (show c))
printfFmt (Dbl fmt) acc = \f => printfFmt fmt (acc ++ (show f))
printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
printfFmt (Lit str fmt) acc = printfFmt fmt (acc ++ str)
printfFmt End acc = acc

||| Convert given char list to format data type
export
toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Num (toFormat chars)
toFormat ('%' :: 'c' :: chars) = Chr (toFormat chars)
toFormat ('%' :: 'f' :: chars) = Dbl (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
                             (Lit lit chars') => Lit (strCons c lit) chars'
                             fmt => Lit (strCons c "") fmt

||| Outputs the given format string as String
||| @fmt Format specification
export
printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Web.Internal.PermissionsTypes

import JS

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

namespace PermissionState

  public export
  data PermissionState = Granted | Denied | Prompt

  public export
  Show PermissionState where
    show Granted = "granted"
    show Denied = "denied"
    show Prompt = "prompt"

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

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

  public export
  read : String -> Maybe PermissionState
  read "granted" = Just Granted
  read "denied" = Just Denied
  read "prompt" = Just Prompt
  read _ = Nothing

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

  export
  ToFFI PermissionState String where
    toFFI = show

  export
  FromFFI PermissionState String where
    fromFFI = read

namespace PermissionName

  public export
  data PermissionName = Geolocation
                      | Notifications
                      | Push
                      | Midi
                      | Camera
                      | Microphone
                      | SpeakerSelection
                      | DeviceInfo
                      | BackgroundFetch
                      | BackgroundSync
                      | Bluetooth
                      | PersistentStorage
                      | AmbientLightSensor
                      | Accelerometer
                      | Gyroscope
                      | Magnetometer
                      | ClipboardRead
                      | ClipboardWrite
                      | DisplayCapture
                      | Nfc

  public export
  Show PermissionName where
    show Geolocation = "geolocation"
    show Notifications = "notifications"
    show Push = "push"
    show Midi = "midi"
    show Camera = "camera"
    show Microphone = "microphone"
    show SpeakerSelection = "speaker-selection"
    show DeviceInfo = "device-info"
    show BackgroundFetch = "background-fetch"
    show BackgroundSync = "background-sync"
    show Bluetooth = "bluetooth"
    show PersistentStorage = "persistent-storage"
    show AmbientLightSensor = "ambient-light-sensor"
    show Accelerometer = "accelerometer"
    show Gyroscope = "gyroscope"
    show Magnetometer = "magnetometer"
    show ClipboardRead = "clipboard-read"
    show ClipboardWrite = "clipboard-write"
    show DisplayCapture = "display-capture"
    show Nfc = "nfc"

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

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

  public export
  read : String -> Maybe PermissionName
  read "geolocation" = Just Geolocation
  read "notifications" = Just Notifications
  read "push" = Just Push
  read "midi" = Just Midi
  read "camera" = Just Camera
  read "microphone" = Just Microphone
  read "speaker-selection" = Just SpeakerSelection
  read "device-info" = Just DeviceInfo
  read "background-fetch" = Just BackgroundFetch
  read "background-sync" = Just BackgroundSync
  read "bluetooth" = Just Bluetooth
  read "persistent-storage" = Just PersistentStorage
  read "ambient-light-sensor" = Just AmbientLightSensor
  read "accelerometer" = Just Accelerometer
  read "gyroscope" = Just Gyroscope
  read "magnetometer" = Just Magnetometer
  read "clipboard-read" = Just ClipboardRead
  read "clipboard-write" = Just ClipboardWrite
  read "display-capture" = Just DisplayCapture
  read "nfc" = Just Nfc
  read _ = Nothing

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

  export
  ToFFI PermissionName String where
    toFFI = show

  export
  FromFFI PermissionName String where
    fromFFI = read

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

export data PermissionStatus : Type where [external]

export
ToFFI PermissionStatus PermissionStatus where toFFI = id

export
FromFFI PermissionStatus PermissionStatus where fromFFI = Just

export
SafeCast PermissionStatus where
  safeCast = unsafeCastOnPrototypeName "PermissionStatus"

export data Permissions : Type where [external]

export
ToFFI Permissions Permissions where toFFI = id

export
FromFFI Permissions Permissions where fromFFI = Just

export
SafeCast Permissions where
  safeCast = unsafeCastOnPrototypeName "Permissions"

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

export data CameraDevicePermissionDescriptor : Type where [external]

export
ToFFI CameraDevicePermissionDescriptor CameraDevicePermissionDescriptor where toFFI = id

export
FromFFI CameraDevicePermissionDescriptor CameraDevicePermissionDescriptor where fromFFI = Just

export data DevicePermissionDescriptor : Type where [external]

export
ToFFI DevicePermissionDescriptor DevicePermissionDescriptor where toFFI = id

export
FromFFI DevicePermissionDescriptor DevicePermissionDescriptor where fromFFI = Just

export data MidiPermissionDescriptor : Type where [external]

export
ToFFI MidiPermissionDescriptor MidiPermissionDescriptor where toFFI = id

export
FromFFI MidiPermissionDescriptor MidiPermissionDescriptor where fromFFI = Just

export data PermissionDescriptor : Type where [external]

export
ToFFI PermissionDescriptor PermissionDescriptor where toFFI = id

export
FromFFI PermissionDescriptor PermissionDescriptor where fromFFI = Just

export data PermissionSetParameters : Type where [external]

export
ToFFI PermissionSetParameters PermissionSetParameters where toFFI = id

export
FromFFI PermissionSetParameters PermissionSetParameters where fromFFI = Just

export data PushPermissionDescriptor : Type where [external]

export
ToFFI PushPermissionDescriptor PushPermissionDescriptor where toFFI = id

export
FromFFI PushPermissionDescriptor PushPermissionDescriptor where fromFFI = Just


text:
||| This module presents a realisation of ARMs AXI4 protocol using our
||| abstract interface definition language.
module Example.Specification.AXI4

import Data.List
import Data.Vect
import Data.Ranged

import Text.Markup.Edda
import Text.Markup.Edda.Org

import Cordial.EDSL.Specification

%access public export
%default partial

data AXI =
  -- system signals
    ACLK
  | ARESETN
  | ACLKEN

  -- write address
  | AWID
  | AWADDR
  | AWLEN
  | AWSIZE
  | AWBURST
  | AWLOCK
  | AWCACHE
  | AWPROT
  | AWQOS
  | AWREGION
  | AWVALID
  | AWREADY

  -- read address
  | ARID
  | ARADDR
  | ARLEN
  | ARSIZE
  | ARBURST
  | ARLOCK
  | ARCACHE
  | ARPROT
  | ARQOS
  | ARREGION
  | ARVALID
  | ARREADY

  -- write data
  | WID
  | WLAST
  | WDATA
  | WSTRB
  | WVALID
  | WREADY

  -- read response
  | RID
  | RLAST
  | RDATA
  | RRESP
  | RVALID
  | RREADY

  -- write response
  | BID
  | BRESP
  | BVALID
  | BREADY

  -- low poer
  | CSYSREQ
  | CSYSACK
  | CACTIVE

Eq AXI where
  (==) ACLK     ACLK     = True
  (==) ARESETN  ARESETN  = True
  (==) ACLKEN   ACLKEN   = True
  (==) AWID     AWID     = True
  (==) AWADDR   AWADDR   = True
  (==) AWLEN    AWLEN    = True
  (==) AWSIZE   AWSIZE   = True
  (==) AWBURST  AWBURST  = True
  (==) AWLOCK   AWLOCK   = True
  (==) AWCACHE  AWCACHE  = True
  (==) AWPROT   AWPROT   = True
  (==) AWQOS    AWQOS    = True
  (==) AWREGION AWREGION = True
  (==) AWVALID  AWVALID  = True
  (==) AWREADY  AWREADY  = True
  (==) ARID     ARID     = True
  (==) ARADDR   ARADDR   = True
  (==) ARLEN    ARLEN    = True
  (==) ARSIZE   ARSIZE   = True
  (==) ARBURST  ARBURST  = True
  (==) ARLOCK   ARLOCK   = True
  (==) ARCACHE  ARCACHE  = True
  (==) ARPROT   ARPROT   = True
  (==) ARQOS    ARQOS    = True
  (==) ARREGION ARREGION = True
  (==) ARVALID  ARVALID  = True
  (==) ARREADY  ARREADY  = True
  (==) WID      WID      = True
  (==) WLAST    WLAST    = True
  (==) WDATA    WDATA    = True
  (==) WSTRB    WSTRB    = True
  (==) WVALID   WVALID   = True
  (==) WREADY   WREADY   = True
  (==) RID      RID      = True
  (==) RLAST    RLAST    = True
  (==) RDATA    RDATA    = True
  (==) RRESP    RRESP    = True
  (==) RVALID   RVALID   = True
  (==) RREADY   RREADY   = True
  (==) BID      BID      = True
  (==) BRESP    BRESP    = True
  (==) BVALID   BVALID   = True
  (==) BREADY   BREADY   = True
  (==) CSYSREQ  CSYSREQ  = True
  (==) CSYSACK  CSYSACK  = True
  (==) CACTIVE  CACTIVE  = True
  (==) _        _        = False

ValidWidths : List Nat
ValidWidths = [8, 16, 32, 64, 128, 256, 512, 1024]

||| Realisation of the AXI4 protocol.
|||
||| @dWidth The width of the data busses.
||| @aWidth The width of the address busses.
AXI4_Gen : (dWidth, aWidth : Nat)
        -> (prfD : ValidArraySpec dWidth ValidWidths)
        -> (prfA : ValidArraySpec aWidth ValidWidths)
        -> IDL AXI
AXI4_Gen dWidth aWidth prfD prfA = do
  setVendor "ambda.com"
  setLibrary "examples"
  setVersion "r2p0_0"
  setName "AXI4"

  ---------------------
  -- [ Global Signals ]
  ---------------------

  aclk <- label ACLK
  aresetn <- label ARESETN

  clock aclk Nothing Nothing Nothing
    # system "sys"
    # fromTargetAlways
    # opt

  reset aresetn
    # opt
    # fromTargetAlways
    # setSensitivity Low

  --------------------
  -- [ write address ]
  --------------------

  awid <- label AWID
  awaddr <- label AWADDR
  awlen <- label AWLEN
  awsize <- label AWSIZE
  awburst <- label AWBURST
  awlock <- label AWLOCK
  awcache <- label AWCACHE
  awprot <- label AWPROT
  awvalid <- label AWVALID
  awready <- label AWREADY

  control awid  # opt
  address awaddr (fromNat aWidth prfA)

  info awlen   (fromNat 8) # initiatorOpt
  info awsize  (fromNat 3) # initiatorOpt
  info awburst (fromNat 2) # initiatorOpt

  control awlock # opt

  info awcache (fromNat 4) # opt

  info awprot (fromNat 3) # targetOpt

  control awvalid

  control awready # fromTarget

  -----------------
  -- [ write data ]
  -----------------

  wid <- label WID
  wlast <- label WLAST
  wdata <- label WDATA
  wstrb <- label WSTRB
  wvalid <- label WVALID
  wready <- label WREADY

  info wid # opt

  bus wdata (fromNat dWidth prfD)

  let strN = assert_total $ div dWidth (the Nat 8)
  replicate strN (control wstrb)

  control wlast
  control wvalid
  control wready # fromTarget

  ---------------------
  -- [ Write Response ]
  ---------------------

  bid <- label BID
  bresp <- label BRESP
  bvalid <- label BVALID
  bready <- label BREADY

  info bid               # fromTarget  # opt
  info bresp (fromNat 2) # fromTarget
  control bvalid         # fromTarget

  control bready

  ---------------------------
  -- [ read address signals ]
  ---------------------------

  arid <- label ARID
  araddr <- label ARADDR
  arlen <- label ARLEN
  arsize <- label ARSIZE
  arburst <- label ARBURST
  arlock <- label ARLOCK
  arcache <- label ARCACHE
  arprot <- label ARPROT
  arvalid <- label ARVALID
  arready <- label ARREADY

  info arid # opt

  address araddr (fromNat aWidth prfA)

  info arlen   (fromNat 4)
  info arsize  (fromNat 3)
  info arburst (fromNat 2)

  info arlock  (fromNat 2) # opt
  info arcache (fromNat 4) # opt
  info arprot  (fromNat 3) # opt

  control arvalid
  control arready # fromTarget

  ----------------
  -- [ Read Data ]
  ----------------

  rid <- label RID
  rdata <- label RDATA
  rresp <- label RRESP
  rlast <- label RLAST
  rvalid <- label RVALID
  rready <- label RREADY

  info rid                        # fromTarget # opt
  bus rdata (fromNat dWidth prfD) # fromTarget
  info rresp (fromNat 2)          # fromTarget
  control rlast                   # fromTarget
  control rvalid                  # fromTarget
  control rready                  # fromTarget

  --------------------------
  -- [ Low Power Interface ]
  --------------------------

  creq <- label CSYSREQ
  cack <- label CSYSACK
  cact <- label CACTIVE

  control creq # opt # system "clock controller"
  control cack # opt # system "peripheral"
  control cact # opt # system "peripheral"

  stop

||| Realisation of the AXI4 protocol as an initiating interface..
|||
||| @dWidth The width of the data busses.
||| @aWidth The width of the address busses.
AXI4 : (dWidth, aWidth : Nat)
    -> {auto prfD : ValidArraySpec dWidth ValidWidths}
    -> {auto prfA : ValidArraySpec aWidth ValidWidths}
    -> InterfaceTy () AXI
AXI4 d a {prfD} {prfA} =
  buildSpec (AXI4_Gen d a prfD prfA)

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Data.Buffer

import Data.List
import System.FFI

%default total

-- Reading and writing binary buffers. Note that this primitives are unsafe,
-- in that they don't check that buffer locations are within bounds.
-- We really need a safe wrapper!
-- They are used in the Idris compiler itself for reading/writing checked
-- files.

-- This is known to the compiler, so maybe ought to be moved to Builtin
export
data Buffer : Type where [external]

bufferClass : String
bufferClass = "io/github/mmhelloworld/idrisjvm/runtime/IdrisBuffer"

stringsClass : String
stringsClass = "io/github/mmhelloworld/idrisjvm/runtime/Strings"

%foreign "scheme:blodwen-buffer-size"
         "RefC:getBufferSize"
         "node:lambda:b => b.length"
         jvm bufferClass "size"
prim__bufferSize : Buffer -> Int

export %inline
rawSize : HasIO io => Buffer -> io Int
rawSize buf = pure (prim__bufferSize buf)

%foreign "scheme:blodwen-new-buffer"
         "RefC:newBuffer"
         "node:lambda:s=>Buffer.alloc(s)"
         jvm bufferClass "create"
prim__newBuffer : Int -> PrimIO Buffer

export
newBuffer : HasIO io => Int -> io (Maybe Buffer)
newBuffer size
    = if size >= 0
            then do buf <- primIO (prim__newBuffer size)
                    pure $ Just buf
                 else pure Nothing
--          if prim__nullAnyPtr buf /= 0
--             then pure Nothing
--             else pure $ Just $ MkBuffer buf size 0

%foreign "scheme:blodwen-buffer-setbyte"
         "RefC:setBufferByte"
         "node:lambda:(buf,offset,value)=>buf.writeUInt8(value, offset)"
         jvm bufferClass "setByte"
prim__setByte : Buffer -> (offset : Int) -> (val : Int) -> PrimIO ()

%foreign "scheme:blodwen-buffer-setbyte"
         "RefC:setBufferByte"
         "node:lambda:(buf,offset,value)=>buf.writeUInt8(value, offset)"
         jvm bufferClass "setByte"
prim__setBits8 : Buffer -> (offset : Int) -> (val: Bits8) -> PrimIO ()

-- Assumes val is in the range 0-255
export %inline
setByte : HasIO io => Buffer -> (offset : Int) -> (val : Int) -> io ()
setByte buf offset val
    = primIO (prim__setByte buf offset val)

export %inline
setBits8 : HasIO io => Buffer -> (offset : Int) -> (val : Bits8) -> io ()
setBits8 buf offset val
    = primIO (prim__setBits8 buf offset val)

%foreign "scheme:blodwen-buffer-getbyte"
         "RefC:getBufferByte"
         "node:lambda:(buf,offset)=>buf.readUInt8(offset)"
         jvm bufferClass "getByte"
prim__getByte : Buffer -> (offset : Int) -> PrimIO Int

%foreign "scheme:blodwen-buffer-getbyte"
         "RefC:getBufferByte"
         "node:lambda:(buf,offset)=>buf.readUInt8(offset)"
         jvm bufferClass "getByte"
prim__getBits8 : Buffer -> (offset : Int) -> PrimIO Bits8

export %inline
getByte : HasIO io => Buffer -> (offset : Int) -> io Int
getByte buf offset
    = primIO (prim__getByte buf offset)

export %inline
getBits8 : HasIO io => Buffer -> (offset : Int) -> io Bits8
getBits8 buf offset
    = primIO (prim__getBits8 buf offset)

%foreign "scheme:blodwen-buffer-setbits16"
         "node:lambda:(buf,offset,value)=>buf.writeUInt16LE(value, offset)"
         jvm bufferClass "setShort"
prim__setBits16 : Buffer -> (offset : Int) -> (value : Bits16) -> PrimIO ()

export %inline
setBits16 : HasIO io => Buffer -> (offset : Int) -> (val : Bits16) -> io ()
setBits16 buf offset val
    = primIO (prim__setBits16 buf offset val)

%foreign "scheme:blodwen-buffer-getbits16"
         "node:lambda:(buf,offset)=>buf.readUInt16LE(offset)"
         jvm bufferClass "getShort"
prim__getBits16 : Buffer -> (offset : Int) -> PrimIO Bits16

export %inline
getBits16 : HasIO io => Buffer -> (offset : Int) -> io Bits16
getBits16 buf offset
    = primIO (prim__getBits16 buf offset)

%foreign "scheme:blodwen-buffer-setbits32"
         "node:lambda:(buf,offset,value)=>buf.writeUInt32LE(value, offset)"
         jvm bufferClass "setInt"
prim__setBits32 : Buffer -> (offset : Int) -> (value : Bits32) -> PrimIO ()

export %inline
setBits32 : HasIO io => Buffer -> (offset : Int) -> (val : Bits32) -> io ()
setBits32 buf offset val
    = primIO (prim__setBits32 buf offset val)

%foreign "scheme:blodwen-buffer-getbits32"
         "node:lambda:(buf,offset)=>buf.readUInt32LE(offset)"
         jvm bufferClass "getInt"
prim__getBits32 : Buffer -> Int -> PrimIO Bits32

export %inline
getBits32 : HasIO io => Buffer -> (offset : Int) -> io Bits32
getBits32 buf offset
    = primIO (prim__getBits32 buf offset)

%foreign "scheme:blodwen-buffer-setbits64"
         jvm bufferClass "setLong"
prim__setBits64 : Buffer -> Int -> Bits64 -> PrimIO ()

export %inline
setBits64 : HasIO io => Buffer -> (offset : Int) -> (val : Bits64) -> io ()
setBits64 buf offset val
    = primIO (prim__setBits64 buf offset val)

%foreign "scheme:blodwen-buffer-getbits64"
         jvm bufferClass "getLong"
prim__getBits64 : Buffer -> (offset : Int) -> PrimIO Bits64

export %inline
getBits64 : HasIO io => Buffer -> (offset : Int) -> io Bits64
getBits64 buf offset
    = primIO (prim__getBits64 buf offset)

%foreign "scheme:blodwen-buffer-setint32"
         "node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)"
         jvm bufferClass "setInt"
prim__setInt32 : Buffer -> (offset : Int) -> (val : Int) -> PrimIO ()

export %inline
setInt32 : HasIO io => Buffer -> (offset : Int) -> (val : Int) -> io ()
setInt32 buf offset val
    = primIO (prim__setInt32 buf offset val)

%foreign "scheme:blodwen-buffer-getint32"
         "node:lambda:(buf,offset)=>buf.readInt32LE(offset)"
         jvm bufferClass "getInt"
prim__getInt32 : Buffer -> (offset : Int) -> PrimIO Int

export %inline
getInt32 : HasIO io => Buffer -> (offset : Int) -> io Int
getInt32 buf offset
    = primIO (prim__getInt32 buf offset)

%foreign "scheme:blodwen-buffer-setint"
         "RefC:setBufferInt"
         "node:lambda:(buf,offset,value)=>buf.writeInt32LE(value, offset)"
         jvm bufferClass "setInt"
prim__setInt : Buffer -> (offset : Int) -> (val : Int) -> PrimIO ()

export %inline
setInt : HasIO io => Buffer -> (offset : Int) -> (val : Int) -> io ()
setInt buf offset val
    = primIO (prim__setInt buf offset val)

%foreign "scheme:blodwen-buffer-getint"
         "RefC:getBufferInt"
         "node:lambda:(buf,offset)=>buf.readInt32LE(offset)"
         jvm bufferClass "getInt"
prim__getInt : Buffer -> (offset : Int) -> PrimIO Int

export %inline
getInt : HasIO io => Buffer -> (offset : Int) -> io Int
getInt buf offset
    = primIO (prim__getInt buf offset)

%foreign "scheme:blodwen-buffer-setdouble"
         "RefC:setBufferDouble"
         "node:lambda:(buf,offset,value)=>buf.writeDoubleLE(value, offset)"
         jvm bufferClass "setDouble"
prim__setDouble : Buffer -> (offset : Int) -> (val : Double) -> PrimIO ()

export %inline
setDouble : HasIO io => Buffer -> (offset : Int) -> (val : Double) -> io ()
setDouble buf offset val
    = primIO (prim__setDouble buf offset val)

%foreign "scheme:blodwen-buffer-getdouble"
         "RefC:getBufferDouble"
         "node:lambda:(buf,offset)=>buf.readDoubleLE(offset)"
         jvm bufferClass "getDouble"
prim__getDouble : Buffer -> (offset : Int) -> PrimIO Double

export %inline
getDouble : HasIO io => Buffer -> (offset : Int) -> io Double
getDouble buf offset
    = primIO (prim__getDouble buf offset)

-- Get the length of a string in bytes, rather than characters
export
%foreign "scheme:blodwen-stringbytelen"
         "C:strlen, libc 6"
         jvm stringsClass "bytesLengthUtf8"
stringByteLength : String -> Int

%foreign "scheme:blodwen-buffer-setstring"
         "RefC:setBufferString"
         "node:lambda:(buf,offset,value)=>buf.write(value, offset,buf.length - offset, 'utf-8')"
         jvm bufferClass "setString"
prim__setString : Buffer -> (offset : Int) -> (val : String) -> PrimIO ()

export %inline
setString : HasIO io => Buffer -> (offset : Int) -> (val : String) -> io ()
setString buf offset val
    = primIO (prim__setString buf offset val)

%foreign "scheme:blodwen-buffer-getstring"
         "RefC:getBufferString"
         "node:lambda:(buf,offset,len)=>buf.slice(offset, offset+len).toString('utf-8')"
         jvm bufferClass "getString"
prim__getString : Buffer -> (offset : Int) -> (len : Int) -> PrimIO String

export %inline
getString : HasIO io => Buffer -> (offset : Int) -> (len : Int) -> io String
getString buf offset len
    = primIO (prim__getString buf offset len)

export
covering
bufferData : HasIO io => Buffer -> io (List Int)
bufferData buf
    = do len <- rawSize buf
         unpackTo [] len
  where
    covering
    unpackTo : List Int -> Int -> io (List Int)
    unpackTo acc 0 = pure acc
    unpackTo acc offset
        = do val <- getByte buf (offset - 1)
             unpackTo (val :: acc) (offset - 1)

%foreign "scheme:blodwen-buffer-copydata"
         "RefC:copyBuffer"
         "node:lambda:(b1,o1,length,b2,o2)=>b1.copy(b2,o2,o1,o1+length)"
         jvm bufferClass "copy"
prim__copyData : (src : Buffer) -> (srcOffset, len : Int) ->
                 (dst : Buffer) -> (dstOffset : Int) -> PrimIO ()

export
copyData : HasIO io => Buffer -> (srcOffset, len : Int) ->
           (dst : Buffer) -> (dstOffset : Int) -> io ()
copyData src start len dest offset
    = primIO (prim__copyData src start len dest offset)

export
resizeBuffer : HasIO io => Buffer -> Int -> io (Maybe Buffer)
resizeBuffer old newsize
    = do Just buf <- newBuffer newsize
              | Nothing => pure Nothing
         -- If the new buffer is smaller than the old one, just copy what
         -- fits
         oldsize <- rawSize old
         let len = if newsize < oldsize then newsize else oldsize
         copyData old 0 len buf 0
         pure (Just buf)

||| Create a buffer containing the concatenated content from a
||| list of buffers.
export
concatBuffers : HasIO io => List Buffer -> io (Maybe Buffer)
concatBuffers xs
    = do let sizes = map prim__bufferSize xs
         let (totalSize, revCumulative) = foldl scanSize (0,[]) sizes
         let cumulative = reverse revCumulative
         Just buf <- newBuffer totalSize
              | Nothing => pure Nothing
         traverse_ (\(b, size, watermark) => copyData b 0 size buf watermark) (zip3 xs sizes cumulative)
         pure (Just buf)
    where
        scanSize : (Int, List Int) -> Int -> (Int, List Int)
        scanSize (s, cs) x  = (s+x, s::cs)

||| Split a buffer into two at a position.
export
splitBuffer : HasIO io => Buffer -> Int -> io (Maybe (Buffer, Buffer))
splitBuffer buf pos = do size <- rawSize buf
                         if pos > 0 && pos < size
                             then do Just first <- newBuffer pos
                                        | Nothing => pure Nothing
                                     Just second <- newBuffer (size - pos)
                                        | Nothing => pure Nothing
                                     copyData buf 0 pos first 0
                                     copyData buf pos (size-pos) second 0
                                     pure $ Just (first, second)
                             else pure Nothing


text:
module Dimp

import Data.Vect

import Assn
import Expr
import Hoare
import Imp
import Maps

-- %hide Assn.(->>)

%access public export

%default total

data DCom : Type where
  DCSkip : Assertion -> DCom
  DCSeq : DCom -> DCom -> DCom
  DCAss : Id -> AExp -> Assertion -> DCom
  DCIf : BExp -> Assertion -> DCom -> Assertion -> DCom -> Assertion -> DCom
  DCWhile : BExp -> Assertion -> DCom -> Assertion -> DCom
  DCPre : Assertion -> DCom -> DCom
  DCPost : DCom -> Assertion -> DCom

data Decorated : Type where
  Decorate : Assertion -> DCom -> Decorated

SKIP : Vect 1 Assertion -> DCom
SKIP [p] = DCSkip p

syntax [x] "::=" [a] "[" [p] "]" = DCAss x a p

syntax IF [b] THEN "[" [pThen] "]" [dt] ELSE "[" [pElse] "]" [df] END "[" [pIf] "]" = DCIf b pThen dt pElse df pIf

syntax WHILE [b] DO "[" [pBody] "]" [d] END "[" [pPost] "]" = DCWhile b pBody d pPost

syntax "->>" "[" [p] "]" [d] = DCPre p d

(->>) : DCom -> Vect 1 Assertion -> DCom
d ->> [p] = DCPost d p

(>>=) : DCom -> (() -> DCom) -> DCom
(>>=) c f = DCSeq c (f ())

syntax "[" [p] "]" [d] = Decorate p d

dec0 : DCom
dec0 = SKIP [const ()]

dec1 : DCom
dec1 = WHILE BTrue DO [const ()] SKIP [const ()] END [const ()]

dec_while : Decorated
dec_while =
  ([const ()]
   WHILE not (X == 0) DO
     [\st => ((), Not (st X = 0))]
     DCAss X (X - 1)
     (const ())
   END
   [\st => ((), st X = 0)] ->>
   [\st => st X = 0])

extract : DCom -> Com
extract (DCSkip _) = CSkip
extract (DCSeq d1 d2) = CSeq (extract d1) (extract d2)
extract (DCAss x e _) = CAss x e
extract (DCIf b _ dt _ df _) = CIf b (extract dt) (extract df)
extract (DCWhile b _ d _) = CWhile b (extract d)
extract (DCPre _ d) = extract d
extract (DCPost d _) = extract d

extract_dec : Decorated -> Com
extract_dec (Decorate _ d) = extract d

post : DCom -> Assertion
post (DCSkip p) = p
post (DCSeq _ d2) = post d2
post (DCAss _ _ p) = p
post (DCIf _ _ _ _ _ p) = p
post (DCWhile _ _ _ p) = p
post (DCPre _ d) = post d
post (DCPost _ p) = p

pre_dec : Decorated -> Assertion
pre_dec (Decorate p _) = p

post_dec : Decorated -> Assertion
post_dec (Decorate _ d) = post d

DecCorrect : (dec : Decorated) -> Type
DecCorrect dec = HoareTriple (pre_dec dec) (extract_dec dec) (post_dec dec)

VerificationConditions : (p : Assertion) -> (d : DCom) -> Type
VerificationConditions p (DCSkip q) = p ->> q
VerificationConditions p (DCSeq d1 d2) =
  ( VerificationConditions p d1
  , VerificationConditions (post d1) d2 )
VerificationConditions p (DCAss x a q) = p ->> AssignSub x a q
VerificationConditions p (DCIf b pt dt pf df q) =
  ( (\st => (p st, BAssn b st)) ->> pt
  , (\st => (p st, Not (BAssn b st))) ->> pf
  , post dt ->> q, post df ->> q
  , VerificationConditions pt dt
  , VerificationConditions pf df )
VerificationConditions p (DCWhile b pBody d q) =
  ( p ->> post d
  , (\st => (post d st, BAssn b st)) ->> pBody
  , (\st => (post d st, Not (BAssn b st))) ->> q
  , VerificationConditions pBody d )
VerificationConditions p (DCPre p' d) = (p ->> p', VerificationConditions p' d)
VerificationConditions p (DCPost d q) =
  (VerificationConditions p d, post d ->> q)

verification_correct : (d : DCom) -> (p : Assertion) ->
                       VerificationConditions p d ->
                       HoareTriple p (extract d) (post d)
verification_correct (DCSkip q) p vc st _ E_Skip p_st = vc st p_st
verification_correct (DCSeq d1 d2) p (vc1, vc2) st st' (E_Seq {st2} c1 c2) p_st =
  let post_d1_st2 = verification_correct d1 p vc1 st st2 c1 p_st
  in verification_correct d2 (post d1) vc2 st2 st' c2 post_d1_st2
verification_correct (DCAss x e q) p vc st _ (E_Ass prf) p_st =
  rewrite sym prf in vc st p_st
verification_correct (DCIf b pt dt pf df q) p
                     (p_pt_imp, p_pf_imp, pt_q_imp, pf_q_imp, vc_pt_dt, vc_pf_df)
                     st st' (E_IfTrue prf ct) p_st =
  let pt_st = p_pt_imp st (p_st, prf)
      post_dt_st' = verification_correct dt pt vc_pt_dt st st' ct pt_st
  in pt_q_imp st' post_dt_st'
verification_correct (DCIf b pt dt pf df q) p
                     (p_pt_imp, p_pf_imp, pt_q_imp, pf_q_imp, vc_pt_dt, vc_pf_df)
                     st st' (E_IfFalse prf cf) p_st =
  let pf_st = p_pf_imp st (p_st, bexp_eval_false prf)
      post_df_st' = verification_correct df pf vc_pf_df st st' cf pf_st
  in pf_q_imp st' post_df_st'
verification_correct (DCWhile b pd d q) p (p_d_imp, d_pd_imp, d_q_imp, vc_pd_d)
                     st _ (E_WhileEnd prf) p_st =
  d_q_imp st (p_d_imp st p_st, bexp_eval_false prf)
verification_correct w@(DCWhile b pd d q) p (p_d_imp, d_pd_imp, d_q_imp, vc_pd_d)
                     st st' (E_WhileLoop {st1} prf cbody cnext) p_st =
  let pd_st = d_pd_imp st (p_d_imp st p_st, prf)
      d_st1 = verification_correct d pd vc_pd_d st st1 cbody pd_st
  in verification_correct
       w
       (post d)
       (\_, d_st2 => d_st2, d_pd_imp, d_q_imp, vc_pd_d)
       st1
       st'
       cnext
       d_st1
verification_correct (DCPre p' d) p (imp, vc) st st' rel p_st =
  verification_correct d p' vc st st' rel (imp st p_st)
verification_correct (DCPost d q) p (vc, imp) st st' rel p_st =
  imp st' (verification_correct d p vc st st' rel p_st)

VerificationConditionsDec : Decorated -> Type
VerificationConditionsDec (Decorate p d) = VerificationConditions p d

verification_correct_dec : (dec : Decorated) -> VerificationConditionsDec dec ->
                           DecCorrect dec
verification_correct_dec (Decorate p d) vc = verification_correct d p vc


text:
module Commons.Text.Lexer.Run

import Commons.Data.Location
import Text.Lexer

%default total
%access public export

public export
record LexError where
  constructor MkLexFail
  location : Location
  input  : String

Show LexError where
  show (MkLexFail l i) =
    unwords ["Lexing Error at ", show l, ":\n", show i]

public export
data LexFail = LError LexError | LIOErr FileError

Show LexFail where
  show (LError (MkLexFail loc i)) =
    unwords ["Lexing Error at ", show loc, ":\n", show i]
  show (LIOErr err) =
    unwords ["FileError", show err]

public export
record Lexer a where
  constructor MkLexer
  tokenMap : TokenMap a
  keep : TokenData a -> Bool
  endInput : a

export
lexString : Lexer a
         -> String
         -> Either LexError (List (TokenData a))
lexString lexer str =
      case Lexer.Core.lex (tokenMap lexer) str of
        (tok, (c,l, "")) => Right (filter (keep lexer) tok ++ [MkToken c l (endInput lexer)])
        (_,   (c,l,i))    => Left (MkLexFail (MkLoc Nothing (toNat c) (toNat l)) i)

export
lexFile : Lexer a -> String -> IO $ Either LexFail (List (TokenData a))
lexFile lexer fname = do
  Right str <- readFile fname | Left err => pure (Left (LIOErr err))
  case lexString lexer str of
        Left err => pure $ Left (LError (record {location->source = Just fname} err))
        Right toks => pure (Right toks)

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module Data.String.Extra

import Data.List
import Data.List1
import Data.Nat
import Data.String

%default total

infixl 5 +>
infixr 5 <+

||| Adds a character to the end of the specified string.
|||
||| ```idris example
||| strSnoc "AB" 'C'
||| ```
||| ```idris example
||| strSnoc "" 'A'
||| ```
public export
strSnoc : String -> Char -> String
strSnoc s c = s ++ (singleton c)

||| Alias of `strSnoc`
|||
||| ```idris example
||| "AB" +> 'C'
||| ```
public export
(+>) : String -> Char -> String
(+>) = strSnoc

||| Alias of `strCons`
|||
||| ```idris example
||| 'A' <+ "AB"
||| ```
public export
(<+) : Char -> String -> String
(<+) = strCons

||| Take the first `n` characters from a string. Returns the whole string
||| if it's too short.
public export
take : (n : Nat) -> (input : String) -> String
take n str = substr Z n str

||| Take the last `n` characters from a string. Returns the whole string
||| if it's too short.
public export
takeLast : (n : Nat) -> (input : String) -> String
takeLast n str with (length str)
  takeLast n str | len with (isLTE n len)
    takeLast n str | len | Yes prf = substr (len `minus` n) len str
    takeLast n str | len | No contra = str

||| Remove the first `n` characters from a string. Returns the empty string if
||| the input string is too short.
public export
drop : (n : Nat) -> (input : String) -> String
drop n str = substr n (length str) str

||| Remove the last `n` characters from a string. Returns the empty string if
||| the input string is too short.
public export
dropLast : (n : Nat) -> (input : String) -> String
dropLast n str = reverse (drop n (reverse str))

||| Remove the first and last `n` characters from a string. Returns the empty
||| string if the input string is too short.
public export
shrink : (n : Nat) -> (input : String) -> String
shrink n str = dropLast n (drop n str)

||| Concatenate the strings from a `Foldable` containing strings, separated by
||| the given string.
public export
join : (sep : String) -> Foldable t => (xs : t String) -> String
join sep xs = drop (length sep)
                   (foldl (\acc, x => acc ++ sep ++ x) "" xs)

||| Get a character from a string if the string is long enough.
public export
index : (n : Nat) -> (input : String) -> Maybe Char
index n str with (unpack str)
  index n str | [] = Nothing
  index Z str | (x :: xs) = Just x
  index (S n) str | (x :: xs) = index n str | xs

||| Indent each line of a given string by `n` spaces.
public export
indentLines : (n : Nat) -> String -> String
indentLines n str = unlines $ map (indent n) $ lines str

||| Left-justify a string to the given length, using the
||| specified fill character on the right.
export
justifyLeft : Nat -> Char -> String -> String
justifyLeft n c s = s ++ replicate (n `minus` length s) c

||| Right-justify a string to the given length, using the
||| specified fill character on the left.
export
justifyRight : Nat -> Char -> String -> String
justifyRight n c s = replicate (n `minus` length s) c ++ s


text:
module Utils

import Data.Fin
import Data.Vect

total
export
finE : Fin n -> {auto lte : LTE n m} -> Fin m
finE {n = Z} f = void $ FinZAbsurd f
finE {n = S Z} (FS f) = void $ FinZAbsurd f
finE {n = S n} {m = Z} f {lte} = void $ succNotLTEzero lte
finE {n = S n} {m = S m} FZ = FZ
finE {n = S$ S$ n} {m = S$ Z} (FS f) {lte = LTESucc lte} = void $ succNotLTEzero lte
finE {n = S$ S$ n} {m = S$ S$ m} (FS f) {lte = LTESucc lte} = FS $ finE f

total
fseq : (a = b) -> (FS a = FS b)
fseq Refl = Refl

public export
data FinOrd : Fin n -> Fin n -> Type where
	FLT : LT (finToNat a) (finToNat b) -> FinOrd a b
	FEQ : a = b -> FinOrd a b
	FGT : GT (finToNat a) (finToNat b) -> FinOrd a b

total
export
fcompare : (a : Fin n) -> (b : Fin n) -> FinOrd a b
fcompare {n=Z} a b = void $ FinZAbsurd a
fcompare {n=S n} FZ FZ = FEQ Refl
fcompare {n=S n} FZ (FS b) = FLT $ LTESucc LTEZero
fcompare {n=S n} (FS a) FZ = FGT $ LTESucc LTEZero
fcompare {n=S n} (FS a) (FS b) with (fcompare a b)
	| FLT lt = FLT $ LTESucc lt
	| FEQ eq = FEQ $ fseq eq
	| FGT gt = FGT $ LTESucc gt

total
export
finD : (f : Fin (S n)) -> {g : Fin (S n)} -> {gt : GT (finToNat f) (finToNat g)} -> Fin n
finD FZ {g} {gt} = void $ succNotLTEzero gt
finD (FS f) = f

total
export
finDown : {l : Fin (S n)} -> (f : Fin (S n)) -> {lt : LT (finToNat f) (finToNat l)} -> Fin n
finDown {l = FZ} _ {lt} = void $ succNotLTEzero lt
finDown {n = Z} {l = FS l} _ = void $ FinZAbsurd l
finDown {n = S n} {l = FS l} FZ = FZ
finDown {n = S n} {l = FS l} (FS f) {lt = LTESucc lt} = FS $ finDown f {lt}

total
export
ltePlus : LTE n m -> LTE (a + n) (a + m)
ltePlus {a=Z} lte = lte
ltePlus {a=S a} lte = LTESucc $ ltePlus lte

total
export
ltePlus' : LTE a (a + n)
ltePlus' {a=Z} = LTEZero
ltePlus' {a=S a} = LTESucc ltePlus'

total
export
ltePlus'' : LTE n (a + n)
ltePlus'' {n=Z} = LTEZero
ltePlus'' {n=S n} {a} = replace (plusSuccRightSucc a n) $ LTESucc ltePlus''

total
export
nonEmptyNub : NonEmpty l -> NonEmpty (nubBy f l)
nonEmptyNub {l=[]} IsNonEmpty impossible
nonEmptyNub {l=h::t} IsNonEmpty = IsNonEmpty

total
export
nonEmptySort : NonEmpty l -> NonEmpty (sortBy f l)
nonEmptySort {l=[]} IsNonEmpty impossible
nonEmptySort {l=h::t} IsNonEmpty = believe_me $ the (NonEmpty [1, 2]) IsNonEmpty

total
export
nonEmptyMap : NonEmpty l -> NonEmpty (map f l)
nonEmptyMap {l=[]} IsNonEmpty impossible
nonEmptyMap {l=h::t} IsNonEmpty = IsNonEmpty

max_stars_repo_name: CoderPuppy/idris-depling

max_issues_repo_name: CoderPuppy/idris-depling

max_forks_repo_name: CoderPuppy/idris-depling


text:
module Test.Bits32

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

allBits32 : Gen Bits32
allBits32 = bits32 (linear 0 0xffffffff)

gt0 : Gen Bits32
gt0 = bits32 (linear 1 MaxBits32)

gt1 : Gen Bits32
gt1 = bits32 (linear 2 MaxBits32)

prop_ltMax : Property
prop_ltMax = property $ do
  b8 <- forAll allBits32
  (b8 <= MaxBits32) === True

prop_ltMin : Property
prop_ltMin = property $ do
  b8 <- forAll allBits32
  (b8 >= MinBits32) === True

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

prop_mod : Property
prop_mod = property $ do
  [n,d] <- forAll $ np [allBits32, 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 [allBits32, gt0]
  let x = n `div` d
      r = n `mod` d
  n === x * d + r

export
props : Group
props = MkGroup "Bits32" $
  [ ("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 allBits32


text:
module Network.HTTP.Cookie

import Utils.String
import Data.String.Extra
import Data.String
import Generics.Derive

%language ElabReflection

public export
record Cookie where
  constructor MkCookie
  key : String
  value : String
  attributes : List (String, Maybe String)

public export
record CookieJar where
  constructor MkCookieJar
  cookies : List Cookie

%runElab derive "Cookie" [Generic, Meta, Eq, Ord, Show]
%runElab derive "CookieJar" [Generic, Meta, Eq, Ord, Show]

export
serialize_cookie_no_attr : Cookie -> String
serialize_cookie_no_attr cookie = "\{cookie.key}=\{cookie.value}"

export
serialize_cookie : Cookie -> String
serialize_cookie cookie = join "; " (serialize_cookie_no_attr cookie :: map serialize_attr cookie.attributes) where
  serialize_attr : (String, Maybe String) -> String
  serialize_attr (k, Nothing) = k
  serialize_attr (k, Just v) = "\{k}=\{v}"

export
same_key : Cookie -> Cookie -> Bool
same_key a b = a.key == b.key

export
add_cookie : CookieJar -> Cookie -> CookieJar
add_cookie jar cookie = MkCookieJar $ (cookie :: filter (not . same_key cookie) jar.cookies)

export
deserialize_cookie : String -> Maybe Cookie
deserialize_cookie string = do
  let (kv ::: attrs) = split (';' ==) string
  guard (isInfixOf "=" kv)
  let (k, v) = splitBy '=' kv
  pure $ MkCookie k v (map parse_attr attrs)
  where
    parse_attr : String -> (String, Maybe String)
    parse_attr attr = bimap ltrim (guard (isInfixOf "=" attr) $>) $ splitBy '=' attr