text:
module Sub13Apply108x36

import ProofColDivSeqBase
import ProofColDivSeqPostulate
import ProofColDivSeqPostuProof

%default total
-- %language ElabReflection

-- 3(36x+12) --F[5,-2]->B[1,-2]--> 3(16x+5)
export
apply108x36 : (Not . P) (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                    (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                              (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                        (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                  (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))),
         (Not . P) m))
apply108x36 {o} col = ((S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))
                                                           ** (lte108x36 o, fb108x36To48x15 o col)) where
  lte108x36 : (o:Nat) -> LTE (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                  (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))
          (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                     (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                               (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))
  lte108x36 Z = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte108x36 (S o) = let lemma = lte108x36 o in

    rewrite (sym (plusSuccRightSucc o o)) in

    rewrite (sym (plusSuccRightSucc (plus o o)  (S (plus o o)))) in
    rewrite (sym (plusSuccRightSucc (plus o o)  (plus o o))) in

    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (S (plus (plus o o) (plus o o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (S (plus (plus o o) (plus o o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (S (plus (plus o o) (plus o o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) (plus o o))  (plus (plus o o) (plus o o)))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (S (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))  (plus (plus (plus o o) (plus o o))
                                                            (plus (plus o o) (plus o o))))) in

    rewrite (sym (plusSuccRightSucc (plus o o)  o)) in

    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (S (plus (plus o o) o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (plus (plus o o) o)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (plus (plus o o) o))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (S (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))
              (S (plus (plus (plus o o) o) (plus (plus o o) o))))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                               (S (plus (plus (plus o o) o) (plus (plus o o) o))))
              (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                    (S (plus (plus (plus o o) o)
                                                  (plus (plus o o) o)))))))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                           (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
              (S (S (plus (plus (plus (plus o o) o)
                                                             (plus (plus o o) o)) (S (plus (plus (plus o o)
                                                                      o)
                                                                (plus (plus o o)
                                                                      o)))))))) in

      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
module Data.Prim.Bits16

import public Control.WellFounded
import public Data.DPair
import public Data.Prim.Ord
import public Algebra.Solver.Ring
import Syntax.PreorderReasoning

%default total

unsafeRefl : a === b
unsafeRefl = believe_me (Refl {x = a})

--------------------------------------------------------------------------------
--          (<)
--------------------------------------------------------------------------------

||| Witness that `m < n === True`.
export
data (<) : (m,n : Bits16) -> Type where
  LT : {0 m,n : Bits16} -> (0 prf : (m < n) === True) -> m < n

||| Contructor for `(<)`.
|||
||| This can only be used in an erased context.
export %hint
0 mkLT : (0 prf : (m < n) === True) -> m < n
mkLT = LT

||| Extractor for `(<)`.
|||
||| This can only be used in an erased context.
export
0 runLT : m < n -> (m < n) === True
runLT (LT prf) = prf

||| We don't trust values of type `(<)` too much,
||| so we use this when creating magical results.
export
strictLT : (0 p : m < n) -> Lazy c -> c
strictLT (LT prf) x = x

--------------------------------------------------------------------------------
--          Aliases
--------------------------------------------------------------------------------

||| Flipped version of `(<)`.
public export
0 (>) : (m,n : Bits16) -> Type
m > n = n < m

||| `m <= n` mean that either `m < n` or `m === n` holds.
public export
0 (<=) : (m,n : Bits16) -> Type
m <= n = Either (m < n) (m === n)

||| Flipped version of `(<=)`.
public export
0 (>=) : (m,n : Bits16) -> Type
m >= n = n <= m

||| `m /= n` mean that either `m < n` or `m > n` holds.
public export
0 (/=) : (m,n : Bits16) -> Type
m /= n = Either (m < n) (m > n)

--------------------------------------------------------------------------------
--          Order
--------------------------------------------------------------------------------

0 ltNotEQ : m < n -> Not (m === n)
ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")

0 ltNotGT : m < n -> Not (n < m)
ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")

0 eqNotLT : m === n -> Not (m < n)
eqNotLT = flip ltNotEQ

export
comp : (m,n : Bits16) -> Trichotomy (<) m n
comp m n = case prim__lt_Bits16 m n of
  0 => case prim__eq_Bits16 m n of
    0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
    x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)

export
Total Bits16 (<) where
  trichotomy   = comp
  transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl

--------------------------------------------------------------------------------
--          Bounds and Well-Foundedness
--------------------------------------------------------------------------------

||| Lower bound of `Bits16`
public export
MinBits16 : Bits16
MinBits16 = 0

||| Upper bound of `Bits16`
public export
MaxBits16 : Bits16
MaxBits16 = 0xffff

||| `m >= 0` for all `m` of type `Bits16`.
export
0 GTE_MinBits16 : (m : Bits16) -> m >= MinBits16
GTE_MinBits16 m = case comp MinBits16 m of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total $ idris_crash "IMPOSSIBLE: Bits16 smaller than 0"

||| Not value of type `Bits16` is less than zero.
export
0 Not_LT_MinBits16 : m < 0 -> Void
Not_LT_MinBits16 = GTE_not_LT (GTE_MinBits16 m)

||| `m <= MaxBits16` for all `m` of type `Bits16`.
export
0 LTE_MaxBits16 : (m : Bits16) -> m <= MaxBits16
LTE_MaxBits16 m = case comp m MaxBits16 of
  LT x f g => %search
  EQ f x g => %search
  GT f g x => assert_total
            $ idris_crash "IMPOSSIBLE: Bits16 greater than \{show MaxBits16}"

||| Not value of type `Bits16` is greater than `MaxBits16`
export
0 Not_GT_MaxBits16 : m > MaxBits16 -> Void
Not_GT_MaxBits16 = LTE_not_GT (LTE_MaxBits16 m)

||| Every value of type `Bits16` is accessible with relation
||| to `(<)`.
export
accessLT : (m : Bits16) -> Accessible (<) m
accessLT m = Access $ \n,lt => accessLT (assert_smaller m n)

||| `(<)` is well founded.
export %inline
WellFounded Bits16 (<) where
  wellFounded = accessLT

||| Every value of type `Bits16` is accessible with relation
||| to `(>)`.
export
accessGT : (m : Bits16) -> Accessible (>) m
accessGT m = Access $ \n,gt => accessGT (assert_smaller m n)

||| `(>)` is well founded.
export %inline
[GT] WellFounded Bits16 (>) where
  wellFounded = accessGT

--------------------------------------------------------------------------------
--          Arithmetics
--------------------------------------------------------------------------------

||| Safe division.
|||
||| This uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
export %inline
sdiv : (n,d : Bits16) -> (0 prf : 0 < d) => Bits16
sdiv n d = n `div` d

||| Refined division.
|||
||| This comes with a proof that the result is
||| strictly smaller than `n`.
|||
||| This uses `0 < n` as a constraint instead
||| of `0 /= n`, because in my experience, the former
||| is much more useful.
export %inline
rdiv :  (n,d : Bits16)
     -> (0 dgt1 : 1 < d)
     => (0 ngt0 : 0 < n)
     => Subset Bits16 (< n)
rdiv n d = Element (n `div` d) (LT unsafeRefl)

||| Safe modulo.
|||
||| This uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
|||
||| If you need the postcondition that the result is strictly
||| smaller than `d`, use `rmod` instead.
export %inline
smod : (n,d : Bits16) -> (0 prf : 0 < d) => Bits16
smod n d = n `mod` d

||| Refined modulo.
|||
||| This comes with a proof that the result is strictly smaller
||| than `d`.
|||
||| It uses `0 < d` as a constraint instead
||| of `0 /= d`, because in my experience, the former
||| is much more useful.
export %inline
rmod : (n,d : Bits16) -> (0 prf : 0 < d) => Subset Bits16 (< d)
rmod n d = Element (n `mod` d) (LT unsafeRefl)

ext: idr


text:
module RingExamples

import Ring
import RingProperties
import Group
import Group_property
import ZZ
import ZZUtils
import Monoid

%access public export

ZZAbGrp: IsAbelianGrp ZZ (+)
ZZAbGrp = ((Assoc, (((Pos Z)**PrfZ), (((Pos Z)**PrfZ)**PfInv))), CommutativeZ) where
  Assoc: (l,c,r:ZZ) -> (l+c)+r = l +(c+r)
  Assoc l c r = sym (plusAssociativeZ l c r)
  PrfZ: (a: ZZ) -> (a+(Pos Z) = a, (Pos Z) + a = a)
  PrfZ a = (plusZeroRightNeutralZ a, plusZeroLeftNeutralZ a)
  PfInv: (a: ZZ) -> DPair ZZ (\a_inv => ((a + a_inv = Pos Z), (a_inv + a = Pos Z)))
  PfInv a = MkDPair (negate a) (plusNegateInverseLZ a, plusNegateInverseRZ a)
  CommutativeZ: (a: ZZ) -> (b: ZZ) -> (a + b = b+a)
  CommutativeZ = plusCommutativeZ

ZZAssoc: Associative ZZ (*)
ZZAssoc l c r = sym (multAssociativeZ l c r)

ZZDist: IsDistributive ZZ (+) (*)
ZZDist l c r = (multDistributesOverPlusRightZ l c r, multDistributesOverPlusLeftZ c r l)

ZZMultCommutes: Commutative ZZ (*)
ZZMultCommutes = multCommutativeZ

ZZIsCRing: IsCommRing ZZ (+) (*)
ZZIsCRing = ((ZZAbGrp, (ZZAssoc, ZZDist)), ZZMultCommutes)

ZZCRing: CRing ZZ
ZZCRing = MkCRing ZZ (+) (*) ZZIsCRing


text:
module Test.SemVar.DataTest

import IdrTest.Test
import IdrTest.Expectation

import Data.List

import SemVar
import SemVar.Data
import SemVar.Parser

repeat : a -> Nat -> List a
repeat _ Z = []
repeat x (S n) = x :: repeat x n

satisfySpecs : List (String, List String, List String)
satisfySpecs =
  [
    (
      "~1.2.3",
      ["1.2.3", "1.2.99"],
      ["1.2.3-prerelease+commit", "1.3.0", "1.3.1"]
    ),
    (
      "^1.2.3",
      ["1.2.3", "1.3.99"],
      ["1.2.3-prerelease+commit", "2.0.0", "5.3.1"]
    )
  ]

export
suite : Test
suite =
  let
    satisfyTests =
      concat $ map (\(reqText, sat, unsat) =>
        let
          reqM = parseRequirement reqText
          satZ = zip sat (repeat True (length sat))
          unsatZ = zip unsat (repeat False (length unsat))
        in
          map (\(v, isSat) =>
            let
              verb = if isSat then " satisfies " else " does not satisfy "
              testName = v ++ verb ++ reqText
            in
              case (parseVersion v, reqM) of
                (Just version, Just req) =>
                  test testName (\_ => assertEq (desc isSat) (desc (satisfy req version)))
                _ =>
                  test testName (\_ => assertEq "Failed to parse test" "")
          )
          (satZ ++ unsatZ)
      ) satisfySpecs
  in
    describe "Data Tests"
      [ describe "Satisfy Specs" satisfyTests
      ]
  where
    desc : Bool -> String
    desc True = "sat"
    desc False = "unsat"

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
import Protocol
import Data.List

%language TypeProviders
%default total

-- A type that enforces valid steps.
%provide (Route : ((String, String) -> Type)) with Protocol "steps.txt"

-- An example implementation of our finite state machine.
door : Route ("locked", "opened")
door = do Begin
--        Then $ Choose ("locked", "opened") -> Won't compile as it's not a valid step.
          Then $ Choose ("locked", "closed")
          Then $ Choose ("closed", "closed")
          Then $ Choose ("closed", "opened")

max_stars_repo_name: ctford/elba

max_issues_repo_name: ctford/elba

max_forks_repo_name: ctford/elba


text:
-- --------------------------------------------------------------- [ DList.idr ]
-- Module    : DList.idr
-- Copyright : (c) 2015,2016,2017 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| A `list` construct to create lists of dependent types.
|||
||| One of the problems with using dependent types is that types
||| depend on values. This affects the ability to construct lists of
||| values that have a dependent type. The existing `List` type cannot
||| be used as it requires all elements to have the same type.
module Data.DList

import Data.List

%access export

using (aTy : Type, elemTy : (aTy -> Type), x : aTy)

  ||| A list construct for dependent types.
  |||
  ||| @aTy    The type of the value contained within the list element type.
  ||| @elemTy The type of the elements within the list
  ||| @as     The List used to contain the different values within the type.
  public export
  data DList : (aTy : Type)
            -> (elemTy : aTy -> Type)
            -> (as : List aTy)
            -> Type where
    ||| Create an empty List
    Nil  : DList aTy elemTy Nil
    ||| Cons
    |||
    ||| @elem The element to add
    ||| @rest The list for `elem` to be added to.
    (::) : (elem : elemTy x)
        -> (rest : DList aTy elemTy xs)
        -> DList aTy elemTy (x::xs)

%name DList rest

-- -------------------------------------------------------------- [ Form Tests ]
isNil : DList aTy eTy as -> Bool
isNil Nil     = True
isNil (x::xs) = False

isCons : DList aTy eTy as -> Bool
isCons l = isNil l == False

-- ------------------------------------------- [ Predicates that are Decidable ]

public export
data NonEmpty : (xs : DList aTy eTy as) -> Type where
  IsNonEmpty : DList.NonEmpty (x::rest)

Uninhabited (DList.NonEmpty []) where
  uninhabited IsNonEmpty impossible

nonEmpty : (xs : DList aTy eTy as) -> Dec (NonEmpty xs)
nonEmpty Nil            = No absurd
nonEmpty (elem :: rest) = Yes IsNonEmpty

public export
data InBounds : (idx : Nat)
             -> (xs  : DList aTy eTy as)
             -> Type
  where
    InFirst : DList.InBounds Z (x::rest)
    InLater : (later : DList.InBounds idx rest)
           -> DList.InBounds (S idx) (x :: rest)

Uninhabited (DList.InBounds idx []) where
  uninhabited InFirst impossible
  uninhabited (InLater _) impossible

inBounds : (idx : Nat)
        -> (xs  : DList aTy eTy as)
        -> Dec (InBounds idx xs)
inBounds idx Nil = No uninhabited
inBounds Z (elem :: rest) = Yes InFirst
inBounds (S k) (elem :: rest) with (inBounds k rest)
  inBounds (S k) (elem :: rest) | (Yes prf) = Yes $ InLater prf
  inBounds (S k) (elem :: rest) | (No contra) =
      No (\p => case p of
                   InLater y => contra y)

-- ------------------------------------------------------------------ [ Length ]

public export
length : DList aTy eTy as -> Nat
length Nil     = Z
length (x::xs) = (S Z) + length xs

Sized (DList aTy eTy as) where
  size = length

-- ---------------------------------------------------------------- [ Indexing ]

public export
index : (idx : Nat)
     -> (xs  : DList aTy eTy as)
     -> {auto ok : InBounds idx xs}
     -> {auto ok' : List.InBounds idx as}
     -> eTy (index idx as)
index Z (y :: rest) {ok = InFirst} = y
index (S k) (y :: rest) {ok = (InLater later)} {ok' = (InLater x)} = index k rest

public export
head : (xs : DList aTy eTy (a::as))
    -> {auto ok : NonEmpty xs}
    -> {auto ok' : NonEmpty (a::as)}
    -> eTy a
head (y :: rest) {ok = IsNonEmpty} {ok' = IsNonEmpty} = y

public export
tail : (xs : DList aTy eTy (a :: as))
    -> {auto ok : NonEmpty xs}
    -> (DList aTy eTy as)
tail (x :: rest) {ok = IsNonEmpty} = rest

public export
last : (xs : DList aTy eTy as)
    -> {auto ok : NonEmpty xs}
    -> {auto ok' : NonEmpty as}
    -> eTy (last as)
last [] {ok = IsNonEmpty} {ok' = _} impossible
last (elem :: []) {ok = ok} {ok' = ok'} = elem
last (elem :: (y :: rest)) {ok = ok} {ok' = ok'} = last (y::rest)

public export
init : (xs : DList aTy eTy as)
    -> {auto ok  : NonEmpty xs}
    -> {auto ok' : NonEmpty as}
    -> DList aTy eTy (init as)
init [] {ok = IsNonEmpty} {ok' = _} impossible
init (elem :: []) {ok = ok} {ok' = ok'} = []
init (elem :: (y :: rest)) {ok = ok} {ok' = ok'} = elem :: init (y::rest)

-- --------------------------------------------------------- [ Bob The Builder ]

public export
(++) : DList aTy eTy xs
    -> DList aTy eTy ys
    -> DList aTy eTy (xs ++ ys)
(++) Nil     ys = ys
(++) (x::xs) ys = x :: (xs ++ ys)

public export
replicate : (n : Nat)
         -> elemTy a
         -> DList aTy elemTy (replicate n a)
replicate Z x = Nil
replicate (S k) x = x :: replicate k x

-- ---------------------------------------------------------------- [ SubLists ]

public export
take : (n : Nat)
    -> DList aTy elemTy as
    -> DList aTy elemTy (take n as)
take Z rest = Nil
take (S k) [] = []
take (S k) (elem :: rest) = elem :: take k rest

takeWhile : ({a : aTy} -> elemTy a -> Bool)
         -> DList aTy elemTy as
         -> (bs : List aTy ** DList aTy elemTy bs)
takeWhile p Nil     = (_ ** Nil)
takeWhile p (x::xs) =
    if p x
      then (_ ** DList.(::) x (snd (takeWhile p xs)))
      else (_ ** Nil)

public export
drop : (n : Nat)
    -> DList aTy elemTy as
    -> DList aTy elemTy (drop n as)
drop Z     rest = rest
drop (S k) [] = []
drop (S k) (elem :: rest) = drop k rest

dropWhile : ({a : aTy} -> elemTy a -> Bool)
         -> DList aTy elemTy as
         -> (bs : List aTy ** DList aTy elemTy bs)
dropWhile p Nil     = (_ ** Nil)
dropWhile p (x::xs) =
    if p x
      then dropWhile p xs
      else (_ ** DList.(::) x xs)

-- ---------------------------------------------------------------- [ Equality ]

eqDList : ({a,b : aTy} -> elemTy a -> elemTy b -> Bool)
       -> DList aTy elemTy as
       -> DList aTy elemTy bs
       -> Bool
eqDList _ Nil     Nil     = True
eqDList p (x::xs) (y::ys) =
  if p x y
    then eqDList p xs ys
    else False
eqDList _ _       _       = False

-- ------------------------------------------------------------------- [ Order ]

cmpDList : ({a,b : aTy} -> elemTy a -> elemTy b -> Bool)
        -> ({a,b : aTy} -> elemTy a -> elemTy b -> Ordering)
        -> DList aTy elemTy as
        -> DList aTy elemTy bs
        -> Ordering
cmpDList _  _   Nil     Nil     = EQ
cmpDList _  _   Nil     _       = LT
cmpDList _  _   _       Nil     = GT
cmpDList eq cmp (x::xs) (y::ys) =
  if not $ eq x y
    then cmp x y
    else cmpDList eq cmp xs ys

-- ----------------------------------------------------------------- [ Folding ]
-- TODO

foldr : ({a : aTy} -> elemTy a -> p -> p)
     -> p
     -> DList aTy elemTy as
     -> p
foldr f init Nil     = init
foldr f init (x::xs) = f x (DList.foldr f init xs)

foldl : ({a : aTy} -> p -> elemTy a -> p)
      -> p
      -> DList aTy elemTy as
      -> p
foldl f init Nil = init
foldl f init (x::xs) = DList.foldl f (f init x) xs

-- ----------------------------------------------------------------- [ Functor ]

map : ({a : aTy} -> elemTy a -> b)
       -> DList aTy elemTy as
       -> List b
map f Nil     = List.Nil
map f (x::xs) = with List f x :: DList.map f xs

-- TODO map from one DList to another.

mapMaybe : ({a : aTy} -> elemTy a -> Maybe b)
         -> DList aTy elemTy as
         -> List b
mapMaybe f Nil     = Nil
mapMaybe f (x::xs) =
  case f x of
    Nothing => mapMaybe f xs
    Just y  => y :: mapMaybe f xs

concatMap : Monoid m
         => (func : {a : aTy} -> elemTy a -> m)
         -> (xs : DList aTy elemTy as)
         -> m
concatMap f = foldr (\e, res => f e <+> res) neutral

-- --------------------------------------------------------- [ Transformations ]
-- TODO

||| From list of Dependent Pairs.
fromLDP : List (x : aTy ** eTy x)
       -> (as ** DList aTy eTy as)
fromLDP Nil     = (_ ** DList.Nil)
fromLDP (x::xs) = (_ ** DList.(++) [snd x] (snd $ fromLDP xs))

-- ---------------------------------------------- [ To List of Dependent Pairs ]

||| To List of Dependent Pairs
toLDP : DList aTy eTy as
     -> List (x : aTy ** eTy x)
toLDP Nil     = Nil
toLDP (x::xs) = (_**x) :: toLDP xs

||| List to DList
fromList : {ty : Type}
        -> {e : ty -> Type}
        -> {x : ty}
        -> (es : List (e x))
        -> DList ty e (replicate (length es) x)
fromList [] = Nil
fromList (x :: xs) = x :: fromList xs

-- -------------------------------------------------------- [ Membership Tests ]

any : ({a : aTy} -> elemTy a -> Bool)
   -> DList aTy elemTy as
   -> Bool
any p = DList.foldr (\e,res => res || p e) False

all : ({a : aTy} -> elemTy a -> Bool)
   -> DList aTy elemTy as
   -> Bool
all p = DList.foldr (\e,res => res && p e) True

elemBy : ({a,b : aTy} -> elemTy a -> elemTy b -> Bool)
      -> elemTy a
      -> DList aTy elemTy as
      -> Bool
elemBy p e = any (\x => p e x)

-- TODO elem

hasAnyBy : ({a,b : aTy} -> elemTy a -> elemTy b -> Bool)
         -> DList aTy elemTy as
         -> DList aTy elemTy bs
         -> Bool
hasAnyBy p es  Nil     = False
hasAnyBy p Nil es      = False
hasAnyBy p es  (x::xs) =
  if elemBy p x es
    then True
    else hasAnyBy p es xs

-- TODO hasAny

-- --------------------------------------------------------------- [ Searching ]

find : ({a : aTy} -> elemTy a -> Bool)
    -> DList aTy elemTy as
    -> Maybe $ DPair aTy elemTy
find p Nil     = Nothing
find p (x::xs) =
  if p x
    then Just (_ ** x)
    else find p xs

private
findIndex' : Nat
          -> ({a : aTy} -> elemTy a -> Bool)
          -> DList aTy elemTy as
          -> Maybe Nat
findIndex' cnt p Nil     = Nothing
findIndex' cnt p (x::xs) =
    if p x
      then Just cnt
      else findIndex' (S cnt) p xs

findIndex : ({a : aTy} -> elemTy a -> Bool)
         -> DList aTy elemTy as
         -> Maybe Nat
findIndex = findIndex' Z

private
findIndices' : Nat
            -> ({a : aTy} -> elemTy a -> Bool)
            -> DList aTy elemTy as
            -> List Nat
findIndices' cnt p Nil     = Nil
findIndices' cnt p (x::xs) =
    if p x
      then cnt :: findIndices' (S cnt) p xs
      else findIndices' (S cnt) p xs

findIndices : ({a : aTy} -> elemTy a -> Bool)
           -> DList aTy elemTy as
           -> List Nat
findIndices = findIndices' Z

elemIndexBy : ({a,b : aTy} -> elemTy a -> elemTy b -> Bool)
            -> elemTy a
            -> DList aTy elemTy as
            -> Maybe Nat
elemIndexBy p e = findIndex (\x => p e x)

-- TODO elemIndex

elemIndicesBy : ({a,b : aTy} -> elemTy a -> elemTy b -> Bool)
              -> elemTy a
              -> DList aTy elemTy as
              -> List Nat
elemIndicesBy p e = findIndices (\x => p e x)

-- TODO elemIndicies

-- ------------------------------------------------------------- [ Conversions ]
-- TODO

-- ----------------------------------------------------------------- [ Filters ]
-- TODO

-- ------------------------------------------------------------ [ Partitioning ]
-- TODO

span : ({a : aTy} -> elemTy a -> Bool)
    -> DList aTy elemTy xys
    -> ((xs ** DList aTy elemTy xs), (ys ** DList aTy elemTy ys))
span f Nil     = ((_ ** Nil), (_ ** Nil))
span f (x::xs) =
  if f x
    then let ((_ ** ys),(_ ** zs)) = span f xs
           in ((_ ** x::ys), (_ ** zs))
    else ((_ ** Nil), (_ ** (x::xs)))

break : ({a : aTy} -> elemTy a -> Bool)
      -> DList aTy elemTy xys
      -> ((xs ** DList aTy elemTy xs), (ys ** DList aTy elemTy ys))
break f xs = span (not . f) xs

split : ({a : aTy} -> elemTy a -> Bool)
     -> DList aTy elemTy xys
     -> (xxs ** DList (List aTy) (\xs => DList aTy elemTy xs) xxs)
split f xs =
  case break f xs of
    ((_ ** chunk), (_ ** Nil))     => (_ ** [chunk])
    ((_ ** chunk), (_ ** (y::ys))) => let (_ ** rest) = DList.split f ys
        in (_ ** DList.(::) chunk rest)

-- ----------------------------------------------------------------- [ Zipping ]
-- TODO

-- -------------------------------------------------------------- [ Predicates ]
-- TODO

-- ----------------------------------------------------------------- [ Sorting ]
-- TODO

mergeBy : Ord aTy => ({a,b : aTy} -> elemTy a -> elemTy b -> Ordering)
        -> DList aTy elemTy as
        -> DList aTy elemTy bs
        -> (cs ** DList aTy elemTy cs) -- Someday replace with (sort (as ++ bs))
mergeBy cmp Nil right = (_ ** right)
mergeBy cmp left Nil  = (_ ** left)
mergeBy cmp (x::xs) (y::ys) =
  if cmp x y == LT
    then let (_ ** rest) = mergeBy cmp xs      (y::ys) in (_ ** DList.(::) x rest)
    else let (_ ** rest) = mergeBy cmp (x::xs) ys      in (_ ** DList.(::) y rest)

-- -------------------------------------------------------------------- [ Show ]
-- A way of doing show, a little nasty but worth it.
private
doDListShow : ({a : aTy} -> elemTy a -> String)
           -> DList aTy elemTy as
           -> List String
doDListShow _  Nil     = Nil
doDListShow f  (x::xs) = (f x) :: doDListShow f xs

||| Function to show a `DList`.
|||
||| Due to limitations in idris wrt to class instances on dependent
||| types a generic show instance cannot be defined for
||| sigmalist. This will cause minor annoyances in its use.
|||
||| @showFunc A function to show the elements
||| @l       The list to be Shown.
showDList : (showFunc : {a : aTy} -> elemTy a -> String)
         -> (l : DList aTy elemTy as)
         -> String
showDList f xs = "[" ++ unwords (intersperse "," (doDListShow f xs)) ++ "]"

-- -------------------------------------------------------------- [ Predicates ]
||| Proof that some element is found in a `DList`.
|||
||| @iTy     The type of the element's index.
||| @elemTy  The type of the list element.
||| @x       An element in the list.
||| @xs      The list itself.
||| @prf     Proof that the element's index is in the list in the same position as the element itself.
public export
data DElem : (iTy    : Type)
          -> (elemTy : iTy -> Type)
          -> (x      : elemTy i)
          -> (xs     : DList iTy elemTy is)
          -> (prf    : Elem i is)
          -> Type
    where
      ||| Proof that the element is at the front of the list.
      Hier : DElem ity elemTy x (x :: xs) Here

      ||| Proof that the element is found later in the list.
      Er : (komst : DElem iTy elemTy x xs xs') -> DElem iTy elemTy x (x' ::xs) (There xs')

Uninhabited (DElem iTy elemTy a Nil prf) where
    uninhabited Hier impossible
    uninhabited (Er _) impossible

%name DElem komst

||| Analgous to `delete` for normal Lists, however, we require explicit proof that the element, and its index, are in the list.
|||
||| @a   The element to remove.
||| @as  The list to remove the element from.
||| @idx Proof that the index of `a` is in the type of `as`.
||| @prf Proof that the element's index is in the list in the same positino as the element itself.
delete' : (a    : elemTy i)
       -> (as   : DList iTy elemTy is)
       -> (idx  : Elem i is)
       -> (prf  : DElem iTy elemTy a as idx)
       -> DList iTy elemTy (dropElem is idx)
delete' a (a  :: rest) Here          Hier       = rest
delete' a (a' :: rest) (There later) (Er komst) = a' :: delete' a rest later komst

||| Analgous to `delete` for normal Lists, however, we must first calculate proof that the element, and its index, are in the list.
|||
||| @a   The element to remove.
||| @as  The list to remove the element from.
delete : (a        : elemTy i)
      -> (as       : DList iTy elemTy is)
      -> {auto idx : Elem i is}
      -> {auto prf : DElem iTy elemTy a as idx}
      -> DList iTy elemTy (dropElem is idx)
delete x xs {idx} {prf} = delete' x xs idx prf

||| Remove an element from the list given proof of its, and its
||| index's, location in the list.
|||
||| @as  The list to remove the element from.
||| @prf Proof that the element's index is in the list in the same
|||      position as the element itself.
public export
dropElem : (as  : DList iTy elemTy is)
        -> (prf : DElem iTy elemTy a as idx)
        -> DList iTy elemTy (dropElem is idx)
dropElem (a  :: rest) Hier       = rest
dropElem (a' :: rest) (Er komst) = a' :: dropElem rest komst

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module Control.Linear.LState

import Control.Linear

%default total

export
data LState : (stateType : Type) -> (a : Type) -> Type where
  MkLState : (1 f : ((1 _ : stateType) -> (LPair a stateType))) -> LState stateType a

export
Functor (LState stateType) where
  map f (MkLState c) = MkLState (\s => let (r # s') = c s in ((f r) # s'))

export
Applicative (LState stateType) where
  pure x = MkLState (\s => x # s)
  (MkLState cf) <*> (MkLState cv) = MkLState (\s =>
                                    let (f # s') = cf s
                                        (r # s'') = cv s'
                                        in ((f r) # s''))

export
LMonad (LState s) where
  (>>=) (MkLState f) c = MkLState (\x => let (res # s') = f x in
                                                 let (MkLState r2) = c res
                                                      in r2 s')

export
run : (f : (1 state : s) -> (LPair a s)) -> LState s a
run f = MkLState f

export
change : (f : (1 state : s) -> s) -> LState s ()
change f = MkLState (\state => (() # f state))

public export
interface SubState a b where
  liftSt : LState a r -> LState b r

export
SubState a (a, b) where
  liftSt (MkLState f) = MkLState (\(sa, sb) => let (res # sa') = f sa in
                                                  (res # (sa', sb)))

export
SubState a (b, a) where
  liftSt (MkLState f) = MkLState (\(sb, sa) => let (res # sa') = f sa in
                                                  (res # (sb, sa')))

export
runLState : (1 initState : stateType) -> (1 c : LState stateType r) -> LPair r stateType
runLState s (MkLState f) = f s

export
execLState : (1 initState : stateType) -> (1 c : LState stateType r) -> stateType
execLState s (MkLState f) = let (_ # finState) = f s in finState


text:
module Data.Version

import Data.List
import Data.List1
import Data.String
import Data.String.Extra
import Data.Vect

||| A Semantic version.
public export
record Version where
  constructor V
  major, minor, patch : Nat
  ||| If the version is pre-release, the part of the version string following
  ||| a dash (e.g. 'alpha.1' in 0.1.0-alpha.1).
  prereleaseIdentifier : Maybe String
  ||| The full tag of the version. In the context of git this is exactly the
  ||| git tag. Elsewhere this field might hold other meaning.
  tag : String

%name Version version

export
Show Version where
  show (V major minor patch Nothing _) = "\{show major}.\{show minor}.\{show patch}"
  show (V major minor patch (Just pre) _) = "\{show major}.\{show minor}.\{show patch}-\{pre}"

export
Eq Version where
  (V major minor patch pre _) == (V i j k p _) = major == i && minor == j && patch == k && pre == p

export
Ord Version where
  compare (V major minor patch pre _) (V i j k p _) = case vectCompare [major, minor, patch] [i, j, k] of
                                                           EQ    => compare pre p
                                                           o@(_) => o
    where
      vectCompare : Vect 3 Nat -> Vect 3 Nat -> Ordering
      vectCompare = compare

version : (tag : String) -> (prereleaseIdentifier : Maybe String) -> Vect 3 Nat -> Version
version tag pre [x, y, z] = V x y z pre tag

||| Drop any pre-release info from the Version. Note that this does
||| not discard the tag if one is stored on the Version.
export
dropPrerelease : Version -> Version
dropPrerelease (V major minor patch _ tag) = (V major minor patch Nothing tag)

||| Parse a semantic version string.
export
parseVersion : String -> Maybe Version
parseVersion str = do
    let (primary, prerelease) = mapSnd (drop 1) $ break (== '-') str
    let components = split (== '.') $ dropPrefix primary
    nums <- sequence $ map parsePositive components
    version str (nonEmpty prerelease) <$> toVect 3 (forget nums)
  where
    dropPrefix : String -> String
    dropPrefix str with (strM str)
      dropPrefix "" | StrNil = ""
      dropPrefix _ | (StrCons x xs) =
        if x == 'v'
           then xs
           else str

    nonEmpty : String -> Maybe String
    nonEmpty str = case strM str of
                        StrNil        => Nothing
                        (StrCons _ _) => Just str

||| Parse the version as printed out by `idris2 --verison`.
|||
||| Important that this will return Nothing for pre-release
||| versions which can be spotted by the commmit hash following
||| the previous semantic version (0.4.0-b03395deb).
export
parseSpokenVersion : String -> Maybe Version
parseSpokenVersion = parseVersion . drop (length "Idris 2, version ")

||| Take two version lists and zip them up post-sorting
||| such that versions exist to the left or right only
||| if the given version was in the first or second list
||| (respectively).
|||
||| [1.0.0, 1.1.0, 2.0.0] `zipmatch` [1.0.0, 2.0.0, 3.0.0]
||| results in:
||| [(1.0.0, 1.0.0), (1.1.0, Nothing), (2.0.0, 2.0.0), (Nothing, 3..0.0)]
export
zipMatch : List Version -> List Version -> List (Maybe Version, Maybe Version)
zipMatch xs ys = go (sort xs) (sort ys) []
  where
    go : List Version
      -> List Version
      -> (acc : List (Maybe Version, Maybe Version))
      -> List (Maybe Version, Maybe Version)
    go [] [] acc = acc
    go [] (y :: ys) acc = go [] ys $ (Nothing, Just y) :: acc
    go (x :: xs) [] acc = go xs [] $ (Just x, Nothing) :: acc
    go (x :: xs) (y :: ys) acc =
      case compare x y of
           LT => go xs (y :: ys) $ (Just x, Nothing) :: acc
           EQ => go xs ys $ (Just x, Just y) :: acc
           GT => go (x :: xs) ys $ (Nothing, Just y) :: acc

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
module Language.Reflection.Types

-- inspired by https://github.com/MarcelineVQ/idris2-elab-deriving/

import public Language.Reflection.Pretty
import public Language.Reflection.Syntax
import public Language.Reflection
import Text.PrettyPrint.Prettyprinter

%language ElabReflection

%default total

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

public export
Res : Type -> Type
Res = Either String

Eq Namespace where
  (MkNS xs) == (MkNS ys) = xs == ys

Eq UserName where
  Basic x    == Basic y    = x == y
  Field x    == Field y    = x == y
  Underscore == Underscore = True
  _          == _          = False

Eq Name where
  (UN a)        == (UN x)        = a == x
  (MN a b)      == (MN x y)      = a == x && b == y
  (NS a b)      == (NS x y)      = a == x && b == y
  (DN a b)      == (DN x y)      = a == x && b == y
  Nested a b    == Nested x y    = a == x && b == y
  CaseBlock a b == CaseBlock x y = a == x && b == y
  WithBlock a b == WithBlock x y = a == x && b == y
  _             == _             = False

--------------------------------------------------------------------------------
--          General Types
--------------------------------------------------------------------------------

||| Constructor of a data type
public export
record Con where
  constructor MkCon
  name : Name
  args : List NamedArg
  type : TTImp

||| Tries to lookup a constructor by name.
export
getCon : Elaboration m => Name -> m Con
getCon n = do (n',tt)    <- lookupName n
              (args,tpe) <- unPiNamed tt
              pure $ MkCon n' args tpe

export
covering
Pretty Con where
  prettyPrec p (MkCon n args tpe) = applyH p "MkCon" [n, args, tpe]

||| Information about a data type
|||
||| @name : Name of the data type
|||         Note: There is no guarantee that the name will be fully
|||         qualified
||| @args : Type arguments of the data type
||| @cons : List of data constructors
public export
record TypeInfo where
  constructor MkTypeInfo
  name : Name
  args : List NamedArg
  cons : List Con

export
covering
Pretty TypeInfo where
  pretty (MkTypeInfo name args cons) =
    let head = applyH Open "MkTypeInfo" [name, args]
        cons = indent 2 $ vsep (map pretty cons)
     in vsep [head,cons]

||| Tries to get information about the data type specified
||| by name. The name need not be fully qualified, but
||| needs to be unambiguous.
export
getInfo' : Elaboration m => Name -> m TypeInfo
getInfo' n =
  do (n',tt)        <- lookupName n
     (args,IType _) <- unPiNamed tt
                    | (_,_) => fail "Type declaration does not end in IType"
     conNames       <- getCons n'
     cons           <- traverse getCon conNames
     pure (MkTypeInfo n' args cons)

||| macro version of `getInfo'`
export %macro
getInfo : Name -> Elab TypeInfo
getInfo = getInfo'

||| Tries to get the name of the sole constructor
||| of data type specified by name. Fails, if
||| the name is not unambiguous, or if the data type
||| in question has not exactly one constructor.
export %macro
singleCon : Name -> Elab Name
singleCon n = do (MkTypeInfo _ _ cs) <- getInfo' n
                 (c::Nil) <- pure cs | _ => fail "not a single constructor"
                 pure $ name c

--------------------------------------------------------------------------------
--          Parameterized Types
--------------------------------------------------------------------------------

||| Explicit arg of a data constructor
|||
||| The `hasParam` flag indicates, whether one of the
||| type parameters of the data type makes an appearance
||| in the arguments type.
|||
||| For instance, in the following data type, arguments
||| a1 and a3 would have `hasParam` set to `True`.
|||
||| ```
|||   data MyData : (f : Type -> Type) -> (t : Type) -> Type where
|||     A : (a1 : f Int) -> (a2 : String) -> MyData f a
|||     B : (a3 : f a)   -> MyData f a
||| ```
public export
record ExplicitArg where
  constructor MkExplicitArg
  ||| Name of the argument
  name        : Name

  ||| Argument's type as a `TTImp` tree
  tpe         : TTImp

  ||| List of types occuring in `tpe` whose outermost
  ||| type constructor is a parameter.
  |||
  ||| Two examples:
  |||   If `tpe` is `Foo a (Maybe b)`, this is `[a,b]`
  |||   if `tpe` is `Bar (f Int) c`, this is `[f Int,c]`
  paramTypes  : List TTImp

  ||| True if the name of the data type itself
  ||| makes an appearance in `tpe`
  isRecursive : Bool

export
covering
Pretty ExplicitArg where
  prettyPrec p (MkExplicitArg n tpe paramTypes isRecursive) =
    applyH p "MkExplicitArg" [n, tpe, paramTypes, isRecursive]

||| Constructor of a parameterized data type.
|||
||| We only accept two types of arguments for
||| such a constructor: Implicit arguments
||| corresponding to the parameters of the data types
||| and explicit arguments.
|||
||| See `ParamTypeInfo` for examples about what is
||| allowed and what not.
public export
record ParamCon where
  constructor MkParamCon
  name         : Name
  explicitArgs : List ExplicitArg

export
covering
Pretty ParamCon where
  prettyPrec p (MkParamCon n explicitArgs) =
    applyH p "MkParamCon" [n, explicitArgs]

||| Information about a parameterized data type.
|||
||| The constructors of such a data type are only
||| allowed to have two kinds of arguments:
||| Implicit arguments corresponding to the data
||| type's parameters and explicit arguments.
|||
||| Auto implicits or existentials are not allowed.
|||
||| Below are some examples of valid parameterized data types
|||
||| ```
||| data Foo a = Val a | Nope
|||
||| data Reader : (m : Type -> Type) -> (e : Type) -> (a : Type) -> Type where
|||   MkReader : (run : e -> m a) -> Reader m e a
|||
||| data Wrapper : (n : Nat) -> (t : Type) -> Type
|||   Wrap : Vect n t -> Wrapper n t
||| ```
|||
||| Examples of invalid parameterized data types
|||
||| Indexed types families:
|||
||| ```
||| data GADT : (t : Type) -> Type where
|||   A : GADT Int
|||   B : GADT ()
|||   Any : a -> GADT a
||| ```
|||
||| Existentials:
|||
||| ```
||| data Forget : Type where
|||  DoForget : a -> Forget
||| ```
|||
||| Constraint types:
|||
||| ```
||| data ShowableForget : Type where
|||  ShowForget : Show a => a -> Forget
||| ```
public export
record ParamTypeInfo where
  constructor MkParamTypeInfo
  name   : Name
  params : List (Name,TTImp)
  cons   : List ParamCon

export
covering
Pretty ParamTypeInfo where
  pretty (MkParamTypeInfo name params cons) =
    let head = applyH Open "MkParamTypeInfo" [name, toList params]
        cons = indent 2 $ vsep (map pretty cons)
     in vsep [head,cons]

||| Given the constructor arguments of a data type, returns
||| the list of those argument types, in which at least one
||| of the data type's parameters makes an appearance.
|||
||| This function uses a rudimentary comparison to make
||| sure that the returned list contains only distinct types.
|||
||| This function is used to calculate the list of required constraints
||| when automatically deriving interface implementations.
export
calcArgTypesWithParams : ParamTypeInfo -> List TTImp
calcArgTypesWithParams = nubBy sameType . concatMap types . cons
  where types : ParamCon -> List TTImp
        types c = c.explicitArgs >>= paramTypes

        sameType : TTImp -> TTImp -> Bool
        sameType (IVar _ x)   (IVar _ a)   = x == a
        sameType (IApp _ x y) (IApp _ a b) = sameType x a && sameType y b
        sameType _ _                       = False

-- Given a Vect of type parameters (from the surrounding
-- data type), tries to extract a list of type parameter names
-- from the type declaration of a constructor.
private
conParams : (con : Name) -> Vect n a -> TTImp -> Res $ Vect n Name
conParams con as t = run as (snd $ unApp t)
  where err : String
        err = show con
            ++ ": Constructor type arguments do not match "
            ++ "data type type arguments."

        run : Vect k a -> List TTImp -> Res $ Vect k Name
        run [] []                        = Right []
        run (_ :: as) ((IVar _ n) :: ts) = (n ::) <$> run as ts
        run _         _                  = Left err

private
sameArgName : (dataType : Name) -> (arg : Name) -> Bool
sameArgName = (==)

private total
inspect : (dataType : Name)
        -> Vect n (Name,Name)
        -> TTImp
        -> (TTImp, List TTImp, Bool)
inspect dt ns x = let (t,ts,_,b) = run x
                   in (t,ts,b)
        -- First Bool: outer-most type constructor is parameter
        -- Second Bool: expression contains data type name
  where run : TTImp -> (TTImp,List TTImp,Bool,Bool)
        run (IVar x n) =
          case lookup n ns of
            Nothing => (IVar x n, Nil, False, sameArgName dt n)
            Just n' => let t = IVar x n'
                        in (t,[t],True,False)

        run (IPi x y z w a r) =
          let (a',as,_,ca) = run a
              (r',rs,_,cr) = run r
           in (IPi x y z w a' r', as ++ rs, False, ca || cr)

        run (IApp x y z) =
          let (y',ys,b,cy) = run y
              (z',zs,_,cz) = run z
              c             = cy || cz
              t             = IApp x y' z'
           in if cy || cz then (t, ys ++ zs, b, True)
              else if b then (t, [t], b, False)
              else (t, ys ++ zs, False, False)

        run t = (t,Nil,False,False)

private
implicitErr : (con: Name) -> (n : Name) -> Res a
implicitErr con n = Left $  show con
                         ++ ": Non-explicit constructor argument \""
                         ++ show n
                         ++ "\" is not a type parameter."

private
indicesErr : (con : Name) -> (ns : Vect k Name) -> Res a
indicesErr con ns = Left $ show con ++ ": Type indices found: " ++ show ns

-- For a constructor, takes a list of type parameter
-- names and tries to remove the corresponding implicit
-- arguments from the head of the given argument list.
-- Extracts explicit argument names and types from the rest of
-- the list.
--
-- Fails if : a) Not all values in `names` are present as implicit
--               function arguments
--            b) The function has additional non-implicit arguments
private
argPairs :  (dataType : Name)
         -> (con : Name)
         -> Vect n (Name,Name)
         -> List NamedArg
         -> Res $ List ExplicitArg
argPairs dt con names = run names
  where delete : Name -> Vect (S k) (Name,a) -> Res $ Vect k (Name,a)
        delete m ((n,a) :: ns)  =
          if m == n then Right ns
                    else case ns of
                              []        => implicitErr con m
                              ns@(_::_) => ((n,a) ::) <$> delete m ns

        mkArg : NamedArg -> Res ExplicitArg
        mkArg (MkArg _ ExplicitArg n t) = let (t',ts,isD) = inspect dt names t
                                           in Right $ MkExplicitArg n t' ts isD
        mkArg (MkArg _ _ n _)           = implicitErr con n

        run : Vect k (Name,a) -> List NamedArg -> Res $ List ExplicitArg
        run [] as = traverse mkArg as
        run ps@(_::_) ((MkArg _ ImplicitArg n _) :: t) = run !(delete n ps) t
        run ps _ = indicesErr con (map fst ps)

private
paramCon : (dt : Name) -> Vect n Name -> Con -> Res $ ParamCon
paramCon dt ns (MkCon n as t) = do params <- conParams n ns t
                                   args   <- argPairs dt n (zip params ns) as
                                   pure $ MkParamCon n args

private
toParamTypeInfo : TypeInfo -> Res ParamTypeInfo
toParamTypeInfo (MkTypeInfo n as cs) =
  do ps  <- traverse expPair as
     let ns = map fst $ fromList ps
     cs' <- traverse (paramCon n ns) cs
     pure $ MkParamTypeInfo n ps cs'
  where expPair : NamedArg -> Res (Name,TTImp)
        expPair  (MkArg _ ExplicitArg n t) = Right (n,t)
        expPair _ = Left $  show n
                         ++ ": Non-explicit type arguments are not supported"

||| Returns information about a parameterized data type
||| specified by the given (probably not fully qualified) name.
|||
||| The implementation makes sure, that all occurences of
||| type parameters in the constructors have been given
||| the same names as occurences in the type declaration.
export
getParamInfo' : Elaboration m => Name -> m ParamTypeInfo
getParamInfo' n = do ti         <- getInfo' n
                     (Right pt) <- pure (toParamTypeInfo ti)
                                | (Left err) => fail err
                     pure pt

||| macro version of `getParamInfo`.
export %macro
getParamInfo : Name -> Elab ParamTypeInfo
getParamInfo = getParamInfo'


text:
module Scheme.Eval

import Data.Vect
import Data.SortedMap
import Control.ST

import Scheme.Core

%default total
%access public export

SErr : Type
SErr = String

SEvalResult : Type
SEvalResult = Either SErr SExp

data Arity : Type where
  AConst : Arity
  AFixed : Nat -> Arity
  AVar   : Arity

Show Arity where
  show AConst     = "AConst"
  show (AFixed n) = "AFixed " ++ show n
  show AVar       = "AVar"

data SFun : Arity -> Type where
  MkSFConst : SExp -> SFun AConst
  MkSFFixed : (Vect n SExp -> SEvalResult) -> SFun (AFixed n)
  MkSFVar   : (List SExp -> SEvalResult) -> SFun AVar

Show SExp => Show (SFun ar) where
  show      (MkSFConst x) = show x
  show {ar} _             = "#<function " ++ show ar

record SEnv where
  constructor MkSEnv
  definedScope : SortedMap String (ar ** SFun ar)

apply : String -> List SExp -> ST m SEvalResult [env ::: State SEnv]
apply {env} t argList = do
  MkSEnv defs <- read env
  case lookup t defs of
       Nothing                           => pure $ Left "Undefined function"
       Just (AConst   ** MkSFConst _   ) => pure $ Left $ "Can't apply constant " ++ t
       Just (AFixed n ** MkSFFixed func) => do
         case decEq n (length argList) of
              Yes prf => pure $ func $ replace {P = \u => Vect u SExp} (sym prf) $ fromList argList
              No  _   => pure $ Left $ "Need " ++ show n ++ " argument(s), got " ++ show (length argList)
       Just (AVar     ** MkSFVar   func) => pure $ func argList

eval : SExp -> ST m SEvalResult [env ::: State SEnv, qql ::: State Nat]

-- Terminals (Unit, Vect, Bool, Char, Str, Num)
eval SEUnit      = pure $ Right $ SEUnit
eval (SEVect xs) = pure $ Right $ SEVect xs
eval (SEBool b ) = pure $ Right $ SEBool b
eval (SEChar c ) = pure $ Right $ SEChar c
eval (SEStr  s ) = pure $ Right $ SEStr s
eval (SENum sn ) = pure $ Right $ SENum sn

-- Symbols
eval {env} {qql} (SESymbol t) = do
  n <- read qql
  case n of
       -- Outside a quasiquote symbols should consult with environment
       Z   => do MkSEnv defs <- read env
                 case lookup t defs of
                      Nothing                         => pure $ Left $ "Unbound symbol " ++ t
                      Just (AConst ** MkSFConst body) => pure $ Right body
                      Just (ar     ** _             ) => pure $ Left "God bless you" -- FIXME consider arity
       -- Inside a quasiquote symbols evaluate to themselves
       S _ => pure $ Right $ SESymbol t

-- Special forms
eval {env} (SECons (SESymbol "define") (SECons (SESymbol name) (SECons x SEUnit))) = do
  MkSEnv defs <- read env
  case !(eval x) of
       Left  err => pure $ Left err
       Right res => do
         write env $ MkSEnv $ insert name (AConst ** MkSFConst res) defs
         pure $ Right $ SEUnit

eval {env} (SECons (SESymbol "define") (SECons (SECons (SESymbol name) args) (SECons x SEUnit))) = do
  MkSEnv defs <- read env
  case !(eval x) of
       Left  err => pure $ Left err
       Right res => do
         ?definingFunctions

eval (SECons (SESymbol "quote") x) = pure $ Right x

eval {qql} (SECons (SESymbol "quasiquote") x) = do
  n <- read qql
  update qql S
  res <- eval x
  write qql n
  pure res

eval {qql} (SECons (SESymbol "unquote") x) = do
  n <- read qql
  case n of
       Z   => pure $ Left "Unquote only works inside a quasiquote"
       S k => do write qql k
                 res <- eval x
                 write qql n
                 pure res

-- Generic cons i.e. function application
eval {env} {qql} (SECons x y) = do
  n <- read qql
  case n of
       -- Outside a quasiquote
       Z   => do
         case x of
              SESymbol f => call $ apply f $ fst $ listify y
              _          => pure $ Left "Not a function"
       -- Inside a quasiquote evaluate to itself deeply
       S k => do
         exr <- eval x
         eyr <- eval y
         case (exr, eyr) of
              (Left xErr, _        ) => pure $ Left xErr
              (_        , Left yErr) => pure $ Left yErr
              (Right xr , Right yr ) => pure $ Right $ SECons xr yr

-- Everything else doesn't exist yet
eval _ = pure $ Left "Not yet implemented"

namespace StdLib

  -- Type predicates
  isSymbol : Vect 1 SExp -> SExp
  isSymbol [SESymbol _] = SEBool True
  isSymbol _            = SEBool False

  isList : Vect 1 SExp -> SExp
  isList [x] = case snd $ listify x of
                    Nothing => SEBool True
                    _       => SEBool False

  isVect : Vect 1 SExp -> SExp
  isVect [SEVect _] = SEBool True
  isVect _          = SEBool False

  isBool : Vect 1 SExp -> SExp
  isBool [SEBool _] = SEBool True
  isBool _          = SEBool False

  isChar : Vect 1 SExp -> SExp
  isChar [SEChar _] = SEBool True
  isChar _          = SEBool False

  isStr : Vect 1 SExp -> SExp
  isStr [SEStr _] = SEBool True
  isStr _         = SEBool False

  isNum : Vect 1 SExp -> SExp
  isNum [SENum _] = SEBool True
  isNum _         = SEBool False

  -- String/Symbol conversion
  symbolToString : Vect 1 SExp -> SEvalResult
  symbolToString [SESymbol t] = Right $ SEStr t
  symbolToString _            = Left $ "Expected a symbol"

  stringToSymbol : Vect 1 SExp -> SEvalResult
  stringToSymbol [SEStr s] = Right $ SESymbol s
  stringToSymbol _         = Left $ "Expected a string"

  -- Numeric
  plusBin' : SExp -> SExp -> SEvalResult
  plusBin' (SENum (SNExactInt x)) (SENum (SNExactInt y)) = Right $ SENum $ SNExactInt $ x + y
  plusBin' _ _ = Left $ "Expected only numbers"

  plusVar : List SExp -> SEvalResult
  plusVar [] = Right $ SENum $ SNExactInt 0
  plusVar (x :: xs) = do
    w <- plusVar xs
    plusBin' x w

  defaultEnv : SEnv
  defaultEnv = MkSEnv $
    insert "symbol?" (AFixed 1 ** MkSFFixed (pure . isSymbol)) $
    insert "list?" (AFixed 1 ** MkSFFixed (pure . isList)) $
    insert "vector?" (AFixed 1 ** MkSFFixed (pure . isVect)) $
    insert "bool?" (AFixed 1 ** MkSFFixed (pure . isBool)) $
    insert "char?" (AFixed 1 ** MkSFFixed (pure . isChar)) $
    insert "string?" (AFixed 1 ** MkSFFixed (pure . isStr)) $
    insert "number?" (AFixed 1 ** MkSFFixed (pure . isNum)) $
    insert "symbol->string" (AFixed 1 ** MkSFFixed symbolToString) $
    insert "string->symbol" (AFixed 1 ** MkSFFixed stringToSymbol) $
    insert "+" (AVar ** MkSFVar plusVar) $
    empty


text:
import Data.String

main : IO ()
main = do printLn ("<" ++ (unlines []) ++ ">")
          printLn ("<" ++ (unlines ["ab"]) ++ ">")
          printLn ("<" ++ (unlines ["a", "b"]) ++ ">")
          printLn ("<" ++ (fastUnlines []) ++ ">")
          printLn ("<" ++ (fastUnlines ["ab"]) ++ ">")
          printLn ("<" ++ (fastUnlines ["a", "b"]) ++ ">")


text:
module Progress

-- Progress theorem for the 'Step' relation.

import Step
import Subst
import Term

%default total
%access export

-------------------------------------
-- Begin: PROGRESS (AND PRESERVATION)

-- Function 'progress' proves the usual progress lemma.
--
-- Progress: a closed, well-typed term is either a value
--           or it can take a step in the reduction relation.
--
-- Preservation: after reducing a term of type 't' by one
--               step, the resulting term is again of type 't'.
--
--   ***  Note that preservation is already built into     ***
--   ***  the relation 'Step' as defined in module "Step". ***
--
progress : (e : Term [] t) -> Either (Value e) (e' : Term [] t ** (Step e e'))
-- Expressions that are variables cannot occur in an empty context:
-- (In other words, variables are not closed expressions.)
progress (TVar i) = absurd $ FinZAbsurd i
-- Abstractions are values already:
progress (TAbs _) = Left VAbs
-- Applications can reduce in three different ways, the most
-- interesting of which occurs when both arguments of 'App'
-- are values already: in this case, the function 'subst'
-- is required:
progress (TApp e1 e2) = case progress e1 of
  Right (e' ** st) => Right (TApp e' e2 ** StApp1 st)
  Left  v1         =>
    case progress e2 of
         Right (e' ** st) => Right (TApp e1 e' ** StApp2 v1 st)
         Left  v2         => case e1 of
                                  TAbs f => let e'' = subst e2 FZ f
                                            in Right (e'' ** StBeta v2)
-- When the fix-point operator is applied to a value,
-- that value is necessarily an abstraction; hence
-- the function 'subst' is used in reducing 'Fix _':
progress (TFix e) = case progress e of
  Right (e' ** st) => Right (TFix e' ** StFix st)
  Left v           =>
    case e of
         TAbs f => let e'' = subst (TFix (TAbs f)) FZ f
                   in Right (e'' ** StFixBeta)
-- The constant 'Zero' is a value already:
progress TZero = Left VZero
--
progress (TSucc e) = case progress e of
  Right (e' ** st) => Right (TSucc e' ** StSucc st)
  Left  v          => Left (VSucc v)
progress (TPred e) = case progress e of
  Right (e' ** st) => Right (TPred e' ** StPred st)
  Left v           =>
    case e of
         TZero    => Right (TZero ** StPredZero)
         TSucc e' => case v of
                          VAbs     impossible
                          VZero    impossible
                          VSucc v' => Right (e' ** StPredSucc v')
--
progress (TIfz e1 e2 e3) = case progress e1 of
  Right (e' ** st) => Right $ (TIfz e' e2 e3 ** StIfz st)
  Left v           => case v of
                           VAbs     impossible
                           VZero    => Right (e2 ** StIfzZero)
                           VSucc v' => Right (e3 ** StIfzSucc v')

-- End: PROGRESS (AND PRESERVATION)
-----------------------------------

-------------------------------
-- Begin: VALUE <=> IRREDUCIBLE

-- Establish that values cannot be further reduced under 'Step'.
valueIrreducible : (e : Term [] t) ->
                   Value e ->
                   {e' : Term [] t} -> Step e e' -> Void
valueIrreducible TZero     VZero     _           impossible
valueIrreducible (TSucc n) (VSucc v) (StSucc st) = valueIrreducible n v st
valueIrreducible (TAbs _)  VAbs      _           impossible

-- Establish that irreducible expressions (under 'Step') are values:
irreducibleValue : (e : Term [] t) ->
                   ({e' : Term [] t} -> Step e e' -> Void) ->
                   Value e
irreducibleValue e notStep = case progress e of
  Right (_ ** st) => absurd $ notStep st
  Left v          => v

-- End: VALUE <=> IRREDUCIBLE
-----------------------------

------------------------------------------
-- Begin: DIVERGENCE OF TERM 'Subst.omega'

-- Term 'omega' steps to itself in one step:
stepOmega : Step Subst.omega Subst.omega
stepOmega = let st = StFixBeta {t=TVar {ctx=[TyNat]} FZ}
            in replace {P = \x => Step Subst.omega x} substOmega st

-- That 'omega' steps to itself under the reflexive,
-- transitive closure of 'Step' is trivial:
transStepOmega : TransStep Subst.omega Subst.omega
transStepOmega = TStRefl _

-- Term 'omega' steps to nothing but itself:
-- (This could also be derived as a consequence of determinism of 'Step'.)
stepOmegaOnly : (e : Term [] TyNat) -> Step Subst.omega e -> e = Subst.omega
stepOmegaOnly (TFix _) (StFix st) = absurd $ valueIrreducible (TAbs $ TVar FZ) VAbs st
stepOmegaOnly (subst (TFix (TAbs (TVar FZ))) FZ (TVar FZ)) StFixBeta = substOmega

-- To extend the previous result 'stepOmegaOnly' to the transitive closure
-- of the 'Step' relation, an indexed version of 'TransStep' is needed:
data TransStepN : Nat -> Term [] t -> Term [] t -> Type where
   TStNRefl   : (e : Term [] t) -> TransStepN Z e e
   TStNTrans  : {e : Term [] t} -> {e' : Term [] t} -> {e'' : Term [] t} ->
                Step e e' -> TransStepN n e' e'' -> TransStepN (S n) e e''

transStepFromN : TransStepN n e1 e2 -> TransStep e1 e2
transStepFromN (TStNRefl e1)       = TStRefl e1
transStepFromN (TStNTrans st tstn) = TStTrans st (transStepFromN tstn)

transStepToN : TransStep e1 e2 -> (n : Nat ** TransStepN n e1 e2)
transStepToN (TStRefl e1)      = (Z ** TStNRefl e1)
transStepToN (TStTrans st tst) = let (m ** tstn) = transStepToN tst
                                 in ((S m) ** TStNTrans st tstn)

transStepNOmegaOnly : (e : Term [] TyNat) -> (n : Nat) ->
                      TransStepN n Subst.omega e -> e = Subst.omega
transStepNOmegaOnly _ Z     (TStNRefl _)        = Refl
transStepNOmegaOnly e (S k) (TStNTrans st tstk) =
  let eq    = stepOmegaOnly _ st
      tstk' = replace {P = \x => TransStepN k x e} eq tstk
  in transStepNOmegaOnly _ k tstk'

-- Finally, the fact that 'omega' only steps to itself is proven
-- by appealing to the indexed version of the transitive closure:
-- (An induction argument analogous to the one in 'transStepNOmegaOnly'
-- is not accepted by Idris' totality checker. Induction would proceed on
-- the structure of the 'TransStep omega e' argument, and the induction
-- hypothesis would be applied to the second argument of the 'TStTrans'
-- constructor, which would again have the type 'TransStep omega e' but
-- only after rewriting with the equation obtained from 'stepOmegaOnly'.)
transStepOmegaOnly : (e : Term [] TyNat) -> TransStep Subst.omega e -> e = Subst.omega
transStepOmegaOnly e tst = let (n ** tstn) = transStepToN tst
                           in transStepNOmegaOnly e n tstn

divergenceOmega : TransStep Subst.omega e -> (Value e -> Void)
divergenceOmega {e} tst v = let eq = transStepOmegaOnly e tst
                            in case (replace {P = \x => Value x} eq v) of
                               VZero     impossible
                               (VSucc _) impossible
                               VAbs      impossible

-- End: DIVERGENCE OF TERM 'Subst.omega'
----------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Core.FC

import Core.Name.Namespace

import Data.Maybe
import Libraries.Text.Bounded
import Libraries.Text.PrettyPrint.Prettyprinter

%default total

------------------------------------------------------------------------
-- Types

public export
FilePos : Type
FilePos = (Int, Int)

showPos : FilePos -> String
showPos (l, c) = show (l + 1) ++ ":" ++ show (c + 1)

public export
FileName : Type
FileName = String

public export
data VirtualIdent : Type where
  Interactive : VirtualIdent

public export
Eq VirtualIdent where
  Interactive == Interactive = True

export
Show VirtualIdent where
  show Interactive = "(Interactive)"

public export
data OriginDesc : Type where
  ||| Anything that originates in physical Idris source files is assigned a
  ||| `PhysicalIdrSrc modIdent`,
  |||   where `modIdent` is the top-level module identifier of that file.
  PhysicalIdrSrc : (ident : ModuleIdent) -> OriginDesc
  ||| Anything parsed from a package file is decorated with `PhysicalPkgSrc fname`,
  |||   where `fname` is path to the package file.
  PhysicalPkgSrc : (fname : FileName) -> OriginDesc
  Virtual : (ident : VirtualIdent) -> OriginDesc

public export
Eq OriginDesc where
  PhysicalIdrSrc ident == PhysicalIdrSrc ident' = ident == ident'
  PhysicalPkgSrc fname == PhysicalPkgSrc fname' = fname == fname'
  Virtual ident        == Virtual ident'        = ident == ident'
  _                    == _                     = False

export
Show OriginDesc where
  show (PhysicalIdrSrc ident) = show ident
  show (PhysicalPkgSrc fname) = show fname
  show (Virtual ident) = show ident

export
Pretty OriginDesc where
  pretty = pretty . show

||| A file context is a filename together with starting and ending positions.
||| It's often carried by AST nodes that might have been created from a source
||| file or by the compiler. That makes it useful to have the notion of
||| `EmptyFC` as part of the type.
public export
data FC = MkFC        OriginDesc FilePos FilePos
        | ||| Virtual FCs are FC attached to desugared/generated code. They can help with marking
          ||| errors, but we shouldn't attach semantic highlighting metadata to them.
          MkVirtualFC OriginDesc FilePos FilePos
        | EmptyFC

||| A version of a file context that cannot be empty
public export
NonEmptyFC : Type
NonEmptyFC = (OriginDesc, FilePos, FilePos)

------------------------------------------------------------------------
-- Conversion between NonEmptyFC and FC

||| NonEmptyFC always embeds into FC
export
justFC : NonEmptyFC -> FC
justFC (fname, start, end) = MkFC fname start end

||| A view checking whether an arbitrary FC happens to be non-empty
export
isNonEmptyFC : FC -> Maybe NonEmptyFC
isNonEmptyFC (MkFC fn start end) = Just (fn, start, end)
isNonEmptyFC (MkVirtualFC fn start end) = Just (fn, start, end)
isNonEmptyFC EmptyFC = Nothing

||| A view checking whether an arbitrary FC originates from a source location
export
isConcreteFC : FC -> Maybe NonEmptyFC
isConcreteFC (MkFC fn start end) = Just (fn, start, end)
isConcreteFC _ = Nothing

||| Turn an FC into a virtual one
export
virtualiseFC : FC -> FC
virtualiseFC (MkFC fn start end) = MkVirtualFC fn start end
virtualiseFC fc = fc

export
defaultFC : NonEmptyFC
defaultFC = (Virtual Interactive, (0, 0), (0, 0))

export
replFC : FC
replFC = justFC defaultFC

export
toNonEmptyFC : FC -> NonEmptyFC
toNonEmptyFC = fromMaybe defaultFC . isNonEmptyFC

------------------------------------------------------------------------
-- Projections

export
origin : NonEmptyFC -> OriginDesc
origin (fn, _, _) = fn

export
startPos : NonEmptyFC -> FilePos
startPos (_, s, _) = s

export
startLine : NonEmptyFC -> Int
startLine = fst . startPos

export
startCol : NonEmptyFC -> Int
startCol = snd . startPos

export
endPos : NonEmptyFC -> FilePos
endPos (_, _, e) = e

export
endLine : NonEmptyFC -> Int
endLine = fst . endPos

export
endCol : NonEmptyFC -> Int
endCol = snd . endPos

------------------------------------------------------------------------
-- Smart constructors

export
boundToFC : OriginDesc -> WithBounds t -> FC
boundToFC mbModIdent b = MkFC mbModIdent (start b) (end b)

------------------------------------------------------------------------
-- Predicates

--- Return whether a given file position is within the file context (assuming we're
--- in the right file)
export
within : FilePos -> NonEmptyFC -> Bool
within (x, y) (_, start, end)
   = (x, y) >= start && (x, y) <= end

-- Return whether a given line is on the same line as the file context (assuming
-- we're in the right file)
export
onLine : Int -> NonEmptyFC -> Bool
onLine x (_, start, end)
   = x >= fst start && x <= fst end

------------------------------------------------------------------------
-- Constant values

export
emptyFC : FC
emptyFC = EmptyFC

------------------------------------------------------------------------
-- Basic operations
export
mergeFC : FC -> FC -> Maybe FC
mergeFC (MkFC fname1 start1 end1) (MkFC fname2 start2 end2) =
  if fname1 == fname2
  then Just $ MkFC fname1 (min start1 start2) (max end1 end2)
  else Nothing
mergeFC _ _ = Nothing

%name FC fc

------------------------------------------------------------------------
-- Instances

export
Eq FC where
  (==) (MkFC n s e) (MkFC n' s' e') = n == n' && s == s' && e == e'
  (==) (MkVirtualFC n s e) (MkVirtualFC n' s' e') = n == n' && s == s' && e == e'
  (==) EmptyFC EmptyFC = True
  (==) _ _ = False

export
Show FC where
  show EmptyFC = "EmptyFC"
  show (MkFC ident startPos endPos) = show ident ++ ":" ++
             showPos startPos ++ "--" ++
             showPos endPos
  show (MkVirtualFC ident startPos endPos) = show ident ++ ":" ++
             showPos startPos ++ "--" ++
             showPos endPos

prettyPos : FilePos -> Doc ann
prettyPos (l, c) = pretty (l + 1) <+> colon <+> pretty (c + 1)

export
Pretty FC where
  pretty EmptyFC = pretty "EmptyFC"
  pretty (MkFC ident startPos endPos) = pretty ident <+> colon
                 <+> prettyPos startPos <+> pretty "--"
                 <+> prettyPos endPos
  pretty (MkVirtualFC ident startPos endPos) = pretty ident <+> colon
                 <+> prettyPos startPos <+> pretty "--"
                 <+> prettyPos endPos


text:
module Hezarfen.Prover

import Hezarfen.Definitions
import Language.Reflection.Utils
%access public export
%hide Prelude.Stream.(::)

||| `Erased` for `Raw`. `idk` standing for "I don't know"
idk : Raw
idk = RConstant Forgot

||| A hacky way to convert any integer to a string.
||| It initially tries to get a single character string,
||| but if the number is too high then it adds some number afterwards.
||| Does not generate good variable names for negative numbers,
||| but it's not using `Nat` for performance reasons.
intToStr : Int -> String
intToStr i = assert_total $ let d = i `div` 25 in
             pack [chr (97 + (i `mod` 25))] ++
             (if d == 0 then "" else show d)

||| A hacky way to generate fresh variable names that are readable.
||| It assumes that the `gensym` function will return a `MN` that holds
||| an integer at least 101, which is currently the case, but
||| this function needs to rewritten if that changes in the future.
fresh : Elab TTName
fresh =
  do MN i "x" <- gensym "x"
        | _ => fail [TextPart "Bug in ", NamePart `{gensym}]
     when (i < 101) (fail [TextPart "Bug in", NamePart `{fresh}])
     let n = UN $ intToStr (i - 101)
     case !(lookupTy n) of
       [] => pure n
       _ => fresh -- we will eventually get a fresh name

Ty : Type
Ty = Raw

Tm : Type
Tm = Raw

data Context = Ctx (List (TTName, Ty)) (List (TTName, Ty))

implementation Semigroup Context where
  (Ctx xs ys) <+> (Ctx xs' ys') = Ctx (xs ++ xs') (ys ++ ys')
implementation Monoid Context where
  neutral = Ctx [] []

ctxPart : Context -> ErrorReportPart
ctxPart (Ctx xs ys) =
    SubReport $ [TextPart "(", g xs, TextPart "||",  g ys, TextPart ")"]
  where
    f : (TTName, Ty) -> ErrorReportPart
    f (n, t) = SubReport [TextPart "(", NamePart n,
                          TextPart ":", RawPart t, TextPart ")"]
    g : List (TTName, Ty) -> ErrorReportPart
    g l = SubReport $ intersperse (TextPart ",") (map f l)

data Sequent = Seq Context Ty

isAtom : Ty -> Bool
isAtom `(Dec ~_) = False
isAtom `(Either ~_ ~_) = False
isAtom `(Pair ~_ ~_) = False
isAtom `(~_ -> ~_) = False
isAtom `(Unit) = False
isAtom `((=) {A=~a} {B=~b} ~x ~y) = not (x == y)
isAtom `(Void) = False
isAtom _ = True

insert : TTName -> Ty -> Context -> Context
insert n p (Ctx g o) = case p of
  `((~a -> ~b) -> ~d) => Ctx ((n, p) :: g) o
  `(~a -> ~b) => if isAtom a then Ctx ((n, p) :: g) o else Ctx g ((n, p) :: o)
  _           => if isAtom p then Ctx ((n, p) :: g) o else Ctx g ((n, p) :: o)

appConjL : Context -> (Ty, Ty, Ty) -> Elab (TTName, TTName, Sequent)
appConjL ctx (a, b, c) =
  let (n1, n2) = (!fresh, !fresh) in
  pure (n1, n2, Seq ((insert n2 b . insert n1 a) ctx) c)

appTopImplL : Context -> Ty -> Ty -> Elab (TTName, Sequent)
appTopImplL ctx b c = do n <- fresh ; pure (n, Seq (insert n b ctx) c)

appDisjImplL : Context -> (Ty, Ty, Ty, Ty) -> Elab (TTName, TTName, Sequent)
appDisjImplL ctx (d, e, b, c) =
  let (n1, n2) = (!fresh, !fresh) in
  pure (n1, n2, Seq ((insert n2 `(~e -> ~b) . insert n1 `(~d -> ~b)) ctx) c)

except : Nat -> List a -> List a
except n xs = (take n xs) ++ (drop (S n) xs)

allCtxs : List a -> List (a, List a)
allCtxs [] = []
allCtxs (x :: xs) = zipWith (\y,i => (y, except i (x :: xs)))
                            (reverse (x :: xs)) [(length xs) .. 0]

appDisjL : Context -> (Ty, Ty, Ty)
        -> Elab ((TTName, Sequent), (TTName, Sequent))
appDisjL ctx (a, b, c) =
  let (n1, n2) = (!fresh, !fresh) in
  let (ctx1, ctx2) = (insert n1 a ctx, insert n2 b ctx) in
  pure ((n1, Seq ctx1 c), (n2, Seq ctx2 c))

appConjImplL : Context -> (Ty, Ty, Ty, Ty) -> Elab (TTName, Sequent)
appConjImplL (Ctx g o) (d, e, b, c) =
  do n <- fresh
     pure (n, Seq (insert n `(~d -> (~e -> ~b)) (Ctx g o)) c)

appAtomImplL : List (TTName, Ty) -> (Ty, Ty, Ty)
            -> Elab (TTName, Sequent, TTName)
appAtomImplL g (p, b, c) =
  do n <- fresh
     case find (\(m, x) => x == p) g of
        Just (m, x) => pure (n, Seq (insert n b (Ctx g [])) c, m)
        _ => fail [TextPart "Not in context in appAtomImplL"]

appImplImplL : Context -> (Ty, Ty, Ty, Ty)
            -> Elab ((TTName, TTName, Sequent), (TTName, Sequent))
appImplImplL (Ctx g o) (d, e, b, c) =
  let (n1, n2, n3) = (!fresh, !fresh, !fresh) in
  let ctx1 = (insert n1 d . insert n2 `(~e -> ~b)) (Ctx g o) in
  let ctx2 = insert n3 b (Ctx g o) in
  pure ((n1, n2, Seq ctx1 e), (n3, Seq ctx2 c))

hErr : String -> Sequent -> Elab a
hErr s (Seq ctx g) =
  fail [ TextPart ("No rule applies in " ++ s ++ " with goal")
       , RawPart g
       , TextPart "with context "
       , ctxPart ctx]

mutual
  ||| The entry point if you want to specify a context.
  ||| The `Bool` argument is a workaround for the lack of
  ||| Haskell-style pattern guards. Initially that argument should be `False`.
  breakdown : (eqIsAtom : Bool) -> Sequent -> Elab Tm
  breakdown False goal@(Seq ctx `((=) {A=~a} {B=~b} ~x ~y)) =
    if x == y
    then pure `(Refl {A=~a} {x=~x})
    else breakdown True goal
  breakdown _ goal = breakdown' goal

  breakdown' : Sequent -> Elab Tm
  breakdown' goal = case goal of
    -- Introduce as many lambdas as soon as possible
    -- This way it's easier to collapse them into function definitions.
    Seq ctx (RBind orig (Pi a _) b) =>
      let newn = !fresh in
      -- If the Pi type has __pi_arg in the beginning, that means it wasn't
      -- explicitly named, hence not used later in the type.
      -- Therefore it is safe it give it a fresh, readable name
      -- Explicitly named Pi arguments can be used in predicates,
      -- which we only handle as atoms, so it's better to keep those names
      -- as they are provided
      let n = case orig of
                   UN s => if isPrefixOf "__pi_arg" s then newn else orig
                   _ => newn in
      let newgoal = Seq (insert n a ctx) b in
      let tm = !(breakdown False newgoal) in
      pure $ RBind n (Lam a) tm
    Seq ctx `(Unit) => pure `(MkUnit)
    Seq (Ctx g ((n, `(Void)) :: o)) c =>
      pure `(void {a=~c} ~(Var n))
    -- Unpack the pairs as soon as possible, so that they happen before
    -- the `Either`s, which allows us to incorporate them into patterns
    -- in definitions easily.
    Seq (Ctx g ((p, `(Pair ~a ~b)) :: o)) c =>
      let (n1, n2, newgoal) = !(appConjL (Ctx g o) (a, b, c)) in
      pure $ RBind n1 (Let a `(Prelude.Basics.fst {a=~a} {b=~b} ~(Var p)))
           $ RBind n2 (Let b `(Prelude.Basics.snd {a=~a} {b=~b} ~(Var p)))
             !(breakdown False newgoal)
    Seq ctx `(Pair ~a ~b) =>
      let (tm1, tm2) = (!(breakdown False (Seq ctx a)), !(breakdown False (Seq ctx b))) in
      pure `(MkPair {A=~a} {B=~b} ~tm1 ~tm2)
    Seq (Ctx g ((_, `(Unit)) :: o)) c => breakdown False (Seq (Ctx g o) c)
    Seq (Ctx g ((n, `(Dec ~a)) :: o)) c =>
      let ((n1, newgoal1), (n2, newgoal2)) =
        !(appDisjL (Ctx g o) (a, `(~a -> Void), c)) in
      let (tm1, tm2) = (!(breakdown False newgoal1), !(breakdown False newgoal2)) in
      let lm1 = RBind n1 (Lam a) tm1 in
      let lm2 = RBind n2 (Lam `(~a -> Void)) tm2 in
      pure `(dec {a=~a} {c=~c} (Delay ~lm1) (Delay ~lm2) ~(Var n))
    Seq (Ctx g ((n, `(Either ~a ~b)) :: o)) c =>
      let ((n1, newgoal1), (n2, newgoal2)) = !(appDisjL (Ctx g o) (a, b, c)) in
      let (tm1, tm2) = (!(breakdown False newgoal1), !(breakdown False newgoal2)) in
      let lm1 = RBind n1 (Lam a) tm1 in
      let lm2 = RBind n2 (Lam b) tm2 in
      pure `(either {c=~c} {b=~b} {a=~a} (Delay ~lm1) (Delay ~lm2) ~(Var n))
    Seq (Ctx g ((n, `(Unit -> ~b)) :: o)) c =>
      let (n', newgoal) = !(appTopImplL (Ctx g o) b c) in
      pure $ RBind n' (Let b (RApp (Var n) `(MkUnit))) !(breakdown False newgoal)
    Seq (Ctx g ((n, `(Void -> ~b)) :: o)) c => breakdown False (Seq (Ctx g o) c)
    Seq (Ctx g ((n, `((Pair ~d ~e) -> ~b)) :: o)) c =>
      let (n', newgoal) = !(appConjImplL (Ctx g o) (d, e, b, c)) in
      pure $ RBind n' (Let `(~d -> ~e -> ~b)
                            `(curry {c=~b} {b=~e} {a=~d} ~(Var n)))
                      !(breakdown False newgoal)
    Seq (Ctx g ((n, `((Dec ~d) -> ~b)) :: o)) c =>
      let (n1, n2, newgoal) = !(appDisjImplL (Ctx g o) (d, `(~d -> Void), b, c)) in
      let (l1, l2) = (!fresh, !fresh) in
      pure $ RBind n1 (Let `(~d -> ~b)
                        (RBind l1 (Lam d) (RApp (Var n)
                          `(Yes {prop=~d} ~(Var l1)))))
           $ RBind n2 (Let `((~d -> Void) -> ~b)
                        (RBind l2 (Lam `(~d -> Void)) (RApp (Var n)
                          `(No {prop=~d} ~(Var l2)))))
             !(breakdown False newgoal)
    Seq (Ctx g ((n, `((Either ~d ~e) -> ~b)) :: o)) c =>
      let (n1, n2, newgoal) = !(appDisjImplL (Ctx g o) (d, e, b, c)) in
      let (l1, l2) = (!fresh, !fresh) in
      pure $ RBind n1 (Let `(~d -> ~b)
                        (RBind l1 (Lam d) (RApp (Var n)
                          `(Left {a=~d} {b=~e} ~(Var l1)))))
           $ RBind n2 (Let `(~e -> ~b)
                        (RBind l2 (Lam e) (RApp (Var n)
                          `(Right {a=~d} {b=~e} ~(Var l2)))))
             !(breakdown False newgoal)
    Seq (Ctx g []) `(Dec ~a) =>
         (searchSync g `(Dec ~a))
     <|> (do t <- breakdown False (Seq (Ctx g []) a); pure `(Yes {prop=~a} ~t))
     <|> (do t <- breakdown False (Seq (Ctx g []) `(~a -> Void)); pure `(No {prop=~a} ~t))
     <|> hErr "breakdown dec case" goal
    Seq (Ctx g []) `(Either ~a ~b) =>
         (searchSync g `(Either ~a ~b))
     <|> (do t <- breakdown False (Seq (Ctx g []) a); pure `(Left {a=~a} {b=~b} ~t))
     <|> (do t <- breakdown False (Seq (Ctx g []) b); pure `(Right {a=~a} {b=~b} ~t))
     <|> hErr "breakdown either case" goal
    Seq (Ctx g []) c => searchSync g c
    _ => hErr "breakdown" goal

  searchSync : List (TTName, Ty) -> Ty -> Elab Tm
  searchSync g c = choiceMap (eliminate c) (allCtxs g)
               <|> hErr "searchSync" (Seq (Ctx g []) c)

  eliminate : Ty -> ((TTName, Ty), List (TTName, Ty)) -> Elab Ty
  eliminate c ((n, `((~d -> ~e) -> ~b)), ctx) =
    let ((a1, a2, newgoal1), (a3, newgoal2)) =
      !(appImplImplL (Ctx ctx []) (d, e, b, c)) in
    let (tm1, tm2) = (!(breakdown False newgoal1), !(breakdown False newgoal2)) in
    let n' = !fresh in
    let q = RBind a2 (Lam `(~e -> ~b)) (RBind a1 (Lam d) tm1) in
    pure $ RApp (RBind a3 (Lam b) tm2) $
             RApp (Var n) $ RApp q $ RBind n' (Lam e)
               (RApp (Var n) (RBind !fresh (Lam d) (Var n')))
  eliminate c ((n, `(~x -> ~b)), ctx) =
    if not (isAtom x)
    then fail [RawPart x, TextPart "is not an atom"]
    else let (n', newgoal, m) = !(appAtomImplL ctx (x, b, c)) in
         let tm = !(breakdown False newgoal) in
         pure $ RApp (RBind n' (Lam b) tm) (RApp (Var n) (Var m))
  eliminate `((=) {A=~a1} {B=~b1} ~(RApp f x1) ~(RApp g y1)) ((n, `((=) {A=~a2} {B=~b2} ~x2 ~y2)), ctx) =
    if ((x1 == x2) && (y1 == y2) && (f == g))
    then pure `(cong {u=~idk} {t=~a2} {b=~y2} {a=~x2} {f = ~f} ~(Var n))
    else if ((x2 == RApp f x1) && (y2 == RApp g y1))
    then pure (Var n)
    else fail [ NamePart `{(=)}, TextPart "comparison failed in eliminate and"
              , NamePart `{cong}, TextPart "not applicable"]
  eliminate `((=) {A=~a1} {B=~b1} ~x1 ~y1) ((n, `((=) {A=~a2} {B=~b2} ~x2 ~y2)), ctx) =
    if ((x1 == y2) && (x2 == y1))
    then pure `(sym {b=~idk} {a=~idk} {left=~x2} {right=~y2} ~(Var n))
    else if ((x1 == x2) && (y1 == y2))
    then pure (Var n)
    else fail [ NamePart `{(=)}, TextPart "comparison failed in eliminate and"
              , NamePart `{sym}, TextPart "not applicable"]
  eliminate y ((n, x), ctx) =
    if x == y
    then pure (Var n)
    else fail [TextPart "Atom comparison failed in eliminate"]
  eliminate _ _ = fail [TextPart "No rule applies in eliminate"]

||| The entry point if there's an empty context.
prove : Ty -> Elab Tm
prove c = breakdown False (Seq (Ctx [] []) c)

max_stars_repo_name: joom/hezarfen

max_issues_repo_name: joom/hezarfen

max_forks_repo_name: joom/hezarfen