text:
||| This module provides a simple common subexpression elimination (CSE)
||| algorithm. The main goal right now is to move duplicate
||| expressions introduced during autosearch (which includes
||| interface resolution) to the top level.
|||
||| As such, the functionality provided by this module should
||| be considered a form of whole program optimization.
||| To keep things simple, it operates only on closed terms right
||| now, which are - in case of several occurences - introduced
||| as new zero-argument toplevel functions.
|||
||| The procedure is very simple: In an analysis step, we
||| iterate over all toplevel definitions once, trying to
||| convert every subexpression to a closed one (no free
||| variables). Closed terms are then stored in a `SortedMap`
||| together with their size and count.
|||
||| This map is then pruned: Expressions with a count of 1 are removed,
||| as are very small terms (some experiments showed, that a
||| cut-off size of 5 is a good heuristic). The remaining duplicate
||| expressions are then introduced as new zero-argument toplevel
||| functions and replaced accordingly in all function definitions
||| (including larger extracted subexpressions, if any).
module Compiler.Opts.CSE

import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.Name
import Core.TT

import Core.Ord
import Data.List
import Data.Nat
import Data.String
import Data.Vect
import Libraries.Data.SortedMap
import Libraries.Data.NameMap

||| Maping from a pairing of closed terms together with
||| their size (for efficiency) to the number of
||| occurences in toplevel definitions.
public export
UsageMap : Type
UsageMap = SortedMap (Integer, CExp []) (Name, Integer)

--------------------------------------------------------------------------------
--          Size of Expressions
--------------------------------------------------------------------------------

mutual
  -- comparison for `Nat` is (or used to be?) O(n),
  -- therefore, we use `Integer`
  size : CExp ns -> Integer
  size (CLocal _ _)         = 1
  size (CRef _ _)           = 1
  size (CLam _ _ y)         = size y + 1
  size (CLet _ _ _ y z)     = size y + size z + 1
  size (CApp _ _ xs)        = sum (map size xs) + 1
  size (CCon _ _ _ _ xs)    = sum (map size xs) + 1
  size (COp _ _ xs)         = sum (map size xs) + 1
  size (CExtPrim _ _ xs)    = sum (map size xs) + 1
  size (CForce _ _ y)       = size y + 1
  size (CDelay _ _ y)       = size y + 1
  size (CPrimVal _ _)       = 1
  size (CErased _)          = 1
  size (CCrash _ _)         = 1
  size (CConCase _ sc xs x) =
    size sc + sum (map sizeConAlt xs) + sum (map size x) + 1

  size (CConstCase _ sc xs x) =
    size sc + sum (map sizeConstAlt xs) + sum (map size x) + 1

  sizeConAlt : CConAlt ns -> Integer
  sizeConAlt (MkConAlt _ _ _ _ z) = 1 + size z

  sizeConstAlt : CConstAlt ns -> Integer
  sizeConstAlt (MkConstAlt _ y) = 1 + size y

--------------------------------------------------------------------------------
--          State
--------------------------------------------------------------------------------

data Sts : Type where

record St where
  constructor MkSt
  map : UsageMap
  idx : Int

-- adds a new closed expression to the `UsageMap`
-- returning the actual count of occurences.
-- very small expressions are being ignored.
store : Ref Sts St => CExp [] -> Core Integer
store exp =
  let sz = size exp
   in if sz < 5
         then pure 0
         else do
           (MkSt map idx)    <- get Sts

           (name,count,idx2) <-
             case lookup (sz,exp) map of
               Just (nm,cnt) => pure (nm, cnt+1, idx)
               Nothing       => pure (MN "csegen" idx, 1, idx + 1)

           put Sts $ MkSt (insert (sz,exp) (name, count) map) idx2
           pure count

--------------------------------------------------------------------------------
--          Strengthening of Expressions
--------------------------------------------------------------------------------

dropVar :  (pre : List Name)
        -> (n : Nat)
        -> (0 p : IsVar x n (pre ++ ns))
        -> Maybe (IsVar x n pre)
dropVar [] _ _        = Nothing
dropVar (y :: xs) 0 First = Just First
dropVar (y :: xs) (S k) (Later p) =
  case dropVar xs k p of
    Just p' => Just $ Later p'
    Nothing => Nothing

mutual
  -- tries to 'strengthen' an expression by removing
  -- a prefix of bound variables. typically, this is invoked
  -- with `{pre = []}`.
  dropEnv : {pre : List Name} -> CExp (pre ++ ns) -> Maybe (CExp pre)
  dropEnv (CLocal {idx} fc p) = (\q => CLocal fc q) <$> dropVar pre idx p
  dropEnv (CRef fc x) = Just (CRef fc x)
  dropEnv (CLam fc x y) = CLam fc x <$> dropEnv y
  dropEnv (CLet fc x inlineOK y z) =
    CLet fc x inlineOK <$> dropEnv y <*> dropEnv z
  dropEnv (CApp fc x xs) = CApp fc <$> dropEnv x <*> traverse dropEnv xs
  dropEnv (CCon fc x y tag xs) = CCon fc x y tag <$> traverse dropEnv xs
  dropEnv (COp fc x xs) = COp fc x <$> traverse dropEnv xs
  dropEnv (CExtPrim fc p xs) = CExtPrim fc p <$> traverse dropEnv xs
  dropEnv (CForce fc x y) = CForce fc x <$> dropEnv y
  dropEnv (CDelay fc x y) = CDelay fc x <$> dropEnv y
  dropEnv (CConCase fc sc xs x) =
    CConCase fc            <$>
    dropEnv sc             <*>
    traverse dropConAlt xs <*>
    traverse dropEnv x

  dropEnv (CConstCase fc sc xs x) =
    CConstCase fc            <$>
    dropEnv sc               <*>
    traverse dropConstAlt xs <*>
    traverse dropEnv x

  dropEnv (CPrimVal fc x) = Just $ CPrimVal fc x
  dropEnv (CErased fc) = Just $ CErased fc
  dropEnv (CCrash fc x) = Just $ CCrash fc x

  dropConAlt :  {pre : List Name}
             -> CConAlt (pre ++ ns)
             -> Maybe (CConAlt pre)
  dropConAlt (MkConAlt x y tag args z) =
    MkConAlt x y tag args . embed <$> dropEnv z

  dropConstAlt :  {pre : List Name}
               -> CConstAlt (pre ++ ns)
               -> Maybe (CConstAlt pre)
  dropConstAlt (MkConstAlt x y) = MkConstAlt x <$> dropEnv y

--------------------------------------------------------------------------------
--          Analysis
--------------------------------------------------------------------------------

mutual
  -- Tries to convert an expression to a closed term (`CExp []`).
  -- If this is successful, the expression's number of occurences
  -- is increased by one, otherwise, its subexpressions are analyzed
  -- in a similar manner.
  --
  -- We have to be careful here not to count subexpressions too
  -- often. For instance, consider a case of `outerExp (innerExp)`,
  -- where both `outerExp` and `innerExp` are closed terms. `innerExp`
  -- should be added to the set of extracted subexpressions, if
  -- and only if it appears somewhere else in the code,
  -- unrelated to `outerExp`. We must
  -- therefore make sure to analyze subexpressions of closed terms
  -- exactly once for each closed term, otherwise they might
  -- be counted as additional common subexpressions although they are not.
  export
  analyze : Ref Sts St => CExp ns -> Core ()

  -- We ignore prim ops here, since moving them to the toplevel
  -- might interfere with other optimizations, for instance
  -- the one dealing with #1320.
  -- Some other terms are ignored, as I (@stefan-hoeck)
  -- am being conservative here,
  -- not daring to inadvertently change the semantics
  -- of the program.
  analyze c@(COp _ _ _)      = analyzeSubExp c
  analyze c@(CExtPrim _ _ _) = analyzeSubExp c
  analyze c@(CForce _ _ _)   = analyzeSubExp c
  analyze c@(CDelay _ _ _)   = analyzeSubExp c

  analyze exp = case dropEnv {pre = []} exp of
    Just e0 => do
      count <- store e0
      -- only analyze subexpressions of closed terms once
      when (count == 1) $ analyzeSubExp exp
    Nothing => analyzeSubExp exp

  analyzeSubExp : Ref Sts St => CExp ns -> Core ()
  analyzeSubExp (CLocal _ _)         = pure ()
  analyzeSubExp (CRef _ _)           = pure ()
  analyzeSubExp (CLam _ _ y)         = analyze y
  analyzeSubExp (CLet _ _ _ y z)     = analyze y >> analyze z
  analyzeSubExp (CApp fc x xs)       = analyze x >> traverse_ analyze xs
  analyzeSubExp (CCon _ _ _ _ [])    = pure ()
  analyzeSubExp (CCon _ _ _ _ xs)    = traverse_ analyze xs
  analyzeSubExp (COp _ _ xs)         = ignore $ traverseVect analyze xs
  analyzeSubExp (CExtPrim _ _ xs)    = traverse_ analyze xs
  analyzeSubExp (CForce _ _ y)       = analyze y
  analyzeSubExp (CDelay _ _ y)       = analyze y
  analyzeSubExp (CConCase _ sc xs x) =
    analyze sc                     >>
    traverse_ analyzeConAlt xs     >>
    ignore (traverseOpt analyze x)

  analyzeSubExp (CConstCase _ sc xs x) =
    analyze sc                     >>
    traverse_ analyzeConstAlt xs   >>
    ignore (traverseOpt analyze x)

  analyzeSubExp (CPrimVal _ _) = pure ()
  analyzeSubExp (CErased _)    = pure ()
  analyzeSubExp (CCrash _ _)   = pure ()

  analyzeConAlt : { auto c : Ref Sts St } -> CConAlt ns -> Core ()
  analyzeConAlt (MkConAlt _ _ _ _ z) = analyze z

  analyzeConstAlt : Ref Sts St => CConstAlt ns -> Core ()
  analyzeConstAlt (MkConstAlt _ y) = analyze y

analyzeDef : Ref Sts St => CDef -> Core ()
analyzeDef (MkFun args x)    = analyze x
analyzeDef (MkCon _ _ _)     = pure ()
analyzeDef (MkForeign _ _ _) = pure ()
analyzeDef (MkError _)       = pure ()

analyzeName : Ref Sts St => Ref Ctxt Defs => Name -> Core ()
analyzeName fn = do
    defs <- get Ctxt
    Just def <- lookupCtxtExact fn (gamma defs)
        | Nothing => pure ()
    let Just cexp = compexpr def
        | Nothing => pure ()
    analyzeDef cexp

||| Generates a `UsageMap` (a mapping from closed terms
||| to their number of occurences plus newly generated
||| name in case they will be lifted to the toplevel)
export
analyzeNames :  Ref Ctxt Defs => List Name -> Core UsageMap
analyzeNames cns = do
  log "compiler.cse" 10 $ "Analysing " ++ show (length cns) ++ " names"
  s <- newRef Sts $ MkSt empty 0
  traverse_ analyzeName cns
  MkSt res _ <- get Sts
  let filtered = reverse
               . sortBy (comparing $ snd . snd)
               . filter ((> 1) . snd . snd)
               $ SortedMap.toList res

  log "compiler.cse" 10 $ unlines $
    "Selected the following definitions:"
    ::  map (\((sz,_),(name,cnt)) =>
                  show name ++
                  ": count " ++ show cnt ++
                  ", size " ++ show sz
           ) filtered

  pure $ fromList filtered

--------------------------------------------------------------------------------
--          Adjusting Expressions
--------------------------------------------------------------------------------

mutual
  export
  adjust : UsageMap -> CExp ns -> CExp ns
  adjust um exp = case dropEnv {pre = []} exp of
    Nothing => adjustSubExp um exp
    Just e0 => case lookup (size e0, e0) um of
      Just (nm,_) => CApp EmptyFC (CRef EmptyFC nm) []
      Nothing     => adjustSubExp um exp

  adjustSubExp : UsageMap -> CExp ns -> CExp ns
  adjustSubExp um e@(CLocal _ _) = e
  adjustSubExp um e@(CRef _ _) = e
  adjustSubExp um e@(CPrimVal _ _) = e
  adjustSubExp um e@(CErased _) = e
  adjustSubExp um e@(CCrash _ _) = e
  adjustSubExp um (CLam fc x y) = CLam fc x $ adjust um y
  adjustSubExp um (CLet fc x inlineOK y z) =
    CLet fc x inlineOK (adjust um y) (adjust um z)

  adjustSubExp um (CApp fc x xs) =
    CApp fc (adjust um x) (map (adjust um) xs)

  adjustSubExp um (CCon fc x y tag xs) =
    CCon fc x y tag $ map (adjust um) xs

  adjustSubExp um (COp fc x xs) = COp fc x $ map (adjust um) xs

  adjustSubExp um (CExtPrim fc p xs) = CExtPrim fc p $ map (adjust um) xs

  adjustSubExp um (CForce fc x y) = CForce fc x $ adjust um y

  adjustSubExp um (CDelay fc x y) = CDelay fc x $ adjust um y

  adjustSubExp um (CConCase fc sc xs x) =
    CConCase fc (adjust um sc) (map (adjustConAlt um) xs) (map (adjust um) x)

  adjustSubExp um (CConstCase fc sc xs x) =
    CConstCase fc (adjust um sc) (map (adjustConstAlt um) xs) (map (adjust um) x)

  adjustConAlt : UsageMap -> CConAlt ns -> CConAlt ns
  adjustConAlt um (MkConAlt x y tag args z) =
    MkConAlt x y tag args $ adjust um z

  adjustConstAlt : UsageMap -> CConstAlt ns -> CConstAlt ns
  adjustConstAlt um (MkConstAlt x y) = MkConstAlt x $ adjust um y

||| Converts occurences of common subexpressions in toplevel
||| definitions to invocations of the corresponding
||| (newly introduced) zero-argument toplevel functions.
export
adjustDef : UsageMap -> CDef -> CDef
adjustDef um (MkFun args x)      = MkFun args $ adjust um x
adjustDef um d@(MkCon _ _ _)     = d
adjustDef um d@(MkForeign _ _ _) = d
adjustDef um d@(MkError _)       = d

export
cseDef :  {auto c : Ref Ctxt Defs}
       -> UsageMap
       -> Name
       -> Core (Maybe (Name, FC, CDef))
cseDef um n = do
  defs <- get Ctxt
  Just def <- lookupCtxtExact n (gamma defs) | Nothing => pure Nothing
  let Just cexpr =  compexpr def             | Nothing => pure Nothing
  pure $ Just (n, location def, adjustDef um cexpr)

export
cseNewToplevelDefs : UsageMap -> List (Name, FC, CDef)
cseNewToplevelDefs um = map toDef $ SortedMap.toList um
  where toDef : ((Integer, CExp[]),(Name,Integer)) -> (Name, FC, CDef)
        toDef ((_,exp),(nm,_)) =
          (nm, EmptyFC, MkFun [] $ adjustSubExp um exp)


text:
module Main

tarai : Int -> Int -> Int -> Int
tarai x y z = if x <= y
	then y
	else tarai (tarai (x - 1) y z) (tarai (y - 1) z x) (tarai (z - 1) x y)

main : JS_IO ()
main = do
	putStr' $ show (tarai 11 5 0)

ext: idr


text:
module Language.LSP.CodeAction.GenerateDef

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List
import Data.List1
import Data.String
import Idris.IDEMode.CaseSplit
import Idris.Pretty
import Idris.REPL
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.Message
import Libraries.Data.List.Extra
import Libraries.Data.PosMap
import Libraries.Text.PrettyPrint.Prettyprinter
import Server.Configuration
import Server.Response
import Server.Utils
import System.File
import Server.Log
import System.Clock
import TTImp.Interactive.GenerateDef
import TTImp.TTImp
import TTImp.Interactive.ExprSearch
import Parser.Unlit

printClause : Ref Ctxt Defs
           => Ref Syn SyntaxInfo
           => Maybe String -> Nat -> ImpClause -> Core String
printClause l i (PatClause _ lhsraw rhsraw) = do
  lhs <- pterm lhsraw
  rhs <- pterm rhsraw
  pure (relit l (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs))
printClause l i (WithClause _ lhsraw wvraw prf flags csraw) = do
  lhs <- pterm lhsraw
  wval <- pterm wvraw
  cs <- traverse (printClause l (i + 2)) csraw
  pure (relit l ((pack (replicate i ' ')
         ++ show lhs
         ++ " with (" ++ show wval ++ ")"
         ++ maybe "" (\ nm => " proof " ++ show nm) prf
         ++ "\n"))
         ++ showSep "\n" cs)
printClause l i (ImpossibleClause _ lhsraw) = do
  do lhs <- pterm lhsraw
     pure (relit l (pack (replicate i ' ') ++ show lhs ++ " impossible"))

number : Nat -> List a -> List (Nat, a)
number n [] = []
number n (x :: xs) = (n,x) :: number (S n) xs

pred : Nat -> Nat
pred Z     = Z
pred (S k) = k

-- This is needed as PosMap is not smart enough yet to track down
-- the non applied functions in the PosMap. This requires a change
-- in the compiler, for that reason the generateDef functionality
-- needs to have a backup strategy for names. If the PosMap
-- creation of the compiler changes probably this functions
-- will be rendered as reduntant one.
guessName : Ref MD Metadata
         => (Int, Int) -> Core (Maybe Name)
guessName (line, col) = do
  meta <- get MD
  let Nothing = findPointInTree (line, col) (nameLocMap meta)
      | Just name => pure (Just name)
  Nothing <- findTypeAt $ anyAt $ within (line, col)
      | Just (name, _, _) => pure (Just name)
  pure Nothing

export
generateDef : Ref LSPConf LSPConfiguration
            => Ref MD Metadata
            => Ref Ctxt Defs
            => Ref UST UState
            => Ref Syn SyntaxInfo
            => Ref ROpts REPLOpts
            => CodeActionParams -> Core (List CodeAction)
generateDef params = do
  defs <- branch
  let True = params.range.start.line == params.range.end.line
      | _ => do
        logString Debug "generateDef: start and end lines were different."
        pure []

  [] <- searchCache params.range GenerateDef
    | actions => do logString Debug "generateDef: found cached action"
                    pure actions

  let line = params.range.start.line
  let col = params.range.start.character

  defs <- get Ctxt
  Just (_, n, _, _) <- findTyDeclAt (\p, n => onLine line p)
    | Nothing => do logString Debug "generateDef: couldn't find type declaration at line \{show line}"
                    pure []

  fuel <- gets LSPConf searchLimit
  solutions <- case !(lookupDefExact n defs.gamma) of
    Just None => do
       catch (do searchdefs@((fc, _) :: _) <- makeDefN (\p, n => onLine line p) fuel n
                   | _ => pure []
                 let l : Nat = integerToNat $ cast $ startCol (toNonEmptyFC fc)
                 Just srcLine <- getSourceLine (line + 1)
                   | Nothing => do logString Error "generateDef: source line \{show line} not found"
                                   pure []
                 let (markM, srcLineUnlit) = isLitLine srcLine
                 for searchdefs $ \(_, cs) => do
                   traverse (printClause markM l) cs)
             (\case Timeout _ => pure []
                    err => do logString Debug "generateDef: unexpected error while searching"
                              throw err)
    Just _ => do logString Debug "generateDef: there is already a definition for \{show n}"
                 pure []
    Nothing => do logString Debug "generateDef: couldn't find type declaration at line \{show line}"
                  pure []

  put Ctxt defs

  let docURI = params.textDocument.uri
  let rng = MkRange (MkPosition (line + 1) 0) (MkPosition (line + 1) 0) -- insert

  actions <- for (number 1 solutions) $ \(i,funcDef) => do
    let lastLine = fromMaybe "" (last' funcDef)
    let edit = MkTextEdit rng (String.unlines funcDef ++ "\n") -- extra newline
    let workspaceEdit = MkWorkspaceEdit
          { changes           = Just (singleton docURI [edit])
          , documentChanges   = Nothing
          , changeAnnotations = Nothing
          }
    pure $ MkCodeAction
      { title = "Generate definition #\{show i} as ~ \{strSubstr 0 50 lastLine} ..."
      , kind        = Just RefactorRewrite
      , diagnostics = Just []
      , isPreferred = Just False
      , disabled    = Nothing
      , edit        = Just workspaceEdit
      , command     = Nothing
      , data_       = Nothing
      }
  -- TODO: retrieve the line length efficiently
  modify LSPConf (record { cachedActions $= insert (MkRange (MkPosition line 0) (MkPosition line 1000), GenerateDef, actions) })
  pure actions


text:
module Network.TLS.Core

import Crypto.Curve
import Crypto.Curve.Weierstrass
import Crypto.Curve.XCurves
import Crypto.ECDH
import Network.TLS.HKDF
import Network.TLS.AEAD
import Network.TLS.Signature
import Crypto.Hash
import Crypto.Hash.OID
import Crypto.Random
import Crypto.RSA
import Data.Bits
import Data.List
import Data.List1
import Data.Vect
import Data.DPair
import Network.Socket
import Network.TLS.Record
import Utils.Bytes
import Utils.Misc
import Utils.Parser
import Control.Monad.Error.Either

hash_to_digest : Hash algo -> Digest algo
hash_to_digest = %search

||| All the implemented TLS 1.3 cipher suites
public export
tls13_supported_cipher_suites : List1 CipherSuite
tls13_supported_cipher_suites =
  TLS_AES_128_GCM_SHA256 ::: [ TLS_AES_256_GCM_SHA384, TLS_CHACHA20_POLY1305_SHA256 ]

||| All the implemented TLS 1.2 cipher suites
public export
tls12_supported_cipher_suites : List1 CipherSuite
tls12_supported_cipher_suites =
  TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 :::
  [ TLS_ECDHE_ECDSA_WITH_AES_128_GCM_SHA256
  , TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384
  , TLS_ECDHE_ECDSA_WITH_AES_256_GCM_SHA384
  , TLS_ECDHE_RSA_WITH_CHACHA20_POLY1305_SHA256
  , TLS_ECDHE_ECDSA_WITH_CHACHA20_POLY1305_SHA256 ]

||| All the implemented groups for key exchange
public export
supported_groups : List1 SupportedGroup
supported_groups = X25519 ::: [SECP256r1, X448, SECP384r1, SECP521r1]

||| All the implemented signature algorithms for handshake verification
public export
supported_signature_algorithms : List1 SignatureAlgorithm
supported_signature_algorithms =
  RSA_PKCS1_SHA256 :::
  [ RSA_PKCS1_SHA384
  , RSA_PKCS1_SHA512
  , ECDSA_SECP256r1_SHA256
  , ECDSA_SECP384r1_SHA384
  , ECDSA_SECP521r1_SHA512
  , RSA_PSS_RSAE_SHA256
  , RSA_PSS_RSAE_SHA384
  , RSA_PSS_RSAE_SHA512
  ]

rsa_pss_params : (algo : _) -> (h : Hash algo) => SignatureParameter
rsa_pss_params algo = RSA_PSS (algo ** h) (digest_nbyte {algo}) (mgf1 {algo})

export
sig_alg_get_params : SignatureAlgorithm -> SignatureParameter
sig_alg_get_params RSA_PKCS1_SHA256 = RSA_PKCSv15 (MkDPair Sha256 %search)
sig_alg_get_params RSA_PKCS1_SHA384 = RSA_PKCSv15 (MkDPair Sha384 %search)
sig_alg_get_params RSA_PKCS1_SHA512 = RSA_PKCSv15 (MkDPair Sha512 %search)
sig_alg_get_params ECDSA_SECP256r1_SHA256 = ECDSA (MkDPair Sha256 %search)
sig_alg_get_params ECDSA_SECP384r1_SHA384 = ECDSA (MkDPair Sha384 %search)
sig_alg_get_params ECDSA_SECP521r1_SHA512 = ECDSA (MkDPair Sha512 %search)
sig_alg_get_params RSA_PSS_RSAE_SHA256 = rsa_pss_params Sha256
sig_alg_get_params RSA_PSS_RSAE_SHA384 = rsa_pss_params Sha384
sig_alg_get_params RSA_PSS_RSAE_SHA512 = rsa_pss_params Sha512

||| Get the server's TLS version from the ServerHello record
||| Since TLS 1.3 records are masqueraded as TLS 1.2 records
||| Using (.version) directly may not yield the current result
||| This function checks for the SupportedVersions extension
||| If there is one, the version specified in the extension will
||| be used, otherwise, returns the specified version in the main body
public export
get_server_version : ServerHello -> TLSVersion
get_server_version hello = go hello.extensions
  where
  go : List (DPair _ ServerExtension) -> TLSVersion
  go [] = hello.version
  go ((SupportedVersions ** (SupportedVersions version)) :: xs) = version
  go (x :: xs) = go xs

||| Get the server's handshake public key for key exchange
public export
get_server_handshake_key : ServerHello -> Either String (SupportedGroup, List Bits8)
get_server_handshake_key hello = go hello.extensions
  where
  go : List (DPair _ ServerExtension) -> Either String (SupportedGroup, List Bits8)
  go [] = Left "Server did not return any handshake keys"
  go ((KeyShare ** (KeyShare x)) :: xs) = Right x
  go (x :: xs) = go xs

||| A type alias for a function that will be used to verify handshake
||| It takes a Certificate record extension, containing all the certificates
||| as raw bytes, along with the certificate extensions fields, and returns a
||| public key that will be used to verify the current handshake hash digest
public export
CertificateCheck : (Type -> Type) -> Type
CertificateCheck m = Certificate -> m (Either String PublicKey)

||| The initial TLS state, before any communication with the server is made
public export
record TLSInitialState where
  constructor MkTLSInitialState
  server_hostname : String
  client_random : Vect 32 Bits8
  session_id : List Bits8
  cipher_suites : List1 CipherSuite
  signature_algos : List1 SignatureAlgorithm
  dh_keys : List1 (DPair SupportedGroup (\g => Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g)))

||| The TLS state after sending client hello to the server
export
record TLSClientHelloState where
  constructor MkTLSClientHelloState
  b_client_hello : List Bits8
  client_random : Vect 32 Bits8
  dh_keys : List1 (DPair SupportedGroup (\g => Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g)))

||| ADT to represent the state of certificate verification in TLS 1.3 handshake
export
data TLS3ServerHelloVerificationState : Type where
  NotVerified : TLS3ServerHelloVerificationState
  HasCertificate : Certificate -> TLS3ServerHelloVerificationState
  Verified : TLS3ServerHelloVerificationState

||| The TLS state after receiving server hello from a TLS 1.3 server
export
data TLS3ServerHelloState : (aead : Type) -> AEAD aead -> (algo : Type) -> Hash algo -> Type where
  MkTLS3ServerHelloState : TLS3ServerHelloVerificationState -> (a' : AEAD a) -> (h' : Hash h) -> h ->
                           HandshakeKeys (fixed_iv_length {a=a}) (enc_key_length {a=a}) -> Nat -> TLS3ServerHelloState a a' h h'

||| The TLS state when communication over TLS 1.3 is ready
export
data TLS3ApplicationState : (aead : Type) -> AEAD aead -> Type where
  MkTLS3ApplicationState : (a' : AEAD a) -> ApplicationKeys (fixed_iv_length {a=a}) (enc_key_length {a=a}) -> Nat -> Nat -> TLS3ApplicationState a a'

||| The TLS state after receiving server hello from a TLS 1.2 server
export
record TLS2ServerHelloState algo where
  constructor MkTLS2ServerHelloState
  client_random : Vect 32 Bits8
  server_random : Vect 32 Bits8
  cipher_suite  : CipherSuite
  dh_keys : List1 (DPair SupportedGroup (\g => Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g)))
  digest_wit : Hash algo
  digest_state : algo

||| The TLS state after receiving server certificate from a TLS 1.2 server
export
record TLS2ServerCertificateState algo where
  constructor MkTLS2ServerCertificateState
  server_hello : TLS2ServerHelloState algo
  certificate : Certificate
  cipher_suite : CipherSuite
  dh_keys : List1 (DPair SupportedGroup (\g => Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g)))
  digest_wit : Hash algo
  digest_state : algo

||| The TLS state after receiving server key exchange from a TLS 1.2 server
export
data TLS2ServerKEXState : (aead : Type) -> AEAD aead -> (algo : Type) -> Hash algo -> Type where
  MkTLS2ServerKEXState : (a' : AEAD a) -> (h' : Hash h) -> h -> Nat -> List Bits8 ->
                         (Application2Keys (fixed_iv_length @{a'}) (enc_key_length @{a'}) (mac_key_length @{a'})) ->
                         TLS2ServerKEXState a a' h h'

||| The TLS state after receiving server key exchange done from a TLS 1.2 server
export
record TLS2ServerKEXDoneState a b c d where
  constructor MkTLS2ServerKEXDoneState
  kex_state : TLS2ServerKEXState a b c d

||| The TLS state after receiving change cipher spec done from a TLS 1.2 server
||| This indicates the server will now begin communicating over an encrypted channel,
||| and that the server is ready to receive application data from the client
export
record TLS2AppReadyState a b c d where
  constructor MkTLS2AppReadyState
  kex_state : TLS2ServerKEXState a b c d

||| The TLS state when communication over TLS 1.2 is ready
export
data TLS2ApplicationState : (aead : Type) -> AEAD aead -> Type where
  MkTLS2ApplicationState : (a' : AEAD a) -> Application2Keys (fixed_iv_length {a=a}) (enc_key_length {a=a}) (mac_key_length @{a'}) -> Nat -> Nat ->
                           TLS2ApplicationState a a'

public export
data TLSStep : Type where
  Init : TLSStep
  ClientHello : TLSStep
  ServerHello2 : TLSStep
  ServerHello3 : TLSStep
  Application3 : TLSStep
  ServerCert2 : TLSStep
  ServerKEX2 : TLSStep
  ServerKEXDone2 : TLSStep
  AppReady2 : TLSStep
  Application2 : TLSStep

public export
data TLSState : TLSStep -> Type where
  TLS_Init : TLSInitialState -> TLSState Init
  TLS_ClientHello : TLSClientHelloState -> TLSState ClientHello
  TLS3_ServerHello : TLS3ServerHelloState a b algo d -> TLSState ServerHello3
  TLS3_Application : TLS3ApplicationState a b -> TLSState Application3
  TLS2_ServerHello : TLS2ServerHelloState algo -> TLSState ServerHello2
  TLS2_ServerCertificate : TLS2ServerCertificateState algo -> TLSState ServerCert2
  TLS2_ServerKEX : TLS2ServerKEXState a b algo d -> TLSState ServerKEX2
  TLS2_ServerKEXDone : TLS2ServerKEXDoneState a b algo d -> TLSState ServerKEXDone2
  TLS2_AppReady : TLS2AppReadyState a b algo d -> TLSState AppReady2
  TLS2_Application : TLS2ApplicationState a b -> TLSState Application2

encode_public_keys : (g : SupportedGroup) -> Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g) ->
                     (SupportedGroup, List Bits8)
encode_public_keys group (sk, pk) = (group, serialize_pk @{snd $ curve_group_to_type group} pk)

||| Given the server supported key exchange group, server's public key as raw byte,
||| find the matching private key in our local list and perform a key exchange
key_exchange : (group : SupportedGroup) ->
               List Bits8 ->
               List (DPair SupportedGroup (\g => Pair (curve_group_to_scalar_type g) (curve_group_to_element_type g))) ->
               Maybe (List Bits8)
key_exchange group pk [] = Nothing
key_exchange group pk ((group' ** (sk, _)) :: xs) =
  if group == group'
    then deserialize_then_dh @{snd $ curve_group_to_type group'} sk pk
    else key_exchange group pk xs

||| Parse a TLS record
parse_record : List Bits8 ->
               (Parserializer Bits8 (List (Posed Bits8)) (SimpleError String) (Either (AlertLevel, AlertDescription) (TLSVersion, DPair _ Record))) ->
               Either String (DPair _ Record)
parse_record b_input parser = do
  let (Pure [] $ Right (TLS12, record')) = feed (map (uncurry MkPosed) $ enumerate Z b_input) parser.decode
  | (Pure [] $ Right (tlsver, _)) => Left $ "Unsupported TLS version: " <+> show tlsver
  | (Pure [] $ Left (_, alert)) => Left $ "TLS alert: " <+> show alert
  | (Pure leftover _) => Left $ "Parsing error: overfed, leftover: " <+> xxd (map get leftover)
  | (Fail err) => Left $ "Parsing error: " <+> show err
  | _ => Left "Parsing error: underfed"
  case record' of
    (_ ** Alert alert) => Left $ show alert
    ok => pure ok

||| Transition from TLS Init state to TLS Client Hello state,
||| and returning the payload that should be sent to the server
public export
tls_init_to_clienthello : TLSState Init -> (List Bits8, TLSState ClientHello)
tls_init_to_clienthello (TLS_Init state) =
  let client_hello_object = MkClientHello
        TLS12
        state.client_random
        state.session_id
        state.cipher_suites
        (singleton Null)
        [ (_ ** ServerName $ DNS state.server_hostname ::: [])
        , (_ ** SupportedGroups $ map fst state.dh_keys)
        , (_ ** SignatureAlgorithms state.signature_algos)
        , (_ ** KeyShare $ map (uncurry encode_public_keys) state.dh_keys)
        , (_ ** SupportedVersions $ TLS13 ::: [ TLS12 ])
        ]
      b_client_hello =
        (arecord {i = List (Posed Bits8)}).encode (TLS12, (_ ** Handshake [(_ ** ClientHello client_hello_object)]))
  in (b_client_hello, TLS_ClientHello $ MkTLSClientHelloState (drop 5 b_client_hello) state.client_random state.dh_keys)

||| Transition from TLS Client Hello to TLS Server Hello state after receiving Server Hello,
||| return the new state depending on the server's TLS version
public export
tls_clienthello_to_serverhello : TLSState ClientHello -> List Bits8 ->
                                 Either String (Either (TLSState ServerHello2) (TLSState ServerHello3))
tls_clienthello_to_serverhello (TLS_ClientHello state) b_server_hello = do
  (MkDPair _ (Handshake [MkDPair _ (ServerHello server_hello)])) <- parse_record b_server_hello alert_or_arecord
  | _ => Left $ "Parsing error: record not server_hello"
  case get_server_version server_hello of
    TLS13 => do
      let (hash_algo ** hwit) = ciphersuite_to_hash_type server_hello.cipher_suite
      let digest_state = update (drop 5 b_server_hello) $ update state.b_client_hello $ init hash_algo
      (group, pk) <- get_server_handshake_key server_hello
      shared_secret <- maybe_to_either (key_exchange group pk $ toList state.dh_keys) "server sent invalid key"
      let (aead ** awit) = ciphersuite_to_aead_type server_hello.cipher_suite
      let hk = tls13_handshake_derive hash_algo (fixed_iv_length {a=aead}) (enc_key_length {a=aead}) shared_secret $ toList $ finalize digest_state
      Right $ Right $ TLS3_ServerHello $ MkTLS3ServerHelloState NotVerified awit hwit digest_state hk Z
    TLS12 =>
      let (hash_algo ** hwit) = ciphersuite_to_prf_type server_hello.cipher_suite
          digest_state = update (drop 5 b_server_hello) $ update state.b_client_hello $ init hash_algo
      in Right
         $ Left
         $ TLS2_ServerHello
         $ MkTLS2ServerHelloState state.client_random server_hello.random server_hello.cipher_suite state.dh_keys hwit digest_state
    tlsvr => Left $ "unsupported version: " <+> show tlsvr

||| Decrypt a handshake wrapper from the server
decrypt_hs_s_wrapper : TLS3ServerHelloState aead aead' algo algo' -> Wrapper (mac_length @{aead'}) -> List Bits8 ->
                       Maybe (TLS3ServerHelloState aead aead' algo algo', List Bits8)
decrypt_hs_s_wrapper (MkTLS3ServerHelloState cert a' h' digest_state hk counter) (MkWrapper ciphertext mac_tag) record_header =
  case decrypt @{a'} hk.server_handshake_key hk.server_handshake_iv zeros zeros counter ciphertext (const record_header) $ toList mac_tag of
    (_, False) => Nothing
    (plaintext, True) => Just (MkTLS3ServerHelloState cert a' h' digest_state hk (S counter), plaintext)

list_minus : List a -> List b -> List a
list_minus a b = take (length a `minus` length b) a

-- I apologize for this mess

||| Handle state transition during handshaking when the server is sending encrypted handshake data
||| This contains encrypted extensions, server's certificate, verifying the handshake data with the certificate,
||| and also a verify token computed by hashing all the records that have be sent so far
tls3_serverhello_to_application_go : Monad m =>
                                     TLSState ServerHello3 ->
                                     List Bits8 ->
                                     CertificateCheck m ->
                                     (EitherT String m (Either (TLSState ServerHello3) (List Bits8, TLSState Application3)))
tls3_serverhello_to_application_go og [] cert_ok = pure $ Left og
tls3_serverhello_to_application_go og@(TLS3_ServerHello {algo} server_hello@(MkTLS3ServerHelloState cert a' h' d' hk c')) plaintext cert_ok =
  case feed (map (uncurry MkPosed) $ enumerate Z plaintext) handshake.decode of
    -- since we do not support any encrypted extensions, it is ignored
    Pure leftover (_ ** EncryptedExtensions x) =>
      --- pass the plaintext bytes representing the record into the digest
      let consumed = plaintext `list_minus` leftover
          new = TLS3_ServerHello $ MkTLS3ServerHelloState cert a' h' (update consumed d') hk c'
      in tls3_serverhello_to_application_go new (map get leftover) cert_ok
    -- handle the server's certificate
    Pure leftover (_ ** Certificate x) =>
      case cert of
        HasCertificate _ => throwE "Certificate was sent twice"
        Verified => throwE "Certificate was sent after verification"
        NotVerified => do
          --- pass the plaintext bytes representing the record into the digest
          let consumed = plaintext `list_minus` leftover
          let new = TLS3_ServerHello $ MkTLS3ServerHelloState (HasCertificate x) a' h' (update consumed d') hk c'
          tls3_serverhello_to_application_go new (map get leftover) cert_ok
    -- handle the server's signature of a digest of all the handshake records received so far, signed by the server's certificate
    Pure leftover (_ ** CertificateVerify x) => do
      certificate' <- case cert of
        NotVerified => throwE "CertificateVerify sent before Certificate"
        Verified => throwE "CertificateVerify sent after verification"
        HasCertificate cert => pure cert
      let verify_token =
            replicate 64 0x20 -- 64 spaces
              <+> string_to_ascii "TLS 1.3, server CertificateVerify"
              <+> [ 0x00 ] -- null
              <+> toList (finalize d')
      public_key <- MkEitherT $ cert_ok certificate'
      let Right () = verify_signature (sig_alg_get_params x.signature_algorithm) public_key verify_token x.signature
      | Left err => throwE $ "error while verifying handshake: " <+> err
      let consumed = plaintext `list_minus` leftover
      let new = TLS3_ServerHello $ MkTLS3ServerHelloState Verified a' h' (update consumed d') hk c'
      tls3_serverhello_to_application_go new (map get leftover) cert_ok
    -- handle the Finished record which contains a hash of all the handshake records received so far
    Pure [] (_ ** Finished x) =>
      case cert of
        Verified =>
          if (tls13_verify_data algo hk.server_traffic_secret $ toList $ finalize d') == verify_data x
          then
            let digest = update plaintext d'
                client_verify_data = tls13_verify_data algo hk.client_traffic_secret $ toList $ finalize digest
                client_handshake_finished =
                  to_application_data
                  $ MkWrappedRecord Handshake ((with_id no_id_finished).encode {i = List (Posed Bits8)}
                  $ Finished
                  $ MkFinished client_verify_data)
                record_length = (length client_handshake_finished) + mac_length @{a'}
                b_record = record_type_with_version_with_length.encode {i = List (Posed Bits8)} (ApplicationData, TLS12, record_length)
                (eiv, chf_encrypted, chf_mac_tag) =
                  encrypt @{a'} hk.client_handshake_key hk.client_handshake_iv zeros Z client_handshake_finished b_record
                app_key = tls13_application_derive algo hk (toList $ finalize digest)
                verify_data_wrapped = MkWrapper chf_encrypted chf_mac_tag
                b_chf_wrapped =
                  (arecord {i = List (Posed Bits8)}).encode (TLS12, MkDPair _ (ApplicationData $ to_application_data $ MkWrapper chf_encrypted chf_mac_tag))
            in pure $ Right (b_chf_wrapped, TLS3_Application $ MkTLS3ApplicationState a' app_key Z Z)
          else
            throwE "verify data does not match"
        _ => throwE "CertificateVerify was not sent"
    Fail err => throwE $ "body: " <+> xxd plaintext <+> "\nbody length: " <+> (show $ length plaintext) <+> "\nparsing error: " <+> show err
    _ => throwE "failed to parse plaintext"

||| Transition from TLS Server Hello to TLS communication ready state after receiving server's handshake data
||| note that the encrypted records containing the handshake records can be sent seperately as different records,
||| or a bunch of handshake records can be concatenated into one encrypted record
public export
tls3_serverhello_to_application : Monad m => TLSState ServerHello3 -> List Bits8 -> CertificateCheck m ->
                                              m (Either String (Either (TLSState ServerHello3) (List Bits8, TLSState Application3)))
tls3_serverhello_to_application og@(TLS3_ServerHello server_hello@(MkTLS3ServerHelloState cert a' h' d' hk c')) b_wrapper cert_ok = runEitherT $ do
  let Right (MkDPair _ (ApplicationData application_data)) = parse_record b_wrapper alert_or_arecord
  | Right (MkDPair _ (ChangeCipherSpec _)) => pure $ Left og
  | Left err => throwE err
  | _ => throwE $ "Parsing error: record not application data"
  let Just wrapper = from_application_data {mac_size = (mac_length @{a'})} application_data
  | Nothing => throwE $ "malformed wrapper:" <+> xxd application_data
  let Just (server_hello, plaintext') = decrypt_hs_s_wrapper server_hello wrapper (take 5 b_wrapper)
  | Nothing => throwE "cannot decrypt wrapper"
  let Just (plaintext, 0x16) = uncons1 <$> toList1' plaintext'
  | Just ([_, alert], 0x15) => throwE $ "alert: " <+> (show $ id_to_alert_description alert)
  | Just (plaintext, i) => throwE $ "invalid record id: " <+> show i <+> " body: " <+> xxd plaintext
  | Nothing => throwE "plaintext is empty"
  tls3_serverhello_to_application_go (TLS3_ServerHello server_hello) plaintext cert_ok

||| Decrypt an application data wrapper from the server, and returns a new TLS state
decrypt_ap_s_wrapper : TLS3ApplicationState aead aead' -> Wrapper (mac_length @{aead'}) -> List Bits8 ->
                       Maybe (TLS3ApplicationState aead aead', List Bits8)
decrypt_ap_s_wrapper (MkTLS3ApplicationState a' ak c_counter s_counter) (MkWrapper ciphertext mac_tag) record_header =
  case decrypt @{a'} ak.server_application_key ak.server_application_iv zeros zeros s_counter ciphertext (const record_header) $ toList mac_tag of
     (_, False) => Nothing
     (plaintext, True) => Just (MkTLS3ApplicationState a' ak c_counter (S s_counter), plaintext)

||| Decrypt an application wrapper from the server, and updates the TLS state
public export
decrypt_from_record : TLSState Application3 -> List Bits8 -> Either String (TLSState Application3, List Bits8)
decrypt_from_record og@(TLS3_Application app_state@(MkTLS3ApplicationState a' ak c_counter s_counter)) b_wrapper = do
  (MkDPair _ (ApplicationData application_data)) <- parse_record b_wrapper alert_or_arecord
  | _ => Left $ "Parsing error: record not application data"
  let Just wrapper = from_application_data {mac_size = (mac_length @{a'})} application_data
  | Nothing => Left $ "malformed wrapper:" <+> xxd application_data
  let Just (app_state, plaintext') = decrypt_ap_s_wrapper app_state wrapper (take 5 b_wrapper)
  | Nothing => Left "cannot decrypt wrapper"
  let Just (plaintext, 0x17) = uncons1 <$> toList1' plaintext'
  | Just (plaintext, 0x16) => Right (TLS3_Application app_state, []) -- implement session ticket in the future?
  | Just ([_, alert], 0x15) => Left $ "alert: " <+> (show $ id_to_alert_description alert)
  | Just (plaintext, i) => Left $ "invalid record id: " <+> show i <+> " body: " <+> xxd plaintext
  | Nothing => Left "plaintext is empty"
  Right (TLS3_Application app_state, plaintext)

||| Encrypt an application data wrapper to the server, and updates the TLS state
public export
encrypt_to_record : TLSState Application3 -> List Bits8 -> (TLSState Application3, List Bits8)
encrypt_to_record (TLS3_Application $ MkTLS3ApplicationState a' ak c_counter s_counter) plaintext =
  let b_application_data = to_application_data $ MkWrappedRecord ApplicationData plaintext
      record_length = (length b_application_data) + mac_length @{a'}
      b_record_header = (record_type_with_version_with_length {i = List (Posed Bits8)}).encode (ApplicationData, TLS12, record_length)
      (eiv, app_encrypted, app_mac_tag) =
        encrypt @{a'} ak.client_application_key ak.client_application_iv zeros c_counter b_application_data b_record_header
      b_app_wrapped =
        arecord.encode {i = List (Posed Bits8)} (TLS12, MkDPair _ (ApplicationData $ to_application_data $ MkWrapper app_encrypted app_mac_tag))
  in (TLS3_Application $ MkTLS3ApplicationState a' ak (S c_counter) s_counter, b_app_wrapped)

||| Transition from TLS Server Hello to TLS Certificate state after receiving server's certificate
public export
serverhello2_to_servercert : TLSState ServerHello2 -> List Bits8 -> Either String (TLSState ServerCert2)
serverhello2_to_servercert (TLS2_ServerHello server_hello) b_cert = do
  (MkDPair _ (Handshake [MkDPair _ (Certificate server_cert)])) <- parse_record b_cert alert_or_arecord2
  | _ => Left "Parsing error: record not server_hello"
  pure $ TLS2_ServerCertificate
       $ MkTLS2ServerCertificateState
           server_hello
           server_cert
           server_hello.cipher_suite
           server_hello.dh_keys
           server_hello.digest_wit
           (update @{hash_to_digest server_hello.digest_wit} (drop 5 b_cert) server_hello.digest_state)

||| Transition from TLS Server Hello to TLS Certificate state after receiving server's public key for key exchange
||| This also contains a signature of the public key signed by the server's certificate
||| The handshake verification step will be done here
public export
servercert_to_serverkex : Monad m => TLSState ServerCert2 -> List Bits8 -> CertificateCheck m -> m (Either String (TLSState ServerKEX2))
servercert_to_serverkex (TLS2_ServerCertificate server_cert) b_kex cert_ok = runEitherT $ do
  let Right (MkDPair _ (Handshake [MkDPair _ (ServerKeyExchange server_kex)])) = parse_record b_kex alert_or_arecord2
  | _ => throwE "Parsing error: record not server_hello"
  let Just shared_secret = key_exchange (server_kex.server_pk_group) (server_kex.server_pk_body) (toList server_cert.dh_keys)
  | Nothing => throwE "cannot parse server public key"
  let (aead ** awit) = ciphersuite_to_aead_type server_cert.cipher_suite
  let app_key =
        tls12_application_derive server_cert.digest_wit
          (fixed_iv_length {a=aead})
          (enc_key_length {a=aead})
          (mac_key_length {a=aead})
          shared_secret
          (toList server_cert.server_hello.client_random)
          (toList server_cert.server_hello.server_random)
  let Just (_, chosen_pk) = find (\(g,_) => g == server_kex.server_pk_group) $ toList $ map (uncurry encode_public_keys) server_cert.dh_keys
  | Nothing => throwE "cannot find public key that match the server's"
  let (curve_info_a, curve_info_b) = supported_group_to_id server_kex.server_pk_group
  let verify_token =
        toList server_cert.server_hello.client_random
        <+> toList server_cert.server_hello.server_random
        <+> [ 0x03, curve_info_a, curve_info_b, cast (length server_kex.server_pk_body) ] -- 0x03 hard coded, value for "named curve"
        <+> server_kex.server_pk_body
  public_key <- MkEitherT $ cert_ok server_cert.certificate
  let Right () = verify_signature (sig_alg_get_params server_kex.signature_algo) public_key verify_token server_kex.signature_body
  | Left err => throwE $ "error while verifying handshake: " <+> err
  pure $ TLS2_ServerKEX
       $ MkTLS2ServerKEXState
           awit
           server_cert.digest_wit
           (update @{hash_to_digest server_cert.digest_wit} (drop 5 b_kex) server_cert.digest_state)
           (ciphersuite_to_verify_data_len server_cert.cipher_suite)
           chosen_pk
           app_key

||| Encrypt a wrapper to the server
encrypt_to_wrapper2 : AEAD a => Vect (enc_key_length {a=a}) Bits8 -> Vect (fixed_iv_length {a=a}) Bits8 -> Vect (mac_key_length {a=a}) Bits8 ->
                      List Bits8 -> RecordType -> Nat -> List Bits8
encrypt_to_wrapper2 key iv mac_key plaintext record_id sequence =
  let aad =
        (toList $ to_be {n=8} (cast {to=Bits64} sequence))
        <+> [record_type_to_id record_id, 0x03, 0x03] -- 0x03 0x03 is the byte representation of TLS 1.2
        <+> (toList $ to_be {n=2} (cast {to=Bits16} $ length plaintext))
      (eiv, ciphertext, mac) = encrypt key iv mac_key sequence plaintext aad
      wrapper = MkWrapper2 eiv ciphertext mac
      b_wrapper = (wrapper2 {i = List (Posed Bits8)}).encode (record_id, TLS12, wrapper)
  in b_wrapper

||| Transition from TLS Key Exchange to TLS Hello Done state after receiving server hello done
||| Also returns a payload to be sent to the server
public export
serverkex_process_serverhellodone : TLSState ServerKEX2 -> List Bits8 -> Either String (TLSState ServerKEXDone2, List Bits8)
serverkex_process_serverhellodone og@(TLS2_ServerKEX (MkTLS2ServerKEXState a' h' digest_state vdlen chosen_pk app_key)) b_hello_done = do
  (MkDPair _ (Handshake [MkDPair _ (ServerHelloDone _)])) <- parse_record b_hello_done alert_or_arecord2
  | _ => Left $ "Parsing error: record not server_hello"
  let b_client_kex =
        (arecord {i = List (Posed Bits8)}).encode (TLS12, (_ ** Handshake [(_ ** ClientKeyExchange $ MkClientKeyExchange chosen_pk)]))
  let b_client_change_cipher_spec =
        (arecord {i = List (Posed Bits8)}).encode (TLS12, (_ ** ChangeCipherSpec [0x01]))
  let digest_state =
        update (drop 5 b_client_kex) $ update (drop 5 b_hello_done) digest_state
  let client_verify_data = (with_id no_id_finished).encode {i = List (Posed Bits8)}
        $ Finished
        $ MkFinished
        $ toList
        (tls12_client_verify_data h' vdlen (toList app_key.master_secret) (toList $ finalize digest_state))
  let b_client_verify_data =
        encrypt_to_wrapper2 app_key.client_application_key app_key.client_application_iv app_key.client_mac_key client_verify_data Handshake Z
  let digest_state =
        update client_verify_data digest_state
  Right (TLS2_ServerKEXDone $ MkTLS2ServerKEXDoneState $ MkTLS2ServerKEXState a' h' digest_state vdlen chosen_pk app_key
        , b_client_kex <+> b_client_change_cipher_spec <+> b_client_verify_data)

||| Transition from TLS Hello Done to TLS server application ready state after receiving change cipher spec
public export
serverhellodone_to_applicationready2 : TLSState ServerKEXDone2 -> List Bits8 -> Either String (TLSState AppReady2)
serverhellodone_to_applicationready2 (TLS2_ServerKEXDone state) b_changecipherspec = do
  (MkDPair _ (ChangeCipherSpec _)) <- parse_record b_changecipherspec alert_or_arecord2
  | _ => Left $ "Parsing error: record not ChangeCipherSpec"
  pure $ TLS2_AppReady $ MkTLS2AppReadyState state.kex_state

||| Parse a TLS 1.2 encrypted wrapper
parse_tls12_wrapper : AEAD a => RecordType -> List Bits8 -> Either String (Wrapper2 (record_iv_length {a=a}) (mac_length {a=a}))
parse_tls12_wrapper recordtype b_input = do
  let (Pure [] (recordtype', TLS12, record')) = feed (map (uncurry MkPosed) $ enumerate Z b_input) (wrapper2 {i = List (Posed Bits8)}).decode
  | (Pure [] (_, tlsver, _)) => Left $ "Unsupported TLS version: " <+> show tlsver
  | (Pure leftover _) => Left $ "Parsing error: overfed, leftover: " <+> xxd (map get leftover)
  | (Fail err) => Left $ "Parsing error: " <+> show err
  | _ => Left "Parsing error: underfed"
  if recordtype == recordtype'
     then pure record'
     else Left $ "expected record type: " <+> show recordtype <+> ", but got: " <+> show recordtype'

||| Decrypt a TLS 1.2 encrypted wrapper from the server
decrypt_from_wrapper2 : AEAD a =>
                        Nat ->
                        RecordType ->
                        Wrapper2 (record_iv_length {a=a}) (mac_length {a=a}) ->
                        Vect (fixed_iv_length {a=a}) Bits8 ->
                        Vect (enc_key_length {a=a}) Bits8 ->
                        Vect (mac_key_length {a=a}) Bits8 ->
                        Either String (List Bits8)
decrypt_from_wrapper2 sequence record_type wrapper iv key mac_key =
  let aadf = (\plaintext =>
        (toList $ to_be {n=8} (cast {to=Bits64} sequence))
        <+> [record_type_to_id record_type, 0x03, 0x03] -- 0x03 0x03 is the byte representation of TLS 1.2
        <+> (toList $ to_be {n=2} (cast {to=Bits16} $ length plaintext)))
      (plaintext, ok) = decrypt key iv wrapper.iv_data mac_key sequence wrapper.encrypted_data aadf (toList wrapper.auth_tag)
  in if ok then Right $ plaintext else Left "cannot decrypt wrapper"

||| Transition from TLS server application ready state to TLS communication ready state after receiving handshake finished from server
public export
applicationready2_to_application2 : TLSState AppReady2 -> List Bits8 -> Either String (TLSState Application2)
applicationready2_to_application2 (TLS2_AppReady state) b_verifydata = do
  let (MkTLS2ServerKEXState a' h' digest_state vdlen chosen_pk app_key) = state.kex_state
  wrapper <- parse_tls12_wrapper @{a'} Handshake b_verifydata
  plaintext <-
    decrypt_from_wrapper2 Z Handshake wrapper app_key.server_application_iv app_key.server_application_key app_key.server_mac_key
  let result = feed (map (uncurry MkPosed) $ enumerate Z plaintext) $ (with_id no_id_finished).decode {i = List (Posed Bits8)}
  let (Pure [] (Finished $ MkFinished verify_data')) = result
  | _ => Left $ "Parsing error: decrypted record not Finished"
  let verify_data = tls12_server_verify_data h' vdlen (toList app_key.master_secret) (toList $ finalize digest_state)
  maybe_to_either (guard $ toList verify_data `s_eq'` toList verify_data') "Verify data not match"
  pure $ TLS2_Application $ MkTLS2ApplicationState a' app_key 1 1

||| Encrypt data into TLS payload to be sent to the server
public export
encrypt_to_record2 : TLSState Application2 -> List Bits8 -> (TLSState Application2, List Bits8)
encrypt_to_record2 (TLS2_Application $ MkTLS2ApplicationState a' ak c_counter s_counter) plaintext =
   let b_wrapper = encrypt_to_wrapper2 ak.client_application_key ak.client_application_iv ak.client_mac_key plaintext ApplicationData c_counter
   in (TLS2_Application $ MkTLS2ApplicationState a' ak (S c_counter) s_counter, b_wrapper)

||| Decrypt TLS payload into data from the server
public export
decrypt_from_record2 : TLSState Application2 -> List Bits8 -> Either String (TLSState Application2, List Bits8)
decrypt_from_record2 (TLS2_Application $ MkTLS2ApplicationState a' ak c_counter s_counter) ciphertext = do
  wrapper <- parse_tls12_wrapper @{a'} ApplicationData ciphertext
  plaintext <- decrypt_from_wrapper2 s_counter ApplicationData wrapper ak.server_application_iv ak.server_application_key ak.server_mac_key
  Right (TLS2_Application $ MkTLS2ApplicationState a' ak c_counter (S s_counter), plaintext)


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

import System.File

data BingoNum = M Nat | U Nat

Card : Type
Card = List (List BingoNum)

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

getNumbers : List String -> Maybe (List Nat, List String)
getNumbers [] = Nothing
getNumbers (x :: xs) = Just (catMaybes $ parsePositive <$> (forget $ split (== ',') x),  xs)

parseCard : List String -> Card
parseCard l = (\s => U <$> (catMaybes $ parsePositive <$> (forget $ split (== ' ') s))) <$> l

parseCards : List String -> List Card
parseCards [] = []
parseCards (_ :: xs) = parseCard (take 5 xs) :: parseCards (drop 5 xs)

isMarked : BingoNum -> Bool
isMarked (M _) = True
isMarked (U _) = False

winRow : Card -> Bool
winRow [] = False
winRow (x :: xs) = all isMarked x || winRow xs

winColumn : Card -> Bool
winColumn c = any id $ foldl (\a => \bs => (\(b1, b2) => b1 && b2) <$> zip a (isMarked <$> bs)) (replicate 5 True) c

wins : List Card -> Maybe Card
wins [] = Nothing
wins (c :: cs) = if winRow c || winColumn c
                    then Just c
                    else wins cs

drawNumber : Nat -> Card -> Card
drawNumber n [] = []
drawNumber n (x :: xs) = ((\d => case d of
                                      M m => M m
                                      U u => if u == n
                                                then M u
                                                else U u) <$> x) :: drawNumber n xs

drawNumbers : List Nat -> List Card -> Maybe (Card, Nat)
drawNumbers [] cs = Nothing
drawNumbers (x :: xs) cs = let ncs = drawNumber x <$> cs in
                               case wins ncs of
                                    Just c => Just (c, x)
                                    Nothing => drawNumbers xs ncs

scoreOf : Card -> Nat
scoreOf [] = 0
scoreOf (x :: xs) = (foldl (\a => \b => case b of
                                             M n => a
                                             U n => n + a) 0 x) + scoreOf xs

run : String -> IO ()
run s = do let lines = lines s
           Just (ns, lines) <- pure $ getNumbers lines
             | Nothing => putStrLn $ "err"
           let cards = parseCards lines
           Just (win, n) <- pure $ drawNumbers ns cards
             | Nothing => putStrLn $ "no win"
           let score = n * scoreOf win
           putStrLn $ show $ score

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


text:
module ZZUtils
import ZZ
import NatUtils
%access public export
%default total

data IsNonNegative : ZZ->Type where
 NonNegative :(IsNonNegative (Pos k))

data NotBothZeroZ :ZZ->ZZ->Type where
  LeftPositive :NotBothZeroZ (Pos (S k)) m
  LeftNegative :NotBothZeroZ (NegS k) m
  RightPositive :NotBothZeroZ m (Pos (S k))
  RightNegative :NotBothZeroZ m (NegS k)

data NotZero:ZZ->Type where
  PositiveZ:NotZero (Pos (S k))
  NegativeZ:NotZero (NegS k)

data IsNegative:ZZ->Type where
  Negative: IsNegative (NegS k)

|||Zero is not positive
zeroNotPos:IsPositive (Pos Z)->Void
zeroNotPos Positive impossible

|||Proof that NotBothZeroZ 0 0 is uninhabited
zeroZeroBothZero:NotBothZeroZ (Pos Z) (Pos Z) ->Void
zeroZeroBothZero LeftPositive impossible
zeroZeroBothZero LeftNegative impossible
zeroZeroBothZero RightPositive impossible
zeroZeroBothZero RightNegative impossible

|||Decides whther two numbers are not both zero or not.
decNotBothZero : (a:ZZ)->(b:ZZ)->Dec (NotBothZeroZ a b)
decNotBothZero (Pos Z) (Pos Z) = No ( zeroZeroBothZero)
decNotBothZero (Pos Z) (Pos (S k)) = Yes RightPositive
decNotBothZero (Pos Z) (NegS k) = Yes RightNegative
decNotBothZero (Pos (S k)) b = Yes LeftPositive
decNotBothZero (NegS k) b = Yes LeftNegative

|||Checks 2 numbers and produces a proof of either (a=0,b=0) or (NotBothZeroZ a b)
checkNotBothZero : (a:ZZ)->(b:ZZ)->Either ((a=0),(b=0)) (NotBothZeroZ a b)
checkNotBothZero (Pos Z) (Pos Z) = Left (Refl, Refl)
checkNotBothZero (Pos Z) (Pos (S k)) = Right RightPositive
checkNotBothZero (Pos Z) (NegS k) = Right RightNegative
checkNotBothZero (Pos (S k)) b = Right LeftPositive
checkNotBothZero (NegS k) b = Right LeftNegative

|||Proof that positive numbers are not zero
posThenNotZero:{a:ZZ}->(IsPositive a)->(NotZero a)
posThenNotZero {a = (Pos (S k))} Positive = PositiveZ

NegSThenNotZero:{a:ZZ}->(IsNegative a)->(NotZero a)
NegSThenNotZero {a = (NegS k)} ZZUtils.Negative = NegativeZ

|||Rewrites a=b as a=1*b
rewriteRightAsOneTimesRight: {a:ZZ}->{b:ZZ}->(a=b)->(a=(1*b))
rewriteRightAsOneTimesRight {a}{b}prf = rewrite ( (multOneLeftNeutralZ b)) in prf
|||Rewrites a=b as 1*a=b
rewriteLeftAsOneTimesLeft: {a:ZZ}->{b:ZZ}->(a=b)->(1*a=b)
rewriteLeftAsOneTimesLeft {a}{b}prf = rewrite ( (multOneLeftNeutralZ a)) in prf
|||Rewrites 1*a = b as a=b
rewriteOneTimesLeftAsLeft:{a:ZZ}->{b:ZZ}->((1*a) = b)->(a=b)
rewriteOneTimesLeftAsLeft {a}{b}prf  =
  rewrite ( sym $(multOneLeftNeutralZ a)) in prf
|||Rewrites   (a*1)=b as a=b
rewriteLeftTimesOneAsLeft : {a:ZZ}->{b:ZZ}->((a*1)=b)->(a=b)
rewriteLeftTimesOneAsLeft {a}{b}prf =
  rewrite ( sym $(multOneRightNeutralZ a)) in prf

|||Proof that negative integers are not non negative
negsAreNotNonNegs:(IsNonNegative (NegS k))->Void
negsAreNotNonNegs NonNegative impossible
|||A function that checks whether an integer is non negative and returns a
|||proof or a contradiction
decideIsNonNeg:(a: ZZ) -> Dec (IsNonNegative   a)
decideIsNonNeg (Pos k) = Yes NonNegative
decideIsNonNeg (NegS k) = No (negsAreNotNonNegs)
|||Proof that natural numbers are non negative
naturalsNonNegative: (x:Nat)->IsNonNegative (Pos x)
naturalsNonNegative x = NonNegative

|||The less than type for ZZ
LTZ :ZZ->ZZ->Type
LTZ a b = LTEZ (1+a) b

|||Theorem that if a and b are natural numbers and a<b
|||then, (Pos a) <(Pos b)
ltNatToZZ:{a:Nat}->{b:Nat}->(LT a b)->(LTZ (Pos a) (Pos b))
ltNatToZZ (LTESucc x) = PositiveLTE (LTESucc x)
|||Proves that a<= a for any integer a
lteReflZ:{a:ZZ}->LTEZ a a
lteReflZ {a =(Pos k)} = PositiveLTE (lteRefl {n=k})
lteReflZ {a= (NegS k)} = NegativeLte (lteRefl {n=k})
|||Proof that a number is less than its successor
numLtSucc:(a:ZZ)->LTZ a (1+a)
numLtSucc a = lteReflZ
|||Proof that one is not less than zero
oneNotLTEZero:(LTEZ (Pos (S Z)) (Pos Z))->Void
oneNotLTEZero (PositiveLTE LTEZero) impossible
oneNotLTEZero (PositiveLTE (LTESucc _)) impossible
|||Proof that a number greater than or equal to 1 is positive
gteOnePositive:(a:ZZ)->(LTEZ 1 a)->(IsPositive a)
gteOnePositive (Pos Z) (PositiveLTE LTEZero) impossible
gteOnePositive (Pos Z) (PositiveLTE (LTESucc _)) impossible
gteOnePositive (Pos (S k)) x = Positive
gteOnePositive (NegS _) (PositiveLTE _) impossible
gteOnePositive (NegS _) NegLessPositive impossible
gteOnePositive (NegS _) (NegativeLte _) impossible

|||Proof that it is impossible that (1+a)<=a
succNotLteNumZ:(a:ZZ)->(LTEZ (1+a) a) ->Void
succNotLteNumZ (Pos k)  y =
  impliesContrapositive (LTEZ (Pos (S k)) (Pos k)) (LTE (S k) k)
    LTEZZtoNat  (succNotLTEnum k) y
succNotLteNumZ (NegS Z)  (PositiveLTE _)  impossible
succNotLteNumZ (NegS Z)  NegLessPositive  impossible
succNotLteNumZ (NegS Z)  (NegativeLte _)  impossible
succNotLteNumZ (NegS (S k))  y  =
  impliesContrapositive (LTEZ (NegS k) (NegS (S k))) (LTE (S k) k)
     LTEZZtoNatNeg (succNotLTEnum k) y

|||Multiplying positive numbers gives a positive number.
posMultPosIsPos: (IsPositive m)->(IsPositive d)->(IsPositive (m*d))
posMultPosIsPos{m = (Pos (S k))}{d = (Pos (S j))} Positive Positive = Positive
|||The theorem that (-a)*(-b)=a*b
negateMultNegateNeutralZ: {a:ZZ}->{b:ZZ}->((-a)*(-b)=a*b)
negateMultNegateNeutralZ{a}{b} =
  rewrite (multNegateRightZ (-a) b) in
  rewrite (multNegateLeftZ a b ) in
  rewrite (doubleNegElim (a*b)) in Refl
|||Proof that zero times an integer is not positive
posIsNotZeroTimesInteger:((Pos (S k))=(Pos Z)*a)->Void
posIsNotZeroTimesInteger{a = (Pos _)} Refl impossible
posIsNotZeroTimesInteger{a = (NegS _)} Refl impossible
|||Proof that Zero times an integer is not negative
negSIsNotZeroTimesInteger :((NegS k)=(Pos Z)*a)->Void
negSIsNotZeroTimesInteger {a = (Pos _)} Refl impossible
negSIsNotZeroTimesInteger {a = (NegS _)} Refl impossible
|||Converts a nonNegative integer into the corresponding Natural number
nonNegIntegerToNat:(a:ZZ)->(IsNonNegative a)->Nat
nonNegIntegerToNat (Pos k) NonNegative = k
|||Proof that a positive number is not zero times a negative number
zeroTimesNegIsNotPos:(Pos (S k)) = (Pos Z)*(NegS j)->Void
zeroTimesNegIsNotPos Refl impossible
|||Proof that a positive number is not a negative number times zero
negTimesZeroIsNotPos :(Pos (S k)) = (NegS j)*(Pos Z)->Void
negTimesZeroIsNotPos {k}{j}prf =
  zeroTimesNegIsNotPos{k=k}{j=j}
     (rewrite (sym(multCommutativeZ (NegS j) (Pos Z))) in prf)

|||Lemma that (c*d)*n = (c*n)*d
multCommuAndAssocZ1: {c:ZZ}->{d:ZZ}->{n:ZZ}->(c*d)*n = (c*n)*d
multCommuAndAssocZ1 {c}{d}{n}= rewrite (sym(multAssociativeZ c n d)) in
                           rewrite (multCommutativeZ n d ) in
                           rewrite( (multAssociativeZ c d n))in
                           Refl

|||Proof that if (a*b=1) then either (a=1,b=1)  or (a=-1,b=-1)
productOneThenNumbersOne: (a:ZZ)->(b:ZZ)->(a*b=1) ->Either (a=1,b=1) (a=(-1),b=(-1))
productOneThenNumbersOne (Pos Z) (Pos _) Refl impossible
productOneThenNumbersOne (Pos Z) (NegS _) Refl impossible
productOneThenNumbersOne (Pos (S Z)) (Pos Z) prf = void (posIsNotPosMultZero {k=Z} (sym prf))
productOneThenNumbersOne (Pos (S Z)) (Pos (S Z)) prf = Left (Refl, Refl)
productOneThenNumbersOne (Pos (S Z)) (Pos (S (S _))) Refl impossible
productOneThenNumbersOne (Pos (S Z)) (NegS _) Refl impossible
productOneThenNumbersOne (Pos (S (S k))) (Pos Z) prf = void (posIsNotPosMultZero  (sym prf))
productOneThenNumbersOne (Pos (S (S _))) (Pos (S Z)) Refl impossible
productOneThenNumbersOne (Pos (S (S _))) (Pos (S (S _))) Refl impossible
productOneThenNumbersOne (Pos (S (S _))) (NegS _) Refl impossible
productOneThenNumbersOne (NegS Z) (Pos Z) Refl impossible
productOneThenNumbersOne (NegS Z) (Pos (S _)) Refl impossible
productOneThenNumbersOne (NegS Z) (NegS Z) prf = Right (Refl,Refl)
productOneThenNumbersOne (NegS Z) (NegS (S _)) Refl impossible
productOneThenNumbersOne (NegS (S k)) (Pos Z) prf = void (negTimesZeroIsNotPos{k=Z} (sym prf))
productOneThenNumbersOne (NegS (S _)) (Pos (S _)) Refl impossible
productOneThenNumbersOne (NegS (S _)) (NegS Z) Refl impossible
productOneThenNumbersOne (NegS (S _)) (NegS (S _)) Refl impossible

|||Right cancellation law for multiplication when right is positive
multRightCancelPosZ:(left1:ZZ)->(left2:ZZ)->(right:ZZ)->
   IsPositive right->(left1*right=left2*right)->(left1 = left2)
multRightCancelPosZ (Pos j) (Pos i) (Pos (S k)) Positive prf =
 cong (multRightCancel j i (S k) SIsNotZ expression) where
   expression = posInjective prf
multRightCancelPosZ (Pos _) (NegS _) (Pos (S _)) Positive Refl impossible
multRightCancelPosZ (NegS _) (Pos _) (Pos (S _)) Positive Refl impossible
multRightCancelPosZ (NegS j) (NegS i) (Pos (S k)) Positive prf =
  cong (succInjective j i (multRightCancel (S j) (S i) (S k) SIsNotZ expression)) where
    expression = posInjective (negativesSameNumbersSame prf)

|||Right cancellation law for multiplication given a proof that right is not zero
multRightCancelZ:(left1:ZZ)->(left2:ZZ)->(right:ZZ)->
   NotZero right->(left1*right=left2*right)->(left1 = left2)
multRightCancelZ left1 left2 (Pos (S k)) PositiveZ prf =
  multRightCancelPosZ left1 left2 (Pos (S k)) Positive prf
multRightCancelZ left1 left2 (NegS k) NegativeZ prf =
  multRightCancelPosZ left1 left2 (-(NegS k)) Positive expression where
    expression = rewrite (multNegateRightZ left1 (NegS k)) in
                 rewrite (multNegateRightZ left2 (NegS k)) in
                  (numbersSameNegativesSame prf)
|||Left Cancellation law for multiplication given a proof that left is not zero
multLeftCancelZ :(left : ZZ) -> (right1 : ZZ) -> (right2 : ZZ) ->
  NotZero left -> (left*right1 = left*right2) -> (right1 = right2)
multLeftCancelZ left right1 right2 x prf =
  multRightCancelZ right1 right2 left x expression where
    expression = rewrite (multCommutativeZ right1 left) in
                 rewrite (multCommutativeZ right2 left) in
                  prf

|||Proof that (-a)*(-b) = a*b
multNegNegNeutralZ: (a:ZZ)->(b:ZZ)->(-a)*(-b)=a*b
multNegNegNeutralZ a b =
  rewrite multNegateRightZ (-a) b in
  rewrite multNegateLeftZ a b in
  rewrite doubleNegElim (a*b) in
  Refl

|||The theorem that if  a =r+q*b and g = (m1*b)+(n1*rem)
|||Then g = (n1*a) + ((m1+n1*(-quot))*b)
bezoutReplace:{a:ZZ}->{b:ZZ}->{m1:ZZ}->{rem:ZZ}->
  {quot:ZZ}->{n1:ZZ}->{g:ZZ}-> (a = rem + (quot *b))->
     (g=(m1*b)+(n1*rem))->(g = (n1*a) + ((m1+n1*(-quot))*b))
bezoutReplace {a}{b}{m1}{rem}{quot}{n1}{g}prf prf1 =
  rewrite multDistributesOverPlusLeftZ m1 (n1*(-quot)) b in
  rewrite prf in
  rewrite multDistributesOverPlusRightZ n1 rem (quot*b) in
  rewrite (sym (plusAssociativeZ (n1*rem) (n1*((quot)*b)) ((m1*b)+((n1*(-quot))*b)))) in
  rewrite (plusCommutativeZ (m1*b) ((n1*(-quot))*b)) in
  rewrite (plusAssociativeZ (n1*((quot)*b)) ((n1*(-quot))*b) (m1*b)) in
  rewrite (multAssociativeZ n1 quot b) in
  rewrite (sym (multDistributesOverPlusLeftZ (n1*quot) (n1*(-quot)) b)) in
  rewrite (sym(multDistributesOverPlusRightZ n1 quot (-quot))) in
  rewrite (plusNegateInverseLZ quot) in
  rewrite (multZeroRightZeroZ n1) in
  rewrite (multZeroLeftZeroZ b) in
  rewrite (plusZeroLeftNeutralZ (m1*b)) in
  rewrite (plusCommutativeZ (n1*rem) (m1*b)) in
   prf1

zeroNotNonZero: (NotZero (Pos Z)) -> Void
zeroNotNonZero PositiveZ impossible
zeroNotNonZero NegativeZ impossible

decZero: (a: ZZ) -> Dec (NotZero a)
decZero (Pos Z) = No zeroNotNonZero
decZero (Pos (S k)) = Yes (posThenNotZero Positive)
decZero (NegS k) = Yes (NegSThenNotZero Negative)

nonZeroNotZero: (a: ZZ) -> ( (a = (Pos Z) ) -> Void) -> (NotZero a)
nonZeroNotZero (Pos Z) f = ?nonZeroNotZero_rhs_1
nonZeroNotZero (Pos (S k)) f = ?nonZeroNotZero_rhs_4
nonZeroNotZero (NegS k) f = ?nonZeroNotZero_rhs_2


text:
module Terminal

%include C "terminal.h"
%link C "terminal.o"

export
setRaw : IO ()
setRaw = foreign FFI_C "set_raw_terminal" (IO ())

--todo: remove after fix of: https://github.com/idris-lang/Idris-dev/issues/4723
theNat : Int -> Nat
theNat x = if x < 0 then Z else fromIntegerNat $ cast x

getRows' : IO Int
getRows' = foreign FFI_C "get_rows" (IO Int)

export
getRows : IO Nat
getRows = theNat <$> getRows'

getColumns' : IO Int
getColumns' = foreign FFI_C "get_columns" (IO Int)

export
getColumns : IO Nat
getColumns = theNat <$> getColumns'

export
escapeString : String -> String
escapeString command = strCons '\ESC' command

export
moveCursor : Nat -> Nat -> IO ()
moveCursor x y = do
  putStrLn $ escapeString $ "[" ++ show y ++ ";" ++ show x ++ "H"

export
clearScreen : IO ()
clearScreen = do
  putStrLn $ escapeString "[2J"
  moveCursor 0 0

export
hideCursor : IO ()
hideCursor = do
  putStrLn $ escapeString "[?25l"

export
showCursor : IO ()
showCursor = do
  putStrLn $ escapeString "[?25h"

public export
data Colour : Type where
  Black : Colour
  Red : Colour
  Green : Colour
  Yellow : Colour
  Blue : Colour
  Magenta : Colour
  Cyan : Colour
  White : Colour
  BrightBlack : Colour
  BrightRed : Colour
  BrightGreen : Colour
  BrightYellow : Colour
  BrightBlue : Colour
  BrightMagenta : Colour
  BrightCyan : Colour
  BrightWhite : Colour

colourCode : Colour -> String
colourCode Black = "[30m"
colourCode Red = "[31m"
colourCode Green = "[32m"
colourCode Yellow = "[33m"
colourCode Blue = "[34m"
colourCode Magenta = "[35m"
colourCode Cyan = "[36m"
colourCode White = "[37m"
colourCode BrightBlack = "[90m"
colourCode BrightRed = "[91m"
colourCode BrightGreen = "[92m"
colourCode BrightYellow = "[93m"
colourCode BrightBlue = "[94m"
colourCode BrightMagenta = "[95m"
colourCode BrightCyan = "[96m"
colourCode BrightWhite = "[97m"

export
setColour : Colour -> IO ()
setColour = putStr . escapeString . colourCode

max_stars_repo_name: PeterHajdu/iterm

max_issues_repo_name: PeterHajdu/iterm

max_forks_repo_name: PeterHajdu/iterm


text:
module Language.Reflection.TT

import public Data.List

%default total

public export
data Namespace = MkNS (List String) -- namespace, stored in reverse order

public export
data ModuleIdent = MkMI (List String) -- module identifier, stored in reverse order

export
showSep : String -> List String -> String
showSep sep [] = ""
showSep sep [x] = x
showSep sep (x :: xs) = x ++ sep ++ showSep sep xs

export
Show Namespace where
  show (MkNS ns) = showSep "." (reverse ns)

-- 'FilePos' represents the position of
-- the source information in the file (or REPL).
-- in the form of '(line-no, column-no)'.
public export
FilePos : Type
FilePos = (Int, Int)

public export
data VirtualIdent : Type where
  Interactive : VirtualIdent

public export
data OriginDesc : Type where
  ||| Anything that originates in physical Idris source files is assigned a
  ||| `PhysicalIdrSrc modIdent`,
  |||   where `modIdent` is the top-level module identifier of that file.
  PhysicalIdrSrc : (ident : ModuleIdent) -> OriginDesc
  ||| Anything parsed from a package file is decorated with `PhysicalPkgSrc fname`,
  |||   where `fname` is path to the package file.
  PhysicalPkgSrc : (fname : String) -> OriginDesc
  Virtual : (ident : VirtualIdent) -> OriginDesc

||| A file context is a filename together with starting and ending positions.
||| It's often carried by AST nodes that might have been created from a source
||| file or by the compiler. That makes it useful to have the notion of
||| `EmptyFC` as part of the type.
public export
data FC = MkFC        OriginDesc FilePos FilePos
        | ||| Virtual FCs are FC attached to desugared/generated code. They can help with marking
          ||| errors, but we shouldn't attach semantic highlighting metadata to them.
          MkVirtualFC OriginDesc FilePos FilePos
        | EmptyFC

public export
emptyFC : FC
emptyFC = EmptyFC

public export
data NameType : Type where
     Bound   : NameType
     Func    : NameType
     DataCon : (tag : Int) -> (arity : Nat) -> NameType
     TyCon   : (tag : Int) -> (arity : Nat) -> NameType

public export
data Constant
    = I Int
    | BI Integer
    | I8 Int8
    | I16 Int16
    | I32 Int32
    | I64 Int64
    | B8 Bits8
    | B16 Bits16
    | B32 Bits32
    | B64 Bits64
    | Str String
    | Ch Char
    | Db Double
    | WorldVal

    | IntType
    | IntegerType
    | Int8Type
    | Int16Type
    | Int32Type
    | Int64Type
    | Bits8Type
    | Bits16Type
    | Bits32Type
    | Bits64Type
    | StringType
    | CharType
    | DoubleType
    | WorldType

public export
data UserName
  = Basic String -- default name constructor       e.g. map
  | Field String -- field accessor                 e.g. .fst
  | Underscore   -- no name                        e.g. _

public export
data Name = NS Namespace Name -- name in a namespace
          | UN UserName -- user defined name
          | MN String Int -- machine generated name
          | DN String Name -- a name and how to display it
          | Nested (Int, Int) Name -- nested function name
          | CaseBlock String Int -- case block nested in (resolved) name
          | WithBlock String Int -- with block nested in (resolved) name

export
Show UserName where
  show (Basic n) = n
  show (Field n) = "." ++ n
  show Underscore = "_"

export
Show Name where
  show (NS ns n) = show ns ++ "." ++ show n
  show (UN x) = show x
  show (MN x y) = "{" ++ x ++ ":" ++ show y ++ "}"
  show (DN str y) = str
  show (Nested (outer, idx) inner)
      = show outer ++ ":" ++ show idx ++ ":" ++ show inner
  show (CaseBlock outer i) = "case block in " ++ show outer
  show (WithBlock outer i) = "with block in " ++ show outer

public export
data Count = M0 | M1 | MW

public export
data PiInfo t = ImplicitArg | ExplicitArg | AutoImplicit | DefImplicit t

public export
data IsVar : Name -> Nat -> List Name -> Type where
     First : IsVar n Z (n :: ns)
     Later : IsVar n i ns -> IsVar n (S i) (m :: ns)

public export
data LazyReason = LInf | LLazy | LUnknown

export
data TT : Type where [external]

{-
-- Type checked terms in the core TT
public export
data TT : List Name -> Type where
     Local : FC -> (idx : Nat) -> (0 prf : IsVar name idx vars) -> TT vars
     Ref : FC -> NameType -> Name -> TT vars
     Pi : FC -> Count -> PiInfo (TT vars) ->
          (x : Name) -> (argTy : TT vars) -> (retTy : TT (x :: vars)) ->
          TT vars
     Lam : FC -> Count -> PiInfo (TT vars) ->
           (x : Name) -> (argTy : TT vars) -> (scope : TT (x :: vars)) ->
           TT vars
     App : FC -> TT vars -> TT vars -> TT vars
     TDelayed : FC -> LazyReason -> TT vars -> TT vars
     TDelay : FC -> LazyReason -> (ty : TT vars) -> (arg : TT vars) -> TT vars
     TForce : FC -> LazyReason -> TT vars -> TT vars
     PrimVal : FC -> Constant -> TT vars
     Erased : FC -> TT vars
     TType : FC -> TT vars
     -}

public export
data TotalReq = Total | CoveringOnly | PartialOK

public export
data Visibility = Private | Export | Public

public export
data BuiltinType = BuiltinNatural | NaturalToInteger | IntegerToNatural


text:
-- ------------------------------------------------------------ [ Sequence.idr ]
-- Module      : UML.Sequence
-- Description : Sequence diagrams.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Sequence

import public UML.Sequence.Model
import public UML.Sequence.Parser
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module Biapplicative

import Bifunctor
import Apply

infixl 4 <<*>>, <<*, *>>, <<**>>

||| Biapplicatives
||| @p the action of the Biapplicative on pairs of objects
public export
interface Bifunctor p => Biapplicative p where -- (p : Type -> Type -> Type) where

  ||| Lifts two values into a Biapplicative
  |||
  ||| ````idris example
  ||| bipure 1 "hello" = (1, "hello")
  ||| ````
  |||
  bipure : a -> b -> p a b

  ||| Applies a Biapplicative of functions to a second Biapplicative
  |||
  ||| ````idris example
  ||| ( (\x => x + 1), reverse ) <<*>> (1, "hello") == (2, "olleh")
  ||| ````
  |||
  (<<*>>) : p (a -> b) (c -> d) -> p a c -> p b d

  ||| Sequences two Biapplicatives rightwards
  |||
  ||| ````idris example
  ||| (1, "hello") *>> (2, "goodbye") = (2, "goodbye")
  ||| ````
  |||
  (*>>) : p a b -> p c d -> p c d
  a *>> b = bimap (const id) (const id) <<$>> a <<*>> b

  ||| Sequences two Biapplicatives leftwards
  |||
  ||| ````idris example
  ||| (1, "hello") <<* (2, "goodbye") = (1, "hello")
  ||| ````
  |||
  (<<*) : p a b -> p c d -> p a b
  a <<* b = bimap const const <<$>> a <<*>> b

||| Applies the second of two Biapplicatives to the first
|||
||| ````idris example
||| (1, "hello") <<**>> ( (\x => x + 1), reverse ) == (2, "olleh")
||| ````
|||
export
(<<**>>) : Biapplicative p => p a c -> p (a -> b) (c -> d) -> p b d
(<<**>>) = flip (<<*>>)

export
biliftA2 : Biapplicative p => (a -> b -> c) ->
                              (d -> e -> f) -> p a d -> p b e -> p c f
biliftA2 f g a b = bimap f g <<$>> a <<*>> b

export
biliftA3 : Biapplicative p =>
  (a -> b -> c -> d) -> (e -> f -> g -> h) -> p a e -> p b f -> p c g -> p d h
biliftA3 f g a b c = bimap f g <<$>> a <<*>> b <<*>> c

public export
implementation Biapplicative Pair where
  bipure a b          = (a, b)
  (f, g) <<*>> (a, b) = (f a, g b)


text:
module Control.Monad.State.State

import Control.Monad.Identity
import Control.Monad.Trans

%default total

||| The transformer on which the State monad is based
public export
record StateT (stateType : Type) (m : Type -> Type) (a : Type) where
  constructor ST
  runStateT' : stateType -> m (stateType, a)

||| Unwrap and apply a StateT monad computation.
public export
%inline
runStateT : stateType -> StateT stateType m a -> m (stateType, a)
runStateT s act = runStateT' act s

||| Unwrap and apply a StateT monad computation, but discard the final state.
public export %inline
evalStateT : Functor m => stateType -> StateT stateType m a -> m a
evalStateT s = map snd . runStateT s

||| Unwrap and apply a StateT monad computation, but discard the resulting value.
public export %inline
execStateT : Functor m => stateType -> StateT stateType m a -> m stateType
execStateT s = map fst . runStateT s

||| Map both the return value and final state of a computation using
||| the given function.
public export %inline
mapStateT : (m (s, a) -> n (s, b)) -> StateT s m a -> StateT s n b
mapStateT f m = ST $ f . runStateT' m

--------------------------------------------------------------------------------
--          State
--------------------------------------------------------------------------------

||| The State monad. See the MonadState interface
public export
State : (stateType : Type) -> (ty : Type) -> Type
State = \s, a => StateT s Identity a

||| Unwrap and apply a State monad computation.
public export %inline
runState : stateType -> State stateType a -> (stateType, a)
runState s act = runIdentity (runStateT s act)

||| Unwrap and apply a State monad computation, but discard the final state.
public export %inline
evalState : stateType -> State stateType a -> a
evalState s = snd . runState s

||| Unwrap and apply a State monad computation, but discard the resulting value.
public export %inline
execState : stateType -> State stateType a -> stateType
execState s = fst . runState s

||| Map both the return value and final state of a computation using
||| the given function.
public export %inline
mapState : ((s, a) -> (s, b)) -> State s a -> State s b
mapState f = mapStateT $ \(Id p) => Id (f p)

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

public export
implementation Functor f => Functor (StateT stateType f) where
    map f (ST g) = ST $ \st => map f <$> g st

public export
implementation Monad f => Applicative (StateT stateType f) where
    pure x = ST $ \st => pure (st, x)

    ST f <*> ST a
        = ST $ \st =>
               do (r, g) <- f st
                  (t, b) <- a r
                  pure (t, g b)

public export
implementation Monad m => Monad (StateT stateType m) where
    ST f >>= k
        = ST $ \st =>
               do (st', v) <- f st
                  runStateT st' $ k v

public export
implementation MonadTrans (StateT stateType) where
    lift x = ST $ \st => (st,) <$> x

public export
implementation (Monad f, Alternative f) => Alternative (StateT st f) where
    empty = lift empty
    ST f <|> mg = ST $ \st => f st <|> runStateT' mg st

public export
implementation HasIO m => HasIO (StateT stateType m) where
  liftIO io = ST $ \s => liftIO $ io_bind io $ \a => pure (s, a)


text:
module Compiler.Codegen.LLVM

import Data.List
import Data.String
import System
import System.File
import System.Info

import Core.Directory
import Core.CompileExpr
import Core.Context
import Core.Options
import Compiler.Common
import Compiler.VMCode
import Libraries.Utils.Path

import Rapid.Common
import Rapid.Driver

shell : List String -> String
shell args = showSep " " $ map shellQuote args
  where
    shellQuote : String -> String
    shellQuote s = s

runShell : List String -> IO ()
runShell args = do
  let cmd = shell args
  ignore $ fPutStrLn stderr $ "+" ++ cmd
  rc <- system cmd
  case rc of
       0 => pure ()
       err_rc => do putStrLn $ "command failed with exit code " ++ show err_rc
                    exitFailure

abort : String -> IO ()
abort msg = do
  ignore $ fPutStrLn stderr ("error: " ++ msg)
  exitFailure

globalizeStackmap : String -> IO Bool
globalizeStackmap fname = do
  (Right outFile) <- openFile fname Append
  | Left err => do putStrLn $ "error opening asm file: " ++ show err
                   pure False
  ignore $ fPutStr outFile "\n.globl __LLVM_StackMaps\n"
  ignore $ closeFile outFile
  pure True

getDebug : List String -> Bool
getDebug = any isDebug
  where
    isDebug : String -> Bool
    isDebug directive = (trim directive) == "debug"

getGCDirective : List String -> Either String GCFlavour
getGCDirective [] = pure Statepoint
getGCDirective ("gc=zero"::_) = pure Zero
getGCDirective ("gc=bdw"::_) = pure BDW
getGCDirective ("gc=statepoint"::_) = pure Statepoint
getGCDirective (x::xs) = if isPrefixOf "gc=" x
  then Left ("invalid GC flavour: " ++ x ++ " (supported: zero,bdw,statepoint)")
  else getGCDirective xs

compile : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
        ClosedTerm -> (outfile : String) -> Core (Maybe String)
compile defs tmpDir outputDir term outfile = do
  let appDirRel = outfile ++ "_rapid" -- relative to build dir
  let appDirGen = outputDir </> appDirRel -- relative to here
  let outputFileName = appDirGen </> (outfile ++ ".ll") -- LLVM IR (text)
  let bcFileName = appDirGen </> (outfile ++ ".bc") -- optimized LLVM bitcode
  let objectFileName = appDirGen </> (outfile ++ ".o") -- object file
  let binaryFileName = outputDir </> outfile
  coreLift_ $ mkdirAll appDirGen

  directives <- getDirectives (Other "llvm")
  let debug = getDebug directives
  coreLift_ $ fPutStrLn stderr ("debug: " ++ show debug)

  (Right gc) <- pure $ getGCDirective directives
    | Left err => (coreLift_ $ fPutStrLn stderr err) >> (pure Nothing)
  coreLift_ $ fPutStrLn stderr ("selected GC strategy: " ++ show gc)

  let opts = MkCompileOpts debug False gc os 0

  -- load supporting files first, so we can fail early
  support <- readDataFile $ "rapid" </> "support.ll"
  runtime <- findDataFile $ "rapid" </> "runtime.bc"
  platformLib <- findDataFile $ "rapid" </> "platform.a"
  rapidLLVMPlugin <- findDataFile $ "rapid" </> "librapid.so"

  cd <- getCompileData False VMCode term
  coreLift_ $ fPutStrLn stderr $ "got compiledata"
  let allFunctions = vmcode cd
  let optFlags = [
    "-mem2reg", "-instsimplify", "-constmerge", "-sccp", "-dce", "-globaldce"
    ]
  let gcPassFlags = if (gc == Statepoint) then ["-rewrite-statepoints-for-gc"] else []
  let gcLDFlags = if (gc == BDW) then ["-lgc"] else []
  let clangDebugFlags = if debug then ["-g"] else []

  coreLift_ $ writeIR allFunctions support outputFileName opts

  let lateTransformFlags = ["-rapid-lower"]
  coreLift $ do
    runShell $ ["opt", outputFileName, "-load-pass-plugin=" ++ rapidLLVMPlugin, "-load=" ++ rapidLLVMPlugin] ++ optFlags ++ gcPassFlags ++ lateTransformFlags ++ ["-o=" ++ bcFileName]
    runShell ["llc", "--frame-pointer=all", "-tailcallopt", "--filetype=obj", "-o=" ++ objectFileName, bcFileName]
    runShell $ ["clang"] ++ clangDebugFlags ++ ["-o", binaryFileName, objectFileName, runtime, platformLib, "-L/usr/local/lib", "-lm", "-lgmp"] ++ gcLDFlags

    pure ()

  pure $ Nothing

execute : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
execute defs tmpDir term = do
  let tmpExecutableFile = "idris_tmp"
  ignore $ compile defs tmpDir tmpDir term tmpExecutableFile
  coreLift_ $ system (tmpDir </> tmpExecutableFile)
  pure ()

export
rapidCodegen : Codegen
rapidCodegen = MkCG compile execute Nothing Nothing


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

s15000 : PrintString m => CanSleep m => (offset : Time) => m String
s15000 = do
  printTime offset "s15000 proc, first"
  for 5 $ do
    printTime offset "s15000 proc, before 1000"
    sleepFor 1.seconds
    printTime offset "s15000 proc, before 2000"
    sleepFor 2.seconds
  "long" <$ printTime offset "s15000 proc, last"

s5500 : PrintString m => CanSleep m => (offset : Time) => m String
s5500 = do
  printTime offset "                         s5500 proc, first"
  for 5 $ do
    printTime offset "                         s5500 proc, before 350"
    sleepFor 350.millis
    printTime offset "                         s5500 proc, before 750"
    sleepFor 750.millis
  "short" <$ printTime offset "                         s5500 proc, last"

n3500 : PrintString m => CanSleep m => (offset : Time) => m Nat
n3500 = do
  printTime offset "                                               n3500 proc, first"
  for 5 $ do
    printTime offset "                                               n3500 proc, before 700"
    sleepFor 700.millis
  700 <$ printTime offset "                                               n3500 proc, last"

n7700 : PrintString m => CanSleep m => (offset : Time) => m Nat
n7700 = do
  printTime offset "                                                                      n7700 proc, first"
  for 5 $ do
    printTime offset "                                                                      n7700 proc, before 1350"
    sleepFor 1350.millis
  sleepFor 950.millis
  333 <$ printTime offset "                                                                      n7700 proc, last"

export
program : PrintString m => CanSleep m => Zippable m => Alternative m => m Unit
program = do
  offset <- currentTime
  printTime offset "start"

  res <- zipWith (\s, n => s ++ show n) (s15000 <|> s5500) (n3500 <|> n7700)
  printTime offset "top: \{res}"

  printTime offset "end"


text:
module Examples.FourPointLattice

import public DepSec.Lattice

%access public export

data FourPoint = H | M1 | M2 | L

implementation JoinSemilattice FourPoint where
  join H _ = H
  join _ H = H
  join L x = x
  join x L = x
  join M1 M1 = M1
  join M1 M2 = H
  join M2 M1 = H
  join M2 M2 = M2

  associative H x y = Refl
  associative M1 H H = Refl
  associative M1 H M1 = Refl
  associative M1 H M2 = Refl
  associative M1 H L = Refl
  associative M1 M1 H = Refl
  associative M1 M1 M1 = Refl
  associative M1 M1 M2 = Refl
  associative M1 M1 L = Refl
  associative M1 M2 H = Refl
  associative M1 M2 M1 = Refl
  associative M1 M2 M2 = Refl
  associative M1 M2 L = Refl
  associative M1 L H = Refl
  associative M1 L M1 = Refl
  associative M1 L M2 = Refl
  associative M1 L L = Refl
  associative M2 H H = Refl
  associative M2 H M1 = Refl
  associative M2 H M2 = Refl
  associative M2 H L = Refl
  associative M2 M1 H = Refl
  associative M2 M1 M1 = Refl
  associative M2 M1 M2 = Refl
  associative M2 M1 L = Refl
  associative M2 M2 H = Refl
  associative M2 M2 M1 = Refl
  associative M2 M2 M2 = Refl
  associative M2 M2 L = Refl
  associative M2 L H = Refl
  associative M2 L M1 = Refl
  associative M2 L M2 = Refl
  associative M2 L L = Refl
  associative L H H = Refl
  associative L H M1 = Refl
  associative L H M2 = Refl
  associative L H L = Refl
  associative L M1 H = Refl
  associative L M1 M1 = Refl
  associative L M1 M2 = Refl
  associative L M1 L = Refl
  associative L M2 H = Refl
  associative L M2 M1 = Refl
  associative L M2 M2 = Refl
  associative L M2 L = Refl
  associative L L H = Refl
  associative L L M1 = Refl
  associative L L M2 = Refl
  associative L L L = Refl

  commutative H H = Refl
  commutative H M1 = Refl
  commutative H M2 = Refl
  commutative H L = Refl
  commutative M1 H = Refl
  commutative M1 M1 = Refl
  commutative M1 M2 = Refl
  commutative M1 L = Refl
  commutative M2 H = Refl
  commutative M2 M1 = Refl
  commutative M2 M2 = Refl
  commutative M2 L = Refl
  commutative L H = Refl
  commutative L M1 = Refl
  commutative L M2 = Refl
  commutative L L = Refl

  idempotent H = Refl
  idempotent M1 = Refl
  idempotent M2 = Refl
  idempotent L = Refl

implementation BoundedJoinSemilattice FourPoint where
  Bottom = L
  unitary H = Refl
  unitary L = Refl
  unitary M1 = Refl
  unitary M2 = Refl

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module Decidable.Order

import Decidable.Decidable
import Decidable.Equality
import Data.Fin
import Data.Fun
import Data.Rel

%hide Prelude.Equal

--------------------------------------------------------------------------------
-- Utility Lemmas
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
-- Preorders, Posets, total Orders, Equivalencies, Congruencies
--------------------------------------------------------------------------------

public export
interface Preorder t (po : t -> t -> Type) where
  total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c
  total reflexive : (a : t) -> po a a

public export
interface (Preorder t po) => Poset t (po : t -> t -> Type) where
  total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b

public export
interface (Poset t to) => Ordered t (to : t -> t -> Type) where
  total order : (a : t) -> (b : t) -> Either (to a b) (to b a)

public export
interface (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where
  total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a

public export
interface (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) where
  total congruent : (a : t) ->
                    (b : t) ->
                    eq a b ->
                    eq (f a) (f b)

public export
minimum : (Ordered t to) => t -> t -> t
minimum {to} x y with (order {to} x y)
  minimum {to} x y | Left _ = x
  minimum {to} x y | Right _ = y

public export
maximum : (Ordered t to) => t -> t -> t
maximum {to} x y with (order {to} x y)
  maximum {to} x y | Left _ = y
  maximum {to} x y | Right _ = x

--------------------------------------------------------------------------------
-- Syntactic equivalence (=)
--------------------------------------------------------------------------------

public export
implementation Preorder t Equal where
  transitive a b c l r = trans l r
  reflexive a = Refl

public export
implementation Equivalence t Equal where
  symmetric a b prf = sym prf

public export
implementation Congruence t f Equal where
  congruent a b eq = cong f eq


text:
module Dart.Core

import Dart.FFI.Constructors
import Dart.FFI.Upcast
import public Dart.FFI.Types
import public System.FFI

%inline
export
print : HasIO io => {a : Type} -> a -> io ()
print value = primIO $ prim__dart_invoke "print,dart:core" [] [value] Parameters.none

%inline
public export
Object : Type
Object = Struct "Object,dart:core" [("hashCode", Int)]

public export
IsAssignableFrom Object _ where

%inline
public export
Symbol : Type
Symbol = Struct "Symbol,dart:core" [("hashCode", Int)]

%inline
public export
Duration : Type
Duration = Struct "Duration,dart:core" []

%inline
public export
Iterable : Type -> Type
Iterable element = GenericType "Iterable,dart:core" [element]

%inline
public export
List : Type -> Type
List element = GenericType "List,dart:core" [element]

%inline
public export
Map : Type -> Type -> Type
Map k v = GenericType "Map,dart:core" [k, v]

%inline
public export
Set : Type -> Type
Set e = GenericType "Set,dart:core" [e]

namespace Object

  public export
  toString : HasIO io => {a : Type} -> a -> io String
  toString this = primIO $ prim__dart_invoke ".toString" [] [this] Parameters.none

%inline
public export
DartBool : Type
DartBool = Struct "bool,dart:core" [("hashCode", Int)]

export
%extern prim__dart_if : DartBool -> a -> a -> a

namespace DartBool

  %inline
  public export
  true : DartBool
  true = prim__dart_get_pure "true" Void

  %inline
  public export
  false : DartBool
  false = prim__dart_get_pure "false" Void

  %inline
  public export
  fromBool : Bool -> DartBool
  fromBool b = prim__dart_invoke_pure "==" [] [b, True] none

  %inline
  public export
  toBool : DartBool -> Bool
  toBool b = prim__dart_if b True False

%inline
export
prim__dart_eq : a -> a -> Bool
prim__dart_eq x y =
  let
    x' = the AnyPtr (believe_me x)
    y' = the AnyPtr (believe_me y)
  in toBool (prim__dart_invoke_pure "==" [] [x', y'] none)

%inline
export
Cast Bool DartBool where
  cast = fromBool

%inline
export
Cast DartBool Bool where
  cast = toBool

%inline
export
Eq DartBool where
  (==) x y = toBool (prim__dart_invoke_pure "==" [] [x, y] none)

export
Show DartBool where
  show b = show (toBool b)

%extern prim__dart_List_new : (element : Type) -> (1 x : %World) -> IORes (Dart.Core.List element)

%extern prim__dart_List_empty : (element : Type) -> Dart.Core.List element

%extern prim__dart_List_fromList : (element : Type) -> Prelude.List element -> Dart.Core.List element

namespace List

  %inline
  export
  empty : {element : Type} -> Dart.Core.List element
  empty = prim__dart_List_empty element

  %inline
  export
  new : HasIO io => {element : Type} -> io (Dart.Core.List element)
  new = primIO $ prim__dart_List_new element

  %inline
  export
  fromList : {element : Type} -> Prelude.List element -> Dart.Core.List element
  fromList l = prim__dart_List_fromList element l

  %inline
  export
  add : HasIO io => {element : Type} -> element -> Dart.Core.List element -> io ()
  add e list = primIO $ prim__dart_invoke ".add" [] [list, e] none

  %inline
  export
  into : HasIO io => {element : Type} -> Dart.Core.List element -> UpcastList element -> io (Dart.Core.List element)
  into result es = do
    traverse_ (`add` result) (UpcastList.toList es)
    pure result

public export
IsAssignableFrom (Iterable element) (Dart.Core.List element) where

namespace Iterable

  %inline
  public export
  forEach : HasIO io => {element : Type} -> {iterable : Type} -> IsAssignableFrom (Iterable element) iterable => (element -> IO ()) -> iterable -> io ()
  forEach action iterable = primIO $ prim__dart_invoke ".forEach" [] [iterable, action] Parameters.none

%extern prim__dart_unsafe_null : a

namespace Nullable

  %inline
  export
  null : Nullable a
  null = prim__dart_unsafe_null

  %inline
  export
  unsafeNull : a
  unsafeNull = prim__dart_unsafe_null

  %inline
  export
  isNull : Nullable a -> Bool
  isNull a = toBool $
    prim__dart_invoke_pure "==" [] [
      the AnyPtr (believe_me a),
      the AnyPtr prim__dart_unsafe_null
    ] none

  %inline
  export
  nullable : Lazy b -> (a -> b) -> Nullable a -> b
  nullable nullValue f a = if isNull a then nullValue else f (believe_me a)

  %inline
  export
  toMaybe : Nullable a -> Maybe a
  toMaybe = nullable Nothing Just

  %inline
  export
  traverse : Applicative f => (a -> f b) -> Nullable a -> f (Nullable b)
  traverse f a =
    if isNull a
      then pure Nullable.null
      else cast <$> f (believe_me a)


text:
module CairoCode.Traversal.Composition

import CairoCode.CairoCode
import CairoCode.Traversal.Base
import Utils.Lens

{-
 Executes f1 and f2 on the same value, but uses state after f1 for f2 and discards value after f1
 start - value & state -----> f1 - value -> _
     | - value -> f2 <- state -|
                   | - value & state -> end
-}
export
seqTraversal : (InstVisit b -> Traversal s ()) -> (InstVisit b -> Traversal s a) -> (InstVisit b -> Traversal s a)
seqTraversal f1 f2 = (\inst => f1 inst >>= (\_ => f2 inst))

{-
 Executes f1 and f2 on the same value, but uses state after f1 for f2 and returns the tuple of the f1 & f2 values
 start - value & state -----> f1 - value -|
     | - value -> f2 <- state -|          v
                   | - value ----> build tuple
                   | - state -> end <- value |
-}
export
joinedTraversal : (InstVisit c -> Traversal s a) -> (InstVisit c -> Traversal s b) -> (InstVisit c -> Traversal s (a,b))
joinedTraversal f1 f2 = (\inst => f1 inst >>= (\av => map (\bv => (av,bv)) (f2 inst)))

{-
 Executes f1 which returns multiple values and then executing f2 on each (routing through the state) collecting the results in a monoid over  <+>
 start - value & state -----> f1 - state & [value] -> for each value : f2 - state & [value]* -> end
 *monoid integrating all f2 results (probably a list)
-}
export
chainedTraversal : Monoid a => (InstVisit b -> Traversal s (List (InstVisit c))) -> (InstVisit c -> Traversal s a) -> (InstVisit b -> Traversal s a)
chainedTraversal f1 f2 = (\inst => f1 inst >>= (\ls => foldlM (\r, inst => (f2 inst) >>= (\rn => pure $ r <+> rn)) neutral ls) )

{-
 Executes f1 which returns multiple values and then executing f2 on each throwing away the result (but routing through the state)
 start - value & state -----> f1 - state & [value] -> for each value : f2 - [value] -> _
                               | - [value] -------> end <------ state - |
-}
export
traverseTransform : (InstVisit b -> Traversal s (List (InstVisit c))) -> (InstVisit c -> Traversal s ()) -> (InstVisit b -> Traversal s (List (InstVisit c)))
traverseTransform f1 f2 = (\inst => f1 inst >>= (\ls => map (\_ => ls) (foldlM (\_, inst => f2 inst) () ls)))

{-
 Executes trav but on a sub-state identified by lens
 start - value & os -> (lens : - value & is -> trav - value & is ->) - value & os -> end
-}
export
lensTraversal : Lens os is -> (InstVisit a -> Traversal is r) -> (InstVisit a -> Traversal os r)
lensTraversal lens trav = (composeState lens) . trav

{-
 Executes trav but on a tupled state using the left part
 start - value & (ls,rs) -> (left : -> value & ls -> trav -> value & ls) - value & (ls,rs) -> end
-}
export
leftTraversal : (InstVisit a -> Traversal ls r) -> (InstVisit a -> Traversal (ls, rs) r)
leftTraversal trav = lensTraversal leftLens trav

{-
 Executes trav but on a tupled state using the right part
 start - value & (ls,rs) -> (left : -> value & rs -> trav -> value & rs) - value & (ls,rs) -> end
-}
export
rightTraversal : (InstVisit a -> Traversal rs r) -> (InstVisit a -> Traversal (ls, rs) r)
rightTraversal trav = lensTraversal rightLens trav

{-
 Executes fn and if defined (Just) uses the result otherwise (Nothing) uses fallback to define the value
 start - value & state -> fn | case Just: - value & state --------------------------v
     |                       | case Nothing: - state -> fallback - value & state -> end
     | - value -----------------------------------------^
-}
export
fallbackTraversal : (InstVisit b ->  Traversal s (Maybe a)) -> (InstVisit b -> Traversal s a)-> (InstVisit b ->  Traversal s a)
fallbackTraversal fn fallback = (\inst => fn inst >>= (execFallback inst))
    where execFallback: InstVisit b -> Maybe a -> Traversal s a
          execFallback inst (Just av) = pure av
          execFallback inst Nothing = fallback inst

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro