text:
module Network.TLS.HKDF

import Crypto.Hash
import Crypto.Hash.HMAC
import Data.Bits
import Data.List
import Data.Stream
import Data.Stream.Extra
import Data.Vect
import Utils.Bytes
import Utils.Misc

public export
hkdf_extract : (0 algo : Type) -> Hash algo => List Bits8 -> List Bits8 -> Vect (digest_nbyte {algo}) Bits8
hkdf_extract algo salt ikm = mac (HMAC algo) salt ikm

hkdf_expand_stream : (0 algo : Type) -> Hash algo => List Bits8 -> List Bits8 -> Stream Bits8
hkdf_expand_stream algo prk info = stream_concat (snd <$> iterate go (Z, []))
  where
    go : (Nat, List Bits8) -> (Nat, List Bits8)
    go (i, last) =
      let i' = cast {to=Bits8} (S i)
          body = last ++ info ++ [i']
      in (S i, toList $ mac (HMAC algo) prk body)

public export
hkdf_expand : (0 algo : Type) -> Hash algo => (l : Nat) -> List Bits8 -> List Bits8 -> Vect l Bits8
hkdf_expand algo l prk info = take l $ hkdf_expand_stream algo prk info

tls13_constant : List Bits8
tls13_constant = string_to_ascii "tls13 "

export
tls13_hkdf_expand_label : (0 algo : Type) -> Hash algo => (secret : List Bits8) -> (label : List Bits8) -> (context : List Bits8) -> (length : Nat) -> Vect length Bits8
tls13_hkdf_expand_label algo secret label context lth =
  let l = to_be {n=2} $ cast {to=Bits16} lth
      l' = cast {to=Bits8} $ (6 + length label)
      i' = cast {to=Bits8} $ length context
      body = ((toList l) <+> [l'] <+> tls13_constant <+> label <+> [i'] <+> context)
  in hkdf_expand algo lth secret body

public export
record HandshakeKeys (iv : Nat) (key : Nat) where
  constructor MkHandshakeKeys
  handshake_secret : List Bits8
  client_handshake_key : Vect key Bits8
  server_handshake_key : Vect key Bits8
  client_handshake_iv  : Vect iv Bits8
  server_handshake_iv  : Vect iv Bits8
  client_traffic_secret : List Bits8
  server_traffic_secret : List Bits8

public export
record ApplicationKeys (iv : Nat) (key : Nat) where
  constructor MkApplicationKeys
  client_application_key : Vect key Bits8
  server_application_key : Vect key Bits8
  client_application_iv  : Vect iv Bits8
  server_application_iv  : Vect iv Bits8

export
tls13_handshake_derive : (0 algo : Type) -> Hash algo => (iv : Nat) -> (key : Nat) -> List Bits8 -> List Bits8 -> HandshakeKeys iv key
tls13_handshake_derive algo iv key shared_secret hello_hash =
  let zeros = List.replicate (digest_nbyte {algo}) (the Bits8 0)
      early_secret = toList $ hkdf_extract algo [the Bits8 0] zeros
      empty_hash = toList $ hash algo []
      derived_secret = tls13_hkdf_expand_label algo early_secret (string_to_ascii "derived") empty_hash $ digest_nbyte {algo}
      handshake_secret = toList $ hkdf_extract algo (toList derived_secret) shared_secret
      client_handshake_traffic_secret = toList $
        tls13_hkdf_expand_label algo handshake_secret (string_to_ascii "c hs traffic") hello_hash $ digest_nbyte {algo}
      server_handshake_traffic_secret = toList $
        tls13_hkdf_expand_label algo handshake_secret (string_to_ascii "s hs traffic") hello_hash $ digest_nbyte {algo}
      client_handshake_key =
        tls13_hkdf_expand_label algo client_handshake_traffic_secret (string_to_ascii "key") [] key
      client_handshake_iv =
        tls13_hkdf_expand_label algo client_handshake_traffic_secret (string_to_ascii "iv") [] iv
      server_handshake_key =
        tls13_hkdf_expand_label algo server_handshake_traffic_secret (string_to_ascii "key") [] key
      server_handshake_iv =
        tls13_hkdf_expand_label algo server_handshake_traffic_secret (string_to_ascii "iv") [] iv
  in MkHandshakeKeys
      handshake_secret
      client_handshake_key
      server_handshake_key
      client_handshake_iv
      server_handshake_iv
      (toList client_handshake_traffic_secret)
      (toList server_handshake_traffic_secret)

public export
tls13_application_derive : {iv : Nat} -> {key : Nat} -> (0 algo : Type) -> Hash algo => HandshakeKeys iv key -> List Bits8 -> ApplicationKeys iv key
tls13_application_derive algo (MkHandshakeKeys handshake_secret _ _ _ _ _ _) handshake_hash =
  let zeros = List.replicate (digest_nbyte {algo}) (the Bits8 0)
      empty_hash = toList $ hash algo []
      derived_secret =
        tls13_hkdf_expand_label algo handshake_secret (string_to_ascii "derived") empty_hash $ digest_nbyte {algo}
      master_secret = toList $ hkdf_extract algo (toList derived_secret) zeros
      client_application_traffic_secret = toList $
        tls13_hkdf_expand_label algo master_secret (string_to_ascii "c ap traffic") handshake_hash $ digest_nbyte {algo}
      server_application_traffic_secret = toList $
        tls13_hkdf_expand_label algo master_secret (string_to_ascii "s ap traffic") handshake_hash $ digest_nbyte {algo}
      client_application_key =
        tls13_hkdf_expand_label algo client_application_traffic_secret (string_to_ascii "key") [] key
      client_application_iv =
        tls13_hkdf_expand_label algo client_application_traffic_secret (string_to_ascii "iv") [] iv
      server_application_key =
        tls13_hkdf_expand_label algo server_application_traffic_secret (string_to_ascii "key") [] key
      server_application_iv =
        tls13_hkdf_expand_label algo server_application_traffic_secret (string_to_ascii "iv") [] iv
  in MkApplicationKeys client_application_key server_application_key client_application_iv server_application_iv

public export
tls13_verify_data : (0 algo : Type) -> Hash algo => List Bits8 -> List Bits8 -> List Bits8
tls13_verify_data algo traffic_secret records_hash =
  let finished_key = toList $
        tls13_hkdf_expand_label algo traffic_secret (string_to_ascii "finished") [] $ digest_nbyte {algo}
  in toList $ hkdf_extract algo finished_key records_hash

public export
record Application2Keys (iv : Nat) (key : Nat) (mac : Nat) where
  constructor MkApplication2Keys
  master_secret : Vect 48 Bits8
  client_mac_key : Vect mac Bits8
  server_mac_key : Vect mac Bits8
  client_application_key : Vect key Bits8
  server_application_key : Vect key Bits8
  client_application_iv  : Vect iv  Bits8
  server_application_iv  : Vect iv  Bits8

hmac_stream : Hash algo -> List Bits8 -> List Bits8 -> Stream Bits8
hmac_stream hwit secret seed =
  stream_concat
  $ map (\ax => toList $ mac (HMAC algo) secret $ ax <+> seed)
  $ drop 1
  $ iterate (toList . mac (HMAC algo) secret) seed

public export
tls12_application_derive : Hash algo -> (iv : Nat) -> (key : Nat) -> (mac : Nat) -> List Bits8 -> List Bits8 -> List Bits8 ->
                           Application2Keys iv key mac
tls12_application_derive hwit iv key mac shared_secret client_random server_random =
  let master_secret =
        Stream.take 48
        $ hmac_stream hwit shared_secret
        $ (string_to_ascii "master secret") <+> client_random <+> server_random
      secret_material =
        hmac_stream hwit
          (toList master_secret)
          (string_to_ascii "key expansion" <+> server_random <+> client_random)
      (client_mac_key, secret_material)         = Misc.splitAt mac secret_material
      (server_mac_key, secret_material)         = Misc.splitAt mac secret_material
      (client_application_key, secret_material) = Misc.splitAt key secret_material
      (server_application_key, secret_material) = Misc.splitAt key secret_material
      (client_application_iv, secret_material)  = Misc.splitAt iv  secret_material
      (server_application_iv, secret_material)  = Misc.splitAt iv  secret_material
  in MkApplication2Keys
       master_secret
       client_mac_key
       server_mac_key
       client_application_key
       server_application_key
       client_application_iv
       server_application_iv

public export
tls12_client_verify_data : Hash algo -> (n : Nat) -> List Bits8 -> List Bits8 -> Vect n Bits8
tls12_client_verify_data algo n master_secret records_hash =
  take _ $ hmac_stream algo master_secret (string_to_ascii "client finished" <+> records_hash)

public export
tls12_server_verify_data : Hash algo -> (n : Nat) -> List Bits8 -> List Bits8 -> Vect n Bits8
tls12_server_verify_data algo n master_secret records_hash =
  take _ $ hmac_stream algo master_secret (string_to_ascii "server finished" <+> records_hash)


text:
module Node.FS

import Coda.Node.Core

%access public export
%default total

||| Sample fs module function
readFileSync : Ptr -> String -> JS_IO String
readFileSync fs fileName = do
  buffer   <- method { a = String } { b = Ptr } fs "readFileSync" fileName
  contents <- method { a = String } { b = String } buffer "toString" "UTF-8"
  pure contents

ext: idr

max_stars_repo_name: ostera/idris-coda

max_issues_repo_name: ostera/idris-coda

max_forks_repo_name: ostera/idris-coda


text:
-- ------------------------------------------------------------- [ Example.idr ]

module Data.ML.Example

import public Data.ML.Categorical

%access public export

-- --------------------------------------------- [ Categorical Feature Example ]

namespace Categorical

  exampleData : List String
  exampleData = [ "male",   "female", "male",   "male"
                , "female", "male",   "female", "female"
                ]

  ||| ```idris example
  ||| catToNum Categorical.exampleData
  ||| ```
  example : List (List Integer)
  example = catToNum Categorical.exampleData

-- --------------------------------------------------------- [ Titanic Example ]

namespace Titanic

  exampleData : List String
  exampleData = [ "C65", "", "E36", "C54", "B57 B59 B63 B66" ]

  -- TODO: record CabinFeature where

  ||| ```idris example
  ||| Titanic.example
  ||| ```
  example : List (Char, Integer, Nat)
  example = go . words <$> Titanic.exampleData
    where
      go : List String -> (Char, Integer, Nat)
      go []                                            = ('X', -1, 0)
      go (cabin :: cabins) with (strM cabin)
        go (""            :: cabins) | StrNil          = ('X', -1, 0)
        go (strCons c num :: cabins) | (StrCons c num) =
           ( c
           , cast num
           , S (length cabins)
           )

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

max_stars_repo_name: yurrriq/real-world-machine-learning

max_issues_repo_name: yurrriq/real-world-machine-learning

max_forks_repo_name: yurrriq/real-world-machine-learning


text:
import Language.JSON

someJSON : JSON
someJSON = JObject [
    ("a", JNull),
    ("b", JBoolean True),
    ("c", JNumber 1),
    ("d", JString "Hello, world"),
    ("e", JArray [JNull, JString "Lorem ipsum"]),
    ("f", JObject [("key", JString "value")])
  ]

main : IO ()
main = do
    putStrLn $ show someJSON
    putStrLn $ show @{Idris} someJSON
    putStrLn $ format 4 someJSON


text:
module Test.SemVar.ParserTest

import IdrTest.Test
import IdrTest.Expectation

import SemVar
import SemVar.Data
import SemVar.Parser

versionSpecs : List (String, Maybe Version)
versionSpecs =
  [
    (
      "1.2.3-prerelease+commit",
      Just (MkVersion 1 2 3 (Just "prerelease") (Just "commit"))
    ),
    (
      "1.2.3",
      Just (MkVersion 1 2 3 Nothing Nothing)
    )
  ]

-- TODO: Build a lot more examples from https://devhints.io/semver
-- TODO: Cover wildcards and partial ranges
reqSpecs : List (String, Maybe Requirement)
reqSpecs =
  [
    (
      "~1.2.3",
      Just (
        AND
          (GTE $ MkVersion 1 2 3 Nothing Nothing)
          (LT $ MkVersion 1 3 0 Nothing Nothing)
      )
    ),
    (
      "^1.2.3",
      Just (
        AND
          (GTE $ MkVersion 1 2 3 Nothing Nothing)
          (LT $ MkVersion 2 0 0 Nothing Nothing)
      )
    ),
    (
      "^0.2.3",
      Just (
        AND
          (GTE $ MkVersion 0 2 3 Nothing Nothing)
          (LT $ MkVersion 0 3 0 Nothing Nothing)
      )
    ),
    (
      "^0.0.1",
      Just (
        EQ $ MkVersion 0 0 1 Nothing Nothing
      )
    ),
    (
      "^1.2",
      Just (
        AND
          (GTE $ MkVersion 1 2 0 Nothing Nothing)
          (LT $ MkVersion 2 0 0 Nothing Nothing)
      )
    ),
    (
      "~1.2",
      Just (
        AND
          (GTE $ MkVersion 1 2 0 Nothing Nothing)
          (LT $ MkVersion 1 3 0 Nothing Nothing)
      )
    ),
    (
      "^1",
      Just (
        AND
          (GTE $ MkVersion 1 0 0 Nothing Nothing)
          (LT $ MkVersion 2 0 0 Nothing Nothing)
      )
    ),
    -- (
    --   "~1",
    --   Just (
    --     AND
    --       (GTE $ MkVersion 1 0 0 Nothing Nothing)
    --       (LT $ MkVersion 2 0 0 Nothing Nothing)
    --   )
    -- ),
    -- (
    --   "1.x",
    --   Just (
    --     AND
    --       (GTE $ MkVersion 1 0 0 Nothing Nothing)
    --       (LT $ MkVersion 2 0 0 Nothing Nothing)
    --   )
    -- ),
    -- (
    --   "1",
    --   Just (
    --     AND
    --       (GTE $ MkVersion 1 0 0 Nothing Nothing)
    --       (LT $ MkVersion 2 0 0 Nothing Nothing)
    --   )
    -- ),
    -- (
    --   "*",
    --   Just (
    --     GTE $ MkVersion 0 0 0 Nothing Nothing
    --   )
    -- ),
    -- (
    --   "x",
    --   Just (
    --     GTE $ MkVersion 0 0 0 Nothing Nothing
    --   )
    -- ),
    -- (
    --   "1.2.x",
    --   Just (
    --     AND
    --       (GTE $ MkVersion 1 2 0 Nothing Nothing)
    --       (LT $ MkVersion 1 3 0 Nothing Nothing)
    --   )
    -- ),
    -- (
    --   ">= 1.2.x",
    --   Just (
    --     GTE $ MkVersion 1 2 0 Nothing Nothing
    --   )
    -- ),
    -- (
    --   "<= 2.x",
    --   Just (
    --     LT $ MkVersion 3 0 0 Nothing Nothing
    --   )
    -- ),
    -- (
    --   "~1.2.x",
    --   Just (
    --     AND
    --       (GTE $ MkVersion 1 2 0 Nothing Nothing)
    --       (LT $ MkVersion 1 3 0 Nothing Nothing)
    --   )
    -- ),
    (
      "1.2.3",
      Just (
        EQ $ MkVersion 1 2 3 Nothing Nothing
      )
    ),
    (
      "=1.2.3",
      Just (
        EQ $ MkVersion 1 2 3 Nothing Nothing
      )
    ),
    (
      ">1.2.3",
      Just (
        GT $ MkVersion 1 2 3 Nothing Nothing
      )
    ),
    (
      "<1.2.3",
      Just (
        LT $ MkVersion 1 2 3 Nothing Nothing
      )
    ),
    (
      ">=1.2.3",
      Just (
        GTE $ MkVersion 1 2 3 Nothing Nothing
      )
    ),
    (
      "1.2.3 -  2.3.4",
      Just (
        AND
          (GTE $ MkVersion 1 2 3 Nothing Nothing)
          (LTE $ MkVersion 2 3 4 Nothing Nothing)
      )
    ),
    -- (
    --   "1.2.3 - 2.3",
    --   Just (
    --     AND
    --       (GTE $ MkVersion 1 2 3 Nothing Nothing)
    --       (LT $ MkVersion 2 4 0 Nothing Nothing)
    --   )
    -- ),
    -- (
    --   "1.2.3 - 2",
    --   Just (
    --     AND
    --       (GTE $ MkVersion 1 2 3 Nothing Nothing)
    --       (LT $ MkVersion 3 0 0 Nothing Nothing)
    --   )
    -- ),
    -- (
    --   "1.2 - 2.3.0",
    --   Just (
    --     AND
    --       (GTE $ MkVersion 1 2 0 Nothing Nothing)
    --       (LTE $ MkVersion 2 3 0 Nothing Nothing)
    --   )
    -- ),
    (
      ">=0.14 <16",
      Just (
        AND
          (GTE $ MkVersion 0 14 0 Nothing Nothing)
          (LT $ MkVersion 16 0 0 Nothing Nothing)
      )
    ),
    (
      "0.14.0 || 15.0.0",
      Just (
        OR
          (EQ $ MkVersion 0 14 0 Nothing Nothing)
          (EQ $ MkVersion 15 0 0 Nothing Nothing)
      )
    )
    -- (
    --   "0.14.x || 15.x.x",
    --   Just (
    --     OR
    --       (AND
    --         (GTE $ MkVersion 0 14 0 Nothing Nothing)
    --         (LT $ MkVersion 16 0 0 Nothing Nothing)
    --       )
    --       (AND
    --         (GTE $ MkVersion 0 14 0 Nothing Nothing)
    --         (LT $ MkVersion 16 0 0 Nothing Nothing)
    --       )
    --   )
    -- )
  ]

export
suite : Test
suite =
  let
    versionTests =
      map (\(text, result) =>
        test text (\_ => assertEq (parseVersion text) result)
      ) versionSpecs

    reqTests =
      map (\(text, result) =>
        test text (\_ => assertEq (parseRequirement text) result)
      ) reqSpecs
  in
    describe "Parser Tests"
      [ describe "Version Specs" versionTests
      , describe "Requirement Specs" reqTests
      ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Data.Time.Clock.System

import Data.Time.Clock.Internal.SystemTime
import Data.Time.Clock.Internal.UTCTime
import Data.Time.Clock.Internal.DiffTime
import Data.Time.Calendar.Days

-- | The day of the epoch of 'SystemTime', 1970-01-01
export
systemEpochDay: Day
systemEpochDay = MkModifiedJulianDay 40587

export
get_nano_res: Integer
get_nano_res = 1000000000

export
systemToUTCTime: SystemTime -> UTCTime
systemToUTCTime (MkSystemTime seconds nanoseconds) =
  let
    days = seconds `div` 86400
    day = addDays days systemEpochDay
    timeSeconds = seconds `mod` 86400
    -- TODO: Add nanoseconds
    --timeNanoseconds = timeSeconds * get_nano_res -- TODO: add nanoseconds + ()
    time = picosecondsToDiffTime (timeSeconds) -- * 1000)
  in
    MkUTCTime day time

-- TODO: Currently we do no capture nanoseconds, therefore coversion to System time looses precision
-- utcToSystemTime: UTCTime -> SystemTime
-- utcToSystemTime (MkUTCTime day diffTime) =
--   let
--     days = diffDays day systemEpochDay
--     timePicoSeconds = diffTimeToPicoseconds diffTime
--     timeNanoseconds = timePicoSeconds `div` 1000
--     timeSeconds = if timeNanoseconds >= 86400000000000 then 86399 else timeNanoseconds `div` get_nano_res
--     seconds = days * 86400 + timeSeconds
--   in
--     MkSystemTime seconds 0

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
test : Nat -> Int
test n =
  let c = if n == Z then 0 else 1
  in c


text:
decl syntax fun {n} ":" [ty] "=" [def]
            = n : ty
              n = def

decl syntax newtype {tname} "=" {conname} [tysyn]
     = data tname = conname tysyn

decl syntax EmptyShow {n} =
     implementation Show n where
        show x = "Nothing"

fun add : (Int -> Int -> Int) = \x, y => x + y

newtype Foo = MkFoo Int

EmptyShow Foo

main : IO ()
main = do printLn (MkFoo 42)
          printLn (add 3 4)

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module BiNat.Properties.Mult

import BiNat
import BiNat.Properties.Plus
import BiNat.Properties.Induction
import BiNat.Properties.LT

%access public export
%default total

multDashAddsAccMinusJ : (m, n : BiNat) -> (acc : BiNat) ->
  mult' m n acc = pred $ plus (mult' m n J) acc
multDashAddsAccMinusJ J         ns acc = rewrite plusJIsSucc ns in rewrite predOfSucc ns in Refl
multDashAddsAccMinusJ (ms -: O) ns acc = multDashAddsAccMinusJ ms (ns -: O) acc
multDashAddsAccMinusJ (ms -: I) ns acc =
  rewrite multDashAddsAccMinusJ ms (ns -: O) (plus' ns acc O []) in
  rewrite multDashAddsAccMinusJ ms (ns -: O) (plus' ns J O []) in
  rewrite plusAssociative (mult' ms (ns -: O) J) ns J in
  rewrite plusJIsSucc (plus' (mult' ms (ns -: O) J) ns O []) in
  rewrite predOfSucc (plus' (mult' ms (ns -: O) J) ns O []) in
  rewrite plusAssociative (mult' ms (ns -: O) J) ns acc in Refl

multDistributesPlusRight : (l, m, n : BiNat) -> mult l (plus m n) = plus (mult l m) (mult l n)
multDistributesPlusRight J m n =
  rewrite plusJIsSucc (plus' m n O []) in
  rewrite predOfSucc (plus' m n O []) in
  rewrite plusJIsSucc m in
  rewrite predOfSucc m in
  rewrite plusJIsSucc n in
  rewrite predOfSucc n in Refl
multDistributesPlusRight (ls -: O) m n =
  rewrite sym $ plusDashAppendsAcc m n O [O] in
  multDistributesPlusRight ls (m -: O) (n -: O)
multDistributesPlusRight (ls -: I) m n =
  rewrite plusJIsSucc (plus' m n O []) in
  rewrite multDashAddsAccMinusJ ls (plus' m n O [] -: O) (succ (plus' m n O [])) in
  rewrite predCommutesToPlusSnd (mult ls (plus m n -: O)) (succ (plus m n)) (succIsNotJ (plus m n)) in
  rewrite predOfSucc (plus m n) in
  rewrite sym $ plusDashAppendsAcc m n O [O] in
  rewrite plusJIsSucc m in
  rewrite plusJIsSucc n in
  rewrite multDashAddsAccMinusJ ls (m -: O) (succ m) in
  rewrite multDashAddsAccMinusJ ls (n -: O) (succ n) in
  rewrite predCommutesToPlusSnd (mult ls (m -: O)) (succ m) (succIsNotJ m) in
  rewrite predCommutesToPlusSnd (mult ls (n -: O)) (succ n) (succIsNotJ n) in
  rewrite predOfSucc m in
  rewrite predOfSucc n in
  rewrite sym $ plusAssociative (mult ls (m -: O)) m (plus (mult ls (n -: O)) n) in
  rewrite plusSymmetric m (plus (mult ls (n -: O)) n) in
  rewrite sym $ plusAssociative (mult ls (n -: O)) n m in
  rewrite plusSymmetric n m in
  rewrite plusAssociative (mult ls (m -: O)) (mult ls (n -: O)) (plus' m n O []) in
  rewrite multDistributesPlusRight ls (m -: O) (n -: O) in Refl

multJIsId : (n : BiNat) -> mult n J = n
multJIsId J = Refl
multJIsId (ns -: O) =
  rewrite multDistributesPlusRight ns J J in
  rewrite multJIsId ns in
  rewrite shiftLeftDoubles ns in Refl
multJIsId (ns -: I) =
  rewrite multDashAddsAccMinusJ ns (J -: O) (J -: O) in
  rewrite multDistributesPlusRight ns J J in
  rewrite multJIsId ns in
  rewrite sym $ shiftLeftDoubles ns in
  rewrite plusDashAppendsAcc ns J O [O] in
  rewrite plusJIsSucc ns in
  rewrite predOfDoubled (succ ns) (succIsNotJ ns) in
  rewrite predOfSucc ns in Refl

jMultIsId : (n : BiNat) -> mult J n = n
jMultIsId J = Refl
jMultIsId (ns -: O) = Refl
jMultIsId (ns -: I) =
  rewrite succDashAppendsAcc ns [O] in
  rewrite predOfDoubled (succ ns) (succIsNotJ ns) in
  rewrite predOfSucc ns in Refl

multDistributesPlusLeft : (l, m, n : BiNat) -> mult (plus l m) n = plus (mult l n) (mult m n)
multDistributesPlusLeft l m n =
  induction
    (\k => mult (plus l m) k = plus (mult l k) (mult m k))
    (\k, pk =>
      rewrite sym $ plusJIsSucc k in
      rewrite multDistributesPlusRight (plus' l m O []) k J in
      rewrite pk in
      rewrite multJIsId (plus' l m O []) in
      rewrite multDistributesPlusRight l k J in
      rewrite multDistributesPlusRight m k J in
      rewrite multJIsId l in
      rewrite multJIsId m in
      rewrite sym $ plusAssociative (mult l k) l (plus (mult m k) m) in
      rewrite plusSymmetric l (plus (mult m k) m) in
      rewrite sym $ plusAssociative (mult m k) m l in
      rewrite plusSymmetric m l in
      sym $ plusAssociative (mult l k) (mult m k) (plus l m)
    )
    (rewrite multJIsId (plus l m) in rewrite multJIsId l in rewrite multJIsId m in Refl)
    n

multOfSuccLeft : (m, n : BiNat) -> mult (succ m) n = plus n (mult m n)
multOfSuccLeft m n =
  rewrite sym $ jPlusIsSucc m in
  rewrite multDistributesPlusLeft J m n in
  rewrite plusJIsSucc n in
  rewrite predOfSucc n in Refl

multOfSuccRight : (m, n : BiNat) -> mult m (succ n) = plus (mult m n) m
multOfSuccRight m n =
  rewrite sym $ plusJIsSucc n in
  rewrite multDistributesPlusRight m n J in
  rewrite multJIsId m in Refl

multSymmetric : (m, n : BiNat) -> mult m n = mult n m
multSymmetric m n =
  induction
    (\k => mult k n = mult n k)
    (\k, pk =>
      rewrite sym $ plusJIsSucc k in
      rewrite multDistributesPlusLeft k J n in
      rewrite multDistributesPlusRight n k J in
      rewrite plusJIsSucc n in
      rewrite predOfSucc n in
      rewrite multJIsId n in
      rewrite pk in Refl
    )
    (
      rewrite plusJIsSucc n in
      rewrite predOfSucc n in
      rewrite multJIsId n in Refl
    )
    m

multAssociative : (l, m, n : BiNat) -> mult l (mult m n) = mult (mult l m) n
multAssociative l m n =
  induction
    (\k => mult k (mult m n) = mult (mult k m) n)
    (\k, pk =>
      rewrite sym $ plusJIsSucc k in
      rewrite multDistributesPlusLeft k J (mult m n) in
      rewrite jMultIsId (mult m n) in
      rewrite multDistributesPlusLeft k J m in
      rewrite jMultIsId m in
      rewrite multDistributesPlusLeft (mult k m) m n in
      rewrite pk in Refl
    )
    (
      rewrite jMultIsId (mult m n) in
      rewrite jMultIsId m in Refl
    )
    l

appendOIsTwice : (n : BiNat) -> n -: O = mult n (J -: O)
appendOIsTwice n =
  induction
    (\k => k -: O = mult k (J -: O))
    (\k, pk =>
      rewrite sym $ plusJIsSucc k in
      rewrite multDistributesPlusLeft k J (J -: O) in
      rewrite sym pk in
      sym $ plusDashAppendsAcc k J O [O]
    )
    Refl
    n

appendIIsTwicePlusJ : (n : BiNat) -> n -: I = plus (mult n (J -: O)) J
appendIIsTwicePlusJ n = rewrite sym $ appendOIsTwice n in Refl

multNKeepsLT : (l, m : BiNat) -> LT l m -> (n : BiNat) -> LT (mult l n) (mult m n)
multNKeepsLT l m lt n =
  induction
    (\k => LT (mult l k) (mult m k))
    (\k, pk =>
      rewrite sym $ plusJIsSucc k in
      rewrite multDistributesPlusRight l k J in
      rewrite multDistributesPlusRight m k J in
      rewrite multJIsId l in
      rewrite multJIsId m in
      lessThanTransitive
        (plusNKeepsLessThan (mult l k) (mult m k) pk l)
        (
          rewrite plusSymmetric (mult m k) l in
          rewrite plusSymmetric (mult m k) m in
          plusNKeepsLessThan l m lt (mult m k)
        )
    )
    (rewrite multJIsId l in rewrite multJIsId m in lt)
    n

max_stars_repo_name: SekiT/BiNat

max_issues_repo_name: SekiT/BiNat

max_forks_repo_name: SekiT/BiNat


text:
||| Prime, coprime, compositie types for `Nat`
||| Extremely slow, but it totally works.
module Extra.Nat.Prime

import Data.Fin
import Data.Nat
import Data.Nat.Factor
import Data.Nat.Order
import Data.Nat.Order.Properties
import Decidable.Decidable

||| A witness of two numbers being relatively prime
public export
data Coprime : Nat -> Nat -> Type where
  MkCoprime : GCD 1 a b -> Coprime a b

||| A witness of two numbers not being relatively prime
public export
data NotCoprime : Nat -> Nat -> Type where
  MkNotCoprime0 : GCD 0 a b -> NotCoprime a b
  MkNotCoprime2 : GCD (S (S n)) a b -> NotCoprime a b

||| Coprimality of two `Nat`s
public export
data Coprimality : Nat -> Nat -> Type where
  TheyAreCoprime : Coprime a b -> Coprimality a b
  TheyArentCoprime : NotCoprime a b -> Coprimality a b

||| Calculate the coprimality of two `Nat`s
public export
coprimality : (a : Nat) -> (b : Nat) -> {auto ok: NotBothZero a b} -> Coprimality a b
coprimality a b with (Data.Nat.Factor.gcd a b)
  coprimality a b | (0 ** gcd_a_b) = TheyArentCoprime (MkNotCoprime0 gcd_a_b)
  coprimality a b | (1 ** gcd_a_b) = TheyAreCoprime (MkCoprime gcd_a_b)
  coprimality a b | ((S (S n)) ** gcd_a_b) = TheyArentCoprime (MkNotCoprime2 gcd_a_b)

||| Check are two numbers coprime to each other
public export
isCoprime : (a : Nat) -> (b : Nat) -> {auto ok: NotBothZero a b} -> Bool
isCoprime a b =
  case coprimality a b {ok = ok} of
   TheyAreCoprime _ => True
   _ => False

||| A witness of a `Nat` being a compositie number
public export
data Composite : Nat -> Type where
  MkComposite : (x : Nat) -> LTE 2 x -> LT x n -> Factor x n -> Composite n

||| A witness of a `Nat` being a prime number
public export
data Prime : Nat -> Type where
  MkPrime : ((x : Nat) -> LTE 2 x -> LT x n -> NotFactor x n) -> Prime n

||| Primality of a `Nat`
public export
data Primality : Nat -> Type where
  ItIsPrime : Prime n -> Primality n
  ItIsComposite : Composite n -> Primality n

||| This module's pseudo prime
data PseudoPrime : Nat -> Nat -> Type where
  MkPseudoPrime : LTE 2 l -> LT l n -> ((x : Nat) -> LTE l x -> LT x n -> NotFactor x n) -> PseudoPrime l n

||| Constructs a trivial pseudo prime of a `Nat`
trivial : (n : Nat) -> LTE 2 n -> PseudoPrime n (S n)
trivial 0 lte_2_n = void $ absurd lte_2_n
trivial 1 lte_2_n = void $ absurd lte_2_n
trivial (S (S n)) lte_2_n = MkPseudoPrime lte_2_n lteRefl lemma
  where
  gamma : (k : Nat) -> S k = plus (mult k 1) 1
  gamma k =
    rewrite multOneRightNeutral k in
    rewrite plusCommutative k 1 in
    Refl
  lemma : (x : Nat) -> LTE (S (S n)) x -> LTE (S x) (S (S (S n))) -> NotFactor x (S (S (S n)))
  lemma x lte lte' =
    let ccc = LTEIsAntisymmetric (S (S n)) x lte (fromLteSucc lte') in
    rewrite sym ccc in
    ProperRemExists 1 0 (gamma (S (S n)))

||| Realize that a `PseudoPrime` is an actual `Prime`
realize : PseudoPrime 2 n -> Prime n
realize (MkPseudoPrime _ _ prf) = MkPrime prf

||| Strengthen a `PseudoPrime`, used to prove some other stuff
strengthen : {l : Nat} -> LTE 2 l -> PseudoPrime (S l) n -> NotFactor l n -> PseudoPrime l n
strengthen lte (MkPseudoPrime _ lt_l_n prf) notfactor_l_n = MkPseudoPrime lte (lteSuccLeft lt_l_n) lemma
  where
  lemma : (x : Nat) -> LTE l x -> LT x n -> NotFactor x n
  lemma x lte_l_x lt_x_n = case isLTE (S l) x of
    Yes lte_Sl_x => prf x lte_Sl_x lt_x_n
    No contra => rewrite (LTEIsAntisymmetric x l (fromLteSucc $ notlteIsLT (S l) x $ notLteIsnotlte (S l) x contra) lte_l_x) in notfactor_l_n

||| The prime number 2, proved manually
public export
prime2 : Prime 2
prime2 = MkPrime lemma
  where
  lemma : (x : Nat) -> LTE 2 x -> LT x 2 -> NotFactor x 2
  lemma 0 lte_2_0 _ = void $ absurd lte_2_0
  lemma 1 lte_2_1 _ = void $ absurd lte_2_1
  lemma (S (S n)) _ lt_2_n = void $ absurd lt_2_n

||| Calculates a `Nat`'s primality
public export
primality : (n : Nat) -> LTE 2 n -> Primality n
primality 0 lte_2_0 = void $ absurd lte_2_0
primality 1 lte_2_1 = void $ absurd lte_2_1
primality 2 lte_2_2 = ItIsPrime prime2
primality n@(S (S (S k))) lte_2_n = lemma (trivial (S (S k)) (LTESucc $ LTESucc $ LTEZero))
  where
  lemma : {x : Nat} -> PseudoPrime (S (S x)) (S (S (S k))) -> Primality (S (S (S k)))
  lemma {x = 0} p = ItIsPrime (realize p)
  lemma {x = (S y)} p@(MkPseudoPrime lte_2_x lte_x_n prf) =
    case decFactor (S (S (S k))) (S (S y)) of
      ItIsFactor factor => ItIsComposite $ MkComposite (S (S y)) (lteAddRight {m = y} 2) (lteSuccLeft lte_x_n) factor
      ItIsNotFactor not_factor => lemma (strengthen (lteAddRight {m = y} 2) p not_factor)

||| Check if a `Nat` is a prime number
public export
isPrime : (n : Nat) -> {auto okay : LTE 2 n} -> Bool
isPrime 1 = void $ absurd okay
isPrime (S (S n)) = case primality (S (S n)) okay of
  ItIsPrime _ => True
  ItIsComposite _ => False


text:
module Protocol.Hex

import Data.Bits
import Data.List

-- Those three imports are for compatibility and should be removed after release of 0.6.0
import Data.DPair
import Data.Nat
import Data.Fin

%default total

hexDigit : Bits64 -> Char
hexDigit 0 = '0'
hexDigit 1 = '1'
hexDigit 2 = '2'
hexDigit 3 = '3'
hexDigit 4 = '4'
hexDigit 5 = '5'
hexDigit 6 = '6'
hexDigit 7 = '7'
hexDigit 8 = '8'
hexDigit 9 = '9'
hexDigit 10 = 'a'
hexDigit 11 = 'b'
hexDigit 12 = 'c'
hexDigit 13 = 'd'
hexDigit 14 = 'e'
hexDigit 15 = 'f'
hexDigit _ = 'X' -- TMP HACK: Ideally we'd have a bounds proof, generated below

-- `i4` is to be replaced with a `4` literal after release of 0.6.0
namespace Old
  export
  i4 : Subset Nat (`LT` 64)
  i4 = Element (the Nat 4) %search
namespace New
  export
  i4 : Fin 64
  i4 = 4

||| Convert a Bits64 value into a list of (lower case) hexadecimal characters
export
asHex : Bits64 -> String
asHex 0 = "0"
asHex n = pack $ asHex' n []
  where
    asHex' : Bits64 -> List Char -> List Char
    asHex' 0 hex = hex
    asHex' n hex = asHex' (assert_smaller n (n `shiftR` i4)) (hexDigit (n .&. 0xf) :: hex)

export
leftPad : Char -> Nat -> String -> String
leftPad paddingChar padToLength str =
  if length str < padToLength
    then pack (List.replicate (minus padToLength (length str)) paddingChar) ++ str
    else str

export
fromHexDigit : Char -> Maybe Int
fromHexDigit '0' = Just 0
fromHexDigit '1' = Just 1
fromHexDigit '2' = Just 2
fromHexDigit '3' = Just 3
fromHexDigit '4' = Just 4
fromHexDigit '5' = Just 5
fromHexDigit '6' = Just 6
fromHexDigit '7' = Just 7
fromHexDigit '8' = Just 8
fromHexDigit '9' = Just 9
fromHexDigit 'a' = Just 10
fromHexDigit 'b' = Just 11
fromHexDigit 'c' = Just 12
fromHexDigit 'd' = Just 13
fromHexDigit 'e' = Just 14
fromHexDigit 'f' = Just 15
fromHexDigit _ = Nothing

export
fromHexChars : List Char -> Maybe Integer
fromHexChars = fromHexChars' 1
  where
    fromHexChars' : Integer -> List Char -> Maybe Integer
    fromHexChars' _ [] = Just 0
    fromHexChars' m (d :: ds)
      = do digit <- fromHexDigit (toLower d)
           digits <- fromHexChars' (m*16) ds
           pure $ cast digit * m + digits

export
fromHex : String -> Maybe Integer
fromHex = fromHexChars . unpack


text:
module Data.Compress.Utils.ConstantTable

import Data.Vect
import Data.Fin
import Data.IOArray.Prims
import PrimIO

||| A constant table that can be read in O(1) time
export
data ConstantTable : Nat -> Type -> Type where
  MkFromArray : ArrayData e -> ConstantTable (S n) e

export
length : {n : Nat} -> ConstantTable n e -> Nat
length _ = n

export
index : Fin (S n) -> ConstantTable (S n) a -> a
index n (MkFromArray array) = unsafePerformIO $ primIO $ prim__arrayGet array (cast $ finToInteger n)

export
index_bits8 : Bits8 -> ConstantTable 256 a -> a
index_bits8 n (MkFromArray array) = unsafePerformIO $ primIO $ prim__arrayGet array (cast n)

export
from_vect : {n : Nat} -> Vect (S n) a -> ConstantTable (S n) a
from_vect (x :: xs) = unsafePerformIO $ do
  array <- primIO $ prim__newArray (cast (S n)) x
  let indexed_array = zip (drop 1 Fin.range) xs
  traverse_ (\(i,v) => primIO $ prim__arraySet array (cast $ finToInteger i) v) indexed_array
  pure $ MkFromArray array


text:
module Language.LSP.Message.Moniker

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
public export
record MonikerClientCapabilities where
  constructor MkMonikerClientCapabilities
  dynamicRegistration : Maybe Bool
%runElab deriveJSON defaultOpts `{{MonikerClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
public export
record MonikerOptions where
  constructor MkMonikersOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{{MonikerOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
public export
record MonikerRegistrationOptions where
  constructor MkMonikersRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
%runElab deriveJSON defaultOpts `{{MonikerRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
public export
record MonikerParams where
  constructor MkMonikersParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
  position           : Position
%runElab deriveJSON defaultOpts `{{MonikerParams}}

namespace UniquenessLevel
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
  public export
  data UniquenessLevel = Document | Project | Group | Scheme | Global

export
ToJSON UniquenessLevel where
  toJSON Document = JString "document"
  toJSON Project = JString "project"
  toJSON Group = JString "group"
  toJSON Scheme = JString "scheme"
  toJSON Global = JString "global"

export
FromJSON UniquenessLevel where
  fromJSON (JString "document") = pure Document
  fromJSON (JString "project") = pure Project
  fromJSON (JString "group") = pure Group
  fromJSON (JString "scheme") = pure Scheme
  fromJSON (JString "global") = pure Global
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
namespace MonikerKind
  public export
  data MonikerKind = Import | Export | Local

export
ToJSON MonikerKind where
  toJSON Import = JString "import"
  toJSON Export = JString "export"
  toJSON Local  = JString "local"

export
FromJSON MonikerKind where
  fromJSON (JString "import") = pure Import
  fromJSON (JString "export") = pure Export
  fromJSON (JString "local")  = pure Local
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_moniker
public export
record Moniker where
  constructor MkMoniker
  scheme     : String
  identifier : String
  unique     : UniquenessLevel
  kind       : Maybe MonikerKind
%runElab deriveJSON defaultOpts `{{Moniker}}


text:
> module Nat.CoprimeProperties

> import Nat.Coprime
> import Nat.GCD
> import Nat.GCDOperations
> import Nat.GCDProperties
> import Nat.Divisor
> import Nat.DivisorOperations
> import Nat.DivisorProperties
> import Nat.OperationsProperties
> import Nat.GCDAlgorithm
> import Nat.GCDEuclid
> import Pairs.Operations
> import Sigma.Sigma

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

> ||| Coprime is decidable
> decCoprime : (m : Nat) -> (n : Nat) -> Dec (Coprime m n)
> decCoprime m n with (decEq (gcdAlg m n) (S Z))
>   | (Yes p) = Yes (MkCoprime p)
>   | (No contra) = No contra' where
>         contra' : Coprime m n -> Void
>         contra' (MkCoprime p) = contra p
> %freeze decCoprime

> ||| Coprime is symmetric
> symmetricCoprime : Coprime m n -> Coprime n m
> symmetricCoprime {m} {n} (MkCoprime prf) = MkCoprime (trans (gcdAlgCommutative n m) prf)
> %freeze symmetricCoprime

> ||| Any number is coprime with one
> anyCoprimeOne : Coprime m (S Z)
> anyCoprimeOne {m} = MkCoprime s3 where
>   s1 : (gcdAlg m (S Z)) `Divisor` (S Z)
>   s1 = gcdDivisorSnd (gcdAlgLemma m (S Z))
>   s2 : (S Z ) `Divisor` (gcdAlg m (S Z))
>   s2 = oneDivisorAny (gcdAlg m (S Z))
>   s3 : gcdAlg m (S Z) = S Z
>   s3 = divisorAntisymmetric (gcdAlg m (S Z)) (S Z) s1 s2
> %freeze anyCoprimeOne

> ||| Division by gcd yields coprime numbers
> gcdCoprimeLemma : (d : Nat) -> (m : Nat) -> (n : Nat) ->
>                   (dDm : d `Divisor` m) -> (dDn : d `Divisor` n) ->
>                   Z `LT` d -> GCD d m n -> Coprime (quotient m d dDm) (quotient n d dDn)
> gcdCoprimeLemma d m n dDm dDn zLTd dGCDmn =
>   let m'         :  Nat
>                  =  quotient m d dDm in
>   let n'         :  Nat
>                  =  quotient n d dDn in
>   let d'         :  Nat
>                  =  gcdAlg m' n' in
>   let d'GCDm'n'  :  (GCD d' m' n')
>                  =  gcdAlgLemma m' n' in
>   let d'Dm'      :  (d' `Divisor` m')
>                  =  gcdDivisorFst d'GCDm'n' in
>   let d'Dn'      :  (d' `Divisor` n')
>                  =  gcdDivisorSnd d'GCDm'n' in
>   let oneDd'     :  ((S Z) `Divisor` d')
>                  =  oneDivisorAny d' in
>   let d'Done     :  (d' `Divisor` (S Z))
>                  =  gcdLemma'' d m n dDm dDn dGCDmn zLTd d' d'Dm' d'Dn' in
>   let d'EQone    :  (d' = (S Z))
>                  =  divisorAntisymmetric d' (S Z) d'Done oneDd' in
>   MkCoprime d'EQone
> %freeze gcdCoprimeLemma

> {-

> ||| Division by gcd yields coprime numbers
> gcdCoprimeLemma : (v : GCD (S d) m n) -> Coprime (quotient m (S d) (gcdDivisorFst v))
>                                                  (quotient n (S d) (gcdDivisorSnd v))
> gcdCoprimeLemma {d} {m} {n} v = MkCoprime (MkGCD d'Dm' d'Dn' d'G) Refl where
>   dDm     : (S d) `Divisor` m
>   dDm     = gcdDivisorFst v
>   dDn     : (S d) `Divisor` n
>   dDn     = gcdDivisorSnd v
>   m'      : Nat
>   m'      = quotient m (S d) dDm
>   n'      : Nat
>   n'      = quotient n (S d) dDn
>   d'Dm'   : S Z `Divisor` m'
>   d'Dm'   = oneDivisorAny m'
>   d'Dn'   : S Z `Divisor` n'
>   d'Dn'   = oneDivisorAny n'
>   d'G     : (d'' : Nat) -> d'' `Divisor` m' -> d'' `Divisor` n' -> d'' `Divisor` (S Z)
>   d'G d'' = gcdLemma v
> %freeze gcdCoprimeLemma

> ||| Division by gcd yields coprime numbers
> gcdCoprimeLemma' : (v : GCD d m n) -> Not (d = Z) -> Coprime (quotient m d (gcdDivisorFst v))
>                                                              (quotient n d (gcdDivisorSnd v))
> gcdCoprimeLemma' {d} {m} {n} v dNotZ = MkCoprime (MkGCD d'Dm' d'Dn' d'G) Refl where
>   dDm     : d `Divisor` m
>   dDm     = gcdDivisorFst v
>   dDn     : d `Divisor` n
>   dDn     = gcdDivisorSnd v
>   m'      : Nat
>   m'      = quotient m d dDm
>   n'      : Nat
>   n'      = quotient n d dDn
>   d'Dm'   : S Z `Divisor` m'
>   d'Dm'   = oneDivisorAny m'
>   d'Dn'   : S Z `Divisor` n'
>   d'Dn'   = oneDivisorAny n'
>   d'G     : (d'' : Nat) -> d'' `Divisor` m' -> d'' `Divisor` n' -> d'' `Divisor` (S Z)
>   d'G d'' = gcdLemma' v dNotZ
> %freeze gcdCoprimeLemma'

> ||| Division by gcd yields coprime numbers
> gcdCoprimeLemma'' : (v : GCD d m n) -> Z `LT` d -> Coprime (quotient m d (gcdDivisorFst v))
>                                                            (quotient n d (gcdDivisorSnd v))
> gcdCoprimeLemma'' {d} {m} {n} v zLTd = MkCoprime (MkGCD d'Dm' d'Dn' d'G) Refl where
>   dDm     : d `Divisor` m
>   dDm     = gcdDivisorFst v
>   dDn     : d `Divisor` n
>   dDn     = gcdDivisorSnd v
>   m'      : Nat
>   m'      = quotient m d dDm
>   n'      : Nat
>   n'      = quotient n d dDn
>   d'Dm'   : S Z `Divisor` m'
>   d'Dm'   = oneDivisorAny m'
>   d'Dn'   : S Z `Divisor` n'
>   d'Dn'   = oneDivisorAny n'
>   dNotZ   : Not (d = Z)
>   dNotZ   = gtZisnotZ zLTd
>   d'G     : (d'' : Nat) -> d'' `Divisor` m' -> d'' `Divisor` n' -> d'' `Divisor` (S Z)
>   d'G d'' = gcdLemma' v dNotZ
> %freeze gcdCoprimeLemma''

GCD / Coprime properties:

> |||
> gcdOneCoprimeLemma1 : (alg : (a : Nat) -> (b : Nat) -> (d : Nat ** GCD d a b)) ->
>                       (m : Nat) -> (n : Nat) ->
>                       gcd (alg m n) = S Z -> Coprime m n
> gcdOneCoprimeLemma1 alg m n prf = MkCoprime (getProof (alg m n)) prf
> %freeze gcdOneCoprimeLemma1

> |||
> gcdOneCoprimeLemma2 : (m : Nat) -> (n : Nat) ->
>                       (alg : (a : Nat) -> (b : Nat) -> (d : Nat ** GCD d a b)) ->
>                       Coprime m n -> gcd (alg m n) = S Z
> gcdOneCoprimeLemma2 m n alg (MkCoprime {d} v prf) = s3 where
>   s1 : d = S Z
>   s1 = prf
>   s2 : gcd (alg m n) = d
>   s2 = gcdUnique (gcd (alg m n)) d (getProof (alg m n)) v
>   s3 : gcd (alg m n) = S Z
>   s3 = trans s2 s1
> %freeze gcdOneCoprimeLemma2

> |||
> gcdAnyOneOne : (alg : (a : Nat) -> (b : Nat) -> (d : Nat ** GCD d a b)) ->
>                (m : Nat) ->
>                gcd (alg m (S Z)) = S Z
> gcdAnyOneOne alg m = gcdOneCoprimeLemma2 m (S Z) alg anyCoprimeOne
> %freeze gcdAnyOneOne

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Compiler.LLVM.Rapid.Builtin

import Data.Vect
import System.Info

import Core.Name

import Compiler.LLVM.IR
import Compiler.LLVM.Instruction
import Compiler.LLVM.Rapid.Foreign
import Compiler.LLVM.Rapid.Object
import Control.Codegen
import Data.Utils
import Rapid.Common

-- we provide our own in Data.Utils
%hide Core.Name.Namespace.showSep

mk_prim__bufferNew : Vect 2 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferNew [sizeObj, _] = do
  size <- unboxInt' sizeObj
  -- TODO: safety check: size < 2^32
  hdrValue <- mkHeader OBJECT_TYPE_ID_BUFFER !(mkTrunc size)
  newObj <- dynamicAllocate size
  putObjectHeader newObj hdrValue
  pure newObj

mk_prim__bufferSize : Vect 1 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferSize [arg0] = do
  hdr <- getObjectHeader arg0
  size <- mkAnd hdr (ConstI64 0xffffffff)
  sizeInt <- cgMkInt size
  pure sizeInt

mk_prim__bufferGetByte : Vect 3 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferGetByte [buf, offsetObj, _] = do
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset
  byte <- load bytePtr
  val <- mkZext {to=I64} byte
  cgMkInt val

mk_prim__bufferSetByte : Vect 4 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferSetByte [buf, offsetObj, valObj, _] = do
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset
  val <- mkTrunc {to=I8} !(unboxInt' valObj)
  store val bytePtr
  mkUnit

mk_prim__bufferGetDouble : Vect 3 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferGetDouble [buf, offsetObj, _] = do
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset
  doublePtr <- bitcastA {n=1} bytePtr
  val <- load doublePtr
  cgMkDouble val

mk_prim__bufferSetDouble : Vect 4 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferSetDouble [buf, offsetObj, valObj, _] = do
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset
  doublePtr <- bitcastA {n=1} bytePtr
  val <- unboxFloat64' valObj
  store val doublePtr
  mkUnit

mk_prim__bufferGetInt : Vect 3 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferGetInt [buf, offsetObj, _] = do
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset
  intPtr <- bitcastA {to=I64} {n=1} bytePtr
  val <- load intPtr
  cgMkInt val

mk_prim__bufferGetInt32 : Vect 3 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferGetInt32 [buf, offsetObj, _] = do
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset
  intPtr <- bitcastA {to=I32} {n=1} bytePtr
  val32 <- load intPtr
  val <- mkZext val32
  cgMkInt val

mk_prim__bufferSetInt : Vect 4 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferSetInt [buf, offsetObj, valObj, _] = do
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset
  intPtr <- bitcastA {to=I64} {n=1} bytePtr
  val <- unboxInt' valObj
  store val intPtr
  mkUnit

mk_prim__bufferSetInt32 : Vect 4 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferSetInt32 [buf, offsetObj, valObj, _] = do
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset
  intPtr <- bitcastA {to=I32} {n=1} bytePtr
  val <- mkTrunc {to=I32} !(unboxInt' valObj)
  store val intPtr
  mkUnit

mk_prim__bufferGetBits16 : Vect 3 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferGetBits16 [buf, offsetObj, _] = do
  -- TODO: this assumes little-endian target architecture
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset
  bitsPtr <- bitcastA {to=I16} {n=1} bytePtr
  valRaw <- load bitsPtr
  val <- mkZext valRaw
  cgMkInt val

mk_prim__bufferSetBits16 : Vect 4 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferSetBits16 [buf, offsetObj, valObj, _] = do
  -- TODO: this assumes little-endian target architecture
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset
  bitsPtr <- bitcastA {to=I16} {n=1} bytePtr
  val <- mkTrunc {to=I16} !(unboxInt' valObj)
  store val bitsPtr
  mkUnit

mk_prim__bufferGetString : Vect 4 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferGetString [buf, offsetObj, lengthObj, _] = do
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  length <- unboxInt' lengthObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset

  newStr <- dynamicAllocate length
  newHeader <- mkHeader OBJECT_TYPE_ID_STR !(mkTrunc length)
  putObjectHeader newStr newHeader
  strPayload <- getObjectPayloadAddr {t=I8} newStr
  appendCode $ "  call void @llvm.memcpy.p1i8.p1i8.i64(" ++ toIR strPayload ++ ", " ++ toIR bytePtr ++ ", " ++ toIR length ++ ", i1 false)"
  pure newStr

mk_prim__bufferSetString : Vect 4 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferSetString [buf, offsetObj, valObj, _] = do
  -- TODO: size check in safe mode
  --hdr <- getObjectHeader buf
  --size <- mkAnd hdr (ConstI64 0xffffffff)
  offset <- unboxInt' offsetObj
  payloadStart <- getObjectPayloadAddr {t=I8} buf
  bytePtr <- getElementPtr payloadStart offset
  strLength <- mkZext {to=I64} !(getStringByteLength valObj)
  strPayload <- getObjectPayloadAddr {t=I8} valObj
  appendCode $ "  call void @llvm.memcpy.p1i8.p1i8.i64(" ++ toIR bytePtr ++ ", " ++ toIR strPayload ++ ", " ++ toIR strLength ++ ", i1 false)"
  mkUnit

mk_prim__bufferCopyData : Vect 6 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__bufferCopyData [src, startObj, lenObj, dest, locObj, _] = do
  start <- unboxInt' startObj
  len <- unboxInt' lenObj
  srcPayloadStart <- getObjectPayloadAddr {t=I8} src
  srcPtr <- getElementPtr srcPayloadStart start

  loc <- unboxInt' locObj
  dstPayloadStart <- getObjectPayloadAddr {t=I8} dest
  dstPtr <- getElementPtr dstPayloadStart loc

  appendCode $ "  call void @llvm.memmove.p1i8.p1i8.i64(" ++ toIR dstPtr ++ ", " ++ toIR srcPtr ++ ", " ++ toIR len ++ ", i1 false)"
  mkUnit

mk_prim__nullAnyPtr : Vect 1 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__nullAnyPtr [p] = do
  lblStart <- genLabel "nullAnyPtr_start"
  lblInside <- genLabel "nullAnyPtr_inside"
  lblEnd <- genLabel "nullAnyPtr_end"

  jump lblStart
  beginLabel lblStart

  ptrObjIsZero <- SSA I1 <$> assignSSA ("call fastcc i1 @rapid.ptrisnull(" ++ toIR p ++ ")")
  branch ptrObjIsZero lblEnd lblInside

  beginLabel lblInside
  payload <- getObjectSlot {t=I64} p 0
  payloadIsZero <- icmp "eq" (ConstI64 0) payload

  jump lblEnd

  beginLabel lblEnd
  isNullPtr <- phi [(ptrObjIsZero, lblStart), (payloadIsZero, lblInside)]
  result <- cgMkInt !(mkZext isNullPtr)
  pure result

mk_prim__getString : Vect 1 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__getString [p] = do
  assertObjectType' p OBJECT_TYPE_ID_POINTER
  payload <- getObjectSlot {t=IRObjPtr} p 0
  assertObjectType' payload OBJECT_TYPE_ID_STR
  pure payload

mk_prim__noop2 : Vect 2 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__noop2 [_, _] = do
  mkUnit

mk_prim__currentDir : Vect 1 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__currentDir [_] = do
  dummy <- mkStr "/tmp"
  newPtr <- dynamicAllocate (Const I64 8)
  putObjectHeader newPtr (constHeader OBJECT_TYPE_ID_POINTER 0)
  putObjectSlot newPtr (Const I64 0) dummy
  pure newPtr

mk_prelude_fastPack : Vect 1 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prelude_fastPack [charListObj] = do
  newObj <- foreignCall {t=IRObjPtr} "@rapid_fast_pack" [toIR charListObj]
  pure newObj

mk_prelude_fastAppend : Vect 1 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prelude_fastAppend [stringListObj] = do
  newObj <- foreignCall {t=IRObjPtr} "@rapid_fast_append" [toIR stringListObj]
  pure newObj

TAG_LIST_NIL : IRValue I32
TAG_LIST_NIL = Const I32 0
TAG_LIST_CONS : IRValue I32
TAG_LIST_CONS = Const I32 1

mk_prelude_fastUnpack : Vect 1 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prelude_fastUnpack [strObj] = do
  nilHdr <- mkHeader OBJECT_TYPE_ID_CON_NO_ARGS TAG_LIST_NIL
  nilObj <- dynamicAllocate (Const I64 0)
  putObjectHeader nilObj nilHdr

  startLbl <- genLabel "start"
  returnLbl <- genLabel "ret"
  loopInitLbl <- genLabel "li"
  loopStartLbl <- genLabel "ls"
  loopBodyLbl <- genLabel "ls"
  loopEndLbl <- genLabel "le"

  jump startLbl
  beginLabel startLbl

  stringByteLength <- getStringByteLength strObj
  isEmpty <- icmp "eq" stringByteLength (Const I32 0)
  branch isEmpty returnLbl loopInitLbl

  beginLabel loopInitLbl
  resultObj <- dynamicAllocate (Const I64 16)
  putObjectHeader resultObj !(mkHeader (OBJECT_TYPE_ID_CON_NO_ARGS + 0x200) TAG_LIST_CONS)
  payload0 <- getObjectPayloadAddr {t=I8} strObj
  jump loopStartLbl

  beginLabel loopStartLbl
  nextBytePos <- SSA I32 <$> mkVarName "%nI."
  nextTail <- SSA IRObjPtr <$> mkVarName "%nT."
  bytePos <- phi [((Const I32 0), loopInitLbl), (nextBytePos, loopBodyLbl)]
  currentTail <- phi [(resultObj, loopInitLbl), (nextTail, loopBodyLbl)]

  payload <- getElementPtr payload0 bytePos
  decodedRaw <- call {t=I64} "ccc" "@utf8_decode1_length" [toIR payload]
  charVal <- mkTrunc {to=I32} decodedRaw
  decodedLength <- mkTrunc {to=I32} !(mkShiftR decodedRaw (Const I64 32))
  ch <- cgMkChar charVal
  putObjectSlot currentTail (Const I64 0) ch

  appendCode $ (showWithoutType nextBytePos) ++ " = add " ++ toIR bytePos ++ ", " ++ showWithoutType decodedLength

  finished <- icmp "uge" nextBytePos stringByteLength
  branch finished loopEndLbl loopBodyLbl

  beginLabel loopBodyLbl

  gc <- gcFlavour <$> getOpts
  dynamicAllocateInto gc (showWithoutType nextTail) (Const I64 16)
  putObjectHeader nextTail !(mkHeader (OBJECT_TYPE_ID_CON_NO_ARGS + 0x200) TAG_LIST_CONS)
  putObjectSlot currentTail (Const I64 1) nextTail

  jump loopStartLbl

  beginLabel loopEndLbl
  putObjectSlot currentTail (Const I64 1) nilObj
  jump returnLbl

  beginLabel returnLbl
  phi [(nilObj, startLbl), (resultObj, loopEndLbl)]

TAG_UNCONS_RESULT_EOF : IRValue I32
TAG_UNCONS_RESULT_EOF = Const I32 0
TAG_UNCONS_RESULT_CHARACTER : IRValue I32
TAG_UNCONS_RESULT_CHARACTER = Const I32 1

mk_prim__stringIteratorNew : Vect 1 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__stringIteratorNew [strObj] = do
  iterObj <- cgMkInt (Const I64 0)
  pure iterObj

mk_prim__stringIteratorNext : Vect 2 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__stringIteratorNext [strObj, iteratorObj] = do
  offset <- unboxInt' iteratorObj
  strLength <- mkZext !(getStringByteLength strObj)
  mkIf (icmp "uge" offset strLength) (do
       eofObj <- dynamicAllocate (Const I64 0)
       hdr <- mkHeader OBJECT_TYPE_ID_CON_NO_ARGS TAG_UNCONS_RESULT_EOF
       putObjectHeader eofObj hdr
       pure eofObj
    ) (do
       resultObj <- dynamicAllocate (Const I64 16)
       hdrWithoutSize <- mkHeader OBJECT_TYPE_ID_CON_NO_ARGS TAG_UNCONS_RESULT_CHARACTER
       hdr <- mkOr hdrWithoutSize (Const I64 (2 `prim__shl_Integer` 40))
       putObjectHeader resultObj hdr

       payload0 <- getObjectPayloadAddr {t=I8} strObj
       payload <- getElementPtr payload0 offset

       decodedRaw <- call {t=I64} "ccc" "@utf8_decode1_length" [toIR payload]
       charVal <- mkTrunc {to=I32} decodedRaw
       decodedLength <- mkTrunc {to=I32} !(mkShiftR decodedRaw (Const I64 32))

       charObj <- cgMkChar charVal
       putObjectSlot resultObj (Const I64 0) charObj

       newOffset <- mkAdd !(mkZext decodedLength) offset
       newIter <- cgMkInt newOffset
       putObjectSlot resultObj (Const I64 1) newIter
       pure resultObj
    )

-- Needs to be kept in sync with time.c:
CLOCK_TYPE_UTC : Int
CLOCK_TYPE_UTC = 1
CLOCK_TYPE_MONOTONIC : Int
CLOCK_TYPE_MONOTONIC = 2
CLOCK_TYPE_DURATION : Int
CLOCK_TYPE_DURATION = 3
CLOCK_TYPE_PROCESS : Int
CLOCK_TYPE_PROCESS = 4
CLOCK_TYPE_THREAD : Int
CLOCK_TYPE_THREAD = 5
CLOCK_TYPE_GCCPU : Int
CLOCK_TYPE_GCCPU = 6
CLOCK_TYPE_GCREAL : Int
CLOCK_TYPE_GCREAL = 7

mk_prim__readTime : Int -> Vect 1 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__readTime clockType [_] = do
  clock <- dynamicAllocate (Const I64 16)
  hdr <- mkHeader OBJECT_TYPE_ID_CLOCK (Const I32 0)
  putObjectHeader clock hdr

  r <- foreignCall {t=I32} "@rapid_clock_read" [toIR clock, "i32 " ++ show clockType]

  pure clock

mk_prim__clockSecond : Vect 2 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__clockSecond [clockObj, _] = do
  secondsAddr <- getObjectSlotAddrVar {t=I64} clockObj (Const I64 0)
  seconds <- cgMkBits64 !(load secondsAddr)
  pure seconds

mk_prim__clockNanoSecond : Vect 2 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__clockNanoSecond [clockObj, _] = do
  nanoSecondsAddr <- getObjectSlotAddrVar {t=I64} clockObj (Const I64 1)
  nanoSeconds <- cgMkBits64 !(load nanoSecondsAddr)
  pure nanoSeconds

mk_prim__clockIsValid : Vect 2 (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mk_prim__clockIsValid [clockObj, _] = do
  -- clock objects store either "1" or "0" in the size field as validity flag
  valid <- cgMkInt !(mkZext !(getObjectSize clockObj))
  pure valid

export
builtinPrimitives : List (String, (n : Nat ** (Vect n (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr))))
builtinPrimitives = [
    ("prim/blodwen-new-buffer", (2 ** mk_prim__bufferNew))
  , ("prim/blodwen-buffer-size", (1 ** mk_prim__bufferSize))
  , ("prim/blodwen-buffer-setbyte", (4 ** mk_prim__bufferSetByte))
  , ("prim/blodwen-buffer-getbyte", (3 ** mk_prim__bufferGetByte))
  , ("prim/blodwen-buffer-setbits16", (4 ** mk_prim__bufferSetBits16))
  , ("prim/blodwen-buffer-getbits16", (3 ** mk_prim__bufferGetBits16))
  , ("prim/blodwen-buffer-setint32", (4 ** mk_prim__bufferSetInt32))
  , ("prim/blodwen-buffer-getint32", (3 ** mk_prim__bufferGetInt32))
  , ("prim/blodwen-buffer-setint", (4 ** mk_prim__bufferSetInt))
  , ("prim/blodwen-buffer-getint", (3 ** mk_prim__bufferGetInt))
  , ("prim/blodwen-buffer-setdouble", (4 ** mk_prim__bufferSetDouble))
  , ("prim/blodwen-buffer-getdouble", (3 ** mk_prim__bufferGetDouble))
  , ("prim/blodwen-buffer-setstring", (4 ** mk_prim__bufferSetString))
  , ("prim/blodwen-buffer-getstring", (4 ** mk_prim__bufferGetString))
  , ("prim/blodwen-buffer-copydata", (6 ** mk_prim__bufferCopyData))

  , ("prim/string-concat", (1 ** mk_prelude_fastAppend))
  , ("prim/string-pack", (1 ** mk_prelude_fastPack))
  , ("prim/string-unpack", (1 ** mk_prelude_fastUnpack))

  , ("prim/blodwen-string-iterator-new", (1 ** mk_prim__stringIteratorNew))
  , ("prim/blodwen-string-iterator-next", (2 ** mk_prim__stringIteratorNext))
  --, ("prim/blodwen-string-iterator-to-string", (4 ** mk_prim__stringIteratorToString))

  , ("prim/blodwen-clock-time-utc", (1 ** mk_prim__readTime CLOCK_TYPE_UTC))
  , ("prim/blodwen-clock-time-monotonic", (1 ** mk_prim__readTime CLOCK_TYPE_MONOTONIC))
  , ("prim/blodwen-clock-time-duration", (1 ** mk_prim__readTime CLOCK_TYPE_DURATION))
  , ("prim/blodwen-clock-time-process", (1 ** mk_prim__readTime CLOCK_TYPE_PROCESS))
  , ("prim/blodwen-clock-time-thread", (1 ** mk_prim__readTime CLOCK_TYPE_THREAD))
  , ("prim/blodwen-clock-time-gccpu", (1 ** mk_prim__readTime CLOCK_TYPE_GCCPU))
  , ("prim/blodwen-clock-time-gcreal", (1 ** mk_prim__readTime CLOCK_TYPE_GCREAL))

  , ("prim/blodwen-clock-second", (2 ** mk_prim__clockSecond))
  , ("prim/blodwen-clock-nanosecond", (2 ** mk_prim__clockNanoSecond))
  , ("prim/blodwen-is-time", (2 ** mk_prim__clockIsValid))

  , ("prim/isNull", (1 ** mk_prim__nullAnyPtr))
  , ("prim/getString", (1 ** mk_prim__getString))
  , ("prim/noop2", (2 ** mk_prim__noop2))
  ]

compileExtPrimFallback : Name -> List (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
compileExtPrimFallback n args =
  do hp <- ((++) "%RuntimePtr ") <$> assignSSA "load %RuntimePtr, %RuntimePtr* %HpVar"
     hpLim <- ((++) "%RuntimePtr ") <$> assignSSA "load %RuntimePtr, %RuntimePtr* %HpLimVar"
     let base = "%TSOPtr %BaseArg"
     result <- assignSSA $ "call fastcc %Return1 @_extprim_" ++ (safeName n) ++ "(" ++ showSep ", " (hp::base::hpLim::(map toIR args)) ++ ")"

     newHp <- assignSSA $ "extractvalue %Return1 " ++ result ++ ", 0"
     appendCode $ "store %RuntimePtr " ++ newHp ++ ", %RuntimePtr* %HpVar"
     newHpLim <- assignSSA $ "extractvalue %Return1 " ++ result ++ ", 1"
     appendCode $ "store %RuntimePtr " ++ newHpLim ++ ", %RuntimePtr* %HpLimVar"
     returnValue <- SSA IRObjPtr <$> assignSSA ("extractvalue %Return1 " ++ result ++ ", 2")
     pure returnValue

export
compileExtPrim : Name -> List (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
compileExtPrim (NS ns n) args with (unsafeUnfoldNamespace ns)
  compileExtPrim (NS ns (UN $ Basic "prim__newArray")) [_, countArg, elemArg, _] | ["Prims", "IOArray", "Data"] = do
    lblStart <- genLabel "new_array_init_start"
    lblLoop <- genLabel "new_array_init_loop"
    lblEnd <- genLabel "new_array_init_end"
    count <- unboxInt' countArg
    size <- mkMul (Const I64 8) count
    newObj <- dynamicAllocate size
    hdr <- mkHeader OBJECT_TYPE_ID_IOARRAY !(mkTrunc count)
    putObjectHeader newObj hdr
    jump lblStart
    beginLabel lblStart

    jump lblLoop
    beginLabel lblLoop
    iPlus1name <- mkVarName "%iplus1."
    let iPlus1 = SSA I64 iPlus1name
    i <- phi [(Const I64 0, lblStart), (iPlus1, lblLoop)]

    addr <- getObjectSlotAddrVar newObj i
    store elemArg addr

    appendCode $ iPlus1name ++ " = add " ++ toIR i ++ ", 1"
    continue <- icmp "ult" iPlus1 count
    branch continue lblLoop lblEnd
    beginLabel lblEnd
    pure newObj

  compileExtPrim (NS ns (UN $ Basic "prim__arrayGet")) [_, array, indexArg, _] | ["Prims", "IOArray", "Data"] = do
    index <- unboxInt' indexArg
    addr <- getObjectSlotAddrVar array index
    load addr

  compileExtPrim (NS ns (UN $ Basic "prim__arraySet")) [_, array, indexArg, val, _] | ["Prims", "IOArray", "Data"] = do
    index <- unboxInt' indexArg
    addr <- getObjectSlotAddrVar array index
    store val addr
    mkUnit

  compileExtPrim (NS ns (UN $ Basic "prim__codegen")) [] | ["Info", "System"] = do
    mkStr "rapid"
  compileExtPrim (NS ns (UN $ Basic "prim__os")) [] | ["Info", "System"] = do
    -- no cross compiling for now:
    mkStr System.Info.os
  compileExtPrim (NS ns (UN $ Basic "void")) _ | ["Uninhabited", "Prelude"] = do
    appendCode $ "  call ccc void @rapid_crash(i8* bitcast ([23 x i8]* @error_msg_void to i8*)) noreturn"
    appendCode $ "unreachable"
    pure nullPtr
  compileExtPrim (NS ns (UN $ Basic "prim__void")) _ | ["Uninhabited", "Prelude"] = do
    appendCode $ "  call ccc void @rapid_crash(i8* bitcast ([23 x i8]* @error_msg_void to i8*)) noreturn"
    appendCode $ "unreachable"
    pure nullPtr
  compileExtPrim (NS ns (UN $ Basic "prim__newIORef")) [_, val, _] | ["IORef", "Data"] = do
    ioRefObj <- dynamicAllocate (Const I64 8)
    putObjectHeader ioRefObj !(mkHeader OBJECT_TYPE_ID_IOREF (Const I32 0))
    putObjectSlot ioRefObj (Const I64 0) val
    pure ioRefObj
  compileExtPrim (NS ns (UN $ Basic "prim__readIORef")) [_, ioRefObj, _] | ["IORef", "Data"] = do
    getObjectSlot ioRefObj 0
  compileExtPrim (NS ns (UN $ Basic "prim__writeIORef")) [_, ioRefObj, payload, _] | ["IORef", "Data"] = do
    putObjectSlot ioRefObj (Const I64 0) payload
    mkUnit
  compileExtPrim (NS ns n) args | _ = compileExtPrimFallback (NS ns n) args
compileExtPrim n args = compileExtPrimFallback n args


text:
module Hands
import Data.Vect

import InsertionSort
import Card
import ElemsAreSame
import Sorted
import SlideWise

public export HAND_SIZE : Nat
HAND_SIZE = 5

--=======================================================================================================
--=======================================================================================================
--Utility proof data structures
--=======================================================================================================
--=======================================================================================================
data ForAll : Vect n elem -> (elem -> Type) -> Type where
  ForVect : prf x -> ForAll xs prf -> ForAll (x::r) prf
  End : ForAll [] pred

data AllSame : Vect n elem -> (elem -> elem -> Type) -> Type where
  EmptyIsSame: AllSame [] prf
  SingleIsSame: AllSame [x] prf
  Same: prf x y -> AllSame (y::ys) prf -> AllSame (x::y::ys) prf

data SameValue: Card -> Card -> Type where
  ValueMatch: SameValue (MkCard v _) (MkCard v _)

data SameSuit: Card -> Card -> Type where
  SuitMatch: SameSuit (MkCard _ s) (MkCard _ s)

--=======================================================================================================
--=======================================================================================================
--Hand Proof data structures
--=======================================================================================================
--=======================================================================================================
data PairH: Vect 2 Card -> Type where
  MkPair: PairH [(MkCard v _), (MkCard v _)]

data TwoPair: Vect HAND_SIZE Card -> Type where
  MkTwoPair: Sorted hand -> (firstpair: SlideWise2 hand PairH) -> (secondPair:SlideWise2 (getRest2 hand firstpair) PairH) -> TwoPair hand

data ThreeOfAKind : Vect 3 Card -> Type where
  MkThree: AllSame x SameValue -> ThreeOfAKind x

data Straight: Vect HAND_SIZE Card -> Type where
  MkStraight: Sorted x -> Consecutive x -> Straight x

data Flush: Vect HAND_SIZE Card -> Type where
  MkFlush: AllSame x SameSuit -> Flush x

data FullHouse: (hand:Vect HAND_SIZE Card) -> Type where
  MkFullHouse: Sorted hand -> (three: SlideWise3 hand ThreeOfAKind) -> (pair: PairH (getRest3 hand three)) -> FullHouse hand

data FourOfAKind : Vect 4 Card -> Type where
  MkFour: AllSame x SameValue -> FourOfAKind x

data StraightFlush: Vect HAND_SIZE Card -> Type where
  MkStraightFlush: Straight x -> Flush x -> StraightFlush x

--=======================================================================================================
--=======================================================================================================
--Hand
--=======================================================================================================
--=======================================================================================================
export data Hand: Vect HAND_SIZE Card -> Type where
  StraightFlushHand:
    StraightFlush x -> Hand x
  FourOfAKindHand:
    {auto p:Sorted y} -> SlideWise4 y FourOfAKind -> Hand y
  FullHouseHand:
    FullHouse y -> Hand y
  FlushHand:
    Flush x -> Hand x
  StraightHand:
    Straight x -> Hand x
  ThreeOfAKindHand:
    {auto p:Sorted y} -> SlideWise3 y ThreeOfAKind -> Hand y
  TwoPairHand:
    {auto p:Sorted y} -> TwoPair y -> Hand y
  PairHand:
    {auto p:Sorted y} -> SlideWise2 y PairH -> Hand y
  HighCardHand:
    {auto p:Sorted kickers} -> (kickers: Vect HAND_SIZE Card) -> Hand kickers

--=======================================================================================================
--=======================================================================================================
-- Utility proofs
--=======================================================================================================
--=======================================================================================================
--=======================================================================================================
-- hasSameSuit
--=======================================================================================================
notSameSuit : (contra : (s1 = s2) -> Void) -> SameSuit (MkCard value s1) (MkCard value1 s2) -> Void
notSameSuit contra SuitMatch = contra Refl

hasSameSuit: (c1: Card) -> (c2: Card) -> Dec (SameSuit c1 c2)
hasSameSuit (MkCard _ s1) (MkCard _ s2) = case decEq s1 s2 of
                                               (Yes prf) => Yes (rewrite prf in SuitMatch)
                                               (No contra) => No (notSameSuit contra)

--=======================================================================================================
-- hasSameValue
--=======================================================================================================
notSameValue : (contra : (v1 = v2) -> Void) -> SameValue (MkCard v1 suit) (MkCard v2 suit1) -> Void
notSameValue contra ValueMatch = contra Refl

hasSameValue: (c1: Card) -> (c2: Card) -> Dec (SameValue c1 c2)
hasSameValue (MkCard v1 _) (MkCard v2 _) = case decEq v1 v2 of
                                                (Yes prf) => Yes (rewrite prf in ValueMatch)
                                                (No contra) => No (notSameValue contra)
--=======================================================================================================
-- allSameSuit
--=======================================================================================================
restNotSameSuit : (contra : AllSame (x2 :: xs) SameSuit -> Void) -> AllSame (x1 :: (x2 :: xs)) SameSuit -> Void
restNotSameSuit contra (Same x y) = contra y

singleNotSameSuit : (contra : SameSuit x1 x2 -> Void) -> AllSame (x1 :: (x2 :: xs)) SameSuit -> Void
singleNotSameSuit contra (Same x y) = contra x

allSameSuit: (x: Vect n Card) -> Dec (AllSame x SameSuit)
allSameSuit [] = Yes EmptyIsSame
allSameSuit [x] = Yes SingleIsSame
allSameSuit (x1 :: x2 :: xs) = case allSameSuit (x2 :: xs) of
                                    (Yes prf_rest) => case hasSameSuit x1 x2 of
                                                               (Yes prf_single) => Yes (Same prf_single prf_rest)
                                                               (No contra) => No (singleNotSameSuit contra)
                                    (No contra) => No (restNotSameSuit contra)

--=======================================================================================================
-- isNoOfKind
--=======================================================================================================
restNotSame: (contra : AllSame (x2 :: xs) SameValue -> Void) -> AllSame (x1 :: (x2 :: xs)) SameValue -> Void
restNotSame contra (Same x y) = contra y

singleNotSame : (contra : SameValue x1 x2 -> Void) -> AllSame (x1 :: (x2 :: xs)) SameValue -> Void
singleNotSame contra (Same x y) = contra x

isNoOfKind: (x: Vect n Card) -> Dec (AllSame x SameValue)
isNoOfKind [] = Yes EmptyIsSame
isNoOfKind [x] = Yes SingleIsSame
isNoOfKind (x1 :: x2 :: xs) = case isNoOfKind (x2 :: xs) of
                           (Yes prf_rest) => (case hasSameValue x1 x2 of
                                              (Yes prf_single) => Yes (Same prf_single prf_rest)
                                              (No contra) => No (singleNotSame contra))
                           (No contra) => No (restNotSame contra)

--=======================================================================================================
--=======================================================================================================
--Hand Proofs
--=======================================================================================================
--=======================================================================================================
--=======================================================================================================
-- Pair
--=======================================================================================================
isNotPair : (contra : (v1 = v2) -> Void) -> PairH [(MkCard v1 suit), (MkCard v2 suit1)] -> Void
isNotPair contra MkPair = contra Refl

isPair: (p: Vect 2 Card) -> Dec (PairH p)
isPair [(MkCard v1 _), (MkCard v2 _)] = case decEq v1 v2 of
                                          (Yes prf) => Yes (rewrite prf in MkPair)
                                          (No contra) => No (isNotPair contra)

isPairHand: (hand: Vect HAND_SIZE Card) -> {auto sort_prf: Sorted hand }-> Dec (SlideWise2 hand PairH)
isPairHand hand {sort_prf} = isSlideWise2 hand isPair
--=======================================================================================================
-- Two Pair
--=======================================================================================================
pairInRest: {hand: Vect HAND_SIZE Card} -> (firstPair: SlideWise2 hand PairH) -> Dec (SlideWise2 (getRest2 hand firstPair) PairH)
pairInRest (HeadMatches2 searched match rest x) = isSlideWise2 (getRest2 (match ++ rest) (HeadMatches2 searched match rest x)) isPair
pairInRest (RestMatches2 x rest y) = isSlideWise2 (getRest2 (x :: rest) (RestMatches2 x rest y)) isPair

||| TODO return Dec instead
isTwoPairHand: (hand: Vect HAND_SIZE Card) -> {auto sort_prf: Sorted hand} ->  Maybe (TwoPair hand)
isTwoPairHand hand {sort_prf} = case isPairHand hand of
                                   (Yes first_prf) => (case pairInRest first_prf of
                                                      (Yes snd_prf) => Just (MkTwoPair sort_prf first_prf snd_prf)
                                                      (No contra) => Nothing)
                                   (No contra) => Nothing

--=======================================================================================================
-- Three of a Kind
--=======================================================================================================
notThreeOfAKind : (contra : AllSame x SameValue -> Void) -> ThreeOfAKind x -> Void
notThreeOfAKind contra (MkThree x) = contra x

isThreeOfAKind: (x: Vect 3 Card) -> Dec (ThreeOfAKind x)
isThreeOfAKind x = case isNoOfKind x of
                        (Yes prf) => Yes (MkThree prf)
                        (No contra) => No (notThreeOfAKind contra)

isThreeOfAKindHand: (hand: Vect 5 Card) -> {auto sort_prf: Sorted hand} -> Dec (SlideWise3 hand ThreeOfAKind)
isThreeOfAKindHand hand = isSlideWise3 hand isThreeOfAKind
--=======================================================================================================
-- Straight
--=======================================================================================================
notConsecSoNotStraight : (contra : Consecutive x -> Void) -> Straight x -> Void
notConsecSoNotStraight contra (MkStraight x y) = contra y

isStraight: (x: Vect HAND_SIZE Card) -> {auto sort_prf:Sorted x} -> Dec (Straight x)
isStraight {sort_prf} x = case isConsecutive x of
                         (Yes prf) => Yes (MkStraight sort_prf prf)
                         (No contra) => No (notConsecSoNotStraight contra)

--=======================================================================================================
-- Flush
--=======================================================================================================
notFlush : (contra : AllSame x SameSuit -> Void) -> Flush x -> Void
notFlush contra (MkFlush (Same z w)) = contra (Same z w)

isFlush: (x: Vect HAND_SIZE Card) -> Dec (Flush x)
isFlush x = case allSameSuit x of
                 (Yes prf) => Yes (MkFlush prf)
                 (No contra) => No (notFlush contra)
--=======================================================================================================
-- Full House
--=======================================================================================================
isFullHouse: (hand: Vect HAND_SIZE Card) -> (sort_prf: Sorted hand) -> Maybe (FullHouse hand)
isFullHouse hand sort_prf = case isThreeOfAKindHand hand of
                                 (No contra) => Nothing
                                 (Yes three_prf) => (case isPair (getRest3 hand three_prf) of
                                                          (Yes pair_prf) => Just (MkFullHouse sort_prf three_prf pair_prf)
                                                          (No contra) => Nothing)

--=======================================================================================================
-- Four of a Kind
--=======================================================================================================
notFourOfAKind : (contra : AllSame x SameValue -> Void) -> FourOfAKind x -> Void
notFourOfAKind contra (MkFour x) = contra x

isFourOfAKind: (x: Vect 4 Card) -> Dec (FourOfAKind x)
isFourOfAKind x = case isNoOfKind x of
                       (Yes prf) => Yes (MkFour prf)
                       (No contra) => No (notFourOfAKind contra)

isFourOfAKindHand: (hand: Vect 5 Card) -> Sorted hand -> Dec (SlideWise4 hand FourOfAKind)
isFourOfAKindHand hand sort_prf = isSlideWise4 hand isFourOfAKind

--=======================================================================================================
-- Straight Flush
--=======================================================================================================
notStraightSoNotSF : (contra : Straight x -> Void) -> StraightFlush x -> Void
notStraightSoNotSF contra (MkStraightFlush straight flush) = contra straight

notFlushSoNotSF : (contra : Flush x -> Void) -> StraightFlush x -> Void
notFlushSoNotSF contra (MkStraightFlush straight flush) = contra flush

isStraightFlush: (x: Vect HAND_SIZE Card) -> {auto sort_prf:Sorted x} -> Dec (StraightFlush x)
isStraightFlush x = case isStraight x of
                         (Yes straight_prf) => (case isFlush x of
                                            (Yes flush_prf) => Yes (MkStraightFlush straight_prf flush_prf)
                                            (No contra) => No (notFlushSoNotSF contra))
                         (No contra) => No (notStraightSoNotSF contra)

--=======================================================================================================
--=======================================================================================================
-- Hand evaluator
--=======================================================================================================
--=======================================================================================================

evalRestHand : (hand: Vect HAND_SIZE Card) -> (sort_prf : Sorted hand) -> (contra_4 : SlideWise4 hand FourOfAKind -> Void) -> (contra_sf : StraightFlush hand -> Void) -> Hand hand
evalRestHand hand sort_prf contra_4 contra_sf = case isFlush hand of
                                                     (Yes prf) => FlushHand prf
                                                     (No contra_flush) => (case isStraight hand of
                                                                                (Yes prf) => StraightHand prf
                                                                                (No contra) => (case isThreeOfAKindHand hand of
                                                                                (Yes prf) => ThreeOfAKindHand prf
                                                                                (No contra) => (case isTwoPairHand  hand of
                                                                                (Just prf) => TwoPairHand prf
                                                                                Nothing => (case isPairHand hand of
                                                                                (Yes prf) => PairHand prf
                                                                                (No contra) => HighCardHand hand))))

export evalHand: (hand: Vect HAND_SIZE Card) -> Sorted hand -> Hand hand
evalHand hand sort_prf = case isStraightFlush hand of
                              (Yes prf) => StraightFlushHand prf
                              (No contra_sf) => (case isFourOfAKindHand hand sort_prf of
                                                Yes prf => FourOfAKindHand prf
                                                No contra_4 => (case isFullHouse hand sort_prf of
                                                                      Just prf => FullHouseHand prf
                                                                      Nothing => evalRestHand hand sort_prf contra_4 contra_sf))

compareStraightFlushes : (x : StraightFlush h1) -> (y : StraightFlush h2) -> Ordering
compareStraightFlushes {h1 = (x1 :: xs1)} {h2 = (x2:: xs2)} x y = compare (cardValue x1) (cardValue x2)

compareFourOfAKinds : (x : SlideWise4 h1 FourOfAKind) -> (y : SlideWise4 h2 FourOfAKind) -> Ordering
compareFourOfAKinds {h1} {h2} x y = let ((x1::xs), kicker1::[]) = getMatchAndRest4 h1 x
                                        ((y1::ys), kicker2::[]) = getMatchAndRest4 h2 y in
                                        (case compare (cardValue x1) (cardValue y1) of
                                              LT => LT
                                              EQ => compare (cardValue kicker1) (cardValue kicker2)
                                              GT => GT)

compareHighCards : (h1 : Vect n Card) -> (h2 : Vect n Card) -> Ordering
compareHighCards [] [] = EQ
compareHighCards (x :: xs) (y :: ys) = case compare (cardValue x) (cardValue y) of
                                            LT => LT
                                            EQ => compareHighCards xs ys
                                            GT => GT

compareFlushes : (x : Flush h1) -> (y : Flush h2) -> Ordering
compareFlushes {h1} {h2} x y = compareHighCards h1 h2

comparePairs : {h1, h2: Vect (S(S n)) Card} -> (x : SlideWise2 h1 PairH) -> (y : SlideWise2 h2 PairH) -> Ordering
comparePairs {h1} {h2} x y = let ((x1::xs), kickers1) = getMatchAndRest2 h1 x
                                 ((y1::ys), kickers2) = getMatchAndRest2 h2 y in
                                 (case compare (cardValue x1) (cardValue y1) of
                                        LT => LT
                                        EQ => compareHighCards kickers1 kickers2
                                        GT => GT)

getHighLowPair: Card -> Card -> (Card, Card)
getHighLowPair x y = case compare (cardValue x) (cardValue y) of
               LT => (y, x)
               gtOrEq => (x, y)

compareTwoPairs : {h1, h2: Vect HAND_SIZE Card} -> (x : TwoPair h1) -> (y : TwoPair h2) -> Ordering
compareTwoPairs {h1} {h2} (MkTwoPair x firstPair1 secondPair1)
                (MkTwoPair y firstPair2 secondPair2) = let (firstmatch1::f1) = getMatch2 h1 firstPair1
                                                           (secondmatch1::s1, kicker1::[]) = getMatchAndRest2 (getRest2 h1 firstPair1) secondPair1
                                                           (firstmatch2::f2) = getMatch2 h2 firstPair2
                                                           (secondmatch2::s2, kicker2::[]) = getMatchAndRest2 (getRest2 h2 firstPair2) secondPair2
                                                           (highestPair1, lowestPair1) = getHighLowPair firstmatch1 secondmatch1
                                                           (highestPair2, lowestPair2) = getHighLowPair firstmatch2 secondmatch2
                                                           in
                                                           (case compare (cardValue highestPair1) (cardValue highestPair2) of
                                                                 LT => LT
                                                                 GT => GT
                                                                 EQ => (case compare (cardValue lowestPair1) (cardValue lowestPair2) of
                                                                             LT => LT
                                                                             EQ => compare (cardValue kicker1) (cardValue kicker2)
                                                                             GT => GT))

compareThreeOfAKinds : {h1, h2: Vect (S(S(S n))) Card} -> (x : SlideWise3 h1 ThreeOfAKind) -> (y : SlideWise3 h2 ThreeOfAKind) -> Ordering
compareThreeOfAKinds {h1} {h2} x y = let ((x1::xs), kickers1) = getMatchAndRest3 h1 x
                                         ((y1::ys), kickers2) = getMatchAndRest3 h2 y in
                                          (case compare (cardValue x1) (cardValue y1) of
                                              LT => LT
                                              EQ => compareHighCards kickers1 kickers2
                                              GT => GT)

comparePairHs : (pair_prf1 : PairH h1) -> (pair_prf2 : PairH h2) -> Ordering
comparePairHs {h1} {h2} pair_prf1 pair_prf2 = compareHighCards h1 h2

compareFullHouseHands : (x : FullHouse h1) -> (y : FullHouse h2) -> Ordering
compareFullHouseHands {h1} (MkFullHouse x three_prf1 pair_prf1)
                      {h2} (MkFullHouse y three_prf2 pair_prf2) = let (threeCard1::_) = (getMatch3 h1 three_prf1)
                                                                      (threeCard2::_) = (getMatch3 h2 three_prf2) in
                                                                      (case compare (cardValue threeCard1) (cardValue threeCard2) of
                                                                            LT => LT
                                                                            EQ => comparePairHs pair_prf1 pair_prf2
                                                                            GT => GT)

compareStraights : {h1, h2: Vect HAND_SIZE Card} -> (x : Straight h1) -> (y : Straight h2) -> Ordering
compareStraights {h1} {h2} x y = compareHighCards h1 h2

export compareHands: {h1, h2: Vect HAND_SIZE Card} -> (hand1: Hand h1) -> (hand2: Hand h2) -> Ordering
compareHands (StraightFlushHand x) (StraightFlushHand y) = compareStraightFlushes x y
compareHands (StraightFlushHand x) hand2 = GT
compareHands (FourOfAKindHand x) (StraightFlushHand y) = LT
compareHands (FourOfAKindHand x) (FourOfAKindHand y) = compareFourOfAKinds x y
compareHands (FourOfAKindHand x) hand2 = GT
compareHands (FullHouseHand x) (StraightFlushHand y) = LT
compareHands (FullHouseHand x) (FourOfAKindHand y) = LT
compareHands (FullHouseHand x) (FullHouseHand y) = compareFullHouseHands x y
compareHands (FullHouseHand x) hand2 = GT
compareHands (FlushHand x) (StraightFlushHand y) = LT
compareHands (FlushHand x) (FourOfAKindHand y) = LT
compareHands (FlushHand x) (FullHouseHand y) = LT
compareHands (FlushHand x) (FlushHand y) = compareFlushes x y
compareHands (FlushHand x) hand2 = GT
compareHands (StraightHand x) (StraightFlushHand y) = LT
compareHands (StraightHand x) (FourOfAKindHand y) = LT
compareHands (StraightHand x) (FullHouseHand y) = LT
compareHands (StraightHand x) (FlushHand y) = LT
compareHands (StraightHand x) (StraightHand y) = compareStraights x y
compareHands (StraightHand x) hand2 = GT
compareHands (ThreeOfAKindHand x) (StraightFlushHand y) = LT
compareHands (ThreeOfAKindHand x) (FourOfAKindHand y) = LT
compareHands (ThreeOfAKindHand x) (FullHouseHand y) = LT
compareHands (ThreeOfAKindHand x) (FlushHand y) = LT
compareHands (ThreeOfAKindHand x) (StraightHand y) = LT
compareHands (ThreeOfAKindHand x) (ThreeOfAKindHand y) = compareThreeOfAKinds x y
compareHands (ThreeOfAKindHand x) hand2 = GT
compareHands (TwoPairHand x) (HighCardHand h2) = GT
compareHands (TwoPairHand x) (PairHand y) = GT
compareHands (TwoPairHand x) (TwoPairHand y) = compareTwoPairs x y
compareHands (TwoPairHand x) hand2 = LT
compareHands (PairHand x) (HighCardHand h2) = GT
compareHands (PairHand x) (PairHand y) = comparePairs x y
compareHands (PairHand x) hand2 = LT
compareHands (HighCardHand h1) (HighCardHand h2) = compareHighCards h1 h2
compareHands (HighCardHand h1) hand2 = LT

showHighCard : (h : Vect HAND_SIZE Card) -> String
showHighCard (x :: xs) = "High Card: " ++ (show (cardValue x))

showPair :{h: Vect HAND_SIZE Card} -> (x : SlideWise2 h PairH) -> String
showPair {h} x = let (m::ms, r::rs) = getMatchAndRest2 h x in
                "Pair: " ++ (show (cardValue m)) ++ "s with a " ++ (show (cardValue r)) ++ " kicker"

showTwoPair : (x : TwoPair h)-> String
showTwoPair {h} (MkTwoPair x firstPair secondPair) = let (m1::ms1) = getMatch2 h firstPair
                                                         (m2::ms2, [kicker]) = getMatchAndRest2 (getRest2 h firstPair) secondPair in
                                                         "Two Pair: " ++ (show (cardValue m1)) ++ "s and " ++ (show (cardValue m2)) ++ "s with a " ++ (show (cardValue kicker)) ++ " kicker"

showThreeOfAKind : (x : SlideWise3 h ThreeOfAKind) -> String
showThreeOfAKind {h} x = let (m::ms, r::rs) = getMatchAndRest3 h x in
                "Three of a kind: " ++ (show (cardValue m)) ++ "s with a " ++ (show (cardValue r)) ++ " kicker"

showStraight : (x : Straight h) -> String
showStraight {h = (z :: xs)} (MkStraight x y) = "Straight: " ++ (show (cardValue z)) ++ " high"

showFlush : (x : Flush h) -> String
showFlush {h = (y :: xs)} x = "Flush: " ++ (show (cardValue y)) ++ " high"

showFullHouse : (x : FullHouse h) -> String
showFullHouse {h} (MkFullHouse x three pair) = let (m1::m1s) = getMatch3 h three
                                                   (m2::m2s) = (getRest3 h three) in
                                                   "Full house: " ++ (show (cardValue m1)) ++ "s over " ++ (show (cardValue m2)) ++ "s"

showFourOfAKind : (x : SlideWise4 h FourOfAKind) -> String
showFourOfAKind {h} x = let (m::ms, [kicker]) = getMatchAndRest4 h x in
                "Four of a kind: " ++ (show (cardValue m)) ++ "s with a " ++ (show (cardValue kicker)) ++ " kicker"

showStraightFlush : (x : StraightFlush h) -> String
showStraightFlush {h = (y :: xs)} x = "Straight flush: " ++ (show (cardValue y)) ++ " high"

export Show (Hand h) where
  show (StraightFlushHand x) = showStraightFlush x
  show (FourOfAKindHand x) = showFourOfAKind x
  show (FullHouseHand x) = showFullHouse x
  show (FlushHand x) = showFlush x
  show (StraightHand x) = showStraight x
  show (ThreeOfAKindHand x) = showThreeOfAKind x
  show (TwoPairHand x) = showTwoPair x
  show (PairHand x) = showPair x
  show (HighCardHand h) = showHighCard h


text:
module Test

import Test.Golden

tests : TestPool
tests
  = MkTestPool "Hello World"
               []
               Nothing
               [ "000-hello"]

export
main : IO ()
main = runner [ tests ]

-- [ EOF ]


text:
module Text.Show.Pretty

import Data.List
import Text.PrettyPrint.Prettyprinter

import public Text.Show.Value
import public Text.Show.PrettyVal

%default total

--------------------------------------------------------------------------------
--          Utilities
--------------------------------------------------------------------------------

-- Don't put parenthesis around constructors in infix chains
isInfixAtom : Value -> Bool
isInfixAtom (InfixCons _ _) = False
isInfixAtom (Neg _)         = False
isInfixAtom _               = True

isAtom : Value -> Bool
isAtom (Con _ (_ :: _))  = False
isAtom v                 = isInfixAtom v

blockWith :  (List (Doc ann) -> Doc ann)
          -> Char
          -> Char
          -> List (Doc ann) -> Doc ann
blockWith _ a b []       = pretty a <+> pretty b
blockWith f a b (d::ds)  = f $  (pretty a <++> d)
                             :: [ pretty ',' <++> x | x <- ds ]
                             ++ [ pretty b ]

block : Char -> Char -> List (Doc ann) -> Doc ann
block = blockWith sep

hangAfter : Doc ann -> Int -> Doc ann -> Doc ann
hangAfter pre n po = sep [pre, nest n po]

toDoc : Value -> Doc ann
toDoc val =
  case val of
    Con (MkName "") vs => sep $ atoms vs
    Con (MkName c)  [] => pretty c
    Con (MkName c)  vs => hangAfter (pretty c) 2 (sep $ atoms vs)
    InfixCons v1 cvs   => hangsep (infx v1 cvs)
    Rec c fs           => hangAfter (pretty c) 2 $ block '{' '}' (fields fs)
    Lst vs             => block '[' ']' (docs vs)
    Tuple v1 v2 vs     => block '(' ')' (toDoc v1 :: toDoc v2 :: docs vs)
    Neg v              => pretty '-' <+> atom v
    Natural x          => pretty x
    Dbl x              => pretty x
    Chr x              => pretty x
    Str x              => pretty x

  where
    atom : Value -> Doc ann
    atom v = if isAtom v then toDoc v else parens (toDoc v)

    -- the explicit list mappings like `atoms`, `docs`, and
    -- `fields` are necessary to convince the totality checker.
    atoms : List Value -> List (Doc ann)
    atoms []        = []
    atoms (x :: xs) = atom x :: atoms xs

    infixAtom : Value -> Doc ann
    infixAtom v = if isInfixAtom v then toDoc v else parens (toDoc v)

    field : (Name,Value) -> Doc ann
    field (x,v) = hangAfter (pretty x <++> pretty '=') 2 (toDoc v)

    fields : List (Name,Value) -> List (Doc ann)
    fields []        = []
    fields (p :: ps) = field p :: fields ps

    docs : List Value -> List (Doc ann)
    docs []        = []
    docs (x :: xs) = toDoc x :: docs xs

    infx : Value -> List (Name,Value) -> List (Doc ann)
    infx v []             = [infixAtom v]
    infx v ((n,v2)::cvs') = (infixAtom v <++> pretty n) :: infx v2 cvs'

    hangsep : List (Doc ann) -> Doc ann
    hangsep []      = neutral
    hangsep (x::xs) = hangAfter x 2 (sep xs)

||| Pretty print a generic value. Our intention is that the result is
||| equivalent to the 'Show' instance for the original value, except possibly
||| easier to understand by a human.
export
valToDoc : Value -> Doc ann
valToDoc = toDoc

||| Pretty print a generic value. Our intention is that the result is
||| equivalent to the 'Show' instance for the original value, except possibly
||| easier to understand by a human.
export
valToStr : Value -> String
valToStr = show . valToDoc {ann = ()}

--------------------------------------------------------------------------------
--          Pretty via Show
--------------------------------------------------------------------------------

export covering
reify : Show a => a -> Maybe Value
reify = parseValue . show

||| Try to show a value, prettily. If we do not understand the value, then we
||| just use its standard 'Show' instance.
export covering
ppDoc : Show a => a -> Doc ann
ppDoc a = let txt = show a
           in maybe (fromString txt) valToDoc (parseValue txt)

||| Convert a generic value into a pretty 'String', if possible.
export covering
ppShow : Show a => a -> String
ppShow = show . ppDoc {ann = ()}

||| Pretty print something that may be converted to a list as a list.
||| Each entry is on a separate line, which means that we don't do clever
||| pretty printing, and so this works well for large strucutures.
export covering
ppDocList : (Foldable f, Show a) => f a -> Doc ann
ppDocList = blockWith vcat '[' ']' . map ppDoc . toList

||| Pretty print something that may be converted to a list as a list.
||| Each entry is on a separate line, which means that we don't do clever
||| pretty printing, and so this works well for large strucutures.
export covering
ppShowList : (Foldable f, Show a) => f a -> String
ppShowList = show . ppDocList {ann = ()}

||| Pretty print a generic value to stdout.
export covering
pPrint : Show a => a -> IO ()
pPrint = putStrLn . ppShow

||| Pretty print something that may be converted to a list as a list.
||| Each entry is on a separate line, which means that we don't do clever
||| pretty printing, and so this works well for large strucutures.
export covering
pPrintList : (Foldable f, Show a) => f a -> IO ()
pPrintList = putStrLn . ppShowList

--------------------------------------------------------------------------------
--          Pretty via PrettyVal
--------------------------------------------------------------------------------

||| Render a value in the `PrettyVal` interface to a `Doc`.
||| The benefit of this function is that `PrettyVal` instances may
||| be derived automatically using generics.
export
dumpDoc : PrettyVal a => a -> Doc ann
dumpDoc = valToDoc . prettyVal

||| Render a value in the `PrettyVal` interface to a `String`.
||| The benefit of this function is that `PrettyVal` instances may
||| be derived automatically using generics.
export
dumpStr : PrettyVal a => a -> String
dumpStr = show . dumpDoc {ann = ()}

||| Render a value using the `PrettyVal` interface
||| and show it to standard out.
export
dumpIO : PrettyVal a => a -> IO ()
dumpIO = putStrLn . dumpStr

--------------------------------------------------------------------------------
--          Pre-processing
--------------------------------------------------------------------------------

||| This type is used to allow pre-processing of values before showing them.
public export
record PreProc a where
  constructor MkPreProc
  preProc : Value -> Value
  val     : a

export
PrettyVal a => PrettyVal (PreProc a) where
  prettyVal (MkPreProc p v) = p (prettyVal v)

||| Hide the given constructors when showing a value.
export covering
ppHide : (Name -> Bool) -> a -> PreProc a
ppHide p = MkPreProc (hideCon False p)

||| Hide the given constructors when showing a value.
||| In addition, hide values if all of their children were hidden.
export covering
ppHideNested : (Name -> Bool) -> a -> PreProc a
ppHideNested p = MkPreProc (hideCon True p)


text:
module Algebra.Solver.Semigroup

import Algebra.Semigroup
import Data.List1
import Syntax.PreorderReasoning

%default total

public export
data Expr : (a : Type) -> Type where
  Var    : (x : a) -> Expr a
  Append : Expr a -> Expr a -> Expr a

public export
Semigroup (Expr a) where
  (<+>) = Append

public export
eval : LSemigroup a => Expr a -> a
eval (Var x)    = x
eval (Append x y) = eval x <+> eval y

--------------------------------------------------------------------------------
--          Sum
--------------------------------------------------------------------------------

public export
esum' : LSemigroup a => a -> List a -> a
esum' v []       = v
esum' v (h :: t) = v <+> esum' h t

public export
esum : LSemigroup a => List1 a -> a
esum (v ::: vs) = esum' v vs

public export
normalize : Expr a -> List1 a
normalize (Var x)      = x ::: []
normalize (Append x y) = normalize x ++ normalize y

--------------------------------------------------------------------------------
--          Proofs
--------------------------------------------------------------------------------

0 psum' :  LSemigroup a
        => (x,y   : a)
        -> (xs,ys : List a)
        -> esum' x (xs ++ (y :: ys)) === esum' x xs <+> esum' y ys
psum' x y []        ys = Refl
psum' x y (v :: vs) ys = Calc $
  |~ x <+> esum' v (vs ++ (y :: ys))
  ~~ x <+> (esum' v vs <+> esum' y ys) ... cong (x <+>) (psum' v y vs ys)
  ~~ (x <+> esum' v vs) <+> esum' y ys ... appendAssociative

0 psum :  LSemigroup a
       => (xs,ys : List1 a)
       -> esum (xs ++ ys) === esum xs <+> esum ys
psum (x ::: xs) (y ::: ys) = psum' x y xs ys

0 pnorm : LSemigroup a => (e : Expr a) -> eval e === esum (normalize e)
pnorm (Var x)      = Refl
pnorm (Append x y) = Calc $
  |~ eval x <+> eval y
  ~~ esum (normalize x) <+> eval y
     ... cong (<+> eval y) (pnorm x)
  ~~ esum (normalize x) <+> esum (normalize y)
     ... cong (esum (normalize x) <+>) (pnorm y)
  ~~ esum (normalize x ++ normalize y)
     ..< psum (normalize x) (normalize y)

--------------------------------------------------------------------------------
--          Solver
--------------------------------------------------------------------------------

export
0 solve :  LSemigroup a
        => (e1,e2 : Expr a)
        -> (prf : normalize e1 === normalize e2)
        => eval e1 === eval e2
solve e1 e2 = Calc $
  |~ eval e1
  ~~ esum (normalize e1) ... pnorm e1
  ~~ esum (normalize e2) ... cong esum prf
  ~~ eval e2             ..< pnorm e2