text:
module Sub08Apply108x63

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(36x+21) --F[5,-2]->B[1,-2]--> 3(16x+9)
fb108x63To48x27 :
  (o:Nat) -> P (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                           (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                     (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                               (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))) 2
    -> P (S (S (S (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))))))))))))) 2
fb108x63To48x27 o prf =
  let prf2 = lvDown (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                           (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                     (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                               (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))) 2
                    prf in
    let prf3 = fb108x63To48x27' o prf2 in lvDown (S (S (S (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))))))))))))) 3 prf3

export
apply108x63 : P (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                           (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                     (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                               (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))) 2
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                        (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                  (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))),
         P m 2))
apply108x63 {o} col = let col2 = fb108x63To48x27 o col in ((S (S (S (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)))))))))))))
                                                           ** (lte108x63 o, col2)) where
  lte108x63 : (o:Nat) -> LTE (S (S (S (S (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) (S (plus (plus o o) o)))
                                           (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                     (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                               (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))))))
  lte108x63 Z = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte108x63 (S o) = let lemma = lte108x63 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 (S (plus (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 (plus o o) o) (S (plus (plus o o) o)))  (S (S (S (S (S (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (plus (plus o o) o)))  (S (S (S (S (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (plus (plus o o) o)))  (S (S (S (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (plus (plus o o) o)))  (S (S (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (plus (plus o o) o)))  (S (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (S (plus (plus o o) o)))  (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (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) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                    (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (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)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o)))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                                                                o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                      (S (plus (plus o o) o)))
                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                          (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                    (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o)
                                                                                (S (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.User

import Data.Either
import Data.Vect
import Language.JSON
import Language.JSON.Accessors

%default total

public export
record User where
  constructor MkUser
  login : String
  name  : String

%name Data.User.User user

export
Show User where
  show (MkUser login name) = show (login, name)

export
json : User -> JSON
json (MkUser login name) =
  JObject [
      ("login", JString login)
    , ("name" , JString name)
    ]

export
parseUser : JSON -> Either String User
parseUser (JObject user) = do [login, name] <- lookupAll ["login", "name"] user
                              l <- string login
                              n <- either (const $ Right "unnamed") (Right . id) $ string name
                              pure $ MkUser {
                                  login = l
                                , name  = n
                                }
parseUser (JArray _) = Left "Expected config JSON to be an Object, not an array."
parseUser _          = Left "Expected config JSON to be an Object."

||| Parse a single user from a JSON String
export
parseUserString : String -> Either String User
parseUserString =
  (maybeToEither "Failed to parse JSON" . JSON.parse) >=> parseUser

||| Parse a list of users from a JSON String
export
parseUsersString : String -> Either String (List User)
parseUsersString =
  (maybeToEither "Failed to parse JSON" . JSON.parse) >=> array parseUser

ext: idr

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
import data.Vect

||| Vect of numbers from a to (b - 1)
total range2 : (start: Nat) -> (end: Nat) -> Vect (end `minus` start) Nat
range2 start end = range' (end `minus` start)
where total range' : (a: Nat) -> Vect a Nat
      range' Z     = []
      range' (S k) = (end `minus` (S k)) :: (range' k)

max_stars_repo_name: minimal/idris-experiments

max_issues_repo_name: minimal/idris-experiments

max_forks_repo_name: minimal/idris-experiments


text:
module Package.IkanAst
import Package.IpkgAst
import Control.Monad.Freer
import Debug.Trace
import Control.Monad.Id
import Data.Fin
import Control.Monad.State

%access public export

data IkanData : Type -> Type where
  AddDependencies : List String -> IkanData Unit
  AddSourcepaths : List String -> IkanData Unit

IkanDataT : Type
IkanDataT = Freer IkanData Unit

implicit liftd : IkanData a -> Freer IkanData a
liftd  = liftF

{-
ex1:IkanDataT
ex1 = do
  AddDependencies []
  AddSourcepaths []

-}

max_stars_repo_name: marcesquerra/ikan

max_issues_repo_name: marcesquerra/ikan

max_forks_repo_name: marcesquerra/ikan


text:
module Gen.Parens

public export
interface ParenLoc a where
	Loc : Type
	parenLoc : a -> List Loc

public export
interface ParenRec a where
	parenRec : a -> String

export
parenthesize : (ParenLoc a, ParenRec a, Eq (Loc {a})) =>  Maybe (Loc {a}) -> a -> String
parenthesize l x =
	let rec = parenRec x
	in case l of
		Nothing => rec
		Just loc => if (loc `elem` parenLoc x) then rec else "(" ++ rec ++ ")"

record InstrlaceR a where
	constructor NewInterlaceR
	init : Bool
	acc : a

export interlace : (Monoid a, Foldable f) => a -> f a -> a
interlace sep list = acc $ foldl go (NewInterlaceR True neutral) list
where
	go : InstrlaceR a -> a -> InstrlaceR a
	go (NewInterlaceR True _) x = NewInterlaceR False x
	go (NewInterlaceR False y) x = NewInterlaceR False (y <+> sep <+> x)

export hcat : (Monoid a, Foldable f) => f a -> a
hcat list = interlace neutral list

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text: module PQ.Schema.Table


text:
module Logic

%access public export

%default total

notInvolutive : (b : Bool) -> not (not b) = b
notInvolutive False = Refl
notInvolutive True = Refl

neqSym : Not (a = b) -> Not (b = a)
neqSym contra prf = contra $ sym prf

band : b1 && b2 = True -> (b1 = True, b2 = True)
band {b1 = False} prf = absurd prf
band {b1 = True} prf = (Refl, prf)

n_eq_succ__n_neq_0 : n = S k -> Not (n = 0)
n_eq_succ__n_neq_0 n_eq_succ n_eq_0 = SIsNotZ $ trans (sym n_eq_succ) n_eq_0

iff : {p, q : Type} -> Type
iff {p} {q} = (p -> q, q -> p)

syntax [p] "↔" [q] = iff {p} {q}

iff_sym : (p ↔ q) -> (q ↔ p)
iff_sym (p_imp_q, q_imp_p) = (q_imp_p, p_imp_q)

not_true_iff_false : (Not (b = True)) ↔ (b = False)
not_true_iff_false {b} = (not_true_is_false b, not_true_and_false b)
  where not_true_and_false : (b : Bool) -> (b = False) -> Not (b = True)
        not_true_and_false False _ Refl impossible
        not_true_and_false True Refl _ impossible
        not_true_is_false : (b : Bool) -> Not (b = True) -> b = False
        not_true_is_false False _ = Refl
        not_true_is_false True h = absurd $ h Refl

iff_refl : p ↔ p
iff_refl = (id, id)

iff_trans : (p ↔ q) -> (q ↔ r) -> (p ↔ r)
iff_trans (p_imp_q, q_imp_p) (q_imp_r, r_imp_q) =
  (q_imp_r . p_imp_q, q_imp_p . r_imp_q)

nat_beq_iff : (n, m : Nat) -> (n == m = True) ↔ (n = m)
nat_beq_iff = \n, m => (forward n m, backward n m)
where forward : (n, m : Nat) -> n == m = True -> n = m
      forward Z Z _ = Refl
      forward Z (S _) prf = absurd prf
      forward (S _) Z prf = absurd prf
      forward (S k) (S j) prf = cong {f=S} (forward k j prf)
      backward : (n, m : Nat) -> n = m -> n == m = True
      backward Z Z _ = Refl
      backward Z (S _) prf = absurd prf
      backward (S _) Z prf = absurd prf
      backward (S k) (S j) prf = backward k j (succInjective k j prf)

nat_nbeq_iff : (n, m : Nat) -> (n == m = False) ↔ (Not (n = m))
nat_nbeq_iff = \n, m => (forward n m, backward n m)
where forward : (n, m : Nat) -> n == m = False -> Not (n = m)
      forward Z Z bprf _ = absurd bprf
      forward Z (S _) _ prf = SIsNotZ $ sym prf
      forward (S _) Z _ prf = SIsNotZ prf
      forward (S k) (S j) bprf prf = forward k j bprf (succInjective k j prf)
      backward : (n, m : Nat) -> Not (n = m) -> n == m = False
      backward Z Z contra = absurd $ contra Refl
      backward Z (S _) _ = Refl
      backward (S _) Z _ = Refl
      backward (S k) (S j) contra =
        backward k j (\prf => contra (cong {f=S} prf))

lte_plus_minus : LTE n m -> n + (minus m n) = m
lte_plus_minus {n = Z} {m} _ = minusZeroRight m
lte_plus_minus {n = S _} {m = Z} succ_lte_m = absurd $ succNotLTEzero succ_lte_m
lte_plus_minus {n = S k} {m = S j} succ_lte_m =
  cong $ lte_plus_minus (fromLteSucc succ_lte_m)

lte_beq_iff : (n, m : Nat) -> ((lte n m = True) ↔ (LTE n m))
lte_beq_iff = \n, m => (forward, backward)
where forward : lte n m = True -> LTE n m
      forward {n = Z} _ = LTEZero
      forward {n = S _} {m = Z} prf = absurd prf
      forward {n = S k} {m = S j} prf = LTESucc (forward prf)
      backward : LTE n m -> lte n m = True
      backward LTEZero = Refl
      backward (LTESucc lte_prf) = backward lte_prf

lte_nbeq_iff : (n, m : Nat) -> ((lte n m = False) ↔ (LT m n))
lte_nbeq_iff = \n, m => (forward, backward)
where forward : lte n m = False -> LT m n
      forward {n = Z} prf = absurd prf
      forward {n = S _} {m = Z} _ = LTESucc LTEZero
      forward {n = S k} {m = S j} prf = LTESucc $ forward {n=k} {m=j} prf
      backward : LT m n -> lte n m = False
      backward {n = Z} lt_prf = absurd $ succNotLTEzero lt_prf
      backward {n = S _} {m = Z} _ = Refl
      backward {n = S k} {m = S j} lt_prf = backward (fromLteSucc lt_prf)

lte_z__eq_z : LTE n 0 -> n = 0
lte_z__eq_z {n = Z} _ = Refl
lte_z__eq_z {n = S _} lte_prf = absurd $ succNotLTEzero lte_prf

lte_succ_minus : LTE n m -> minus (S m) n = S (minus m n)
lte_succ_minus {n = Z} {m} lte_prf = rewrite minusZeroRight m in Refl
lte_succ_minus {n = S _} {m = Z} lte_prf = absurd $ succNotLTEzero lte_prf
lte_succ_minus {n = S k} {m = S j} lte_prf = lte_succ_minus (fromLteSucc lte_prf)

lte_minus_plus_sum : LTE k n -> minus n k + plus m k = n + m
lte_minus_plus_sum {k = Z} {n} {m} lte_prf =
  rewrite minusZeroRight n
  in rewrite plusZeroRightNeutral m
  in Refl
lte_minus_plus_sum {k = S _} {n = Z} lte_prf = absurd $ succNotLTEzero lte_prf
lte_minus_plus_sum {k = S i} {n = S k} {m} lte_prf =
  rewrite sym (plusSuccRightSucc m i)
  in rewrite sym (plusSuccRightSucc (minus k i) (m + i))
  in cong (lte_minus_plus_sum (fromLteSucc lte_prf))

bounded__eq : LTE n m -> LTE m n -> n = m
bounded__eq {n = Z} _ above = sym $ lte_z__eq_z above
bounded__eq {n = S _} {m = Z} below _ = absurd $ succNotLTEzero below
bounded__eq {n = S _} {m = S _} below above =
  cong $ bounded__eq (fromLteSucc below) (fromLteSucc above)

notZeroImpliesGTZero : Not (n = 0) -> LT 0 n
notZeroImpliesGTZero {n = Z} contra = absurd $ contra Refl
notZeroImpliesGTZero {n = (S _)} _ = LTESucc LTEZero

plusCong : {a, b, n, m : Nat} -> a = n -> b = m -> a + b = n + m
plusCong prf1 prf2 = rewrite prf1 in rewrite prf2 in Refl

fromNotLteSucc : Not (LTE (S n) (S m)) -> Not (LTE n m)
fromNotLteSucc contra lte_prf = contra (LTESucc lte_prf)

lteImpliesNotGT : LTE n m -> Not (GT n m)
lteImpliesNotGT {n = Z} _ = succNotLTEzero
lteImpliesNotGT {n = S _} {m = Z} lte_prf = absurd $ succNotLTEzero lte_prf
lteImpliesNotGT {n = S k} {m = S j} lte_prf = \succ_prf =>
  lteImpliesNotGT (fromLteSucc lte_prf) (fromLteSucc succ_prf)

Relation : (p : Type) -> Type
Relation p = p -> p -> Type

Deterministic : (r : Relation p) -> Type
Deterministic {p} r = {x, y1, y2 : p} -> r x y1 -> r x y2 -> y1 = y2

NormalForm : (r : Relation t) -> (x : t) -> Type
NormalForm r x = Not (x' ** r x x')

data Multi : {t : Type} -> (r : Relation t) -> Relation t where
  MultiRefl : Multi r x x
  MultiStep : r x y -> Multi r y z -> Multi r x z

multi_R : {r : Relation t} -> r x y -> Multi r x y
multi_R rxy = MultiStep rxy MultiRefl

multi_trans : {r : Relation t} -> Multi r x y -> Multi r y z -> Multi r x z
multi_trans MultiRefl ryz = ryz
multi_trans (MultiStep once next) ryz = MultiStep once (multi_trans next ryz)


text:
module Text.WebIDL.Types.Symbol

import Generics.Derive

%default total

%language ElabReflection

||| A single non-alphanumeric character that is not
||| part of another recognized text token like a comment
||| or floating point literal.
public export
data Symbol : Type where
  ||| An ellipsis : ...
  Ellipsis : Symbol

  ||| A single non-alphanumeric character like '=' or '{'.
  Symb     : (symb : Char) -> Symbol

%runElab derive "Symbol" [Generic,Meta,Eq,Show]


text:
module IdrisJvm.Data.Buffer

import IdrisJvm.IO
import IdrisJvm.File
import Java.Nio
import IdrisJvm.FileChannelIo
import IdrisJvm.ClientServerSocket

%hide Prelude.File.File

-- JVM version of Idris Data.Buffer

namespace IdrisBuffer
  idrisBufferClass : String
  idrisBufferClass = "io/github/mmhelloworld/idrisjvm/runtime/IdrisBuffer"

  IdrisBufferClass : JVM_NativeTy
  IdrisBufferClass = Class idrisBufferClass

  IdrisBuffer : Type
  IdrisBuffer = JVM_Native IdrisBufferClass

||| A buffer is a pointer to a sized, unstructured, mutable chunk of memory.
||| There are primitive operations for getting and setting bytes, ints (32 bit)
||| and strings at a location in the buffer. These operations silently fail
||| if the location is out of bounds, so bounds checking should be done in
||| advance.
export
record Buffer where
  constructor MkBuffer
  ||| Raw bytes, as a pointer to a block of memory
  rawdata : IdrisBuffer
  ||| Cached size of block
  buf_size : Int
  ||| Next location to read/write (e.g. when reading from file)
  location : Int

||| Create a new buffer 'size' bytes long. Returns 'Nothing' if allocation
||| fails
export
newBuffer : (size : Int) -> JVM_IO (Maybe Buffer)
newBuffer size = do bptr <- FFI.new (Int -> JVM_IO IdrisBuffer) size
                    pure (Just (MkBuffer bptr size 0))

||| Reset the 'next location' pointer of the buffer to 0.
||| The 'next location' pointer gives the location for the next file read/write
||| so resetting this means you can write it again
export
resetBuffer : Buffer -> Buffer
resetBuffer buf = record { location = 0 } buf

||| Return the space available in the buffer
export
rawSize : Buffer -> JVM_IO Int
rawSize b = invokeInstance "size" (IdrisBuffer -> JVM_IO Int) (rawdata b)

export
size : Buffer -> Int
size b = buf_size b

||| Set the byte at position 'loc' to 'val'.
||| Does nothing if the location is outside the bounds of the buffer
export
setByte : Buffer -> (loc : Int) -> (val : Bits8) -> JVM_IO ()
setByte b loc val = invokeInstance "setByte" (IdrisBuffer -> Int -> Bits8 -> JVM_IO ()) (rawdata b) loc val

||| Set the int at position 'loc' to 'val'.
||| Uses 4 bytes (assumes up to 32 bit Int).
||| Does nothing if the location is outside the bounds of the buffer
export
setInt : Buffer -> (loc : Int) -> (val : Int) -> JVM_IO ()
setInt b loc val = invokeInstance "setInt" (IdrisBuffer -> Int -> Int -> JVM_IO ()) (rawdata b) loc val

||| Set the double at position 'loc' to 'val'.
||| Uses 8 bytes (assumes 64 bit double).
||| Does nothing if the location is outside the bounds of the buffer
export
setDouble : Buffer -> (loc : Int) -> (val : Double) -> JVM_IO ()
setDouble b loc val = invokeInstance "setDouble" (IdrisBuffer -> Int -> Double -> JVM_IO ()) (rawdata b) loc val

||| Set the byte at position 'loc' to 'val'.
||| Does nothing if the location is out of bounds of the buffer, or the string
||| is too long for the location
export
setString : Buffer -> Int -> String -> JVM_IO ()
setString b loc val
    = do invokeInstance "setString" (IdrisBuffer -> Int -> String -> JVM_IO ()) (rawdata b) loc val
         pure ()

||| Copy data from 'src' to 'dest'. Reads 'len' bytes starting at position
||| 'start' in 'src', and writes them starting at position 'loc' in 'dest'.
||| Does nothing if a location is out of bounds, or there is not enough room
export
copyData : (src : Buffer) -> (start, len : Int) ->
           (dest : Buffer) -> (loc : Int) -> JVM_IO ()
copyData src start len dest loc
    = invokeInstance "copy" (IdrisBuffer -> Int -> Int -> IdrisBuffer -> Int -> JVM_IO ())
              (rawdata src) start len (rawdata dest) loc

||| Return the value at the given location in the buffer.
||| Returns 0 if out of bounds.
export
getByte : Buffer -> (loc : Int) -> JVM_IO Bits8
getByte b loc = invokeInstance "getByte" (IdrisBuffer -> Int -> JVM_IO Bits8) (rawdata b) loc

||| Return the value at the given location in the buffer, assuming 4
||| bytes to store the Int.
||| Returns 0 if out of bounds.
export
getInt : Buffer -> (loc : Int) -> JVM_IO Int
getInt b loc = invokeInstance "getInt" (IdrisBuffer -> Int -> JVM_IO Int) (rawdata b) loc

||| Return the value at the given location in the buffer, assuming 8
||| bytes to store the Double.
||| Returns 0 if out of bounds.
export
getDouble : Buffer -> (loc : Int) -> JVM_IO Double
getDouble b loc = invokeInstance "getDouble" (IdrisBuffer -> Int -> JVM_IO Double) (rawdata b) loc

||| Return the string at the given location in the buffer, with the given
||| length. Returns "" if out of bounds.
export
getString : Buffer -> (loc : Int) -> (len : Int) -> JVM_IO String
getString b loc len = invokeInstance "getString" (IdrisBuffer -> Int -> Int -> JVM_IO String) (rawdata b) loc len

export
readBufferFromReadableByteChannel :
    Inherits ReadableByteChannel channel => channel -> Buffer -> (maxbytes : Int) -> JVM_IO Buffer
readBufferFromReadableByteChannel channel buf max = do
    numread <- invokeInstance "readFromFile" (IdrisBuffer -> ReadableByteChannel -> Int -> Int -> JVM_IO Int)
                       (rawdata buf) (believe_me channel) (location buf) max
    pure (record { location $= (+numread) } buf)

export
writeBufferToWritableByteChannel :
    Inherits WritableByteChannel channel => channel -> Buffer -> (maxbytes : Int) -> JVM_IO Buffer
writeBufferToWritableByteChannel channel buf max = do
    let maxwrite = size buf - location buf
    let max' = if maxwrite < max then maxwrite else max
    invokeInstance "writeToFile" (IdrisBuffer -> WritableByteChannel -> Int -> Int -> JVM_IO ())
            (rawdata buf) (believe_me channel) (location buf) max'
    pure (record { location $= (+max') } buf)

||| Read 'maxbytes' into the buffer from a file, returning a new
||| buffer with the 'locaton' pointer moved along
export
total
readBufferFromFile : File -> Buffer -> (maxbytes : Int) -> JVM_IO Buffer
readBufferFromFile (MkFile fileChannelIo) buf max =
    readBufferFromReadableByteChannel fileChannelIo buf max
readBufferFromFile (MkFileClientServerSocket clientServerSocket) buf max =
    readBufferFromReadableByteChannel clientServerSocket buf max
readBufferFromFile _ buf max = pure buf

||| Write 'maxbytes' from the buffer from a file, returning a new
||| buffer with the 'location' pointer moved along
export
total
writeBufferToFile : File -> Buffer -> (maxbytes : Int) -> JVM_IO Buffer
writeBufferToFile (MkFile channel) buf max = writeBufferToWritableByteChannel channel buf max
writeBufferToFile (MkFileClientServerSocket channel) buf max = writeBufferToWritableByteChannel channel buf max
writeBufferToFile _ buf max = pure buf

||| Return the contents of the buffer as a list
export
bufferData : Buffer -> JVM_IO (List Bits8)
bufferData b = do let len = size b
                  unpackTo [] len
  where unpackTo : List Bits8 -> Int -> JVM_IO (List Bits8)
        unpackTo acc 0 = pure acc
        unpackTo acc loc = do val <- getByte b (loc - 1)
                              unpackTo (val :: acc)
                                       (assert_smaller loc (loc - 1))

||| Create a new buffer, copying the contents of the old buffer to the new.
||| Returns 'Nothing' if resizing fails
export
resizeBuffer : Buffer -> Int -> JVM_IO (Maybe Buffer)
resizeBuffer old newsize
    = do Just buf <- newBuffer newsize
              | Nothing => pure Nothing
         -- If the new buffer is smaller than the old one, just copy what
         -- fits
         let oldsize = size old
         let len = if newsize < oldsize then newsize else oldsize
         copyData old 0 len buf 0
         pure (Just buf)


text:
module Data.IOArray

import Data.IOArray.Prims
import Data.List

%default total

export
record IOArray elem where
  constructor MkIOArray
  maxSize : Int
  content : ArrayData (Maybe elem)

export
max : IOArray elem -> Int
max = maxSize

export
newArray : HasIO io => Int -> io (IOArray elem)
newArray size
    = pure (MkIOArray size !(primIO (prim__newArray size Nothing)))

export
writeArray : HasIO io => IOArray elem -> Int -> elem -> io Bool
writeArray arr pos el
    = if pos < 0 || pos >= max arr
         then pure False
         else do primIO (prim__arraySet (content arr) pos (Just el))
                 pure True

export
readArray : HasIO io => IOArray elem -> Int -> io (Maybe elem)
readArray arr pos
    = if pos < 0 || pos >= max arr
         then pure Nothing
         else primIO (prim__arrayGet (content arr) pos)

-- Make a new array of the given size with the elements copied from the
-- other array
export
newArrayCopy : HasIO io =>
               (newsize : Int) -> IOArray elem -> io (IOArray elem)
newArrayCopy newsize arr
    = do let newsize' = if newsize < max arr then max arr else newsize
         arr' <- newArray newsize'
         copyFrom (content arr) (content arr') (max arr - 1)
         pure arr'
  where
    copyFrom : ArrayData (Maybe elem) ->
               ArrayData (Maybe elem) ->
               Int -> io ()
    copyFrom old new pos
        = if pos < 0
             then pure ()
             else do el <- primIO $ prim__arrayGet old pos
                     primIO $ prim__arraySet new pos el
                     copyFrom old new $ assert_smaller pos (pos - 1)

export
toList : HasIO io => IOArray elem -> io (List (Maybe elem))
toList arr = iter 0 (max arr) []
  where
    iter : Int -> Int -> List (Maybe elem) -> io (List (Maybe elem))
    iter pos end acc
         = if pos >= end
              then pure (reverse acc)
              else do el <- readArray arr pos
                      assert_total (iter (pos + 1) end (el :: acc))

export
fromList : HasIO io => List (Maybe elem) -> io (IOArray elem)
fromList ns
    = do arr <- newArray (cast (length ns))
         addToArray 0 ns arr
         pure arr
  where
    addToArray : Int -> List (Maybe elem) -> IOArray elem -> io ()
    addToArray loc [] arr = pure ()
    addToArray loc (Nothing :: ns) arr = addToArray (loc + 1) ns arr
    addToArray loc (Just el :: ns) arr
        = do primIO $ prim__arraySet (content arr) loc (Just el)
             addToArray (loc + 1) ns arr


text:
import Data.Vect

record Person where
    constructor MkPerson
    firstName, middleName, lastName : String
    age : Int

record SizedClass (size : Nat) where
    constructor SizedClassInfo
    students : Vect size Person
    className : String

record Class where
    constructor ClassInfo
    students : Vect n Person
    className : String

addStudent : Person -> Class -> Class
addStudent p c = { students := p :: students c } c

addStudent' : Person -> SizedClass n -> SizedClass (S n)
addStudent' p c =  SizedClassInfo (p :: students c) (className c)

addStudent'' : Person -> SizedClass n -> SizedClass (S n)
addStudent'' p c = { students := p :: students c } c


text:
module Control.Codegen

import public Control.Monad.State
import Data.List
import Data.String

import Libraries.Data.SortedMap

import Debug.Trace
import Rapid.Common

ConstDef : Type
ConstDef = (String, String)

export
record CGBuffer where
  constructor MkCGBuf
  opts : CompileOpts
  i : Int
  consts : List ConstDef
  code : List String
  errors : List String
  constantValues : SortedMap Int String

public export
Codegen : Type -> Type
Codegen = State CGBuffer

emptyCG : CompileOpts -> CGBuffer
emptyCG opts = MkCGBuf opts 0 [] [] [] empty

export
getOpts : Codegen CompileOpts
getOpts = (.opts) <$> get

export
appendCode : String -> Codegen ()
appendCode c = modify { code $= (c::)}

export
getUnique : Codegen Int
getUnique = do
  st <- get
  let i = st.i
  put ({i := i+1} st)
  pure i

export
addConstant : String -> Codegen String
addConstant v = do
  ci <- getUnique
  st <- get
  let name = "@glob_" ++ show (st.opts.constNamespace) ++ "_c" ++ show ci
  put ({ consts $= ((name, v)::)} st)
  pure name

export
addError : String -> Codegen ()
addError msg = do
  appendCode ("; ERROR: " ++ msg)
  st <- get
  put $ trace ("add error: " ++ msg) ({errors $= (msg::)} st)

export
addMetadata : String -> Codegen String
addMetadata v = do
  i <- (.constNamespace) <$> getOpts
  u <- getUnique
  let mdId = u * 0x10000 + i
  let name = "!" ++ show mdId
  modify { consts $= ((name, v)::)}
  pure name

export
appendMetadata : String -> Codegen String
appendMetadata value = do
  o <- (.constNamespace) <$> getOpts
  i <- getUnique
  let varname = "!" ++ show (i * 1000000 + o)
  appendCode ("  " ++ varname ++ " = " ++ value)
  pure varname

export
trackValueConst : Int -> String -> Codegen ()
trackValueConst v c = do
  modify {constantValues $= insert v c}

export
removeValueConst : Int -> Codegen ()
removeValueConst v = do
  modify {constantValues $= delete v}

export
isValueConst : Int -> Codegen (Maybe String)
isValueConst v = do
  lookup v . (.constantValues) <$> get

export
forgetAllValuesConst : Codegen ()
forgetAllValuesConst = modify {constantValues := empty}

export
mkVarName : String -> Codegen String
mkVarName pfx = do
  i <- getUnique
  pure $ (pfx ++ show i)

export
runCodegen : CompileOpts -> Codegen () -> String
runCodegen o r = let (MkCGBuf _ _ cs ls errors _) = fst $ runState (emptyCG o) r in
                     fastConcat $ intersperse "\n" $ (map (\(n,v) => n ++ " = " ++ v) $ reverse cs) ++ reverse ls


text:
double : Num ty => ty -> ty
double x = x + x


text:
module ErrorHandlers

import Queries
import Schema
import SQLiteTypes
import Language.Reflection
import Language.Reflection.Errors

%language ErrorReflection

%access public export

||| Convert a reflected schema to a nice formatted error view
getAttrs : TT -> List ErrorReportPart
getAttrs `(~a ::: ~b) = [SubReport
                          [ TermPart a
                          , TextPart ":::"
                          , TermPart b] ]
getAttrs `(Schema.(::) ~hd ~tl) = getAttrs hd ++ getAttrs tl
getAttrs `(Schema.append ~a ~b) = getAttrs a ++ getAttrs b
getAttrs x = []

||| Rewrite column missing errors
hasColErr : Err -> Maybe (List ErrorReportPart)
hasColErr (CantSolveGoal `(HasCol ~s ~want) _) =
  [| getWant want ++
     pure ([TextPart "in the schema"] ++ getAttrs s) |]
  where getWant : TT -> Maybe (List ErrorReportPart)
        getWant `(~c ::: ~typ : Attribute)=
          pure [ TextPart "The column"
               , TermPart c
               , TextPart "was not found with type"
               , TermPart typ
               ]
        getWant _ = Nothing
hasColErr _ = Nothing

||| Rewrite subschema errors
notSubSchemaErr : Err -> Maybe (List ErrorReportPart)
notSubSchemaErr (CantSolveGoal `(SubSchema ~s1 ~s2) ctxt) =
  Just $ [TextPart "Bad schema:"] ++
         getAttrs s1 ++
         [SubReport $
           [TextPart "Expected subschema of"] ++
            getAttrs s2]
notSubSchemaErr (CantSolveGoal (App (App (App (App equals _) _) l) _) xs) = getSchemas l
  where getSchemas (App (App _ s1) s2) =
          Just $ [TextPart "Bad schema:"] ++
                 getAttrs s1 ++
                 [SubReport $
                   [TextPart "Expected subschema of"] ++
                    getAttrs s2]
        getSchemas _ = Nothing
notSubSchemaErr _ = Nothing

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
module Compo1

import Incrementer
import Twicer

%default total

-- Realized (twicer . incrementer).
rlz_compo1_attrs : RealizedAttributes
rlz_compo1_attrs = MkRealizedAttributes (MkCosts 300 30 3) 0.9
-- The following does not work because 301 ≠ 200+100
-- rlz_compo1_attrs = MkRealizedAttributes (MkCosts 301 30 3) 0.9
rlz_compo1 : RealizedFunction (Int -> Int) Compo1.rlz_compo1_attrs
rlz_compo1 = compose rlz_twicer rlz_incrementer

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module Play.RankN

example2 : ({a : Type} -> a -> a) -> (Int, String)
example2 f = (f 2, f "hello")

example2' : ({a : Type} -> a -> a) -> Int
example2' = fst . example2
-- also compiles and works fine
-- example2' f = fst . example2 $ f

example3 : (({a : Type} -> a -> a) -> Int) -> String
example3 f = show . f $ id

max_stars_repo_name: rpeszek/IdrisTddNotes

max_issues_repo_name: rpeszek/IdrisTddNotes

max_forks_repo_name: rpeszek/IdrisTddNotes


text:
||| Axioms and propsitions for primitive types with an
||| `Ord` implementation.
module Data.Prim.Ord

import public Data.Trichotomy

%default total

||| Similar to `Either` but with erased fields.
public export
data Either0 : Type -> Type -> Type where
  Left0  : (0 v : a) -> Either0 a b
  Right0 : (0 v : b) -> Either0 a b

||| We often don't trust values of type `a === b`, as they might
||| have been magically crafted using `believe_me` or `assert_total`
||| followed by `idris_crash`. If a value of another type follows
||| from a (potentially) magically crafted one, we only want the
||| second value to reduce at compile time, if the first value
||| reduces to `Refl`. Otherwise, we risk blowing up the compiler
||| in an absurd context.
export
strictRefl : (0 prf : a === b) -> Lazy c -> c
strictRefl Refl x = x

--------------------------------------------------------------------------------
--          Interface
--------------------------------------------------------------------------------

||| This interface is a witness that the given primitive type
||| comes with a relation `lt`, with `lt` being a strict total order.
||| We typically define the following aliases
||| (or name the relation accordingly):
|||
|||   `m < n`  := lt m n
|||   `m > n`  := lt n m
|||   `m <= n` := Either (lt m n) (m === n)
|||   `m >= n` := Either (lt n m) (n === m)
|||   `m /= n` := Either (lt m n) (lt n m)
|||
||| The following axioms must hold:
|||   1. (<) is transitive: From `k < m` and `m < n` follows `k < n`.
|||
|||   2. Trichotomy: For all values `m` and `n` exactly one of the
|||      following holds: `m < n`, `m === n`, or `n < m`.
|||
||| It is in the nature of a primitive that we can't proof these axioms
||| in Idris itself. We must therefore assume that they hold on all backends,
||| and it is the responsibility of programmers implementing
||| interface `Total` to make sure that the axioms actually hold.
public export
interface Total (0 a : Type) (0 lt : a -> a -> Type) | lt where
  ||| Axiom I: `<` is transitive.
  0 transLT : {k,m,n : a} -> lt k m -> lt m n -> lt k n

  ||| Axiom II: Trichotomy of `<`, `===`, and `>`.
  trichotomy : (m,n : a) -> Trichotomy lt m n

||| Tests if the first value is strictly less than the second or not
export
testLT : Total a lt => (x,y : a) -> Either0 (lt x y) (Either (lt y x) (y === x))
testLT x y = case trichotomy {lt} x y of
  LT p _ _ => Left0 p
  EQ _ p _ => Right0 (Right $ sym p)
  GT _ _ p => Right0 (Left p)

||| Tests if the first value is strictly greater than the second or not
export
testGT : Total a lt => (x,y : a) -> Either0 (lt y x) (Either (lt x y) (x === y))
testGT x y = case trichotomy {lt} x y of
  GT _ _ p => Left0 p
  LT p _ _ => Right0 (Left p)
  EQ _ p _ => Right0 (Right p)

||| Tests if the two values are provably equal or not
export
testEQ : Total a lt => (x,y : a) -> Either0 (x === y) (Either (lt x y) (lt y x))
testEQ x y = case trichotomy {lt} x y of
  EQ _ p _ => Left0 p
  LT p _ _ => Right0 (Left p)
  GT _ _ p => Right0 (Right p)

--------------------------------------------------------------------------------
--          Corollaries
--------------------------------------------------------------------------------

||| `<` is irreflexive.
export
0 irrefl : Total a lt => Not (lt m m)
irrefl x = case trichotomy m m of
  LT y _ f => f y
  EQ f _ _ => f x
  GT f _ y => f y

--------------------------------------------------------------------------------
--          Transitivities
--------------------------------------------------------------------------------

namespace LT

  ||| This is an alias for `transLT`
  export
  0 trans : Total a lt => lt k m -> lt m n -> lt k n
  trans = transLT

||| `k === m` and `m /= n` implies `k /= n`.
export
0 trans_EQ_NEQ :  Total a lt
               => k === m
               -> Either (lt m n) (lt n m)
               -> Either (lt k n) (lt n k)
trans_EQ_NEQ eqv neq  = rewrite eqv in neq

||| `k === m` and `m /= n` implies `k /= n`.
export
0 trans_NEQ_EQ :  Total a lt
               => Either (lt k m) (lt m k)
               -> m === n
               -> Either (lt k n) (lt n k)
trans_NEQ_EQ neq eqv = rewrite (sym eqv) in neq

||| `k < m` and `m === n` implies `k < n`
export
0 trans_LT_EQ : Total a lt => lt k m -> m === n -> lt k n
trans_LT_EQ p eqv = rewrite sym eqv in p

||| `k === m` and `m < n` implies `k < n`
export
0 trans_EQ_LT : Total a lt => k === m -> lt m n -> lt k n
trans_EQ_LT eqv q = rewrite eqv in q

||| `k <= m` and `m < n` implies `k < n`
export
0 trans_LTE_LT : Total a lt => Either (lt k m) (k === m) -> lt m n -> lt k n
trans_LTE_LT x y = either (`trans` y) (`trans_EQ_LT` y) x

||| `k < m` and `m <= n` implies `k < n`
export
0 trans_LT_LTE : Total a lt => lt k m -> Either (lt m n) (m === n) -> lt k n
trans_LT_LTE x = either (trans x) (trans_LT_EQ x)

||| `k > m` and `m === n` implies `k > n`
export
0 trans_GT_EQ : Total a lt => lt m k -> m === n -> lt n k
trans_GT_EQ p eqv = rewrite sym eqv in p

||| `k === m` and `m > n` implies `k > n`
export
0 trans_EQ_GT : Total a lt => k === m -> lt n m -> lt n k
trans_EQ_GT eqv q = rewrite eqv in q

||| `k >= m` and `m > n` implies `k > n`
export
0 trans_GTE_GT : Total a lt => Either (lt m k) (m === k) -> lt n m -> lt n k
trans_GTE_GT x y = either (trans y) (\v => trans_EQ_GT (sym v) y) x

||| `k > m` and `m >= n` implies `k > n`
export
0 trans_GT_GTE : Total a lt => lt m k -> Either (lt n m) (n === m) -> lt n k
trans_GT_GTE x (Left y)  = trans y x
trans_GT_GTE x (Right y) = trans_GT_EQ x (sym y)

namespace LTE

  ||| `<=` is reflexive.
  export
  0 refl : Total a lt => Either (lt m m) (m === m)
  refl = Right Refl

  ||| `<=` is transitive.
  export
  0 trans :  Total a lt
          => Either (lt k m) (k === m)
          -> Either (lt m n) (m === n)
          -> Either (lt k n) (k === n)
  trans (Left x)  y         = Left (trans_LT_LTE x y)
  trans (Right x) (Left y)  = Left (trans_EQ_LT x y)
  trans (Right x) (Right y) = Right (trans x y)

  ||| `<=` is antisymmetric.
  export
  0 antisym :  Total a lt
            => Either (lt m n) (m === n)
            -> Either (lt n m) (m === n)
            -> m === n
  antisym (Right x) _         = x
  antisym (Left x)  (Right y) = y
  antisym (Left x)  (Left y)  = void (irrefl $ trans x y)

||| `k <= m` and `m === n` implies `k <= n`
export
0 trans_LTE_EQ :  Total a lt
               => Either (lt k m) (k === m)
               -> m === n
               -> Either (lt k n) (k === n)
trans_LTE_EQ lte eq = trans lte (Right eq)

||| `k === m` and `m <= n` implies `(k <= n)`
export
0 trans_EQ_LTE :  Total a lt
               => k === m
               -> Either (lt m n) (m === n)
               -> Either (lt k n) (k === n)
trans_EQ_LTE eq lte = trans (Right eq) lte

namespace GTE

  ||| `>=` is transitive.
  export
  0 trans :  Total a lt
          => Either (lt m k) (m === k)
          -> Either (lt n m) (n === m)
          -> Either (lt n k) (n === k)
  trans (Left x)  y         = Left (trans_GT_GTE x y)
  trans (Right x) (Left y)  = Left (trans_EQ_GT (sym x) y)
  trans (Right x) (Right y) = Right (trans y x)

  ||| `>=` is antisymmetric.
  export
  0 antisym :  Total a lt
            => Either (lt n m) (m === n)
            -> Either (lt m n) (m === n)
            -> m === n
  antisym (Right x) _         = x
  antisym (Left x)  (Right y) = y
  antisym (Left x)  (Left y)  = void (irrefl $ trans x y)

||| `k >= m` and `m === n` implies `k >= n`
export
0 trans_GTE_EQ :  Total a lt
               => Either (lt m k) (m === k)
               -> m === n
               -> Either (lt n k) (n === k)
trans_GTE_EQ gte eq = trans gte (Right $ sym eq)

||| `k === m` and `m <= n` implies `(k <= n)`
export
0 trans_EQ_GTE :  Total a lt
               => k === m
               -> Either (lt n m) (n === m)
               -> Either (lt n k) (n === k)
trans_EQ_GTE eq gte = trans (Right $ sym eq) gte

--------------------------------------------------------------------------------
--          Conversions
--------------------------------------------------------------------------------

||| `m < n` implies `Not (m > n)`.
export
0 LT_not_GT : Total a lt => lt m n -> Not (lt n m)
LT_not_GT isLT isGT = case trichotomy m n of
  LT _ _ g => g isGT
  EQ _ _ g => g isGT
  GT f _ _ => f isLT

||| `m < n` implies `Not (m === n)`.
export
0 LT_not_EQ : Total a lt => lt m n -> Not (m === n)
LT_not_EQ isLT isEQ = case trichotomy m n of
  LT _ g _ => g isEQ
  EQ f _ _ => f isLT
  GT _ g _ => g isEQ

||| `m < n` implies `Not (m >= n)`.
export
0 LT_not_GTE : Total a lt => lt m n -> Not (Either (lt n m) (n === m))
LT_not_GTE l = either (LT_not_GT l) (\e => LT_not_EQ l (sym e))

||| `Not (m < n)` implies `m >= n`.
export
0 Not_LT_to_GTE : Total a lt => Not (lt m n) -> Either (lt n m) (n === m)
Not_LT_to_GTE f = case trichotomy m n of
  LT x _ _ => void (f x)
  EQ _ x _ => Right (sym x)
  GT _ _ x => Left x

||| `m === n` implies `Not (m < n)`.
export
0 EQ_not_LT : Total a lt => m === n -> Not (lt m n)
EQ_not_LT = flip LT_not_EQ

||| `m === n` implies `Not (m > n)`.
export
0 EQ_not_GT : Total a lt => m === n -> Not (lt n m)
EQ_not_GT isEQ = EQ_not_LT (sym isEQ)

||| `m === n` implies `Not (m /= n)`.
export
0 EQ_not_NEQ : Total a lt => m === n -> Not (Either (lt m n) (lt n m))
EQ_not_NEQ isEQ = either (EQ_not_LT isEQ) (EQ_not_GT isEQ)

||| `Not (m < n)` implies `m /= n`.
export
0 Not_EQ_to_NEQ : Total a lt => Not (m === n) -> Either (lt m n) (lt n m)
Not_EQ_to_NEQ f = case trichotomy m n of
  LT x _ _ => Left x
  EQ _ x _ => void (f x)
  GT _ _ x => Right x

||| `m > n` implies `Not (m < n)`.
export
0 GT_not_LT : Total a lt => lt n m -> Not (lt m n)
GT_not_LT = LT_not_GT

||| `m > n` implies `Not (m === n)`.
export
0 GT_not_EQ : Total a lt => lt n m -> Not (m === n)
GT_not_EQ = flip EQ_not_GT

||| `m > n` implies `Not (m <= n)`.
export
0 GT_not_LTE : Total a lt => lt n m -> Not (Either (lt m n) (m === n))
GT_not_LTE gt = either (GT_not_LT gt) (GT_not_EQ gt)

||| `Not (m > n)` implies `m <= n`.
export
0 Not_GT_to_LTE : Total a lt => Not (lt n m) -> Either (lt m n) (m === n)
Not_GT_to_LTE f = case trichotomy m n of
  LT x _ _ => Left x
  EQ _ x _ => Right x
  GT _ _ x => void (f x)

||| `m <= n` implies `Not (m > n)`.
export
0 LTE_not_GT : Total a lt => (Either (lt m n) (m === n)) -> Not (lt n m)
LTE_not_GT = either LT_not_GT EQ_not_GT

||| `Not (m <= n)` implies `m > n`.
export
0 Not_LTE_to_GT : Total a lt => Not (Either (lt m n) (m === n)) -> lt n m
Not_LTE_to_GT f = case trichotomy m n of
  LT x _ _ => void (f $ Left x)
  EQ _ x _ => void (f $ Right x)
  GT _ _ x => x

||| `m <= n` and `m >= n` implies `m === n`.
export
0 LTE_and_GTE_to_EQ :  Total a lt
                    => Either (lt m n) (m === n)
                    -> Either (lt n m) (n === m)
                    -> m === n
LTE_and_GTE_to_EQ (Left x)  (Right y) = sym y
LTE_and_GTE_to_EQ (Right x) _         = x
LTE_and_GTE_to_EQ (Left x)  (Left y)  = void (LT_not_GT x y)

||| `m <= n` and `m /= n` implies `m < n`.
export
0 LTE_and_NEQ_to_LT :  Total a lt
                    => Either (lt m n) (m === n)
                    -> Either (lt m n) (lt n m)
                    -> lt m n
LTE_and_NEQ_to_LT (Left x)  _         = x
LTE_and_NEQ_to_LT (Right _) (Left x)  = x
LTE_and_NEQ_to_LT (Right x) (Right y) = void (EQ_not_GT x y)

||| `m /= n` implies `Not (m === n)`.
export
0 NEQ_not_EQ : Total a lt => Either (lt m n) (lt n m) -> Not (m === n)
NEQ_not_EQ = either LT_not_EQ GT_not_EQ

||| `Not (m /= n)` implies `m === n`.
export
0 Not_NEQ_to_EQ : Total a lt => Not (Either (lt m n) (lt n m)) -> m === n
Not_NEQ_to_EQ f = case trichotomy m n of
  LT x _ _ => void (f $ Left x)
  EQ _ x _ => x
  GT _ _ x => void (f $ Right x)

||| `m /= n` and `m <= n` implies `m < n`.
export
0 NEQ_and_LTE_to_LT :  Total a lt
                    => Either (lt m n) (lt n m)
                    -> Either (lt m n) (m === n)
                    -> lt m n
NEQ_and_LTE_to_LT = flip LTE_and_NEQ_to_LT

||| `m /= n` and `m <= n` implies `m < n`.
export
0 NEQ_and_GTE_to_GT :  Total a lt
                    => Either (lt m n) (lt n m)
                    -> Either (lt n m) (n === m)
                    -> lt n m
NEQ_and_GTE_to_GT (Right x) _         = x
NEQ_and_GTE_to_GT (Left _)  (Left y)  = y
NEQ_and_GTE_to_GT (Left x)  (Right y) = void (GT_not_EQ x y)

||| `m >= n` implies `Not (m < n)`.
export
0 GTE_not_LT : Total a lt => Either (lt n m) (n === m) -> Not (lt m n)
GTE_not_LT = either GT_not_LT EQ_not_GT

||| `Not (m >= n)` implies `m < n`.
export
0 Not_GTE_to_LT : Total a lt => Not (Either (lt n m) (n === m)) -> lt m n
Not_GTE_to_LT f = case trichotomy m n of
  LT x _ _ => x
  EQ _ x _ => void (f $ Right (sym x))
  GT _ _ x => void (f $ Left x)

||| `m >= n` and `m <= n` implies `m === n`.
export
0 GTE_and_LTE_to_EQ :  Total a lt
                    => Either (lt n m) (n === m)
                    -> Either (lt m n) (m === n)
                    -> m === n
GTE_and_LTE_to_EQ = flip LTE_and_GTE_to_EQ

||| `m >= n` and `m /= n` implies `m > n`.
export
0 GTE_and_NEQ_to_GT :  Total a lt
                    => Either (lt n m) (n === m)
                    -> Either (lt m n) (lt n m)
                    -> lt n m
GTE_and_NEQ_to_GT = flip NEQ_and_GTE_to_GT


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

%default total
%access public export

sets : ((a -> b) -> s -> t) -> Setter s t a b
sets l (Mor f) = Mor $ Id . l (runIdentity . f)

over : Setter s t a b -> (a -> b) -> s -> t
over l f = runIdentity . applyMor (l (Mor (Id . f)))

set : Setter s t a b -> b -> s -> t
set l b = over l (const b)

infixr 4 .~
(.~) : Setter s t a b -> b -> s -> t
(.~) = set

infixr 4 &~

(&~) : Setter s t a b -> (a -> b) -> s -> t
(&~) = over

infixl 1 &
(&) : a -> (a -> b) -> b
(&) a f = f a

mapped : Functor f => LensLike Identity (f a) (f b) a b
mapped = sets map

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

max_stars_repo_name: andrevidela/idris-lens

max_issues_repo_name: andrevidela/idris-lens

max_forks_repo_name: andrevidela/idris-lens


text:
-- ----------------------------------------------------------------- [ Key.idr ]
-- Module      : Keys
-- Description : Types Cryptographic Keys MkII
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Crypto.Adv.Key

import Crypto.Common

--- Question is do I paramiterise over a Key Type...

data Key : ( vis : Visibility) -> (setting : s ) -> Type where
  MkEncKey    : a -> (setting : s) -> (value : v ) -> Key Public s
  MkDecKey    : a -> (setting : s) -> (value : v ) -> Key Private s
  MkSignKey   : a -> (setting : s) -> (value : v ) -> Key Private s
  MkVerifyKey : a -> (setting : s) -> (value : v ) -> Key Public s

max_stars_repo_name: silky/idris-crypto-types

max_issues_repo_name: silky/idris-crypto-types

max_forks_repo_name: silky/idris-crypto-types


text:
-- Additional FFI help for more interesting C types
-- Some assumptions are made about the existence of this module in
-- Compiler.CompileExpr

module System.FFI

%default total

export
data Struct : String -> -- C struct name
              List (String, Type) -> -- field names and types
              Type where

public export
data FieldType : String -> Type -> List (String, Type) -> Type where
     First : FieldType n t ((n, t) :: ts)
     Later : FieldType n t ts -> FieldType n t (f :: ts)

%extern
prim__getField : {s : _} -> forall fs, ty .
                         Struct s fs -> (n : String) ->
                         FieldType n ty fs -> ty
%extern
prim__setField : {s : _} -> forall fs, ty .
                         Struct s fs -> (n : String) ->
                         FieldType n ty fs -> ty -> PrimIO ()

public export %inline
getField : {s : _} -> Struct s fs -> (n : String) ->
           {auto fieldok : FieldType n ty fs} -> ty
getField s n = prim__getField s n fieldok

public export %inline
setField : {s : _} -> Struct s fs -> (n : String) ->
           {auto fieldok : FieldType n ty fs} -> ty -> IO ()
setField s n val = primIO (prim__setField s n fieldok val)

public export
runtimeClass : String
runtimeClass = "io/github/mmhelloworld/idrisjvm/runtime/Runtime"

public export
jvm' : String -> String -> String -> String -> String
jvm' className methodName arguments ret = "jvm:" ++ methodName ++ "(" ++ arguments ++ " " ++ ret ++ ")," ++ className

public export
jvm : String -> String -> String
jvm className methodName = "jvm:" ++ methodName ++ "," ++ className

%foreign "C:idris2_malloc, libidris2_support, idris_memory.h"
         "jvm:malloc(int java/lang/Object),io/github/mmhelloworld/idrisjvm/runtime/IdrisSystem"
prim__malloc : (size : Int) -> PrimIO AnyPtr

%foreign "C:idris2_free, libidris2_support, idris_memory.h"
         jvm' runtimeClass "free" "java/lang/Object" "void"
prim__free : AnyPtr -> PrimIO ()

||| Allocate memory with libc `malloc`.
export
malloc : HasIO io => (size : Int) -> io AnyPtr
malloc size = primIO $ prim__malloc size

||| Release memory with libc `free`.
export
free : HasIO io => AnyPtr -> io ()
free ptr = primIO $ prim__free ptr


text:
module BST_Tornai

import Data.So

import Syntax.WithProof

%default total

infix 6 <<, >>

namespace WithExplicitPredicates_So

  -- not so effective solution, but easier to be understood for liquidhaskellers, I think

  data BST : (a : Type) -> Ord a -> Type
  (<<) : a -> BST a ord -> Bool
  (>>) : a -> BST a ord -> Bool

  data BST : (a : Type) -> Ord a -> Type where
    Leaf : BST a o
    Node : (o : Ord a) => (k : a) -> (l : BST a o) -> (r : BST a o) -> So (k >> l) -> So (k << r) -> BST a o

  x << Leaf = True
  x << (Node k _ Leaf             _ _) = x < k
  x << (Node k l (Node _ _ _ _ _) _ _) = x << l

  x >> Leaf = True
  x >> (Node k Leaf             _ _ _) = x > k
  x >> (Node k (Node _ _ _ _ _) r _ _) = x >> r

  insert : (o : Ord a) => (x : a) -> BST a o -> BST a o

  insertPresL : (o : Ord a) => {x, j : a} -> {t : BST a o} ->
                So (x < j) -> So (j >> l) -> So (j >> insert x t)
  insertPresR : (o : Ord a) => {x, j : a} -> {t : BST a o} ->
                So (x > j) -> So (j << l) -> So (j << insert x t)

  insert x Leaf = Node x Leaf Leaf Oh Oh
  insert x n@(Node k l r kMoreL kLessR) with (x < k) proof xLessK
    _ | True = Node k (insert x l) r (insertPresL (eqToSo xLessK) kMoreL) kLessR
    _ | False with (x > k) proof xMoreK
      _ | True = Node k l (insert x r) kMoreL (insertPresR (eqToSo xMoreK) kLessR)
      _ | False = n

  -- Long-long proofs, left to the reader
  -- One particular complexity is quadratic notion of `>>` and `<<` checks
  insertPresL y z = ?insertPresL_rhs
  insertPresR y z = ?insertPresR_rhs

namespace WithExplicitPredicates_Inductive

  data BST : (a : Type) -> Ord a -> Type
  data (<<) : a -> BST a o -> Type
  data (>>) : a -> BST a o -> Type

  data BST : (a : Type) -> Ord a -> Type where
    Leaf : BST a o
    Node : (o : Ord a) => (k : a) -> (l : BST a o) -> (r : BST a o) -> k >> l -> k << r -> BST a o

  data (<<) : a -> BST a o -> Type where
    LL : x << Leaf
    LP : (o : Ord a) => {0 l : BST a o} -> {0 kl : k >> l} -> {0 kr : k << Leaf} ->
         So (x < k) -> x << Node k l Leaf kl kr
    LN : (o : Ord a) => {0 l, l', r' : BST a o} -> {0 kl : k >> l} -> {0 kl' : k' >> l'} -> {0 kr' : k' << r'} ->
         {0 kr : k << Node k' l' r' kl' kr'} ->
         x << l -> x << Node k l (Node k' l' r' kl' kr') kl kr

  data (>>) : a -> BST a ord -> Type where

  -- unfinished

namespace WithTypeParams

  data BdTree : (a : Type) -> Ord a -> (min : a) -> (max : a) -> Type where
    Leaf : (o : Ord a) => (k : a) -> BdTree a o k k
    NL   : (o : Ord a) => (k : a) -> (l : BdTree a o lmin lmax) -> (0 _ : So (lmax < k)) -> BdTree a o lmin k
    NR   : (o : Ord a) => (k : a) -> (r : BdTree a o rmin rmax) -> (0 _ : So (k < rmin)) -> BdTree a o k rmax
    NLR  : (o : Ord a) => (k : a) -> (l : BdTree a o lmin lmax) -> (r : BdTree a o rmin rmax) ->
           (0 _ : So (lmax < k)) -> (0 _ : So (k < rmin)) -> BdTree a o lmin rmax

  minLTEmax : (o : Ord a) => BdTree a o mi ma -> mi <= ma = True -- true only when `<=` is coherent with `<` and `=` is reflexive

  %hide Prelude.EqOrd.min
  %hide Prelude.EqOrd.max

  max : Ord a => a -> a -> a
  max x y = if y < x then x else y

  min : Ord a => a -> a -> a
  min x y = if x < y then x else y

  -- These must be an additional requirement to `Ord`, but I'm declaring it with no body for simplicity
  rev : Ord a => {0 x, y : a} -> x < y = False -> y < x = True
  trans_o  : Ord a => {0 x, y, z : a} -> x < y = True -> y < z = True -> x < z = True
  trans_el : Ord a => {0 x, y, z : a} -> x <= y = True -> y < z = True -> x < z = True
  trans_er : Ord a => {0 x, y, z : a} -> x < y = True -> y <= z = True -> x < z = True

  insert' : (o : Ord a) => (x : a) -> BdTree a o mi ma -> BdTree a o (mi `min` x) (x `max` ma)
  insert' x (Leaf k) with (k < x) proof kx
    _ | True  = NR k (Leaf x) (eqToSo kx)
    _ | False = NL k (Leaf x) (eqToSo $ rev kx)
  insert' x (NL k {lmax} l kg) with (k < x) proof kx
    _ | True  = rewrite the (mi < x = True) $ minLTEmax (NL k l kg) `trans_el` kx in
                NLR k l (Leaf x) kg (eqToSo kx)
    _ | False = let newL = insert' x l in
                NL k newL $ case @@ (lmax < x) of
                              (True  ** prf) => rewrite prf in eqToSo $ rev kx
                              (False ** prf) => rewrite prf in kg
  insert' x (NR k r kl) = ?insert'_rhs_3
  insert' x (NLR k l r kg kl) = ?insert'_rhs_4

  data BST : Type -> Type where
    Empty : BST a
    NonEmpty : BdTree a o min max -> BST a

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module CairoCode.CairoCodeUtils

import Core.Name.Namespace
import Compiler.Common
import Core.Context
import Data.List
import Data.String
import Data.Vect
import Data.Either
import Data.SortedSet
import Data.SortedMap
import  Utils.Helpers

import CommonDef
import CairoCode.CairoCode
import CairoCode.Traversal.Base
import CairoCode.Traversal.Defaults

%hide Prelude.toList

public export
Substitutions : Type
Substitutions = CairoReg -> Maybe CairoReg

substituteRegister : Substitutions -> CairoReg -> CairoReg
substituteRegister subst reg = fromMaybe reg (subst reg)

substituteRegisters : Substitutions -> List CairoReg -> List CairoReg
substituteRegisters subst regs = map (substituteRegister subst) regs

substituteLinearImplicits : Substitutions -> LinearImplicitArgs -> LinearImplicitArgs
substituteLinearImplicits subs linImpls = mapValueMap (\(f,t) => (substituteRegister subs f, substituteRegister subs t)) linImpls

substituteRetLinearImplicits : Substitutions -> SortedMap LinearImplicit CairoReg -> SortedMap LinearImplicit CairoReg
substituteRetLinearImplicits subs linImpls = mapValueMap (substituteRegister subs) linImpls

export
substituteDefRegisters : Substitutions -> (Name, CairoDef) -> (Name, CairoDef)
substituteDefRegisters subst def = snd $ runVisitTransformCairoDef (pureTraversal substituteTransform) def
    where substituteTransform : InstVisit CairoReg -> List (InstVisit CairoReg)
          substituteTransform (VisitFunction name params linImpls rets) = [VisitFunction name (substituteRegisters subst params) (substituteRetLinearImplicits subst linImpls) rets]
          substituteTransform (VisitAssign res reg) = [VisitAssign (substituteRegister subst res) (substituteRegister subst reg)]
          substituteTransform (VisitMkCon res tag args) = [VisitMkCon (substituteRegister subst res) tag (substituteRegisters subst args)]
          substituteTransform (VisitMkClosure res name miss args) = [VisitMkClosure (substituteRegister subst res) name miss (substituteRegisters subst args)]
          substituteTransform (VisitApply res linImpls f arg) = [VisitApply (substituteRegister subst res) (substituteLinearImplicits subst linImpls) (substituteRegister subst f) (substituteRegister subst arg)]
          substituteTransform (VisitMkConstant res const) = [VisitMkConstant (substituteRegister subst res) const]
          substituteTransform (VisitCall res linImpls name args) = [VisitCall (substituteRegisters subst res) (substituteLinearImplicits subst linImpls) name (substituteRegisters subst args)]
          substituteTransform (VisitOp res linImpls fn args) = [VisitOp (substituteRegister subst res) (substituteLinearImplicits subst linImpls) fn (map (substituteRegister subst) args)]
          substituteTransform (VisitExtprim res linImpls name args) = [VisitExtprim (substituteRegisters subst res) (substituteLinearImplicits subst linImpls) name (substituteRegisters subst args)]
          substituteTransform (VisitReturn res linImpls) = [VisitReturn (substituteRegisters subst res) (substituteRetLinearImplicits subst linImpls)]
          substituteTransform (VisitProject res reg pos) = [VisitProject (substituteRegister subst res) (substituteRegister subst reg) pos]
          substituteTransform (VisitNull res) = [VisitNull (substituteRegister subst res)]
          substituteTransform (VisitError res err) = [VisitError (substituteRegister subst res) err]
          substituteTransform (VisitCase reg) = [VisitCase (substituteRegister subst reg)]
          substituteTransform visit = [visit]

extractRegs : List CairoReg -> LinearImplicitArgs -> List CairoReg
extractRegs regs linImpls = (regs ++ ((toList linImpls) >>= (\(_,(f,t)) => [f,t])))

public export
RegisterGen : Type
RegisterGen = (String, Int)

-- Assumes String is unique between orderUnassignedRegIndexes runs
export
mkRegisterGen : String -> RegisterGen
mkRegisterGen p =  (p, 0)

export
subRegisterGen : CairoReg -> String -> RegisterGen
subRegisterGen reg p = mkRegisterGen ((show reg) ++ "_" ++ p)

export
deriveRegister : RegisterGen -> CairoReg -> CairoReg
deriveRegister (p1,_) (Unassigned (Just p2) i d) = Unassigned (Just (p1 ++ "_u_" ++ p2)) i d
deriveRegister (p1,_) (Unassigned Nothing i d) = Unassigned (Just (p1 ++ "_u")) i d
deriveRegister (p,_) (Param i) = Unassigned (Just (p ++ "_p")) i 0
deriveRegister (p,_) (NamedParam pn) = Unassigned (Just (p ++ "_np_" ++ pn)) 0 0
deriveRegister (p,_) (Local i d) = Unassigned (Just (p ++ "_lc")) i d
deriveRegister (p,_) (Let i d) = Unassigned (Just (p ++ "_lt")) i d
deriveRegister (p,_) (Temp i d) = Unassigned (Just (p ++ "_t")) i d
deriveRegister (p,_) (Const c) = Unassigned (Just (p ++ "_c_" ++ (show c))) 0 0
deriveRegister (p,_) Eliminated = Unassigned (Just (p ++ "_e")) 0 0

export
splitRegisterGen : RegisterGen -> (RegisterGen, RegisterGen)
splitRegisterGen (p, n) = (("\{p}:\{show n}",0), (p, n+1))

export
nextRegister : RegisterGen -> (depth:Int) -> (CairoReg, RegisterGen)
nextRegister (p,i) d = (Unassigned (Just p) i d,(p,i+1))

export
branchRegisterGen: Show a => Maybe a -> RegisterGen -> RegisterGen
branchRegisterGen Nothing (p,i) = ("\{p}_\{show i}_def" ,0)
branchRegisterGen (Just c) (p,i) = ("\{p}_\{show i}_\{show c}",0)

SeqRegAlloc : Type
SeqRegAlloc = (RegisterGen, SortedMap CairoReg CairoReg)

prepareRegDefSubst : CairoReg -> Traversal SeqRegAlloc ()
prepareRegDefSubst reg@(Unassigned _ _ d) = updateState (\(gen, subst) => updatedIfMissing (gen, subst) (lookup reg subst))
    where updatedIfMissing : SeqRegAlloc -> Maybe CairoReg -> SeqRegAlloc
          updatedIfMissing (gen, subst) Nothing = let (nReg, nextGen) = nextRegister gen d in (nextGen, insert reg nReg subst)
          updatedIfMissing state _ = state
prepareRegDefSubst _ = pure ()

export
orderUnassignedRegIndexes : (Name, CairoDef) -> (Name, CairoDef)
orderUnassignedRegIndexes def =  substituteDefRegisters (\r => lookup r substitution) def
    where seqRegNumberCollector : (rets:List CairoReg) -> SortedMap LinearImplicit (CairoReg, CairoReg) -> (params:List CairoReg) -> Traversal SeqRegAlloc ()
          seqRegNumberCollector regs impls _ = foldlM (\_,reg => prepareRegDefSubst reg) () (extractRegs regs impls)
          substitution: SortedMap CairoReg CairoReg
          substitution = snd $ runVisitCairoDef (rawTraversal (generalize seqRegNumberCollector) (mkRegisterGen "root",empty)) def

export
isLocal : CairoReg -> Bool
isLocal (Local _ _) = True
isLocal (Unassigned _ _ _) = True -- we treat undefined as locals: Reason -- Everything works without RegAlloc
isLocal _ = False

export
isConst : CairoReg -> Bool
isConst (Const _) = True
isConst _ = False

export
isLet : CairoReg -> Bool
isLet (Let _ _) = True
isLet _ = False

export
collectLocals : (Name, CairoDef) -> SortedSet CairoReg
collectLocals def = snd $ runVisitConcatCairoDef (pureTraversal $ generalize general) def
    where general : (rets:List CairoReg) -> LinearImplicitArgs -> (params:List CairoReg) -> SortedSet CairoReg
          general regs impls _ = fromList $ filter isLocal (extractRegs regs impls)

export
countDefInsts : (Name, CairoDef) -> Nat
countDefInsts def = snd $ runVisitConcatCairoDef (pureTraversal $ generalize general) def
    where general : (rets:List CairoReg) -> LinearImplicitArgs -> (params:List CairoReg) -> Nat
          general _ _ _ = 1
          Semigroup Nat where
            (<+>) a b = a + b
          Monoid Nat where
            neutral = Z

export
countDefsInsts : List (Name, CairoDef) -> Nat
countDefsInsts defs = sum $ map countDefInsts defs

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
||| Show length of the input string
module StrLen

main : IO ()
main = do
  putStr "Enter a string: "
  x <- getLine
  putStrLn ("Length is " ++ show (length x))

max_stars_repo_name: DejanMilicic/IdrisPlayground

max_issues_repo_name: DejanMilicic/IdrisPlayground

max_forks_repo_name: DejanMilicic/IdrisPlayground


text:
module Circuits.NetList.Main

import System
import System.File

import Data.String
import Data.Fin
import Data.List.Elem
import Data.List1

import Text.Lexer
import Text.Parser

import Toolkit.Data.Location
import Toolkit.Text.Lexer.Run
import Toolkit.Text.Parser.Run

import Toolkit.Data.Graph.EdgeBounded
import Toolkit.Data.Graph.EdgeBounded.HasExactDegree
import Toolkit.Data.List.Occurs.Does

import Circuits.NetList.Types
import Circuits.NetList.Terms
import Circuits.NetList.AST
import Circuits.NetList.Lexer
import Circuits.NetList.Parser
import Circuits.NetList.Check
import Circuits.NetList.Interp

export
Show a => Show (ParseFailure a) where
  show err
    = trim $ unlines [show (location err), (error err)]

export
Show a => Show (ParseError a) where
  show (FError err)
    = trim $ unlines ["File Error: "
                     , show err]
  show (PError err)
    = trim $ unlines (forget (map show err))

  show (LError (MkLexFail l i))
    = trim $ unlines [show l, show i]

Show (Term ctxt t) where
  show (Var x)
      = unwords ["(var", showElem x <+> ")"]
    where
      toNat : Elem ty xs -> Nat
      toNat Here = Z
      toNat (There x) = S (toNat x)

      showElem : Elem ty xs -> String
      showElem =  (show . toNat)

  show (Port flow x body)
    = unwords ["(port", show (flow,x), show body <+> ")"]

  show (Wire x body)
    = unwords ["(wire", show x, show body <+> ")"]

  show (GateDecl g body)
    = unwords ["(gate", show g, show body <+> ")"]

  show (Assign i o body)
    = unwords ["(assign", show i, show o, show body <+> ")"]

  show Stop = ""

  show (Index dir x y)
    = show x <+> "[" <+> show y <+> "](" <+> show dir <+>")"

  show (Mux o c l r)
    = unwords ["(mux" <+> show o, show c, show l, show r <+> ")"]

  show (GateB x o l r)
    = unwords ["(" <+> show x, show o, show l, show r <+> ")"]

  show (GateU x o i)
    = unwords ["(" <+> show x, show o, show i <+> ")"]

  show (Project WRITE y)
    = unwords ["(project write", show y <+> ")"]

  show (Project READ y)
    = unwords ["(project read", show y <+> ")"]

  show (Cast x y)
    = unwords ["(cast", show y <+> ")"]

  show (Collect o a b)
    = unwords ["(collect", show o, show a, show b <+> ")"]

  show (Split a b i)
    = unwords ["(split", show a, show b, show i <+> ")"]

export
Show (Vertex String) where
  show (Node d k j i) = show k <+> " [label=\"" <+> show (j,i) <+> " " <+> d <+> "\"];"
  show (Leaf d x k j) = show k <+> " [label=\"" <+> withFlow x j <+> " " <+> d <+> "\"];"
    where withFlow : Flow -> Nat -> String
          withFlow f k = show f <+> "(" <+> show k <+>")"

export
showGraph : Graph String -> String
showGraph (MkGraph nodes edges)
    = unlines $ ["digraph G {"]
                ++
                  map show nodes
                ++
                  map (\(x,y) => unwords ["\t" <+> show x, "->", show y <+> ";"]) edges
                ++
                ["}"]

export
Show DegreeType where
  show I = "IN"
  show O = "OUT"

export
showErr : (Graph String, HasExactDegree.Error String)  -> String
showErr (g, MkError vertex kind (MkError vertexID k values))
 = unlines [showGraph g
           , "//because:"
           , "// Vertex " <+> show (ident vertex)
           , "//  has expected degree " <+> show k <+> " " <+> show (values.expected)
           , "//  but we found degree " <+> show k <+> " " <+> show (values.found)
           ]

main : IO Unit
main
  = do putStrLn "// LOG : Starting NetList "
       args <- getArgs

       case args of
         [x,y] => do Right ast <- fromFile y
                       | Left err => do putStrLn "// LOG : Failure Parsing"
                                        printLn err
                                        exitFailure

                     Right term <- typeCheckIO ast
                       | Left err => do putStrLn "// LOG : Failure Type Checking"
                                        printLn err
                                        exitFailure
                     Right res <- runIO term
                       | Left err => do putStrLn "// LOG : Failure Interpreting"
                                        putStrLn (showErr err)
                                        exitFailure
                     putStrLn ((showGraph . fst . getGraph) res)
                     exitSuccess
         _ => do putStrLn "need at least a file name"
                 exitFailure

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Test.Inigo.Package.PackageTest

import IdrTest.Test
import IdrTest.Expectation

import Inigo.Async.Promise
import Inigo.Package.Package
import SemVar.Data

%default total

export
examplePackage : Package
examplePackage =
  MkPackage
    "Example"
    "Inigo"
    (MkVersion 0 0 1 (Just "pre") Nothing)
    (Just "My Description")
    (Just "http://example.com")
    (Just "README.md")
    ["MyDir"]
    ["idris2"]
    (Just "MIT")
    (Just "MyFile")
    (Just "MyExec")
    [
      (["MyDep"], (
        AND
          (GTE $ MkVersion 1 2 3 Nothing Nothing)
          (LT $ MkVersion 2 0 0 Nothing Nothing)
      ))
    ]
    [
      (["MyDevDep"], (
        EQ (MkVersion 2 0 0 Nothing Nothing)
      ))
    ]

examplePackageTest : Test
examplePackageTest =
  test "Parse Example Package" (\_ => assertEq
    (parsePackage """
      ns='Example'
      package='Inigo'
      version='0.0.1-pre'

      description='My Description'
      readme='README.md'
      link='http://example.com'
      modules=['MyDir']
      depends=['idris2']
      license='MIT'
      main='MyFile'
      executable='MyExec'

      [deps]
      MyDep='^1.2.3'

      [dev-deps]
      MyDevDep='2.0.0'
      """
    )
    (Right examplePackage)
  )

invalidVersionTest : Test
invalidVersionTest =
  test "Invalid version test" (\_ => assertEq
    (parsePackage
      """
      ns='Example'
      package='Inigo'
      version='0.0.1zz'
      """
    )
    (
      Left "Invalid version: 0.0.1zz"
    )
  )

-- Note: this is a little ugly, but it's technically correct
encodePackageTest : Test
encodePackageTest =
  test "Encode Example Package" (\_ => assertEq
    (encodePackage $
      MkPackage
        "Example"
        "Inigo"
        (MkVersion 0 0 1 (Just "pre") Nothing)
        (Just "My Description")
        (Just "http://example.com")
        (Just "README.md")
        ["MyDir"]
        ["idris2"]
        (Just "MIT")
        (Just "MyFile")
        (Just "MyExec")
        [
          (["MyDep"], (
            AND
              (GTE $ MkVersion 1 2 3 Nothing Nothing)
              (LT $ MkVersion 2 0 0 Nothing Nothing)
          ))
        ]
        [
          (["MyDevDep"], (
            EQ (MkVersion 2 0 0 Nothing Nothing)
          ))
        ]
    )
    (
      """
      ns=\"Example\"
      package=\"Inigo\"
      version=\"0.0.1-pre\"
      description=\"My Description\"
      link=\"http://example.com\"
      readme=\"README.md\"
      modules=[\"MyDir\"]
      depends=[\"idris2\"]
      license=\"MIT\"
      main=\"MyFile\"
      executable=\"MyExec\"
      deps.MyDep=\">=1.2.3 <2.0.0\"
      dev-deps.MyDevDep=\"=2.0.0\"
      """
    )
  )

generateIPkgTest : Test
generateIPkgTest =
  test "Encode IPkg" (\_ => assertEq
    (generateIPkg
      True $ MkPackage
        "Example"
        "Inigo"
        (MkVersion 0 0 1 (Just "pre") Nothing)
        (Just "My Description")
        (Just "http://example.com")
        (Just "README.md")
        ["MyDir"]
        ["idris2"]
        (Just "MIT")
        (Just "MyFile")
        (Just "MyExec")
        [
          (["MyDep"], (
            AND
              (GTE $ MkVersion 1 2 3 Nothing Nothing)
              (LT $ MkVersion 2 0 0 Nothing Nothing)
          ))
        ]
        []
    )
    (
      """
      package Inigo

      modules = MyDir
      depends = idris2

      sourcedir = \"Deps/Example/Inigo\"

      version = \"0.0.1-pre\"
      main = MyFile
      executable = MyExec
      """
    )
  )

export
suite : Test
suite =
  describe "Package" [
    examplePackageTest,
    invalidVersionTest,
    encodePackageTest,
    generateIPkgTest
  ]

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Language.JSON.Decode

import Language.JSON
import Language.JSON.Data

%access export
%default total

||| Describes how to turn a `JSON` into a `v`.
||| Use with `decodeJSON` or `decodeString`.
Decoder : Type -> Type
Decoder = \v => JSON -> Either String v

private
error : String -> Decoder a
error expected actual =
    Left $ "Expected " ++ expected ++ ", got: " ++ format 0 actual

||| Run a `Decoder` on some `JSON`.
decodeJSON : Decoder a -> JSON -> Either String a
decodeJSON decoder json =
    decoder json

||| Parse a `String` to `JSON` and run a `Decoder` on it
decodeString : Decoder a -> String -> Either String a
decodeString decoder str =
    case parse str of
        Just json => decoder json
        Nothing => Left "parse error"

||| Given a function, transform a decoder's result
map : (a -> b) -> Decoder a -> Decoder b
map f decoder =
    \json =>
    case decoder json of
        Right x => Right (f x)
        Left x => Left x

||| Always decode the given value. Alias of `pure`.
succeed : a -> Decoder a
succeed x _ =
    Right x

||| Always fail with the given error string.
fail : String -> Decoder a
fail err _ =
    Left err

||| Apply a function to the result of a decoder to get another decoder, then run that
andThen : (a -> Decoder b) -> Decoder a -> Decoder b
andThen f decoder json =
    case decoder json of
        Right x => (f x) json
        Left x => Left x

||| Always decode the given value
pure : a -> Decoder a
pure x json =
    Right x

||| Given a decoder of function and one argument, return a decoder of result
ap : Decoder (a -> b) -> Decoder a -> Decoder b
ap df dx json =
    case (df json, dx json) of
        (Right f, Right x) => Right $ f x
        (Right f, Left err) => Left err
        (Left err, _ ) => Left err

||| Alias of apply
(<*>) : Decoder (a -> b) -> Decoder a -> Decoder b
(<*>) = ap

||| Alias of map
(<$>) : (a -> b) -> Decoder a -> Decoder b
(<$>) = map

||| Avoid infinite loops in recursive decoders by wrapping the recursive call with lazy
lazy : (() -> Decoder a) -> Decoder a
lazy thunk =
  andThen thunk (succeed ())

||| Decode the given value when encountering JNull
null : a -> Decoder a
null x JNull = Right x
null _ json = error "null" json

||| Decode a JString
string : Decoder String
string (JString str) = Right str
string json = error "string" json

||| Decode JBoolean
bool : Decoder Bool
bool (JBoolean bool) = Right bool
bool json = error "bool" json

||| Decode a `JNumber` by casting it to `Int`
int : Decoder Int
int (JNumber x) =
    if floor x == x
    then Right (cast x)
    else error {a = Int } "int" (JNumber x)
int json = error "int" json

||| Decode a `JNumber` as `Double`
float : Decoder Double
float (JNumber x) = Right x
float json = error "string" json

||| Given a list of decoders, use the first one that succeeds
oneOf : List (Decoder a) -> Decoder a
oneOf [] json = error "oneOf" json
oneOf (d :: ds) json =
    case d json of
        Right v => Right v
        Left err => oneOf ds json

||| Decode a list of elements
list : Decoder a -> Decoder (List a)
list decoder json@(JArray lst) =
    Prelude.Functor.map reverse $ foldr f (Right []) $ map decoder $ lst
    where
        f (Right v) (Right l) = Right (v :: l)
        f (Left err) _ = Left err
        f (Right v) (Left err) = Left err
list _ json = error "list" json

||| Decode a JObject as key-value pairs
keyValuePairs : Decoder a -> Decoder (List (String, a))
keyValuePairs decoder (JObject o) =
    Prelude.Functor.map reverse $ foldr f (Right []) $ map (\( k, v ) => ( k, decoder v)) $ o
    where
        f : ( String, Either String a ) -> Either String (List ( String, a )) -> Either String (List ( String, a ))
        f ( k, Right v ) (Right lst) = Right (( k, v ) :: lst)
        f ( k, Right v) (Left err) = Left err
        f ( k, Left err ) _ = Left err
keyValuePairs _ json = error "keyValuePairs" json

||| Decode the given field in a `JObject`
field : String -> Decoder a -> Decoder a
field key decoder json@(JObject fields) =
    case filter ((== key) . fst) fields of
        ( _, v ) :: _ => decoder v
        _ => error ("object with field \"" ++ key ++ "\"") json
field key _ json = error ("object with field \"" ++ key ++ "\"") json

||| Decode a nested `JObject` field
at : List String -> Decoder a -> Decoder a
at fields decoder =
    foldr field decoder fields

||| Decode the `n`th element of a `JArray`
index : Int -> Decoder a -> Decoder a
index n decoder json@(JArray lst) =
    case index' (cast n) lst of
        Just j => decoder j
        Nothing => error ("list of length > " ++ cast n ) json
index n decoder json =
    error "list" json

||| Decode `Just` a value if the given decoder succeeds, `Nothing` otherwise
maybe : Decoder a -> Decoder (Maybe a)
maybe decoder json =
    Right $ either (const Nothing) Just (decoder json)

||| Decode `Just` a value or `Nothing` in case of `JNull`
nullable : Decoder a -> Decoder (Maybe a)
nullable decoder =
  oneOf
    [ null Nothing
    , map Just decoder
    ]

max_stars_repo_name: brainrape/idris-json-decode

max_issues_repo_name: brainrape/idris-json-decode

max_forks_repo_name: brainrape/idris-json-decode


text:
ifthenelse : String
ifthenelse = "\{ if True then "a" else "b" }"