text:
module IdrisWeb.DB.SQLite.SQLiteNew
import Effects
import IdrisWeb.DB.SQLite.SQLiteCodes

%link C "sqlite3api.o"
%include C "sqlite3api.h"
%lib C "sqlite3"
%access public

data ConnectionPtr = ConnPtr Ptr
data StmtPtr = PSPtr Ptr

data DBVal = DBInt Int
           | DBText String
           | DBFloat Float
           | DBNull

-- Type synonym for a table
ResultSet : Type
ResultSet = List (List DBVal)

DBName : Type
DBName = String

QueryString : Type
QueryString = String

Column : Type
Column = Int

ArgPos : Type
ArgPos = Int
data BindError = BE ArgPos SQLiteCode

{- Connection-stage resources -}
data SQLiteConnected : Type where
  SQLConnection : ConnectionPtr -> SQLiteConnected

{- PreparedStatement resources -}
data BindStep = Binding | Bound

data SQLitePSSuccess : BindStep -> Type where
  -- We record potential bind failures within the resource,
  -- and branch on the finishBind step. This prevents us from
  -- having to branch on every bind, which would be impractical.
  SQLitePS : ConnectionPtr -> StmtPtr -> SQLitePSSuccess a
  SQLiteBindFail : ConnectionPtr -> StmtPtr -> BindError -> SQLitePSSuccess a

data SQLitePSFail : Type where
  PSFail : ConnectionPtr -> SQLitePSFail

data SQLiteFinishBindFail : Type where
  SQLiteFBFail : ConnectionPtr -> StmtPtr -> SQLiteFinishBindFail

{- Executing Resources -}
-- Tag used to indicate whether another row may be fetched
data ExecutionResult = ValidRow
                     | InvalidRow

data SQLiteExecuting : ExecutionResult -> Type where
  SQLiteE : ConnectionPtr -> StmtPtr -> SQLiteExecuting a

data QueryError = ConnectionError SQLiteCode
                | BindingError BindError
                | StatementError SQLiteCode
                | ExecError String
                | InternalError

instance Show QueryError where
  show (ConnectionError code) = "Error connecting to database, code: " ++ (show code)
  show (BindingError (BE ap code)) = "Error binding variable, pos: " ++ (show ap) ++ ", code: " ++ (show code)
  show (StatementError code) = "Error creating prepared statement, code: " ++ (show code)
  show (ExecError err) = err
  show (InternalError) = "Internal Error."
data Sqlite : Effect where
  -- Opens a connection to the database
  OpenDB : DBName -> Sqlite () (Either () SQLiteConnected) (Either QueryError ())
  -- Closes the database handle
  CloseDB : Sqlite (SQLiteConnected) () ()
  -- Prepares a statement, given a basic query string
  PrepareStatement : QueryString -> Sqlite (SQLiteConnected) (Either (SQLitePSFail) (SQLitePSSuccess Binding))
                                              (Either QueryError ())
  -- Binds arguments to the given argument position
  BindInt : ArgPos -> Int -> Sqlite (SQLitePSSuccess Binding) (SQLitePSSuccess Binding) ()
  BindFloat : ArgPos -> Float -> Sqlite (SQLitePSSuccess Binding) (SQLitePSSuccess Binding) ()
  BindText : ArgPos -> String -> Int -> Sqlite (SQLitePSSuccess Binding) (SQLitePSSuccess Binding) ()
  BindNull : ArgPos -> Sqlite (SQLitePSSuccess Binding) (SQLitePSSuccess Binding) ()

  -- Checks to see whether all the binds were successful, if not then fails with the bind error
  FinishBind : Sqlite (SQLitePSSuccess Binding) (Either SQLiteFinishBindFail (SQLitePSSuccess Bound))
                                                (Maybe QueryError)

  -- Executes the statement, and fetches the first row
  ExecuteStatement : Sqlite (SQLitePSSuccess Bound) (Either (SQLiteExecuting InvalidRow)
                                                                (SQLiteExecuting ValidRow)) StepResult

  RowStep : Sqlite (SQLiteExecuting ValidRow) (Either (SQLiteExecuting InvalidRow)
                                                      (SQLiteExecuting ValidRow)) StepResult

  -- We need two separate effects, but this is entirely non-user-facing due to
  -- if_valid in the wrapper function
  ResetFromEnd : Sqlite (SQLiteExecuting InvalidRow)
                        (Either (SQLiteExecuting InvalidRow)
                        (SQLiteExecuting ValidRow)) StepResult

  Reset : Sqlite (SQLiteExecuting ValidRow) (Either (SQLiteExecuting InvalidRow)
                                                    (SQLiteExecuting ValidRow)) StepResult

  -- Column access functions
  GetColumnName : Column -> Sqlite (SQLiteExecuting ValidRow) (SQLiteExecuting ValidRow) String
  GetColumnDataSize : Column -> Sqlite (SQLiteExecuting ValidRow) (SQLiteExecuting ValidRow) Int
  GetColumnText : Column -> Sqlite (SQLiteExecuting ValidRow) (SQLiteExecuting ValidRow) String
  GetColumnInt : Column -> Sqlite (SQLiteExecuting ValidRow) (SQLiteExecuting ValidRow) Int

  -- Finalisation Functions
  FinaliseValid : Sqlite (SQLiteExecuting ValidRow) (SQLiteConnected) ()
  FinaliseInvalid : Sqlite (SQLiteExecuting InvalidRow) (SQLiteConnected) ()

  -- Cleanup functions to handle error states
  CleanupPSFail : Sqlite (SQLitePSFail) () ()
  CleanupBindFail : Sqlite (SQLiteFinishBindFail) () ()

private
foreignGetError : ConnectionPtr -> IO Int
foreignGetError (ConnPtr ptr) = mkForeign (FFun "idr_errcode" [FPtr] FInt) ptr

private
foreignNextRow : ConnectionPtr -> IO StepResult
foreignNextRow (ConnPtr ptr) =
  map stepResult (mkForeign (FFun "sqlite3_step_idr" [FPtr] FInt) ptr)

private
foreignFinalise : ConnectionPtr -> IO ()
foreignFinalise (ConnPtr c) = do mkForeign (FFun "sqlite3_finalize_idr" [FPtr] FInt) c
                                 return ()

private
foreignClose : ConnectionPtr -> IO ()
foreignClose (ConnPtr c) = do mkForeign (FFun "sqlite3_close_idr" [FPtr] FInt) c
                              return ()
-- That's the painful bit done, since exception branching will allow us to not have to do
-- the ugliness of pass-through handlers
instance Handler Sqlite IO where
  handle () (OpenDB file) k = do
    ff <- mkForeign (FFun "sqlite3_open_idr" [FString] FPtr) file
    is_null <- nullPtr ff
    if (not is_null) then k (Right (SQLConnection (ConnPtr ff))) (Right ())
                     else k (Left ()) (Left (ConnectionError sqlite_ERROR))

  handle (SQLConnection (ConnPtr conn) ) CloseDB k = do
    mkForeign (FFun "sqlite3_close_idr" [FPtr] FInt) conn
    k () ()

  handle (SQLConnection (ConnPtr conn)) (PrepareStatement str) k = do
    res <- mkForeign (FFun "sqlite3_prepare_idr" [FPtr, FString] FPtr) conn str
    is_null <- nullPtr res
    if (not is_null) then k (Right (SQLitePS (ConnPtr conn) (PSPtr res))) (Right ())
                     else do err <- foreignGetError (ConnPtr conn)
                             k (Left (PSFail (ConnPtr conn))) (Left (StatementError err))

  handle (SQLitePS (ConnPtr conn) (PSPtr res)) (BindInt pos i) k = do
    res <- mkForeign (FFun "sqlite3_bind_int_idr" [FPtr, FInt, FInt] FPtr) conn pos i
    is_null <- nullPtr res
    if (not is_null) then k (SQLitePS (ConnPtr conn) (PSPtr res)) ()
                     else do err <- foreignGetError (ConnPtr conn)
             --                putStrLn $ "BindInt error: " ++ (show err)
                             k (SQLiteBindFail (ConnPtr conn) (PSPtr res) (BE pos err)) ()

  handle (SQLitePS (ConnPtr conn) (PSPtr res)) (BindFloat pos f) k = do
    res <- mkForeign (FFun "sqlite3_bind_float_idr" [FPtr, FInt, FFloat] FPtr) conn pos f
    is_null <- nullPtr res
    if (not is_null) then k (SQLitePS (ConnPtr conn) (PSPtr res)) ()
                     else do err <- foreignGetError (ConnPtr conn)
                             k (SQLiteBindFail (ConnPtr conn) (PSPtr res) (BE pos err)) ()

  handle (SQLitePS (ConnPtr conn) (PSPtr res)) (BindText pos str str_len) k = do
    res <- mkForeign (FFun "sqlite3_bind_text_idr" [FPtr, FString, FInt, FInt] FPtr) conn str pos str_len
    is_null <- nullPtr res
    if (not is_null) then k (SQLitePS (ConnPtr conn) (PSPtr res)) ()
                     else do err <- foreignGetError (ConnPtr conn)
               --              putStrLn $ "BindStr error: " ++ (show err)
                             k (SQLiteBindFail (ConnPtr conn) (PSPtr res) (BE pos err)) ()

  handle (SQLitePS (ConnPtr conn) (PSPtr res)) (BindNull pos) k = do
    res <- mkForeign (FFun "sqlite3_bind_null_idr" [FPtr, FInt] FPtr) conn pos
    is_null <- nullPtr res
    if (not is_null) then k (SQLitePS (ConnPtr conn) (PSPtr res)) ()
                     else do err <- foreignGetError (ConnPtr conn)
                             k (SQLiteBindFail (ConnPtr conn) (PSPtr res) (BE pos err)) ()

  -- Ok, I lied, we have to do *some* pass-throughs. But they're not terrible.
  handle (SQLiteBindFail conn ps be) (BindInt _ _) k = k (SQLiteBindFail conn ps be) ()
  handle (SQLiteBindFail conn ps be) (BindText _ _ _) k = k (SQLiteBindFail conn ps be) ()
  handle (SQLiteBindFail conn ps be) (BindFloat _ _) k = k (SQLiteBindFail conn ps be) ()
  handle (SQLiteBindFail conn ps be) (BindNull _) k = k (SQLiteBindFail conn ps be) ()

  -- Finishing binding, reporting any bind errors if they occurred
  handle (SQLitePS c p) (FinishBind) k =
    k (Right (SQLitePS c p)) Nothing

  handle (SQLiteBindFail c ps be) (FinishBind) k =
    k (Left (SQLiteFBFail c ps)) (Just (BindingError be))

  handle (SQLitePS (ConnPtr c) (PSPtr p)) (ExecuteStatement) k = do
    step <- foreignNextRow (ConnPtr c)
    case step of
      StepComplete => k (Right (SQLiteE (ConnPtr c) (PSPtr p))) step
      StepFail => k (Left (SQLiteE (ConnPtr c) (PSPtr p))) step
      NoMoreRows => k (Left (SQLiteE (ConnPtr c) (PSPtr p))) step

  handle (SQLiteE (ConnPtr c) (PSPtr p)) (RowStep) k = do
    step <- foreignNextRow (ConnPtr c)
    case step of
      StepComplete => k (Right (SQLiteE (ConnPtr c) (PSPtr p))) step
      StepFail => k (Left (SQLiteE (ConnPtr c) (PSPtr p))) step
      NoMoreRows => k (Left (SQLiteE (ConnPtr c) (PSPtr p))) step

  -- Getting values from the current row
  handle (SQLiteE (ConnPtr c) (PSPtr p)) (GetColumnName i) k = do
    res <- mkForeign (FFun "sqlite3_column_name_idr" [FPtr, FInt] FString) c i
    k (SQLiteE (ConnPtr c) (PSPtr p)) res

  handle (SQLiteE (ConnPtr c) (PSPtr p)) (GetColumnDataSize i) k = do
    res <- mkForeign (FFun "sqlite3_column_bytes_idr" [FPtr, FInt] FInt) c i
    k (SQLiteE (ConnPtr c) (PSPtr p)) res

  handle (SQLiteE (ConnPtr c) (PSPtr p)) (GetColumnInt i) k = do
    res <- mkForeign (FFun "sqlite3_column_int_idr" [FPtr, FInt] FInt) c i
    k (SQLiteE (ConnPtr c) (PSPtr p)) res

  handle (SQLiteE (ConnPtr c) (PSPtr p)) (GetColumnText i) k = do
    res <- mkForeign (FFun "sqlite3_column_text_idr" [FPtr, FInt] FString) c i
    k (SQLiteE (ConnPtr c) (PSPtr p)) res

  -- Resetting our position
  handle (SQLiteE (ConnPtr c) (PSPtr p)) (Reset) k = do
    mkForeign (FFun "sqlite3_reset_idr" [FPtr] FInt) c
    step <- foreignNextRow (ConnPtr c)
    case step of
      StepComplete => k (Right (SQLiteE (ConnPtr c) (PSPtr p))) step
      StepFail => k (Left (SQLiteE (ConnPtr c) (PSPtr p))) step
      NoMoreRows => k (Left (SQLiteE (ConnPtr c) (PSPtr p))) step

  handle (SQLiteE (ConnPtr c) (PSPtr p)) (ResetFromEnd) k = do
    mkForeign (FFun "sqlite3_reset_idr" [FPtr] FInt) c
    step <- foreignNextRow (ConnPtr c)
    case step of
      StepComplete => k (Right (SQLiteE (ConnPtr c) (PSPtr p))) step
      StepFail => k (Left (SQLiteE (ConnPtr c) (PSPtr p))) step
      NoMoreRows => k (Left (SQLiteE (ConnPtr c) (PSPtr p))) step

      -- Finalising the SQL Statement
  handle (SQLiteE c p) (FinaliseValid) k = do
    foreignFinalise c
    k (SQLConnection c) ()

  handle (SQLiteE c p) (FinaliseInvalid) k = do
    foreignFinalise c
    k (SQLConnection c) ()

  handle (PSFail c) CleanupPSFail k = do
    foreignClose c
    k () ()

  handle (SQLiteFBFail c p) CleanupBindFail k = do
    foreignFinalise c
    foreignClose c
    k () ()

SQLITE : Type -> EFFECT
SQLITE t = MkEff t Sqlite
{- User-facing functions -}
openDB : DBName -> EffM IO [SQLITE ()] [SQLITE (Either () SQLiteConnected)]
                                       (Either QueryError ())
openDB name = (OpenDB name)

closeDB : EffM IO [SQLITE (SQLiteConnected)] [SQLITE ()] ()
closeDB = CloseDB

prepareStatement : QueryString -> EffM IO [SQLITE SQLiteConnected]
                                          [SQLITE (Either SQLitePSFail
                                                  (SQLitePSSuccess Binding))]
                                          (Either QueryError ())
prepareStatement stmt = (PrepareStatement stmt)

bindInt : ArgPos -> Int -> Eff IO [SQLITE (SQLitePSSuccess Binding)] ()
bindInt pos i = (BindInt pos i)

bindFloat : ArgPos -> Float -> Eff IO [SQLITE (SQLitePSSuccess Binding)] ()
bindFloat pos f = (BindFloat pos f)

bindText : ArgPos -> String -> Eff IO [SQLITE (SQLitePSSuccess Binding)] ()
bindText pos str = (BindText pos str str_len)
  where natToInt : Nat -> Int
        natToInt Z = 0
        natToInt (S k) = 1 + (natToInt k)

        str_len : Int
        str_len = natToInt (length str)

bindNull : ArgPos -> Eff IO [SQLITE (SQLitePSSuccess Binding)] ()
bindNull pos = (BindNull pos)

finishBind : EffM IO [SQLITE (SQLitePSSuccess Binding)]
                     [SQLITE (Either SQLiteFinishBindFail (SQLitePSSuccess Bound))]
                     (Maybe QueryError)
finishBind = FinishBind

nextRow : EffM IO [SQLITE (SQLiteExecuting ValidRow)]
                  [SQLITE (Either (SQLiteExecuting InvalidRow)
                                  (SQLiteExecuting ValidRow))] StepResult
nextRow = RowStep

reset : EffM IO [SQLITE (Either (SQLiteExecuting InvalidRow) (SQLiteExecuting ValidRow))]
                [SQLITE (Either (SQLiteExecuting InvalidRow)
                                (SQLiteExecuting ValidRow))] StepResult
reset = if_left then ResetFromEnd else Reset

getColumnName : Column -> Eff IO [SQLITE (SQLiteExecuting ValidRow)] String
getColumnName col = (GetColumnName col)

getColumnText: Column -> Eff IO [SQLITE (SQLiteExecuting ValidRow)] String
getColumnText col = (GetColumnText col)

getColumnInt : Column -> Eff IO [SQLITE (SQLiteExecuting ValidRow)] Int
getColumnInt col = (GetColumnInt col)

getColumnDataSize : Column -> Eff IO [SQLITE (SQLiteExecuting ValidRow)] Int
getColumnDataSize col = (GetColumnDataSize col)

finaliseValid : EffM IO [SQLITE (SQLiteExecuting ValidRow)] [SQLITE (SQLiteConnected)] ()
finaliseValid = FinaliseValid

finaliseInvalid : EffM IO [SQLITE (SQLiteExecuting InvalidRow)] [SQLITE (SQLiteConnected)] ()
finaliseInvalid = FinaliseInvalid

--isOne : (a : Type) -> Either a b

finalise : EffM IO [SQLITE (Either (SQLiteExecuting InvalidRow) (SQLiteExecuting ValidRow))]
                   [SQLITE (SQLiteConnected)] ()
finalise = if_valid then finaliseValid else finaliseInvalid

cleanupPSFail : EffM IO [SQLITE (SQLitePSFail)] [SQLITE ()] ()
cleanupPSFail = CleanupPSFail

cleanupBindFail : EffM IO [SQLITE (SQLiteFinishBindFail)] [SQLITE ()] ()
cleanupBindFail = CleanupBindFail

-- Just makes it a tad nicer to write
executeStatement : EffM IO [SQLITE (SQLitePSSuccess Bound)]
                        [SQLITE (Either (SQLiteExecuting InvalidRow)
                                        (SQLiteExecuting ValidRow))] StepResult
executeStatement = ExecuteStatement

getQueryError : Either QueryError b -> QueryError
getQueryError (Left qe) = qe
getQueryError _ = InternalError

multiBind' : List (Int, DBVal) -> Eff IO [SQLITE (SQLitePSSuccess Binding)] ()
multiBind' [] = Effects.pure ()
multiBind' ((pos, (DBInt i)) :: xs) = do bindInt pos i
                                         multiBind' xs
multiBind' ((pos, (DBFloat f)) :: xs) = do bindFloat pos f
                                           multiBind' xs
multiBind' ((pos, (DBText t)) :: xs) = do bindText pos t
                                          multiBind' xs
-- Binds multiple values within a query
multiBind : List (Int, DBVal) ->
            EffM IO [SQLITE (SQLitePSSuccess Binding)]
                    [SQLITE (Either (SQLiteFinishBindFail) (SQLitePSSuccess Bound))]
            (Maybe QueryError)
multiBind vals = do
  multiBind' vals
  finishBind

getRowCount' : StepResult -> EffM IO [SQLITE (Either (SQLiteExecuting InvalidRow) (SQLiteExecuting ValidRow))]
                        [SQLITE ()]
                        (Either QueryError Int)
getRowCount' id_res = do
  if_valid then do
    last_insert_id <- getColumnInt 0
    finaliseValid
    closeDB
    return $ Right last_insert_id
  else do finaliseInvalid
          closeDB
          case id_res of
            NoMoreRows => return $ Left (ExecError "Unable to get row count")
            StepFail => return $ Left (ExecError "Error whilst getting row count")

getBindError : Maybe QueryError -> QueryError
getBindError (Just (BindingError be)) = (BindingError be)
getBindError _ = InternalError

getRowCount : EffM IO [SQLITE (SQLiteConnected)] [SQLITE ()] (Either QueryError Int)
getRowCount = do
  let insert_id_sql = "SELECT last_insert_rowid()"
  sql_prep_res <- prepareStatement insert_id_sql
  if_valid then do
    bind_res_2 <- finishBind
    if_valid then do
      exec_res <- executeStatement
      getRowCount' exec_res
    else do
      let be = getBindError bind_res_2
      cleanupBindFail
      return $ Left be
  else do
    cleanupPSFail
    return $ Left (getQueryError sql_prep_res)

executeInsert : String ->
                String ->
                List (Int, DBVal) ->
                Eff IO [SQLITE ()] (Either QueryError Int)
executeInsert db_name query bind_vals = do
  db_res <- openDB db_name
  if_valid then do
    ps_res <- prepareStatement query
    if_valid then do
      bind_res <- multiBind bind_vals
      if_valid then do
        er_1 <- executeStatement
        finalise
        case er_1 of
          StepFail => do closeDB
                         return $ Left (ExecError "Error inserting")
          Unstarted => do closeDB
                          return $ Left (ExecError "Internal error: 'Unstarted' after execution")
          _ => getRowCount
      else do
        let be = getBindError bind_res
        cleanupBindFail
        return $ Left be
    else do
      cleanupPSFail
      return $ Left (getQueryError ps_res)
  else
    return $ Left (getQueryError db_res)

-- Helper functions for selection from a DB
collectResults : (Eff IO [SQLITE (SQLiteExecuting ValidRow)] (List DBVal)) ->
                 EffM IO [SQLITE (Either (SQLiteExecuting InvalidRow)
                                         (SQLiteExecuting ValidRow))]
                         [SQLITE (SQLiteExecuting InvalidRow)] ResultSet
collectResults fn = do
  if_valid then do
    results <- fn
    step_res <- nextRow
    xs <- collectResults fn
    return $ results :: xs
  else return []

-- Convenience function to abstract around some of the boilerplate code.
-- Takes in the DB name, query, a list of (position, variable value) tuples,
-- a function to process the returned data,
executeSelect : String ->
                String ->
                List (Int, DBVal) ->
                (Eff IO [SQLITE (SQLiteExecuting ValidRow)] (List DBVal)) ->
                Eff IO [SQLITE ()] (Either QueryError ResultSet)
executeSelect db_name q bind_vals fn = do
  conn_res <- openDB db_name
  if_valid then do
    ps_res <- prepareStatement q
    if_valid then do
      bind_res <- multiBind bind_vals
      if_valid then do
        executeStatement
        res <- collectResults fn
        finaliseInvalid
        closeDB
        return $ Right res
      else do
        let be = getBindError bind_res
        cleanupBindFail
        return $ Left be
    else do
      cleanupPSFail
      return $ Left (getQueryError ps_res)
  else
    return $ Left (getQueryError conn_res)

-- Helper function for when there's no binding needed to the PS
-- noBinds : EffM IO [SQLITE (

ext: idr

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
> module Num.Properties

> import Data.Fin
> import Data.Vect
> import Syntax.PreorderReasoning

> import Matrix.Matrix
> import Matrix.Operations
> import Num.Refinements
> import Num.Operations

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

The following

> foldrVectLemma : {A, B : Type} -> {n : Nat} ->
>                  (f : A -> B -> B) -> (e : B) ->
>                  (a : A) -> (as : Vect n A) ->
>                  foldr f e (a :: as) = f a (foldr f e as)

should hold by definition and

< foldrVectLemma f e a as = Refl

should, in principle, type check. In fact, however, |foldr| is
implemented in terms of an accumulator and a proof of |foldrVectLemma|
is not that simple. We start from the "classical" (traditional)
definition of |foldr| for vectors:

> total foldrClassic : (t -> acc -> acc) -> acc -> Vect n t -> acc
> foldrClassic f e []      = e
> foldrClassic f e (x::xs) = f x (foldrClassic f e xs)

In the Idris libraries |foldrImpl| is used instead, but we can prove
the following specification:

> foldrImplLemma : {A, B : Type} -> {n : Nat} ->
>                  (f : A -> B -> B) -> (e : B) -> (go : B -> B) ->
>                  (as : Vect n A) ->
>                  foldrImpl f e go as = go (foldrClassic f e as)
> foldrImplLemma f e go []        = Refl
> foldrImplLemma f e go (a :: as) =
>     ( foldrImpl f e go (a :: as) )
>   ={ Refl }=
>     ( foldrImpl f e (go . (f a)) as )
>   ={ foldrImplLemma f e (go . (f a)) as }=
>     ( (go . (f a)) (foldrClassic f e as) )
>   ={ Refl }=
>     ( go (f a (foldrClassic f e as)) )
>   ={ Refl }=
>     ( go (foldrClassic f e (a :: as) ) )
>   QED
> %freeze foldrImplLemma

Then we can specialise to when |go| is |id| as in the definition of
|foldr|:

> foldrImplCorr :  {A, B : Type} -> {n : Nat} ->
>                  (f : A -> B -> B) -> (e : B) ->
>                  (as : Vect n A) ->
>                  foldrImpl f e Prelude.Basics.id as = foldrClassic f e as
> foldrImplCorr f e as = foldrImplLemma f e Prelude.Basics.id as
> %freeze foldrImplCorr

Now we can continue with the proof:

> foldrVectLemma g e a as =
>     ( foldr g e (a :: as) )
>   ={ Refl }=
>     ( foldrImpl g e id (a :: as) )
>   ={ foldrImplCorr g e (a :: as) }=
>     ( foldrClassic g e (a :: as) )
>   ={ Refl }=
>     ( g a (foldrClassic g e as) )
>   ={ cong {f = g a} (sym (foldrImplCorr g e as)) }=
>     ( g a (foldrImpl g e id as) )
>   ={ Refl }=
>     ( g a (foldr g e as) )
>   QED
> %freeze foldrVectLemma

Finally we get to the one-step unfolding of |sum|:

> sumLemma : (Num t) => (x : t) -> (xs : Vect m t) -> sum (x :: xs) = x + sum xs
> sumLemma x xs = ( sum (x :: xs) )
>               ={ Refl }=
>                 ( foldr (+) (fromInteger 0) (x :: xs) )
>               ={ foldrVectLemma (+) (fromInteger 0) x xs }=
>                 ( x + foldr (+) (fromInteger 0) xs )
>               ={ Refl }=
>                 ( x + sum xs )
>               QED
> %freeze sumLemma

The corresponding lemma for append (|++|) follows from the definition
of append (because it is not defined in terms of |foldrImpl|)

> appendLemma : (x : t) -> (xs : Vect m t) -> (ys : Vect n t) ->
>               ((x :: xs) ++ ys) = (x :: (xs ++ ys))
> appendLemma x xs ys =
>     ( (x :: xs) ++ ys )
>   ={ Refl }=
>     ( x :: (xs ++ ys) )
>   QED
> %freeze appendLemma

> |||
> multSumLemma : (NumMultDistributesOverPlus t) =>
>                (x : t) -> (xs : Vect m t) ->
>                x * sum xs = sum (multSV x xs)
> multSumLemma x  Nil      = ( x * (fromInteger 0) )
>                          ={ multZeroRightZero x }=
>                            ( fromInteger 0 )
>                          ={ Refl }=
>                            ( sum Data.Vect.Nil )
>                          QED
> multSumLemma x (y :: ys) = ( x * (sum (y :: ys)) )
>                          ={ cong (sumLemma y ys) }=
>                            ( x * (y + sum ys) )
>                          ={ Num.Refinements.multDistributesOverPlusRight x y (sum ys) }=
>                            ( (x * y) + (x * sum ys) )
>                          ={ cong (multSumLemma x ys) }=
>                            ( x * y + sum (multSV x ys) )
>                          ={ sym (sumLemma (x * y) (multSV x ys)) }=
>                            ( sum (x * y :: multSV x ys) )
>                          ={ Refl }=
>                            ( sum (multSV x (y :: ys)) )
>                          QED
> %freeze multSumLemma

> sumsTo : Num t => (s : t) -> (xs : Vect m t) -> Type
> sumsTo s xs = (sum xs = s)

> sumOne : Num t => (xs : Vect m t) -> Type
> sumOne = sumsTo (fromInteger 1)

> lemma0 : (NumPlusZeroNeutral t) => (x : t) -> sum (Data.Vect.(::) x Nil) = x
> lemma0 x = ( x + 0 )
>          ={ plusZeroRightNeutral x }=
>            ( x )
>          QED

> lemma1 :  (NumMultDistributesOverPlus t) =>
>           (x : t) -> (xs : Vect n t) ->
>           sumOne xs -> sumsTo x (multSV x xs)
> lemma1 x xs pxs =
>     ( sum (multSV x xs) )
>   ={ sym (multSumLemma x xs) }=
>     ( x * sum xs )
>   ={ cong pxs }=
>     ( x * fromInteger 1 )
>   ={ multOneRightNeutral x }=
>     x
>   QED

> sumPlusAppendLemma :  NumPlusAssociative t =>
>                       (xs : Vect n t) -> (ys : Vect m t) ->
>                       (sum xs + sum ys) = sum (xs ++ ys)
> sumPlusAppendLemma Nil       ys = plusZeroLeftNeutral (sum ys)
> sumPlusAppendLemma (x :: xs) ys =
>     ( sum (x :: xs) + sum ys )
>   ={ cong {f = (+ sum ys)} (sumLemma x xs) }=
>     ( (x + sum xs) + sum ys )
>   ={ sym (plusAssociative x (sum xs) (sum ys)) }=
>     ( x + (sum xs + sum ys) )
>   ={ cong (sumPlusAppendLemma xs ys) }=
>     ( x + sum (xs ++ ys) )
>   ={ sym (sumLemma x (xs ++ ys)) }=
>     ( sum (x :: (xs ++ ys)) )
>   ={ Refl }=
>     ( sum ((x :: xs) ++ ys) )
>   QED
>
> sumMapConcat : (NumPlusAssociative t) => (xss : Matrix m n t) ->
>                sum (map sum xss) = sum (Vect.concat xss)
> sumMapConcat Nil           = Refl
> sumMapConcat (row :: rows) =
>     ( sum (map sum (row :: rows)) )
>   ={ Refl }=
>     ( sum (sum row :: map sum rows) )
>   ={ sumLemma (sum row) (map sum rows) }=
>     ( sum row + sum (map sum rows) )
>   ={ cong (sumMapConcat rows) }=
>     ( sum row + sum (Vect.concat rows) )
>   ={ sumPlusAppendLemma row (Vect.concat rows) }=
>     ( sum (row ++ Vect.concat rows) )
>   ={ Refl }=
>     ( sum (Vect.concat (row :: rows)) )
>   QED

The |multVMLemma| requires both NumAssocPlus and
NumMultDistributesOverPlus and currently there is some problem with
"multiple constraints" so we changed the NumRefinements classes to a
chain instead of a tree.

> ||| 'Tail' of a finite dependently typed function
> depTail : {n : Nat} -> {P : Fin (S n) -> Type} ->
>           ((k : Fin (S n)) -> P k) -> ((j : Fin n) -> P (FS j))
> depTail f k = f (FS k)

> |||
> multVMLemma0 : (NumMultDistributesOverPlus t) =>
>                (xs : Vect m t) -> (xss : Matrix m n t) ->
>                ((k : Fin m) -> sumOne (row k xss)) ->
>                sum (Vect.concat (multVM xs xss)) = sum xs
> multVMLemma0 {m = Z}    {n}  Nil       Nil        _  = Refl
> multVMLemma0 {m = S m'} {n} (x :: xs) (ys :: yss) ps =
>     ( sum (Vect.concat (multVM (x :: xs) (ys :: yss))) )
>   ={ Refl }=
>     ( sum (Vect.concat ((multSV x ys) :: (multVM xs yss))) )
>   ={ sym (sumMapConcat ((multSV x ys) :: (multVM xs yss))) }=
>     ( sum (map sum ((multSV x ys) :: (multVM xs yss))) )
>   ={ Refl }=
>     ( sum (sum (multSV x ys) :: (map sum (multVM xs yss))) )
>   ={ cong {f = \ X => sum (X :: (map sum (multVM xs yss)))}
>           (lemma1 x ys (ps FZ)) }=
>     ( sum (x :: (map sum (multVM xs yss))) )
>   ={ sumLemma x (map sum (multVM xs yss)) }=
>     ( x + sum (map sum (multVM xs yss)) )
>   ={ cong (sumMapConcat (multVM xs yss)) }=
>     ( x + sum (Vect.concat (multVM xs yss)) )
>   ={ cong (multVMLemma0 xs yss (depTail {P = \ k => sumOne (row k (ys :: yss))} ps)) }=
>     ( x + sum xs )
>   ={ sym (sumLemma x xs) }=
>     ( sum (x :: xs) )
>   QED

> multVMLemma : (NumMultDistributesOverPlus t) =>
>               (m : Nat) ->
>               (xs : Vect m t) -> sumOne xs ->
>               (n : Nat) ->
>               (xss : Matrix m n t) ->
>               ((k : Fin m) -> sumOne (row k xss)) ->
>               sumOne (Vect.concat (multVM xs xss))
> multVMLemma m xs pxs n xss pxss =
>     ( sum (Vect.concat (multVM xs xss)) )
>   ={ multVMLemma0 xs xss pxss }=
>     ( sum xs )
>   ={ pxs }=
>     ( fromInteger 1 )
>   QED

> {-
> ||| Alternative - no case analysis, but would need a few lemmas.
> multVMLemma m xs pxs n xss pxss =
>     ( sum (Vect.concat (multVM xs xss)) )
>   ={ sym (sumMapConcat (multVM xs xss)) }=
>     ( sum (map sum     (multVM xs xss)) )
>   ={ Refl }=
>     ( sum (map sum (map (uncurry multSV)  (zip xs xss))) )
>   ={ ?mapFunctorLemma }=
>     ( sum (map (sum .    uncurry multSV ) (zip xs xss)) )
>   ={ ?mapZipLemma }=
>     ( sum (zipWith (\x, xs => sum (multSV x xs)) xs xss) )
>   ={ ?roughlyLemma1UnderLambdas }=
>     ( sum (zipWith (\x, xs => x         ) xs xss) )
>   ={ ?lala4 }=
>     ( sum xs )
>   ={ pxs }=
>     ( fromInteger 1 )
>   QED
> -}

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Network.DefaultHttpEngine
import Network.Wai
import Control.ST
import Network.ST.TcpSockets
import Network.ST.IOUtils
import Network.Socket.Data
import Data.Bool.BoolTheorems
import Data.String.StringUtils

record DefaultHttpEngineState where
  constructor MkDefaultHttpEngineState
  enginePendingRequestVar : Var
  engineBufferedSocket : BufferedSocket

DefaultHttpPendingRequest : Type
DefaultHttpPendingRequest = State ()

%error_reduce
defaultHttpEngineActions : {tcpSockets: TcpSockets m} -> DefaultHttpEngineState -> (ty : Type) -> List (Action ty)
defaultHttpEngineActions {tcpSockets} st ty =
    [ioBuffer (engineBufferedSocket st) ::: State (IOBuffer $ ioSocket (engineBufferedSocket st)),
     ioSocket (engineBufferedSocket st) ::: CFSock tcpSockets]

data DefaultHttpApplication : (m : Type -> Type) -> (tcpSockets: TcpSockets m) -> Type where
  MkDefaultHttpApplication :
    ((engineState : DefaultHttpEngineState) -> HttpRequest
       -> ST m () ((remove (enginePendingRequestVar engineState) DefaultHttpPendingRequest)::(defaultHttpEngineActions {tcpSockets} engineState ()))) -> DefaultHttpApplication m tcpSockets

joinByCRLF : List String -> String
joinByCRLF args =
    go "" args
  where
    go : String -> List String -> String
    go pfx [] = pfx
    go pfx (h::t) = go (pfx ++ h ++ "\n") t

httpHeaderToString : HttpHeader -> String
httpHeaderToString (MkHttpHeader n v) =
  n ++ ": " ++ v

httpResponseToString : HttpResponse -> String
httpResponseToString resp =
  joinByCRLF $
   ("HTTP/1.1 " ++ (show . responseNumber . code $ resp) ++ " " ++
    (show . responseText . code $ resp))::
   ((map httpHeaderToString
         ((MkHttpHeader "Content-Length" (show . Strings.length . body $ resp)) ::
          (headers resp))) ++ ["", body resp])

defaultHttpEngineSendResponse : (m : Type -> Type) -> (tcpSockets: TcpSockets m)
    -> (engineState: DefaultHttpEngineState)
    -> HttpResponse
    -> ST m () ((remove (enginePendingRequestVar engineState) DefaultHttpPendingRequest)::
                              (defaultHttpEngineActions {m} {tcpSockets} engineState ()))
defaultHttpEngineSendResponse m tcpSockets st resp =
     with ST do
       delete (enginePendingRequestVar st)
       True <- call $ fromCFSock tcpSockets (ioSocket (engineBufferedSocket st))
         | False => with ST do
             call $ toCFSock tcpSockets Failed Refl (ioSocket (engineBufferedSocket st))
             pure ()
       True <- call $ writeSocketFully {m} {tcpSocketInstance = tcpSockets}
                (httpResponseToString resp)
                (ioSocket (engineBufferedSocket st))
         | False => with ST do
             call $ toCFSock tcpSockets Failed Refl (ioSocket (engineBufferedSocket st))
             pure ()
       call $ toCFSock tcpSockets Connected Refl (ioSocket (engineBufferedSocket st))

defaultHttpEngineRunApplication : {m : Type -> Type}
                 -> {tcpSockets: TcpSockets m}
                 -> (bindTo: Maybe SocketAddress)
                 -> (port: Int)
                 -> (app: DefaultHttpApplication m tcpSockets)
                 -> ST m String []
defaultHttpEngineRunApplication {m} {tcpSockets} bindTo port app =
  do
    Right listenerSocket <- socket tcpSockets
      | Left code => pure  ("Can't create listener socket on address " ++ (show bindTo) ++ ", error code: " ++ (show code))
    True <- bind tcpSockets bindTo port listenerSocket
      | False => do
         close tcpSockets listenerSocket
         pure "Can't bind listener to port"
    True <- listen tcpSockets listenerSocket
      | False => do
         close tcpSockets listenerSocket
         pure "Can't listen on listener socket"
    err <- applicationAcceptLoop listenerSocket
    close tcpSockets listenerSocket
    pure err
  where
    rtrim : String -> String
    rtrim = reverse . ltrim . reverse
    readHTTPHeaders : (sock : BufferedSocket) -> List HttpHeader -> ST m (Maybe (InvalidRequestOr (List HttpHeader))) (maybeBufferedSocketFails {tcpSocketInstance = tcpSockets} {ty = (InvalidRequestOr (List HttpHeader))} sock)
    readHTTPHeaders sock otherHeaders = do
      Just line <- readLineFromSocket sock
        | Nothing => pure Nothing
      if rtrim line == "" then
        pure $ Just $ ValidRequest otherHeaders
      else do
        let (headerNameUntrimmed, headerValueWithPfx) = break (==':') line
        ifWithProofs (headerValueWithPfx == "")
          (\_ => pure $ Just $ InvalidRequest)
          (\prfNonEmpty => do
            let headerName = rtrim headerNameUntrimmed
            let headerValue = trim (strTail' headerValueWithPfx prfNonEmpty)
            readHTTPHeaders sock (MkHttpHeader headerName headerValue :: otherHeaders)
          )

    readHTTPHead : (sock : BufferedSocket) ->
                      ST m (Maybe (InvalidRequestOr HttpRequest)) (maybeBufferedSocketFails {tcpSocketInstance = tcpSockets} {ty = (InvalidRequestOr HttpRequest)} sock)
    readHTTPHead sock = with ST do
      Just result <- readLineFromSocket sock
        | Nothing => pure Nothing
      let (method, afterMethod) = break (==' ') (trim result)
      let (path, versionAndSpace) = break (==' ') (ltrim afterMethod)
      let version = ltrim versionAndSpace
      Just (ValidRequest httpHeaders) <- readHTTPHeaders sock []
        | Nothing => pure Nothing
        | Just InvalidRequest => pure (Just InvalidRequest)
      -- TODO: HTTP/2
      if (version == "HTTP/1.1" || version == "HTTP/1.0")
        then pure $ Just $ ValidRequest $ MkHttpRequest method httpHeaders ""
        else pure (Just InvalidRequest)

    withContentLength : HttpRequest -> Maybe Nat
    withContentLength req = do
      contentLengthStr <- getHttpHeader "Content-Length" req
      cast (headerValue contentLengthStr)

    readHTTPBody : (sock : BufferedSocket) -> (req : HttpRequest) ->
                      ST m (Maybe String) (maybeBufferedSocketFails {tcpSocketInstance = tcpSockets} {ty = String} sock)
    readHTTPBody sock req =
      case withContentLength req of
        Nothing => pure $ Just ""
        Just contentLength =>
          readFullyFromSocket {tcpSocketInstance = tcpSockets} contentLength sock

    e400Content : String
    e400Content = "Your browser sent a request the server couldn't understand."
    e400Msg : String
    e400Msg = "HTTP/1.1 400 Bad Request\r\nContent-Length: " ++ (show . length $ e400Content)
               ++ "\r\n\r\n" ++ e400Content

    send400 : (sock : BufferedSocket) -> ST m (Maybe ()) (maybeBufferedSocketFails {tcpSocketInstance = tcpSockets} {ty = ()} sock)
    send400 sock = do
      True <- call (writeSocketFully {m} {tcpSocketInstance = tcpSockets}
                     e400Msg (ioSocket sock))
        | False => pure Nothing
      pure $ Just ()

    runAppCall : (sock : BufferedSocket) -> HttpRequest -> DefaultHttpApplication m tcpSockets -> ST m (Maybe ()) (maybeBufferedSocketFails {tcpSocketInstance = tcpSockets} {ty = ()} sock)
    runAppCall sock req (MkDefaultHttpApplication appFn) =
        with ST do
          call $ toCFSock tcpSockets Connected Refl (ioSocket sock)
          pendingRequest <- new ()
          let engineState : DefaultHttpEngineState = MkDefaultHttpEngineState pendingRequest sock
          appFn engineState req
          let engineBufferedSocketPrf : (engineBufferedSocket engineState = sock) = Refl
          doFromCFSock
      where
        doFromCFSock : ST m (Maybe ()) [
            (ioBuffer sock) ::: State (IOBuffer (ioSocket sock))
          , ioSocket sock ::: (CFSock tcpSockets) :-> wrappedMaybeCaseOnly (Sock tcpSockets) Failed Connected
        ]
        doFromCFSock = with ST do
          True <- call $ fromCFSock tcpSockets (ioSocket sock)
          | False => pure Nothing
          pure (Just ())

    incomingConnectionLoop : (sourceAddr : SocketAddress)
                          -> (rawSock : Var)
                          -> ST m () [remove rawSock (Sock tcpSockets Connected)]
    incomingConnectionLoop sourceAddr rawSock = do
        (sock ** prfSockEquiv) <- initBufferedSocket rawSock
        (rewrite prfSockEquiv in go sock)
        closeBufferedSocket sock
      where
        go : (sock : BufferedSocket) -> ST m (Maybe ()) (maybeBufferedSocketFails {tcpSocketInstance = tcpSockets} {ty = ()} sock)
        go sock = with ST do
          -- TODO: Consider some kind of timeout on incoming connections
          Just (ValidRequest headers) <- readHTTPHead sock
            | Nothing => pure Nothing
            | Just InvalidRequest =>
              send400 sock
          Just body <- readHTTPBody sock headers
            | Nothing => pure Nothing
          let req = record { body = body } headers
          Just _ <- runAppCall sock req app
            | Nothing => pure Nothing
          go sock

    applicationAcceptLoop : (listener: Var) -> ST m String [listener ::: Sock tcpSockets Listening :-> Sock tcpSockets Failed]
    applicationAcceptLoop listener = do
      -- TODO: Consider some kind of limit on the number of open connections to
      -- avoid a DoS
      Just _ <- accept tcpSockets listener incomingConnectionLoop
        | Nothing => pure "Failed to accept"
      applicationAcceptLoop listener

export
defaultHttpEngine : (m : Type -> Type) -> (tcpSockets : TcpSockets m) -> HttpEngine m
defaultHttpEngine m tcpSockets = MkHttpEngine
  {- Application -} (DefaultHttpApplication m tcpSockets)
  {- EngineState -} DefaultHttpEngineState
  {- httpEngineActions -} defaultHttpEngineActions
  {- pendingRequestVar -} enginePendingRequestVar
  {- PendingRequest -} DefaultHttpPendingRequest
  {- sendResponse -} (defaultHttpEngineSendResponse m tcpSockets)
  {- mkApplication -} MkDefaultHttpApplication
  {- runApplication -} (defaultHttpEngineRunApplication {m} {tcpSockets})


text:
module Bautzen.REPL.SExpInstances

import Bautzen.Combats
import Bautzen.GameUnit
import Bautzen.Game.Core
import Bautzen.Pos
import Bautzen.Terrain
import Bautzen.SExp

import Data.Fin
import Data.Vect

export
ToSExp Side where
  toSExp Axis = SSym "Axis"
  toSExp Allies = SSym "Allies"

export
ToSExp Nation where
  toSExp German = SSym "German"
  toSExp Russian = SSym "Russian"
  toSExp Polish = SSym "Polish"

export
ToSExp UnitType where
  toSExp Armored = SSym "Armored"
  toSExp HeavyArmored = SSym "HeavyArmored"
  toSExp MechInfantry = SSym "MechInfantry"
  toSExp Infantry = SSym "Infantry"
  toSExp HeavyEngineer = SSym "HeavyEngineer"
  toSExp Artillery = SSym "Artillery"
  toSExp AntiTank = SSym "AntiTank"
  toSExp HQ = SSym "HQ"
  toSExp SupplyColumn = SSym "SupplyColumn"

export
ToSExp UnitSize where
  toSExp Regiment = SSym "Regiment"
  toSExp Brigade = SSym "Brigade"
  toSExp Division = SSym "Division"
  toSExp Corps = SSym "Corps"
  toSExp Army = SSym "Army"

export
ToSExp StdFactors where
  toSExp (MkStdFactors attack defense) =
    SList [ toSExp attack
          , toSExp defense
          ]

export
ToSExp Arty where
  toSExp (MkArty support distance) =
    SList [ toSExp support
          , toSExp distance
          ]

export
ToSExp Pak where
  toSExp (MkPak antitank) = toSExp antitank

export
ToSExp GameUnit where
  toSExp (MkGameUnit nation unitType name parent size move currentMP steps hits combat) =
    SList [ SSym ":unit"
          , toSExp nation
          , toSExp unitType
          , toSExp name
          , toSExp parent
          , toSExp size
          , toSExp move
          , toSExp currentMP
          , toSExp steps
          , toSExp hits
          , case unitType of
              Armored       => toSExp combat
              HeavyArmored  => toSExp combat
              MechInfantry  => toSExp combat
              Infantry      => toSExp combat
              HeavyEngineer => toSExp combat
              Artillery     => toSExp combat
              AntiTank      => toSExp combat
              HQ            => toSExp combat
              SupplyColumn  => toSExp combat
          ]

export
ToSExp Pos where
  toSExp (Hex col row) =
    SList [ toSExp col
          , toSExp row
          ]

export
ToSExp Cost where
  toSExp = toSExp . toNat

export
ToSExp GameError where
  toSExp (NoSuchUnits unitNames) = SList [ SSym ":error", SSym "NoSuchUnit", toSExp unitNames ]
  toSExp (NotYourTurn side) = SList [ SSym ":error", SSym "NotYourTurn", toSExp side ]
  toSExp (EnemyInHex unit hex) = SList [ SSym ":error", SSym "EnemyInHex", toSExp unit, toSExp hex ]
  toSExp (MoveFromZocToZoc unit to) = SList [ SSym ":error", SSym "MoveFromZocToZoc", toSExp unit, toSExp to ]
  toSExp (ForbiddenTerrain from to) = SList [ SSym ":error", SSym "ForbiddenTerrain", toSExp from, toSExp to ]
  toSExp (InvalidMove from to) = SList [ SSym ":error", SSym "InvalidMove", toSExp from, toSExp to ]
  toSExp (NotEnoughMPs unit from to mp) = SList [ SSym ":error", SSym "NotEnoughMPs", toSExp unit, toSExp from, toSExp to, toSExp mp ]
  toSExp (NotAdjacentTo units to) = SList [ SSym ":error", SSym "NotAdjacentTo", toSExp units , toSExp to ]
  toSExp (NothingToAttack target) = SList [ SSym ":error", SSym "NothingToAttack", toSExp target ]
  toSExp (AttackingOwnUnits units target) = SList [ SSym ":error", SSym "AttackingOwnUnits", toSExp units , toSExp target ]
  toSExp (NotInSupportRange units) = SList [ SSym ":error", SSym "NotInSupportRange", toSExp units ]
  toSExp (NotSupportingUnits units) = SList [ SSym ":error", SSym "NotSupportingUnits", toSExp units ]
  toSExp (NotInChainOfCommand units) = SList [ SSym ":error", SSym "NotInChainOfCommand", toSExp units ]
  toSExp (NoSupplyColumnThere hex) = SList [ SSym ":error", SSym "NoSupplyColumnThere", toSExp hex ]
  toSExp (NoStepsToLose side) = SList [ SSym ":error", SSym "NoStepsToLose", toSExp side ]
  toSExp (CombatInProgress side) = SList [ SSym ":error", SSym "CombatInProgress", toSExp side ]
  toSExp GameHasEnded = SList [ SSym ":error", SSym "GameHasEnded" ]

export
ToSExp Losses where
  toSExp (attackerLoss /> defenderLoss) = SList [ toSExp attackerLoss, toSExp defenderLoss ]

export
ToSExp EngagedUnits where
  toSExp (MkEngagedUnits base tacticalSupport strategicSupport) =
    SList [ SSym ":engaged"
          , SSym ":base", toSExp base
          , SSym ":tactical-support", toSExp tacticalSupport
          , SSym ":strategic-support", toSExp strategicSupport
          ]

export
ToSExp CombatState where
  toSExp (MkCombatState hex attackers defenders losses) =
    SList [ SSym ":combat-state"
          , SSym ":combat-hex", toSExp hex
          , SSym ":attackers", toSExp attackers
          , SSym ":defenders", toSExp defenders
          , SSym ":losses", toSExp losses
          ]

export
ToSExp CombatPhase where
  toSExp NoCombat = SSym "NoCombat"
  toSExp (AssignTacticalSupport side combat) = SList [ SSym "AssignTacticalSupport",  toSExp side, toSExp combat ]
  toSExp (AssignStrategicSupport side combat) = SList [ SSym "AssignStrategicSupport",  toSExp side, toSExp combat ]
  toSExp (ApplyLosses side combat) = SList [ SSym "ApplyLosses",  toSExp side, toSExp combat ]
  toSExp (Resolve combat) = SList [ SSym "Resolve", toSExp combat ]

export
ToSExp GameSegment where
  toSExp Supply = SSym "Supply"
  toSExp Move = SSym "Move"
  toSExp (Combat phase) = SList [ SSym "Combat", toSExp phase ]
  toSExp GameEnd = SSym "GameEnd"

export
ToSExp Event where
  toSExp (Moved unit from to cost) =
      SList [ SSym ":moved"
            , SSym ":unit", toSExp unit
            , SSym ":from", toSExp from
            , SSym ":to", toSExp to
            , SSym ":cost", toSExp cost
            ]
  toSExp (CombatEngaged atk def target) =
      SList [ SSym ":combat-engaged"
            , SSym ":attackers", toSExp atk
            , SSym ":defenders", toSExp def
            , SSym ":target", toSExp target
            ]
  toSExp (TacticalSupportProvided side units) =
      SList [ SSym ":tactical-support-provided"
            , SSym ":supported-side", toSExp side
            , SSym ":supporting-units", toSExp units
            ]
  toSExp (SupplyColumnUsed side hex) =
      SList [ SSym ":supply-column-used"
            , SSym ":supported-side", toSExp side
            , SSym ":position", toSExp hex
            ]
  toSExp (CombatResolved state losses) =
      SList [ SSym ":combat-resolved"
            , SSym ":state", toSExp state
            , SSym ":losses", toSExp losses
            ]
  toSExp (StepLost side unit remain) =
      SList [ SSym ":step-lost"
            , SSym ":side", toSExp side
            , SSym ":unit", toSExp unit
            , SSym ":remaining-losses", toSExp remain
            ]
  toSExp (SegmentChanged from to) =
      SList [ SSym ":segment-changed"
            , SSym ":from", toSExp from
            , SSym ":to", toSExp to
            ]
  toSExp (TurnEnded n) =
      SList [ SSym ":turn-ended"
            , SSym ":new-turn", toSExp n
            ]
  toSExp AxisTurnDone =
      SList [ SSym ":axis-turn-done" ]
  toSExp GameEnded =
      SList [ SSym ":game-ended" ]

export
splice : SExp -> SExp -> SExp
splice first (SList xs) = SList $ first :: xs
splice first s  = SList [ first, s ]

export
ToSExp Terrain where
  toSExp Clear = SSym "Clear"
  toSExp Wood = SSym "Wood"
  toSExp Rough = SSym "Rough"
  toSExp RoughWood = SSym "RoughWood"
  toSExp (Hill base) = splice (SSym "Hill") (toSExp base)
  toSExp (Village base) = splice (SSym "Village") (toSExp base)
  toSExp Town = SSym "Town"
  toSExp (SupplySource side base) = splice (SList [ SSym "Supply", toSExp side] ) (toSExp base)

export
ToSExp Connection where
  toSExp Plain = SSym "Plain"
  toSExp (Road base) = splice (SSym "Road") (toSExp base)
  toSExp (River base) = splice (SSym "River") (toSExp base)
  toSExp Lake = SSym "Lake"

export
ToSExp Map where
  toSExp (MkMap hexes edges) = SList [ SList [ SSym ":hexes", toSExp (tabulate hexes) ]
                                     , SList [ SSym ":edges", toSExp edges ]
                                     ]
export
ToSExp QueryError where
  toSExp (NoSupplyPathFor unitName pos) = SList [ SSym "NoSupplyPathFor", SStr unitName, toSExp pos ]
  toSExp (UnitDoesNotExist unitName) = SList [ SSym "UnitDoesNotExist", SStr unitName ]

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Main

record TestRecord where
  constructor MkTestRecord
  recField : Int

testRec : TestRecord
testRec = MkTestRecord 0

updatedRec : TestRecord
updatedRec = record { recField = 1 } testRec


text:
module ConstructedInt

import MoreNatProofs
import NonZeroNat

%access public export
%default total

data ConsInt : Type where
  Negative : (n : Nat) -> ConsInt
  Positive : (n : Nat) -> ConsInt

%name ConsInt h, i, j, k, l

getSign : (i : ConsInt) -> (Nat -> ConsInt)
getSign (Negative n) = Negative
getSign (Positive n) = Positive

castIntegerToConsInt : Integer -> ConsInt
castIntegerToConsInt x = case x < 0 of
                              False => Positive (toNat x)
                              True => Negative (toNat (abs x))

negPlusPos : Nat -> Nat -> ConsInt
negPlusPos n k = case isLTE n k of
                      (Yes prf) => Positive (k - n)
                      (No contra) => Negative ((-) n k {smaller = notLTEFlips contra})

addConsInt : ConsInt -> ConsInt -> ConsInt
addConsInt (Negative n) (Negative k) = Negative (n + k)
addConsInt (Negative n) (Positive k) = negPlusPos n k
addConsInt (Positive n) (Positive k) = Positive (n + k)
addConsInt (Positive n) (Negative k) = negPlusPos k n

multConsInt : ConsInt -> ConsInt -> ConsInt
multConsInt (Negative n) (Negative k) = Positive (n * k)
multConsInt (Positive n) (Positive k) = Positive (n * k)
multConsInt (Negative n) (Positive k) = Negative (n * k)
multConsInt (Positive n) (Negative k) = Negative (n * k)

Num ConsInt where
  (+) = addConsInt
  (*) = multConsInt

  fromInteger = castIntegerToConsInt

Abs ConsInt where
  abs (Negative n) = Positive n
  abs (Positive n) = Positive n

negateConsInt : ConsInt -> ConsInt -> ConsInt
negateConsInt x (Negative n) = x + (Positive n)
negateConsInt x (Positive n) = x + (Negative n)

Neg ConsInt where
  negate x = negateConsInt (fromInteger 0) x
  (-) = negateConsInt

equalConsInt : ConsInt -> ConsInt -> Bool
equalConsInt (Negative n) (Negative k) = n == k
equalConsInt (Negative Z) (Positive Z) = True
equalConsInt (Negative Z) (Positive (S k)) = False
equalConsInt (Negative (S j)) (Positive Z) = False
equalConsInt (Negative (S j)) (Positive (S k)) = False
equalConsInt (Positive Z) (Negative Z) = True
equalConsInt (Positive Z) (Negative (S k)) = False
equalConsInt (Positive (S j)) (Negative k) = False
equalConsInt (Positive n) (Positive k) = n == k

Eq ConsInt where
  (==) = equalConsInt

Cast Integer ConsInt where
  cast = castIntegerToConsInt

castConsIntToInteger : (orig : ConsInt) -> Integer
castConsIntToInteger (Positive n) = cast n
castConsIntToInteger (Negative n) = -(cast n)

Cast ConsInt Integer where
  cast = castConsIntToInteger

castNatToConsInt : (orig : Nat) -> ConsInt
castNatToConsInt orig = Positive orig

Cast Nat ConsInt where
  cast = castNatToConsInt

castConsIntToString : (orig : ConsInt) -> String
castConsIntToString orig = cast (castConsIntToInteger orig)

Cast ConsInt String where
  cast = castConsIntToString

Show ConsInt where
  show = castConsIntToString

-- Proofs
negSameNumberEq : {m : Nat} -> Negative m = Negative m
negSameNumberEq {m = Z} = Refl
negSameNumberEq {m = (S k)} = Refl

sameSignSameAbsValueEq : {sign : (Nat -> ConsInt)} -> {auto n : Nat} -> (sign m) = (sign m)
sameSignSameAbsValueEq {sign = sign} {n = n} = Refl

negativeZNotEqNegSk : {auto n : Nat} -> ((Negative Z) = (Negative (S n)) -> Void)
negativeZNotEqNegSk Refl impossible

negEqImpliesNegSuccEq : (prf : k = j) -> Negative (S k) = Negative (S j)
negEqImpliesNegSuccEq Refl = Refl

notEqNegativeImpliesNotEq : (contra : (k = j) -> Void) -> (Negative (S k) = Negative (S j)) -> Void
notEqNegativeImpliesNotEq contra Refl = contra Refl

data Eq : (m, n : ConsInt) -> Type where
  EqZeroBothNeg : Eq (Negative Z) (Negative Z)
  EqZeroFirstPos : Eq (Positive Z) (Negative Z)
  EqZeroFirstNeg : Eq (Negative Z) (Positive Z)
  EqZeroBothPos : Eq (Positive Z) (Positive Z)
  EqSuccPos : Eq (Positive (S k)) (Positive (S k))
  EqSuccNeg : Eq (Negative (S l)) (Negative (S l))

NegZeroNotEqSucc : Eq (Negative 0) (Negative (S k)) -> Void
NegZeroNotEqSucc EqZeroBothNeg impossible
NegZeroNotEqSucc EqZeroFirstPos impossible
NegZeroNotEqSucc EqZeroFirstNeg impossible
NegZeroNotEqSucc EqZeroBothPos impossible
NegZeroNotEqSucc EqSuccPos impossible
NegZeroNotEqSucc EqSuccNeg impossible

NegSuccNotEqZero : Eq (Negative (S j)) (Negative 0) -> Void
NegSuccNotEqZero EqZeroBothNeg impossible
NegSuccNotEqZero EqZeroFirstPos impossible
NegSuccNotEqZero EqZeroFirstNeg impossible
NegSuccNotEqZero EqZeroBothPos impossible
NegSuccNotEqZero EqSuccPos impossible
NegSuccNotEqZero EqSuccNeg impossible

NegSuccEq : (prf : j = k) -> Eq (Negative (S j)) (Negative (S k))
NegSuccEq Refl = EqSuccNeg

NegSuccNotEq : (contra : (j = k) -> Void) -> Eq (Negative (S j)) (Negative (S k)) -> Void
NegSuccNotEq contra EqSuccNeg = contra Refl

negZeroNotEqPositiveSucc : Eq (Negative 0) (Positive (S k)) -> Void
negZeroNotEqPositiveSucc EqZeroBothNeg impossible
negZeroNotEqPositiveSucc EqZeroFirstPos impossible
negZeroNotEqPositiveSucc EqZeroFirstNeg impossible
negZeroNotEqPositiveSucc EqZeroBothPos impossible
negZeroNotEqPositiveSucc EqSuccPos impossible
negZeroNotEqPositiveSucc EqSuccNeg impossible

negSuccNotEqPositiveZero : Eq (Negative (S j)) (Positive 0) -> Void
negSuccNotEqPositiveZero EqZeroBothNeg impossible
negSuccNotEqPositiveZero EqZeroFirstPos impossible
negSuccNotEqPositiveZero EqZeroFirstNeg impossible
negSuccNotEqPositiveZero EqZeroBothPos impossible
negSuccNotEqPositiveZero EqSuccPos impossible
negSuccNotEqPositiveZero EqSuccNeg impossible

negSuccNotEqPosSucc : Eq (Negative (S j)) (Positive (S k)) -> Void
negSuccNotEqPosSucc EqZeroBothNeg impossible
negSuccNotEqPosSucc EqZeroFirstPos impossible
negSuccNotEqPosSucc EqZeroFirstNeg impossible
negSuccNotEqPosSucc EqZeroBothPos impossible
negSuccNotEqPosSucc EqSuccPos impossible
negSuccNotEqPosSucc EqSuccNeg impossible

posZeroNotEqNegSucc : Eq (Positive 0) (Negative (S k)) -> Void
posZeroNotEqNegSucc EqZeroBothNeg impossible
posZeroNotEqNegSucc EqZeroFirstPos impossible
posZeroNotEqNegSucc EqZeroFirstNeg impossible
posZeroNotEqNegSucc EqZeroBothPos impossible
posZeroNotEqNegSucc EqSuccPos impossible
posZeroNotEqNegSucc EqSuccNeg impossible

posSuccNotEqNegZero : Eq (Positive (S j)) (Negative 0) -> Void
posSuccNotEqNegZero EqZeroBothNeg impossible
posSuccNotEqNegZero EqZeroFirstPos impossible
posSuccNotEqNegZero EqZeroFirstNeg impossible
posSuccNotEqNegZero EqZeroBothPos impossible
posSuccNotEqNegZero EqSuccPos impossible
posSuccNotEqNegZero EqSuccNeg impossible

posSuccNotEqNegSucc : Eq (Positive (S j)) (Negative (S k)) -> Void
posSuccNotEqNegSucc EqZeroBothNeg impossible
posSuccNotEqNegSucc EqZeroFirstPos impossible
posSuccNotEqNegSucc EqZeroFirstNeg impossible
posSuccNotEqNegSucc EqZeroBothPos impossible
posSuccNotEqNegSucc EqSuccPos impossible
posSuccNotEqNegSucc EqSuccNeg impossible

posZeroNotEqSucc : Eq (Positive 0) (Positive (S k)) -> Void
posZeroNotEqSucc EqZeroBothNeg impossible
posZeroNotEqSucc EqZeroFirstPos impossible
posZeroNotEqSucc EqZeroFirstNeg impossible
posZeroNotEqSucc EqZeroBothPos impossible
posZeroNotEqSucc EqSuccPos impossible
posZeroNotEqSucc EqSuccNeg impossible

posSuccNotEqZero : Eq (Positive (S j)) (Positive 0) -> Void
posSuccNotEqZero EqZeroBothNeg impossible
posSuccNotEqZero EqZeroFirstPos impossible
posSuccNotEqZero EqZeroFirstNeg impossible
posSuccNotEqZero EqZeroBothPos impossible
posSuccNotEqZero EqSuccPos impossible
posSuccNotEqZero EqSuccNeg impossible

posSuccEq : (prf : j = k) -> Eq (Positive (S j)) (Positive (S k))
posSuccEq Refl = EqSuccPos

posSuccNotEq : (contra : (j = k) -> Void) -> Eq (Positive (S j)) (Positive (S k)) -> Void
posSuccNotEq contra EqSuccPos = contra Refl

-- I really wish I could find a way to make proofs here more concise.
isEq : (i, j : ConsInt) -> Dec (i `Eq` j)
isEq (Negative Z) (Negative Z) = Yes EqZeroBothNeg
isEq (Negative Z) (Negative (S k)) = No NegZeroNotEqSucc
isEq (Negative (S j)) (Negative Z) = No NegSuccNotEqZero
isEq (Negative (S j)) (Negative (S k)) = case isEq j k of
                                              (Yes prf) => Yes (NegSuccEq prf)
                                              (No contra) => No (NegSuccNotEq contra)
isEq (Negative Z) (Positive Z) = Yes EqZeroFirstNeg
isEq (Negative Z) (Positive (S k)) = No negZeroNotEqPositiveSucc
isEq (Negative (S j)) (Positive Z) = No negSuccNotEqPositiveZero
isEq (Negative (S j)) (Positive (S k)) = No negSuccNotEqPosSucc
isEq (Positive Z) (Negative Z) = Yes EqZeroFirstPos
isEq (Positive Z) (Negative (S k)) = No posZeroNotEqNegSucc
isEq (Positive (S j)) (Negative Z) = No posSuccNotEqNegZero
isEq (Positive (S j)) (Negative (S k)) = No posSuccNotEqNegSucc
isEq (Positive Z) (Positive Z) = Yes EqZeroBothPos
isEq (Positive Z) (Positive (S k)) = No posZeroNotEqSucc
isEq (Positive (S j)) (Positive Z) = No posSuccNotEqZero
isEq (Positive (S j)) (Positive (S k)) = case isEq j k of
                                              (Yes prf) => Yes (posSuccEq prf)
                                              (No contra) => No (posSuccNotEq contra)

||| Proofs that `m` is not equal to `n`
||| @ m the first number
||| @ n the second number
NotEq : (m, n : ConsInt) -> Type
NotEq m n = Not (m `Eq` n)

eQImplNotNotEq : (prf : Eq h i) -> (Eq h i -> Void) -> Void
eQImplNotNotEq prf f = f prf

notEqImplNotEq : (contra : Eq h i -> Void) -> Eq h i -> Void
notEqImplNotEq contra x = contra x

isNotEq : (h, i : ConsInt) -> Dec (h `NotEq` i)
isNotEq h i = case isEq h i of
                   (Yes prf) => No (eQImplNotNotEq prf)
                   (No contra) => Yes (notEqImplNotEq contra)

data LTE : (j, k : ConsInt) -> Type where
  ||| -m <= +n
  LTENegPos : LTE (Negative m) (Positive n)
  ||| -(m + 1) <= -0
  LTEBothNegWZero : LTE (Negative (S m)) (Negative Z)
  ||| +0 <= +(n + 1)
  LTEBothPosWZero : LTE (Positive Z) (Positive (S n))
  ||| left >= right -> -left <= -right
  LTEBothNegLTE : LTE right left -> LTE (Negative left) (Negative right)
  ||| left >= right -> +left >= + right
  LTEBothPosLTE : Nat.LTE left right -> LTE (Positive left) (Positive right)
  ||| j = k -> j <= k
  LTEBothEq : Eq j k -> LTE j k

negZeroNotLTENegSucc : LTE (Negative 0) (Negative (S k)) -> Void
negZeroNotLTENegSucc (LTEBothEq EqZeroBothNeg) impossible
negZeroNotLTENegSucc (LTEBothEq EqZeroFirstPos) impossible
negZeroNotLTENegSucc (LTEBothEq EqZeroFirstNeg) impossible
negZeroNotLTENegSucc (LTEBothEq EqZeroBothPos) impossible
negZeroNotLTENegSucc (LTEBothEq EqSuccPos) impossible
negZeroNotLTENegSucc (LTEBothEq EqSuccNeg) impossible

posZeroNotLTENegSucc : LTE (Positive 0) (Negative (S k)) -> Void
posZeroNotLTENegSucc (LTEBothEq EqZeroBothNeg) impossible
posZeroNotLTENegSucc (LTEBothEq EqZeroFirstPos) impossible
posZeroNotLTENegSucc (LTEBothEq EqZeroFirstNeg) impossible
posZeroNotLTENegSucc (LTEBothEq EqZeroBothPos) impossible
posZeroNotLTENegSucc (LTEBothEq EqSuccPos) impossible
posZeroNotLTENegSucc (LTEBothEq EqSuccNeg) impossible

posSuccNotLTENeg : LTE (Positive (S j)) (Negative k) -> Void
posSuccNotLTENeg (LTEBothEq EqZeroBothNeg) impossible
posSuccNotLTENeg (LTEBothEq EqZeroFirstPos) impossible
posSuccNotLTENeg (LTEBothEq EqZeroFirstNeg) impossible
posSuccNotLTENeg (LTEBothEq EqZeroBothPos) impossible
posSuccNotLTENeg (LTEBothEq EqSuccPos) impossible
posSuccNotLTENeg (LTEBothEq EqSuccNeg) impossible

posSuccNotLTEZero : LTE (Positive (S j)) (Positive 0) -> Void
posSuccNotLTEZero (LTEBothPosLTE LTEZero) impossible
posSuccNotLTEZero (LTEBothPosLTE (LTESucc _)) impossible
posSuccNotLTEZero (LTEBothEq EqZeroBothNeg) impossible
posSuccNotLTEZero (LTEBothEq EqZeroFirstPos) impossible
posSuccNotLTEZero (LTEBothEq EqZeroFirstNeg) impossible
posSuccNotLTEZero (LTEBothEq EqZeroBothPos) impossible
posSuccNotLTEZero (LTEBothEq EqSuccPos) impossible
posSuccNotLTEZero (LTEBothEq EqSuccNeg) impossible

negSuccNotGTEImposs : (contra : GTE l k -> Void) -> LTE (Negative (S l)) (Negative (S k)) -> Void
negSuccNotGTEImposs contra (LTEBothNegLTE (LTESucc x)) = contra x
negSuccNotGTEImposs {l = l} {k = l} contra (LTEBothEq EqSuccNeg) = contra lteRefl

posSuccNotLTEImposs : (contra : LTE l k -> Void) -> LTE (Positive (S l)) (Positive (S k)) -> Void
posSuccNotLTEImposs contra (LTEBothPosLTE (LTESucc x)) = contra x
posSuccNotLTEImposs {l = l} {k = l} contra (LTEBothEq EqSuccPos) = contra lteRefl

isLTE : (i, j : ConsInt) -> Dec (i `LTE` j)
isLTE (Negative Z) (Negative Z) = Yes (LTEBothEq EqZeroBothNeg)
isLTE (Negative Z) (Negative (S k)) = No negZeroNotLTENegSucc
isLTE (Negative (S j)) (Negative Z) = Yes LTEBothNegWZero
isLTE (Negative (S l)) (Negative (S k)) = case isGTE l k of
                                               (Yes prf) => Yes (LTEBothNegLTE (LTESucc prf))
                                               (No contra) => No (negSuccNotGTEImposs contra)
isLTE (Negative n) (Positive k) = Yes LTENegPos
isLTE (Positive Z) (Negative Z) = Yes (LTEBothEq EqZeroFirstPos)
isLTE (Positive Z) (Negative (S k)) = No posZeroNotLTENegSucc
isLTE (Positive (S j)) (Negative k) = No posSuccNotLTENeg
isLTE (Positive Z) (Positive Z) = Yes (LTEBothEq EqZeroBothPos)
isLTE (Positive Z) (Positive (S k)) = Yes LTEBothPosWZero
isLTE (Positive (S j)) (Positive Z) = No posSuccNotLTEZero
isLTE (Positive (S l)) (Positive (S k)) = case isLTE l k of
                                               (Yes prf) => Yes (LTEBothPosLTE (LTESucc prf))
                                               (No contra) => No (posSuccNotLTEImposs contra)

GTE : ConsInt -> ConsInt -> Type
GTE h i = LTE i h

isGTE : (h, i : ConsInt) -> Dec (h `GTE` i)
isGTE h i = isLTE i h

data LT : (h, i : ConsInt) -> Type where
  LTPosZeroPosSucc : LT (Positive Z) (Positive (S m))
  LTNegPosSucc : LT (Negative (S m)) (Positive i)
  LTNegLTSwap : Nat.LT m n -> LT (Negative n) (Negative m)
  LTPosLT : Nat.LT m n -> LT (Positive m) (Positive n)
  LTNotEqLTE : ConstructedInt.NotEq h i -> LTE h i -> LT h i

notLTEImplNotEq : (contra : ConstructedInt.LTE h i -> Void) -> NotEq h i
notLTEImplNotEq {h} {i} contra = case ConstructedInt.isEq h i of
                                      (Yes prf) => void (contra (LTEBothEq prf))
                                      (No contra1) => contra1

-- Basically a computer generated proof, with lots of case splits and searches.  Hopefully Idris 2 will do this sort of thing better.  Alternatively, maybe I can find out what I'm doing wrong.
isLTAndIsEqImposs : (prf1 : Eq h i) -> (prf : LT h i) -> NotEq h i
isLTAndIsEqImposs EqZeroBothNeg (LTNegLTSwap LTEZero) impossible
isLTAndIsEqImposs EqZeroBothNeg (LTNegLTSwap (LTESucc _)) impossible
isLTAndIsEqImposs EqZeroBothNeg (LTNotEqLTE f (LTEBothNegLTE LTEZero)) = \__pi_arg => f EqZeroBothNeg
isLTAndIsEqImposs EqZeroBothNeg (LTNotEqLTE f (LTEBothEq EqZeroBothNeg)) = \__pi_arg => f EqZeroBothNeg
isLTAndIsEqImposs EqZeroFirstPos (LTNotEqLTE f (LTEBothEq EqZeroFirstPos)) = \__pi_arg => f EqZeroFirstPos
isLTAndIsEqImposs EqZeroFirstNeg (LTNotEqLTE f LTENegPos) = \__pi_arg => f EqZeroFirstNeg
isLTAndIsEqImposs EqZeroFirstNeg (LTNotEqLTE f (LTEBothEq EqZeroFirstNeg)) = \__pi_arg => f EqZeroFirstNeg
isLTAndIsEqImposs EqZeroBothPos (LTPosLT LTEZero) impossible
isLTAndIsEqImposs EqZeroBothPos (LTPosLT (LTESucc _)) impossible
isLTAndIsEqImposs EqZeroBothPos (LTNotEqLTE f (LTEBothPosLTE LTEZero)) = \__pi_arg => f EqZeroBothPos
isLTAndIsEqImposs EqZeroBothPos (LTNotEqLTE f (LTEBothEq EqZeroBothPos)) = \__pi_arg => f EqZeroBothPos
isLTAndIsEqImposs EqSuccPos (LTPosLT (LTESucc x)) = \__pi_arg => lTELeftNotSuccOfRight x
isLTAndIsEqImposs EqSuccPos (LTNotEqLTE f (LTEBothPosLTE (LTESucc x))) = \__pi_arg => f EqSuccPos
isLTAndIsEqImposs EqSuccPos (LTNotEqLTE f (LTEBothEq EqSuccPos)) = \__pi_arg => f EqSuccPos
isLTAndIsEqImposs EqSuccNeg (LTNegLTSwap (LTESucc x)) = \__pi_arg => lTELeftNotSuccOfRight x
isLTAndIsEqImposs EqSuccNeg (LTNotEqLTE f (LTEBothNegLTE x)) = \__pi_arg => f EqSuccNeg
isLTAndIsEqImposs EqSuccNeg (LTNotEqLTE f (LTEBothEq EqSuccNeg)) = \__pi_arg => f EqSuccNeg

lTImplNotEq : (prf : ConstructedInt.LT h i) -> NotEq h i
lTImplNotEq {h} {i} prf = case isEq h i of
                               (Yes prf1) => isLTAndIsEqImposs prf1 prf
                               (No contra) => contra

lTEAndLTImplNotEq : (prf : ConstructedInt.LTE h i) -> (x : LT h i) -> NotEq h i
lTEAndLTImplNotEq {h} {i} prf x = case isLTE h i of
                               (Yes prf) => lTImplNotEq x
                               (No contra) => notLTEImplNotEq contra

makeNotEq : (contra : NotEq h i -> Void) -> (prf : LTE h i) -> (x : LT h i) -> Eq h i -> Void
makeNotEq contra prf x y = contra (lTEAndLTImplNotEq prf x)

lteLtImplNotEq : (prf : ConstructedInt.LTE h i) -> (x : LT h i) -> NotEq h i
lteLtImplNotEq {h} {i} prf x = case isNotEq h i of
                            (Yes prf1) => prf1
                            (No contra) => makeNotEq contra prf x

lTNotNotEq : (contra : ConstructedInt.NotEq h i -> Void) -> (prf : LTE h i) -> LT h i -> Void
lTNotNotEq contra prf x = contra (lteLtImplNotEq prf x)

eQImpliesLTE : (h, i : ConsInt) -> (prf : Eq h i) -> LTE h i
eQImpliesLTE (Negative Z) (Negative Z) EqZeroBothNeg = LTEBothNegLTE LTEZero
eQImpliesLTE (Positive Z) (Negative Z) EqZeroFirstPos = LTEBothEq EqZeroFirstPos
eQImpliesLTE (Negative Z) (Positive Z) EqZeroFirstNeg = LTENegPos
eQImpliesLTE (Positive Z) (Positive Z) EqZeroBothPos = LTEBothPosLTE LTEZero
eQImpliesLTE (Positive (S k)) (Positive (S k)) EqSuccPos = LTEBothPosLTE (LTESucc lTEkk)
eQImpliesLTE (Negative (S l)) (Negative (S l)) EqSuccNeg = LTEBothNegLTE (LTESucc lTEkk)

notEqAndNotLTEImplLT : (h, i : ConsInt) -> (contra1 : Eq h i -> Void) -> (contra : LTE h i -> Void) -> LT h i
notEqAndNotLTEImplLT (Negative Z) (Negative Z) contra1 contra = LTNegLTSwap ?notEqAndNotLTEImplLT_rhs_6
notEqAndNotLTEImplLT (Negative Z) (Negative (S k)) contra1 contra = ?notEqAndNotLTEImplLT_rhs_7
notEqAndNotLTEImplLT (Negative (S j)) (Negative Z) contra1 contra = ?notEqAndNotLTEImplLT_rhs_2
notEqAndNotLTEImplLT (Negative (S j)) (Negative (S k)) contra1 contra = ?notEqAndNotLTEImplLT_rhs_8
notEqAndNotLTEImplLT (Negative Z) (Positive Z) contra1 contra = ?notEqAndNotLTEImplLT_rhs_4
notEqAndNotLTEImplLT (Negative Z) (Positive (S k)) contra1 contra = ?notEqAndNotLTEImplLT_rhs_10
notEqAndNotLTEImplLT (Negative (S j)) (Positive k) contra1 contra = ?notEqAndNotLTEImplLT_rhs_9
notEqAndNotLTEImplLT (Positive n) (Negative k) contra1 contra = ?notEqAndNotLTEImplLT_rhs_1
notEqAndNotLTEImplLT (Positive n) (Positive k) contra1 contra = ?notEqAndNotLTEImplLT_rhs_5

notLTEImplLT : (contra : ConstructedInt.LTE h i -> Void) -> LT h i
notLTEImplLT {h} {i} contra = case isEq h i of
                                   (Yes prf) => void (contra (eQImpliesLTE h i prf))
                                   (No contra1) => notEqAndNotLTEImplLT h i contra1 contra

isLT : (h, i : ConsInt) -> Dec (h `LT` i)
isLT h i = case isLTE h i of
                (Yes prf) => (case isNotEq h i of
                                   (Yes prf1) => Yes (LTNotEqLTE prf1 prf)
                                   (No contra) => No (lTNotNotEq contra prf))
                (No contra) => Yes (notLTEImplLT contra)

-- Testing with types

%access private

fourMinusTenIsNegativeSix : Eq ((Positive 4) - (Positive 10)) (Negative 6)
fourMinusTenIsNegativeSix = EqSuccNeg

fourMinusNegativeTenIsNotNegativeSix : Eq ((Positive 4) - (Negative 10)) (Negative 6) -> Void
fourMinusNegativeTenIsNotNegativeSix EqZeroBothNeg impossible
fourMinusNegativeTenIsNotNegativeSix EqZeroFirstPos impossible
fourMinusNegativeTenIsNotNegativeSix EqZeroFirstNeg impossible
fourMinusNegativeTenIsNotNegativeSix EqZeroBothPos impossible
fourMinusNegativeTenIsNotNegativeSix EqSuccPos impossible
fourMinusNegativeTenIsNotNegativeSix EqSuccNeg impossible

fourMinusTenIsLessThanNegativeTwo : LTE ((Positive 4) - (Positive 10)) (Negative 2)
fourMinusTenIsLessThanNegativeTwo = LTEBothNegLTE (LTESucc (LTESucc LTEZero))

fourMinusTenIsNotLessThanNegativeFour : LTE ((Positive 4) - (Positive 5)) (Negative 4) -> Void
fourMinusTenIsNotLessThanNegativeFour (LTEBothNegLTE (LTESucc LTEZero)) impossible
fourMinusTenIsNotLessThanNegativeFour (LTEBothNegLTE (LTESucc (LTESucc _))) impossible
fourMinusTenIsNotLessThanNegativeFour (LTEBothEq EqZeroBothNeg) impossible
fourMinusTenIsNotLessThanNegativeFour (LTEBothEq EqZeroFirstPos) impossible
fourMinusTenIsNotLessThanNegativeFour (LTEBothEq EqZeroFirstNeg) impossible
fourMinusTenIsNotLessThanNegativeFour (LTEBothEq EqZeroBothPos) impossible
fourMinusTenIsNotLessThanNegativeFour (LTEBothEq EqSuccPos) impossible
fourMinusTenIsNotLessThanNegativeFour (LTEBothEq EqSuccNeg) impossible

aNegativeTimesANegativeIsAPositive : LTE (Positive Z) ((Negative n) * (Negative m))
aNegativeTimesANegativeIsAPositive = LTEBothPosLTE LTEZero

max_stars_repo_name: zenntenn/Idris-NumericProofs

max_issues_repo_name: zenntenn/Idris-NumericProofs

max_forks_repo_name: zenntenn/Idris-NumericProofs


text:
||| The `Javascript` code generator.
module Compiler.ES.Javascript

import Compiler.ES.Codegen

import Compiler.Common
import Compiler.CompileExpr

import Core.Context
import Core.TT
import Core.Options
import Libraries.Utils.Path

import System
import System.File

import Data.Maybe
import Data.String
import Libraries.Data.String.Extra

%default covering

||| Compile a TT expression to Javascript
compileToJS : Ref Ctxt Defs ->
              ClosedTerm -> Core String
compileToJS c tm = compileToES c Javascript tm ["browser", "javascript"]

htmlHeader : String
htmlHeader = concat $ the (List String) $
           [ "<html>\n"
           , " <head>\n"
           , "  <meta charset='utf-8'>\n"
           , " </head>\n"
           , " <body>\n"
           , "  <script type='text/javascript'>\n"
           ]

htmlFooter : String
htmlFooter = concat $ the (List String) $
           [ "\n  </script>\n"
           , " </body>\n"
           , "</html>"
           ]

addHeaderAndFooter : String -> String -> String
addHeaderAndFooter outfile es =
  case toLower <$>  extension outfile of
    Just "html" => htmlHeader ++ es ++ htmlFooter
    _ => es

||| Javascript implementation of the `compileExpr` interface.
compileExpr :  Ref Ctxt Defs
            -> (tmpDir : String)
            -> (outputDir : String)
            -> ClosedTerm
            -> (outfile : String)
            -> Core (Maybe String)
compileExpr c tmpDir outputDir tm outfile =
  do es <- compileToJS c tm
     let res = addHeaderAndFooter outfile es
     let out = outputDir </> outfile
     Core.writeFile out res
     pure (Just out)

||| Node implementation of the `executeExpr` interface.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm =
  throw $ InternalError "Javascript backend is only able to compile, use Node instead"

||| Codegen wrapper for Javascript implementation.
export
codegenJavascript : Codegen
codegenJavascript = MkCG compileExpr executeExpr Nothing Nothing


text:
import Http
import Http.Uri
import Http.Error
import Http.RawResponse
import Http.Request
import Http.Response
import Data.SortedMap -- Remove after upgrading to idris 0.9.19
import Network.Socket
import System

processArgs : List String -> Maybe (Host, Port, String)
processArgs (_::host::port::path::_) =
  Just (host, (cast port), path)
processArgs (_::host::path::_) = Just (host, 80, path)
processArgs _ = Nothing

partial
main : IO ()
main =
  case processArgs !getArgs of
    Just (host, port, path) =>
      case !(simpleHttp host port path) of
        Left err => print err >>= \_ => putStr "\n"
        Right res => do
          putStrLn "Response status:"
          print (responseStatus res)
          putStr "\n\n"

          putStrLn "Headers Received:"
          traverse (\x => do print x; putStr "\n") (Data.SortedMap.toList $ responseHeaders res)
          putStr "\n\n"

          putStrLn "Body:"
          print (responseBody res)
          putStr "\n\n"
    Nothing => putStrLn "Usage: ./simple host [port] path"

max_stars_repo_name: unthingable/idris-https

max_issues_repo_name: unthingable/idris-https

max_forks_repo_name: unthingable/idris-https


text:
module Test.API

import Common

UserId : Type
record User where
  userId : UserId
  name : String
data A = A1 Int | A2 String
data B : Type where
  B1 : Int -> B
  B2 : String -> B

ユーザ一覧 : API UserId (Int, Double, String)


text:
module Extra.OpenSSL.OBJ

import Control.Linear.LIO
import Extra.C.CPtr
import Extra.OpenSSL.FFI
import public Extra.OpenSSL.OBJData

%foreign libcrypto "OBJ_nid2sn"
export
prim__OBJ_nid2sn : CInt -> PrimIO CString

export
OBJ_nid2sn : LinearIO io => NID -> L io (CPtr (NullTerminated False))
OBJ_nid2sn (MkNID id) = do
  ptr <- primIO $ prim__OBJ_nid2sn id
  pure $ MkCPtr ptr


text:
module Main

import Data.Nat
import Data.DPair

fib : (n : Nat) -> Int
fib Z = 0
fib (S Z) = 1
fib (S (S k)) = fib k + fib (S k)

fibc : (n : Nat) -> Int
fibc n = loop n 0 1
  where
    loop : (n : Nat) -> (f0 : Int) -> (f1 : Int) -> Int
    loop Z     f0 _  = f0
    loop (S n) f0 f1 = loop n f1 (f0 + f1)

data Fib : (0 _ : Nat) -> Int -> Type where
  Fib0 : Fib 0 0
  Fib1 : Fib 1 1
  FibN :  {0 n : Nat}
       -> {r0, r1 : Int}
       -> (0 _ : Fib n r0) -> (0 _ : Fib (S n) r1)
       -> Fib (S (S n)) (r0 + r1)

fibCert : (n : Nat) -> (r : Int ** Fib n r)
fibCert 0         = (_ ** Fib0)
fibCert (S 0)     = (_ ** Fib1)
fibCert (S (S k)) =
  case (fibCert k , fibCert (S k)) of
    ((r0 ** p0) , (r1 ** p1)) => (r0 + r1 ** FibN p0 p1)

fibcCert : (n : Nat) -> Int
fibcCert n = fst calc
  where
    loop : {r0, r1 : Int} -> (i : Nat) -> (ni : Nat) -> Fib i r0 -> Fib (S i) r1 -> Subset Int (Fib (ni + i))
    loop i Z     pf0 pf1 = (Element _ pf0)
    loop i (S k) pf0 pf1 = rewrite (plusSuccRightSucc k i) in loop (S i) k pf1 (FibN pf0 pf1)

    calc : Subset Int (Fib n)
    calc = rewrite (sym (plusZeroRightNeutral n)) in loop 0 n Fib0 Fib1

main : IO ()
main = printLn $ fibcCert 40

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module VirtualDOM.DOM

import Data.List

%default total
%access export

export
record Node where
  constructor MkNode
  unNode : Ptr

%inline
jscall : (name : String) -> (ty : Type) -> {auto fty : FTy FFI_JS [] ty} ->ty
jscall name ty = foreign FFI_JS name ty

documentBody : JS_IO Node
documentBody = MkNode <$> jscall "document.body" _

getElementById : (elementId : String) -> JS_IO Node
getElementById elementId = MkNode <$>
  jscall "document.getElementById(%0)"
    (String -> JS_IO Ptr) elementId

nthChild : (parent : Node) -> (n : Int) -> JS_IO Node
nthChild parent n = MkNode <$>
  jscall "%0.childNodes[%1]" (Ptr -> Int -> JS_IO Ptr) (unNode parent) n

appendChild : (parent : Node) -> (child : Node) -> JS_IO Node
appendChild parent child = MkNode <$>
  jscall "%0.appendChild(%1)" (Ptr -> Ptr -> JS_IO Ptr)
  (unNode parent) (unNode child)

removeChild : (parent : Node) -> (child : Node) -> JS_IO Node
removeChild parent child = MkNode <$>
  jscall "%0.removeChild(%1)" (Ptr -> Ptr -> JS_IO Ptr)
  (unNode parent) (unNode child)

replaceChild : (parent : Node) -> (newChild : Node) -> (oldChild : Node) ->
               JS_IO ()
replaceChild parent newChild oldChild =
  jscall "%0.replaceChild(%1, %2)" (Ptr -> Ptr -> Ptr -> JS_IO ())
  (unNode parent) (unNode newChild) (unNode oldChild)

setAttribute : Node -> (name : String) -> (value : String) -> JS_IO ()
setAttribute = jscall "%0.setAttribute(%1, %2)"
  (Ptr -> String -> String -> JS_IO ()) . unNode

removeAttribute : Node -> (name : String) -> JS_IO ()
removeAttribute = jscall "%0.removeAttribute(%1)"
  (Ptr -> String -> JS_IO ()) . unNode

createElement : (tag : String) -> JS_IO Node
createElement = liftA MkNode . jscall "document.createElement(%0)" _

createTextNode : (text : String) -> JS_IO Node
createTextNode = liftA MkNode . jscall "document.createTextNode(%0)" _

setInnerHTML : (element : Node) -> (html : String) -> JS_IO ()
setInnerHTML = jscall "%0.innerHTML = %1" (Ptr -> String -> JS_IO ()) . unNode

record ListenerOptions where
  constructor MkListenerOptions
  once : Maybe Bool
  capture : Maybe Bool
  passive : Maybe Bool

noOptions : ListenerOptions
noOptions = MkListenerOptions Nothing Nothing Nothing

jsonParse : (json : String) -> JS_IO Ptr
jsonParse = jscall "JSON.parse(%0)" _

optionsToPtr : ListenerOptions -> JS_IO Ptr
optionsToPtr options =
  let
    optStrings =
      mapMaybe optToJsonField
        [ ("once", once)
        , ("capture", capture)
        , ("passive", passive)
        ]
    optString = "{" ++ (foldr (++) "" (intersperse "," optStrings)) ++ "}"
  in
    jsonParse optString
  where
    optToJsonField : (String, ListenerOptions -> Maybe Bool) -> Maybe String
    optToJsonField (name, getVal) = do
      val <- getVal options
      let valJson = if val then "true" else "false"
      pure ("\"" ++ name ++ "\"" ++ ":" ++ valJson)

partial
addEventListener : (eventTarget : Node) -> (eventName : String) ->
                   (listener : Ptr -> JS_IO ()) ->
                   (options : ListenerOptions) ->
                   JS_IO ()
addEventListener eventTarget eventName listener options =
  optionsToPtr options >>=
    jscall "%0.addEventListener(%1, %2, %3)"
      (Ptr -> String -> JsFn (Ptr -> JS_IO ()) -> Ptr -> JS_IO ())
      (unNode eventTarget) eventName (MkJsFn listener)

partial
removeEventListener : (eventTarget : Node) -> (eventName : String) ->
                      (listener : Ptr -> JS_IO ()) ->
                      (options : ListenerOptions) ->
                      JS_IO ()
removeEventListener eventTarget eventName listener options =
  optionsToPtr options >>=
    jscall "%0.removeEventListener(%1, %2, %3)"
      (Ptr -> String -> JsFn (Ptr -> JS_IO ()) -> Ptr -> JS_IO ())
      (unNode eventTarget) eventName (MkJsFn listener)

dispatchEvent : (eventName : String) -> (bubbles : Bool) -> (eventTarget : Node) -> JS_IO Bool
dispatchEvent eventName bubbles eventTarget = do
  let bubblesInt = if bubbles then 1 else 0
  sbool <- jscall "%0.dispatchEvent(new Event(%1,{bubbles:%2===1})).toString()"
    (Ptr -> String -> Int -> JS_IO String)
    (unNode eventTarget) eventName bubblesInt
  pure $ sbool == "true"

max_stars_repo_name: concert/idris-vdom

max_issues_repo_name: concert/idris-vdom

max_forks_repo_name: concert/idris-vdom


text:
module PullRequest

import Data.Config
import Data.Fin.Extra
import Data.Fuel
import Data.List
import Data.List1
import Data.Nat
import Data.Pagination
import Data.Promise
import Data.PullRequest
import Data.Review
import Data.String
import Data.String.Extra
import FFI.Concurrency
import FFI.Git
import FFI.GitHub
import Language.JSON
import Language.JSON.Accessors
import Reviewer
import Text.PrettyPrint.Prettyprinter
import Text.PrettyPrint.Prettyprinter.Render.Terminal
import Util

%default total

public export
data IdentifiedOrCreated = Identified | Created

public export
record PRHistory where
  constructor MkPRHistory
  openPRs   : List PullRequest
  closedPRs : List PullRequest

empty : PRHistory
empty = MkPRHistory { openPRs = [], closedPRs = [] }

||| Produce a tuple of (open, closed) from the PR History.
export
tuple : PRHistory -> (List PullRequest, List PullRequest)
tuple (MkPRHistory openPRs closedPRs) = (openPRs, closedPRs)

export
combined : PRHistory -> List PullRequest
combined history = history.openPRs ++ history.closedPRs

||| Extract a tuple of open and closed PR reviewer names
||| from a PR history. A given reviewer's login appears
||| in the result once for each review request.
export
(.allReviewers) : PRHistory -> (List String, List String)
(.allReviewers) = mapHom (join . map reviewers) . tuple

||| Extract a list of author logins. A given author's login
||| appears in the result once for each PR authored.
export
(.allAuthors) : PRHistory -> List String
history.allAuthors = author <$> (history.openPRs ++ history.closedPRs)

partition : List PullRequest -> PRHistory
partition = uncurry MkPRHistory . partition ((== Open) . (.state))

||| Create a fork of this program that retrieves the given page of PRs
||| and outputs the result as JSON.
forkedPRs : (perPage : Nat) -> (currentPageIdx : Nat) -> (currentPageSize : Nat) -> (x : ()) -> Promise Future
forkedPRs perPage page _ _ = fork "pulls --json \{show perPage} \{show page}"

||| Grab all of the given pages of PRs and create a history from them.
partition' : Pagination _ _ _ () -> Promise PRHistory
partition' pgs =
  do prJsons <- promiseAll =<< traverse' forkedPRs pgs
     pulls   <- either $ traverse (array parsePR) prJsons
     pure $ partition (join pulls)

||| Get the most recent PRs by creation date and partition them
||| into open and closed PRs.
|||
||| @prCount The number of PRs to retrieve.
||| @pageBreaks The number of pages over which to break the requests up.
export
listPartitionedPRs : Config => Octokit =>
                     {default 0 pageBreaks : Nat}
                  -> (prCount : Fin 101)
                  -> Promise PRHistory
listPartitionedPRs @{config} {pageBreaks} prCount with ((finToNat prCount) `isGT` 0, pageBreaks `isGT` 0)
  _ | (No _, _) = pure empty
  _ | (_, No _) = partition <$> listPullRequests config.org config.repo Nothing prCount
  _ | (Yes prf, Yes prf') with ((S pageBreaks) `isLTE` (finToNat prCount))
    _ | (No _)       = partition' (metaPages  (finToNat prCount)  1)
    _ | (Yes prf'') = partition' (metaPages' (finToNat prCount) (S pageBreaks))

export
listReviewers : Config => Octokit =>
                {default 0 pageBreaks : Nat}
             -> (prCount : Fin 101)
             -> Promise (List String, List String)
listReviewers = map (.allReviewers) . (listPartitionedPRs {pageBreaks})

||| Get the reviews on the given PRs by the given user.
export
reviewsForUser : Config => Octokit =>
                 (author : String)
              -> List PullRequest
              -> Promise (List Review)
reviewsForUser @{config} author prs =
  do let filteredPrs = filter (\pr => not $ isAuthor author pr || isRequestedReviewer author pr) prs
     -- ^ we know we aren't looking for reviews on the author's PRs.
     reviewsJson <- promiseAll =<< traverse forkedReviews filteredPrs
     -- ^ list of JSON Arrays
     reviews <- either $ traverse (array parseReview) reviewsJson
     pure $ filter (isAuthor author) (join reviews)
  where
    forkedReviews : PullRequest -> Promise Future
    forkedReviews = fork . ("reviews --json " ++) . show . number

||| Request reviews.
||| @ teamNames       The slugs of teams from which to draw potential review candidates.
||| @ forcedReviewers The logins of users to force review from (in addition to the reviewer
|||                   chosen from the selected teams).
export
requestReviewers : Config => Octokit =>
                   PullRequest
                -> (teamNames : List String)
                -> (forcedReviewers : List String)
                -> {default False dry: Bool}
                -> Promise ()
requestReviewers @{config} pr teamNames forcedReviewers {dry} =
  do (openReviewers, closedReviewers) <- listReviewers 100 {pageBreaks=4}
     teamMembers <- join <$> traverse (listTeamMembers config.org) teamNames
     -- printLn teamMembers
     let chosenCandidates = chooseReviewers closedReviewers openReviewers teamMembers [] pr.author
     -- printLn chosenCandidates
     chosenUser <- randomReviewer chosenCandidates
     let users = (toList chosenUser) ++ forcedReviewers
     let teams = if config.assignTeams then teamNames else []
     when (not dry) $
       do ignore $ addPullReviewers config.org config.repo pr.number users teams
          when config.commentOnAssign $
            whenJust chosenUser $ \cu =>
              createComment config.org config.repo pr.number (prComment cu)
     if null users
       then putStrLn . maybeDecorate $ vsep [
                       annotate (color Yellow) $ pretty "Could not pick a user from the given Team "
                     , pretty "(perhaps the only option was the author of the pull request?)."
                     ]
       else putStrLn . maybeDecorate $ vsep [
                       pretty "Assigned \{userNotice chosenUser}\{teamNotice teams} to the open PR "
                     , pretty "for the current branch (\{pr.webURI})."
                     ]
  where
    maybeDecorate : Doc AnsiStyle -> String
    maybeDecorate doc =
      let render = if config.colors then id else unAnnotate
      in  renderString . layoutPretty defaultLayoutOptions $ render doc

    csv : List String -> String
    csv = maybeDecorate . encloseSep emptyDoc emptyDoc (pretty ", ") . map (annotate (color Green) . pretty)

    userNotice : (chosenReviewer : Maybe String) -> String
    userNotice Nothing       = case forcedReviewers of
                                    []         => "no users"
                                    reviewers  => "\{csv reviewers}"
    userNotice (Just chosen) = "\{csv (chosen :: forcedReviewers)}"

    teamNotice : List String -> String
    teamNotice []     = ""
    teamNotice [name] = " and team \{csv [name]}"
    teamNotice names  = " and teams \{csv names}"

    prComment : String -> String
    prComment chosenUser = """
    :musical_note: Harmoniously assigned @\{chosenUser} to review this PR.
    """

export
identifyOrCreatePR : Config => Git => Octokit =>
                     (branch : String)
                  -> Promise (IdentifiedOrCreated, PullRequest)
identifyOrCreatePR @{config} branch =
  do [openPr] <- listPRsForBranch config.org config.repo branch
       | [] => (Created,) <$> createPR
       | _  => reject "Multiple PRs for the current brach. We only handle 1 PR per branch currently."
     pure (Identified, openPr)
  where
    createPR : Promise PullRequest
    createPR =
      do when (!remoteTrackingBranch == Nothing) $
           do -- TODO: Don't assume origin. we can get that from git. store in config?
              putStrLn "Creating a new remote branch..."
              pushNewBranch "origin" branch
         putStrLn "Creating a new PR for the current branch (\{branch})."
         putStrLn "What branch are you merging into (ENTER for default: \{config.mainBranch})?"
         baseBranchInput <- trim <$> getLine
         let baseBranch = case strM baseBranchInput of
                               (StrCons c cs) => c `strCons` cs
                               StrNil         => config.mainBranch
         putStrLn "What would you like the title to be?"
         let titlePrefix = fromMaybe "" $ (++ " - ") <$> parseJiraPrefix branch
         putStr titlePrefix
         title <- (titlePrefix ++) . trim <$> getLine
         putStrLn "What would you like the description to be (two blank lines to finish)?"
         description <- unlines <$> getManyLines (limit 100)
         putStrLn "Creating PR..."
         putStrLn branch
         GitHub.createPR config.org config.repo branch baseBranch title description

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony