text:
module Equiv

import Expr
import Imp
import Logic
import Maps

%access public export

%default total

AEquiv : (a1, a2 : AExp) -> Type
AEquiv a1 a2 = (st : State) -> aeval st a1 = aeval st a2

BEquiv : (b1, b2 : BExp) -> Type
BEquiv b1 b2 = (st : State) -> beval st b1 = beval st b2

AEquiv_example : AEquiv (X - X) 0
AEquiv_example st with (st X)
  AEquiv_example st | Z = Refl
  AEquiv_example st | S k = sym $ minusZeroN k

BEquiv_example : BEquiv (X - X == 0) BTrue
BEquiv_example st with (st X)
  BEquiv_example st | Z = Refl
  BEquiv_example st | S k = rewrite sym $ minusZeroN k in Refl

btrue_is_true : BEquiv BTrue BTrue
btrue_is_true _ = Refl

bfalse_is_false : BEquiv BFalse BFalse
bfalse_is_false _ = Refl

bnot_btrue_is_bfalse : BEquiv (BNot BTrue) BFalse
bnot_btrue_is_bfalse _ = Refl

bnot_bfalse_is_btrue : BEquiv (BNot BFalse) BTrue
bnot_bfalse_is_btrue _ = Refl

CEquiv : (c1, c2 : Com) -> Type
CEquiv c1 c2 = (st, st' : State) -> ((c1 / st \\ st') ↔ (c2 / st \\ st'))

skip_left : CEquiv (do SKIP; c) c
skip_left st st' = (forward, backward)
where forward : ((do SKIP; c) / st \\ st') -> (c / st \\ st')
      forward (E_Seq E_Skip rel) = rel
      backward : (c / st \\ st') -> ((do SKIP; c) / st \\ st')
      backward rel = E_Seq E_Skip rel

skip_right : CEquiv (do c; SKIP) c
skip_right st st' = (forward, backward)
where forward : ((do c; SKIP) / st \\ st') -> (c / st \\ st')
      forward (E_Seq rel E_Skip) = rel
      backward : (c / st \\ st') -> ((do c; SKIP) / st \\ st')
      backward rel = E_Seq rel E_Skip

test_true_simple : CEquiv (IFB BTrue THEN c1 ELSE c2 FI) c1
test_true_simple st st' = (forward, backward)
where forward : ((IFB BTrue THEN c1 ELSE c2 FI) / st \\ st') ->
                (c1 / st \\ st')
      forward (E_IfTrue _ rel) = rel
      forward (E_IfFalse prf _) = absurd prf
      backward : (c1 / st \\ st') ->
                 ((IFB BTrue THEN c1 ELSE c2 FI) / st \\ st')
      backward rel = E_IfTrue Refl rel

test_true : BEquiv b BTrue -> CEquiv (IFB b THEN c1 ELSE c2 FI) c1
test_true {b} btrue st st' = (forward, backward)
where forward : ((IFB b THEN c1 ELSE c2 FI) / st \\ st') ->
                (c1 / st \\ st')
      forward (E_IfTrue _ rel) = rel
      forward (E_IfFalse prf _) = absurd $ trans (sym $ btrue st) prf
      backward : (c1 / st \\ st') ->
                 ((IFB b THEN c1 ELSE c2 FI) / st \\ st')
      backward rel = E_IfTrue (btrue st) rel

test_false : BEquiv b BFalse -> CEquiv (IFB b THEN c1 ELSE c2 FI) c2
test_false {b} bfalse st st' = (forward, backward)
where forward : ((IFB b THEN c1 ELSE c2 FI) / st \\ st') ->
                (c2 / st \\ st')
      forward (E_IfTrue prf _) = absurd $ trans (sym $ bfalse st) prf
      forward (E_IfFalse _ rel) = rel
      backward : (c2 / st \\ st') ->
                 ((IFB b THEN c1 ELSE c2 FI) / st \\ st')
      backward rel = E_IfFalse (bfalse st) rel

swap_if_branches : CEquiv (IFB b THEN c1 ELSE c2 FI)
                          (IFB not b THEN c2 ELSE c1 FI)
swap_if_branches {b} st st' = (forward, backward)
where forward : ((IFB b THEN c1 ELSE c2 FI) / st \\ st') ->
                ((IFB BNot b THEN c2 ELSE c1 FI) / st \\ st')
      forward (E_IfTrue prf rel) = E_IfFalse (cong {f=not} prf) rel
      forward (E_IfFalse prf rel) = E_IfTrue (cong {f=not} prf) rel
      backward : ((IFB BNot b THEN c2 ELSE c1 FI) / st \\ st') ->
                 ((IFB b THEN c1 ELSE c2 FI) / st \\ st')
      backward (E_IfTrue prf rel) =
        E_IfFalse (trans (sym $ notInvolutive (beval st b))
                         (cong {f=not} prf))
                  rel
      backward (E_IfFalse prf rel) =
        E_IfTrue (trans (sym $ notInvolutive (beval st b))
                        (cong {f=not} prf))
                 rel

if1_if_equiv : CEquiv (CIf1 b c) (CIf b c SKIP)
if1_if_equiv {b} {c} st st' = (forward, backward)
where forward : CEval (CIf1 b c) st st' -> CEval (CIf b c SKIP) st st'
      forward rel = case rel of
        E_If1True prf cc => E_IfTrue prf cc
        E_If1False prf => E_IfFalse prf E_Skip
      backward : CEval (CIf b c SKIP) st st' -> CEval (CIf1 b c) st st'
      backward rel = case rel of
        E_IfTrue prf cct => E_If1True prf cct
        E_IfFalse prf E_Skip => E_If1False prf

if1_true : BEquiv b BTrue -> CEquiv (CIf1 b c) c
if1_true {b} btrue st st' = (forward, backward)
where forward : CEval (CIf1 b c) st st' -> CEval c st st'
      forward rel = case rel of
        E_If1True _ cc => cc
        E_If1False prf => absurd $ trans (sym prf) (btrue st)
      backward : CEval c st st' -> CEval (CIf1 b c) st st'
      backward cc = E_If1True (btrue st) cc

if1_false : BEquiv b BFalse -> CEquiv (CIf1 b c) SKIP
if1_false {b} bfalse st st' = (forward, backward)
where forward : CEval (CIf1 b c) st st' -> CEval SKIP st st'
      forward rel = case rel of
        E_If1True prf _ => absurd $ trans (sym prf) (bfalse st)
        E_If1False _ => E_Skip
      backward : CEval SKIP st st' -> CEval (CIf1 b c) st st'
      backward rel = case rel of
        E_Skip => E_If1False (bfalse st)

while_false : BEquiv b BFalse -> CEquiv (WHILE b c) SKIP
while_false {b} bfalse st _ = (forward, backward)
where forward : ((WHILE b c) / st \\ st') -> (SKIP / st \\ st')
      forward rel = case rel of
        E_WhileEnd _ => E_Skip
        E_WhileLoop prf _ _ => absurd $ trans (sym $ bfalse st) prf
      backward : (SKIP / st \\ st') -> ((WHILE b c) / st \\ st')
      backward rel = case rel of
        E_Skip => E_WhileEnd (bfalse st)

while_true_nonterm : BEquiv b BTrue -> Not ((WHILE b c) / st \\ st')
while_true_nonterm {st'} btrue (E_WhileEnd prf) =
  absurd $ trans (sym $ btrue st') prf
while_true_nonterm btrue (E_WhileLoop prf rel next) =
  while_true_nonterm btrue next

while_true : BEquiv b BTrue -> CEquiv (WHILE b c) (WHILE BTrue SKIP)
while_true {b} btrue st st' = (forward, backward)
where forward : ((WHILE b c) / st \\ st') -> ((WHILE BTrue SKIP) / st \\ st')
      forward rel = case rel of
        E_WhileEnd prf => absurd $ trans (sym $ btrue st) prf
        E_WhileLoop _ _ next => void $ while_true_nonterm btrue next
      backward : ((WHILE BTrue SKIP) / st \\ st') -> ((WHILE b c) / st \\ st')
      backward rel = case rel of
        E_WhileEnd prf => absurd prf
        E_WhileLoop Refl _ next => void $ while_true_nonterm btrue_is_true next

loop_unrolling : CEquiv (WHILE b c) (IFB b THEN (do c; WHILE b c) ELSE SKIP FI)
loop_unrolling st st' = (forward, backward)
where forward : ((WHILE b c) / st \\ st') ->
                ((IFB b THEN (do c; WHILE b c) ELSE SKIP FI) / st \\ st')
      forward rel = case rel of
        E_WhileEnd prf => E_IfFalse prf E_Skip
        E_WhileLoop prf rel next => E_IfTrue prf (E_Seq rel next)
      backward : ((IFB b THEN (do c; WHILE b c) ELSE SKIP FI) / st \\ st') ->
                 ((WHILE b c) / st \\ st')
      backward (E_IfTrue prf (E_Seq rel next)) = E_WhileLoop prf rel next
      backward (E_IfFalse prf rel) = case rel of
        E_Skip => E_WhileEnd prf

for_while_equiv : CEquiv (CFor c1 b c2 c3) (CSeq c1 (CWhile b (CSeq c3 c2)))
for_while_equiv {c1} {b} {c2} {c3} st st' = (forward, backward)
where forward : ((CFor c1 b c2 c3) / st \\ st') ->
                ((CSeq c1 (CWhile b (CSeq c3 c2))) / st \\ st')
      forward (E_For cinit cwhile) = E_Seq cinit cwhile
      backward : ((CSeq c1 (CWhile b (CSeq c3 c2))) / st \\ st') ->
                 ((CFor c1 b c2 c3) / st \\ st')
      backward (E_Seq cinit cwhile) = E_For cinit cwhile

repeat_while_equiv : CEquiv (CRepeat c b) (CSeq c (CWhile (not b) c))
repeat_while_equiv {c} {b} st st' = (forward, backward)
where forward : CEval (CRepeat c b) st st' ->
                CEval (CSeq c (CWhile (not b) c)) st st'
      forward (E_Repeat cc cwhile) = E_Seq cc cwhile
      backward : CEval (CSeq c (CWhile (not b) c)) st st' ->
                 CEval (CRepeat c b) st st'
      backward (E_Seq cc cwhile) = E_Repeat cc cwhile

seq_assoc : CEquiv (do (do c1; c2); c3) (do c1; (do c2; c3))
seq_assoc st st' = (forward, backward)
where forward : ((do (do c1; c2); c3) / st \\ st') ->
                ((do c1; (do c2; c3)) / st \\ st')
      forward (E_Seq (E_Seq r1 r2) r3) = E_Seq r1 (E_Seq r2 r3)
      backward : ((do c1; (do c2; c3)) / st \\ st') ->
                 ((do (do c1; c2); c3) / st \\ st')
      backward (E_Seq r1 (E_Seq r2 r3)) = E_Seq (E_Seq r1 r2) r3

identity_assignment : CEquiv (x ::= AId x) SKIP
identity_assignment {x} st st' = (forward, backward)
where forward : ((x ::= AId x) / st \\ st') -> (SKIP / st \\ st')
      forward rel = case rel of
        E_Ass prf => rewrite sym prf
                     in rewrite t_update_same {m=st} {x=x}
                     in E_Skip
      backward : (SKIP / st \\ st') -> ((x ::= AId x) / st \\ st')
      backward rel = case rel of
        E_Skip => replace (t_update_same {m=st} {x=x}) (E_Ass Refl)
                    {P=\s => (x ::= AId x) / st \\ s}

assign_aequiv : AEquiv (AId x) e -> CEquiv SKIP (x ::= e)
assign_aequiv {x} {e} x_eq_e st st' = (forward, backward)
where forward : (SKIP / st \\ st') -> ((x ::= e) / st \\ st')
      forward rel = case rel of
        E_Skip => replace (t_update_same {m=st} {x=x}) (E_Ass (sym $ x_eq_e st))
                    {P=\s => (x ::= e) / st \\ s}
      backward : ((x ::= e) / st \\ st') -> (SKIP / st \\ st')
      backward rel = case rel of
        E_Ass prf => rewrite sym prf
                     in rewrite sym $ x_eq_e st
                     in rewrite t_update_same {m=st} {x=x}
                     in E_Skip

prog_a : Com
prog_a =
  WHILE (not (X <= 0)) $
    X ::= X + 1

prog_b : Com
prog_b = do
  IFB X == 0
      THEN do X ::= X + 1
              Y ::= 1
      ELSE Y ::= 0
  FI
  X ::= X - Y
  Y ::= 0

prog_c : Com
prog_c = SKIP

prog_d : Com
prog_d =
  WHILE (not (X == 0)) $
    X ::= X * Y + 1

prog_e : Com
prog_e = Y ::= 0

prog_f : Com
prog_f = do
  Y ::= X + 1
  WHILE (not (X == Y)) $
    Y ::= X + 1

prog_g : Com
prog_g = WHILE BTrue SKIP

prog_h : Com
prog_h =
  WHILE (not (X == X)) $
    X ::= X + 1

prog_i : Com
prog_i =
  WHILE (not (X == Y)) $
    X ::= Y + 1

equiv_classes : List (List Com)
equiv_classes = [ [prog_a, prog_f, prog_g]
                , [prog_b]
                , [prog_c, prog_h]
                , [prog_d]
                , [prog_e]
                , [prog_i] ]

refl_aequiv : AEquiv a a
refl_aequiv _ = Refl

sym_aequiv : AEquiv a1 a2 -> AEquiv a2 a1
sym_aequiv a1_equiv_a2 st = sym $ a1_equiv_a2 st

trans_aequiv : AEquiv a1 a2 -> AEquiv a2 a3 -> AEquiv a1 a3
trans_aequiv a1_equiv_a2 a2_equiv_a3 st = rewrite a1_equiv_a2 st
                                          in a2_equiv_a3 st

refl_bequiv : BEquiv b b
refl_bequiv _ = Refl

sym_bequiv : BEquiv b1 b2 -> BEquiv b2 b1
sym_bequiv b1_equiv_b2 st = sym $ b1_equiv_b2 st

trans_bequiv : BEquiv b1 b2 -> BEquiv b2 b3 -> BEquiv b1 b3
trans_bequiv b1_equiv_b2 b2_equiv_b3 st = rewrite b1_equiv_b2 st
                                          in b2_equiv_b3 st

refl_cequiv : CEquiv c c
refl_cequiv _ _ = (id, id)

sym_cequiv : CEquiv c1 c2 -> CEquiv c2 c1
sym_cequiv c1_equiv_c2 st st' = swap $ c1_equiv_c2 st st'

trans_cequiv : CEquiv c1 c2 -> CEquiv c2 c3 -> CEquiv c1 c3
trans_cequiv c1_equiv_c2 c2_equiv_c3 st st' =
  let (forward_c1_c2, backward_c2_c1) = c1_equiv_c2 st st'
      (forward_c2_c3, backward_c3_c2) = c2_equiv_c3 st st'
  in (forward_c2_c3 . forward_c1_c2, backward_c2_c1 . backward_c3_c2)

cAss_congruence : AEquiv a1 a2 -> CEquiv (x ::= a1) (x ::= a2)
cAss_congruence {a1} {a2} a1_equiv_a2 st st' = (forward, backward)
where forward : ((x ::= a1) / st \\ st') -> ((x ::= a2) / st \\ st')
      forward rel = case rel of
        E_Ass prf => rewrite sym prf
                     in rewrite a1_equiv_a2 st
                     in E_Ass Refl
      backward : ((x ::= a2) / st \\ st') -> ((x ::= a1) / st \\ st')
      backward rel = case rel of
        E_Ass prf => rewrite sym prf
                     in rewrite sym $ a1_equiv_a2 st
                     in E_Ass Refl

cWhile_congruence : BEquiv b1 b2 -> CEquiv c1 c2 ->
                    CEquiv (WHILE b1 c1) (WHILE b2 c2)
cWhile_congruence {b1} {b2} {c1} {c2} b1_equiv_b2 c1_equiv_c2 _ _ =
  (forward, backward)
where forward : ((WHILE b1 c1) / st \\ st') -> ((WHILE b2 c2) / st \\ st')
      forward {st} rel = case rel of
        E_WhileEnd prf => E_WhileEnd $ trans (sym $ b1_equiv_b2 st) prf
        E_WhileLoop {st1} prf rel next =>
          E_WhileLoop (trans (sym $ b1_equiv_b2 st) prf)
                      (fst (c1_equiv_c2 st st1) rel)
                      (forward {st=st1} next)
      backward : ((WHILE b2 c2) / st \\ st') -> ((WHILE b1 c1) / st \\ st')
      backward {st} rel = case rel of
        E_WhileEnd prf => E_WhileEnd $ trans (b1_equiv_b2 st) prf
        E_WhileLoop {st1} prf rel next =>
          E_WhileLoop (trans (b1_equiv_b2 st) prf)
                      (snd (c1_equiv_c2 st st1) rel)
                      (backward {st=st1} next)

cSeq_congruence : CEquiv c1 c2 -> CEquiv c3 c4 -> CEquiv (do c1; c3) (do c2; c4)
cSeq_congruence {c1} {c2} {c3} {c4} c1_equiv_c2 c3_equiv_c4 st st' =
  (forward, backward)
where forward : ((do c1; c3) / st \\ st') -> ((do c2; c4) / st \\ st')
      forward (E_Seq {st2} r1 r2) = E_Seq (fst (c1_equiv_c2 st st2) r1)
                                          (fst (c3_equiv_c4 st2 st') r2)
      backward : ((do c2; c4) / st \\ st') -> ((do c1; c3) / st \\ st')
      backward (E_Seq {st2} r3 r4) = E_Seq (snd (c1_equiv_c2 st st2) r3)
                                           (snd (c3_equiv_c4 st2 st') r4)

for_false : BEquiv cond BFalse -> CEquiv (CFor init cond updt body) init
for_false {init} {cond} {updt} {body} cond_equiv =
  trans_cequiv (for_while_equiv {c1=init} {b=cond} {c2=updt} {c3=body})
               (trans_cequiv (cSeq_congruence (refl_cequiv {c=init})
                                              (while_false cond_equiv))
                             (skip_right {c=init}))

for_true : BEquiv cond BTrue -> CEquiv (CFor init cond updt body)
                                       (CSeq init (CWhile BTrue SKIP))
for_true {init} {cond} {updt} {body} cond_equiv =
  trans_cequiv (for_while_equiv {c1=init} {b=cond} {c2=updt} {c3=body})
               (cSeq_congruence (refl_cequiv {c=init}) (while_true cond_equiv))

cFor_congruence : CEquiv init1 init2 -> BEquiv cond1 cond2 ->
                  CEquiv updt1 updt2 -> CEquiv body1 body2 ->
                  CEquiv (CFor init1 cond1 updt1 body1)
                         (CFor init2 cond2 updt2 body2)
cFor_congruence init_equiv cond_equiv updt_equiv body_equiv =
  trans_cequiv for_while_equiv
               (trans_cequiv
                  (cSeq_congruence init_equiv
                                   (cWhile_congruence
                                      cond_equiv
                                      (cSeq_congruence body_equiv updt_equiv)))
                  (sym_cequiv for_while_equiv))

repeat_false : BEquiv b BFalse -> CEquiv (CRepeat c b)
                                         (CSeq c (CWhile BTrue SKIP))
repeat_false {b} {c} cond_equiv =
  let not_cond_equiv = \st1 => cong {f=not} (cond_equiv st1)
  in trans_cequiv repeat_while_equiv
                  (cSeq_congruence refl_cequiv (while_true not_cond_equiv))

repeat_true : BEquiv b BTrue -> CEquiv (CRepeat c b) c
repeat_true {b} {c} cond_equiv =
  let not_cond_equiv = \st1 => cong {f=not} (cond_equiv st1)
  in trans_cequiv repeat_while_equiv
                  (trans_cequiv (cSeq_congruence refl_cequiv
                                                 (while_false not_cond_equiv))
                                skip_right)

cRepeat_congruence : CEquiv body1 body2 -> BEquiv cond1 cond2 ->
                     CEquiv (CRepeat body1 cond1) (CRepeat body2 cond2)
cRepeat_congruence body_equiv cond_equiv =
  let not_cond_equiv = \st1 => cong {f=not} (cond_equiv st1)
  in trans_cequiv repeat_while_equiv
                  (trans_cequiv
                     (cSeq_congruence body_equiv
                                      (cWhile_congruence not_cond_equiv
                                                         body_equiv))
                     (sym_cequiv repeat_while_equiv))

cIf_congruence : BEquiv b1 b2 -> CEquiv c1 c2 -> CEquiv c3 c4 ->
                 CEquiv (IFB b1 THEN c1 ELSE c3 FI) (IFB b2 THEN c2 ELSE c4 FI)
cIf_congruence {b1} {b2} {c1} {c2} {c3} {c4}
               b1_equiv_b2 c1_equiv_c2 c3_equiv_c4 st st' =
  (forward, backward)
where forward : ((IFB b1 THEN c1 ELSE c3 FI) / st \\ st') ->
                ((IFB b2 THEN c2 ELSE c4 FI) / st \\ st')
      forward (E_IfTrue prf rel) = E_IfTrue (trans (sym $ b1_equiv_b2 st) prf)
                                            (fst (c1_equiv_c2 st st') rel)
      forward (E_IfFalse prf rel) = E_IfFalse (trans (sym $ b1_equiv_b2 st) prf)
                                              (fst (c3_equiv_c4 st st') rel)
      backward : ((IFB b2 THEN c2 ELSE c4 FI) / st \\ st') ->
                 ((IFB b1 THEN c1 ELSE c3 FI) / st \\ st')
      backward (E_IfTrue prf rel) = E_IfTrue (trans (b1_equiv_b2 st) prf)
                                             (snd (c1_equiv_c2 st st') rel)
      backward (E_IfFalse prf rel) = E_IfFalse (trans (b1_equiv_b2 st) prf)
                                               (snd (c3_equiv_c4 st st') rel)

cIf1_congruence : BEquiv b1 b2 -> CEquiv c1 c2 ->
                  CEquiv (CIf1 b1 c1) (CIf1 b2 c2)
cIf1_congruence b_equiv c_equiv =
  trans_cequiv
    (trans_cequiv if1_if_equiv
                  (cIf_congruence b_equiv c_equiv (refl_cequiv {c=SKIP})))
    (sym_cequiv if1_if_equiv)

congruence_example : CEquiv
  (do X ::= 0
      IFB X == 0
          THEN Y ::= 0
          ELSE Y ::= 42
      FI)
  (do X ::= 0
      IFB X == 0
          THEN Y ::= X - X
          ELSE Y ::= 42
      FI)
congruence_example =
  cSeq_congruence refl_cequiv
                  (cIf_congruence refl_bequiv statements_equiv refl_cequiv)
where forward : ((Y ::= 0) / st \\ st') ->
                ((Y ::= X - X) / st \\ st')
      forward {st} (E_Ass prf) = E_Ass $ trans (sym $ minusZeroN (st X)) prf
      backward : ((Y ::= X - X) / st \\ st') ->
                 ((Y ::= 0) / st \\ st')
      backward {st} (E_Ass prf) = rewrite minusZeroN (st X)
                                  in rewrite prf
                                  in E_Ass Refl
      statements_equiv : CEquiv (Y ::= 0) (Y ::= X - X)
      statements_equiv _ _ = (forward, backward)

ATransSound : (atrans : AExp -> AExp) -> Type
ATransSound atrans = (a : AExp) -> AEquiv a (atrans a)

BTransSound : (btrans : BExp -> BExp) -> Type
BTransSound btrans = (b : BExp) -> BEquiv b (btrans b)

CTransSound : (ctrans : Com -> Com) -> Type
CTransSound ctrans = (c : Com) -> CEquiv c (ctrans c)


text:
module VDOM.VDOM

import HTML.Types
import HTML.Elements

%access public export
%include JavaScript "vdom.js"

jscall : (fname : String) -> (ty : Type) ->
          {auto fty : FTy FFI_JS [] ty} -> ty
jscall fname ty = foreign FFI_JS fname ty

makeJSList : List Ptr -> JS_IO Ptr
makeJSList [] = jscall "[]" (() -> JS_IO Ptr) ()
makeJSList (x::xs) =
  do
    res <- makeJSList xs
    jscall "%0.unshift(%1)" (Ptr -> Ptr -> JS_IO ()) res x
    pure res

makeJSObj : List (String, Ptr) -> JS_IO Ptr
makeJSObj [] =
  jscall "{}" (() -> JS_IO Ptr) ()
makeJSObj ((k,v)::xs) =
  do
    o <- makeJSObj xs
    jscall "%0[%1]=%2" (Ptr -> String -> Ptr -> JS_IO ()) o k v
    pure o

mkAtt : Ptr -> Attr -> JS_IO Ptr
mkAtt obj (MkAttr name value) =
    jscall "window.pamperscript.makeAttr(%0, %1, %2)"
        (Ptr -> String -> String -> JS_IO Ptr)
        obj name value

attrsToPtr : List Attr -> JS_IO Ptr
attrsToPtr attrs = do
    obj <- makeJSObj []
    foldlM mkAtt obj attrs

htmlToJs : HTMLElement -> JS_IO Ptr
htmlToJs (MkHTMLTextNode (MkTextNode s)) =
    jscall "window.pamperscript.makeElement('text', null, null, %0)" (String -> JS_IO Ptr) s
htmlToJs (MkHTMLElement (MkElement type omitTag attrs children)) = do
    jsAttrs <- attrsToPtr attrs
    children' <- traverse htmlToJs children
    jsChildren <- makeJSList children'
    jscall "window.pamperscript.makeElement(%0, %1, %2)" (String -> Ptr -> Ptr -> JS_IO Ptr) (show type) jsAttrs jsChildren

ext: idr

max_stars_repo_name: ebenpack/pamperscript

max_issues_repo_name: ebenpack/pamperscript

max_forks_repo_name: ebenpack/pamperscript


text:
import NewEden.Natural
import NewEden.NaturalTheorems
import NewEden.Implementations.GMP

import Prelude

-- some purely abstract numbers

x : Natural p
x = 20129384192384912830491283948120384129348293841923842985102985230948509485923485023948529304859342805298309124982395810293410293

y : Natural p
y = 1023944127934827938571928453485912384029341029348029582039452034951028349023845938451829341829340192384019250192830192580192840

-- we can reason about them, even in their abstract state

z : Natural p
z = x * y

-- and we can use them with respect to some implementation!

render : Natural GMP -> Natural GMP
render n = n + z

main : IO ()
main = do
  putStrLn "Give me a natural number (a big one. come on.)"
  n' <- getLine
  let n = prim__fromStrBigInt n'
  case show n == n' of
    True => do
      putStrLn "Nice! Here's your number n added to our purely abstract (no defined implementation!), internal constants:"
      putStrLn $ show $ value $ render $ fromInteger n
    False => do
      putStrLn "You sure that's a natural number?"
      main

max_stars_repo_name: identicalsnowflake/neweden

max_issues_repo_name: identicalsnowflake/neweden

max_forks_repo_name: identicalsnowflake/neweden


text:
module NonZeroInt

%access public export
%default total
%auto_implicits off

record NonZeroInt where
  constructor MkNonZeroInt
  num : Int
  nonZero : Not (num = 0)

postulate
zeroProductProperty : (a, b : Int) -> a * b = 0 -> Either (a = 0) (b = 0)

productOfNonZeroIsNonZero : NonZeroInt -> NonZeroInt -> NonZeroInt
productOfNonZeroIsNonZero (MkNonZeroInt num1 nonZero1) (MkNonZeroInt num2 nonZero2) = MkNonZeroInt (num1 * num2) prf
  where
    prf = \prodIsZero => case zeroProductProperty num1 num2 prodIsZero of
      Left  aIsZero => nonZero1 aIsZero
      Right bIsZero => nonZero2 bIsZero

max_stars_repo_name: marcosh/idris-rationals

max_issues_repo_name: marcosh/idris-rationals

max_forks_repo_name: marcosh/idris-rationals


text:
module Minecraft.Core.Entity.Pickup

import Minecraft.Core
import public Minecraft.Data.Type.As

%default total

public export
interface Entity e => Pickup (e : Type) where
  collect : e -> Inf (As Item)

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
> module LinCombHeadtailsEq

> import Data.Matrix.LinearCombinations
> import Data.Matrix.ZZModuleSpan

> import Control.Algebra
> import Control.Algebra.VectorSpace -- definition of module
> import Classes.Verified -- definition of verified algebras other than modules
> import Data.Matrix
> import Data.Matrix.Algebraic -- module instances; from Idris 0.9.20

> import Data.ZZ

# Contents
* Introduction
* vecSingletonReplicateEq
* reduceMultUnderHeadTo1D
* rewriteZipWithUnderTail
* References

# Introduction

Suppose we have

< vecHeadtailsEq : {xs,ys : Vect _ _} -> ( headeq : x = y ) -> ( taileq : xs = ys ) -> x::xs = y::ys

Then we can replace efforts in proofs with this expression.

These are proofs of equality of two Vects expressed in (x::xs) form, mainly inductive proofs:

< vecSingletonReplicateEq : ((u : a) -> v=u) -> (xs : Vect n a) -> (xs = replicate n v)

< reduceMultUnderHeadTo1D : {xxs : Matrix n (S m) ZZ} -> map Data.Vect.head (zipWith (<#>) (vv::vvs) (xx::xxs)) = zipWith (the (ZZ -> ZZ -> ZZ) (*)) (vv::vvs) (map Data.Vect.head (xx::xxs))
< reduceMultUnderHeadTo1D_triv
< reduceMultUnderHeadTo1D'

< rewriteZipWithUnderTail : {scals : Vect n ZZ} -> {vects : Matrix n (S predw) ZZ} -> map Data.Vect.tail $ Data.Vect.zipWith (<#>) scals vects = Data.Vect.zipWith (<#>) scals (map Data.Vect.tail vects)
< rewriteZipWithUnderTail'

# vecSingletonReplicateEq

Out of these, `vecSingletonReplicateEq` is the simplest to analyze the replacement.

Let us write

> vecSingletonReplicateEq_2 : ((u : a) -> v=u) -> (xs : Vect n a) -> (xs = replicate n v)
> vecSingletonReplicateEq_2 f [] = Refl
> vecSingletonReplicateEq_2 f (x::xs) = vecHeadtailsEq (sym $ f x) (vecSingletonReplicateEq_2 f xs)

this improves the clarity of

< vecSingletonReplicateEq : ((u : a) -> v=u) -> (xs : Vect n a) -> (xs = replicate n v)
< vecSingletonReplicateEq f [] = Refl
< vecSingletonReplicateEq f (x::xs) {v} = rewrite sym (f x) in cong {f=(v::)} (vecSingletonReplicateEq f xs)

# reduceMultUnderHeadTo1D

The ones in `reduceMultUnderHeadTo1D` are most aggregious. Let us write

> reduceMultUnderHeadTo1D_2 : {xxs : Matrix n (S m) ZZ} -> map Data.Vect.head (zipWith (<#>) (vv::vvs) (xx::xxs)) = zipWith (the (ZZ -> ZZ -> ZZ) (*)) (vv::vvs) (map Data.Vect.head (xx::xxs))
> reduceMultUnderHeadTo1D_2 {n=Z} {xxs=[]} {vvs=[]} = vecHeadtailsEq headMapChariz Refl
> reduceMultUnderHeadTo1D_2 {n=S predn} {xxs=xxx::xxxs} {vvs=vvv::vvvs} = vecHeadtailsEq headMapChariz reduceMultUnderHeadTo1D_2
>

Note the greater improvement of the proof for the case {n=Z} by pattern matching on the variables `xxs` and `vvs` rather than applying `zeroVecEq` to prove they're both [].

Further, the corresponding finer-grained pattern matching in the longer-tailed cases eliminates the need for the second `vecHeadtailsEq` argument to be given by the proof

< mapheads_eq_zipwith = proof
<   intros
<   rewrite sym $ headtails vvs
<   rewrite sym $ headtails xxs
<   exact reduceMultUnderHeadTo1D_2 {vv=head vvs} {vvs=tail vvs} {xx=head xxs} {xxs=tail xxs}

as in

< reduceMultUnderHeadTo1D_2 {n=S predn} {vv} {xx} = vecHeadtailsEq headMapChariz ?mapheads_eq_zipwith

The original, however, is comparatively illegible

< reduceMultUnderHeadTo1D : {xxs : Matrix n (S m) ZZ} -> map Data.Vect.head (zipWith (<#>) (vv::vvs) (xx::xxs)) = zipWith (the (ZZ -> ZZ -> ZZ) (*)) (vv::vvs) (map Data.Vect.head (xx::xxs))
< reduceMultUnderHeadTo1D {n=Z} {vv} {xx} = ?reduceMultUnderHeadTo1D_triv
< reduceMultUnderHeadTo1D {n=S predn} {vv} {xx} = ?reduceMultUnderHeadTo1D'
<
< reduceMultUnderHeadTo1D_triv = proof
<   intros
<   rewrite sym (the (xxs = []) zeroVecEq)
<   rewrite sym (the (vvs = []) zeroVecEq)
<   compute
<   exact cong {f=(::[])} _
<   exact headMapChariz {xs=xx}
<
< reduceMultUnderHeadTo1D' = proof
<   intros
<   -- Not required in the REPL: {f=multZ vv}
<   exact trans (cong {f=(::(map head $ zipWith (<#>) vvs xxs))} $ headMapChariz {f=multZ vv} {xs=xx}) _
<   compute
<   exact cong {f=(::) (multZ vv (head xx))} _
<   rewrite sym $ headtails vvs
<   rewrite sym $ headtails xxs
<   exact reduceMultUnderHeadTo1D {vv=head vvs} {vvs=tail vvs} {xx=head xxs} {xxs=tail xxs}

# rewriteZipWithUnderTail

Finally, `rewriteZipWithUnderTail` plays a full mind game with Idris to discuss one of these problems. We may write

> rewriteZipWithUnderTail_2 : {scals : Vect n ZZ} -> {vects : Matrix n (S predw) ZZ} -> map Data.Vect.tail $ Data.Vect.zipWith (<#>) scals vects = Data.Vect.zipWith (<#>) scals (map Data.Vect.tail vects)
> rewriteZipWithUnderTail_2 {scals=[]} {vects=[]} = Refl
> rewriteZipWithUnderTail_2 {scals=z::zs} {vects=v::vs} = vecHeadtailsEq (rewrite sym $ sym $ headtails v in Refl) rewriteZipWithUnderTail_2

whereas originally we had to write

< rewriteZipWithUnderTail {scals=z::zs} {vects=v::vs} = ?rewriteZipWithUnderTail'
<
< rewriteZipWithUnderTail' = proof
<   intros
<   let headv = map (z <.>) (tail v)
<   exact trans _ (cong {f=(headv::)} $ rewriteZipWithUnderTail {scals=zs} {vects=vs})
<   claim headeq tail (map (z<.>) v) = headv
<   compute -- reduce the headv in the proposition to its value for prepping substitution
<   unfocus
<   rewrite sym headeq
<   compute -- apply the (\x => headv::x) from the earlier cong
<   exact Refl
<   rewrite sym $ headtails v
<   exact Refl

# References

* Idris 0.9.20 src: /test/regex007/A.lidr

Notes

* Idris 0.9.20 src: /samples/misc/reflection.idr
* modules.rst

ext: lidr


text:
module Main

main : IO ()
main = putStrLn (?convert 'x')

max_stars_repo_name: jeremy-miller/type-driven-development

max_issues_repo_name: jeremy-miller/type-driven-development

max_forks_repo_name: jeremy-miller/type-driven-development


text:
countFrom : Integer -> List Integer
countFrom n = n :: countFrom (n + 1)

partial
labelWith : List Integer -> List a -> List (Integer, a)
labelWith lbls [] = []
labelWith (lbl :: lbls) (val :: vals) = (lbl, val) :: labelWith lbls vals


text:
module lib.sublib.Sublibrary

export
salutation : String
salutation = "Hello"


text:
= Basics

**REMINDER**:

             #####################################################
             ###  PLEASE DO NOT DISTRIBUTE SOLUTIONS PUBLICLY  ###
             #####################################################

                           (See the Preface for why.)

> ||| Basics: Functional Programming in Idris
> module Basics
>
> %access public export
>

\idr{postulate} is Idris's "escape hatch" that says accept this definition
without proof. Instead of using it to mark the holes, similar to Coq's
\mintinline[]{Coq}{Admitted}, we use Idris's holes directly. In practice, holes
(and \idr{postulate}) are useful when you're incrementally developing large
proofs.

== Introduction

The functional programming style brings programming closer to simple, everyday
mathematics: If a procedure or method has no side effects, then (ignoring
efficiency) all we need to understand about it is how it maps inputs to outputs
-- that is, we can think of it as just a concrete method for computing a
mathematical function. This is one sense of the word "functional" in "functional
programming." The direct connection between programs and simple mathematical
objects supports both formal correctness proofs and sound informal reasoning
about program behavior.

The other sense in which functional programming is "functional" is that it
emphasizes the use of functions (or methods) as \gls{first-class} values --
i.e., values that can be passed as arguments to other functions, returned as
results, included in data structures, etc. The recognition that functions can be
treated as data in this way enables a host of useful and powerful idioms.

Other common features of functional languages include \glspl{algebraic data
type} and \gls{pattern matching}, which make it easy to construct and manipulate
rich data structures, and sophisticated \glspl{polymorphic type system}
supporting abstraction and code reuse. Idris shares all of these features.

The first half of this chapter introduces the most essential elements of Idris's
functional programming language. The second half introduces some basic
\glspl{tactic} that can be used to prove simple properties of Idris programs.

== Enumerated Types

One unusual aspect of Idris, similar to Coq, is that its set of built-in
features (see the \idr{base} package in the Idris distribution) is _extremely_
small. For example, instead of providing the usual palette of atomic data types
(booleans, integers, strings, etc.), Idris offers a powerful mechanism for
defining new data types from scratch, from which all these familiar types arise
as instances.

Naturally, the Idris distribution comes with extensive standard libraries
providing definitions of booleans, numbers, and many common data structures like
lists and hash tables (see the \idr{prelude} and \idr{contrib} packages), as
well as the means to write type-safe effectful code (see the \idr{effects}
package) and \idr{pruvlioj}, a toolkit for proof automation and program
construction. But there is nothing magic or primitive about these library
definitions. To illustrate this, we will explicitly recapitulate all the
definitions we need in this course, rather than just getting them implicitly
from the library.

To see how this definition mechanism works, let's start with a very simple
example.

=== Days of the Week

The following declaration tells Idris that we are defining a new set of data
values -- a \gls{type}.

> namespace Days
>
>   ||| Days of the week.
>   data Day = ||| `Monday` is a `Day`.
>              Monday
>            | ||| `Tuesday` is a `Day`.
>              Tuesday
>            | ||| `Wednesday` is a `Day`.
>              Wednesday
>            | ||| `Thursday` is a `Day`.
>              Thursday
>            | ||| `Friday` is a `Day`.
>              Friday
>            | ||| `Saturday` is a `Day`.
>              Saturday
>            | ||| `Sunday` is a `Day`.
>              Sunday
>

The type is called \idr{Day}, and its members are \idr{Monday}, \idr{Tuesday},
etc. The right hand side of the definition can be read "\idr{Monday} is a
\idr{Day}, \idr{Tuesday} is a \idr{Day}, etc."

Using the \idr{%name} directive, we can tell Idris how to choose default
variable names for a particular \gls{type}.

>   %name Day day, day1, day2
>

Now, if Idris needs to choose a name for a variable of type \idr{Day}, it will
choose \idr{day} by default, followed by \idr{day1} and \idr{day2} if any of its
predecessors are already in scope.

Having defined \idr{Day}, we can write functions that operate on days.

Type the following:

```idris
  nextWeekday : Day -> Day
```

Then with the point on \idr{nextWeekday}, call \gls{idris-add-clause}.

```idris
  nextWeekday : Day -> Day
  nextWeekday day = ?nextWeekday_rhs
```

With the point on \idr{day}, call \gls{idris-case-split}.

```idris
  nextWeekday : Day -> Day
  nextWeekday Monday = ?nextWeekday_rhs_1
  nextWeekday Tuesday = ?nextWeekday_rhs_2
  nextWeekday Wednesday = ?nextWeekday_rhs_3
  nextWeekday Thursday = ?nextWeekday_rhs_4
  nextWeekday Friday = ?nextWeekday_rhs_5
  nextWeekday Saturday = ?nextWeekday_rhs_6
  nextWeekday Sunday = ?nextWeekday_rhs_7
```

Fill in the proper \idr{Day} constructors and align whitespace as you like.

>   ||| Determine the next weekday after a day.
>   nextWeekday : Day -> Day
>   nextWeekday Monday    = Tuesday
>   nextWeekday Tuesday   = Wednesday
>   nextWeekday Wednesday = Thursday
>   nextWeekday Thursday  = Friday
>   nextWeekday Friday    = Monday
>   nextWeekday Saturday  = Monday
>   nextWeekday Sunday    = Monday
>

Call \gls{idris-load-file} to load the \idr{Basics} module with the finished
\idr{nextWeekday} definition.

Having defined a function, we should check that it works on some examples. There
are actually three different ways to do this in Idris.

First, we can evaluate an expression involving \idr{nextWeekday} in a REPL.

```idris
λΠ> nextWeekday Friday
Monday : Day
```

```idris
λΠ> nextWeekday (nextWeekday Saturday)
Tuesday : Day
```

\todo[inline]{Mention other editors? Discuss idris-mode?}

We show Idris's responses in comments, but, if you have a computer handy, this
would be an excellent moment to fire up the Idris interpreter under your
favorite Idris-friendly text editor -- such as Emacs or Vim -- and try this for
and try this for yourself. Load this file, `Basics.lidr` from the book's
accompanying Idris sources, find the above example, submit it to the Idris REPL,
and observe the result.

Second, we can record what we _expect_ the result to be in the form of a proof.

>   ||| The second weekday after `Saturday` is `Tuesday`.
>   testNextWeekday :
>     (nextWeekday (nextWeekday Saturday)) = Tuesday

This declaration does two things: it makes an assertion (that the second weekday
after \idr{Saturday} is \idr{Tuesday}) and it gives the assertion a name that
can be used to refer to it later.

Having made the assertion, we can also ask Idris to verify it, like this:

>   testNextWeekday = Refl
>

\todo[inline]{Edit this}

The details are not important for now (we'll come back to them in a bit), but
essentially this can be read as "The assertion we've just made can be proved by
observing that both sides of the equality evaluate to the same thing, after some
simplification."

(For simple proofs like this, you can call \gls{idris-add-clause} with the point
on the name (\idr{testNextWeekday}) in the type signature and then call
\gls{idris-proof-search} with the point on the resultant hole to have Idris
solve the proof for you.)

\todo[inline]{Verify the "main uses" claim.}

Third, we can ask Idris to _generate_, from our definition, a program in some
other, more conventional, programming (C, JavaScript and Node are bundled with
Idris) with a high-performance compiler. This facility is very interesting,
since it gives us a way to construct \gls{fully certified} programs in
mainstream languages. Indeed, this is one of the main uses for which Idris was
developed. We'll come back to this topic in later chapters.

== Booleans

> namespace Booleans
>

In a similar way, we can define the standard type \idr{Bool} of booleans, with
members \idr{False} and \idr{True}.

```idris
  ||| Boolean Data Type
  data Bool = True | False
```

This definition is written in the simplified style, similar to \idr{Day}. It can
also be written in the verbose style:

```idris
  data Bool : Type where
       True : Bool
      False : Bool
```

The verbose style is more powerful because it allows us to assign precise
types to individual constructors. This will become very useful later on.

Although we are rolling our own booleans here for the sake of building up
everything from scratch, Idris does, of course, provide a default implementation
of the booleans in its standard library, together with a multitude of useful
functions and lemmas. (Take a look at \idr{Prelude} in the Idris library
documentation if you're interested.) Whenever possible, we'll name our own
definitions and theorems so that they exactly coincide with the ones in the
standard library.

Functions over booleans can be defined in the same way as above:

```idris
  not : (b : Bool) -> Bool
  not True  = False
  not False = True
```

>   andb : (b1 : Bool) -> (b2 : Bool) -> Bool
>   andb True  b2 = b2
>   andb False b2 = False
>
>   orb : (b1 : Bool) -> (b2 : Bool) -> Bool
>   orb True  b2 = True
>   orb False b2 = b2
>

The last two illustrate Idris's syntax for multi-argument function definitions.
The corresponding multi-argument application syntax is illustrated by the
following four "unit tests," which constitute a complete specification -- a
truth table -- for the \idr{orb} function:

>   testOrb1 : (orb True  False) = True
>   testOrb1 = Refl
>
>   testOrb2 : (orb False False) = False
>   testOrb2 = Refl
>
>   testOrb3 : (orb False True)  = True
>   testOrb3 = Refl
>
>   testOrb4 : (orb True  True)  = True
>   testOrb4 = Refl
>

\todo[inline]{Edit this.}

We can also introduce some familiar syntax for the boolean operations we have
just defined. The \idr{syntax} command defines a new symbolic notation for an
existing definition, and \idr{infixl} specifies left-associative fixity.

```idris
  infixl 4 &&, ||

  (&&) : Bool -> Bool -> Bool
  (&&) = andb

  (||) : Bool -> Bool -> Bool
  (||) = orb
```

>   testOrb5 : False || False || True = True
>   testOrb5 = Refl
>

==== Exercise: 1 star (nandb)

Fill in the hole \idr{?nandb_rhs} and complete the following function; then make
sure that the assertions below can each be verified by Idris. (Fill in each of
the holes, following the model of the \idr{orb} tests above.) The function
should return \idr{True} if either or both of its inputs are \idr{False}.

>   nandb : (b1 : Bool) -> (b2 : Bool) -> Bool
>   nandb b1 b2 = ?nandb_rhs
>
>   test_nandb1 : (nandb True  False) = True
>   test_nandb1 = ?test_nandb1_rhs
>
>   test_nandb2 : (nandb False False) = True
>   test_nandb2 = ?test_nandb2_rhs
>
>   test_nandb3 : (nandb False True)  = True
>   test_nandb3 = ?test_nandb3_rhs
>
>   test_nandb4 : (nandb True  True)  = False
>   test_nandb4 = ?test_nandb4_rhs
>

$\square$

==== Exercise: 1 star (andb3)

Do the same for the \idr{andb3} function below. This function should return
\idr{True} when all of its inputs are \idr{True}, and \idr{False} otherwise.

>   andb3 : (b1 : Bool) -> (b2 : Bool) -> (b3 : Bool) -> Bool
>   andb3 b1 b2 b3 = ?andb3_rhs
>
>   test_andb31 : (andb3 True  True  True)  = True
>   test_andb31 = ?test_andb31_rhs
>
>   test_andb32 : (andb3 False True  True)  = False
>   test_andb32 = ?test_andb32_rhs
>
>   test_andb33 : (andb3 True  False True)  = False
>   test_andb33 = ?test_andb33_rhs
>
>   test_andb34 : (andb3 True  True  False) = False
>   test_andb34 = ?test_andb34_rhs
>

$\square$

== Function Types

Every expression in Idris has a type, describing what sort of thing it computes.
The \idr{:type} (or \idr{:t}) REPL command asks Idris to print the type of an
expression.

For example, the type of \idr{not True} is \idr{Bool}.

```idris
λΠ> :type True
True : Bool
λΠ> :t not True
not True : Bool
```

\todo[inline]{Confirm the "function types" wording.}

Functions like \idr{not} itself are also data values, just like \idr{True} and
\idr{False}. Their types are called \glspl{function type}, and they are written
with arrows.

```idris
λΠ> :t not
not : Bool -> Bool
```

The type of \idr{not}, written \idr{Bool -> Bool} and pronounced "\idr{Bool}
arrow \idr{Bool}," can be read, "Given an input of type \idr{Bool}, this
function produces an output of type \idr{Bool}." Similarly, the type of
\idr{andb}, written \idr{Bool -> Bool -> Bool}, can be read, "Given two inputs,
both of type \idr{Bool}, this function produces an output of type \idr{Bool}."

== Modules

\todo[inline]{Flesh this out and discuss namespaces}

Idris provides a \gls{module system}, to aid in organizing large developments.

== Numbers

> namespace Numbers
>

The types we have defined so far are examples of "enumerated types": their
definitions explicitly enumerate a finite set of elements. A More interesting
way of defining a type is to give a collection of \glspl{inductive rule}
describing its elements. For example, we can define the natural numbers as
follows:

```idris
  data Nat : Type where
         Z : Nat
         S : Nat -> Nat
```

The clauses of this definition can be read:

- \idr{Z} is a natural number.
- \idr{S} is a "constructor" that takes a natural number and yields another one
  -- that is, if \idr{n} is a natural number, then \idr{S n} is too.

Let's look at this in a little more detail.

Every inductively defined set (\idr{Day}, \idr{Nat}, \idr{Bool}, etc.) is
actually a set of \glspl{expression}. The definition of \idr{Nat} says how
expressions in the set \idr{Nat} can be constructed:

- the expression \idr{Z} belongs to the set \idr{Nat};
- if \idr{n} is an expression belonging to the set \idr{Nat}, then \idr{S n} is
  also an expression belonging to the set \idr{Nat}; and
- expression formed in these two ways are the only ones belonging to the set
  \idr{Nat}.

The same rules apply for our definitions of \idr{Day} and \idr{Bool}. The
annotations we used for their constructors are analogous to the one for the
\idr{Z} constructor, indicating that they don't take any arguments.

These three conditions are the precise force of inductive declarations. They
imply that the expression \idr{Z}, the expression \idr{S Z}, the expression
\idr{S (S Z)}, the expression \idr{S (S (S Z))} and so on all belong to the set
\idr{Nat}, while other expressions like \idr{True}, \idr{andb True False}, and
\idr{S (S False)} do not.

We can write simple functions that pattern match on natural numbers just as we
did above -- for example, the predecessor function:

>   pred : (n : Nat) -> Nat
>   pred  Z    = Z
>   pred (S k) = k
>

The second branch can be read: "if \idr{n} has the form \idr{S k} for some
\idr{k}, then return \idr{k}."

>   minusTwo : (n : Nat) -> Nat
>   minusTwo  Z        = Z
>   minusTwo (S  Z)    = Z
>   minusTwo (S (S k)) = k
>

Because natural numbers are such a pervasive form of data, Idris provides a tiny
bit of built-in magic for parsing and printing them: ordinary Arabic numerals
can be used as an alternative to the "unary" notation defined by the
constructors \idr{S} and \idr{Z}. Idris prints numbers in Arabic form by
default:

```idris
λΠ> S (S (S (S Z)))
4 : Nat
λΠ> minusTwo 4
2 : Nat
```

The constructor \idr{S} has the type \idr{Nat -> Nat}, just like the functions
\idr{minusTwo} and \idr{pred}:

```idris
λΠ> :t S
λΠ> :t pred
λΠ> :t minusTwo
```

These are all things that can be applied to a number to yield a number. However,
there is a fundamental difference between the first one and the other two:
functions like \idr{pred} and \idr{minusTwo} come with \glspl{computation rule}
-- e.g., the definition of \idr{pred} says that \idr{pred 2} can be simplified
to \idr{1} -- while the definition of \idr{S} has no such behavior attached.
Although it is like a function in the sense that it can be applied to an
argument, it does not _do_ anything at all!

For most function definitions over numbers, just pattern matching is not enough:
we also need recursion. For example, to check that a number \idr{n} is even, we
may need to recursively check whether \idr{n-2} is even.

>   ||| Determine whether a number is even.
>   ||| @n a number
>   evenb : (n : Nat) -> Bool
>   evenb  Z        = True
>   evenb (S  Z)    = False
>   evenb (S (S k)) = evenb k
>

We can define \idr{oddb} by a similar recursive declaration, but here is a
simpler definition that is a bit easier to work with:

>   ||| Determine whether a number is odd.
>   ||| @n a number
>   oddb : (n : Nat) -> Bool
>   oddb n = not (evenb n)
>
>   testOddb1 : oddb 1 = True
>   testOddb1 = Refl
>
>   testOddb2 : oddb 4 = False
>   testOddb2 = Refl
>

Naturally, we can also define multi-argument functions by recursion.

> namespace Playground2
>
>   plus : (n : Nat) -> (m : Nat) -> Nat
>   plus  Z    m = m
>   plus (S k) m = S (Playground2.plus k m)
>

Adding three to two now gives us five, as we'd expect.

```idris
λΠ> plus 3 2
```

The simplification that Idris performs to reach this conclusion can be
visualized as follows:

\idr{plus (S (S (S Z))) (S (S Z))}

$\hookrightarrow$ \idr{S (plus (S (S Z)) (S (S Z)))}
                    by the second clause of \idr{plus}

$\hookrightarrow$ \idr{S (S (plus (S Z) (S (S Z))))}
                    by the second clause of \idr{plus}

$\hookrightarrow$ \idr{S (S (S (plus Z (S (S Z)))))}
                    by the second clause of \idr{plus}

$\hookrightarrow$ \idr{S (S (S (S (S Z))))}
                    by the first clause of \idr{plus}

As a notational convenience, if two or more arguments have the same type, they
can be written together. In the following definition, \idr{(n, m : Nat)} means
just the same as if we had written \idr{(n : Nat) -> (m : Nat)}.

```idris
  mult : (n, m : Nat) -> Nat
  mult  Z    = Z
  mult (S k) = plus m (mult k m)
```

>   testMult1 : (mult 3 3) = 9
>   testMult1 = Refl
>

You can match two expressions at once:

```idris
  minus : (n, m : Nat) -> Nat
  minus  Z     _    = Z
  minus  n     Z    = n
  minus (S k) (S j) = minus k j
```

\todo[inline]{Verify this.}

The \idr{_} in the first line is a \gls{wildcard pattern}. Writing \idr{_} in a
pattern is the same as writing some variable that doesn't get used on the
right-hand side. This avoids the need to invent a bogus variable name.

>   exp : (base, power : Nat) -> Nat
>   exp base  Z    = S Z
>   exp base (S p) = mult base (exp base p)
>

==== Exercise: 1 star (factorial)

Recall the standard mathematical factorial function:

\[
    factorial(n)=
\begin{cases}
    1,                      & \text{if } n = 0 \\
    n \times factorial(n-1),& \text{otherwise}
\end{cases}
\]

Translate this into Idris.

>   factorial : (n : Nat) -> Nat
>   factorial n = ?factorial_rhs
>
>   testFactorial1 : factorial 3 = 6
>   testFactorial1 = ?testFactorial1_rhs
>
>   testFactorial2 : factorial 5 = mult 10 12
>   testFactorial2 = ?testFactorial2_rhs
>

$\square$

We can make numerical expressions a little easier to read and write by
introducing \gls{syntax} for addition, multiplication, and subtraction.

```idris
  syntax [x] "+" [y] = plus  x y
  syntax [x] "-" [y] = minus x y
  syntax [x] "*" [y] = mult  x y
```

```idris
λΠ> :t (0 + 1) + 1
```

(The details are not important, but interested readers can refer to the optional
"More on Syntax" section at the end of this chapter.)

Note that these do not change the definitions we've already made: they are
simply instructions to the Idris parser to accept \idr{x + y} in place of
\idr{plus x y} and, conversely, to the Idris pretty-printer to display \idr{plus
x y} as \idr{x + y}.

\todo[inline]{Mention interfaces here? Say this is infix}

The \idr{(==)} function tests \idr{Nat}ural numbers for equality, yielding a
\idr{Bool}ean.

```idris
  ||| Test natural numbers for equality.
  (==) : (n, m : Nat) -> Bool
  (==)  Z     Z    = True
  (==)  Z    (S j) = False
  (==) (S k)  Z    = False
  (==) (S k) (S j) = (==) k j
```

The \idr{lte} function tests whether its first argument is less than or equal to
its second argument, yielding a boolean.

```idris
||| Test whether a number is less than or equal to another.
lte : (n, m : Nat) -> Bool
lte  Z     m    = True
lte  n     Z    = False
lte (S k) (S j) = lte k j
```

>   testLte1 : lte 2 2 = True
>   testLte1 = Refl
>
>   testLte2 : lte 2 4 = True
>   testLte2 = Refl
>
>   testLte3 : lte 4 2 = False
>   testLte3 = Refl
>

==== Exercise: 1 star (blt_nat)

The \idr{blt_nat} function tests \idr{Nat}ural numbers for
\idr{l}ess-\idr{t}han, yielding a \idr{b}oolean. Instead of making up a new
recursive function for this one, define it in terms of a previously defined
function.

>   blt_nat : (n, m : Nat) -> Bool
>   blt_nat n m = ?blt_nat_rhs
>
>   test_blt_nat_1 : blt_nat 2 2 = False
>   test_blt_nat_1 = ?test_blt_nat_1_rhs
>
>   test_blt_nat_2 : blt_nat 2 4 = True
>   test_blt_nat_2 = ?test_blt_nat_2_rhs
>
>   test_blt_nat_3 : blt_nat 4 2 = False
>   test_blt_nat_3 = ?test_blt_nat_3_rhs
>

$\square$

== Proof by Simplification

Now that we've defined a few datatypes and functions, let's turn to stating and
proving properties of their behavior. Actually, we've already started doing
this: each of the functions beginning with \idr{test} in the previous sections
makes a precise claim about the behavior of some function on some particular
inputs. The proofs of these claims were always the same: use \idr{Refl} to check
that both sides contain identical values.

The same sort of "proof by simplification" can be used to prove more interesting
properties as well. For example, the fact that \idr{0} is a "neutral element"
for \idr{+} on the left can be proved just by observing that \idr{0 + n} reduces
to \idr{n} no matter what \idr{n} is, a fact that can be read directly off the
definition of \idr{plus}.

>   plus_Z_n : (n : Nat) -> 0 + n = n
>   plus_Z_n n = Refl
>

It will be useful later to know that [reflexivity] does some simplification --
for example, it tries "unfolding" defined terms, replacing them with their
right-hand sides. The reason for this is that, if reflexivity succeeds, the
whole goal is finished and we don't need to look at whatever expanded
expressions \idr{Refl} has created by all this simplification and unfolding.

Other similar theorems can be proved with the same pattern.

>   plus_1_l : (n : Nat) -> 1 + n = S n
>   plus_1_l n = Refl
>
>   mult_0_l : (n : Nat) -> 0 * n = 0
>   mult_0_l n = Refl
>

The \idr{_l} suffix in the names of these theorems is pronounced "on the left."

Although simplification is powerful enough to prove some fairly general facts,
there are many statements that cannot be handled by simplification alone. For
instance, we cannot use it to prove that \idr{0} is also a neutral element for
\idr{+} _on the right_.

```idris
plus_n_Z : (n : Nat) -> n = n + 0
plus_n_Z n = Refl
```

```
When checking right hand side of plus_n_Z with expected type
             n = n + 0

     Type mismatch between
             plus n 0 = plus n 0 (Type of Refl)
     and
             n = plus n 0 (Expected type)

     Specifically:
             Type mismatch between
                     plus n 0
             and
                     n
```

(Can you explain why this happens?)

The next chapter will introduce \gls{induction}, a powerful technique that can
be used for proving this goal. For the moment, though, let's look at a few more
simple tactics.

== Proof by Rewriting

This theorem is a bit more interesting than the others we've seen:

>   plus_id_example : (n, m : Nat) -> (n = m) -> n + n = m + m

Instead of making a universal claim about all numbers \idr{n} and \idr{m}, it
talks about a more specialized property that only holds when \idr{n = m}. The
arrow symbol is pronounced "implies."

As before, we need to be able to reason by assuming the existence of some
numbers \idr{n} and \idr{m}. We also need to assume the hypothesis \idr{n = m}.

\todo[inline]{Edit, mention the "generate initial pattern match" editor command}

The \idr{intros} tactic will serve to move all three of these from the goal into
assumptions in the current context.

Since \idr{n} and \idr{m} are arbitrary numbers, we can't just use
simplification to prove this theorem. Instead, we prove it by observing that, if
we are assuming \idr{n = m}, then we can replace \idr{n} with \idr{m} in the
goal statement and obtain an equality with the same expression on both sides.
The tactic that tells Idris to perform this replacement is called \idr{rewrite}.

>   plus_id_example n m prf = rewrite prf in Refl
>

The first two variables on the left side move the universally quantified
variables \idr{n} and \idr{m} into the context. The third moves the hypothesis
\idr{n = m} into the context and gives it the name \idr{prf}. The right side
tells Idris to rewrite the current goal (\idr{n + n = m + m}) by replacing the
left side of the equality hypothesis \idr{prf} with the right side.

==== Exercise: 1 star (plus_id_exercise)

Fill in the proof.

>   plus_id_exercise : (n, m, o : Nat) -> (n = m) -> (m = o) -> n + m = m + o
>   plus_id_exercise n m o prf prf1 = ?plus_id_exercise_rhs
>

$\square$

The prefix \idr{?} on the right-hand side of an equation tells Idris that we
want to skip trying to prove this theorem and just leave a hole. This can be
useful for developing longer proofs, since we can state subsidiary lemmas that
we believe will be useful for making some larger argument, use holes to delay
defining them for the moment, and continue working on the main argument until we
are sure it makes sense; then we can go back and fill in the proofs we skipped.

\todo[inline]{Decide whether to discuss \idr{postulate}.}

>   -- Be careful, though: every time you say `postulate` you are leaving a door
>   -- open for total nonsense to enter Idris's nice, rigorous, formally checked
>   -- world!

We can also use the \idr{rewrite} tactic with a previously proved theorem
instead of a hypothesis from the context. If the statement of the previously
proved theorem involves quantified variables, as in the example below, Idris
tries to instantiate them by matching with the current goal.

>   mult_0_plus : (n, m : Nat) -> (0 + n) * m = n * (0 + m)
>   mult_0_plus n m = Refl
>

Unlike in Coq, we don't need to perform such a rewrite for \idr{mult_0_plus} in
Idris and can just use \idr{Refl} instead.

==== Exercise: 2 starts (mult_S_1)

>   mult_S_1 : (n, m : Nat) -> (m = S n) -> m * (1 + n) = m * m
>   mult_S_1 n m prf = ?mult_S_1_rhs
>

$\square$

== Proof by Case Analysis

Of course, not everything can be proved by simple calculation and rewriting: In
general, unknown, hypothetical values (arbitrary numbers, booleans, lists, etc.)
can block simplification. For example, if we try to prove the following fact
using the \idr{Refl} tactic as above, we get stuck.

```idris
plus_1_neq_0_firsttry : (n : Nat) -> (n + 1) == 0 = False
plus_1_neq_0_firsttry n = Refl -- does nothing!
```

The reason for this is that the definitions of both \idr{(==)} and \idr{+}
begin by performing a \idr{match} on their first argument. But here, the first
argument to \idr{+} is the unknown number \idr{n} and the argument to
\idr{(==)} is the compound expression \idr{n + 1}; neither can be simplified.

To make progress, we need to consider the possible forms of \idr{n} separately.
If \idr{n} is \idr{Z}, then we can calculate the final result of \idr{(n + 1) ==
0} and check that it is, indeed, \idr{False}. And if \idr{n = S k} for some
\idr{k}, then, although we don't know exactly what number \idr{n + 1} yields, we
can calculate that, at least, it will begin with one \idr{S}, and this is enough
to calculate that, again, \idr{(n + 1) == 0} will yield \idr{False}.

To tell Idris to consider, separately, the cases where \idr{n = Z} and where
\idr{n = S k}, simply case split on \idr{n}.

\todo[inline]{Mention case splitting interactively in Emacs, Atom, etc.}

>   plus_1_neq_0 : (n : Nat) -> (n + 1) == 0 = False
>   plus_1_neq_0  Z    = Refl
>   plus_1_neq_0 (S k) = Refl
>

Case splitting on \idr{n} generates _two_ holes, which we must then prove,
separately, in order to get Idris to accept the theorem.

In this example, each of the holes is easily filled by a single use of
\idr{Refl}, which itself performs some simplification -- e.g., the first one
simplifies \idr{(S k + 1) == 0} to \idr{False} by first rewriting \idr{(S k +
1)} to \idr{S (k + 1)}, then unfolding \idr{(==)}, simplifying its pattern
matching.

There are no hard and fast rules for how proofs should be formatted in Idris.
However, if the places where multiple holes are generated are lifted to lemmas,
then the proof will be readable almost no matter what choices are made about
other aspects of layout.

This is also a good place to mention one other piece of somewhat obvious advice
about line lengths. Beginning Idris users sometimes tend to the extremes, either
writing each tactic on its own line or writing entire proofs on one line. Good
style lies somewhere in the middle. One reasonable convention is to limit
yourself to 80-character lines.

The case splitting strategy can be used with any inductively defined datatype.
For example, we use it next to prove that boolean negation is involutive --
i.e., that negation is its own inverse.

>   ||| A proof that boolean negation is involutive.
>   not_involutive : (b : Bool) -> not (not b) = b
>   not_involutive True  = Refl
>   not_involutive False = Refl
>

Note that the case splitting here doesn't introduce any variables because none
of the subcases of the patterns need to bind any, so there is no need to specify
any names.

It is sometimes useful to case split on more than one parameter, generating yet
more proof obligations. For example:

>   andb_commutative : (b, c : Bool) -> b && c = c && b
>   andb_commutative True  True  = Refl
>   andb_commutative True  False = Refl
>   andb_commutative False True  = Refl
>   andb_commutative False False = Refl
>

In more complex proofs, it is often better to lift subgoals to lemmas:

>   andb_commutative'_rhs_1 : (c : Bool) -> c = c && True
>   andb_commutative'_rhs_1 True  = Refl
>   andb_commutative'_rhs_1 False = Refl
>
>   andb_commutative'_rhs_2 : (c : Bool) -> False = c && False
>   andb_commutative'_rhs_2 True  = Refl
>   andb_commutative'_rhs_2 False = Refl
>
>   andb_commutative' : (b, c : Bool) -> b && c = c && b
>   andb_commutative' True  = andb_commutative'_rhs_1
>   andb_commutative' False = andb_commutative'_rhs_2
>

==== Exercise: 2 stars (andb_true_elim2)

Prove the following claim, lift cases (and subcases) to lemmas when case split.

>   andb_true_elim_2 : (b, c : Bool) -> (b && c = True) -> c = True
>   andb_true_elim_2 b c prf = ?andb_true_elim_2_rhs
>

$\square$

==== Exercise: 1 star (zero_nbeq_plus_1)

>   zero_nbeq_plus_1 : (n : Nat) -> 0 == (n + 1) = False
>   zero_nbeq_plus_1 n = ?zero_nbeq_plus_1_rhs
>

$\square$

\todo[inline]{Discuss associativity.}

== Structural Recursion (Optional)

Here is a copy of the definition of addition:

```idris
plus' : Nat -> Nat -> Nat
plus'  Z       right = right
plus' (S left) right = S (plus' left right)
```

When Idris checks this definition, it notes that \idr{plus'} is "decreasing on
1st argument." What this means is that we are performing a \gls{structural
recursion} over the argument \idr{left} -- i.e., that we make recursive calls
only on strictly smaller values of \idr{left}. This implies that all calls to
\idr{plus'} will eventually terminate. Idris demands that some argument of
_every_ recursive definition is "decreasing."

This requirement is a fundamental feature of Idris's design: In particular, it
guarantees that every function that can be defined in Idris will terminate on
all inputs. However, because Idris's "decreasing analysis" is not very
sophisticated, it is sometimes necessary to write functions in slightly
unnatural ways.

\todo[inline]{Verify the previous claims.}

\todo[inline]{Add decreasing exercise.}

== More Exercises

==== Exercise: 2 stars (boolean_functions)

Use the tactics you have learned so far to prove the following theorem about
boolean functions.

>   identity_fn_applied_twice : (f : Bool -> Bool) ->
>                               ((x : Bool) -> f x = x) ->
>                               (b : Bool) -> f (f b) = b
>   identity_fn_applied_twice f g b = ?identity_fn_applied_twice_rhs

Now state and prove a theorem \idr{negation_fn_applied_twice} similar to the
previous one but where the second hypothesis says that the function \idr{f} has
the property that \idr{f x = not x}.

>
>   -- FILL IN HERE
>

$\square$

==== Exercise: 2 start (andb_eq_orb)

Prove the following theorem. (You may want to first prove a subsidiary lemma or
two. Alternatively, remember that you do not have to introduce all hypotheses at
the same time.)

>   andb_eq_orb : (b, c : Bool) -> (b && c = b || c) -> b = c
>   andb_eq_orb b c prf = ?andb_eq_orb_rhs

$\square$

==== Exercise: 3 stars (binary)

Consider a different, more efficient representation of natural numbers using a
binary rather than unary system. That is, instead of saying that each natural
number is either zero or the successor of a natural number, we can say that each
binary number is either

- zero,
- twice a binary number, or
- one more than twice a binary number.

(a) First, write an inductive definition of the type \idr{Bin} corresponding to
    this description of binary numbers.

(Hint: Recall that the definition of \idr{Nat} from class,

```idris
data Nat : Type where
       Z : Nat
       S : Nat -> Nat
```

says nothing about what \idr{Z} and \idr{S} "mean." It just says "\idr{Z} is in
the set called \idr{Nat}, and if \idr{n} is in the set then so is \idr{S n}."
The interpretation of \idr{Z} as zero and \idr{S} as successor/plus one comes
from the way that we _use_ \idr{Nat} values, by writing functions to do things
with them, proving things about them, and so on. Your definition of \idr{Bin}
should be correspondingly simple; it is the functions you will write next that
will give it mathematical meaning.)

(b) Next, write an increment function \idr{incr} for binary numbers, and a
    function \idr{bin_to_nat} to convert binary numbers to unary numbers.

(c) Write five unit tests \idr{test_bin_incr_1}, \idr{test_bin_incr_2}, etc. for
    your increment and binary-to-unary functions. Notice that incrementing a
    binary number and then converting it to unary should yield the same result
    as first converting it to unary and then incrementing.

>
>   -- FILL IN HERE
>

$\square$

max_stars_repo_name: MarcelineVQ/software-foundations

max_issues_repo_name: MarcelineVQ/software-foundations

max_forks_repo_name: MarcelineVQ/software-foundations


text:
-- Idris2

import System
import System.Concurrency

||| Test double-release errors correctly
main : IO ()
main =
  do m <- makeMutex
     mutexAcquire m
     putStrLn "Mutex acquired"
     mutexRelease m
     putStrLn "1st release"
     mutexRelease m
     putStrLn "2nd release (SHOULDN'T HAPPEN)"


text:
idF : a -> a
idF = id

extensionality : (f : a -> b) -> (g : a -> b) -> ((x : a) -> f x = g x) -> f = g
extensionality f g = believe_me

leftIdPoint : (f : a -> b) -> (x : a) -> idF (f x) = f x
leftIdPoint f x = Refl

leftId : (f : a -> b) -> (idF . f = f)
leftId f = ?hole


text:
module Solutions.Interfaces

%default total

--------------------------------------------------------------------------------
--          Basics
--------------------------------------------------------------------------------

interface Comp a where
  comp : a -> a -> Ordering

-- 1
anyLarger : Comp a => a -> List a -> Bool
anyLarger va []        = False
anyLarger va (x :: xs) = comp va x == GT || anyLarger va xs

-- 2
allLarger : Comp a => a -> List a -> Bool
allLarger va []        = True
allLarger va (x :: xs) = comp va x == GT && allLarger va xs

-- 3
maxElem : Comp a => List a -> Maybe a
maxElem []        = Nothing
maxElem (x :: xs) = case maxElem xs of
  Nothing => Just x
  Just v  => if comp x v == GT then Just x else Just v

minElem : Comp a => List a -> Maybe a
minElem []        = Nothing
minElem (x :: xs) = case minElem xs of
  Nothing => Just x
  Just v  => if comp x v == LT then Just x else Just v

-- 4
interface Concat a where
  concat : a -> a -> a

implementation Concat String where
  concat = (++)

implementation Concat (List a) where
  concat = (++)

-- 5
concatList : Concat a => List a -> Maybe a
concatList []        = Nothing
concatList (x :: xs) = case concatList xs of
  Nothing => Just x
  Just v  => Just (concat x v)

--------------------------------------------------------------------------------
--          More about Interfaces
--------------------------------------------------------------------------------

-- 1
interface Equals a where
  eq : a -> a -> Bool

  neq : a -> a -> Bool
  neq x y = not (eq x y)

interface Concat a => Empty a where
  empty : a

Equals a => Equals b => Equals (a,b) where
  eq (x1,y1) (x2,y2) = eq x1 x2 && eq y1 y2

Comp a => Comp b => Comp (a,b) where
  comp (x1,y1) (x2,y2) = case comp x1 x2 of
    EQ => comp y1 y2
    v  => v

Concat a => Concat b => Concat (a,b) where
  concat (x1,y1) (x2,y2) = (concat x1 x2, concat y1 y2)

Empty a => Empty b => Empty (a,b) where
  empty = (empty, empty)

-- 2
data Tree : Type -> Type where
  Leaf : a -> Tree a
  Node : Tree a -> Tree a -> Tree a

Equals a => Equals (Tree a) where
  eq (Leaf x)     (Leaf y)     = eq x y
  eq (Node l1 r1) (Node l2 r2) = eq l1 l2 && eq r1 r2
  eq _            _            = False

Concat (Tree a) where
  concat = Node

--------------------------------------------------------------------------------
--          Interfaces in the Prelude
--------------------------------------------------------------------------------

-- 1
record Complex where
  constructor MkComplex
  rel : Double
  img : Double

Eq Complex where
  MkComplex r1 i1 == MkComplex r2 i2 = r1 == r2 && i1 == i2

Num Complex where
  MkComplex r1 i1 + MkComplex r2 i2 = MkComplex (r1 + r2) (i1 + i2)
  MkComplex r1 i1 * MkComplex r2 i2 =
    MkComplex (r1 * r2 - i1 * i2) (r1 * i2 + r2 * i1)
  fromInteger n = MkComplex (fromInteger n) 0.0

Neg Complex where
  negate (MkComplex r i) = MkComplex (negate r) (negate i)
  MkComplex r1 i1 - MkComplex r2 i2 = MkComplex (r1 - r2) (i1 - i2)

Fractional Complex where
  MkComplex r1 i1 / MkComplex r2 i2 = case r2 * r2 + i2 * i2 of
    denom => MkComplex ((r1 * r2 + i1 * i2) / denom)
                       ((i1 * r2 - r1 * i2) / denom)

-- 2
Show Complex where
  showPrec p c = showCon p "MkComplex" (showArg c.rel ++ showArg c.img)

-- 3
record First a where
  constructor MkFirst
  value : Maybe a

pureFirst : a -> First a
pureFirst = MkFirst . Just

mapFirst : (a -> b) -> First a -> First b
mapFirst f = MkFirst . map f . value

mapFirst2 : (a -> b -> c) -> First a -> First b -> First c
mapFirst2 f (MkFirst (Just va)) (MkFirst (Just vb)) = pureFirst (f va vb)
mapFirst2 _ _ _ = MkFirst Nothing

Eq a => Eq (First a) where
  (==) = (==) `on` value

Ord a => Ord (First a) where
  compare = compare `on` value

Show a => Show (First a) where
  show = show . value

FromString a => FromString (First a) where
  fromString = pureFirst . fromString

FromDouble a => FromDouble (First a) where
  fromDouble = pureFirst . fromDouble

FromChar a => FromChar (First a) where
  fromChar = pureFirst . fromChar

Num a => Num (First a) where
  (+) = mapFirst2 (+)
  (*) = mapFirst2 (*)
  fromInteger = pureFirst . fromInteger

Neg a => Neg (First a) where
  negate = mapFirst negate
  (-) = mapFirst2 (-)

Integral a => Integral (First a) where
  mod = mapFirst2 mod
  div = mapFirst2 div

Fractional a => Fractional (First a) where
  (/) = mapFirst2 (/)
  recip = mapFirst recip

-- 4
Semigroup (First a) where
  l@(MkFirst (Just _)) <+> _ = l
  _                    <+> r = r

Monoid (First a) where
  neutral = MkFirst Nothing

-- 5
record Last a where
  constructor MkLast
  value : Maybe a

pureLast : a -> Last a
pureLast = MkLast . Just

mapLast : (a -> b) -> Last a -> Last b
mapLast f = MkLast . map f . value

mapLast2 : (a -> b -> c) -> Last a -> Last b -> Last c
mapLast2 f (MkLast (Just va)) (MkLast (Just vb)) = pureLast (f va vb)
mapLast2 _ _ _ = MkLast Nothing

Eq a => Eq (Last a) where
  (==) = (==) `on` value

Ord a => Ord (Last a) where
  compare = compare `on` value

Show a => Show (Last a) where
  show = show . value

FromString a => FromString (Last a) where
  fromString = pureLast . fromString

FromDouble a => FromDouble (Last a) where
  fromDouble = pureLast . fromDouble

FromChar a => FromChar (Last a) where
  fromChar = pureLast . fromChar

Num a => Num (Last a) where
  (+) = mapLast2 (+)
  (*) = mapLast2 (*)
  fromInteger = pureLast . fromInteger

Neg a => Neg (Last a) where
  negate = mapLast negate
  (-) = mapLast2 (-)

Integral a => Integral (Last a) where
  mod = mapLast2 mod
  div = mapLast2 div

Fractional a => Fractional (Last a) where
  (/) = mapLast2 (/)
  recip = mapLast recip

Semigroup (Last a) where
  _ <+> r@(MkLast (Just _)) = r
  l <+> _                   = l

Monoid (Last a) where
  neutral = MkLast Nothing

-- 6
last : List a -> Maybe a
last = value . foldMap pureLast

-- 7
record Any where
  constructor MkAny
  any : Bool

Semigroup Any where
  MkAny x <+> MkAny y = MkAny (x || y)

Monoid Any where
  neutral = MkAny False

record All where
  constructor MkAll
  all : Bool

Semigroup All where
  MkAll x <+> MkAll y = MkAll (x && y)

Monoid All where
  neutral = MkAll True

-- 8
anyElem : (a -> Bool) -> List a -> Bool
anyElem f = any . foldMap (MkAny . f)

allElems : (a -> Bool) -> List a -> Bool
allElems f = all . foldMap (MkAll . f)

-- 9
record Sum a where
  constructor MkSum
  value : a

record Product a where
  constructor MkProduct
  value : a

Num a => Semigroup (Sum a) where
  MkSum x <+> MkSum y = MkSum (x + y)

Num a => Monoid (Sum a) where
  neutral = MkSum 0

Num a => Semigroup (Product a) where
  MkProduct x <+> MkProduct y = MkProduct (x * y)

Num a => Monoid (Product a) where
  neutral = MkProduct 1

-- 10

sumList : Num a => List a -> a
sumList = value . foldMap MkSum

productList : Num a => List a -> a
productList = value . foldMap MkProduct


text:
module Text.CSS.Render

||| An interface for rendering CSS rules, selectors and
||| properties.
public export
interface Render t where
  render : t -> String


text:
module Selection

import Flexidisc.Record
import Flexidisc.Record.Transformation

person : Record String ["Age" ::: Nat, "Lastname" ::: String, "Firstname" ::: String]
person = ["Age" := 40, "Lastname" := "Doe", "Firstname" := "John"]

justSelection : Maybe (Record String ["Firstname" ::: String, "Lastname" ::: String, "Age" ::: Nat])
justSelection = patchRecord ["Age" := keepIf (>= 18)] person

kid : Record String ["Age" ::: Nat, "Lastname" ::: String, "Firstname" ::: String]
kid = ["Age" := 10, "Lastname" := "Doe", "Firstname" := "John"]

nothingSelection : Maybe (Record String ["Firstname" ::: String, "Lastname" ::: String, "Age" ::: Nat])
nothingSelection = patchRecord ["Age" := keepIf (>= 18)] kid

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
import WebServer
import WebServer.Routes

%default total

standardHeaders : (body : String) -> List Header
standardHeaders body =
  [ ContentLengthFor body
  , ContentType TextHtmlUtf8
  , Custom "Foo" "Bar"
  ]

ok : (body : String) -> Response
ok body =
  MkResponse OK body $ standardHeaders body

created : (uri : String) -> Response
created uri =
  let body = "Location: " ++ uri in
  MkResponse Created body $ Location uri :: standardHeaders body

notFound : Response
notFound =
  let body = "Not Found\n" in
  MkResponse NotFound body $ standardHeaders body

appRoutes : Routes
appRoutes =
  [ get "/" $ \req => ok $
    "I ♥ ur " ++ show (method req) ++ " method\n"

  , get "/" $ \req => ok $
    "Unreachable endpoint\n"

  , get "/posts" $ \_ => ok $
    "Post a, Post b\n"

  , post "/posts" $ \_ => created $
    "/posts/thenewpost"

  , delete "/posts/:num.id/foo/:bar/:str.baz" $ \req, id, bar, baz => ok $
    "You passed " ++ show id ++ " and " ++ bar ++ " and " ++ baz ++ "\n"
  ]

handler : Routes -> Request -> Response
handler routes req =
  fromMaybe notFound (handle req routes)

partial
main : JS_IO ()
main = do
  putStrLn' "Server starting..."
  startServer 4000
              (putStrLn' "The server is ready!")
              (handler appRoutes)

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

max_stars_repo_name: camelpunch/idris-web-server

max_issues_repo_name: camelpunch/idris-web-server

max_forks_repo_name: camelpunch/idris-web-server


text:
import Effects
import Effect.StdIO
import IdrisNet.UDP.UDPServer
import DNSParser
import DNS
import IdrisNet.Socket

recvAndParse : { [UDPSERVER UDPBound, STDIO, DNSPARSER ()] ==>
                 [UDPSERVER (), STDIO, DNSPARSER()] } Eff IO ()
recvAndParse = do
  udp_dns <- udpReadPacket' dns 1024
  case udp_dns of
    UDPSuccess (addr, Just (dns_pckt, len, ptr)) => do
      parsed_dns <- parseDNS ptr len dns_pckt
      case parsed_dns of
        Left err => do putStr $ "Error decoding: " ++ show err ++ "\n"
                       udpClose
        Right decoded_dns => do putStr $ "Decoded successfully! " ++ (show decoded_dns)
                                udpClose
    UDPSuccess (addr, Nothing) => do putStr "Error in readPacket... :'(\n"
                                     udpClose
    UDPFailure err => do putStr $ "Error receiving: " ++ (show err) ++ "\n"
                         udpFinalise
    UDPRecoverableError err => do putStr $ "Error receiving: " ++ (show err) ++ "\n"
                                  udpClose

dnsRespTest : Port -> { [UDPSERVER (), STDIO, DNSPARSER ()] } Eff IO ()
dnsRespTest port =
  case !(udpBind Nothing port) of
    UDPSuccess _ => recvAndParse
    UDPFailure err => putStr ("Error connecting: " ++ (show err))
    UDPRecoverableError err => putStr ("Error connecting: " ++ (show err))

main : IO ()
main = run (dnsRespTest 4099)


text:
module Order

%default total
%access public export

data InclusiveEither : (typeLeft : Type) -> (typRight : Type) -> Type where
	LeftInc : typLeft -> Not typRight -> InclusiveEither typLeft typRight
	RightInc : Not typLeft -> typRight -> InclusiveEither typLeft typRight
	Both : typLeft -> typRight -> InclusiveEither typLeft typRight

data ExclusiveEither : (typLeft : Type) -> (typRight : Type) -> Type where
	LeftExc : typLeft -> Not typRight -> ExclusiveEither typLeft typRight
	RightExc : Not typLeft -> typRight -> ExclusiveEither typLeft typRight

|||Type of subset of a set
subset : Type -> Type
subset typ = (typ -> Bool)

|||Type of proof that an element x belongs to a subset
isIn : {typ : Type} -> (subset typ) -> (x : typ) -> Type
isIn {typ} subSet x = ((subSet x) = True)

|||Type of proof that two relations are equal
relEqual : {typ : Type} -> (typ -> typ -> Type) -> (typ -> typ -> Type) -> Type
relEqual {typ} r1 r2 = (a : typ) -> (b : typ) -> ((r1 a b) -> (r2 a b), (r2 a b) -> (r1 a b))

|||Induces a strict relation from a relation
toStrictRelation : {typ : Type} -> (r : (typ -> typ -> Type)) -> (typ -> typ -> Type)
toStrictRelation r = (\a => (\b => (r a b, Not (a = b))))

|||Induces a reverse relation from a relation
toReverseRelation : {typ : Type} -> (r : (typ -> typ -> Type)) -> (typ -> typ -> Type)
toReverseRelation r = (\a => (\b => (r b a)))

|||Induces a strict reverse relation from a relation
toStrictReverseRelation : {typ : Type} -> (r : (typ -> typ -> Type)) -> (typ -> typ -> Type)
toStrictReverseRelation r = (\a => (\b => (r b a, Not (b = a))))

|||Type of proof that a relation is reflexive
isReflexive : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isReflexive {typ} r = {a : typ} -> (r a a)

|||Type of proof that a relation is symmetric
isSymmetric : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isSymmetric {typ} r = {a : typ} -> {b : typ} -> (r a b) -> (r b a)

|||Type of proof that a relation is anti-symmetric
isAntiSymmetric : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isAntiSymmetric {typ} r = {a : typ} -> {b : typ} -> (r a b) -> (r b a) -> (a = b)

|||Type of proof that a relation is transitive
isTransitive : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isTransitive {typ} r = {a : typ} -> {b : typ} -> {c : typ} -> (r a b) -> (r b c) -> (r a c)

|||Type of proof that a relation is an equivalence
isEquivalence : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isEquivalence {typ} r = (isReflexive r, isSymmetric r, isTransitive r)

|||Type of proof that a relation is a partial order
isPartialOrder : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isPartialOrder {typ} r = (isReflexive r, isAntiSymmetric r, isTransitive r)

|||Type of proof that a relation is a total order
isTotalOrder : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isTotalOrder {typ} r = (isPartialOrder r, (a : typ) -> (b : typ) -> (InclusiveEither (r a b) ((toReverseRelation r) a b)))

|||Type of proof that a relation is a well-order
isWellOrder : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isWellOrder {typ} r = (isPartialOrder r, (subSet : (subset typ)) -> (a : typ ** (isIn subSet a, ((x : typ) -> (isIn subSet x) -> (r a x)))))

|||Proof that the reverse of the reverse of the relation is the relation
reverseIdempotent : {typ : Type} -> {r : (typ -> typ -> Type)} ->
				(relEqual r (toReverseRelation (toReverseRelation r)))
reverseIdempotent {typ} {r} a b = (id, id)

|||Proof that the reverse of a reflexive relation is reflexive
reversePreservesRefl : {typ : Type} -> {r : (typ -> typ -> Type)} ->
					(isReflexive r) -> (isReflexive (toReverseRelation r))
reversePreservesRefl {typ} {r} rIsRefl = rIsRefl

|||Proof that the reverse of a symmetric relation is symmetric
reversePreservesSymm : {typ : Type} -> {r : (typ -> typ -> Type)} ->
					(isSymmetric r) -> (isSymmetric (toReverseRelation r))
reversePreservesSymm {typ} {r} rIsSymm = rIsSymm

|||Proof that the reverse of an anti-symmetric relation is anti-symmetric
reversePreservesAntiSymm : {typ : Type} -> {r : (typ -> typ -> Type)} ->
						(isAntiSymmetric r) -> (isAntiSymmetric (toReverseRelation r))
reversePreservesAntiSymm {typ} {r} rIsAntiSymm relLeft relRight = rIsAntiSymm relRight relLeft

|||Proof that the reverse of a transitive relation is transitive
reversePreservesTrans : {typ : Type} -> {r : (typ -> typ -> Type)} ->
					(isTransitive r) -> (isTransitive (toReverseRelation r))
reversePreservesTrans {typ} {r} rIsTrans relLeft relRight = rIsTrans relRight relLeft

|||Proof that a reverse order of a symmetric relation is the relation itself
reverseSymmEq : {typ : Type} -> {r : (typ -> typ -> Type)} ->
				(isSymmetric r) -> (relEqual r (toReverseRelation r))
reverseSymmEq {typ} {r} rIsSymmetric a b = (rIsSymmetric, rIsSymmetric)

|||Proof that a reverse order of a partial order is a partial order
reversePOrderIsPOrder : {typ : Type} -> {r : (typ -> typ -> Type)} ->
					(isPartialOrder r) -> (isPartialOrder (toReverseRelation r))
reversePOrderIsPOrder {typ} {r} (rIsRefl, rIsAntiSym, rIsTrans) = (rIsRefl, reversePreservesAntiSymm rIsAntiSym, reversePreservesTrans {typ} {r} rIsTrans)

|||Proof that !(b <= a) implies a != b
notSymmImpliesNotEq : {typ : Type} -> {r : (typ -> typ -> Type)} -> (isReflexive r) -> (Not ((toReverseRelation r) a b)) -> (Not (a = b))
notSymmImpliesNotEq {typ} {r} rIsRefl notLTE Refl = void(notLTE rIsRefl)

|||Proof that a total order leads to a strict order
toStrictOrder : {typ : Type} -> {r : (typ -> typ -> Type)} -> (isTotalOrder r) -> ((a : typ) -> (b : typ) -> (Either (a = b) (ExclusiveEither ((toStrictRelation r) a b) ((toStrictReverseRelation r) a b))))
toStrictOrder {typ} {r} rIsTotalOrder a b =
	case rIsTotalOrder of
	(rIsPartialOrder, rIsTotal) =>
		case (rIsPartialOrder) of
		(rIsRefl, rIsAntiSymm, rIsTrans) =>
				case (rIsTotal a b) of
				(Both leftOrder rightOrder) => Left (rIsAntiSymm leftOrder rightOrder)
				(LeftInc leftOrder notRightOrder) => Right (LeftExc (leftOrder, notSymmImpliesNotEq rIsRefl notRightOrder) (\rightOrder => notRightOrder (fst rightOrder)))
				(RightInc notLeftOrder rightOrder) => Right (RightExc (\leftOrder => notLeftOrder (fst leftOrder)) (rightOrder, notSymmImpliesNotEq rIsRefl notLeftOrder))


text:
-- --------------------------------------------------------------- [ Error.idr ]
-- Module    : Error.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Frigg.Error

import XML.XPath

%access export

public export
data FriggError : Type where
  FeatureNotImpl    : FriggError
  NoFormatSpecified : FriggError
  NoModeSpecified   : FriggError
  FileExpected      : FriggError
  MissingFile       : String -> FriggError
  MalformedPattern  : FriggError
  InvalidMapping    : FriggError
  PatternDocMissing : FriggError
  NoSuchCommand     : FriggError
  ParseError        : String -> FriggError
  GeneralError      : String -> FriggError
  EvalError         : String -> FriggError
  ExtractionError   : XPathError -> FriggError

Show FriggError where
  show NoSuchCommand     = "Command Not Recognised"
  show PatternDocMissing = "External Document needs to be specified."
  show NoModeSpecified   = "No Mode Specified"
  show NoFormatSpecified = "No output format specified"
  show FeatureNotImpl    = "Feature Not Implemented"
  show MalformedPattern  = "Pattern is malformed."
  show InvalidMapping    = "Mappings must be greater than zero"
  show FileExpected      = "File Expected"

  show (GeneralError msg) = unwords ["General Error", msg]
  show (MissingFile fn)   = unwords ["Missing file:", fn]
  show (ParseError  msg)  = unlines ["Parse Error:", msg]
  show (EvalError fn)     = unwords ["Error During Evaluation:", fn]
  show (ExtractionError msg) = unwords ["Extraction Error", show msg]

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

max_stars_repo_name: jfdm/frigg-tool

max_issues_repo_name: jfdm/frigg-tool

max_forks_repo_name: jfdm/frigg-tool


text:
module Web.Internal.VisibilityPrim

import JS
import Web.Internal.Types


text:
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

record MyDPair a p where
  constructor MkMyDPair
  dfst : a
  dsnd : p dfst

cons : t -> MyDPair Nat (\n => Vect n t) -> MyDPair Nat (\n => Vect n t)
cons val xs
    = { dfst := S (dfst xs),
        dsnd := val :: dsnd xs } xs

cons' : t -> MyDPair Nat (\n => Vect n t) -> MyDPair Nat (\n => Vect n t)
cons' val
    = { dfst $= S,
        dsnd $= (val ::) }

record Stats where
  constructor MkStats
  height : Int
  weight : Int

record Person where
  constructor MkPerson
  name : String
  age, shoesize : Int
  more : Stats

testPair : MyDPair Nat (\n => Vect n Int)
testPair = MkMyDPair _ [1,2,3,4,5]

testPerson : Person
testPerson = MkPerson "Fred" 1337 10 (MkStats 10 10)

grow : Person -> Person
grow = { more.height $= (+1) }


text:
module Data.String.Extra

%access public export

parseInteger : List Char -> Integer -> Maybe Integer
parseInteger []        acc = Just acc
parseInteger (c :: cs) acc =
  if (c >= '0' && c <= '9')
  then parseInteger cs ((acc * 10) + (cast ((ord c) - (ord '0'))))
  else Nothing

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Proof

%default total
%access export

invert : (a : Nat) -> (b : Nat) -> (a + a = b + b) -> a = b
invert Z     Z     = const Refl
invert Z     (S k) = absurd . SIsNotZ . sym
invert (S k) Z     = absurd . SIsNotZ
invert (S k) (S j) = rewrite sym $ plusSuccRightSucc k k in rewrite sym $ plusSuccRightSucc j j in
                     eqSucc k j . invert k j . succInjective (k+k) (j+j) . succInjective (S $ k+k) (S $ j+j)

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Main

import Minesweeper.REPL

main : IO ()
main = repl

max_stars_repo_name: RossMeikleham/Idris-Minesweeper

max_issues_repo_name: RossMeikleham/Idris-Minesweeper

max_forks_repo_name: RossMeikleham/Idris-Minesweeper


text:
module ProcessLib

import Data.Fuel
import System.Concurrency.Channels

%default total

export
data MessagePID : (iface : reqType -> Type) -> Type where
     MkMessage : PID -> MessagePID iface

public export
NoRecv : Void -> Type
NoRecv = const Void

public export
data ProcState = Ready | Sent | Looping

public export
data Process : (iface : reqType -> Type) ->
               Type -> ProcState -> ProcState -> Type where
     Request : MessagePID service_iface ->
               (msg : service_reqType) ->
               Process iface (service_iface msg) st st
     Respond : ((msg : reqType) -> Process iface (iface msg) Ready Ready) ->
               Process iface (Maybe reqType) st Sent
     Spawn : Process service_iface () Ready Looping ->
             Process iface (Maybe (MessagePID service_iface)) st st

     Loop : Inf (Process iface a Ready Looping) ->
            Process iface a Sent Looping
     Action : IO a -> Process iface a st st
     Pure : a -> Process iface a st st
     (>>=) : Process iface a st1 st2 -> (a -> Process iface b st2 st3) ->
             Process iface b st1 st3

export total
run : Fuel -> Process iface t in_state out_state -> IO (Maybe t)
run fuel (Request {service_iface} (MkMessage process) msg)
          = do Just chan <- connect process
                    | _ => pure Nothing
               ok <- unsafeSend chan msg
               if ok then do Just x <- unsafeRecv (service_iface msg) chan
                                  | Nothing => pure Nothing
                             pure (Just x)
                     else pure Nothing
run fuel (Respond {reqType} calc)
          = do Just sender <- listen 1
                    | Nothing => pure (Just Nothing)
               Just msg <- unsafeRecv reqType sender
                    | Nothing => pure (Just Nothing)
               Just res <- run fuel (calc msg)
                    | Nothing => pure Nothing
               unsafeSend sender res
               pure (Just (Just msg))
run (More fuel) (Loop proc) = run fuel proc
run fuel (Spawn proc) = do Just pid <- spawn (do run fuel proc
                                                 pure ())
                                | Nothing => pure (Just Nothing)
                           pure (Just (Just (MkMessage pid)))
run fuel (Action act) = do res <- act
                           pure (Just res)
run fuel (Pure val) = pure (Just val)
run fuel (act >>= next) = do Just x <- run fuel act
                                  | Nothing => pure Nothing
                             run fuel (next x)
run Dry _ = pure Nothing

public export
Service : (iface : reqType -> Type) -> Type -> Type
Service iface a = Process iface a Ready Looping

public export
Client : Type -> Type
Client a = Process NoRecv a Ready Ready

partial export
runProc : Process iface () in_state out_state -> IO ()
runProc proc = do run forever proc
                  pure ()

max_stars_repo_name: jameshaydon/smproc

max_issues_repo_name: jameshaydon/smproc

max_forks_repo_name: jameshaydon/smproc


text:
record Foo (param : Nat) where
  constructor MkFoo
  num : Int

implementation Show (Foo n) where
  show f = show (param_param f) ++ ", " ++ show (num f)

main : IO ()
main = do let x = MkFoo {param=10} 20
          putStrLn (show (record { param_param = 42 } x))
          putStrLn (show (record { num = 42 } x))

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
import Data.Vect

-- Exercise 1
readToBlank : IO (List String)
readToBlank = do line <- getLine
                 case line of
                   "" => pure []
                   _ => do lines <- readToBlank
                           pure $ line :: lines

-- Exercise 2
readAndSave : IO ()
readAndSave = do lines <- readToBlank
                 putStrLn "Filename: "
                 fname <- getLine
                 Right () <- writeFile fname (unlines lines)
                   | Left err => putStrLn (show err)
                 pure ()

-- Exercise 3
readVectFile : (filename : String) -> IO (n ** Vect n String)
readVectFile filename = do Right h <- openFile filename Read
                               | Left err => pure (_ ** [])
                           Right contents <- readContents h
                               | Left err => pure (_ ** [])
                           closeFile h
                           pure contents
    where readContents : File -> IO (Either FileError (n ** Vect n String))
          readContents h = do eof <- fEOF h
                              if eof then pure (Right (_ ** [])) else do
                                 Right str <- fGetLine h
                                    | Left err => pure (Left err)
                                 Right (_ ** rest) <- readContents h
                                    | Left err => pure (Left err)
                                 pure (Right (_ ** str :: rest))


text:
module Main

import GameServer.Protocol.Options
import GameServer.Protocol.Tester
import GameServer.Protocol.Mock
import System

%cg chez libidris_net.so

main : IO ()
main = do
  (_ :: args) <- getArgs
  case processOptions args of
    Left err => putStrLn err
    Right options@(MkOptions _ _ TesterMode) => do
      Right () <- tester options
        | Left err => putStrLn err
      pure ()
    Right options@(MkOptions _ _ MockMode) => do
      Right () <- mock options
        | Left err => putStrLn err
      pure ()


text:
module Main

import Prelude

-- https://stackoverflow.com/a/11554793/3574379

interface Twice f where
  twice : f -> f

Twice (a -> a) where
  twice f = f . f

interface Example a where
  transform : Int -> a

Example Int where
  transform n = n + 1

Example Char where
  transform _ = 'x'

-- run in REPL to see that it derives properly:

-- $ idris src/15_EqualityConstraint_Twice_class.idr
-- *src/15_EqualityConstraint_Twice_class> :t twice transform
-- twice transform : Int -> Int

-- Summary:
-- in idris you dont need equality constaint to derive type of such functions properly

max_stars_repo_name: srghma/hask-test

max_issues_repo_name: BjornMelgaard/hask-test

max_forks_repo_name: BjornMelgaard/hask-test


text:
{--- -}
fun : Int -> Bool
fun x = (x /= 0)
{-
-}
main : IO ()
main = print (fun 5)

-- EXPLANATION:
-- this is about parsing the opening `{---`
-- which used to be parsed as two separate tokens `{-` and `--`
-- making the above program fail


text:
module Test.Pattern

import Data.SortedMap
import Test.Assertions
import Idrlisp.Pattern
import Idrlisp.Sexp

%default covering

build' : Sexp () -> Either (Sexp ()) Pattern
build' = Pattern.build

bind' : List String -> Maybe String -> List (Sexp ()) -> Either String (List (String, Sexp ()))
bind' f r args = Pattern.bind (MkPattern f r) args

export
test : IO ()
test = describe "Idrlisp.Pattern" $ do
  describe "show" $ do
    MkPattern [] Nothing
      `shouldShow` "()"
    MkPattern ["x"] Nothing
      `shouldShow` "(x)"
    MkPattern ["x", "y"] Nothing
      `shouldShow` "(x y)"
    MkPattern [] (Just "a")
      `shouldShow` "a"
    MkPattern ["x"] (Just "a")
      `shouldShow` "(x . a)"
    MkPattern ["x", "y"] (Just "a")
      `shouldShow` "(x y . a)"
  describe "build" $ do
    build' []
      `shouldBe` Right (MkPattern [] Nothing)
    build' [Sym "x"]
      `shouldBe` Right (MkPattern ["x"] Nothing)
    build' [Sym "x", Sym "y"]
      `shouldBe` Right (MkPattern ["x", "y"] Nothing)
    build' (Sym "a")
      `shouldBe` Right (MkPattern [] (Just "a"))
    build' (Sym "x" :: Sym "a")
      `shouldBe` Right (MkPattern ["x"] (Just "a"))
    build' (Sym "x" :: Sym "y" :: Sym "a")
      `shouldBe` Right (MkPattern ["x", "y"] (Just "a"))
    build' (Num 123)
      `shouldBe` Left (Num 123)
    build' [Sym "x", Str "f", Sym "y"]
      `shouldBe` Left (Str "f")
  describe "bind" $ do
    bind' [] Nothing []
      `shouldBe` Right []
    bind' ["x", "y"] Nothing [Num 1, Num 2]
      `shouldBe` Right [("x", Num 1), ("y", Num 2)]
    bind' ["x", "y"] (Just "z") [Num 1, Num 2]
      `shouldBe` Right [("x", Num 1), ("y", Num 2), ("z", [])]
    bind' ["x", "y"] (Just "z") [Num 1, Num 2, Num 3, Num 4]
      `shouldBe` Right [("x", Num 1), ("y", Num 2), ("z", [Num 3, Num 4])]
    bind' ["x", "y"] Nothing [Num 1]
      `shouldSatisfy` isLeft
    bind' ["x", "y"] (Just "z") [Num 1]
      `shouldSatisfy` isLeft
    bind' ["x", "y"] Nothing [Num 1, Num 2, Num 3]
      `shouldSatisfy` isLeft

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Refined

import Data.List

%access public export

Refined : (a : Type) -> (P : a -> Type) -> Type
Refined = DPair

implicit
toRefined : { a : Type } -> { P : a -> Type } -> (x:a) -> { auto property : P x } -> Refined a P
toRefined value {property} = (value ** property)

-- Havent yet figured out how to make Idris use an implicit generic fromRefined
implicit
fromCharRefined : { P : Char -> Type } -> Refined Char P -> Char
fromCharRefined = fst

implicit
fromStringRefined : { P : String -> Type } -> Refined String P -> String
fromStringRefined = fst

implicit
fromNatRefined : { P : Nat -> Type } -> Refined Nat P -> Nat
fromNatRefined = fst

max_stars_repo_name: janschultecom/idris-refined

max_issues_repo_name: janschultecom/idris-refined

max_forks_repo_name: janschultecom/idris-refined


text:
module Door

import Effects

data DoorState = Closed | Open
data DoorInfo : DoorState -> Type where
     DI : DoorInfo s

data Door : Effect where
     OpenDoor : sig Door () (DoorInfo Closed) (DoorInfo Open)
     CloseDoor : sig Door () (DoorInfo Open) (DoorInfo Closed)
     Knock : sig Door () (DoorInfo Closed)

DOOR : DoorState -> EFFECT
DOOR t = MkEff (DoorInfo t) Door

openDoor : Eff () [DOOR Closed] [DOOR Open]
openDoor = call OpenDoor

closeDoor : Eff () [DOOR Open] [DOOR Closed]
closeDoor = call CloseDoor

knock : Eff () [DOOR Closed]
knock = call Knock

doorProg : Eff () [DOOR Closed]
doorProg = do knock
              openDoor
              closeDoor

max_stars_repo_name: idris-hackers/idris-demos

max_issues_repo_name: idris-hackers/idris-demos

max_forks_repo_name: idris-hackers/idris-demos


text:
module TypeSynonym

import Data.Vect

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

-- Type Synonym, similar to type alias in Scala and Haskell
Position : Type
Position = (Double, Double)

triBetter : Vect 3 Position
triBetter = [(0.0, 0.0), (3.0, 0.0), (0.0, 4.0)]

-- Type Synonym, which is actually a function which computes a type
Polygon : Nat -> Type
Polygon n = Vect n Position

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

triEval : Polygon 3
triEval = [(?triEval_rhs1, ?triEval_rhs2),
           (?triEval_rhs3, ?triEval_rhs4),
           (?triEval_rhs5, ?triEval_rhs6)]

max_stars_repo_name: balajisivaraman/idris-book

max_issues_repo_name: balajisivaraman/idris-book

max_forks_repo_name: balajisivaraman/idris-book


text:
module Client.Action.Exec

import Client.Action.Build
import Fmt
import Inigo.Async.Base
import Inigo.Async.Package
import Inigo.Async.Promise
import Inigo.Package.CodeGen as CodeGen
import Inigo.Package.Package
import System.Path

execDir : String
execDir =
  "build/exec"

-- TODO: Better handling of base paths
export
exec : CodeGen -> Bool -> List String -> Promise ()
exec codeGen build userArgs =
  do
    pkg <- Client.Action.Build.writeIPkgFile
    when build $ runBuild codeGen
    let Just e = executable pkg
      | Nothing => reject "No executable set in Inigo config"
    let (cmd, args) = CodeGen.cmdArgs codeGen (execDir </> e)
    log (fmt "Executing %s with args %s..." e (show userArgs))
    ignore $ systemWithStdIO cmd (args ++ userArgs) True True

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module India.Union

import public Data.List.AtIndex
import public Data.OpenUnion
import Text.Lexer

export
(t : _) =>
Show (elt t) =>
Show (Union elt [t]) where
  show = show . decomp0

export
(t : _) =>
Show (elt t) => Show (Union elt ts) =>
Show (Union elt (t::ts)) where
  show x = case decomp x of
                Left y  => show y
                Right y => show y

export
(t : _) =>
Eq (elt t) =>
Eq (Union elt [t]) where
  (==) = (==) `on` decomp0
  (/=) = (/=) `on` decomp0

export
(t : _) =>
Eq (elt t) => Eq (Union elt ts) =>
Eq (Union elt (t::ts)) where
  (==) = (==) `on` decomp
  (/=) = (/=) `on` decomp

export
(t : a) =>
TokenKind (elt t) =>
TokenKind (Union elt [t]) where
    TokType x = TokType $ decomp0 x
    tokValue x = tokValue $ decomp0 x

export
(t : a) =>
TokenKind (elt t) => TokenKind (Union elt ts) =>
TokenKind (Union elt (t::ts)) where
  TokType x with (decomp x)
    TokType x | (Left y) = TokType y
    TokType x | (Right y) = TokType y
  tokValue x str with (decomp x)
    tokValue x str | (Left y) = tokValue y str
    tokValue x str | (Right y) = tokValue y str

max_stars_repo_name: berewt/india

max_issues_repo_name: berewt/india

max_forks_repo_name: berewt/india


text:
import Data.List.Views

total
qsort : Ord a => (xs : List a) -> List a
qsort inp with (filtered (<) inp)
  qsort [] | FNil = []
  qsort (x :: xs) | (FRec lrec rrec)
     = qsort (filter (\v => v < x) xs) | lrec ++
         x :: qsort (filter (\v => not (v < x)) xs) | rrec

testList : Int -> Int -> List Int -> List Int
testList 0 seed acc = acc
-- Need to explicitly mod since different back ends overflow differently
testList x seed acc = let seed' = (seed * 12345 + 768) `mod` 65536 in
                          testList (x - 1) seed'
                               ((seed' `mod` 100) :: acc)

myhead : List a -> a
myhead (x :: xs) = x

main : IO ()
main = do let list = testList 100 12345 []
          putStrLn "Sorting list"
          let list' = qsort list
          printLn list'