text:
module ProofColDivSeqPostuProof

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection
%access export

%hide Language.Reflection.P

--            from ProofColDivSeqBase
-- ########################################
base0 : P Z
base0 = rewrite definiP Z in
        rewrite definiDivSeq0 in IsLimited00 (Z ** definiLimited0)
-- ########################################

--            from ProofColDivSeqMain
-- ########################################
-- ########################################

--            from sub0xxxxx
-- ########################################
-- 01 3(6x+1) --B[1,-2]--> 3x
b18x3To3x : (k : Nat)
  -> (Not . P) (S (plus (plus (plus k k) (plus k k)) (plus k k))) -> (Not . P) k
b18x3To3x k = rewrite definiP (S (plus (plus (plus k k) (plus k k)) (plus k k))) in
              rewrite definiP k in \prfF, prf => (prfF . IsLimited01 k) prf

-- 02 3(18x+4) --A[6,-4]--> 3(24x+3) -->E[2,-4]--> 3(2x)
ae54x12To6x : (l : Nat)
  -> (Not . P) (S (S (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                 (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                           (S (plus (plus (plus l l) l) (plus (plus l l) l))))))
    -> (Not . P) (plus l l)
ae54x12To6x l = rewrite definiP (S (S (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                                  (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                            (S (plus (plus (plus l l) l) (plus (plus l l) l)))))) in
                rewrite definiP (plus l l) in \prfF, prf => (prfF . IsLimited02 l) prf

-- 03 3(18x+10) --A[6,-4]->C[4,-4]--> 3(8x+3)
ac54x30To24x9 : (l : Nat)
  -> (Not . P) (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l)))
                                    (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                              (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l)))))))))
    -> (Not . P) (S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))))))
ac54x30To24x9 l = rewrite definiP (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l)))
                                                       (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                                                 (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))) in
                  rewrite definiP (S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))) in \prfF, prf => (prfF . IsLimited03 l) prf

-- 04 3(18x+16) --A[6,-4]->B[1,-2]--> 3(4x+3)
ab54x30To12x9 : (l : Nat)
  -> (Not . P) (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                       (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                 (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))))))
    -> (Not . P) (S (S (S (plus (plus l l) (plus l l)))))
ab54x30To12x9 l = rewrite definiP (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                                          (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                                    (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))))) in
                  rewrite definiP (S (S (S (plus (plus l l) (plus l l))))) in \prfF, prf => (prfF . IsLimited04 l) prf

-- 05 3(3x+2) --C[4,-4]--> 3x
c9x6To3x : (j : Nat)
  -> (Not . P) (S (S (plus (plus j j) j))) -> (Not . P) j
c9x6To3x j = rewrite definiP (S (S (plus (plus j j) j))) in
             rewrite definiP j in \prfF, prf => (prfF . IsLimited05 j) prf

-- 06 3(12x+3) --E[2,-4]--> 3x
e36x9To3x : (l : Nat)
  -> (Not . P) (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l))))))
    -> (Not . P) l
e36x9To3x l = rewrite definiP (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l)))))) in
              rewrite definiP l in \prfF, prf => (prfF . IsLimited06 l) prf

-- 07 3(36x+9) --F[5,-2]->C[4,-4]--> 3(32x+7)
fc108x27To96x21 :
  (o:Nat) -> (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))))))))))
    -> (Not . P) (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))))))))))))
fc108x27To96x21 o =
  rewrite definiP (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)))))))))) in
  rewrite definiP (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))))))))))))
  in \prfF, prf => (prfF . IsLimited07 o) prf

-- 08 3(36x+21) --F[5,-2]->B[1,-2]--> 3(16x+9)
fb108x63To48x27 :
  (o:Nat) -> (Not . P) (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                        (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                  (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                            (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))))))
    -> (Not . P) (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))))
fb108x63To48x27 o =
  rewrite definiP (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                   (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                             (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                       (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))) in
  rewrite definiP (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 \prfF, prf => (prfF . IsLimited08 o) prf

-- 09 3(36x+33) --F[5,-2]->E[2,-4]--> 3(8x+7)
fe108x99To24x21 :
  (o:Nat) -> (Not . P) (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                   (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                             (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))
                                       (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))))
    -> (Not . P) (S (S (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))
fe108x99To24x21 o = rewrite definiP (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                        (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                  (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))
                                                            (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))))))) in
                    rewrite definiP (S (S (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))
                    in \prfF, prf => (prfF . IsLimited09 o) prf

-- 10 3(36x+6) --F[5,-2]->E[2,-4]--> 3(8x+1)
fe108x18To24x3 :
  (o:Nat) ->  (Not . P) (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                        (plus (plus (plus o o) o) (plus (plus o o) o)))
                                  (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                            (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))))))
    -> (Not . P) (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
fe108x18To24x3 o = rewrite definiP (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                 (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                           (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                                     (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o))))))))) in
                   rewrite definiP (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                   in \prfF, prf => (prfF . IsLimited10 o) prf

-- 11 3(36x+18) --F[5,-2]->C[4,-4]--> 3(32x+15)
fc108x54To96x45 :
  (o:Nat) -> (Not . 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)))))))))))))
    -> (Not . 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))))))))))))))))))))
fc108x54To96x45 o = rewrite definiP (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))))))))))))) in
                    rewrite definiP (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))))))))))))))))))))
                    in \prfF, prf => (prfF . IsLimited11 o) prf

-- 12 3(36x+30) --F[5,-2]->B[1,-2]--> 3(16x+13)
fb108x90To48x39 :
  (o:Nat) -> (Not . P) (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                   (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                             (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))
                                       (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))))))
    -> (Not . P) (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)))))))))))))))))
fb108x90To48x39 o = rewrite definiP (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                   (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                             (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))
                                       (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))) in
                    rewrite definiP (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 \prfF, prf => (prfF . IsLimited12 o) prf

-- 13 3(36x+12) --F[5,-2]->B[1,-2]--> 3(16x+5)
fb108x36To48x15 :
  (o:Nat) -> (Not . P) (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                          (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                    (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))
    -> (Not . P) (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)))))))))
fb108x36To48x15 o = rewrite definiP (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                          (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                    (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))) in
                    rewrite definiP (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 \prfF, prf => (prfF . IsLimited13 o) prf

-- 14 3(36x+24) --F[5,-2]->E[2,-4]--> 3(8x+5)
fe108x72To24x15 :
  (o:Nat) ->  (Not . P) (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                              (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                  (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))))))))
    -> (Not . P) (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))
fe108x72To24x15 o = rewrite definiP (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                              (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                  (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))) in
                    rewrite definiP (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))
                    in \prfF, prf => (prfF . IsLimited14 o) prf

-- 15 3(36x+36) --F[5,-2]->C[4,-4]--> 3(32x+31)
fc108x108To96x93 :
  (o:Nat) -> (Not . P) (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                      (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))
                                          (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))))))
    -> (Not . P) (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (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))))))))))))))))))))))))))))))))))))
fc108x108To96x93 o = rewrite definiP (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                      (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))
                                          (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))) (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))))))))) in
                     rewrite definiP (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (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))))))))))))))))))))))))))))))))))))
                     in \prfF, prf => (prfF . IsLimited15 o) prf
-- ########################################


text:
module Parser

import Lightyear
import Control.Monad.Identity
import Lexer
import Syntax

public export
Parser : Type -> Type
Parser = ParserT (List Lexeme) Identity

is : (Monad m, Stream tok str, Eq tok)
     => tok
     -> ParserT str m tok
is l = satisfy (== l)

implementation Stream Lexeme (List Lexeme) where
  uncons []        = Nothing
  uncons (x :: xs) = Just (x, xs)

E : Type
E = Expr

infixOp : Lexeme -> (a -> a -> a) -> Parser (a -> a -> a)
infixOp l ctor = do
  _ <- satisfy (== l)
  pure ctor

addOp : Parser (E -> E -> E)
addOp = infixOp PLUS Plus <|> infixOp MINUS Minus

mulOp : Parser (E -> E -> E)
mulOp = infixOp TIMES Times

boolOp : Parser (E -> E -> E)
boolOp = infixOp EQUAL Equal <|> infixOp LESS Less

tyOp : Parser (Ty -> Ty -> Ty)
tyOp = infixOp TARROW TArrow

-- Actually no "operator" here. Function application is just juxtaposition.
applyOp : Parser (E -> E -> E)
applyOp = pure Apply

isInt : Lexeme -> Bool
isInt (INT n) = True
isInt _       = False

int : Parser Expr
int = do
  (INT i) <- satisfy isInt
  pure (EInt i)

neg : Parser Expr
neg = do
  _ <- is MINUS
  (EInt i) <- int
  pure $ EInt (-i)

lparen : Parser Lexeme
lparen = is LPAREN

rparen : Parser Lexeme
rparen = is RPAREN

semicolon2 : Parser Lexeme
semicolon2 = is SEMICOLON2

true : Parser Expr
true = is TRUE *> pure (EBool True)

false : Parser Expr
false = is FALSE *> pure (EBool False)

isVar : Lexeme -> Bool
isVar (VAR _) = True
isVar _         = False

nm : Parser Name
nm = do
  (VAR nm) <- satisfy isVar
  pure $ nm

var : Parser Expr
var = do
  name <- nm
  pure $ Var name

mutual
  def : Parser TopLevelCmd
  def = do
    _ <- is LET
    name <- nm
    _ <- is EQUAL
    e <- expr
    pure $ TopDef name e

  expr : Parser Expr
  expr = boolean

  boolean : Parser Expr
  boolean = arith `chainl1` boolOp

  arith : Parser Expr
  arith = term `chainl1` addOp

  term : Parser Expr
  term = factor `chainl1` mulOp

  ifExpr : Parser Expr
  ifExpr = do
    _ <- is IF
    c <- expr
    _ <- is THEN
    t <- expr
    _ <- is ELSE
    f <- expr
    pure $ If c t f

  ty : Parser Ty
  ty = tyFactor `chainr1` tyOp

  tyFactor : Parser Ty
  tyFactor = (is TBOOL *> pure TBool)
         <|> (is TINT  *> pure TInt)
         <|> (lparen *>| ty <*| rparen)

  fun : Parser Expr
  fun = do
    _ <- is FUN
    funName <- nm
    _ <- lparen
    parName <- nm
    _ <- is COLON
    parTy <- ty
    _ <- rparen
    _ <- is COLON
    resTy <- ty
    _ <- is IS
    body <- expr
    pure $ Fun funName parName parTy resTy body

  factor : Parser Expr
  factor = (nonApp `chainl1` applyOp)
       <|> ifExpr
       <|> fun

  nonApp : Parser Expr
  nonApp = var
       <|> true
       <|> false
       <|> int
       <|> (lparen *>| expr <*| rparen)

export
toplevel : Parser (List TopLevelCmd)
toplevel = do
  cmd <- TopExpr <$> expr <|> def
  esOpt <- opt (semicolon2 *> toplevel)
  _ <- opt semicolon2
  pure $ cmd :: case esOpt of
    Just es => es
    None    => []

{-
toplevel ::=
  | EOF
  | def EOF
  | def ";;" EOF
  | expr EOF
  | expr ";; EOF
  | def ";;" toplevel
  | expr ";; toplevel

def ::= LET VAR EQUAL expr

expr ::=
  | non_app
  | app
  | arith
  | boolean
  | IF expr THEN expr ELSE expr
  | FUN VAR "(" VAR ":" ty ")" ":" ty IS expr

app ::=
  | app non_app -- huh?
  | non_app non_app

non_app ::=
  | VAR
  | TRUE
  | FALSE
  | INT
  | "(" expr ")"

arith ::=
  | MINUS INT
  | expr PLUS expr
  | expr MINUS expr
  | expr TIMES expr

boolean ::=
  | expr EQUAL expr
  | expr LESS expr

ty ::=
  | TBOOL
  | TINT
  | ty "->" ty
  | "(" ty ")"
-}

ext: idr

max_stars_repo_name: steshaw/idris-miniml

max_issues_repo_name: steshaw/idris-miniml

max_forks_repo_name: steshaw/idris-miniml


text:
module xquant.Core.Helicity

import xquant.Core.Types
import Data.Matrix.Numeric

%default total

---- Helicity type synonyms ----

Bispinor : Type
Bispinor = Matrix 2 2 Amp

Gamma : Type
Gamma = Matrix 4 4 Amp

---- Constant bispinors: Pauli matrices, antisym tensor ----

private i : Amp
i = 0 :+ 1

%access public

sx : Bispinor
sx = [[0,1],[1,0]]

sy : Bispinor
sy = [[0,i],[-i,0]]

sz : Bispinor
sz = [[1,0],[0,-1]]

ep : Bispinor
ep = [[0,-1],[1,0]]

---- Momentum bispinors σ(p) ----

||| Produce a bispinor from a Minkowski 4-vector
bispin : Mink -> Bispinor
bispin [e,px,py,pz] = (e  <#> Id)
                    + (px <#> sx)
                    + (py <#> sy)
                    + (pz <#> sz)

||| Produce a bispinor from a Minkowski 4-vector;
||| Upstairs spinor index (barred) version
bispin' : Mink -> Bispinor
bispin' [e,px,py,pz] = (e  <#> Id)
                     - (px <#> sx)
                     - (py <#> sy)
                     - (pz <#> sz)

||| Minkowski inner product
mink : Mink -> Mink -> Amp
mink (x0 :: xs) (y0 :: ys) = -(x0 * y0) + (xs <:> ys)

|||
eta : Gamma
eta = diag_ [-1,1,1,1]

gx : Matrix 4 4 Amp
gx = concatMatrix [[0,-sx],[sx,0]]

gy : Matrix 4 4 Amp
gy = concatMatrix [[0,-sy],[sy,0]]

gz : Matrix 4 4 Amp
gz = concatMatrix [[0,-sz],[sz,0]]

g0 : Matrix 4 4 Amp
g0 = concatMatrix {x=2} [[0,Id],[Id,0]]

||| Feynman slash: Dot a minkowski vector
||| into the gamma matrix vector
slash : Mink -> Matrix 4 4 Amp
slash [e,x,y,z] = (e <#> Id)
                + (x <#> gx)
                + (y <#> gy)
                + (z <#> gz)

||| 4 standard gamma matrices for D=4
gammas : Vect 4 Gamma
gammas = [g0,gx,gy,gz]

||| implicit conversion from Float to Complex Float
private implicit toCF : Fl -> Amp
toCF x = x :+ 0

g5 : Gamma
g5 = i <#> foldr1 (<>) gammas

||| Left-handed spinor projection
pL : Gamma
pL = 0.5 <#> (1 - g5)

||| Right-handed spinor projection
pR : Gamma
pR = 0.5 <#> (1 + g5)

||| Generate a vector from function
vecGen : (Fin n -> a) -> Vect n a
vecGen f = map f (fins _)

||| Generate a matrix from function
matGen : (Fin n -> Fin m -> a) -> Matrix n m a
matGen f = vecGen <$> vecGen f

||| Spin matrix
spin : Fin 4 -> Fin 4 -> Gamma
spin j k = i*(1/4) <#> index j gammas <<>> index k gammas

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module Main

import Erlang

||| Helper function used to simulate delay.
sleep : Int -> IO ()
sleep ms = do
  erlCall "timer" "sleep" [ms]
  pure ()

loop : IO ()
loop = do
  Just (MkTuple2 from msg) <- erlReceive 5000 Nothing
    (map Just (tuple2 pid atom) <|>
      (exact (MkAtom "stop") *> pure Nothing))
    | Nothing => putStrLn "[LOOP] Loop ended"
  putStrLn ("[LOOP] Message received: " ++ show msg)
  sleep 1000
  currentPid <- erlSelf
  erlSend from (MkTuple2 currentPid msg)
  loop

main : IO ()
main = do
  loopPid <- erlSpawnLink loop
  putStrLn "[MAIN] Loop spawned"
  currentPid <- erlSelf
  erlSend loopPid (MkTuple2 currentPid (MkAtom "hello"))
  putStrLn "[MAIN] Waiting on message from loop"
  Just (MkTuple2 from msg) <- erlReceive 5000 Nothing
    (map Just (tuple2 pid atom))
    | Nothing => do
      putStrLn ("[MAIN] Timed out")
      sleep 10000
  putStrLn ("[MAIN] Message received: " ++ show msg)
  erlSend loopPid (MkAtom "stop")
  putStrLn "[MAIN] Program ended"


text:
> module SequentialDecisionProblems.applications.GoodBad

> import Data.Fin
> import Control.Isomorphism

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Sigma.Sigma

> %default total
> %auto_implicits off
> %access public export

* Good / Bad options:

> data GoodBad = Good | Bad

* |GoodBad| is finite and non-empty:

> to : GoodBad -> Fin 2
> to Good   =    FZ
> to Bad = FS FZ

> from : Fin 2 -> GoodBad
> from             FZ   = Good
> from         (FS FZ)  = Bad
> from     (FS (FS  k)) = absurd k

> toFrom : (k : Fin 2) -> to (from k) = k
> toFrom             FZ   = Refl
> toFrom         (FS FZ)  = Refl
> toFrom     (FS (FS  k)) = absurd k

> fromTo : (a : GoodBad) -> from (to a) = a
> fromTo Good = Refl
> fromTo  Bad = Refl

> |||
> finiteGoodBad : Finite GoodBad
> finiteGoodBad = MkSigma 2 (MkIso to from toFrom fromTo)

> |||
> cardNotZGoodBad : CardNotZ finiteGoodBad
> cardNotZGoodBad = cardNotZLemma finiteGoodBad Good

* |GoodBad| is in |DecEq|:

> goodNotBad : Good = Bad -> Void
> goodNotBad Refl impossible

> implementation [DecEqGoodBad] DecEq GoodBad where
>   decEq Good Good = Yes Refl
>   decEq Good  Bad = No goodNotBad
>   decEq  Bad Good = No (negEqSym goodNotBad)
>   decEq  Bad  Bad = Yes Refl

* |GoodBad| is in |Eq|:

> implementation Eq GoodBad where
>   (==) Good Good = True
>   (==) Good  Bad = False
>   (==)  Bad Good = False
>   (==)  Bad  Bad = True

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Stream.File

import Data.ByteString
import Stream.Internal
import Stream.Util
import System.File

export
chars : HasIO io => Bits32 -> File -> Stream (Of String) io (Maybe FileError)
chars n h = tillRight $ do
  False <- fEOF h | True => pure (Right Nothing)
  Right s <- fGetChars h (cast n) | Left err => pure (Right $ Just err)
  pure (Left s)

export
lines : HasIO io => File -> Stream (Of String) io (Maybe FileError)
lines h = tillRight $ do
  False <- fEOF h | True => pure (Right Nothing)
  Right s <- fGetLine h | Left err => pure (Right $ Just err)
  pure (Left s)

export
withLines :  HasIO io
          => String
          -> (Stream (Of String) io (Maybe FileError) -> io res)
          -> io (Either FileError res)
withLines s f = withFile s Read (pure . id) (\h => Right <$> f (lines h))

export
stdinLn : HasIO io => Stream (Of String) io r
stdinLn = tillRight $ Left <$> getLine

export
bytes :  HasIO io
      => Bits32
      -> File
      -> Stream (Of ByteString) io (Maybe FileError)
bytes n h = tillRight $ do
  False <- fEOF h | True => pure (Right Nothing)
  Right s <- readChunk n h | Left err => pure (Right $ Just err)
  pure (Left s)

export
withBytes :  HasIO io
          => String
          -> Bits32
          -> (Stream (Of ByteString) io (Maybe FileError) -> io res)
          -> io (Either FileError res)
withBytes s n f = withFile s Read (pure . id) (\h => Right <$> f (bytes n h))

export
stdoutLn : HasIO io => Stream (Of String) io r -> Stream Empty io r
stdoutLn = mapM_ putStrLn

export
printLn : HasIO io => Show a => Stream (Of a) io r -> Stream Empty io r
printLn = mapM_ printLn

export
writeBytes :  HasIO io
           => File
           -> Stream (Of ByteString) io r
           -> Stream Empty io r
writeBytes = mapM_ . write


text:
module Interfaces

%default total
-- Define function equality

public export
data FuncEqType : func1 -> func2 -> Type where
  funcEqType : (f : a -> b) -> (g : a -> b) -> ((x : a) -> f x = g x) -> FuncEqType f g

public export
stateFuncEqTransitive : {f : a -> b} -> {g : a -> b} -> {h : a -> b} -> FuncEqType f g -> FuncEqType g h ->  FuncEqType f h
stateFuncEqTransitive (funcEqType f g f_eq_g) (funcEqType g h g_eq_h) = funcEqType f h (\z => rewrite f_eq_g z in g_eq_h z)

public export
stateFuncEqReflexive : {f : a -> b} -> FuncEqType f f
stateFuncEqReflexive = funcEqType f f (\z => Refl)

public export
stateFuncEqSymmetry : FuncEqType a b -> FuncEqType b a
stateFuncEqSymmetry (funcEqType f g a_eq_b) = funcEqType g f (\z => sym (a_eq_b z))

-- Functor Interface

public export
interface MyFunctor (f : Type -> Type) where
  -- equality
  equalsTo : (x : f a) -> (y : f a) -> Type
  eqReflexive : {x : f a} -> x `equalsTo` x
  eqSymmetry : {x, y : f a} -> x `equalsTo` y -> y `equalsTo` x
  eqTransitive :  {x, y, z : f a} -> x `equalsTo` y -> y `equalsTo` z -> x `equalsTo` z

  -- map
  myMap : (func : a -> b) -> (x : f a) -> f b

  -- functor law
  functorLawIdentity : (x : f a) -> myMap Prelude.id x `equalsTo` x
  functorLawComposition : (v : (b -> c)) -> (u : (a -> b)) -> (x : f a) -> myMap (v . u) x `equalsTo` myMap v (myMap u x)

infixl 3 <<*>>

public export
interface MyFunctor f => MyApplicative (f : Type -> Type) where
  myPure : a -> f a
  (<<*>>): f (a -> b) -> f a -> f b

  -- applicative law
  applicativeLawIdentity : (u : f a) ->
    (myPure Prelude.id <<*>> u) `equalsTo` u
  applicativeLawHomomorphism : (x : a) -> (func : a -> b) ->
    (myPure func <<*>> myPure x) `equalsTo` myPure (func x)
  applicativeLawInterchange : (u : f (a -> b)) -> (x : a) ->
    (u <<*>> myPure x) `equalsTo` (myPure ($ x) <<*>> u)
  applicativeLawComposition : (u : f (b -> c)) -> (v : f (a -> b)) -> (w : f a) ->
                              (myPure (\f => \g => \x => f (g x)) <<*>> u <<*>> v <<*>> w) `equalsTo` (u <<*>> (v <<*>> w))

infixl 1 >>>=
public export
interface MyFunctor m => MyMonad (m : Type -> Type) where
  myReturn : a -> m a
  (>>>=) : m a -> (a -> m b) -> m b

  monadLawIdentityLeft : (x : a) -> (f : a -> m b) -> (myReturn x >>>= f) `equalsTo` (f x)
  monadLawIdentityRight : (n : m a) -> (n >>>= myReturn) `equalsTo` n
  monadLawComposition : (n : m a) -> (f : a -> m b) -> (g : b -> m c) ->
                        ((n >>>= f) >>>= g) `equalsTo` (n >>>= \x => f x >>>= g)

max_stars_repo_name: yutaro-sakamoto/prove-monad

max_issues_repo_name: yutaro-sakamoto/prove-monad

max_forks_repo_name: yutaro-sakamoto/prove-monad


text:
module Corecords

-- Standard Streams

corecord Stream' : Type -> Type where
  hd : Stream' a -> a
  tl : Stream' a -> Stream' a
  constructor MkStream' (hd tl)

record Foo : Type -> Type where
  MkFoo : (bar : a) -> (baz : Foo a) -> Foo a

-- Bisimilarity for streams
-- Thanks to asal@itu.dk
-- Ahmad Salim Al-Sibahi

{-
Does not work.

corecord BisimStream' : Stream' a -> Stream' a -> Type where
  phd : BisimStream' s s' -> (hd s) = (hd s')
  ptl : BisimStream' s s' -> BisimStream' (tl s) (tl s')
-}

corecord BisimStream' : (a : Type) -> Stream' a -> Stream' a -> Type where
  phd : BisimStream' a s s' -> (hd s) = (hd s')
  ptl : BisimStream' a s s' -> BisimStream' a (tl s) (tl s')

-- CoTree

corecord CoTree : Type -> Type where
  value : CoTree a -> a
  left  : CoTree a -> CoTree a
  right : CoTree a -> CoTree a

-- Globular types
-- https://code.google.com/p/agda/issues/detail?id=906

corecord Glob : Type where
  Ob : Glob -> Type
  Hom : Glob -> Glob -> Glob -> Glob

Unit_glob : Glob
Unit_glob = MkGlob Unit (\_, _ => Unit_glob)

Id_glob : Type -> Glob
Id_glob a = MkGlob a (\a, b => Id_glob (a = b))

-- Dependent Projections
{-
corecord Foo : Type where
  bar : Foo -> Bool
  baz : (f : Foo) -> if bar f then Nat else Bool -> Foo
  constructor MkFoo (bar baz)-}

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis


text:
module MyLibrary.ZZ2
--mainly code from:https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Data/ZZ.idr and adjusted for Idris2
--includes Sign functionality adjusted for Idris2 from:https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Data/Sign.idr

import Data.Nat
import Decidable.Equality
--import MyLibrary.Sign

%default total

||| A representation of signs for signed datatypes such as `ZZ`
public export
data Sign = Plus | Zero | Minus

public export
opposite : Sign -> Sign
opposite Plus  = Minus
opposite Zero  = Zero
opposite Minus = Plus

public export
multiply : Sign -> Sign -> Sign
multiply Zero  _    = Zero
multiply _     Zero = Zero
multiply Plus  x    = x
multiply Minus x    = opposite x

||| Discover the sign of some type
public export
interface Signed t where
  total sign : t -> Sign

public export
Signed Int where
  sign x = if (compare x 0) == LT then Minus else
           if (compare x 0) == EQ then Zero else Plus
    --| LT = Minus
    --| EQ = Zero
    --| GT = Plus...could use case statements => etc

public export
Signed Integer where
  sign x = if (compare x 0) == LT then Minus else
           if (compare x 0) == EQ then Zero else Plus

public export
Signed Double where
  sign x = if (compare x 0) == LT then Minus else
           if (compare x 0) == EQ then Zero else Plus

||| An integer is either a positive `Nat` or the negated successor of a `Nat`.
|||
||| For example, 3 is `Pos 3` and -2 is `NegS 1`. Zero is arbitrarily chosen
||| to be positive.
|||
public export
data ZZ = Pos Nat | NegS Nat

public export
implementation Signed ZZ where
  sign (Pos Z) = Zero
  sign (Pos _) = Plus
  sign (NegS _) = Minus

||| Take the absolute value of a `ZZ`
public export
absZ : ZZ -> Nat
absZ (Pos n) = n
absZ (NegS n) = S n

public export
implementation Show ZZ where
  showPrec d (Pos n) = showPrec d n
  showPrec d (NegS n) = showParens (d >= PrefixMinus) $ "-" ++ showPrec PrefixMinus (S n)

public export
negNat : Nat -> ZZ
negNat Z = Pos Z
negNat (S n) = NegS n

||| Construct a `ZZ` as the difference of two `Nat`s
public export
minusNatZ : Nat -> Nat -> ZZ
minusNatZ n Z = Pos n
minusNatZ Z (S m) = NegS m
minusNatZ (S n) (S m) = minusNatZ n m

||| Add two `ZZ`s. Consider using `(+) {a=ZZ}`.
public export
plusZ : ZZ -> ZZ -> ZZ
plusZ (Pos n) (Pos m) = Pos (n + m)
plusZ (NegS n) (NegS m) = NegS (S (n + m))
plusZ (Pos n) (NegS m) = minusNatZ n (S m)
plusZ (NegS n) (Pos m) = minusNatZ m (S n)

public export
implementation Eq ZZ where
  (Pos n) == (Pos m) = n == m
  (NegS n) == (NegS m) = n == m
  _ == _ = False

public export
implementation Ord ZZ where
  compare (Pos n) (Pos m) = compare n m
  compare (NegS n) (NegS m) = compare m n
  compare (Pos _) (NegS _) = GT
  compare (NegS _) (Pos _) = LT

||| Multiply two `ZZ`s. Consider using `(*) {a=ZZ}`.
public export
multZ : ZZ -> ZZ -> ZZ
multZ (Pos n) (Pos m) = Pos $ n * m
multZ (NegS n) (NegS m) = Pos $ (S n) * (S m)
multZ (NegS n) (Pos m) = negNat $ (S n) * m
multZ (Pos n) (NegS m) = negNat $ n * (S m)

||| Convert an `Integer` to an inductive representation.
public export
fromInt : Integer -> ZZ
fromInt n = if n < 0
            then NegS $ fromInteger ((-n) - 1)
            else Pos $ fromInteger n

public export
implementation Cast Nat ZZ where
  cast n = Pos n

public export
implementation Num ZZ where
  (+) = plusZ
  (*) = multZ
  fromInteger = fromInt

public export
implementation Abs ZZ where
    abs = cast . absZ

public export
implementation Neg ZZ where
  negate (Pos Z)     = Pos Z
  negate (Pos (S n)) = NegS n
  negate (NegS n)    = Pos (S n)
  (-) n m = plusZ n (negate m)

||| Subtract two `ZZ`s. Consider using `(-) {a=ZZ}`.
public export
subZ : ZZ -> ZZ -> ZZ
subZ n m = (-) n m

public export
implementation Cast ZZ Integer where
  cast (Pos n) = cast n
  cast (NegS n) = (-1) * (cast n + 1)

public export
implementation Cast Integer ZZ where
  cast = fromInteger

--------------------------------------------------------------------------------
-- Properties
--------------------------------------------------------------------------------

public export
natPlusZPlus : (n : Nat) -> (m : Nat) -> (x : Nat)
             -> n + m = x -> (Pos n) + (Pos m) = Pos x
natPlusZPlus n m x h = (cong Pos) h

public export
natMultZMult : (n : Nat) -> (m : Nat) -> (x : Nat)
             -> n * m = x -> (Pos n) * (Pos m) = Pos x
natMultZMult n m x h = (cong Pos) h

public export
doubleNegElim : (z : ZZ) -> negate (negate z) = z
doubleNegElim (Pos Z) = Refl
doubleNegElim (Pos (S n)) = Refl
doubleNegElim (NegS Z) = Refl
doubleNegElim (NegS (S n)) = Refl

-- Injectivity
public export
posInjective : Pos n = Pos m -> n = m
posInjective Refl = Refl

public export
negSInjective : NegS n = NegS m -> n = m
negSInjective Refl = Refl

public export
posNotNeg : Pos n = NegS m -> Void
posNotNeg Refl impossible

-- Decidable equality
public export
implementation DecEq ZZ where
  decEq (Pos n) (NegS m) = No posNotNeg
  decEq (NegS n) (Pos m) = No $ negEqSym posNotNeg
  decEq (Pos n) (Pos m) = case (decEq n m) of
    Yes p => Yes $ (cong Pos) p
    No p => No $ \h => p $ posInjective h
  decEq (NegS n) (NegS m) = case (decEq n m) of
    Yes p => Yes $ (cong NegS) p
    No p => No $ \h => p $ negSInjective h

-- Plus
public export
plusZeroLeftNeutralZ : (right : ZZ) -> 0 + right = right
plusZeroLeftNeutralZ (Pos n) = Refl
plusZeroLeftNeutralZ (NegS n) = Refl

public export
plusZeroRightNeutralZ : (left : ZZ) -> left + 0 = left
plusZeroRightNeutralZ (Pos n) = (cong Pos) $ plusZeroRightNeutral n
plusZeroRightNeutralZ (NegS n) = Refl

public export
plusCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left + right = right + left)
plusCommutativeZ (Pos n) (Pos m) = (cong Pos) $ plusCommutative n m
plusCommutativeZ (Pos n) (NegS m) = Refl
plusCommutativeZ (NegS n) (Pos m) = Refl
plusCommutativeZ (NegS n) (NegS m) = (cong NegS)
  $ (cong S) $ plusCommutative n m

public export
minusNatZAntiCommutative : (j, k : Nat) -> negate (minusNatZ j k) = minusNatZ k j
minusNatZAntiCommutative Z Z = Refl
minusNatZAntiCommutative Z (S k) = Refl
minusNatZAntiCommutative (S j) Z = Refl
minusNatZAntiCommutative (S j) (S k) = minusNatZAntiCommutative j k

public export
negateDistributesPlus : (a, b : ZZ) -> negate (a + b) = (negate a) + (negate b)
negateDistributesPlus (Pos Z) b = rewrite plusZeroLeftNeutralZ b in
                                  rewrite plusZeroLeftNeutralZ (negate b) in Refl
negateDistributesPlus (Pos (S k)) (Pos Z) = rewrite plusZeroRightNeutral k in Refl
negateDistributesPlus (Pos (S k)) (Pos (S j)) = rewrite plusCommutative k (S j) in
                                                rewrite plusCommutative j k in Refl
negateDistributesPlus (Pos (S k)) (NegS j) = minusNatZAntiCommutative k j
negateDistributesPlus (NegS k) (Pos Z) = rewrite plusZeroRightNeutral k in Refl
negateDistributesPlus (NegS k) (Pos (S j)) = minusNatZAntiCommutative j k
negateDistributesPlus (NegS k) (NegS j) = rewrite plusCommutative k (S j) in
                                          rewrite plusCommutative k j in Refl

public export
lemmaMinusSucc : (k, j, i : Nat) -> plusZ (minusNatZ k (S j)) (Pos i) = plusZ (minusNatZ k (S (S j))) (Pos (S i))
lemmaMinusSucc Z j i = Refl
lemmaMinusSucc (S Z) Z i = Refl
lemmaMinusSucc (S (S k)) Z i = rewrite plusCommutative k (S i) in
                               rewrite plusCommutative i k in Refl
lemmaMinusSucc (S k) (S j) i = lemmaMinusSucc k j i

public export
lemmaAssocNegation : (k : Nat) -> (c, r : ZZ) -> (Pos (S k)) + (c + r) = ((Pos (S k)) + c) + r -> (NegS k) + ((negate c) + (negate r)) = ((NegS k) + (negate c)) + (negate r)
lemmaAssocNegation k c r prf = rewrite sym $ negateDistributesPlus c r in
                               rewrite sym $ negateDistributesPlus (Pos (S k)) (plusZ c r) in
                               rewrite sym $ negateDistributesPlus (Pos (S k)) c in
                               rewrite sym $ negateDistributesPlus (plusZ (Pos (S k)) c) r in
                               (cong negate) $ prf

public export
lemmaAssocPos : (k : Nat) -> (c, r : ZZ) -> (Pos k) + (c + r) = ((Pos k) + c) + r
lemmaAssocPos k (Pos j) (Pos i) = (cong Pos) $ plusAssociative k j i
lemmaAssocPos k (Pos Z) (NegS i) = rewrite plusZeroRightNeutral k in Refl
lemmaAssocPos k (Pos (S j)) (NegS Z) = rewrite plusCommutative k (S j) in
                                       rewrite plusCommutative j k in Refl
lemmaAssocPos k (Pos (S j)) (NegS (S i)) = let ind = lemmaAssocPos k (assert_smaller (Pos (S j)) (Pos j)) (assert_smaller (NegS (S i)) (NegS i)) in
                                           rewrite ind in
                                           rewrite plusCommutative k (S j) in
                                           rewrite plusCommutative j k in Refl
lemmaAssocPos k (NegS j) (Pos Z) = rewrite plusZeroRightNeutralZ (minusNatZ k (S j)) in Refl
lemmaAssocPos k (NegS (S j)) (Pos (S i)) = let ind = lemmaAssocPos k (assert_smaller (NegS (S j)) (NegS j)) (assert_smaller (Pos (S i)) (Pos i)) in
                                           rewrite ind in
                                           rewrite lemmaMinusSucc k j i in Refl
lemmaAssocPos Z (NegS Z) (Pos (S i)) = Refl
lemmaAssocPos (S k) (NegS Z) (Pos (S i)) = rewrite plusCommutative k (S i) in
                                           rewrite plusCommutative k i in Refl
lemmaAssocPos Z (NegS j) (NegS i) = Refl
lemmaAssocPos (S k) (NegS Z) (NegS i) = Refl
lemmaAssocPos (S k) (NegS (S j)) (NegS i) = let ind = lemmaAssocPos (assert_smaller (S k) k) (assert_smaller (NegS (S j)) (NegS j)) (NegS i) in
                                            rewrite ind in Refl

public export
plusAssociativeZ : (l, c, r : ZZ) -> l + (c + r) = (l + c) + r
plusAssociativeZ (Pos k) c r = lemmaAssocPos k c r
plusAssociativeZ (NegS k) c r = rewrite sym $ doubleNegElim c in
                                rewrite sym $ doubleNegElim r in
                                lemmaAssocNegation k (negate c) (negate r) (lemmaAssocPos (S k) (negate c) (negate r))

public export
lemmaMinusSymmZero : (k : Nat) -> minusNatZ k k = Pos 0
lemmaMinusSymmZero Z = Refl
lemmaMinusSymmZero (S k) = let ind = lemmaMinusSymmZero k in
                           rewrite ind in Refl

public export --should be RZ? - changed from LZ in original file
plusNegateInverseRZ2 : (a : ZZ) -> a + negate a = Pos Z
plusNegateInverseRZ2 (Pos Z) = Refl
plusNegateInverseRZ2 (Pos (S k)) = rewrite lemmaMinusSymmZero k in Refl
plusNegateInverseRZ2 (NegS k) = rewrite lemmaMinusSymmZero k in Refl

public export --should be LZ? changed from RZ in original file
plusNegateInverseLZ2 : (a : ZZ) -> negate a + a = Pos Z
plusNegateInverseLZ2 (Pos Z) = Refl
plusNegateInverseLZ2 (Pos (S k)) = rewrite lemmaMinusSymmZero k in Refl
plusNegateInverseLZ2 (NegS k) = rewrite lemmaMinusSymmZero k in Refl

-- Mult
public export
multZeroLeftZeroZ : (right : ZZ) -> (Pos Z) * right = (Pos Z)
multZeroLeftZeroZ (Pos k) = Refl
multZeroLeftZeroZ (NegS k) = Refl

public export
multZeroRightZeroZ : (left : ZZ) -> left * (Pos Z) = (Pos Z)
multZeroRightZeroZ (Pos k) = rewrite multZeroRightZero k in Refl
multZeroRightZeroZ (NegS k) = rewrite multZeroRightZero k in Refl

public export
multOneLeftNeutralZ : (right : ZZ) -> 1 * right = right
multOneLeftNeutralZ (Pos k) = rewrite plusZeroRightNeutral k in Refl
multOneLeftNeutralZ (NegS k) = rewrite plusZeroRightNeutral k in Refl

public export
multOneRightNeutralZ : (left : ZZ) -> left * 1 = left
multOneRightNeutralZ (Pos Z) = Refl
multOneRightNeutralZ (Pos (S k)) = (cong Pos) $ multOneRightNeutral (S k)
multOneRightNeutralZ (NegS k) = (cong NegS) $ multOneRightNeutral k

public export
multCommutativeZ : (left : ZZ) -> (right : ZZ) -> (left * right = right * left)
multCommutativeZ (Pos k) (Pos j) = (cong Pos) $ multCommutative k j
multCommutativeZ (Pos k) (NegS j) = rewrite multCommutative j k in
                                    (cong negNat) $ multRightSuccPlus k j
multCommutativeZ (NegS k) (Pos j) = rewrite multCommutative j (S k) in Refl
multCommutativeZ (NegS k) (NegS j) = (cong Pos) $ multCommutative (S k) (S j)

public export
lemmaPosMultNegNat : (k, j : Nat) -> multZ (Pos k) (negNat j) = negNat (mult k j)
lemmaPosMultNegNat k Z = rewrite multZeroRightZero k in Refl
lemmaPosMultNegNat k (S j) = Refl

public export
lemmaNegMultNegNat : (k, j : Nat) -> multZ (NegS k) (negNat j) = multZ (Pos (S k)) (Pos j)
lemmaNegMultNegNat k Z = rewrite multZeroRightZero k in Refl
lemmaNegMultNegNat k (S j) = Refl

public export
lemmaNegatePosNegNat : (k : Nat) -> negate (Pos k) = negNat k
lemmaNegatePosNegNat Z = Refl
lemmaNegatePosNegNat (S k) = Refl

public export
multNegLeftZ : (k : Nat) -> (j : ZZ) -> (NegS k) * j = negate (Pos (S k) * j)
multNegLeftZ k (Pos j) = rewrite lemmaNegatePosNegNat ((S k) * j) in Refl
multNegLeftZ k (NegS j) = Refl

public export
multNegateLeftZ : (k, j : ZZ) -> (negate k) * j = negate (k * j)
multNegateLeftZ (Pos Z) j = rewrite multZeroLeftZeroZ j in Refl
multNegateLeftZ (Pos (S k)) (Pos j) = rewrite lemmaNegatePosNegNat ((S k) * j) in Refl
multNegateLeftZ (Pos (S k)) (NegS j) = Refl
multNegateLeftZ (NegS k) j = rewrite sym $ doubleNegElim (multZ (Pos (S k)) j) in
                             rewrite multNegLeftZ k j in Refl

public export
multAssociativeZPos : (k : Nat) -> (c, r : ZZ) -> (Pos k) * (c * r) = ((Pos k) * c) * r
multAssociativeZPos k (Pos j) (Pos i) = (cong Pos) $ multAssociative k j i
multAssociativeZPos k (Pos j) (NegS i) = rewrite sym $ multAssociative k j (S i) in lemmaPosMultNegNat k (mult j (S i))
multAssociativeZPos k (NegS j) (Pos i) = rewrite multCommutative j i in
                                         rewrite sym $ multRightSuccPlus i j in
                                         rewrite lemmaPosMultNegNat k (mult i (S j)) in
                                         rewrite multCommutativeZ (negNat (mult k (S j))) (Pos i) in
                                         rewrite lemmaPosMultNegNat i (mult k (S j)) in
                                         rewrite multAssociative k i (S j) in
                                         rewrite multAssociative i k (S j) in
                                         rewrite multCommutative i k in Refl
multAssociativeZPos k (NegS j) (NegS i) = rewrite multCommutativeZ (negNat (mult k (S j))) (NegS i) in
                                          rewrite lemmaNegMultNegNat i (mult k (S j)) in
                                          rewrite multAssociative k (S j) (S i) in
                                          rewrite multCommutative (mult k (S j)) (S i) in Refl

public export
multAssociativeZ : (l, c, r : ZZ) -> l * (c * r) = (l * c) * r
multAssociativeZ (Pos k) c r = multAssociativeZPos k c r
multAssociativeZ (NegS k) c r = rewrite multNegLeftZ k (c * r) in
                                rewrite multNegLeftZ k c in
                                rewrite multNegateLeftZ (multZ (Pos (S k)) c) r in
                                (cong negate) $ multAssociativeZPos (S k) c r

public export
lemmaPlusPosNegCancel : (k, j, i : Nat) -> plusZ (Pos (plus k j)) (negNat (plus k i)) = plusZ (Pos j) (negNat i)
lemmaPlusPosNegCancel Z j i = Refl
lemmaPlusPosNegCancel (S Z) j Z = rewrite plusZeroRightNeutral j in Refl
lemmaPlusPosNegCancel (S Z) j (S i) = Refl
lemmaPlusPosNegCancel (S (S k)) j i = lemmaPlusPosNegCancel (S k) j i

public export
lemmaPlusPosNegZero : (k : Nat) -> plusZ (Pos k) (negNat k) = Pos Z
lemmaPlusPosNegZero Z = Refl
lemmaPlusPosNegZero (S k) = rewrite lemmaMinusSymmZero k in Refl

public export
negNatDistributesPlus : (j, k : Nat) -> plusZ (negNat j) (negNat k) = negNat (plus j k)
negNatDistributesPlus Z k = rewrite plusZeroLeftNeutralZ (negNat k) in Refl
negNatDistributesPlus (S j) Z = rewrite plusZeroRightNeutral j in Refl
negNatDistributesPlus (S j) (S k) = rewrite plusSuccRightSucc j k in Refl

-- Distributivity
public export
multDistributesOverPlusRightPosPosZ : (l, c : Nat) -> (r : ZZ) -> (Pos l) * ((Pos c) + r) = ((Pos l) * (Pos c)) + ((Pos l) * r)
multDistributesOverPlusRightPosPosZ l c (Pos i) = rewrite multDistributesOverPlusRight l c i in Refl
multDistributesOverPlusRightPosPosZ l Z (NegS i) = rewrite multZeroRightZero l in
                                                   rewrite plusZeroLeftNeutralZ (negNat (mult l (S i))) in Refl
multDistributesOverPlusRightPosPosZ l (S c) (NegS Z) = rewrite multOneRightNeutral l in
                                                       rewrite multRightSuccPlus l c in
                                                       rewrite sym $ plusAssociativeZ (Pos l) (Pos (mult l c)) (negNat l) in
                                                       rewrite plusCommutativeZ (Pos (mult l c)) (negNat l) in
                                                       rewrite plusAssociativeZ (Pos l) (negNat l) (Pos (mult l c)) in
                                                       rewrite lemmaPlusPosNegZero l in Refl
multDistributesOverPlusRightPosPosZ l (S c) (NegS (S i)) = let ind = multDistributesOverPlusRightPosPosZ l (assert_smaller (S c) c) (assert_smaller (NegS (S i)) (NegS i)) in
                                                           rewrite ind in
                                                           rewrite multRightSuccPlus l (S i) in
                                                           rewrite multRightSuccPlus l c in
                                                           rewrite lemmaPlusPosNegCancel l (mult l c) (mult l (S i)) in Refl

public export
multDistributesOverPlusRightPosZ : (k : Nat) -> (c, r : ZZ) -> (Pos k) * (c + r) = ((Pos k) * c) + ((Pos k) * r)
multDistributesOverPlusRightPosZ k (Pos j) r = multDistributesOverPlusRightPosPosZ k j r
multDistributesOverPlusRightPosZ k (NegS j) (Pos i) = rewrite plusCommutativeZ ((Pos k) * (NegS j)) ((Pos k) * (Pos i)) in
                                                      rewrite multDistributesOverPlusRightPosPosZ k i (NegS j) in Refl
multDistributesOverPlusRightPosZ k (NegS j) (NegS i) = rewrite negNatDistributesPlus (mult k (S j)) (mult k (S i)) in
                                                       rewrite sym $ multDistributesOverPlusRight k (S j) (S i) in
                                                       rewrite plusSuccRightSucc j i in Refl

public export
multDistributesOverPlusRightZ : (l, c, r : ZZ) -> l * (c + r) = (l * c) + (l * r)
multDistributesOverPlusRightZ (Pos k) c r = multDistributesOverPlusRightPosZ k c r
multDistributesOverPlusRightZ (NegS k) c r = rewrite multNegLeftZ k (plusZ c r) in
                                             rewrite multNegLeftZ k c in
                                             rewrite multNegLeftZ k r in
                                             rewrite sym $ negateDistributesPlus (multZ (Pos (S k)) c) (multZ (Pos (S k)) r) in
                                             rewrite multDistributesOverPlusRightPosZ (S k) c r in Refl

public export
multDistributesOverPlusLeftZ : (l, c, r : ZZ) -> (l + c) * r = (l * r) + (c * r)
multDistributesOverPlusLeftZ l c r = rewrite multCommutativeZ (l + c) r in
                                     rewrite multDistributesOverPlusRightZ r l c in
                                     rewrite multCommutativeZ r l in
                                     rewrite multCommutativeZ r c in Refl

max_stars_repo_name: reswatson/ZZ

max_issues_repo_name: reswatson/ZZ

max_forks_repo_name: reswatson/ZZ


text:
||| A simply expression language, adapted from PLFA Part 2 [1],
||| together with mechanical proof of type-safety.
|||
||| `PLFA` is an expression language supporting:
|||
||| + Let-bindings;
||| + Products; and
||| + Sums
|||
||| Well-known construction techniques are used to represent the
||| language as an intrindsically well-typed EDSL, together with it's
||| mechanical proof of progress.
|||
||| This module corresponds to Section 2 of the Functional Pearl.
|||
||| [1] https://plfa.github.io/
|||
module Razor.PLFA

import Razor.Common

%default total

namespace Types

  public export
  data Ty = TyInt
          | TyChar
          | TyProd Ty Ty
          | TySum Ty Ty

namespace Terms

  public export
  data PLFA : (ctxt : List Ty) -> (type : Ty) -> Type where
    -- Let-Bindings & Variables
    Var : Elem ty g -> PLFA g ty
    Let : (this     : PLFA        g  expr)
       -> (beInThis : PLFA (expr::g) body)
                   -> PLFA        g  body

    -- Base Values
    I : Int  -> PLFA g TyInt
    C : Char -> PLFA g TyChar

    -- Products and accessors
    MkPair : (left  : PLFA g l)
          -> (right : PLFA g r)
                   -> PLFA g (TyProd l r)

    First  : (pair : PLFA g (TyProd l r))
                  -> PLFA g l

    Second : (pair : PLFA g (TyProd l r))
                  -> PLFA g r

    Split : (pair : PLFA g         (TyProd l r))
         -> (body : PLFA (r::l::g) b)
                 -> PLFA g         b

    -- Sums and accessors
    Left : (left : PLFA g        l)
                -> PLFA g (TySum l r)

    Right : (right : PLFA g          r)
                  -> PLFA g (TySum l r)

    Match : (variant   : PLFA g      (TySum l r))
         -> (whenLeft  : PLFA (l::g) b)
         -> (whenRight : PLFA (r::g) b)
                      -> PLFA g      b

namespace Renaming

  public export
  weaken : (Contains  old           type -> Contains  new           type)
        -> (Contains (old += type') type -> Contains (new += type') type)

  weaken func Here         = Here
  weaken func (There rest) = There (func rest)

  public export
  rename : (forall type . Contains old type -> Contains new type)
        -> (forall type . PLFA     old type -> PLFA     new type)
  -- Let Bindings & Variables
  rename f (Var x) = Var (f x)
  rename f (Let this beInThis) = Let (rename f this)
                                     (rename (weaken f) beInThis)

  -- Base Values
  rename f (I x) = I x
  rename f (C x) = C x

  -- Products & Accessors
  rename f (MkPair left right) = MkPair (rename f left) (rename f right)
  rename f (First pair) = First (rename f pair)
  rename f (Second pair) = Second (rename f pair)
  rename f (Split pair body) = Split (rename f pair)
                                     (rename ((weaken (weaken f))) body)

  -- Sums & Accessors
  rename f (Left left) = Left (rename f left)
  rename f (Right right) = Right (rename f right)
  rename f (Match variant whenLeft whenRight) = Match (rename f variant)
                                                      (rename (weaken f) whenLeft)
                                                      (rename (weaken f) whenRight)

namespace Substitution

  public export
  weakens : (forall type. Contains  old           type -> PLFA  new           type)
         -> (forall type. Contains (old += type') type -> PLFA (new += type') type)
  weakens f Here         = Var Here
  weakens f (There rest) = rename There (f rest)

  -- general substitute
  namespace General
    public export
    subst : (forall type . Contains old type -> PLFA new type)
         -> (forall type . PLFA     old type -> PLFA new type)

    -- Let-Bindings & Variables
    subst f (Var x) = (f x)
    subst f (Let this beInThis) = Let (subst f this)
                                      (subst (weakens f) beInThis)

    -- Base Values
    subst f (I x) = I x
    subst f (C x) = C x

    -- Products & Accessors
    subst f (MkPair left right) = MkPair (subst f left) (subst f right)
    subst f (First pair) = First (subst f pair)
    subst f (Second pair) = Second (subst f pair)
    subst f (Split pair body) = Split (subst f pair)
                                      (subst ((weakens (weakens f))) body)

    -- Sums & Accessors
    subst f (Left left) = Left (subst f left)
    subst f (Right right) = Right (subst f right)
    subst f (Match variant whenLeft whenRight) = Match (subst f variant)
                                                       (subst (weakens f) whenLeft)
                                                       (subst (weakens f) whenRight)
  namespace Single
    public export
    apply : (this   : PLFA ctxt typeB)
         -> (idx    : Contains (ctxt += typeB) typeA)
                   -> PLFA ctxt typeA
    apply this Here         = this
    apply this (There rest) = Var rest

    public export
    subst : (this   : PLFA  ctxt           typeB)
         -> (inThis : PLFA (ctxt += typeB) typeA)
                   -> PLFA  ctxt           typeA
    subst {ctxt} {typeA} {typeB} this inThis = General.subst (apply this) inThis

  namespace Double

    public export
    apply : (this    : PLFA       ctxt                     typeA)
         -> (andThis : PLFA       ctxt                     typeB)
         -> (idx     : Contains ((ctxt += typeA) += typeB) typeC)
                    -> PLFA       ctxt                     typeC
    apply this andThis Here              = andThis
    apply this andThis (There Here)      = this
    apply this andThis (There (There x)) = Var x

    public export
    subst : (this    : PLFA  ctxt                     typeA)
         -> (andThis : PLFA  ctxt                     typeB)
         -> (inThis : PLFA ((ctxt += typeA) += typeB) typeC)
                   -> PLFA   ctxt                     typeC
    subst {ctxt} {typeA} {typeB} {typeC} this andThis inThis = General.subst (apply this andThis) inThis

namespace Values

  public export
  data Value : PLFA ctxt type -> Type where
    IV : Value (I i)
    CV : Value (C c)
    MkPairV : Value left
           -> Value right
           -> Value (MkPair left right)

    LeftV : Value value
         -> Value (Left value)

    RightV : Value value
          -> Value (Right value)

namespace Reduction
  public export
  data Redux : (this, that : PLFA ctxt type) -> Type where
    -- Let Bindings
    SimplifyLetValue : Redux this that
                    -> Redux (Let this body)
                             (Let that body)
    ReduceLetBody : Value value
                 -> Redux (Let value body)
                          (subst value body)

    -- MkPairs
    SimplifyPairFirst : Redux this that
                    -> Redux (MkPair this right)
                             (MkPair that right)
    SimplifyPairSecond : Value left
                      -> Redux this that
                      -> Redux (MkPair left this)
                               (MkPair left that)

    -- Accessors
    SimplifyFirst : Redux this that
                 -> Redux (First this) (First that)

    ReduceFirst : Value left -> Value right -> Redux (First (MkPair left right)) left

    SimplifySecond : Redux this that
                  -> Redux (Second this) (Second that)

    ReduceSecond : Value left -> Value right -> Redux (Second (MkPair left right)) right

    -- Split Pairs
    SimplifySplitPair : Redux this that
                     -> Redux (Split this body) (Split that body)

    ReduceSplitPair : {right : PLFA g r}
                   -> {left  : PLFA g l}
                   -> {body : PLFA (r::l::g) b}
                   -> Value left
                   -> Value right
                   -> Redux (Split (MkPair left right) body)
                            (subst left right body)

    -- Variants
    SimplifyLeft : Redux this that
                -> Redux (Left this) (Left that)

    SimplifyRight : Redux this that
                 -> Redux (Right this) (Right that)

    SimplifyMatchCase : Redux this that
                     -> Redux (Match this whenleft whenright)
                              (Match that whenleft whenright)

    ReduceMatchBodyWhenLeft : Value value
                           -> Redux (Match (Left value) whenleft whenright)
                                    (subst value whenleft)

    ReduceMatchBodyWhenRight : Value value
                            -> Redux (Match (Right value) whenleft whenright)
                                     (subst value whenright)

namespace Progress
  public export
  data Progress : (term : PLFA Nil type)
                       -> Type
    where
      Done : {term : PLFA Nil mty} -> Value term -> Progress term
      Step : {this, that : PLFA Nil type}
          -> (prf  : Redux this that)
                  -> Progress this

  public export
  progress : (term : PLFA Nil type) -> Progress term

  -- Let-Bindings & Variables
  progress (Var _) impossible
  progress (Let this beInThis) with (progress this)
    progress (Let this beInThis) | (Done x) = Step (ReduceLetBody x)
    progress (Let this beInThis) | (Step prf) = Step (SimplifyLetValue prf)

  -- Base Values
  progress (I x) = Done IV
  progress (C x) = Done CV

  -- Products & Accessors
  progress (MkPair left right) with (progress left)
    progress (MkPair left right) | (Done vl) with (progress right)
      progress (MkPair left right) | (Done vl) | (Done vr) = Done (MkPairV vl vr)
      progress (MkPair left right) | (Done vl) | (Step pr) = Step (SimplifyPairSecond vl pr)

    progress (MkPair left right) | (Step pl) = Step (SimplifyPairFirst pl)

  progress (First pair) with (progress pair)
    progress (First (MkPair left right)) | (Done (MkPairV l r)) = Step (ReduceFirst l r)
    progress (First pair) | (Step pp) = Step (SimplifyFirst pp)

  progress (Second pair) with (progress pair)
    progress (Second (MkPair left right)) | (Done (MkPairV l r)) = Step (ReduceSecond l r)
    progress (Second pair) | (Step pp) = Step (SimplifySecond pp)

  progress (Split pair body) with (progress pair)
    progress (Split (MkPair left right) body) | (Done (MkPairV l r)) = Step (ReduceSplitPair l r)
    progress (Split pair body) | (Step pp) = Step (SimplifySplitPair pp)

  -- Sums & Accessors
  progress (Left left) with (progress left)
    progress (Left left) | (Done lv) = Done (LeftV lv)
    progress (Left left) | (Step lp) = Step (SimplifyLeft lp)

  progress (Right right)  with (progress right)
    progress (Right right) | (Done rv) = Done (RightV rv)
    progress (Right right) | (Step rp) = Step (SimplifyRight rp)

  progress (Match variant whenLeft whenRight) with (progress variant)
    progress (Match (Left left)   whenLeft whenRight) | (Done (LeftV  lv)) = Step (ReduceMatchBodyWhenLeft  lv)
    progress (Match (Right right) whenLeft whenRight) | (Done (RightV rv)) = Step (ReduceMatchBodyWhenRight rv)
    progress (Match variant whenLeft whenRight) | (Step vp) = Step (SimplifyMatchCase vp)

namespace Evaluation

  public export
  data Reduces : (this : PLFA ctxt type)
              -> (that : PLFA ctxt type)
              -> Type
    where
      Refl  : Reduces this this
      Trans : Redux this that
           -> Reduces that end
           -> Reduces this end

  public export
  data Finished : (term : PLFA ctxt type)
                       -> Type
    where
      Normalised : {term : PLFA ctxt type} -> Value term -> Finished term
      OOF : Finished term

  public export
  data Evaluate : (term : PLFA Nil type) -> Type where
    RunEval : (steps  : Inf (Reduces this that))
           -> (result : Finished that)
           -> Evaluate this

  public export
  data Fuel = Empty | More (Lazy Fuel)

  public export
  covering
  forever : Fuel
  forever = More forever

  public export
  compute : (fuel : Fuel)
         -> (term : PLFA Nil type)
                 -> Evaluate term
  compute Empty term = RunEval Refl OOF
  compute (More fuel) term with (progress term)
    compute (More fuel) term | (Done value) = RunEval Refl (Normalised value)
    compute (More fuel) term | (Step step {that}) with (compute fuel that)
      compute (More fuel) term | (Step step {that = that}) | (RunEval steps result)
        = RunEval (Trans step steps) result

public export
covering
run : (this : PLFA Nil type)
           -> Maybe (Subset (PLFA Nil type) (Reduces this))
run this with (compute forever this)
  run this | (RunEval steps (Normalised {term} x)) = Just (Element term steps)
  run this | (RunEval steps OOF) = Nothing

namespace Examples
  public export
  ab : PLFA Nil (TyProd TyInt TyChar)
  ab = MkPair (I 1) (C 'c')

  public export
  a : PLFA Nil TyInt
  a = First ab

  public export
  b : PLFA Nil TyChar
  b = Second ab

  public export
  ba : PLFA Nil (TyProd TyChar TyInt)
  ba = Split ab (MkPair (Var Here) (Var $ There Here))

  public export
  l : PLFA Nil (TySum TyChar TyInt)
  l = Left (C 'c')

  public export
  r : PLFA Nil (TySum TyChar TyInt)
  r = Right (I 1)

  public export
  lp : PLFA Nil (TyProd TyInt TyChar)
  lp = Match l (MkPair (I 2) (Var Here)) (MkPair (Var Here) (C 'w'))

  public export
  rp : PLFA Nil (TyProd TyInt TyChar)
  rp = Match r (MkPair (I 2) (Var Here)) (MkPair (Var Here) (C 'w'))

--  snip : PLFA Nil TyInt
--  snip = Match (Left (I 1)) (Var Here) (Split (Var Here) (Var Here))

max_stars_repo_name: border-patrol/pearly-razors

max_issues_repo_name: border-patrol/pearly-razors

max_forks_repo_name: border-patrol/pearly-razors


text:
import Control.Monad.Identity

public export
interface Foo (sA : Type) where
  A : Type
  Elem : A -> sA -> Type
  Empty : sA -> Type
  Empty as = (a : A) -> Not (Elem a as)

public export
implementation Foo (Identity Bool) where
  A = Bool
  Elem x (Id y) = x = y


text:
module Interface

interface Show a => Pretty (0 a : Type) where
  constructor MkPretty

  0 Doc : Type
  toDoc : String -> Doc

  pretty : a -> Doc
  pretty n = toDoc (show n)

  prettys : List a -> List Doc
  prettys [] = []
  prettys (a :: as) = pretty a :: prettys as


text:
module Replica.Options

%default total

public export
record Options where

  constructor MkOptions

  interactive : Bool
  tests : List String

defaultOutputFile : String
defaultOutputFile = "output"

mkOpt : Options
mkOpt = MkOptions False []

parseParams :  Options -> List String -> Options
parseParams opts ("--interactive" :: xs)
  = parseParams (record {interactive = True} opts) xs
parseParams opts (x :: xs)
  = parseParams (record {tests $= (++ [x])} opts) xs
parseParams opts []
  = opts

export
options : List String -> Options
options params = parseParams mkOpt params

max_stars_repo_name: xvw/REPLica

max_issues_repo_name: xvw/REPLica

max_forks_repo_name: xvw/REPLica


text:
module Web.Dom

import JS
import public Web.Internal.Types
import public Web.Raw.Dom as Dom

%default total

--------------------------------------------------------------------------------
--          Main entry points
--------------------------------------------------------------------------------

%foreign "browser:lambda:()=>window"
prim__window : PrimIO Window

%foreign "browser:lambda:()=>document"
prim__document : PrimIO Document

export
window : JSIO Window
window = primJS prim__window

export
document : JSIO Document
document = primJS prim__document

export
body : JSIO HTMLElement
body = unMaybe "Web.Dom.body" $ document >>= to body

--------------------------------------------------------------------------------
--          Elements
--------------------------------------------------------------------------------

||| HTML Element Tags.
|||
||| This is mainly to be used with `Web.Dom.createElement` and `newElement`.
||| Some deprecated tags have been left out, some others might
||| still be missing.
public export
data ElementType : (tag : String) -> (htmlElement : Type) -> Type where
  A          : ElementType "a" HTMLAnchorElement
  Area       : ElementType "area" HTMLAreaElement
  Audio      : ElementType "audio" HTMLAudioElement
  Base       : ElementType "base" HTMLBaseElement
  Blockquote : ElementType "blockquote" HTMLQuoteElement
  Body       : ElementType "body" HTMLBodyElement
  Br         : ElementType "br" HTMLBRElement
  Button     : ElementType "button" HTMLButtonElement
  Canvas     : ElementType "canvas" HTMLCanvasElement
  Caption    : ElementType "caption" HTMLTableCaptionElement
  Col        : ElementType "col" HTMLTableColElement
  Colgroup   : ElementType "colgroup" HTMLTableColElement
  Data       : ElementType "data" HTMLDataElement
  Datalist   : ElementType "datalist" HTMLDataListElement
  Del        : ElementType "del" HTMLModElement
  Details    : ElementType "details" HTMLDetailsElement
  Dialog     : ElementType "dialog" HTMLDialogElement
  Div        : ElementType "div" HTMLDivElement
  Dl         : ElementType "dl" HTMLDListElement
  Embed      : ElementType "embed" HTMLEmbedElement
  FieldSet   : ElementType "fieldset" HTMLFieldSetElement
  Form       : ElementType "form" HTMLFormElement
  H1         : ElementType "h1" HTMLHeadingElement
  H2         : ElementType "h2" HTMLHeadingElement
  H3         : ElementType "h3" HTMLHeadingElement
  H4         : ElementType "h4" HTMLHeadingElement
  H5         : ElementType "h5" HTMLHeadingElement
  H6         : ElementType "h6" HTMLHeadingElement
  HR         : ElementType "hr" HTMLHRElement
  Html       : ElementType "html" HTMLHtmlElement
  IFrame     : ElementType "iframe" HTMLIFrameElement
  Ime        : ElementType "img" HTMLImageElement
  Input      : ElementType "input" HTMLInputElement
  Ins        : ElementType "ins" HTMLModElement
  Label      : ElementType "label" HTMLLabelElement
  Legend     : ElementType "legend" HTMLLegendElement
  Li         : ElementType "li" HTMLLIElement
  Link       : ElementType "link" HTMLLinkElement
  Map        : ElementType "map" HTMLMapElement
  Menu       : ElementType "menu" HTMLMenuElement
  Meta       : ElementType "meta" HTMLMetaElement
  Meter      : ElementType "meter" HTMLMeterElement
  Object     : ElementType "object" HTMLObjectElement
  Ol         : ElementType "ol" HTMLOListElement
  OptGroup   : ElementType "optgroup" HTMLOptGroupElement
  Option     : ElementType "option" HTMLOptionElement
  Output     : ElementType "output" HTMLOutputElement
  P          : ElementType "p" HTMLParagraphElement
  Param      : ElementType "param" HTMLParamElement
  Picture    : ElementType "picture" HTMLPictureElement
  Pre        : ElementType "pre" HTMLPreElement
  Progress   : ElementType "progress" HTMLProgressElement
  Q          : ElementType "q" HTMLQuoteElement
  Script     : ElementType "script" HTMLScriptElement
  Select     : ElementType "Select" HTMLSelectElement
  Slot       : ElementType "slot" HTMLSlotElement
  Source     : ElementType "source" HTMLSourceElement
  Span       : ElementType "span" HTMLSpanElement
  Style      : ElementType "style" HTMLStyleElement
  Table      : ElementType "table" HTMLTableElement
  Tbody      : ElementType "tbody" HTMLTableSectionElement
  Td         : ElementType "td" HTMLTableCellElement
  Template   : ElementType "template" HTMLTemplateElement
  TextArea   : ElementType "textarea" HTMLTextAreaElement
  Tfoot      : ElementType "tfoot" HTMLTableSectionElement
  Th         : ElementType "th" HTMLTableCellElement
  Thead      : ElementType "thead" HTMLTableSectionElement
  Time       : ElementType "time" HTMLTimeElement
  Title      : ElementType "title" HTMLTitleElement
  Tr         : ElementType "tr" HTMLTableRowElement
  Track      : ElementType "track" HTMLTrackElement
  Ul         : ElementType "ul" HTMLUListElement
  Video      : ElementType "video" HTMLVideoElement

||| Extracts the `tag` String from a known `ElementType`.
public export
elementTag : {tag : _} -> ElementType tag t -> String
elementTag _ = tag

||| Proof, that each element type has an instance of `SafeCast`.
export
elemCast :  (0 f : Type -> Type)
         -> ({0 a : Type} -> SafeCast a => f a)
         -> (e : ElementType s t)
         -> f t
elemCast _ fun A          = fun
elemCast _ fun Area       = fun
elemCast _ fun Audio      = fun
elemCast _ fun Base       = fun
elemCast _ fun Blockquote = fun
elemCast _ fun Body       = fun
elemCast _ fun Br         = fun
elemCast _ fun Button     = fun
elemCast _ fun Canvas     = fun
elemCast _ fun Caption    = fun
elemCast _ fun Col        = fun
elemCast _ fun Colgroup   = fun
elemCast _ fun Data       = fun
elemCast _ fun Datalist   = fun
elemCast _ fun Del        = fun
elemCast _ fun Details    = fun
elemCast _ fun Dialog     = fun
elemCast _ fun Div        = fun
elemCast _ fun Dl         = fun
elemCast _ fun Embed      = fun
elemCast _ fun FieldSet   = fun
elemCast _ fun Form       = fun
elemCast _ fun H1         = fun
elemCast _ fun H2         = fun
elemCast _ fun H3         = fun
elemCast _ fun H4         = fun
elemCast _ fun H5         = fun
elemCast _ fun H6         = fun
elemCast _ fun HR         = fun
elemCast _ fun Html       = fun
elemCast _ fun IFrame     = fun
elemCast _ fun Ime        = fun
elemCast _ fun Input      = fun
elemCast _ fun Ins        = fun
elemCast _ fun Label      = fun
elemCast _ fun Legend     = fun
elemCast _ fun Li         = fun
elemCast _ fun Link       = fun
elemCast _ fun Map        = fun
elemCast _ fun Menu       = fun
elemCast _ fun Meta       = fun
elemCast _ fun Meter      = fun
elemCast _ fun Object     = fun
elemCast _ fun Ol         = fun
elemCast _ fun OptGroup   = fun
elemCast _ fun Option     = fun
elemCast _ fun Output     = fun
elemCast _ fun P          = fun
elemCast _ fun Param      = fun
elemCast _ fun Picture    = fun
elemCast _ fun Pre        = fun
elemCast _ fun Progress   = fun
elemCast _ fun Q          = fun
elemCast _ fun Script     = fun
elemCast _ fun Select     = fun
elemCast _ fun Slot       = fun
elemCast _ fun Source     = fun
elemCast _ fun Span       = fun
elemCast _ fun Style      = fun
elemCast _ fun Table      = fun
elemCast _ fun Tbody      = fun
elemCast _ fun Td         = fun
elemCast _ fun Template   = fun
elemCast _ fun TextArea   = fun
elemCast _ fun Tfoot      = fun
elemCast _ fun Th         = fun
elemCast _ fun Thead      = fun
elemCast _ fun Time       = fun
elemCast _ fun Title      = fun
elemCast _ fun Tr         = fun
elemCast _ fun Track      = fun
elemCast _ fun Ul         = fun
elemCast _ fun Video      = fun

||| Creates a new element using the given `ElementType`'s `tag`
||| and casting the result to the corresponding HTML element type.
||| See also `newElement`.
export
createElement : {tag : _} -> (e : ElementType tag t) -> JSIO t
createElement e =
   elemCast JSIO ( castingTo #"JS.Dom.createElement [\#{tag}]"# $
                   document >>= (`createElement'` tag)) e

||| Like `createElement` but applies the given set of
||| modifiers. This is especially useful for setting an element's
||| attributes.
export
newElement :  {tag : _}
           -> (e : ElementType tag t)
           -> (mods : List (t -> JSIO ()))
           -> JSIO t
newElement e mods = do res <- createElement e
                       for_ mods \m => m res
                       pure res

--------------------------------------------------------------------------------
--          Finding Elements
--------------------------------------------------------------------------------

export
getElementById : String -> JSIO (Maybe Element)
getElementById s = getElementById !document s

export
castElementById_ : SafeCast a => String -> JSIO (Maybe a)
castElementById_ = map (>>= safeCast) . getElementById

export
castElementById : (0 a : Type) -> SafeCast a => String -> JSIO (Maybe a)
castElementById _ = castElementById_

export
htmlElementById : ElementType tag a -> String -> JSIO (Maybe a)
htmlElementById e s = elemCast (JSIO . Maybe) (castElementById_ s) e

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

export
ArrayLike NodeList Node where

export
ArrayLike DOMTokenList String where

export
Callback EventListener (Event -> JSIO ()) where
  callback f = toEventListener (runJS . f)

export
Callback MutationCallback (  Array MutationRecord
                          -> MutationObserver
                          -> JSIO () ) where
  callback f = toMutationCallback \a,m => runJS (f a m)

||| In case of an error, the error is logged to the console and
||| the node is rejected
export
Callback NodeFilter (Node -> JSIO Bits16) where
  callback f = toNodeFilter (runJSWithDefault FILTER_REJECT . f)

export
Callback XPathNSResolver (Maybe String -> JSIO (Maybe String) ) where
  callback f = toXPathNSResolver $ map maybeToNullable
                                 . runJSWithDefault Nothing
                                 . f
                                 . nullableToMaybe


text:
-- Idris2

import System
import System.Concurrency

-- Test `conditionBroadcast` wakes all threads for 1 main and N child threads

main : IO ()
main =
  let n = 3 in
  do cvMutex <- makeMutex
     cv <- makeCondition
     ts <- for [1..n] $ \_ => fork $ do mutexAcquire cvMutex
                                        conditionWait cv cvMutex
                                        putStrLn "Hello mother"
                                        mutexRelease cvMutex
     putStrLn "Hello children"
     sleep 1
     conditionBroadcast cv
     ignore $ for ts $ \t => threadWait t
     sleep 1


text:
module TreeQ

%default total
%access public export

||| A tree structure for combining queries, perhaps slightly less expressive
||| than a free monad, but easier to prove total, etc. I say less expressive,
||| because I do not believe it is a monad, whereas my applicative instance
||| seems pretty solid. Moreover, it has a nice monoid instance, given a monoid
||| on the type it is parameterized over (but requiring no effort from the query
||| GADT). I have also provided a generalized semigroup operation based on
||| pairing items together. However, regrettable, it does not seem to be
||| foldable, since some of it's data is based on a future promise and isn't
||| available yet. This means it is not traversable. However, I think this may
||| be okay: ultimately the point of traversing is to push the query to the
||| outside until we're ready to run it, so the traverse instances of list,
||| maybe and either should serve us well enough, since we just barely make the
||| minimum requirement (applicative) to play ball with them.
data QryTree : (Type -> Type) -> Type -> Type where
  ||| Pure for monad/applicative: lift a plain value into the tree
  PureLeaf : a -> QryTree q a
  ||| Lift a query into the tree
  LiftLeaf : q i -> (i -> a) -> QryTree q a
  ||| Gives us a monoid operation
  Branch : QryTree q a -> QryTree q b -> ((a, b) -> c) -> QryTree q c

liftQ : q a -> QryTree q a
liftQ qry = LiftLeaf qry id

infixr 5 ^+^

||| Generalized semigroup operation
(^+^) : QryTree q a -> QryTree q b -> QryTree q (a, b)
q ^+^ r = Branch q r id

Semigroup a => Semigroup (QryTree q a) where
  q <+> r = Branch q r (uncurry (<+>))

Monoid a => Monoid (QryTree q a) where
  neutral = PureLeaf neutral

Functor q => Functor (QryTree q) where
  map f (PureLeaf x) = PureLeaf (f x)
  map f (LiftLeaf q handle) = LiftLeaf q (f . handle)
  map f (Branch q r handle) = Branch q r (f . handle)

-- A foldable instance does not seem possible. You could start easily enough:
-- Foldable (QryTree q) where
--   foldr func init (PureLeaf x) = func x init
-- But where would you go from there?
--   foldr func init (LiftLeaf x f) = ?foldable_moldable_2
--   foldr func init (Branch x y f) = ?foldable_moldable_3
-- The data you have promised right now is stuck in the future...

||| The s combinator, with a dash of uncurrying
s' : (a -> (b -> c)) -> (d -> b) -> (a, d) -> c
s' f g (x, y) = f x (g y)

||| I am not any good at equality proofs in Idris. However, I am not content to
||| rest uncertain about whether this applicative instance is lawful! So here
||| you go: back to geometry class: a long-hand proof, in the comments!
|||
||| identity: pure id <*> v = v
|||   PureLeaf id <*> v = v
|||   | PureLeaf id <*> PureLeaf x = v
|||     -> PureLeaf (id x) = v
|||     -> PureLeaf x = v
|||     -> v = v
|||     -> QED
|||   | PureLeaf id <*> LiftLeaf q g = v
|||     -> LiftLeaf q (id . g) = v
|||     -> LiftLeaf q g = v
|||     -> v = v
|||     -> QED
|||   | PureLeaf id <*> Branch q r g = v
|||     -> Branch q r (id . g) = v
|||     -> Branch q r g = v
|||     -> v = v
|||     -> QED
|||   -> QED
|||
||| composition: pure (.) <*> u <*> v <*> w = u <*> (v <*> w)
|||   PureLeaf (.) <*> u <*> v <*> w = u <*> (v <*> w)
|||   PureLeaf (\f g x => f (g x)) <*> u <*> v <*> w = u <*> (v <*> w)
|||   | PureLeaf (.) <*> PureLeaf u' <*> v <*> w = PureLeaf u' <*> (v <*> w)
|||     | PureLeaf (u' .) <*> PureLeaf v' <*> w = PureLeaf u' <*> (PureLeaf v' <*> w)
|||       -> PureLeaf (u' . v') <*> w = PureLeaf u' <*> (PureLeaf v' <*> w)
|||          | PureLeaf (\x => u' (v' x)) <*> PureLeaf w' = PureLeaf u' <*> (PureLeaf v' <*> PureLeaf w')
|||            -> PureLeaf (u' (v' w')) = PureLeaf u' <*> PureLeaf (v' w')
|||            -> PureLeaf (u' (v' w')) = PureLeaf (u' (v' w'))
|||            -> QED
|||          | PureLeaf (u' . v') <*> LiftLeaf q w' = PureLeaf u' <*> (PureLeaf v' <*> LiftLeaf q w')
|||            -> LiftLeaf q ((u' . v') . w') = PureLeaf u' <*> (LiftLeaf q (v' . w'))
|||            -> LiftLeaf q (u' . (v' . w')) = LiftLeaf q (u' . (v' . w'))
|||            -> QED
|||          | PureLeaf (u' . v') <*> Branch q r w' = PureLeaf u' <*> (PureLeaf v' <*> Branch q r w')
|||            -> Branch q r ((u' . v') . w') = PureLeaf u' <*> (Branch q r (v' . w'))
|||            -> Branch q r (u' . (v' . w')) = Branch q r (u' . (v' . w'))
|||            -> QED
|||       -> QED
|||     | PureLeaf (u' .) <*> LiftLeaf q v' <*> w = PureLeaf u' <*> (LiftLeaf q v' <*> w)
|||       -> LiftLeaf q ((u' .) . v') <*> w = PureLeaf u' <*> (LiftLeaf q v' <*> w)
|||       -> LiftLeaf q ((\g x => u' (g x)) . v') <*> w = PureLeaf u' <*> (LiftLeaf q v' <*> w)
|||       -> LiftLeaf q (\y => (\g x => u' (g x)) (v' y)) <*> w = PureLeaf u' <*> (LiftLeaf q v' <*> w)
|||       -> LiftLeaf q (\y x => u' (v' y x)) <*> w = PureLeaf u' <*> (LiftLeaf q v' <*> w)
|||          | LiftLeaf q (\y x => u' (v' y x)) <*> PureLeaf w' = PureLeaf u' <*> (LiftLeaf q v' <*> PureLeaf w')
|||            -> LiftLeaf q (\z => (\y x => u' (v' y x)) z w') = PureLeaf u' <*> (LiftLeaf q (\y => v' y w'))
|||            -> LiftLeaf q (\z => (\x => u' (v' z x)) w') = LiftLeaf q (\z => u' ((\y => v' y w') z))
|||            -> LiftLeaf q (\z => u' (v' z w')) = LiftLeaf q (\z => u' (v' z w'))
|||            -> QED
|||          | LiftLeaf q (\y x => u' (v' y x)) <*> LiftLeaf r w' = PureLeaf u' <*> (LiftLeaf q v' <*> LiftLeaf r w')
|||            -> Brand (LiftLeaf q id) (LiftLeaf r id) (s' (\y x => u' (v' y x)) w') = PureLeaf u' <*> (Branch (LiftLeaf q id) (LiftLeaf r id) (s' v' w'))
|||            -> Brand (LiftLeaf q id) (LiftLeaf r id)  (\(a, b) => (\y x => u' (v' y x)) a (w' b)) = Branch (LiftLeaf q id) (LiftLeaf r id)  (u' . s' v' w')
|||            -> ... (\(a, b) => (\x => u' (v' a x)) (w' b)) = ... (u' . s' v' w')
|||            -> ... (\(a, b) => u' (v' a (w' b))) = ... (u' . s' v' w')
|||            -> ... (\(a, b) => u' (s' v' w' (a, b))) = ... (u' . s' v' w')
|||            -> ... (\(a, b) => (u' . s' v' w') (a, b)) = ... (u' . s' v' w')
|||            -> ... (u' . s' v' w') = ... (u' . s' v' w')
|||            -> QED
|||          | LiftLeaf q (\y x => u' (v' y x)) <*> Branch r s w' = PureLeaf u' <*> (LiftLeaf q v' <*> Branch r s w')
|||            -> Brand (LiftLeaf q id) (Breanch r s id) (s' (\y x => u' (v' y x)) w') = PureLeaf u' <*> (Branch (LiftLeaf q id) (Breanch r s id) (s' v' w'))
|||            -> Brand (LiftLeaf q id) (Breanch r s id)  (\(a, b) => (\y x => u' (v' y x)) a (w' b)) = Branch (LiftLeaf q id) (Breanch r s id)  (u' . s' v' w')
|||            -> ... (\(a, b) => (\x => u' (v' a x)) (w' b)) = ... (u' . s' v' w')
|||            -> ... (\(a, b) => u' (v' a (w' b))) = ... (u' . s' v' w')
|||            -> ... (\(a, b) => u' (s' v' w' (a, b))) = ... (u' . s' v' w')
|||            -> ... (\(a, b) => (u' . s' v' w') (a, b)) = ... (u' . s' v' w')
|||            -> ... (u' . s' v' w') = ... (u' . s' v' w')
|||            -> QED
|||       -> QED
||| Suddenly I do the math and realized that I'm only 2/9th's done... perhaps
||| there is a better way to approach this than doing it late at night. The
||| results so far are very promising in that it seems that the same laborious
||| technique should continue to work. Perhaps this could be reduced more easily
||| by introducing some lemmas. Or by figuring out how to do it with Idris. Or
||| by researching if it has been done before. Or one could argue this way: we
||| have at this point really encountered all the scenarios. Things work right
||| if pure comes before, or after; it cancels out. LiftLeaf and Branch
||| fundamentally have the same semanticcs, and the proof above regarding the
||| semantics of the S-combinator seem conclusive for all cases involving them.
||| It seems that for a proof of this length, it is foolhardy to continue
||| without computer assistance and checking. My sense that this is not a bogus
||| implementation of applicative is quite high at this point. I leave it as an
||| exercise for the reader to complete, where by "the reader" I mean "me, I
||| hope, at some later date."
|||
||| homomorphism: pure f <*> pure x = pure (f x)
|||   PureLeaf f <*> PureLeaf x = PureLeaf (f x)
|||   -> QED
|||
||| interchange: u <*> pure y = pure ($ y) <*> u
|||   u <*> PureLeaf y = PureLeaf ($ y) <*> u
|||   | PureLeaf f <*> PureLeaf y = PureLeaf ($ y) <*> PureLeaf f
|||     -> PureLeaf (f y) = PureLeaf (f $ y)
|||     -> PureLeaf (f y) = PureLeaf (f y)
|||     -> QED
|||   | LiftLeaf q f <*> PureLeaf y = PureLeaf ($ y) <*> LiftLeaf q f
|||     -> LiftLeaf q f <*> PureLeaf y = PureLeaf ($ y) <*> LiftLeaf q f
|||     -> LiftLeaf q (\z => f z y) = LiftLeaf q ((\x => \g => g x) y . f)
|||     -> LiftLeaf q (\z => f z y) = LiftLeaf q ((\g => g y) . f)
|||     -> LiftLeaf q (\z => f z y) = LiftLeaf q (\z => (\g => g y) (f z))
|||     -> LiftLeaf q (\z => f z y) = LiftLeaf q (\z => f z y)
|||     -> QED
|||   | Branch q r f <*> PureLeaf y = PureLeaf ($ y) <*> Branch q r f
|||     -> Branch q r f <*> PureLeaf y = PureLeaf ($ y) <*> Branch q r f
|||     -> Branch q r (\z => f z y) = Branch q r ((\x => \g => g x) y . f)
|||     -> Branch q r (\z => f z y) = Branch q r ((\g => g y) . f)
|||     -> Branch q r (\z => f z y) = Branch q r (\z => (\g => g y) (f z))
|||     -> Branch q r (\z => f z y) = Branch q r (\z => f z y)
|||     -> QED
|||   -> QED
|||
||| These are the four properties I found needful to prove based on my
||| understanding of Haskell's Control.Applicative documentation.
Functor q => Applicative (QryTree q) where
  pure = PureLeaf
  (PureLeaf f) <*> (PureLeaf x) =
    PureLeaf (f x)
  (PureLeaf f) <*> (LiftLeaf q g) =
    LiftLeaf q (f . g)
  (PureLeaf f) <*> (Branch q r g) =
    Branch q r (f . g)
  (LiftLeaf q f) <*> (PureLeaf x) =
    LiftLeaf q (\y => f y x)
  (LiftLeaf q f) <*> (LiftLeaf r g) =
    Branch (LiftLeaf q id) (LiftLeaf r id) $ s' f g
  (LiftLeaf q f) <*> (Branch r s g) =
    Branch (LiftLeaf q id) (Branch r s id) $ s' f g
  (Branch q r f) <*> (PureLeaf x) =
    Branch q r (\y => f y x)
  (Branch q r f) <*> (LiftLeaf s g) =
    Branch (Branch q r id) (LiftLeaf s id) $ s' f g
  (Branch q r f) <*> (Branch s t g) =
    Branch (Branch q r id) (Branch s t id) $ s' f g

-- How would you implement a monad?
-- Functor q => Monad (QryTree q) where
-- The first case would be easy:
--   (PureLeaf x) >>= f = f x
-- However, wouldn't you get stuck on these?
--   (LiftLeaf x g) >>= f = ?monads_yikes_2
--   (Branch x y g) >>= f = ?monads_yikes_3
-- It seems that we have insufficient power to smash down the results, since we
-- cannot actually produce the tree from f in these cases, without introducing
-- another lambda abstraction: but if we do that, we have to wrap it in a tree:
-- but then, inside the lambda abstraction, we cannot destroy the tree that we
-- got out of the f; I take this as a proof that there is no monad instance.

||| Example specific query GADT
data FSQry : Type -> Type where
  LsFiles : String -> FSQry (List String)
  ReadText : String -> FSQry String
  DirExists : String -> FSQry Bool

||| Example accompanying commands, to in conjunction with the FSQry, form a sort
||| of little filesystem DSL.
data FSCmd
  = WriteLines String (List String)
  | CreateDir String
  | DeleteFile String
  | DeleteDir String

lsFiles : String -> QryTree FSQry (List String)
lsFiles = liftQ . LsFiles

readText : String -> QryTree FSQry String
readText  = liftQ . ReadText

consolidate' : String -> String -> List String -> List String -> List FSCmd
consolidate' from to files texts =
  map DeleteFile files
  ++ [ DeleteDir from
     , CreateDir to
     , WriteLines (to ++ "/" ++ "consolidated.txt") texts
     ]

-- Very sadly, it here appears that our type has insufficient power.
--consolidate : String -> String -> QryTree FSQry (List FSCmd)
consolidate from to = ?tragedy
--  (\files => consolidate' from to files <$> traverse readText files)
--  <*> lsFiles from


text:
module ClientTest

import Network.HTTP
import Network.HTTP.URL
import Utils.String
import System.File
import System.File.Mode
import Data.Nat
import Control.Monad.Error.Either
import Control.Monad.Error.Interface

%hide Data.String.Nil

||| `fputc` in C
%foreign "C:fputc,libc"
export
prim__fputc : Int -> FilePtr -> PrimIO Int

||| `fputc` with higher level primitives in idris2
export
fputc : HasIO io => Bits8 -> File -> io (Either FileError ())
fputc b (FHandle ptr) = do
  let c = cast b
  c' <- primIO $ prim__fputc c ptr
  pure $ if c' == c then Right () else Left FileWriteError

||| Write to a `File` from a `Stream`
export
toFile : HasIO m => File -> Stream (Of Bits8) m r -> m (Either FileError r)
toFile file = fold (pure . Right) join $ \(a :> b) => do
  Right () <- fputc a file
    | Left err => pure (Left err)
  b

with_client : {e : _} -> IO (HttpClient e) -> (HttpClient e -> EitherT (HttpError e) IO a) -> EitherT (HttpError e) IO a
with_client client f = MkEitherT $ do
  c <- client
  Right ok <- runEitherT (f c)
  | Left err => close c *> pure (Left err)
  close c
  pure (Right ok)

map_error : Functor m => (e -> e') -> EitherT e m a -> EitherT e' m a
map_error f = bimapEitherT f id

export
test_redirect : EitherT String IO ()
test_redirect = map_error show $ with_client {e=()} new_client_default $ \client => do
  putStrLn "sending request"
  (response, content) <- request client GET (url' "http://openbsd.org/70.html") [] ()
  putStrLn "response header received"
  printLn response
  putStrLn "downloading response"
  content <- toList_ content
  printLn $ "\{show $ length content} bytes read"

export
test_cookie : EitherT String IO ()
test_cookie = map_error show $ with_client {e=()} (new_client certificate_ignore_check 25 5 True False) $ \client => do
  putStrLn "sending cookie set request"
  (response, content) <- request client GET (url' "https://httpbin.org/cookies/set/sessioncookie/123456789") [] ()
  putStrLn "response header received"
  printLn response
  content <- toList_ content
  printLn $ utf8_pack $ content

  putStrLn "sending cookie get request"
  (response, content) <- request client GET (url' "https://httpbin.org/cookies") [] ()
  putStrLn "response header received"
  printLn response
  content <- toList_ content
  printLn $ utf8_pack $ content

export
test_post : EitherT String IO ()
test_post = map_error show $ with_client {e=()} new_client_default $ \client => do
  putStrLn "sending cookie set request"
  let body = "this is the body"
  (response, content) <- request client POST (url' "https://httpbin.org/post") [] body
  putStrLn "response header received"
  printLn response
  content <- toList_ content
  printLn $ utf8_pack $ content

export
test_close_without_read : EitherT String IO ()
test_close_without_read = map_error show $ with_client {e=()} new_client_default $ \client => do
  putStrLn "sending request"
  (response, content) <- request client GET (url' "http://openbsd.org/70.html") [] ()
  putStrLn "response header received"
  printLn response

export
test_json_gzip : EitherT String IO ()
test_json_gzip = map_error show $ with_client {e=()} new_client_default $ \client => do
  putStrLn "sending request"
  (response, content) <- request client GET (url' "https://httpbin.org/gzip") [] ()
  putStrLn "response header received"
  printLn response
  content <- toList_ content
  putStrLn $ maybe "Nothing" id $ utf8_pack $ content
  close client

export
test_json_deflate : EitherT String IO ()
test_json_deflate = map_error show $ with_client {e=()} new_client_default $ \client => do
  putStrLn "sending request"
  (response, content) <- request client GET (url' "https://httpbin.org/deflate") [] ()
  putStrLn "response header received"
  printLn response
  content <- toList_ content
  putStrLn $ maybe "Nothing" id $ utf8_pack $ content
  close client


text:
module Pythag

import Data.Strings

%default total

pythag : Int -> List (Int, Int, Int)
pythag n = [(x, y, z) | z <- [1..n], y <- [1..z], x <- [1..y], x * x + y * y == z * z]

readNum : HasIO io => io (Maybe Int)
readNum = do ns <- getLine
             case all isDigit (unpack ns) of
                  False => pure Nothing
                  True => pure $ Just (cast ns)

main : HasIO io => io ()
main = do Just n <- readNum
            | Nothing => do putStrLn "Error: you should have entered a number!"
                            pure ()
          let res = pythag n
          printLn res

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Nat

public export
data Nat = Z | S Nat

public export
plus : Nat -> Nat -> Nat
plus Z y = y
plus (S k) y = S (plus k y)