text:
module FLK_bos

import Data.SortedMap
import FLK_ast

mutual
  syntax "[" [ex1] "=>>" [ex2] "]" =
      ex1 >- _ `BigStep` ex2 >- _

  syntax "[" [ex1] "," [env1] "=>>" [ex2] "," [env2] "]" =
      ex1 >- env1 `BigStep` ex2 >- env2

  -- Big Step rules for FLK
  data BigStep : (CF a) -> (CF b) -> Type where
    DoneEv : {d : Exp Done} -> [d, e =>> d, e]

    Prim1Ev : [e =>> (B b)]
           -> [Prim1 Not e, env =>> B (not b), env]

    Prim2NEv : [e1 =>> (N n1)]
            -> [e2 =>> (N n2)]
            -> [(Prim2 o e1 e2), env =>> (N (arithOp o n1 n2)), env]

    Prim2REv : [e1 =>> (N n1)]
            -> [e2 =>> (N n2)]
            -> [(Prim2 o e1 e2), env =>> (B (relop o n1 n2)), env]

    Prim2Gen : {v1 : Exp Done} -> {v2 : Exp Done}
            -> [e1 =>> v1]
            -> [e2 =>> v2]
            -> [(Prim2 o e1 e2), env =>> genOp o v1 v2, env]
    IfTEv : [cond =>> (B True)]
         -> [t =>> v]
         -> [If cond t f, e =>> v, e]

    IfFEv : [cond =>> (B False)]
         -> [f =>> v]
         -> [If cond t f, e =>> v, e]

    IdValEv : {ident : Ident} -> {e : Env} -> {v : Exp Done}
           -> (v ** lookup ident e = Just $ Left v)
           -> [v, e =>> r, e']
           -> [Id ident, e =>> r, e']

    IdRecEv : {ident : Ident} -> {e : Env} -> {v : Exp RecLam}
           -> (v ** lookup ident e = Just $ Right v)
           -> [v, e =>> r, e']
           -> [Id ident, e =>> r, e']

    LamEv : [Abs x body, env =>> Clos env (Abs x body), env]

    RecEv : {env : Env} -> {ident : Ident} -> {body : Exp a}
         -> [body, (insert ident (Right $ Rec ident body) env) =>> v, env']
         -> [Rec ident body, env =>> v, env']

    AppEv : [func =>> (Clos e (Abs ident body))]
         -> [arg =>> argval]
         -> [body, (insert ident (Left $ argval) e) =>> v,e']
         -> [App func arg, e'' =>> v,e']

  instance Show (BigStep a b) where
    show DoneEv = "DoneEv"
    show (Prim1Ev z) = (show z) ++ " -> PrimEv"
    show (Prim2NEv w u) = (show w) ++ " and " ++ (show u) ++ " -> " ++ "Prim2NEv"
    show (Prim2REv w u) = (show w) ++ " and " ++ (show u) ++ " -> " ++ "Prim2REv"
    show (Prim2Gen w u) = (show w) ++ " and " ++ (show u) ++ " -> " ++ "Prim2GEv"
    show (IfTEv w x1) = (show w) ++ " and " ++ (show x1) ++ " -> " ++ "IfTEv"
    show (IfFEv w x1) = (show w) ++ " and " ++ (show x1) ++ " -> " ++ "IfFEv"
    show (IdValEv x y) = (show y) ++ " -> IdValEv"
    show (IdRecEv x y) = (show y) ++ " -> IdRecEv"
    show LamEv = "LamEv"
    show (RecEv x) = (show x) ++ "-> RecEv"
    show (AppEv s x1 y1) = (show s) ++ " and " ++ (show x1) ++ " and " ++ (show y1) ++ " -> " ++ "AppEv"

  transStr : (CF a) -> (CF b) -> String
  transStr c d = "["++(show c)++"] =>> ["++(show d)++"]"

prim2Lemma : (ot : OpTy) -> (op : Op2 ot) -> (e1 : Exp Done) -> (e2 : Exp Done)
          -> (tr1 : [e1' =>> e1]) -> (tr2 : [e2' =>> e2])
          -> (env : Env)
          -> Maybe (Sigma (CF Done) (\res => Prim2 op e1' e2' >- env `BigStep` res))
prim2Lemma Arith op (N k) (N j) tr1 tr2 y =
  Just ((N $ arithOp op k j) >- y ** Prim2NEv tr1 tr2)
prim2Lemma Arith op e1 e2 tr1 tr2 y = Nothing
prim2Lemma Rel op (N k) (N j) tr1 tr2 y =
  Just ((B $ relop op k j) >- y ** Prim2REv tr1 tr2)
prim2Lemma Rel op e1 e2 tr1 tr2 y = Nothing
prim2Lemma Gen op e1 e2 tr1 tr2 y = Just ((genOp op e1 e2) >- y ** Prim2Gen tr1 tr2)
prim2Lemma Bool op e1 e2 tr1 tr2 y = Nothing

mutual
  syntax "[[" [exp] "," [env] "]]" = evalCF (getTag exp) (exp >- env);

  evalCFI : (st : CF Inter) -> Maybe (Sigma (CF Done) (\st' => st `BigStep` st'))
  evalCFI ((App x z) >- y) = do
    ((stateF >- yF) ** transF) <- [[x, y]]
    ((stateA >- yA) ** transA) <- [[z, y]]
    case stateF of
         (Clos env (Abs ident body)) => do
           ((stateRes >- yRes) ** transRes) <- [[body, (insert ident (Left $ stateA) env)]]
           pure $ ((stateRes >- yRes) ** AppEv transF transA transRes)
         otherwise => Nothing

  evalCFI ((If x z w) >- y) = do
    ((stateC >- _) ** transC) <- [[x, y]]
    case stateC of
         (B False) => do
           ((stateF >- _) ** transF) <- [[w, y]]
           pure (stateF >- y ** (IfFEv transC transF))
         (B True)  => do
           ((stateT >- _) ** transT) <- [[z, y]]
           pure (stateT >- y ** (IfTEv transC transT))
         otherwise => Nothing

  evalCFI ((Prim1 Not z) >- y) = do
    ((state >- _) ** trans') <- [[z, y]]
    case state of
         (B b) => pure ((B $ not b) >- y ** (Prim1Ev trans'))
         otherwise => Nothing

  evalCFI ((Prim2 z w s) >- y) = do
    ((st1 >- _) ** tr1) <- [[w, y]]
    ((st2 >- _) ** tr2) <- [[s, y]]
    prim2Lemma (getOpT z) z st1 st2 tr1 tr2 y

  evalCFI ((Id x) >- y) with (idSteps x y)
    evalCFI ((Id x) >- y) | (Just (MkSigma z pf)) = do {
        ((st >- y') ** trans) <- [[z, y]];
        pure $ ((st >- y') ** (IdValEv (MkSigma z pf) trans))
      }
    evalCFI ((Id x) >- y) | Nothing with (idRecSteps x y)
      evalCFI ((Id x) >- y) | Nothing | Nothing = Nothing
      evalCFI ((Id x) >- y) | Nothing | (Just (MkSigma z pf)) = do {
        ((st >- y') ** trans) <- [[z, y]];
        pure $ ((st >- y') ** (IdRecEv (MkSigma z pf) trans))
      }

  evalCFD : (st : CF Done) -> (Sigma (CF Done) (\st' => st `BigStep` st'))
  evalCFD (x >- z) = (x >- z ** DoneEv)

  evalCFL : (st : CF Lam) -> (Sigma (CF Done) (\st' => st `BigStep` st'))
  evalCFL ((Abs x z) >- y) = ((Clos y (Abs x z)) >- y ** LamEv)

  evalCFR : (st : CF RecLam) -> Maybe (Sigma (CF Done) (\st' => st `BigStep` st'))
  evalCFR ((Rec x z) >- y) = do
    ((stateN >- y') ** transN) <- [[z, (insert x (Right $ Rec x z) y)]]
    pure (stateN >- y' ** RecEv transN)

  evalCF : (s : Status) -> (st : CF s) -> Maybe (Sigma (CF Done) (\st' => st `BigStep` st'))
  evalCF Inter st = evalCFI st
  evalCF Done st = Just $ evalCFD st
  evalCF Lam st = Just $ evalCFL st
  evalCF RecLam st = evalCFR st

evalErase : (Exp s) -> Maybe (CF Done)
evalErase x = [[x, emptyEnv]] >>= (\ (cf ** _) => pure cf)

max_stars_repo_name: ezrosent/FLK-Semantics

max_issues_repo_name: ezrosent/FLK-Semantics

max_forks_repo_name: ezrosent/FLK-Semantics


text:
codata HList : Type -> Type where
    Nil : HList a
    Cons : a -> HList a -> HList a

countdown : Nat -> HList Nat
countdown Z = Nil
countdown (S n) = Cons n (countdown n)

countup : Nat -> HList Nat
countup n = Cons n (countup (S n))

take : Nat -> HList a -> HList a
take _ Nil = Nil
take Z _ = Nil
take (S n) (Cons a as) = Cons a (take n as)

toList : HList a -> List a
toList Nil = Nil
toList (Cons a as) = a :: toList as

everyOther : HList a -> HList a
everyOther Nil = Nil
everyOther (Cons a Nil) = Cons a Nil
everyOther (Cons a (Cons b xs)) = Cons a (everyOther xs)

ext: idr


text:
module Test.Char

import Data.Prim.Char
import Data.SOP
import Hedgehog

allChar : Gen Char
allChar = unicodeAll

prop_ltMin : Property
prop_ltMin = property $ do
  b8 <- forAll allChar
  (b8 >= MinChar) === True

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

export
props : Group
props = MkGroup "Char"
  [ ("prop_ltMin",  prop_ltMin)
  , ("prop_comp",   prop_comp)
  ]


text:
module BasicProofs

%default total

{-
  data Equal : a -> b -> Type where
    Refl : Equal x x
-}

proofNotTrue : (not True) = False
proofNotTrue = Refl

proofNotFalse : (not False) = True
proofNotFalse = Refl

proofOnePlusOne : 1 + 1 = 2
proofOnePlusOne = Refl

proofNotInvolutive : (x : Bool) -> not (not x) = x
proofNotInvolutive False = Refl
proofNotInvolutive True = Refl

plusZeroRightNeutral : (left : Nat) -> left + 0 = left
plusZeroRightNeutral Z = Refl
plusZeroRightNeutral (S k) =
  let inductiveHypothesis = plusZeroRightNeutral k in
      rewrite inductiveHypothesis in Refl

varEquality : m = m
varEquality = Refl

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 Ex2

import Data.List
import Data.Strings

%default total

-- 2.

palindrome : String -> Bool
palindrome s = s == reverse s

-- 3.

palindrome1 : String -> Bool
palindrome1 s = toLower s == toLower (reverse s)

-- 4.

palindrome2 : String -> Bool
palindrome2 s = if len > 10
                   then toLower s == toLower (reverse s)
                   else False
  where
    len : Nat
    len = length s

-- 5.

palindrome3 : Nat -> String -> Bool
palindrome3 n s = if length s > n
                     then toLower s == toLower (reverse s)
                     else False

-- 6.

partial
counts : String -> (Nat, Nat)
counts str = (length (words str), length str)

-- 7.

topTen : Ord a => List a -> List a
topTen = take 10 . sortBy (\x, y => compare y x)

-- 8.

overLength : Nat -> List String -> Nat
overLength n = length . filter (\s => length s > n)

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
-- Copyright (c) 2013 Radek Micek

module Main

import Common
import D3

data Item = MkItem String String

getKey : Item -> String
getKey (MkItem k _) = k

getValue : Item -> String
getValue (MkItem _ v) = v

main : IO ()
main = do
  let items : List Item =
    [ MkItem "a" "porch"
    , MkItem "d" "larder"
    , MkItem "b" "utility room"
    , MkItem "f" "shed"
    ]
  arr <- mkArray items

  d3 ?? select "ul" >=>
    selectAll "li" >=>
    bindK arr (\d, i => return $ getKey d)  >=>
    enter >=>
    append "li" >=>
    text' (\d, i => return $ getValue d)

  let items2 : List Item =
    [ MkItem "b" "Utility room"
    , MkItem "B" "kitchen"
    , MkItem "d" "Larder"
    ]
  arr2 <- mkArray items2

  li <- d3 ?? selectAll "ul" >=>
          bind' (\d, i => mkArray [arr2]) >=>
          selectAll "li" >=>
          bindK' (\d, i => return d) (\d, i => return $ getKey d)
  li ?? style "background-color" "orange"
  li ?? enter >=>
    append "li" >=>
    style "background-color" "green"
  li ?? exit >=>
    remove
  li ?? text' (\d, i => return $ getValue d)

  return ()

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
module Rational
import SignedInt

%default total
%access public export

-- a/(1+b)
record Rational where
    constructor MkRat
    a: SignedInt
    b: Nat

implementation Num Rational where
    (MkRat a1 b1) + (MkRat a2 b2) = MkRat (a1 $* (S b2) + a2 $* (S b1)) (b1 * b2 + b1 + b2)
    (MkRat a1 b1) * (MkRat a2 b2) = MkRat (a1 * a2) (b1 * b2 + b1 + b2)
    fromInteger a = MkRat (fromInteger a) 0

implementation Neg Rational where
    negate (MkRat a b) = MkRat (negate a) b
    a - b = a + negate b

data RationalEq : Rational -> Rational -> Type where
    RationalRefl : (eq : a1 $* (S b2) `SignedEq` a2 $* (S b1)) -> RationalEq (MkRat a1 b1) (MkRat a2 b2)


text:
module Data.Void

export
absurdity : Uninhabited t => (0 _ : t) -> s
absurdity x = void (uninhabited x)

export
contradiction : Uninhabited t => (0 _ : x -> t) -> (x -> s)
contradiction since x = absurdity (since x)


text:
module Blackbird

import Data.Nat

f : Nat -> Nat -> Nat
f = (+1) .: (+) . (+1)

g : Nat -> Nat -> Nat
-- instead of `g = (+1) . (+1) .: (+)` write, since double `.:` works for any priority and "`.` then `.:`" works only when `.:` has smaller priority.
g = (+1) .: (+1) .: (+)

-- Assumes that `.:` has the same priority as `.`
x : String -> List String -> String
x = concatMap . (++ "e") .: (++) . (++ "x")

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
import Data.String

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
    then pure (Just (stringToNatOrZ input))
    else pure Nothing

readNumbers : IO (Maybe (Nat, Nat))
readNumbers = do
  Just num1_ok <- readNumber
    | Nothing => pure Nothing
  Just num2_ok <- readNumber
    | Nothing => pure Nothing
  pure (Just (num1_ok, num2_ok))

max_stars_repo_name: brunoflores/type-driven-with-idris

max_issues_repo_name: brunoflores/type-driven-with-idris

max_forks_repo_name: brunoflores/type-driven-with-idris


text:
||| Interface and utilities for marshalling Idris2 values from JSON
||| via an intermediate `Value` representation.
|||
||| For regular algebraic data types, implementations can automatically
||| be derived using elaborator reflection.
|||
||| Operators and functionality strongly influenced by Haskell's aeson
||| library
module JSON.FromJSON

import JSON.ToJSON
import JSON.Option
import JSON.Value
import Language.JSON

import Generics.Derive

%language ElabReflection

--------------------------------------------------------------------------------
--          Types
--------------------------------------------------------------------------------

public export
data JSONPathElement = Key String | Index Bits32

%runElab derive "JSONPathElement" [Generic,Meta,Show,Eq]

public export
JSONPath : Type
JSONPath = List JSONPathElement

public export
JSONErr : Type
JSONErr = (JSONPath,String)

public export
Result : Type -> Type
Result = Either JSONErr

public export
Parser : Type -> Type -> Type
Parser v a = v -> Either JSONErr a

public export
orElse : Either a b -> Lazy (Either a b) -> Either a b
orElse r@(Right _) _ = r
orElse _           v = v

--------------------------------------------------------------------------------
--          Error Formatting
--------------------------------------------------------------------------------

||| Format a <http://goessner.net/articles/JsonPath/ JSONPath> as a 'String'
||| which represents the path relative to some root object.
export
formatRelativePath : JSONPath -> String
formatRelativePath path = format "" path
  where
    isIdentifierKey : List Char -> Bool
    isIdentifierKey []      = False
    isIdentifierKey (x::xs) = isAlpha x && all isAlphaNum xs

    escapeChar : Char -> String
    escapeChar '\'' = "\\'"
    escapeChar '\\' = "\\\\"
    escapeChar c    = singleton c

    escapeKey : List Char -> String
    escapeKey = fastConcat . map escapeChar

    formatKey : String -> String
    formatKey key =
      let chars = fastUnpack key
       in if isIdentifierKey chars then fastPack $ '.' :: chars
          else "['" ++ escapeKey chars ++ "']"

    format : String -> JSONPath -> String
    format pfx []                = pfx
    format pfx (Index idx :: parts) = format (pfx ++ "[" ++ show idx ++ "]") parts
    format pfx (Key key :: parts)   = format (pfx ++ formatKey key) parts

||| Format a <http://goessner.net/articles/JsonPath/ JSONPath> as a 'String',
||| representing the root object as @$@.
export
formatPath : JSONPath -> String
formatPath path = "$" ++ formatRelativePath path

||| Annotate an error message with a
||| <http://goessner.net/articles/JsonPath/ JSONPath> error location.
export
formatError : JSONPath -> String -> String
formatError path msg = "Error in " ++ formatPath path ++ ": " ++ msg

--------------------------------------------------------------------------------
--          Interface
--------------------------------------------------------------------------------

public export
interface FromJSON a  where
  constructor MkFromJSON
  fromJSON : forall v,obj . Value v obj => Parser v a

export %inline
decodeVia : (0 v : Type) -> Value v obj => FromJSON a => String -> Result a
decodeVia v s = mapFst (Nil,) (parse {v} s) >>= fromJSON

export %inline
decodeEitherVia : (0 v : Type)
                -> Value v obj
                => FromJSON a
                => String
                -> Either String a
decodeEitherVia v = mapFst (uncurry formatError) . decodeVia v

export %inline
decodeMaybeVia : (0 v : Type) -> Value v obj => FromJSON a => String -> Maybe a
decodeMaybeVia v = either (const Nothing) Just . decodeVia v

export %inline
decode : FromJSON a => String -> Result a
decode = decodeVia JSON

export %inline
decodeEither : FromJSON a => String -> Either String a
decodeEither = decodeEitherVia JSON

export %inline
decodeMaybe : FromJSON a => String -> Maybe a
decodeMaybe = decodeMaybeVia JSON

--------------------------------------------------------------------------------
--          Parsing Utilities
--------------------------------------------------------------------------------

export %inline
fail : String -> Result a
fail s = Left (Nil,s)

typeMismatch : Value v obj => String -> Parser v a
typeMismatch expected actual =
  fail $ #"expected \#{expected}, but encountered \#{typeOf actual}"#

unexpected : Value v obj => Parser v a
unexpected actual = fail $ #"unexpected \#{typeOf actual}"#

export %inline
modifyFailure : (String -> String) -> Result a -> Result a
modifyFailure f = mapFst (map f)

||| If the inner 'Parser' failed, prepend the given string to the failure
||| message.
export %inline
prependFailure : String -> Result a -> Result a
prependFailure = modifyFailure . (++)

export %inline
prependContext : String -> Result a -> Result a
prependContext name = prependFailure #"parsing \#{name} failed, "#

infixr 3 <?>, .:, .:?, .:!

export %inline
(<?>) : Result a -> JSONPathElement -> Result a
r <?> elem = mapFst (\(path,s) => (elem :: path,s)) r

withValue :  Value v obj
          => (type : String)
          -> (v -> Maybe t)
          -> (name : Lazy String)
          -> Parser t a
          -> Parser v a
withValue s get n f val = case get val of
                            Just v  => f v
                            Nothing => prependContext n $ typeMismatch s val

export %inline
withObject : Value v obj => Lazy String -> Parser obj a -> Parser v a
withObject = withValue "Object" getObject

export %inline
withBoolean : Value v obj => Lazy String -> Parser Bool a -> Parser v a
withBoolean = withValue "Boolean" getBoolean

export %inline
withString : Value v obj => Lazy String -> Parser String a -> Parser v a
withString = withValue "String" getString

export %inline
withNumber : Value v obj => Lazy String -> Parser Double a -> Parser v a
withNumber = withValue "Number" getNumber

export
withInteger : Value v obj => Lazy String -> Parser Integer a -> Parser v a
withInteger s f =
  withNumber s $ \d =>
    let n = the Integer (cast d)
    in if d == fromInteger n
          then f n
          else fail #"not an integer: \#{show d}"#

export
withLargeInteger : Value v obj => Lazy String -> Parser Integer a -> Parser v a
withLargeInteger s f v =
  withInteger s f v `orElse` withString s parseStr v
  where parseStr : Parser String a
        parseStr str = case parseInteger {a = Integer} str of
                            Nothing => fail #"not an integer: \#{show str}"#
                            Just n  => f n

export
boundedIntegral :  Num a
                => Value v obj
                => Lazy String
                -> (lower : Integer)
                -> (upper : Integer)
                -> Parser v a
boundedIntegral s lo up =
  withInteger s $ \n => if n >= lo && n <= up
                         then pure $ fromInteger n
                         else fail #"integer out of bounds: \#{show n}"#

export
boundedLargeIntegral :  Num a
                     => Value v obj
                     => Lazy String
                     -> (lower : Integer)
                     -> (upper : Integer)
                     -> Parser v a
boundedLargeIntegral s lo up =
  withLargeInteger s $ \n => if n >= lo && n <= up
                              then pure $ fromInteger n
                              else fail #"integer out of bounds: \#{show n}"#

export %inline
withArray : Value v obj => Lazy String -> Parser (List v) a -> Parser v a
withArray = withValue "Array" getArray

||| See `.:`
export
explicitParseField : Object obj v => Value v obj =>
                     Parser v a -> obj -> Parser String a
explicitParseField p o key =
  case lookup key o of
       Nothing => fail #"key \#{show key} not found"#
       Just v  => p v <?> Key key

||| See `.:?`
export
explicitParseFieldMaybe : Object obj v => Value v obj =>
                          Parser v a -> obj -> Parser String (Maybe a)
explicitParseFieldMaybe p o key =
  case lookup key o of
       Nothing => Right Nothing
       Just v  => if isNull v then Right Nothing else Just <$> p v <?> Key key

||| See `.:!`
export
explicitParseFieldMaybe' : Object obj v => Value v obj =>
                           Parser v a -> obj -> Parser String (Maybe a)
explicitParseFieldMaybe' p o key =
  case lookup key o of
       Nothing   => Right Nothing
       Just v    => Just <$> p v <?> Key key

||| Retrieve the value associated with the given key of an `IObject`.
||| The result is `empty` if the key is not present or the value cannot
||| be converted to the desired type.
|||
||| This accessor is appropriate if the key and value /must/ be present
||| in an object for it to be valid.  If the key and value are
||| optional, use `.:?` instead.
export
(.:) : Object obj v => Value v obj => FromJSON a => obj -> Parser String a
(.:) = explicitParseField fromJSON

||| Retrieve the value associated with the given key of an `IObject`. The
||| result is `Nothing` if the key is not present or if its value is `Null`,
||| or `empty` if the value cannot be converted to the desired type.
|||
||| This accessor is most useful if the key and value can be absent
||| from an object without affecting its validity.  If the key and
||| value are mandatory, use `.:` instead.
export
(.:?) : Object obj v => Value v obj => FromJSON a =>
        obj -> Parser String (Maybe a)
(.:?) = explicitParseFieldMaybe fromJSON

||| Retrieve the value associated with the given key of an `IObject`
||| The result is `Nothing` if the key is not present or 'empty' if the
||| value cannot be converted to the desired type.
|||
||| This differs from `.:?` by attempting to parse `Null` the same as any
||| other JSON value, instead of interpreting it as `Nothing`.
export
(.:!) : Object obj v => Value v obj => FromJSON a =>
        obj -> Parser String (Maybe a)
(.:!) = explicitParseFieldMaybe' fromJSON

||| Function variant of `.:`.
export
parseField : Object obj v => Value v obj => FromJSON a =>
             obj -> Parser String a
parseField = (.:)

||| Function variant of `.:?`.
export
parseFieldMaybe : Object obj v => Value v obj => FromJSON a =>
                  obj -> Parser String (Maybe a)
parseFieldMaybe = (.:?)

||| Function variant of `.:!`.
export
parseFieldMaybe' : Object obj v => Value v obj => FromJSON a =>
                   obj -> Parser String (Maybe a)
parseFieldMaybe' = (.:!)

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

export
FromJSON Void where
  fromJSON v = fail "Cannot parse Void"

export
FromJSON () where
  fromJSON = withArray "()" $
    \case Nil    => pure ()
          _ :: _ => fail "parsing () failed, expected empty list"

export
FromJSON Bool where
  fromJSON = withBoolean "Bool" pure

export
FromJSON Double where
  fromJSON = withNumber "Double" pure

export
FromJSON Bits8 where
  fromJSON = boundedIntegral "Bits8" 0 0xff

export
FromJSON Bits16 where
  fromJSON = boundedIntegral "Bits16" 0 0xffff

export
FromJSON Bits32 where
  fromJSON = boundedIntegral "Bits32" 0 0xffffffff

export
FromJSON Bits64 where
  fromJSON = boundedLargeIntegral "Bits64" 0 0xffffffffffffffff

export
FromJSON Int where
  fromJSON = boundedLargeIntegral "Int" (-0x8000000000000000) 0x7fffffffffffffff

export
FromJSON Int8 where
  fromJSON = boundedLargeIntegral "Int8" (-0x80) 0x7f

export
FromJSON Int16 where
  fromJSON = boundedLargeIntegral "Int16" (-0x8000) 0x7fff

export
FromJSON Int32 where
  fromJSON = boundedLargeIntegral "Int32" (-0x80000000) 0x7fffffff

export
FromJSON Int64 where
  fromJSON = boundedLargeIntegral "Int64" (-0x8000000000000000) 0x7fffffffffffffff

export
FromJSON Nat where
  fromJSON = withLargeInteger "Nat" $ \n =>
    if n >= 0 then pure $ fromInteger n
    else fail #"not a natural number: \#{show n}"#

export
FromJSON Integer where
  fromJSON = withLargeInteger "Integer" pure

export
FromJSON String where
  fromJSON = withString "String" pure

export
FromJSON Char where
  fromJSON = withString "Char" $
    \str => case strM str of
                 (StrCons c "") => pure c
                 _ => fail "expected a string of length 1"

export
FromJSON a => FromJSON (Maybe a) where
  fromJSON v = if isNull v then pure Nothing else Just <$> fromJSON v

export
FromJSON a => FromJSON (List a) where
  fromJSON = withArray "List" $ traverse fromJSON

export
FromJSON a => FromJSON (List1 a) where
  fromJSON = withArray "List1" $
    \case Nil    => fail #"expected non-empty list"#
          h :: t => traverse fromJSON (h ::: t)

export
{n : Nat} -> FromJSON a => FromJSON (Vect n a) where
  fromJSON = withArray #"Vect \#{show n}"# $
    \vs => case toVect n vs of
                Just vect => traverse fromJSON vect
                Nothing   => fail #"expected list of length \#{show n}"#

export
(FromJSON a, FromJSON b) => FromJSON (Either a b) where
  fromJSON = withObject "Either" $ \o =>
               map Left (o .: "Left") `orElse` map Right (o .: "Right")

--------------------------------------------------------------------------------
--          SOP Implementations
--------------------------------------------------------------------------------

np : Value v obj => (all : NP (FromJSON . f) ks) => Parser (List v) (NP f ks)
np vs = case fromListNP all vs of
          Just npVS => hctraverse (FromJSON . f) fromJSON npVS
          Nothing   => fail #"expected array of \#{show $ hsize all} values"#

export
NP (FromJSON . f) ks => FromJSON (NP f ks) where
  fromJSON = withArray "NP" np

export
(FromJSON a, FromJSON b) => FromJSON (a,b) where
  fromJSON = map (\[x,y] => (x,y)) . fromJSON {a = NP I [a,b] }

firstSuccess :  NP (K (Parser v a)) ts -> Parser v a
firstSuccess []        _ = fail #"Can't parse nullary sum"#
firstSuccess (f :: []) o = f o
firstSuccess (f :: fs) o = f o `orElse` firstSuccess fs o

ns : Value v obj =>
     (all : NP (FromJSON . f) ks) => Parser v (NS f ks)
ns = withObject "NS"
   $ firstSuccess
   $ hcliftA2 (FromJSON . f) parse (injectionsNP all) (indices all)
  where parse : FromJSON (f a) =>
                (f a -> NS f ks) -> Bits32 -> obj -> Result (NS f ks)
        parse f ix o = map f (o .: show ix)

export
NP (FromJSON . f) ks => FromJSON (NS f ks) where
  fromJSON = ns

||| Decodes a newtype-like sum of products
||| (exactly one single value constructor) by wrapping
||| the decoded value in `MkSOP . Z`.
export
sopNewtype : Value v obj => FromJSON (f k) => Parser v (SOP f [[k]])
sopNewtype = map (\x => MkSOP $ Z [x]) . fromJSON

consAsEnum :  Value v obj
           => String
           -> NP_ (List k) (ConInfo_ k) kss
           -> (0 prf : EnumType kss)
           -> Parser v (NS_ (List k) (NP_ k f) kss)
consAsEnum tn np prf =
  withString tn $ \s => firstSuccess (hliftA2 run np (nullaryInjections np prf)) s
  where run :  ConInfo_ k ks
            -> NS_ (List k) (NP f) kss
            -> Parser String (NS_ (List k) (NP f) kss)
        run i res s = if i.conName == s then Right res
                                        else fail #"expected \#{i.conName}"#

||| Decodes an enum-like sum of products
||| (only nullary constructors) by trying to extract one of the
||| constructors' name
export
sopEnum :  Value v obj
        => TypeInfo' k kss
        -> {auto 0 prf : EnumType kss}
        -> Parser v (SOP f kss)
sopEnum (MkTypeInfo _ tn cs) v = MkSOP <$> consAsEnum tn cs prf v

-- Decodes an applied, record-like constructor as list of key-value pairs.
conFields : Value v obj => NP (FromJSON . f) ks =>
            String -> NP (K String) ks -> Parser v (NP f ks)
conFields cn names = withObject cn $ \o =>
                       hctraverse (FromJSON . f) (parseField o) names

untagged : Value v obj => NP (FromJSON . f) ks =>
           ConInfo ks -> Parser v (NP f ks)
untagged info = maybe fromJSON (conFields info.conName) (argNames info)

||| Decodes a single-constructor sum of products. The
||| constructor's name is ignored.
export
sopRecord : Value v obj => NP (FromJSON . f) ks =>
            TypeInfo [ks] -> Parser v (SOP f [ks])
sopRecord (MkTypeInfo _ n [i]) v = map (MkSOP . Z) (untagged i v)

-- Decodes an applied constructor as a tagged object, if it is record-like,
-- that is, all fields do have a field name. Otherwise, it is
-- encoded as a two-field object, one field for the constructor's name
-- the other for the encoded heterogeneous array.
tagged :  Value v obj
       => NP (FromJSON . f) ks
       => (tagField : String)
       -> (contentField : String)
       -> ConInfo ks
       -> Parser v (NP f ks)
tagged tf cf ci v =
  do nm <- withObject ci.conName (.: tf) v
     if nm == ci.conName
        then case argNames ci of
                  Nothing => withObject ci.conName (.: cf) v
                  Just ns => conFields ci.conName ns v
        else fail #"expected \#{ci.conName}"#

-- Decodes a constructer as a single-field object. The constructor's name
-- is used as the field name.
asObject : Value v obj => NP (FromJSON . f) ks =>
           (typeName : String) -> ConInfo ks -> Parser v (NP f ks)
asObject tn i@(MkConInfo _ n _) =
  withObject tn $ \o => explicitParseField (untagged i) o n

-- Decodes a single constructor as a two element array: The first element
-- being the constructor's name, the second its encoded values.
asTwoElemArray : Value v obj => NP (FromJSON . f) ks =>
                 (typeName : String) -> ConInfo ks -> Parser v (NP f ks)
asTwoElemArray tn i@(MkConInfo _ cn _) =
  withArray tn $ \vs => case vs of
                             [n,c] => do n2 <- fromJSON n
                                         if n2 == cn
                                            then untagged i c
                                            else fail #"expected \#{cn} but got \#{n2}"#
                             _     => fail #"expected 2-element array"#

||| Decodes a sum of products as specified by the passed
||| `SumEncoding` (see its documentation for details) using
||| the given `TypeInfo` to decode constructor and argument names.
|||
||| See also `sopRecord` for decoding values with a single constructor,
||| `sopEnum` for decoding enum types (only nullary constructors),
||| and `sopNewtype` for decoding newtype wrappers.
export
sop : Value v obj
    => (all : POP (FromJSON . f) kss)
    => SumEncoding
    -> TypeInfo' k kss
    -> Parser v (SOP_ k f kss)
sop {all = MkPOP nps} enc (MkTypeInfo _ tn cs) =
  case enc of
       UntaggedValue         => impl untagged
       ObjectWithSingleField => impl (asObject tn)
       TwoElemArray          => impl (asTwoElemArray tn)
       (TaggedObject tf cf)  => impl (tagged tf cf)

  where injSOP : NP_ (List k) (InjectionSOP f kss) kss
        injSOP = hmap (MkSOP .) $ injectionsNP nps

        impl : (forall ks . NP (FromJSON . f) ks =>
                            ConInfo ks -> Parser v (NP f ks))
             -> Parser v (SOP f kss)
        impl g = firstSuccess $ hcliftA2 (NP $ FromJSON . f) apply injSOP cs
          where apply :  NP_ k (FromJSON . f) ts
                      => (NP_ k f ts -> SOP_ k f kss)
                      -> ConInfo_ k ts
                      -> Parser v (SOP_ k f kss)
                apply f c = map f . g c

--------------------------------------------------------------------------------
--          Generic Decoders
--------------------------------------------------------------------------------

||| Generic version of `sopNewtype`.
export
genNewtypeFromJSON : Value v obj => Generic a [[k]] => FromJSON k => Parser v a
genNewtypeFromJSON = map to . sopNewtype

||| Generic version of `sopEnum`.
export
genEnumFromJSON :  Value v obj => Meta a kss => {auto 0 prf : EnumType kss}
                -> Parser v a
genEnumFromJSON = map to . sopEnum (metaFor a)

||| Like `genEnumFromJSON`, but uses the given function to adjust
||| constructor names before being used as tags.
export
genEnumFromJSON' :  Value v obj => Meta a kss => {auto 0 prf : EnumType kss}
                 -> (String -> String) -> Parser v a
genEnumFromJSON' f = let meta = adjustConnames f (metaFor a)
                      in map to . sopEnum meta {prf}

||| Generic version of `sopRecord`.
export
genRecordFromJSON : Value v obj => Meta a [ks] => NP FromJSON ks => Parser v a
genRecordFromJSON = map to . sopRecord (metaFor a)

||| Like `genRecordFromJSON`, but uses the given function to adjust
||| field names before being used as tags.
export
genRecordFromJSON' : Value v obj => Meta a [ks] => NP FromJSON ks =>
                     (String -> String) -> Parser v a
genRecordFromJSON' f = let meta = adjustFieldNames f (metaFor a)
                        in map to . sopRecord meta

export
genFromJSON : Value v obj => Meta a code => POP FromJSON code =>
              SumEncoding -> Parser v a
genFromJSON enc = map to . sop enc (metaFor a)

export
genFromJSON' :  Value v obj
             => Meta a code
             => POP FromJSON code
             => (adjFieldLabel : String -> String)
             -> (adjConstructorTag : String -> String)
             -> SumEncoding
             -> Parser v a
genFromJSON' ff fc enc = let meta = adjustInfo ff fc (metaFor a)
                          in map to . sop enc meta

--------------------------------------------------------------------------------
--          Elab Deriving
--------------------------------------------------------------------------------

namespace Derive
  export
  customFromJSON : TTImp -> DeriveUtil -> InterfaceImpl
  customFromJSON tti g = MkInterfaceImpl "FromJSON" Export []
                           `(MkFromJSON ~(tti))
                           (implementationType `(FromJSON) g)

  ||| Derives a `FromJSON` implementation for the given data type
  export
  FromJSON : DeriveUtil -> InterfaceImpl
  FromJSON = customFromJSON `(genFromJSON defaultTaggedObject)

  ||| Derives a `FromJSON` implementation for the given single-constructor
  ||| data type
  export
  RecordFromJSON : DeriveUtil -> InterfaceImpl
  RecordFromJSON = customFromJSON `(genRecordFromJSON)

  ||| Derives a `FromJSON` implementation for the given enum type
  export
  EnumFromJSON : DeriveUtil -> InterfaceImpl
  EnumFromJSON = customFromJSON `(\v => genEnumFromJSON v)

  ||| Derives a `FromJSON` implementation for the given newtype
  export
  NewtypeFromJSON : DeriveUtil -> InterfaceImpl
  NewtypeFromJSON = customFromJSON `(genNewtypeFromJSON)


text:
module Network.TLS.Parsing

import Data.List1
import Data.Vect
import Utils.Bytes
import public Utils.Parser

namespace Parserializer
  ||| bidirectional serializer
  ||| `decode` is assumed to be the inverse of `encode` and vice versa
  public export
  record Parserializer (c : Type) (i : Type) (e : Type) (a : Type) where
    constructor MkParserializer
    encode : a -> List c
    decode : Parser i e a

  infixr 5 <*>>

  export
  apair : (Semigroup e, Monoid i) => Parserializer c i e a -> Parserializer c i e b -> Parserializer c i e (a, b)
  apair ma mb = MkParserializer (\(a, b) => ma.encode a <+> mb.encode b) $ (,) <$> ma.decode <*> mb.decode

  ||| infixr for `apair`
  export
  (<*>>) : (Semigroup e, Monoid i) => Parserializer c i e a -> Parserializer c i e b -> Parserializer c i e (a, b)
  (<*>>) = apair

  export
  map : (to : a -> b) -> (from : b -> a) -> Parserializer c i e a -> Parserializer c i e b
  map to from pser = MkParserializer (pser.encode . from) (map to pser.decode)

  export
  mapEither : (Semigroup e, Monoid i) => (to : a -> Either e b) -> (from : b -> a) -> Parserializer c i e a -> Parserializer c i e b
  mapEither to from pser = MkParserializer (pser.encode . from) $ do
    a <- pser.decode
    case to a of
      Right b => pure b
      Left e => fail e

  export
  (*>) : (Semigroup e, Monoid i) => Parserializer c i e () -> Parserializer c i e a -> Parserializer c i e a
  ma *> mb = map snd ((),) (ma <*>> mb)

  export
  (<*) : (Semigroup e, Monoid i) => Parserializer c i e a -> Parserializer c i e () -> Parserializer c i e a
  ma <* mb = map fst (,()) (ma <*>> mb)

  export
  aeither : (Semigroup e, Monoid i) => Parserializer c i e a -> Parserializer c i e b -> Parserializer c i e (Either a b)
  aeither ma mb = MkParserializer (either ma.encode mb.encode) $ (map Left ma.decode) <|> (map Right mb.decode)

  export
  (<|>) : (Semigroup e, Monoid i) => Parserializer c i e a -> Parserializer c i e b -> Parserializer c i e (Either a b)
  (<|>) = aeither

||| essentially (Nat, `a`), where Nat denotes the position, usually starts with 0
public export
record Posed (a : Type) where
  constructor MkPosed
  pos : Nat
  get : a

||| `Parser.token` but for `Posed`
export
p_get : Cons (Posed c) i => Parser i e c
p_get = map get token

-- serializer utils

||| prepend the length of `body` into `n` bytes in big endian
export
prepend_length : (n : Nat) -> (body : List Bits8) -> List Bits8
prepend_length n body = (toList $ integer_to_be n $ cast $ length body) <+> body

-- parser utils

||| parse the next `n` bytes as a natural number in big endian style
export
p_nat : (Semigroup e, Monoid i, Cons (Posed Bits8) i) => (n : Nat) -> Parser i e Nat
p_nat n = cast {to = Nat} . be_to_integer <$> count n p_get

||| make sure that `p` MUST consume at least `n` tokens, fails otherwise
public export
p_exact : (Cons c i, Monoid i) => (n : Nat) -> (p : Parser i (SimpleError String) a) -> Parser i (SimpleError String) a
p_exact Z (Pure leftover x) = pure x
p_exact (S i) (Pure leftover x) = fail $ msg $ "over fed, " <+> show (S i) <+> " bytes more to go"
p_exact i (Fail msg) = fail msg
p_exact Z parser = fail $ msg $ "under fed, wants more"
p_exact (S i) parser = do
  b <- token
  p_exact i (feed (singleton b) parser)

--- parserializer utils

||| put parser error messages under another message
||| used for creating a treeish error message
export
under : e -> Parserializer c i (SimpleError e) a -> Parserializer c i (SimpleError e) a
under msg pser = MkParserializer pser.encode (under msg pser.decode)

||| parserialize a single posed token
export
token : (Semigroup e, Cons (Posed c) i, Monoid i) => Parserializer c i e c
token = MkParserializer pure p_get

||| parserialize `n` posed tokens
export
ntokens : (Semigroup e, Cons (Posed c) i, Monoid i) => (n : Nat) -> Parserializer c i e (Vect n c)
ntokens n = MkParserializer (toList) (count n p_get)

||| parserialize the next `n` bytes in big endian style as a length describing the number of bytes of the following data to be fed to `pser`
export
lengthed : (Cons (Posed Bits8) i, Monoid i) => (n : Nat) -> (pser : Parserializer Bits8 i (SimpleError String) a) -> Parserializer Bits8 i (SimpleError String) a
lengthed n pser = MkParserializer (prepend_length n . pser.encode) $ do
  len <- p_nat n
  p_exact len pser.decode

||| parserialize the next `n` bytes in big endian style as a length describing the number of bytes of the following data to be fed to `pser`
||| when `pser` completes, the result becomes an entry in the resulting list
||| when there are exactly zero bytes left, the list of results is returned
||| if under feeding `pser` for the last entry, the parser fails
export
lengthed_list : (Cons (Posed Bits8) i, Monoid i) => (n : Nat) -> (pser : Parserializer Bits8 i (SimpleError String) a) -> Parserializer Bits8 i (SimpleError String) (List a)
lengthed_list youmu pser = MkParserializer (prepend_length youmu . concat . map pser.encode) $ do
  S len <- p_nat youmu
  | Z => pure []
  go (S len) pser.decode
  where
  go : Nat -> Parser i (SimpleError String) a -> Parser i (SimpleError String) (List a)
  go Z (Pure leftover x) = pure [x]
  go (S i) (Pure leftover x) = (x ::) <$> go (S i) pser.decode
  go i (Fail msg) = fail msg
  go Z parser = fail $ msg $ "under fed, want more"
  go (S i) parser = do
    b <- token
    go i (feed (singleton b) parser)

||| `lengthed_list` but `List1`
export
lengthed_list1 : (Cons (Posed Bits8) i, Monoid i) => (youmu : Nat) -> Parserializer Bits8 i (SimpleError String) a -> Parserializer Bits8 i (SimpleError String) (List1 a)
lengthed_list1 youmu pser =
  let
    pser' = lengthed_list youmu pser
  in
    MkParserializer (pser'.encode . toList) $ do
      (x :: xs) <- pser'.decode
      | [] => fail $ msg $ "empty list"
      pure (x ::: xs)

||| basically the parserializer version of `p_nat`
export
nat : Semigroup e => (Cons (Posed Bits8) i, Monoid i) => (n : Nat) -> Parserializer Bits8 i e Nat
nat n = MkParserializer (toList . integer_to_be n . cast) (p_nat n)

||| parserialize a list of bytes with nice error messages specialized for displaying byte sequences
export
is : (Cons (Posed Bits8) i, Monoid i) => {k : Nat} -> Vect (S k) Bits8 -> Parserializer Bits8 i (SimpleError String) ()
is cs = MkParserializer (const $ toList cs) $ do
  bs <- count (S k) token
  let cs' = map get bs
  case cs == cs' of
    True => pure ()
    False =>
      let
        (begin, end) = mapHom pos (head bs, last bs)
      in
        fail $ msg $ "at position " <+> show begin <+> "-" <+> show end <+> ", expected " <+> xxd (toList cs) <+> " but got " <+> xxd (toList cs')


text:
module TTImp.Parser

import Core.Context
import Core.Core
import Core.Metadata
import Core.Env
import Core.TT
import Parser.Source
import TTImp.TTImp

import public Libraries.Text.Parser
import Data.List
import Data.List.Views
import Data.List1
import Data.Maybe
import Data.String

topDecl : OriginDesc -> IndentInfo -> Rule ImpDecl
-- All the clauses get parsed as one-clause definitions. Collect any
-- neighbouring clauses with the same function name into one definition.
export
collectDefs : List ImpDecl -> List ImpDecl

%default covering

%hide Prelude.(>>=)
%hide Prelude.(>>)
%hide Core.Core.(>>=)
%hide Prelude.pure
%hide Core.Core.pure

%hide Lexer.Core.(<|>)
%hide Prelude.(<|>)

atom : OriginDesc -> Rule RawImp
atom fname
    = do start <- location
         x <- constant
         end <- location
         pure (IPrimVal (MkFC fname start end) x)
  <|> do start <- location
         str <- simpleStr
         end <- location
         pure (IPrimVal (MkFC fname start end) (Str str))
  <|> do start <- location
         exactIdent "Type"
         end <- location
         pure (IType (MkFC fname start end))
  <|> do start <- location
         symbol "_"
         end <- location
         pure (Implicit (MkFC fname start end) True)
  <|> do start <- location
         symbol "?"
         end <- location
         pure (Implicit (MkFC fname start end) False)
  <|> do start <- location
         pragma "search"
         end <- location
         pure (ISearch (MkFC fname start end) 1000)
  <|> do start <- location
         x <- name
         end <- location
         pure (IVar (MkFC fname start end) x)
  <|> do start <- location
         symbol "$"
         x <- unqualifiedName
         end <- location
         pure (IBindVar (MkFC fname start end) x)
  <|> do start <- location
         x <- holeName
         end <- location
         pure (IHole (MkFC fname start end) x)

visOption : Rule Visibility
visOption
    = do keyword "public"
         keyword "export"
         pure Public
  <|> do keyword "export"
         pure Export
  <|> do keyword "private"
         pure Private

visibility : EmptyRule Visibility
visibility
    = visOption
  <|> pure Private

totalityOpt : Rule TotalReq
totalityOpt
    = do keyword "partial"
         pure PartialOK
  <|> do keyword "total"
         pure Total
  <|> do keyword "covering"
         pure CoveringOnly

fnOpt : Rule FnOpt
fnOpt = do x <- totalityOpt
           pure $ Totality x

fnDirectOpt : Rule FnOpt
fnDirectOpt
    = do pragma "hint"
         pure (Hint True)
  <|> do pragma "chaser"
         pure (Hint False)
  <|> do pragma "globalhint"
         pure (GlobalHint True)
  <|> do pragma "defaulthint"
         pure (GlobalHint False)
  <|> do pragma "inline"
         pure Inline
  <|> do pragma "extern"
         pure ExternFn

visOpt : Rule (Either Visibility FnOpt)
visOpt
    = do vis <- visOption
         pure (Left vis)
  <|> do tot <- fnOpt
         pure (Right tot)
  <|> do opt <- fnDirectOpt
         pure (Right opt)

getVisibility : Maybe Visibility -> List (Either Visibility FnOpt) ->
                EmptyRule Visibility
getVisibility Nothing [] = pure Private
getVisibility (Just vis) [] = pure vis
getVisibility Nothing (Left x :: xs) = getVisibility (Just x) xs
getVisibility (Just vis) (Left x :: xs)
   = fatalError "Multiple visibility modifiers"
getVisibility v (_ :: xs) = getVisibility v xs

getRight : Either a b -> Maybe b
getRight (Left _) = Nothing
getRight (Right v) = Just v

bindSymbol : Rule (PiInfo RawImp)
bindSymbol
    = do symbol "->"
         pure Explicit
  <|> do symbol "=>"
         pure AutoImplicit

mutual
  appExpr : OriginDesc -> IndentInfo -> Rule RawImp
  appExpr fname indents
      = case_ fname indents
    <|> lazy fname indents
    <|> do start <- location
           f <- simpleExpr fname indents
           args <- many (argExpr fname indents)
           end <- location
           pure (applyExpImp start end f args)
    where
      applyExpImp : FilePos -> FilePos ->
                    RawImp -> List (Either RawImp (Maybe Name, RawImp)) ->
                    RawImp
      applyExpImp start end f [] = f
      applyExpImp start end f (Left exp :: args)
          = applyExpImp start end (IApp (MkFC fname start end) f exp) args
      applyExpImp start end f (Right (Just n, imp) :: args)
          = applyExpImp start end (INamedApp (MkFC fname start end) f n imp) args
      applyExpImp start end f (Right (Nothing, imp) :: args)
          = applyExpImp start end (IAutoApp (MkFC fname start end) f imp) args

  argExpr : OriginDesc -> IndentInfo ->
            Rule (Either RawImp (Maybe Name, RawImp))
  argExpr fname indents
      = do continue indents
           arg <- simpleExpr fname indents
           pure (Left arg)
    <|> do continue indents
           arg <- implicitArg fname indents
           pure (Right arg)

  implicitArg : OriginDesc -> IndentInfo -> Rule (Maybe Name, RawImp)
  implicitArg fname indents
      = do start <- location
           symbol "{"
           x <- UN . Basic <$> unqualifiedName
           (do symbol "="
               commit
               tm <- expr fname indents
               symbol "}"
               pure (Just x, tm))
             <|> (do symbol "}"
                     end <- location
                     pure (Just x, IVar (MkFC fname start end) x))
    <|> do symbol "@{"
           commit
           tm <- expr fname indents
           symbol "}"
           pure (Nothing, tm)

  as : OriginDesc -> IndentInfo -> Rule RawImp
  as fname indents
      = do start <- location
           x <- UN . Basic <$> unqualifiedName
           nameEnd <- location
           symbol "@"
           pat <- simpleExpr fname indents
           end <- location
           pure (IAs (MkFC fname start end) (MkFC fname start nameEnd) UseRight x pat)

  simpleExpr : OriginDesc -> IndentInfo -> Rule RawImp
  simpleExpr fname indents
      = as fname indents
    <|> atom fname
    <|> binder fname indents
    <|> rewrite_ fname indents
    <|> record_ fname indents
    <|> do symbol "("
           e <- expr fname indents
           symbol ")"
           pure e

  multiplicity : EmptyRule (Maybe Integer)
  multiplicity
      = do c <- intLit
           pure (Just c)
    <|> pure Nothing

  getMult : Maybe Integer -> EmptyRule RigCount
  getMult (Just 0) = pure erased
  getMult (Just 1) = pure linear
  getMult Nothing = pure top
  getMult _ = fatalError "Invalid multiplicity (must be 0 or 1)"

  pibindAll : FC -> PiInfo RawImp -> List (RigCount, Maybe Name, RawImp) ->
              RawImp -> RawImp
  pibindAll fc p [] scope = scope
  pibindAll fc p ((rig, n, ty) :: rest) scope
           = IPi fc rig p n ty (pibindAll fc p rest scope)

  bindList : OriginDesc -> FilePos -> IndentInfo ->
             Rule (List (RigCount, Name, RawImp))
  bindList fname start indents
      = forget <$> sepBy1 (symbol ",")
                          (do rigc <- multiplicity
                              n <- unqualifiedName
                              end <- location
                              ty <- option
                                       (Implicit (MkFC fname start end) False)
                                       (do symbol ":"
                                           appExpr fname indents)
                              rig <- getMult rigc
                              pure (rig, UN (Basic n), ty))

  pibindListName : OriginDesc -> FilePos -> IndentInfo ->
                   Rule (List (RigCount, Name, RawImp))
  pibindListName fname start indents
       = do rigc <- multiplicity
            ns <- sepBy1 (symbol ",") unqualifiedName
            symbol ":"
            ty <- expr fname indents
            atEnd indents
            rig <- getMult rigc
            pure (map (\n => (rig, UN (Basic n), ty)) (forget ns))
     <|> forget <$> sepBy1 (symbol ",")
                           (do rigc <- multiplicity
                               n <- name
                               symbol ":"
                               ty <- expr fname indents
                               rig <- getMult rigc
                               pure (rig, n, ty))

  pibindList : OriginDesc -> FilePos -> IndentInfo ->
               Rule (List (RigCount, Maybe Name, RawImp))
  pibindList fname start indents
    = do params <- pibindListName fname start indents
         pure $ map (\(rig, n, ty) => (rig, Just n, ty)) params

  autoImplicitPi : OriginDesc -> IndentInfo -> Rule RawImp
  autoImplicitPi fname indents
      = do start <- location
           symbol "{"
           keyword "auto"
           commit
           binders <- pibindList fname start indents
           symbol "}"
           symbol "->"
           scope <- typeExpr fname indents
           end <- location
           pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)

  forall_ : OriginDesc -> IndentInfo -> Rule RawImp
  forall_ fname indents
      = do start <- location
           keyword "forall"
           commit
           nstart <- location
           ns <- sepBy1 (symbol ",") unqualifiedName
           nend <- location
           let nfc = MkFC fname nstart nend
           let binders = map (\n => ( erased {a=RigCount}
                                    , Just (UN $ Basic n)
                                    , Implicit nfc False))
                             (forget ns)
           symbol "."
           scope <- typeExpr fname indents
           end <- location
           pure (pibindAll (MkFC fname start end) Implicit binders scope)

  implicitPi : OriginDesc -> IndentInfo -> Rule RawImp
  implicitPi fname indents
      = do start <- location
           symbol "{"
           binders <- pibindList fname start indents
           symbol "}"
           symbol "->"
           scope <- typeExpr fname indents
           end <- location
           pure (pibindAll (MkFC fname start end) Implicit binders scope)

  explicitPi : OriginDesc -> IndentInfo -> Rule RawImp
  explicitPi fname indents
      = do start <- location
           symbol "("
           binders <- pibindList fname start indents
           symbol ")"
           exp <- bindSymbol
           scope <- typeExpr fname indents
           end <- location
           pure (pibindAll (MkFC fname start end) exp binders scope)

  lam : OriginDesc -> IndentInfo -> Rule RawImp
  lam fname indents
      = do start <- location
           symbol "\\"
           binders <- bindList fname start indents
           symbol "=>"
           mustContinue indents Nothing
           scope <- expr fname indents
           end <- location
           pure (bindAll (MkFC fname start end) binders scope)
     where
       bindAll : FC -> List (RigCount, Name, RawImp) -> RawImp -> RawImp
       bindAll fc [] scope = scope
       bindAll fc ((rig, n, ty) :: rest) scope
           = ILam fc rig Explicit (Just n) ty (bindAll fc rest scope)

  let_ : OriginDesc -> IndentInfo -> Rule RawImp
  let_ fname indents
      = do start <- location
           keyword "let"
           rigc <- multiplicity
           rig <- getMult rigc
           n <- bounds name
           symbol "="
           commit
           val <- expr fname indents
           continue indents
           keyword "in"
           scope <- typeExpr fname indents
           end <- location
           pure (let fc = MkFC fname start end in
                     ILet fc (boundToFC fname n) rig n.val (Implicit fc False) val scope)
    <|> do start <- location
           keyword "let"
           ds <- block (topDecl fname)
           continue indents
           keyword "in"
           scope <- typeExpr fname indents
           end <- location
           pure (ILocal (MkFC fname start end) (collectDefs ds) scope)

  case_ : OriginDesc -> IndentInfo -> Rule RawImp
  case_ fname indents
      = do start <- location
           keyword "case"
           scr <- expr fname indents
           keyword "of"
           alts <- block (caseAlt fname)
           end <- location
           pure (let fc = MkFC fname start end in
                     ICase fc scr (Implicit fc False) alts)

  caseAlt : OriginDesc -> IndentInfo -> Rule ImpClause
  caseAlt fname indents
      = do start <- location
           lhs <- appExpr fname indents
           caseRHS fname indents start lhs

  caseRHS : OriginDesc -> IndentInfo -> (Int, Int) -> RawImp ->
            Rule ImpClause
  caseRHS fname indents start lhs
      = do symbol "=>"
           continue indents
           rhs <- expr fname indents
           atEnd indents
           end <- location
           pure (PatClause (MkFC fname start end) lhs rhs)
    <|> do keyword "impossible"
           atEnd indents
           end <- location
           pure (ImpossibleClause (MkFC fname start end) lhs)

  record_ : OriginDesc -> IndentInfo -> Rule RawImp
  record_ fname indents
      = do start <- location
           keyword "record"
           symbol "{"
           commit
           fs <- sepBy1 (symbol ",") (field fname indents)
           symbol "}"
           sc <- expr fname indents
           end <- location
           pure (IUpdate (MkFC fname start end) (forget fs) sc)

  field : OriginDesc -> IndentInfo -> Rule IFieldUpdate
  field fname indents
      = do path <- sepBy1 (symbol "->") unqualifiedName
           upd <- (do symbol "="; pure ISetField)
                      <|>
                  (do symbol "$="; pure ISetFieldApp)
           val <- appExpr fname indents
           pure (upd (forget path) val)

  rewrite_ : OriginDesc -> IndentInfo -> Rule RawImp
  rewrite_ fname indents
      = do start <- location
           keyword "rewrite"
           rule <- expr fname indents
           keyword "in"
           tm <- expr fname indents
           end <- location
           pure (IRewrite (MkFC fname start end) rule tm)

  lazy : OriginDesc -> IndentInfo -> Rule RawImp
  lazy fname indents
      = do start <- location
           exactIdent "Lazy"
           tm <- simpleExpr fname indents
           end <- location
           pure (IDelayed (MkFC fname start end) LLazy tm)
    <|> do start <- location
           exactIdent "Inf"
           tm <- simpleExpr fname indents
           end <- location
           pure (IDelayed (MkFC fname start end) LInf tm)
    <|> do start <- location
           exactIdent "Delay"
           tm <- simpleExpr fname indents
           end <- location
           pure (IDelay (MkFC fname start end) tm)
    <|> do start <- location
           exactIdent "Force"
           tm <- simpleExpr fname indents
           end <- location
           pure (IForce (MkFC fname start end) tm)

  binder : OriginDesc -> IndentInfo -> Rule RawImp
  binder fname indents
      = autoImplicitPi fname indents
    <|> forall_ fname indents
    <|> implicitPi fname indents
    <|> explicitPi fname indents
    <|> lam fname indents
    <|> let_ fname indents

  typeExpr : OriginDesc -> IndentInfo -> Rule RawImp
  typeExpr fname indents
      = do start <- location
           arg <- appExpr fname indents
           (do continue indents
               rest <- some (do exp <- bindSymbol
                                op <- appExpr fname indents
                                pure (exp, op))
               end <- location
               pure (mkPi start end arg (forget rest)))
             <|> pure arg
    where
      mkPi : FilePos -> FilePos -> RawImp -> List (PiInfo RawImp, RawImp) -> RawImp
      mkPi start end arg [] = arg
      mkPi start end arg ((exp, a) :: as)
            = IPi (MkFC fname start end) top exp Nothing arg
                  (mkPi start end a as)

  export
  expr : OriginDesc -> IndentInfo -> Rule RawImp
  expr = typeExpr

tyDecl : OriginDesc -> IndentInfo -> Rule ImpTy
tyDecl fname indents
    = do start <- location
         n <- name
         nameEnd <- location
         symbol ":"
         ty <- expr fname indents
         end <- location
         atEnd indents
         pure (MkImpTy (MkFC fname start end) (MkFC fname start nameEnd) n ty)

mutual
  parseRHS : (withArgs : Nat) ->
             OriginDesc -> IndentInfo -> (Int, Int) -> RawImp ->
             Rule (Name, ImpClause)
  parseRHS withArgs fname indents start lhs
      = do symbol "="
           commit
           rhs <- expr fname indents
           atEnd indents
           end <- location
           let fc = MkFC fname start end
           pure (!(getFn lhs), PatClause fc lhs rhs)
    <|> do keyword "with"
           wstart <- location
           symbol "("
           wval <- expr fname indents
           symbol ")"
           prf <- optional (keyword "proof" *> name)
           ws <- nonEmptyBlock (clause (S withArgs) fname)
           end <- location
           let fc = MkFC fname start end
           pure (!(getFn lhs), WithClause fc lhs wval prf [] (forget $ map snd ws))

    <|> do keyword "impossible"
           atEnd indents
           end <- location
           let fc = MkFC fname start end
           pure (!(getFn lhs), ImpossibleClause fc lhs)
    where
      getFn : RawImp -> EmptyRule Name
      getFn (IVar _ n) = pure n
      getFn (IApp _ f a) = getFn f
      getFn (IAutoApp _ f a) = getFn f
      getFn (INamedApp _ f _ a) = getFn f
      getFn _ = fail "Not a function application"

  clause : Nat -> OriginDesc -> IndentInfo -> Rule (Name, ImpClause)
  clause withArgs fname indents
      = do start <- location
           lhs <- expr fname indents
           extra <- many parseWithArg
           ifThenElse (withArgs /= length extra)
              (fatalError "Wrong number of 'with' arguments")
              (parseRHS withArgs fname indents start (applyArgs lhs extra))
    where
      applyArgs : RawImp -> List (FC, RawImp) -> RawImp
      applyArgs f [] = f
      applyArgs f ((fc, a) :: args) = applyArgs (IApp fc f a) args

      parseWithArg : Rule (FC, RawImp)
      parseWithArg
          = do symbol "|"
               start <- location
               tm <- expr fname indents
               end <- location
               pure (MkFC fname start end, tm)

definition : OriginDesc -> IndentInfo -> Rule ImpDecl
definition fname indents
    = do start <- location
         nd <- clause 0 fname indents
         end <- location
         pure (IDef (MkFC fname start end) (fst nd) [snd nd])

dataOpt : Rule DataOpt
dataOpt
    = do exactIdent "noHints"
         pure NoHints
  <|> do exactIdent "uniqueSearch"
         pure UniqueSearch
  <|> do exactIdent "search"
         ns <- forget <$> some name
         pure (SearchBy ns)

dataDecl : OriginDesc -> IndentInfo -> Rule ImpData
dataDecl fname indents
    = do start <- location
         keyword "data"
         n <- name
         symbol ":"
         ty <- expr fname indents
         keyword "where"
         opts <- option [] (do symbol "["
                               dopts <- sepBy1 (symbol ",") dataOpt
                               symbol "]"
                               pure $ forget dopts)
         cs <- block (tyDecl fname)
         end <- location
         pure (MkImpData (MkFC fname start end) n ty opts cs)

recordParam : OriginDesc -> IndentInfo -> Rule (List (Name, RigCount, PiInfo RawImp, RawImp))
recordParam fname indents
    = do symbol "("
         start <- location
         params <- pibindListName fname start indents
         symbol ")"
         pure $ map (\(c, n, tm) => (n, c, Explicit, tm)) params
  <|> do symbol "{"
         commit
         start <- location
         info <- (pure  AutoImplicit <* keyword "auto"
              <|>(do
                  keyword "default"
                  t <- simpleExpr fname indents
                  pure $ DefImplicit t)
              <|> pure      Implicit)
         params <- pibindListName fname start indents
         symbol "}"
         pure $ map (\(c, n, tm) => (n, c, info, tm)) params
  <|> do start <- location
         n <- name
         end <- location
         pure [(n, top, Explicit, Implicit (MkFC fname start end) False)]

fieldDecl : OriginDesc -> IndentInfo -> Rule (List IField)
fieldDecl fname indents
      = do symbol "{"
           commit
           fs <- fieldBody Implicit
           symbol "}"
           atEnd indents
           pure fs
    <|> do fs <- fieldBody Explicit
           atEnd indents
           pure fs
  where
    fieldBody : PiInfo RawImp -> Rule (List IField)
    fieldBody p
        = do start <- location
             ns <- sepBy1 (symbol ",") unqualifiedName
             symbol ":"
             ty <- expr fname indents
             end <- location
             pure (map (\n => MkIField (MkFC fname start end)
                                       linear p (UN $ Basic n) ty) (forget ns))

recordDecl : OriginDesc -> IndentInfo -> Rule ImpDecl
recordDecl fname indents
    = do start <- location
         vis <- visibility
         col <- column
         keyword "record"
         commit
         n <- name
         paramss <- many (recordParam fname indents)
         let params = concat paramss
         keyword "where"
         exactIdent "constructor"
         dc <- name
         flds <- assert_total (blockAfter col (fieldDecl fname))
         end <- location
         pure (let fc = MkFC fname start end in
                   IRecord fc Nothing vis
                           (MkImpRecord fc n params dc (concat flds)))

namespaceDecl : Rule Namespace
namespaceDecl
    = do keyword "namespace"
         commit
         namespaceId

logLevel : Rule (Maybe (List String, Nat))
logLevel
  = (Nothing <$ exactIdent "off")
    <|> do topic <- option [] ((::) <$> unqualifiedName <*> many aDotIdent)
           lvl <- intLit
           pure (Just (topic, fromInteger lvl))

directive : OriginDesc -> IndentInfo -> Rule ImpDecl
directive fname indents
    = do pragma "logging"
         commit
         lvl <- logLevel
         atEnd indents
         pure (ILog lvl)
  <|> do b <- bounds (do pragma "builtin"
                         commit
                         t <- builtinType
                         n <- name
                         pure (t, n))
         (t, n) <- pure b.val
         pure $ IBuiltin (boundToFC fname b) t n

         {- Can't do IPragma due to lack of Ref Ctxt. Should we worry about this?
  <|> do pragma "pair"
         commit
         start <- location
         p <- name
         f <- name
         s <- name
         end <- location
         pure (let fc = MkFC fname start end in
                   IPragma (\nest, env => setPair {c} fc p f s))
  <|> do pragma "rewrite"
         commit
         start <- location
         eq <- name
         rw <- name
         end <- location
         pure (let fc = MkFC fname start end in
                   IPragma (\c, nest, env => setRewrite {c} fc eq rw))
    -}
-- Declared at the top
-- topDecl : OriginDesc -> IndentInfo -> Rule ImpDecl
topDecl fname indents
    = do start <- location
         vis <- visibility
         dat <- dataDecl fname indents
         end <- location
         pure (IData (MkFC fname start end) vis dat)
  <|> do start <- location
         ns <- namespaceDecl
         ds <- assert_total (nonEmptyBlock (topDecl fname))
         end <- location
         pure (INamespace (MkFC fname start end) ns (forget ds))
  <|> do start <- location
         visOpts <- many visOpt
         vis <- getVisibility Nothing visOpts
         let opts = mapMaybe getRight visOpts
         m <- multiplicity
         rig <- getMult m
         claim <- tyDecl fname indents
         end <- location
         pure (IClaim (MkFC fname start end) rig vis opts claim)
  <|> recordDecl fname indents
  <|> directive fname indents
  <|> definition fname indents

-- Declared at the top
-- collectDefs : List ImpDecl -> List ImpDecl
collectDefs [] = []
collectDefs (IDef loc fn cs :: ds)
    = let (cs', rest) = spanMap (isClause fn) ds in
          IDef loc fn (cs ++ cs') :: assert_total (collectDefs rest)
  where
    spanMap : (a -> Maybe (List b)) -> List a -> (List b, List a)
    spanMap f [] = ([], [])
    spanMap f (x :: xs) = case f x of
                               Nothing => ([], x :: xs)
                               Just y => case spanMap f xs of
                                              (ys, zs) => (y ++ ys, zs)

    isClause : Name -> ImpDecl -> Maybe (List ImpClause)
    isClause n (IDef _ n' cs)
        = if n == n' then Just cs else Nothing
    isClause n _ = Nothing
collectDefs (INamespace loc ns nds :: ds)
    = INamespace loc ns (collectDefs nds) :: collectDefs ds
collectDefs (d :: ds)
    = d :: collectDefs ds

-- full programs
export
prog : OriginDesc -> Rule (List ImpDecl)
prog fname
    = do ds <- nonEmptyBlock (topDecl fname)
         pure (collectDefs $ forget ds)

-- TTImp REPL commands
export
command : Rule ImpREPL
command
    = do symbol ":"; exactIdent "t"
         tm <- expr (Virtual Interactive) init
         pure (Check tm)
  <|> do symbol ":"; exactIdent "s"
         n <- name
         pure (ProofSearch n)
  <|> do symbol ":"; exactIdent "es"
         n <- name
         pure (ExprSearch n)
  <|> do symbol ":"; exactIdent "gd"
         l <- intLit
         n <- name
         pure (GenerateDef (fromInteger l) n)
  <|> do symbol ":"; exactIdent "missing"
         n <- name
         pure (Missing n)
  <|> do symbol ":"; keyword "total"
         n <- name
         pure (CheckTotal n)
  <|> do symbol ":"; exactIdent "di"
         n <- name
         pure (DebugInfo n)
  <|> do symbol ":"; exactIdent "q"
         pure Quit
  <|> do tm <- expr (Virtual Interactive) init
         pure (Eval tm)


text:
module TyTTP.Adapter.Node.URI

import Control.Monad.Maybe
import Node.URI
import TyTTP

export
decodeUri : Alternative m
  => (
    Context me String h1 s h2 a b
    -> m $ Context me' String h1' s' h2' a' b'
  )
  -> Context me String h1 s h2 a b
  -> m $ Context me' String h1' s' h2' a' b'
decodeUri handler ctx = case Node.URI.decodeURI ctx.request.url of
  Right str => handler $ { request.url := str } ctx
  Left _ => empty

export
decodeUri' : Monad m
  => (
    Context me String h1 s h2 a b
    -> m $ Context me' String h1' s' h2' a' b'
  )
  -> (
    Context me String h1 s h2 a b
    -> MaybeT m $ Context me' String h1' s' h2' a' b'
  )
  -> Context me String h1 s h2 a b
  -> m $ Context me' String h1' s' h2' a' b'
decodeUri' defHandler handler ctx = do
  Just result <- runMaybeT $ decodeUri handler ctx
    | Nothing => defHandler ctx
  pure result

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Replica

import Data.So
import Data.String
import Data.List.AtIndex
import Data.List
import Data.List1
import Data.OpenUnion

import System

import Replica.App
import Replica.Core
import Replica.Command
import Replica.Option.Types
import Replica.Other.Decorated
import Replica.Other.Validation

%default total

covering
runRun : RunCommand -> IO Int
runRun ctx = run $ new ctx.global $ new ctx $ handle runReplica
    (\stats => pure (cast $ stats.failures + stats.errors))
    (\err : ReplicaError => putStrLn (show err) >> pure 253)

covering
runInfo : InfoCommand -> IO Int
runInfo info = run $ new info.global $ new info $ handle infoReplica
    (const $ pure 0)
    (\err : ReplicaError => putStrLn (show err) >> pure 253)

runHelp : Help -> IO ()
runHelp = putStrLn . display

covering
runCommand : Commands -> IO Int
runCommand a0 = let
  Left a1 = decomp a0
    | Right cmd => runRun cmd
  Left a2 = decomp a1
    | Right cmd => runInfo cmd
  in runHelp (decomp0 a2) $> 0

covering
main : IO ()
main = do
  (cmd::args) <- getArgs
    | _ => putStrLn "Error"
  let Just args' = toList1' args
    | Nothing => runHelp help
  let x = parseArgs args'
  case x of
       InvalidMix e => do
         putStrLn e
         runHelp help
         exitWith $ ExitFailure 254
       InvalidOption ys => do
         putStrLn "Invalid command : \{ys.head}"
         runHelp help
         exitWith $ ExitFailure 254
       Done cmd => do
         exitCode <- runCommand cmd
         exitWith $ case choose (exitCode == 0) of
           Right x => ExitFailure exitCode
           Left  x => ExitSuccess

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
import Data.Either
import Data.List
import Data.Maybe
import Data.String

import System.File

increases : List Int -> Int
increases [] = 0
increases (x :: []) = 0
increases (x :: (y :: xs)) = (if x < y then 1 else 0) + increases (y ::xs)

parseLines : (String -> Maybe a) -> String -> List a
parseLines f s = catMaybes $ f <$> lines s

run : String -> IO ()
run s = do let l = parseLines parseInteger {a=Int} s
           putStrLn $ show $ increases l

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s


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

import Lightyear
import Lightyear.Char
import Lightyear.Strings

import Freyja.Convert

word : Parser String
word = lexeme (map pack $ some (alphaNum) ) <?> "Identity"

-- ---------------------------------------------------------------- [ Commands ]

public export
data DisplayPattern = All
                    | Summary
                    | MData
                    | Context
                    | Problem
                    | Solution
                    | Evidence
                    | Studies
                    | Related

public export
data EvalPattern : Type where
  EvalAll     : EvalPattern
  Readability : EvalPattern
  TemplateAd  : EvalPattern
--  SolutionApp : EvalPattern
  SifModel    : EvalPattern

public export
data FriggCMD : Type where
  Query   : String -> FriggCMD
  Display : DisplayPattern  -> FriggCMD
  Convert : FreyjaOutFormat -> FriggCMD
  Eval    : EvalPattern     -> FriggCMD
  Quit : FriggCMD
  Help : FriggCMD

export
showHelp : String
showHelp = """
Command                 | Description
------------------------|-------------------------------------------------------
:display <what>         | Display part of the pattern. One Of:
                        | [ all, info, metadata, context, problem,
                        |   solution, evidence, studies, related]
                        |
:evaluate <what>        | Perform an evaluation. One of:
                        | [sif, read, template]
                        |
:convert <to>           | Convert to a valid out format: One of:
                        | [latex, org, markdown, xml ]
                        |
:query <string>         | Query XML Doc using XPath
                        |
:quit :q :exit          | Quit the repl
:? :help                | Show this help
"""

display : Parser FriggCMD
display = do
      string ":display"
      space
      o <- displayOpts
      pure $ Display o
    <?> "Display"
  where
    displayOpts : Parser (DisplayPattern)
    displayOpts = (string "all"      *> return All)
              <|> (string "info"     *> return Summary)
              <|> (string "metadata" *> return MData)
              <|> (string "context"  *> return Context)
              <|> (string "problem"  *> return Problem)
              <|> (string "solution" *> return Solution)
              <|> (string "evidence" *> return Evidence)
              <|> (string "studies"  *> return Studies)
              <|> (string "related"  *> return Related)

convert : Parser FriggCMD
convert = do
    string ":convert"
    space
    fmt <- format
    pure $ Convert fmt
  where
    format : Parser (FreyjaOutFormat)
    format = do
      w <- word
      case (readOutFMT w) of
        Just fmt => pure fmt
        Nothing  => fail "Expected out format"

evaluate : Parser FriggCMD
evaluate = do
    string ":evaluate"
    space
    evl <- aspect
    pure $ Eval evl
  where
    aspect : Parser EvalPattern
    aspect = (string "sif"      *> return SifModel)
         <|> (string "read"     *> return Readability)
         <|> (string "template" *> return TemplateAd)
         <|> (string "all"      *> return EvalAll)

query : Parser FriggCMD
query = do
    string ":query"
    space
    qStr <- quoted '"'
    pure $ Query qStr

quit : Parser FriggCMD
quit = (string ":quit" *> return Quit)
   <|> (string ":q"    *> return Quit)
   <|> (string ":exit" *> return Quit)

help : Parser FriggCMD
help = (string ":?"    *> return Help)
   <|> (string ":help" *> return Help)

cmd : Parser FriggCMD
cmd = convert
  <|> evaluate
  <|> display
  <|> query
  <|> quit
  <|> help
  <?> "Command"

export
parseCMD : String -> Either String FriggCMD
parseCMD s = parse cmd s

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

max_stars_repo_name: jfdm/frigg-tool

max_issues_repo_name: jfdm/frigg-tool

max_forks_repo_name: jfdm/frigg-tool


text:
module Streaming

import public Data.Functor.Of
import public Streaming.Core


text:
module AutoF

import Data.So
import Data.Vect
import Data.Vect.Quantifiers

%default total

notEq : Eq a -> (x : a) -> (y : a) -> Type
notEq eq x y = So (x /= y)

mutual
  ||| Uqtor (uniquetor), a vector with unique values (according to `Eq`)
  data Uqt : (n : Nat) -> (a : Type) -> {auto eq : Eq a} -> Type where
    Nil  : Eq a => Uqt Z a
    (::) : (x : a) -> (xs : Uqt n a {eq}) -> {auto unq : All (notEq eq x) (unUqt xs)} -> Uqt (S n) a

  unUqt : Uqt n a {eq} -> Vect n a
  unUqt Nil     = Nil
  unUqt (x::xs) = x::(unUqt xs)

summon : {auto u : a} -> a
summon {u} = u

data X = A | B | C

Eq X where
  A == A = True
  B == B = True
  C == C = True
  _ == _ = False

-- just testing Uqt
uS : Uqt 3 String
uS = ["a", "b", "c"]

-- just testing Uqt
uX : Uqt 3 X
uX = [A, B, C]

%hint
a : X
a = A

%hint
b : X
b = B

%hint
c : X
c = C

y0 : Uqt 0 X
y0 = summon

yF : Uqt 1 X
yF = summon

yG : Uqt 2 X
yG = ?yG_rhs

yHint : Uqt 3 X
yHint = ?yHint_rhs

yLoc : Uqt 3 X
yLoc =
  let a = A in
  let b = B in
  let c = C in
  ?yLoc_rhs


text:
module Cursor

import Data.Fin
import MaybeFin

import Movement

%default total
%access public

private
crimp : Fin (S (S n)) -> Fin (S n)
crimp x =
  case (strengthen x) of
       Left _ => last
       Right x' => x'

private
boundedSubtract : Fin (S k) -> Nat -> Fin (S k)
boundedSubtract FZ _ = FZ
boundedSubtract (FS x) Z = (FS x)
boundedSubtract (FS x) (S k) = boundedSubtract (weaken x) k

private
boundedAdd : Fin (S k) -> Nat -> Fin (S k)
boundedAdd x Z = x
boundedAdd x (S k) =
  case strengthen x of
       Left _ => x
       Right x' => boundedAdd (FS x') k

record Cursor (bottomRow : Nat) where
  constructor Cursor'
  rowIndex : Fin (S bottomRow)
  colIndex : Nat

%name Cursor cursor

zeroCursor : Cursor n
zeroCursor = Cursor' FZ Z

private
updateColIndex : (Nat -> Nat) -> Cursor n -> Cursor n
updateColIndex update cursor = record { colIndex = update $ colIndex cursor } cursor

private
updateRowIndex : (Fin (S n) -> Fin (S m)) -> Cursor n -> Cursor m
updateRowIndex update (Cursor' rowIndex colIndex) = Cursor' (update rowIndex) colIndex

private
natToNullableFin : Nat -> MaybeFin n
natToNullableFin {n = Z} _ = NoFin
natToNullableFin {n = (S _)} k = SomeFin $ fromMaybe last $ natToFin k _

columnCursor : Cursor _ -> MaybeFin n
columnCursor (Cursor' _ colIndex) = natToNullableFin colIndex

private
moveByCharInLine : Move ByCharacter -> Nat -> Nat -> Nat
moveByCharInLine movement Z colIndex = colIndex
moveByCharInLine (Backward move) (S k) colIndex = minus colIndex move
moveByCharInLine (Forward move) (S k) colIndex =
  case natToFin colIndex (S k) of
       Nothing => colIndex
       Just fin => finToNat $ boundedAdd fin move

moving_within_empty_line_is_idempotent : moveByCharInLine move Z colIndex = colIndex
moving_within_empty_line_is_idempotent = Refl

-- TODO further proofs here once I understand how

moveByChar : Move ByCharacter -> Nat -> Cursor n -> Cursor n
moveByChar movement lineLength =
  updateColIndex $ moveByCharInLine movement lineLength

private
moveRowCursorByLine : Move ByLine -> Fin (S n) -> Fin (S n)
moveRowCursorByLine (Backward k) rowCursor =
  boundedSubtract rowCursor k
moveRowCursorByLine (Forward k) rowCursor =
  boundedAdd rowCursor k

moveByLine : Move ByLine -> Cursor v -> Cursor v
moveByLine movement =
  updateRowIndex $ moveRowCursorByLine movement

deleteLine : Cursor (S n) -> Cursor n
deleteLine = updateRowIndex crimp

insertLineAbove : Cursor n -> Cursor (S n)
insertLineAbove = updateRowIndex weaken

-- TODO should actually truncate to end of line here
insertAfter : Nat -> Cursor n -> Cursor n
insertAfter n = updateColIndex (+ n)

-- TODO should actually behave differently than insertAfter
insertBefore : Nat -> Cursor n -> Cursor n
insertBefore k = updateColIndex (+ n)


text:
module Main

import Json
import JsonDSL
import AST
import Server
import TCPServer

import Effects
import Effect.System
import Effect.StdIO
import Effect.State
import Network.Socket
import IdrisNet.TCP.TCPServer
import IdrisNet.TCP.TCPCommon

effects' : List EFFECT
effects' = [STDIO, SYSTEM, STATE String]

processRequest : processReq effects'
processRequest "subtract" (Just j[x :f y :f []]) = return $ Right (JsonNumber $ x - y)
processRequest "subtract" _ = return $ Left InvalidParams
processRequest "getTime" Nothing = do
  t <- time
  return . Right . JsonString . show $ t
processRequest "getTime" _ = return $ Left InvalidParams
processRequest "put" (Just j{["data" .s str]}) = do
  put str
  return . Right . JsonString $ "ok"
processRequest "put" _ = return $ Left InvalidParams
processRequest "get" Nothing = do
  str <- get
  return . Right . JsonString $ str
processRequest "get" _ = return $ Left InvalidParams
processRequest _ _ = return $ Left MethodNotFound

receive : receiveFunc effects'
receive = do
  t <- time
  putStr (show t ++ ": Waiting for a message\n")
  -- Receive
  OperationSuccess (str, len) <- tcpRecv 1024
    | RecoverableError _ => receive
    | FatalError err => do putStr ("Error receiving: " ++ (show err))
                           tcpFinalise
    | ConnectionClosed => return ()
  -- Process
  (Just out) <- handleStr processRequest str
    | Nothing => receive
  -- Echo
  OperationSuccess _ <- tcpSend out
    | RecoverableError err => do putStr ("Error sending: " ++ (show err))
                                 tcpClose
    | FatalError err => do putStr ("Error sending: " ++ (show err))
                           tcpFinalise
    | ConnectionClosed => return ()
  receive

main : IO ()
main = run (setupServer 1234 receive [default, default, default])

-- nc localhost 1234
-- {"jsonrpc": "2.0", "method": "subtract", "params": [42, 23], "id": 1}
-- {"jsonrpc": "2.0", "method": "getTime", "id": 2}
-- [{"jsonrpc": "2.0", "method": "subtract", "params": [42, 23], "id": 1}, {"jsonrpc": "2.0", "method": "getTime", "params": [], "id": 2}]
-- [{"jsonrpc": "2.0", "method": "subtract", "params": [42, 23], "id": 1}, {"jsonrpc": "2.0", "method": "getTime", "params": []}]
-- [err{"jsonrpc": "2.0", "method": "subtract", "params": [42, 23], "id": 1}, {"jsonrpc": "2.0", "method": "getTime", "params": [], "id": 2}]
-- [{"jsonrpc": "2.0", "method": "err", "params": [42, 23], "id": 1}, {"jsonrpc": "2.0", "method": "getTime", "params": [], "id": 2}]
-- {"jsonrpc": "2.0", "method": "put", "params": {"data": "hello"}, "id": 1}
-- {"jsonrpc": "2.0", "method": "get", "id": 1}
-- [{"jsonrpc": "2.0", "method": "put", "params": {"data": "blah"}, "id": 1}, {"jsonrpc": "2.0", "method": "get", "id": 2}]

max_stars_repo_name: archaeron/idris-json-rpc

max_issues_repo_name: archaeron/idris-json-rpc

max_forks_repo_name: archaeron/idris-json-rpc


text:
module RecordProjection

record Name where
  constructor MkName
  firstName : String
  lastName : String

(.fullName) : Name -> String
name.fullName = name.firstName ++ " " ++ name.lastName

johnSmith : Name
johnSmith = MkName
  { firstName = "John"
  , lastName = "Smith"
  }

main : IO ()
main = assert_total $ do
  putStrLn johnSmith.firstName
  putStrLn johnSmith.lastName
  putStrLn johnSmith.fullName


text:
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

%name Vect xs, ys, zs

dupAll : Vect n a -> Vect n (a, a)
dupAll xs = zipHere xs xs
  where
    zipHere : forall n . Vect n a -> Vect n b -> Vect n (a, b)


text:
module Core.Normalise.Quote

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Normalise.Eval
import Core.Options
import Core.Primitives
import Core.TT
import Core.Value

import Libraries.Data.IntMap
import Data.List
import Data.Maybe
import Data.Nat
import Data.Vect

%default covering

export
data QVar : Type where

public export
record QuoteOpts where
  constructor MkQuoteOpts
  topLevel : Bool -- At the top level application
  patterns : Bool -- only quote as far as is useful to get LHS patterns.
                  -- That means, stop on encountering a block function or
                  -- local
  sizeLimit : Maybe Nat

public export
interface Quote tm where
    quote : {auto c : Ref Ctxt Defs} ->
            {vars : List Name} ->
            Defs -> Env Term vars -> tm vars -> Core (Term vars)
    quoteLHS : {auto c : Ref Ctxt Defs} ->
               {vars : List Name} ->
               Defs -> Env Term vars -> tm vars -> Core (Term vars)
    quoteOpts : {auto c : Ref Ctxt Defs} ->
                {vars : List Name} ->
                QuoteOpts -> Defs -> Env Term vars -> tm vars -> Core (Term vars)

    quoteGen : {auto c : Ref Ctxt Defs} ->
               {vars : _} ->
               Ref QVar Int -> QuoteOpts ->
               Defs -> Env Term vars -> tm vars -> Core (Term vars)

    quote defs env tm
        = do q <- newRef QVar 0
             quoteGen q (MkQuoteOpts True False Nothing) defs env tm

    quoteLHS defs env tm
        = do q <- newRef QVar 0
             quoteGen q (MkQuoteOpts True True Nothing) defs env tm

    quoteOpts opts defs env tm
        = do q <- newRef QVar 0
             quoteGen q opts defs env tm

export
genName : {auto q : Ref QVar Int} -> String -> Core Name
genName n
    = do i <- get QVar
         put QVar (i + 1)
         pure (MN n i)

mutual
  quoteArg : {auto c : Ref Ctxt Defs} ->
              {bound, free : _} ->
              Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->
              Env Term free -> Closure free ->
              Core (Term (bound ++ free))
  quoteArg q opts defs bounds env a
      = quoteGenNF q opts defs bounds env !(evalClosure defs a)

  quoteArgWithFC : {auto c : Ref Ctxt Defs} ->
                   {bound, free : _} ->
                   Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->
                   Env Term free -> (FC, Closure free) ->
                   Core ((FC, Term (bound ++ free)))
  quoteArgWithFC q opts defs bounds env
       = traversePair (quoteArg q opts defs bounds env)

  quoteArgs : {auto c : Ref Ctxt Defs} ->
              {bound, free : _} ->
              Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->
              Env Term free -> List (Closure free) ->
              Core (List (Term (bound ++ free)))
  quoteArgs q opts defs bounds env = traverse (quoteArg q opts defs bounds env)

  quoteArgsWithFC : {auto c : Ref Ctxt Defs} ->
                    {bound, free : _} ->
                    Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->
                    Env Term free -> List (FC, Closure free) ->
                    Core (List (FC, Term (bound ++ free)))
  quoteArgsWithFC q opts defs bounds env
      = traverse (quoteArgWithFC q opts defs bounds env)

  quoteHead : {auto c : Ref Ctxt Defs} ->
              {bound, free : _} ->
              Ref QVar Int -> QuoteOpts -> Defs ->
              FC -> Bounds bound -> Env Term free -> NHead free ->
              Core (Term (bound ++ free))
  quoteHead {bound} q opts defs fc bounds env (NLocal mrig _ prf)
      = let MkVar prf' = addLater bound prf in
            pure $ Local fc mrig _ prf'
    where
      addLater : {idx : _} ->
                 (ys : List Name) -> (0 p : IsVar n idx xs) ->
                 Var (ys ++ xs)
      addLater [] isv = MkVar isv
      addLater (x :: xs) isv
          = let MkVar isv' = addLater xs isv in
                MkVar (Later isv')
  quoteHead q opts defs fc bounds env (NRef Bound (MN n i))
      = pure $ case findName bounds of
             Just (MkVar p) => Local fc Nothing _ (varExtend p)
             Nothing => Ref fc Bound (MN n i)
    where
      findName : Bounds bound' -> Maybe (Var bound')
      findName None = Nothing
      findName (Add x (MN n' i') ns)
          = if i == i' -- this uniquely identifies it, given how we
                       -- generated the names, and is a faster test!
               then Just (MkVar First)
               else do MkVar p <-findName ns
                       Just (MkVar (Later p))
      findName (Add x _ ns)
          = do MkVar p <-findName ns
               Just (MkVar (Later p))
  quoteHead q opts defs fc bounds env (NRef nt n) = pure $ Ref fc nt n
  quoteHead q opts defs fc bounds env (NMeta n i args)
      = do args' <- quoteArgs q opts defs bounds env args
           pure $ Meta fc n i args'

  quotePi : {auto c : Ref Ctxt Defs} ->
            {bound, free : _} ->
            Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->
            Env Term free -> PiInfo (Closure free) ->
            Core (PiInfo (Term (bound ++ free)))
  quotePi q opts defs bounds env Explicit = pure Explicit
  quotePi q opts defs bounds env Implicit = pure Implicit
  quotePi q opts defs bounds env AutoImplicit = pure AutoImplicit
  quotePi q opts defs bounds env (DefImplicit t)
      = do t' <- quoteGenNF q opts defs bounds env !(evalClosure defs t)
           pure (DefImplicit t')

  quoteBinder : {auto c : Ref Ctxt Defs} ->
                {bound, free : _} ->
                Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->
                Env Term free -> Binder (Closure free) ->
                Core (Binder (Term (bound ++ free)))
  quoteBinder q opts defs bounds env (Lam fc r p ty)
      = do ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)
           p' <- quotePi q opts defs bounds env p
           pure (Lam fc r p' ty')
  quoteBinder q opts defs bounds env (Let fc r val ty)
      = do val' <- quoteGenNF q opts defs bounds env !(evalClosure defs val)
           ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)
           pure (Let fc r val' ty')
  quoteBinder q opts defs bounds env (Pi fc r p ty)
      = do ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)
           p' <- quotePi q opts defs bounds env p
           pure (Pi fc r p' ty')
  quoteBinder q opts defs bounds env (PVar fc r p ty)
      = do ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)
           p' <- quotePi q opts defs bounds env p
           pure (PVar fc r p' ty')
  quoteBinder q opts defs bounds env (PLet fc r val ty)
      = do val' <- quoteGenNF q opts defs bounds env !(evalClosure defs val)
           ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)
           pure (PLet fc r val' ty')
  quoteBinder q opts defs bounds env (PVTy fc r ty)
      = do ty' <- quoteGenNF q opts defs bounds env !(evalClosure defs ty)
           pure (PVTy fc r ty')

  quoteGenNF : {auto c : Ref Ctxt Defs} ->
               {bound, vars : _} ->
               Ref QVar Int -> QuoteOpts ->
               Defs -> Bounds bound ->
               Env Term vars -> NF vars -> Core (Term (bound ++ vars))
  quoteGenNF q opts defs bound env (NBind fc n b sc)
      = do var <- genName "qv"
           sc' <- quoteGenNF q opts defs (Add n var bound) env
                       !(sc defs (toClosure defaultOpts env (Ref fc Bound var)))
           b' <- quoteBinder q opts defs bound env b
           pure (Bind fc n b' sc')
  quoteGenNF q opts defs bound env (NApp fc f args)
      = do f' <- quoteHead q opts defs fc bound env f
           opts' <- case sizeLimit opts of
                         Nothing => pure opts
                         Just Z => throw (InternalError "Size limit exceeded")
                         Just (S k) => pure (record { sizeLimit = Just k } opts)
           args' <- if patterns opts && not (topLevel opts) && isRef f
                       then do empty <- clearDefs defs
                               quoteArgsWithFC q opts' empty bound env args
                               else quoteArgsWithFC q (record { topLevel = False } opts')
                                                    defs bound env args
           pure $ applyWithFC f' args'
    where
      isRef : NHead vars -> Bool
      isRef (NRef{}) = True
      isRef _ = False
  quoteGenNF q opts defs bound env (NDCon fc n t ar args)
      = do args' <- quoteArgsWithFC q opts defs bound env args
           pure $ applyWithFC (Ref fc (DataCon t ar) n) args'
  quoteGenNF q opts defs bound env (NTCon fc n t ar args)
      = do args' <- quoteArgsWithFC q opts defs bound env args
           pure $ applyWithFC (Ref fc (TyCon t ar) n) args'
  quoteGenNF q opts defs bound env (NAs fc s n pat)
      = do n' <- quoteGenNF q opts defs bound env n
           pat' <- quoteGenNF q opts defs bound env pat
           pure (As fc s n' pat')
  quoteGenNF q opts defs bound env (NDelayed fc r arg)
      = do argQ <- quoteGenNF q opts defs bound env arg
           pure (TDelayed fc r argQ)
  quoteGenNF q opts defs bound env (NDelay fc r ty arg)
      = do argNF <- evalClosure defs (toHolesOnly arg)
           argQ <- quoteGenNF q opts defs bound env argNF
           tyNF <- evalClosure defs (toHolesOnly ty)
           tyQ <- quoteGenNF q opts defs bound env tyNF
           pure (TDelay fc r tyQ argQ)
    where
      toHolesOnly : Closure vs -> Closure vs
      toHolesOnly (MkClosure opts locs env tm)
          = MkClosure (record { holesOnly = True,
                                argHolesOnly = True } opts)
                      locs env tm
      toHolesOnly c = c
  quoteGenNF q opts defs bound env (NForce fc r arg args)
      = do args' <- quoteArgsWithFC q opts defs bound env args
           case arg of
                NDelay fc _ _ arg =>
                   do argNF <- evalClosure defs arg
                      pure $ applyWithFC !(quoteGenNF q opts defs bound env argNF) args'
                _ => do arg' <- quoteGenNF q opts defs bound env arg
                        pure $ applyWithFC (TForce fc r arg') args'
  quoteGenNF q opts defs bound env (NPrimVal fc c) = pure $ PrimVal fc c
  quoteGenNF q opts defs bound env (NErased fc i) = pure $ Erased fc i
  quoteGenNF q opts defs bound env (NType fc) = pure $ TType fc

export
Quote NF where
  quoteGen q opts defs env tm = quoteGenNF q opts defs None env tm

export
Quote Term where
  quoteGen q opts defs env tm = pure tm

export
Quote Closure where
  quoteGen q opts defs env c = quoteGen q opts defs env !(evalClosure defs c)

quoteWithPiGen : {auto _ : Ref Ctxt Defs} ->
                 {bound, vars : _} ->
                 Ref QVar Int -> QuoteOpts -> Defs -> Bounds bound ->
                 Env Term vars -> NF vars -> Core (Term (bound ++ vars))
quoteWithPiGen q opts defs bound env (NBind fc n (Pi bfc c p ty) sc)
    = do var <- genName "qv"
         empty <- clearDefs defs
         sc' <- quoteWithPiGen q opts defs (Add n var bound) env
                     !(sc defs (toClosure defaultOpts env (Ref fc Bound var)))
         ty' <- quoteGenNF q opts empty bound env !(evalClosure empty ty)
         p' <- quotePi q opts empty bound env p
         pure (Bind fc n (Pi bfc c p' ty') sc')
quoteWithPiGen q opts defs bound env tm
    = do empty <- clearDefs defs
         quoteGenNF q opts empty bound env tm

-- Quote back to a term, but only to find out how many Pi bindings there
-- are, don't reduce anything else
export
quoteWithPi : {auto c : Ref Ctxt Defs} ->
              {vars : List Name} ->
              Defs -> Env Term vars -> NF vars -> Core (Term vars)
quoteWithPi defs env tm
    = do q <- newRef QVar 0
         quoteWithPiGen q (MkQuoteOpts True False Nothing) defs None env tm


text:
module Libraries.Utils.Binary

import Data.Buffer
import Data.List

import System.File

import Libraries.Utils.String

-- Serialising data as binary. Provides an interface TTC which allows
-- reading and writing to chunks of memory, "Binary", which can be written
-- to and read from files.

%default covering

public export
record Binary where
  constructor MkBin
  buf : Buffer
  loc : Int
  size : Int -- Capacity
  used : Int -- Amount used

export
newBinary : Buffer -> Int -> Binary
newBinary b s = MkBin b 0 s 0

export
blockSize : Int
blockSize = 655360

export
avail : Binary -> Int
avail c = (size c - loc c) - 1

export
toRead : Binary -> Int
toRead c = used c - loc c

export
appended : Int -> Binary -> Binary
appended i (MkBin b loc s used) = MkBin b (loc+i) s (used + i)

export
incLoc : Int -> Binary -> Binary
incLoc i c = record { loc $= (+i) } c

export
dumpBin : Binary -> IO ()
dumpBin chunk
   = do -- printLn !(traverse bufferData (map buf done))
        printLn !(bufferData (buf chunk))
        -- printLn !(traverse bufferData (map buf rest))

export
nonEmptyRev : {xs : _} ->
              NonEmpty (xs ++ y :: ys)
nonEmptyRev {xs = []} = IsNonEmpty
nonEmptyRev {xs = (x :: xs)} = IsNonEmpty

export
fromBuffer : Buffer -> IO Binary
fromBuffer buf
    = do len <- rawSize buf
         pure (MkBin buf 0 len len)

export
writeToFile : (fname : String) -> Binary -> IO (Either FileError ())
writeToFile fname c
    = writeBufferToFile fname (buf c) (used c)

export
readFromFile : (fname : String) -> IO (Either FileError Binary)
readFromFile fname
    = do Right b <- createBufferFromFile fname
               | Left err => pure (Left err)
         bsize <- rawSize b
         pure (Right (MkBin b 0 bsize bsize))