text:
module Sub07Apply108x27

import ProofColDivSeqBase
import ProofColDivSeqPostulate
import ProofColDivSeqPostuProof

%default total
-- %language ElabReflection

-- 3(36x+9) --F[5,-2]->C[4,-4]--> 3(32x+7)
export
apply108x27 : (Not . P) (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                          (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                     (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                               (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))),
         (Not . P) m))
apply108x27 {o} col = ((S (S (S (S (S (S (S (plus (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))))
                                                  (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)))))))))))) ** (lte108x27 o, fc108x27To96x21 o col)) where
  lte108x27 : (o:Nat) -> LTE (S (S (S (S (S (S (S (S (plus (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))))
                                        (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 (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))
  lte108x27 Z = (lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte108x27 (S o) = let lemma = lte108x27 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 o o)  o)) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (S (plus (plus o o) o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (S (plus (plus o o) o)))) in
    rewrite (sym (plusSuccRightSucc (plus (plus o o) o)  (plus (plus o o) o))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (S (plus (plus (plus o o) o) (plus (plus o o) o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (S (plus (plus (plus o o) o) (plus (plus o o) o)))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus o o) o) (plus (plus o o) o))  (S (plus (plus (plus o o) o) (plus (plus o o) o))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o)))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                                (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))
                                    (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))))) in

    rewrite (sym (plusSuccRightSucc (plus (plus (plus 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 (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 (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))))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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)))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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))))))))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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)))))))))))) in
    rewrite (sym (plusSuccRightSucc (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 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 (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 (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)))))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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))))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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)))))))) in
    rewrite (sym (plusSuccRightSucc (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 (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))))))) in
    rewrite (sym (plusSuccRightSucc (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))))
                                    (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)))))) in
      (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
> module NonNegDouble.Properties

> import Data.So
> import Syntax.PreorderReasoning

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

> %default total
> %access public export

* Positivity of constants

> ||| zero is not positive
> notPositiveZero : Not (Positive (toDouble NonNegDouble.Constants.zero))
> notPositiveZero = s3 where
>   s0 : toDouble (Element 0.0 (MkLTE Oh)) = 0.0
>   s0 = Refl
>   s1 : Element 0.0 (MkLTE Oh) = NonNegDouble.Constants.zero
>   s1 = Refl
>   s2 : toDouble NonNegDouble.Constants.zero = 0.0
>   s2 = replace {P = \ X => toDouble X = 0.0} s1 s0
>   s3 : Not (Positive (toDouble NonNegDouble.Constants.zero))
>   s3 = replace {P = \ X => Not (Positive X)} (sym s2) Double.Properties.notPositiveZero

> ||| one is positive
> positiveOne : Positive (toDouble NonNegDouble.Constants.one)
> positiveOne = MkLT Oh

* Implementations:

> ||| NonNegDouble is an implementation of Show
> -- implementation [ShowNonNegDouble] Show NonNegDouble where
> implementation [ShowNonNegDouble] Show NonNegDouble where
>   show = show . toDouble

> ||| NonNegDouble is an implementation of Num
> implementation [NumNonNegDouble] Num NonNegDouble where
>   (+) = plus
>   (*) = mult
>   fromInteger = fromNat . fromIntegerNat

> using implementation NumNonNegDouble
>   ||| NonNegDouble is an implementation of Fractional
>   implementation [FractionalNonNegDouble] Fractional NonNegDouble where
>     (/) = div

> ||| NonNegDouble is an implementation of Eq
> implementation [EqNonNegDouble] Eq NonNegDouble where
>   (==) x y = (toDouble x) == (toDouble y)

> using implementation NumNonNegDouble
>   using implementation EqNonNegDouble
>     ||| NonNegDouble is an implementation of Ord
>     implementation [OrdNonNegDouble] Ord NonNegDouble where
>       compare x y = compare (toDouble x) (toDouble y)

* Properties of |toDouble|:

> using implementation NumNonNegDouble
>   |||
>   toDoublePlusLemma : (x : NonNegDouble) -> (y : NonNegDouble) -> toDouble (x + y) = (toDouble x) + (toDouble y)
>   toDoublePlusLemma (Element x px) (Element y py) =
>       ( toDouble ((Element x px) + (Element y py)) )
>     ={ Refl }=
>       ( toDouble (plus (Element x px) (Element y py)) )
>     ={ Refl }=
>       ( toDouble (Element (x + y) (plusPreservesNonNegativity px py)) )
>     ={ Refl }=
>       ( x + y )
>     ={ Refl }=
>       ( (toDouble (Element x px)) + (toDouble (Element y py)) )
>     QED

> using implementation NumNonNegDouble
>   |||
>   toDoubleMultLemma : (x : NonNegDouble) -> (y : NonNegDouble) -> toDouble (x * y) = (toDouble x) * (toDouble y)
>   toDoubleMultLemma (Element x px) (Element y py) =
>       ( toDouble ((Element x px) * (Element y py)) )
>     ={ Refl }=
>       ( toDouble (mult (Element x px) (Element y py)) )
>     ={ Refl }=
>       ( toDouble (Element (x * y) (multPreservesNonNegativity px py)) )
>     ={ Refl }=
>       ( x * y )
>     ={ Refl }=
>       ( (toDouble (Element x px)) * (toDouble (Element y py)) )
>     QED

> using implementation FractionalNonNegDouble
>   |||
>   toDoubleDivLemma : (x : NonNegDouble) -> (y : NonNegDouble) -> toDouble (x / y) = (toDouble x) / (toDouble y)
>   toDoubleDivLemma (Element x px) (Element y py) =
>       ( toDouble ((Element x px) / (Element y py)) )
>     ={ Refl }=
>       ( toDouble (div (Element x px) (Element y py)) )
>     ={ Refl }=
>       ( toDouble (Element (x / y) (divPreservesNonNegativity px py)) )
>     ={ Refl }=
>       ( x / y )
>     ={ Refl }=
>       ( (toDouble (Element x px)) / (toDouble (Element y py)) )
>     QED

* Properties entailed by postulates and properties of |Double|s:

> using implementation FractionalNonNegDouble
>   |||
>   divPreservesPositivity : {x, y : NonNegDouble} ->
>                            Positive (toDouble x) -> Positive (toDouble y) -> Positive (toDouble (x / y))
>   divPreservesPositivity {x} {y} pdx pdy = replace s1 s2 where
>     s1 : (toDouble x) / (toDouble y) = toDouble (x / y)
>     s1 = sym (toDoubleDivLemma x y)
>     s2 : Positive ((toDouble x) / (toDouble y))
>     s2 = Double.Postulates.divPreservesPositivity pdx pdy

> using implementation NumNonNegDouble
>   |||
>   plusAssociative : (x : NonNegDouble) -> (y : NonNegDouble) -> (z : NonNegDouble) ->
>                     x + (y + z) = (x + y) + z
>   plusAssociative (Element x px) (Element y py) (Element z pz) =
>       ( Element x px + ((Element y py) + (Element z pz)) )
>     ={ Refl }=
>       ( Element x px + Element (y + z) (plusPreservesNonNegativity py pz) )
>     ={ Refl }=
>       ( Element (x + (y + z)) (plusPreservesNonNegativity px (plusPreservesNonNegativity py pz)) )
>     ={ subsetEqLemma1 (Element (x + (y + z)) (plusPreservesNonNegativity px (plusPreservesNonNegativity py pz)))
>                       (Element ((x + y) + z) (plusPreservesNonNegativity (plusPreservesNonNegativity px py) pz))
>                       (plusAssociative x y z) uniqueLTE }=
>       ( Element ((x + y) + z) (plusPreservesNonNegativity (plusPreservesNonNegativity px py) pz) )
>     ={ Refl }=
>       ( Element (x + y) (plusPreservesNonNegativity px py) + Element z pz )
>     ={ Refl }=
>       ( ((Element x px) + (Element y py)) + Element z pz )
>     QED

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
data Bar = MkBar
data Baz = MkBaz

foo : (x : Type) -> String
foo Nat = "Nat"
foo Bool = "Bool"
foo (List x) = "List of " ++ foo x
foo Int = "Int"
foo Type = "Type"
foo _ = "Something else"

strangeId : {a : Type} -> a -> a
strangeId {a=Integer} x = x+1
strangeId x = x

partial
strangeId' : {a : Type} -> a -> a
strangeId' {a=Integer} x = x+1

main : IO ()
main = do printLn (foo Nat)
          printLn (foo (List Nat))
          printLn (foo (List Bar))
          printLn (foo (List Baz))
          printLn (foo (List Bool))
          printLn (foo Int)
          printLn (foo String)
          printLn (foo (List Type))
          printLn (foo (List Int))
          printLn (strangeId 42)
          printLn (strangeId (the Int 42))

ext: idr

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Task

import public Control.Monad.Trace

import Task.Internal

import Helpers

%default total
%access export

%hide Language.Reflection.Elab.Tactics.normalise

-- Errors ----------------------------------------------------------------------

data NotApplicable
  = CouldNotChange
  | CouldNotFind Label
  | CouldNotContinue
  | CouldNotHandle Input

Show NotApplicable where
  show (CouldNotChange)   = "Could not change value because types do not match"
  show (CouldNotFind l)   = "Could not find label `" ++ l ++ "`"
  show (CouldNotContinue) = "Could not continue because there is no value to continue with"
  show (CouldNotHandle i) = "Could not handle input `" ++ show i ++ "`"

-- Observations ----------------------------------------------------------------

ui : MonadRef l m => TaskT m a -> m String
ui (Edit {r} (Just x))   with ( show r )
  | show_r               = pure $ "□(" ++ show x ++ ")"
ui (Edit Nothing)        = pure $ "□(_)"
ui (Store {r} loc)       with ( show r )
  | show_r               = pure $ "■(" ++ show !(deref loc) ++ ")"
ui (And left rght)       = pure $ !(ui left) ++ "   ⋈   " ++ !(ui rght)
ui (Or left rght)        = pure $ !(ui left) ++ "   ◆   " ++ !(ui rght)
ui (Xor left rght) with ( delabel left, delabel rght )
  | ( Xor _ _, Xor _ _ ) = pure $                 !(ui left) ++ " ◇ " ++ !(ui rght)
  | ( Xor _ _, _       ) = pure $                 !(ui left) ++ " ◇ " ++ fromMaybe "…" (label rght)
  | ( _,       Xor _ _ ) = pure $ fromMaybe "…" (label left) ++ " ◇ " ++ !(ui rght)
  | ( _,       _       ) = pure $ fromMaybe "…" (label left) ++ " ◇ " ++ fromMaybe "…" (label rght)
ui (Fail)                = pure $ "↯"
ui (Then this cont)      = pure $ !(ui this) ++ " ▶…"
ui (Next this cont)      = pure $ !(ui this) ++ " ▷…"
ui (Label l this)        = pure $ l ++ ":\n\t" ++ !(ui this)
ui (Lift _)              = pure $ "<lift>"

value : MonadRef l m => TaskT m a -> m (Maybe (typeOf a))
value (Edit val)      = pure $ val
value (Store loc)     = pure $ Just !(deref loc)
value (And left rght) = pure $ !(value left) <&> !(value rght)
value (Or left rght)  = pure $ !(value left) <|> !(value rght)
value (Xor _ _)       = pure $ Nothing
value (Fail)          = pure $ Nothing
value (Then _ _)      = pure $ Nothing
value (Next _ _)      = pure $ Nothing
value (Label _ this)  = value this
value (Lift _)        = pure $ Nothing

choices : TaskT m a -> List Path
choices (Xor left rght) =
  --XXX: No with-block possible?
  case ( delabel left, delabel rght ) of
    ( Fail, Fail ) => []
    ( left, Fail ) => map GoLeft (GoHere :: choices left)
    ( Fail, rght ) => map GoRight (GoHere :: choices rght)
    ( left, rght ) => map GoLeft (GoHere :: choices left) ++ map GoRight (GoHere :: choices rght)
choices _          = []

inputs : MonadRef l m => TaskT m a -> m (List Input)
inputs (Edit {r} _)     = pure $ [ ToHere (Change {c=r} Anything), ToHere Empty ]
inputs (Store {r} _)    = pure $ [ ToHere (Change {c=r} Anything) ]
inputs (And left rght)  = pure $ map ToLeft !(inputs left) ++ map ToRight !(inputs rght)
inputs (Or left rght)   = pure $ map ToLeft !(inputs left) ++ map ToRight !(inputs rght)
inputs this@(Xor _ _)   = pure $ map (ToHere . PickWith) (labels this) ++ map (ToHere . Pick) (choices this)
inputs (Fail)           = pure $ []
inputs (Then this _)    = inputs this
inputs (Next this next) = do
    always <- inputs this
    Just v <- value this | Nothing => pure always
    pure $ map ToHere (go (next v)) ++ always
  where
    go : TaskT m a -> List Action
    go task with (delabel task)
      | Xor _ _ = map ContinueWith $ labels task
      | Fail    = []
      | _       = [ Continue ]
inputs (Label _ this)   = inputs this
inputs (Lift _)         = pure $ []

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

failing : TaskT m a -> Bool
failing (Edit _)        = False
failing (Store _)       = False
failing (And left rght) = failing left && failing rght
failing (Or left rght)  = failing left && failing rght
failing (Xor left rght) = failing left && failing rght
failing (Fail)          = True
failing (Then this _)   = failing this
failing (Next this _)   = failing this
failing (Label _ this)  = failing this
failing (Lift _)        = False --FIXME: needs normalisation!!!

-- Normalisation ---------------------------------------------------------------

normalise : MonadRef l m => TaskT m a -> m (TaskT m a)

-- Step --
normalise (Then this cont) = do
  this_new <- normalise this
  case !(value this_new) of
    Nothing => pure $ Then this_new cont
    Just v  =>
      --FIXME: should we use normalise here instead of just eval?
      let next = cont v in
      if failing next then
        pure $ Then this_new cont
      else
        normalise next

-- Evaluate --
normalise (And left rght) = do
  left_new <- normalise left
  rght_new <- normalise rght
  pure $ And left_new rght_new

normalise (Or left rght) = do
  left_new <- normalise left
  case !(value left_new) of
    Just _  => pure $ left_new
    Nothing => do
      rght_new <- normalise rght
      case !(value rght_new) of
        Just _  => pure $ rght_new
        Nothing => pure $ Or left_new rght_new

normalise (Next this cont) = do
  this_new <- normalise this
  pure $ Next this_new cont

-- Label --
normalise (Label l this) with (keeper this)
  | False = normalise this
  | True  = do
      this_new <- normalise this
      pure $ Label l this_new

-- Lift --
normalise (Lift a) = do
  x <- a
  pure $ Edit (Just x)

-- Values --
normalise task = do
  pure $ task

initialise : MonadRef l m => TaskT m a -> m (TaskT m a)
initialise = normalise

-- Input handling --------------------------------------------------------------

covering
handle : MonadTrace NotApplicable m => MonadRef l m => TaskT m a -> Input -> m (TaskT m a)

-- Edit --
handle (Edit _) (ToHere Empty) =
  pure $ Edit Nothing

handle (Edit {r} val) (ToHere (Change {c} val_new)) with (decEq c r)
  handle (Edit _)   (ToHere (Change val_new))       | Yes Refl = pure $ Edit $ toMaybe val_new
  handle (Edit val) (ToHere (Change _))             | No _     = trace CouldNotChange $ Edit val

handle (Store {r} loc) (ToHere (Change {c} val_new)) with (decEq c r)
  handle (Store loc) (ToHere (Change (Exactly val_new))) | Yes Refl = do
    loc := val_new
    pure $ Store loc
  handle (Store loc) (ToHere (Change (Anything)))        | Yes Refl = trace CouldNotChange $ Store loc
  handle (Store loc) (ToHere (Change _))                 | No _     = trace CouldNotChange $ Store loc

-- Pass to left or rght --
handle (And left rght) (ToLeft input) = do
  -- Pass the input to left
  left_new <- handle left input
  pure $ And left_new rght

handle (And left rght) (ToRight input) = do
  -- Pass the input to rght
  rght_new <- handle rght input
  pure $ And left rght_new

handle (Or left rght) (ToLeft input) = do
  -- Pass the input to left
  left_new <- handle left input
  pure $ Or left_new rght

handle (Or left rght) (ToRight input) = do
  -- Pass the input to rght
  rght_new <- handle rght input
  pure $ Or left rght_new

-- Interact --
handle task@(Xor left _) (ToHere (Pick (GoLeft p))) =
  -- Go left
  --FIXME: add failing for left?
  handle (assert_smaller task (delabel left)) (ToHere (Pick p))

handle task@(Xor _ rght) (ToHere (Pick (GoRight p))) =
  -- Go rght
  --FIXME: add failing for rght?
  handle (assert_smaller task (delabel rght)) (ToHere (Pick p))

handle task (ToHere (Pick GoHere)) =
  -- Go here
  pure $ task

handle task@(Xor _ _) (ToHere (PickWith l)) =
  case find l task of
    Nothing => trace (CouldNotFind l) task
    --XXX: needs `assert_smaller` for totallity, be aware of long type checks...
    -- Just p  => handle task (assert_smaller (ToHere (PickWith l)) (ToHere (Pick p)))
    Just p  => handle task (ToHere (Pick p))

handle task@(Next this cont) (ToHere Continue) =
  -- When pressed continue rewrite to an internal step
  pure $ Then this cont

handle task@(Next this cont) (ToHere (ContinueWith l)) =
  case !(value this) of
    Nothing => trace CouldNotContinue task
    Just v  =>
      let
        next = cont v
      in
      case find l next of
        Nothing => trace (CouldNotFind l) task
        Just p  => handle next (ToHere (Pick p))

-- Pass to this --
handle (Then this cont) input = do
  -- Pass the input to this
  this_new <- handle this input
  pure $ Then this_new cont

handle (Next this cont) input = do
  -- Pass the input to this
  this_new <- handle this input
  pure $ Next this_new cont

-- Label --
handle (Label l this) input with (keeper this)
  | False = handle this input
  | True = do
      this_new <- handle this input
      pure $ Label l this_new

-- Rest --
handle task input =
  -- Case `Fail`: Evaluation continues indefinitely
  trace (CouldNotHandle input) task

covering
drive : MonadTrace NotApplicable m => MonadRef l m => TaskT m a -> Input -> m (TaskT m a)
drive task input =
  handle task input >>= normalise

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
plus2 : Nat -> Nat -> Nat
plus2 Z y = y
plus2 (S k) y = S (plus2 k y)

reverse : List a -> List a
reverse xs = revAcc [] xs where
  revAcc : List a -> List a -> List a
  revAcc acc [] = acc
  revAcc acc (x :: xs) = revAcc (x :: acc) xs

-- foo : Int -> Int
-- foo x = case isLT of
--             Yes => x*2
--             No => x*4
--     where
--        data MyLT = Yes | No
--
--        isLT : MyLT
--        isLT = if x < 20 then Yes else No

mutual
  even : Nat -> Bool
  even Z = True
  even (S k) = odd k

  odd : Nat -> Bool
  odd Z = False
  odd (S k) = even k

-- test : List Nat
-- test = [c (S 1), c Z, d (S Z)]
--   where c : Nat -> Nat
--     c x = 42 + x
--
--     d : Nat -> Nat
--     d y = c (y + 1 + z y)
--       where z : Nat -> Nat
--         z w = y + w

partial fromMaybe : Maybe a -> a
fromMaybe (Just x) = x

max_stars_repo_name: nunet-io/snet-ai-dsl

max_issues_repo_name: nunet-io/snet-ai-dsl

max_forks_repo_name: nunet-io/snet-ai-dsl


text:
module Main

%language TypeProviders

implicit intString : Int -> String
intString = show

f : Int
f = the Int 2

main : IO ()
main = do args <- getArgs
          case args of
               -- one arg followed by another arg, followed by one or many args
               (_ :: arg :: _) => putStrLn arg
               -- exactly one arg:
               -- [_, arg, _] => putStrLn arg
               _ => putStrLn $ show $ f -- "need some args"

-- type providers

strToType : String -> Type
strToType "Int" = Int
strToType _ = Nat

fromFile : String -> IO (Provider Type)
fromFile fname = do str <- readFile fname
                    case str of
                         Right value =>
                            return (Provide (strToType (trim value)))
                         _ => return (Error "fail")

%provide (T1 : Type) with fromFile "theType"

foo : T1
foo = 1

-- hlists

namespace HList
  data HList : List Type -> Type where
       Nil : HList []
       (::) : a -> HList xs -> HList (a :: xs)

t: Integer -> Integer
t x = x * 2

hhead: HList(t :: ts) -> t --Type -> Type -- HList
hhead (l :: _) = l

htail: HList(t :: ts) -> HList ts --Type -> Type -- HList
htail (_ :: tail) = tail

hmap: {F: Type -> Type} -> ({a: Type} -> a -> F a) -> HList ts -> HList(map F ts)
hmap f [] = []
hmap f (x :: xs) = f x :: (hmap f xs)

max_stars_repo_name: joprice/idris-scratchpad

max_issues_repo_name: joprice/idris-scratchpad

max_forks_repo_name: joprice/idris-scratchpad


text:
module Unsigned

%access export
%default total

||| An unsigned binary number represented with `n` bits
data Unsigned : (n : Nat) -> Type where
  ||| Built from an underlying integer
  U : Integer -> Unsigned n

-- We could require a proof for this contructor that our Integer is indeed in
-- the range 0 -> 2*n-1. We don't bother because only (trusted) functions in
-- this module can use the constructor.

||| Cast instance for `Unsigned n` to an integer
Cast (Unsigned n) Integer where
  cast (U x) = x

||| Eq instacne for equality of `Unsigned n`
Eq (Unsigned n) where
  (==) (U x) (U y) = x==y

||| Ord instance for ordering of `Unsigned n`
Ord (Unsigned n) where
  compare (U x) (U y) = compare x y

||| MinBound instance for generating extremes of `Unsigned n`
MinBound (Unsigned n) where
  minBound = U 0

||| MaxBound instance for generating extremes of `Unsigned n`
MaxBound (Unsigned n) where
  maxBound = U $ cast (power 2 n)-1

||| Safely create an `Unsigned n` from an Integer using saturation
saturate : Integer -> Unsigned n
saturate x = let tryU = U {n} x
             in if tryU > maxBound then maxBound else
                if tryU < minBound then minBound else tryU

||| Num instance for saturating arithmetic with `Unsigned n`
Num (Unsigned n) where
  (+) (U x) (U y) = saturate $ (x+y)
  (*) (U x) (U y) = saturate $ (x*y)
  fromInteger x   = saturate $ x

||| Minus operations for two `Unsigned`s. Note that we cannot implement the Neg
||| typeclass because there are no negative representations.
minus : Unsigned n -> Unsigned n -> Unsigned n
minus (U x) (U y) = U (x-y)

||| Helper function to prove that 2^n for all natural n is not 0
private
powerTwoIsNotZ : (n : Nat) -> Not (power 2 n = 0)
powerTwoIsNotZ n = believe_me -- TODO prove properly

||| Add operations for two `Unsigned`s with wrapping overflow.
addWrap : Unsigned n -> Unsigned n -> Unsigned n
addWrap (U x) (U y) = let max = power 2 n
                          res = cast x + cast y
                      in U . cast $ modNatNZ res max (powerTwoIsNotZ n)

||| Minus operations for two `Unsigned`s with wrapping overflow.
minusWrap : Unsigned n -> Unsigned n -> Unsigned n
minusWrap (U x) (U y) = let max = power 2 n
                            res = max + cast x `minus` cast y
                        in U . cast $ modNatNZ res max (powerTwoIsNotZ n)

||| Show instance for printing `Unsigned n`
Show (Unsigned n) where
  show (U x) = "U" ++ show n ++ " " ++ show x

-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:


text:
incDim : Array (m * n::xs) t ->
         Array (m::n::xs) t

incDim v {m = Z}  = []
incDim v {m = S r} {n} =
    let (fstN, rest) =
      (take n v, drop n v) in
        fstN :: (incDim rest)

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
module CupCap

import Data.Vect
import VectHelp
import ProcessLib
import Proto
import Primitives

%default total

capT': Slot a -> Hom [] [Up a, Down a]
capT' {a} EmptySlot = do Just blam <- Respond initResp | _ => Loop (capT' EmptySlot)
                         Loop (capT' (fillSlot blam))
  where
    fillSlot: Req (MkNiche [] [Up a, Down a]) -> Slot a
    fillSlot (Conn (BotOutWire (There Here)) pid target) = FullSlot pid target
    fillSlot (Val _ _)                                   = EmptySlot
    fillSlot (Conn (BotOutWire (There (There _))) _ _)   impossible
    fillSlot (Conn (TopOutWire Here) _ _)                impossible
    fillSlot (Conn (TopOutWire (There _)) _ _)           impossible

    initResp: (msg: Req (MkNiche [] [Up a, Down a])) ->
              SubProc (MkNiche [] [Up a, Down a]) (ProcIF (MkNiche [] [Up a, Down a]) msg)
    initResp (Conn (BotOutWire (There Here)) _ _)      = do Action $ putStrLn "cap: accepted connection request"
                                                            Pure ConnAccepted
    initResp (Val _ _)                                 = do Action $ putStrLn "cap: got val before initialised"
                                                            Pure Error
    initResp (Conn (BotOutWire (There (There _))) _ _) impossible
    initResp (Conn (TopOutWire _) _ _)                 impossible

capT' {a} (FullSlot pid target) = do Action $ putStrLn "cap: starting loop"
                                     Respond (normal pid target)
                                     Loop (capT' (FullSlot pid target))
  where
    normal : MessagePID (ProcIF niche) ->
             InWire niche a ->
             (msg : Req (MkNiche [] [Up a, Down a])) ->
             SubProc (MkNiche [] [Up a, Down a]) (ProcIF (MkNiche [] [Up a, Down a]) msg)
    normal _ _ (Conn _ _ _) = do Action $ putStrLn "ERROR: cap got conn req when taken"
                                 Pure Taken
    normal _ _ (Val (BotInWire Here) x)              = do Action $ putStrLn $ "Passing through cap!"
                                                          r <- Request pid (Val target x)
                                                          Action $ putStrLn $ "cap got resp: " ++ show r
                                                          Pure r
    normal _ _ (Val (TopInWire _) _)                 impossible
    normal _ _ (Val (BotInWire (There (There _))) _) impossible

-- cap going the other way

cap': Slot a -> Hom [] [Down a, Up a]
cap' {a} EmptySlot = do Just blam <- Respond initResp | _ => Loop (cap' EmptySlot)
                        Loop (cap' (fillSlot blam))
  where
    -- TODO: the following two functions do the same deconstructing work
    fillSlot: Req (MkNiche [] [Down a, Up a]) -> Slot a
    fillSlot (Conn (BotOutWire Here) pid tar) = FullSlot pid tar
    fillSlot (Val _ _) = EmptySlot
    fillSlot (Conn (BotOutWire (There (There later))) pid tar) impossible
    fillSlot (Conn (TopOutWire Here) _ _) impossible
    fillSlot (Conn (TopOutWire (There _)) _ _) impossible

    initResp: (msg: Req (MkNiche [] [Down a, Up a])) ->
              SubProc (MkNiche [] [Down a, Up a]) (ProcIF (MkNiche [] [Down a, Up a]) msg)
    initResp (Conn (BotOutWire Here) pid tar) = Pure ConnAccepted
    initResp (Val _ _) = Pure Error
    initResp (Conn (BotOutWire (There (There later))) pid tar) impossible
    initResp (Conn (TopOutWire Here) _ _) impossible
    initResp (Conn (TopOutWire (There _)) _ _) impossible

-- do Action $ putStrLn $ "Passing through cap!"
--                                              r <- Request pid (Val target x)
--                                              Action $ putStrLn $ "capS got response: " ++ show r
--                                              Pure r

cap' {a} slot@(FullSlot pid target) = do Just msg <- Respond normal | _ => Loop (cap' slot)
                                         forward msg
                                         Loop (cap' slot)
  where
    forward : Req (MkNiche [] [Down a, Up a]) ->
              Process (ProcIF (MkNiche [] [Down a, Up a])) () Sent Sent
    forward (Conn _ _ _) = Pure ()
    forward (Val (BotInWire (There Here)) x) = do Request pid (Val target x)
                                                  Action $ putStrLn "passing through capS!"
    forward (Val (BotInWire (There (There l))) _) = absurd l
    forward (Val (TopInWire e) _) = absurd e

    normal : (msg : Req (MkNiche [] [Down a, Up a])) ->
             SubProc (MkNiche [] [Down a, Up a]) (ProcIF (MkNiche [] [Down a, Up a]) msg)
    normal (Val (BotInWire (There Here)) x) = Pure Accepted
    normal (Conn _ _ _) = do Action $ putStrLn "ERROR: cap got conn req when taken"
                             Pure Taken
    normal (Val (BotInWire (There (There l))) _) = absurd l
    normal (Val (TopInWire e) _) = absurd e

-- cup

cup': Slot a -> Hom [Down a, Up a] []
cup' {a} EmptySlot = do Just blam <- Respond initResp | _ => Loop (cup' EmptySlot)
                        Loop (cup' (fillSlot blam))
  where
    fillSlot: Req (MkNiche [Down a, Up a] []) -> Slot a
    fillSlot (Conn (TopOutWire (There Here)) pid tar) = FullSlot pid tar
    fillSlot (Val inWire y) = EmptySlot
    fillSlot (Conn (TopOutWire (There (There later))) pid tar) impossible
    fillSlot (Conn (BotOutWire Here) _ _) impossible
    fillSlot (Conn (BotOutWire (There _)) _ _) impossible

    initResp: (msg: Req (MkNiche [Down a, Up a] [])) ->
              SubProc (MkNiche [Down a, Up a] []) (ProcIF (MkNiche [Down a, Up a] []) msg)
    initResp (Conn (TopOutWire (There Here)) pid tar) = do --Action $ putStrLn $ "cup: accepted conn req"
                                                           Pure ConnAccepted
    initResp (Val inWire y) = do Action $ putStrLn "ERROR: cup: got val when not ready"
                                 Pure Error
    initResp (Conn (TopOutWire (There (There later))) pid tar) impossible
    initResp (Conn (BotOutWire Here) _ _) impossible
    initResp (Conn (BotOutWire (There _)) _ _) impossible

cup' {a} (FullSlot pid target) = do Just msg <- Respond normal | _ => Loop (cup' (FullSlot pid target))
                                    forward msg
                                    Loop (cup' (FullSlot pid target))
  where
    forward : Req (MkNiche [Down a, Up a] []) ->
              Process (ProcIF (MkNiche [Down a, Up a] [])) () Sent Sent
    forward (Conn _ _ _) = Pure ()
    forward (Val (BotInWire _) _) = Pure ()
    forward (Val (TopInWire Here) x) = do Action $ putStrLn "cup: about to forward"
                                          r <- Request pid (Val target x)
                                          Action $ putStrLn $ "cup: forward result: " ++ show r
    forward (Val (TopInWire (There (There _))) _) impossible

    normal : (msg : Req (MkNiche [Down a, Up a] [])) ->
             SubProc (MkNiche [Down a, Up a] []) (ProcIF (MkNiche [Down a, Up a] []) msg)
    normal (Conn _ _ _) = do Action $ putStrLn "ERROR: cup got conn req when taken"
                             Pure Taken
    normal (Val (TopInWire Here) x) = Pure Accepted
    normal (Val (TopInWire (There (There later))) x) impossible
    normal (Val (BotInWire Here) _) impossible
    normal (Val (BotInWire (There _)) _) impossible

-- public:

export capT: Hom [] [Up a, Down a]
capT = capT' EmptySlot

export cap: Hom [] [Down a, Up a]
cap = cap' EmptySlot

export cup: Hom [Down a, Up a] []
cup = cup' EmptySlot

max_stars_repo_name: jameshaydon/smproc

max_issues_repo_name: jameshaydon/smproc

max_forks_repo_name: jameshaydon/smproc


text:
module Inigo.Paths

import public System.Path

export
inigoTomlPath : String
inigoTomlPath = "Inigo.toml"

export
inigoDhallPath : String
inigoDhallPath = "Inigo.dhall"

export
inigoIPkgPath : String
inigoIPkgPath = "Inigo.ipkg"

export
inigoWorkDir : String
inigoWorkDir = "./.inigo-work"

export
inigoDepDir : String
inigoDepDir = inigoWorkDir </> "deps"

export
inigoDepPkgCache : String
inigoDepPkgCache = inigoWorkDir </> "deps.cache"

export
DEBUG : Bool
DEBUG = True

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Main

import Specdris.SpecIO
import VirtualDOM
import VirtualDOM.DOM

querySelector : String -> JS_IO Ptr
querySelector = jscall "document.querySelector(%0)" _

isNull : Ptr -> JS_IO Bool
isNull ptr = (== "true") <$>
  jscall "(%0 === null) + ''" (Ptr -> JS_IO String) ptr

selectorExists : String -> JS_IO Bool
selectorExists selector = not <$> (querySelector selector >>= isNull)

dispatchEventOnId : (eventName : String) -> (elementId : String) -> JS_IO ()
dispatchEventOnId eventName elementId = do
  getElementById elementId >>= dispatchEvent eventName True
  pure ()

assertSelect : (shouldExist : Bool) -> (selector : String) ->
                          JS_IO SpecResult
assertSelect shouldExist selector = do
  exists <- selectorExists selector
  let reason =
    if shouldExist
      then "selector should match elements"
      else "selector should not match elements"
  if exists == shouldExist
    then pure Success
    else pure $ UnaryFailure selector reason

shouldSelect : String -> JS_IO SpecResult
shouldSelect = assertSelect True

shouldNotSelect : String -> JS_IO SpecResult
shouldNotSelect = assertSelect False

appendBodyParagraph : JS_IO ()
appendBodyParagraph = do
  body <- documentBody
  paragraph <- createElement "p"
  appendChild body paragraph
  pure ()

appendBodyParagraphWithId : String -> JS_IO ()
appendBodyParagraphWithId elementId = do
  body <- documentBody
  paragraph <- createElement "p"
  setAttribute paragraph "id" elementId
  appendChild body paragraph
  pure ()

elementsSpec : SpecTree' FFI_JS
elementsSpec =
  describe "elements" $ do
    it "creates a single element" $ do
      body <- documentBody
      render body Nothing $ Just $ node "p" [] [] []
      shouldSelect "p"
    it "creates a nested element" $ do
      body <- documentBody
      render body Nothing $ Just $ node "p" [] [] [ node "span" [] [] []
                               ]
      shouldSelect "p > span"
    it "creates elements in the given order" $ do
      body <- documentBody
      render body Nothing $ Just $ node "div" [] [] [ node "p" [] [] []
                                 , node "span" [] [] []
                                 ]
      para1st <- shouldSelect "p:nth-child(1)"
      span2nd <- shouldSelect "span:nth-child(2)"
      pure $ para1st >>= const span2nd
    it "creates an element on a specified parent" $ do
      let divId = "putithere"
      body <- documentBody
      render body Nothing $ Just $ node "div" [] [("id", divId)] []
      parentDiv <- getElementById divId
      render parentDiv Nothing $ Just $ node "p" [] [] []
      shouldSelect "div > p"

attributesSpec : SpecTree' FFI_JS
attributesSpec =
  describe "attributes" $ do
    it "sets a single attribute on an element" $ do
      body <- documentBody
      render body Nothing $ Just $ node "p" [] [("class", "testval")] []
      shouldSelect "p.testval"
    it "overwrites attributes with duplicate keys" $ do
      body <- documentBody
      render body Nothing $ Just $ node "p" [] [ ("class", "badval")
                            , ("class", "goodval")
                            ] []
      noBadval <- shouldNotSelect "p.badval"
      hasGoodval <- shouldSelect "p.goodval"
      pure $ noBadval >>= const hasGoodval
    it "sets multiple attributes on an element" $ do
      body <- documentBody
      render body Nothing $ Just $ node "p" [] [ ("class", "classval")
                            , ("title", "titleval")
                            ] []
      shouldSelect "p.classval[title=titleval]"
    it "sets different attributes on multiple elements" $ do
      body <- documentBody
      render body Nothing $ Just $ node "div" [] [] [ node "p" [] [("class", "a")] []
                                 , node "p" [] [("class", "b")] []
                                 ]
      a <- shouldSelect "p.a"
      b <- shouldSelect "p.b"
      ab <- shouldNotSelect "p.a.b"
      pure $ a >>= const b >>= const ab

eventsSpec : SpecTree' FFI_JS
eventsSpec =
  describe "events" $ do
    it "executes an event handler" $ do
      body <- documentBody
      render body Nothing $ Just $ node "button"
        [on "click" (const appendBodyParagraph) noOptions] [("id", "doit")] []
      dispatchEventOnId "click" "doit"
      shouldSelect "p"
    it "does not execute a handler before dispatch" $ do
      body <- documentBody
      render body Nothing $ Just $ node "button"
        [on "click" (const appendBodyParagraph) noOptions] [("id", "doit")] []
      pre <- shouldNotSelect "p"
      dispatchEventOnId "click" "doit"
      post <- shouldSelect "p"
      pure $ pre >>= const post
    it "respects the once option on listeners" $ do
      let opts = record { once = Just True } noOptions
      body <- documentBody
      render body Nothing $ Just $ node "button"
        [on "click" (const appendBodyParagraph) opts] [("id", "doit")] []
      dispatchEventOnId "click" "doit"
      dispatchEventOnId "click" "doit"

      p1 <- shouldSelect "p:only-of-type"
      p2 <- shouldNotSelect "p:nth-of-type(2)"
      pure $ p1 >>= const p2
    it "responds on capture when capture == true" $ do
      let opts = record { capture = Just True } noOptions
      body <- documentBody
      render body Nothing $ Just $ node "div"
        [ on "click" (const $ appendBodyParagraphWithId "first") opts] []
        [ node "button"
            [on "click" (const $ appendBodyParagraphWithId "second") opts]
            [("id", "doit")] []
        ]
      dispatchEventOnId "click" "doit"
      p1 <- shouldSelect "p#first:nth-of-type(1)"
      p2 <- shouldSelect "p#second:nth-of-type(2)"
      pure $ p1 >>= const p2
    it "responds on bubble when capture == false" $ do
      let opts = record { capture = Just False } noOptions
      body <- documentBody
      render body Nothing $ Just $ node "div"
        [ on "click" (const $ appendBodyParagraphWithId "second") opts] []
        [ node "div"
            [ on "click" (const $ appendBodyParagraphWithId "first") opts ]
            [("id", "doit")] []
        ]
      dispatchEventOnId "click" "doit"
      p1 <- shouldSelect "p#first:nth-of-type(1)"
      p2 <- shouldSelect "p#second:nth-of-type(2)"
      pure $ p1 >>= const p2

elementsSpecSubsequent : SpecTree' FFI_JS
elementsSpecSubsequent =
  describe "elements" $ do
    it "leaves empty DOM empty when old and new virtual DOMs are Nothing" $ do
      body <- documentBody
      pre <- shouldNotSelect "body *"
      render body Nothing Nothing
      post <- shouldNotSelect "body *"
      pure $ pre >>= const post
    it "empties DOM when old virtual DOM is Just and new one is Nothing" $ do
      body <- documentBody
      let html = node "div" [] [] [ node "p" [] [] [] ]
      render body Nothing (Just html)
      pre <- shouldSelect "body > div > p"
      render body (Just html) Nothing
      post <- shouldNotSelect "body *"
      pure $ pre >>= const post
    it "replaces DOM elements when old and new virtual DOMs are Just" $
      let
        oldHtml = Just $ node "div" [] []
          [ node "p" [] [] [ text "paragraph 1" ]
          , node "p" [] [] [ text "paragraph 2" ]
          ]
        newHtml = Just $ node "p" [] []
          [ node "div" [] [] [ text "div 1" ]
          , node "div" [] [] [ text "div 2" ]
          ]
      in do
        body <- documentBody
        render body Nothing oldHtml
        render body oldHtml newHtml
        noDiv <- shouldNotSelect "body > div"
        twoParas <- shouldSelect "body > p > div:nth-of-type(2)"
        pure $ noDiv >>= const twoParas

attributesSpecSubsequent : SpecTree' FFI_JS
attributesSpecSubsequent =
  describe "attributes" $ do
    it "removes element attributes when they are in old virtual DOM and not in new" $
      let
        oldHtml = Just $ node "div" []
          [ ("style", "color:red")
          , ("title", "The div")
          ] []
        newHtml = Just $ node "div" []
          [ ("title", "The div") ] []
      in do
        body <- documentBody
        render body Nothing oldHtml
        pre <- shouldSelect "body > div[style][title]"
        render body oldHtml newHtml
        noStyle <- shouldNotSelect "body > div[style][title]"
        hasTitle <- shouldSelect "body > div[title]"
        pure $ pre >>= const noStyle >>= const hasTitle
    it "adds element attributes when they are in new virtual DOM and not in old" $
      let
        oldHtml = Just $ node "div" []
          [ ("title", "The div") ] []
        newHtml = Just $ node "div" []
          [ ("style", "color:red")
          , ("title", "The div")
          ] []
      in do
        body <- documentBody
        render body Nothing oldHtml
        pre1 <- shouldNotSelect "body > div[style][title]"
        pre2 <- shouldSelect "body > div[title]"
        render body oldHtml newHtml
        post <- shouldSelect "body > div[style][title]"
        pure $ pre1 >>= const pre2 >>= const post

eventsSpecSubsequent : SpecTree' FFI_JS
eventsSpecSubsequent =
  describe "events" $ do
    it "does not execute removed event handlers" $ do
      let makeButton = \handlers =>
        Just $ node "button" handlers [("id", "doit")] []
      let html1 = makeButton [on "click" (const appendBodyParagraph) noOptions]
      let html2 = makeButton []
      body <- documentBody
      render body Nothing html1
      render body html1 html2
      dispatchEventOnId "click" "doit"
      shouldNotSelect "p"
    it "executes replacement event handlers" $ do
      let makeButton = \handlers =>
        Just $ node "button" handlers [("id", "doit")] []
      let makeHandler = \paraId =>
        on "click" (const $ appendBodyParagraphWithId paraId) noOptions
      let html1 = makeButton [makeHandler "old"]
      let html2 = makeButton [makeHandler "new"]
      body <- documentBody
      render body Nothing html1
      render body html1 html2
      dispatchEventOnId "click" "doit"
      shouldSelect "p#new"
    it "leaves descendants intact when replacing handlers" $
      let
        makeHtml = \event => Just $
          node "div" [ on event (const $ pure ()) noOptions ] []
            [ node "p" [] []
              [ node "button" [] [("id","thebutton")] [] ]
            , node "span" [] [("id","thespan")] []
            ]
        html1 = makeHtml "mousedown"
        html2 = makeHtml "mouseup"
      in do
        body <- documentBody
        render body Nothing html1
        render body html1 html2
        btnExists <- shouldSelect "div>p>button#thebutton"
        spanExists <- shouldSelect "div>span:nth-child(2)#thespan"
        pure $ btnExists >>= const spanExists

clearBody : JS_IO SpecResult -> JS_IO SpecResult
clearBody resultIO = do
  result <- resultIO
  body <- documentBody
  setInnerHTML body ""
  pure result

main : JS_IO ()
main = specIO' {around = clearBody} $ do
  describe "initial rendering" $ do
    elementsSpec
    attributesSpec
    eventsSpec
  describe "subsequent rendering" $ do
    elementsSpecSubsequent
    attributesSpecSubsequent
    eventsSpecSubsequent

max_stars_repo_name: concert/idris-vdom

max_issues_repo_name: concert/idris-vdom

max_forks_repo_name: concert/idris-vdom


text:
-- -------------------------------------------------------------- [ ReSkin.idr ]
-- Module    : ReSkin.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| TODO list achieved through reskinning the GRL.
module GRL.Test.DSML.TLang

import public GRL.Common
import public GRL.IR
import public GRL.Model
import public GRL.Builder
import public GRL.Pretty

%access public export

-- --------------------------------------------------------- [ DSML Definition ]

data ETy = TaskTy | STaskTy | ActionTy
data TTy = ElemTy ETy | LinkTy | SubLinkTy

data ValidAction : ETy -> ETy -> Type where
  TaskAction    : ValidAction ActionTy TaskTy
  SubTaskAction : ValidAction ActionTy STaskTy

data TLang : TTy -> GTy -> Type where
  MkTask   : String -> TLang (ElemTy TaskTy)   ELEM
  MkSTask  : String -> TLang (ElemTy STaskTy)  ELEM
  MkAction : String -> TLang (ElemTy ActionTy) ELEM

  ActsOn  : CValue
         -> TLang (ElemTy x) ELEM
         -> TLang (ElemTy y) ELEM
         -> {auto prf : ValidAction x y}
         -> TLang LinkTy INTENT

  HasSubTask : TLang (ElemTy TaskTy) ELEM
            -> TLang (ElemTy STaskTy) ELEM
            -> TLang SubLinkTy STRUCT

GRL (\x => TLang ty x) where
  mkElem (MkTask s)   = Elem GOALty s Nothing
  mkElem (MkSTask s)  = Elem GOALty s Nothing
  mkElem (MkAction s) = Elem TASKty s (Just SATISFIED)

  mkIntent (ActsOn c x y) = ILink IMPACTSty c (mkElem x) (mkElem y)

  mkStruct (HasSubTask x y) = SLink ANDty (mkElem x) [(mkElem y)]

-- ------------------------------------------------------------ [ Pretty Stuff ]

syntax [a] "==>" [b] "|" [c] = ActsOn c a b
syntax [a] "&=" [b]          = HasSubTask a b

TASK : Type
TASK = TLang (ElemTy TaskTy) ELEM

SUBTASK : Type
SUBTASK = TLang (ElemTy STaskTy) ELEM

ACTION : Type
ACTION = TLang (ElemTy ActionTy) ELEM

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Test

export
pythag : Int -> List (Int, Int, Int)
pythag max
    = [ (x,y,z) | z <- [1..max],
                  y <- [1..z],
                  x <- [1..y],

                  x * x + y * y == z * z ]

namespace Inside
  -- Needs to be recursive (or at least refer to a name in this module)
  -- to check that definitions are updated on import...as
  export
  fact : Nat -> Nat
  fact Z = 1
  fact (S k) = (S k) * fact k

public export
interface Needle a where
  nardle : a -> a
  noo : a -> a


text:
module TypeDrivenDevelopment

||| Map a list of strings to their length
allLengths : List String -> List Nat
allLengths xs = map length xs

||| Negate a boolean
invert : (t : Bool) -> Bool
invert True = False
invert False = True

||| Describe whether a list is empty or not
describeList : List Int -> String
describeList [] = "Empty"
describeList (x :: xs) = "Non-empty"

xor : Bool -> Bool -> Bool
xor False y = y
xor True y = not y

mutual
  isEven : Nat -> Bool
  isEven Z = True
  isEven (S k) = isOdd k

  isOdd : Nat -> Bool
  isOdd Z = False
  isOdd (S k) = isEven k

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
import System.File
import Data.Strings
import Data.List1
import Data.List

selfClosing : List String
selfClosing = ["area", "base", "br", "col", "command", "embed", "hr", "img", "input", "keygen", "link", "param", "meta", "track", "wbr"]

idrisReserved : List String
idrisReserved = ["data"]

tagType : String
tagType = "List Attribute -> List (DOM V) -> DOM V"

voidTagType : String
voidTagType = "List Attribute -> DOM V"

getTags : IO (Maybe (List String))
getTags = do
  input <- readFile ("tags.txt")
  case input of
       Right contents => pure . Just . filter (\line => line /= "") . forget . lines $ contents
       Left err => pure Nothing

header : String
header = """
  -- This file is automatically generated, do not edit
  module TagList
  import Attributes
  import VNode
  """

makeTag : String -> String
makeTag tag = let
  tag = trim tag
  tagName = if elem tag idrisReserved
               then tag ++ "'"
               else tag
  tagString = "\"" ++ tag ++ "\""

  (tagFunc, tagType) = if elem tag selfClosing
                          then ("defineVoidTag", voidTagType)
                          else ("defineTag", tagType)
  in
  unlines ["export", tagName ++ " : " ++ tagType, tagName ++ " = " ++ tagFunc ++ " " ++ tagString, ""]

main : IO ()
main = do
  Just tags <- getTags
    | Nothing => putStrLn "Failed to read tags"
  let contents = header ++ "\n\n" ++ (unlines . map makeTag $ tags)
  _ <- writeFile "TagList.idr" contents
  pure ()

max_stars_repo_name: Stinners/alder

max_issues_repo_name: Stinners/alder

max_forks_repo_name: Stinners/alder


text:
module PhysicistsQueue

import Queue

%default total
%access private

export
data PhysicistsQueue a = PQ (List a) Int (Lazy (List a)) Int (List a)

checkw : List a -> Int -> List a -> Int -> List a -> PhysicistsQueue a
checkw [] lenf f lenr r = PQ f lenf f lenr r
checkw w  lenf f lenr r = PQ w lenf f lenr r

check : List a -> Int -> List a -> Int -> List a -> PhysicistsQueue a
check w lenf f lenr r =
  if lenr <= lenf then checkw w lenf f lenr r
  else checkw f (lenf + lenr) (f ++ reverse r) 0 []

export
Queue PhysicistsQueue where
  empty = PQ [] 0 [] 0 []
  isEmpty (PQ w lenf f lenr r) = lenf == 0

  snoc (PQ w lenf f lenr r) x = check w lenf f (lenr + 1) (x :: r)

  head (PQ []       lenf f lenr r) = idris_crash "empty queue"
  head (PQ (x :: w) lenf f lenr r) = x

  tail (PQ []       lenf f lenr r) = idris_crash "empty queue"
  tail (PQ (x :: w) lenf f lenr r) = check w (lenf - 1) (Prelude.List.tail {ok = nef} f) lenr r
   where nef = believe_me "f = x :: w ++ _"


text:
module Main

data Format = End | FInt Format | FStr Format | FChar Char Format

fromList : List Char -> Format
fromList Nil                = End
fromList ('%' :: 'd' :: cs) = FInt    (fromList cs)
fromList ('%' :: 's' :: cs) = FStr (fromList cs)
fromList (c :: cs)          = FChar c (fromList cs)

PrintfType : Format -> Type
PrintfType End            = String
PrintfType (FInt rest)    = Int -> PrintfType rest
PrintfType (FStr rest) = String -> PrintfType rest
PrintfType (FChar c rest) = PrintfType rest

printf : (fmt: String) -> PrintfType (fromList $ unpack fmt)
printf fmt = printFormat (fromList $ unpack fmt) where
 printFormat : (fmt: Format) -> PrintfType fmt
 printFormat fmt = rec fmt "" where
   rec : (f: Format) -> String -> PrintfType f
   rec End acc            = acc
   rec (FInt rest) acc    = \i: Int => rec rest (acc ++ (show i))
   rec (FStr rest) acc = \s: String => rec rest (acc ++ s)
   rec (FChar c rest) acc = rec rest (acc ++ (strCons c ""))

test : String
test = printf "The %s is %d" "answer" 42

main : IO ()
main = putStrLn test

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
import Control.Monad.Identity
import System

fib : Integer -> Identity Integer
fib 0 = pure 0
fib 1 = pure 1
fib n = pure $ !(fib (n - 1)) + !(fib (n - 2))

main : IO ()
main = do
  value <- getLine
  printLn $ runIdentity (fib (cast value))


text:
module Foo

plusAssoc : plus n (plus m o) = plus (plus n m) o
plusAssoc = ?impl


text:
module Main

range : Int
range = 1000

testProg : Int -> Int
testProg n = loop n
where
	lmt : Int
	lmt = min (n + 100) range

	loop : Int -> Int
	loop i = if i >= lmt then i else loop (i + 1)

main : IO()
main = printLn $ testProg 0


text:
import Common

depVect : (init: Iso a b) ->
        (step: a -> Iso a b) ->
        Iso (Vect n a) (Vect n b)
depVect init step = MkIso (to init) (from init) (tf init) (ft init)
  where
  to : Iso a b -> Vect n a -> Vect n b
  to s [] = []
  to s (x::xs) = appIso s x :: to (step x) xs
  from : Iso a b -> Vect n b -> Vect n a
  from s [] = []
  from s (x::xs) = unappIso s x :: from (step (unappIso s x)) xs
  tf : (step : Iso a b) -> (v : Vect n b) -> to step (from step v) = v
  tf i [] = Refl
  tf i (x::xs) = rewrite (tf (step (unappIso i x)) xs) in case i of
    (MkIso ito ifrom itf ift) => cong (itf x) {f=flip (::) xs}
  ft : (step : Iso a b) -> (v : Vect n a) -> from step (to step v) = v
  ft i [] = Refl
  ft (MkIso ito ifrom itf ift) (x::xs) = rewrite (ift x) in cong (ft (step x) xs) {f=(::) x}

stateVect : (init: Iso a b) ->
          (initS: s) ->
          (step: s -> a -> s) ->
          (gen: s -> Iso a b) ->
          Iso (Vect n a) (Vect n b)
stateVect {s=s} i is step gen = MkIso (to is i) (from is i) (tf is i) (ft is i)
  where
  to : s -> Iso a b -> Vect n a -> Vect n b
  to _ _ [] = []
  to st iso (x::xs) = appIso iso x :: to (step st x) (gen (step st x)) xs
  from : s -> Iso a b -> Vect n b -> Vect n a
  from st iso [] = []
  from st iso (x::xs) = unappIso iso x :: from (step st (unappIso iso x)) (gen (step st (unappIso iso x))) xs
  tf : (st : s) -> (iso : Iso a b) -> (v : Vect n b) -> to st iso (from st iso v) = v
  tf _ _ [] = Refl
  tf st iso (x::xs) = rewrite (tf (step st (unappIso iso x)) (gen (step st (unappIso iso x))) xs) in
    case iso of
      (MkIso ito ifrom itf ift) => cong (itf x) {f=flip (::) xs}
  ft : (st : s) -> (iso : Iso a b) -> (v : Vect n a) -> from st iso (to st iso v) = v
  ft _ _ [] = Refl
  ft st (MkIso ito ifrom itf ift) (x::xs) = rewrite (ift x) in
     cong (ft (step st x) (gen (step st x)) xs) {f=(::) x}

-- examples

xor : Bool -> Bool -> Bool
xor = (/=)

xorTwice : (x,y : Bool) -> xor x (xor x y) = y
xorTwice True True = Refl
xorTwice False False = Refl
xorTwice False True = Refl
xorTwice True False = Refl

test : Iso (Vect n Bool) (Vect n Bool)
test = stateVect idIso False step gen
  where
    idIso = (MkIso id id (\x => Refl) (\x => Refl))
    -- change state when state and value match
    step True True = False
    step False False = True
    step s _ = s
    -- just xor with state
    gen s = MkIso (xor s) (xor s) (xorTwice s) (xorTwice s)

-- λΠ> appIso test [True, True, True, True, True, True, True]
-- [True, True, True, True, True, True, True] : Vect 7 Bool
-- λΠ> appIso test [False, True, False, True, False, True, False]
-- [False, False, False, False, False, False, False] : Vect 7 Bool
-- λΠ> appIso test [False, True, False, False, False, True, False]
-- [False, False, False, True, True, False, False] : Vect 7 Bool

test2 : Iso (Vect n Bool) (Vect n Bool)
test2 = stateVect idIso Z step gen
  where
    idIso = (MkIso id id (\x => Refl) (\x => Refl))
    step Z False = Z
    step (S n) False = n
    step n True = S n
    gen s = MkIso (xor (s == 0)) (xor (s == 0)) (xorTwice (s == 0)) (xorTwice (s == 0))

-- λΠ> appIso test2 [True, True, True, False, False, False, False]
-- [True, True, True, False, False, False, True] : Vect 7 Bool

max_stars_repo_name: defanor/morphisms

max_issues_repo_name: defanor/morphisms

max_forks_repo_name: defanor/morphisms


text:
module Data.DistinctElements

import public Data.Vect
import public Data.Function

%access public export
%default total

DistinctElements : Vect n a -> Type
DistinctElements [] = ()
DistinctElements (x :: xs) = (Not (Elem x xs), DistinctElements xs)

isDistinctElements : DecEq a => (xs : Vect n a) -> Dec (DistinctElements xs)
isDistinctElements [] = Yes ()
isDistinctElements (x :: xs) with (isElem x xs)
    | Yes p = No (\(f, _) => f p)
    | No p1 with (isDistinctElements xs)
        | Yes p2 = Yes (p1,p2)
        | No  p2 = No (\(_, d) => p2 d)

elemSplit : Elem x (y::xs) -> Either (x=y) (Elem x xs)
elemSplit Here {x = y} {y = y} {xs = xs} = Left Refl
elemSplit (There later) {x = x} {y = y} {xs = xs} = Right later

equalityElem : x=y -> Elem x (y::xs)
equalityElem Refl {x = x} {y = x} = Here

reduceNotElem : Not (Elem x (y::xs)) -> Not (Elem x xs)
reduceNotElem p Here {x = x} {xs = xs} impossible
reduceNotElem p (There _) {x = x} {xs = xs} impossible

notElemMapInjective : Injective f -> DistinctElements xs -> Not (Elem x xs) -> Elem (f x) (Prelude.Functor.map f xs) -> Void
notElemMapInjective inj p ne el {x} {xs=[]} = absurd el
notElemMapInjective inj (p,ps) ne el {f} {x} {xs=(y::xs)} = case elemSplit el of
    Left p2 => ne (equalityElem (inj p2))
    Right p2 => notElemMapInjective inj ps (reduceNotElem ne) p2

mapInjectiveFunction : Injective f -> DistinctElements xs -> DistinctElements (Prelude.Functor.map f xs)
mapInjectiveFunction inj p {f} {xs = []} = p
mapInjectiveFunction inj (p, ps) {f} {xs = (x::xs)} = (notElemMapInjective inj ps p, mapInjectiveFunction inj ps)


text:
some : Bool -> Bool
some True = True
some False = True
some False = True
some False = False


text:
module Main

import Erlang

intTest : IO ()
intTest = do
  putStrLn "intTest"
  let tuple = erlUnsafeCall (List Int) "test_support" "integers" []
  printLn tuple

integerTest : IO ()
integerTest = do
  putStrLn "integerTest"
  let tuple = erlUnsafeCall (List Integer) "test_support" "integers" []
  printLn tuple

stringTest : IO ()
stringTest = do
  putStrLn "stringTest"
  let tuple = erlUnsafeCall (List String) "test_support" "strings" []
  printLn tuple

charTest : IO ()
charTest = do
  putStrLn "charTest"
  let tuple = erlUnsafeCall (List Char) "test_support" "chars" []
  printLn tuple

doubleTest : IO ()
doubleTest = do
  putStrLn "doubleTest"
  let tuple = erlUnsafeCall (List Double) "test_support" "doubles" []
  printLn tuple

listTest : IO ()
listTest = do
  putStrLn "listTest"
  let tuple = erlUnsafeCall (List (List String)) "test_support" "lists" []
  printLn tuple

-- Skips function calls, (Raw a), ErlTerm for now

erlAtomTest : IO ()
erlAtomTest = do
  putStrLn "erlAtomTest"
  let tuple = erlUnsafeCall (List ErlAtom) "test_support" "erl_atoms" []
  printLn tuple

erlCharlistTest : IO ()
erlCharlistTest = do
  putStrLn "erlCharlistTest"
  let tuple = erlUnsafeCall (List ErlCharlist) "test_support" "erl_charlists" []
  printLn tuple

erlNilTest : IO ()
erlNilTest = do
  putStrLn "erlNilTest"
  let nil = erlUnsafeCall ErlNil "test_support" "erl_nil" []
  printLn nil

erlConsTest : IO ()
erlConsTest = do
  putStrLn "erlConsTest"
  let tuple = erlUnsafeCall (ErlTuple4 (ErlCons Integer Integer) (ErlCons Integer String) (ErlCons Integer ErlNil) (ErlCons Integer (ErlCons Integer ErlNil))) "test_support" "erl_cons" []
  printLn tuple

erlListTest : IO ()
erlListTest = do
  putStrLn "erlListTest"
  let tuple = erlUnsafeCall (ErlTuple2 (ErlList []) (ErlList [String, Int, Char])) "test_support" "erl_lists" []
  printLn tuple

erlTuplesTest : IO ()
erlTuplesTest = do
  putStrLn "erlTuplesTest"
  let tuple = erlUnsafeCall (ErlTuple5 ErlTuple0 (ErlTuple1 Int) (ErlTuple2 Int Int) (ErlTuple3 Int Int Int) (ErlTuple4 Int Int Int Int)) "test_support" "erl_tuples" []
  printLn tuple

main : IO ()
main = do
  intTest
  integerTest
  stringTest
  charTest
  doubleTest
  listTest
  erlAtomTest
  erlCharlistTest
  erlNilTest
  erlConsTest
  erlListTest
  erlTuplesTest


text:
module Mergesort

import Data.Vect

import Lecture.Evens

--Takes the first m elements from a vector
Vecttake : (m:Nat)->Vect n elem->Vect m  elem
Vecttake Z xs = []
Vecttake (S k) (x::xs) = x::(Vecttake k xs)

--Takes the last m elements from a vector
Vecttakefromlast :(m:Nat)->Vect n elem ->Vect m elem
Vecttakefromlast m xs = reverse (Vecttake  m (reverse xs))

insertend : (x:elem)->Vect n elem->Vect (S n) elem
insertend x [] = [x]
insertend x (y :: xs) = y::(insertend x xs)

half : (n: Nat) -> IsEven n -> Nat
half Z ZEven = 0
half (S (S k)) (SSEven k x) = S (half k x)

nOrSnEven: (n: Nat) -> Either (IsEven n) (IsEven (S n))
nOrSnEven Z = Left ZEven
nOrSnEven (S k) = case (nOrSnEven k) of
                       (Left l) => Right (SSEven k l)
                       (Right r) => Left r

--Defined in class. This is used to split the input vector into two parts.
--The length of the first part is halfRoof n.
halfRoof: Nat -> Nat
halfRoof n = case (nOrSnEven n) of
                  (Left nEven) => half n nEven
                  (Right snEven) => half (S n) snEven

--function that returns (n - halfRoof n) i.e. the length of the second part
--after input vector is split.
halfRoofComplement : Nat -> Nat
halfRoofComplement Z = Z
halfRoofComplement (S k) = halfRoof k

--function that splits a vector into two parts at its mid point.
--if n is even, it gives two halves of length n/2 each.
--if n is odd, the first half is (n+1)/2 length and the second half is
--(n-1)/2 length
halfVect : Vect n elem -> ((Vect (halfRoof n) elem), (Vect (halfRoofComplement n) elem))
halfVect {n} xs = ((Vecttake (halfRoof n) xs), (Vecttakefromlast (halfRoofComplement n) xs))

--this function is to cast a vector from one type to another
sillycast: (v1:(Vect ((S k) + j) elem)) ->( Vect (k+ (S j)) elem)
sillycast {k} {j} v1 = (Vecttake k v1) ++ (Vecttakefromlast (S j) v1)

--function to cast a vector from one type to another.
--makes the vector obtained on applying merge to two halves same as
--the type of the input vector.
sillycast2 : (Vect ((halfRoof n) + (halfRoofComplement n)) elem) -> Vect n elem
sillycast2 {n} xs = Vecttake n xs

--The merge function
merge1 :Ord elem =>Vect  n elem ->Vect  m elem ->Vect (n+m) elem
merge1 [] ys = ys
merge1  (x :: xs) [] =  (x::xs)++[]
merge1 {n= (S k)}{m= (S j)} (x :: xs) (y :: ys) = case x<=y of
                                 False => y::(sillycast( (merge1  (x::xs) ys)))
                                 True => x::(merge1 xs (y::ys))

--The mergesort function
mergesort :Ord elem => Vect n elem -> Vect n elem
mergesort [] = []
mergesort [x] = [x]
mergesort xs = sillycast2 (merge1 (mergesort (fst(halfVect xs))) (mergesort (snd(halfVect xs))))


text:
import Data.Vect

removeElem : (value : a) -> (xs : Vect (S n) a) -> {auto prf : Elem value xs} -> Vect n a
removeElem value (value :: ys) {prf = Here} = ys
removeElem value {n = Z} (y :: []) {prf = There later} = absurd later
removeElem value {n = (S k)} (y :: ys) {prf = There later} = y :: removeElem value ys

data WordState : (guessesRemaining : Nat) -> (letters : Nat) -> Type where
    MkWordState : (word : String) -> (missing : Vect letters Char) ->
        WordState guessesRemaining letters

data Finished : Type where
    Lost : (game : WordState 0 (S letters)) -> Finished
    Won : (game : WordState (S guesses) 0) -> Finished

data ValidInput : List Char -> Type where
    Letter : (c : Char) -> ValidInput [c]

notEmpty : ValidInput [] -> Void
notEmpty (Letter _) impossible

multipleLetters : ValidInput (x :: (y :: xs)) -> Void
multipleLetters (Letter _) impossible

isValidInput : (cs : List Char) -> Dec (ValidInput cs)
isValidInput [] = No notEmpty
isValidInput (x :: []) = Yes (Letter x)
isValidInput (x :: (y :: xs)) = No multipleLetters

isValidString : (s : String) -> Dec (ValidInput (unpack s))
isValidString s = isValidInput (unpack s)

readGuess : IO (x ** ValidInput x)
readGuess =
    do
        putStr "Guess: "
        x <- getLine
        case isValidString (toUpper x) of
            Yes prf => pure (_ ** prf)
            No contra =>
                do
                    putStrLn "Invalid guess"
                    readGuess

processGuess : (letter : Char) -> WordState (S guesses) (S letters) ->
    Either (WordState guesses (S letters)) (WordState (S guesses) letters)
processGuess letter (MkWordState word missing) =
    case isElem letter missing of
        Yes prf => Right (MkWordState word (removeElem letter missing))
        No contra => Left (MkWordState word missing)

game : WordState (S guesses) (S letters) -> IO Finished
game {guesses} {letters} st =
    do
        (_ ** Letter letter) <- readGuess
        case processGuess letter st of
            Left l =>
                do
                    putStrLn "Wrong!"
                    case guesses of
                        Z => pure (Lost l)
                        S k => game l

            Right r =>
                do
                    putStrLn "Right!"
                    case letters of
                        Z => pure (Won r)
                        S k => game r

main : IO ()
main =
    do
        result <- game {guesses = 2} (MkWordState "Test" ['T', 'E', 'S'])
        case result of
            Lost (MkWordState word missing) =>
                putStrLn ("You lose. The word was " ++ word)
            Won game =>
                putStrLn "You win!"