text:
module Optimisation.GlobalStaticOptimizer

import Data.SortedSet
import Data.SortedMap
import Core.Context
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import Utils.Helpers
import CairoCode.Traversal.Base
import Optimisation.StaticProcessing.IterativeBaseTransformer
import Optimisation.StaticProcessing.StaticTracker
import Optimisation.StaticProcessing.StaticTransformer

%hide Prelude.toList

export
globalStaticOptimize : Name -> List (Name, CairoDef) -> List (Name, CairoDef)
globalStaticOptimize = iterativeCallTransform (mkRegisterGen "global_optim") noTransform (\id => id)

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
import FCTypes
import Hello
import HelloHole
import HoleFix

ext: idr


text:
> module BoundedNat.BoundedNat

> import Sigma.Sigma

> %default total

> %access public export

> ||| Natural numbers bounded by LT
> LTB : Nat -> Type
> LTB b = Sigma Nat (\ n  => LT n b)

> ||| Natural numbers bounded by LTE
> LTEB : Nat -> Type
> LTEB b = Sigma Nat (\ n  => LTE n b)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
-- PacketLang implementation of DNS packets.
-- Also data representations of DNS packet.

-- PacketLang representations:
module DNS

import IdrisNet.PacketLang
import IdrisNet.Socket
import DNSCodes

%access public
%default total

-- Data representations of DNS Packets

-- DNS Types:
-- These are record types, so for example CNAME or MX.
-- Types are basic ones, but QTypes are a superset.

data DNSQuestion : Type where
  MkDNSQuestion : (dnsQNames : List DomainFragment) ->
                  (dnsQQType : DNSQType) ->
                  (dnsQQClass : DNSQClass) ->
                  DNSQuestion

instance Show DNSQuestion where
  show (MkDNSQuestion qns qqt qqc) =
    "DNS Question: \n" ++
    "DNS QNames: \n" ++ (show qns) ++ "\n" ++
    "DNS QType: \n" ++ (show qqt) ++ "\n" ++
    "DNS QClass: \n" ++ (show qqc) ++ "\n"

data DNSRecord : Type where
  MkDNSRecord : (dnsRRName : List DomainFragment) ->
                (dnsRRType : DNSType) ->
                (dnsRRClass : DNSClass) ->
                (dnsRRTTL : Int) ->
                (dnsRRRel : DNSPayloadRel dnsRRType dnsRRClass pl_ty) ->
                (dnsRRPayload : DNSPayload pl_ty) ->
                DNSRecord

instance Show DNSRecord where
  show (MkDNSRecord name ty cls ttl rel pl) = "DNS Record: \n" ++
    "DNS RR Name: " ++ (show name) ++ "\n" ++
    "DNS RR Type: " ++ (show ty) ++ "\n" ++
    "DNS RR Class: " ++ (show cls) ++ "\n" ++
    "DNS RR TTL: " ++ (show ttl) ++ "\n" ++
    "DNS RR Payload: " ++ (showPayload rel pl) ++ "\n"

record DNSHeader : Type where
  MkDNSHeader : (dnsHdrId : Int) ->
                (dnsHdrIsQuery : Bool) ->
                (dnsHdrOpcode : DNSHdrOpcode) ->
                (dnsHdrIsAuthority : Bool) ->
                (dnsHdrIsTruncated : Bool) ->
                (dnsHdrRecursionDesired : Bool) ->
                (dnsHdrRecursionAvailable : Bool) ->
                (dnsAnswerAuthenticated : Bool) ->
                (dnsNonAuthAcceptable : Bool) ->
                (dnsHdrResponse : DNSResponse) ->
                DNSHeader

instance Show DNSHeader where
  show (MkDNSHeader hdr_id query op auth trunc rd ra aa naa resp) =
    "DNS Header\n" ++
    "ID : " ++ (show hdr_id) ++ "\n" ++
    "Is query? : " ++ (show query) ++ "\n" ++
    "Opcode : " ++ (show op) ++ "\n" ++
    "Is authority? : " ++ (show auth) ++ "\n" ++
    "Is truncated? : " ++ (show trunc) ++ "\n" ++
    "Is recursion desired? : " ++ (show rd) ++ "\n" ++
    "Is recursion available? : " ++ (show ra) ++ "\n" ++
    "Is answer authenticated? : " ++ (show aa) ++ "\n" ++
    "Is non-authenticated data acceptable? : " ++ (show naa) ++ "\n" ++
    "Response : " ++ (show resp) ++ "\n"

record DNSPacket : Type where
  MkDNS : (dnsPcktHeader : DNSHeader) ->
          (dnsPcktQDCount : Nat) ->
          (dnsPcktANCount : Nat) ->
          (dnsPcktNSCount : Nat) ->
          (dnsPcktARCount : Nat) ->
          (dnsPcktQuestions : Vect dnsPcktQDCount DNSQuestion) ->
          (dnsPcktAnswers : Vect dnsPcktANCount DNSRecord) ->
          (dnsPcktAuthorities : Vect dnsPcktNSCount DNSRecord) ->
          (dnsPcktAdditionals : Vect dnsPcktARCount DNSRecord) ->
          DNSPacket

instance Show DNSPacket where
  show (MkDNS hdr qdc anc nsc arc qs as auths adds) =
    "DNS Packet: " ++ "\n" ++
    "Header: " ++ (show hdr) ++ "\n" ++
    "QD Count: " ++ (show qdc) ++ "\n" ++
    "AN Count: " ++ (show anc) ++ "\n" ++
    "NS Count: " ++ (show nsc) ++ "\n" ++
    "AR Count: " ++ (show arc) ++ "\n" ++
    "Questions: " ++ (show qs) ++ "\n" ++
    "Answers: " ++ (show as) ++ "\n" ++
    "Authorities: " ++ (show auths) ++ "\n" ++
    "Additionals: " ++ (show adds) ++ "\n"

nullterm : PacketLang
nullterm = with PacketLang do
  nt <- bits 8
  check ((val nt) == 0)

validRespCode : Int -> Bool
validRespCode i = i >= 0 && i <= 5

-- DNS allows compression in the form of references.
-- These take the form of two octets, the first two bits of which
-- are 11. The rest is 14 bits.
tagCheck : Int -> PacketLang
tagCheck i = with PacketLang do
  tag1 <- bits 1
  tag2 <- bits 1
  let v1 = val tag1
  let v2 = val tag2
  prop (prop_eq v1 i)
  prop (prop_eq v2 i)

dnsReference : PacketLang
dnsReference = with PacketLang do
  tagCheck 1
  bits 14

dnsLabel: PacketLang
dnsLabel = with PacketLang do
  tagCheck 0
  len <- bits 6
  let vl = (val len)
  check (vl /= 0)
  listn (intToNat vl) (bits 8)

dnsLabels : PacketLang
dnsLabels = with PacketLang do
  list dnsLabel
  nullterm // dnsReference

dnsDomain : PacketLang
dnsDomain = dnsReference // dnsLabels

dnsQuestion : PacketLang
dnsQuestion = with PacketLang do
  dnsDomain
  decodable 16 DNSQType dnsCodeToQType dnsQTypeToCode
  decodable 16 DNSQClass dnsCodeToQClass dnsQClassToCode

dnsIP : PacketLang
dnsIP = with PacketLang do
  bits 8
  bits 8
  bits 8
  bits 8

dnsSOA : PacketLang
dnsSOA = with PacketLang do
  mname <- dnsDomain
  rname <- dnsDomain
  serial <- bits 32
  refresh <- bits 32
  retry <- bits 32
  expire <- bits 32
  bits 32 -- minimum

dnsPayloadLang : DNSType -> DNSClass -> PacketLang
dnsPayloadLang DNSTypeA DNSClassIN = dnsIP
dnsPayloadLang DNSTypeAAAA DNSClassIN = null
dnsPayloadLang DNSTypeNS DNSClassIN = dnsDomain
dnsPayloadLang DNSTypeCNAME DNSClassIN = dnsDomain
dnsPayloadLang DNSTypeSOA DNSClassIN = dnsSOA
dnsPayloadLang _ _ = null

dnsHeader : PacketLang
dnsHeader =
  with PacketLang do
     ident <- bits 16 -- Request identifier
     qr <- bool -- Query or response
     opcode <- decodable 4 DNSHdrOpcode dnsCodeToOpcode dnsOpcodeToCode
     aa <- bool -- Only set in response, is responding server authority?
     tc <- bool -- Was message truncated?
     rd <- bool -- Recursion desired, set in query, copied into response
     ra <- bool -- Recursion available; is support available in NS?
     z  <- bool -- Must be 0.
     check (not z)
     ans_auth <- bool
     auth_acceptable <- bool
     decodable 4 DNSResponse dnsCodeToResponse dnsResponseToCode

-- DNS Resource Record
-- The same for answers, authorities and additional info.
%assert_total
dnsRR : PacketLang
dnsRR = with PacketLang do
           domain <- dnsDomain
           ty <- decodable 16 DNSType dnsCodeToType' dnsTypeToCode'
           cls <- decodable 16 DNSClass dnsCodeToClass' dnsClassToCode'
           ttl <- bits 32
           len <- bits 16 -- Length in octets of next field
           let pl_lang = dnsPayloadLang ty cls
           pl_data <- pl_lang
           let data_len = (bitLength pl_lang pl_data) `div` 8
           prop (prop_eq (val len) data_len)

dns : PacketLang
dns = with PacketLang do
         header <- dnsHeader
         -- Technically these are parts of the header, but we
         -- need them in scope for later
         qdcount <- bits 16 -- Number of entries in question section
         ancount <- bits 16 -- Number of entries in the answer section
         nscount <- bits 16 -- Number of NS resource records in auth records
         arcount <- bits 16 -- Number of resource records in additional records section
         questions <- listn (intToNat $ val qdcount) dnsQuestion
         answers <- listn (intToNat $ val ancount) dnsRR
         authorities <- listn (intToNat $ val nscount) dnsRR
         listn (intToNat $ val arcount) dnsRR -- Additional


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 15

-- check that all functions are total
%default total

--
-- section 15.1
-- see AdderChannel.idr
--

--
-- section 15.2
-- see Process.idr
-- see ProcessLoop.idr
-- see ProcessState.idr
-- see ProcessInterface.idr
-- see ProcessLib.idr and ListProc.idr
--

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Language.LSP.Message.DocumentFormatting

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_formatting
public export
record DocumentFormattingClientCapabilities where
  constructor MkDocumentFormattingClientCapabilities
  dynamicRegistration : Maybe Bool
%runElab deriveJSON defaultOpts `{{DocumentFormattingClientCapabilities}}

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

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

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting
public export
record FormattingOptions where
  constructor MkFormattingOptions
  tabSize                : Int
  insertSpaces           : Bool
  trimTrailingWhitespace : Maybe Bool
  insertFinalNewline     : Maybe Bool
  trimFinalNewlines      : Maybe Bool
  other                  : List (String, OneOf [Bool, Int, String])

export
ToJSON FormattingOptions where
  toJSON opts =
    JObject ((catMaybes [ Just ("tabSize", toJSON opts.tabSize)
                        , Just ("insertSpaces", toJSON opts.insertSpaces)
                        , ("trimTrailingWhitespace",) . toJSON <$> opts.trimTrailingWhitespace
                        , ("insertFinalNewline",) . toJSON <$> opts.insertFinalNewline
                        , ("trimFinalNewlines",) . toJSON <$> opts.trimFinalNewlines
                        ]) ++ (mapSnd toJSON <$> opts.other))

export
FromJSON FormattingOptions where
  fromJSON (JObject arg) =
      pure MkFormattingOptions <*> (lookup "tabSize" arg >>= fromJSON)
                               <*> (lookup "insertSpaces" arg >>= fromJSON)
                               <*> (pure $ lookup "trimTrailingWhitespace" arg >>= fromJSON)
                               <*> (pure $ lookup "insertFinalNewline" arg >>= fromJSON)
                               <*> (pure $ lookup "trimFinalNewlines" arg >>= fromJSON)
                               <*> (pure $ catMaybes $ map sequence $ map (mapSnd fromJSON) $ filter (\(k, _) => not $ k `elem` fields) $ toList arg)
    where
      fields : List String
      fields = ["tabSize", "insertSpaces", "trimTrailingWhitespace", "insertFinalNewline", "trimFinalNewlines"]
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_formatting
public export
record DocumentFormattingParams where
  constructor MkDocumentFormattingParams
  workDoneToken : Maybe ProgressToken
  textDocument  : TextDocumentIdentifier
  options       : FormattingOptions
%runElab deriveJSON defaultOpts `{{DocumentFormattingParams}}

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

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

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

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_rangeFormatting
public export
record DocumentRangeFormattingParams where
  constructor MkDocumentRangeFormattingParams
  workDoneToken : Maybe ProgressToken
  textDocument  : TextDocumentIdentifier
  range         : Range
  options       : FormattingOptions
%runElab deriveJSON defaultOpts `{{DocumentRangeFormattingParams}}

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

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_onTypeFormatting
public export
record DocumentOnTypeFormattingOptions where
  constructor MkDocumentOnTypeFormattingOptions
  firstTriggerCharacter : Char
  moreTriggerCharacter  : Maybe (List Char)
%runElab deriveJSON defaultOpts `{{DocumentOnTypeFormattingOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_onTypeFormatting
public export
record DocumentOnTypeFormattingRegistrationOptions where
  constructor MkDocumentOnTypeFormattingRegistrationOptions
  firstTriggerCharacter : Char
  moreTriggerCharacter  : Maybe (List Char)
  documentSelector      : OneOf [DocumentSelector, Null]
%runElab deriveJSON defaultOpts `{{DocumentOnTypeFormattingRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_onTypeFormatting
public export
record DocumentOnTypeFormattingParams where
  constructor MkDocumentOnTypeFormattingParams
  textDocument : TextDocumentIdentifier
  ch           : Char
  options      : FormattingOptions
%runElab deriveJSON defaultOpts `{{DocumentOnTypeFormattingParams}}


text:
||| Provide Do-Notation support for Transition Indexed Monad.
||| Withouth this, the Indexed interfaces use operators that
||| do not collide with the non-Indexed interfaces.
module Control.Monad.TransitionIndexed.Do

import Control.Monad.TransitionIndexed

public export
(>>=) : TransitionIndexedMonad z m => m a x f -> ((res : a) -> m b (f res) g) -> m b x g
(>>=) = (>>>=)

public export
(>>) : TransitionIndexedMonad z m => m () x f -> Lazy (m b (f ()) g) -> m b x g
(>>) = (>>>)

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
{- Ctrl-Alt-A: Add definition
   Ctrl-Alt-C: Case split
   Ctrl-Alt-D: Documentation
   Ctrl-Alt-L: Lift hole: Lifts a hole to the top level as a new function definition
   Ctrl-Alt-M: Match: Replaces a hole with a case expression that matches on an intermediate result
   Ctrl-Alt-R: Reloads and typechecks the current buffer
   Ctrl-Alt-S: Search
   Ctrl-Alt-T: Type-check: Displays the type under cursor -}
module Main

import Data.SortedMap
import Data.SortedSet
import Control.Monad.State
import Control.Monad.Reader
import Prelude.Traversable
import Text.PrettyPrint.WL

interface Pretty p where
  doc : p -> Doc

(Pretty p1, Pretty p2) => Pretty (Pair p1 p2) where
  doc (p1, p2) = brackets (doc p1 |++| text "," |++| doc p2)

Pretty p => Pretty (List p) where
  doc ps = vsep (map doc ps)

Pretty Nat where
  doc = text . show

-- Arity
data Arity = MkArity Nat
Eq Arity where
  (MkArity a1) == (MkArity a2) = a1 == a2
Show Arity where
  show (MkArity a) = show a
Pretty Arity where
  doc (MkArity a) = text $ show a

-- Var
data Var = MkVar String
Eq Var where
  (MkVar v1) == (MkVar v2) = v1 == v2
Ord Var where
  compare (MkVar v1) (MkVar v2) = compare v1 v2
Pretty Var where
  doc (MkVar v) = text v

--  Constructor
data Cnst
  = MkCnst String
  | PCnst String
Eq Cnst where
  (MkCnst v1) == (MkCnst v2) = v1 == v2
  (PCnst c1) == (PCnst c2) = c1 == c2
  _ == _ = False
Show Cnst where
  show (MkCnst v) = show v
  show (PCnst v) = show v
Ord Cnst where
  compare (MkCnst c1) (MkCnst c2) = compare c1 c2
  compare (PCnst c1) (PCnst c2) = compare c1 c2
  compare (MkCnst c1) (PCnst c2) = LT
  compare (PCnst c1) (MkCnst c2) = GT
Pretty Cnst where
  doc (MkCnst v) = text v
  doc (PCnst c) = text c

-- Expr
data Expr
  = Call Cnst (List Var)
  | Pap Cnst (List Var)
  | App Var Var
  | Ctor Int (List Var)
  | Proj Int Var
  | Reset Var
  | Reuse Var Int (List Var)
Eq Expr where
  (Call c1 vs1)     == (Call c2 vs2)      = c1 == c2 && vs1 == vs2
  (Pap c1 vs1)      == (Pap c2 vs2)       = c1 == c2 && vs1 == vs2
  (App v11 v12)     == (App v21 v22)      = v11 == v21 && v21 == v22
  (Ctor i1 v1)      == (Ctor i2 v2)       = i1 == i2 && v1 == v2
  (Proj i1 v1)      == (Proj i2 v2)       = i1 == i2 && v1 == v2
  (Reset v1)        == (Reset v2)         = v1 == v2
  (Reuse v1 i1 vs1) == (Reuse v2 i2 vs2)  = v1 == v2 && i1 == i2 && vs1 == vs2
  _ == _ = False
Pretty Expr where
  doc e = case e of
    Call c vs     => hsep (doc c :: map doc vs)
    Pap c vs      => hsep (text "pap" :: doc c :: map doc vs)
    App x y       => hsep [doc x, doc y]
    Ctor i vs     => hsep (text "ctor" :: text (show i) :: map doc vs)
    Proj i v      => hsep [text "proj", text (show i), doc v]
    Reset v       => hsep [text "reset", doc v]
    Reuse v i vs  => hsep (text "reuse" :: doc v :: text "in" :: text "ctor" :: text (show i) :: map doc vs)

data Phase
  = Pure
  | RC -- Reset/Reuse
  | OC -- Owned Const

data FnBody : Phase -> Type where
  Ret  : Var                            -> FnBody p
  Let  : Var -> Expr -> FnBody p        -> FnBody p
  Case : Var -> List (Arity, FnBody p)  -> FnBody p
  Inc  : Var -> FnBody p                -> FnBody p
  Dec  : Var -> FnBody p                -> FnBody p
  LetC : Cnst -> Cnst -> FnBody p       -> FnBody p -- let cO := c
Pretty (FnBody p) where
  doc e = case e of
    Ret  v      => text "ret" |++| doc v
    Let  v e b  => text "let" |++| doc v |++| text "=" |++| doc e |+| text ";" |$$| doc b
    Case v alts => text "case" |++| doc v |$$| indent 2 (vsep (map (\(a,b) => parens (indent 1 (doc b) |+| text " ")) alts))
    Inc  v b    => text "inc" |++| doc v |++| text ";" |$$| doc b
    Dec  v b    => text "dec" |++| doc v |++| text ";" |$$| doc b
    LetC o c b  => text "let" |++| doc o |++| text ":=" |$$| doc b

eqFnBody : FnBody p -> FnBody p -> Bool
eqFnBody b1 b2 = case (b1, b2) of
  (Ret v1, Ret v2)              => v1 == v2
  (Let v1 e1 b1, Let v2 e2 b2)  => v1 == v2 && e1 == e2 && eqFnBody b1 b2
  (Case v1 as1, Case v2 as2)    => v1 == v2 && length as1 == length as2 && and (zipWith (\(a1,c1) , (a2,c2) => a1 == a2 && eqFnBody c1 c2) as1 as2)
  (Inc v1 b1, Inc v2 b2)        => v1 == v2 && eqFnBody b1 b2
  (Dec v1 b1, Dec v2 b2)        => v1 == v2 && eqFnBody b1 b2
  (LetC o1 c1 b1, LetC o2 c2 b2) => o1 == o2 && c1 == c2 && eqFnBody b1 b2
  (_, _)                        => False

data Fun : Phase -> Type where
  MkFun : List Var -> FnBody p -> Fun p
Pretty (Fun p) where
  doc (MkFun ps b) = hsep (map doc ps) |++| text "=" |$$| indent 2 (doc b)

data Program : Phase -> Type where
  MkProgram : List (Cnst, Fun p) -> Program p
Pretty (Program p) where
  doc (MkProgram fs) = vsep $ map (\(n,f) => doc n |++| doc f) fs

swapExample : Program Pure
swapExample = MkProgram
  [ ( swap
    , MkFun [xs]
      $ Case xs
        [ (MkArity 0, Ret xs)
        , (MkArity 2, Let t1 (Proj 2 xs)
                    $ Case t1
                      [ (MkArity 0, Ret xs)
                      , (MkArity 2, Let h1 (Proj 1 xs)
                                  $ Let h2 (Proj 2 t1)
                                  $ Let t2 (Proj 2 t1)
                                  $ Let r1 (Ctor 2 [h1, t2])
                                  $ Let r2 (Ctor 2 [h2, r1])
                                  $ Ret r2
  )])])]
  where
    swap = MkCnst "swap"
    xs = MkVar "xs"
    t1 = MkVar "t1"
    t2 = MkVar "t2"
    h1 = MkVar "h1"
    h2 = MkVar "h2"
    r1 = MkVar "r1"
    r2 = MkVar "r2"

mapExample : Program Pure
mapExample = MkProgram
  [ ( map
    , MkFun [f, xs]
        $ Case xs
          [ (MkArity 0, Ret xs)
          , (MkArity 2, Let x  (Proj 1 xs)
                      $ Let s  (Proj 2 xs)
                      $ Let y  (App f x)
                      $ Let ys (Call map [f, s])
                      $ Let r  (Ctor 2 [y, ys])
                      $ the (FnBody Pure) (Ret r))
          ]
    )
  ]
  where
    map = MkCnst "map"
    f = MkVar "f"
    x = MkVar "x"
    s = MkVar "s"
    r = MkVar "r"
    y = MkVar "y"
    ys = MkVar "ys"
    xs = MkVar "xs"

-- Originally S
insertReuse : Var -> Arity -> FnBody RC -> FnBody RC
insertReuse w n f = case f of
  Ret x     => Ret x
  Case x fs => Case x (map (\(a, f) => (a, insertReuse w n f)) fs)
  Let x e g => case e of
    Ctor i ys => if MkArity (List.length ys) == n
                    then Let x (Reuse w i ys) g
                    else Let x (Ctor i ys) (insertReuse w n g)
    e' => Let x e (insertReuse w n g)
  Dec x g => Dec x g
  Inc x g => Inc x g
  LetC c1 c2 g => LetC c1 c2 g

-- NewName
data NewNameT : (f : Type -> Type) -> (a : Type) -> Type where
  NewName : StateT Nat m a -> NewNameT m a

unNewName : NewNameT m a -> StateT Nat m a
unNewName (NewName m) = m

runNewNameT : Monad m => NewNameT m a -> m a
runNewNameT (NewName s) = fst <$> runStateT s 0

runNewName : NewNameT Identity a -> a
runNewName = runIdentity . runNewNameT

Functor f => Functor (NewNameT f) where
  map f (NewName s) = NewName (map f s)

(Functor (NewNameT f), Applicative (StateT Nat f)) => Applicative (NewNameT f) where
  pure x                      = NewName (pure x)
  (NewName f) <*> (NewName x) = NewName (f <*> x)

(Monad (StateT Nat f), Applicative (NewNameT f)) => Monad (NewNameT f) where
   (NewName m) >>= k = NewName $ do
     x <- m
     unNewName (k x)

freshVar : Monad m => NewNameT m Var
freshVar = NewName $ do
  n <- get
  put (S n) -- TODO: How to increment nat??? :)
  pure $ MkVar $ "w" ++ show n

freshCnst : Monad m => NewNameT m Cnst
freshCnst = NewName $ do
  n <- get
  put (S n)
  pure $ PCnst ("c" ++ show n)

total
inExpr : Var -> Expr -> Bool
inExpr v e = case e of
  (Call c vs)     => v `elem` vs
  (Pap c vs)      => v `elem` vs
  (App x y)       => x == v || y == v
  (Ctor i vs)     => v `elem` vs
  (Proj i x)      => v == x
  (Reuse x i vs)  => (v `elem` vs) || (v == x)
  (Reset x)       => v == x

-- total : TODO: List is not strong enough
inFBody : Var -> FnBody p -> Bool
inFBody v f = case f of
  Ret  x      => v == x
  Let  x e b  => v == x || (inExpr v e) || (inFBody v b)
  Case x alts => v == x || (foldl (\x,y => x && y) True (map (inFBody v . snd) alts)) -- TODO: How to use and here?
  Inc  x b    => v == x || (inFBody v b)
  Dec  x b    => v == x || (inFBody v b)
  LetC _ _ b  => inFBody v b

insertResetIns : Monad m => Var -> Arity -> FnBody RC -> NewNameT m (FnBody RC)
insertResetIns z n f = do
  w <- freshVar
  let g = insertReuse w n f
  pure $ if not $ eqFnBody g f
            then Let w (Reset z) g
            else f

-- Originally D
insertReset : Monad m => Var -> Arity -> FnBody RC -> NewNameT m (FnBody RC)
insertReset z n f = case f of
  Dec x g   => pure $ Dec x g
  Inc x g   => pure $ Inc x g
  LetC o c g => LetC o c <$> insertReset z n g
  Ret x     => pure $ Ret x
  Case x gs => Case x <$> traverse (\(a, g) => (\v => (a,v)) <$> insertReset z n g) gs
  Let x e g =>
    case ((inExpr z e) || (inFBody z g)) of
      True  => Let x e <$> insertReset z n g
      False => insertResetIns z n f

-- Originally R
resetReuse : Monad m => FnBody Pure -> NewNameT m (FnBody RC)
resetReuse b = case b of
  Ret x     => pure $ Ret x
  Let x e f => Let x e <$> resetReuse f
  LetC o c f => LetC o c <$> resetReuse f
  Case x bs => Case x <$> traverse (\(arity, body) => do
                                        body' <- resetReuse body
                                        (MkPair arity) <$> (insertReset x arity body'))
                                   bs

resetReuseFun : Monad m => Fun Pure -> NewNameT m (Fun RC)
resetReuseFun (MkFun ps body) = MkFun ps <$> resetReuse body

resetReuseProgram : Monad m => Program Pure -> NewNameT m (Program RC)
resetReuseProgram (MkProgram defs) = MkProgram <$> traverse (\(n,f) => (MkPair n <$> resetReuseFun f)) defs

||| Inserts local constant
insertLetCFnBody : Monad m => FnBody p -> NewNameT m (FnBody p) -- TODO: Right phase parameter
insertLetCFnBody b = case b of
  Ret  v => pure $ Ret v
  Let  v e g => case e of
                  (Pap c xs) => do
                    c2 <- freshCnst
                    (LetC c2 c . Let v (Pap c2 xs)) <$> insertLetCFnBody g
                  e0 => Let v e0 <$> insertLetCFnBody g
  Case v alts => Case v <$> traverse (\(a,g) => MkPair a <$> insertLetCFnBody g) alts
  Inc  v g => Inc v <$> insertLetCFnBody g
  Dec  v g => Dec v <$> insertLetCFnBody g
  LetC c1 c2 g => LetC c1 c2 <$> insertLetCFnBody g

insertLetCFun : Monad m => Fun p -> NewNameT m (Fun p)
insertLetCFun (MkFun ps body) = MkFun ps <$> insertLetCFnBody body

insertLetCProgram : Monad m => Program p -> NewNameT m (Program p)
insertLetCProgram (MkProgram defs) = MkProgram <$> traverse (\(n,f) => (MkPair n <$> insertLetCFun f)) defs

{-
Inferring borrowing signatures:
Every function parameter is annotated with Owned or Borrowed

Our heruristing pcollects which parameters and variables should be owned.
We say a parameter should be owned
  - if x or one of its projections is used in a reset
  - is passed to a function that takes an owned reference.
    (This is heuristic and not required for correctness)
-}

data Borrowing
  = Owned
  | Borrowed
Eq Borrowing where
  Owned     == Owned    = True
  Borrowed  == Borrowed = True
  _         == _        = False
Show Borrowing where
  show Owned = "Owned"
  show Borrowing = "Borrowing"
Pretty Borrowing where
  doc Owned     = text "Owned"
  doc Borrowed  = text "Borrowed"

BorrowingMap : Type
BorrowingMap = SortedMap (Cnst, Nat) Borrowing

borrowed : BorrowingMap -> (Cnst, Nat) -> Maybe Borrowing
borrowed b (PCnst _, _) = Just Owned
borrowed b (c,n)        = Data.SortedMap.lookup (c,n) b

constBorrowingParams : BorrowingMap -> Cnst -> List Borrowing
constBorrowingParams bm c
  = map snd
  $ sortBy (\((_, e1), _) , ((_, e2), _) => compare e1 e2)
  $ filter ((c ==) . fst . fst) $ Data.SortedMap.toList bm

number : List a -> List (Nat, a)
number = snd . foldl (\(n, ns), a => (S n, (n,a) :: ns)) (Z, [])

||| Collects the owned variables in a function body
collectOwnedVars : BorrowingMap -> FnBody rc -> SortedSet Var
collectOwnedVars beta b = case b of -- TODO: Unicode Beta
  Let z (Ctor i xs)     f => collectOwnedVars beta f
  Let z (Reuse x i xs)  f => collectOwnedVars beta f
  Let z (Call c xs)     f
    => union (collectOwnedVars beta f)
             (fromList
              (concatMap (\(n,x) => maybe [x]
                                          (\b => if b == Owned then [x] else [])
                                          (borrowed beta (c,n)))
                         (number xs)))
  Let z (Reset x)       f => insert x (collectOwnedVars beta f)
  Let z (App x y)       f => union (collectOwnedVars beta f) (fromList [x, y])
  Let z (Pap cO xs)     f => union (collectOwnedVars beta f) (fromList xs)
  -- TODO: Define a wrapper constant transformation for partial application
  -- as we assume that partially applied functions always have Owned parameters.
  Let z (Proj i x)      f => let c = collectOwnedVars beta f
                             in if contains z c
                                  then insert x c
                                  else c
  Ret x => empty
  Case z alts => foldl1 union $ map (collectOwnedVars beta . snd) alts
  Inc z f => collectOwnedVars beta f
  Dec z f => collectOwnedVars beta f
  LetC o c f => collectOwnedVars beta f

ownedFunctionVar : BorrowingMap -> Fun p -> List (Nat, Borrowing)
ownedFunctionVar beta (MkFun ps body) = snd $ foldl borrowed (0, []) ps
  where
    c : SortedSet Var
    c = collectOwnedVars beta body

    borrowed : (Nat, List (Nat, Borrowing)) -> Var -> (Nat, List (Nat, Borrowing))
    borrowed (n, vs) v = (n + 1, (n, if contains v c then Owned else Borrowed) :: vs)

ownedParameters : BorrowingMap -> Program p -> BorrowingMap
ownedParameters beta (MkProgram funs) = foldl insertFun empty funs
  where
    insertFun : BorrowingMap -> (Cnst, Fun p) -> BorrowingMap
    insertFun s (name, fun) = foldl (\s1, (n, b) => insert (name, n) b s1) s (ownedFunctionVar beta fun)

startBorrowingMap : Program p -> BorrowingMap
startBorrowingMap (MkProgram funs) = foldl insertFunSignature empty funs
  where
    insertFunSignature : BorrowingMap -> (Cnst, Fun p) -> BorrowingMap
    insertFunSignature beta (cnst, MkFun ps _) = fromList
      [ ((cnst, n), Borrowed) | (n,_) <- number ps ]

Eq BorrowingMap where
  m1 == m2 = toList m1 == toList m2

calculateOwnedParameters : Program p -> BorrowingMap
calculateOwnedParameters program = go empty (startBorrowingMap program)
  where
    go : BorrowingMap -> BorrowingMap -> BorrowingMap
    go previous actual = if previous == actual
                            then actual
                            else ownedParameters previous program

BorrowVarMap : Type
BorrowVarMap = Var -> Borrowing

varsInExp : Expr -> SortedSet Var
varsInExp e = case e of
  Call c  vs    => SortedSet.fromList vs
  Pap  c  vs    => SortedSet.fromList vs
  App  v1 v2    => SortedSet.fromList [v2] -- ???
  Ctor i  vs    => SortedSet.fromList vs
  Proj i  v     => SortedSet.fromList [v]
  Reset v       => SortedSet.fromList [v]
  Reuse v i vs  => SortedSet.fromList $ v :: vs

freeVars : FnBody p -> SortedSet Var
freeVars f = case f of
  Ret  x        => fromList [x]
  Let  x e b    => delete x $ union (varsInExp e) (freeVars b)
  Case x alts   => insert x $ foldl1 union $ map (freeVars . snd) alts
  -- Special cases
  Inc  x b      => insert x $ freeVars b
  Dec  x b      => insert x $ freeVars b
  LetC c1 c2 b  => freeVars b

ownPlus : Var -> SortedSet Var -> BorrowVarMap -> FnBody p -> FnBody p
ownPlus x vars beta f = if (not (contains x vars)) && (beta x == Owned)
  then f
  else Inc x f

ownMinus_ : Var -> SortedSet Var -> BorrowVarMap -> FnBody p -> FnBody p
ownMinus_ x freeVars beta f = if (not (contains x freeVars)) && (beta x == Owned)
  then Dec x f
  else f

ownMinuses_ : List Var -> SortedSet Var -> BorrowVarMap -> FnBody p -> FnBody p
ownMinuses_ []        freeVars beta f = f
ownMinuses_ (x :: xs) freeVars beta f = ownMinuses_ xs freeVars beta (ownMinus_ x freeVars beta f)

ownMinus : Var -> BorrowVarMap -> FnBody p -> FnBody p
ownMinus x beta f = ownMinus_ x (freeVars f) beta f

ownMinuses : List Var -> BorrowVarMap -> FnBody p -> FnBody p
ownMinuses xs beta f = ownMinuses_ xs (freeVars f) beta f

assignBorrowMap : Var -> Borrowing -> BorrowVarMap -> BorrowVarMap
assignBorrowMap x b f v = if x == v then b else f v

insertIncDecApp : Monad m => List Var -> List Borrowing -> BorrowVarMap -> FnBody p -> m (FnBody p)
insertIncDecApp (y :: ys) (Owned    :: bs) beta (Let z e f)
  = ownPlus y (union (freeVars f) (fromList ys)) beta <$> insertIncDecApp ys bs beta (Let z e f)
insertIncDecApp (y :: ys) (Borrowed :: bs) beta (Let z e f)
  = insertIncDecApp ys bs beta (Let z e (ownMinus y beta f))
insertIncDecApp ys os beta f = pure f

--insertIncDec1 : (Monad m, MonadReader BorrowingMap m) => BorrowVarMap -> FnBody p -> m (FnBody p)
--insertIncDec1 beta (Ret v)        = pure (ownPlus v empty beta (Ret v))
--insertIncDec1 beta (Inc v b)      = Inc v <$> insertIncDec1 beta b
--insertIncDec1 beta (Dec v b)      = Dec v <$> insertIncDec1 beta b
--insertIncDec1 beta (LetC c1 c2 b) = LetC c1 c2 <$> insertIncDec1 beta b
--insertIncDec1 beta f@(Case v alts)
--  = Case v <$> traverse
--      (\(arity, b0) => map (MkPair arity . ownMinuses (SortedSet.toList (freeVars f)) beta) $ insertIncDec1 beta b0)
--      alts
--insertIncDec1 beta (Let w e b) with (e)
--  insertIncDec1 beta (Let w e b) | Proj i x     = insertIncDec1 beta b
--  insertIncDec1 beta (Let w e b) | Reset x      = insertIncDec1 beta b
--  insertIncDec1 beta (Let w e b) | Call c ys    = insertIncDec1 beta b
--  insertIncDec1 beta (Let w e b) | Pap c ys     = insertIncDec1 beta b
--  insertIncDec1 beta (Let w e b) | App x y      = insertIncDec1 beta b
--  insertIncDec1 beta (Let w e b) | Ctor i ys    = insertIncDec1 beta b
--  insertIncDec1 beta (Let w e b) | Reuse x i ys = insertIncDec1 beta b

insertIncDec : (Monad m, MonadReader BorrowingMap m) => BorrowVarMap -> FnBody p -> m (FnBody p)
insertIncDec beta f = case f of
  Ret  v     => pure $ ownPlus v empty beta (Ret v)
  Let  w e b => case e of
                  (Proj i x)     => case beta x of
                                      Owned  => Let w (Proj i x) . Inc w . ownMinus x beta <$> insertIncDec beta b
                                      Borrowed => Let w (Proj i x) <$> insertIncDec (assignBorrowMap w Borrowed beta) b
                  (Reset x)      => Let w (Reset x) <$> insertIncDec beta b
                  (Call c ys)    => do
                    bm <- ask
                    b1 <- insertIncDec beta b
                    insertIncDecApp ys (constBorrowingParams bm c) beta $ Let w (Call c ys) b1
                  (Pap c ys)     => do
                    bm <- ask
                    b1 <- insertIncDec beta b
                    insertIncDecApp ys (constBorrowingParams bm c) beta $ Let w (Pap c ys) b1
                  (App x y)      => do
                    b1 <- insertIncDec beta b
                    insertIncDecApp [x,y] [Owned, Owned] beta $ Let w (App x y) b1
                  (Ctor i ys)    => do
                    b1 <- insertIncDec beta b
                    insertIncDecApp ys (const Owned <$> ys) beta $ Let w (Ctor i ys) b1
                  (Reuse x i ys) => do
                    b1 <- insertIncDec beta b
                    insertIncDecApp ys (const Owned <$> ys) beta $ Let w (Reuse x i ys) b1
  Case v alts => let fv = SortedSet.toList (freeVars f)
                 in Case v <$> traverse
                                (\(arity, b0) => do
                                    b1 <- insertIncDec beta b0
                                    let b2 = ownMinuses fv beta b1
                                    pure (arity, b2))
                                alts
  Inc  v     b  => Inc  v      <$> insertIncDec beta b
  Dec  v     b  => Dec  v      <$> insertIncDec beta b
  LetC c1 c2 b  => LetC c1 c2  <$> insertIncDec beta b

funInsertIncDec : (Monad m, MonadReader BorrowingMap m) => Cnst -> Fun p -> m (Fun p)
funInsertIncDec funName (MkFun args body) = do
  bm <- ask
  let argNum = \x => findIndex (x==) args
  let beta = \x => case argNum x of
                    Nothing => Owned
                    Just n => case Data.SortedMap.lookup (funName, n) bm of
                      Nothing => Owned
                      Just r  => r
  (MkFun args . ownMinuses args beta) <$> insertIncDec beta body

programInsertIncDec : (Monad m, MonadReader BorrowingMap m) => Program p -> m (Program p)
programInsertIncDec (MkProgram funDefs) = MkProgram <$> traverse (\(c, f) => MkPair c <$> funInsertIncDec c f) funDefs

prettyPutStrLn : (Pretty p) => p -> IO ()
prettyPutStrLn = putStrLn . toString 1.0 80 . doc

main : IO ()
main = do
  let mapExampleRC = runNewName $ do
        p1 <- resetReuseProgram mapExample
        p2 <- insertLetCProgram p1
        pure p2
  let swapExampleRC = runNewName $ do
        p1 <- resetReuseProgram swapExample
        p2 <- insertLetCProgram p1
        pure p2
  putStrLn ""
  prettyPutStrLn mapExample
  prettyPutStrLn mapExampleRC
  putStrLn ""
  prettyPutStrLn swapExample
  prettyPutStrLn swapExampleRC
  putStrLn "Owned parameters: Map example"
  printLn $ ownedParameters empty mapExampleRC
  prettyPutStrLn $ toList $ ownedParameters empty mapExampleRC
  putStrLn "Owned parameters: Swap example"
  printLn $ ownedParameters empty swapExampleRC
  prettyPutStrLn $ toList $ ownedParameters empty swapExampleRC
  printLn "Start Borrowing Maps"
  let mco = calculateOwnedParameters mapExampleRC
  let sco = calculateOwnedParameters swapExampleRC
  printLn mco
  printLn sco
  let mapExampleRC2 = runIdentity $ runReaderT (programInsertIncDec mapExampleRC) sco
  prettyPutStrLn (the (Program RC) mapExampleRC2)
  let swapExampleRC2 = runIdentity $ runReaderT (programInsertIncDec swapExampleRC) sco
  prettyPutStrLn (the (Program RC) swapExampleRC2)

{-
Implementation of the Counting Immutable Beans (CIB) for the GRIN compiler.

CIB uses instrumentation of the original program. There are four new instructions in the syntax
that are inserted via instrumentation. This can be categorized into two;
- reference counter instructions:
  - inc
  - dec
- heap location reuse:
  - reset
  - reuse

In the CIB approach every heap location has a reference counter associated with it.
Inc increments the counter for the location, and also increments all the referred locations transitively.
Dec decrements the counter for the location, and also decrements all the referred locations transitively.

Reset, reuse:
From the CIB paper:
let y = reset x.
If x is a shared value, than y is set to a special pointer value BOX, otherwise to the heap location associated with x.
If x is not shared than reset decrements the reference counters of the components of x, and y is set to x.

let z = reuse y in ctor_i w.
If y is BOX reuse allocates a new heap for the constructor.
If y is not Box the runtime reuses the heap location for storing the constructor.

Application of the same idea for GRIN:
Differences: meanwhile Lean's IR put every variable on the heap, GRIN uses variables as were registers
and only a subset of the registers are associated with heap locations. A register is associated
with heap location if its type is Loc. This means the GRIN implementation of the CIB approach needs
a type environment which tells which variables can be affected by the CIB operations.

In GRIN:
 * The CIB instrumentation should happen after the optimization steps.
 * Special interpreter should be implemented which handles the CIB instructions.
 * Probably it should have its own LLVM code generator and LLVM implemented runtime, preferably a plugin
   for the existing one.

We need to add 4 new instructions:
 * `x <- reset y;`   where y is a heap location, x can be a special heap location, which can be BOX too.
 * `z <- reuse x y;` where x is a special heap location created by reset, and y is a Node value.
 * `z <- inc x;`     where x is a heap location, it transitively increments the reference counters in the locations.
                     cycle detection should happen. The increment operation computes unit as its return value.
 * `z <- dec x;`     where x is a heap location, it transitively decrements the reference counters in the locations.
                     cycle detection should happen. When the counter reaches zero, the runtime must deallocate
                     the location. The decrement operation computes unit as its return value.

The GRIN nodes store primitive values, but the runtime makes the difference between location values and
primitive values, thus it is able to create the transitive closure of the reachability relation of a location
and manipulate its reference counters.

Every of the four instructions needs to be implemented in the GRIN runtime/interpreter.

In the original paper reuse of the constructors could happen only of the arity of the constructors
are the same. But in GRIN as the runtime needs to allocate heaps based on the type of the heap location.
This means every heap location can have its own arity, and reuse if the heap location is possible
only if the new node does not exceeds the arity of the heap node. Otherwise a new node needs to
be allocated, with the maximum arity.

The most important change is the reuse construction. It changes certain instances of the
store operation to the reuse operation.

```
Before:
x <- store y;

After:
z <- reset w;
...
x <- reuse z y;
```

In this case we need to decide to reuse the heap location associated with w only if w can accommodate
all the possible values of x. This means the max-arity(w) >= max-arity(x). Meanwhile Lean's
approach uses the arity of the constructors in the alternatives, we can use the abstract information
of all the possible runs.

Implementation steps:
[ ] Import abstracting the definitional interpreters from the mini-grin repo
[ ] Change the implementation to use base functors instead of Expr datatype
[ ] Implement reference statistics with the new interpreter, as a warm-up exercise
[ ] Implement CIB program instrumentation for GRIN producing ExprF :+: CibF AST
[ ] Implement interpreter for CIB extended GRIN program
[ ] Extra: Implement LLVM codegen plugin for CIB instructions
-}

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 Main

import FndType

-- Lifted increment function. Input fund must be at least 1.
inc : (FndType (10 + fund) Int) -> (FndType fund Int)
-- inc = upliftFun (\x => (x + 1))
inc (FT i) = FT (i + 1)

-- Lifted decrement function. Input fund must be at least 1.
dec : (FndType (10 + fund) Int) -> (FndType fund Int)
-- dec = upliftFun (\x => (x - 1))
dec (FT i) = FT (i - 1)

-- Main
rich_42 : FndType 99 Int
rich_42 = FT 42
poor_42 : FndType 1 Int
poor_42 = FT 42
main : IO ()
main = do
  putStrLn (FndType.show rich_42)
  putStrLn (FndType.show (inc rich_42)) -- Decrement the fund while incrementing the content
  -- putStrLn (FndType.show (inc poor_42)) -- Just enough fund
  -- putStrLn (FndType.show ((compose inc dec) rich_42)) -- Decrement the fund by 2
  -- putStrLn (show ((compose inc dec) poor_42)) -- Not enough fund

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Consensus

import Types

%access public export

max_stars_repo_name: cwgoes/ibc-idris-ref

max_issues_repo_name: cwgoes/ibc-idris-ref

max_forks_repo_name: cwgoes/ibc-idris-ref


text:
module Data.HashMapSpec

import Data.HashMap
import Data.Vect
import Data.Vect
import Hedgehog

%hide Prelude.Range

data Op : Type -> Type -> Type where
    Insert : k -> v -> Op k v
    Delete : k -> Op k v

runOp : Op k v -> HashMap k v -> HashMap k v
runOp (Insert k v) = insert k v
runOp (Delete k) = delete k

runOps' : List (Op k v) -> HashMap k v -> HashMap k v
runOps' [] m = m
runOps' (op :: ops) m = runOps' ops (runOp op m)

runOps : Hashable k => Eq k => List (Op k v) -> HashMap k v
runOps ops = runOps' ops empty

genOp : Gen k -> Gen v -> Gen (Op k v)
genOp k v = choice [ [| Insert k v |], [| Delete k |] ]

genHashMap : Hashable k => Eq k => Range Nat -> Gen (Op k v) -> Gen (HashMap k v)
genHashMap size op = runOps <$> list size op

int1000 : Gen Int
int1000 = int $ linear 0 1000

genHMDefault : Gen (HashMap Int Int)
genHMDefault = genHashMap (linear 25 100) (genOp int1000 int1000)

insertLookupProp : Property
insertLookupProp = property $ do
    hm <- forAll genHMDefault
    k <- forAll int1000
    v <- forAll int1000
    Just v === lookup k (insert k v hm)

deleteLookupProp : Property
deleteLookupProp = property $ do
    hm <- forAll genHMDefault
    k <- forAll int1000
    v <- forAll int1000
    Nothing === lookup k (delete k (insert k v hm))

str25 : Gen String
str25 = string (linear 20 30) ascii

strInsertLookupProp : Property
strInsertLookupProp = property $ do
    hm <- forAll $ genHashMap (linear 100 150) (genOp str25 int1000)
    k <- forAll str25
    v <- forAll int1000
    Just v === lookup k (insert k v hm)

export
specHashMap : IO Bool
specHashMap =
    checkGroup $
        MkGroup "HashMap"
            [ ("lookup/insert", insertLookupProp)
            , ("lookup/delete", deleteLookupProp)
            , ("String lookup/insert", strInsertLookupProp)
            ]


text:
module Minecraft.Core.Item.Put.Export

import public Minecraft.Core.Item.Put

%default total

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
-- ------------------------------------------------------------ [ Solution.idr ]
-- Module    : Solution.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Parser problem specifications
module Sif.DSL.Parser.Solution

-- ----------------------------------------------------------------- [ Imports ]
import Lightyear
import Lightyear.Char
import Lightyear.Strings

import GRL.Lang.GLang

import Sif.Types
import Sif.AbsSyntax

import Sif.DSL.Parser.Utils
import Sif.DSL.Parser.Common
import Sif.DSL.Parser.Problem

import Test.Parsing

-- -------------------------------------------------------------- [ Directives ]
%default partial
%access private

-- ----------------------------------------------------------------- [ Parsers ]

traitTy : Parser TTy
traitTy = (keyword "Advantage"    *> return ADV)
      <|> (keyword "Disadvantage" *> return DIS)
      <|> (keyword "Trait"        *> return GEN)
      <?> "Trait Type"

cValue : Parser CValue
cValue = (keyword "Makes"   *> return MAKES)
     <|> (keyword "Helps"   *> return HELPS)
     <|> (keyword "SomePos" *> return SOMEPOS)
     <|> (keyword "Unknown" *> return UNKNOWN)
     <|> (keyword "SomeNeg" *> return SOMENEG)
     <|> (keyword "Breaks"  *> return BREAK)
     <|> (keyword "Hurts"   *> return HURTS)
     <?> "CValue"

sValue : Parser SValue
sValue = (keyword "Denied"    *> return DENIED)
     <|> (keyword "WeakDen"   *> return WEAKDEN)
     <|> (keyword "WeakSatis" *> return WEAKSATIS)
     <|> (keyword "Satisfied" *> return SATISFIED)
     <|> (keyword "Undecided" *> return UNDECIDED)
     <|> (keyword "None"      *> return NONE)
     <?> "Trait Type"

affect : Parser $ SifAST TyAFFECTS
affect = do
    c <- cValue
    spaces
    i <- ident
    spaces
    d <- opt $ (keyword "by" *> descString <* spaces)
    pure $ AST.Affect c i d
  <?> "Affects"

affects : Parser $ List $ SifAST TyAFFECTS
affects = do
    keyword "Affects"
    as <- braces $ commaSep1 affect
    sifComment
    pure as

trait : Parser $ SifAST TyTRAIT
trait = do
      d <- opt sifDoc
      ty <- traitTy
      t <- title
      keyword "is"
      s <- sValue
      as <- braces affects
      sifComment
      pure $ AST.Trait ty t s d as
    <?> "Trait"

property : Parser $ SifAST TyPROPERTY
property = do
      d <- opt sifDoc
      keyword "Property"
      t <- title
      ts <- braces $ some trait
      sifComment
      pure $ AST.Property t d ts
    <?> "Property"

doctype : Parser ()
doctype = do
      sifComment
      keyword "sif"
      spaces
      string "solution"
      sifComment
  <?> "DocType"

solHeader : Parser (Maybe String, String, String, String)
solHeader = do
      d <- opt sifDoc
      keyword "Solution"
      t <- title
      keyword "solves"
      spaces
      pID <- ident
      keyword "in"
      cID <- ident
      pure (d, t, pID, cID)
  <?> "Solution Header"

export
solution : Parser $ (SifAST TySOLUTION)
solution = do
      doctype
      pd <- opt desc
      (d, t, pID, cID) <- solHeader
      ps <- braces $ some property
      pure $ AST.Solution t (pID,pd) d cID ps
    <?> "Solution"

export
runTests : IO ()
runTests = do
  putStrLn $ heading "Parsing Solution Tests"
  canParse (Just "Solution Header") solHeader "Solution \"Why does this not work\" solves adt in blah"

  canParse (Just "Solution Header with Docs")
           solHeader
           """> I am docs
> I am docs

Solution "Why does this not work" solves adt in blah"""

  canParse (Just "Affect") affect "Hurts foobar"
  canParse (Just "Affect") affect "Hurts foobar by \"doing something\""

  canParse (Just "Affects")
           (many affects)
           """Affects { Makes foobar }

Affects {Makes foobar, Breaks bank by "dropping like its hot"}
"""
  canParse (Just "Affect with Docs")
           (many affects)
           """> I am doc
Affects { Makes foobar }

> AASAS
Affects {Makes foobar, Breaks bank by "dropping like its hot"}
"""

  canParse (Just "Trait")
            (trait)
            """Trait "A Trait" is Satisfied {
  Affects {Makes foobar, Breaks bank by "dropping like its hot"}}
"""

  canParse (Just "Trait with Docs")
            (trait)
            """> Asasasasas
Trait "A Trait" is Satisfied {
  Affects {Makes foobar, Breaks bank by "dropping like its hot"}}
"""

  canParse (Just "Property")
            (property)
            """Property "A Property" { Trait "A Trait" is Satisfied {
  Affects {Makes foobar, Breaks bank by "dropping like its hot"}}}
"""

  canParse (Just "Property with Docs")
            (property)
            """> I am docs

Property "A Property" { Trait "A Trait" is Satisfied {
  Affects {Makes foobar, Breaks bank by "dropping like its hot"}}}
"""

  canParse (Just "A Trait")
           trait
           """> There is possibility that the implementation of the algorithm is insecure/poor.
	Trait "Implementation InSecure" is WeakSatis {
	  Affects {
	    SomeNeg recipConf, SomeNeg dataConf, Unknown minDisrupt, SomeNeg secureImpl
	  }
	}
           """

  canParse (Just "Another Heading")
           solHeader
           """> Public key crypto schemes are an application of asymmetric
> cryptography in which the public/private key pair is used for
> encryption/decryption respectively. Asymmetric crypto schemes
> consist of three algorithms.
> \
> + keygen :: Given a security parameter generates a public private key pair.
> + encrypt :: Given a public key and a message, encrypts the message under the given public key.
> + decrypt :: Given a private key and a ciphertext, =decrypt= returns a readable plaintext if the private key was paired with the ciphertexts encryption key.
Solution "Public Key Cryptography" solves infosec in std
           """

  canParse (Just "Maths Algorithm")
           property
           """> The underlying mathematical algorithm that provides the asymmetric cipher used.
  Property "Maths Algorithm" {

    > There will be a formal proof of the operations working.
    Advantage "Formal Guarantee" is Satisfied {
      Affects { Helps dataConf, Helps recipConf }
    }

	> The maths algorithm is generally computationally expensive on large data.
    Disadvantage "Computationally Expensive" is WeakSatis {
      Affects { Hurts mechPerf, Hurts minDisrupt }
    }

  }
"""
  canParse (Just "Implementation in Code")
           property
           """> The implementation in Code
  Property "Implementation in Code" {

    > There is possibility that the implementation of the algorithm is insecure/poor.
	Trait "Implementation InSecure" is WeakSatis {
	  Affects {
	    SomeNeg recipConf, SomeNeg dataConf, Unknown minDisrupt, SomeNeg secureImpl
	  }
	}

	> Some implementations really make it hard to understand things
	Trait "Implementation obfuscates understanding" is WeakDen {
	  Affects { Hurts understandable, Hurts minDisrupt }
    }
  }
"""

  canParse (Just "Ket Distribution Trait")
           trait
           """> A means of key distribution is required to ensure that public key ownership can be attested.
	Trait "Key Distribution" is Satisfied {
       Affects {
         SomeNeg recipConf by "Keys are distributed insecurely.",
		 SomeNeg minDisrupt by "Incorrect Distribution."
       }
    }"""

  canParse (Just "Key Pairs")
           property
           """> There are two keys in use.
  Property "Key Pairs" {

    > Reduces problems with Key Security
    Advantage "PublicEnc/PrivateDec Keys" is Satisfied {
       Affects { Makes recipConf by "Only recipient has key to unlock the message" }
    }

	> A means of key distribution is required to ensure that public key ownership can be attested.
	Trait "Key Distribution" is Satisfied {
       Affects {
         SomeNeg recipConf by "Keys are distributed insecurely.",
		 SomeNeg minDisrupt by "Incorrect Distribution."
       }
    }

	> This solution requires the management of keys. That is, for each recipient the sender has to obtain a encryption key.
    Trait "Key Management" is Satisfied {
	   Affects {
	     SomeNeg dataConf by "Possibly sending data encrypted under the wrong key."
	   }
	}
  }
"""

  canParse (Just "Var Sec Params")
           property
           """> Different algorithm's will have different security parameters, and may allow different key lengths.
  Property "Variable Security Parameters" {

    > Many algorithms have variable security levels. Data can been secured at various levels.
    Advantage "Greater Security" is Satisfied {
	    Affects { Helps multiSecLevels }
	}

   > Common parameters are required to be selected and agreed upon.
   Trait "Parameter Selection" is Satisfied {
        Affects {
		    SomeNeg multiSecLevels by "insecure parameters being selected."
		  , SomeNeg secureImpl     by "insecure paremeters being selected."
		}
   }

   > Some parameters though secure might occur a greater processing cost.
   Disadvantage "Parameter Computation" is Satisfied {
       Affects { Hurts mechPerf, Hurts minDisrupt }
   }
  }"""

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Q
import ZZ
import GCDZZ
import Divisors
import Monoid
import Rationals
import ZZUtils
import TwoVarDiophEq
import NatUtils

|||data type for rationals
data Q : Type where
  PbySq : (p: ZZ) -> (q: Nat) -> Q

ZQ : Q
ZQ = PbySq (Pos Z) Z

OneQ : Q
OneQ = PbySq (Pos (S Z)) Z

|||data type which has the simplified form of a Rational number, a transversal group
data SimpQ : Type where
 SimplifiedQ : (p:ZZ) -> (q:ZZ) -> .(IsPositive q) -> .(GCDZ p q 1) -> SimpQ

--Auxillary conversions to convert Q into a SimpQ
QtoZZPair : Q -> ZZPair
QtoZZPair (PbySq p q) = (p, Pos(S q))

SimplifyToZZPair : (x:Q)-> (y: ZZPair ** (GCDZ (fst y) (snd y) 1))
SimplifyToZZPair (PbySq p q)= simplifyWithProof (QtoZZPair (PbySq p q)) (PositiveZ{k=q})

ZZPairtoQ : ZZPair -> Q
ZZPairtoQ (p, Pos(S q)) = PbySq p q

--auxillary functions for conversion of data types

blah: {b:ZZ}-> {d:ZZ}-> (IsPositive b) -> (IsPositive d) -> (x: IsDivisibleZ b d) -> (IsPositive (fst x))
blah Positive Positive ((Pos Z) ** pf) =  void (posIsNotPosTimesZero pf)
blah Positive Positive ((NegS l)** pf) = void(PosTimesNegIsNotPos pf)
blah Positive Positive ((Pos (S l))**pf) = Positive

dDivsb: (GCDZ a b d) -> (IsDivisibleZ b d)
dDivsb dgcdab = (snd (fst (snd dgcdab)))
-- aux end

ZZtoSimpQ : (p:ZZ) ->(q:ZZ) -> (pf: IsPositive q) -> (d : ZZ ** GCDZ p q d) -> SimpQ
ZZtoSimpQ p q pf (d**dgcdab) = SimplifiedQ (aByd dgcdab) (fst (dDivsb dgcdab)) (blah pf (fst dgcdab) (dDivsb dgcdab)) (divideByGcdThenGcdOne dgcdab)

|||Simplifies a rational number to its coprime form
QtoSimpQ : Q -> SimpQ
QtoSimpQ (PbySq p q) = ZZtoSimpQ p (Pos(S q)) Positive (gcdZZ p (Pos (S q)) RightPositive)

|||addition over rational number
addQ: Q -> Q -> Q
addQ (PbySq p1 q1) (PbySq p2 q2) =
  let
    num : ZZ = (p1 * (Pos(S q2))) + (p2 * (Pos (S q1)))
    denom: Nat = q1 * q2 + q1 + q2
  in
  PbySq num denom

|||addition over the transversal group
addSimpQ : SimpQ -> SimpQ -> SimpQ
addSimpQ (SimplifiedQ p1 (Pos(S q1)) Positive gcd1) (SimplifiedQ p2 (Pos(S q2)) Positive gcd2) =
                                          QtoSimpQ (addQ (PbySq p1 q1) (PbySq p2 q2))

||| multiplication over Rationals
multQ: Q-> Q -> Q
multQ (PbySq p1 q1) (PbySq p2 q2) = PbySq (p1 * p2) (q1 * q2 + q1 + q2)

|||Multiplication over the transversal group
multSimpQ : SimpQ -> SimpQ -> SimpQ
multSimpQ (SimplifiedQ p1 (Pos(S q1)) Positive gcd1) (SimplifiedQ p2 (Pos(S q2)) Positive gcd2) =
                                          QtoSimpQ (multQ (PbySq p1 q1) (PbySq p2 q2))

--Conversions from integers to aforementioned types
ZZtoQ : ZZ  -> Q
ZZtoQ x = PbySq x Z

IntegertoQ : Integer -> Q
IntegertoQ x = ZZtoQ(fromInt x)

IntegertoSimpQ : Integer -> SimpQ
IntegertoSimpQ x = QtoSimpQ (IntegertoQ x)

--defining the + and * signs for Q and SimpQ
implementation Num Q where
  (+) = addQ
  (*) = multQ
  fromInteger = IntegertoQ

implementation Num SimpQ where
  (+) = addSimpQ
  (*) = multSimpQ
  fromInteger = IntegertoSimpQ

|||Proves that addition over Q is commutative
addQIsComm : (x:Q)->(y: Q)-> (x+y=y+x)
addQIsComm (PbySq p1 q1) (PbySq p2 q2) =
  rewrite plusCommutativeZ (p1 * (Pos(S q2))) (p2 * (Pos (S q1))) in
  rewrite multCommutative q1 q2 in
  rewrite plusCommutative (q2*q1 + q1) q2 in
  rewrite plusAssociative q2 (q2 * q1) q1 in
  rewrite plusCommutative q2 (q2 * q1) in
  Refl
--auxillary function
apYX : (x: Type)->(y: Type) -> (f: y -> x) -> (n: y) -> (m: y) -> n = m -> f n = f m
apYX x y f m m Refl = Refl

{-
addSimpQisComm : (x: SimpQ) -> (y: SimpQ) ->(x+y = y+x)
addSimpQisComm (SimplifiedQ p1 (Pos(S q1)) Positive gcd1) (SimplifiedQ p2 (Pos(S q2)) Positive gcd2) =
  let
  sum :Q = ( (PbySq p1 q1)+(PbySq p2 q2))
  in
  rewrite addQIsComm (PbySq p1 q1) (PbySq p2 q2) in
  Refl
-}

|||proves that multiplication over Q is commutative
multQisComm : (x:Q)-> (y: Q) -> (x*y = y*x)
multQisComm (PbySq p1 q1) (PbySq p2 q2) =
  rewrite multCommutativeZ p1 p2 in
  rewrite multCommutative q1 q2 in
  rewrite plusCommutative (q2*q1 + q1) q2 in
  rewrite plusAssociative q2 (q2 * q1) q1 in
  rewrite plusCommutative q2 (q2 * q1) in
  Refl

|||Functions to give the IsIdentity type for Q over *
leftMultId : (r : Q) -> (OneQ * r = r)
leftMultId (PbySq p q) = rewrite multOneLeftNeutralZ p in Refl

RightMultId : (r: Q)-> (r * OneQ = r)
RightMultId r = trans (multQisComm r OneQ) (leftMultId r)

OneIsQMultId : (a: Q) -> (a*OneQ =a, OneQ * a = a)
OneIsQMultId a = (RightMultId a, leftMultId a)

|||functions to give the IsIdentity type for Q over +
leftAddId : (r : Q) ->  (ZQ + r = r)
leftAddId (PbySq p q) =
  rewrite multOneRightNeutralZ p in
  rewrite plusZeroLeftNeutralZ p in
  Refl

rightAddId : (r: Q) -> (r + ZQ = r)
rightAddId r = trans (addQIsComm r ZQ) (leftAddId r)

ZIsQAddId : (a:Q)->((a+ZQ)=a, (ZQ+a)=a)
ZIsQAddId a = (rightAddId a, leftAddId a)

|||Auxillary functions
multZero : (n: Nat) -> mult n Z = Z
multZero Z = Refl
multZero (S k) = multZero k

Aux1 : (n: Nat) -> (q : Nat) -> Nat -> Q
Aux1 n q m = PbySq (Pos (plus m n)) q

Aux2: (n: Nat) -> (q: Nat) -> Nat -> Q
Aux2 n q m = PbySq (plusZ (plusZ (Pos 0) (negNat m)) (NegS n)) q
{-
||| The IdentityExists type for Q over +
QAddIdExists : Type
QAddIdExists = (ZQ ** (ZIsQAddId))
-}


text:
plusidex1 : (n, m : Nat) -> (n = m) -> n + n = m + m
plusidex1 n m prf = rewrite prf in Refl

-- Exercise 8.1
plusidex2 : (n, m, o : Nat) -> (n = m) -> (m = o) -> n + m = m + o
plusidex2 n m o prf prf1 = rewrite prf in (rewrite prf1 in Refl)

-- Exercise 8.2
multS1 : (n, m : Nat) -> (m = S n) -> m * (1 + n) = m * m
multS1 n m prf = rewrite prf in Refl

-- Random practice proof
mu : (n, m : Nat) -> (m = 50) -> (n = m + 50) -> 200 = n + n
mu n m prf prf1 = rewrite prf1 in rewrite prf in Refl


text:
module Futures

import Data.List
import Data.So
import System
import System.Future
import System.Info

constant : IO ()
constant = do
  let a = await $ fork "String"
  putStrLn a

-- Issue in MacOS brew chez related to clock ( https://github.com/Homebrew/homebrew-core/pull/10159 )
-- Windows seems to be really flaky with usleep
extraSleep : (us : Int) -> So (us >= 0) => IO ()
extraSleep us =
  if (os == "darwin" || isWindows)
    then sleep (us `div` 10000)
    else usleep us

partial
futureHelloWorld : (Int, String) -> IO (Future Unit)
futureHelloWorld (us, n) with (choose (us >= 0))
  futureHelloWorld (us, n) | Left p = forkIO $ do
    extraSleep us
    putStrLn $ "Hello " ++ n ++ "!"

partial
simpleIO : IO (List Unit)
simpleIO = do
  futures <- sequence $ futureHelloWorld <$> [(30000, "World"), (10000, "Bar"), (0, "Foo"), (20000, "Idris")]
  let awaited = await <$> futures
  pure awaited

nonbind : IO (Future ())
nonbind = forkIO $ putStrLn "This shouldn't print"

erasureAndNonbindTest : IO ()
erasureAndNonbindTest = do
  _ <- forkIO $ do
    putStrLn "This line is printed"
  notUsed <- forkIO $ do
    extraSleep 10000
    putStrLn "This line is also printed"
  let _ = nonbind
  let n = nonbind
  extraSleep 20000 -- Even if not explicitly awaited, we should let threads finish before exiting

map : IO ()
map = do
  future1 <- forkIO $ do
    extraSleep 10000
    putStrLn "#2"
  let future3 = map (const "#3") future1
  future2 <- forkIO $ do
    putStrLn "#1"
  pure $ await future2
  putStrLn (await future3)


text:
module System.Bindings.LibUSB.Devices

import System.Bindings.LibUSB

data Device = MkDevice Ptr
data DeviceHandle = MkDeviceHandle Ptr
data DeviceList = MkDeviceList Ptr

data Speed = Unknown | Low | Full | High | Super

%lib C "usb-1.0"
%include C "libusb-1.0/libusb.h"

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

libusb_get_device_list : Context -> IO (Maybe DeviceList)
libusb_get_device_list (MkContext p) = do
  r <- mkForeign (FFun "idris_libusb_get_device_list" [FPtr] FPtr) p
  is_null <- nullPtr r
  return $ if is_null then Nothing else Just (MkDeviceList r)

libusb_get_device_list_length : DeviceList -> IO Int
libusb_get_device_list_length (MkDeviceList l) =
  mkForeign (FFun "idris_libusb_get_device_list_length" [FPtr] FInt) l

libusb_get_device_from_list : DeviceList -> Int -> IO (Maybe Device)
libusb_get_device_from_list (MkDeviceList l) i = do
  r <- mkForeign (FFun "idris_libusb_get_device_from_list" [FPtr, FInt] FPtr) l i
  is_null <- nullPtr r
  return $ if is_null then Nothing else Just (MkDevice r)

-- I should really learn that monad stuff properly
libusb_get_device_list' : Context -> IO (List Device)
libusb_get_device_list' ctx = do
  dl <- libusb_get_device_list ctx
  case dl of
       Nothing => return []
       (Just ds) => do
         len <- libusb_get_device_list_length ds
         d <- traverse (\i => libusb_get_device_from_list ds i) [0..len-1]
         return $ catMaybes d

libusb_free_device_list : DeviceList -> Int -> IO ()
libusb_free_device_list (MkDeviceList l) u =
  mkForeign (FFun "idris_libusb_free_device_list" [FPtr, FInt] FUnit) l u

libusb_get_bus_number : Device -> IO Bits8
libusb_get_bus_number (MkDevice d) =
  mkForeign (FFun "libusb_get_bus_number" [FPtr] FBits8) d

libusb_get_device_address : Device -> IO Bits8
libusb_get_device_address (MkDevice d) =
  mkForeign (FFun "libusb_get_device_address" [FPtr] FBits8) d

libusb_get_device_speed : Device -> IO Int
libusb_get_device_speed (MkDevice d) =
  mkForeign (FFun "libusb_get_device_speed" [FPtr] FInt) d

libusb_get_max_packet_size : Device -> IO Int
libusb_get_max_packet_size (MkDevice d) =
  mkForeign (FFun "libusb_get_max_packet_size" [FPtr] FInt) d

libusb_get_max_iso_packet_size : Device -> IO Int
libusb_get_max_iso_packet_size (MkDevice d) =
  mkForeign (FFun "libusb_get_max_iso_packet_size" [FPtr] FInt) d

libusb_ref_device : Device -> IO Device
libusb_ref_device (MkDevice d) = do
  r <- mkForeign (FFun "libusb_ref_device" [FPtr] FPtr) d
  return (MkDevice r)

libusb_unref_device : Device -> IO ()
libusb_unref_device (MkDevice d) =
  mkForeign (FFun "libusb_unref_device" [FPtr] FUnit) d

libusb_open : Device -> IO (Either Int DeviceHandle)
libusb_open (MkDevice d) = do
  r <- mkForeign (FFun "idris_libusb_open" [FPtr] FPtr) d
  err <- libusb_get_errno
  return $ if err == 0
           then Right (MkDeviceHandle r)
           else Left err

libusb_open_device_with_vid_pid : Context -> Bits16 -> Bits16 -> IO (Maybe DeviceHandle)
libusb_open_device_with_vid_pid (MkContext ctx) vid pid = do
  r <- mkForeign (FFun "libusb_open_device_with_vid_pid" [FPtr, FBits16, FBits16] FPtr) ctx vid pid
  is_null <- nullPtr r
  return $ if is_null then Nothing else Just (MkDeviceHandle r)

libusb_close : DeviceHandle -> IO ()
libusb_close (MkDeviceHandle h) =
  mkForeign (FFun "libusb_close" [FPtr] FUnit) h

libusb_get_device : DeviceHandle -> IO (Maybe Device)
libusb_get_device (MkDeviceHandle h) = do
  r <- mkForeign (FFun "libusb_get_device" [FPtr] FPtr) h
  is_null <- nullPtr r
  return $ if is_null then Nothing else Just (MkDevice r)

libusb_get_configuration : DeviceHandle -> IO Int
libusb_get_configuration (MkDeviceHandle h) =
  mkForeign (FFun "idris_libusb_get_configuration" [FPtr] FInt) h

libusb_set_configuration : DeviceHandle -> Int -> IO Int
libusb_set_configuration (MkDeviceHandle h) c =
  mkForeign (FFun "libusb_set_configuration" [FPtr, FInt] FInt) h c

libusb_claim_interface : DeviceHandle -> Int -> IO Int
libusb_claim_interface (MkDeviceHandle h) i =
  mkForeign (FFun "libusb_claim_interface" [FPtr, FInt] FInt) h i

libusb_release_interface : DeviceHandle -> Int -> IO Int
libusb_release_interface (MkDeviceHandle h) i =
  mkForeign (FFun "libusb_release_interface" [FPtr, FInt] FInt) h i

libusb_set_interface_alt_setting : DeviceHandle -> Int -> Int -> IO Int
libusb_set_interface_alt_setting (MkDeviceHandle h) i s =
  mkForeign (FFun "libusb_set_interface_alt_setting" [FPtr, FInt, FInt] FInt) h i s

libusb_clear_halt : DeviceHandle -> Bits8 -> IO Int
libusb_clear_halt (MkDeviceHandle h) ep =
  mkForeign (FFun "libusb_clear_halt" [FPtr, FBits8] FInt) h ep

libusb_reset_device : DeviceHandle -> IO Int
libusb_reset_device (MkDeviceHandle h) =
  mkForeign (FFun "libusb_reset_device" [FPtr] FInt) h

libusb_kernel_driver_active : DeviceHandle -> Int -> IO Int
libusb_kernel_driver_active (MkDeviceHandle h) i =
  mkForeign (FFun "libusb_kernel_driver_active" [FPtr, FInt] FInt) h i

libusb_detach_kernel_driver : DeviceHandle -> Int -> IO Int
libusb_detach_kernel_driver (MkDeviceHandle h) i =
  mkForeign (FFun "libusb_detach_kernel_driver" [FPtr, FInt] FInt) h i

libusb_attach_kernel_driver : DeviceHandle -> Int -> IO Int
libusb_attach_kernel_driver (MkDeviceHandle h) i =
  mkForeign (FFun "libusb_attach_kernel_driver" [FPtr, FInt] FInt) h i

max_stars_repo_name: idris-hackers/usb

max_issues_repo_name: idris-hackers/usb

max_forks_repo_name: idris-hackers/usb


text:
module Markdown.Format.Html

import Extra.String
import Markdown.Data

-- TODO: This probably isn't total
-- TODO: Make this safe
htmlElementProps : String -> List (String, String) -> String -> String
htmlElementProps el props contents =
  "<" ++ el ++ (showProps props) ++ ">" ++ contents ++ "</" ++ el ++ ">"
    where
      showProps : List (String, String) -> String
      showProps ps = -- Dunno why this wouldn't type check when I split function defs
        case ps of
          [] => ""
          p :: ps =>
            let (k, v) = p
            in " " ++ k ++ "=\"" ++ v ++ "\"" ++ (showProps ps)

htmlElement : String -> String -> String
htmlElement el contents =
  htmlElementProps el [] contents

||| TODO: Escape HTML-type elements
escapeText : String -> String
escapeText =
  (replace "<" "<")
  . (replace ">" ">")

mutual
  inlineToHtml : Inline -> String
  inlineToHtml (Text text) = text
  inlineToHtml (Pre text) = htmlElement "tt" (escapeText text)
  inlineToHtml (CodeBlock text _) = htmlElement "pre" (escapeText text)
  inlineToHtml (Italics inlines) = htmlElement "em" (inlinesToHtml inlines)
  inlineToHtml (Bold inlines) = htmlElement "strong" (inlinesToHtml inlines)
  inlineToHtml (Image alt src) = htmlElementProps "img" [("src", src), ("alt", alt)] ""
  inlineToHtml (Link desc href) = htmlElementProps "a" [("href", href)] desc
  inlineToHtml (Html tag inlines) = htmlElement tag (inlinesToHtml inlines)

  inlinesToHtml : List Inline -> String
  inlinesToHtml inlines =
    join "" (map inlineToHtml inlines)

blockToHtml : Block -> String
blockToHtml (Header level inlines) = htmlElement ("h" ++ (show level)) (inlinesToHtml inlines)
blockToHtml (Paragraph inlines) = htmlElement "p" (inlinesToHtml inlines)

||| Convert a Markdown value into Html
public export
toHtml : Markdown -> String
toHtml (Doc els) =
  join "\n" (map blockToHtml els)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import System
import Data.Fin

%default total

monadMap : Monad m => (a -> b) -> m a -> m b
monadMap f ma = ma >>= pure . f

infixr 2 >=>
(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
(>=>) f g a = join $ monadMap g (f a)

infixr 2 <=<
(<=<) : Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
(<=<) = flip (>=>)

(>>) : Monad m => m a -> m b -> m b
g >> f = (>>=) g (const f)

printLength : IO ()
printLength = putStr "Input string: "
              >> getLine
              >>= (putStrLn . show . Strings.length)

printLonger : IO ()
printLonger = do putStr "First string: "
                 first <- getLine
                 putStr "Second string: "
                 second <- getLine
                 let fLen = length first
                 let sLen = length second
                 let message = case compare fLen sLen of
                                    GT => "The biggest is the first one with " ++ show fLen
                                    EQ => "They're the same bro"
                                    LT => "The biggest is the second one with " ++ show sLen
                 putStrLn message

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

readPair : IO (String, String)
readPair = [| MkPair getLine getLine |]

readNumbers : IO (Maybe (Nat, Nat))
readNumbers = do
  Just num1 <- readNat | Nothing => pure Nothing
  Just num2 <- readNat | Nothing => pure Nothing
  pure $ Just (num1, num2)

countdown : (secs : Nat) -> IO ()
countdown Z = putStrLn "Get up and stretch"
countdown (S secs) = do printLn secs
                        -- A million of microseconds, that is, one second.
                        usleep 1000000
                        countdown secs

partial
guessGame : Nat -> IO ()
guessGame n = do
  putStr "Guess: "
  Just guess <- readNat
      | Nothing => do putStrLn "Whaaaat?"
                      guessGame n
  case compare guess n of
       LT => putStrLn "Too small!!" >> guessGame n
       EQ => putStrLn "Hooray!!"
       GT => putStrLn "Too big!!" >> guessGame n

partial myReplWith : (state : a) -> (prompt : String)
             -> (a -> String -> Maybe (String, a))
             -> IO ()
myReplWith state prompt step = do
  putStr prompt
  input <- getLine
  case step state input of
      Nothing => pure ()
      Just (output, nextState) => do
        putStr output
        myReplWith nextState prompt step

partial myRepl : (prompt : String) -> (String -> String) -> IO ()
myRepl prompt f = do
  putStr prompt
  input <- getLine
  putStr (f input)
  myRepl prompt f

partial main : IO ()
main = do
  -- Let's use the time as randomness
  currentTime <- time
  guessGame (cast $ mod currentTime 100)


text:
module LightClick.IR.Channel.Normalise.LetFloat

import Data.List
import Data.Vect

import Toolkit.Data.DList
import Toolkit.Data.DVect

import LightClick.Types
import LightClick.Terms

import LightClick.IR.ModuleCentric
import LightClick.IR.ChannelCentric

import LightClick.IR.Channel.Normalise.Error

%default total

isNF : ChannelIR type -> Bool

isNF (CSeq (CSeq this thenThis) andThis) = False

isNF (CSeq (CLet _ _ _) (CLet _ _ _)) = False

isNF (CSeq (CLet _ _ _) thenThis) = False

isNF (CSeq this (CLet _ _ _)) = False

isNF (CSeq this thenThis) = isNF this && isNF thenThis
isNF (CLet this beThis inThis) = isNF beThis && isNF inThis
isNF expr = True

letFloat : ChannelIR type -> ChannelIR type
letFloat (CSeq (CSeq this thenThis) rest) =
    CSeq (letFloat this)
         (CSeq (letFloat thenThis)
               (letFloat rest))

letFloat (CSeq (CLet outerName beOuterThis inOuterThis)
                  (CLet innerName beInnerThis inInnerThis)) =
    CLet outerName (letFloat beOuterThis)
         (CLet innerName (letFloat beInnerThis)
               (CSeq (letFloat inOuterThis)
                     (letFloat inInnerThis)))

letFloat (CSeq (CLet name beThis inThis)
                  thenDoThis) =
    CLet name (letFloat beThis)
         (CSeq (letFloat inThis)
               (letFloat thenDoThis))

letFloat (CSeq this
                  (CLet name beThis inThis)) =
    CLet name (letFloat beThis)
         (CSeq (letFloat this)
               (letFloat inThis))

letFloat (CLet x y z) = CLet x (letFloat y) (letFloat z)
letFloat (CSeq x y) = CSeq (letFloat x) (letFloat y)
letFloat expr = expr

export
covering -- due to totality checker not liking recursive calls.
runLetFloat : ChannelIR type -> Normalise (ChannelIR type)
runLetFloat expr =
  if isNF expr
  then Right expr
  else runLetFloat (letFloat expr)

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Syntax

public export
data Expression
  = Numeral Integer
  | Plus Expression Expression
  | Minus Expression Expression
  | Times Expression Expression
  | Divide Expression Expression
  | Negate Expression

max_stars_repo_name: steshaw/idris-calc

max_issues_repo_name: steshaw/idris-calc

max_forks_repo_name: steshaw/idris-calc


text:
module Main

import Vec3
import Ray
-- import shapes.Sphere
import Hittable

aspectRatio : Double
aspectRatio = 16.0 / 9.0

width : Int
width = 400

height : Int
height = cast (cast width / aspectRatio)

-- World
world : List (Sphere)
world = [
    MkSphere (0, 0, -1) 0.5,
    MkSphere (0, -100.5, -1) 100
]

viewport_height : Double
viewport_height = 2.0

viewport_width : Double
viewport_width = aspectRatio * viewport_height

focalLength : Double
focalLength = 1.0

origin : Vec3
origin = (0.0, 0.0, 0.0)

horizontal : Vec3
horizontal = (viewport_width, 0.0, 0.0)

vertical : Vec3
vertical = (0.0, viewport_height, 0.0)

lower_left_corner : Vec3
lower_left_corner = origin - horizontal/2 - vertical/2 - (0.0, 0.0, focalLength)

rayColor : Ray -> HittableList -> Vec3
rayColor ray world =
        let hit' = hit world ray 0.0 99999
        in
            if isHitted hit'
                then
                    0.5 * (normal hit' + (1, 1, 1))
                else
                    (1.0 - t) * (1.0, 1.0, 1.0) + t * (0.5, 0.7, 1.0)
                    where
                        direction : Vec3
                        direction = unitVector (dir ray)
                        t         = 0.5 * (getY direction + 1.0)

pixelColor : Int -> Int -> Vec3
pixelColor h w =
    rayColor (MkRay origin (lower_left_corner + (cast h / (cast width-1)) * horizontal + (cast w / (cast height-1)) * vertical - origin)) Main.world

writeColor : Vec3 -> Vec3
writeColor v = 255.999 * v

-- //TODO: seg fault !!!
createImg : Int -> Int -> List (Vec3)
createImg w h = [writeColor $ pixelColor j i | i <- [(h - 1)..0], j <- [1..w]]

main : IO ()
main = do putStrLn $ concat ["P3\n", show width, " ", show height, "\n255\n"]
          traverse putStrLn (map vecToStr $ createImg width height)
          pure ()

max_stars_repo_name: MarkMarkyMarkus/YART

max_issues_repo_name: MarkMarkyMarkus/YART

max_forks_repo_name: MarkMarkyMarkus/YART


text:
import System.Info

main : IO ()
main = do Just np <- getNProcessors
            | Nothing => putStrLn "ERROR: Couldn't get number of processors!"
          putStrLn $ (show np) ++ " processors"


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

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

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

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

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

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

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

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

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

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

|||Negative numbers are not zero
NegSThenNotZero:{a:ZZ}->(IsNegative a)->(NotZero a)
NegSThenNotZero {a = (NegS k)} ZZUtils.Negative = NegativeZ
|||negative of a negative number is positive
negateNegativePos:(IsNegative c) ->IsPositive (-c)
negateNegativePos {c = (NegS k)} Negative = Positive
|||negative of a positive number is negative
negatePosIsNeg: IsPositive q ->IsNegative (-q)
negatePosIsNeg {q = (Pos (S k))} Positive =Negative

|||If c and d are negative and c = d*q, then q is positive
negDivByNegIsPos:{c:ZZ}->{d:ZZ}->{q:ZZ}->(IsNegative c)->
      (IsNegative d)->(c=(d*q))->(IsPositive q)
negDivByNegIsPos {c = (NegS k)}{d = (NegS j)}{q = q}
    Negative Negative prf = posDivByPosIsPos {c=(-(NegS k))}{d=(-(NegS j))}
        Positive Positive (rewrite multNegateLeftZ (NegS j) q in (numbersSameNegativesSame prf))
|||If c is negative, d is positive and c = d*q, then q is negative
negDivByPosIsNeg:{c:ZZ}->{d:ZZ}->{q:ZZ}->(IsNegative c)->
      (IsPositive d)->(c=(d*q))->(IsNegative q)
negDivByPosIsNeg {c}{d}{q} cNeg dPos prf =
  (case (posDivByPosIsPos {c =(-c)} {d=d} {q=-q}
         (negateNegativePos cNeg) dPos
            (rewrite  multNegateRightZ d q in
             numbersSameNegativesSame prf)) of
               negqpos => (rewrite sym $ doubleNegElim q in
                               negatePosIsNeg negqpos))
|||Rewrites a=b as a=1*b
rewriteRightAsOneTimesRight: {a:ZZ}->{b:ZZ}->(a=b)->(a=(1*b))
rewriteRightAsOneTimesRight {a}{b}prf = rewrite ( (multOneLeftNeutralZ b)) in prf
|||Rewrites a=b as 1*a=b
rewriteLeftAsOneTimesLeft: {a:ZZ}->{b:ZZ}->(a=b)->(1*a=b)
rewriteLeftAsOneTimesLeft {a}{b}prf = rewrite ( (multOneLeftNeutralZ a)) in prf
|||Rewrites 1*a = b as a=b
rewriteOneTimesLeftAsLeft:{a:ZZ}->{b:ZZ}->((1*a) = b)->(a=b)
rewriteOneTimesLeftAsLeft {a}{b}prf  =
  rewrite ( sym $(multOneLeftNeutralZ a)) in prf
|||Rewrites   (a*1)=b as a=b
rewriteLeftTimesOneAsLeft : {a:ZZ}->{b:ZZ}->((a*1)=b)->(a=b)
rewriteLeftTimesOneAsLeft {a}{b}prf =
  rewrite ( sym $(multOneRightNeutralZ a)) in prf

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

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

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

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

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

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

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

|||Right cancellation law for addition
|||Proves that a+r=b+r implies a = b
plusRightCancelZ:(left1:ZZ)->(left2:ZZ)->(right:ZZ)->
   (left1+right=left2+right)->(left1 = left2)
plusRightCancelZ left1 left2 right prf =
  rewrite sym $plusZeroRightNeutralZ left1 in
  rewrite sym $plusZeroRightNeutralZ left2 in
  rewrite sym $plusNegateInverseRZ right in
  rewrite plusAssociativeZ left1 (-right) right in
  rewrite plusAssociativeZ left2 (-right) right in
  rewrite plusCommutativeZ left1 (-right) in
  rewrite plusCommutativeZ left2 (-right) in
  rewrite sym $ plusAssociativeZ (-right) left1 right in
  rewrite sym $ plusAssociativeZ (-right) left2 right in
  cong prf

|||Left cancellation law for addition
|||Proves that l+a=l+b implies a =b
plusLeftCancelZ:(left : ZZ) -> (right1 : ZZ) -> (right2 : ZZ) ->
   (left+right1 = left+right2) -> (right1 = right2)
plusLeftCancelZ left right1 right2 prf =
  plusRightCancelZ right1 right2 left (rewrite plusCommutativeZ right1 left in
                                       rewrite plusCommutativeZ right2 left in
                                       prf)

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

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

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

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

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

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

nonZeroNotZero: (a: ZZ) -> ( (a = (Pos Z) ) -> Void) -> (NotZero a)
nonZeroNotZero (Pos Z) f = void (f Refl)
nonZeroNotZero (Pos (S k)) f = PositiveZ
nonZeroNotZero (NegS k) f = NegativeZ

notNotZeroThenZero: ((NotZero c)->Void)->c= 0
notNotZeroThenZero {c = (Pos Z)} f = Refl
notNotZeroThenZero {c = (Pos (S k))} f = void ( f (PositiveZ))
notNotZeroThenZero {c = (NegS k)} f = void ( f (NegativeZ))

notZeroNonZero:(NotZero a)->(a=0->Void)
notZeroNonZero {a = (Pos (S _))} PositiveZ Refl impossible
notZeroNonZero {a = (NegS _)} NegativeZ Refl impossible

ZZSisNotZ: (k: Nat) -> ((Pos (S k))= (Pos Z)) -> Void
ZZSisNotZ _ Refl impossible

ZZNegisNotZ: (k: Nat) -> ((NegS k) = Pos Z) -> Void
ZZNegisNotZ _ Refl impossible

negZeroZero: (a: ZZ) -> (a = (Pos Z)) -> (negate a = (Pos Z))
negZeroZero (Pos Z) Refl = Refl
negZeroZero (Pos (S k)) prf = void ((ZZSisNotZ k) prf)
negZeroZero (NegS k) prf = void ((ZZNegisNotZ k) prf)

negNegSIsPos: (a: ZZ) -> (a = (NegS k)) -> (-a = (Pos (S k)))
negNegSIsPos (Pos k) Refl impossible
negNegSIsPos (NegS k) Refl = Refl

negPosIsNeg: (a: ZZ) -> (a = (Pos (S k))) -> (-a = (NegS k))
negPosIsNeg (Pos Z) Refl impossible
negPosIsNeg (Pos (S k)) Refl = Refl
negPosIsNeg (NegS k) Refl impossible

|||The theorem (a=(b*c)) => ((-a)=((-b)*c)))
multNegateLeftIsNegateZ:(a:ZZ)->(b:ZZ)->(c:ZZ)->(a=(b*c))->((-a)=(-b)*c)
multNegateLeftIsNegateZ a b c prf = (rewrite (multNegateLeftZ b c) in ( numbersSameNegativesSame prf))

quotproof1: {a: ZZ} -> {b: ZZ} -> {quot: ZZ} -> (a=quot*b) -> (-a = (-quot)*b)
quotproof1 {a} {b} {quot} prf = (multNegateLeftIsNegateZ a quot b prf)

quotproof2: {a: ZZ} -> {b: ZZ} -> {quot: ZZ} -> (a=quot*b) -> (a = (-quot)*(-b))
quotproof2 {a} {b} {quot} prf = trans (prf) (sym (multNegNegNeutralZ (quot) (b)))

quotproof3: {a: ZZ} -> {b: ZZ} -> {quot: ZZ} -> (a=quot*b) -> (-a = (quot)*(-b))
quotproof3 {a} {b} {quot} prf = (multNegateRightIsNegateZ a quot b prf)

QRproof1: (a:ZZ) -> (b: ZZ) -> (a = (Pos (S k))) -> (b= (Pos (S j))) -> (quot: ZZ ** a = (quot)*b) -> (nquot: ZZ ** -a=(nquot)*b)
QRproof1 (Pos Z) b Refl Refl x impossible
QRproof1 (Pos (S k)) (Pos Z) Refl Refl x impossible
QRproof1 (Pos (S k)) (Pos (S j)) Refl Refl (quot ** pf) = ((-quot) ** quotproof1(pf))
QRproof1 (Pos (S k)) (NegS j) Refl Refl x impossible
QRproof1 (NegS k) b Refl Refl x impossible

QRproof3: (a:ZZ) -> (b: ZZ) -> (a = (Pos (S k))) -> (b= (Pos (S j))) -> (quot: ZZ ** a = (quot)*b) -> (nquot: ZZ ** a=(nquot)*(-b))
QRproof3 (Pos Z) b Refl Refl x impossible
QRproof3 (Pos (S k)) (Pos Z) Refl Refl x impossible
QRproof3 (Pos (S k)) (Pos (S j)) Refl Refl (quot ** pf) = ((-quot) ** quotproof2(pf))
QRproof3 (Pos (S k)) (NegS j) Refl Refl x impossible
QRproof3 (NegS k) b Refl Refl x impossible

QRproof4: (a:ZZ) -> (b: ZZ) -> (a = (Pos (S k))) -> (b= (Pos (S j))) -> (quot: ZZ ** a = (quot)*b) -> (quot: ZZ ** (-a)=(quot)*(-b))
QRproof4 (Pos Z) b Refl Refl x impossible
QRproof4 (Pos (S k)) (Pos Z) Refl Refl x impossible
QRproof4 (Pos (S k)) (Pos (S j)) Refl Refl (quot ** pf) = (quot ** quotproof3(pf))
QRproof4 (Pos (S k)) (NegS j) Refl Refl x impossible
QRproof4 (NegS k) b Refl Refl x impossible

succIsPlusOneRight:{n:Nat}->(Pos (S n)) = (Pos n) +1
succIsPlusOneRight {n} = rewrite plusCommutativeZ (Pos n) 1 in
                       Refl
succIsPlusOneLeft :{n:Nat}->(Pos (S n)) =1+ (Pos n)
succIsPlusOneLeft = Refl

subSuccSuccNeutrtalZ: ((Pos k)=(Pos n)+(-(Pos m)))->((Pos k)=(Pos (S n))+(-(Pos (S m))))
subSuccSuccNeutrtalZ {n = n}{m = Z}{k = k} prf = rewrite sym $ plusZeroRightNeutralZ (Pos n) in prf
subSuccSuccNeutrtalZ {n = n}{m = (S j)}{k = k} prf = prf


text:
> module TestFramework
> %access export

> assertEq : Eq a => (testName : String) -> (given : a) -> (expected : a) -> IO ()
> assertEq testName g e = if g == e
>    then putStrLn (testName ++ "Passed")
>    else putStrLn (testName ++ "Failed")

> assertEqDetail : (Eq a, Show a) => (given : a) -> (expected : a) -> IO ()

max_stars_repo_name: nicklecompte/idris-finite-sets

max_issues_repo_name: nicklecompte/idris-finite-sets

max_forks_repo_name: nicklecompte/idris-finite-sets


text:
module SemVar.Sat

import Extra.Debug as Debug
import Data.List
import Data.Maybe
import Extra.Op
import Fmt
import SemVar.Data

public export
VersionNode : Type
VersionNode = (List String, Version, List (List String, Requirement))

compareBy : Ord b => (a -> b) -> (a -> a -> Ordering)
compareBy f =
  (\x, y => compare (f x) (f y))

versOf : VersionNode -> Version
versOf (_, v, _) = v

pkgVersOf : VersionNode -> (List String, Version)
pkgVersOf (p, v, _) = (p, v)

matchPkgVers : VersionNode -> VersionNode -> Bool
matchPkgVers x y =
  pkgVersOf x == pkgVersOf y

||| I think the idea is that we'll walk the list of requirements and
||| narrow down from the list of choices until either we've satisfied
||| all requirements or we've found one we can't solve.
||| Two caveats:
|||  a. We'll need to pick up new reqs as we go (for sub deps)
|||    i. Note: we can't let ourselves get into an infinite loop here and may have to track "completed"
|||  b. If we end up with multiple acceptable packages, we'll just choose the latest of all available options
satisfyAll_ : List VersionNode -> List (List String, Version) -> List (List String, Requirement) -> Either String (List (List String, Version))
satisfyAll_ versions pinned [] = Right pinned
satisfyAll_ versions pinned ((pkg, req) :: reqs) =
  -- let _ = Debug.log "Resolving req" (pkg, req, pinned) in
  case step pinned versions (pkg, req) of
    Left Nothing =>
      -- This current req is incompatible with current reqs
      Left (fmt "Package %s req %s is incompatible" (show pkg) (show req))
    Left (Just _) =>
      -- This current req is already satisfied
      -- let _ = Debug.log "Using existing package for" pkg in
      satisfyAll_ versions pinned reqs
    Right matches =>
      -- Let's see if any of these matches work
      let
        -- Try the highest versions first
        sorted = sortBy (compareBy versOf) matches
        -- This new req can't be satisfied, quit
        -- TODO: Show possible versions?
        baseErr = fmt "Cannot match %s req %s" (show pkg) (show req)
      in
        foldl tryVersion (Left baseErr) sorted
  where
    tryVersion : Either String (List (List String, Version)) -> VersionNode -> Either String (List (List String, Version))
    tryVersion (Right r) _ = Right r
    tryVersion (Left _) hd =
      case find (matchPkgVers hd) versions of
        Nothing =>
          -- TODO: Should we collect errors
          Left (fmt "Cannot find deps for %s" (show hd))

        Just (_, _, depReqs) =>
          -- Good, we found at least one potential match, let's start by just recursing on head
          -- TODO: We need to accumulate here, maybe?
          -- let _ = Debug.log " " hd in
          -- Non-TCO and non-total
          satisfyAll_ versions ((pkgVersOf hd) :: pinned) (reqs ++ depReqs)

    matchReq : List VersionNode -> (List String, Requirement) -> List VersionNode
    matchReq versions (pkg, req) =
      filter (\(name, version, _) => name == pkg && satisfy req version) versions

    step : List (List String, Version) -> List VersionNode -> (List String, Requirement) -> Either (Maybe Version) (List VersionNode)
    step pinned versions (pkg, req) =
      case find ((== pkg) . fst) pinned of
        Just (_, pin) =>
          if satisfy req pin then
            Left (Just pin)
          else
            Left Nothing
        Nothing =>
          Right $ matchReq versions (pkg, req)

export
satisfyAll : List VersionNode -> List (List String, Requirement) -> Either String (List (List String, Version))
satisfyAll versions reqs =
  satisfyAll_ versions [] reqs