text:
%default total

data MyBit = A | B

fullCoverage : MyBit -> Int
fullCoverage A = 1
fullCoverage B = 2

extraDefault : MyBit -> Int
extraDefault A = 1
extraDefault B = 2
extraDefault _ = 3

usefulDefault : MyBit -> Int
usefulDefault A = 1
usefulDefault _ = 2

earlyDefault : MyBit -> Int
earlyDefault _ = 1
earlyDefault A = 2

onlyDefault : MyBit -> Int
onlyDefault _ = 1

nestedFullCoverage : MyBit -> MyBit -> Int
nestedFullCoverage A A = 1
nestedFullCoverage A B = 2
nestedFullCoverage B A = 3
nestedFullCoverage B B = 4

nestedExtraDefault : MyBit -> MyBit -> Int
nestedExtraDefault A A = 1
nestedExtraDefault A B = 2
nestedExtraDefault B A = 3
nestedExtraDefault B B = 4
nestedExtraDefault _ _ = 5

nestedUsefulDefault : MyBit -> MyBit -> Int
nestedUsefulDefault A A = 1
nestedUsefulDefault A B = 2
nestedUsefulDefault B A = 3
nestedUsefulDefault _ _ = 4

nestedEarlyDefault : MyBit -> MyBit -> Int
nestedEarlyDefault A A = 1
nestedEarlyDefault A B = 2
nestedEarlyDefault B A = 3
nestedEarlyDefault _ _ = 4
nestedEarlyDefault B B = 5


text:
module DepSec.Labeled

import public DepSec.DIO
import public DepSec.Poset

%access public export

||| Labeled value
||| @ label label
||| @ valueType type of labeled value
data Labeled : (label : labelType)
            -> (valueType : Type)
            -> Type where
  ||| TCB
  MkLabeled : valueType -> Labeled label valueType

||| Label a value
||| @ value value to label
label : Poset labelType
     => {l : labelType}
     -> (value : a)
     -> Labeled l a
label = MkLabeled

||| Upgrade the security level of a labeled value
||| @ flow evidence that l may flow to l'
||| @ labeled labeled value to relabel
relabel : Poset labelType
       => {l, l' : labelType}
       -> {auto flow : l `leq` l'}
       -> (labeled : Labeled l a)
       -> Labeled l' a
relabel (MkLabeled x) = MkLabeled x

||| Unlabel a labeled value
||| @ flow evidence that l may flow to l'
||| @ labeled labeled value to unlabel
unlabel : Poset labelType
       => {l,l' : labelType}
       -> {auto flow : l `leq` l'}
       -> (labeled : Labeled l a)
       -> DIO l' a
unlabel (MkLabeled val) = pure val

||| Unlabel a labeled value while retaining a proof of relationship
||| @ flow evidence that l may flow to l'
||| @ labeled labeled value to unlabel
unlabel' : Poset labelType
        => {l,l' : labelType}
        -> {auto flow : l `leq` l'}
        -> (labeled : Labeled l a)
        -> DIO l' (c : a ** label c = labeled)
unlabel' (MkLabeled x) = pure (x ** Refl)

||| Plug a secure computation into a less secure computation
||| @ flow evidence that l may flow to l'
||| @ dio secure computation to plug
plug : Poset labelType
    => {l,l' : labelType}
    -> (dio : DIO l' a)
    -> {auto flow : l `leq` l'}
    -> DIO l (Labeled l' a)
plug dio = lift . run $ dio >>= pure . MkLabeled

ext: idr

max_stars_repo_name: simongregersen/DepSec

max_issues_repo_name: simongregersen/DepSec

max_forks_repo_name: simongregersen/DepSec


text:
module Sub11Apply108x54

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(36x+18) --F[5,-2]->C[4,-4]--> 3(32x+15)
fc108x54To96x45 :
  (o:Nat) -> P (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                           (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                     (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                               (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))))) 2
    -> P (S (S (S (S (S (S (S (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)))))))))))))))))))) 2
fc108x54To96x45 o prf =
  let prf2 = lvDown (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                           (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                     (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                               (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))))) 2
                    prf in
    let prf3 = fc108x54To96x45' o prf2 in lvDown (S (S (S (S (S (S (S (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)))))))))))))))))))) 3 prf3

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

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

    rewrite (sym (plusSuccRightSucc (plus (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

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

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

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

    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                          o)))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                          o))))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                          o)))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                          o))))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                          o)))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                          o))))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                          o)))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                          o))))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                          o)))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                          o))))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o)
                                          o)))))))))) in
    rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                                (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                    (S (S (plus (plus (plus (plus o o) o)
                                                                                (S (plus (plus o o) o)))
                                                                                (S (plus (plus (plus o o) o)
                                                                                (S (plus (plus o 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 Rapid.Common

public export
data GCFlavour = Zero | BDW | Statepoint

export
Show GCFlavour where
  show Zero = "zero"
  show BDW = "bdw"
  show Statepoint = "statepoint"

export
Eq GCFlavour where
  (==) Zero Zero = True
  (==) BDW BDW = True
  (==) Statepoint Statepoint = True
  (==) _ _ = False

export
encodeGCFlavourAsInt : GCFlavour -> Int
encodeGCFlavourAsInt Zero = 1
encodeGCFlavourAsInt BDW = 2
encodeGCFlavourAsInt Statepoint = 3

public export
record CompileOpts where
  constructor MkCompileOpts
  debugEnabled : Bool
  traceEnabled : Bool
  gcFlavour : GCFlavour
  targetOS : String
  constNamespace : Int


text:
module Js.ASync

import Control.ST
import public Js.Utils

%include JavaScript "js/async.js"
%include Node "js/async.js"

public export
data ASync : Type -> Type where
  MkASync : ((a -> JS_IO()) -> JS_IO ()) -> ASync a

export
setASync : (a -> JS_IO ()) -> ASync a -> JS_IO ()
setASync onEvent (MkASync set) =
  do
    set onEvent
    pure ()

export
setASync_ : ASync a -> JS_IO ()
setASync_ x = setASync (\_=>pure ()) x

export
total
setTimeout : Int -> a -> ASync a
setTimeout millis x =
  MkASync $ \onevt => assert_total $
    jscall  "setTimeout(%0, %1)" ( JsFn (() -> JS_IO ()) -> Int -> JS_IO ()) (MkJsFn $ \() => onevt x) millis

export
never : ASync a
never = MkASync (\onevt => pure ())

export
debugError : String -> ASync a
debugError s = MkASync (\_ => jscall "throw2(%0)" (String -> JS_IO ()) s)

export
liftJS_IO : JS_IO a -> ASync a
liftJS_IO x = MkASync (\onevt => x >>= onevt)

export
Functor ASync where
  map f (MkASync oldset) = MkASync (\onevt => oldset (\x => onevt (f x)) )

export
Applicative ASync where
  pure x = setTimeout 0 x
  (MkASync stepf) <*> (MkASync stepx) =
    MkASync (\onevt => stepf (\f => stepx (\x => onevt (f x)) ))

export
Monad ASync where
  (>>=) (MkASync stepx) f =
    MkASync $ \onevt => stepx (\x => let MkASync stepf = f x in stepf onevt )

export
data JSIOFifoQueue : (b : Type) -> Type where
  MkJSIOFifoQueue : Ptr -> JSIOFifoQueue a

export
newJSIOFifoQueue : (x : Type) -> JS_IO (JSIOFifoQueue x)
newJSIOFifoQueue _ =
  MkJSIOFifoQueue <$> jscall "{queue: [], callback: undefined}" (JS_IO Ptr)

export
putInQueue : a -> JSIOFifoQueue a -> JS_IO ()
putInQueue x (MkJSIOFifoQueue q) =
  jscall
    "$JSLIB$async.putInQueue(%0,%1)"
    (Ptr -> Ptr -> JS_IO ())
    (believe_me x)
    q

export
getQueuePtr : JSIOFifoQueue a -> Ptr
getQueuePtr (MkJSIOFifoQueue q) = q

export
getFromQueue : JSIOFifoQueue a -> ASync a
getFromQueue (MkJSIOFifoQueue q) =
  MkASync $ \proc =>
    believe_me <$>
      jscall
        "$JSLIB$async.getFromQueue(%0, %1)"
        (Ptr -> JsFn (Ptr -> JS_IO ()) -> JS_IO Ptr)
        q
        (MkJsFn (\x => proc $ believe_me x) )

export
implementation Console ASync where
  consoleLog s = lift $ liftJS_IO $ jscall "console.log(%0)" (String -> JS_IO ()) s

public export
interface Wait (m:Type -> Type) where
    wait : Int -> STrans m () xs (const xs)

export
implementation Wait ASync where
  wait millis = lift $ setTimeout millis ()

export
implementation JSRandom ASync where
  randInt i = lift $ liftJS_IO $ randomInt i

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module TestClock

import System.Clock

clockSmall : Clock type -> Bool
clockSmall (MkClock {type} s n) = MkClock {type} s n < MkClock 1 0

clockBig : Clock type -> Bool
clockBig (MkClock {type} s n) = MkClock {type} s n > MkClock 1600000000 0

main : IO ()
main = do
    utc <- clockTime UTC
    monotonicStart <- clockTime Monotonic
    process <- clockTime Process
    thread <- clockTime Thread

    monotonicEnd <- clockTime Monotonic

    putStrLn $ show $ [
        clockBig utc,
        monotonicStart < monotonicEnd,
        clockSmall process,
        clockSmall thread
    ]


text:
module Main

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]

println : Show a => a -> IO ()
println a = do
  print a
  putStrLn ""

main : IO ()
main = print (pythag 50)

max_stars_repo_name: steshaw/idris-elisp

max_issues_repo_name: steshaw/idris-elisp

max_forks_repo_name: steshaw/idris-elisp


text:
-- Vect.idr
--
-- Vector type to demonstrate dependent types

||| Vect data type: A List with defined length
data Vect : Nat -> Type -> Type where
  ||| Empty vector
  Nil : Vect Z a
  ||| Prepend a new element to vector
  (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a

%name Vect xs, ys, zs

||| appends two vectors
append : Vect n elem -> Vect m elem -> Vect (n + m) elem
append [] ys = ys
append (x :: xs) ys = x :: append xs ys

||| Combine two vectors to a vector of pairs
zip : Vect n a -> Vect n b -> Vect n (a, b)
zip [] ys = []
zip (x :: xs) (y :: ys) = (x, y) :: zip xs ys

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
import Data.List
import Data.List1
import Data.String.Parser

import System.File

Coord : Type
Coord = (Nat, Nat)

Dots : Type
Dots = List Coord

data Fold = Up Nat | Left Nat

Show Fold where
  show (Up n) = "fold up " ++ show n
  show (Left n) = "fold left " ++ show n

Input : Type
Input = (Dots, List Fold)

pairParser : Parser Coord
pairParser = do x <- natural
                token ","
                y <- natural
                pure (x, y)

foldParser : Parser Fold
foldParser = do token "fold along"
                (token "y=" *> Up <$> natural) <|>
                (token "x=" *> Left <$> natural)

parser : Parser Input
parser = do coords <- some (pairParser <* spaces)
            spaces
            folds <- some (foldParser <* spaces)
            pure (coords, folds)

fold1 : Fold -> Coord -> Coord
fold1 (Up f)   (x, y) = if y > f
                           then (x, minus f (minus y f))
                           else (x, y)
fold1 (Left f) (x, y) = if x > f
                           then (minus f (minus x f), y)
                           else (x, y)

fold : Fold -> Dots -> Dots
fold f dots = .head <$> (group $ sort $ fold1 f <$> dots)

part1 : Input -> IO String
part1 (dots, []) = pure "No folds"
part1 (dots, (f :: _)) = pure $ show $ length $ fold f dots

printDots : Coord -> Dots -> IO ()
printDots (_, _) [] = pure ()
printDots (lx, ly) ((y, x) :: cs) =
  do if y > ly
        then putStr $ pack $ replicate (minus y ly) '\n'
        else putStr $ pack $ replicate (minus x (lx + 1)) ' '
     putChar '#'
     printDots (x, y) cs

part2 : Input -> IO String
part2 (dots, fs) = do let r = sort $ (\(x, y) => (y, x)) <$> foldl (flip fold) dots fs
                      printDots (0, 0) r
                      pure ""

main : IO ()
main = do Right input <- readFile "input.txt"
            | Left err => printLn err
          Right (a, _) <- pure $ parse parser input
            | Left err => printLn err
          part1 a >>= putStrLn
          part2 a >>= putStrLn


text:
module Text.Markup.Edda.Process.Shunt

import Data.AVL.Dict
import Data.Stack
import Data.List.Views

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

%access private
%default total

-- @ TODO make more precise.

data SecInfo : Type where
  MkSInfo : (depth : Nat)
         -> (label : Maybe String)
         -> (title : List (Edda INLINE))
         -> (attrs : Dict String String)
         -> (body  : List (Edda BLOCK))
         -> SecInfo
  NoInfo : SecInfo

popThings : Nat -> List (Edda BLOCK)
                -> List (Edda BLOCK)
                -> (List (Edda BLOCK), List (Edda BLOCK))
popThings k xs Nil = (xs, Nil)
popThings k xs ((Section d l t as b)::ys) with (compare d k)
  popThings k xs ((Section d l t as b)::ys) | LT = (xs, Section d l t as b :: ys)
  popThings k xs ((Section d l t as b)::ys) | _ = popThings k (xs ++ [Section d l t as b]) ys

popThings k xs (block::ys) = popThings k (xs ++ [block]) ys

performShunt : (stack  : Stack (Edda BLOCK))
            -> (output : List (Edda BLOCK))
            -> (input : List (Edda BLOCK))
            -> List (Edda BLOCK)
performShunt stack output input with (snocList input)
  performShunt stack output [] | Empty = stack ++ output
  performShunt stack output (xs ++ [x]) | (Snoc rec) with (x)
    performShunt stack output (xs ++ [x]) | (Snoc rec) | (Section depth label title attrs body) with (output)
      performShunt stack output (xs ++ [x]) | (Snoc rec) | (Section depth label title attrs body) | [] =
        performShunt mkStack [Section depth label title attrs (body ++ stack)] xs | rec
      performShunt stack output (xs ++ [x]) | (Snoc rec) | (Section depth label title attrs body) | (y :: ys) with (y)

        performShunt stack output (xs ++ [x]) | (Snoc rec) | (Section depth label title attrs body) | (y :: ys) | (Section k z zs w ws) with (compare depth k)
          performShunt stack output (xs ++ [x]) | (Snoc rec) | (Section depth label title attrs body) | (y :: ys) | (Section k z zs w ws) | LT =
              let (ls,rs) = popThings k Nil (output) in
               performShunt mkStack ([Section depth label title attrs (body ++ stack ++ ls)] ++ rs) xs | rec
          performShunt stack output (xs ++ [x]) | (Snoc rec) | (Section depth label title attrs body) | (y :: ys) | (Section k z zs w ws) | GT =

              performShunt mkStack ([Section depth label title attrs (body ++ stack)] ++ output) xs | rec
          performShunt stack output (xs ++ [x]) | (Snoc rec) | (Section depth label title attrs body) | (y :: ys) | (Section k z zs w ws) | EQ =
              performShunt mkStack ([Section depth label title attrs (body ++ stack)] ++ output) xs | rec

        performShunt stack output (xs ++ [x]) | (Snoc rec) | (Section depth label title attrs body) | (y :: ys) | block =
          performShunt mkStack ([Section depth label title attrs (body ++ stack)] ++ output) xs | rec

    performShunt stack output (xs ++ [x]) | (Snoc rec) | block = performShunt (pushS block stack) output xs | rec

export
shunt : List (Edda BLOCK) -> List (Edda BLOCK)
shunt = performShunt Nil Nil

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module IdrisWeb.Session.SessionUtils
import IdrisWeb.CGI.CgiTypes
import IdrisWeb.CGI.Cgi
import IdrisWeb.Session.Session
import IdrisWeb.DB.SQLite.SQLiteNew
import Effects
%access public

-- Key for the session id in the cookie
public
SESSION_VAR : String
SESSION_VAR = "session_id"

getOrCreateSession : EffM IO [CGI (InitialisedCGI TaskRunning), SESSION (SessionRes SessionUninitialised)]
                                [CGI (InitialisedCGI TaskRunning), SESSION (SessionRes SessionInitialised)]
                                (Maybe (SessionID, SessionData))
getOrCreateSession = do
  -- Firstly grab the session ID from the cookies, if it exists
  s_var <- lift' (queryCookieVar SESSION_VAR)
  case s_var of
       -- If it does exist, then attempt to load the session
       Just s_id => do res <- lift' (loadSession s_id)
                       case res of
                         Just res' => Effects.pure $ Just (s_id, res') -- (s_id, res')
                        -- TODO: This should create a new session
                         Nothing => Effects.pure $ Nothing
       -- If it doesn't, create a new, empty session
       Nothing => do res <- lift (Drop (Keep (SubNil))) (createSession [])
                     case res of
                          Just s_id' => Effects.pure $ Just (s_id', [])
                          Nothing => Effects.pure $ Nothing

setSessionCookie : Eff IO [CGI (InitialisedCGI TaskRunning), SESSION (SessionRes SessionInitialised)] Bool
setSessionCookie = do s_id <- lift (Drop (Keep (SubNil))) getSessionID
                      case s_id of
                           Just s_id => do lift (Keep (Drop (SubNil))) (setCookie SESSION_VAR s_id)
                                           pure True
                           Nothing => pure False

total
updateVar : String -> SessionDataType -> SessionData -> SessionData
updateVar new_key new_val [] = [(new_key, new_val)]
updateVar new_key new_val ((key, val)::xs) = if (key == new_key) then ((key, new_val):: xs)
                                                                 else ((key, val) :: (updateVar new_key new_val xs))

-- Takes in two functions: one to execute if there is a valid, authenticated
-- session cookie, and one to execute if there isn't.
withSession : (SessionData ->
               EffM IO [CGI (InitialisedCGI TaskRunning),
                        SESSION (SessionRes SessionInitialised),
                        SQLITE ()]
                       [CGI (InitialisedCGI TaskRunning),
                        SESSION (SessionRes SessionUninitialised),
                        SQLITE ()] ()) ->
               EffM IO [CGI (InitialisedCGI TaskRunning),
                        SESSION (SessionRes SessionInitialised),
                        SQLITE ()]
                       [CGI (InitialisedCGI TaskRunning),
                        SESSION (SessionRes SessionUninitialised),
                        SQLITE ()] () ->
               Eff IO [CGI (InitialisedCGI TaskRunning),
                       SESSION (SessionRes SessionUninitialised),
                       SQLITE ()] ()
withSession is_auth_fn not_auth_fn = do
  s_var <- queryCookieVar SESSION_VAR
  case s_var of
       -- If it does exist, then attempt to load the session
       Just s_id => do res <- loadSession s_id--(lift (Drop (Keep (SubNil))) (loadSession s_id))
                       case res of
                           -- If we've got a valid session, execute the user-specified
                           -- function with the gathered session data
                           Just res' => do is_auth_fn res'
                                           pure ()
                           -- If not, execute the specified failure function
                           Nothing => do not_auth_fn
                                         pure ()
      -- If there's no session variable, execute the failure function (somehow)
      -- HACK: this loadSession won't succeed, yet will transfer into the other state so
      -- that the not_auth_fn can be run. Probably better ways of doing it
       Nothing => do loadSession ""
                     not_auth_fn
                     pure ()

max_stars_repo_name: idris-hackers/IdrisWeb

max_issues_repo_name: idris-hackers/IdrisWeb

max_forks_repo_name: idris-hackers/IdrisWeb


text:
module Props.Char

import Data.List
import public Props.Util

%access public export

digits : List Char
digits = ['0'..'9']

lowerCase : List Char
lowerCase = ['a'..'z']

upperCase : List Char
upperCase = ['A'..'Z']

letters : List Char
letters = lowerCase ++ upperCase

whiteSpace : List Char
whiteSpace = ['\n','\t',' ']

Digit : Char -> Type
Digit c = Elem c digits

LowerCase : Char -> Type
LowerCase c = Elem c lowerCase

UpperCase : Char -> Type
UpperCase c = Elem c upperCase

Whitespace : Char -> Type
Whitespace c = Elem c whiteSpace

Letter : (c:Char) -> Type
Letter = EitherK LowerCase UpperCase

AlphaNumeric : Char -> Type
AlphaNumeric = EitherK Letter Digit

max_stars_repo_name: janschultecom/idris-refined

max_issues_repo_name: janschultecom/idris-refined

max_forks_repo_name: janschultecom/idris-refined


text:
module ConsoleIO

%default total

public export
data ConsoleCmnd : Type -> Type where
  PutStr : String -> ConsoleCmnd ()
  GetLine : ConsoleCmnd String

  Pure : a -> ConsoleCmnd a
  Bind : ConsoleCmnd a -> (a -> ConsoleCmnd b) -> ConsoleCmnd b

export
Functor ConsoleCmnd where
  map f c = Bind c (Pure . f)

export
Applicative ConsoleCmnd where
  pure = Pure
  mf <*> ma = Bind mf (\f => map f ma)

public export
data ConsoleIO : Type -> Type where
  Quit : a -> ConsoleIO a
  Do : ConsoleCmnd a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b

namespace ConsoleDo
  export
  (>>=) : ConsoleCmnd a -> (a -> Inf (ConsoleIO b)) -> ConsoleIO b
  (>>=) = Do

namespace CommandDo
  export
  (>>=) : ConsoleCmnd a -> (a -> ConsoleCmnd b) -> ConsoleCmnd b
  (>>=) = Bind

export
runConsoleCmnd : ConsoleCmnd a -> IO a
runConsoleCmnd (PutStr s) = putStr s
runConsoleCmnd GetLine    = getLine
runConsoleCmnd (Pure a)   = pure a
runConsoleCmnd (Bind c f) =
  do res <- runConsoleCmnd c
     runConsoleCmnd (f res)

  -- We need some fuel, for totality
  --
export
data Fuel = Dry | More (Lazy Fuel)

export
tank : Nat -> Fuel
tank    Z  = Dry
tank (S n) = More (tank n)

-- Bringing back infinity...
--

export partial
forever : Fuel
forever = More forever

-- forever
-- data Fuel = Dry | More (Lazy Fuel)

export
runConsoleIO : Fuel -> ConsoleIO a -> IO (Maybe a)
runConsoleIO _ (Quit a) = pure (Just a)
runConsoleIO Dry _      =
  do putStrLn "Out of fuel"
     pure Nothing
runConsoleIO (More f) (Do cmnd cont) =
  do res <- runConsoleCmnd cmnd
     runConsoleIO f (cont res)

-- Working with the console, badly
--
namespace InfIO

  data InfIO : Type where
    Do : IO a -> (a -> Inf InfIO) -> InfIO

  partial
  run : InfIO -> IO ()
  run (Do action cont) =
      do res <- action
         run (cont res)

  runWithFuel : Fuel -> InfIO -> IO ()
  runWithFuel Dry _ = putStrLn "Out of fuel"
  runWithFuel (More f) (Do act cont)
    = do res <- act
         runWithFuel f (cont res)

max_stars_repo_name: braje/totality-talk

max_issues_repo_name: braje/totality-talk

max_forks_repo_name: braje/totality-talk


text:
module CIL.FFI

%default total

%access public export

||| The universe of foreign CIL types.
data CILTy =
  ||| a foreign reference type
  CILTyRef String String |
  ||| a foreign value type
  CILTyVal String String |
  ||| a foreign array type
  CILTyArr CILTy |
  ||| a foreign generic type
  CILTyGen CILTy (List CILTy) |
  ||| a foreign generic parameter of a generic type
  CILTyGenParam String |
  ||| a foreign generic parameter of a generic method
  CILTyGenMethodParam String

Eq CILTy where
  (CILTyRef as tn)    == (CILTyRef as' tn')    = as   == as'  && tn == tn'
  (CILTyVal as tn)    == (CILTyVal as' tn')    = as   == as'  && tn == tn'
  (CILTyArr elTy)     == (CILTyArr elTy')      = elTy == elTy'
  (CILTyGen def args) == (CILTyGen def' args') = def  == def' && assert_total (args == args')
  _                   == _                     = False

%inline
CILTyObj : CILTy
CILTyObj = CILTyRef "" "object"

%inline
CILTyStr : CILTy
CILTyStr = CILTyRef "" "string"

%inline
CILTyBool : CILTy
CILTyBool = CILTyVal "" "bool"

%inline
CILTyInt32 : CILTy
CILTyInt32 = CILTyVal "" "int"

%inline
CILTyChar : CILTy
CILTyChar = CILTyVal "" "char"

%inline
CILTyVoid : CILTy
CILTyVoid = CILTyRef "" "void"

||| A foreign CIL type.
data CIL   : CILTy -> Type where
     MkCIL : (ty : CILTy) -> CIL ty

||| A foreign CIL array type.
data TypedArray   : CILTy -> Type -> Type where
     MkTypedArray : (ty : CILTy) -> (elemTy : Type) -> TypedArray ty elemTy

||| A foreign method calling convention.
data CILCallConv =
  ||| Static calling convention.
  CCCStatic |
  ||| Instance calling convention.
  CCCInstance

||| A foreign method descriptor.
data CILMethod =
  ||| A generic method given its calling convention, declaring type, name, type arguments, parameter types and return type.
  CILGenMethod CILCallConv CILTy String (List CILTy) (List CILTy) CILTy

||| A foreign descriptor.
data CILForeign =
  ||| Call the given foreign method.
  CILCall CILMethod | -- TODO: replace all other method forms by this one and introduce helper functions instead
  ||| Call the named instance method.
  CILInstance String |
  ||| Call the named instance method with the given signature.
  CILInstanceCustom String (List CILTy) CILTy |
  ||| Read the value of the named instance field.
  CILInstanceField String |
  ||| Call the named static method of the given foreign type.
  CILStatic CILTy String |
  ||| Read the value of the named static field of the given foreign type.
  CILStaticField CILTy String |
  ||| Call a constructor to instantiate an object.
  CILConstructor |
  ||| Load the given runtime type.
  CILTypeOf CILTy |
  ||| Convert a function to a delegate of the given type.
  CILDelegate CILTy |
  ||| Export a function under the given name.
  CILExport String |
  ||| Export a function under its original name.
  CILDefault

||| A CIL enum type.
|||
||| @cilTy the external CIL type
||| @reprTy the native representation type (must be either Bits16 or Bits32)
data CILEnum : (cilTy : CILTy) -> (reprTy : Type) -> Type

data CILRef  : CILTy -> Type -> Type

mutual
  data CIL_IntTypes  : Type -> Type where
       CIL_IntChar   : CIL_IntTypes Char
       CIL_IntNative : CIL_IntTypes Int

  data CIL_Types : Type -> Type where
       CIL_Ref   : CIL_Types (CILRef refTy refT)
       CIL_Array : CIL_Types (TypedArray cilTy elTy)
       CIL_Str   : CIL_Types String
       CIL_Float : CIL_Types Double
       CIL_Ptr   : CIL_Types Ptr
       CIL_Bool  : CIL_Types Bool
       CIL_Unit  : CIL_Types ()
       CIL_IntT  : CIL_IntTypes i -> CIL_Types i
       CIL_CILT  : CIL_Types (CIL ty)
       CIL_FnT   : CIL_FnTypes fnT -> CIL_Types (CilFn delegateTy fnT)
       CIL_EnumT : CIL_Types (CILEnum cilTy reprTy)
       CIL_MaybeT : CIL_Types ty -> CIL_Types (Maybe ty)

  data CilFn   : CILTy -> Type -> Type where
       MkCilFn : (delegateTy : CILTy) -> (fn : fnT) -> CilFn delegateTy fnT

  data CIL_FnTypes : Type -> Type where
       CIL_Fn      : CIL_Types s -> CIL_FnTypes t -> CIL_FnTypes (s -> t)
       CIL_FnIO    : CIL_Types t -> CIL_FnTypes (IO' l t)
       CIL_FnBase  : CIL_Types t -> CIL_FnTypes t

%used MkCilFn fn

FFI_CIL : FFI
FFI_CIL = MkFFI CIL_Types CILForeign String

CIL_IO : Type -> Type
CIL_IO = IO' FFI_CIL

||| CIL FFI.
%inline
invoke : CILForeign -> (ty : Type) -> {auto fty : FTy FFI_CIL [] ty} -> ty
invoke ffi ty = foreign FFI_CIL ffi ty

%inline
new : (ty : Type) -> {auto fty : FTy FFI_CIL [] ty} -> ty
new ty = invoke CILConstructor ty

%inline
invokeInstance : String -> (ty : Type) -> {auto fty : FTy FFI_CIL [] ty} -> ty
invokeInstance memberName = invoke (CILInstance memberName)

%inline
invokeStatic : CILTy -> String -> (ty : Type) -> {auto fty : FTy FFI_CIL [] ty} -> ty
invokeStatic declTy memberName = invoke (CILStatic declTy memberName)

%inline
delegate : (ty : CILTy) -> (fnT : Type) -> fnT ->
           {auto fty : FTy FFI_CIL [] (CilFn ty fnT -> CIL_IO (CilFn ty fnT))} ->
           CIL_IO (CilFn ty fnT)
delegate ty fnT fn = invoke (CILDelegate ty)
                            (CilFn ty fnT -> CIL_IO (CilFn ty fnT))
                            (MkCilFn ty fn)

%inline
corlibTy : String -> CILTy
corlibTy = CILTyRef "mscorlib"

%inline
corlibTyVal : String -> CILTy
corlibTyVal = CILTyVal "mscorlib"

%inline
corlib : String -> Type
corlib = CIL . corlibTy

namespace System

  Object : Type
  Object = CIL CILTyObj

  %inline
  RuntimeTypeTy : CILTy
  RuntimeTypeTy = corlibTy "System.Type"

  %inline
  RuntimeType : Type
  RuntimeType = CIL RuntimeTypeTy

%inline
typeOf : CILTy -> CIL_IO RuntimeType
typeOf t = invoke (CILTypeOf t) (CIL_IO RuntimeType)

||| `IsA a b` means `b` is a subtype of `a` in the CIL type system.
interface IsA a b where {}

%inline
upcast : IsA a b => b -> a
upcast b = believe_me b

||| Subtyping is reflexive.
IsA a a where {}
IsA Object String where {}
IsA Object Int where {}
IsA Object Integer where {}
IsA Object Bool where {}
IsA Object Double where {}
IsA Object RuntimeType where {}

namespace System.Object

  %inline
  ToString : IsA Object o => o -> CIL_IO String
  ToString obj =
    invokeInstance
      "ToString"
      (Object -> CIL_IO String)
      (upcast obj)

  %inline
  Equals : IsA Object a => a -> a -> CIL_IO Bool
  Equals x y =
    invokeInstance
      "Equals"
      (Object -> Object -> CIL_IO Bool)
      (upcast x) (upcast y)

namespace System.Array

  ArrayTy : CILTy
  ArrayTy = corlibTy "System.Array"

  Array : Type
  Array = CIL ArrayTy

  CreateInstance : RuntimeType -> Int -> CIL_IO Array
  CreateInstance =
    invokeStatic ArrayTy "CreateInstance" (RuntimeType -> Int -> CIL_IO Array)

  SetValue : Array -> Object -> Int -> CIL_IO ()
  SetValue =
    invokeInstance "SetValue" (Array -> Object -> Int -> CIL_IO ())

namespace System.Console

  ConsoleTy : CILTy
  ConsoleTy = corlibTy "System.Console"

  invokeConsole : String -> (ty: Type) -> {auto fty : FTy FFI_CIL [] ty} -> ty
  invokeConsole = invokeStatic ConsoleTy

  namespace Char

    Read : CIL_IO Int
    Read = invokeConsole "Read" (CIL_IO Int)

    Write : Char -> CIL_IO ()
    Write = invokeConsole "Write" (Char -> CIL_IO ())

  namespace String

    Write : String -> CIL_IO ()
    Write = invokeConsole "Write" (String -> CIL_IO ())

namespace System.Convert

  ToInt32 : IsA Object a => a -> CIL_IO Int
  ToInt32 o =
    invokeStatic (corlibTy "System.Convert") "ToInt32" (Object -> CIL_IO Int) (upcast o)

namespace System.Math

  %inline
  SystemMathMax : CILForeign
  SystemMathMax = CILStatic (CILTyRef "mscorlib" "System.Math") "Max"

  namespace Int32

    Max : Int -> Int -> CIL_IO Int
    Max = invoke SystemMathMax (Int -> Int -> CIL_IO Int)

  namespace Double

    Max : Double -> Double -> CIL_IO Double
    Max = invoke SystemMathMax (Double -> Double -> CIL_IO Double)

namespace System.Text

  StringBuilder : Type
  StringBuilder = corlib "System.Text.StringBuilder"

  IsA Object StringBuilder where {}

  %inline
  invokeStringBuilder : String -> StringBuilder -> String -> CIL_IO StringBuilder
  invokeStringBuilder fn = invokeInstance fn (StringBuilder -> String -> CIL_IO StringBuilder)

  Append : StringBuilder -> String -> CIL_IO StringBuilder
  Append = invokeStringBuilder "Append"

  AppendLine : StringBuilder -> String -> CIL_IO StringBuilder
  AppendLine = invokeStringBuilder "AppendLine"

namespace System

  GuidTy : CILTy
  GuidTy = corlibTyVal "System.Guid"

  Guid : Type
  Guid = CIL $ GuidTy

  IsA Object Guid where {}

  namespace Guid

    NewGuid : CIL_IO Guid
    NewGuid = invokeStatic GuidTy "NewGuid" (CIL_IO Guid)

    Parse : String -> CIL_IO Guid
    Parse = invokeStatic GuidTy "Parse" (String -> CIL_IO Guid)

    Empty : CIL_IO Guid
    Empty = invoke (CILStaticField GuidTy "Empty") (CIL_IO Guid)

namespace Enums

  export
  theEnum : reprTy -> CILEnum cilTy reprTy
  theEnum e = believe_me e

  export
  fromEnum : CILEnum cilTy reprTy -> reprTy
  fromEnum e = believe_me e

  export
  (+) : (Num reprTy) => CILEnum cilTy reprTy -> CILEnum cilTy reprTy -> CILEnum cilTy reprTy
  (+) lhs rhs = theEnum (fromEnum lhs + fromEnum rhs)

(Num reprTy) => Semigroup (CILEnum cilTy reprTy) where
  (<+>) = (+)

(Num reprTy) => Monoid (CILEnum cilTy reprTy) where
  neutral = theEnum 0

putStr : String -> CIL_IO ()
putStr = putStr'

putStrLn : String -> CIL_IO ()
putStrLn = putStrLn'

print : Show a => a -> CIL_IO ()
print = print'

printLn : Show a => a -> CIL_IO ()
printLn = printLn'

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
-- SPDX-FileCopyrightText: 2021 The toml-idr developers
--
-- SPDX-License-Identifier: CC0-1.0

module Lexer

import Text.Lexer

import Tester

import Language.TOML.Lexer
import Language.TOML.Tokens

tokenize : Test
tokenize = test "tokenize" $ do
    let Just res = lexTOML "hello world\n"
        | Nothing => throwE "lexer error"
    assertEq (length res) 4

integerLiteral : Test
integerLiteral = test "lex integer literals" $ do
    let Just res = lexTOML "12345 12_345 0x12345 0x12_345"
        | Nothing => throwE "lexer error"
    assertEq (length res) 7

floatLiteral : Test
floatLiteral = test "lex float literals" $ do
    let Just res = lexTOML "5.0 0.55 0.0 -7.8e7 nan +nan -inf +inf"
        | Nothing => throwE "lexer error"
    assertEq (length res) 15

stringLiteral : Test
stringLiteral = test "lex string literals" $ do
    let Just res = lexTOML #""hello world""#
        | Nothing => throwE "lexer error"
    assertEq (length res) 1

export
tests : List Test
tests = [tokenize, integerLiteral, floatLiteral, stringLiteral]

max_stars_repo_name: sepiina/toml-idr

max_issues_repo_name: sepiina/toml-idr

max_forks_repo_name: sepiina/toml-idr


text:
module Index

-- Definitions and encodings of some linear type formers
import Linear.Types

-- Some equality combinators and lemmas for linear types
import Linear.Equality

-- Quantitative containers
import QCont

-- Quantitative polynomial functors
import QPF

-- Examples of using both QCont and QPF
import Examples

max_stars_repo_name: g-nakov/quantitative-poly

max_issues_repo_name: g-nakov/quantitative-poly

max_forks_repo_name: g-nakov/quantitative-poly


text:
module Web.Internal.ClipboardTypes

import JS

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace PresentationStyle

  public export
  data PresentationStyle = Unspecified | Inline | Attachment

  public export
  Show PresentationStyle where
    show Unspecified = "unspecified"
    show Inline = "inline"
    show Attachment = "attachment"

  public export
  Eq PresentationStyle where
    (==) = (==) `on` show

  public export
  Ord PresentationStyle where
    compare = compare `on` show

  public export
  read : String -> Maybe PresentationStyle
  read "unspecified" = Just Unspecified
  read "inline" = Just Inline
  read "attachment" = Just Attachment
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (PresentationStyle.read s)}
             -> PresentationStyle
  fromString s = fromJust $ read s

  export
  ToFFI PresentationStyle String where
    toFFI = show

  export
  FromFFI PresentationStyle String where
    fromFFI = read

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

export data Clipboard : Type where [external]

export
ToFFI Clipboard Clipboard where toFFI = id

export
FromFFI Clipboard Clipboard where fromFFI = Just

export
SafeCast Clipboard where
  safeCast = unsafeCastOnPrototypeName "Clipboard"

export data ClipboardEvent : Type where [external]

export
ToFFI ClipboardEvent ClipboardEvent where toFFI = id

export
FromFFI ClipboardEvent ClipboardEvent where fromFFI = Just

export
SafeCast ClipboardEvent where
  safeCast = unsafeCastOnPrototypeName "ClipboardEvent"

export data ClipboardItem : Type where [external]

export
ToFFI ClipboardItem ClipboardItem where toFFI = id

export
FromFFI ClipboardItem ClipboardItem where fromFFI = Just

export
SafeCast ClipboardItem where
  safeCast = unsafeCastOnPrototypeName "ClipboardItem"

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

export data ClipboardEventInit : Type where [external]

export
ToFFI ClipboardEventInit ClipboardEventInit where toFFI = id

export
FromFFI ClipboardEventInit ClipboardEventInit where fromFFI = Just

export data ClipboardItemOptions : Type where [external]

export
ToFFI ClipboardItemOptions ClipboardItemOptions where toFFI = id

export
FromFFI ClipboardItemOptions ClipboardItemOptions where fromFFI = Just

export data ClipboardPermissionDescriptor : Type where [external]

export
ToFFI ClipboardPermissionDescriptor ClipboardPermissionDescriptor where toFFI = id

export
FromFFI ClipboardPermissionDescriptor ClipboardPermissionDescriptor where fromFFI = Just

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

export data ClipboardItemDelayedCallback : Type where [external]

export
ToFFI ClipboardItemDelayedCallback ClipboardItemDelayedCallback where toFFI = id

export
FromFFI ClipboardItemDelayedCallback ClipboardItemDelayedCallback where fromFFI = Just


text:
module lib.Library3

import lib.Library4

export
salute3 : String
salute3 = "Hello, this is Library3, friend of: " ++ salute4


text:
module Decidable.Decidable

import Data.Rel
import Data.Fun

%default total

public export
isNo : Dec a -> Bool
isNo (Yes _) = False
isNo (No _) = True

public export
isYes : Dec a -> Bool
isYes (Yes _) = True
isYes (No _) = False

||| Proof that some `Dec` is actually `Yes`
public export
data IsYes : Dec a -> Type where
  ItIsYes : IsYes (Yes prf)

public export
Uninhabited (IsYes (No contra)) where
  uninhabited ItIsYes impossible

||| Decide whether a 'Dec' is 'Yes'
public export
isItYes : (v : Dec a) -> Dec (IsYes v)
isItYes (Yes _) = Yes ItIsYes
isItYes (No _) = No absurd

||| An n-ary relation is decidable if we can make a `Dec`
||| of its result type for each combination of inputs
public export
IsDecidable : (k : Nat) -> (ts : Vect k Type) -> Rel ts -> Type
IsDecidable k ts p = liftRel ts p Dec

||| Interface for decidable n-ary Relations
public export
interface Decidable k ts p where
  total decide : IsDecidable k ts p

||| Given a `Decidable` n-ary relation, provides a decision procedure for
||| this relation.
decision : (ts : Vect k Type) -> (p : Rel ts) -> (Decidable k ts p) => liftRel ts p Dec
decision ts p = decide {ts} {p}

using (a : Type, x : a)
  public export
  data Given : Dec a -> Type where
    Always : Given (Yes x)


text:
import Data.Vect

||| A type synonym for describing positions as (x,y) coordinates.
Position : Type
Position = (Double, Double)

||| A type synonym for describing polygons with n corners.
Polygon : Nat -> Type
Polygon n = Vect n Position

tri : Polygon 3
tri = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]