text:
module BiNat.Properties.Minus

import BiNat
import BiNat.Properties.Plus
import BiNat.Properties.Induction
import BiNat.Properties.LT
import BiNat.Properties.Mult

%access public export
%default total

minusLast00 : (ms, ns : BiNat) -> (tail : List Bit) ->
  minus' (ms -: O) (ns -: O) tail = minus' ms ns (O :: tail)
minusLast00 J         J         tail = Refl
minusLast00 J         (ns -: O) tail = Refl
minusLast00 J         (ns -: I) tail = Refl
minusLast00 (ms -: O) J         tail = Refl
minusLast00 (ms -: I) J         tail = Refl
minusLast00 (ms -: O) (ns -: O) tail = Refl
minusLast00 (ms -: O) (ns -: I) tail = Refl
minusLast00 (ms -: I) (ns -: O) tail = Refl
minusLast00 (ms -: I) (ns -: I) tail = Refl

minusLast10 : (ms, ns : BiNat) -> (tail : List Bit) ->
  minus' (ms -: I) (ns -: O) tail = minus' ms ns (I :: tail)
minusLast10 J         J         tail = Refl
minusLast10 J         (ns -: O) tail = Refl
minusLast10 J         (ns -: I) tail = Refl
minusLast10 (ms -: O) J         tail = Refl
minusLast10 (ms -: I) J         tail = Refl
minusLast10 (ms -: O) (ns -: O) tail = Refl
minusLast10 (ms -: O) (ns -: I) tail = Refl
minusLast10 (ms -: I) (ns -: O) tail = Refl
minusLast10 (ms -: I) (ns -: I) tail = Refl

minusLast11 : (ms, ns : BiNat) -> (tail : List Bit) ->
  minus' (ms -: I) (ns -: I) tail = minus' ms ns (O :: tail)
minusLast11 J         J         tail = Refl
minusLast11 J         (ns -: O) tail = Refl
minusLast11 J         (ns -: I) tail = Refl
minusLast11 (ms -: O) J         tail = Refl
minusLast11 (ms -: I) J         tail = Refl
minusLast11 (ms -: O) (ns -: O) tail = Refl
minusLast11 (ms -: O) (ns -: I) tail = Refl
minusLast11 (ms -: I) (ns -: O) tail = Refl
minusLast11 (ms -: I) (ns -: I) tail = Refl

minusLast01 : (ms, ns : BiNat) -> (tail : List Bit) -> Not (ms = J) ->
  minus' (ms -: O) (ns -: I) tail = minus' (pred ms) ns (I :: tail)
minusLast01 J         ns         tail notJ = absurd (notJ Refl)
minusLast01 (ms -: O) J          tail _    = Refl
minusLast01 (ms -: I) J          tail _    = Refl
minusLast01 (ms -: O) (ns -: O)  tail _    = Refl
minusLast01 (ms -: O) (ns -: I)  tail _    = Refl
minusLast01 (ms -: I) (ns -: O)  tail _    = Refl
minusLast01 (ms -: I) (ns -: I)  tail _    = Refl

minusLast0J : (ms : BiNat) -> (tail : List Bit) -> Not (ms = J) ->
  minus' (ms -: O) J tail = foldl (-:) (pred ms -: I) tail
minusLast0J J         tail notJ = absurd (notJ Refl)
minusLast0J (ms -: O) tail _    = Refl
minusLast0J (ms -: I) tail _    = Refl

minusLast1J : (ms : BiNat) -> (tail : List Bit) -> Not (ms = J) ->
  minus' (ms -: I) J tail = foldl (-:) (ms -: O) tail
minusLast1J J         tail notJ = absurd (notJ Refl)
minusLast1J (ms -: O) tail _    = Refl
minusLast1J (ms -: I) tail _    = Refl

jMinusIsJ : (n : BiNat) -> minus J n = J
jMinusIsJ J         = Refl
jMinusIsJ (ns -: n) = Refl

minusJIsPred : (n : BiNat) -> minus n J = pred n
minusJIsPred J              = Refl
minusJIsPred (J -: O)       = Refl
minusJIsPred (ns -: n -: O) = rewrite predDashAppendsAcc (ns -: n) [I] in Refl
minusJIsPred (J -: I)       = Refl
minusJIsPred (ns -: n -: I) = Refl

minusOfItSelf : (n : BiNat) -> (tail : List Bit) -> minus' n n tail = tailToBiNat tail
minusOfItSelf J              tail = Refl
minusOfItSelf (J -: O)       tail = Refl
minusOfItSelf (ns -: O -: O) tail = rewrite minusOfItSelf (ns -: O) (O :: tail) in Refl
minusOfItSelf (ns -: I -: O) tail = rewrite minusOfItSelf (ns -: I) (O :: tail) in Refl
minusOfItSelf (J -: I)       tail = Refl
minusOfItSelf (ns -: O -: I) tail = rewrite minusOfItSelf (ns -: O) (O :: tail) in Refl
minusOfItSelf (ns -: I -: I) tail = rewrite minusOfItSelf (ns -: I) (O :: tail) in Refl

minusDashAppendsTail : (m, n : BiNat) -> GT m n -> (tail : List Bit) ->
  minus' m n tail = foldl (-:) (minus' m n []) tail
minusDashAppendsTail J              n              lt tail impossible
minusDashAppendsTail (J -: O)       J              lt tail = Refl
minusDashAppendsTail (ms -: m -: O) J              lt tail = Refl
minusDashAppendsTail (J -: I)       J              lt tail = Refl
minusDashAppendsTail (ms -: m -: I) J              lt tail = Refl
minusDashAppendsTail (ms -: O)      (ns -: O) (LTAppend ns ms lt O O) tail =
  rewrite minusLast00 ms ns tail in
  rewrite minusLast00 ms ns [] in
  rewrite minusDashAppendsTail ms ns lt (O :: tail) in
  rewrite minusDashAppendsTail ms ns lt [O] in Refl
minusDashAppendsTail (J -: O)       (ns -: I)      (LTAppend ns J lt I O) tail impossible
minusDashAppendsTail (ms -: m -: O) (J -: I)       (LTAppend J (ms -: m) lt I O) tail =
  case lessThanImpliesLTEPred J (ms -: m) lt of
    LTEEqual _ _ eq =>
      rewrite sym $ eq in Refl
    LTELessThan _ _ lt2 =>
      rewrite minusDashAppendsTail (pred (ms -: m)) J lt2 (I :: tail) in
      rewrite minusDashAppendsTail (pred (ms -: m)) J lt2 [I] in Refl
minusDashAppendsTail (ms -: m -: O) (ns -: n -: I) (LTAppend (ns -: n) (ms -: m) lt I O) tail =
  case lessThanImpliesLTEPred (ns -: n) (ms -: m) lt of
    LTEEqual _ _ eq =>
      rewrite sym $ eq in
      rewrite minusOfItSelf (ns -: n) (I :: tail) in
      rewrite minusOfItSelf (ns -: n) [I] in Refl
    LTELessThan _ _ lt2 =>
      rewrite minusDashAppendsTail (pred (ms -: m)) (ns -: n) lt2 (I :: tail) in
      rewrite minusDashAppendsTail (pred (ms -: m)) (ns -: n) lt2 [I] in Refl
minusDashAppendsTail (ms -: I)      (ns -: O)      (LTLeading ns ms eq) tail =
  rewrite eq in
  rewrite minusLast10 ms ms tail in
  rewrite minusLast10 ms ms [] in
  case ms of
    J          => Refl
    (ms2 -: m) =>
      rewrite minusOfItSelf (ms2 -: m) (I :: tail) in
      rewrite minusOfItSelf (ms2 -: m) [I] in Refl
minusDashAppendsTail (ms -: m -: I) (ns -: O)      (LTAppend ns (ms -: m) lt O I) tail =
  rewrite minusDashAppendsTail (ms -: m) ns lt (I :: tail) in
  rewrite minusDashAppendsTail (ms -: m) ns lt [I] in Refl
minusDashAppendsTail (J -: I)       (ns -: I)      (LTAppend ns J lt I I) tail impossible
minusDashAppendsTail (ms -: m -: I) (ns -: I)      (LTAppend ns (ms -: m) lt I I) tail =
  rewrite minusDashAppendsTail (ms -: m) ns lt (O :: tail) in
  rewrite minusDashAppendsTail (ms -: m) ns lt [O] in Refl

plusNMinusN : (m, n : BiNat) -> minus (plus m n) n = m
plusNMinusN J              J              = Refl
plusNMinusN J              (J -: O)       = Refl
plusNMinusN J              (ns -: O -: O) = minusOfItSelf (ns -: O) [I]
plusNMinusN J              (ns -: I -: O) = minusOfItSelf (ns -: I) [I]
plusNMinusN J              (J -: I)       = Refl
plusNMinusN J              (ns -: O -: I) = minusOfItSelf (ns -: O) [I]
plusNMinusN J              (ns -: I -: I) =
  rewrite succDashAppendsAcc ns [O, O] in
  rewrite predOfDoubled (succ ns) (succIsNotJ ns) in
  rewrite predOfSucc ns in
  rewrite minusOfItSelf (ns -: I) [I] in Refl
plusNMinusN (J -: O)       J              = Refl
plusNMinusN (ms -: O -: O) J              = Refl
plusNMinusN (ms -: I -: O) J              = Refl
plusNMinusN (J -: I)       J              = Refl
plusNMinusN (ms -: O -: I) J              = Refl
plusNMinusN (ms -: I -: I) J              =
  rewrite succDashAppendsAcc ms [O, O] in
  rewrite predOfDoubled (succ ms) (succIsNotJ ms) in
  rewrite predOfSucc ms in Refl
plusNMinusN (ms -: O)      (ns -: O)      =
  rewrite plusDashAppendsAcc ms ns O [O] in
  rewrite minusLast00 (plus ms ns) ns [] in
  rewrite minusDashAppendsTail (plus ms ns) ns (lessThanPlus ns ms) [O] in
  rewrite plusNMinusN ms ns in Refl
plusNMinusN (ms -: O)      (ns -: I)      =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite minusLast11 (plus ms ns) ns [] in
  rewrite minusDashAppendsTail (plus ms ns) ns (lessThanPlus ns ms) [O] in
  rewrite plusNMinusN ms ns in Refl
plusNMinusN (ms -: I)      (ns -: O)      =
  rewrite plusDashAppendsAcc ms ns O [I] in
  rewrite minusLast10 (plus ms ns) ns [] in
  rewrite minusDashAppendsTail (plus ms ns) ns (lessThanPlus ns ms) [I] in
  rewrite plusNMinusN ms ns in Refl
plusNMinusN (ms -: I)      (ns -: I)      =
  rewrite plusDashAppendsAcc ms ns I [O] in
  rewrite sym $ succGoesToCarry ms ns [] in
  rewrite minusLast01 (succ (plus ms ns)) ns [] (succIsNotJ (plus ms ns)) in
  rewrite predOfSucc (plus ms ns) in
  rewrite minusDashAppendsTail (plus ms ns) ns (lessThanPlus ns ms) [I] in
  rewrite plusNMinusN ms ns in Refl

minusNPlusN : (m, n : BiNat) -> GT m n -> plus (minus m n) n = m
minusNPlusN m n =
  induction
    (\k => LT n k -> plus (minus k n) n = k)
    (\k, pk, lt =>
      case lessThanImpliesLTEPred n (succ k) lt of
        LTEEqual _ _ eq =>
          rewrite eq in
          rewrite predOfSucc k in
          rewrite sym $ jPlusIsSucc k in
          rewrite plusNMinusN J k in Refl
        LTELessThan _ _ lt2 =>
          let pk' = pk (replace {P = \z => LT n z} (predOfSucc k) lt2) in
          replace {P = \z => plus (minus (succ z) n) n = succ k} pk' $
          rewrite sym $ jPlusIsSucc (plus (minus k n) n) in
          rewrite plusAssociative J (minus k n) n in
          rewrite plusNMinusN (plus J (minus k n)) n in
          rewrite sym $ plusAssociative J (minus k n) n in
          rewrite pk' in jPlusIsSucc k
    )
    (\lt => absurd (uninhabited lt))
    m

succIntoMinus : (m, n : BiNat) -> GT m n -> succ (minus m n) = minus (succ m) n
succIntoMinus m n lt =
  induction
    (\k => LT n k -> succ (minus k n) = minus (succ k) n)
    (\k, pk, ltSucc =>
      case lessThanImpliesLTEPred n (succ k) ltSucc of
        LTEEqual _ _ eq =>
          rewrite eq in
          rewrite predOfSucc k in
          rewrite sym $ jPlusIsSucc k in
          rewrite plusNMinusN J k in
          rewrite sym $ jPlusIsSucc (plus J k) in
          rewrite plusAssociative J J k in
          rewrite plusNMinusN (J -: O) k in Refl
        LTELessThan _ _ lt =>
          rewrite sym $ minusNPlusN (succ k) n ltSucc in
          rewrite sym $ jPlusIsSucc (plus (minus (succ k) n) n) in
          rewrite plusAssociative J (minus (succ k) n) n in
          rewrite plusNMinusN (plus J (minus (succ k) n)) n in
          rewrite jPlusIsSucc (minus (succ k) n) in
          rewrite plusNMinusN (minus (succ k) n) n in Refl
    )
    (absurd . uninhabited)
    m lt

succNMinusNIsJ : (n : BiNat) -> minus (succ n) n = J
succNMinusNIsJ J         = Refl
succNMinusNIsJ (ns -: O) = rewrite minusLast10 ns ns [] in minusOfItSelf ns [I]
succNMinusNIsJ (ns -: I) =
  rewrite succDashAppendsAcc ns [O] in
  rewrite minusLast01 (succ ns) ns [] (succIsNotJ ns) in
  rewrite predOfSucc ns in
  minusOfItSelf ns [I]

nMinusPredNIsJ : (n : BiNat) -> minus n (pred n) = J
nMinusPredNIsJ J              = Refl
nMinusPredNIsJ (J -: O)       = Refl
nMinusPredNIsJ (ns -: n -: O) = rewrite predDashAppendsAcc (ns -: n) [I] in minusOfItSelf (pred (ns -: n)) [I]
nMinusPredNIsJ (ns -: I)      = rewrite minusLast10 ns ns [] in minusOfItSelf ns [I]

minusIntoPlusLeft : (l, m, n : BiNat) -> GT l n -> minus (plus l m) n = plus (minus l n) m
minusIntoPlusLeft l m n lt =
  induction
    (\k => minus (plus l k) n = plus (minus l n) k)
    (\k, pk =>
      rewrite sym $ plusJIsSucc k in
      rewrite plusAssociative l k J in
      rewrite plusJIsSucc (plus l k) in
      let nLtLPlusK = lessThanTransitive lt (replace (plusSymmetric k l) (lessThanPlus l k)) in
      rewrite sym $ succIntoMinus (plus l k) n nLtLPlusK in
      rewrite pk in
      rewrite sym $ plusJIsSucc (plus (minus l n) k5) in
      rewrite sym $ plusAssociative (minus l n) k J in Refl
    )
    (
      rewrite plusJIsSucc l in
      rewrite plusJIsSucc (minus l n) in
      sym $ succIntoMinus l n lt
    )
    m

minusIntoPlusRight : (l, m, n : BiNat) -> GT m n -> minus (plus l m) n = plus l (minus m n)
minusIntoPlusRight l m n lt =
  rewrite plusSymmetric l m in
  rewrite minusIntoPlusLeft m l n lt in
  plusSymmetric (minus m n) l

minusGreater : (m, n : BiNat) -> LT m n -> (tail : List Bit) -> minus' m n tail = J
minusGreater m              J         lt tail impossible
minusGreater J              (ns -: n) lt tail = Refl
minusGreater (ms -: O)      (ns -: O) (LTAppend ms ns lt O O) tail =
  rewrite minusLast00 ms ns tail in minusGreater ms ns lt (O :: tail)
minusGreater (ms -: I)      (ns -: O) (LTAppend ms ns lt I O) tail =
  rewrite minusLast10 ms ns tail in minusGreater ms ns lt (I :: tail)
minusGreater (ms -: I)      (ns -: I) (LTAppend ms ns lt I I) tail =
  rewrite minusLast11 ms ns tail in minusGreater ms ns lt (O :: tail)
minusGreater (J -: O)       (ns -: I) lt tail = Refl
minusGreater (ms -: m -: O) (ns -: I) (LTAppend (ms -: m) ns lt O I) tail =
  let lt2 = lessThanTransitive (predIsLessThan (ms -: m) (JLT ms m)) lt in
  minusGreater (pred (ms -: m)) ns lt2 (I :: tail)
minusGreater (ms -: m -: O) (ns -: I) (LTLeading (ms -: m) ns eq) tail =
  let lt = replace {P = \z => LT (pred (ms -: m)) z} eq (predIsLessThan (ms -: m) (JLT ms m)) in
  minusGreater (pred (ms -: m)) ns lt (I :: tail)

minusOfSuccs : (m, n : BiNat) -> minus m n = minus (succ m) (succ n)
minusOfSuccs J              J         = Refl
minusOfSuccs J              (ns -: O) = Refl
minusOfSuccs J              (ns -: I) =
  rewrite succDashAppendsAcc ns [O] in
  rewrite minusGreater J (succ ns) (succGreaterThanJ ns) [O] in Refl
minusOfSuccs (J -: O)       J         = Refl
minusOfSuccs (ms -: m -: O) J         =
  rewrite minusDashAppendsTail (ms -: m) J (JLT ms m) [I] in
  rewrite minusJIsPred (ms -: m) in Refl
minusOfSuccs (J -: I)       J         = Refl
minusOfSuccs (ms -: m -: I) J         =
  rewrite succDashAppendsAcc (ms -: m) [O] in
  rewrite minusLast00 (succ (ms -: m)) J [] in
  rewrite minusDashAppendsTail (succ (ms -: m)) J (succGreaterThanJ (ms -: m)) [O] in
  rewrite minusJIsPred (succ (ms -: m)) in
  rewrite predOfSucc (ms -: m) in Refl
minusOfSuccs (ms -: O)      (ns -: O) = rewrite minusLast11 ms ns [] in minusLast00 ms ns []
minusOfSuccs (J -: O)       (ns -: I) =
  rewrite succDashAppendsAcc ns [O] in
  sym $ minusGreater J (succ ns) (succGreaterThanJ ns) [I]
minusOfSuccs (ms -: m -: O) (ns -: I) =
  rewrite succDashAppendsAcc ns [O] in
  case lessThanOrGTE ns (pred (ms -: m)) of
    Left nLTpredm =>
      let succnLTm = replace {P = \z => LT (succ ns) z} (succOfPred (ms -: m) uninhabited) $
                     succKeepsLessThan ns (pred (ms -: m)) nLTpredm in
      rewrite minusDashAppendsTail (pred (ms -: m)) ns nLTpredm [I] in
      rewrite minusDashAppendsTail (ms -: m) (succ ns) succnLTm [I] in
      rewrite minusOfSuccs (pred (ms -: m)) ns in
      rewrite succOfPred (ms -: m) uninhabited in Refl
    Right (LTEEqual (pred (ms -: m)) ns eq) =>
      rewrite sym $ succOfPred (ms -: m) uninhabited in
      rewrite eq in
      rewrite predOfSucc ns in
      rewrite minusOfItSelf ns [I] in
      rewrite minusOfItSelf (succ ns) [I] in Refl
    Right (LTELessThan (pred (ms -: m)) ns predmLTn) =>
      let mLTsuccn = replace {P = \z => LT z (succ ns)} (succOfPred (ms -: m) uninhabited) $
                     succKeepsLessThan (pred (ms -: m)) ns predmLTn in
      rewrite minusGreater (pred (ms -: m)) ns predmLTn [I] in
      rewrite minusGreater (ms -: m) (succ ns) mLTsuccn [I] in Refl
minusOfSuccs (ms -: I)      (ns -: O) =
  rewrite minusLast10 ms ns [] in
  rewrite succDashAppendsAcc ms [O] in
  rewrite minusLast01 (succ ms) ns [] (succIsNotJ ms) in
  rewrite predOfSucc ms in Refl
minusOfSuccs (ms -: I)      (ns -: I) =
  rewrite minusLast11 ms ns [] in
  rewrite succDashAppendsAcc ms [O] in
  rewrite succDashAppendsAcc ns [O] in
  rewrite minusLast00 (succ ms) (succ ns) [] in
  case lessThanOrGTE ns ms of
    Left gt =>
      rewrite minusDashAppendsTail ms ns gt [O] in
      rewrite minusDashAppendsTail (succ ms) (succ ns) (succKeepsLessThan ns ms gt) [O] in
      rewrite minusOfSuccs ms ns in Refl
    Right (LTEEqual ms ns eq) =>
      rewrite eq in
      rewrite minusOfItSelf ns [O] in
      rewrite minusOfItSelf (succ ns) [O] in Refl
    Right (LTELessThan ms ns lt) =>
      rewrite minusGreater ms ns lt [O] in
      rewrite minusGreater (succ ms) (succ ns) (succKeepsLessThan ms ns lt) [O] in Refl

predIntoMinus' : (m, n : BiNat) -> GT m n -> pred (minus m n) = minus (pred m) n
predIntoMinus' m n gt = induction
  (\k => GT k n -> pred (minus k n) = minus (pred k) n)
  (\k, pk, nLTsucck =>
    case lessThanImpliesLTEPred n (succ k) nLTsucck of
      LTEEqual n (pred $ succ k) eq =>
        rewrite eq in
        rewrite predOfSucc k in
        rewrite succNMinusNIsJ k in
        rewrite minusOfItSelf k [] in Refl
      LTELessThan n (pred $ succ k) lt =>
        let nLTk = replace (predOfSucc k) lt in
        rewrite sym $ succIntoMinus k n nLTk in
        rewrite predOfSucc (minus k n) in
        rewrite predOfSucc k in Refl
  )
  (\gt => absurd $ uninhabited gt)
  m gt

predIntoMinus : (m, n : BiNat) -> pred (minus m n) = minus (pred m) n
predIntoMinus m n =
  case lessThanOrGTE n m of
    Left gt =>
      predIntoMinus' m n gt
    Right (LTEEqual m n eq) =>
      rewrite eq in
      rewrite minusOfItSelf n [] in
      case predLessThanEqual n of
        LTEEqual (pred n) n eq2 =>
          rewrite eq2 in
          sym $ minusOfItSelf n []
        LTELessThan (pred n) n lt =>
          rewrite minusGreater (pred n) n lt [] in Refl
    Right (LTELessThan m n lt) =>
      rewrite minusGreater m n lt [] in
      let predmLTn = transLTEandLT (predLessThanEqual m) lt in
      rewrite minusGreater (pred m) n predmLTn [] in Refl

predIntoMinusSucc : (m, n : BiNat) -> pred (minus m n) = minus m (succ n)
predIntoMinusSucc J         n = rewrite jMinusIsJ n in rewrite jMinusIsJ (succ n) in Refl
predIntoMinusSucc (ms -: m) n =
  rewrite predIntoMinus (ms -: m) n in
  rewrite minusOfSuccs (pred (ms -: m)) n in
  rewrite succOfPred (ms -: m) uninhabited in Refl

minusTwiceLeft : (l, m, n : BiNat) -> minus (minus l m) n = minus l (plus m n)
minusTwiceLeft l m n = induction
  (\k => minus (minus l k) n = minus l (plus k n))
  (\k, pk =>
    rewrite sym $ predIntoMinusSucc l k in
    rewrite sym $ jPlusIsSucc k in
    rewrite sym $ plusAssociative J k n in
    rewrite jPlusIsSucc (plus k n) in
    rewrite sym $ predIntoMinusSucc l (plus k n) in
    rewrite sym $ predIntoMinus (minus l k) n in
    rewrite pk in Refl
  )
  (
    rewrite minusJIsPred l in
    rewrite sym $ predIntoMinus l n in
    rewrite jPlusIsSucc n in
    rewrite sym $ predIntoMinusSucc l n in Refl
  )
  m

minusLessThanOriginal : (m, n : BiNat) -> GT m J -> LT (minus m n) m
minusLessThanOriginal m n mgtj = induction
  (\k => LT (minus m k) m)
  (\k, pk =>
    let lte1 = predLessThanEqual (minus m k) in
    replace {P = \z => LT z m} (predIntoMinusSucc m k) (transLTEandLT lte1 pk)
  )
  (replace {P = \z => LT z m} (sym $ minusJIsPred m) (predIsLessThan m mgtj))
  n

multDistributesMinusLeft : (l, m, n : BiNat) -> GT l m -> mult (minus l m) n = minus (mult l n) (mult m n)
multDistributesMinusLeft l m n gt = induction
  (\k => GT k m -> mult (minus k m) n = minus (mult k n) (mult m n))
  (\k, pk, succkGTm =>
    case lessThanImpliesLTEPred m (succ k) succkGTm of
      LTEEqual _ _ eq =>
        rewrite eq in
        rewrite predOfSucc k in
        rewrite succNMinusNIsJ k in
        rewrite plusJIsSucc n in
        rewrite predOfSucc n in
        rewrite multOfSuccLeft k n in
        rewrite plusNMinusN n (mult k n) in Refl
      LTELessThan _ _ lt =>
        let mLTk = replace (predOfSucc k) lt in
        rewrite sym $ succIntoMinus k m mLTk in
        rewrite multOfSuccLeft (minus k m) n in
        rewrite pk mLTk in
        rewrite multOfSuccLeft k n in
        rewrite minusIntoPlusRight n (mult k n) (mult m n) (multNKeepsLT m k mLTk n) in Refl
  )
  (absurd . uninhabited)
  l gt

multDistributesMinusRight : (l, m, n : BiNat) -> GT m n -> mult l (minus m n) = minus (mult l m) (mult l n)
multDistributesMinusRight l m n gt =
  rewrite multSymmetric l (minus m n) in
  rewrite multDistributesMinusLeft m n l gt in
  rewrite multSymmetric l m in
  rewrite multSymmetric l n in Refl

max_stars_repo_name: SekiT/BiNat

max_issues_repo_name: SekiT/BiNat

max_forks_repo_name: SekiT/BiNat


text:
module Language.LSP.CodeAction

public export
data IdrisAction
  = CaseSplit
  | ExprSearch
  | GenerateDef
  | MakeCase
  | MakeClause
  | MakeLemma
  | MakeWith

export
Eq IdrisAction where
  CaseSplit   == CaseSplit   = True
  ExprSearch  == ExprSearch  = True
  GenerateDef == GenerateDef = True
  MakeCase    == MakeCase    = True
  MakeClause  == MakeClause  = True
  MakeLemma   == MakeLemma   = True
  MakeWith    == MakeWith    = True
  _ == _ = False

export
Show IdrisAction where
  show CaseSplit   = "CaseSplit"
  show ExprSearch  = "ExprSearch"
  show GenerateDef = "GenerateDef"
  show MakeCase    = "MakeCase"
  show MakeClause  = "MakeClause"
  show MakeLemma   = "MakeLemma"
  show MakeWith    = "MakeWith"

ext: idr


text:
module Eff

-- The Eff monad, based on http://okmij.org/ftp/Haskell/extensible/more.pdf

data Exists : List a -> a -> Type where
    Here : Exists (x :: xs) x
    There : Exists xs x -> Exists (y :: xs) x

data Eff : List (Type -> Type) -> Type -> Type where
  Pure : a -> Eff xs a
  Bind : {e : Exists xs f} -> f a -> (a -> Eff xs b) -> Eff xs b

(>>=) : Eff xs a -> (a -> Eff xs b) -> Eff xs b
(>>=) (Pure x) f = f x
(>>=) (Bind {e} x g) f = Bind {e} x (\a => (g a) >>= f)

-- State effect
data State : (s : Type) -> Type -> Type where
  Get : State s s
  Put : s -> State s ()

get : {auto e : Exists xs (State s)} -> Eff xs s
get {e} = Bind {e} Get Pure

put : {auto e : Exists xs (State s)} -> s -> Eff xs ()
put {e} s = Bind {e} (Put s) Pure

-- Reader effect
data Reader : (e : Type) -> Type -> Type where
  Ask : Reader e e

ask : {auto e : Exists xs (Reader en)} -> Eff xs en
ask {e} = Bind {e} Ask Pure

-- Interpreters
runState : s -> Eff ((State s) :: xs) a -> Eff xs (a, s)
runState s (Pure x) = Pure (x, s)
runState s (Bind {e = Here} Get f) = runState s (f s)
runState s (Bind {e = Here} (Put s') f) = runState s' (f ())
runState s (Bind {e = (There e')} fa f) = Bind {e = e'} fa (\x => runState s (f x))

runReader : en -> Eff ((Reader en) :: xs) a -> Eff xs a
runReader en (Pure x) = Pure x
runReader en (Bind {e = Here} Ask f) = runReader en (f en)
runReader en (Bind {e = (There e')} fa f) = Bind {e = e'} fa (\x => runReader en (f x))

run : Eff [] a -> a
run (Pure x) = x
run (Bind {e = Here} _ _) impossible
run (Bind {e = (There _)} _ _) impossible

--
example : Eff [State Int, Reader Int] Int
example = do s <- get
             put (s + 1)
             s <- get
             a <- ask
             Pure (s + a)

test : Int
test = (fst . run . runReader 1 . runState 0) example

max_stars_repo_name: vikfret/idris-snippets

max_issues_repo_name: vikfret/idris-snippets

max_forks_repo_name: vikfret/idris-snippets


text:
module OfficialCrashCourse.PTypes
-- Primitive Types

clue: String
clue = "Codes, Life, Universe and Everything"

theAnswer: Int
theAnswer = 42

me: Char
me = 'u'

thisIsFalse: Bool
thisIsFalse = True

max_stars_repo_name: umbrela-academy/idrusti

max_issues_repo_name: umbrela-academy/idrusti

max_forks_repo_name: umbrela-academy/idrusti


text:
||| Matrix operations with vector space dimensionalities enforced
||| at the type level. Uses operations from classes in `Control.Algebra`
||| and `Control.Algebra.VectorSpace`.
module Data.Matrix.Algebraic

import public Control.Algebra
import public Control.Algebra.VectorSpace
import public Control.Algebra.NumericInstances

import public Data.Matrix

%default total

infixr 2 <:>  -- vector inner product
infixr 2 ><   -- vector outer product
infixr 2 <<>> -- matrix commutator
infixr 2 >><< -- matrix anticommutator
infixl 3 <\>  -- row times a matrix
infixr 4 </>  -- matrix times a column
infixr 5 <>   -- matrix multiplication
infixr 7 \&\  -- vector tensor product
infixr 7 <&>  -- matrix tensor product

-----------------------------------------------------------------------
--               Vectors as members of algebraic classes
-----------------------------------------------------------------------

instance Semigroup a => Semigroup (Vect n a) where
  (<+>)= zipWith (<+>)

instance Monoid a => Monoid (Vect n a) where
  neutral = replicate _ neutral

instance Group a => Group (Vect n a) where
  inverse = map inverse

instance AbelianGroup a => AbelianGroup (Vect n a) where {}

instance Ring a => Ring (Vect n a) where
  (<.>) = zipWith (<.>)

instance RingWithUnity a => RingWithUnity (Vect n a) where
  unity = replicate _ unity

instance RingWithUnity a => Module a (Vect n a) where
  (<#>) r = map (r <.>)

instance RingWithUnity a => Module a (Vect n (Vect l a)) where
  (<#>) r = map (r <#>)
-- should be Module a b => Module a (Vect n b), but results in 'overlapping instance'

-----------------------------------------------------------------------
--                        (Ring) Vector functions
-----------------------------------------------------------------------

||| Inner product of ring vectors
(<:>) : Ring a => Vect n a -> Vect n a -> a
(<:>) w v = foldr (<+>) neutral (zipWith (<.>) w v)

||| Tensor multiply (⊗) ring vectors
(\&\) : Ring a => Vect n a -> Vect m a -> Vect (n * m) a
(\&\) {n} {m} v w = zipWith (<.>) (oextend m v) (orep n w) where
  orep : (n : Nat) -> Vect m a -> Vect (n * m) a
  orep n v = concat $ replicate n v
  oextend : (n : Nat) -> Vect k a -> Vect (k * n) a
  oextend n w = concat $ map (replicate n) w

||| Standard basis vector with one nonzero entry, ring data type and vector-length unfixed
basis : RingWithUnity a => (Fin d) -> Vect d a
basis i = replaceAt i unity neutral

-----------------------------------------------------------------------
--                         Ring Matrix functions
-----------------------------------------------------------------------

||| Matrix times a column vector
(</>) : Ring a => Matrix n m a -> Vect m a -> Vect n a
(</>) m v = map (v <:>) m

||| Matrix times a row vector
(<\>) : Ring a => Vect n a -> Matrix n m a -> Vect m a
(<\>) r = map (r <:>) . transpose

||| Matrix multiplication
(<>) : Ring a => Matrix n k a ->
                 Matrix k m a ->
                 Matrix n m a
(<>) m1 m2 = map (<\> m2) m1

||| Tensor multiply (⊗) for ring matrices
(<&>) : Ring a => Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) (w1 * w2) a
(<&>) m1 m2 = zipWith (\&\) (stepOne m1 m2) (stepTwo m1 m2) where
  stepOne : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w1 a
  stepOne {h2} m1 m2 = concat $ map (replicate h2) m1
  stepTwo : Matrix h1 w1 a -> Matrix h2 w2 a -> Matrix (h1 * h2) w2 a
  stepTwo {h1} m1 m2 = concat $ replicate h1 m2

||| Outer product between ring vectors
(><) : Ring a => Vect n a -> Vect m a -> Matrix n m a
(><) x y = col x <> row y

||| Matrix commutator
(<<>>) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
(<<>>) m1 m2 = (m1 <> m2) <-> (m2 <> m1)

||| Matrix anti-commutator
(>><<) : Ring a => Matrix n n a -> Matrix n n a -> Matrix n n a
(>><<) m1 m2 = (m1 <> m2) <+> (m2 <> m1)

||| Identity matrix
Id : RingWithUnity a => Matrix d d a
Id = map (\n => basis n) (fins _)

||| Square matrix from diagonal elements
diag_ : Monoid a => Vect n a -> Matrix n n a
diag_ = zipWith (\f => \x => replaceAt f x neutral) (fins _)

||| Combine two matrices to make a new matrix in block diagonal form
blockDiag : Monoid a => Matrix n n a -> Matrix m m a -> Matrix (n+m) (n+m) a
blockDiag g h = map (++ replicate _ neutral) g ++ map ((replicate _ neutral) ++) h

-----------------------------------------------------------------------
--                           Determinants
-----------------------------------------------------------------------

||| Alternating sum
altSum : Group a => Vect n a -> a
altSum (x::y::zs) = (x <-> y) <+> altSum zs
altSum [x]        = x
altSum []         = neutral

||| Determinant of a 2-by-2 matrix
det2 : Ring a => Matrix 2 2 a -> a
det2 [[x1,x2],[y1,y2]] = x1 <.> y2 <-> x2 <.> y1

||| Determinant of a square matrix
det : Ring a => Matrix (S (S n)) (S (S n)) a -> a
det {n} m = case n of
  Z     => det2 m
  (S k) => altSum . map (\c => indices FZ c m <.> det (subMatrix FZ c m))
         $ fins (S (S (S k)))

-----------------------------------------------------------------------
--                      Matrix Algebra Properties
-----------------------------------------------------------------------

-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module Test.Chapter4

import Data.Vect
import Test
import Exercises.Chapter4

%access public export

testOneTwo : IO ()
testOneTwo = assertEq [1..9] (treeToList (listToTree [4,1,8,7,2,3,9,5,6]))

testMaxMaybe1 : IO ()
testMaxMaybe1 = assertEq (Just 5) (maxMaybe (Just 4) (Just 5))

testMaxMaybe2 : IO ()
testMaxMaybe2 = assertEq (Just 4) (maxMaybe (Just 4) Nothing)

testMaxMaybe3 : IO ()
testMaxMaybe3 = assertEq (Just 5) (maxMaybe Nothing (Just 5))

rectangle : Picture
rectangle = Primitive (Rectangle 20 10)

circle : Picture
circle = Primitive (Circle 5)

triangle : Picture
triangle = Primitive (Triangle 10 10)

test_picture : Picture
test_picture = Combine (Translate 5 5 rectangle)
                       (Combine (Translate 35 5 circle)
                                (Translate 15 25 triangle))

testBiggestTriangle1 : IO ()
testBiggestTriangle1 =
  assertEq (Just (picture_area triangle)) (biggestTriangle test_picture)

testSumEntries1 : IO ()
testSumEntries1 = assertEq (Just 10) (sumEntries 2 [1,2,3,4] [5,6,7,8])

testSumEntries2 : IO ()
testSumEntries2 = assertEq Nothing (sumEntries 4 [1,2,3,4] [5,6,7,8])

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
> module SequentialDecisionProblems.NonDeterministicDefaults

> import Data.List
> import Data.List.Quantifiers

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.Utils

> import List.Operations
> import List.Properties

> %default total
> %auto_implicits off

In non-deterministic SDPs, |M = List|:

> SequentialDecisionProblems.CoreTheory.M =
>   List

Thus, |M| is a functor:

> SequentialDecisionProblems.CoreTheory.fmap =
>   List.Operations.fmap

, |M| is a monad:

> SequentialDecisionProblems.Utils.ret =
>   List.Operations.ret

> SequentialDecisionProblems.Utils.bind =
>   List.Operations.bind

Moreover, |M| is a container monad

> SequentialDecisionProblems.CoreTheory.Elem =
>   Data.List.Elem

> SequentialDecisionProblems.CoreTheory.NotEmpty =
>   List.Operations.NonEmpty

> SequentialDecisionProblems.CoreTheory.All =
>   Data.List.Quantifiers.All

> SequentialDecisionProblems.CoreTheory.elemNotEmptySpec0 =
>   List.Properties.elemNonEmptySpec0

> SequentialDecisionProblems.CoreTheory.elemNotEmptySpec1 =
>   List.Properties.elemNonEmptySpec1

> SequentialDecisionProblems.CoreTheory.tagElem =
>   List.Operations.tagElem

> SequentialDecisionProblems.CoreTheory.allElemSpec0 =
>   List.Properties.containerMonadSpec3

and |All| and |NotEmpty| are finite and decidable:

> SequentialDecisionProblems.Utils.finiteAll =
>   List.Properties.finiteAll

> SequentialDecisionProblems.Utils.finiteNotEmpty =
>   List.Properties.finiteNonEmpty

> SequentialDecisionProblems.Utils.decidableAll =
>   List.Properties.decidableAll

> SequentialDecisionProblems.Utils.decidableNotEmpty =
>   List.Properties.decidableNonEmpty

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Data.Mod

import Control.Algebra
import Data.Fin

%default total
%access public export

||| Modular arithmetic
data Mod : (n : Nat) -> Type where
  MkMod : (fin : Fin n) -> Mod n

implementation Eq (Mod n) where
  (==) (MkMod x) (MkMod y) = x == y

implementation Cast (Mod n) Nat where
  cast (MkMod x) = cast x

implementation Cast (Mod n) (Fin n) where
  cast (MkMod x) = x

implementation Ord (Mod (S n)) where
  compare (MkMod x) (MkMod y) = compare x y

implementation MinBound (Mod (S n)) where
  minBound = MkMod FZ

implementation MaxBound (Mod (S n)) where
  maxBound = MkMod last

natToMod : Nat -> Mod (S n)
natToMod {n=(S m)} x =
  MkMod (finMod (modNatNZ x (S (S m)) (uninhabited . sym))) where
    finMod : Nat -> Fin (S k)
    finMod Z = FZ
    finMod {k=S k'} (S l) = FS (finMod {k=k'} l)
    finMod _ = FZ
natToMod _ = MkMod FZ

modToInteger : Mod n -> Integer
modToInteger (MkMod x) = finToInteger x

modToNat : Mod n -> Nat
modToNat (MkMod x) = finToNat x

rotate : Fin (S n) -> Fin (S n)
rotate {n=Z} _ = FZ
rotate {n = S m} FZ = FS FZ
rotate {n = S m} (FS g) = if (FS g) == last
                          then FZ
                          else FS (rotate g)

private
modplus : Mod (S n) -> Mod (S n) -> Mod (S n)
modplus (MkMod left) (MkMod right) = MkMod (spin left right)
  where spin : Fin (S n') -> Fin (S n) -> Fin (S n)
        spin FZ right = right
        spin {n' = Z} left right = rotate right
        spin {n' = S m} (FS left) right = rotate (spin left right)

implementation Semigroup (Mod (S n)) where
  (<+>) = modplus

implementation Monoid (Mod (S n)) where
  neutral = MkMod FZ

implementation Group (Mod (S n)) where
  inverse (MkMod FZ) = MkMod FZ
  inverse {n=n} (MkMod m) = natToMod ((S n) `minus` (finToNat m))

implementation Num (Mod (S n)) where
  (+) = modplus
  (*) (MkMod a) (MkMod b) = fromInteger (finToInteger a * finToInteger b)
  fromInteger {n=n} x = if x < 0
                        then inverse (natToMod (modNatNZ (fromInteger (-x)) (S n) (uninhabited . sym)))
                        else natToMod (modNatNZ (fromInteger x) (S n) (uninhabited . sym))

implementation Neg (Mod (S n)) where
  negate = const (MkMod FZ)
  (-) = (<->)

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


text:
||| Immutable strings of raw bytes.
module Data.ByteString

import public Data.ByteString.Internal

-- import Data.Buffer
-- import Data.So
-- import System.File
-- import System.File.Support
--
-- %default total
--
-- --------------------------------------------------------------------------------
-- --          FFI
-- --------------------------------------------------------------------------------
--
-- ||| Immutable wrapper around `Buffer`.
-- export
-- record Buf where
--   constructor MkBuf
--   buf : Buffer
--
-- %foreign "scheme:blodwen-buffer-getbyte"
--          "RefC:getBufferByte"
--          "node:lambda:(buf,offset)=>buf.readUInt8(offset)"
-- prim__getBits8 : Buffer -> (offset : Bits32) -> Bits8
--
-- %foreign "scheme:blodwen-new-buffer"
--          "RefC:newBuffer"
--          "node:lambda:s=>Buffer.alloc(s)"
-- prim__newBuffer : Bits32 -> PrimIO Buffer
--
-- %foreign "scheme:blodwen-buffer-setbyte"
--          "RefC:setBufferByte"
--          "node:lambda:(buf,offset,value)=>buf.writeUInt8(value, offset)"
-- prim__setBits8 : Buffer -> (offset : Bits32) -> (val : Bits8) -> PrimIO Int
--
-- %foreign support "idris2_readBufferData"
--          "node:lambda:(f,b,l,m) => require('fs').readSync(f.fd,b,l,m)"
-- prim__readBufferData :  FilePtr
--                      -> Buffer
--                      -> (offset : Bits32)
--                      -> (maxbytes : Bits32) -> PrimIO Int
--
-- --------------------------------------------------------------------------------
-- --          API
-- --------------------------------------------------------------------------------
--
-- public export
-- record ByteString where
--   constructor MkBS
--   buf    : Buf
--   offset : Bits32
--   length : Bits32
--
-- export
-- toList : ByteString -> List Bits8
-- toList (MkBS (MkBuf buf) o l) = go Nil l
--   where go : List Bits8 -> Bits32 -> List Bits8
--         go bs 0 = bs
--         go bs n =
--           let ix = assert_smaller n (n-1)
--            in go (prim__getBits8 buf (o + ix) :: bs) ix
--
-- export
-- empty : ByteString
-- empty = MkBS (MkBuf . unsafePerformIO . primIO $ prim__newBuffer 0) 0 0
--
-- export
-- fromList : List Bits8 -> ByteString
-- fromList ns =
--   let len = cast {to = Bits32} $ length ns
--    in MkBS (MkBuf . unsafePerformIO $ go' len) 0 len
--   where go : List Bits8 -> Bits32 -> Buffer -> PrimIO Buffer
--         go []        _  buf w = MkIORes buf w
--         go (b :: bs) ix buf w =
--           case prim__setBits8 buf ix b w of
--             -- this is a hack: Without this (completely useless) pattern
--             -- match, the call to `prim__setBits8` is erased and ignored
--             MkIORes 0 w2 => go bs (ix+1) buf w2
--             MkIORes _ w2 => go bs (ix+1) buf w2
--
--         go' : Bits32 -> IO Buffer
--         go' l = do
--           buf <- fromPrim $ prim__newBuffer l
--           fromPrim $ go ns 0 buf
--
-- export
-- Show ByteString where
--   showPrec p bs = showCon p "fromList" $ showArg (toList bs)
--
-- export
-- getBits8 : Bits32 -> ByteString -> Maybe Bits8
-- getBits8 x (MkBS (MkBuf bf) o l) =
--   if x < l then Just $ prim__getBits8 bf (o + x) else Nothing
--
-- export
-- bits8 :  (ix : Bits32)
--       -> (bs : ByteString)
--       -> {auto 0 _ : So (ix < bs.length)}
--       -> Bits8
-- bits8 x (MkBS (MkBuf bf) o l) = prim__getBits8 bf (o + x)
--
-- --------------------------------------------------------------------------------
-- --          Reading and Writing from and to Files
-- --------------------------------------------------------------------------------
--
-- export
-- readChunk : HasIO io => Bits32 -> File -> io (Either FileError ByteString)
-- readChunk max (FHandle h) = do
--   Just buf <- newBuffer (cast max) | Nothing => pure (Left FileReadError)
--   read     <- primIO (prim__readBufferData h buf 0 max)
--   if read >= 0
--      then pure (Right $ MkBS (MkBuf buf) 0 (cast read))
--      else pure (Left FileReadError)
--
-- export
-- write : HasIO io => File -> ByteString -> io (Either FileError ())
-- write h (MkBS (MkBuf buf) o l) = writeBufferData h buf (cast o) (cast l)
--
-- --------------------------------------------------------------------------------
-- --          Utilities (Lots of stuff still missing)
-- --------------------------------------------------------------------------------
--
-- export
-- splitAt : Bits32 -> ByteString -> (ByteString,ByteString)
-- splitAt n (MkBS buf offset l) =
--   if n >= l
--      then (MkBS buf offset l, empty)
--      else (MkBS buf offset n, MkBS buf (offset + n) (l - n))
--
-- export
-- break : Bits8 -> ByteString -> (ByteString,ByteString)
-- break b bs@(MkBS bf o l) = go 0
--   where go : Bits32 -> (ByteString,ByteString)
--         go n = if n < l
--                   then if prim__getBits8 bf.buf (o + n) == b
--                           then (MkBS bf o n, MkBS bf (o + n) (l - n))
--                           else go (assert_smaller n (n+1))
--                   else (bs,empty)


text:
module Node.Async.FileSystem

import Node.Free.FileSystem
import Control.Monad.AsyncJS_IO
import Data.JSError

%lib Node "fs"
%access public export

toPtr : (JSError -> JS_IO ()) -> (Ptr -> JS_IO ())
toPtr errorCb = (\e => errorCb $ MkJSError e)

writeFile' : String -> String -> (JSError -> JS_IO ()) -> (() -> JS_IO ()) -> JS_IO ()
writeFile' path contents error success =
  foreign FFI_JS "fs.writeFile(%0, %1, function(err, data) { %3(data) })"
    (String -> String -> JsFn (Ptr -> JS_IO ()) -> JsFn (() -> JS_IO ()) -> JS_IO ()) path contents (MkJsFn $ toPtr error) (MkJsFn success)

writeFileAsync : String -> String -> AsyncJS_IO ()
writeFileAsync path contents = MkAsync $ \e => \f => writeFile' path contents (\x => e x) (\x => f x)

readFile' : String -> (JSError -> JS_IO ()) -> (String -> JS_IO ()) -> JS_IO ()
readFile' path error success = foreign FFI_JS "fs.readFile(%0, 'utf8', function(err, data) { err ? %1(err) : %2(data) })"
  (String -> JsFn (Ptr -> JS_IO ()) -> JsFn (String -> JS_IO ()) -> JS_IO ()) path (MkJsFn $ toPtr error) (MkJsFn success)

readFileAsync : String -> AsyncJS_IO String
readFileAsync path = MkAsync $ \e => \f => readFile' path (\x => e x) (\s => f s)

interpret : FileSystemF a -> AsyncJS_IO a
interpret (WriteFile filePath contents next) = writeFileAsync filePath contents *> pure next
interpret (ReadFile filePath nextFn) = do
  contents <- readFileAsync filePath
  pure (nextFn contents)

max_stars_repo_name: Risto-Stevcev/idris-node-fs

max_issues_repo_name: Risto-Stevcev/idris-node-fs

max_forks_repo_name: Risto-Stevcev/idris-node-fs


text:
module Data.Prim.Int

import public Control.WellFounded
import public Data.DPair
import public Data.Prim.Ord
import public Algebra.Solver.Ring
import Syntax.PreorderReasoning

%default total

unsafeRefl : a === b
unsafeRefl = believe_me (Refl {x = a})

--------------------------------------------------------------------------------
--          (<)
--------------------------------------------------------------------------------

||| Witness that `m < n === True`.
export
data (<) : (m,n : Int) -> Type where
  LT : {0 m,n : Int} -> (0 prf : (m < n) === True) -> m < n

||| Contructor for `(<)`.
|||
||| This can only be used in an erased context.
export %hint
0 mkLT : (0 prf : (m < n) === True) -> m < n
mkLT = LT

||| Extractor for `(<)`.
|||
||| This can only be used in an erased context.
export
0 runLT : m < n -> (m < n) === True
runLT (LT prf) = prf

||| We don't trust values of type `(<)` too much,
||| so we use this when creating magical results.
export
strictLT : (0 p : m < n) -> Lazy c -> c
strictLT (LT prf) x = x

--------------------------------------------------------------------------------
--          Aliases
--------------------------------------------------------------------------------

||| Flipped version of `(<)`.
public export
0 (>) : (m,n : Int) -> Type
m > n = n < m

||| `m <= n` mean that either `m < n` or `m === n` holds.
public export
0 (<=) : (m,n : Int) -> Type
m <= n = Either (m < n) (m === n)

||| Flipped version of `(<=)`.
public export
0 (>=) : (m,n : Int) -> Type
m >= n = n <= m

||| `m /= n` mean that either `m < n` or `m > n` holds.
public export
0 (/=) : (m,n : Int) -> Type
m /= n = Either (m < n) (m > n)

--------------------------------------------------------------------------------
--          Order
--------------------------------------------------------------------------------

0 ltNotEQ : m < n -> Not (m === n)
ltNotEQ x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and EQ")

0 ltNotGT : m < n -> Not (n < m)
ltNotGT x = strictLT x $ assert_total (idris_crash "IMPOSSIBLE: LT and GT")

0 eqNotLT : m === n -> Not (m < n)
eqNotLT = flip ltNotEQ

export
comp : (m,n : Int) -> Trichotomy (<) m n
comp m n = case prim__lt_Int m n of
  0 => case prim__eq_Int m n of
    0 => GT (ltNotGT $ LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (LT unsafeRefl)
    x => EQ (eqNotLT unsafeRefl) (unsafeRefl) (eqNotLT unsafeRefl)
  x => LT (LT unsafeRefl) (ltNotEQ $ LT unsafeRefl) (ltNotGT $ LT unsafeRefl)

export
Total Int (<) where
  trichotomy   = comp
  transLT p q  = strictLT p $ strictLT q $ LT unsafeRefl

--------------------------------------------------------------------------------
--          Arithmetics
--------------------------------------------------------------------------------

||| Safe division.
export %inline
sdiv : (n,d : Int) -> (0 prf : d /= 0) => Int
sdiv n d = n `div` d

||| Safe modulo.
export %inline
smod : (n,d : Int) -> (0 prf : d /= 0) => Int
smod n d = n `mod` d


text:
module DPairQuoteProblem

import Language.Reflection

%default total

extract : Type -> Elab Unit
extract ty = logTerm "debug.elab" 0 "type" !(quote ty)

%macro
extract' : Type -> Elab Unit
extract' = extract -- logTerm "debug.elab" 0 "type" !(quote ty)

%language ElabReflection

-----------------------------
--- One-parameter example ---
-----------------------------

namespace OneParameter

  data Y : Nat -> Type where
    Y0 : Y 0
    Y1 : Y 1

  %runElab logMsg "debug.elab" 0 "----------------------"
  namespace NonInlined

    X : Type
    X = (n : Nat ** Y n)

    %runElab extract X

    v : Unit
    v = %runElab extract X

    u : Unit
    u = extract' X

  %runElab logMsg "debug.elab" 0 "----------------------"
  namespace Inlined

    -- When there are not so many stuff inside the dpair, all is okay being inlined

    %runElab extract (n : Nat ** Y n)

    v : Unit
    v = %runElab extract (n : Nat ** Y n)

    u : Unit
    u = extract' (n : Nat ** Y n)

-----------------------------
--- Two-parameter example ---
-----------------------------

namespace TwoParameters

  data Y : Nat -> Type -> Type where
    Y0 : Y 0 Int
    Y1 : Y 1 Nat

  %runElab logMsg "debug.elab" 0 "----------------------"
  namespace NotInlined

    -- The following two elaboration runnings log the same result:

    X : Type
    X = (n : Nat ** x : Type ** Y n x)

    %runElab extract X

    v : Unit
    v = %runElab extract X

    u : Unit
    u = extract' X

  %runElab logMsg "debug.elab" 0 "----------------------"
  namespace Inlined

    -- The following two elaboration runnings log different results,
    -- but we expect them to be the same as above.

    %runElab extract (n : Nat ** x : Type ** Y n x)

    v : Unit
    v = %runElab extract (n : Nat ** x : Type ** Y n x)

    u : Unit
    u = extract' (n : Nat ** x : Type ** Y n x)

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Main

main : IO ()
main = putStrLn "Hello, world. Again."

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

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

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


text:
-- --------------------------------------------------------------- [ Graph.idr ]
-- Module    : Graph.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Testing Stacks using silly stupid tests
module Data.AVL.Test.Graph

import Test.Unit

import Data.AVL.Graph

%access export
-- ------------------------------------------------------------ [ Construction ]

towns : List String
towns = ["Munchen",
         "Augsburg",
         "Nurnburg",
         "Stuttgart",
         "Kassel",
         "Erfurt",
         "Wurzburg",
         "Karlsruhe",
         "Frankfurt",
         "Mannheim"]

links : List (String, String, Maybe Int)
links = [("Frankfurt"  ,"Mannheim" , Just 85),
         ("Frankfurt"  ,"Wurzburg"  , Just 217),
         ("Frankfurt"  ,"Kassel"    , Just 173),
         ("Mannheim"   ,"Karlsruhe" , Just 80),
         ("Karlsruhe"  ,"Augsburg"  , Just 250),
         ("Augsburg"   ,"Munchen"   , Just 84),
         ("Wurzburg"   ,"Erfurt"    , Just 186),
         ("Wurzburg"   ,"Nurnburg"  , Just 167),
         ("Nurnburg"   ,"Stuttgart" , Just 183),
         ("Nurnburg"   ,"Munchen"   , Just 167),
         ("Kassel"     ,"Munchen"   , Just 502)]

g : Graph String Int
g = with List buildG towns links

-- ---------------------------------------------------------------- [ Updating ]
partial
testBuild : IO Bool
testBuild = genericTest
    (Just "Insert")
    [ hasValue "Frankfurt" g
    , hasValue "Kassel" g
    , hasValue "Dortmund" g
    , hasValue "Berlin" g]
    [True,True,False,False]
    (==)

partial
testSuccs : IO Bool
testSuccs = genericTest
    (Just "Succs")
    (getSuccs "Wurzburg" g)
    [2,5]
    (==)

partial
testEdges : IO Bool
testEdges = genericTest
    (Just "Edges")
    ([getEdgesByID 0 g, getEdges "Kassel" g])
    ([Nil, [(0, Just 502)]])
    (==)

partial
testLeafs : IO Bool
testLeafs = genericTest
  (Just "Get Leaf Nodes")
  (catMaybes $ map (\x => getValueByID x g) (leafNodes g))
  ["Erfurt", "Stuttgart", "Munchen"]
  (\x,y => sort x == sort y)

partial
testRoots : IO Bool
testRoots = genericTest
  (Just "Get Root Nodes")
  (getValuesByID (rootNodes g) g)
  ["Frankfurt"]
  (\x,y => sort x == sort y)

partial
testDiscon : IO Bool
testDiscon = genericTest
  (Just "Disconnected")
  (isDisconnected g)
  False
  (==)

partial
testDiscon2 : IO Bool
testDiscon2 = genericTest
  (Just "Disconnected")
  (isDisconnected (addNode "Aachen" g))
  True
  (==)

partial
runTest : IO ()
runTest = do
    putStrLn "Testing Graph"
    putStrLn infoLine
    NonReporting.runTests [
        testBuild
      , testSuccs
      , testEdges
      , testLeafs
      , testRoots
      , testDiscon
      , testDiscon2
    ]

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

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module Motivation.Exfer

import Data.Vect

-- NOTE totality check, gentlemen's agreement when defining proofs in Haskell
%default total

-- implement using Idris interactive features
-- note increase precision of this type over List

mapV : (a -> b) -> Vect m a -> Vect m b

appendV : Vect n a -> Vect m a -> Vect (n + m) a

---
-- possible rearrangements

rL : List a -> List a

rV : Vect n a -> Vect n a


text:
-- the commented-out cases are still wrong,
-- but fixing them as well would make other tests fail for mysterious reasons
-- see https://github.com/edwinb/Idris2/pull/281
main : IO ()
main = do
  printLn $ 3
  printLn $ 4.2
  printLn $ "1.2"

  printLn $ cast {to = Int} 4.8
  printLn $ cast {to = Integer} 1.2
  printLn $ cast {to = String} 2.7

  -- printLn $ cast {to = Int} "1.2"
  -- printLn $ cast {to = Integer} "2.7"
  printLn $ cast {to = Double} "5.9"

  printLn $ (the Int 6 `div` the Int 3)
  printLn $ (the Integer 6 `div` the Integer 3)
  -- printLn $ (cast {to = Int} "6.6" `div` cast "3.9")
  -- printLn $ (cast {to = Integer} "6.6" `div` cast "3.9")


text:
zeroNotSucc : (0 = S k) -> Void
zeroNotSucc Refl impossible

succNotZero : (S k = 0) -> Void
succNotZero Refl impossible

noRec : (contra : (k = j) -> Void) -> (S k = S j) -> Void
noRec contra Refl = contra Refl

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Dec (num1 = num2)
checkEqNat Z Z = Yes Refl
checkEqNat Z (S k) = No zeroNotSucc
checkEqNat (S k) Z = No succNotZero
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Yes prf => Yes (cong prf)
                              No contra => No (noRec contra)


text:
module Main

import CommandLineParser
import Lightyear
import Lightyear.Combinators
import Lightyear.Core
import Lightyear.Char
import Lightyear.Strings
import System

%access public export

record Arguments where
    constructor MkArguments
    input: List String
    output: List String
    num: Nat

fromDigits : List (Fin 10) -> Nat
fromDigits = foldl (\a, b => 10 * a + cast b) 0

parseNat : Parser Nat
parseNat = do digits <- some digit
              eof
              pure $ fromDigits digits

argumentsParser : Monad m => ParserT (List String) m Arguments
argumentsParser = do
    -- Parse a list of string parameters
    i <- (key "-i" *> (manyTill anyToken (key "-o"))) <?> "input"
    -- Parse another list of string parameters
    o <- manyTill anyToken (key "-n") <?> "output"
    -- Parse a single typed value
    n <- (value parseNat) <* eof <?> "num"
    pure $ MkArguments i o n

main : IO ()
main = do
    (path :: args) <- getArgs
    case (parseList argumentsParser args) of
        Left error => do
            putStrLn $ "Error: " ++ error
            exit 1
        Right (MkArguments i o n) => do
            putStrLn "Success:"
            putStrLn $ "input: " ++ (show i)
            putStrLn $ "output: " ++ (show o)
            putStrLn $ "num: " ++ (show n)


text:
module UninhabitedRec

import Data.Nat
import Data.List.Elem

ff : Uninhabited (a, b) => Int
ff = 4

callFGood : Int
callFGood = ff {b = (Left 4 = Right 4)} {a = 5 = 5}

------------------

data Lookup : a -> List (a, b) -> Type where
  Here : (y : b) -> Lookup x $ (x, y)::xys
  There : (0 _ : Uninhabited $ x === z) => Lookup z xys -> Lookup z $ (x, y)::xys

fff : (xs : List (Nat, String)) -> (n : Nat) -> (0 _ : Lookup n xs) => String

xxs : List (Nat, String)
xxs = [(1, "one"), (2, "two"), (4, "four")]

lkup1Good : String
lkup1Good = fff xxs 1

lkup2Good : String
lkup2Good = fff xxs 2

lkup3Bad : String
lkup3Bad = fff xxs 3

------------------

data Uniq : Type -> Type

toList : Uniq a -> List a

data Uniq : Type -> Type where
  Nil  : Uniq a
  (::) : (x : a) -> (xs : Uniq a) -> Uninhabited (Elem x $ toList xs) => Uniq a

toList [] = []
toList (x::xs) = x :: toList xs

uniqGood : Uniq Nat
uniqGood = [1, 2, 3]

uniqBad : Uniq Nat
uniqBad = [1, 2, 1]


text:
||| This module provides a helper to implement a `DecEq`, `Eq`, and `Ord`
||| instances, which are required for a type that is used as a key in a `Record`.
||| You only have to provide a `InjectiveKey` interface, and it will build
||| the required instances on its own.
||| Most of the time, you will end up writing O(n) statements instead of O(n^2).
module Flexidisc.InjectiveKey

import Decidable.Order

%default total
%access public export

||| Proof that `f` is an injection
IsInjection : (a : Type) -> (f : a -> b) -> Type
IsInjection a f = (x,y : a) -> f x = f y -> x = y

||| Decide equality via an injection
decEqViaInjection : DecEq b =>
                    (toInj : a -> b) -> (isInj : IsInjection a toInj) ->
                    (x,y : a) -> Dec (x = y)
decEqViaInjection f isInj x y with (decEq (f x) (f y))
  | Yes prf   = Yes $ isInj x y prf
  | No contra = No  $ contra . cong

||| Build an injection out of a function,
||| an inverse function for the target elements, and an
||| equality proof.
retrieveInjection : (func : a -> b) -> (cnuf : b -> a) ->
                    ((x : a) -> cnuf (func x) = x) ->
                    IsInjection a func
retrieveInjection func cnuf prf x y funcEq =
  rewrite sym (prf x) in
  rewrite sym (prf y) in cong funcEq

||| Comparaison thanks to an injection function
compareInj : Ord b => (a -> b) -> (x,y : a) -> Ordering
compareInj f x y = compare (f x) (f y)

||| Interface that provides a default implementation of typeclasses required to
||| be a record key.
interface (DecEq a, Eq a, Ord a,
           DecEq b, Eq b, Ord b) => InjectiveKey a b | a where

  implementation DecEq a where
    decEq x y = let
      isInj = retrieveInjection inj ret inv
      in decEqViaInjection inj isInj x y

  implementation Eq a where
    (==) x y = inj x == inj y

  implementation Ord a where
    compare x y = compareInj inj x y
    (<) x y  = compareInj inj x y == LT
    (>) x y  = compareInj inj x y == GT
    (<=) x y = compareInj inj x y /= GT
    (>=) x y = compareInj inj x y /= LT
    min x y  = if compareInj inj x y == GT then y else x
    max x y  = if compareInj inj x y == LT then y else x

  inj : a -> b
  ret : b -> a
  inv : (x : a) -> ret (inj x) = x

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Compiler.Scheme.Chez

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Inline
import Compiler.Scheme.Common

import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Name
import Core.Options
import Core.TT
import Utils.Hex
import Utils.Path

import Data.List
import Data.List1
import Data.Maybe
import Data.NameMap
import Data.Strings
import Data.Vect

import System
import System.Directory
import System.File
import System.Info

%default covering

pathLookup : IO String
pathLookup
    = do path <- getEnv "PATH"
         let pathList = forget $ split (== pathSeparator) $ fromMaybe "/usr/bin:/usr/local/bin" path
         let candidates = [p ++ "/" ++ x | p <- pathList,
                                           x <- ["chez", "chezscheme9.5", "scheme", "scheme.exe"]]
         e <- firstExists candidates
         pure $ fromMaybe "/usr/bin/env scheme" e

findChez : IO String
findChez
    = do Just chez <- getEnv "CHEZ" | Nothing => pathLookup
         pure chez

-- Given the chez compiler directives, return a list of pairs of:
--   - the library file name
--   - the full absolute path of the library file name, if it's in one
--     of the library paths managed by Idris
-- If it can't be found, we'll assume it's a system library and that chez
-- will thus be able to find it.
findLibs : {auto c : Ref Ctxt Defs} ->
           List String -> Core (List (String, String))
findLibs ds
    = do let libs = mapMaybe (isLib . trim) ds
         traverse locate (nub libs)
  where
    isLib : String -> Maybe String
    isLib d
        = if isPrefixOf "lib" d
             then Just (trim (substr 3 (length d) d))
             else Nothing

escapeString : String -> String
escapeString s = pack $ foldr escape [] $ unpack s
  where
    escape : Char -> List Char -> List Char
    escape '"' cs = '\\' :: '\"' :: cs
    escape '\\' cs = '\\' :: '\\' :: cs
    escape c   cs = c :: cs

schHeader : String -> List String -> String
schHeader chez libs
  = (if os /= "windows" then "#!" ++ chez ++ " --script\n\n" else "") ++
    "; @generated\n" ++
    "(import (chezscheme))\n" ++
    "(case (machine-type)\n" ++
    "  [(i3le ti3le a6le ta6le) (load-shared-object \"libc.so.6\")]\n" ++
    "  [(i3osx ti3osx a6osx ta6osx) (load-shared-object \"libc.dylib\")]\n" ++
    "  [(i3nt ti3nt a6nt ta6nt) (load-shared-object \"msvcrt.dll\")" ++
    "                           (load-shared-object \"ws2_32.dll\")]\n" ++
    "  [else (load-shared-object \"libc.so\")])\n\n" ++
    showSep "\n" (map (\x => "(load-shared-object \"" ++ escapeString x ++ "\")") libs) ++ "\n\n" ++
    "(let ()\n"

schFooter : String
schFooter = "(collect 4)\n(blodwen-run-finalisers))\n"

showChezChar : Char -> String -> String
showChezChar '\\' = ("\\\\" ++)
showChezChar c
   = if c < chr 32 || c > chr 126
        then (("\\x" ++ asHex (cast c) ++ ";") ++)
        else strCons c

showChezString : List Char -> String -> String
showChezString [] = id
showChezString ('"'::cs) = ("\\\"" ++) . showChezString cs
showChezString (c ::cs) = (showChezChar c) . showChezString cs

chezString : String -> String
chezString cs = strCons '"' (showChezString (unpack cs) "\"")

mutual
  tySpec : NamedCExp -> Core String
  -- Primitive types have been converted to names for the purpose of matching
  -- on types
  tySpec (NmCon fc (UN "Int") _ []) = pure "int"
  tySpec (NmCon fc (UN "String") _ []) = pure "string"
  tySpec (NmCon fc (UN "Double") _ []) = pure "double"
  tySpec (NmCon fc (UN "Char") _ []) = pure "char"
  tySpec (NmCon fc (NS _ n) _ [_])
     = cond [(n == UN "Ptr", pure "void*"),
             (n == UN "GCPtr", pure "void*"),
             (n == UN "Buffer", pure "u8*")]
          (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
  tySpec (NmCon fc (NS _ n) _ [])
     = cond [(n == UN "Unit", pure "void"),
             (n == UN "AnyPtr", pure "void*"),
             (n == UN "GCAnyPtr", pure "void*")]
          (throw (GenericMsg fc ("Can't pass argument of type " ++ show n ++ " to foreign function")))
  tySpec ty = throw (GenericMsg (getFC ty) ("Can't pass argument of type " ++ show ty ++ " to foreign function"))

  handleRet : String -> String -> String
  handleRet "void" op = op ++ " " ++ mkWorld (schConstructor chezString (UN "") (Just 0) [])
  handleRet _ op = mkWorld op

  getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp))
  getFArgs (NmCon fc _ (Just 0) _) = pure []
  getFArgs (NmCon fc _ (Just 1) [ty, val, rest]) = pure $ (ty, val) :: !(getFArgs rest)
  getFArgs arg = throw (GenericMsg (getFC arg) ("Badly formed c call argument list " ++ show arg))

  chezExtPrim : Int -> ExtPrim -> List NamedCExp -> Core String
  chezExtPrim i GetField [NmPrimVal _ (Str s), _, _, struct,
                          NmPrimVal _ (Str fld), _]
      = do structsc <- schExp chezExtPrim chezString 0 struct
           pure $ "(ftype-ref " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++ ")"
  chezExtPrim i GetField [_,_,_,_,_,_]
      = pure "(error \"bad getField\")"
  chezExtPrim i SetField [NmPrimVal _ (Str s), _, _, struct,
                          NmPrimVal _ (Str fld), _, val, world]
      = do structsc <- schExp chezExtPrim chezString 0 struct
           valsc <- schExp chezExtPrim chezString 0 val
           pure $ mkWorld $
              "(ftype-set! " ++ s ++ " (" ++ fld ++ ") " ++ structsc ++
              " " ++ valsc ++ ")"
  chezExtPrim i SetField [_,_,_,_,_,_,_,_]
      = pure "(error \"bad setField\")"
  chezExtPrim i SysCodegen []
      = pure $ "\"chez\""
  chezExtPrim i OnCollect [_, p, c, world]
      = do p' <- schExp chezExtPrim chezString 0 p
           c' <- schExp chezExtPrim chezString 0 c
           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
  chezExtPrim i OnCollectAny [p, c, world]
      = do p' <- schExp chezExtPrim chezString 0 p
           c' <- schExp chezExtPrim chezString 0 c
           pure $ mkWorld $ "(blodwen-register-object " ++ p' ++ " " ++ c' ++ ")"
  chezExtPrim i prim args
      = schExtCommon chezExtPrim chezString i prim args

-- Reference label for keeping track of loaded external libraries
data Loaded : Type where

-- Label for noting which struct types are declared
data Structs : Type where

cftySpec : FC -> CFType -> Core String
cftySpec fc CFUnit = pure "void"
cftySpec fc CFInt = pure "int"
cftySpec fc CFUnsigned8 = pure "unsigned-8"
cftySpec fc CFUnsigned16 = pure "unsigned-16"
cftySpec fc CFUnsigned32 = pure "unsigned-32"
cftySpec fc CFUnsigned64 = pure "unsigned-64"
cftySpec fc CFString = pure "string"
cftySpec fc CFDouble = pure "double"
cftySpec fc CFChar = pure "char"
cftySpec fc CFPtr = pure "void*"
cftySpec fc CFGCPtr = pure "void*"
cftySpec fc CFBuffer = pure "u8*"
cftySpec fc (CFFun s t) = pure "void*"
cftySpec fc (CFIORes t) = cftySpec fc t
cftySpec fc (CFStruct n t) = pure $ "(* " ++ n ++ ")"
cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
                         " to foreign function"))

cCall : {auto c : Ref Ctxt Defs} ->
        {auto l : Ref Loaded (List String)} ->
        String -> FC -> (cfn : String) -> (clib : String) ->
        List (Name, CFType) -> CFType -> Core (String, String)
cCall appdir fc cfn clib args (CFIORes CFGCPtr)
    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args CFGCPtr
    = throw (GenericMsg fc "Can't return GCPtr from a foreign function")
cCall appdir fc cfn clib args (CFIORes CFBuffer)
    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn clib args CFBuffer
    = throw (GenericMsg fc "Can't return Buffer from a foreign function")
cCall appdir fc cfn clib args ret
    = do loaded <- get Loaded
         lib <- if clib `elem` loaded
                   then pure ""
                   else do (fname, fullname) <- locate clib
                           copyLib (appdir </> fname, fullname)
                           put Loaded (clib :: loaded)
                           pure $ "(load-shared-object \""
                                    ++ escapeString fname
                                    ++ "\")\n"
         argTypes <- traverse (\a => cftySpec fc (snd a)) args
         retType <- cftySpec fc ret
         let call = "((foreign-procedure #f " ++ show cfn ++ " ("
                      ++ showSep " " argTypes ++ ") " ++ retType ++ ") "
                      ++ showSep " " !(traverse buildArg args) ++ ")"

         pure (lib, case ret of
                         CFIORes _ => handleRet retType call
                         _ => call)
  where
    mkNs : Int -> List CFType -> List (Maybe String)
    mkNs i [] = []
    mkNs i (CFWorld :: xs) = Nothing :: mkNs i xs
    mkNs i (x :: xs) = Just ("cb" ++ show i) :: mkNs (i + 1) xs

    applyLams : String -> List (Maybe String) -> String
    applyLams n [] = n
    applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as
    applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as

    getVal : String -> String
    getVal str = "(vector-ref " ++ str ++ "1)"

    mkFun : List CFType -> CFType -> String -> String
    mkFun args ret n
        = let argns = mkNs 0 args in
              "(lambda (" ++ showSep " " (mapMaybe id argns) ++ ") " ++
              (applyLams n argns ++ ")")

    notWorld : CFType -> Bool
    notWorld CFWorld = False
    notWorld _ = True

    callback : String -> List CFType -> CFType -> Core String
    callback n args (CFFun s t) = callback n (s :: args) t
    callback n args_rev retty
        = do let args = reverse args_rev
             argTypes <- traverse (cftySpec fc) (filter notWorld args)
             retType <- cftySpec fc retty
             pure $
                 "(let ([c-code (foreign-callable #f " ++
                       mkFun args retty n ++
                       " (" ++ showSep " " argTypes ++ ") " ++ retType ++ ")])" ++
                       " (lock-object c-code) (foreign-callable-entry-point c-code))"

    buildArg : (Name, CFType) -> Core String
    buildArg (n, CFFun s t) = callback (schName n) [s] t
    buildArg (n, CFGCPtr) = pure $ "(car " ++ schName n ++ ")"
    buildArg (n, _) = pure $ schName n

schemeCall : FC -> (sfn : String) ->
             List Name -> CFType -> Core String
schemeCall fc sfn argns ret
    = let call = "(" ++ sfn ++ " " ++ showSep " " (map schName argns) ++ ")" in
          case ret of
               CFIORes _ => pure $ mkWorld call
               _ => pure call

-- Use a calling convention to compile a foreign def.
-- Returns any preamble needed for loading libraries, and the body of the
-- function call.
useCC : {auto c : Ref Ctxt Defs} ->
        {auto l : Ref Loaded (List String)} ->
        String -> FC -> List String -> List (Name, CFType) -> CFType -> Core (String, String)
useCC appdir fc [] args ret = throw (NoForeignCC fc)
useCC appdir fc (cc :: ccs) args ret
    = case parseCC cc of
           Nothing => useCC appdir fc ccs args ret
           Just ("scheme,chez", [sfn]) =>
               do body <- schemeCall fc sfn (map fst args) ret
                  pure ("", body)
           Just ("scheme", [sfn]) =>
               do body <- schemeCall fc sfn (map fst args) ret
                  pure ("", body)
           Just ("C", [cfn, clib]) => cCall appdir fc cfn clib args ret
           Just ("C", [cfn, clib, chdr]) => cCall appdir fc cfn clib args ret
           _ => useCC appdir fc ccs args ret

-- For every foreign arg type, return a name, and whether to pass it to the
-- foreign call (we don't pass '%World')
mkArgs : Int -> List CFType -> List (Name, Bool)
mkArgs i [] = []
mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs i cs
mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs

mkStruct : {auto s : Ref Structs (List String)} ->
           CFType -> Core String
mkStruct (CFStruct n flds)
    = do defs <- traverse mkStruct (map snd flds)
         strs <- get Structs
         if n `elem` strs
            then pure (concat defs)
            else do put Structs (n :: strs)
                    pure $ concat defs ++ "(define-ftype " ++ n ++ " (struct\n\t"
                           ++ showSep "\n\t" !(traverse showFld flds) ++ "))\n"
  where
    showFld : (String, CFType) -> Core String
    showFld (n, ty) = pure $ "[" ++ n ++ " " ++ !(cftySpec emptyFC ty) ++ "]"
mkStruct (CFIORes t) = mkStruct t
mkStruct (CFFun a b) = do mkStruct a; mkStruct b
mkStruct _ = pure ""

schFgnDef : {auto c : Ref Ctxt Defs} ->
            {auto l : Ref Loaded (List String)} ->
            {auto s : Ref Structs (List String)} ->
            String -> FC -> Name -> NamedDef -> Core (String, String)
schFgnDef appdir fc n (MkNmForeign cs args ret)
    = do let argns = mkArgs 0 args
         let allargns = map fst argns
         let useargns = map fst (filter snd argns)
         argStrs <- traverse mkStruct args
         retStr <- mkStruct ret
         (load, body) <- useCC appdir fc cs (zip useargns args) ret
         defs <- get Ctxt
         pure (load,
                concat argStrs ++ retStr ++
                "(define " ++ schName !(full (gamma defs) n) ++
                " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++
                body ++ "))\n")
schFgnDef _ _ _ _ = pure ("", "")

getFgnCall : {auto c : Ref Ctxt Defs} ->
             {auto l : Ref Loaded (List String)} ->
             {auto s : Ref Structs (List String)} ->
             String -> (Name, FC, NamedDef) -> Core (String, String)
getFgnCall appdir (n, fc, d) = schFgnDef appdir fc n d

startChez : String -> String -> String
startChez appdir target = unlines
    [ "#!/bin/sh"
    , ""
    , "case `uname -s` in            "
    , "    OpenBSD|FreeBSD|NetBSD)   "
    , "        DIR=\"`grealpath $0`\""
    , "        ;;                    "
    , "                              "
    , "    *)                        "
    , "        DIR=\"`realpath $0`\" "
    , "        ;;                    "
    , "esac                          "
    , ""
    , "export LD_LIBRARY_PATH=\"$LD_LIBRARY_PATH:`dirname \"$DIR\"`/\"" ++ appdir ++ "\"\""
    , "\"`dirname \"$DIR\"`\"/\"" ++ target ++ "\" \"$@\""
    ]

startChezCmd : String -> String -> String -> String
startChezCmd chez appdir target = unlines
    [ "@echo off"
    , "set APPDIR=%~dp0"
    , "set PATH=%APPDIR%\\" ++ appdir ++ ";%PATH%"
    , "\"" ++ chez ++ "\" --script \"%APPDIR%/" ++ target ++ "\" %*"
    ]

startChezWinSh : String -> String -> String -> String
startChezWinSh chez appdir target = unlines
    [ "#!/bin/sh"
    , "DIR=\"`realpath \"$0\"`\""
    , "CHEZ=$(cygpath \"" ++ chez ++"\")"
    , "export PATH=\"`dirname \"$DIR\"`/\"" ++ appdir ++ "\":$PATH\""
    , "\"$CHEZ\" --script \"$(dirname \"$DIR\")/" ++ target ++ "\" \"$@\""
    ]

||| Compile a TT expression to Chez Scheme
compileToSS : Ref Ctxt Defs ->
              String -> ClosedTerm -> (outfile : String) -> Core ()
compileToSS c appdir tm outfile
    = do ds <- getDirectives Chez
         libs <- findLibs (map snd ds)
         traverse_ copyLib libs
         cdata <- getCompileData Cases tm
         let ndefs = namedDefs cdata
         let ctm = forget (mainExpr cdata)

         defs <- get Ctxt
         l <- newRef {t = List String} Loaded ["libc", "libc 6"]
         s <- newRef {t = List String} Structs []
         fgndefs <- traverse (getFgnCall appdir) ndefs
         compdefs <- traverse (getScheme chezExtPrim chezString) ndefs
         let code = fastAppend (map snd fgndefs ++ compdefs)
         main <- schExp chezExtPrim chezString 0 ctm
         chez <- coreLift findChez
         support <- readDataFile "chez/support.ss"
         extraRuntime <- getExtraRuntime (map snd ds)
         let scm = schHeader chez (map snd libs) ++
                   support ++ extraRuntime ++ code ++
                   concat (map fst fgndefs) ++
                   "(collect-request-handler (lambda () (collect) (blodwen-run-finalisers)))\n" ++
                   main ++ schFooter
         Right () <- coreLift $ writeFile outfile scm
            | Left err => throw (FileErr outfile err)
         coreLift $ chmodRaw outfile 0o755
         pure ()

||| Compile a Chez Scheme source file to an executable, daringly with runtime checks off.
compileToSO : {auto c : Ref Ctxt Defs} ->
              String -> (appDirRel : String) -> (outSsAbs : String) -> Core ()
compileToSO chez appDirRel outSsAbs
    = do let tmpFileAbs = appDirRel </> "compileChez"
         let build = "(parameterize ([optimize-level 3] [compile-file-message #f]) (compile-program " ++
                    show outSsAbs ++ "))"
         Right () <- coreLift $ writeFile tmpFileAbs build
            | Left err => throw (FileErr tmpFileAbs err)
         coreLift $ chmodRaw tmpFileAbs 0o755
         coreLift $ system (chez ++ " --script \"" ++ tmpFileAbs ++ "\"")
         pure ()

makeSh : String -> String -> String -> Core ()
makeSh outShRel appdir outAbs
    = do Right () <- coreLift $ writeFile outShRel (startChez appdir outAbs)
            | Left err => throw (FileErr outShRel err)
         pure ()

||| Make Windows start scripts, one for bash environments and one batch file
makeShWindows : String -> String -> String -> String -> Core ()
makeShWindows chez outShRel appdir outAbs
    = do let cmdFile = outShRel ++ ".cmd"
         Right () <- coreLift $ writeFile cmdFile (startChezCmd chez appdir outAbs)
            | Left err => throw (FileErr cmdFile err)
         Right () <- coreLift $ writeFile outShRel (startChezWinSh chez appdir outAbs)
            | Left err => throw (FileErr outShRel err)
         pure ()

||| Chez Scheme implementation of the `compileExpr` interface.
compileExpr : Bool -> Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
              ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr makeitso c tmpDir outputDir tm outfile
    = do let appDirRel = outfile ++ "_app" -- relative to build dir
         let appDirGen = outputDir </> appDirRel -- relative to here
         coreLift $ mkdirAll appDirGen
         Just cwd <- coreLift currentDir
              | Nothing => throw (InternalError "Can't get current directory")
         let outSsFile = appDirRel </> outfile <.> "ss"
         let outSoFile = appDirRel </> outfile <.> "so"
         let outSsAbs = cwd </> outputDir </> outSsFile
         let outSoAbs = cwd </> outputDir </> outSoFile
         chez <- coreLift $ findChez
         compileToSS c appDirGen tm outSsAbs
         logTime "Make SO" $ when makeitso $ compileToSO chez appDirGen outSsAbs
         let outShRel = outputDir </> outfile
         if isWindows
            then makeShWindows chez outShRel appDirRel (if makeitso then outSoFile else outSsFile)
            else makeSh outShRel appDirRel (if makeitso then outSoFile else outSsFile)
         coreLift $ chmodRaw outShRel 0o755
         pure (Just outShRel)

||| Chez Scheme implementation of the `executeExpr` interface.
||| This implementation simply runs the usual compiler, saving it to a temp file, then interpreting it.
executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm
    = do Just sh <- compileExpr False c tmpDir tmpDir tm "_tmpchez"
            | Nothing => throw (InternalError "compileExpr returned Nothing")
         coreLift $ system sh
         pure ()

compileLibrary : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) -> (libName : String) -> (changedModules : Maybe (List ModuleIdent)) -> Core (Maybe (String, List String))
compileLibrary c tmpDir outputDir libName changedModules = do
  coreLift $ putStrLn "Compiling to library is not supported."
  pure Nothing

||| Codegen wrapper for Chez scheme implementation.
export
codegenChez : Codegen
codegenChez = MkCG (compileExpr True) executeExpr compileLibrary


text:
module Main

import Remotelib2
import Testlib2
import System

main : IO ()
main = do
  putStr "Starting test... "
  if length val2 == 0 || length rem2 == 0
    then putStrLn "FAILED." >> exitFailure
    else putStrLn "Succeeded."

max_stars_repo_name: idream-build/idream

max_issues_repo_name: idream-build/idream

max_forks_repo_name: idream-build/idream


text:
module DepPairs

import Data.Vect

%default total

partial
readVect : HasIO io => io (n : Nat ** Vect n String)
readVect = do x <- getLine
              if x == ""
                 then pure $ MkDPair _ []
                 else do MkDPair _ xs <- readVect
                         pure $ MkDPair _ (x :: xs)

 -- since the dependent pair syntax is merely syntactic sugar for
 -- the DPair type
partial
readVect' : HasIO io => io (n : Nat ** Vect n String)
readVect' = do x <- getLine
               if x == ""
                  then pure $ (_ ** [])
                  else do (_ ** xs) <- readVect'
                          pure $ (_ ** (x :: xs))

printVect : HasIO io => (n : Nat ** Vect n String) -> io ()
printVect (n ** xs) = putStrLn $ show xs ++ " (length " ++ show n ++ ")"

printVect' : HasIO io => (n : Nat ** Vect n String) -> io ()
printVect' (MkDPair n xs) = putStrLn $ show xs ++ " (length " ++ show n ++ ")"

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
data Matter = Solid | Liquid | Gas

Eq Matter where
    (==) Solid Solid = True
    (==) Liquid Liquid = True
    (==) Gas Gas = True
    (==) _ _ = False
    (/=) x y = not (x == y)

data Tree elem = Empty | Node (Tree elem) elem (Tree elem)

Eq elem => Eq (Tree elem) where
    (==) Empty Empty = True
    (==) (Node left elem right) (Node 'left 'elem 'right) =
      left == left' && elem == 'elem && right == 'right
    (==) _ _ = False

occurrences : Eq ty => (item : ty) -> (values : List ty) -> Nat
occurrences item [] = 0
occurrences item (x :: xs) = case x == item of
                                  True => S (occurrences item xs)
                                  False => occurrences item xs

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Language.LSP.CodeAction.MakeWith

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Idris.IDEMode.MakeClause
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.CodeAction.Utils
import Language.LSP.Message
import Libraries.Data.PosMap
import Parser.Unlit
import Server.Configuration
import Server.Log
import Server.Utils
import TTImp.TTImp

buildCodeAction : Name -> URI -> TextEdit -> CodeAction
buildCodeAction name uri edit =
  MkCodeAction
    { title       = "Make with for hole ?\{show name}"
    , kind        = Just RefactorRewrite
    , diagnostics = Nothing
    , isPreferred = Nothing
    , disabled    = Nothing
    , edit        = Just $ MkWorkspaceEdit
        { changes           = Just (singleton uri [edit])
        , documentChanges   = Nothing
        , changeAnnotations = Nothing
        }
    , command     = Nothing
    , data_       = Nothing
    }

export
makeWithKind : CodeActionKind
makeWithKind = Other "refactor.rewrite.MakeWith"

isAllowed : CodeActionParams -> Bool
isAllowed params =
  maybe True (\filter => (makeWithKind `elem` filter) || (RefactorRewrite `elem` filter)) params.context.only

export
makeWith : Ref LSPConf LSPConfiguration
        => Ref MD Metadata
        => Ref Ctxt Defs
        => Ref UST UState
        => Ref Syn SyntaxInfo
        => Ref ROpts REPLOpts
        => CodeActionParams -> Core (Maybe CodeAction)
makeWith params = do
  let True = isAllowed params
    | False => logI MakeWith "Skipped" >> pure Nothing
  logI MakeWith "Checking for \{show params.textDocument.uri} at \{show params.range}"

  withSingleLine MakeWith params (pure Nothing) $ \line => do
    withSingleCache MakeWith params MakeWith $ do
      nameLocs <- gets MD nameLocMap
      let col = params.range.start.character
      let Just (loc@(_, nstart, nend), name) = findPointInTreeLoc (line, col) nameLocs
        | Nothing => logD MakeWith "No name found at \{show line}:\{show col}}" >> pure Nothing
      logD MakeCase "Found name \{show name}"

      context <- gets Ctxt gamma
      [(_, _, Hole locs _, _)] <- lookupNameBy (\g => (definition g, type g)) name context
        | _ => logD MakeWith "\{show name} is not a metavariable" >> pure Nothing

      logD MakeCase "Found metavariable \{show name}"
      litStyle <- getLitStyle
      Just src <- getSourceLine (line + 1)
        | Nothing => logE MakeWith "Error while fetching the referenced line" >> pure Nothing
      let Right l = unlit litStyle src
        | Left err => logE MakeWith "Invalid literate Idris" >> pure Nothing
      let (markM, _) = isLitLine src
      let with_ = makeWith name l
      let range = MkRange (MkPosition line 0) (MkPosition line (cast (length src) - 1))
      let edit = MkTextEdit range with_

      pure $ Just (cast loc, buildCodeAction name params.textDocument.uri edit)


text:
module ReadVect

import Data.Vect

readVectLen : (len : Nat) -> IO (Vect len String)
readVectLen Z = pure []
readVectLen (S k) = do x <- getLine
                       xs <- readVectLen k
                       pure (x :: xs)  -- nice..

---- why do we have to define the length??
--data VectUnknown : Type -> Type where
--     MkVect : (len : Nat) -> Vect len a -> VectUnknown a
--
--readVect : IO (VectUnknown String)
--readVect = do x <- getLine
--              if x == "" then pure (MkVect 0 [])
--                         else do MkVect len xs <- readVect
--                                 pure (MkVect (S len) (x :: xs))

data VectUnknown : Type -> Type where
  MkVect : Vect len a -> VectUnknown a

readVect' : IO (VectUnknown String)
readVect' = do
  x <- getLine
  if x == ""
     then pure (MkVect [])
     else do
       MkVect xs <- readVect'
       pure (MkVect (x :: xs))

readVect : IO (n ** Vect n String)  -- Oooh, interesting!
readVect = do
  x <- getLine
  if x == ""
     then pure (_ ** [])
     else do
       (_ ** xs) <- readVect
       pure (_ ** x :: xs)

-- This is fairly ugly.  Do we have (a : Nat) -> (b : Nat) -> Maybe (a with (_)
  -- This is fairly ugly.  Do we have (a : Nat) -> (b : Nat) -> Maybe (a | with_pat = ?This_rhs
myExactLength : (l : Nat) -> (Vect len a) -> Maybe (Vect l a)
myExactLength Z [] = Just []
myExactLength Z (x :: xs) = Nothing
myExactLength (S k) [] = Nothing
myExactLength (S k) (x :: xs) = case myExactLength k xs of
                                     Nothing => Nothing
                                     Just ys => Just (x :: ys)

zipInputs : IO ()
zipInputs = do
  putStrLn "Enter first vector (blank line to end): "
  (l1 ** v1) <- readVect
  putStrLn "Enter second vector (blank line to end): "
  (l2 ** v2) <- readVect
  --(Just v2l1) <- exactLength l1 v2 | Nothing putStrLn "Vectors have different lengths."
  case myExactLength l1 v2 of  -- how DO we implement exact length?
       Nothing => putStrLn "Vectors have different lengths."
       Just v2l1 => putStrLn (show (zip v1 v2l1))

-- Go back to Chapter5.idr

max_stars_repo_name: neduard/type-driven-development

max_issues_repo_name: neduard/type-driven-development

max_forks_repo_name: neduard/type-driven-development


text:
module TTImp.Elab.Binders

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.Metadata
import Core.Normalise
import Core.Unify
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.TTImp

%default covering

-- Drop the name from the nested function declarations. We do this when
-- going into a new scope, so that we're resolving to the most recently
-- bound name.
export
dropName : Name -> NestedNames vars -> NestedNames vars
dropName n nest = record { names $= drop } nest
  where
    drop : List (Name, a) -> List (Name, a)
    drop [] = []
    drop ((x, y) :: xs)
        = if x == n then drop xs
             else (x, y) :: drop xs

checkPiInfo : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              {auto e : Ref EST (EState vars)} ->
              RigCount -> ElabInfo -> NestedNames vars -> Env Term vars ->
              PiInfo RawImp -> (expTy : Maybe (Glued vars)) ->
              Core (PiInfo (Term vars))
checkPiInfo rig elabinfo nest env Explicit exp = pure Explicit
checkPiInfo rig elabinfo nest env Implicit exp = pure Implicit
checkPiInfo rig elabinfo nest env AutoImplicit exp = pure AutoImplicit
checkPiInfo rig elabinfo nest env (DefImplicit t) exp
    = do (tv, _) <- check rig elabinfo nest env t exp
         pure (DefImplicit tv)

export
checkPi : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto m : Ref MD Metadata} ->
          {auto u : Ref UST UState} ->
          {auto e : Ref EST (EState vars)} ->
          RigCount -> ElabInfo ->
          NestedNames vars -> Env Term vars ->
          FC ->
          RigCount -> PiInfo RawImp -> (n : Name) ->
          (argTy : RawImp) -> (retTy : RawImp) ->
          (expTy : Maybe (Glued vars)) ->
          Core (Term vars, Glued vars)
checkPi rig elabinfo nest env fc rigf info n argTy retTy expTy
    = do let pirig = getRig (elabMode elabinfo)
         (tyv, tyt) <- check pirig elabinfo nest env argTy
                             (Just (gType fc))
         info' <- checkPiInfo rigf elabinfo nest env info (Just (gnf env tyv))
         let env' : Env Term (n :: _) = Pi fc rigf info' tyv :: env
         let nest' = weaken (dropName n nest)
         (scopev, scopet) <-
            inScope fc env' (\e' =>
              check {e=e'} pirig elabinfo nest' env' retTy (Just (gType fc)))
         checkExp rig elabinfo env fc (Bind fc n (Pi (getFC argTy) rigf info' tyv) scopev) (gType fc) expTy
  where
    -- Might want to match on the LHS, so use the context rig, otherwise
    -- it's always erased
    getRig : ElabMode -> RigCount
    getRig (InLHS _) = rig
    getRig _ = erased

findLamRig : {auto c : Ref Ctxt Defs} ->
             Maybe (Glued vars) -> Core RigCount
findLamRig Nothing = pure top
findLamRig (Just expty)
    = do tynf <- getNF expty
         case tynf of
              NBind _ _ (Pi _ c _ _) sc => pure c
              _ => pure top

inferLambda : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              {auto e : Ref EST (EState vars)} ->
              RigCount -> ElabInfo ->
              NestedNames vars -> Env Term vars ->
              FC ->
              RigCount -> PiInfo RawImp -> (n : Name) ->
              (argTy : RawImp) -> (scope : RawImp) ->
              (expTy : Maybe (Glued vars)) ->
              Core (Term vars, Glued vars)
inferLambda rig elabinfo nest env fc rigl info n argTy scope expTy
    = do rigb_in <- findLamRig expTy
         let rigb = rigb_in `glb` rigl
         (tyv, tyt) <- check erased elabinfo nest env argTy (Just (gType fc))
         info' <- checkPiInfo rigl elabinfo nest env info (Just (gnf env tyv))
         let env' : Env Term (n :: _) = Lam fc rigb info' tyv :: env
         let nest' = weaken (dropName n nest)
         (scopev, scopet) <- inScope fc env' (\e' =>
                                check {e=e'} rig elabinfo
                                      nest' env' scope Nothing)
         let lamty = gnf env (Bind fc n (Pi fc rigb info' tyv) !(getTerm scopet))
         logGlue "elab.binder" 5 "Inferred lambda type" env lamty
         maybe (pure ())
               (logGlueNF "elab.binder" 5 "Expected lambda type" env) expTy
         checkExp rig elabinfo env fc
                  (Bind fc n (Lam fc rigb info' tyv) scopev)
                  lamty expTy

getTyNF : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          Env Term vars -> Term vars -> Core (Term vars)
getTyNF env x@(Bind _ _ _ _) = pure x
getTyNF env x
    = do defs <- get Ctxt
         xnf <- nf defs env x
         empty <- clearDefs defs
         quote empty env xnf

export
checkLambda : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto m : Ref MD Metadata} ->
              {auto u : Ref UST UState} ->
              {auto e : Ref EST (EState vars)} ->
              RigCount -> ElabInfo ->
              NestedNames vars -> Env Term vars ->
              FC ->
              RigCount -> PiInfo RawImp -> (n : Name) ->
              (argTy : RawImp) -> (scope : RawImp) ->
              (expTy : Maybe (Glued vars)) ->
              Core (Term vars, Glued vars)
checkLambda rig_in elabinfo nest env fc rigl info n argTy scope Nothing
    = let rig = if isErased rig_in then erased else linear in
          inferLambda rig elabinfo nest env fc rigl info n argTy scope Nothing
checkLambda rig_in elabinfo nest env fc rigl info n argTy scope (Just expty_in)
    = do let rig = if isErased rig_in then erased else linear
         let solvemode = case elabMode elabinfo of
                              InLHS _ => inLHS
                              _ => inTerm
         solveConstraints solvemode Normal
         expty <- getTerm expty_in
         exptynf <- getTyNF env expty
         defs <- get Ctxt
         case exptynf of
              Bind bfc bn (Pi fc' c _ pty) psc =>
                 do (tyv, tyt) <- check erased elabinfo nest env
                                        argTy (Just (gType fc))
                    info' <- checkPiInfo rigl elabinfo nest env info (Just (gnf env tyv))
                    let rigb = rigl `glb` c
                    let env' : Env Term (n :: _) = Lam fc rigb info' tyv :: env
                    ignore $ convert fc elabinfo env (gnf env tyv) (gnf env pty)
                    let nest' = weaken (dropName n nest)
                    (scopev, scopet) <-
                       inScope fc env' (\e' =>
                          check {e=e'} rig elabinfo nest' env' scope
                                (Just (gnf env' (renameTop n psc))))
                    logTermNF "elab.binder" 10 "Lambda type" env exptynf
                    logGlueNF "elab.binder" 10 "Got scope type" env' scopet

                    -- Currently, the fc a PLam holds (and that ILam gets as a consequence)
                    -- is the file context of the argument to the lambda. This fits nicely
                    -- in this exact use, but is likely a bug.
                    log "metadata.names" 7 "checkLambda is adding ↓"
                    addNameType fc n env pty -- Add the type of the argument to the metadata

                    -- We've already checked the argument and scope types,
                    -- so we just need to check multiplicities
                    when (rigb /= c) $
                        throw (CantConvert fc (gamma defs) env
                                  (Bind fc n (Pi fc' rigb info' tyv) !(getTerm scopet))
                                  (Bind fc bn (Pi fc' c info' pty) psc))
                    pure (Bind fc n (Lam fc' rigb info' tyv) scopev,
                          gnf env (Bind fc n (Pi fc' rigb info' tyv) !(getTerm scopet)))
              _ => inferLambda rig elabinfo nest env fc rigl info n argTy scope (Just expty_in)

weakenExp : {x, vars : _} ->
            Env Term (x :: vars) ->
            Maybe (Glued vars) -> Core (Maybe (Glued (x :: vars)))
weakenExp env Nothing = pure Nothing
weakenExp env (Just gtm)
    = do tm <- getTerm gtm
         pure (Just (gnf env (weaken tm)))

export
checkLet : {vars : _} ->
           {auto c : Ref Ctxt Defs} ->
           {auto m : Ref MD Metadata} ->
           {auto u : Ref UST UState} ->
           {auto e : Ref EST (EState vars)} ->
           RigCount -> ElabInfo ->
           NestedNames vars -> Env Term vars ->
           FC -> (lhsFC : FC) -> RigCount -> (n : Name) ->
           (nTy : RawImp) -> (nVal : RawImp) -> (scope : RawImp) ->
           (expTy : Maybe (Glued vars)) ->
           Core (Term vars, Glued vars)
checkLet rigc_in elabinfo nest env fc lhsFC rigl n nTy nVal scope expty {vars}
    = do let rigc = if isErased rigc_in then erased else linear
         (tyv, tyt) <- check erased elabinfo nest env nTy (Just (gType fc))
         -- Try checking at the given multiplicity; if that doesn't work,
         -- try checking at Rig1 (meaning that we're using a linear variable
         -- so the resulting binding should be linear)
         -- Also elaborate any case blocks in the value via runDelays
         (valv, valt, rigb) <- handle
              (do c <- runDelays (==CaseBlock) $ check (rigl |*| rigc)
                             (record { preciseInf = True } elabinfo)
                             nest env nVal (Just (gnf env tyv))
                  pure (fst c, snd c, rigl |*| rigc))
              (\err => case linearErr err of
                            Just r
                              => do branchOne
                                     (do c <- runDelays (==CaseBlock) $ check linear elabinfo
                                                  nest env nVal (Just (gnf env tyv))
                                         pure (fst c, snd c, linear))
                                     (do c <- check (rigl |*| rigc)
                                                  elabinfo -- without preciseInf
                                                  nest env nVal (Just (gnf env tyv))
                                         pure (fst c, snd c, rigMult rigl rigc))
                                     r
                            _ => do c <- check (rigl |*| rigc)
                                               elabinfo -- without preciseInf
                                               nest env nVal (Just (gnf env tyv))
                                    pure (fst c, snd c, rigl |*| rigc))
         let env' : Env Term (n :: _) = Lam fc rigb Explicit tyv :: env
         let nest' = weaken (dropName n nest)
         expScope <- weakenExp env' expty
         (scopev, gscopet) <-
            inScope fc env' (\e' =>
              check {e=e'} rigc elabinfo nest' env' scope expScope)
         scopet <- getTerm gscopet

         -- No need to 'checkExp' here - we've already checked scopet
         -- against the expected type when checking the scope, so just
         -- build the term directly

         -- Add the lhs of the let to metadata
         log "metadata.names" 7 $ "checkLet is adding ↓"
         addNameType lhsFC n env tyv

         pure (Bind fc n (Let fc rigb valv tyv) scopev,
               gnf env (Bind fc n (Let fc rigb valv tyv) scopet))
  where
    linearErr : Error -> Maybe RigCount
    linearErr (LinearMisuse _ _ r _) = Just r
    linearErr (InType _ _ e) = linearErr e
    linearErr (InCon _ _ e) = linearErr e
    linearErr (InLHS _ _ e) = linearErr e
    linearErr (InRHS _ _ e) = linearErr e
    linearErr _ = Nothing


text:
module BadSystemCode

import System

main : IO ()
main = system "some-non-existent-command" >>= putStrLn . show -- should print `-1`


text:
module IdvPaths

import public IdvPaths.Generated

import Data.Version
import System.Path
import System.Directory.Extra
import System
import System.File

export
idrisRepoURL : String
idrisRepoURL = "https://github.com/idris-lang/Idris2.git"

export
relativeCheckoutPath : String
relativeCheckoutPath = "checkout"

export
relativeVersionsPath : String
relativeVersionsPath = "versions"

export
relativeBinPath : String
relativeBinPath = "bin"

||| The full path & executable name of the Idris 2
||| binary within the Idv directory (which is a symlink
||| pointing at the actual installed binary of whichever
||| version of Idris 2 is currently selected).
export
idrisSymlinkedPath : String
idrisSymlinkedPath =
  idvLocation </> relativeBinPath </> "idris2"

||| Get the name of the directory where the given version is installed
||| This is the directory relative to `idvLocation`/`relativeVersionsPath`
export
versionDirName : Version -> String
versionDirName (V major minor patch Nothing _) = "\{show major}_\{show minor}_\{show patch}"
versionDirName (V major minor patch (Just pre) _) = "\{show major}_\{show minor}_\{show patch}-\{pre}"

||| The full path where the given version is installed.
export
versionPath : Version -> String
versionPath version =
  idvLocation </> relativeVersionsPath </> (versionDirName version)

||| The build prefix (PREFIX) to use when making and installing the
||| the given version of the Idris 2 compiler.
export
buildPrefix : Version -> String
buildPrefix = versionPath

||| The full path & executable name of the Idris 2
||| binary within the _versions_ subdirectory of the
||| Idv directory. This is the _actual_ installed binary
||| for the given version that is in turn symlinked to
||| by `idrisSymlinkedPath` when the given version is
||| selected.
export
installedIdrisPath : Version -> String
installedIdrisPath version =
  versionPath version </> "bin" </> "idris2"

||| The install location of the system copy of Idris 2.
||| If Idris 2 cannot be located on the system (i.e.
||| outside of the Idv versions directory) this function
||| returns Nothing.
export
systemIdrisPath : HasIO io => io (Maybe String)
systemIdrisPath = do
  Nothing <- checkLocation =<< getEnv "IDRIS2"
    | Just envOverride => pure $ Just envOverride
  checkLocation =<< defaultPath
    where
      defaultPath : io (Maybe String)
      defaultPath = pathExpansion defaultIdris2Location

      checkLocation : Maybe String -> io (Maybe String)
      checkLocation Nothing     = pure Nothing
      checkLocation (Just path) = pure $ if !(exists path) then Just path else Nothing

max_stars_repo_name: mattpolzin/idrv

max_issues_repo_name: mattpolzin/idrv

max_forks_repo_name: mattpolzin/idrv


text:
module Sidharths.Odds

import Evens

import Intro

data IsOdd : Nat -> Type where
  OneOdd : IsOdd 1
  SSOdd : (n: Nat) -> IsOdd n -> IsOdd (S (S n))

ThreeOdd : IsOdd 3
ThreeOdd = SSOdd 1 OneOdd

TwoOdd : IsOdd 2 -> Void
TwoOdd OneOdd impossible
TwoOdd (SSOdd _ _) impossible

NOddSnEven : (n : Nat) -> (IsOdd n) -> (IsEven (S n))
NOddSnEven (S Z) OneOdd = twoEven
NOddSnEven (S (S k)) (SSOdd k x) = (SSEven (S k) (NOddSnEven k x))

NEvenSnOdd : (n : Nat) -> (IsEven n) -> (IsOdd (S n))
NEvenSnOdd Z ZEven = OneOdd
NEvenSnOdd (S (S k)) (SSEven k x) = (SSOdd (S k)) (NevenSnOdd k x))

NEvenorOdd : (n : Nat) -> Either (IsEven n) (IsOdd n)
NEvenorOdd Z = Left ZEven
NEvenorOdd (S k) = case (NEvenorOdd k) of
                        (Left l) => Right (NEvenSnOdd k l)
                        (Right r) => Left (NOddSnEven k r)

NnotbothOddEven : (n : Nat) -> (IsEven n) -> (IsOdd n) -> Void
NnotbothOddEven Z ZEven OneOdd impossible
NnotbothOddEven (S (S k)) (SSEven k x) (SSOdd k y) = NnotbothOddEven k x y

AddEven : (n : Nat) -> (m : Nat) -> IsOdd n -> IsOdd m -> IsEven (add n m)
AddEVen (S Z) m OneOdd x = NOddSnEven m x
AddEven (S (S k)) m (SSOdd k x) y = SSEVen (add k m) (AddEven k m x y)

NOddHalf : (n : Nat) -> IsOdd n -> Nat
NOddHalf (S Z) OneOdd = Z
NOddHalf (S (S k)) (SSOdd k x) = S (NOddHalf k x)


text:
module Data.Bool.BoolTheorems

%default total
%access export

public export
ifWithProofs : (x : Bool) -> ((x = True) -> a) -> (not x = True -> a) -> a
ifWithProofs True f _ = f Refl
ifWithProofs False _ f = f Refl

AOrFalseIsA : (a : Bool) -> a || False = a
AOrFalseIsA True = Refl
AOrFalseIsA False = Refl

NotAEqNotBImpliesAEqB : (a : Bool) -> (b : Bool) -> (not a = not b) -> (a = b)
NotAEqNotBImpliesAEqB True True _ = Refl
NotAEqNotBImpliesAEqB False False _ = Refl
NotAEqNotBImpliesAEqB True False prf = absurd prf
NotAEqNotBImpliesAEqB False True prf = absurd prf

NotNotCancels : (a : Bool) -> a = True -> not (not a) = True
NotNotCancels True prf = prf
NotNotCancels False prf = prf