text:
-- --------------------------------------------------------------- [ Graph.idr ]
-- Module    : Graph.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A Graph implementation based on Adjacency Lists.
|||
||| The underlying implementation is that of an AVL-based Dictionary
||| that associates a `(id,value)` pair to an adjacency list
||| `(id,label)`.
module Data.AVL.Graph

import Data.AVL
import Data.AVL.Set

import public Data.AVL.Dict

%access export

||| Node Identifier
public export
NodeID : Type
NodeID = Nat

||| A labelled edge between two nodes using NodeID
public export
Edge : Type -> Type
Edge b = (NodeID, NodeID, Maybe b)

||| A demi labeld Edge
public export
DemiEdge : Type -> Type
DemiEdge b = (NodeID, Maybe b)

||| Adjacency 'list' denoting adjacent nodes in the graph.
||| The list is a dict between destination `NodeID` and label.
|||
||| Note:: Should probably change this to a dict with a list of edges,
||| but that is too much work at the momemt.
public export
AList : Type -> Type
AList b = List (NodeID, Maybe b)

-- ------------------------------------------------------------------- [ Types ]
public export
GraphRep : (vTy : Type) -> (eTy : Type) -> Type
GraphRep vTy eTy = Dict NodeID (vTy, AList eTy)

||| A compact adjacency list representation of a graph.
|||
||| Implementation details:
|||
||| The Graph is actually a record that contains:
|||
||| 1. A labelling `counter`.
||| 2. An association list to contain value to identifier pairings.
||| 3. A BST-based dictionary containing the adjacency Lists.
|||
||| A BST based (AVL) Dictionary is used as the underlying data
||| structure, access to a node's adjaceny list should be `O(log
||| n)`. Constant time access to elements in the graph is not
||| guaranteed.
|||
||| The dictionary is indexed using a *Node Identifier* (`Nat`), as
||| Idris does not have support for hashes, cryptographic or
||| otherwise. Future work will be to replace the simple labelling
||| mnemoic with a hash. As such we need a secondary map to keep
||| record of what values map to what `NodeID`. To simplify matters a
||| association list is used to reduce the need for values in the
||| graph to be orderable.
|||
||| The dictionary stores a node value, successor list pairing as the
||| value.
|||
||| @vTy The type of the value associated with the vertex.
||| @eTy The type of the label used on edges.
public export
record Graph (vTy : Type) (eTy : Type) where
  constructor MkGraph
  counter : NodeID
  legend  : List (vTy, NodeID)
  graph   : GraphRep vTy eTy

public export
Legend : Type -> Type
Legend vTy = List (vTy, NodeID)

implementation (Show v, Show e) => Show (Graph v e) where
  show (MkGraph _ _ g) = show g

-- ---------------------------------------------------------- [ Legend Utility ]
private
delFromLegend : ((v,NodeID) -> Bool) -> Legend v -> Legend v
delFromLegend f Nil = Nil
delFromLegend f (x::xs) =
  if f x
    then xs
    else x::xs

private
insertLegend : Eq v => v -> NodeID -> Legend v -> Legend v
insertLegend val id l = (val, id) :: delFromLegend (\(x,_) => x == val) l

private
updateLegend : Eq v => v -> v -> Legend v -> Legend v
updateLegend old new l = map (\(x,id) => if x == old then (new,id) else (x,id)) l

-- ------------------------------------------------------------ [ Construction ]

mkEmptyGraph : Graph v e
mkEmptyGraph = MkGraph Z Nil empty

||| Add an orphan node to the graph.
|||
||| To insert a connected node use `insert` instead.
addNode : Eq v => v -> Graph v e -> Graph v e
addNode val (MkGraph c l g) = MkGraph (S c) newL newG
  where
    newG : GraphRep v e
    newG = insert c (val,Nil) g

    newL : Legend v
    newL = insertLegend val c l

||| Add many orphan nodes to the graph.
addNodes : Eq v => List v -> Graph v e -> Graph v e
addNodes vs g = foldl (flip $ addNode) g vs

getNodeIDUsing : (v -> Bool) -> Graph v e -> Maybe NodeID
getNodeIDUsing f g = doLook f (legend g)
  where
    doLook : (v -> Bool) -> List (v,NodeID) -> Maybe NodeID
    doLook _ Nil         = Nothing
    doLook f ((x,id)::xs) = if f x then Just id else doLook f xs

||| For a given value return the node id
getNodeID : Eq v => v -> Graph v e -> Maybe NodeID
getNodeID v g = List.lookup v (legend g)

||| Add a labelled edge to the Graph.
addEdge : Edge e -> Graph v e -> Graph v e
addEdge (x,y,l) g =
    case validEdge x y of
      True  => record {graph = doUpdate (x,y,l) (graph g)} g
      False => g
  where
    validEdge : NodeID -> NodeID -> Bool
    validEdge x' y' = hasKey x' (graph g) && hasKey y' (graph g)

    doUpdate : (NodeID, NodeID, Maybe e) -> GraphRep v e -> GraphRep v e
    doUpdate (x'',y'',l') gr = update x'' (\(val,as) => (val, (y'',l')::as)) gr

||| Add multiple labelled edges to the Graph.
addEdges : List (Edge e) -> Graph v e -> Graph v e
addEdges es g = foldl (flip $ addEdge) g es

||| Add Value Edge
addValueEdge : Eq v => (v, v, Maybe e) -> Graph v e -> Graph v e
addValueEdge l g =
    case newEdge l of
      Just e' => addEdge e' g
      Nothing => g
  where
    conv : v -> v -> Maybe (NodeID, NodeID)
    conv x y =
      case getNodeID x g of
        Nothing  => Nothing
        Just xID =>
          case getNodeID y g of
            Nothing  => Nothing
            Just yID => Just (xID,yID)

    newEdge : (v, v, Maybe e) -> Maybe $ (Edge e)
    newEdge (x',y',l') =
      case conv x' y' of
        Just (xID', yID') => Just (xID',yID',l')
        otherwise       => Nothing

addValueEdges : Eq v => List (v,v, Maybe e) -> Graph v e -> Graph v e
addValueEdges vs g  = foldl (flip $ addValueEdge) g vs

||| Insert a node, complete with predefined adjacency list to the graph.
insertNode : Eq v => v -> AList e -> Graph v e -> Graph v e
insertNode val es (MkGraph c l g) = MkGraph (S c) newL (insert c (val,es) g)
  where
    newL : Legend v
    newL = insertLegend val c l

-- ------------------------------------------------------------------- [ Dumps ]

||| Return the a list of node identifiers used in the graph.
verticesID : Graph v e -> List NodeID
verticesID g = map (snd) (legend g)

||| Return the list of nodes in the graph.
vertices : Graph v e -> List v
vertices g = map (fst) (legend g)

||| Return the list of edges within the graph.
edges : Graph v e -> List (Edge e)
edges g = func $ toList $ graph g
  where
    func' : NodeID -> (v, AList e) -> List (Edge e)
    func' id (_,es) = map (\(y,l) => (id,y,l)) es

    func : List (NodeID, (v,AList e)) -> List (Edge e)
    func xs = foldl (\res,(x,y) => func' x y ++ res) Nil xs

-- ----------------------------------------------------------------- [ Lookups ]

||| Using Node ID, extract the node value and adjacency list from the graph.
lookupNodeByID : NodeID -> Graph v e -> Maybe $ (v, AList e)
lookupNodeByID n g = lookup n (graph g)

||| Using the node value, extract the node value and adjaceny list from the graph.
lookupNode : Eq v => v -> Graph v e -> Maybe (v, AList e)
lookupNode val g =
  case List.lookup val (legend g) of
    Just id => lookup id (graph g)
    Nothing => Nothing

-- ----------------------------------------------------------------- [ Queries ]

||| Does the graph contain a node with a specific value.
hasValue : Eq v => v -> Graph v e -> Bool
hasValue v g = isJust $ getNodeID v g

||| Get a nodes value
getValueByID : NodeID -> Graph v e -> Maybe v
getValueByID id g =
   case lookup id (graph g) of
      Just (val,_) => Just val
      Nothing      => Nothing

||| Get Node Value
getValueUsing : (v -> Bool) -> Graph v e -> Maybe v
getValueUsing f g = doLook f (legend g)
  where
    doLook : (v -> Bool) -> List (v,NodeID) -> Maybe v
    doLook _ Nil         = Nothing
    doLook f ((x,_)::xs) = if f x then Just x else doLook f xs

||| Get a nodes successors.
getSuccsByID : NodeID -> Graph v e -> List NodeID
getSuccsByID id g =
  case lookup id (graph g) of
    Just (_,as) => map fst as
    Nothing     => Nil

||| Get a nodes successor
getSuccs : Eq v => v -> Graph v e -> List NodeID
getSuccs val g =
  case getNodeID val g of
    Nothing => Nil
    Just id => getSuccsByID id g

||| Get the adjaceny list for an node
getEdgesByID : NodeID -> Graph v e -> List (DemiEdge e)
getEdgesByID id g =
  case lookup id (graph g) of
    Nothing     => Nil
    Just (_,as) => as

||| Get the adjaceny list for an node.
getEdges : Eq v => v -> Graph v e -> List (DemiEdge e)
getEdges val g =
  case getNodeID val g of
    Just id => getEdgesByID id g
    Nothing => Nil

||| Get the full edge description
getEdgesVerboseByID : NodeID -> Graph v e -> List (Edge e)
getEdgesVerboseByID id g =
  case lookup id (graph g) of
    Nothing     => Nil
    Just (_,as) => map (\(destID,label) => (id,destID,label)) as

||| Get the full edge description
getEdgesVerbose : Eq v => v -> Graph v e -> List (Edge e)
getEdgesVerbose val g =
  case getNodeID val g of
    Just id => getEdgesVerboseByID id g
    Nothing => Nil

-- ----------------------------------------------------------------- [ Updates ]
private
updateLegendByID : NodeID -> (v -> v) -> Legend v -> Legend v
updateLegendByID x f l = map (\(oval,y) => if x == y then (f oval,y) else (oval,y)) l

updateNodeValueByIDUsing : Eq v => NodeID -> (v -> v) -> Graph v e -> Graph v e
updateNodeValueByIDUsing id f g = record {graph = newG id f, legend = newL id f} g
  where
    newG : Eq v => NodeID -> (v -> v) -> GraphRep v e
    newG i f = update i (\(o,as) => (f o, as)) (graph g)

    newL : NodeID -> (v -> v) -> Legend v
    newL i f = updateLegendByID i f (legend g)

updateNodeValueUsing : Eq v => v -> (v -> v) -> Graph v e -> Graph v e
updateNodeValueUsing oldval f g =
  case getNodeID oldval g of
    Nothing => g
    Just id => updateNodeValueByIDUsing id f g

replaceNodeValueByID : Eq v => NodeID -> v -> Graph v e -> Graph v e
replaceNodeValueByID id val g = updateNodeValueByIDUsing id (\x => val) g

replaceNodeValue : Eq v => v -> v -> Graph v e -> Graph v e
replaceNodeValue val newVal g =
  case getNodeID val g of
    Just id => replaceNodeValueByID id newVal g
    Nothing => g

-- -------------------------------------------------------------------- [ Misc ]

getValuesByID : List NodeID -> Graph v e -> List v
getValuesByID is g = catMaybes $ map (\x => getValueByID x g) is

-- foldr (\(v,id),res => if elem id is then v::res else res) List.Nil (legend g)

leafNodes : Graph v e -> List NodeID
leafNodes g = filter (\x => isNil (getSuccsByID x g)) (verticesID g)

rootNodes : Graph v e -> List NodeID
rootNodes g = Set.toList $ Set.difference parents succs
  where
    parents : Set NodeID
    parents = Set.fromList $ filter (\x => isCons (getSuccsByID x g)) (verticesID g)

    nodes : Set NodeID
    nodes = Set.fromList (verticesID g)

    succs : Set NodeID
    succs = Set.fromList $ concatMap (\x => getSuccsByID x g) (verticesID g)

disconnectedNodes : Graph v e -> List NodeID
disconnectedNodes g = Set.toList $ Set.difference (Set.fromList nodes) cNodes
  where
    nodes : List NodeID
    nodes = (verticesID g)

    yNodes : List NodeID
    yNodes = concatMap (\x => getSuccsByID x g) nodes

    xNodes : List NodeID
    xNodes = filter (\x => isCons (getSuccsByID x g)) nodes

    cNodes : Set NodeID
    cNodes = Set.fromList $ xNodes ++ yNodes

isDisconnected : Graph v e -> Bool
isDisconnected g = isCons $ (disconnectedNodes g)

-- ------------------------------------------------------------- [ Build Graph ]

||| Construct a graph using a list of nodes and a list of edges.
buildG : Eq v => List v -> List (v,v, Maybe e) -> Graph v e
buildG Nil _   = mkEmptyGraph
buildG ns  Nil = addNodes ns mkEmptyGraph
buildG ns  es  = addValueEdges es $ addNodes ns mkEmptyGraph
  where
    g : Graph v e
    g = addNodes ns mkEmptyGraph

    g' : Graph v e
    g' = addValueEdges es g

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
> module Permutation
> import Data.List
> import Data.List.DecIn

> ||| Proofs that two lists `xs` and `ys` have the same length and same elements;
> ||| i.e., that `xs` and `ys` are related by a permutation of their elements.
> Permutation : DecIn t => List t -> List t -> Type
> Permutation xs ys =
>   ((length xs = length ys),ElementPreservingCorrespondence xs ys)

ext: lidr

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 Data.Range

%access public export
%default total

||| Range is a generic data type over the `Ord` type class. It describes a value
||| between two bounds.
data Range : Ord a => a -> a -> Type where
  MkRange : Ord a => (x,y,z : a) ->
                     {auto prf : (x >= y && x <= z = True)} ->
                     Range y z

ext: idr

max_stars_repo_name: blau-io/idris-range

max_issues_repo_name: blau-io/idris-range

max_forks_repo_name: blau-io/idris-range


text:
module Main

import Python
import Python.Prim
import Python.Exceptions

-- These modules contain signatures for Python libraries.
import Python.Lib.Os
import Python.Lib.Requests
import Python.Lib.BeautifulSoup
import Python.Lib.Queue
import Python.Lib.Threading

%default total

-- Even though field names are strings,
-- everything is typechecked according to the signatures imported above.

partial
main : PIO ()
main = do
  reqs <- Requests.import_

  -- (/) extracts the named attribute
  -- ($) calls a function
  -- (/.) and ($.) work with pure LHS
  -- (/:) and ($:) work with monadic LHS (useful for chaining)
  --
  -- equivalent to: session = reqs.Session()
  session <- reqs /. "Session" $. []

  -- equivalent to: html = session.get("http://idris-lang.org").text
  -- Notice that chaining is not a problem.
  html <- session /. "get" $. ["http://idris-lang.org"] /: "text"

  -- import Beautiful Soup
  bs4 <- BeautifulSoup.import_

  -- construct soup from HTML
  soup <- bs4 /. "BeautifulSoup" $. [html, Parsers.HTML]

  -- get the iterator over <li> elements, given by CSS selector
  features <- soup /. "select" $. ["div.entry-content li"]

  -- print all <li> elements as features
  putStrLn' $ "Idris has got the following exciting features:"
  count <- iterate features 0 $ \i : Int, li : Obj Element => do
    -- collect : Iterator a -> PIO (List a)
    line <- concat <$> collect (li /. "strings")
    putStrLn' $ show (i+1) ++ ". " ++ line
    pure $ i + 1

  putStrLn' $ "Total number of features: " ++ show count
  putStrLn' ""

  -- ###  Concurrency  ###

  let thread : (String -> PIO Nat) = \name => do
    putStrLn' $ "thread " ++ name ++ " starting"
    html <- session /. "get" $. ["http://idris-lang.org"] /: "text"
    putStrLn' $ "thread " ++ name ++ " done"
    pure $ length html

  thrA <- forkPIO $ thread "A"
  thrB <- forkPIO $ thread "B"
  resA <- wait thrA
  resB <- wait thrB

  putStrLn' $ "thread A says " ++ show resA
  putStrLn' $ "thread B says " ++ show resB
  putStrLn' ""

  -- ###  Exceptions  ###

  os <- Os.import_
  putStrLn' "And now, let's fail!"

  -- the standard try-catch variant
  try (do
    os /. "mkdir" $. ["/root/hello"]
    putStrLn' $ "Something's wrong, your root's homedir is writable!"
  ) `catch` (\etype, e => case etype of
    OSError => putStrLn' $ "  -> (1) everything's fine: " ++ showException e
    _       => raise e
  )

  -- Idris sugar, originally used in Effects
  OK ret <- try $ os /. "mkdir" $. ["/root/hello"]
    | Except OSError e => putStrLn' ("  -> (2) everything's fine: " ++ showException e)
    | Except _       e => raise e
  putStrLn' $ "Your root could probably use some security lessons!"

exports : FFI_Export FFI_Py "example.py" []
exports =
    Fun greet "greet" $
    End
  where
    greet : String -> PIO ()
    greet name = putStrLn' $ "Hello " ++ name ++ "!"

max_stars_repo_name: ziman/idris-py

max_issues_repo_name: ziman/idris-py

max_forks_repo_name: ziman/idris-py


text:
||| There are different flavours of induction-recursion. This is the one
||| introduced in Dybjer and Setzer's paper:
||| Indexed induction-recursion

module Data.InductionRecursion.DybjerSetzer

public export
data Code : (input : sort -> Type) -> (output : Type) -> Type where
  Yield  : output -> Code input output
  Store  : (payload : Type) -> (payload -> Code input output) -> Code input output
  Branch : (label : Type) -> (toSort : label -> sort) ->
           (((l : label) -> input (toSort l)) -> Code input output) ->
           Code input output

public export
DecodeType
  : Code input output -> (x : sort -> Type) ->
    (f : {s : sort} -> x s -> input s) ->
    Type
DecodeType (Yield _) x f = ()
DecodeType (Store payload k) x f = (v : payload ** DecodeType (k v) x f)
DecodeType (Branch label toSort k) x f
  = (r : ((l : label) -> x (toSort l)) ** DecodeType (k (\ l => f (r l))) x f)

public export
DecodeOutput
  : (c : Code input output) -> (x : Lazy (sort -> Type)) ->
    (f : {s : sort} -> x s -> input s) ->
    DecodeType c x f -> output
DecodeOutput (Yield o) x f _ = o
DecodeOutput (Store p k) x f (v ** d) = DecodeOutput (k v) x f d
DecodeOutput (Branch l s k) x f (r ** d) = DecodeOutput (k (\ l => f (r l))) x f d

mutual

  public export
  data Mu : (f : (s : sort) -> Code input (input s)) -> (s : sort) -> Type where
    MkMu : {f : (s : sort) -> Code input (input s)} -> {s : sort} ->
           DecodeType (f s) (Mu f) Decode -> Mu {input} f s

  public export
  Decode : {f : (s : sort) -> Code input (input s)} ->
           {s : sort} -> Mu {input} f s -> input s
  Decode (MkMu d) = DecodeOutput (f s) (Mu f) (\ d => assert_total (Decode d)) d

public export
bind : Code i o -> (o -> Code i o') -> Code i o'
bind (Yield v) f = f v
bind (Store p k) f = Store p (\ v => bind (k v) f)
bind (Branch l s k) f = Branch l s (\ r => bind (k r) f)

public export
Functor (Code i) where
  map f v = bind v (Yield . f)

public export
Applicative (Code i) where
  pure = Yield
  cf <*> co = bind cf (\ f => map (f $) co)

public export
Monad (Code i) where
  (>>=) = bind


text:
-- ------------------------------------------------------------ [ Readfile.idr ]
-- Module      : UML.Utils.Readfile
-- Description : Read file into memory
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module UML.Utils.Reading

import Effects
import Effect.Exception
import Effect.File

%access private

||| Do the consuming.
consumeFile : { [FILE_IO (OpenFile Read)] } Eff String
consumeFile = readAcc ""
  where
    readAcc : String -> { [FILE_IO (OpenFile Read)] } Eff String
    readAcc acc = if (not !eof)
                     then readAcc (acc ++ !readLine)
                     else pure acc

||| Read file...
public
readFile : (fname : String) -> {[EXCEPTION String, FILE_IO ()]} Eff String
readFile fname = do
    case !(open fname Read) of
      True => do
        src <- consumeFile
        close
        pure src
      False => raise "Unable to read file"
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module ReflNotRefl1

import Data.Fin
import Data.Vect

import public Decidable.Decidable
import public Decidable.Equality

public export
data X : Nat -> Type where
  B : (0 n : Nat) -> X n
  W : X n -> (Fin n, Bool) -> X n

public export
ind : Fin n -> X n -> Bool
ind _ (B _) = False
ind i (W x (j, y)) = if isYes $ decEq i j then y else ind i x

prop : ind 3 (B 4 `W` (3, True)) = True
prop = Refl

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
> module NonNegDouble.Operations

> import Data.So

> import Double.Predicates
> import Double.Postulates
> import Double.Properties
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Predicates
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import Pairs.Operations

> %default total
> %access public export

> ||| Addition of positive double precision floating point numbers
> plus : NonNegDouble -> NonNegDouble -> NonNegDouble
> plus (Element x nnx) (Element y nny) = Element (x + y) (plusPreservesNonNegativity nnx nny)

> ||| Subtraction of positive double precision floating point numbers
> minus : (x : NonNegDouble) -> (y : NonNegDouble) -> {auto prf : y `LTE` x} -> NonNegDouble
> minus (Element x nnx) (Element y nny) {prf} = Element (x - y) (minusPreservesNonNegativity nnx nny prf)

> (-) : (x : NonNegDouble) -> (y : NonNegDouble) -> {auto prf : y `LTE` x} -> NonNegDouble
> (-) = minus

> ||| Multiplication of positive double precision floating point numbers
> mult : NonNegDouble -> NonNegDouble -> NonNegDouble
> mult (Element x nnx) (Element y nny) = Element (x * y) (multPreservesNonNegativity nnx nny)

> ||| Division of positive double precision floating point numbers
> div : NonNegDouble -> NonNegDouble -> NonNegDouble
> div (Element x nnx) (Element y nny) = Element (x / y) (divPreservesNonNegativity nnx nny)

> |||
> fromNat : (n : Nat) -> NonNegDouble
> fromNat  Z    = zero
> fromNat (S m) = one `plus` (fromNat m)

> {-

> ---}

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Applicative
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Control.Lens.Prism
import Control.Lens.Types
import Control.Monad.Identity
import Data.Profunctor

%default total

||| Create a `Prism`
public export
prism : (b -> t) -> (s -> Either t a) -> Prism s t a b
prism bt seta = dimap seta (either pure (map bt)) . right'

public export
prism' : (b -> s) -> (s -> Maybe a) -> Prism s s a b
prism' bs sma = prism bs (\s => maybe (Left s) Right (sma s))

-- Note that in Haskell the naming convention is _Left however _ isn't allowed in Idris2
public export
left_ : Prism (Either a c) (Either b c) a b
left_ = prism Left $ either Right (Left . Right)

public export
right_ : Prism (Either c a) (Either c b) a b
right_ = prism Right $ either (Left . Left) Right

public export
just_ : Prism (Maybe a) (Maybe b) a b
just_ = prism Just $ maybe (Left Nothing) Right

public export
nothing_ : Prism' (Maybe a) ()
nothing_ = prism' (const Nothing) $ maybe (Just ()) (const Nothing)

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


text:
import Data.Vect

myReverse : Vect n el -> Vect n el
myReverse [] = []
myReverse (x :: xs) = reverseProof (myReverse xs ++ [x])
    where
        reverseProof : Vect (k + 1) el -> Vect (S k) el
        reverseProof {k} result = rewrite plusCommutative 1 k in result

appendNil : Vect m elem -> Vect (plus m 0) elem
appendNil {m} xs = rewrite plusZeroRightNeutral m in xs

appendXs : Vect (S (m + k)) elem -> Vect (plus m (S k)) elem
appendXs {m} {k} xs = rewrite sym (plusSuccRightSucc m k) in xs

myAppend : Vect n elem -> Vect m elem -> Vect (m + n) elem
myAppend [] ys = appendNil ys
myAppend (x :: xs) ys = appendXs (x :: myAppend xs ys)

myPlusCommutes : (n : Nat) -> (m : Nat) -> n + m = m + n
myPlusCommutes Z m = sym (plusZeroRightNeutral m)
myPlusCommutes (S k) m = rewrite myPlusCommutes k m in plusSuccRightSucc m k

reverseProofXs : Vect ((S n) + len) el -> Vect (plus n (S len)) el
reverseProofXs {n} {len} result = rewrite sym (plusSuccRightSucc n len) in result

myReverse' : Vect n el -> Vect n el
myReverse' xs = reverse' [] xs where
    reverse' : Vect n el -> Vect m el -> Vect (n + m) el
    reverse' {n} acc [] = rewrite plusZeroRightNeutral n in acc
    reverse' acc (x :: xs) = reverseProofXs (reverse' (x :: acc) xs)


text:
module Main

corecord Foo (n : Nat) where
  constructor MkFoo
  bar : String
  baz : Foo n

corecord Blargh where
  constructor MkBlargh
  num : Nat
  argh : Foo num

total
foo : Foo 7
foo = MkFoo "Foo" foo

total
blargh : Blargh
blargh = MkBlargh 7 foo

main : IO ()
main = do printLn (record { argh->bar } blargh)
          printLn (record { argh->baz->bar } blargh)
          printLn (record { argh->baz->baz->bar } blargh)

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 Simplicity

-- Simplicity, based on https://blockstream.com/simplicity.pdf

data Ty = One | Sum Ty Ty | Prod Ty Ty

interpTy : Ty -> Type
interpTy One = Unit
interpTy (Sum x y) = Either (interpTy x) (interpTy y)
interpTy (Prod x y) = ((interpTy x), (interpTy y))

data Term : Ty -> Ty -> Type where
  Iden : Term a a
  Comp : Term a b -> Term b c -> Term a c
  Unit : Term a One
  InjL : Term a b -> Term a (Sum b c)
  InjR : Term a c -> Term a (Sum b c)
  Case : Term (Prod a c) d -> Term (Prod b c) d -> Term (Prod (Sum a b) c) d
  Pair : Term a b -> Term a c -> Term a (Prod b c)
  Take : Term a c -> Term (Prod a b) c
  Drop : Term b c -> Term (Prod a b) c

eval : Term a b -> interpTy a -> interpTy b
eval Iden = \a => a
eval (Comp x y) = \a => eval y (eval x a)
eval Unit = \_ => ()
eval (InjL x) = \a => Left (eval x a)
eval (InjR x) = \a => Right (eval x a)
eval (Case x y) = \(ab, c) => case ab of
                                Left l => eval x (l, c)
                                Right r => eval y (r, c)
eval (Pair x y) = \a => ((eval x a), (eval y a))
eval (Take x) = \(a, b) => eval x a
eval (Drop x) = \(a, b) => eval x b

Bit : Ty
Bit = Sum One One

not : Term Bit Bit
not = Comp (Pair Iden Unit) (Case (InjR Unit) (InjL Unit))

not' : interpTy Bit -> interpTy Bit
not' b = eval not b

zero : interpTy Bit
zero = Left ()

one : interpTy Bit
one = Right ()

test : interpTy Bit
test = not' zero

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 4

-- check that all functions are total
%default total

--
-- Expressions
--

||| An integer arithmetic expression
data Expr = ||| A single integer
            Value Int
          | ||| Addition of an expression to an expression
            Addition Expr Expr
          | ||| Subtraction of an expression from an expression
            Subtraction Expr Expr
          | ||| Multiplication of an expression with an expression
            Multiplication Expr Expr

||| Evaluate an expression
evaluate : Expr -> Int
evaluate (Value x) = x
evaluate (Addition x y) = evaluate x + evaluate y
evaluate (Subtraction x y) = evaluate x - evaluate y
evaluate (Multiplication x y) = evaluate x * evaluate y

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Depling.PrettyPrint

import Depling
import Control.Monad.State
import Data.Vect

total
pp_pull : State (Stream String) String
pp_pull = do
	st <- get
	put $ Prelude.Stream.tail st
	pure $ head st

public export
data DPrec = DPOpen | DPApp | DPSingle
Eq DPrec where
	DPOpen == DPOpen = True
	DPApp == DPApp = True
	DPSingle == DPSingle = True
	_ == _ = True

Ord DPrec where
	compare DPOpen DPOpen = EQ
	compare DPApp DPApp = EQ
	compare DPSingle DPSingle = EQ
	compare DPOpen b = LT
	compare a DPOpen = GT
	compare a DPSingle = LT
	compare DPSingle b = GT

total
mapM : Monad m => (a -> m b) -> List a -> m (List b)
mapM f [] = pure []
mapM f (h :: t) = (::) <$> f h <*> mapM f t

total
vmapM : Monad m => (a -> m b) -> Vect n a -> m (Vect n b)
vmapM f [] = pure []
vmapM f (h :: t) = (::) <$> f h <*> vmapM f t

mutual
	total
	pp_ℙ : Vect n String -> DAST n -> DAST n -> State (Stream String) String
	pp_ℙ c ov p@(ℙ v (DConV {a} n ats rt) t f) =
		if ov == v
		then do
			names <- vmapM (const pp_pull) $ replicate a ()
			t' <- pp' DPOpen (reverse names ++ c) t
			f' <- pp_ℙ c ov f
			pure $ "ℂ" ++ n ++ "(" ++ (pack $ intercalate [',', ' '] $ map unpack $ toList names) ++ ") => " ++ t' ++ " ;; " ++ f'
		else do
			p' <- assert_total $ pp' DPOpen c p
			pure $ "_ => " ++ p'
	pp_ℙ c _ a = do
		a' <- assert_total $ pp' DPOpen c a
		pure $ "_ => " ++ a'

	total
	pp' : DPrec -> Vect n String -> DAST n -> State (Stream String) String
	pp' d c (ʌ v) = pure $ index v c
	pp' d c (λ at b) = do
		name <- pp_pull
		at' <- pp' DPOpen c at
		b <- pp' DPOpen (name :: c) b
		pure $ showParens (d > DPOpen) $ "\\(" ++ name ++ " : " ++ at' ++ ") => " ++ b
	pp' d c (λT at rt) = do
		name <- pp_pull
		at' <- pp' DPOpen c at
		rt' <- pp' DPOpen (name :: c) rt
		pure $ showParens (d > DPOpen) $ "(" ++ name ++ " : " ++ at' ++ ") -> " ++ rt'
	pp' d c (f =!= a) = do
		f' <- pp' DPApp c f
		a' <- pp' DPSingle c a
		pure $ showParens (d > DPApp) $ f' ++ " " ++ a'
	pp' d c 𝕋 = pure $ "Type"
	pp' d c (𝔽 at rt b) = do
		rName <- pp_pull
		aName' <- pp_pull
		at'' <- pp' DPOpen c at
		rt'' <- pp' DPOpen (aName' :: c) rt
		aName <- pp_pull
		at' <- pp' DPOpen c at
		b' <- pp' DPOpen (aName :: rName :: c) b
		pure $ showParens (d > DPOpen) $ "𝔽 (" ++ rName ++ " : (" ++ aName' ++ " : " ++ at'' ++ ") -> " ++ rt'' ++ ") (" ++ aName ++ " : " ++ at' ++ ") => " ++ b'
	pp' d c (𝕌 n t) = do
		t' <- pp' DPOpen c t
		pure $ showParens (d > DPOpen) $ "𝕌 " ++ n ++ " : " ++ t'
	pp' d c (ℂ (DConV n ats rt) as) = do
		as' <- assert_total $ mapM (pp' DPApp c) $ toList as
		pure $ "ℂ" ++ n ++ "(" ++ (pack $ intercalate [',', ' '] $ map unpack as') ++ ")"
	pp' d c p@(ℙ v (DConV {a} n ats rt) t f) = do
		v' <- pp' DPApp c v
		p' <- pp_ℙ c v p
		pure $ showParens (d > DPOpen) $ "case " ++ v' ++ " of " ++ p'
	pp' d c (𝔹 t) = do
		t' <- pp' DPOpen c t
		pure $ showParens (d > DPOpen) $ "𝔹 : " ++ t'

total
pp_next : String -> String
pp_next "" = "a"
pp_next p with (assert_total $ strHead p)
	| 'z' = assert_total $ strCons 'a' $ pp_next $ strTail p
	| c = assert_total $ strCons (succ c) $ strTail p

total
pp_names : Stream String
pp_names = map reverse $ iterate pp_next "a"

total
export
pp : DPrec -> Vect n String -> DAST n -> String
pp d c a = fst $ runState (pp' d c a) pp_names

total
pp_n' : DPrec -> Vect n String -> DAST (m + n) -> State (Stream String) String
pp_n' {m=Z} d c a = pp' d c a
pp_n' {m=S m} d c a = assert_total $ do
	name <- pp_pull
	pp_n' {m} d (name :: c) (replace (plusSuccRightSucc _ _) a)

total
export
pp_n : DPrec -> Vect n String -> DAST (m + n) -> String
pp_n d c a = fst $ runState (pp_n' d c a) pp_names

max_stars_repo_name: CoderPuppy/idris-depling

max_issues_repo_name: CoderPuppy/idris-depling

max_forks_repo_name: CoderPuppy/idris-depling


text:
||| Utility types and functions for automatically deriving
||| interface instances. So far, this module does not provide
||| deriving functions for existing interfaces. See
||| Doc.Generic4 for examples, how this could be done
||| using the functionality provided here.
module Language.Reflection.Derive

import Decidable.Equality
import public Language.Reflection.Syntax
import public Language.Reflection.Types

%language ElabReflection

||| Utility type for deriving interface implementations
||| automatically. See implementations of `Eq'` and `Ord'`
||| in Doc.Generic4 as examples, how this can be done.
public export
record DeriveUtil where
  constructor MkDeriveUtil

  ||| The underlying type info containing the list and names
  ||| of data constructors plus their arguments as well as
  ||| the data type's name and type arguments.
  typeInfo           : ParamTypeInfo

  ||| Fully applied data type, i.e. `var "Either" .$ var "a" .$ var "b"`
  appliedType        : TTImp

  ||| The names of type parameters
  paramNames         : List Name

  ||| Types of constructor arguments where at least one
  ||| type parameter makes an appearance. These are the
  ||| `tpe` fields of `ExplicitArg` where `hasParam`
  ||| is set to true and `isRecursive` is set
  ||| to false. See the documentation of `ExplicitArg`
  ||| when this is the case
  argTypesWithParams : List TTImp

||| Creates a deriving utility from information about
||| a (possibly) parameterized type.
export
genericUtil : ParamTypeInfo -> DeriveUtil
genericUtil ti = let pNames = map fst $ params ti
                     appTpe = appNames (name ti) pNames
                     twps   = calcArgTypesWithParams ti
                  in MkDeriveUtil ti appTpe pNames twps

||| Generates the name of an interface's implementation function
export
implName : DeriveUtil -> String -> Name
implName g interfaceName =  UN $ "impl" ++ interfaceName
                                        ++ nameStr g.typeInfo.name

||| Syntax tree and additional info about the
||| implementation function of an interface.
|||
||| With 'implementation function', we mean the following:
||| When deriving an interface implementation, the elaborator
||| creates a function returning the corresponding record value.
||| Values of this record should provide both the full type
||| and implementation of this function as `TTImp` values.
|||
||| ```idris exampel
||| public export
||| implEqEither : {0 a : _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b)
||| implEqEither = ?impl
||| ```
public export
record InterfaceImpl where
  constructor MkInterfaceImpl
  ||| The interface's name, for instance "Eq" ord "Ord".
  ||| This is used to generate the name of the
  ||| implementation function.
  interfaceName : String

  ||| Visibility of the implementation function.
  visibility    : Visibility

  ||| Visibility of the implementation function.
  options       : List FnOpt

  ||| Actual implementation of the implementation function.
  ||| This will be the right hand side of the sole pattern clause
  ||| in the function definition.
  |||
  ||| As an example, assume there is a `genEq` function used
  ||| as an implementation for `(==)` for data types with
  ||| some kind of `Generic` instance (see the tutorial on
  ||| Generics for more information about this). An implementation
  ||| for interface `Eq` could then look like this:
  |||
  ||| ```idirs example
  ||| impl = var (singleCon "Eq") .$ `(genEq) .$ `(\a,b => not (a == b))
  ||| ```
  impl          : TTImp

  ||| Full type of the implementation function, including
  ||| implicit arguments (type parameters), which have to be part
  ||| of the `TTImp`.
  |||
  ||| See also `implementationType`, a utility function to create this
  ||| kind of function types for type classes with a single parameter
  ||| of type `Type`.
  |||
  ||| Example:
  |||
  ||| ```idirs example
  ||| `({0 a: _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b))
  ||| ```
  type          : TTImp

-- pair of type and implementation
private
implDecl : DeriveUtil -> (DeriveUtil -> InterfaceImpl) ->  (Decl,Decl)
implDecl g f = let (MkInterfaceImpl iname vis opts impl type) = f g
                   function = implName g iname

                in ( interfaceHintOpts vis opts function type
                   , def function [var function .= impl] )

||| Generates a list of pairs of declarations for the
||| implementations of the interfaces specified.
|||
||| The first elements of the pairs are type declarations, while
||| the second elements are the actual implementations.
|||
||| This separation of type declaration and implementation
||| allows us to first declare all types before declaring
||| the actual implementations. This is essential in the
||| implementation of `deriveMutual`.
export
deriveDecls : Name -> List (DeriveUtil -> InterfaceImpl) -> Elab $ List (Decl,Decl)
deriveDecls name fs = mkDecls <$> getParamInfo' name
  where mkDecls : ParamTypeInfo -> List (Decl,Decl)
        mkDecls pi = let g = genericUtil pi
                      in map (implDecl g) fs

||| Given a name of a data type plus a list of interfaces, tries
||| to implement these interfaces automatically using
||| elaborator reflection.
|||
||| Again, see Doc.Generic4 for a tutorial and examples how
||| to use this.
export
derive : Name -> List (DeriveUtil -> InterfaceImpl) -> Elab ()
derive name fs = do decls <- deriveDecls name fs
                    -- Declare types first. Then declare implementations.
                    declare $ map fst decls
                    declare $ map snd decls

||| Allows the derivation of mutually dependant interface
||| implementations by first defining type declarations before
||| declaring implementations.
|||
||| Note: There is no need to call this from withi a `mutual` block.
export
deriveMutual : List (Name, List (DeriveUtil -> InterfaceImpl)) -> Elab()
deriveMutual pairs = do declss <- traverse (uncurry deriveDecls) pairs
                        -- Declare types first. Then declare implementations.
                        traverse_ (declare . map fst) declss
                        traverse_ (declare . map snd) declss

||| Given a `TTImp` representing an interface, generates
||| the type of the implementation function with all type
||| parameters applied and auto implicits specified.
|||
||| Example: Given the `DeriveUtil` info of `Either`, this
||| will generate the following type for input ``(Eq)`:
|||
||| ```idris example
||| {0 a : _} -> {0 b : _} -> Eq a => Eq b => Eq (Either a b)
||| ```
|||
||| Note: This function is only to be used with single-parameter
||| type classes, whose type parameters are of type `Type`.
export
implementationType : (iface : TTImp) -> DeriveUtil -> TTImp
implementationType iface (MkDeriveUtil _ appTp names argTypesWithParams) =
  let appIface = iface .$ appTp
      autoArgs = piAllAuto appIface $ map (iface .$) argTypesWithParams
   in piAllImplicit autoArgs names

--------------------------------------------------------------------------------
--          Interface Factories
--------------------------------------------------------------------------------

||| Creates an `Eq` value from the passed implementation functions
||| for (==) and (/=).
public export %inline
mkEq' : (eq : a -> a -> Bool) -> (neq : a -> a -> Bool) -> Eq a
mkEq' = %runElab check (var $ singleCon "Eq")

||| Like `mkEq'` but generates (/=) from the passed `eq` function.
public export %inline
mkEq : (eq : a -> a -> Bool) -> Eq a
mkEq eq = mkEq' eq (\a,b => not $ eq a b)

||| Creates an `Ord` value from the passed implementation functions
||| for `compare`, `(<)`, `(>)`, `(<=)`, `(>=)`, `min`, `max`.
public export %inline
mkOrd' : Eq a
       => (compare : a -> a -> Ordering)
       -> (lt : a -> a -> Bool)
       -> (gt : a -> a -> Bool)
       -> (leq : a -> a -> Bool)
       -> (geq : a -> a -> Bool)
       -> (min : a -> a -> a)
       -> (max : a -> a -> a)
       -> Ord a
mkOrd' = %runElab check (var $ singleCon "Ord")

||| Creates an `Ord` value from the passed comparison function
||| using default implementations based on `comp` for all
||| other function.
public export
mkOrd : Eq a => (comp : a -> a -> Ordering) -> Ord a
mkOrd comp = mkOrd' comp
                    (\a,b => comp a b == LT)
                    (\a,b => comp a b == GT)
                    (\a,b => comp a b /= GT)
                    (\a,b => comp a b /= LT)
                    (\a,b => if comp a b == GT then a else b)
                    (\a,b => if comp a b == LT then a else b)

||| Creates a `Num` value from the passed functions.
public export %inline
mkNum :  (plus : a -> a -> a)
      -> (times : a -> a -> a)
      -> (fromInt : Integer -> a)
      -> Num a
mkNum = %runElab check (var $ singleCon "Num")

||| Creates a `Neg` value from the passed functions.
public export %inline
mkNeg : Num a
      => (negate : a -> a)
      -> (minus  : a -> a -> a)
      -> Neg a
mkNeg = %runElab check (var $ singleCon "Neg")

||| Creates an `Abs` value from the passed function
||| and `Num` instance.
public export
mkAbs :  Num a => (abs : a -> a) -> Abs a
mkAbs = %runElab check (var $ singleCon "Abs")

||| Creates a `Fractional` value from the passed functions
||| and `Num` instance.
public export %inline
mkFractional : Num a => (div : a -> a -> a) -> (recip : a -> a) -> Fractional a
mkFractional = %runElab check (var $ singleCon "Fractional")

||| Creates an `Integral` value from the passed functions.
mkIntegral : Num a => (div : a -> a -> a) -> (mod : a -> a -> a) -> Integral a
mkIntegral = %runElab check (var $ singleCon "Integral")

||| Creates a `Show` value from the passed functions.
public export %inline
mkShow' : (show : a -> String) -> (showPrec : Prec -> a -> String) -> Show a
mkShow' = %runElab check (var $ singleCon "Show")

||| Creates a `Show` value from the passed `show` functions.
public export %inline
mkShow : (show : a -> String) -> Show a
mkShow show = mkShow' show (\_ => show)

||| Creates a `Show` value from the passed `showPrec` functions.
public export %inline
mkShowPrec : (showPrec : Prec -> a -> String) -> Show a
mkShowPrec showPrec = mkShow' (showPrec Open) showPrec

||| Creates an `Uninhabited` value from the passed function.
public export %inline
mkUninhabited : (uninhabited : a -> Void) -> Uninhabited a
mkUninhabited = %runElab check (var $ singleCon "Uninhabited")

||| Creates a `Semigroup` value from the passed function.
public export %inline
mkSemigroup : (mappend : a -> a -> a) -> Semigroup a
mkSemigroup = %runElab check (var $ singleCon "Semigroup")

||| Creates a `Monoid` value from the passed neutral value.
public export %inline
mkMonoid : Semigroup a => (neutral : a) -> Monoid a
mkMonoid = %runElab check (var $ singleCon "Monoid")

||| Creates a `DecEq` value from the passed implementation function
||| for `decEq`
public export %inline
mkDecEq : (decEq : (x1 : a) -> (x2 : a) -> Dec (x1 = x2)) -> DecEq a
mkDecEq = %runElab check (var $ singleCon "DecEq")


text:
module Core.SchemeEval.Builtins

import Core.Context
import Core.SchemeEval.ToScheme
import Core.TT

import Data.Vect
import Libraries.Utils.Scheme

-- Integers are wrapped, so unwrap then wrap again
add : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
add (Just (Signed (P n))) x y = Apply (Var "ct-s+") [x, y, toScheme (n-1)]
add (Just (Unsigned n)) x y = Apply (Var "ct-u+") [x, y, toScheme n]
add _ x y = Apply (Var "ct+") [x, y]

sub : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
sub (Just (Signed (P n))) x y = Apply (Var "ct-s-") [x, y, toScheme (n-1)]
sub (Just (Unsigned n)) x y = Apply (Var "ct-u-") [x, y, toScheme n]
sub _ x y = Apply (Var "ct-") [x, y]

mul : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
mul (Just (Signed (P n))) x y = Apply (Var "ct-s*") [x, y, toScheme (n-1)]
mul (Just (Unsigned n)) x y = Apply (Var "ct-u*") [x, y, toScheme n]
mul _ x y = Apply (Var "ct*") [x, y]

div : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
div (Just (Signed Unlimited)) x y = Apply (Var "ct/") [x, y]
div (Just (Signed (P n))) x y = Apply (Var "ct-s/") [x, y, toScheme (n-1)]
div (Just (Unsigned n)) x y = Apply (Var "ct-u/") [x, y, toScheme n]
div _ x y = Apply (Var "ct/") [x, y]

mod : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
mod x y = Apply (Var "ct-mod") [x, y]

shl : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
shl (Just (Signed (P n))) x y = Apply (Var "ct-bits-shl-signed") [x, y, toScheme (n-1)]
shl (Just (Unsigned n)) x y = Apply (Var "ct-bits-shl") [x, y, toScheme n]
shl _ x y = Apply (Var "ct-shl") [x, y]

shr : Maybe IntKind -> SchemeObj Write -> SchemeObj Write -> SchemeObj Write
shr _ x y = Apply (Var "ct-shr") [x, y]

-- Doubles don't need wrapping, since there's only one double type
addDbl : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
addDbl x y = Apply (Var "+") [x, y]

subDbl : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
subDbl x y = Apply (Var "-") [x, y]

mulDbl : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
mulDbl x y = Apply (Var "*") [x, y]

divDbl : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
divDbl x y = Apply (Var "/") [x, y]

-- Check necessary arguments are in canonical form before applying the
-- operator, otherwise return the blocked form
-- Current assumption is that all primitives that we can evaluate at
-- compile time work on constants, if they do anything in Scheme at all.
canonical : SchemeObj Write ->
            Vect n (SchemeObj Write) -> SchemeObj Write -> SchemeObj Write
canonical blk [] body = body
canonical blk (n :: ns) body
   = If (Apply (Var "ct-isConstant") [n]) (canonical blk ns body) blk

-- Return blocked application if a partial operator is given an input
-- on which it's undefined
testPartial : SchemeObj Write -> SchemeObj Write -> SchemeObj Write
testPartial blk res
    = Let "p-0" res $
          (If (Apply (Var "ct-isConstant") [Var "p-0"])
              (Var "p-0")
              blk)

unaryOp : SchemeObj Write -> String ->
          SchemeObj Write -> SchemeObj Write
unaryOp blk op x = canonical blk [x] $ Apply (Var op) [x]

binOp : SchemeObj Write -> String ->
        SchemeObj Write -> SchemeObj Write -> SchemeObj Write
binOp blk op x y = canonical blk [x, y] $ Apply (Var op) [x, y]

ternaryOp : SchemeObj Write -> String ->
            SchemeObj Write -> SchemeObj Write -> SchemeObj Write ->
            SchemeObj Write
ternaryOp blk op x y z = canonical blk [x, y, z] $ Apply (Var op) [x, y, z]

int : SchemeObj Write -> SchemeObj Write
int obj = Vector (-100) [obj]

int8 : SchemeObj Write -> SchemeObj Write
int8 obj = Vector (-101) [obj]

int16 : SchemeObj Write -> SchemeObj Write
int16 obj = Vector (-102) [obj]

int32 : SchemeObj Write -> SchemeObj Write
int32 obj = Vector (-103) [obj]

int64 : SchemeObj Write -> SchemeObj Write
int64 obj = Vector (-104) [obj]

integer : SchemeObj Write -> SchemeObj Write
integer obj = Vector (-105) [obj]

bits8 : SchemeObj Write -> SchemeObj Write
bits8 obj = Vector (-106) [obj]

bits16 : SchemeObj Write -> SchemeObj Write
bits16 obj = Vector (-107) [obj]

bits32 : SchemeObj Write -> SchemeObj Write
bits32 obj = Vector (-108) [obj]

bits64 : SchemeObj Write -> SchemeObj Write
bits64 obj = Vector (-109) [obj]

wrap : IntKind -> SchemeObj Write -> SchemeObj Write
wrap (Signed Unlimited) = integer
wrap (Signed (P 8)) = int8
wrap (Signed (P 16)) = int16
wrap (Signed (P 32)) = int32
wrap (Signed (P 64)) = int64
wrap (Unsigned 8) = bits8
wrap (Unsigned 16) = bits16
wrap (Unsigned 32) = bits32
wrap (Unsigned 64) = bits64
wrap _ = integer

-- Result has to be wrapped in Int, which is Vector (-100)
boolOp : SchemeObj Write -> String ->
         SchemeObj Write -> SchemeObj Write -> SchemeObj Write
boolOp blk op x y
    = canonical blk [x, y] $
         int $
             Apply (Var "or")
                [Apply (Var "and") [Apply (Var op) [x, y],
                                    IntegerVal 1],
                 IntegerVal 0]

applyIntCast : IntKind -> IntKind -> SchemeObj Write -> SchemeObj Write
applyIntCast _ (Signed Unlimited) x = x
applyIntCast (Signed m) k@(Signed (P n)) x
    = if P n >= m
         then x
         else wrap k $ Apply (Var "ct-cast-signed") [x, toScheme (n - 1)]
applyIntCast (Unsigned m) k@(Signed (P n)) x
    = if n > m
         then x
         else wrap k $ Apply (Var "ct-cast-signed") [x, toScheme (n - 1)]
applyIntCast (Signed _) k@(Unsigned n) x
    = wrap k $ Apply (Var "ct-cast-unsigned") [x, toScheme n]
applyIntCast (Unsigned m) (Unsigned n) x
    = if n >= m
         then x
         else Apply (Var "ct-cast-unsigned") [x, toScheme n]

applyCast : SchemeObj Write ->
            Constant -> Constant ->
            SchemeObj Write -> SchemeObj Write
applyCast blk CharType to x
    = canonical blk [x] $
        case intKind to of
           Nothing =>
              case to of
                   StringType => Apply (Var "string") [x]
                   _ => blk
           Just (Signed Unlimited) => integer $ Apply (Var "char->integer") [x]
           Just k@(Signed (P n)) => wrap k $ Apply (Var "ct-cast-char-boundedInt") [x, toScheme (n - 1)]
           Just k@(Unsigned n) => wrap k $ Apply (Var "ct-cast-char-boundedUInt") [x, toScheme n]
applyCast blk from CharType x
    = canonical blk [x] $
        case intKind from of
           Nothing => blk
           Just k => Apply (Var "ct-cast-int-char") [x]
applyCast blk StringType to x
    = canonical blk [x] $
        case intKind to of
           Nothing => case to of
                           DoubleType => Apply (Var "ct-cast-string-double") [x]
                           _ => blk
           Just (Signed Unlimited) => integer $ Apply (Var "ct-cast-string-int") [x]
           Just k@(Signed (P n)) => wrap k $ Apply (Var "ct-cast-string-boundedInt") [x, toScheme (n - 1)]
           Just k@(Unsigned n) => wrap k $ Apply (Var "ct-cast-string-boundedUInt") [x, toScheme n]
applyCast blk from StringType x
    = canonical blk [x] $
        case intKind from of
           Nothing => case from of
                           DoubleType => Apply (Var "number->string") [x]
                           _ => blk
           Just k => Apply (Var "ct-cast-number-string") [x]
applyCast blk DoubleType to x
    = canonical blk [x] $
        case intKind to of
           Nothing => case to of
                           StringType => Apply (Var "number->string") [x]
                           _ => blk
           Just (Signed Unlimited) => integer $ Apply (Var "ct-exact-truncate") [x]
           Just k@(Signed (P n)) => wrap k $ Apply (Var "ct-exact-truncate-boundedInt") [x, toScheme (n - 1)]
           Just k@(Unsigned n) => wrap k $ Apply (Var "ct-exact-truncate-boundedUInt") [x, toScheme n]
applyCast blk from DoubleType x
    = canonical blk [x] $
        case intKind from of
           Nothing => case from of
                           StringType => Apply (Var "ct-cast-string-double") [x]
                           _ => blk
           Just k => Apply (Var "ct-int-double") [x]
applyCast blk from to x
    = canonical blk [x] $
        case (intKind from, intKind to) of
           (Just f, Just t) => applyIntCast f t x
           _ => blk

applyOp : SchemeObj Write -> -- if we don't have arguments in canonical form
          PrimFn n -> Vect n (SchemeObj Write) ->
          SchemeObj Write
applyOp blk (Add DoubleType) [x, y] = binOp blk "+" x y
applyOp blk (Sub DoubleType) [x, y] = binOp blk "-" x y
applyOp blk (Mul DoubleType) [x, y] = binOp blk "*" x y
applyOp blk (Div DoubleType) [x, y] = binOp blk "/" x y
applyOp blk (Neg DoubleType) [x] = unaryOp blk "-" x
applyOp blk (Add ty) [x, y] = canonical blk [x, y] $ add (intKind ty) x y
applyOp blk (Sub ty) [x, y] = canonical blk [x, y] $ sub (intKind ty) x y
applyOp blk (Mul ty) [x, y] = canonical blk [x, y] $ mul (intKind ty) x y
applyOp blk (Div ty) [x, y] = canonical blk [x, y] $ div (intKind ty) x y
applyOp blk (Mod ty) [x, y] = canonical blk [x, y] $ mod x y
applyOp blk (Neg ty) [x] = canonical blk [x] $ Apply (Var "ct-neg") [x]
applyOp blk (ShiftL ty) [x, y] = canonical blk [x, y] $ shl (intKind ty) x y
applyOp blk (ShiftR ty) [x, y] = canonical blk [x, y] $ shr (intKind ty) x y
applyOp blk (BAnd ty) [x, y] = binOp blk "ct-and" x y
applyOp blk (BOr ty) [x, y] = binOp blk "ct-or" x y
applyOp blk (BXOr ty) [x, y] = binOp blk "ct-xor" x y
applyOp blk (LT CharType) [x, y] = boolOp blk "char<?" x y
applyOp blk (LTE CharType) [x, y] = boolOp blk "char<=?" x y
applyOp blk (EQ CharType) [x, y] = boolOp blk "char=?" x y
applyOp blk (GTE CharType) [x, y] = boolOp blk "char>=?" x y
applyOp blk (GT CharType) [x, y] = boolOp blk "char>?" x y
applyOp blk (LT StringType) [x, y] = boolOp blk "string<?" x y
applyOp blk (LTE StringType) [x, y] = boolOp blk "string<=?" x y
applyOp blk (EQ StringType) [x, y] = boolOp blk "string=?" x y
applyOp blk (GTE StringType) [x, y] = boolOp blk "string>=?" x y
applyOp blk (GT StringType) [x, y] = boolOp blk "string>?" x y
applyOp blk (LT DoubleType) [x, y] = boolOp blk "<" x y
applyOp blk (LTE DoubleType) [x, y] = boolOp blk "<=" x y
applyOp blk (EQ DoubleType) [x, y] = boolOp blk "=" x y
applyOp blk (GTE DoubleType) [x, y] = boolOp blk ">=" x y
applyOp blk (GT DoubleType) [x, y] = boolOp blk ">" x y
applyOp blk (LT ty) [x, y] = boolOp blk "ct<" x y
applyOp blk (LTE ty) [x, y] = boolOp blk "ct<=" x y
applyOp blk (EQ ty) [x, y] = boolOp blk "ct=" x y
applyOp blk (GTE ty) [x, y] = boolOp blk "ct>=" x y
applyOp blk (GT ty) [x, y] = boolOp blk "ct>" x y
applyOp blk StrLength [x]
    = canonical blk [x] $ Vector (-100) [Apply (Var "string-length") [x]]
applyOp blk StrHead [x]
    = canonical blk [x] $ Apply (Var "string-ref")
                                [x, IntegerVal 0]
applyOp blk StrTail [x]
    = canonical blk [x] $ Apply (Var "substring")
                                [x, IntegerVal 1,
                                 Apply (Var "string-length") [x]]
applyOp blk StrIndex [x, y]
    = canonical blk [x, y] $ testPartial blk $
         Apply (Var "ct-string-ref") [x, y]
applyOp blk StrCons [x, y]
    = canonical blk [x, y] $ Apply (Var "ct-string-cons") [x, y]
applyOp blk StrAppend [x, y]
    = canonical blk [x, y] $ Apply (Var "string-append") [x, y]
applyOp blk StrReverse [x]
    = canonical blk [x] $ Apply (Var "ct-string-reverse") [x]
applyOp blk StrSubstr [x, y, z]
    = canonical blk [x, y, z] $ Apply (Var "ct-string-substr") [x]

applyOp blk DoubleExp [x] = unaryOp blk "flexp" x
applyOp blk DoubleLog [x] = unaryOp blk "fllog" x
applyOp blk DoublePow [x, y] = binOp blk "expt" x y
applyOp blk DoubleSin [x] = unaryOp blk "flsin" x
applyOp blk DoubleCos [x] = unaryOp blk "flcos" x
applyOp blk DoubleTan [x] = unaryOp blk "fltan" x
applyOp blk DoubleASin [x] = unaryOp blk "flasin" x
applyOp blk DoubleACos [x] = unaryOp blk "flacos" x
applyOp blk DoubleATan [x] = unaryOp blk "flatan" x
applyOp blk DoubleSqrt [x] = unaryOp blk "flsqrt" x
applyOp blk DoubleFloor [x] = unaryOp blk "flfloor" x
applyOp blk DoubleCeiling [x] = unaryOp blk "flceiling" x

applyOp blk (Cast from to) [x] = applyCast blk from to x
applyOp blk BelieveMe [_, _, x] = x
applyOp blk Crash [_, msg] = blk

mkArgList : Int -> (n : Nat) -> Vect n String
mkArgList i Z = []
mkArgList i (S k) = ("x-" ++ show i) :: mkArgList (i + 1) k

export
compileBuiltin : {farity : Nat} ->
                Name -> PrimFn farity -> SchemeObj Write
compileBuiltin nm fn
    = let args = mkArgList 0 farity in
          bindArgs args [] args
  where
    makeBlockedApp : Vect n String -> SchemeObj Write
    makeBlockedApp args = Vector (-2) [toScheme nm, vars args]
      where
        vars : forall n . Vect n String -> SchemeObj Write
        vars [] = Null
        vars (x :: xs) = Cons (Var x) (vars xs)

    bindArgs : Vect n String -> Vect n' String ->
               Vect farity String -> SchemeObj Write
    bindArgs [] done args = applyOp (makeBlockedApp args) fn (map Var args)
    bindArgs (x :: xs) done args
        = Vector (-9) [makeBlockedApp (reverse done),
                       Lambda [x] (bindArgs xs (x :: done) args)]


text:
module Text.CSS.ListStyleType

import Text.CSS.Render

%default total

public export
data ListStyleType : Type where
  None                : ListStyleType
  Disc                : ListStyleType
  Circle              : ListStyleType
  Square              : ListStyleType
  Decimal             : ListStyleType
  LowerAlpha          : ListStyleType
  UpperAlpha          : ListStyleType
  LowerRoman          : ListStyleType
  UpperRoman          : ListStyleType

export
Render ListStyleType where
  render None                = "none"
  render Disc                = "disc"
  render Circle              = "circle"
  render Square              = "square"
  render Decimal             = "decimal"
  render LowerAlpha          = "lower-alpha"
  render UpperAlpha          = "upper-alpha"
  render LowerRoman          = "lower-roman"
  render UpperRoman          = "upper-roman"


text:
import Aoc
import Data.List
import Data.List1
import Data.Strings
%default total

record Range where
  constructor mkRange
  low : Int
  high : Int
Show Range where
  show r = show r.low ++ "~" ++ show r.high

inRange : Range -> Int -> Bool
inRange r i = i >= r.low && i <= r.high

inRanges : List Range -> Int -> Bool
inRanges rs i = any (flip inRange i) rs

record Field where
  constructor mkField
  name : String
  ranges : List Range

Show Field where
  show f = show (f.name, f.ranges)

parseRange : String -> Maybe Range
parseRange s =
  case split (=='-') s of
    (a:::[b]) => mkRange <$> parseInteger a <*> parseInteger b
    _ => Nothing

parseField : String -> Maybe Field
parseField s =
  case split (==':') s of
    (name:::[rs]) => Just $ mkField name $ mapMaybe parseRange $ assert_total words rs
    _ => Nothing

onlyOne : List a -> Maybe a
onlyOne [x] = Just x
onlyOne _ = Nothing

whittle : Eq a => List (List a) -> List (List a)
whittle sets =
  let isolated = mapMaybe onlyOne sets
  in map (\s => if length s == 1 then s else filter (not . (`elem` isolated)) s) sets

main : IO ()
main = do
  let pcsi = parseCommaSeparatedIntegers {a=Int}
  (sfs:::[[_,smt],_::snts]) <- readParagraphs | _ => putStrLn "need 3 paragraphs"
  Just fs <- pure (traverse parseField sfs) | _ => putStrLn "fields parse error"
  Just mt <- pure (pcsi smt) | _ => putStrLn "my ticket parse error"
  Just nts <- pure (traverse pcsi snts) | _ => putStrLn "nearby tickets parse error"

  let values = concat nts
  let validAtAll = \i => any (`inRange` i) (concatMap (.ranges) fs)
  putStr "*   "; printLn $ sum $ filter (not . validAtAll) values

  let validTickets = filter (all validAtAll) nts
  let columns = transpose validTickets
  let sudoku = [[f.name | f <- fs, all (inRanges f.ranges) col] | col <- columns]
  let merryChristmas = 40 -- :) !!!!
  let solution = times merryChristmas whittle sudoku
  Just fieldOrder <- pure $ traverse onlyOne solution | _ => putStrLn "not enough progress"
  putStr "**  "; printLn $ product [v | (k,v) <- zip fieldOrder mt, "departure" `isPrefixOf` k]


text:
import System

import InfIO
import Fuel
import Arith

%default total

quiz : Stream Int -> (score : Nat) -> InfIO
quiz (num1 :: num2 :: nums) score
  = do putStrLn ("Score: " ++ show score)
       putStr (show num1 ++ " * " ++ show num2 ++ " ")
       answer <- getLine
       if (cast answer == num1 * num2)
       then do putStrLn "Correct!"
               quiz nums (score + 1)
       else do putStrLn ("Wrong, the answer is " ++ show (num1 * num2))
               quiz nums score

partial
main : IO ()
main = do
  seed <- time
  run forever (quiz (arithInputs (fromInteger seed)) 0)

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
{-

Using do notation, write a printLonger program that reads two strings and then displays the length of the longer string.

Write the same program using >>= instead of do notation.

 -}

printLonger : IO ()
printLonger = do putStr "First string: "
                 str1 <- getLine
                 putStr "Second string: "
                 str2 <- getLine
                 let len1 = length str1
                 let len2 = length str2
                 let longer = if len1 > len2
                              then str1
                              else str2
                 putStrLn (longer ++ " is longer with length " ++ show (length longer))

printLonger2 : IO ()
printLonger2 = putStr "First string: " >>= \_ =>
               getLine >>= \str1 =>
               let len1 = length str1 in
               putStr "Second string: " >>= \_ =>
               getLine >>= \str2 =>
               let len2 = length str2 in
               let longer = if len1 > len2
                            then str1
                            else str2 in
               putStrLn (longer ++ " is longer with length " ++ show (length longer))


text:
module Lib
import Types
import Data.List

public export
calculateDeltas : (Double,Double) -> (Double, Double) -> Double
calculateDeltas (t0, t1) (x, y) = t0 + t1 * x-y

avg : List Double -> Double
avg [] = 0.0
avg xs = (sum xs) / (cast (length xs))

getmult: List Double -> List Double -> List Double
getmult = zipWith (*)

public export
adjustDeltas : List Double -> List (Double,Double) -> List Double
adjustDeltas deltas examples =
  let xs = map fst examples in getmult deltas  xs

public export
newthetas : (Double, Double) -> Double -> List (Double, Double) ->  (Double, Double)
newthetas thetas alpha examples =
  let deltas = (map (calculateDeltas thetas) examples)
      adjusted = adjustDeltas deltas examples
      t0 = fst thetas
      t1 = snd thetas
      newt0 = t0 - alpha * avg deltas
      newt1 = t1 - alpha * avg adjusted
  in (newt0, newt1)

public export
linearRegression : (Double, Double) -> Double ->List (Double, Double) -> Int -> (Double, Double)
linearRegression coefficients alpha dataset iterations =
 case iterations == 0 of
      True => coefficients
      False => let thetas = newthetas coefficients alpha dataset in linearRegression thetas alpha dataset (iterations -1)

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:
||| https://idris2.readthedocs.io/en/latest/ffi/ffi.html translated to the
||| ElabReflection based Dart FFI.
module Main

import Dart.FFI.Elab

%language ElabReflection

%runElab importDart [
  package "./libsmall.dart" [

    fun "Int" "add" ["x" :: "Int", "y" :: "Int"],

    io "Int" "addWithMessage" ["s" :: "String", "x" :: "Int", "y" :: "Int"],

    io "String" "applyFn" [
      "c" :: "String",
      "i" :: "Int",
      "f" :: "String" :-> "Int" :-> "IO" :<> "String"
    ],

    class' "Point" [
      final "Int" "x",
      final "Int" "y",
      new "" [],
      new "at" ["x" :: "Int", "y" :: "Int"],
      io "void" "moveTo" ["x" :: "Int", "y" :: "Int"],
      static $ io "Point" "origin" []
    ]
  ]
]

Show Point where
  show pt = show (pt @. x, pt @. y)

pluralise : String -> Int -> String
pluralise str x =
  show x ++ " " ++
    if x == 1
      then str
      else str ++ "s"

pluraliseIO : String -> Int -> IO String
pluraliseIO str x = pure (pluralise str x)

main : IO ()
main = do
  -- Global functions
  printLn (add 70 24)
  addWithMessage "Sum" 70 24 >>= printLn
  applyFn "Biscuit" 10 pluraliseIO >>= putStrLn
  applyFn "Tree" 1 pluraliseIO >>= putStrLn

  -- Classes
  pt <- Point.at 0 1
  printLn pt
  pt @. moveTo 4 5
  printLn pt

  -- Static functions
  printLn !Point.origin

  -- Constructor with no arguments
  printLn !Point.new


text:
module Toolkit.Data.Whole

import Decidable.Equality

import Data.Nat

%default total

public export
data Whole : Type where
  W : (n : Nat) -> (prf : IsSucc n) -> Whole

public export
data IsOne : Whole -> Type where
  ItIsOne : IsOne (W (S Z) ItIsSucc)

wholeIsNotOne : Not (IsOne $ W (S (S n)) ItIsSucc)
wholeIsNotOne ItIsOne impossible

export
isOne : (w : Whole) -> Dec (IsOne w)
isOne (W n prf) with (prf)
  isOne (W (S k) prf) | ItIsSucc with (k)
    isOne (W (S k) prf) | ItIsSucc | Z = Yes ItIsOne
    isOne (W (S k) prf) | ItIsSucc | (S j) = No wholeIsNotOne

public export
data IsGreaterThanOne : Whole -> Type where
  IsGT1 : (LTE 2 (S n)) -> IsGreaterThanOne (W (S n) ItIsSucc)

wholeIsOne : Not (IsGreaterThanOne $ W (S Z) ItIsSucc)
wholeIsOne (IsGT1 (LTESucc LTEZero)) impossible
wholeIsOne (IsGT1 (LTESucc (LTESucc _))) impossible

decEqWholeNotEqual : (contra : (k = j) -> Void) -> (W (S k) ItIsSucc = W (S j) ItIsSucc) -> Void
decEqWholeNotEqual contra Refl = contra Refl

export
isGreaterThanOne : (w : Whole) -> Dec (IsGreaterThanOne w)
isGreaterThanOne (W n prf) with (prf)
  isGreaterThanOne (W (S k) prf) | ItIsSucc with (isLTE 2 (S k))
    isGreaterThanOne (W (S k) prf) | ItIsSucc | (Yes x) = Yes (IsGT1 x)
    isGreaterThanOne (W (S k) prf) | ItIsSucc | (No contra) with (k)
      isGreaterThanOne (W (S k) prf) | ItIsSucc | (No contra) | Z = No wholeIsOne
      isGreaterThanOne (W (S k) prf) | ItIsSucc | (No contra) | (S j) = Yes (IsGT1 (LTESucc (LTESucc LTEZero)))

export
DecEq Whole where
  decEq (W (S k) ItIsSucc) (W (S j) ItIsSucc) with (decEq k j)
    decEq (W (S j) ItIsSucc) (W (S j) ItIsSucc) | (Yes Refl) = Yes Refl
    decEq (W (S k) ItIsSucc) (W (S j) ItIsSucc) | (No contra) = No (decEqWholeNotEqual contra)

export
Show Whole where
  show (W n prf) = show n

export
toNat : Whole -> Nat
toNat (W n prf) = n

namespace Auto
  export
  fromNat : (x : Nat) -> {auto prf : IsSucc x} -> Whole
  fromNat x {prf} = W x prf

public export
data LT : Whole -> Whole -> Type where
  IsLT : (prf : LT min max)
       -> LT (W min prfA) (W max prfB)

isNotLT : (LTE (S n) k -> Void) -> LT (W n prf) (W k x) -> Void
isNotLT f (IsLT y) = f y

export
isLT : (a,b : Whole) -> Dec (LT a b)
isLT (W n prf) (W k x) with (isLTE (S n) k)
  isLT (W n prf) (W k x) | (Yes y) = Yes (IsLT y)
  isLT (W n prf) (W k x) | (No contra) = No (isNotLT contra)

public export
data LTE : Whole -> Whole -> Type where
  IsLTE : (prf : LTE min max)
       -> LTE (W min prfA) (W max prfB)

isLTENot : (contra : LTE n k -> Void)
        -> LTE (W n prf) (W k x) -> Void
isLTENot contra (IsLTE y) = contra y

export
isLTE : (a,b : Whole) -> Dec (LTE a b)
isLTE (W n prf) (W k x) with (isLTE n k)
  isLTE (W n prf) (W k x) | (Yes y) = Yes (IsLTE y)
  isLTE (W n prf) (W k x) | (No contra) = No (isLTENot contra)

export
Eq Whole where
  (W l prfL) == (W r prfR) = l == r

export
Ord Whole where
  compare (W l prfL) (W r prfR) = compare l r

namespace IsLteNatWhole

  public export
  data LTE : Nat -> Whole -> Type where
    IsLTE : (prf : LTE min max)
                -> LTE min (W max prfMax)

  isLTENot : (LTE n k -> Void) -> IsLteNatWhole.LTE n (W k prf) -> Void
  isLTENot f (IsLTE x) = f x

  export
  isLTE : (n : Nat) -> (w : Whole) -> Dec (LTE n w)
  isLTE n (W k prf) with (isLTE n k)
    isLTE n (W k prf) | (Yes x) = Yes (IsLTE x)
    isLTE n (W k prf) | (No contra) = No (isLTENot contra)

namespace Nat
  public export
  data IsWhole : Nat -> Type where
    YesIsWhole : IsWhole (S n)

  isZero : IsWhole 0 -> Void
  isZero YesIsWhole impossible

  export
  isWhole : (n : Nat) -> Dec (IsWhole n)
  isWhole 0 = No isZero
  isWhole (S k) = Yes YesIsWhole

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

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Data.ZZ

import Decidable.Equality
import Sign

%default total
%access public export

||| An integer is either a positive `Nat` or the negated successor of a `Nat`.
|||
||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen
||| to be positive.
|||
data ZZ = Pos Nat | NegS Nat

implementation Signed ZZ where
  sign (Pos Z) = Zero
  sign (Pos _) = Plus
  sign (NegS _) = Minus

||| Take the absolute value of a `ZZ`
absZ : ZZ -> Nat
absZ (Pos n) = n
absZ (NegS n) = S n

implementation Show ZZ where
  showPrec d (Pos n) = showPrec d n
  showPrec d (NegS n) = showParens (d >= PrefixMinus) $ "-" ++ showPrec PrefixMinus (S n)

negNat : Nat -> ZZ
negNat Z = Pos Z
negNat (S n) = NegS n

||| Construct a `ZZ` as the difference of two `Nat`s
minusNatZ : Nat -> Nat -> ZZ
minusNatZ n Z = Pos n
minusNatZ Z (S m) = NegS m
minusNatZ (S n) (S m) = minusNatZ n m

||| Add two `ZZ`s. Consider using `(+) {a=ZZ}`.
plusZ : ZZ -> ZZ -> ZZ
plusZ (Pos n) (Pos m) = Pos (n + m)
plusZ (NegS n) (NegS m) = NegS (S (n + m))
plusZ (Pos n) (NegS m) = minusNatZ n (S m)
plusZ (NegS n) (Pos m) = minusNatZ m (S n)

implementation Eq ZZ where
  (Pos n) == (Pos m) = n == m
  (NegS n) == (NegS m) = n == m
  _ == _ = False

implementation Ord ZZ where
  compare (Pos n) (Pos m) = compare n m
  compare (NegS n) (NegS m) = compare m n
  compare (Pos _) (NegS _) = GT
  compare (NegS _) (Pos _) = LT

||| Multiply two `ZZ`s. Consider using `(*) {a=ZZ}`.
multZ : ZZ -> ZZ -> ZZ
multZ (Pos n) (Pos m) = Pos $ n * m
multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
multZ (NegS n) (Pos m) = negNat $ (S n) * m
multZ (Pos n) (NegS m) = negNat $ n * (S m)

||| Convert an `Integer` to an inductive representation.
fromInt : Integer -> ZZ
fromInt n = if n < 0
            then NegS $ fromInteger ((-n) - 1)
            else Pos $ fromInteger n

implementation Cast Nat ZZ where
  cast n = Pos n

implementation Num ZZ where
  (+) = plusZ
  (*) = multZ
  fromInteger = fromInt

implementation Abs ZZ where
    abs = cast . absZ

mutual
  implementation Neg ZZ where
    negate (Pos Z)     = Pos Z
    negate (Pos (S n)) = NegS n
    negate (NegS n)    = Pos (S n)

    (-) = subZ

  ||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
  subZ : ZZ -> ZZ -> ZZ
  subZ n m = plusZ n (negate m)

implementation Cast ZZ Integer where
  cast (Pos n) = cast n
  cast (NegS n) = (-1) * (cast n + 1)

implementation Cast Integer ZZ where
  cast = fromInteger

--------------------------------------------------------------------------------
-- Properties
--------------------------------------------------------------------------------

natPlusZPlus : (n : Nat) -> (m : Nat) -> (x : Nat)
             -> n + m = x -> (Pos n) + (Pos m) = Pos x
natPlusZPlus n m x h = cong h

natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
             -> n * m = x -> (Pos n) * (Pos m) = Pos x
natMultZMult n m x h = cong h

doubleNegElim : (z : ZZ) -> negate (negate z) = z
doubleNegElim (Pos Z) = Refl
doubleNegElim (Pos (S n)) = Refl
doubleNegElim (NegS Z) = Refl
doubleNegElim (NegS (S n)) = Refl

-- Injectivity
posInjective : Pos n = Pos m -> n = m
posInjective Refl = Refl

negSInjective : NegS n = NegS m -> n = m
negSInjective Refl = Refl

posNotNeg : Pos n = NegS m -> Void
posNotNeg Refl impossible

-- Decidable equality
implementation DecEq ZZ where
  decEq (Pos n) (NegS m) = No posNotNeg
  decEq (NegS n) (Pos m) = No $ negEqSym posNotNeg
  decEq (Pos n) (Pos m) with (decEq n m)
    | Yes p = Yes $ cong p
    | No p = No $ \h => p $ posInjective h
  decEq (NegS n) (NegS m) with (decEq n m)
    | Yes p = Yes $ cong p
    | No p = No $ \h => p $ negSInjective h

-- Plus

plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right
plusZeroLeftNeutralZ (Pos n) = Refl
plusZeroLeftNeutralZ (NegS n) = Refl

plusZeroRightNeutralZ : (left : ZZ) -> left + 0 = left
plusZeroRightNeutralZ (Pos n) = cong $ plusZeroRightNeutral n
plusZeroRightNeutralZ (NegS n) = Refl

plusCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left + right = right + left)
plusCommutativeZ (Pos n) (Pos m) = cong $ plusCommutative n m
plusCommutativeZ (Pos n) (NegS m) = Refl
plusCommutativeZ (NegS n) (Pos m) = Refl
plusCommutativeZ (NegS n) (NegS m) = cong {f=NegS} $ cong {f=S} $ plusCommutative n m

minusNatZAntiCommutative : (j, k : Nat) -> negate (minusNatZ j k) = minusNatZ k j
minusNatZAntiCommutative Z Z = Refl
minusNatZAntiCommutative Z (S k) = Refl
minusNatZAntiCommutative (S j) Z = Refl
minusNatZAntiCommutative (S j) (S k) = minusNatZAntiCommutative j k

negateDistributesPlus : (a, b : ZZ) -> negate (a + b) = (negate a) + (negate b)
negateDistributesPlus (Pos Z) b = rewrite plusZeroLeftNeutralZ b in
                                  rewrite plusZeroLeftNeutralZ (negate b) in Refl
negateDistributesPlus (Pos (S k)) (Pos Z) = rewrite plusZeroRightNeutral k in Refl
negateDistributesPlus (Pos (S k)) (Pos (S j)) = rewrite plusCommutative k (S j) in
                                                rewrite plusCommutative j k in Refl
negateDistributesPlus (Pos (S k)) (NegS j) = minusNatZAntiCommutative k j
negateDistributesPlus (NegS k) (Pos Z) = rewrite plusZeroRightNeutral k in Refl
negateDistributesPlus (NegS k) (Pos (S j)) = minusNatZAntiCommutative j k
negateDistributesPlus (NegS k) (NegS j) = rewrite plusCommutative k (S j) in
                                          rewrite plusCommutative k j in Refl

lemmaMinusSucc : (k, j, i : Nat) -> plusZ (minusNatZ k (S j)) (Pos i) = plusZ (minusNatZ k (S (S j))) (Pos (S i))
lemmaMinusSucc Z j i = Refl
lemmaMinusSucc (S Z) Z i = Refl
lemmaMinusSucc (S (S k)) Z i = rewrite plusCommutative k (S i) in
                               rewrite plusCommutative i k in Refl
lemmaMinusSucc (S k) (S j) i = lemmaMinusSucc k j i

lemmaAssocNegation : (k : Nat) -> (c, r : ZZ) -> (Pos (S k)) + (c + r) = ((Pos (S k)) + c) + r -> (NegS k) + ((negate c) + (negate r)) = ((NegS k) + (negate c)) + (negate r)
lemmaAssocNegation k c r prf = rewrite sym $ negateDistributesPlus c r in
                               rewrite sym $ negateDistributesPlus (Pos (S k)) (plusZ c r) in
                               rewrite sym $ negateDistributesPlus (Pos (S k)) c in
                               rewrite sym $ negateDistributesPlus (plusZ (Pos (S k)) c) r in
                               cong $ prf

lemmaAssocPos : (k : Nat) -> (c, r : ZZ) -> (Pos k) + (c + r) = ((Pos k) + c) + r
lemmaAssocPos k (Pos j) (Pos i) = cong $ plusAssociative k j i
lemmaAssocPos k (Pos Z) (NegS i) = rewrite plusZeroRightNeutral k in Refl
lemmaAssocPos k (Pos (S j)) (NegS Z) = rewrite plusCommutative k (S j) in
                                       rewrite plusCommutative j k in Refl
lemmaAssocPos k (Pos (S j)) (NegS (S i)) = let ind = lemmaAssocPos k (assert_smaller (Pos (S j)) (Pos j)) (assert_smaller (NegS (S i)) (NegS i)) in
                                           rewrite ind in
                                           rewrite plusCommutative k (S j) in
                                           rewrite plusCommutative j k in Refl
lemmaAssocPos k (NegS j) (Pos Z) = rewrite plusZeroRightNeutralZ (minusNatZ k (S j)) in Refl
lemmaAssocPos Z (NegS Z) (Pos (S i)) = Refl
lemmaAssocPos (S k) (NegS Z) (Pos (S i)) = rewrite plusCommutative k (S i) in
                                           rewrite plusCommutative k i in Refl
lemmaAssocPos k (NegS (S j)) (Pos (S i)) = let ind = lemmaAssocPos k (assert_smaller (NegS (S j)) (NegS j)) (assert_smaller (Pos (S i)) (Pos i)) in
                                           rewrite ind in
                                           rewrite lemmaMinusSucc k j i in Refl
lemmaAssocPos Z (NegS j) (NegS i) = Refl
lemmaAssocPos (S k) (NegS Z) (NegS i) = Refl
lemmaAssocPos (S k) (NegS (S j)) (NegS i) = let ind = lemmaAssocPos (assert_smaller (S k) k) (assert_smaller (NegS (S j)) (NegS j)) (NegS i) in
                                            rewrite ind in Refl

plusAssociativeZ : (l, c, r : ZZ) -> l + (c + r) = (l + c) + r
plusAssociativeZ (Pos k) c r = lemmaAssocPos k c r
plusAssociativeZ (NegS k) c r = rewrite sym $ doubleNegElim c in
                                rewrite sym $ doubleNegElim r in
                                lemmaAssocNegation k (negate c) (negate r) (lemmaAssocPos (S k) (negate c) (negate r))

lemmaMinusSymmZero : (k : Nat) -> minusNatZ k k = Pos 0
lemmaMinusSymmZero Z = Refl
lemmaMinusSymmZero (S k) = let ind = lemmaMinusSymmZero k in
                           rewrite ind in Refl

plusNegateInverseLZ : (a : ZZ) -> a + negate a = Pos Z
plusNegateInverseLZ (Pos Z) = Refl
plusNegateInverseLZ (Pos (S k)) = rewrite lemmaMinusSymmZero k in Refl
plusNegateInverseLZ (NegS k) = rewrite lemmaMinusSymmZero k in Refl

plusNegateInverseRZ : (a : ZZ) -> negate a + a = Pos Z
plusNegateInverseRZ (Pos Z) = Refl
plusNegateInverseRZ (Pos (S k)) = rewrite lemmaMinusSymmZero k in Refl
plusNegateInverseRZ (NegS k) = rewrite lemmaMinusSymmZero k in Refl

-- Mult
multZeroLeftZeroZ : (right : ZZ) -> (Pos Z) * right = (Pos Z)
multZeroLeftZeroZ (Pos k) = Refl
multZeroLeftZeroZ (NegS k) = Refl

multZeroRightZeroZ : (left : ZZ) -> left * (Pos Z) = (Pos Z)
multZeroRightZeroZ (Pos k) = rewrite multZeroRightZero k in Refl
multZeroRightZeroZ (NegS k) = rewrite multZeroRightZero k in Refl

multOneLeftNeutralZ : (right : ZZ) -> 1 * right = right
multOneLeftNeutralZ (Pos k) = rewrite plusZeroRightNeutral k in Refl
multOneLeftNeutralZ (NegS k) = rewrite plusZeroRightNeutral k in Refl

multOneRightNeutralZ : (left : ZZ) -> left * 1 = left
multOneRightNeutralZ (Pos Z) = Refl
multOneRightNeutralZ (Pos (S k)) = cong $ multOneRightNeutral (S k)
multOneRightNeutralZ (NegS k) = cong $ multOneRightNeutral k

multCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left * right = right * left)
multCommutativeZ (Pos k) (Pos j) = cong $ multCommutative k j
multCommutativeZ (Pos k) (NegS j) = rewrite multCommutative j k in
                                    cong $ multRightSuccPlus k j
multCommutativeZ (NegS k) (Pos j) = rewrite multCommutative j (S k) in Refl
multCommutativeZ (NegS k) (NegS j) = cong $ multCommutative (S k) (S j)

lemmaPosMultNegNat : (k, j : Nat) -> multZ (Pos k) (negNat j) = negNat (mult k j)
lemmaPosMultNegNat k Z = rewrite multZeroRightZero k in Refl
lemmaPosMultNegNat k (S j) = Refl

lemmaNegMultNegNat : (k, j : Nat) -> multZ (NegS k) (negNat j) = multZ (Pos (S k)) (Pos j)
lemmaNegMultNegNat k Z = rewrite multZeroRightZero k in Refl
lemmaNegMultNegNat k (S j) = Refl

lemmaNegatePosNegNat : (k : Nat) -> negate (Pos k) = negNat k
lemmaNegatePosNegNat Z = Refl
lemmaNegatePosNegNat (S k) = Refl

multNegLeftZ : (k : Nat) -> (j : ZZ) -> (NegS k) * j = negate (Pos (S k) * j)
multNegLeftZ k (Pos j) = rewrite lemmaNegatePosNegNat ((S k) * j) in Refl
multNegLeftZ k (NegS j) = Refl

multNegateLeftZ : (k, j : ZZ) -> (negate k) * j = negate (k * j)
multNegateLeftZ (Pos Z) j = rewrite multZeroLeftZeroZ j in Refl
multNegateLeftZ (Pos (S k)) (Pos j) = rewrite lemmaNegatePosNegNat ((S k) * j) in Refl
multNegateLeftZ (Pos (S k)) (NegS j) = Refl
multNegateLeftZ (NegS k) j = rewrite sym $ doubleNegElim (multZ (Pos (S k)) j) in
                             rewrite multNegLeftZ k j in Refl

multAssociativeZPos : (k : Nat) -> (c, r : ZZ) -> (Pos k) * (c * r) = ((Pos k) * c) * r
multAssociativeZPos k (Pos j) (Pos i) = cong $ multAssociative k j i
multAssociativeZPos k (Pos j) (NegS i) = rewrite sym $ multAssociative k j (S i) in lemmaPosMultNegNat k (mult j (S i))
multAssociativeZPos k (NegS j) (Pos i) = rewrite multCommutative j i in
                                         rewrite sym $ multRightSuccPlus i j in
                                         rewrite lemmaPosMultNegNat k (mult i (S j)) in
                                         rewrite multCommutativeZ (negNat (mult k (S j))) (Pos i) in
                                         rewrite lemmaPosMultNegNat i (mult k (S j)) in
                                         rewrite multAssociative k i (S j) in
                                         rewrite multAssociative i k (S j) in
                                         rewrite multCommutative i k in Refl
multAssociativeZPos k (NegS j) (NegS i) = rewrite multCommutativeZ (negNat (mult k (S j))) (NegS i) in
                                          rewrite lemmaNegMultNegNat i (mult k (S j)) in
                                          rewrite multAssociative k (S j) (S i) in
                                          rewrite multCommutative (mult k (S j)) (S i) in Refl

multAssociativeZ : (l, c, r : ZZ) -> l * (c * r) = (l * c) * r
multAssociativeZ (Pos k) c r = multAssociativeZPos k c r
multAssociativeZ (NegS k) c r = rewrite multNegLeftZ k (c * r) in
                                rewrite multNegLeftZ k c in
                                rewrite multNegateLeftZ (multZ (Pos (S k)) c) r in
                                cong $ multAssociativeZPos (S k) c r

lemmaPlusPosNegCancel : (k, j, i : Nat) -> plusZ (Pos (plus k j)) (negNat (plus k i)) = plusZ (Pos j) (negNat i)
lemmaPlusPosNegCancel Z j i = Refl
lemmaPlusPosNegCancel (S Z) j Z = rewrite plusZeroRightNeutral j in Refl
lemmaPlusPosNegCancel (S Z) j (S i) = Refl
lemmaPlusPosNegCancel (S (S k)) j i = lemmaPlusPosNegCancel (S k) j i

lemmaPlusPosNegZero : (k : Nat) -> plusZ (Pos k) (negNat k) = Pos Z
lemmaPlusPosNegZero Z = Refl
lemmaPlusPosNegZero (S k) = rewrite lemmaMinusSymmZero k in Refl

negNatDistributesPlus : (j, k : Nat) -> plusZ (negNat j) (negNat k) = negNat (plus j k)
negNatDistributesPlus Z k = rewrite plusZeroLeftNeutralZ (negNat k) in Refl
negNatDistributesPlus (S j) Z = rewrite plusZeroRightNeutral j in Refl
negNatDistributesPlus (S j) (S k) = rewrite plusSuccRightSucc j k in Refl

-- Distributivity

multDistributesOverPlusRightPosPosZ : (l, c : Nat) -> (r : ZZ) -> (Pos l) * ((Pos c) + r) = ((Pos l) * (Pos c)) + ((Pos l) * r)
multDistributesOverPlusRightPosPosZ l c (Pos i) = rewrite multDistributesOverPlusRight l c i in Refl
multDistributesOverPlusRightPosPosZ l Z (NegS i) = rewrite multZeroRightZero l in
                                                   rewrite plusZeroLeftNeutralZ (negNat (mult l (S i))) in Refl
multDistributesOverPlusRightPosPosZ l (S c) (NegS Z) = rewrite multOneRightNeutral l in
                                                       rewrite multRightSuccPlus l c in
                                                       rewrite sym $ plusAssociativeZ (Pos l) (Pos (mult l c)) (negNat l) in
                                                       rewrite plusCommutativeZ (Pos (mult l c)) (negNat l) in
                                                       rewrite plusAssociativeZ (Pos l) (negNat l) (Pos (mult l c)) in
                                                       rewrite lemmaPlusPosNegZero l in Refl
multDistributesOverPlusRightPosPosZ l (S c) (NegS (S i)) = let ind = multDistributesOverPlusRightPosPosZ l (assert_smaller (S c) c) (assert_smaller (NegS (S i)) (NegS i)) in
                                                           rewrite ind in
                                                           rewrite multRightSuccPlus l (S i) in
                                                           rewrite multRightSuccPlus l c in
                                                           rewrite lemmaPlusPosNegCancel l (mult l c) (mult l (S i)) in Refl

multDistributesOverPlusRightPosZ : (k : Nat) -> (c, r : ZZ) -> (Pos k) * (c + r) = ((Pos k) * c) + ((Pos k) * r)
multDistributesOverPlusRightPosZ k (Pos j) r = multDistributesOverPlusRightPosPosZ k j r
multDistributesOverPlusRightPosZ k (NegS j) (Pos i) = rewrite plusCommutativeZ ((Pos k) * (NegS j)) ((Pos k) * (Pos i)) in
                                                      rewrite multDistributesOverPlusRightPosPosZ k i (NegS j) in Refl
multDistributesOverPlusRightPosZ k (NegS j) (NegS i) = rewrite negNatDistributesPlus (mult k (S j)) (mult k (S i)) in
                                                       rewrite sym $ multDistributesOverPlusRight k (S j) (S i) in
                                                       rewrite plusSuccRightSucc j i in Refl

multDistributesOverPlusRightZ : (l, c, r : ZZ) -> l * (c + r) = (l * c) + (l * r)
multDistributesOverPlusRightZ (Pos k) c r = multDistributesOverPlusRightPosZ k c r
multDistributesOverPlusRightZ (NegS k) c r = rewrite multNegLeftZ k (plusZ c r) in
                                             rewrite multNegLeftZ k c in
                                             rewrite multNegLeftZ k r in
                                             rewrite sym $ negateDistributesPlus (multZ (Pos (S k)) c) (multZ (Pos (S k)) r) in
                                             rewrite multDistributesOverPlusRightPosZ (S k) c r in Refl

multDistributesOverPlusLeftZ : (l, c, r : ZZ) -> (l + c) * r = (l * r) + (c * r)
multDistributesOverPlusLeftZ l c r = rewrite multCommutativeZ (l + c) r in
                                     rewrite multDistributesOverPlusRightZ r l c in
                                     rewrite multCommutativeZ r l in
                                     rewrite multCommutativeZ r c in Refl
plusConstantRightZ : (left : ZZ) ->
                    (right : ZZ) ->
                    (c : ZZ) -> (left = right) -> left+c = right+c
plusConstantRightZ right right c Refl = Refl

plusConstantLeftZ :(left : ZZ) ->
    (right : ZZ) -> (c : ZZ) -> (p : left = right) -> c + left = c + right
plusConstantLeftZ right right c Refl = Refl

|||A type that is occupied only when the integer is positive
data IsPositive :ZZ->Type where
  Positive : (IsPositive (Pos(S k)))
data IsNotPositive :ZZ->Type where
  Zero:(IsNotPositive (Pos 0))
  Negative :(IsNotPositive (NegS k))
|||Proof that 0 is not positive
ZeroNOtPositive : IsPositive (Pos 0) -> Void
ZeroNOtPositive Positive impossible
|||Proof that negative numbers are not positive
NegNotPositive : IsPositive (NegS k) -> Void
NegNotPositive Positive impossible
|||A function that returns either a proof that a function is positive or a contradiction
DecidePositive:(a:ZZ)->Dec (IsPositive a)
DecidePositive (Pos Z) = No ZeroNOtPositive
DecidePositive (Pos (S k)) = Yes Positive
DecidePositive (NegS k) = No (NegNotPositive)

|||A proof that a=b => (-a)=(-b)
numbersSameNegativesSame: {a:ZZ}->{b:ZZ}->((a)=(b))->((-a)=(-b))
numbersSameNegativesSame Refl = Refl
|||A proof that  (-a)=(-b) => a=b
negativesSameNumbersSame :{a:ZZ}->{b:ZZ}->((-a)=(-b))->((a)=(b))
negativesSameNumbersSame {a} {b} prf = rewrite sym (doubleNegElim a) in (rewrite sym (doubleNegElim b) in (numbersSameNegativesSame prf))
|||The theorem k*(-j) = -(k*j)
multNegateRightZ:(k, j : ZZ) -> k * (negate j) = negate (k * j)
multNegateRightZ k j = (rewrite (multCommutativeZ k (-j)) in(rewrite ((multCommutativeZ k j)) in (multNegateLeftZ j k)))

|||The theorem (a=(b*c)) => ((-a)=(b*(-c)))
multNegateRightIsNegateZ:(a:ZZ)->(b:ZZ)->(c:ZZ)->(a=(b*c))->((-a)=(b*(-c)))
multNegateRightIsNegateZ a b c prf = (rewrite (multNegateRightZ b c) in ( numbersSameNegativesSame prf))
|||The theorem that ((a+b)+(-b))=a
addAndSubNeutralZ: (a:ZZ)->(b:ZZ)->(((a+b)+(-b))=a)
addAndSubNeutralZ a b = rewrite (sym (plusAssociativeZ a b (-b))) in (rewrite (plusNegateInverseLZ b) in (rewrite (plusZeroRightNeutralZ a) in Refl))

--------------------------------------------------------------------------------------------------------------------------------------------------------------------
--Some more functions of Natural numbers that might be useful
---------------------------------------------------------------------------------------------------------------------------------------------------------------------
|||The theorem that (m<=n) and (n<=m) implies n=m
lteAndGteImpliesEqual:{m:Nat}-> {n:Nat}->(LTE m n)-> (LTE n m)->(n=m)
lteAndGteImpliesEqual LTEZero LTEZero = Refl
lteAndGteImpliesEqual (LTESucc x) (LTESucc y) = cong (lteAndGteImpliesEqual x y)
|||The theorem (m<=n) implies (m<=(c+n))
plusConstantLeftSide:{m:Nat}->{n:Nat}->(c:Nat)->LTE m n ->LTE m (c+n)
plusConstantLeftSide Z x = x
plusConstantLeftSide (S k) x = lteSuccRight (plusConstantLeftSide k x)

plusConstantLeftPreservesLte:{m:Nat}-> {n:Nat}->(c:Nat)->(LTE m n)->(LTE (c+m) (c+n))
plusConstantLeftPreservesLte Z x = x
plusConstantLeftPreservesLte (S k) x = LTESucc (plusConstantLeftPreservesLte k x)

plusConstantRightPreservesLte:{m:Nat}-> {n:Nat}->(c:Nat)->(LTE m n)->(LTE (m+c) (n+c))
plusConstantRightPreservesLte {m}{n}c x = rewrite (plusCommutative m c)  in (rewrite (plusCommutative n c) in (plusConstantLeftPreservesLte c x))

|||The theorem that for any natural numbers k and m (m<= (S k)*m)
natLteMultNatNat: (k:Nat)->(m:Nat)->(LTE m ((S k)*m))
natLteMultNatNat Z m = rewrite (multOneLeftNeutral m) in (lteRefl)
natLteMultNatNat (S k) m =     plusConstantLeftSide m (natLteMultNatNat  k m)

-----------------------------------------------------------------------------------------------------------------
--Implementation of LTE for ZZ
----------------------------------------------------------------------------------------------------------------
|||The less than or equal to type for ZZ
data LTEZ :ZZ->ZZ->Type where
  PositiveLTE: (LTE m n)->LTEZ (Pos m) (Pos n)
  NegLessPositive:LTEZ (NegS m) (Pos n)
  NegativeLte:(LTE m n)->LTEZ (NegS n) (NegS m)

|||The theorem that for positive integers n and m (n<=(m*n))
posLteMultPosPosZ:  (n:ZZ)->(m:ZZ)->(IsPositive n)->(IsPositive m)->(LTEZ n  (m*n))
posLteMultPosPosZ (Pos (S j)) (Pos (S k)) Positive Positive = PositiveLTE (natLteMultNatNat k (S j))

|||The proof that if an integer is not not positive , it is positive (This  looks useless , but I couldnt find a better way to implement some other theorems)
notNotPositiveimpliesPositive:{k:ZZ}->((IsNotPositive k)->Void)->(IsPositive k)
notNotPositiveimpliesPositive {k = (Pos Z)} f = void (f Zero)
notNotPositiveimpliesPositive {k = (Pos (S k))} f = Positive
notNotPositiveimpliesPositive {k = (NegS k)} f = void (f Negative)

|||Proof that Multiplying two Positive numbers doesnt give Zero
zeroIsNotPosMultPos: ((Pos Z) = (Pos (S k))*(Pos(S j)))->Void
zeroIsNotPosMultPos Refl impossible
|||Proof that a positive number is not 0 times a positive number
posIsNotZeroMultPos:((Pos (S j)) = (Pos (Z))*(Pos (S k) ))->Void
posIsNotZeroMultPos Refl impossible
|||Proof that a positive number is not a positive number times 0
posIsNotPosMultZero:((Pos (S j)) = (Pos (S k))*(Pos (Z) ))->Void
posIsNotPosMultZero {j} {k}prf =  posIsNotZeroMultPos {k} (rewrite (multCommutativeZ (Pos Z) (Pos (S k))) in prf)
|||Proof that a positive number times a negative number is not Positive
posIsNotPosMultNeg :((Pos (S j)) = (Pos (S k))*(NegS p ))->Void
posIsNotPosMultNeg Refl impossible

|||Just a helper function for posDivByPosIsPos
PosEqualsPosNegIsContra:(c:ZZ)->(d:ZZ)->(q:ZZ)->(IsPositive c)->(IsPositive d)->(c=(d*q))->((IsNotPositive q)->Void)
PosEqualsPosNegIsContra (Pos (S k)) (Pos (S j)) (Pos Z) Positive Positive prf Zero =posIsNotPosMultZero prf
PosEqualsPosNegIsContra (Pos (S i)) (Pos (S j)) (NegS k) Positive Positive prf Negative = posIsNotPosMultNeg prf

|||Proof that if (c = d*q) and c and d are positive , then q is positive
posDivByPosIsPos:{c:ZZ}->{d:ZZ}->{q:ZZ}->(IsPositive c)->(IsPositive d)->(c=(d*q))->(IsPositive q)
posDivByPosIsPos {c}{d}{q} cPos dPos eqProof = notNotPositiveimpliesPositive (PosEqualsPosNegIsContra c d q cPos dPos eqProof)

|||The theorem (m<=n) and (n<=m) implies n=m for integers
lteAndGteImpliesEqualZ:{m:ZZ}-> {n:ZZ}->(LTEZ m n)-> (LTEZ n m)->(n=m)
lteAndGteImpliesEqualZ (PositiveLTE x) (PositiveLTE y) =  cong (lteAndGteImpliesEqual x y)
lteAndGteImpliesEqualZ NegLessPositive (PositiveLTE _) impossible
lteAndGteImpliesEqualZ NegLessPositive NegLessPositive impossible
lteAndGteImpliesEqualZ NegLessPositive (NegativeLte _) impossible
lteAndGteImpliesEqualZ (NegativeLte x) (NegativeLte y) = cong (lteAndGteImpliesEqual y x)

|||A proof that if c and d are positive and d =c*q then (c<=d)
posLteMultPosPosEqZ: {q:ZZ}->(c:ZZ)->(d:ZZ)->(IsPositive c)->(IsPositive d)->(d=c*q)->(LTEZ c d)
posLteMultPosPosEqZ {q} c d cPos dPos prf = rewrite prf in (rewrite (multCommutativeZ c q) in (posLteMultPosPosZ c q cPos qPos)) where
  qPos= posDivByPosIsPos dPos cPos prf


text:
module Examples.Declassificcation.PWHatch

import Control.ST
import Data.Vect

import DepSec.DIO
import DepSec.Labeled
import DepSec.Ref

import Examples.TwoPointLattice

%default total

printBool : Bool -> DIO L ()
printBool False = lift $ putStrLn "Wrong guess"
printBool True = lift $ putStrLn "Correct guess!"

--------------------------------------------------------------------------------
-- Library code
--------------------------------------------------------------------------------
DIO' : l -> (ty : Type) -> List (Action ty) -> Type
DIO' l = ST (DIO l)

data Counter : Nat -> Type where
  ||| TCB
  MkCounter : (n : Nat) -> Counter n

Attempts : Nat -> Type
Attempts = State . Counter

decCounter : Counter (S n) -> Counter n
decCounter _ {n} = MkCounter n

limit : (f : a -> b)
     -> (arg : a)
     -> DIO' l b [attempts ::: Attempts (S n) :-> Attempts n]
limit f arg {attempts} = returning (f arg) $ update attempts decCounter

hatch : (labeled : Labeled H Int) ->
        (guess : Int) ->
        DIO' l Bool [attempts ::: Attempts (S n) :-> Attempts n]
hatch (MkLabeled v) = limit (\g => g == v)

||| TCB
run : DIO' l a [] -> IO a
run = DepSec.DIO.run . Control.ST.run

--------------------------------------------------------------------------------
-- Bob (untrusted)
--------------------------------------------------------------------------------
bob : Labeled H Int ->
      DIO' L () [attempts ::: Attempts (3 + n) :-> Attempts n]
bob secret =
  do x1 <- hatch secret 1
     lift $ printBool x1
     x2 <- hatch secret 2
     lift $ printBool x2
     x3 <- hatch secret 42
     lift $ printBool x3
     -- x4 <- hatch secret 4 -- illegal!
     pure ()

--------------------------------------------------------------------------------
-- Alice (trusted)
--------------------------------------------------------------------------------
alice : DIO' L () []
alice =
  do attempts <- new (MkCounter 3)
     let secret : Labeled H Int = label 42
     bob secret
     delete attempts

main : IO ()
main = run $ alice

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
-- Network.TCP.TCPClient: TCP Client
module IdrisNet.TCP.TCPClient
import IdrisNet.PacketLang
import IdrisNet.Packet
import IdrisNet.TCP.TCPCommon
import Network.Socket
import Effects

%access public

data ClientConnected : Type where
  CC : Socket -> ClientConnected

-- State recording that an error occurred (therefore no operations
-- may be performed)
data ErrorState : Type where
  ES : Socket -> ErrorState

-- Interprets the result of
interpConnectRes : SocketOperationRes a -> Type
interpConnectRes (OperationSuccess _) = ClientConnected
interpConnectRes _ = ()

-- Interprets the result of a socket operation (for example reading, writing or binding
interpOperationRes : SocketOperationRes a -> Type
interpOperationRes (OperationSuccess _) = ClientConnected
interpOperationRes (FatalError _) = ErrorState
interpOperationRes (RecoverableError _) = ClientConnected
interpOperationRes ConnectionClosed = ()

-- TCP Client Effect
data TCPClient : Effect where
  Connect      : SocketAddress -> Port -> {() ==> {result} interpConnectRes result}
                                          TCPClient (SocketOperationRes Socket)
  Close        : { ClientConnected ==> ()} TCPClient ()
  Finalise     : { ErrorState ==> () } TCPClient ()
  WriteString  : String -> { ClientConnected ==> {result} interpOperationRes result}
                           TCPClient (SocketOperationRes ByteLength)
  ReadString   : ByteLength ->
                 { ClientConnected ==> {result} interpOperationRes result }
                 TCPClient (SocketOperationRes (String, ByteLength))

  WritePacket  : (pl : PacketLang) ->
                 (mkTy pl) ->
                 { ClientConnected ==> {result} interpOperationRes result }
                 TCPClient (SocketOperationRes ByteLength)

  ReadPacket   : (pl : PacketLang) ->
                 Length -> -- I really dislike this sod being here
                 { ClientConnected ==> {result} interpOperationRes result }
                 TCPClient (SocketOperationRes (Maybe (mkTy pl, ByteLength)))

TCPCLIENT : Type -> EFFECT
TCPCLIENT t = MkEff t TCPClient

-- Attempts to connect to a remote host and port. If it fails, remains in
-- the uninitialised state. If it succeeds, transitions to ClientConnected.
tcpConnect : SocketAddress -> Port -> { [TCPCLIENT ()] ==> {result}
                                        [TCPCLIENT (interpConnectRes result)] }
                                      Eff (SocketOperationRes Socket)
tcpConnect sa port = call (Connect sa port)

-- Closes a connected socket.
tcpClose : { [TCPCLIENT (ClientConnected)] ==> [TCPCLIENT ()] } Eff ()
tcpClose = call Close

-- Finalises a socket that has errored
tcpFinalise : { [TCPCLIENT (ErrorState)] ==> [TCPCLIENT ()] } Eff ()
tcpFinalise = call Finalise

{- vv These may all fail, so must be checked for failures after the operations -}

-- Sends a string
tcpSend : String -> { [TCPCLIENT (ClientConnected)] ==> {result}
                      [TCPCLIENT (interpOperationRes result)] }
                     Eff (SocketOperationRes ByteLength)
tcpSend dat = call (WriteString dat)

-- Receives a string
tcpRecv : ByteLength ->
          { [TCPCLIENT (ClientConnected)] ==> {result}
            [TCPCLIENT (interpOperationRes result)] }
          Eff (SocketOperationRes (String, ByteLength))
tcpRecv bl = call (ReadString bl)

-- Sends a PacketLang packet
tcpWritePacket : (pl : PacketLang) ->
                 (mkTy pl) ->
                 { [TCPCLIENT ClientConnected] ==> {result}
                   [TCPCLIENT (interpOperationRes result)] }
                 Eff (SocketOperationRes ByteLength)
tcpWritePacket pl dat = call (WritePacket pl dat)

-- Receives a PacketLang packet
tcpReadPacket : (pl : PacketLang) ->
                Length -> -- TODO: Ideally we won't need this parameter
                { [TCPCLIENT ClientConnected] ==> {result}
                  [TCPCLIENT (interpOperationRes result)] }
                Eff (SocketOperationRes (Maybe (mkTy pl, ByteLength)))
tcpReadPacket pl len = call (ReadPacket pl len)

instance Handler TCPClient IO where
  handle () (Connect sa port) k = do
    -- Firstly create a socket
    sock_res <- socket AF_INET Stream 0
    case sock_res of
         Left err => k (FatalError err) ()
         Right sock => do
           conn_res <- connect sock sa port
           if (conn_res == 0) then -- Success
             k (OperationSuccess sock) (CC sock)
           else do
             close sock
             k (FatalError conn_res) ()

  handle (CC sock) (Close) k = do
    close sock
    k () ()

  handle (ES sock) (Finalise) k = do
    close sock
    k () ()

  handle (CC sock) (WriteString dat) k = do
    send_res <- send sock dat
    case send_res of
      Left err =>
      -- Some errors are benign, meaning the connection survives.
        if (err == EAGAIN) then
          k (RecoverableError err) (CC sock)
        else -- Some aren't
          k (FatalError err) (ES sock)
      -- Success: return number of bytes sent
      Right bytes => k (OperationSuccess bytes) (CC sock)

  handle (CC sock) (ReadString byte_len) k = do
    recv_res <- recv sock byte_len
    either (\err => if (err == EAGAIN) then
                               k (RecoverableError err) (CC sock)
                             else
                               if (err == 0) then -- socket closed
                                 k (ConnectionClosed) ()
                               else
                                 k (FatalError err) (ES sock))
           (\res => k (OperationSuccess res) (CC sock)) recv_res

  handle (CC sock) (WritePacket pl dat) k = do
    (pckt, len) <- marshal pl dat
    send_res <- sendBuf sock pckt len
    case send_res of
         Left err =>
          if err == EAGAIN then
            k (RecoverableError err) (CC sock)
          else
            k (FatalError err) (ES sock)
         Right bl => k (OperationSuccess bl) (CC sock)

  handle (CC sock) (ReadPacket pl len) k = do
    ptr <- sock_alloc len
    recv_res <- recvBuf sock ptr len
    case recv_res of
         Left err =>
           if err == EAGAIN then
             k (RecoverableError err) (CC sock)
           else if err == 0 then
             k (ConnectionClosed) ()
           else
             k (FatalError err) (ES sock)
         Right bl => do
           res <- unmarshal pl ptr bl
           sock_free ptr
           -- The OperationSuccess depends on the actual network-y
           -- part, not the unmarshalling. If the unmarshalling fails,
           -- we still keep the connection open.
           k (OperationSuccess res) (CC sock)