text:
-- --------------------------------------------------------------- [ Utils.idr ]
-- Module    : Utils.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module GRL.Utils

import Data.GraphViz.SimpleDot

import GRL.Common
import GRL.Model

%access export

toSimpleDot : GModel -> SimpleDot GRAPH
toSimpleDot g = Digraph (nodes (verticesID g)) (edges' (edges g))
  where

    f : NodeID -> String
    f n = case getValueByID n g of
        Nothing => ""
        Just u  => getNodeTitle u

    nodes : List NodeID -> List (SimpleDot NODE)
    nodes vs = map (\x => Node (x) [("label", (f x))]) vs

    convEdge : Edge GoalEdge -> SimpleDot EDGE
    convEdge (x,y, Nothing)     = Edge (y) (x) Nil

    convEdge (x,y, Just Decomp) =
        Edge (y) (x) [("label", "Decomp FIX")]

    convEdge (x,y, Just (Contribution l)) =
        Edge (x) (y) [("label", "Impacts " ++ show l)]

    convEdge (x,y, Just (Correlation  l)) =
        Edge (x) (y) [("label", "Affects " ++ show l)]

    edges' : List (Edge GoalEdge) -> List (SimpleDot EDGE)
    edges' es = map (convEdge) es

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
import Data.DPair
import Data.List.Elem
import Data.List.Quantifiers

data IsEven : Nat -> Type where
  Z : IsEven Z
  S : IsEven k -> IsEven $ S $ S k

data IsPower2 : Nat -> Type where
  Base : IsPower2 1
  Next : IsPower2 k -> IsPower2 (k + k)

InterestingList : Type
InterestingList = List Nat `Subset` \xs => (All IsEven xs, (p1 ** p2 ** (Elem p1 xs, Elem p2 xs, IsPower2 p1, IsPower2 p2, Not $ p1 === p2)))

lxs : InterestingList
lxs = Element [2, 4] (%search, (2 ** 4 ** (%search, %search, Next Base, Next $ Next Base, \case Refl impossible)))

ext: idr

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Replica.Other.Decorated

import Replica.Option.Types
import Replica.Other.Free

%default total

public export
Builder : (ty : (Type -> Type) -> Type) -> Type
Builder ty = ty (\a => Either (Maybe a) a)

public export
Default : (ty : (Type -> Type) -> Type) -> Type
Default ty = ty Maybe

public export
Done : (ty : (Type -> Type) -> Type) -> Type
Done ty = ty id

public export
interface TyMap (0 ty : (Type -> Type) -> Type) where
  tyMap : (forall x. f x -> g x) -> ty f -> ty g

public export
interface TyTraversable (0 ty : (Type -> Type) -> Type) where
  tyTraverse : Applicative g => (forall a. f a -> g a) -> ty f -> g (Done ty)

export
initBuilder : TyMap ty => Default ty -> Builder ty
initBuilder = tyMap Left

export
build : TyTraversable ty => Builder ty -> Maybe (Done ty)
build = tyTraverse (either id Just)

export
one : (get : b -> Either c a) -> (set : a -> b -> b) -> (errMsg : a -> a -> err) ->
      a -> b -> Either err b
one get set errMsg x y = case get y of
                              Left _ => Right $ set x y
                              Right z => Left $ errMsg x z

export
ifSame : Eq a =>
         (get : b -> Either c a) -> (set : a -> b -> b) -> (errMsg : a -> a -> err) ->
         a -> b -> Either err b
ifSame get set errMsg x y = case get y of
  Left  _ => Right $ set x y
  Right z => if x /= z
                then Left $ errMsg x z
                else Right y

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module Generics.Newtype

import public Generics.Newtype.Num
import public Generics.Newtype.Neg
import public Generics.Newtype.Abs
import public Generics.Newtype.Fractional
import public Generics.Newtype.FromDouble
import public Generics.Newtype.Integral
import public Generics.Derive

-- %language ElabReflection
--
-- public export
-- data Raf = MkRaf Double
-- %runElab derive "Raf"
--   [Generic, Eq, Ord, Num, Neg, Abs, Fractional, FromDouble]
--
-- public export
-- data Raff a b = MkRaff a b
-- %runElab derive "Raff"
--   [Generic, Eq, Ord, Num, Neg, Abs, Fractional, FromDouble, Integral]


text:
> module Matrix.Matrix

> import Data.Vect

> %default total

> %access public export

> Matrix : (m : Nat) -> (n : Nat) -> Type -> Type
> Matrix m n t = Vect m (Vect n t)

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
import Data.String
import Data.Vect

StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True = Int

getStringOrInt : (isInt : Bool) -> StringOrInt isInt
getStringOrInt False = "Ninety four"
getStringOrInt True = 94

valToString : (isInt : Bool) -> StringOrInt isInt -> String
valToString False y = trim y
valToString True y = cast y

valToString' : (isInt : Bool) -> (case isInt of
                                       False => String
                                       True => Int) -> String
valToString' False y = trim y
valToString' True y = cast y


text:
module Main

import Data.Vect
import Data.Vect.Quantifiers
import System

%default total

fiveIsNotZero : Not (the Nat 5 = 0)
fiveIsNotZero = \Refl impossible

threeIsNotZero : Not (the Nat 3 = 0)
threeIsNotZero = \Refl impossible

modFive : Nat -> Nat
modFive k = modNatNZ k 5 fiveIsNotZero

modThree : Nat -> Nat
modThree k = modNatNZ k 3 threeIsNotZero

record FizzBuzzValue where
    constructor MkFizzBuzzValue
    i : Nat
    s : String

data FizzBuzzProp : FizzBuzzValue -> Type where
     FizzCase : (modThree x = 0) ->
                (Not (modFive x = 0)) ->
                FizzBuzzProp (MkFizzBuzzValue x "Fizz")
     BuzzCase : (Not (modThree x = 0)) ->
                (modFive x = 0) ->
                FizzBuzzProp (MkFizzBuzzValue x "Buzz")
     FizzBuzzCase : (modThree x = 0) ->
                    (modFive x = 0) ->
                    FizzBuzzProp (MkFizzBuzzValue x "FizzBuzz")
     NatCase : (Not (modThree x = 0)) ->
               (Not (modFive x = 0)) ->
               FizzBuzzProp (MkFizzBuzzValue x (show x))

data TotalOrderVect : (p : a -> a -> Type) -> (v : Vect n a) -> Type where
     EmptyVectCase : TotalOrderVect p []
     SingletonCase : TotalOrderVect p [x]
     ConsCase : (tailPrf : TotalOrderVect p (y::ys)) ->
                (headPrf : (p x y)) ->
                TotalOrderVect p (x :: y :: ys)

data FizzBuzzValueNatProp : (p : Nat -> Nat -> Type) ->
                            (a : FizzBuzzValue) ->
                            (b : FizzBuzzValue) ->
                            Type where
     FromNatProp : (natProp : p (i a) (i b)) -> FizzBuzzValueNatProp p a b

oneIsNotMulThree : Not (modThree 1 = fromInteger 0)
oneIsNotMulThree Refl impossible

oneIsNotMulFive : Not (modFive 1 = fromInteger 0)
oneIsNotMulFive Refl impossible

safeHead : (Not (n = Z)) -> (Vect n a) -> a
safeHead {n = Z} nIsNotZP [] = void (nIsNotZP Refl)
safeHead {n = (S len)} nIsNotZP (y :: xs) = y

sGTNotS : GT (S k) k
sGTNotS {k = Z} = LTESucc LTEZero
sGTNotS {k = (S n)} = LTESucc sGTNotS

fizzBuzz : (n : Nat) ->
           (nIsNotZP : Not (n = Z)) ->
           (v : Vect n FizzBuzzValue **
                (All FizzBuzzProp v,
                 n = (i (safeHead nIsNotZP v)),
                 TotalOrderVect (FizzBuzzValueNatProp GT) v))
fizzBuzz Z nIsNotZP = void $ nIsNotZP Refl
fizzBuzz (S Z) _ = (_ ** ([NatCase oneIsNotMulThree oneIsNotMulFive], Refl, SingletonCase))
fizzBuzz (S (S k)) _ = let (_::_ ** (fizzBuzzInTailP, skInHeadP, totalOrderPoof))
                            = (fizzBuzz (S k) SIsNotZ) in
                         case (decEq (modThree (S (S k))) 0, decEq (modFive (S (S k))) 0) of
                            (Yes mulOfThreeP, No notMulOfFiveP) =>
                                 (_ ** (FizzCase mulOfThreeP notMulOfFiveP :: fizzBuzzInTailP,
                                       Refl,
                                       ConsCase totalOrderPoof $
                                                rewrite skInHeadP in FromNatProp sGTNotS))
                            (No notMulOfThreeP, Yes mulOfFiveP) =>
                                (_ ** (BuzzCase notMulOfThreeP mulOfFiveP :: fizzBuzzInTailP,
                                      Refl,
                                      ConsCase totalOrderPoof $
                                               rewrite skInHeadP in FromNatProp sGTNotS))
                            (Yes mulOfThreeP, Yes mulOfFiveP) =>
                                 (_ ** (FizzBuzzCase mulOfThreeP mulOfFiveP :: fizzBuzzInTailP,
                                       Refl,
                                       ConsCase totalOrderPoof $
                                                rewrite skInHeadP in FromNatProp sGTNotS))
                            (No notMulOfThreeP, No notMulOfFiveP) =>
                                (_ ** (NatCase notMulOfThreeP notMulOfFiveP :: fizzBuzzInTailP,
                                      Refl,
                                      ConsCase totalOrderPoof $
                                               rewrite skInHeadP in FromNatProp sGTNotS))

fizzBuzzDriver : (n : Nat) -> Maybe String
fizzBuzzDriver n = case decEq n Z of
                        Yes _ => Nothing
                        No nIsNotZP => Just $ concatMap (++"\n") $
                                              reverse $
                                              map s $
                                              fst $
                                              fizzBuzz n nIsNotZP

partial
main : IO ()
main = do
     args <- getArgs
     case args of
          (_ :: n :: []) => case all isDigit $ unpack n of
                True => case fizzBuzzDriver $ cast n of
                              Just fizzBuzzString => do putStr fizzBuzzString
                                                        exitSuccess
                              Nothing => do putStrLn "The argument can't be zero."
                                            exitFailure
                False => do putStrLn "The argument isn't a number."
                            exitFailure
          _ => do putStrLn "Wrong number of arguments."
                  exitFailure

max_stars_repo_name: batonius/idris-fizzbuzz

max_issues_repo_name: batonius/idris-fizzbuzz

max_forks_repo_name: batonius/idris-fizzbuzz


text:
module Data.Subset.Interfaces

import Data.Subset.Predicates
import Data.List
import public Decidable.Equality

%default total

||| In order to verify a predicate to hold for a given value
||| at runtime, it has to implement this interface.
public export
interface Predicate t (0 p : t -> Type) | p where
  ||| Validates a value against the given predicate.
  validate : (v : t) -> Dec (p v)

||| Runtime refinement of values.
public export
refineMay : Predicate t p => (v : t) -> Maybe (Subset t p)
refineMay v = case validate {p = p} v of
                   (Yes prf) => Just (Element v prf)
                   (No _)    => Nothing

public export
Predicate (List a) NonEmpty where
  validate []       = No absurd
  validate (_ :: _) = Yes IsNonEmpty

public export
Predicate k p => Predicate k (Neg p) where
  validate v with (validate { p = p } v)
    validate v | (Yes prf)   = No \(IsNeg c) => c prf
    validate v | (No contra) = Yes $ IsNeg contra

public export
{f : t -> Bool} -> Predicate t (Is f) where
  validate v = case decEq (f v) True of
                    (Yes prf)   => Yes $ ItIs prf
                    (No contra) => No \(ItIs prf) => contra prf

public export
{f : a -> b} -> Predicate b p => Predicate a (Via f p) where
  validate v = case validate {p = p} (f v) of
                    (Yes prf)   => Yes $ Go v prf
                    (No contra) => No \(Go _ prf) => contra prf

consInjective : And (p::ps) v -> (p v, And ps v)
consInjective (prf :: prfs) = (prf, prfs)

public export
Predicate t (And []) where
  validate v = Yes Nil

public export
Predicate t p => Predicate t (And ps) => Predicate t (And (p :: ps)) where
  validate v with (validate {p = p} v)
    validate v | No contra = No (contra . fst . consInjective)
    validate v | Yes phead with (validate {p = And ps} v)
      validate v | Yes phead | Yes ptail = Yes $ phead :: ptail
      validate v | Yes phead | No contra = No (contra . snd . consInjective)

public export
Uninhabited (Or [] v) where
  uninhabited _ impossible

public export
Predicate t (Or []) where
  validate v = No absurd

public export
Predicate t p => Predicate t (Or ps) => Predicate t (Or (p::ps)) where
  validate v with (validate {p = p} v)
    validate v | Yes prf = Yes $ Z prf
    validate v | No contra with (validate {p = Or ps} v)
      validate v | No contra | Yes prf = Yes $ S prf
      validate v | No contra | No contra2 =
        No $ \any => case any of
                          (Z p) => contra p
                          (S p) => contra2 p


text:
module Meriv.Core.Queries

||| A query in the schema s with result type r.
data Query (s : MvBaseSchema) r where
  -- Given a relation, and some constraints on the arguments
  -- based on mode...
  -- MkQuery :

max_stars_repo_name: Sintrastes/meriv-idr-prototype

max_issues_repo_name: Sintrastes/meriv-idr-prototype

max_forks_repo_name: Sintrastes/meriv-idr-prototype


text:
import Language.Reflection

%language ElabReflection

foo : Elab (NameType, NameType, NameType)
foo
  = do [n] <- getInfo `{ Prelude.Nat }
           | _ => fail "Can't find Nat"
       [s] <- getInfo `{ Prelude.S }
           | _ => fail "Can't find S"
       [p] <- getInfo `{ Prelude.plus }
           | _ => fail "Can't find plus"
       pure (nametype (snd n), nametype (snd s), nametype (snd p))


text:
module Examples.FileExamples

import Data.List

import DepSec.DIO
import DepSec.Labeled
import DepSec.File

import Examples.TwoPointLattice as TPL
import Examples.FourPointLattice as FPL

%default total

--------------------------------------------------------------------------------
-- Bob/library, untrusted
--------------------------------------------------------------------------------

||| Generic file for keeping files of diffent level in same datastructure
GenFile : Type -> Type
GenFile label = (l : label ** SecFile l)

annotateStr : Either FileError String -> String
annotateStr (Left error) = "Deduced information that no file with this name existed"
annotateStr (Right str) = str ++ "\n The above was annotated by Bob."

annotateFile : Poset labelType
            => {l : labelType}
            -> (file: SecFile l)
            -> DIO l ()
annotateFile {l} file =
  do labeledSecContent <- readFile {flow = reflexive l} file
     secComp <- unlabel {flow = reflexive l} labeledSecContent
     let labeledSecret = label $ annotateStr secComp
     writeFile {flow = reflexive l} {flow' = reflexive l} file labeledSecret
     pure ()

moveContent : Poset labelType
           => {l, l' : labelType}
           -> {auto flowup : l `leq` l'}
           -> (source: SecFile l)
           -> (dest: SecFile l')
           -> DIO l ()
moveContent {flowup} {l} {l'} source dest =
  do labeledSecContent <- readFile {flow = reflexive l} source
     secComp <- unlabel {flow = reflexive l} labeledSecContent
     let labeledSecret = label $ annotateStr secComp
     writeFile {flow = flowup} {flow' = reflexive l'} dest labeledSecret
     pure ()

||| Read two files to join
readTwoFiles : BoundedJoinSemilattice label
            => {l, l' : label}
            -> SecFile l
            -> SecFile l'
            -> DIO (Bottom {a=label}) (Labeled (join l l') (Either FileError String))
readTwoFiles file1 file2 {l} {l'} =
  do file1' <- readFile {flow = leq_bot_x l} file1
     file2' <- readFile {flow = leq_bot_x l'} file2
     let dio : DIO (join l l') (Either FileError String)
       = do c1 <- unlabel {flow = join_x_xy l l'} file1'
            c2 <- unlabel {flow = join_y_xy l l'} file2'
            pure $ case (c1, c2) of
                        (Right c1', Right c2') => Right $ c1' ++ c2'
                        (Left e1, _) => Left e1
                        (_, Left e2) => Left e2
     plug {flow = leq_bot_x (join l l')} dio

||| Get list of labels from list of files.
getLabels : List (GenFile labelType) -> List labelType
getLabels [] = []
getLabels ((l ** _) :: files) = l :: getLabels files

||| Get total join of a list of labels.
getJoinOfLabels : BoundedJoinSemilattice labelType => List labelType -> labelType
getJoinOfLabels [] = Bottom
getJoinOfLabels (x :: xs) = join x (getJoinOfLabels xs)

||| Get join of security levels from a list of files.
joinOfFiles : BoundedJoinSemilattice label => List (GenFile label) -> label
joinOfFiles xs = getJoinOfLabels $ getLabels xs

||| Convenient helper function for converting Either FileError String to String.
getString : Either FileError String -> String
getString (Left error) = "----Missing file----\n"
getString (Right str) = str ++ "\n"

||| Convenient helper function for concatenating content of same level.
addContent : DIO l String
          -> DIO l (Either FileError String)
          -> DIO l String
addContent accDIO newDIO = do pure $ !accDIO ++ (getString !newDIO)

addContent' : DIO l (Either (List FileError) String)
           -> DIO l (Either FileError String)
           -> DIO l (Either (List FileError) String)
addContent' c1 c2 =
  do pure $ case (!c1, !c2) of
                 (Right c1', Right c2') => Right $ c1' ++ c2'
                 (Left e1, Left e2) => Left $ e2 :: e1
                 (Left e1, Right c1) => Left e1
                 (Right c1', Left e2) => Left [e2]

||| A type which describes that a list is a sublist of another list
data SubOrEqualList : List a -> List a -> Type where
  Base : SubOrEqualList list list
  Greater : (prf: SubOrEqualList xs bs) -> SubOrEqualList xs (b::bs)

||| A proof that if a l is allowed to flow to join of sublist then it can flow to join of superlist as well
total subSuperListFlow : BoundedJoinSemilattice lt
                      => (l : lt)
                      -> (superList : List lt)
                      -> (subList : List lt)
                      -> (setPrf : SubOrEqualList subList superList)
                      -> (flowPrf : l `leq` (getJoinOfLabels subList))
                      -> l `leq` (getJoinOfLabels superList)
subSuperListFlow l [] [] x flowPrf = flowPrf
subSuperListFlow _ [] (_ :: _) Base _ impossible
subSuperListFlow _ [] (_ :: _) (Greater _) _ impossible
subSuperListFlow l (z :: xs) (z :: xs) Base flowPrf = flowPrf
subSuperListFlow l (z :: xs) subList (Greater prf) flowPrf =
  let proofOfSubList  = subSuperListFlow l xs subList prf flowPrf
      nearlyThere = join_x_xy (getJoinOfLabels xs) z
      evenBetter: leq (getJoinOfLabels xs) (join z (getJoinOfLabels xs))
        = rewrite commutative z (getJoinOfLabels xs) in nearlyThere
  in transitive l (getJoinOfLabels xs) (join z (getJoinOfLabels xs)) proofOfSubList evenBetter

||| Function for constructing a proof that a list is sublist or equal to itself.
buildSubList : (list : List a) -> SubOrEqualList list list
buildSubList list = Base

||| Function for constructing a proof that if (x::xs) is sublist then xs will be a sublist as well.
buildSubListProf : (subsetProf: SubOrEqualList (x::xs) list)
               -> SubOrEqualList xs list
buildSubListProf Base = Greater Base
buildSubListProf (Greater prf) = Greater (buildSubListProf prf)

||| Proof that a specific label in a list of labels is allowed to flow to join of that list.
||| @l the label which we want a proof for.
||| @list the list of labels.
||| @prf a proof that l is in the list.
total listElemProver : BoundedJoinSemilattice lt
                    => (l : lt)
                    -> (list : List lt)
                    -> {auto prf :Elem l list}
                    -> leq l (getJoinOfLabels list)
listElemProver _ [] {prf = Here} impossible
listElemProver _ [] {prf = There _} impossible
listElemProver _ (z :: xs) {prf = Here} =
  join_x_xy z (getJoinOfLabels xs)
listElemProver l (z :: xs) {prf = (There later)} =
  let flowTail = listElemProver l xs
      help = join_x_xy (getJoinOfLabels xs) z
      nearlyThere = transitive l (getJoinOfLabels xs) (join (getJoinOfLabels xs) z) flowTail help
  in rewrite (commutative z (getJoinOfLabels xs)) in nearlyThere

readFiles : BoundedJoinSemilattice a
         => (files: (List (GenFile a)))
         -> DIO (Bottom {a}) (Labeled (joinOfFiles files) (Either (List FileError) String))
readFiles {a} files
  = let initialAcc : DIO Bottom (Labeled (joinOfFiles files) (Either (List FileError) String))
      = pure $ label $ Right ""
    in readFilesAcc files initialAcc

  where
  readFilesAcc : (trailingList : List (GenFile a))
              -> {auto subsetProf: SubOrEqualList (getLabels trailingList) (getLabels files)}
              -> (acc : DIO (Bottom {a}) (Labeled (joinOfFiles files) (Either (List FileError) String)))
              -> DIO (Bottom {a}) (Labeled (joinOfFiles files) (Either (List FileError) String))
  readFilesAcc [] acc = acc
  readFilesAcc {subsetProf} ((l ** file) :: xs) acc =
    do labeledNewContent <- readFile file {flow = leq_bot_x l}
       let subsetProofy : leq l (joinOfFiles ((l ** file) :: xs))
         = listElemProver {prf = Here} l (getLabels ((l ** file) :: xs))
       let trueProof : leq l (joinOfFiles files)
         = subSuperListFlow l (getLabels files)
                            (getLabels ((l ** file) :: xs)) subsetProf subsetProofy
       let content : DIO (joinOfFiles files) (Either FileError String)
         = unlabel {flow = trueProof} labeledNewContent
       let dioAcc : DIO (joinOfFiles files) (Either (List FileError) String)
         = unlabel !acc {flow = reflexive (joinOfFiles files)}
       let newDIOAcc : DIO (Bottom {a}) (Labeled (joinOfFiles files) (Either (List FileError) String))
         = plug {flow = leq_bot_x (joinOfFiles files)} $ addContent' dioAcc content
       readFilesAcc {subsetProf = (buildSubListProf subsetProf)} xs newDIOAcc

readFiles' : BoundedJoinSemilattice a => DecEq a => (files: (List (GenFile a)))
          -> DIO (Bottom {a}) (Labeled (joinOfFiles files) (Either (List FileError) String))
readFiles' {a} files
  = readFilesAcc files $ pure $ label $ Right ""
  where
  readFilesAcc : (trailingList : List (GenFile a))
              -> (acc : DIO (Bottom {a}) (Labeled (joinOfFiles files) (Either (List FileError) String)))
              -> DIO (Bottom {a}) (Labeled (joinOfFiles files) (Either (List FileError) String))
  readFilesAcc [] acc = acc
  readFilesAcc ((l ** file) :: xs) acc =
    case decLeq l (joinOfFiles files) of --JIF actsfor check.
      Yes prf =>
        do labeledNewContent <- readFile file {flow = leq_bot_x l}
           let content = unlabel {flow = prf} labeledNewContent
           let uacc  = unlabel !acc {flow = reflexive (joinOfFiles files)}
           let acc' = plug {flow = leq_bot_x (joinOfFiles files)} $ addContent' uacc content
           readFilesAcc xs acc'
      No _ => acc -- Never gonna happen.

||| Reads all files of certain level to a string of that particular level.
readAllFilesOfLevel : BoundedJoinSemilattice lt
                   => DecEq lt
                   => (level: lt)
                   -> (list: List (GenFile lt))
                   -> DIO (Bottom {a = lt}) (Labeled level String)
readAllFilesOfLevel {lt} level list =
  let init : DIO (Bottom {a = lt}) (Labeled level String) = pure $ label ""
  in readSameLevelFiles (createListOfSameLevel list []) init

  where
  readSameLevelFiles : (list' : List (SecFile level))
                    -> (acc: DIO (Bottom {a = lt}) (Labeled level String))
                    -> DIO (Bottom {a = lt}) (Labeled level String)
  readSameLevelFiles [] acc = acc
  readSameLevelFiles (file :: xs) acc
    = do labeledNewContent <- readFile file {flow = (leq_bot_x level)}
         let content : DIO level (Either FileError String)
           = unlabel labeledNewContent {flow = reflexive level}
         let dioAcc : DIO level String
           = unlabel !acc {flow = reflexive level}
         let newDIOAcc : DIO (Bottom {a = lt}) (Labeled level String)
           = plug {flow = (leq_bot_x level)} $ addContent dioAcc content
         readSameLevelFiles xs newDIOAcc

  createListOfSameLevel : (list' : List (GenFile lt))
                       -> (acc : List (SecFile level))
                       -> List (SecFile level)
  createListOfSameLevel [] acc = acc
  createListOfSameLevel ((l ** file) :: xs) acc
    = case decEq level l of
        Yes Refl => createListOfSameLevel xs (file :: acc)
        No contra => createListOfSameLevel xs acc

||| Read all files below a certain level to a string of that particular level
readAllFilesBelowLevel : BoundedJoinSemilattice a
                      => DecEq a
                      => (list : List (GenFile a))
                      -> (level : a)
                      -> DIO (Bottom {a}) (Labeled level String)
readAllFilesBelowLevel {a} list level =
  readFilesAcc list $ pure $ label ""

  where
  readFilesAcc : (trailingList : List (GenFile a))
              -> (acc : DIO (Bottom {a}) (Labeled level String))
              -> DIO (Bottom {a}) (Labeled level String)
  readFilesAcc [] acc = acc
  readFilesAcc ((l ** file) :: xs) acc =
    case decLeq l level of
      (Yes prf) =>
        do labeledNewContent <- readFile file {flow = (leq_bot_x l)}
           let content : DIO level (Either FileError String)
             = unlabel labeledNewContent {flow = prf}
           let dioAcc : DIO level String
             = unlabel !acc {flow = reflexive level}
           let newDIOAcc : DIO (Bottom {a}) (Labeled level String)
             = plug {flow = leq_bot_x level} $ addContent dioAcc content
           readFilesAcc xs newDIOAcc
      (No contra) => readFilesAcc xs acc

-- Alice, trusted
namespace tp

  secretFile : SecFile TPL.H
  secretFile = makeFile "tpSecretFile.txt"

  publicFile : SecFile TPL.L
  publicFile = makeFile "tpPublicFile.txt"

  listOfFiles : List (GenFile TwoPoint)
  listOfFiles = [(_ ** secretFile), (_ ** publicFile)]

namespace fp
  secretFile : SecFile FPL.H
  secretFile = makeFile "fpSecretFile.txt"

  publicFile : SecFile FPL.L
  publicFile = makeFile "fpPublicFile.txt"

  medium1File : SecFile FPL.M1
  medium1File = makeFile "fpMedium1File.txt"

  medium2File : SecFile FPL.M2
  medium2File = makeFile "fpMedium2File.txt"

  listOfFilesH : List (GenFile FourPoint)
  listOfFilesH = [(_ ** medium1File), (_ ** publicFile), (_ ** medium2File)]

  listOfFilesM1 : List (GenFile FourPoint)
  listOfFilesM1 = [(_ ** medium1File), (_ ** publicFile)]

-- Silent fail on file errors
stringOfEither : BoundedJoinSemilattice a
              => {l : a}
              -> DIO (Bottom {a}) (Labeled l (Either (List FileError) String))
              -> DIO (Bottom {a}) (Labeled l String)
stringOfEither {a} {l} comp =
  do labeled <- comp
     let stringComp : DIO l String =
       do comp' <- unlabel {flow = reflexive l} labeled
          case comp' of
            Left _  => pure ""
            Right b => pure b
     plug {flow = leq_bot_x l} stringComp

main : IO ()
main =
  do putStrLn "Started.."

     -- annotateFile examples
     --------------------------------------------------
     run $ annotateFile tp.secretFile
     run $ annotateFile fp.secretFile

     -- moveContent examples
     --------------------------------------------------
     run $ moveContent {flowup = Refl} tp.publicFile tp.secretFile
     run $ moveContent {flowup = Refl} tp.secretFile tp.secretFile
     -- run $ moveContent tp.secretFile tp.publicFile -- Illegal flow!
     run $ moveContent {flowup = Refl} fp.publicFile fp.secretFile
     run $ moveContent {flowup = Refl} fp.secretFile fp.secretFile
     run $ moveContent {flowup = Refl} fp.medium1File fp.secretFile
     -- run $ moveContent fp.secretFile fp.medium1File -- Illegal flow!
     -- run $ moveContent fp.medium2File fp.medium1File -- Illegal flow!

     --------------------------------------------------
     tpLabeledString <- run $ stringOfEither $ readFiles tp.listOfFiles
     run $ writeFile {l = TPL.L} {flow = leq_bot_x (joinOfFiles tp.listOfFiles)} {flow' = Refl} tp.secretFile $ tpLabeledString
     -- run $ writeFile tp.publicFile tpLabeledString -- Illegal flow!
     fpLabeledStringH <- run $ stringOfEither $ readFiles fp.listOfFilesH
     run $ writeFile {l = FPL.L} {flow = leq_bot_x (joinOfFiles fp.listOfFilesH)} {flow' = Refl} fp.secretFile fpLabeledStringH
     -- run $ writeFile fp.medium1File fpLabeledStringH -- Illegal flow!
     fpLabeledStringM1 <- run $ stringOfEither $ readFiles fp.listOfFilesM1
     run $ writeFile {l = FPL.L} {flow = leq_bot_x (joinOfFiles fp.listOfFilesM1)} {flow' = Refl} fp.secretFile fpLabeledStringM1
     run $ writeFile {l = FPL.L} {flow = leq_bot_x (joinOfFiles fp.listOfFilesM1)} {flow' = Refl} fp.medium1File fpLabeledStringM1
     -- run $ writeFile fp.medium2File fpLabeledStringM1 -- Illegal flow!
     -- run $ writeFile fp.publicFile fpLabeledStringM1 -- Illegal flow!
     putStrLn "Done!"

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
import System.Info

main : IO ()
main = printLn (os /= "")


text:
module BiNat.Views

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

%default total

||| View for BiNat which represents whether the number is J or succ of something
public export
data SuccView : BiNat -> Type where
  IsJ    : SuccView J
  IsSucc : SuccView (succ n)

||| Determines whether the BiNat is J or succ of something.
export
succView : (n : BiNat) -> SuccView n
succView J = IsJ
succView (x -: I) = IsSucc {n = x -: O}
succView (x -: O) with (succView x)
  succView (J      -: O) | IsJ    = IsSucc {n = J}
  succView (succ n -: O) | IsSucc =
    rewrite sym $ plusJIsSucc n in
    rewrite sym $ plusDashAppendsAcc n J O [O] in
    rewrite plusAssociative (n -: O) J J in
    IsSucc {n = n -: I}

||| Recursive view for BiNat like Nat.
public export
data NatView : BiNat -> Type where
  NJ : NatView J
  NS : Lazy (NatView n) -> NatView (succ n)

||| Reconstruct the BiNat with NJ and NS, like Nat.
export
natView : (n : BiNat) -> NatView n
natView n = induction NatView (\k, nv => NS nv) NJ n

max_stars_repo_name: SekiT/BiNat

max_issues_repo_name: SekiT/BiNat

max_forks_repo_name: SekiT/BiNat


text:
import Data.Vect

hello : String
hello = "Hello World"

x : Int
x = 5

add : Int -> Int -> Int
add x y = x + y

Calc : Nat -> Type
Calc Z = String
Calc (S k) = Nat

divide : (dividend:Nat) -> (divisor:Nat) -> Calc divisor
divide dividend Z = "Divisor was 0"
divide dividend (S k) = div dividend (S k)

data VVect : (n:Nat) -> (a:Type) -> Type where
  VNil : VVect Z a
  VCons : (head : a) -> (tail : VVect k a) -> VVect (S k) a

vtake : (m : Nat) -> Vect (m + n) a -> Vect m a
vtake Z xs = []
vtake (S k) (x :: xs) = x :: vtake k xs

vappend : Vect m a -> Vect n a -> Vect (m+n) a
vappend [] ys = ys
vappend (x :: xs) ys = x :: vappend xs ys

main : IO ()
main = printLn ( vtake 4 [1,2,3,4] )


text:
module Main

id' : t -> t
id' x = x

-- type Dependent version of id
-- taking an explicit type as its first argument
the' : (t : Type) -> t -> t
the' t x = x

-- *hai> the' (Int)
-- the' Int : Int -> Int
-- *hai> the' (Int) 1
-- 1 : Int
-- *hai> id' 1
-- 1 : Integer

main : IO ()
main = putStrLn "Oh, hai"

StringOrIntType : Bool -> Type
StringOrIntType x = case x of
                  True => Int
                  False => String

stringOrIntVal : (x : Bool) -> StringOrIntType x
stringOrIntVal x = case x of
                      True => 7
                      False => "Seven"

valToString : (x : Bool) -> StringOrIntType x -> String
valToString x val = case x of
                        True => cast val
                        False => val

valToStringWithHole : (x : Bool) -> StringOrIntType x -> String
valToStringWithHole x val = case x of
                        True => ?xTrueType -- holes
                        False => ?xFalseType -- ctrl + alt + t

-- idris hai.idr
-- hai> valToString False "yaay"
-- "yaay" : String
-- *hai> valToString True 2
-- "2" : String


text:
module Control.Monad.RWS

import public Control.Monad.RWS.CPS as Control.Monad.RWS
import public Control.Monad.RWS.Interface as Control.Monad.RWS
import public Control.Monad.Reader.Interface as Control.Monad.RWS
import public Control.Monad.Writer.Interface as Control.Monad.RWS
import public Control.Monad.State.Interface as Control.Monad.RWS


text:
module Language.LSP.Definition

import Core.Context
import Core.Core
import Core.Directory
import Core.Env
import Core.Metadata
import Core.Options
import Data.List
import Data.String
import Data.String.Parser
import Data.URI
import Language.LSP.Message
import Libraries.Data.PosMap
import Server.Configuration
import Server.Log
import Server.Utils
import System.File
import System.Path

mkLocation' : Ref Ctxt Defs
           => Ref LSPConf LSPConfiguration
           => OriginDesc -> (Int, Int) -> (Int, Int) -> Core (Maybe Location)
mkLocation' origin (sline, scol) (eline, ecol) = do
  defs <- get Ctxt
  let PhysicalIdrSrc modIdent = origin
    | _ => logD GotoDefinition "Origin doesn't have an Idris file attached to it \{show origin}" >> pure Nothing
  let wdir = defs.options.dirs.working_dir
  let pkg_dirs = filter (/= ".") defs.options.dirs.extra_dirs
  let exts = show <$> listOfExtensions
  Just fname_abs <- catch
      (Just . (wdir </>) <$> nsToSource replFC modIdent) -- Try local source first
      -- if not found, try looking for the file amongst the loaded packages.
      (const $ firstAvailable $ do
        pkg_dir <- pkg_dirs
        -- Assume that if the package dir is relative, then it must be relative to
        -- the working directory of the running Idris2 instance.
        let pkg_dir_abs = ifThenElse (isRelative pkg_dir) (wdir </> pkg_dir) pkg_dir
        ext <- exts
        pure (pkg_dir_abs </> toPath modIdent <.> ext))
    | _ => logD GotoDefinition "Can't find file for module \{show modIdent}" >> pure Nothing

  let fname_abs_uri = "file://\{fname_abs}"

  -- Escape is needed, filename may contain characters reserved in URI, like whitespace
  let Right uri = escapeAndParseURI fname_abs_uri
    | Left err => do logE GotoDefinition "URI parse error: \{err} \{show (fname_abs_uri, sline, scol)}"
                     pure Nothing

  pure $ Just $ MkLocation uri (MkRange (MkPosition sline scol) (MkPosition eline ecol))

export
mkLocation : Ref Ctxt Defs
          => Ref LSPConf LSPConfiguration
          => FC -> Core (Maybe Location)
mkLocation (MkFC f s e) = mkLocation' f s e
mkLocation (MkVirtualFC f s e) = mkLocation' f s e
mkLocation _ = pure Nothing

export
gotoDefinition : Ref Ctxt Defs
              => Ref MD Metadata
              => Ref LSPConf LSPConfiguration
              => DefinitionParams -> Core (Maybe Location)
gotoDefinition params = do
  logI GotoDefinition "Checking for \{show params.textDocument.uri} at \{show params.position}"
  -- Check actual doc
  Just (actualUri, _) <- gets LSPConf openFile
    | Nothing => logE GotoDefinition "No open file" >> pure Nothing
  let True = actualUri == params.textDocument.uri
      | False => do
          logD GotoDefinition "Expected request for the currently opened file \{show actualUri}, instead received \{show params.textDocument.uri}"
          pure Nothing

  let line = params.position.line
  let col  = params.position.character

  nameLocs <- gets MD nameLocMap
  let Just (_, name) = findPointInTreeLoc (line, col) nameLocs
    | Nothing => logD GotoDefinition "No name found at \{show line}:\{show col}}" >> pure Nothing
  logI GotoDefinition "Found name \{show name}"

  Nothing <- findTypeAt $ anyWithName name $ within (line, col)
    | Just _ => logD GotoDefinition "\{show name} is a local name" >> pure Nothing

  context <- gets Ctxt gamma
  Just globalDef <- lookupCtxtExact name context
    | Nothing => logD GotoDefinition "\{show name} is not in the global context" >> pure Nothing
  logI GotoDefinition "Found definition of \{show name}"

  mkLocation globalDef.location


text:
module CertTest

import Network.TLS.Certificate.System
import Network.TLS.Certificate
import Control.Monad.Error.Either

export
test_cert : EitherT String IO ()
test_cert = do
  certs <- MkEitherT get_system_trusted_certs
  putStrLn "\{show (length certs)} certificates found"


text:
module Test.Spec

import Specdris.Spec

export

specSuite : IO ()
specSuite = spec $ do
  describe "something trivial" $
    it "should add two numbers correctly" $
      14 + 3 `shouldBe` 17

max_stars_repo_name: vmchale/project-init

max_issues_repo_name: vmchale/project-init

max_forks_repo_name: vmchale/project-init


text:
module Core.CaseTree

import Core.TT

import Data.Bool
import Data.List

import Libraries.Data.NameMap
import Libraries.Text.PrettyPrint.Prettyprinter

%default covering

mutual
  ||| Case trees in A-normal forms
  ||| i.e. we may only dispatch on variables, not expressions
  public export
  data CaseTree : List Name -> Type where
       ||| case x return scTy of { p1 => e1 ; ... }
       Case : {name : _} ->
              (idx : Nat) ->
              (0 p : IsVar name idx vars) ->
              (scTy : Term vars) -> List (CaseAlt vars) ->
              CaseTree vars
       ||| RHS: no need for further inspection
       ||| The Int is a clause id that allows us to see which of the
       ||| initial clauses are reached in the tree
       STerm : Int -> Term vars -> CaseTree vars
       ||| error from a partial match
       Unmatched : (msg : String) -> CaseTree vars
       ||| Absurd context
       Impossible : CaseTree vars

  ||| Case alternatives. Unlike arbitrary patterns, they can be at most
  ||| one constructor deep.
  public export
  data CaseAlt : List Name -> Type where
       ||| Constructor for a data type; bind the arguments and subterms.
       ConCase : Name -> (tag : Int) -> (args : List Name) ->
                 CaseTree (args ++ vars) -> CaseAlt vars
       ||| Lazy match for the Delay type use for codata types
       DelayCase : (ty : Name) -> (arg : Name) ->
                   CaseTree (ty :: arg :: vars) -> CaseAlt vars
       ||| Match against a literal
       ConstCase : Constant -> CaseTree vars -> CaseAlt vars
       ||| Catch-all case
       DefaultCase : CaseTree vars -> CaseAlt vars

mutual
  public export
  measure : CaseTree vars -> Nat
  measure (Case idx p scTy xs) = sum $ measureAlts <$> xs
  measure (STerm x y) = 0
  measure (Unmatched msg) = 0
  measure Impossible = 0

  measureAlts : CaseAlt vars -> Nat
  measureAlts (ConCase x tag args y) = 1 + (measure y)
  measureAlts (DelayCase ty arg x) = 1 + (measure x)
  measureAlts (ConstCase x y) = 1 + (measure y)
  measureAlts (DefaultCase x) = 1 + (measure x)

export
isDefault : CaseAlt vars -> Bool
isDefault (DefaultCase _) = True
isDefault _ = False

mutual
  export
  StripNamespace (CaseTree vars) where
    trimNS ns (Case idx p scTy xs)
        = Case idx p (trimNS ns scTy) (map (trimNS ns) xs)
    trimNS ns (STerm x t) = STerm x (trimNS ns t)
    trimNS ns c = c

    restoreNS ns (Case idx p scTy xs)
        = Case idx p (restoreNS ns scTy) (map (restoreNS ns) xs)
    restoreNS ns (STerm x t) = STerm x (restoreNS ns t)
    restoreNS ns c = c

  export
  StripNamespace (CaseAlt vars) where
    trimNS ns (ConCase x tag args t) = ConCase x tag args (trimNS ns t)
    trimNS ns (DelayCase ty arg t) = DelayCase ty arg (trimNS ns t)
    trimNS ns (ConstCase x t) = ConstCase x (trimNS ns t)
    trimNS ns (DefaultCase t) = DefaultCase (trimNS ns t)

    restoreNS ns (ConCase x tag args t) = ConCase x tag args (restoreNS ns t)
    restoreNS ns (DelayCase ty arg t) = DelayCase ty arg (restoreNS ns t)
    restoreNS ns (ConstCase x t) = ConstCase x (restoreNS ns t)
    restoreNS ns (DefaultCase t) = DefaultCase (restoreNS ns t)

public export
data Pat : Type where
     PAs : FC -> Name -> Pat -> Pat
     PCon : FC -> Name -> (tag : Int) -> (arity : Nat) ->
            List Pat -> Pat
     PTyCon : FC -> Name -> (arity : Nat) -> List Pat -> Pat
     PConst : FC -> (c : Constant) -> Pat
     PArrow : FC -> (x : Name) -> Pat -> Pat -> Pat
     PDelay : FC -> LazyReason -> Pat -> Pat -> Pat
     -- TODO: Matching on lazy types
     PLoc : FC -> Name -> Pat
     PUnmatchable : FC -> Term [] -> Pat

export
isPConst : Pat -> Maybe Constant
isPConst (PConst _ c) = Just c
isPConst _ = Nothing

showCT : {vars : _} -> (indent : String) -> CaseTree vars -> String
showCA : {vars : _} -> (indent : String) -> CaseAlt vars  -> String

showCT indent (Case {name} idx prf ty alts)
  = "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of"
  ++ "\n" ++ indent ++ " { "
  ++ showSep ("\n" ++ indent ++ " | ")
             (assert_total (map (showCA ("  " ++ indent)) alts))
  ++ "\n" ++ indent ++ " }"
showCT indent (STerm i tm) = "[" ++ show i ++ "] " ++ show tm
showCT indent (Unmatched msg) = "Error: " ++ show msg
showCT indent Impossible = "Impossible"

showCA indent (ConCase n tag args sc)
        = showSep " " (map show (n :: args)) ++ " => " ++
          showCT indent sc
showCA indent (DelayCase _ arg sc)
        = "Delay " ++ show arg ++ " => " ++ showCT indent sc
showCA indent (ConstCase c sc)
        = "Constant " ++ show c ++ " => " ++ showCT indent sc
showCA indent (DefaultCase sc)
        = "_ => " ++ showCT indent sc

export
{vars : _} -> Show (CaseTree vars) where
  show = showCT ""

export
{vars : _} -> Show (CaseAlt vars) where
  show = showCA ""

mutual
  export
  {vars : _} -> Pretty (CaseTree vars) where
    pretty (Case {name} idx prf ty alts)
      = "case" <++> pretty name <++> ":" <++> pretty ty <++> "of"
         <+> nest 2 (hardline
         <+> vsep (assert_total (map pretty alts)))
    pretty (STerm i tm) = pretty tm
    pretty (Unmatched msg) = pretty "Error:" <++> pretty msg
    pretty Impossible = pretty "Impossible"

  export
  {vars : _} -> Pretty (CaseAlt vars) where
    pretty (ConCase n tag args sc)
      = hsep (map pretty (n :: args)) <++> pretty "=>"
        <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))
    pretty (DelayCase _ arg sc) =
        pretty "Delay" <++> pretty arg <++> pretty "=>"
        <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))
    pretty (ConstCase c sc) =
        pretty c <++> pretty "=>"
        <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))
    pretty (DefaultCase sc) =
        pretty "_ =>"
        <+> Union (spaces 1 <+> pretty sc) (nest 2 (hardline <+> pretty sc))

mutual
  export
  eqTree : CaseTree vs -> CaseTree vs' -> Bool
  eqTree (Case i _ _ alts) (Case i' _ _ alts')
      = i == i'
       && length alts == length alts'
       && all (uncurry eqAlt) (zip alts alts')
  eqTree (STerm _ t) (STerm _ t') = eqTerm t t'
  eqTree (Unmatched _) (Unmatched _) = True
  eqTree Impossible Impossible = True
  eqTree _ _ = False

  eqAlt : CaseAlt vs -> CaseAlt vs' -> Bool
  eqAlt (ConCase n t args tree) (ConCase n' t' args' tree')
      = n == n' && eqTree tree tree' -- assume arities match, since name does
  eqAlt (DelayCase _ _ tree) (DelayCase _ _ tree')
      = eqTree tree tree'
  eqAlt (ConstCase c tree) (ConstCase c' tree')
      = c == c' && eqTree tree tree'
  eqAlt (DefaultCase tree) (DefaultCase tree')
      = eqTree tree tree'
  eqAlt _ _ = False

export
Show Pat where
  show (PAs _ n p) = show n ++ "@(" ++ show p ++ ")"
  show (PCon _ n i _ args) = show n ++ " " ++ show i ++ " " ++ assert_total (show args)
  show (PTyCon _ n _ args) = "<TyCon>" ++ show n ++ " " ++ assert_total (show args)
  show (PConst _ c) = show c
  show (PArrow _ x s t) = "(" ++ show s ++ " -> " ++ show t ++ ")"
  show (PDelay _ _ _ p) = "(Delay " ++ show p ++ ")"
  show (PLoc _ n) = show n
  show (PUnmatchable _ tm) = ".(" ++ show tm ++ ")"

export
Pretty Pat where
  prettyPrec d (PAs _ n p) = pretty n <++> pretty "@" <+> parens (pretty p)
  prettyPrec d (PCon _ n _ _ args) =
    parenthesise (d > Open) $ hsep (pretty n :: map (prettyPrec App) args)
  prettyPrec d (PTyCon _ n _ args) =
    parenthesise (d > Open) $ hsep (pretty n :: map (prettyPrec App) args)
  prettyPrec d (PConst _ c) = pretty c
  prettyPrec d (PArrow _ _ p q) =
    parenthesise (d > Open) $ pretty p <++> pretty "->" <++> pretty q
  prettyPrec d (PDelay _ _ _ p) = parens (pretty "Delay" <++> pretty p)
  prettyPrec d (PLoc _ n) = pretty n
  prettyPrec d (PUnmatchable _ tm) = pretty "." <+> parens (pretty tm)

mutual
  insertCaseNames : SizeOf outer ->
                    SizeOf ns ->
                    CaseTree (outer ++ inner) ->
                    CaseTree (outer ++ (ns ++ inner))
  insertCaseNames outer ns (Case idx prf scTy alts)
      = let MkNVar prf' = insertNVarNames outer ns (MkNVar prf) in
            Case _ prf' (insertNames outer ns scTy)
                (map (insertCaseAltNames outer ns) alts)
  insertCaseNames outer ns (STerm i x) = STerm i (insertNames outer ns x)
  insertCaseNames _ _ (Unmatched msg) = Unmatched msg
  insertCaseNames _ _ Impossible = Impossible

  insertCaseAltNames : SizeOf outer ->
                       SizeOf ns ->
                       CaseAlt (outer ++ inner) ->
                       CaseAlt (outer ++ (ns ++ inner))
  insertCaseAltNames p q (ConCase x tag args ct)
      = ConCase x tag args
           (rewrite appendAssociative args outer (ns ++ inner) in
                    insertCaseNames (mkSizeOf args + p) q {inner}
                        (rewrite sym (appendAssociative args outer inner) in
                                 ct))
  insertCaseAltNames outer ns (DelayCase tyn valn ct)
      = DelayCase tyn valn
                  (insertCaseNames (suc (suc outer)) ns ct)
  insertCaseAltNames outer ns (ConstCase x ct)
      = ConstCase x (insertCaseNames outer ns ct)
  insertCaseAltNames outer ns (DefaultCase ct)
      = DefaultCase (insertCaseNames outer ns ct)

export
Weaken CaseTree where
  weakenNs ns t = insertCaseNames zero ns t

total
getNames : (forall vs . NameMap Bool -> Term vs -> NameMap Bool) ->
           NameMap Bool -> CaseTree vars -> NameMap Bool
getNames add ns sc = getSet ns sc
  where
    mutual
      getAltSet : NameMap Bool -> CaseAlt vs -> NameMap Bool
      getAltSet ns (ConCase n t args sc) = getSet ns sc
      getAltSet ns (DelayCase t a sc) = getSet ns sc
      getAltSet ns (ConstCase i sc) = getSet ns sc
      getAltSet ns (DefaultCase sc) = getSet ns sc

      getAltSets : NameMap Bool -> List (CaseAlt vs) -> NameMap Bool
      getAltSets ns [] = ns
      getAltSets ns (a :: as) = getAltSets (getAltSet ns a) as

      getSet : NameMap Bool -> CaseTree vs -> NameMap Bool
      getSet ns (Case _ x ty xs) = getAltSets ns xs
      getSet ns (STerm i tm) = add ns tm
      getSet ns (Unmatched msg) = ns
      getSet ns Impossible = ns

export
getRefs : (aTotal : Name) -> CaseTree vars -> NameMap Bool
getRefs at = getNames (addRefs False at) empty

export
addRefs : (aTotal : Name) -> NameMap Bool -> CaseTree vars -> NameMap Bool
addRefs at ns = getNames (addRefs False at) ns

export
getMetas : CaseTree vars -> NameMap Bool
getMetas = getNames addMetas empty

export
mkTerm : (vars : List Name) -> Pat -> Term vars
mkTerm vars (PAs fc x y) = mkTerm vars y
mkTerm vars (PCon fc x tag arity xs)
    = apply fc (Ref fc (DataCon tag arity) x)
               (map (mkTerm vars) xs)
mkTerm vars (PTyCon fc x arity xs)
    = apply fc (Ref fc (TyCon 0 arity) x)
               (map (mkTerm vars) xs)
mkTerm vars (PConst fc c) = PrimVal fc c
mkTerm vars (PArrow fc x s t)
    = Bind fc x (Pi fc top Explicit (mkTerm vars s)) (mkTerm (x :: vars) t)
mkTerm vars (PDelay fc r ty p)
    = TDelay fc r (mkTerm vars ty) (mkTerm vars p)
mkTerm vars (PLoc fc n)
    = case isVar n vars of
           Just (MkVar prf) => Local fc Nothing _ prf
           _ => Ref fc Bound n
mkTerm vars (PUnmatchable fc tm) = embed tm


text:
foo : Int -> Int -> Int
foo x x = x + x


text:
module IdrisNet.UDP.UDPClient
-- UDPClient: basically the same as UDPClient but without the need to bind
import Effects
import IdrisNet.Packet
import IdrisNet.PacketLang
import Network.Socket
import IdrisNet.UDP.UDPCommon

%access public

data UDPClient : Effect where
  UDPWriteString :  SocketAddress ->
                    Port ->
                    String ->
                    { () }
                    UDPClient (UDPRes ByteLength)

  UDPReadString :   ByteLength ->
                    { () }
                    UDPClient (UDPRes (UDPAddrInfo, String, ByteLength))

  UDPWritePacket :  SocketAddress ->
                    Port ->
                    (pl : PacketLang) ->
                    (mkTy pl) ->
                    { () }
                    UDPClient (UDPRes ByteLength)

  UDPReadPacket : (pl : PacketLang) ->
                   Length -> -- As with other occurrences, ideally this would go
                   { () }
                   UDPClient (UDPRes (UDPAddrInfo, Maybe (mkTy pl, ByteLength)))

UDPCLIENT : EFFECT
UDPCLIENT = MkEff () UDPClient

-- Writes a string to the given remote host
udpWriteString : SocketAddress -> Port -> String ->
                 { [UDPCLIENT] }
                 Eff (UDPRes ByteLength)
udpWriteString sa p s = call (UDPWriteString sa p s)

-- Reads a string, returning the address, data, and length
udpReadString : ByteLength ->
                { [UDPCLIENT] }
                Eff (UDPRes (UDPAddrInfo, String, ByteLength))
udpReadString len = call (UDPReadString len)

-- Writes a packet to the given remote host
udpWritePacket : SocketAddress ->
                 Port ->
                 (pl : PacketLang) ->
                 (mkTy pl) ->
                 { [UDPCLIENT] }
                 Eff (UDPRes ByteLength)
udpWritePacket sa p pl pckt = call (UDPWritePacket sa p pl pckt)

-- Reads a packet from the givem remote host
udpReadPacket : (pl : PacketLang) ->
                Length ->
                { [UDPCLIENT] }
                Eff (UDPRes (UDPAddrInfo, Maybe (mkTy pl, ByteLength)))
udpReadPacket pl len = call (UDPReadPacket pl len)

-- Saves us repeating ourselves in the handler...
withSocket : (a : Type) ->
             (Socket -> IO (UDPRes a)) -> -- socket function
             IO (UDPRes a)
withSocket _ fn = do
  sock_res <- socket AF_INET Datagram 0
  case sock_res of
    Left err => return (UDPFailure err)
    Right sock => fn sock

instance Handler UDPClient IO where
  handle () (UDPWriteString sa p str) k = do
    res <- withSocket ByteLength (\sock => do
      send_res <- sendTo sock sa p str
      case send_res of
        Left err =>
          if err == EAGAIN then
            return $ UDPRecoverableError err
          else
            return $ UDPFailure err
        Right bl => return $ UDPSuccess bl)
    k res ()

  handle () (UDPReadString bl) k = do
    res <- withSocket (UDPAddrInfo, String, ByteLength) (\sock => do
      recv_res <- recvFrom sock bl
      case recv_res of
        Left err =>
          if err == EAGAIN then
            return (UDPRecoverableError err)
          else return (UDPFailure err)
        Right (addr, str, bl) => return $ UDPSuccess (addr, str, bl))
    k res ()

  handle () (UDPWritePacket sa p pl dat) k = do
    res <- withSocket ByteLength (\sock => do
      (pckt, len) <- marshal pl dat
      send_res <- sendToBuf sock sa p pckt len
      case send_res of
           Left err =>
            if err == EAGAIN then
              return (UDPRecoverableError err)
            else
              return (UDPFailure err)
           Right bl => return (UDPSuccess bl))
    k res ()

  handle () (UDPReadPacket pl len) k = do
    res <- withSocket (UDPAddrInfo, Maybe (mkTy pl, Length)) (\sock => do
      ptr <- sock_alloc len
      recv_res <- recvFromBuf sock ptr len
      case recv_res of
           Left err =>
             if err == EAGAIN then
               return (UDPRecoverableError err)
             else
               return (UDPFailure err)
           Right (addr, bl) => do
             res <- unmarshal pl ptr bl
             sock_free ptr
             -- The UDPSuccess depends on the actual network-y
             -- part, not the unmarshalling. If the unmarshalling fails,
             -- we still keep the connection open.
             return (UDPSuccess (addr, res) ))
    k res ()


text:
module EquivOptimize0Plus

import Equiv
import Expr
import Logic
import Imp
import Maps

%access public export

%default total

optimize_0plus_aexp : AExp -> AExp
optimize_0plus_aexp (ANum n) = ANum n
optimize_0plus_aexp (AId x) = AId x
optimize_0plus_aexp (APlus (ANum Z) y) = optimize_0plus_aexp y
optimize_0plus_aexp (APlus x y) = APlus (optimize_0plus_aexp x)
                                        (optimize_0plus_aexp y)
optimize_0plus_aexp (AMinus x y) = AMinus (optimize_0plus_aexp x)
                                          (optimize_0plus_aexp y)
optimize_0plus_aexp (AMult x y) = AMult (optimize_0plus_aexp x)
                                        (optimize_0plus_aexp y)

optimize_0plus_bexp : BExp -> BExp
optimize_0plus_bexp BTrue = BTrue
optimize_0plus_bexp BFalse = BFalse
optimize_0plus_bexp (BEq a1 a2) =
  case (optimize_0plus_aexp a1, optimize_0plus_aexp a2) of
    (ANum n1, ANum n2) => if n1 == n2
                             then BTrue
                             else BFalse
    (e1, e2) => BEq e1 e2
optimize_0plus_bexp (BLe a1 a2) =
  case (optimize_0plus_aexp a1, optimize_0plus_aexp a2) of
    (ANum n1, ANum n2) => if lte n1 n2
                             then BTrue
                             else BFalse
    (e1, e2) => BLe e1 e2
optimize_0plus_bexp (BNot b) = case optimize_0plus_bexp b of
  BTrue => BFalse
  BFalse => BTrue
  e => BNot e
optimize_0plus_bexp (BAnd b1 b2) =
  case (optimize_0plus_bexp b1, optimize_0plus_bexp b2) of
    (BTrue, e2) => e2
    (BFalse, _) => BFalse
    (e1, e2) => BAnd e1 e2

optimize_0plus_com : Com -> Com
optimize_0plus_com CSkip = CSkip
optimize_0plus_com (CAss x e) = CAss x (optimize_0plus_aexp e)
optimize_0plus_com (CSeq c1 c2) = CSeq (optimize_0plus_com c1)
                                       (optimize_0plus_com c2)
optimize_0plus_com (CIf b ct cf) = case optimize_0plus_bexp b of
  BTrue => optimize_0plus_com ct
  BFalse => optimize_0plus_com cf
  e => CIf e (optimize_0plus_com ct) (optimize_0plus_com cf)
optimize_0plus_com (CIf1 b c) = case optimize_0plus_bexp b of
  BTrue => optimize_0plus_com c
  BFalse => SKIP
  e => CIf1 e (optimize_0plus_com c)
optimize_0plus_com (CWhile b c) = case optimize_0plus_bexp b of
  BTrue => CWhile BTrue CSkip
  BFalse => CSkip
  e => CWhile e (optimize_0plus_com c)
optimize_0plus_com (CFor init cond updt body) = case optimize_0plus_bexp cond of
  BTrue => CSeq (optimize_0plus_com init) (CWhile BTrue SKIP)
  BFalse => optimize_0plus_com init
  e => CFor (optimize_0plus_com init)
            e
            (optimize_0plus_com updt)
            (optimize_0plus_com body)
optimize_0plus_com (CRepeat body cond) = case optimize_0plus_bexp cond of
  BTrue => optimize_0plus_com body
  BFalse => CSeq (optimize_0plus_com body) (CWhile BTrue SKIP)
  e => CRepeat (optimize_0plus_com body) e

optimize_0plus_aexp_sound : ATransSound EquivOptimize0Plus.optimize_0plus_aexp
optimize_0plus_aexp_sound {a = ANum _} _ = Refl
optimize_0plus_aexp_sound {a = AId _} _ = Refl
optimize_0plus_aexp_sound {a = APlus (ANum Z) a2} st =
  optimize_0plus_aexp_sound a2 st
optimize_0plus_aexp_sound {a = APlus (ANum (S _)) a2} st =
  rewrite optimize_0plus_aexp_sound a2 st
  in Refl
optimize_0plus_aexp_sound {a = APlus (AId _) a2} st =
  rewrite optimize_0plus_aexp_sound a2 st
  in Refl
optimize_0plus_aexp_sound {a = APlus a1@(APlus _ _) a2} st =
  rewrite optimize_0plus_aexp_sound a1 st
  in rewrite optimize_0plus_aexp_sound a2 st
  in Refl
optimize_0plus_aexp_sound {a = APlus a1@(AMinus _ _) a2} st =
  rewrite optimize_0plus_aexp_sound a1 st
  in rewrite optimize_0plus_aexp_sound a2 st
  in Refl
optimize_0plus_aexp_sound {a = APlus a1@(AMult _ _) a2} st =
  rewrite optimize_0plus_aexp_sound a1 st
  in rewrite optimize_0plus_aexp_sound a2 st
  in Refl
optimize_0plus_aexp_sound {a = AMinus a1 a2} st =
  rewrite optimize_0plus_aexp_sound a1 st
  in rewrite optimize_0plus_aexp_sound a2 st
  in Refl
optimize_0plus_aexp_sound {a = AMult a1 a2} st =
  rewrite optimize_0plus_aexp_sound a1 st
  in rewrite optimize_0plus_aexp_sound a2 st
  in Refl

optimize_0plus_bexp_sound : BTransSound EquivOptimize0Plus.optimize_0plus_bexp
optimize_0plus_bexp_sound {b = BTrue} _ = Refl
optimize_0plus_bexp_sound {b = BFalse} _ = Refl
optimize_0plus_bexp_sound {b = BEq a1 a2} st
  with (optimize_0plus_aexp a1) proof a1prf
    optimize_0plus_bexp_sound {b = BEq a1 a2} st | ANum k
      with (optimize_0plus_aexp a2) proof a2prf
        optimize_0plus_bexp_sound {b = BEq a1 a2} st | ANum k | ANum j
          with (k == j) proof eprf
            optimize_0plus_bexp_sound {b = BEq a1 a2} st
            | ANum k | ANum j | False =
              rewrite optimize_0plus_aexp_sound a1 st
              in rewrite sym a1prf
              in rewrite optimize_0plus_aexp_sound a2 st
              in rewrite sym a2prf
              in sym eprf
            optimize_0plus_bexp_sound {b = BEq a1 a2} st
            | ANum k | ANum j | True =
              rewrite optimize_0plus_aexp_sound a1 st
              in rewrite sym a1prf
              in rewrite optimize_0plus_aexp_sound a2 st
              in rewrite sym a2prf
              in sym eprf
        optimize_0plus_bexp_sound {b = BEq a1 a2} st | ANum _ | AId _ =
          rewrite optimize_0plus_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite optimize_0plus_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        optimize_0plus_bexp_sound {b = BEq a1 a2} st | ANum _ | APlus _ _ =
          rewrite optimize_0plus_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite optimize_0plus_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        optimize_0plus_bexp_sound {b = BEq a1 a2} st | ANum _ | AMinus _ _ =
          rewrite optimize_0plus_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite optimize_0plus_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        optimize_0plus_bexp_sound {b = BEq a1 a2} st | ANum _ | AMult _ _ =
          rewrite optimize_0plus_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite optimize_0plus_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
    optimize_0plus_bexp_sound {b = BEq a1 a2} st | AId _ =
      rewrite optimize_0plus_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite optimize_0plus_aexp_sound a2 st
      in Refl
    optimize_0plus_bexp_sound {b = BEq a1 a2} st | APlus _ _ =
      rewrite optimize_0plus_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite optimize_0plus_aexp_sound a2 st
      in Refl
    optimize_0plus_bexp_sound {b = BEq a1 a2} st | AMinus _ _ =
      rewrite optimize_0plus_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite optimize_0plus_aexp_sound a2 st
      in Refl
    optimize_0plus_bexp_sound {b = BEq a1 a2} st | AMult _ _ =
      rewrite optimize_0plus_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite optimize_0plus_aexp_sound a2 st
      in Refl
optimize_0plus_bexp_sound {b = BLe a1 a2} st
  with (optimize_0plus_aexp a1) proof a1prf
    optimize_0plus_bexp_sound {b = BLe a1 a2} st | ANum k
      with (optimize_0plus_aexp a2) proof a2prf
        optimize_0plus_bexp_sound {b = BLe a1 a2} st | ANum k | ANum j
          with (lte k j) proof eprf
            optimize_0plus_bexp_sound {b = BLe a1 a2} st
            | ANum k | ANum j | False =
              rewrite optimize_0plus_aexp_sound a1 st
              in rewrite sym a1prf
              in rewrite optimize_0plus_aexp_sound a2 st
              in rewrite sym a2prf
              in sym eprf
            optimize_0plus_bexp_sound {b = BLe a1 a2} st
            | ANum k | ANum j | True =
              rewrite optimize_0plus_aexp_sound a1 st
              in rewrite sym a1prf
              in rewrite optimize_0plus_aexp_sound a2 st
              in rewrite sym a2prf
              in sym eprf
        optimize_0plus_bexp_sound {b = BLe a1 a2} st | ANum _ | AId _ =
          rewrite optimize_0plus_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite optimize_0plus_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        optimize_0plus_bexp_sound {b = BLe a1 a2} st | ANum _ | APlus _ _ =
          rewrite optimize_0plus_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite optimize_0plus_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        optimize_0plus_bexp_sound {b = BLe a1 a2} st | ANum _ | AMinus _ _ =
          rewrite optimize_0plus_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite optimize_0plus_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
        optimize_0plus_bexp_sound {b = BLe a1 a2} st | ANum _ | AMult _ _ =
          rewrite optimize_0plus_aexp_sound a1 st
          in rewrite sym a1prf
          in rewrite optimize_0plus_aexp_sound a2 st
          in rewrite sym a2prf
          in Refl
    optimize_0plus_bexp_sound {b = BLe a1 a2} st | AId _ =
      rewrite optimize_0plus_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite optimize_0plus_aexp_sound a2 st
      in Refl
    optimize_0plus_bexp_sound {b = BLe a1 a2} st | APlus _ _ =
      rewrite optimize_0plus_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite optimize_0plus_aexp_sound a2 st
      in Refl
    optimize_0plus_bexp_sound {b = BLe a1 a2} st | AMinus _ _ =
      rewrite optimize_0plus_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite optimize_0plus_aexp_sound a2 st
      in Refl
    optimize_0plus_bexp_sound {b = BLe a1 a2} st | AMult _ _ =
      rewrite optimize_0plus_aexp_sound a1 st
      in rewrite sym a1prf
      in rewrite optimize_0plus_aexp_sound a2 st
      in Refl
optimize_0plus_bexp_sound {b = BNot b} st
  with (optimize_0plus_bexp b) proof bprf
    optimize_0plus_bexp_sound {b = BNot b} st | BTrue =
      rewrite optimize_0plus_bexp_sound b st
      in rewrite sym bprf
      in Refl
    optimize_0plus_bexp_sound {b = BNot b} st | BFalse =
      rewrite optimize_0plus_bexp_sound b st
      in rewrite sym bprf
      in Refl
    optimize_0plus_bexp_sound {b = BNot b} st | BEq _ _ =
      rewrite optimize_0plus_bexp_sound b st
      in rewrite sym bprf
      in Refl
    optimize_0plus_bexp_sound {b = BNot b} st | BLe _ _ =
      rewrite optimize_0plus_bexp_sound b st
      in rewrite sym bprf
      in Refl
    optimize_0plus_bexp_sound {b = BNot b} st | BNot _ =
      rewrite optimize_0plus_bexp_sound b st
      in rewrite sym bprf
      in Refl
    optimize_0plus_bexp_sound {b = BNot b} st | BAnd _ _ =
      rewrite optimize_0plus_bexp_sound b st
      in rewrite sym bprf
      in Refl
optimize_0plus_bexp_sound {b = BAnd b1 b2} st
  with (optimize_0plus_bexp b1) proof b1prf
    optimize_0plus_bexp_sound {b = BAnd b1 b2} st | BTrue =
      rewrite optimize_0plus_bexp_sound b1 st
      in rewrite sym b1prf
      in rewrite optimize_0plus_bexp_sound b2 st
      in Refl
    optimize_0plus_bexp_sound {b = BAnd b1 b2} st | BFalse =
      rewrite optimize_0plus_bexp_sound b1 st
      in rewrite sym b1prf
      in Refl
    optimize_0plus_bexp_sound {b = BAnd b1 b2} st | BEq _ _ =
      rewrite optimize_0plus_bexp_sound b1 st
      in rewrite sym b1prf
      in rewrite optimize_0plus_bexp_sound b2 st
      in Refl
    optimize_0plus_bexp_sound {b = BAnd b1 b2} st | BLe _ _ =
      rewrite optimize_0plus_bexp_sound b1 st
      in rewrite sym b1prf
      in rewrite optimize_0plus_bexp_sound b2 st
      in Refl
    optimize_0plus_bexp_sound {b = BAnd b1 b2} st | BNot _ =
      rewrite optimize_0plus_bexp_sound b1 st
      in rewrite sym b1prf
      in rewrite optimize_0plus_bexp_sound b2 st
      in Refl
    optimize_0plus_bexp_sound {b = BAnd b1 b2} st | BAnd _ _ =
      rewrite optimize_0plus_bexp_sound b1 st
      in rewrite sym b1prf
      in rewrite optimize_0plus_bexp_sound b2 st
      in Refl

optimize_0plus_com_sound : CTransSound EquivOptimize0Plus.optimize_0plus_com
optimize_0plus_com_sound {c = CSkip} st st' = refl_cequiv {c=CSkip} st st'
optimize_0plus_com_sound {c = (CAss _ e)} st st' =
  let c_equiv = cAss_congruence (optimize_0plus_aexp_sound e)
  in c_equiv st st'
optimize_0plus_com_sound {c = (CSeq c1 c2)} st st' =
  let c_equiv = cSeq_congruence (optimize_0plus_com_sound c1)
                                (optimize_0plus_com_sound c2)
  in c_equiv st st'
optimize_0plus_com_sound {c = (CIf b ct cf)} st st'
  with (optimize_0plus_bexp b) proof bprf
    optimize_0plus_com_sound {c = (CIf b ct cf)} st st' | BTrue =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
      in trans_cequiv (test_true b_equiv) (optimize_0plus_com_sound ct) st st'
    optimize_0plus_com_sound {c = (CIf b ct cf)} st st' | BFalse =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
      in trans_cequiv (test_false b_equiv) (optimize_0plus_com_sound cf) st st'
    optimize_0plus_com_sound {c = (CIf b ct cf)} st st' | BEq _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
          ct_equiv = optimize_0plus_com_sound ct
          cf_equiv = optimize_0plus_com_sound cf
          if_equiv = cIf_congruence b_equiv ct_equiv cf_equiv
      in if_equiv st st'
    optimize_0plus_com_sound {c = (CIf b ct cf)} st st' | BLe _ _ =
      let b_equiv = \st1 =>
            replace {P=\x => beval st1 b = beval st1 x}
                    (sym bprf) (optimize_0plus_bexp_sound b st1)
          ct_equiv = optimize_0plus_com_sound ct
          cf_equiv = optimize_0plus_com_sound cf
          if_equiv = cIf_congruence b_equiv ct_equiv cf_equiv
      in if_equiv st st'
    optimize_0plus_com_sound {c = (CIf b ct cf)} st st' | BNot _ =
      let b_equiv = \st1 =>
            replace {P=\x => beval st1 b = beval st1 x}
                    (sym bprf) (optimize_0plus_bexp_sound b st1)
          ct_equiv = optimize_0plus_com_sound ct
          cf_equiv = optimize_0plus_com_sound cf
          if_equiv = cIf_congruence b_equiv ct_equiv cf_equiv
      in if_equiv st st'
    optimize_0plus_com_sound {c = (CIf b ct cf)} st st' | BAnd _ _ =
      let b_equiv = \st1 =>
            replace {P=\x => beval st1 b = beval st1 x}
                    (sym bprf) (optimize_0plus_bexp_sound b st1)
          ct_equiv = optimize_0plus_com_sound ct
          cf_equiv = optimize_0plus_com_sound cf
          if_equiv = cIf_congruence b_equiv ct_equiv cf_equiv
      in if_equiv st st'
optimize_0plus_com_sound {c = (CIf1 b c)} st st'
  with (optimize_0plus_bexp b) proof bprf
    optimize_0plus_com_sound {c = (CIf1 b c)} st st' | BTrue =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
      in trans_cequiv (if1_true b_equiv) (optimize_0plus_com_sound c) st st'
    optimize_0plus_com_sound {c = (CIf1 b c)} st st' | BFalse =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
      in if1_false b_equiv st st'
    optimize_0plus_com_sound {c = (CIf1 b c)} st st' | BEq _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
          cif1_equiv = cIf1_congruence b_equiv (optimize_0plus_com_sound c)
      in cif1_equiv st st'
    optimize_0plus_com_sound {c = (CIf1 b c)} st st' | BLe _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
          cif1_equiv = cIf1_congruence b_equiv (optimize_0plus_com_sound c)
      in cif1_equiv st st'
    optimize_0plus_com_sound {c = (CIf1 b c)} st st' | BNot _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
          cif1_equiv = cIf1_congruence b_equiv (optimize_0plus_com_sound c)
      in cif1_equiv st st'
    optimize_0plus_com_sound {c = (CIf1 b c)} st st' | BAnd _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
          cif1_equiv = cIf1_congruence b_equiv (optimize_0plus_com_sound c)
      in cif1_equiv st st'
optimize_0plus_com_sound {c = (CWhile b c)} st st'
  with (optimize_0plus_bexp b) proof bprf
    optimize_0plus_com_sound {c = (CWhile b c)} st st' | BTrue =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
      in while_true b_equiv st st'
    optimize_0plus_com_sound {c = (CWhile b c)} st st' | BFalse =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
      in while_false b_equiv st st'
    optimize_0plus_com_sound {c = (CWhile b c)} st st' | BEq _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
          while_equiv = cWhile_congruence b_equiv (optimize_0plus_com_sound c)
      in while_equiv st st'
    optimize_0plus_com_sound {c = (CWhile b c)} st st' | BLe _ _ =
      let b_equiv = \st1 => replace {P=\x => beval st1 b = beval st1 x}
                                    (sym bprf) (optimize_0plus_bexp_sound b st1)
          while_equiv = cWhile_congruence b_equiv (optimize_0plus_com_sound c)
      in while_equiv st st'
    optimize_0plus_com_sound {c = (CWhile b c)} st st' | BNot _ =
      let b_equiv = \st1 =>
                         replace {P=\x => beval st1 b = beval st1 x}
                                 (sym bprf) (optimize_0plus_bexp_sound b st1)
          while_equiv = cWhile_congruence b_equiv (optimize_0plus_com_sound c)
      in while_equiv st st'
    optimize_0plus_com_sound {c = (CWhile b c)} st st' | BAnd _ _ =
      let b_equiv = \st1 =>
                         replace {P=\x => beval st1 b = beval st1 x}
                                 (sym bprf) (optimize_0plus_bexp_sound b st1)
          while_equiv = cWhile_congruence b_equiv (optimize_0plus_com_sound c)
      in while_equiv st st'
optimize_0plus_com_sound {c = (CFor init cond updt body)} st st'
  with (optimize_0plus_bexp cond) proof cond_prf
    optimize_0plus_com_sound {c = (CFor init cond updt body)} st st' | BTrue =
      let cond_equiv = \st1 => cong {f=beval st1} (sym cond_prf)
          while_equiv = trans_cequiv
                          (trans_cequiv
                             (cFor_congruence
                                {cond1=optimize_0plus_bexp cond} {cond2=BTrue}
                                refl_cequiv cond_equiv refl_cequiv refl_cequiv)
                             for_while_equiv)
                          (cSeq_congruence (optimize_0plus_com_sound init)
                                           (while_true btrue_is_true))
          equiv = trans_cequiv (cFor_congruence
                                  refl_cequiv
                                  (optimize_0plus_bexp_sound cond)
                                  refl_cequiv
                                refl_cequiv)
                               while_equiv
      in equiv st st'
    optimize_0plus_com_sound {c = (CFor init cond updt body)} st st' | BFalse =
      let cond_equiv = \st1 => cong {f=beval st1} (sym cond_prf)
          while_equiv = trans_cequiv
                          (trans_cequiv
                             (cFor_congruence
                                {cond1=optimize_0plus_bexp cond} {cond2=BFalse}
                                refl_cequiv cond_equiv refl_cequiv refl_cequiv)
                             for_while_equiv)
                          (cSeq_congruence (optimize_0plus_com_sound init)
                                           (while_false bfalse_is_false))
          equiv = trans_cequiv (cFor_congruence
                                  refl_cequiv
                                  (optimize_0plus_bexp_sound cond)
                                  refl_cequiv
                                  refl_cequiv)
                               (trans_cequiv while_equiv skip_right)
      in equiv st st'
    optimize_0plus_com_sound {c = (CFor init cond updt body)} st st' | BEq _ _ =
      let cond_equiv = trans_bequiv (optimize_0plus_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cFor_congruence (optimize_0plus_com_sound init)
                                  cond_equiv
                                  (optimize_0plus_com_sound updt)
                                  (optimize_0plus_com_sound body)
      in equiv st st'
    optimize_0plus_com_sound {c = (CFor init cond updt body)} st st' | BLe _ _ =
      let cond_equiv = trans_bequiv (optimize_0plus_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cFor_congruence (optimize_0plus_com_sound init)
                                  cond_equiv
                                  (optimize_0plus_com_sound updt)
                                  (optimize_0plus_com_sound body)
      in equiv st st'
    optimize_0plus_com_sound {c = (CFor init cond updt body)} st st' | BNot _ =
      let cond_equiv = trans_bequiv (optimize_0plus_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cFor_congruence (optimize_0plus_com_sound init)
                                  cond_equiv
                                  (optimize_0plus_com_sound updt)
                                  (optimize_0plus_com_sound body)
      in equiv st st'
    optimize_0plus_com_sound {c = (CFor init cond updt body)} st st' | BAnd _ _ =
      let cond_equiv = trans_bequiv (optimize_0plus_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cFor_congruence (optimize_0plus_com_sound init)
                                  cond_equiv
                                  (optimize_0plus_com_sound updt)
                                  (optimize_0plus_com_sound body)
      in equiv st st'
optimize_0plus_com_sound {c = (CRepeat body cond)} st st'
  with (optimize_0plus_bexp cond) proof cond_prf
    optimize_0plus_com_sound {c = (CRepeat body cond)} st st' | BTrue =
      let cond_equiv = trans_bequiv
                         (optimize_0plus_bexp_sound cond)
                         (\st1 => cong {f=beval st1} (sym cond_prf))
          while_equiv = trans_cequiv
                          (cRepeat_congruence (optimize_0plus_com_sound body)
                                              cond_equiv)
                          (trans_cequiv
                             repeat_while_equiv
                             (cSeq_congruence
                                refl_cequiv
                                (while_false bnot_btrue_is_bfalse)))
          equiv = trans_cequiv while_equiv skip_right
      in equiv st st'
    optimize_0plus_com_sound {c = (CRepeat body cond)} st st' | BFalse =
      let cond_equiv = trans_bequiv
                         (optimize_0plus_bexp_sound cond)
                         (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = trans_cequiv
                    (cRepeat_congruence (optimize_0plus_com_sound body)
                                        cond_equiv)
                    (trans_cequiv
                       repeat_while_equiv
                       (cSeq_congruence
                          refl_cequiv
                          (while_true bnot_bfalse_is_btrue)))
      in equiv st st'
    optimize_0plus_com_sound {c = (CRepeat body cond)} st st' | BEq _ _ =
      let cond_equiv = trans_bequiv (optimize_0plus_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cRepeat_congruence (optimize_0plus_com_sound body) cond_equiv
      in equiv st st'
    optimize_0plus_com_sound {c = (CRepeat body cond)} st st' | BLe _ _ =
      let cond_equiv = trans_bequiv (optimize_0plus_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cRepeat_congruence (optimize_0plus_com_sound body) cond_equiv
      in equiv st st'
    optimize_0plus_com_sound {c = (CRepeat body cond)} st st' | BNot _ =
      let cond_equiv = trans_bequiv (optimize_0plus_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cRepeat_congruence (optimize_0plus_com_sound body) cond_equiv
      in equiv st st'
    optimize_0plus_com_sound {c = (CRepeat body cond)} st st' | BAnd _ _ =
      let cond_equiv = trans_bequiv (optimize_0plus_bexp_sound cond)
                                    (\st1 => cong {f=beval st1} (sym cond_prf))
          equiv = cRepeat_congruence (optimize_0plus_com_sound body) cond_equiv
      in equiv st st'


text:
module GRIN.Name

import Control.Monad.State
import Data.SortedMap

||| A name and resolved index.
public export
record Resolved a where
    constructor MkResolved
    res : Int
    orig : a

export
Eq (Resolved a) where
    (==) = (==) `on` res

export
Ord (Resolved a) where
    compare = compare `on` res

export
Show a => Show (Resolved a) where
    show = show . orig

||| State for resolving names.
record ResolveState name where
    constructor MkResState
    nextId : Int
    resolved : SortedMap name Int

||| Monad for resolving names.
export
record ResolveM name a where
    constructor MkResolveM
    unResolveM : State (ResolveState name) a

export
runResolveM : Ord name => ResolveM name a -> a
runResolveM = evalState (MkResState 0 empty) . unResolveM

export
Functor (ResolveM name) where
    map f = MkResolveM . map f . unResolveM

export
Applicative (ResolveM name) where
    pure = MkResolveM . pure
    f <*> x = MkResolveM $ unResolveM f <*> unResolveM x

export
Monad (ResolveM name) where
    x >>= f = MkResolveM $ unResolveM x >>= (unResolveM . f)

MonadState (ResolveState name) (ResolveM name) where
    get = MkResolveM get
    put = MkResolveM . put
    state = MkResolveM . state

export
resolve : name -> ResolveM name (Resolved name)
resolve orig = do
    st <- get
    case lookup orig st.resolved of
        Just res => pure $ MkResolved res orig
        Nothing => do
            let res = st.nextId
            put (record { nextId $= (+ 1), resolved $= insert orig res } st)
            pure $ MkResolved res orig