text:
module Interfaces.HeytingAlgebra

import Control.Algebra.Lattice
import Interfaces.Verified

%hide Prelude.Monad.join
%access public export

--------------------------------------------------------------------------------
-- Interfaces
--------------------------------------------------------------------------------

interface (BoundedJoinSemilattice a, BoundedMeetSemilattice a, Ord a) => HeytingAlgebra a where
  not : a -> a
  implies : a -> a -> a

--------------------------------------------------------------------------------
-- Verified Interfaces
--------------------------------------------------------------------------------

interface (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
  boundedJoinSemilatticeIdentity : (x : a) -> join x Control.Algebra.Lattice.bottom = x

interface (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
  boundedMeetSemilatticeIdentity : (x : a) -> meet x Control.Algebra.Lattice.top = x

interface (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where {}

interface Lattice a => VerifiedDistributiveLattice a where
  meetDistributesOverJoin : (x, y, z : a) -> x `meet` (y `join` z) = (x `meet` y) `join` (x `meet` z)

interface (VerifiedLattice a, VerifiedDistributiveLattice a, HeytingAlgebra a) => VerifiedHeytingAlgebra a where
  total heytingAlgebraPseudoComplement : (x : a) -> HeytingAlgebra.not x = x `implies` Control.Algebra.Lattice.bottom
  total heytingAlgebraRelativePseudoComplement : (x, y, z : a) -> (z `meet` x) <= y = z <= (x `implies` y)

interface VerifiedHeytingAlgebra a => VerifiedInvolutiveHeytingAlgebra a where
  heytingAlgebraInvolution : (x : a) -> HeytingAlgebra.not (HeytingAlgebra.not x) = x

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

JoinSemilattice Bool where
  join x y = x || y

BoundedJoinSemilattice Bool where
  bottom = False

MeetSemilattice Bool where
  meet x y = x && y

BoundedMeetSemilattice Bool where
  top = True

Lattice Bool where {}

HeytingAlgebra Bool where
  not = Prelude.Bool.not
  implies x y = (not x) || y

--------------------------------------------------------------------------------
-- Verified Implementations
--------------------------------------------------------------------------------

VerifiedJoinSemilattice Bool where
  joinSemilatticeJoinIsAssociative False False False = Refl
  joinSemilatticeJoinIsAssociative False False True = Refl
  joinSemilatticeJoinIsAssociative False True False = Refl
  joinSemilatticeJoinIsAssociative False True True = Refl
  joinSemilatticeJoinIsAssociative True False False = Refl
  joinSemilatticeJoinIsAssociative True False True = Refl
  joinSemilatticeJoinIsAssociative True True False = Refl
  joinSemilatticeJoinIsAssociative True True True = Refl
  joinSemilatticeJoinIsCommutative False False = Refl
  joinSemilatticeJoinIsCommutative False True = Refl
  joinSemilatticeJoinIsCommutative True False = Refl
  joinSemilatticeJoinIsCommutative True True = Refl
  joinSemilatticeJoinIsIdempotent False = Refl
  joinSemilatticeJoinIsIdempotent True = Refl

VerifiedBoundedJoinSemilattice Bool where
  boundedJoinSemilatticeIdentity False = Refl
  boundedJoinSemilatticeIdentity True = Refl

VerifiedMeetSemilattice Bool where
  meetSemilatticeMeetIsAssociative False False False = Refl
  meetSemilatticeMeetIsAssociative False False True = Refl
  meetSemilatticeMeetIsAssociative False True False = Refl
  meetSemilatticeMeetIsAssociative False True True = Refl
  meetSemilatticeMeetIsAssociative True False False = Refl
  meetSemilatticeMeetIsAssociative True False True = Refl
  meetSemilatticeMeetIsAssociative True True False = Refl
  meetSemilatticeMeetIsAssociative True True True = Refl
  meetSemilatticeMeetIsCommutative False False = Refl
  meetSemilatticeMeetIsCommutative False True = Refl
  meetSemilatticeMeetIsCommutative True False = Refl
  meetSemilatticeMeetIsCommutative True True = Refl
  meetSemilatticeMeetIsIdempotent False = Refl
  meetSemilatticeMeetIsIdempotent True = Refl

VerifiedBoundedMeetSemilattice Bool where
  boundedMeetSemilatticeIdentity False = Refl
  boundedMeetSemilatticeIdentity True = Refl

VerifiedLattice Bool where {}

VerifiedDistributiveLattice Bool where
  meetDistributesOverJoin False False False = Refl
  meetDistributesOverJoin False False True = Refl
  meetDistributesOverJoin False True False = Refl
  meetDistributesOverJoin False True True = Refl
  meetDistributesOverJoin True False False = Refl
  meetDistributesOverJoin True False True = Refl
  meetDistributesOverJoin True True False = Refl
  meetDistributesOverJoin True True True = Refl

VerifiedHeytingAlgebra Bool where
  heytingAlgebraPseudoComplement False = Refl
  heytingAlgebraPseudoComplement True = Refl
  heytingAlgebraRelativePseudoComplement False False False = Refl
  heytingAlgebraRelativePseudoComplement False False True = Refl
  heytingAlgebraRelativePseudoComplement False True False = Refl
  heytingAlgebraRelativePseudoComplement False True True = Refl
  heytingAlgebraRelativePseudoComplement True False False = Refl
  heytingAlgebraRelativePseudoComplement True False True = Refl
  heytingAlgebraRelativePseudoComplement True True False = Refl
  heytingAlgebraRelativePseudoComplement True True True = Refl

VerifiedInvolutiveHeytingAlgebra Bool where
  heytingAlgebraInvolution False = Refl
  heytingAlgebraInvolution True = Refl

max_stars_repo_name: Risto-Stevcev/idris-heyting-algebra

max_issues_repo_name: Risto-Stevcev/idris-heyting-algebra

max_forks_repo_name: Risto-Stevcev/idris-heyting-algebra


text:
module ZipperTraversable

-- Based on http://okmij.org/ftp/continuations/zipper.html#traversable

import Control.Monad.Identity
import src.ContT

data Zipper : (t : Type -> Type) -> (a : Type) -> Type where
  ZDone : t a -> Zipper t a
  Z : a -> (Maybe a -> Zipper t a) -> Zipper t a

makeZipper : Traversable t => t a -> Zipper t a
makeZipper tr = runIdentity . reset $ traverse f tr >>= pure . ZDone
  where
    f : a -> Cont (Zipper t a) a
    f a = shift (\k => pure $ Z a (runIdentity . k . maybe a id))

update : Zipper List Int -> List Int
update (ZDone x) = x
update (Z x f) = update $ f (Just (x + 1))

test : List Int
test = update $ makeZipper [1..10]

ext: idr

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
module Data.InSet

import Data.Bool
import Data.Bool.Xor

import public Data.InSet.Equality

import Decidable.Equality

%default total

---------------------
---------------------
---               ---
---  DEFINITIONS  ---
---               ---
---------------------
---------------------

infix 6 ==
infix 7 `isin`, `notin`
infixl 8 +, -, ^
infixl 9 *, #

-------------------
--- Type itself ---
-------------------

public export
InSet : Type -> Type
InSet a = a -> Bool

-- TODO To think, maybe equality relation should be shown in the `InSet` type as a parameter?
--      However, if this is only in the append operation, this gives an ability to union sets with different equalities.

------------------------------------
--- Intesional test of existence ---
------------------------------------

export
isin : a -> InSet a -> Bool
isin = flip apply

public export %inline
notin : a -> InSet a -> Bool
notin x y = not $ isin x y

----------------
--- Creation ---
----------------

--- Syntax for list-like literals ---

public export
Nil : InSet a
Nil _ = False

public export
(::) : Equality a => a -> InSet a -> InSet a
(::) added parent x = if x =?= added then True else x `isin` parent

--- Constants

public export %inline
Empty : InSet a
Empty = []

public export
Universe : InSet a
Universe _ = True

---------------------------
--- Basic set relations ---
---------------------------

public export
(==) : InSet a -> InSet a -> Type
sa == sb = (x : a) -> x `isin` sa = x `isin` sb

public export
(<=) : InSet a -> InSet a -> Type
sa <= sb = (x : a) -> x `isin` sa = True -> x `isin` sb = True

public export
NotEmpty : {a : Type} -> InSet a -> Type
NotEmpty s = (x ** x `isin` s = True)

----------------------------
--- Basic set operations ---
----------------------------

export
(+) : InSet a -> InSet a -> InSet a -- union
(+) sa sb x = x `isin` sa || x `isin` sb

export
(#) : InSet a -> InSet a -> InSet a -- intersection
(#) sa sb x = x `isin` sa && x `isin` sb

export
(-) : InSet a -> InSet a -> InSet a -- set difference
(-) sa sb x = x `isin` sa && x `notin` sb

export
(^) : InSet a -> InSet a -> InSet a -- symmetrical difference
(^) sa sb x = (x `isin` sa) `xor` (x `isin` sb)

export %inline
complement : InSet a -> InSet a
complement s x = x `notin` s

------------------------------------
--- Non-algebraic set operations ---
------------------------------------

export
(*) : InSet a -> InSet b -> InSet (a, b)
(*) sx sy (x, y) = x `isin` sx && y `isin` sy

--------------
--------------
---        ---
---  LAWS  ---
---        ---
--------------
--------------

------------------------
--- Laws of equality ---
------------------------

export
eq_reflexivity : (0 s : InSet a) -> s == s
eq_reflexivity _ _ = Refl

export
eq_symmerty : {0 sa, sb : InSet a} -> (0 _ : sa == sb) -> sb == sa
eq_symmerty f x = rewrite f x in Refl

export
eq_transitivity : {0 sa, sb, sc : InSet a} -> (0 _ : sa == sb) -> (0 _ : sb == sc) -> sa == sc
eq_transitivity f g x = rewrite f x in
                        rewrite g x in
                        Refl

-- Definition above can be written as
--   sa <= sb = (x : a) -> So (x `isin` sa) -> So (x `isin` sb)
-- but this leads to constant using `soToEq` and `eqToSo` in proofs.

--- Negative equality-related laws ---

trueNotFalse : Not (True = False)
trueNotFalse Refl impossible

export
non_empty_is_not_empty : NotEmpty s -> Not (s = Empty)
non_empty_is_not_empty (x ** prf_t) prf_f = trueNotFalse $ rewrite sym prf_t in rewrite prf_f in Refl

export
non_empty_not_eq_empty : NotEmpty s -> Not (s == Empty)
non_empty_not_eq_empty (x ** prf_t) prf_f = trueNotFalse $ rewrite sym prf_t in rewrite prf_f x in Refl

export
cant_in_and_not_in : (s : InSet a) -> (x : a) -> Not (x `isin` s = x `notin` s)
cant_in_and_not_in s x prf with (s x)
  cant_in_and_not_in _ _ Refl | True impossible

-------------------------------
--- Laws of subset relation ---
-------------------------------

--- Order laws of subset relation ---

export
subset_equal : {0 sa, sb : InSet a} -> (0 _ : sa == sb) -> sa <= sb
subset_equal f x prf = rewrite sym $ f x in
                       rewrite prf in
                       Refl

export
subset_reflexivity : (0 s : InSet a) -> s <= s
subset_reflexivity _ _ = id

export
subset_antisymmetry : {sa, sb : InSet a} -> sa <= sb -> sb <= sa -> sa == sb
subset_antisymmetry f g x with (decEq (sa x) True)
  subset_antisymmetry f _ x | Yes pa with (decEq (sb x) True)
    subset_antisymmetry _ _ _ | Yes pa | Yes pb = rewrite pa in
                                                  rewrite pb in
                                                  Refl
    subset_antisymmetry f _ x | Yes pa | No nb = absurd . nb $ f x pa
  subset_antisymmetry _ g x | No pa with (decEq (sb x) True)
    subset_antisymmetry _ _ _ | No na | No nb = rewrite notTrueIsFalse na in
                                                rewrite notTrueIsFalse nb in
                                                Refl
    subset_antisymmetry _ g x | No na | Yes pb = absurd . na $ g x pb

export
subset_transitivity : {0 sa, sb, sc : InSet a} -> (0 _ : sa <= sb) -> (0 _ : sb <= sc) -> sa <= sc
subset_transitivity f g x y = rewrite g x (f x y) in Refl

-- Subset relation's totality seems to be unprovable for intensional sets neither in
--   `Either (sa <= sb) (sb <= sa)`, nor in `Not $ sa <= sb => sb <= sa` variant.

--- Alternative subset representations with unions and intersections ---

export
subset_thru_union : {sa, sb : InSet a} -> (0 _ : sa <= sb) -> sa + sb == sb
subset_thru_union f x with (decEq (sa x) True)
  subset_thru_union f x | Yes pa = rewrite pa in
                                   rewrite f x pa in
                                   Refl
  subset_thru_union _ _ | No na = rewrite notTrueIsFalse na in Refl

export
union_thru_subset : {0 sa, sb : InSet a} -> (0 _ : sa + sb == sb) -> sa <= sb
union_thru_subset f x y = rewrite sym $ f x in
                          rewrite y in
                          Refl

export
subset_thru_intersection : {sa, sb : InSet a} -> (0 _ : sa <= sb) -> sa # sb == sa
subset_thru_intersection f x with (decEq (sa x) True)
  subset_thru_intersection f x | Yes pa = rewrite pa in
                                          rewrite f x pa in
                                          Refl
  subset_thru_intersection _ _ | No na = rewrite notTrueIsFalse na in Refl

export
intersection_thru_subset : {0 sa, sb : InSet a} -> (0 _ : sa # sb == sa) -> sa <= sb
intersection_thru_subset f x pa = rewrite sym pa in
                                  rewrite sym $ f x in
                                  rewrite pa in
                                  Refl

--- Subset with binary set operations ---

export
subset_for_unioned_right : {0 sa, sb : InSet a} -> (0 sc : InSet a) -> (0 _ : sa <= sb) -> sa <= sb + sc
subset_for_unioned_right sc f x prf = rewrite f x prf in Refl

and_true_left_true : (a, b : Bool) -> a && b = True -> a = True
and_true_left_true True _ _ = Refl

export
subset_for_intersected_left : {0 sa, sb : InSet a} -> (0 sc : InSet a) -> (0 _ : sa <= sb) -> (sa # sc) <= sb
subset_for_intersected_left sc f x prf = rewrite f x $ and_true_left_true (sa x) (sc x) prf in Refl

export
subset_for_diffed_left : {0 sa, sb : InSet a} -> (0 sc : InSet a) -> (0 _ : sa <= sb) -> (sa - sc) <= sb
subset_for_diffed_left sc f x prf = rewrite f x $ and_true_left_true (sa x) (x `notin` sc) prf in Refl

-- Particular cases for the properties from above, where `sb = sa`

export
subset_refl_unioned_right : (0 sa, sc : InSet a) -> sa <= sa + sc
subset_refl_unioned_right sa sc = subset_for_unioned_right sc $ subset_reflexivity sa

export
subset_refl_intersected_left : (0 sa, sc : InSet a) -> (sa # sc) <= sa
subset_refl_intersected_left sa sc = subset_for_intersected_left sc $ subset_reflexivity sa

export
subset_refl_diffed_left : (0 sa, sc : InSet a) -> (sa - sc) <= sa
subset_refl_diffed_left sa sc = subset_for_diffed_left sc $ subset_reflexivity sa

--- Subset with complement ---

export
subset_of_complements : {0 sa, sb : InSet a} -> (0 _ : sa <= sb) -> complement sb <= complement sa
subset_of_complements f x prf = rewrite sym $ subset_thru_intersection f x in
                                rewrite the (sb x = False) $ rewrite sym $ notInvolutive $ sb x in cong not prf in
                                rewrite andFalseFalse $ sa x in
                                Refl

export
subset_of_complements_back : {0 sa, sb : InSet a} -> (0 _ : complement sb <= complement sa) -> sa <= sb
subset_of_complements_back f x prf = rewrite sym $ subset_of_complements f x (rewrite notInvolutive $ sa x in prf) in
                                     rewrite notInvolutive $ sb x in
                                     Refl

--------------------------------------------------
--- Congruence of relations in specializations ---
--------------------------------------------------

--- Append ---

export
append_eq_cong_l : Equality a => (0 s : InSet a) -> {0 n, m : a} -> (0 _ : n = m) -> n::s == m::s
append_eq_cong_l _ prf _ = rewrite prf in Refl

export
append_eq_cong_r : Equality a => {0 sa, sb : InSet a} -> (n : a) -> (0 _ : sa == sb) -> n::sa == n::sb
append_eq_cong_r n f x with (x =?= n)
  append_eq_cong_r _ _ _ | True = Refl
  append_eq_cong_r _ f x | False = rewrite f x in Refl

--- Union ---

export
union_eq_cong_l : {0 sa, sb : InSet a} -> (0 sc : InSet a) -> (0 _ : sa == sb) -> sa + sc == sb + sc
union_eq_cong_l _ f x = rewrite f x in Refl

export
union_eq_cong_r : {0 sa, sb : InSet a} -> (0 sc : InSet a) -> (0 _ : sa == sb) -> sc + sa == sc + sb
union_eq_cong_r _ f x = rewrite f x in Refl

-- particular case for `append_eq_cong_l`
export
union_singleton_eq_cong_l : Equality a => (0 s : InSet a) -> {0 n, m : a} -> (0 _ : n = m) -> [n] + s == [m] + s
union_singleton_eq_cong_l _ prf x = rewrite append_eq_cong_l [] prf x in Refl

-- TODO to add for subset

--- Intersection ---

-- TODO to add for equality

-- TODO to add for subset

--- Difference ---

-- TODO to add for equality

-- TODO to add for subset

--- Symmetrical difference ---

-- TODO to add for equality

-- TODO to add for subset

--- Complement ---

-- TODO to add for equality

-- TODO to add for subset

--- Cartesian product ---

export
cart_eq_cong_l : {0 sa, sb : InSet a} -> (0 sc : InSet c) -> (0 _ : sa == sb) -> sc * sa == sc * sb
cart_eq_cong_l _ f (_, y) = rewrite f y in Refl

export
cart_eq_cong_r : {0 sa, sb : InSet a} -> (0 sc : InSet c) -> (0 _ : sa == sb) -> sa * sc == sb * sc
cart_eq_cong_r _ f (x, _) = rewrite f x in Refl

and_true_then_left_true : (a : Bool) -> {b : Bool} -> a && b = True -> a = True
and_true_then_left_true True {b=True} Refl = Refl

and_true_then_right_true : {a : Bool} -> (b : Bool) -> a && b = True -> b = True
and_true_then_right_true {a=True} True Refl = Refl

export
cart_subset_cong_l : {0 sa, sb : InSet a} -> (0 sc : InSet c) -> (0 _ : sa <= sb) -> sc * sa <= sc * sb
cart_subset_cong_l sc f (y, x) prf = rewrite f x $ and_true_then_right_true _ prf in
                                     rewrite and_true_then_left_true (sc y) prf in
                                     Refl

export
cart_subset_cong_r : {0 sa, sb : InSet a} -> (0 sc : InSet c) -> (0 _ : sa <= sb) -> sa * sc <= sb * sc
cart_subset_cong_r sc f (x, y) prf = rewrite f x $ and_true_then_left_true _ prf in
                                     rewrite and_true_then_right_true (sc y) prf in
                                     Refl

----------------------
--- Laws of `isin` ---
----------------------

export
not_in_empty : Equality a => (0 x : a) -> x `isin` [] = False
not_in_empty _ = Refl

export
x_in_x_etc : Equality a => (0 x : a) -> (0 s : InSet a) -> x `isin` (x::s) = True
x_in_x_etc x s = rewrite equ_reflexive x in Refl

export
x_in_same_etc : Equality a => (0 x, y : a) -> (0 s : InSet a) -> (0 _ : x =?= y = True) -> x `isin` (y::s) = True
x_in_same_etc _ _ _ prf = rewrite prf in Refl

export
not_x_not_in_x_etc : Equality a => (x, y : a) -> NeqPrf x y -> x `isin` [y] = False
not_x_not_in_x_etc x y neq = case @@(x =?= y) of
  (False ** prf) => rewrite prf in Refl
  (True ** prf) => absurd $ cant_eq_neq (eq_val_to_prf prf) neq

export
not_in_both : Equality a => (0 x, y : a) -> (0 ys : InSet a) -> (0 _ : x =?= y = False) -> (0 _ : x `isin` ys = False) -> x `isin` (y::ys) = False
not_in_both x y ys xy xys = rewrite xy in
                            rewrite xys in
                            Refl

export
is_in_tail : Equality a => (0 x, y : a) -> (0 ys : InSet a) -> (0 _ : x =?= y = False) -> (0 _ : x `isin` (y::ys) = True) -> x `isin` ys = True
is_in_tail _ _ _ xy xyys = rewrite sym xyys in
                           rewrite xy in
                           Refl

----------------------
--- Laws of append ---
----------------------

export
append_is_union : Equality a => (n : a) -> (0 s : InSet a) -> n::s == [n] + s
append_is_union n _ x with (x =?= n)
  append_is_union _ _ _ | True = Refl
  append_is_union _ _ _ | False = Refl

---------------------
--- Laws of union ---
---------------------

export
union_of_self : (0 s : InSet a) -> s + s == s
union_of_self s x = rewrite orSameNeutral $ s x in Refl

export
union_commutative : (0 sa, sb : InSet a) -> sa + sb == sb + sa
union_commutative sa sb x = rewrite orCommutative (sa x) (sb x) in Refl

export
union_associative : (0 sa, sb, sc : InSet a) -> sa + (sb + sc) == (sa + sb) + sc
union_associative sa sb sc x = rewrite orAssociative (sa x) (sb x) (sc x) in Refl

export
union_empty_neutral : (0 s : InSet a) -> s + [] == s
union_empty_neutral s x = rewrite orFalseNeutral $ s x in Refl

export
union_preserves_universe : (0 s : InSet a) -> s + Universe == Universe
union_preserves_universe s x = rewrite orTrueTrue $ s x in Refl

-- ... with intersection

export
union_distributes_over_intersection : (0 sa, sb, sc : InSet a) -> sa + (sb # sc) == (sa + sb) # (sa + sc)
union_distributes_over_intersection sa sb sc x = rewrite orDistribAndR (sa x) (sb x) (sc x) in Refl

-- ... with diff

export
union_with_diff : (0 sa, sb, sc : InSet a) -> sa + (sb - sc) == (sa + sb) - (sc - sa)
union_with_diff sa sb sc x = rewrite orDistribAndR (sa x) (sb x) (not $ sc x) in
                             rewrite notAndIsOr (sc x) (not $ sa x) in
                             rewrite notInvolutive $ sa x in
                             rewrite orCommutative (sa x) (not $ sc x) in
                             Refl

-- ... with symdiff

-- TODO To make this functon to have `(0 sa, sb : InSet a)` in the signature.
export
union_thru_symdiff_and_intersection : (sa, sb : InSet a) -> sa + sb == (sa ^ sb) ^ (sa # sb)
union_thru_symdiff_and_intersection sa sb x = case (decEq (sa x) True, decEq (sb x) True) of
  (Yes pa, Yes pb) => rewrite pa in                 rewrite pb in                 Refl
  (Yes pa, No  nb) => rewrite pa in                 rewrite notTrueIsFalse nb in  Refl
  (No  na, Yes pb) => rewrite notTrueIsFalse na in  rewrite pb in                 Refl
  (No  na, No  nb) => rewrite notTrueIsFalse na in  rewrite notTrueIsFalse nb in  Refl

-- ... with complement

export
union_with_its_complement : (0 s : InSet a) -> s + complement s == Universe
union_with_its_complement s x = rewrite orNotTrue $ s x in Refl

----------------------------
--- Laws of intersection ---
----------------------------

export
intersection_of_self : (0 s : InSet a) -> s # s == s
intersection_of_self s x = rewrite andSameNeutral $ s x in Refl

export
intersection_commutative : (0 sa, sb : InSet a) -> sa # sb == sb # sa
intersection_commutative sa sb x = rewrite andCommutative (sa x) (sb x) in Refl

export
intersection_associative : (0 sa, sb, sc : InSet a) -> sa # (sb # sc) == (sa # sb) # sc
intersection_associative sa sb sc x = rewrite andAssociative (sa x) (sb x) (sc x) in Refl

export
intersection_universe_neutral : (0 s : InSet a) -> s # Universe == s
intersection_universe_neutral s x = rewrite andTrueNeutral $ s x in Refl

export
intersection_preserves_empty : (0 s : InSet a) -> s # [] == []
intersection_preserves_empty s x = rewrite andFalseFalse $ s x in Refl

-- ... with union

export
intersection_distributes_over_union : (0 sa, sb, sc : InSet a) -> sa # (sb + sc) == (sa # sb) + (sa # sc)
intersection_distributes_over_union sa sb sc x = rewrite andDistribOrR (sa x) (sb x) (sc x) in Refl

-- ... with set diff

export
intersection_diff_swap : (0 sa, sb, sc : InSet a) -> sa # (sb - sc) == sb # (sa - sc)
intersection_diff_swap sa sb sc x = rewrite andAssociative (sa x) (sb x) (not $ sc x) in
                                    rewrite andAssociative (sb x) (sa x) (not $ sc x) in
                                    rewrite andCommutative (sa x) (sb x) in
                                    Refl

export
intersection_diff_assoc : (0 sa, sb, sc : InSet a) -> sa # (sb - sc) == (sa # sb) - sc
intersection_diff_assoc sa sb sc x = rewrite sym $ andAssociative (sa x) (sb x) (not $ sc x) in Refl

-- ... with symmetrical diff

-- TODO To make this functon to have `(0 sa, sb, sc : InSet a)` in the signature.
export
intersection_distributes_over_symdiff : (sa, sb, sc : InSet a) -> sa # (sb ^ sc) == (sa # sb) ^ (sa # sc)
intersection_distributes_over_symdiff sa sb sc x = case decEq (sa x) True of
  Yes pa => rewrite pa in Refl
  No na => rewrite notTrueIsFalse na in Refl

-- ... with complement

export
intersection_with_complement : (0 sa, sb : InSet a) -> sa # complement sb == sa - sb
intersection_with_complement _ _ _ = Refl

export
intersection_with_its_complement : (0 s : InSet a) -> s # complement s == []
intersection_with_its_complement s x = rewrite andNotFalse $ s x in Refl

------------------------------
--- Laws of set difference ---
------------------------------

export
diff_of_intersection : (0 sa, sb, sc : InSet a) -> sc - (sa # sb) == (sc - sa) + (sc - sb)
diff_of_intersection sa sb sc x = rewrite notAndIsOr (sa x) (sb x) in
                                  rewrite andDistribOrR (sc x) (not $ sa x) (not $ sb x) in
                                  Refl

export
diff_of_union : (0 sa, sb, sc : InSet a) -> sc - (sa + sb) == (sc - sa) # (sc - sb)
diff_of_union sa sb sc x = rewrite notOrIsAnd (sa x) (sb x) in
                           rewrite andAssociative (sc x && not (sa x)) (sc x) (not $ sb x) in
                           rewrite sym $ andAssociative (sc x) (not $ sa x) (sc x) in
                           rewrite andCommutative (not $ sa x) (sc x) in
                           rewrite andAssociative (sc x) (sc x) (not $ sa x) in
                           rewrite andSameNeutral $ sc x in
                           rewrite andAssociative (sc x) (not $ sa x) (not $ sb x) in
                           Refl

export
diff_of_diff : (0 sa, sb, sc : InSet a) -> sc - (sb - sa) == (sc # sa) + (sc - sb)
diff_of_diff sa sb sc x = rewrite notAndIsOr (sb x) (not $ sa x) in
                          rewrite notInvolutive $ sa x in
                          rewrite orCommutative (not $ sb x) (sa x) in
                          rewrite andDistribOrR (sc x) (sa x) (not $ sb x) in
                          Refl

export
diff_of_self : (0 s : InSet a) -> s - s == []
diff_of_self s x = rewrite andNotFalse $ s x in Refl

export
diff_of_empty_left : (0 s : InSet a) -> [] - s == []
diff_of_empty_left _ _ = Refl

export
diff_of_empty_right : (0 s : InSet a) -> s - [] == s
diff_of_empty_right s x = rewrite andTrueNeutral $ s x in Refl

export
diff_of_universe : (0 s : InSet a) -> s - Universe == []
diff_of_universe s x = rewrite andFalseFalse $ s x in Refl

export
diff_of_complements : (0 sa, sb : InSet a) -> complement sa - complement sb == sb - sa
diff_of_complements sa sb x = rewrite andCommutative (sb x) (not $ sa x) in
                              rewrite notInvolutive $ sb x in
                              Refl

--------------------------------------
--- Laws of symmetrical difference ---
--------------------------------------

-- TODO To make this functon to have `(0 sa, sb : InSet a)` in the signature.
export
symdiff_as_union_of_diffs : (sa, sb : InSet a) -> sa ^ sb == (sa - sb) + (sb - sa)
symdiff_as_union_of_diffs sa sb x = case (decEq (sa x) True, decEq (sb x) True) of
  (Yes pa, Yes pb) => rewrite pa in                 rewrite pb in                 Refl
  (Yes pa, No  nb) => rewrite pa in                 rewrite notTrueIsFalse nb in  Refl
  (No  na, Yes pb) => rewrite notTrueIsFalse na in  rewrite pb in                 Refl
  (No  na, No  nb) => rewrite notTrueIsFalse na in  rewrite notTrueIsFalse nb in  Refl

-- TODO To make this functon to have `(0 sa, sb : InSet a)` in the signature.
export
symdiff_as_diff_of_ui : (sa, sb : InSet a) -> sa ^ sb == (sa + sb) - (sa # sb)
symdiff_as_diff_of_ui sa sb x = case (decEq (sa x) True, decEq (sb x) True) of
  (Yes pa, Yes pb) => rewrite pa in                 rewrite pb in                 Refl
  (Yes pa, No  nb) => rewrite pa in                 rewrite notTrueIsFalse nb in  Refl
  (No  na, Yes pb) => rewrite notTrueIsFalse na in  rewrite pb in                 Refl
  (No  na, No  nb) => rewrite notTrueIsFalse na in  rewrite notTrueIsFalse nb in  Refl

export
symdiff_commutative : (0 sa, sb : InSet a) -> sa ^ sb == sb ^ sa
symdiff_commutative sa sb x = rewrite xorCommutative (sa x) (sb x) in Refl

export
symdiff_associative : (0 sa, sb, sc : InSet a) -> sa ^ (sb ^ sc) == (sa ^ sb) ^ sc
symdiff_associative sa sb sc x = rewrite xorAssociative (sa x) (sb x) (sc x) in Refl

export
symdiff_with_empty : (0 s : InSet a) -> s ^ [] == s
symdiff_with_empty s x = rewrite xorCommutative (s x) False in
                         rewrite xorFalseNeutral $ s x in
                         Refl

export
symdiff_with_self : (0 s : InSet a) -> s ^ s == []
symdiff_with_self s x = rewrite xorSameFalse $ s x in Refl

-- TODO To make this functon to have `(0 sa, sb, sc : InSet a)` in the signature.
export
symdiff_twice_negates : (sa, sb, sc : InSet a) -> (sa ^ sb) ^ (sb ^ sc) == sa ^ sc
symdiff_twice_negates sa sb sc x = rewrite xorCommutative (sa x) (sb x) in
                                   case decEq (sb x) True of
                                     Yes pb => rewrite pb in
                                               rewrite xorTrueNot $ sa x in
                                               rewrite xorTrueNot $ sc x in
                                               rewrite notXorCancel (sa x) (sc x) in
                                               Refl
                                     No nb => rewrite notTrueIsFalse nb in
                                              rewrite xorFalseNeutral $ sa x in
                                              rewrite xorFalseNeutral $ sc x in
                                              Refl

export
symdiff_of_complements : (0 sa, sb : InSet a) -> sa ^ sb == complement sa ^ complement sb
symdiff_of_complements sa sb x = rewrite notXorCancel (sa x) (sb x) in Refl

--------------------------
--- Laws of complement ---
--------------------------

export
comp_of_union : (0 sa, sb : InSet a) -> complement (sa + sb) == complement sa # complement sb
comp_of_union sa sb x = rewrite notOrIsAnd (sa x) (sb x) in Refl

export
comp_of_intersection : (0 sa, sb : InSet a) -> complement (sa # sb) == complement sa + complement sb
comp_of_intersection sa sb x = rewrite notAndIsOr (sa x) (sb x) in Refl

export
comp_of_empty : complement [] == Universe
comp_of_empty _ = Refl

export
comp_of_universe : complement Universe == []
comp_of_universe _ = Refl

export
comp_involutive : (0 s : InSet a) -> complement (complement s) == s
comp_involutive s x = rewrite notInvolutive $ s x in Refl

export
comp_of_diff : (0 sa, sb : InSet a) -> complement (sa - sb) == complement sa + sb
comp_of_diff sa sb x = rewrite notAndIsOr (sa x) (not $ sb x) in
                       rewrite notInvolutive $ sb x in
                       Refl

---------------------------------
--- Laws of cartesian product ---
---------------------------------

--- Operations over cartesian products at both sides:

export
intersection_of_carts : (0 sa, sb : InSet a) -> (0 sc, sd : InSet c) -> (sa * sc) # (sb * sd) == (sa # sb) * (sc # sd)
intersection_of_carts sa sb sc sd (x, y) = rewrite sym $ andAssociative (sa x) (sc y) (sb x && sd y) in
                                           rewrite sym $ andAssociative (sa x) (sb x) (sc y && sd y) in
                                           rewrite andAssociative (sc y) (sb x) (sd y) in
                                           rewrite andAssociative (sb x) (sc y) (sd y) in
                                           rewrite andCommutative (sb x) (sc y) in
                                           Refl

export
diff_of_carts : (0 sa, sb : InSet a) -> (0 sc, sd : InSet c) -> (sa * sc) - (sb * sd) == sa * (sc - sd) + (sa - sb) * sc

export
union_of_carts : (0 sa, sb : InSet a) -> (0 sc, sd : InSet c) -> (sa * sc) + (sb * sd) == ((sa - sb) * sc) # ((sa # sb) * (sc + sd)) # ((sb - sa) * sd)

--- Distributivity:

export
cart_distributes_over_intersection : (0 sa : InSet a) -> (0 sb, sc : InSet b) -> sa * (sb # sc) == (sa * sb) # (sa * sc)
cart_distributes_over_intersection sa sb sc (x, y) = rewrite sym $ andAssociative (sa x) (sb y) (sa x && sc y) in
                                                     rewrite andAssociative (sb y) (sa x) (sc y) in
                                                      rewrite andCommutative (sb y) (sa x) in
                                                     rewrite sym $ andAssociative (sa x) (sb y) (sc y) in
                                                     rewrite andAssociative (sa x) (sa x) (sb y && sc y) in
                                                      rewrite andSameNeutral (sa x) in
                                                     Refl

export
cart_distributes_over_union : (0 sa : InSet a) -> (0 sb, sc : InSet b) -> sa * (sb + sc) == (sa * sb) + (sa * sc)

export
cart_distributes_over_diff : (0 sa : InSet a) -> (0 sb, sc : InSet b) -> sa * (sb - sc) == (sa * sb) - (sa * sc)

export
complement_of_cart : (0 sa : InSet a) -> (0 sb : InSet b) -> complement (sa * sb) = (complement sa * complement sb) + (complement sa * sb) + (sa * complement sb)

--- Cartesian products with relations

export
subset_of_carts_drops_l : {0 sa, sb : InSet a} -> {0 sc, sd : InSet c} -> (0 _ : NotEmpty sa) -> (0 _ : NotEmpty sc) ->
                          (0 _ : (sa * sc) <= (sb * sd)) -> sa <= sb

export
subset_of_carts_drops_r : {0 sa, sb : InSet a} -> {0 sc, sd : InSet c} -> (0 _ : NotEmpty sa) -> (0 _ : NotEmpty sc) ->
                          (0 _ : (sa * sc) <= (sb * sd)) -> sc <= sd

export
cart_of_subsets : {0 sa, sb : InSet a} -> {0 sc, sd : InSet c} -> (0 _ : sa <= sb) -> (0 _ : sc <= sd) -> (sa * sc) <= (sb * sd)

max_stars_repo_name: buzden/prog-prove-exercises

max_issues_repo_name: buzden/prog-prove-exercises

max_forks_repo_name: buzden/prog-prove-exercises


text:
parameters (X : Nat)
  Foo : Type
  Foo = Nat

  record Bar where
    constructor MkBar
    Gnu : Foo

  Baz : Foo -> Nat
  Baz x = x

  Quux : Bar -> Foo
  Quux x = Gnu x


text:
module IdrisJvm.Core.Function

import IdrisJvm.Core.Asm
import IdrisJvm.Core.Common
import IdrisJvm.Core.Constant
import IdrisJvm.Core.ControlFlow
import IdrisJvm.Core.Foreign
import IdrisJvm.Core.Operator
import IdrisJvm.Core.Inference
import IdrisJvm.IR.Types
import Data.SortedMap
import Java.Lang

%access public export

data ExportCall = ExportCallConstructor
                | ExportCallInstance
                | ExportCallStatic
                | ExportCallSuper

Show ExportCall where
    show ExportCallConstructor = "ExportCallConstructor"
    show ExportCallInstance = "ExportCallInstance"
    show ExportCallStatic = "ExportCallStatic"
    show ExportCallSuper = "ExportCallSuper"

Eq ExportCall where
    ExportCallConstructor == ExportCallConstructor = True
    ExportCallInstance == ExportCallInstance = True
    ExportCallStatic == ExportCallStatic = True
    ExportCallSuper == ExportCallSuper = True
    _ == _ = False

createIdrisObject : Int -> List LVar -> Asm ()
createIdrisObject constructorId [] =
  if constructorId < cast unrolledConstructorPropsCount then
    let fieldName = "NO_ARG_CONSTRUCTOR_" ++ cast constructorId
    in Field FGetStatic idrisObjectType fieldName (classSig idrisObjectType)
  else do
    New idrisObjectType
    Dup
    Iconst constructorId
    InvokeMethod InvokeSpecial idrisObjectType "<init>" "(I)V" False

createIdrisObject constructorId args = do
  locTypes <- GetFunctionLocTypes
  New idrisObjectType
  Dup
  Iconst constructorId
  let unrolledArgs = take unrolledConstructorPropsCount args
  let unrolledArgTys = getLocTy locTypes <$> unrolledArgs
  loadUnrolledArgs $ List.zip unrolledArgs unrolledArgTys
  createArrayProperties
  InvokeMethod InvokeSpecial idrisObjectType "<init>" constructorSig False
where
  argsLength : Int
  argsLength = cast $ length args

  arrayProps : List LVar
  arrayProps = drop unrolledConstructorPropsCount args

  loadUnrolledArgs : List (LVar, InferredType) -> Asm ()
  loadUnrolledArgs [] = pure ()
  loadUnrolledArgs ((var, varTy) :: vars) = do
    locTys <- GetFunctionLocTypes
    loadVar locTys varTy inferredObjectType var
    loadUnrolledArgs vars

  arrayPropsLength : Int
  arrayPropsLength = cast $ length arrayProps

  constructorSig : String
  constructorSig =
    if arrayPropsLength == 0 then
      "(I" ++ repeatObjectDesc (cast argsLength) ++ ")V"
    else
      "(I" ++ repeatObjectDesc unrolledConstructorPropsCount ++ "[Ljava/lang/Object;)V"

  storeArrayProp : InferredTypeStore -> Int -> LVar -> Asm ()
  storeArrayProp types idx var = do
    Dup
    Iconst idx
    let varTy = getLocTy types var
    loadVar types varTy inferredObjectType var
    Aastore

  storeArrayProps : Asm ()
  storeArrayProps =
    when (arrayPropsLength > 0) $ do
        locTypes <- GetFunctionLocTypes
        sequence_ $ List.zipWith (storeArrayProp locTypes) [0 .. (arrayPropsLength - 1)] arrayProps

  createArrayProperties : Asm ()
  createArrayProperties =
    if arrayPropsLength == 0 then
      Pure ()
    else do
      Iconst arrayPropsLength
      Anewarray "java/lang/Object"
      storeArrayProps

hasConstructorExport : List Export -> Bool
hasConstructorExport = any isConstructorExport where
    isConstructorExport (ExportFun _ (FCon "Constructor") _ _) = True
    isConstructorExport _                                      = False

tailRecStartLabelName : String
tailRecStartLabelName = "$tailRecStartLabel"

tailRecEndLabelName : String
tailRecEndLabelName = "$tailRecEndLabel"

assignNull : InferredType -> LVar -> Asm ()
assignNull ty var = do Aconstnull; storeVar ty ty var

initializeInferredVar : InferredType -> Int -> Asm ()
initializeInferredVar ty varIndex =
    let var = Loc varIndex
    in case ty of
        IBool => do Iconst 0; storeVar ty ty var
        IByte => do Iconst 0; storeVar ty ty var
        IChar => do Iconst 0; storeVar ty ty var
        IShort => do Iconst 0; storeVar ty ty var
        IInt => do Iconst 0; storeVar ty ty var
        ILong => do Lconst 0; storeVar ty ty var
        IFloat => do Fconst 0; storeVar ty ty var
        IDouble => do Dconst 0; storeVar ty ty var
        Ref refTy => assignNull ty var
        IArray elemTy => assignNull ty var
        IUnknown => assignNull ty var

initializeLocalVars : List (Int, InferredType) -> Asm ()
initializeLocalVars [] = pure ()
initializeLocalVars ((var, ty) :: vars) = do
    initializeInferredVar ty var
    initializeLocalVars vars

mutual
  parseAnnotation : FDesc -> Annotation
  parseAnnotation (FApp "Ann" [FStr annTypeName, attr]) =
    let typeDesc = "L" ++ annTypeName ++ ";"
    in (MkAnnotation typeDesc (parseAnnotationAttr attr))
  parseAnnotation desc = jerror $ "Unable to parse annotation: " ++ show desc

  parseAnnotations : FDesc -> List Annotation
  parseAnnotations (FApp "::" [FCon "Annotation", desc, rest])
    = parseAnnotation desc :: parseAnnotations rest

  parseAnnotations (FApp "Nil" [FCon "Annotation"]) = []

  parseAnnotations (FCon "Annotation") = []

  parseAnnotations desc = parseAnnotation desc :: []

  parseParamAnnotations : FDesc -> List (List Annotation)
  parseParamAnnotations (FApp "::" [FApp "List" [FCon "Annotation"], ann, rest])
    = parseAnnotations ann :: parseParamAnnotations rest
  parseParamAnnotations (FApp "Nil" [FApp "List" [FCon "Annotation"]]) = []

  parseAnnotationAttr : FDesc -> List AnnotationProperty
  parseAnnotationAttr (FApp "::" [ FApp "Pair" [ FUnknown, FCon "AnnotationValue" ]
                                 , FApp "MkPair" [ FUnknown
                                                 , FCon "AnnotationValue"
                                                 , FStr attrName
                                                 , annValueDesc
                                                 ]
                                  , rest
                                  ])
    = (attrName, parseAnnotationValue annValueDesc) :: parseAnnotationAttr rest
  parseAnnotationAttr (FApp "Nil" [ FApp "Pair" [ FUnknown , FCon "AnnotationValue"]]) = []
  parseAnnotationAttr desc = jerror $ "Annotation attribute value not yet supported: " ++ show desc

  parseAnnArrayElements : List FDesc -> List AnnotationValue
  parseAnnArrayElements [] = []
  parseAnnArrayElements [FApp "::" (FCon "AnnotationValue" :: value :: values)] =
    parseAnnotationValue value :: parseAnnArrayElements values
  parseAnnArrayElements [FApp "Nil" [FCon "AnnotationValue"]] = []

  parseAnnotationValue : FDesc -> AnnotationValue
  parseAnnotationValue (FApp "AnnString" [FStr value]) = AnnString value
  parseAnnotationValue (FApp "AnnInt" [FStr value]) = AnnInt $ cast value
  parseAnnotationValue (FApp "AnnBoolean" [FStr value]) = AnnBoolean $ (value == "true")
  parseAnnotationValue (FApp "AnnByte" [FStr value]) = AnnByte $ Byte.parseByte value
  parseAnnotationValue (FApp "AnnChar" [FStr value]) = AnnChar $ strHead value
  parseAnnotationValue (FApp "AnnShort" [FStr value]) = AnnShort $ Short.parseShort value
  parseAnnotationValue (FApp "AnnLong" [FStr value]) = AnnLong $ Long.parseLong value
  parseAnnotationValue (FApp "AnnFloat" [FStr value]) = AnnFloat $ JDouble.parseDouble value
  parseAnnotationValue (FApp "AnnDouble" [FStr value]) = AnnDouble $ JDouble.parseDouble value
  parseAnnotationValue (FApp "AnnClass" [FStr value]) = AnnClass value
  parseAnnotationValue (FApp "AnnEnum" [FStr enum, FStr value]) = AnnEnum (asmRefTyDesc (ClassDesc enum)) value
  parseAnnotationValue (FApp "AnnArray" values) = AnnArray (parseAnnArrayElements values)
  parseAnnotationValue (FApp "AnnAnnotation" [ann]) = AnnAnnotation (parseAnnotation ann)
  parseAnnotationValue desc = jerror $ "Invalid or unsupported annotation value: " ++ show desc

mutual

  cgBody : (InferredType -> Asm ()) -> SExp -> Asm ()
  cgBody ret (SV (Glob n)) = do
    let fname = jname n
    let MkJMethodName cname mname = fname
    (retTy, _) <- getFunctionType fname
    let desc = getInferredFunDesc [] retTy
    InvokeMethod InvokeStatic cname mname desc False
    ret inferredObjectType

  cgBody ret (SV var) = do
    locTypes <- GetFunctionLocTypes
    let varTy = getLocTy locTypes var
    loadVar locTypes varTy varTy var
    ret varTy

  cgBody ret (SApp True f args) = do
    caller <- GetFunctionName
    let targetMethodName = jname f
    if targetMethodName == caller then
       -- self tail call, assign parameters then loop
       let argsLength = the Int $ cast $ length args
       in when (argsLength > 0) $ assign (Loc <$> [0 .. (pred argsLength)]) args
    -- non-self tail call
    else do
      createThunk caller targetMethodName args
      ret (Ref thunkClass)

  cgBody ret (SApp False f args) = cgSApp ret False f args

  cgBody ret (SLet i v sc) = do
      locTys <- GetFunctionLocTypes
      let iTy = getLocTy locTys i
      assign iTy
      cgBody ret sc
    where
      assign : InferredType -> Asm ()
      assign iTy = case v of
                     SNothing => do Aconstnull; storeVar inferredObjectType iTy i
                     _ => cgBody (\vTy => storeVar vTy iTy i) v

  cgBody ret (SUpdate _ e) = cgBody ret e

  cgBody ret (SProj (Loc v) i) = do
    idrisObjectProperty v i
    ret inferredObjectType

  cgBody ret (SCon _ 0 "Prelude.Bool.False" []) = do
    Iconst 0
    ret IBool
  cgBody ret (SCon _ 1 "Prelude.Bool.True" []) = do
    Iconst 1
    ret IBool

  cgBody ret (SCon _ t _ args) = do createIdrisObject t args; ret inferredIdrisObjectType

  cgBody ret (SCase _ e ((SConCase _ 0 "Prelude.Bool.False" [] falseAlt) ::
                         (SConCase _ 1 "Prelude.Bool.True" [] trueAlt) ::
                         _))
    = cgIfTrueElse ret cgBody e trueAlt falseAlt

  cgBody ret (SCase _ e ((SConCase _ 1 "Prelude.Bool.True" [] trueAlt) ::
                        (SDefaultCase falseAlt) ::
                        _))
    = cgIfTrueElse ret cgBody e trueAlt falseAlt

  cgBody ret (SCase _ e ((SConCase _ 0 "Prelude.Bool.False" [] falseAlt) ::
                        (SDefaultCase trueAlt) ::
                        _))
    = cgIfTrueElse ret cgBody e trueAlt falseAlt

  cgBody ret (SCase _ e [SDefaultCase defaultCaseExpr]) = cgBody ret defaultCaseExpr

  cgBody ret (SCase _ e alts) =
    if any defaultCase alts
        then cgSwitch ret cgBody e alts
        else cgSwitch ret cgBody e (alts ++ [SDefaultCase SNothing])

  cgBody ret (SChkCase e [SDefaultCase defaultCaseExpr]) = cgBody ret defaultCaseExpr

  cgBody ret (SChkCase e alts) = cgSwitch ret cgBody e alts

  cgBody ret (SConst c) = cgConst ret c

  cgBody ret (SOp op args) = cgOp ret op args

  cgBody ret SNothing = do
    invokeError "Unexpected case encountered. This could be due to non-exhaustive patterns."
    ret inferredObjectType

  cgBody ret (SError x) = do invokeError (show x); ret IUnknown

  cgBody ret (SForeign returns fdesc args) = cgForeign (parseDescriptor returns fdesc args) where

    argsLength : Nat
    argsLength = length args

    argVars : List LVar
    argVars = snd <$> args

    targetArgIndices : List Int
    targetArgIndices = if argsLength > 0 then [0 .. (pred $ the Int $ cast argsLength)] else []

    lambdaArgVars : List LVar
    lambdaArgVars = Loc <$> targetArgIndices

    inferredRetTy : TypeDescriptor -> InferredType
    inferredRetTy returnDesc = typeDescriptorToInferredType returnDesc

    retVoidOrBoxed : TypeDescriptor -> Asm ()
    retVoidOrBoxed VoidDescriptor = Aconstnull
    retVoidOrBoxed returnDesc = box (inferredRetTy returnDesc)

    synthenticMethodArgTys : InferredTypeStore
    synthenticMethodArgTys = SortedMap.fromList $ List.zip targetArgIndices $ replicate argsLength inferredObjectType

    targetLocTys : InferredTypeStore
    targetLocTys =
      let targetArgTys = List.zip targetArgIndices $ fst <$> args
      in SortedMap.fromList $
        (\(var, fdesc) => (var, fieldTypeDescriptorToInferredType $ fdescFieldDescriptor fdesc)) <$> targetArgTys

    cgForeign (JStatic clazz fn) = case fdescTypeDescriptor returns of
      ThrowableDescriptor returnDesc => do
        locTys <- GetFunctionLocTypes
        let descriptor = asmMethodDesc $ MkMethodDescriptor (fdescFieldDescriptor . fst <$> args) returnDesc
        let arity = length args
        let lambdaBody = do
          loadVars synthenticMethodArgTys targetLocTys lambdaArgVars
          InvokeMethod InvokeStatic clazz fn descriptor False
          retVoidOrBoxed returnDesc
        caller <- GetFunctionName
        let targetMethodName = MkJMethodName clazz fn
        createExceptionHandlerThunk caller targetMethodName argVars lambdaBody
        InvokeMethod InvokeStatic utilClass "throwable" ("(" ++ rtThunkSig ++ ")Ljava/lang/Object;") False
        ret inferredObjectType
      returnDesc => do
        locTys <- GetFunctionLocTypes
        let descriptor = asmMethodDesc $ MkMethodDescriptor (fdescFieldDescriptor . fst <$> args) returnDesc
        loadVars locTys targetLocTys argVars
        InvokeMethod InvokeStatic clazz fn descriptor False
        when (returnDesc == VoidDescriptor) Aconstnull
        ret (inferredRetTy returnDesc)

    cgForeign (JGetStaticField clazz fieldName) = do
      let returnDesc = fdescTypeDescriptor returns
      Field FGetStatic clazz fieldName (asmTypeDesc returnDesc)
      ret (typeDescriptorToInferredType returnDesc)

    cgForeign (JSetStaticField clazz fieldName) = case args of
      [ty] => do
        locTys <- GetFunctionLocTypes
        loadVars locTys targetLocTys argVars
        let desc = asmFieldTypeDesc $ fdescFieldDescriptor . fst $ ty
        Field FPutStatic clazz fieldName desc
        let returnDesc = fdescTypeDescriptor returns
        Aconstnull
        ret (typeDescriptorToInferredType returnDesc)
      otherwise => jerror $ "There can be only one argument for setting a static field: " ++ clazz ++ "." ++ fieldName

    cgForeign (JVirtual clazz fn) = case fdescTypeDescriptor returns of
      ThrowableDescriptor returnDesc => do
        let descriptor = asmMethodDesc $ MkMethodDescriptor (fdescFieldDescriptor . fst <$> drop 1 args) returnDesc
        locTys <- GetFunctionLocTypes
        let lambdaBody = do
          loadVars synthenticMethodArgTys targetLocTys lambdaArgVars
          InvokeMethod InvokeVirtual clazz fn descriptor False
          retVoidOrBoxed returnDesc
        caller <- GetFunctionName
        let targetMethodName = MkJMethodName clazz fn
        createExceptionHandlerThunk caller targetMethodName argVars lambdaBody
        InvokeMethod InvokeStatic utilClass "throwable" ("(" ++ rtThunkSig ++ ")Ljava/lang/Object;") False
        ret inferredObjectType
      returnDesc => do
          locTys <- GetFunctionLocTypes
          -- drop first arg type as it is an implicit 'this'
          let descriptor = asmMethodDesc $ MkMethodDescriptor (fdescFieldDescriptor . fst <$> drop 1 args) returnDesc
          loadVars locTys targetLocTys argVars
          InvokeMethod InvokeVirtual clazz fn descriptor False
          when (returnDesc == VoidDescriptor) Aconstnull
          ret (inferredRetTy returnDesc)

    cgForeign (JGetInstanceField clazz fieldName) = do
      locTys <- GetFunctionLocTypes
      let returnDesc = fdescTypeDescriptor returns
      loadVars locTys targetLocTys argVars
      Field FGetField clazz fieldName (asmTypeDesc returnDesc)
      ret (inferredRetTy returnDesc)

    cgForeign (JSetInstanceField clazz fieldName) = case args of
      [_, arg] => do
        locTys <- GetFunctionLocTypes
        loadVars locTys targetLocTys argVars
        let desc = asmTypeDesc . fdescTypeDescriptor . fst $ arg
        Field FPutField clazz fieldName desc
        let returnDesc = fdescTypeDescriptor returns
        Aconstnull
        ret (typeDescriptorToInferredType returnDesc)
      otherwise => jerror "Setting an instance field must take 2 arguments: the instance and the field value"

    cgForeign (JInterface clazz fn) = case fdescTypeDescriptor returns of
        ThrowableDescriptor returnDesc => do
          locTys <- GetFunctionLocTypes
          let descriptor = asmMethodDesc $ MkMethodDescriptor (fdescFieldDescriptor . fst <$> drop 1 args) returnDesc
          let lambdaBody = do
            loadVars synthenticMethodArgTys targetLocTys lambdaArgVars
            InvokeMethod InvokeInterface clazz fn descriptor True
            retVoidOrBoxed returnDesc
          caller <- GetFunctionName
          let targetMethodName = MkJMethodName clazz fn
          createExceptionHandlerThunk caller targetMethodName argVars lambdaBody
          InvokeMethod InvokeStatic utilClass "throwable" ("(" ++ rtThunkSig ++ ")Ljava/lang/Object;") False
          ret inferredObjectType
        returnDesc => do
          locTys <- GetFunctionLocTypes
          let descriptor = asmMethodDesc $ MkMethodDescriptor (fdescFieldDescriptor . fst <$> drop 1 args) returnDesc
          loadVars locTys targetLocTys argVars
          InvokeMethod InvokeInterface clazz fn descriptor True
          when (returnDesc == VoidDescriptor) Aconstnull
          ret (inferredRetTy returnDesc)

    cgForeign (JNew clazz) = case fdescTypeDescriptor returns of
      ThrowableDescriptor returnDesc => do
        locTys <- GetFunctionLocTypes
        let descriptor = asmMethodDesc $ MkMethodDescriptor (fdescFieldDescriptor . fst <$> args) VoidDescriptor
        let lambdaBody = do
          New clazz
          Dup
          loadVars synthenticMethodArgTys targetLocTys lambdaArgVars
          InvokeMethod InvokeSpecial clazz "<init>" descriptor False
        caller <- GetFunctionName
        let targetMethodName = MkJMethodName clazz "<init>"
        createExceptionHandlerThunk caller targetMethodName argVars lambdaBody
        InvokeMethod InvokeStatic utilClass "throwable" ("(" ++ rtThunkSig ++ ")Ljava/lang/Object;") False
        ret inferredObjectType
      returnDesc => do
        locTys <- GetFunctionLocTypes
        let descriptor = asmMethodDesc $ MkMethodDescriptor (fdescFieldDescriptor . fst <$> args) VoidDescriptor
        New clazz
        Dup
        loadVars locTys targetLocTys argVars
        InvokeMethod InvokeSpecial clazz "<init>" descriptor False
        ret (inferredRetTy returnDesc)

    cgForeign JNewArray = case args of
      [ty] => do
        locTys <- GetFunctionLocTypes
        loadVars locTys targetLocTys argVars
        let arrDesc = fdescFieldDescriptor returns
        let elemDesc = case arrDesc of
          FieldTyDescReference (ArrayDesc elem) => elem
          otherwise => jerror $ "Invalid return type while creating an array" ++ show returns
        anewarray elemDesc
        ret $ typeDescriptorToInferredType (FieldDescriptor arrDesc)
      otherwise => jerror $ "There can be only one argument (length) to create an array" ++ show args

    cgForeign JMultiNewArray = do
        locTys <- GetFunctionLocTypes
        loadVars locTys targetLocTys argVars
        let returnDesc = fdescRefDescriptor returns
        let arrayType = refTyClassName returnDesc
        Multianewarray arrayType (List.length args)
        ret $ fieldTypeDescriptorToInferredType (FieldTyDescReference returnDesc)

    cgForeign JSetArray = case args of
      ((arrFDesc, arr) :: rest@(arg1 :: arg2 :: args)) => do
        let value = last rest
        let indices = init rest
        let valueDesc = fdescFieldDescriptor (fst value)
        aload $ locIndex arr
        Checkcast $ refTyClassName (fdescRefDescriptor arrFDesc)
        idrisToJavaLoadArray $ (\(fdesc, lvar) => (fdescFieldDescriptor fdesc, lvar)) <$> indices
        idrisToJava [(valueDesc, snd value)]
        arrayStore valueDesc
        Aconstnull
        ret IUnknown
      otherwise => jerror $ "Invalid arguments while trying to set an element inside array: " ++ show args

    cgForeign JGetArray = case args of
      ((arrFDesc, arr) :: indices@(index :: restIndices)) => do
        aload $ locIndex arr
        Checkcast $ refTyClassName (fdescRefDescriptor arrFDesc)
        idrisToJavaLoadArray $ (\(fdesc, lvar) => (fdescFieldDescriptor fdesc, lvar)) <$> indices
        let returnDesc = fdescTypeDescriptor returns
        arrayLoad $ typeDescToarrayElemDesc returnDesc
        ret $ typeDescriptorToInferredType returnDesc
      otherwise => jerror $ "Invalid arguments while trying to get an element from array: " ++ show args

    cgForeign JArrayLength = case args of
      [(arrFDesc, arr)] => do
        aload $ locIndex arr
        Checkcast $ refTyClassName (fdescRefDescriptor arrFDesc)
        Arraylength
        ret IInt
      otherwise => jerror $ "Invalid arguments while trying to get length of an array: " ++ show args

    cgForeign (JInstanceOf className) = case args of
      [ty] => do
          locTys <- GetFunctionLocTypes
          loadVars locTys targetLocTys argVars
          InstanceOf className
          let returnDesc = fdescTypeDescriptor returns
          ret $ typeDescriptorToInferredType returnDesc

    cgForeign (JClassLiteral "int") = do getPrimitiveClass "java/lang/Integer"; ret $ Ref "java/lang/Class"
    cgForeign (JClassLiteral "byte") = do getPrimitiveClass "java/lang/Byte"; ret $ Ref "java/lang/Class"
    cgForeign (JClassLiteral "char") = do getPrimitiveClass "java/lang/Character"; ret $ Ref "java/lang/Class"
    cgForeign (JClassLiteral "short") = do getPrimitiveClass "java/lang/Short"; ret $ Ref "java/lang/Class"
    cgForeign (JClassLiteral "boolean") = do getPrimitiveClass "java/lang/Boolean"; ret $ Ref "java/lang/Class"
    cgForeign (JClassLiteral "long") = do getPrimitiveClass "java/lang/Long"; ret $ Ref "java/lang/Class"
    cgForeign (JClassLiteral "float") = do getPrimitiveClass "java/lang/Float"; ret $ Ref "java/lang/Class"
    cgForeign (JClassLiteral "double") = do getPrimitiveClass "java/lang/Double"; ret $ Ref "java/lang/Class"
    cgForeign (JClassLiteral clazz) = do
      Ldc $ TypeConst $ classSig clazz
      ret $ Ref "java/lang/Class"

    cgForeign (JLambda clazz interfaceFnName) = case args of
      [(interfaceFnTy, _), (lambdaTy, lambdaVar)] => do
        caller <- GetFunctionName
        createJvmFunctionalObject lambdaVar caller (MkJMethodName clazz interfaceFnName) interfaceFnTy lambdaTy
        ret $ Ref clazz
      otherwise => jerror $ "There can be only two arguments while passing a java lambda for " ++ clazz ++
        "." ++ interfaceFnName ++ ": the interface method signature and the lambda signature"

  cgBody _ _ = jerror "NOT IMPLEMENTED!!!!"

  cgSApp : (InferredType -> Asm ()) -> Bool -> String -> List LVar -> Asm ()
  cgSApp ret isTailCall f args = do
    callerLocTys <- GetFunctionLocTypes
    let fname = jname f
    let MkJMethodName cname mname = fname
    let argsLength = length args
    (targetRetTy, targetLocTys) <- getFunctionType fname
    loadVars callerLocTys targetLocTys args
    let targetArgTys = if argsLength > 0
        then getLocTy targetLocTys . Loc . cast <$> [0 .. (Nat.pred argsLength)]
        else []
    let targetMethodDesc = getInferredFunDesc targetArgTys targetRetTy
    InvokeMethod InvokeStatic cname mname targetMethodDesc False
    when (not isTailCall && (isThunk targetRetTy || isObject targetRetTy)) $
        InvokeMethod InvokeStatic (rtClass "Runtime") "unwrap" "(Ljava/lang/Object;)Ljava/lang/Object;" False
    ret targetRetTy

  exportCode : SortedMap JMethodName InferredFunctionType -> ExportIFace -> Asm ()
  exportCode types (MkExportIFace "IdrisJvm.FFI.FFI_JVM" exportedClassName exportItems) = do
      let (cls, parent, intf) = parseExportedClassName exportedClassName
      let (classAnns, otherExports) = parseClassAnnotations exportItems
      CreateClass ComputeMaxs
      ClassCodeStart 52 Public cls Nothing parent intf classAnns
      SourceInfo "IdrisGenerated.idr"
      when (not $ hasConstructorExport exportItems) $ defaultConstructor cls parent
      sequence_ $ (cgExport types cls parent) <$> otherExports
  exportCode _ e = jerror $ "Unsupported Export: " ++ show e

  cgExport : SortedMap JMethodName InferredFunctionType -> ClassName -> ClassName -> Export -> Asm ()
  cgExport _ _ _ (ExportData (FStr exportedType)) = createClassForIdrisType exportedType

  cgExport _ cname _ (ExportFun _ (FApp "ExportInstanceField" [FStr fieldName]) typeDesc _)
    = createField [Public] cname fieldName typeDesc

  cgExport _ cname _ (ExportFun _ (FApp "ExportStaticField" [FStr fieldName]) typeDesc _)
    = createField [Public, Static] cname fieldName typeDesc

  cgExport types cname parent (ExportFun n (FApp "Super" [FStr superMethodName]) returns args)
    = exportFun types cname (jmethName (jname n)) parent superMethodName ExportCallSuper parent returns args [] []

  cgExport types cname parent (ExportFun n (FApp "ExportStatic" [FStr mname]) returns args)
    = let MkJMethodName sourceCname sourceMname = jname n
      in exportFun types cname mname sourceCname sourceMname ExportCallStatic parent returns args [] []

  cgExport types cname parent (ExportFun n (FCon "ExportDefault") returns args)
    = let MkJMethodName sourceCname sourceMname = jname n
      in exportFun types cname sourceMname sourceCname sourceMname ExportCallInstance parent returns args [] []

  cgExport types cname parent (ExportFun n (FCon "Constructor") returns args)
    = let MkJMethodName sourceCname sourceMname = jname n
      in exportFun types cname "<init>" sourceCname sourceMname ExportCallConstructor parent returns args [] []

  cgExport types cname parent (ExportFun n (FApp "ExportInstance" [FStr mname]) returns args)
    = let MkJMethodName sourceCname sourceMname = jname n
      in exportFun types cname mname sourceCname sourceMname ExportCallInstance parent returns args [] []

  cgExport types cname parent
      (ExportFun n (FApp "ExportInstanceWithAnn" [FStr mname, FApp "::" annDescs, paramAnnDescs]) returns args)
    = let MkJMethodName sourceCname sourceMname = jname n
          anns = join $ parseAnnotations <$> annDescs
          paramAnns = parseParamAnnotations paramAnnDescs
      in exportFun types cname mname sourceCname sourceMname ExportCallInstance parent returns args anns paramAnns

  cgExport types cname parent
        (ExportFun n (FApp "ExportStaticWithAnn" [FStr mname, FApp "::" annDescs, paramAnnDescs]) returns args)
    = let MkJMethodName sourceCname sourceMname = jname n
          anns = join $ parseAnnotations <$> annDescs
          paramAnns = parseParamAnnotations paramAnnDescs
      in exportFun types cname mname sourceCname sourceMname ExportCallStatic parent returns args anns paramAnns

  cgExport _ _ _ exportDef = jerror $ "Unsupported export definition: " ++ show exportDef

  parseClassAnnotations : List Export -> (List Annotation, List Export)
  parseClassAnnotations exports@(ExportFun n (FApp "Anns" desc) _ _:: rest) =
    if jmethName (jname n) == "classWith" then (join $ parseAnnotations <$> desc, rest)
    else ([], exports)
  parseClassAnnotations nonClassAnnotations = ([], nonClassAnnotations)

  loadExportFunArgs : List (Int, FieldTypeDescriptor) -> InferredTypeStore -> InferredType -> Int -> Asm ()
  loadExportFunArgs exportedArgs argTys argTy argIndex = do
    let loc = Loc argIndex
    case find (\(index, argDesc) => index == argIndex) exportedArgs of
        Just (index, (FieldTyDescReference refTy)) => do
            let cname = refTyClassName refTy
            loadVar argTys (getLocTy argTys loc) (Ref cname) loc
            InvokeMethod InvokeVirtual cname "getValue" "()Ljava/lang/Object;" False
            cgCast inferredObjectType argTy
        Nothing => loadVar argTys (getLocTy argTys loc) argTy loc

  exportFun : SortedMap JMethodName InferredFunctionType
           -> ClassName
           -> MethodName
           -> ClassName
           -> MethodName
           -> ExportCall
           -> ClassName
           -> FDesc
           -> List FDesc
           -> List Annotation
           -> List (List Annotation)
           -> Asm ()
  exportFun types targetCname targetMethName sourceCname sourceMname exportCall parent returns args anns paramAnns = do
      let isStatic = exportCall == ExportCallStatic
      let sourceMethodName = MkJMethodName sourceCname sourceMname
      let argsLength = length args
      let sourceMethodArity = maybe argsLength arity (lookup sourceMethodName types)
      let accessMods = if isStatic then [Public, Static] else [Public]
      let argStartIndex = the Int $ if isStatic then 0 else 1 -- drop `this` for instance methods
      let isSuperExport = exportCall == ExportCallSuper
      let isConstructor = exportCall == ExportCallConstructor
      let isIo = isExportIO returns
      let argDescs = fdescFieldDescriptor <$> (if isStatic then args else drop 1 args) -- for instance method, drop `this`
      let returnDesc = if isConstructor then VoidDescriptor else fdescTypeDescriptor returns
      let mdesc = asmMethodDesc $ MkMethodDescriptor argDescs returnDesc
      let argIndices = intRange argStartIndex (cast argsLength)
      let exportedArgs = filter (\(index, arg) => isExportedDesc arg) $ List.zip argIndices argDescs
      let targetArgTys = SortedMap.fromList $ List.zip argIndices $ fieldTypeDescriptorToInferredType <$> argDescs
      let f = \toTy, index => loadExportFunArgs exportedArgs targetArgTys toTy index
      (sourceRetTy, sourceLocTyStore) <- getFunctionType (MkJMethodName sourceCname sourceMname)
      let sourceLocTys = values sourceLocTyStore
      let sourceArgTys = List.take (length argDescs) $ (if isStatic then sourceLocTys else drop 1 sourceLocTys)
      let loadArgs = sequence_ $ List.zipWith f sourceArgTys argIndices
      let invType = if isSuperExport then InvokeSpecial else InvokeStatic
      let shouldApplyCallIo = argsLength == sourceMethodArity
      let sourceMdesc = if isSuperExport
                            then asmMethodDesc $ MkMethodDescriptor argDescs returnDesc
                            else getInferredFunDesc (take sourceMethodArity $ values sourceLocTyStore) sourceRetTy
      let nullAdditionalArgs = the (Asm ()) $ case isLTE argsLength sourceMethodArity of
          Yes smaller =>
              let diff = sourceMethodArity - argsLength
              in case diff of
                   Z => pure ()
                   n => sequence_ $ replicate n Aconstnull
          No _ => pure ()
      CreateMethod accessMods targetCname targetMethName mdesc Nothing Nothing anns paramAnns
      MethodCodeStart
      when isConstructor $ do -- Call matching super Constructor
        Aload 0 -- load "this"
        loadArgs
        InvokeMethod InvokeSpecial parent "<init>" mdesc False
      when (not isSuperExport && isIo && shouldApplyCallIo) $ do
        Aconstnull -- Setup the 2 null args for "call__IO"
        Dup
      when (not isStatic) $ Aload 0 -- load "this"
      loadArgs
      nullAdditionalArgs
      InvokeMethod invType sourceCname sourceMname sourceMdesc False
      let isPossibleThunk = isThunk sourceRetTy || isObject sourceRetTy
      when (not isSuperExport && isPossibleThunk) $
          InvokeMethod InvokeStatic (rtClass "Runtime") "unwrap" (sig 1) False
      when (not isSuperExport && isIo) $ unwrapExportedIO sourceRetTy shouldApplyCallIo
      case returnDesc of
          (FieldDescriptor (FieldTyDescReference (IdrisExportDesc cname))) =>
              let desc = "(Ljava/lang/Object;)L" ++ cname ++ ";"
              in InvokeMethod InvokeStatic cname "create" desc False
          _ => when (not isSuperExport && (isPossibleThunk || isIo)) $
                  cgCast inferredObjectType (typeDescriptorToInferredType returnDesc)
      javaReturn returnDesc
      MaxStackAndLocal (-1) (-1)
      MethodCodeEnd
    where
      unwrapExportedIO : InferredType -> (shouldApplyCallIo: Bool) -> Asm ()
      unwrapExportedIO sourceRetTy shouldApplyCallIo =
        if shouldApplyCallIo then do
          let fname = MkJMethodName "main/Main" "call__IO"
          (retTy, locTys) <- getFunctionType fname
          let argTys = getLocTy locTys <$> the (List LVar) [Loc 0, Loc 1, Loc 2]
          let (_ :: _ :: lastArgTy :: _) = argTys
          let desc = getInferredFunDesc argTys retTy
          cgCast sourceRetTy lastArgTy
          InvokeMethod InvokeStatic "main/Main" "call__IO" desc False
          InvokeMethod InvokeStatic (rtClass "Runtime") "unwrap" (sig 1) False
        else do
          cgCast sourceRetTy inferredObjectType
          InvokeMethod InvokeStatic (rtClass "Runtime") "unwrap" (sig 1) False

  cgFun : List Access -> String -> ClassName -> MethodName -> List String -> Int -> SExp -> Asm ()
  cgFun access idrisName clsName fname args locs def = do
      let jMethodName = MkJMethodName clsName fname
      UpdateFunctionName jMethodName
      functionTypes <- GetFunctionTypes
      let (retTy, types, nLocVars) = calculateFunctionType jMethodName functionTypes
      UpdateFunctionTypes $ SortedMap.insert jMethodName
        (MkInferredFunctionType jMethodName retTy types arity) functionTypes
      UpdateFunctionLocTypes types
      UpdateFunctionRetType retTy
      UpdateLocalVarCount $ cast (if shouldEliminateTco then nLocVars + 2 else nLocVars + 1)
      locTys <- GetFunctionLocTypes
      Debug ("### " ++ clsName ++ "." ++ fname ++ ": " ++ show (toList locTys) ++ " -> " ++ show retTy)
      UpdateShouldDescribeFrame True
      let argTys = if nArgs > 0 then getLocTy types <$> (Loc <$> [0 .. pred nArgs]) else []
      CreateMethod access clsName fname (getInferredFunDesc argTys retTy) Nothing Nothing [] []
      MethodCodeStart
      UpdateSwitchIndex 0 -- reset
      UpdateIfIndex 0 -- reset
      initializeLocalVars $ drop (cast nArgs) $ toList types
      methBody nLocVars

      let resultVarIndex = nLocVars
      loadVar locTys retTy retTy (Loc resultVarIndex)
      javaReturn (FieldDescriptor $ inferredTypeToFieldTypeDesc retTy)

      MaxStackAndLocal (-1) (-1)
      MethodCodeEnd
    where
      arity : Nat
      arity = length args

      nArgs : Int
      nArgs = cast arity

      getLocalVarCount : InferredTypeStore -> Int
      getLocalVarCount locTys = case keys locTys of
        [] => nArgs + locs
        locVars@(_ :: _) => max (last locVars + 1) (nArgs + locs)

      shouldEliminateTco : Bool
      shouldEliminateTco = any (== idrisName) (findTailCallApps [] def)

      calculateFunctionType : JMethodName
                           -> SortedMap JMethodName InferredFunctionType
                           -> (InferredType, InferredTypeStore, Int)
      calculateFunctionType fname types =
        let MkInferredFunctionType _ retTy localTys _ =
                fromMaybe (MkInferredFunctionType fname IUnknown SortedMap.empty arity)
                  $ lookup fname types
            nLocVars = getLocalVarCount localTys
            resultVarIndex = nLocVars
            tailRecVarIndex = nLocVars + 1
            withTcoType = if shouldEliminateTco then SortedMap.insert tailRecVarIndex IInt localTys else localTys
            withResultVarType = SortedMap.insert resultVarIndex retTy withTcoType
            totalVars = if shouldEliminateTco then nLocVars + 2 else nLocVars + 1
            allVarIndices = if totalVars > 0 then [0 .. pred totalVars] else []
            missingVars = (\var => (var, IUnknown)) <$> (allVarIndices \\ keys withResultVarType)
            allVars = insertFrom missingVars withResultVarType
        in (retTy, allVars, nLocVars)

      methBody : Int -> Asm ()
      methBody nLocVars =
            if shouldEliminateTco
            then do
              types <- GetFunctionLocTypes
              Iconst 1
              let tailRecVar = Loc tailRecVarIndex
              opWithWordSize types Istore tailRecVar
              CreateLabel tailRecStartLabelName
              LabelStart tailRecStartLabelName
              UpdateShouldDescribeFrame True
              addFrame
              opWithWordSize types Iload tailRecVar
              CreateLabel tailRecEndLabelName
              Ifeq tailRecEndLabelName
              cgBody ret def
              Goto tailRecStartLabelName
              LabelStart tailRecEndLabelName
              Frame FSame 0 [] 0 []
            else cgBody ret def
        where
            tailRecVarIndex : Int
            tailRecVarIndex = nLocVars + 1

            ret : InferredType -> Asm ()
            ret ty = do
              retTy <- GetFunctionRetType
              let resultVarIndex = nLocVars
              storeVar ty retTy (Loc resultVarIndex)
              when shouldEliminateTco $
                 do Iconst 0
                    Istore tailRecVarIndex -- Base case for tailrec. Set the tailrec flag to false.

  createClassForIdrisType : String -> Asm ()
  createClassForIdrisType idrisType = do
      CreateClass ComputeMaxs
      ClassCodeStart 52 Public idrisType Nothing "java/lang/Object" [] []
      SourceInfo "IdrisGenerated.idr"
      CreateField [Private, Final] idrisType "value" "Ljava/lang/Object;" Nothing Nothing
      FieldEnd
      createConstructor
      getter
      createDef
    where
      createConstructor : Asm ()
      createConstructor = do
        CreateMethod [Public] idrisType "<init>" "(Ljava/lang/Object;)V" Nothing Nothing [] []
        MethodCodeStart
        Aload 0
        InvokeMethod InvokeSpecial "java/lang/Object" "<init>" "()V" False
        Aload 0
        Aload 1
        Field FPutField idrisType "value" "Ljava/lang/Object;"
        Return
        MaxStackAndLocal (-1) (-1)
        MethodCodeEnd

      getter : Asm ()
      getter = do
        CreateMethod [Public] idrisType "getValue" "()Ljava/lang/Object;" Nothing Nothing [] []
        MethodCodeStart
        Aload 0
        Field FGetField idrisType "value" "Ljava/lang/Object;"
        Areturn
        MaxStackAndLocal (-1) (-1)
        MethodCodeEnd

      createDesc : String
      createDesc = "(Ljava/lang/Object;)L" ++ idrisType ++ ";"

      createDef : Asm ()
      createDef = do
        CreateMethod [Public, Static] idrisType "create" createDesc Nothing Nothing [] []
        New idrisType
        Dup
        Aload 0
        InvokeMethod InvokeSpecial idrisType "<init>"  "(Ljava/lang/Object;)V" False
        Areturn
        MaxStackAndLocal (-1) (-1)
        MethodCodeEnd

  createField : List Access -> ClassName -> FieldName -> FDesc -> Asm ()
  createField access cname fieldName typeDesc = do
      CreateField access cname fieldName desc Nothing Nothing
      FieldEnd
    where
      desc = asmTypeDesc $ fdescTypeDescriptor typeDesc

  findTailCallApps : List String -> SExp -> List String
  findTailCallApps acc (SApp tailCall f _) = if tailCall then f :: acc else acc
  findTailCallApps acc (SLet _ v sc) =  acc ++ findTailCallApps [] v ++ findTailCallApps [] sc
  findTailCallApps acc (SUpdate _ e) = findTailCallApps acc e
  findTailCallApps acc (SCase _ _ alts) = acc ++ concat (findTailCallAppsCase <$> alts)
  findTailCallApps acc (SChkCase _ alts) = acc ++ concat (findTailCallAppsCase <$> alts)
  findTailCallApps acc _ = acc

  findTailCallAppsCase : SAlt -> List String
  findTailCallAppsCase (SConstCase _ e)     = findTailCallApps [] e
  findTailCallAppsCase (SDefaultCase e)     = findTailCallApps [] e
  findTailCallAppsCase (SConCase _ _ _ _ e) = findTailCallApps [] e


text:
-- Minimal implicational logic, PHOAS approach, initial encoding

module STLC

%default total

-- Types

infixr 0 :=>

data Ty : Type where
  UNIT  :             Ty
  (:=>) : Ty -> Ty -> Ty

-- Context

Cx : Type
Cx = Ty -> Type

-- Terms

infixl 1 :$

data Tm : Cx -> Ty -> Type
  where
    var  :  tc a
         ----------
         -> Tm tc a

    lam  :  (tc a -> Tm tc b)
         --------------------
          -> Tm tc (a :=> b)

    (:$) : Tm tc (a :=> b) -> Tm tc a
         ----------------------------
                 -> Tm tc b

T : Ty -> Type
T a = {tc : Cx} -> Tm tc a

-- Example theorems

I : T (a :=> a)
I = lam $ \x =>
      var x

K : T (a :=> b :=> a)
K = lam $ \x =>
      lam $ \_ =>
        var x

S : T ((a :=> b :=> c) :=> (a :=> b) :=> a :=> c)
S = lam $ \f =>
      lam $ \g =>
        lam $ \x =>
          (var f :$ var x) :$ (var g :$ var x)

SKK : T (a :=> a)
SKK {a} =
  S {b = a :=> a} :$ K :$ K


text:
module India.Language.Core

import public India.Language.Core.Lexer
import public India.Language.Core.Parser
import public India.Language.Core.Types

%default total

max_stars_repo_name: berewt/india

max_issues_repo_name: berewt/india

max_forks_repo_name: berewt/india


text:
import Data.IOArray

main : IO ()
main
    = do x <- newArray 20
         ignore $ writeArray x 10 "Hello"
         ignore $ writeArray x 11 "World"
         printLn !(toList x)

         y <- fromList (map Just [1,2,3,4,5])
         printLn !(toList y)


text:
module Main

import Effect.Baseline
import Effect.StdIO
import Effects
import Baseline

program : Eff () [BASELINE, STDIO]
program = do
  readHistory ".history"
  addDictEntries
    [ "multidiscipline"
    , "multivitamin"
    , "multiplex"
    , "monocrystalline"
    , "streamline"
    , "waterline"
    , "skyline"
    , "online"
    , "byline" ]
  loop
  writeHistory ".history"
  putStrLn "Exit!"
where
  loop : Eff () [BASELINE, STDIO]
  loop = case !(baseline "$> ") of
              Just "" => loop
              Just s  => do
                putStrLn ("You typed: " ++ s)
                loop
              otherwise => pure ()

main : IO ()
main = run program

max_stars_repo_name: laserpants/baseline-idris

max_issues_repo_name: laserpants/baseline-idris

max_forks_repo_name: laserpants/baseline-idris


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
module XLA.FFI

import Data.Vect
import Types
import Util

export
enumerate : Vect n ty -> Vect n (Nat, ty)
enumerate xs = rewrite sym $ lengthCorrect xs in
    zip (range (length xs)) (rewrite lengthCorrect xs in xs)

libxla : String -> String
libxla fname = "C:" ++ fname ++ ",libxla"

{-
 -
 - Array shape
 -
 -}

%foreign (libxla "alloc_int_array")
prim__allocIntArray : Int -> PrimIO (Ptr Int)

%foreign (libxla "free_int_array")
prim__freeIntArray : Ptr Int -> PrimIO ()

%foreign (libxla "set_array_int")
prim__setArrayInt : Ptr Int -> Int -> Int -> PrimIO ()

export
mkIntArray : Cast ty Int => Vect n ty -> IO (Ptr Int)
mkIntArray xs = do
    ptr <- primIO $ prim__allocIntArray (cast (length xs))
    traverse_ (\(idx, x) => primIO $ prim__setArrayInt ptr (cast idx) (cast x)) (enumerate xs)
    pure ptr

export
free : Ptr Int -> IO ()
free = primIO . prim__freeIntArray

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
module Data.Time.Clock.Internal.UTCTime

import Data.Time.Clock.DiffTime
import Data.Time.Calendar.Days

import Generics.Derive

%default total
%language ElabReflection

-- --------------------------------------------------------------------------

public export
record UTCTime where
  constructor MkUTCTime
  day : Day
  daytime : DiffTime
%runElab derive "UTCTime" [Generic, Eq, Ord]

-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Text.Markup.Edda.Walk

import Data.AVL.Dict

import Text.Markup.Edda.Model.Common
import Text.Markup.Edda.Model.Raw
import Text.Markup.Edda.Model.Processed

%access export

interface Walkable a z where
  walk : (a -> a) -> z -> z

Walkable a b => Walkable a (List b) where
  walk f xs = map (walk f) xs

(Walkable a b, Walkable a c) => Walkable a (b,c) where
  walk f (x,y) = (walk f x, walk f y)

Walkable (Edda INLINE) (Edda INLINE) where
  -- inline to inline
  walk f (Emph xs)   = f $ Emph (walk f xs)
  walk f (Bold xs)   = f $ Bold (walk f xs)
  walk f (Strike xs) = f $ Strike (walk f xs)
  walk f (Uline xs)  = f $ Uline (walk f xs)

  walk f (Quote ty xs)  = f $ Quote ty (walk f xs)
  walk f (Parens ty xs) = f $ Parens ty (walk f xs)

  walk f (Ref uri)        = f $ Ref uri
  walk f (Cite ty uri)    = f $ Cite ty uri
  walk f (Hyper uri desc) = f $ Hyper uri (walk f desc)
  walk f (FNote uri desc) = f $ FNote uri (walk f desc)
  walk f (MiscPunc c)     = f $ MiscPunc c

  walk f inline = f inline

Walkable (Edda INLINE) (Edda BLOCK) where
  -- Inline structures from Blocks
  walk f (Section d l t as bs) = Section d l (walk f t) as (walk f bs)
  walk f (Figure l c as fig)   = Figure l (walk f c) as (walk f fig)
  walk f (DList kvs)           = DList (walk f kvs)

  walk f (OList xs) = OList (walk f xs)
  walk f (BList xs) = BList (walk f xs)

  walk f (Literal l c ss)       = Literal l (walk f c) ss
  walk f (Listing l c ty ops as s)  = Listing l (walk f c) ty ops as s

  walk f (Para xs)        = Para $ walk f xs
  walk f (Quotation l xs) = Quotation l (walk f xs)

  walk f (Theorem l c xs)     = Theorem l (walk f c) (walk f xs)
  walk f (Corollary l c xs)   = Corollary l (walk f c) (walk f xs)
  walk f (Lemma l c xs)       = Lemma l (walk f c) (walk f xs)
  walk f (Proposition l c xs) = Proposition l (walk f c) (walk f xs)
  walk f (Proof l c xs)       = Proof l (walk f c) (walk f xs)
  walk f (Definition l c xs)  = Definition l (walk f c) (walk f xs)
  walk f (Exercise l c xs)    = Exercise l (walk f c) (walk f xs)
  walk f (Note l c xs)        = Note l (walk f c) (walk f xs)
  walk f (Remark l c xs)      = Remark l (walk f c) (walk f xs)
  walk f (Problem l c xs)     = Problem l (walk f c) (walk f xs)
  walk f (Question l c xs)    = Question l (walk f c) (walk f xs)
  walk f (Solution l c xs)    = Solution l (walk f c) (walk f xs)
  walk f (Example l c xs)     = Example l (walk f c) (walk f xs)

  walk f block = block

Walkable (Edda BLOCK) (Edda INLINE) where
  walk  f (Emph xs)   = Emph (walk f xs)
  walk  f (Bold xs)   = Bold (walk f xs)
  walk  f (Strike xs) = Strike (walk f xs)
  walk  f (Uline xs)  = Uline (walk f xs)

  walk  f (Quote ty xs)  = Quote ty (walk f xs)
  walk  f (Parens ty xs) = Parens ty (walk f xs)

  walk  f (Hyper l xs) = Hyper l (walk f xs)
  walk  f (FNote l xs) = FNote l (walk f xs)
  walk  f inline = inline

Walkable (Edda BLOCK) (Edda BLOCK) where
  -- Walk Block structures from Blocks
  walk  f (Section d l t as bs)  = f $ Section d l (walk f t) as (walk f bs)
  walk  f (Figure l c as fig) = f $ Figure l (walk f c) as (walk f fig)
  walk  f (DList kvs)         = f $ DList (walk f kvs)

  walk  f (OList xs)  = f $ OList (walk f xs)
  walk  f (BList xs)  = f $ BList (walk f xs)

  walk  f (Para xs)           = f $ Para $ walk f xs
  walk  f (Quotation l xs)    = f $ Quotation l (walk f xs)

  walk  f (Theorem l c xs)     = f $ Theorem l c (walk f xs)
  walk  f (Corollary l c xs)   = f $ Corollary l c (walk f xs)
  walk  f (Lemma l c xs)       = f $ Lemma l c (walk f xs)
  walk  f (Proposition l c xs) = f $ Proposition l c (walk f xs)
  walk  f (Proof l c xs)       = f $ Proof l c (walk f xs)
  walk  f (Definition l c xs)  = f $ Definition l c (walk f xs)
  walk  f (Exercise l c xs)    = f $ Exercise l c (walk f xs)
  walk  f (Note l c xs)        = f $ Note l c (walk f xs)
  walk  f (Remark l c xs)      = f $ Remark l c (walk f xs)
  walk  f (Problem l c xs)     = f $ Problem l c (walk f xs)
  walk  f (Question l c xs)    = f $ Question l c (walk f xs)
  walk  f (Solution l c xs)    = f $ Solution l c (walk f xs)
  walk  f (Example l c xs)     = f $ Example l c (walk f xs)

  walk  f block  = f block

Walkable (Edda BLOCK) (Edda DOC) where
  -- Walk block structures from Doc
  walk f (Doc t as bs) = Doc t as (walk f bs)

Walkable (Edda INLINE) (Edda DOC) where
  -- Walk Inline structures from Doc
  walk f (Doc t as bs) = Doc (walk f t) as (walk f bs)

Walkable (Edda DOC) (Edda DOC) where
  -- Walk the doc
  walk f x = f x

Walkable (Edda BLOCK) (Edda SNIPPET) where
  -- Walk block structures from Doc
  walk f (Snippet snippet prf) with (prf)
    walk f (Snippet snippet prf) | IsInLine = Snippet (walk f snippet) prf
    walk f (Snippet snippet prf) | IsBlock = Snippet (walk f snippet) prf

  -- Snippet (map (walk f) ss) prf

Walkable (Edda INLINE) (Edda SNIPPET) where
  -- Walk Inline structures from Doc
  walk f (Snippet snippet prf) with (prf)
    walk f (Snippet snippet prf) | IsInLine = Snippet (walk f snippet) prf
    walk f (Snippet snippet prf) | IsBlock = Snippet (walk f snippet) prf

--  walk f (Snippet ss prf) = Snippet (map (walk f {z=INLINE}) ss) prf

Walkable (Edda SNIPPET) (Edda SNIPPET) where
  -- Walk the doc
  walk f x = f x

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
||| Stuff that goes wrong.
|||
||| Module    : Error.idr
||| Copyright : (c) Jan de Muijnck-Hughes
||| License   : see LICENSE
|||
module Circuits.NetList.Error

import Data.String
import Toolkit.Text.Parser.Run
import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Graph.EdgeBounded.HasExactDegree.All
import Toolkit.Data.Whole
import Toolkit.Data.Location
import Toolkit.Data.DList

import Toolkit.Data.List.AtIndex
import Toolkit.DeBruijn.Context.Item
import Toolkit.DeBruijn.Context
import Toolkit.DeBruijn.Renaming

import Circuits.Common.Pretty
import Circuits.NetList.Lexer
import Circuits.NetList.Types

%default total

export
Show Direction where
  show INPUT  = "input"
  show OUTPUT = "output"
  show INOUT  = "inout"

export
Show (Types.Cast.Cast f t) where
  show BI = "down"
  show BO = "up"

export
Show (Index f) where
  show (UP _) = "UP"
  show (DOWN _) = "DOWN"

export
Show Gate.Binary.Kind where
  show AND  = "and"
  show IOR  = "or"
  show XOR  = "xor"
  show ANDN = "nand"
  show IORN = "nor"
  show XORN = "xnor"

export
Show Ty where
  show TyUnit         = "()"
  show (TyPort (d,t)) = "TyPort(" <+> show d <+> "," <+> show t <+> ")"
  show TyGate         = "TyGate"
  show (TyChan t)     = "TyChan(" <+> show t <+> ")"

namespace Check
  public export
  data Error = Mismatch Ty Ty
             | MismatchD DType DType
             | NotBound String
             | VectorExpected
             | PortChanExpected
             | PortExpected
             | OOB Nat Nat
             | ErrI String
             | Err FileContext Check.Error

  export
  Show Check.Error where
    show (Mismatch x y)
      = "Type Mismatch:\n\n"
        <+>
        unlines [unwords ["\tExpected:",show x], unwords ["\tGiven:", show y]]

    show (MismatchD x y)
      = "Type Mismatch:\n\n"
        <+>
        unlines [unwords ["\tExpected:",show x], unwords ["\tGiven:", show y]]

    show (NotBound x)
      = unwords ["Undeclared variable:", x]

    show (VectorExpected)
      = "Vector Expected"

    show (PortChanExpected)
      = "Port or Wire Expected"

    show (PortExpected)
      = "Port Expected"

    show (ErrI msg)
      = "Internal Err: " <+> msg
    show (OOB x y)
      = unwords ["Out of Bounds:" , show x, "is not within", show y]

    show (Err x y) = unwords [show x, show y]

namespace NetList

  public export
  data Error = TyCheck Check.Error
             | Parse   String (ParseError Token)
             | Sound   (Graph String) (HasExactDegree.Error String)

  export
  Show (NetList.Error) where
    show (TyCheck x) = show x
    show (Parse f n) = show @{circuitspe} n
    show (Sound g e)
      = unlines ["// LOG : Soundness Error:", showErr (g, e)]

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module NatProps

import Basic
import Unit
import Void
import Coproduct
import Nat
import Sigma
import Path
import CoproductProps
import PreorderReasoning
import General
import Dec

%default total

NegN : (n : Nat) -> Type -> Type
NegN Z p = p
NegN (S k) p = Neg (NegN k p)

dni : p -> NegN N.two p
dni a u = u a

contrapositive : (a -> b) -> (Neg b -> Neg a)
contrapositive f v a = v (f a)

tno : NegN N.three p -> Neg p
tno = contrapositive dni

absurdityX3IsAbsurdity : {p : _} -> NegN N.three p <=> Neg p
absurdityX3IsAbsurdity = firstly # secondly
 where
  firstly : NegN N.three p -> Neg p
  firstly = tno

  secondly : Neg p -> NegN N.three p
  secondly = dni

PositiveNotZero : (x : Nat) -> S x /= Z
-- p : S x == Z
PositiveNotZero x p = UnitNotVoid (g p)
 where
  f : Nat -> Type
  f Z = Void
  f (S _) = Unit

  g : S x == Z -> Unit == Void
  g = ap f

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

SuccLeftCancel : {x, y : _} -> S x == S y -> x == y
SuccLeftCancel = ap pred

NatNotSuccNat : (x : Nat) -> x /= S x
NatNotSuccNat Z = negSym (PositiveNotZero Z)
NatNotSuccNat (S k) = let r = NatNotSuccNat k in \l =>
  r (SuccLeftCancel l)

-- Proof that Nat has decidable equality.
-- Doesn't use pattern matching.
-- OMG
-- You'll never know the true value of pattern matching
-- until you are left without it (as an exercise).
namespace NatDec
  Lemma0 : {x, y : _} -> x == y -> (S x /= y)
  Lemma0 p = J (\x, y, _ => (S x /= y))
    (\x => negSym (NatNotSuccNat x)) x y p

  Lemma1 : {x, y : _} -> Dec (x == y) -> Dec (S x == S y)
  Lemma1 = SumInduction (const $ Dec (S x == S y))
    (\p => Inl (ap S p))
    (\p => Inr (\l => p (SuccLeftCancel l)))

  export
  NatDecEq : DecEq Nat
  NatDecEq x y = NatInduction (\x => (y : Nat) -> (x == y) + (x /= y))
    -- p0 : (y : Nat) -> (Z == y) + (Z /= y)
    (\y => (NatInduction (\y => (Z == y) + (Z /= y))
      -- p0
      (Inl $ Refl Z)
      -- pn
      (\y, _ => Inr (negSym $ PositiveNotZero y))
      --n
      y))
    -- pn : (x : Nat) -> (y : Nat) -> (S x == y) + (S x /= y)
    -- hyp : Dec (x == y)
    (\x, hyp, y =>
      NatInduction (\y => (S x == y) + (S x /= y))
        --p0
        (Inr (PositiveNotZero x))
        --pn
        (\y, _ => Lemma1 $ hyp y)
        --n
        y)
    x y

plusAssoc : (x, y, z : Nat) -> (x + y) + z == x + (y + z)
plusAssoc  Z    y z = Chain $ ||  (Z + y) + z
                             |=> Z + (y + z)     ...(Refl _)
plusAssoc (S x) y z = Chain $ ||  (S x + y) + z
                             |=> S ((x + y) + z) ...(Refl _)
                             |=> S (x + (y + z)) ...(ap S $ plusAssoc x y z)
                             |=> (S x + (y + z)) ...(Refl _)

BaseOnRight : (x : Nat) -> x + Z == x
BaseOnRight Z = Refl _
BaseOnRight (S x) = ap S (BaseOnRight x)

StepOnRight : (x, y : Nat) -> x + S y == S (x + y)
-- goal : S y == S (Z + y)
StepOnRight Z y = Refl _
-- goal : S (x + S y) == S (S (x + y))
StepOnRight (S x) y = Chain $ ||  S (x + S y)
                             |=> S (S (x + y)) ...(ap S $ StepOnRight x y)

PlusComm : (x, y : Nat) -> x + y == y + x
PlusComm x Z = BaseOnRight x
-- goal : x + S y == S (y + x)
PlusComm x (S y) = Chain $ ||  x + S y
                          |=> S (x + y) ...(StepOnRight x y)
                          |=> S (y + x) ...(ap S $ PlusComm x y)

OnLhs : {x, y, z : _} -> x == z -> x == y -> z == y
OnLhs p q = sym p . q

OnRhs : {x, y, z : _} -> y == z -> x == y -> x == z
OnRhs p q = q . p

PlusRightCancel : (x, y, z : Nat) -> x + y == z + y -> x == z
-- goal : x == z
-- prf  : x + Z == z + Z
PlusRightCancel x Z z prf = Chain $ ||  x
                                   |=> x + Z   ...(sym $ BaseOnRight x)
                                   |=> z + Z   ...prf
                                   |=> z       ...(BaseOnRight z)
-- goal : x == z
-- prf : x + S y == z + S y
-- prf' : TypeOf prf -> x + y == z + y
-- hyp : x + y == z + y -> x == z
PlusRightCancel x (S y) z prf =
  let prf' =
    Chain $ ||  x + S y == z + S y
            |=> S (x + y) == z + S y   ...(OnLhs $ StepOnRight x y)
            |=> S (x + y) == S (z + y) ...(OnRhs $ StepOnRight z y)
            |=> x + y == z + y         ...SuccLeftCancel
          $
            prf
  in PlusRightCancel x y z prf'

||| Alternative definition of non-strict inequality.
Lte' : Nat -> Nat -> Type
Lte' x y = Sigma Nat (\z => z + x == y)

LteImpliesLte' : (x, y : Nat) -> x <= y -> Lte' x y
LteImpliesLte' Z y _ = y # (Chain $ ||  y + Z
                                    |=> Z + y ...(PlusComm y Z))
LteImpliesLte' (S _) Z l = VoidRecursion _ l
-- prf  : z + x == y
-- goal : z + S x == S y
LteImpliesLte' (S x) (S y) l = let z # prf = LteImpliesLte' x y l in
  let prf' = Chain $ ||     z +   x ==   y
                      |=>   x +   z ==   y ...(OnLhs $ PlusComm z x)
                      |=> S x +   z == S y ...(ap S)
                      |=>   z + S x == S y ...(OnLhs $ PlusComm (S x) z)
                   $ prf
  in  z # prf'

Lte'ImpliesLte : (x, y : Nat) -> Lte' x y -> x <= y
Lte'ImpliesLte Z _ _ = ()
Lte'ImpliesLte (S x) Z (z # contra) =
  let contra' = OnLhs (PlusComm z (S x)) contra in
  let p = PositiveNotZero (x + z) in
  p contra'
Lte'ImpliesLte (S x) (S y) (z # prf) =
  let prf' = Chain $ ||  z + S x == S y
                     |=> S x + z == S y ...(OnLhs $ PlusComm z (S x))
                     |=> x + z == y ...(ap pred)
                     |=> z + x == y ...(OnLhs $ PlusComm x z)
                   $ prf in
  Lte'ImpliesLte x y (z # prf')

LogicallyEqualivalentLte : (x, y : Nat) -> x <= y <=> Lte' x y
LogicallyEqualivalentLte x y = LteImpliesLte' x y
                             # Lte'ImpliesLte x y

LteRefl : (n : Nat) -> n <= n
LteRefl Z = ()
LteRefl (S n) = LteRefl n

LteTrans : (l, m, n : Nat) -> l <= m -> m <= n -> l <= n
LteTrans Z m n q p = ()
LteTrans (S l) Z n q p = VoidRecursion _ q
LteTrans (S l) (S m) Z q p = VoidRecursion _ p
LteTrans (S l) (S m) (S n) q p = LteTrans l m n q p

LteAnti : (m, n : Nat) -> m <= n -> n <= m -> m == n
LteAnti Z Z q p = Refl Z
LteAnti (S m) Z q p = VoidRecursion _ q
LteAnti Z (S n) q p = VoidRecursion _ p
LteAnti (S m) (S n) q p = ap S $ LteAnti m n q p

LteSucc : (n : Nat) -> n <= S n
LteSucc Z = ()
LteSucc (S n) = LteSucc n

ZeroMinimal : (n : Nat) -> Z <= n
ZeroMinimal _ = ()

UniqueMinimal : (n : Nat) -> n <= Z -> n == Z
UniqueMinimal Z p = Refl Z
UniqueMinimal (S n) p = VoidRecursion _ p

LteSplit : (m, n : Nat) -> m <= S n -> (m <= n) + (m == S n)
LteSplit Z n p = Inl ()
LteSplit (S m) Z p with (UniqueMinimal _ p)
 LteSplit (S Z) Z p | Refl _ = Inr (Refl (S Z))
LteSplit (S m) (S n) p = let H = LteSplit m n p in
  case H of
    Inl p => Inl p
    Inr p => Inr (ap S p)

LteSplit' : (m, n : Nat) -> m <= n -> (S m <= n) + (m == n)
LteSplit' Z Z p = Inr (Refl Z)
LteSplit' Z (S n) p = Inl ()
LteSplit' (S m) Z p = VoidRecursion _ p
LteSplit' (S m) (S n) p =
  case LteSplit' m n p of
    Inl x => Inl x
    Inr x => Inr (ap S x)

infixl 1 <

(<) : Nat -> Nat -> Type
x < y = S x <= y

NotLtGivesLte : (m, n : Nat) -> Neg (n < m) -> m <= n
NotLtGivesLte Z n _ = ()
NotLtGivesLte (S m) Z p = p ()
NotLtGivesLte (S m) (S n) p = NotLtGivesLte m n p

BoundedForallNext : (p : Nat -> Type)
                 -> (k : Nat)
                 -> p k
                 -> ((n : Nat) -> n < k -> p n)
                 -> (n : Nat) -> n < S k -> p n
BoundedForallNext p k pk f n l with (LteSplit' n k l)
 BoundedForallNext p k pk f n l | Inl prf = f n prf
 BoundedForallNext p k pk f k l | Inr (Refl _) = pk

||| The type of roots of a function.
Root : (Nat -> Nat) -> Type
Root f = Sigma Nat (\n => f n == Z)

HasNoRootLt : (Nat -> Nat) -> Nat -> Type
HasNoRootLt f k = (n : Nat) -> n < k -> f n /= Z

IsMinimalRoot : (Nat -> Nat) -> Nat -> Type
IsMinimalRoot f m = Pair (f m == Z) (f `HasNoRootLt` m)

AtMostOneMinimalRoot : (f : Nat -> Nat)
                    -> (m, n : Nat)
                    -> IsMinimalRoot f m
                    -> IsMinimalRoot f n
                    -> m == n
-- prfm : forall n. n < m -> f n == Z -> Void
-- prfn : forall m. m < n -> f m == Z -> Void
AtMostOneMinimalRoot f m n (rm # prfm) (rn # prfn) = c _ _ a b
 where
  a : Neg (m < n)
  a contra = prfn m contra rm

  b : Neg (n < m)
  b contra = prfm n contra rn

  c : (m, n : Nat) -> Neg (m < n) -> Neg (n < m) -> m == n
  c m n q q' = LteAnti m n (NotLtGivesLte _ _ q') (NotLtGivesLte _ _ q)

MinimalRoot : (Nat -> Nat) -> Type
MinimalRoot f = Sigma Nat (IsMinimalRoot f)

MinimalRootIsRoot : MinimalRoot f -> Root f
MinimalRootIsRoot (r # prf # _) = r # prf

BoundedNatSearch : (k, f : _) -> MinimalRoot f + (f `HasNoRootLt` k)
BoundedNatSearch Z f = Inr (\_, v, _ => v)
BoundedNatSearch (S k) f = SumRecursion _ Inl y
  (BoundedNatSearch k f)
 where
  A : Nat -> (Nat -> Nat) -> Type
  A k f = MinimalRoot f + (f `HasNoRootLt` k)

  y : f `HasNoRootLt` k -> A (S k) f
  y u = SumRecursion _ y0 y1 (NatDecEq (f k) Z)
   where
    y0 : f k == Z -> A (S k) f
    y0 p = Inl (k # p # u)

    y1 : f k /= Z -> A (S k) f
    y1 v = Inr (BoundedForallNext (\n => f n /= Z) k v u)

RightFailsGivesLeftHolds : {P, Q : Type} -> P + Q -> Neg Q -> P
RightFailsGivesLeftHolds (Inl p) u = p
RightFailsGivesLeftHolds (Inr q) u = VoidRecursion _ (u q)

RootGivesMinimalRoot : (f : _) -> Root f -> MinimalRoot f
RootGivesMinimalRoot f (n # p) = y
 where
  g : Neg (f `HasNoRootLt` S n)
  g phi = phi n (LteRefl n) p

  y : MinimalRoot f
  y = RightFailsGivesLeftHolds (BoundedNatSearch (S n) f) g


text:
module Main

data State : (stateType : Type) -> Type -> Type where
  Get : State stateType stateType
  Put : stateType -> State stateType ()

  Pure : ty -> State stateType ty
  Bind : State stateType a -> (a -> State stateType b) -> State stateType b

(>>=) : State stateType a -> (a -> State stateType b) -> State stateType b
(>>=) = Bind

runState : State stateType a -> (st : stateType) -> (a, stateType)
runState Get              st = (st, st)
runState (Put newState)   st = ((), newState)
runState (Pure x)         st = (x, st)
runState (Bind cmd prog)  st =
  let (val, nextState) = runState cmd st
  in runState (prog val) nextState

Functor (State stateType) where
  map func x = Bind x (\val => Pure (func val))

Applicative (State stateType) where
  pure      = Pure
  (<*>) f a =
    Bind f (\f' =>
    Bind a (\a' =>
    Pure (f' a')))

Monad (State stateType) where
  (>>=) = Bind

data Tree a = Empty
            | Node (Tree a) a (Tree a)

Show a => Show (Tree a) where
  show Empty = "Empty"
  show (Node left val right) = "(Node " ++ show left ++ " " ++ show val ++ " " ++ show right ++ ")"

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty)
                      "Fred"
                      (Node Empty "Sheila" Empty))
                "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

treeLabelWith : Tree a -> State (Stream labelType) (Tree (labelType, a))
treeLabelWith Empty = Pure Empty
treeLabelWith (Node left val right) = do
  leftLabelled <- treeLabelWith left
  (this :: rest) <- Get
  Put rest
  rightLabelled <- treeLabelWith right
  Pure (Node leftLabelled (this, val) rightLabelled)

treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = fst (runState (treeLabelWith tree) [1..])

main : IO ()
main = do
  printLn $ treeLabel testTree

max_stars_repo_name: luc-tielen/idris-grin

max_issues_repo_name: luc-tielen/idris-grin

max_forks_repo_name: luc-tielen/idris-grin