text:
module Sub13LTE108t111

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total

-- 6(18t+18)+3 --FB[5,-1,-2]--> 6(8t+7)+3
export
lte108t111 : (l : Nat) -> LTE (S (S (S (S (S (S (S (S (l+l+l+l)+(l+l+l+l)))))))))
  (S (S (S ((S ((S (S (l+l+l)))+(S (S (l+l+l))))) + (S ((S (S (l+l+l)))+(S (S (l+l+l))))) + (S ((S (S (l+l+l)))+(S (S (l+l+l)))))))))
lte108t111 Z     = (lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
lte108t111 (S l) =
  let lemma = lte108t111 l in
  rewrite (sym (plusSuccRightSucc l l)) in
  rewrite (sym (plusSuccRightSucc (plus l l) l)) in
  rewrite (sym (plusSuccRightSucc (plus (plus l l) l) l)) in

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

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

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

  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))) (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                  (S (S (S (S (S (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))) (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                  (S (S (S (S (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))) (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                  (S (S (S (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))) (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                  (S (S (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))) (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                  (S (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))) (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                  (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))) in
    (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
import Data.Either
import Data.Fin
import Data.List
import Data.List1
import Data.Nat
import Data.Maybe
import Data.Stream
import Data.String
import Data.String.Parser
import Data.Vect

import System.File

Energy : Type
Energy = Fin 10

data Flash = Flashed | E Energy

incEnergy : Energy -> Flash
incEnergy e = maybe Flashed E $ strengthen $ shift 1 e

isFlash : Flash -> Bool
isFlash Flashed = True
isFlash _ = False

resetFlash : Flash -> Energy
resetFlash Flashed = 0
resetFlash (E e) = e

-- A Non empty grid
Grid : Nat -> Type -> Type
Grid n a = Vect (S n) (Vect (S n) a)

parser : Parser (n ** Grid n Energy)
parser = do row <- some digit <* char '\n'
            let n = length row
            Just v <- pure $ toVect n row
              | Nothing => fail "not length"
            Yes ItIsSucc <- pure $ isItSucc n
              | No _ => fail "Row is zero"
            vs <- ntimes (pred n) ((ntimes n digit) <* char '\n')
            pure $ MkDPair (pred n) (v :: vs)

decFin : Fin n -> Maybe (Fin n)
decFin FZ = Nothing
decFin (FS x) = Just $ weaken $ x
incFin : {n : Nat} -> Fin n -> Maybe (Fin n)
incFin f = strengthen $ shift 1 f
neighbours1 : {n : Nat} -> Fin n -> List (Fin n)
neighbours1 x = catMaybes $ [ decFin x, Just x, incFin x ]

neighbours : {n : Nat} -> Fin (S n) -> Fin (S n) -> List (Fin (S n), Fin (S n))
neighbours x y = delete (x, y) $ join $ (\x => (x,) <$> (neighbours1 y)) <$> neighbours1 x

incNeighbours : {n : Nat} -> List (Fin (S n), Fin (S n)) -> Grid n Flash -> Grid n Flash
incNeighbours [] g = g
incNeighbours ((x, y) :: ps) g = case index x $ index y $ g of
                                      Flashed => incNeighbours ps g
                                      (E e) => case incEnergy e of
                                                    Flashed => incNeighbours (neighbours x y ++ ps) (updateAt y (replaceAt x Flashed) g)
                                                    en@(E _) => incNeighbours ps (updateAt y (replaceAt x en) g)

step : {n : Nat} -> Grid n Energy -> Grid n Flash
step {n} g = let gf = (E <$>) <$> g
                 ps = join $ (\y => (, y) <$> (forget $ allFins n)) <$> (forget $ allFins n) in
                 incNeighbours ps gf

reset : Grid n Flash -> (Nat, Grid n Energy)
reset g = (sum $ count isFlash <$> g, (resetFlash <$>) <$> g)

simulate : {n : Nat} -> Nat -> Grid n Energy -> Nat
simulate 0 = const 0
simulate (S s) = (\(f, g) => f + simulate s g) . reset . step

allFlash : {n : Nat} -> Nat -> Grid n Energy -> Nat
allFlash s g = let (c, gf) = reset $ step g in
                 if c == (S n) * (S n)
                    then S s
                    else allFlash (S s) gf

run : String -> IO ()
run s = do Right (MkDPair n g, _) <- pure $ parse parser s
             | Left err => putStrLn $ show err
           putStrLn $ show $ simulate 195 g
           putStrLn $ show $ allFlash 0 g

main : IO ()
main = do Right s <- readFile "input.txt"
            | Left err => putStrLn $ show err
          run s

ext: idr


text:
module Main

{-- comment 1 --}

someFunction : IO ()

{-- comment 2 --}

main : IO ()
main = do
    someFunction
    pure ()


text:
module Numeric
import Data.Nat

%default total

||| Well-founded Integer.  All Integers are either a natural number or
||| the inversion of a positive number.
public export
data WFInt : Type where
     Nat : (n : Nat) -> WFInt
     Neg : (n : Nat) -> WFInt --Note: In the negative case, n=Z represents -1.

||| Casting from well founded to normal integer
public export
Cast WFInt Integer where
     cast (Nat n) = cast n
     cast (Neg n) = negate $ cast (S n)

||| Casting from normal to well founded integer
public export
Cast Integer WFInt where
     cast n = case (compare n 0) of
           EQ => Nat (fromInteger n)
           GT => Nat (fromInteger n)
           LT => Neg (fromInteger $ negate $ n + 1)

||| For arithmetic operations, cast to Integer and then cast back
public export
Num WFInt where
   (+) a b = cast $ (cast a) + (cast b)
   (*) a b = cast $ (cast a) * (cast b)
   fromInteger a = cast a

public export
Neg WFInt where
    negate a = cast $ negate $ (the Integer $ cast a)
    (-) a b = cast $ (the Integer $ cast a) - (the Integer $ cast b)

public export
partial
Integral WFInt where
         div a b = cast $ the Integer $ div (cast a) (cast b)
         mod a b = cast $ the Integer $ mod (cast a) (cast b)

||| n-parity, i.e. proof that an integer a is evenly divisible by n.
public export
data Parity : (a : WFInt) -> (n : WFInt) -> Type where
     -- a has even n-parity if there exists an integer multiple x s.t. x*n = a.
     Factor : (x : WFInt ** (x * n) = a) -> Parity a n

||| Alias type for even integer
public export
EvenInteger : Type
EvenInteger = (n : WFInt ** Parity n 2)

||| Casting from even to normal integer
public export
Cast EvenInteger Integer where
     cast x = cast (the WFInt (fst x))

||| Force an integer to be even
force_even : Integer -> Integer
force_even x = case (mod x 2) of
                    0 => x
                    _ => x - 1

||| Implement casting from normal to even integer
-- TODO: solve ?pr by using EvenNat
public export
Cast Integer EvenInteger where
     cast e = ((cast (force_even e)) ** (Factor ((div (cast e) 2) ** ?pr)))

max_stars_repo_name: nunet-io/ai-dsl

max_issues_repo_name: nunet-io/ai-dsl

max_forks_repo_name: nunet-io/ai-dsl


text:
module IntNum

import IntEqOrd

-- This file to be deleted once these interfaces are added to prelude

-- Int8

%inline
public export
Num Int8 where
  (+) = prim__add_Int8
  (*) = prim__mul_Int8
  fromInteger = prim__cast_IntegerInt8

public export
Neg Int8 where
  negate x = prim__sub_Int8 0 x
  (-) = prim__sub_Int8

public export
Abs Int8 where
  abs x = if x < 0 then -x else x

public export
Integral Int8 where
  div x y
      = case y == 0 of
             False => prim__div_Int8 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Int8 x y

-- Int16

%inline
public export
Num Int16 where
  (+) = prim__add_Int16
  (*) = prim__mul_Int16
  fromInteger = prim__cast_IntegerInt16

public export
Neg Int16 where
  negate x = prim__sub_Int16 0 x
  (-) = prim__sub_Int16

public export
Abs Int16 where
  abs x = if x < 0 then -x else x

public export
Integral Int16 where
  div x y
      = case y == 0 of
             False => prim__div_Int16 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Int16 x y

-- Int32

%inline
public export
Num Int32 where
  (+) = prim__add_Int32
  (*) = prim__mul_Int32
  fromInteger = prim__cast_IntegerInt32

public export
Neg Int32 where
  negate x = prim__sub_Int32 0 x
  (-) = prim__sub_Int32

public export
Abs Int32 where
  abs x = if x < 0 then -x else x

public export
Integral Int32 where
  div x y
      = case y == 0 of
             False => prim__div_Int32 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Int32 x y

-- Int64

%inline
public export
Num Int64 where
  (+) = prim__add_Int64
  (*) = prim__mul_Int64
  fromInteger = prim__cast_IntegerInt64

public export
Neg Int64 where
  negate x = prim__sub_Int64 0 x
  (-) = prim__sub_Int64

public export
Abs Int64 where
  abs x = if x < 0 then -x else x

public export
Integral Int64 where
  div x y
      = case y == 0 of
             False => prim__div_Int64 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Int64 x y

-- Bits8

public export
Neg Bits8 where
  negate x = prim__sub_Bits8 0 x
  (-) = prim__sub_Bits8

public export
Abs Bits8 where
  abs = id

public export
Integral Bits8 where
  div x y
      = case y == 0 of
             False => prim__div_Bits8 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Bits8 x y

-- Bits16

public export
Neg Bits16 where
  negate x = prim__sub_Bits16 0 x
  (-) = prim__sub_Bits16

public export
Abs Bits16 where
  abs = id

public export
Integral Bits16 where
  div x y
      = case y == 0 of
             False => prim__div_Bits16 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Bits16 x y

-- Bits32

public export
Neg Bits32 where
  negate x = prim__sub_Bits32 0 x
  (-) = prim__sub_Bits32

public export
Abs Bits32 where
  abs = id

public export
Integral Bits32 where
  div x y
      = case y == 0 of
             False => prim__div_Bits32 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Bits32 x y

-- Bits64

public export
Neg Bits64 where
  negate x = prim__sub_Bits64 0 x
  (-) = prim__sub_Bits64

public export
Abs Bits64 where
  abs = id

public export
Integral Bits64 where
  div x y
      = case y == 0 of
             False => prim__div_Bits64 x y
  mod x y
      = case y == 0 of
             False => prim__mod_Bits64 x y

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
data PowerSource = Petrol | Pedal | Electric

data Vehicle : PowerSource -> Type where
    Unicycle : Vehicle Pedal
    Bicycle : Vehicle Pedal
    Car : (fuel : Nat) -> Vehicle Petrol
    Bus : (fuel : Nat) -> Vehicle Petrol
    Motorcycle : (fuel : Nat) -> Vehicle Petrol

wheels : Vehicle power -> Nat
wheels Unicycle = 1
wheels Bicycle = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4
wheels (Motorcycle fuel) = 2

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200
refuel (Motorcycle fuel) = Motorcycle 50
refuel Bicycle impossible
refuel Unicycle impossible

max_stars_repo_name: DimaSamoz/idris-book

max_issues_repo_name: DimaSamoz/idris-book

max_forks_repo_name: DimaSamoz/idris-book


text:
module IdrisScript.Arrays

import IdrisScript

%access public export

infixr 7 ++

Array : JS_IO (JSValue JSFunction)
Array = do
  arr <- jscall "Array" (JS_IO Ptr)
  pure $ MkJSFunction arr

||| Creates an empty JavaScript array.
empty : JS_IO (JSValue JSArray)
empty = do
  arr <- jscall "new Array()" (JS_IO Ptr)
  pure $ MkJSObject arr

||| Appends two JavaScript arrays.
(++) : JSValue JSArray -> JSValue JSArray -> JS_IO (JSValue JSArray)
arr ++ arr' = do
  res <- jscall "%0.concat(%1)" (Ptr -> Ptr -> JS_IO Ptr)
                (unpack arr) (unpack arr')
  pure $ MkJSObject res

||| Inserts a JavaScript value at position `idx`. Modifies the original value.
||| @ idx insert position.
insert : (idx : Nat) -> JSValue t -> JSValue JSArray -> JS_IO (JSValue JSArray)
insert idx val arr = do
  jscall "%0[%1] = %2" (Ptr -> Int -> Ptr -> JS_IO ())
    (unpack arr) (cast idx) (unpack val)
  pure arr

||| Returns the position of `val` in the array `arr`. Returns -1
||| if `val` is not present.
indexOf : (val : JSValue a) -> (arr : JSValue JSArray) -> JS_IO Int
indexOf val arr =
  jscall "%0.indexOf(%1)" (Ptr -> Ptr -> JS_IO Int)
    (unpack arr) (unpack val)

||| Flatten nested arrays.
join : JSValue JSArray -> JS_IO (JSValue JSArray)
join arr = do
  res <- jscall "%0.join()" (Ptr -> JS_IO Ptr) (unpack arr)
  pure $ MkJSObject res

||| Reverse an array. Modifies the original value.
reverse : JSValue JSArray -> JS_IO (JSValue JSArray)
reverse arr = do
  res <- jscall "%0.reverse()" (Ptr -> JS_IO Ptr) (unpack arr)
  pure $ MkJSObject res

||| Sort an array. Modifies the original value.
sort : JSValue JSArray -> JS_IO (JSValue JSArray)
sort arr = do
  res <- jscall "%0.sort()" (Ptr -> JS_IO Ptr) (unpack arr)
  pure $ MkJSObject res

||| Pushes the value `val` to the end of a array. Modifies original value.
push : JSValue JSArray -> (val : JSValue t) -> JS_IO ()
push arr val =
      jscall "%0.push(%1)" (Ptr -> Ptr -> JS_IO ())
              (unpack arr) (unpack val)

||| Pops a value from a the end of an array. Modifies the original value.
pop : JSValue JSArray -> JS_IO (Maybe (t : JSType ** JSValue t))
pop arr = do
  elm <- jscall "%0.pop()" (Ptr -> JS_IO Ptr) (unpack arr)
  case !(typeOf elm) of
       JSUndefined => pure Nothing
       _           => pure $ Just !(pack elm)

infixl 6 !!
(!!) : JSValue JSArray -> (idx : Nat) -> JS_IO (Maybe (t : JSType ** JSValue t))
arr !! idx = do
  elm <- jscall "%0[%1]" (Ptr -> Int -> JS_IO Ptr)
              (unpack arr) (cast idx)
  case !(typeOf elm) of
       JSUndefined => pure Nothing
       _           => pure $ Just !(pack elm)

||| Pops an element from the front of an array. Modifies the original value.
shift : JSValue JSArray -> JS_IO (Maybe (t ** JSValue t))
shift arr = do
  elm <- jscall "%0.shift()" (Ptr -> JS_IO Ptr) (unpack arr)
  case !(typeOf elm) of
       JSUndefined => pure Nothing
       _           => pure $ Just !(pack elm)

||| Pushes an element to the front of an array. Modifies the original value.
unshift : JSValue JSArray -> JSValue a -> JS_IO Nat
unshift arr val = do
  res <- jscall "%0.unshift(%1)" (Ptr -> Ptr -> JS_IO Int)
                 (unpack arr) (unpack val)
  pure $ cast {to=Nat} res

||| Return the head element of an array.
head : JSValue JSArray -> JS_IO (Maybe (t ** JSValue t))
head arr = do
  elm <- jscall "%0[0]" (Ptr -> JS_IO Ptr) (unpack arr)
  case !(typeOf elm) of
       JSUndefined => pure Nothing
       _           => pure $ Just !(pack elm)

||| Return the tail of an array. Returns an empty array in case
||| of an empty array.
tail : JSValue JSArray -> JS_IO (JSValue JSArray)
tail arr = do
  elm <- jscall
      """(function(arr) {
           return arr.slice(1, arr.length);
         })(%0)""" (Ptr -> JS_IO Ptr) (unpack arr)

  pure (MkJSObject elm)

||| Slices out an array form position `form` to `to`. Modifies original value.
slice : JSValue JSArray -> (from : Int) -> (to : Int) -> JS_IO (JSValue JSArray)
slice arr from to = do
  res <- jscall "%0.slice(%1,%2)" (Ptr -> Int -> Int -> JS_IO Ptr)
                (unpack arr) from to
  pure $ MkJSObject res

||| Creates an array with a single element.
singleton : JSValue t -> JS_IO (JSValue JSArray)
singleton val = do
  arr <- jscall "[%0]" (Ptr -> JS_IO Ptr) (unpack val)
  pure $ MkJSObject arr

||| Return the length of an array.
length : JSValue JSArray -> JS_IO Nat
length arr = do
  len <- jscall "%0.length" (Ptr -> JS_IO Int) (unpack arr)
  pure $ cast len

||| Runs an `JS_IO` action for every element of an array.
forEach : (JSRef -> JS_IO ()) -> JSValue JSArray -> JS_IO ()
forEach f arr =
    jscall "(function(arr,f){for(var i=0;i<arr.length;i++)f(arr[i])})(%0,%1)"
        (Ptr -> JsFn (Ptr -> JS_IO ()) -> JS_IO ())
         (unpack arr) (MkJsFn f)

||| Creates an arry from a `Traversable` data structure.
toJSArray : (Traversable f, ToJS from to) => f from -> JS_IO (JSValue JSArray)
toJSArray {from} {to} xs = do
  arr <- empty
  traverse_ (\x => arr `push` (toJS {from} {to} x)) xs
  pure arr

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module Quotient_Group

import Monoid
import Group
import Group_property
import Group_property2

%access public export

||| Given a map f : g -> h, the image of f along with the proofs
total
ImageOf : (x : Type) -> (y : Type) -> (f : x -> y) -> Type
ImageOf x y f = (b : y ** (a : x ** ( (f a) = b)))

||| Generates the (right) coset over h of a given element in g
total
Coset: (h : Type) -> ((+) : h -> h -> h) -> (pf1 : IsGroup h (+)) ->
       (g : Type) -> ((*) : g -> g -> g) -> (pf2 : IsGroup g (*)) ->
       (Subgroup h (+) pf1 g (*) pf2) -> (a : g) -> Type

Coset h (+) pf1 g (*) pf2 (f ** pfSub) a = (y : g ** (y1 : ImageOf h g f ** ((fst y1)*a = y)))
--Imgfn h g (\r => a*(fst(sbgrp) r))

||| The property that a particular element is in the coset
total
Is_in_Coset : (h : Type) -> ((+) : h -> h -> h) -> (pf1 : IsGroup h (+)) ->
              (g : Type) -> ((*) : g -> g -> g) -> (pf2 : IsGroup g (*)) ->
              (Subgroup h (+) pf1 g (*) pf2) -> (a : g) -> (b : g) -> Type

Is_in_Coset h (+) pf1 g (*) pf2 (f ** pfSub) a b = (y1 : ImageOf h g f ** ((fst y1)*a = b))

||| If b is in the coset of a, then a is in the coset of b
total
Coset_property_1 : (h : Type) -> ((+) : h -> h -> h) -> (pf1 : IsGroup h (+)) ->
                   (g : Type) -> ((*) : g -> g -> g) -> (pf2 : IsGroup g (*)) ->
                   (Subgroup h (+) pf1 g (*) pf2) -> (a : g) -> (b : g) ->
                   (Is_in_Coset  h (+) pf1 g (*) pf2 (f ** pfSub) a b) ->
                   (Is_in_Coset  h (+) pf1 g (*) pf2 (f ** pfSub) b a)

Coset_property_1 h (+) pfh g (*) pfg pfSub a b pf_a_in_Cb = let
                                                            y = fst (fst pf_a_in_Cb)
                                                            x = fst (snd (fst pf_a_in_Cb))
                                                            pf_fx_is_y = (snd (snd (fst pf_a_in_Cb))) -- proof that (f x) = y
                                                            pfy = snd pf_a_in_Cb -- proof that y*a = b

                                                            f = (fst pfSub) -- the inclusion map from h to g
                                                            pfhom = (fst (snd pfSub)) -- proof that f is a homomorphism

                                                            x1 = Inv h (+) pfh x
                                                            y1.1 = (f x1)
                                                            y1.2 = Inv g (*) pfg y
                                                            pf_y12_eq = (Group_property_8 h (+) pfh g (*) pfg f pfhom x1) -- proof that
                                                                                -- y1.1 = y1.2

                                                            in
                                                            ?rhs

{-
||| Property 2 - A proof that C(a) * C(b) and C(a*b) are equal as sets
total
Coset_property_2 : (h : Type) -> ((+) : h -> h -> h) -> (pf1 : IsGroup h (+)) ->
                   (g : Type) -> ((*) : g -> g -> g) -> (pf2 : IsGroup g (*)) ->
                   (Subgroup h (+) pf1 g (*) pf2) -> Type
-}


text:
import Data.Fin

foo : (n : Nat) -> (i : Fin n) -> Bool
foo n@(_) i = ?foo_rhs


text:
module Node.Core

%access public export
%default total

{-
  Proof and Type Function helpers
-}
ffi_js : Type -> Type
ffi_js = FTy FFI_JS []

JsMethod : Type -> Type -> Type
JsMethod a b = Ptr -> String -> a -> JS_IO b

JsProp : (a : Type) -> Type
JsProp a = Ptr -> String -> JS_IO a

||| The infamous `eval` function. As evil as they come, it'll let you escape
||| this fantasy land and access the node environment. Use with care.
|||
||| @s the raw string to be evaluated
eval : { ty : Type } -> { auto prf : (ffi_js ty) } -> ( s : String ) -> ty
eval { ty } s = foreign FFI_JS s ty

||| General property accessing, useful for quickly exatracting properties from
||| objects, be it primitives or pointers to other objects
|||
||| @ty the type of the value to be retrieved
prop : { auto ty : Type } -> { auto prf : (ffi_js (JsProp ty)) } -> JsProp ty
prop {ty} = eval { ty = (JsProp ty) } "%0[%1]"

||| General method application, unary thou.
|||
||| @a method input type
||| @b method output type
method : { auto a : Type } ->
         { auto b : Type } ->
         { auto prf : (ffi_js (JsMethod a b)) } -> JsMethod a b
method {a} {b} = eval { ty = (JsMethod a b) } "%0[%1](%2)"

||| Logging utility using the default global `console` object
|||
||| @s the string to log
log : (s : String) -> JS_IO ()
log s = do console <- eval { ty = JS_IO Ptr } "console"
           method { a = String } { b = () } console "log" s

||| Default require wrapper; relies on the globally available require function
||| to import packages as pointers.
|||
||| @name package name to require
require : (name : String) -> JS_IO Ptr
require = eval { ty = (String -> JS_IO Ptr) } "require(%0)"

max_stars_repo_name: ostera/idris-coda

max_issues_repo_name: ostera/idris-coda

max_forks_repo_name: ostera/idris-coda


text:
data Expr = Val Int
          | Add Expr Expr
          | Sub Expr Expr
          | Mul Expr Expr

evaluate : Expr -> Int
evaluate (Val x) = x
evaluate (Add x y) = evaluate x + evaluate y
evaluate (Sub x y) = evaluate x - evaluate y
evaluate (Mul x y) = evaluate x * evaluate y


text:
module NamedImplementations

import Data.List

%default total

-- named implementations allow us to have multiple implementations for a particular interface
-- for a particular type.

{-
  [name] Interface Type where
    func

  and then use as: func @{name} instead of the normal func
-}

[myord] Ord Nat where
  compare Z (S k) = GT
  compare (S k) Z = LT
  compare Z Z = EQ
  compare (S k) (S j) = compare @{myord} k j

testList : List Nat
testList = [3, 4, 1, 2, 3, 5, 4, 4, 5]

normalSort : List Nat -> List Nat
normalSort = sort

reverseSort : List Nat -> List Nat
reverseSort = sort @{myord} -- use the custom interface implementation with the name `myord`

-- this is something that Haskell cannot do - and the reason why it has to define wrapper classes
-- like `Sum` and `Product` in the Data.Monoid module. Named Implementations provides an elegant way
-- out of this boilerplate.

{-
  interface Semigroup ty where
    (<+>) : ty -> ty -> ty

  interface Semigroup ty => Monoid ty where
    neutral : ty
-}

[PlusNatSemi] Semigroup Nat where
  (<+>) x y = x + y

[MultNatSemi] Semigroup Nat where
  (<+>) x y = x * y

[PlusNatMonoid] Monoid Nat using PlusNatSemi where -- note the `using` clause
  neutral = 0

[MultNatMonoid] Monoid Nat using MultNatSemi where
  neutral = 1

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

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

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


text:
module Utils.Time

import Utils.Num
import Data.Fin
import Data.String.Parser
import Data.Vect
import Data.String
import Data.Fin.Extra
import Utils.Misc
import Decidable.Equality
import Generics.Derive

%language ElabReflection

public export
data Month : Type where
  January : Month
  February : Month
  March : Month
  April : Month
  May : Month
  June : Month
  July : Month
  August : Month
  September : Month
  October : Month
  November : Month
  December : Month

export
next_month : Month -> Month
next_month January    = February
next_month February   = March
next_month March      = April
next_month April      = May
next_month May        = June
next_month June       = July
next_month July       = August
next_month August     = September
next_month September  = October
next_month October    = November
next_month November   = December
next_month December   = January

export
prev_month : Month -> Month
prev_month January    = December
prev_month February   = January
prev_month March      = February
prev_month April      = March
prev_month May        = April
prev_month June       = May
prev_month July       = June
prev_month August     = July
prev_month September  = August
prev_month October    = September
prev_month November   = October
prev_month December   = November

public export
next_prev_month : (m : Month) -> (next_month $ prev_month m) = m
next_prev_month January    = Refl
next_prev_month February   = Refl
next_prev_month March      = Refl
next_prev_month April      = Refl
next_prev_month May        = Refl
next_prev_month June       = Refl
next_prev_month July       = Refl
next_prev_month August     = Refl
next_prev_month September  = Refl
next_prev_month October    = Refl
next_prev_month November   = Refl
next_prev_month December   = Refl

public export
prev_next_month : (m : Month) -> (prev_month $ next_month m) = m
prev_next_month January    = Refl
prev_next_month February   = Refl
prev_next_month March      = Refl
prev_next_month April      = Refl
prev_next_month May        = Refl
prev_next_month June       = Refl
prev_next_month July       = Refl
prev_next_month August     = Refl
prev_next_month September  = Refl
prev_next_month October    = Refl
prev_next_month November   = Refl
prev_next_month December   = Refl

export
nat_to_month : Nat -> Maybe Month
nat_to_month 1  = Just January
nat_to_month 2  = Just February
nat_to_month 3  = Just March
nat_to_month 4  = Just April
nat_to_month 5  = Just May
nat_to_month 6  = Just June
nat_to_month 7  = Just July
nat_to_month 8  = Just August
nat_to_month 9  = Just September
nat_to_month 10 = Just October
nat_to_month 11 = Just November
nat_to_month 12 = Just December
nat_to_month _ = Nothing

export
fin_to_month : Fin 12 -> Month
fin_to_month 0  = January
fin_to_month 1  = February
fin_to_month 2  = March
fin_to_month 3  = April
fin_to_month 4  = May
fin_to_month 5  = June
fin_to_month 6  = July
fin_to_month 7  = August
fin_to_month 8  = September
fin_to_month 9  = October
fin_to_month 10 = November
fin_to_month 11 = December

export
month_to_nat : Month -> Nat
month_to_nat January   = 1
month_to_nat February  = 2
month_to_nat March     = 3
month_to_nat April     = 4
month_to_nat May       = 5
month_to_nat June      = 6
month_to_nat July      = 7
month_to_nat August    = 8
month_to_nat September = 9
month_to_nat October   = 10
month_to_nat November  = 11
month_to_nat December  = 12

export
month_num_of_dates : Integer -> Month -> Nat
month_num_of_dates _ January = 31
month_num_of_dates year February =
  if year `mod` 4 /= 0 then 28
    else if year `mod` 100 /= 0 then 29
    else if year `mod` 400 /= 0 then 28
    else 29
month_num_of_dates _ March = 31
month_num_of_dates _ April = 30
month_num_of_dates _ May = 31
month_num_of_dates _ June = 30
month_num_of_dates _ July = 31
month_num_of_dates _ August = 31
month_num_of_dates _ September = 30
month_num_of_dates _ October = 31
month_num_of_dates _ November = 30
month_num_of_dates _ December = 31

%runElab derive "Month" [Generic, Meta, DecEq, Eq, Ord, Show]

public export
data FinNonZero : Fin n -> Type where
  FSIsNonZero : FinNonZero (FS x)

show_nat_pad : Nat -> Nat -> String
show_nat_pad p n =
  let str = show n
      pad_len = minus p $ length str
      pad = replicate pad_len '0'
  in pad <+> str

show_fin_pad : Nat -> Fin n -> String
show_fin_pad p n = show_nat_pad p $ finToNat n

public export
record Date where
  constructor MkDate
  year : Integer
  month : Month
  day : Fin (S (month_num_of_dates year month))
  day_non_zero : FinNonZero day

export
epoch_date : Date
epoch_date = MkDate 1970 January 1 FSIsNonZero

export
Eq Date where
  a == b =
    case decEq a.year b.year of
      Yes prf0 =>
        case decEq a.month b.month of
          Yes prf1 => a.day == (rewrite prf0 in rewrite prf1 in b.day)
          No _ => False
      No _ => False

export
Ord Date where
  a `compare` b =
    case decEq a.year b.year of
      Yes prf0 =>
        case decEq a.month b.month of
          Yes prf1 =>
            let b_day = rewrite prf0 in rewrite prf1 in b.day
            in a.day `compare` b_day
          No _ => a.month `compare` b.month
      No _ => a.year `compare` b.year

export
Show Date where
  show date =
    (show $ date.year)
    <+> "/"
    <+> (show $ month_to_nat date.month)
    <+> "/"
    <+> (show_fin_pad 2 date.day)

date_to_tuple : Date -> (Integer, Integer, Integer)
date_to_tuple date = (date.year, natToInteger $ pred $ month_to_nat date.month, finToInteger date.day - 1)

date_to_normalized_tuple : Date -> (Integer, Month, Integer)
date_to_normalized_tuple date = (date.year, date.month, finToInteger date.day - 1)

tuple_normalize_month : (Integer, Integer, Integer) -> (Integer, Month, Integer)
tuple_normalize_month (year, month, day) =
  ( if month >= 0 then year + month `div` 12 else year + ((month + 1) `div` 12) - 1
  , fin_to_month $ modFinNZ (integerToNat $ month `mod'` 12) 12 SIsNonZero
  , day)

tuple_normalize_next_month : (Integer, Month, Integer) -> (Integer, Month, Integer)
tuple_normalize_next_month (year, month, day) =
  let next = next_month month
      new_year = case month of { December => year + 1; _ => year; }
  in (new_year, next, day - (natToInteger $ month_num_of_dates year month))

tuple_normalize_prev_month : (Integer, Month, Integer) -> (Integer, Month, Integer)
tuple_normalize_prev_month (year, month, day) =
  let prev = prev_month month
      new_year = case month of { January => year - 1; _ => year; }
  in (new_year, prev, day + (natToInteger $ month_num_of_dates year prev))

tuple_normalize_day : (Integer, Month, Integer) -> Date
tuple_normalize_day (year, month, day) =
  case integerToFin day (month_num_of_dates year month) of
    Just day' => MkDate year month (FS day') FSIsNonZero
    Nothing =>
      if day < 0
        then tuple_normalize_day $ tuple_normalize_prev_month (year, month, day)
        else tuple_normalize_day $ tuple_normalize_next_month (year, month, day)

tuple_normalize_date : (Integer, Integer, Integer) -> Date
tuple_normalize_date = tuple_normalize_day . tuple_normalize_month

days_between_dates' : (Integer, Month, Integer) -> (Integer, Month, Integer) -> Integer
days_between_dates' a@(a_year, a_month, a_day) b@(b_year, b_month, b_day) =
  case collapse_ordering [a_year `compare` b_year, a_month `compare` b_month] of
    LT => days_between_dates' (tuple_normalize_next_month a) b
    GT => days_between_dates' (tuple_normalize_prev_month a) b
    EQ => a_day - b_day

export
days_between_dates : Date -> Date -> Integer
days_between_dates a b = days_between_dates' (date_to_normalized_tuple a) (date_to_normalized_tuple b)

day_in_seconds : Nat
day_in_seconds = 24 * 60 * 60

day_in_milliseconds : Nat
day_in_milliseconds = 24 * 60 * 60 * 1000

day_in_seconds' : Integer
day_in_seconds' = natToInteger day_in_seconds

day_in_milliseconds' : Integer
day_in_milliseconds' = natToInteger day_in_milliseconds

public export
record DateTime where
  constructor MkDateTime
  date : Date
  hour : Fin 24
  minute : Fin 60
  second : Fin 60
  subsecond : Fin 1000
  offset_plus_or_minus : Bool
  hour_offset : Nat
  minute_offset : Fin 60

second_of_day : Nat -> (Fin 24, Fin 60, Fin 60)
second_of_day x =
  let second = modFinNZ x 60 SIsNonZero
      x = divNatNZ x 60 SIsNonZero
      minute = modFinNZ x 60 SIsNonZero
      x = divNatNZ x 60 SIsNonZero
      hour = modFinNZ x 24 SIsNonZero
  in (hour, minute, second)

export
epoch_to_datetime : Integer -> DateTime
epoch_to_datetime epoch =
  let (hour, minute, second) = second_of_day $ integerToNat $ epoch `mod'` day_in_seconds'
      dayno = if epoch >= 0 then epoch `div` day_in_seconds' else ((epoch + 1) `div` day_in_seconds') - 1
      date = tuple_normalize_date (1970, 0, dayno)
  in MkDateTime date hour minute second 0 True 0 0

export
millisecond_epoch_to_datetime : Integer -> DateTime
millisecond_epoch_to_datetime epoch =
  let subsecond' = integerToNat $ epoch `mod'` 1000
  in { subsecond := modFinNZ subsecond' 1000 SIsNonZero } (epoch_to_datetime $ epoch `div` 1000)

datetime_to_epoch' : DateTime -> Integer
datetime_to_epoch' datetime =
  (days_between_dates datetime.date epoch_date) * day_in_seconds'
  + (finToInteger datetime.hour * 60 * 60)
  + (finToInteger datetime.minute * 60)
  + (finToInteger datetime.second)

millisecond_datetime_to_epoch' : DateTime -> Integer
millisecond_datetime_to_epoch' datetime = (datetime_to_epoch' datetime) * 1000 + finToInteger datetime.subsecond

export
gmt_datetime : DateTime -> DateTime
gmt_datetime datetime =
  let epoch = millisecond_datetime_to_epoch' datetime
      offset = (1000 * 3600 * natToInteger datetime.hour_offset) + (1000 * 60 * finToInteger datetime.minute_offset)
      epoch = if datetime.offset_plus_or_minus then epoch - offset else epoch + offset
  in millisecond_epoch_to_datetime epoch

export
datetime_to_epoch : DateTime -> Integer
datetime_to_epoch = datetime_to_epoch' . gmt_datetime

export
millisecond_datetime_to_epoch : DateTime -> Integer
millisecond_datetime_to_epoch = millisecond_datetime_to_epoch' . gmt_datetime

export
Show DateTime where
  show datetime =
    (show $ datetime.date)
    <+> " "
    <+> (show_fin_pad 2 datetime.hour)
    <+> ":"
    <+> (show_fin_pad 2 datetime.minute)
    <+> ":"
    <+> (show_fin_pad 2 datetime.second)
    <+> "."
    <+> (show_fin_pad 3 datetime.subsecond)
    <+> " "
    <+> (if datetime.offset_plus_or_minus then "+" else "-")
    <+> (show_nat_pad 2 datetime.hour_offset)
    <+> ":"
    <+> (show_fin_pad 2 datetime.minute_offset)

fromDigits : Num a => (Fin 10 -> a) -> List (Fin 10) -> a
fromDigits f xs = foldl addDigit 0 xs
  where
    addDigit : a -> Fin 10 -> a
    addDigit num d = 10*num + f d

natFromDigits : List (Fin 10) -> Nat
natFromDigits = fromDigits finToNat

natFromNDigits : Monad m => Nat -> ParseT m Nat
natFromNDigits n = natFromDigits . toList <$> ntimes n digit

finNFromNDigits : Monad m => String -> (n : Nat) -> Nat -> ParseT m (Fin n)
finNFromNDigits name bound n = do
  number <- natFromNDigits n
  case natToFin number bound of
    Just fin => pure fin
    Nothing => fail $ "invalid " <+> name <+> ": " <+> show number

export
utc_time : Monad m => ParseT m DateTime
utc_time = do
  yy <- natFromDigits . toList <$> ntimes 2 digit
  mm <- natFromDigits . toList <$> ntimes 2 digit
  let year = if yy < 50 then 2000 + natToInteger yy else 1900 + natToInteger yy
  let Just month = nat_to_month mm
  | Nothing => fail $ "invalid month: " <+> show mm
  FS fs_day <- finNFromNDigits "day" (S $ month_num_of_dates year month) 2
  | FZ => fail "invalid day: 0"
  hour <- finNFromNDigits "hour" 24 2
  minute <- finNFromNDigits "minute" 60 2
  second <- option 0 $ finNFromNDigits "second" 60 2
  sign <- satisfy (const True)
  let date = MkDate year month (FS fs_day) FSIsNonZero
  let mk_date_time = MkDateTime date hour minute second 0
  case sign of
    'Z' => pure $ mk_date_time True 0 0
    '+' => uncurry (mk_date_time True) <$> utc_time_offset
    '-' => uncurry (mk_date_time False) <$> utc_time_offset
    err => fail $ "unrecognized timezone sign: " <+> show err
  where
    utc_time_offset : ParseT m (Nat, Fin 60)
    utc_time_offset = do
      hh <- natFromDigits . toList <$> ntimes 2 digit
      minute_off <- finNFromNDigits "minute offset" 60 2
      pure (hh, minute_off)

export
generalized_time : Monad m => ParseT m DateTime
generalized_time = do
  year <- natToInteger . natFromDigits . toList <$> ntimes 4 digit
  mm <- natFromDigits . toList <$> ntimes 2 digit
  let Just month = nat_to_month mm
  | Nothing => fail $ "invalid month: " <+> show mm

  FS fs_day <- finNFromNDigits "day" (S $ month_num_of_dates year month) 2
  | FZ => fail "invalid day: 0"

  hour <- finNFromNDigits "hour" 24 2
  minute <- option 0 $ finNFromNDigits "minute" 60 2
  second <- option 0 $ finNFromNDigits "second" 60 2

  subsecond <- option 0 subsecond

  sign <- satisfy (const True)
  let date = MkDate year month (FS fs_day) FSIsNonZero
  let mk_date_time = MkDateTime date hour minute second subsecond
  case sign of
    'Z' => pure $ mk_date_time True 0 0
    '+' => uncurry (mk_date_time True) <$> utc_time_offset
    '-' => uncurry (mk_date_time False) <$> utc_time_offset
    err => fail $ "unrecognized timezone sign: " <+> show err
  where
    utc_time_offset : ParseT m (Nat, Fin 60)
    utc_time_offset = do
      hh <- natFromDigits . toList <$> ntimes 2 digit
      minute_off <- finNFromNDigits "minute offset" 60 2
      pure (hh, minute_off)
    subsecond : ParseT m (Fin 1000)
    subsecond = do
      a <- char '.' *> natFromNDigits 1
      b <- option 0 $ natFromNDigits 1
      c <- option 0 $ natFromNDigits 1
      case natToFin (a * 100 + b * 10 + c) 1000 of
        Just x => pure x
        Nothing => fail "how"

export
parse_utc_time : String -> Either String DateTime
parse_utc_time = map fst . parse utc_time

export
parse_generalized_time : String -> Either String DateTime
parse_generalized_time = map fst . parse generalized_time


text:
module Invincy.Core

%access public export

interface Monoid s => Stream t s | s where
  single : t -> s
  uncons : s -> Maybe (t, s)
  cons : t -> s -> s
  cons x s = single x <+> s

implementation Stream t (List t) where
  single = pure
  uncons (x::xs) = Just (x, xs)
  uncons [] = Nothing
  cons = (::)

implementation Stream Char String where
  single = singleton
  uncons s = case strM s of
    StrNil => Nothing
    StrCons x xs => Just (x, xs)
  cons = strCons

fromString : Stream Char s => String -> s
fromString = concatMap single . unpack

toList : Stream t s => s -> List t
toList s = case uncons s of
  Nothing => []
  Just (x, xs) => x :: toList xs

fromList : Stream t s => List t -> s
fromList [] = neutral
fromList (x::xs) = cons x $ fromList xs

max_stars_repo_name: defanor/invincy

max_issues_repo_name: defanor/invincy

max_forks_repo_name: defanor/invincy


text:
import Data.Vect

vappend : Vect n a -> Vect m a -> Vect (n+m) a
vappend [] ys = ys
vappend (x :: xs) ys = x :: vappend xs ys


text:
module Main

counts : String -> (Nat, Nat)
counts str = (length (words str), length str)

main : IO ()
main = repl "Enter a string: " show_counts
  where
    show_counts : String -> String
    show_counts x = show (counts x) ++ "\n"

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

sp : PrintString m => CanSleep m => CanSpawn m => (offset : Time) -> m Nat
sp offset = do
  spawn $ do
    for 5 $ do
      printTime offset "spawned, before 1000"
      sleepFor 1.seconds
      printTime offset "spawned, before 2000"
      sleepFor 2.seconds
    printTime offset "spawned, end"
  pure 127

export
program : PrintString m => CanSleep m => CanSpawn m => m Unit
program = do
  offset <- currentTime
  printTime offset "start"
  x <- sp offset
  printTime offset "                      trunk, returned when spawning: \{show x}"
  for 10 $ do
    printTime offset "                      trunk, before 350"
    sleepFor 350.millis
    printTime offset "                      trunk, before 750"
    sleepFor 750.millis
  printTime offset "                      trunk, end"


text:
-- ----------------------------------------------------------------- [ Key.idr ]
-- Module      : Keys
-- Description : Types for Cryptographic Keys
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Crypto.Std.Key

import Crypto.Common
import Data.Bits

||| Keys are vectors of bits.
|||
||| @ v The Visibility of the key with respect to the owner.
||| @ s The setting in which the key is to be used.
||| @ l The length of the key in bits.
data Key : (v : Visibility) -> (s : Setting) -> (l : Nat) -> Type where
  ||| PKE Encryption keys.
  MkEncKey : Bits n -> Key Public Asymm n

  ||| PKE Decryption keys
  MkDecKey : Bits n -> Key Private Asymm n

  ||| DS Signing keys.
  MkSignKey : Bits n -> Key Private Sign n

  ||| DS Verifying keys.
  MkVerifyKey : Bits n -> Key Public Sign n

  ||| Symmetric keys
  MkSymmKey : Bits n -> Key Private Symm n

||| Key pairs
|||
||| @ s The setting in which the key is to be used.
||| @ l The length of the key in bits.
data KeyPair : (s : Setting) -> (l : Nat) -> Type where
  ||| Key pair for PKE.
  |||
  ||| @ pub The public key.
  ||| @ priv The private key.
  MkAsymmKeyPair : (pub : Key Public Asymm n)
                 -> (priv : Key Private Asymm n)
                 -> KeyPair Asymm n

  ||| Key pair for DS.
  |||
  ||| @ sig The signing key.
  ||| @ ver The verifying key.
  MkSignKeyPair : (sig : Key Private Sign n)
                -> (ver : Key Public Sign n)
                -> KeyPair Sign n

data TDESKeyOption = KeyOption1 | KeyOption2 | KeyOption3

||| Representation of a Triple DES
|||
||| @ s The setting in ehich the key is to be used.
||| @ n The length of each key
||| @ option The Keying option used.
data TDESKey : (s : Setting) -> (n : Nat) -> (option : TDESKeyOption)-> Type where
  |||
  MkTDESKey : (key1 : Bits n)
             -> (key2 : Bits n)
             -> (key3 : Bits n)
             -> (opt : TDESKeyOption)
             -> TDESKey Symm n opt
-- --------------------------------------------------------------------- [ EOF ]

max_stars_repo_name: silky/idris-crypto-types

max_issues_repo_name: silky/idris-crypto-types

max_forks_repo_name: silky/idris-crypto-types


text:
module Network.TLS

import public Network.TLS.Core
import public Network.TLS.Certificate
import public Network.TLS.Handle
import public Network.TLS.Parse.DER
import public Network.TLS.Parse.PEM
import public Network.TLS.Verify
import public Network.TLS.Magic


text:
module WebServer.Routes

import WebServer.Requests
import public WebServer.Format

%default total

public export
record Route where
  constructor MkRoute
  method : RequestMethod
  path : String
  format : Format
  handler : Request -> HandlerType format
%name Route route

public export
RouteConfig : Type
RouteConfig = (path : String) ->
              (Request -> HandlerType (parseFormat path)) ->
              Route
public export
routeConfig : RequestMethod -> RouteConfig
routeConfig method path = MkRoute method path (parseFormat path)

public export
delete : RouteConfig
delete = routeConfig Delete
public export
get : RouteConfig
get = routeConfig Get
public export
head : RouteConfig
head = routeConfig Head
public export
options : RouteConfig
options = routeConfig Head
public export
post : RouteConfig
post = routeConfig Post
public export
put : RouteConfig
put = routeConfig Put

public export
Routes : Type
Routes = List Route
%name Routes routes

pathMatch : (reqPath : String) -> (routePath : String) -> Maybe (List String)
pathMatch reqPath routePath =
  if reqPath == routePath then
    Just []
  else
    partsMatch [] (divide reqPath) (divide routePath)

  where

  divide : (path : String) -> List String
  divide = split (== '/')

  partsMatch : (matches : List String) ->
               (req : List String) ->
               (route : List String) ->
               Maybe (List String)
  partsMatch (match :: matches) [] [] = Just (match :: matches)
  partsMatch _ [] _ = Nothing
  partsMatch _ _ [] = Nothing
  partsMatch matches (reqPart :: reqParts) (routePart :: routeParts) =
    if reqPart == routePart then
      partsMatch matches reqParts routeParts
    else case unpack routePart of
      (':' :: chars) => partsMatch (matches ++ [reqPart]) reqParts routeParts
      _              => Nothing

export
handle : Request -> Routes -> Maybe Response
handle req [] = Nothing
handle req (route :: routes) =
  case (method req == method route, path req `pathMatch` path route) of
    (True, Just args) =>
      applyHandler (format route) (handler route req) args
    _ =>
      handle req routes

  where

  str2Nat : String -> Maybe Nat
  str2Nat s = all isDigit (unpack s) `toMaybe` cast s

  applyHandler : (fmt : Format) ->
                 (f : HandlerType fmt) ->
                 (args : List String) ->
                 Maybe Response
  applyHandler (Num format) f (arg :: args) =
    applyHandler format (f !(str2Nat arg)) args
  applyHandler (Str format) f (arg :: args) =
    applyHandler format (f arg) args
  applyHandler End f _ =
    Just f
  applyHandler _ f [] =
    Nothing

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

max_stars_repo_name: camelpunch/idris-web-server

max_issues_repo_name: camelpunch/idris-web-server

max_forks_repo_name: camelpunch/idris-web-server


text:
module Data.Vect.Properties.Fin

import Data.Vect
import Data.Vect.Elem
import Data.Vect.Extra
import Data.Fin
import Data.Nat

||| Witnesses non-empty runtime-irrelevant vectors. Analogous to Data.List.NonEmpty
public export
data NonEmpty : Vect n a -> Type where
  IsNonEmpty : NonEmpty (x :: xs)

||| eta-law (extensionality) of head-tail cons
export
etaCons : (xs : Vect (S n) a) -> head xs :: tail xs = xs
etaCons (x :: xs) = Refl

||| Inhabitants of `Fin n` witness `NonZero n`
export
finNonZero : Fin n -> NonZero n
finNonZero  FZ    = SIsNonZero
finNonZero (FS i) = SIsNonZero

||| Inhabitants of `Fin n` witness runtime-irrelevant vectors of length `n` aren't empty
export
finNonEmpty : (0 xs : Vect n a) -> NonZero n -> NonEmpty xs
finNonEmpty xs SIsNonZero = replace {p = NonEmpty} (etaCons xs) IsNonEmpty

||| Cast an index into a runtime-irrelevant `Vect` into the position
||| of the corresponding element
public export
finToElem : (0 xs : Vect n a) -> (i : Fin n) -> (index i xs) `Elem` xs
finToElem  {n      }       xs  i with (finNonEmpty xs $ finNonZero i)
 finToElem {n = S n} (x :: xs)  FZ    | IsNonEmpty = Here
 finToElem {n = S n} (x :: xs) (FS i) | IsNonEmpty = There (finToElem xs i)

||| Analogus to `indexNaturality`, but morhisms can (irrelevantly) know the context
export
indexNaturalityWithElem : (i : Fin n) -> (xs : Vect n a) -> (f : (x : a) -> (0 pos : x `Elem` xs) -> b)
  -> index i (mapWithElem xs f) = f (index i xs) (finToElem xs i)
indexNaturalityWithElem  {n    } i       xs  f with (finNonEmpty xs (finNonZero i))
 indexNaturalityWithElem {n = _}  FZ    (x :: xs) f | IsNonEmpty = Refl
 indexNaturalityWithElem {n = _} (FS i) (x :: xs) f | IsNonEmpty = indexNaturalityWithElem i xs _


text:
module Data.IntMap

-- Hand specialised map, for efficiency...

%default total

Key : Type
Key = Int

-- TODO: write split

private
data Tree : Nat -> Type -> Type where
  Leaf : Key -> v -> Tree Z v
  Branch2 : Tree n v -> Key -> Tree n v -> Tree (S n) v
  Branch3 : Tree n v -> Key -> Tree n v -> Key -> Tree n v -> Tree (S n) v

branch4 :
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v ->
  Tree (S (S n)) v
branch4 a b c d e f g =
  Branch2 (Branch2 a b c) d (Branch2 e f g)

branch5 :
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v ->
  Tree (S (S n)) v
branch5 a b c d e f g h i =
  Branch2 (Branch2 a b c) d (Branch3 e f g h i)

branch6 :
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v ->
  Tree (S (S n)) v
branch6 a b c d e f g h i j k =
  Branch3 (Branch2 a b c) d (Branch2 e f g) h (Branch2 i j k)

branch7 :
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v -> Key ->
  Tree n v ->
  Tree (S (S n)) v
branch7 a b c d e f g h i j k l m =
  Branch3 (Branch3 a b c d e) f (Branch2 g h i) j (Branch2 k l m)

merge1 : Tree n v -> Key -> Tree (S n) v -> Key -> Tree (S n) v -> Tree (S (S n)) v
merge1 a b (Branch2 c d e) f (Branch2 g h i) = branch5 a b c d e f g h i
merge1 a b (Branch2 c d e) f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
merge1 a b (Branch3 c d e f g) h (Branch2 i j k) = branch6 a b c d e f g h i j k
merge1 a b (Branch3 c d e f g) h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

merge2 : Tree (S n) v -> Key -> Tree n v -> Key -> Tree (S n) v -> Tree (S (S n)) v
merge2 (Branch2 a b c) d e f (Branch2 g h i) = branch5 a b c d e f g h i
merge2 (Branch2 a b c) d e f (Branch3 g h i j k) = branch6 a b c d e f g h i j k
merge2 (Branch3 a b c d e) f g h (Branch2 i j k) = branch6 a b c d e f g h i j k
merge2 (Branch3 a b c d e) f g h (Branch3 i j k l m) = branch7 a b c d e f g h i j k l m

merge3 : Tree (S n) v -> Key -> Tree (S n) v -> Key -> Tree n v -> Tree (S (S n)) v
merge3 (Branch2 a b c) d (Branch2 e f g) h i = branch5 a b c d e f g h i
merge3 (Branch2 a b c) d (Branch3 e f g h i) j k = branch6 a b c d e f g h i j k
merge3 (Branch3 a b c d e) f (Branch2 g h i) j k = branch6 a b c d e f g h i j k
merge3 (Branch3 a b c d e) f (Branch3 g h i j k) l m = branch7 a b c d e f g h i j k l m

treeLookup : Key -> Tree n v -> Maybe v
treeLookup k (Leaf k' v) =
  if k == k' then
    Just v
  else
    Nothing
treeLookup k (Branch2 t1 k' t2) =
  if k <= k' then
    treeLookup k t1
  else
    treeLookup k t2
treeLookup k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    treeLookup k t1
  else if k <= k2 then
    treeLookup k t2
  else
    treeLookup k t3

treeInsert' : Key -> v -> Tree n v -> Either (Tree n v) (Tree n v, Key, Tree n v)
treeInsert' k v (Leaf k' v') =
  case compare k k' of
    LT => Right (Leaf k v, k, Leaf k' v')
    EQ => Left (Leaf k v)
    GT => Right (Leaf k' v', k', Leaf k v)
treeInsert' k v (Branch2 t1 k' t2) =
  if k <= k' then
    case treeInsert' k v t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right (a, b, c) => Left (Branch3 a b c k' t2)
  else
    case treeInsert' k v t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right (a, b, c) => Left (Branch3 t1 k' a b c)
treeInsert' k v (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeInsert' k v t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right (a, b, c) => Right (Branch2 a b c, k1, Branch2 t2 k2 t3)
  else
    if k <= k2 then
      case treeInsert' k v t2 of
        Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
        Right (a, b, c) => Right (Branch2 t1 k1 a, b, Branch2 c k2 t3)
    else
      case treeInsert' k v t3 of
        Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
        Right (a, b, c) => Right (Branch2 t1 k1 t2, k2, Branch2 a b c)

treeInsert : Key -> v -> Tree n v -> Either (Tree n v) (Tree (S n) v)
treeInsert k v t =
  case treeInsert' k v t of
    Left t' => Left t'
    Right (a, b, c) => Right (Branch2 a b c)

delType : Nat -> Type -> Type
delType Z v = ()
delType (S n) v = Tree n v

treeDelete : {n : _} -> Key -> Tree n v -> Either (Tree n v) (delType n v)
treeDelete k (Leaf k' v) =
  if k == k' then
    Right ()
  else
    Left (Leaf k' v)
treeDelete {n=S Z} k (Branch2 t1 k' t2) =
  if k <= k' then
    case treeDelete k t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right () => Right t2
  else
    case treeDelete k t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right () => Right t1
treeDelete {n=S Z} k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeDelete k t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right () => Left (Branch2 t2 k2 t3)
  else if k <= k2 then
    case treeDelete k t2 of
      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
      Right () => Left (Branch2 t1 k1 t3)
  else
    case treeDelete k t3 of
      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
      Right () => Left (Branch2 t1 k1 t2)
treeDelete {n=S (S _)} k (Branch2 t1 k' t2) =
  if k <= k' then
    case treeDelete k t1 of
      Left t1' => Left (Branch2 t1' k' t2)
      Right t1' =>
        case t2 of
          Branch2 a b c => Right (Branch3 t1' k' a b c)
          Branch3 a b c d e => Left (branch4 t1' k' a b c d e)
  else
    case treeDelete k t2 of
      Left t2' => Left (Branch2 t1 k' t2')
      Right t2' =>
        case t1 of
          Branch2 a b c => Right (Branch3 a b c k' t2')
          Branch3 a b c d e => Left (branch4 a b c d e k' t2')
treeDelete {n=(S (S _))} k (Branch3 t1 k1 t2 k2 t3) =
  if k <= k1 then
    case treeDelete k t1 of
      Left t1' => Left (Branch3 t1' k1 t2 k2 t3)
      Right t1' => Left (merge1 t1' k1 t2 k2 t3)
  else if k <= k2 then
    case treeDelete k t2 of
      Left t2' => Left (Branch3 t1 k1 t2' k2 t3)
      Right t2' => Left (merge2 t1 k1 t2' k2 t3)
  else
    case treeDelete k t3 of
      Left t3' => Left (Branch3 t1 k1 t2 k2 t3')
      Right t3' => Left (merge3 t1 k1 t2 k2 t3')

treeToList : Tree n v -> List (Key, v)
treeToList = treeToList' []
  where
    treeToList' : forall n . List (Key, v) -> Tree n v -> List (Key, v)
    treeToList' rest (Leaf k v) = (k, v) :: rest
    treeToList' rest (Branch2 t1 _ t2)
        = treeToList' (treeToList' rest t2) t1
    treeToList' rest (Branch3 t1 _ t2 _ t3)
        = treeToList' (treeToList' (treeToList' rest t3) t2) t1

export
data IntMap : Type -> Type where
  Empty : IntMap v
  M : (n : Nat) -> Tree n v -> IntMap v

export
empty : IntMap v
empty = Empty

export
lookup : Int -> IntMap v -> Maybe v
lookup _ Empty = Nothing
lookup k (M _ t) = treeLookup k t

export
insert : Int -> v -> IntMap v -> IntMap v
insert k v Empty = M Z (Leaf k v)
insert k v (M _ t) =
  case treeInsert k v t of
    Left t' => (M _ t')
    Right t' => (M _ t')

export
insertFrom : List (Int, v) -> IntMap v -> IntMap v
insertFrom = flip $ foldl $ flip $ uncurry insert

export
delete : Int -> IntMap v -> IntMap v
delete _ Empty = Empty
delete k (M Z t) =
  case treeDelete k t of
    Left t' => (M _ t')
    Right () => Empty
delete k (M (S _) t) =
  case treeDelete k t of
    Left t' => (M _ t')
    Right t' => (M _ t')

export
fromList : List (Int, v) -> IntMap v
fromList l = foldl (flip (uncurry insert)) empty l

export
toList : IntMap v -> List (Int, v)
toList Empty = []
toList (M _ t) = treeToList t

||| Gets the Keys of the map.
export
keys : IntMap v -> List Int
keys = map fst . toList

||| Gets the values of the map. Could contain duplicates.
export
values : IntMap v -> List v
values = map snd . toList

treeMap : (a -> b) -> Tree n a -> Tree n b
treeMap f (Leaf k v) = Leaf k (f v)
treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)
treeMap f (Branch3 t1 k1 t2 k2 t3)
    = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)

export
implementation Functor IntMap where
  map _ Empty = Empty
  map f (M n t) = M _ (treeMap f t)

||| Merge two maps. When encountering duplicate keys, using a function to combine the values.
||| Uses the ordering of the first map given.
export
mergeWith : (v -> v -> v) -> IntMap v -> IntMap v -> IntMap v
mergeWith f x y = insertFrom inserted x where
  inserted : List (Key, v)
  inserted = do
    (k, v) <- toList y
    let v' = (maybe id f $ lookup k x) v
    pure (k, v')

||| Merge two maps using the Semigroup (and by extension, Monoid) operation.
||| Uses mergeWith internally, so the ordering of the left map is kept.
export
merge : Semigroup v => IntMap v -> IntMap v -> IntMap v
merge = mergeWith (<+>)

||| Left-biased merge, also keeps the ordering specified  by the left map.
export
mergeLeft : IntMap v -> IntMap v -> IntMap v
mergeLeft = mergeWith const

-- TODO: is this the right variant of merge to use for this? I think it is, but
-- I could also see the advantages of using `mergeLeft`. The current approach is
-- strictly more powerful I believe, because `mergeLeft` can be emulated with
-- the `First` monoid. However, this does require more code to do the same
-- thing.
export
Semigroup v => Semigroup (IntMap v) where
  (<+>) = merge

export
(Semigroup v) => Monoid (IntMap v) where
  neutral = empty


text:
module Graphics.Util.Transforms

import Data.So
import Data.Matrix
import Data.Matrix.Algebraic
import Data.Vect
import Control.Algebra
import Debug.Trace

%access public export

-- ----------------------------------------------------------------- [ Types ]

data Angle = Radians Double | Degree Double

Pos : Type
Pos = Vect 3 Double

TransformationMatrix : Type
TransformationMatrix = Matrix 4 4 Double

vmult : Matrix n m Double -> Vect m Double -> Vect n Double
vmult m v = map (<:> v) m

-- ----------------------------------------------------------------- [ Utilities ]
data Interval : Type where
   MkInterval : (lower : Double) -> (upper : Double) ->
                So (lower < upper) -> Interval

pattern syntax "[" [x] "..." [y] "]" = MkInterval x y Oh
term    syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma

UnitInterval : Interval
UnitInterval = MkInterval 0.0 1.0 Oh

clamp : Double -> Interval -> Double
clamp val (MkInterval lower upper _) =
  if val < lower
  then lower
  else if val > upper
       then upper
       else val

-- ----------------------------------------------------------------- [ Angles ]

export
getRadians : Angle -> Double
getRadians (Radians a) = a
getRadians (Degree a)  = a * pi / 180

private
cosA : Angle -> Double
cosA a = cos $ getRadians a

private
sinA : Angle -> Double
sinA a = sin $ getRadians a

-- ----------------------------------------------------------------- [ Vectors + Matrices ]

||| 3D Vector cross product
cross: Pos -> Pos -> Pos
cross (x1 :: x2 :: x3 :: []) (y1 :: y2 :: y3 :: []) = [x2*y3-x3*y2, x3*y1-x1*y3, x1*y2-x2*y1]

dot: Pos -> Pos -> Double
dot x y = x <:> y

||| scalar multiplication
scalar : Double -> Vect n Double -> Vect n Double
scalar s v = map (\e => s*e) v

norm : Vect n Double -> Double
norm v = sqrt $ v <:> v

||| normalizes a vector to a unit vector
normalize : Vect n Double -> Vect n Double
normalize v = map (\e => e / l ) v
              where l = norm v

||| convert to a row major List
toGl : TransformationMatrix -> Vect 16 Double
toGl m = concat $ transpose m

-- ----------------------------------------------------------------- [ Transformation Matrices ]

identity : TransformationMatrix
identity = [
           [1, 0, 0, 0],
           [0, 1, 0, 0],
           [0, 0, 1, 0],
           [0, 0, 0, 1]
           ]

translate : Pos -> TransformationMatrix
translate (x :: y :: z :: []) = [
           [1, 0, 0, x],
           [0, 1, 0, y],
           [0, 0, 1, z],
           [0, 0, 0, 1]
           ]

scale : Pos -> TransformationMatrix
scale (sx :: sy :: sz :: []) = [
           [sx, 0,  0, 0],
           [0, sy,  0, 0],
           [0,  0, sz, 0],
           [0,  0,  0, 1]
           ]

scaleAll : Double -> TransformationMatrix
scaleAll s = scale [s, s, s]

rotateX : Angle -> TransformationMatrix
rotateX angle = [
           [1,       0,         0,  0],
           [0,  (cos a),  -(sin a), 0],
           [0,  (sin a),   (cos a), 0],
           [0,       0,         0,  1]
           ]
           where a = getRadians angle

rotateY : Angle -> TransformationMatrix
rotateY angle = [
           [  (cos a),       0, (sin a),  0],
           [       0 ,       1,      0 ,  0],
           [ -(sin a),       0, (cos a),  0],
           [       0 ,       0,      0 ,  1]
           ]
           where a = getRadians angle

rotateZ : Angle -> TransformationMatrix
rotateZ angle = [
           [  (cos a), -(sin a), 0,  0],
           [  (sin a),  (cos a), 0,  0],
           [       0 ,       0 , 1,  0],
           [       0 ,       0,  0,  1]
           ]
           where a = getRadians angle

rotate : Vect 3 Angle -> TransformationMatrix
rotate (ax :: ay :: az :: []) = (rotateX ax) <> (rotateY ay) <> (rotateZ az)

-- ----------------------------------------------------------------- [ Projection Matrices ]

orthographicProjection : (Double, Double) -> (Double, Double) -> (Double, Double) -> TransformationMatrix
orthographicProjection (right, left) (top, bottom) (near, far) = [
           [ 2/(right-left),              0,             0,  -(right + left)/ (right-left)],
           [       0,        2/(top-bottom),             0,  -(top+bottom)  / (top-bottom)],
           [       0,                     0, -2/(far-near),  -(far+near)    / (far-near)  ],
           [       0,                     0,             0,                1              ]
           ]

||| Matrix for Perspective Projection
||| @ fov    field of view / viewing angle
||| @ aspect aspect ration for the projection
||| @ clipping near and far clipping planes
perspectiveProjection : (fov: Angle) -> (aspect: Double) -> (clipping: (Double, Double)) -> TransformationMatrix
perspectiveProjection fov aspect (near, far) = [
           [ 2 * near/(right-left),                    0,  (right + left)/ (right-left),              0                ],
           [       0,                2*near/(top-bottom),  (top+bottom)  / (top-bottom),              0                ],
           [       0,                                  0, -(far+near)    / (far - near), -2 * far * near / (far - near)],
           [       0,                                  0,               -1             ,              0                ]
           ]
           where top    = near * tan((getRadians fov)/ 2)
                 bottom = -top
                 right  = top * aspect
                 left   = -right

||| transformation matrix to transform from world coordinates to view coordinates
||| @ eye where the camera aims - a vector
||| @ center location of the center of the camera
||| @ up up direction for the viewer
viewMatrix : (eye: Pos) -> (center: Pos) -> (up: Pos) -> TransformationMatrix
viewMatrix eye center up = (transpose m) ++ [v]
                           where
                               f : Pos
                               f = normalize (eye <-> center)
                               s : Pos
                               s = normalize (cross f up)
                               u : Pos
                               u = cross s f
                               m : Matrix 4 3 Double
                               m = [s, u, (scalar (-1) f), [0,0,0]]
                               v : Vect 4 Double
                               v = [0,0,0,1]

||| a view matrix where the camera is located at the origin and points down the z-axis
||| while the y-axis is the "up" direction
defaultViewMatrix : TransformationMatrix
defaultViewMatrix = viewMatrix [0,0,-1] [0,0,0] [0,1,0]

||| a view matrix for a camer located at the origin
||| @ eye direction of the camera (where the camera is pointing)
standardViewMatrix : (eye: Pos) -> TransformationMatrix
standardViewMatrix eye = viewMatrix eye [0,0,0] [0,1,0]

-- ----------------------------------------------------------------- [ Quaternions ]

-- Quaternions
-- TODO: introduce a separate type for unit quaternions
namespace Quaternions

  record Quaternion where
    constructor Q
    scalar : Double
    vector : Vect 3 Double

  realPart : Quaternion -> Double
  realPart = scalar

  imagPart : Quaternion -> Vect 3 Double
  imagPart = vector

  qnorm : Quaternion -> Double
  qnorm (Q s v) = let q = s :: v
                  in norm q

  implementation Show Quaternion where
    show (Q s (v1 :: v2 :: v3 :: [])) = (show s)++" + " ++ (show v1) ++"i + "++ (show v2) ++ "k + "++ (show v3)++"j"

  implementation Eq Quaternion where
    (==) q p = realPart q == realPart p && imagPart q == imagPart p

  ||| returns the quaternion as a 4 dimensional Vector with the scalar part last
  ||| this corresponds to the representation as a (x,y,z,w) vector
  toVect : Quaternion -> Vect 4 Double
  toVect (Q s v) = v ++ [s]

  fromVect : Vect 4 Double -> Quaternion
  fromVect (x :: y :: z :: w :: Nil) = Q w [x, y, z]

  export
  fromAxis : (rotation: Angle) -> (axis: Vect 3 Double) -> Quaternion
  fromAxis rot (bx :: by :: bz :: Nil) =
    let a = (getRadians rot) / 2
    in Q (cos a) [(sin a)*bx, (sin a)*by, (sin a)*bz]

  toMatrix : Quaternion -> TransformationMatrix
  toMatrix q@(Q w (x :: y :: z :: Nil)) =
    let s = 2 / (qnorm q)
    in [
       [(1-s*(y*y+z*z)),     s*(x*y-w*z),       s*(x*z+w*y),   0],
       [    s*(x*y+w*z),  (1-s*(x*x+z*z)),      s*(y*z-w*x),   0],
       [    s*(x*z-w*y),     s*(y*z+w*x),    (1-s*(x*x+y*y)),  0],
       [              0,               0,                 0,   1]
       ]

  conjugate : Quaternion -> Quaternion
  conjugate (Q s v) = Q s (scalar (-1) v)

  qsum : Quaternion -> Quaternion -> Quaternion
  qsum (Q s1 v1) (Q s2 v2) = Q (s1+s2) (v1 <+> v2)

  qmultiply : Quaternion -> Quaternion -> Quaternion
  qmultiply (Q s1 v1) (Q s2 v2) = Q (s1*s2 - (dot v1 v2)) ( (scalar s1 v2) <+> (scalar s2 v1) <+> (cross v1 v2))

  qinverse : Quaternion -> Quaternion
  qinverse q@(Q s v) = let q' = s :: v
                           q'' = (1 / (q' <:> q'))
                       in Q (s / q'') (scalar q'' v)

  ||| Exponential e^q
  qexp : Quaternion -> Quaternion
  qexp (Q s v) = let n = norm v
                     e = exp s
                 in Q (e * cos n) ( scalar ((sin n) / n) v)

  qlog : Quaternion -> Quaternion
  qlog q@(Q s v) = let q' = qnorm q
                   in Q (log q') (scalar ((acos (s / q')) / (norm v)) v)

  qnormalize : Quaternion -> Quaternion
  qnormalize q = fromVect $ normalize (toVect q)

  ||| x ^ y
  rpow : Double -> Double -> Double
  rpow y x = let e = x * (log (abs y))
             in if y < 0
                then 1 / (exp e)
                else if y > 0
                     then exp e
                     else 1

  ||| q^t where t is a Real
  qpow : Quaternion -> Double -> Quaternion
  qpow q@(Q s v) a = let e     = (rpow (qnorm q) a)
                         theta = acos (s / (qnorm q))
                     in Q (e * cos (s * theta)) (scalar (sin (s*theta)) v)

  ||| scalar multiplication
  qscalar : Double -> Quaternion -> Quaternion
  qscalar s (Q w v) = Q (s*w) (scalar s v)

  data GimbalPole = NorthPole | SouthPole | NoPole

  ||| Get the pole of the gimbal lock, if any.
  ||| If we have either a north pole or a south pole there is a gimbal lock
  gimbalPole : Quaternion -> GimbalPole
  gimbalPole (Q s v) = let v' = s :: v
                           n' = v' <:> v'
                       in if n' > 0.499
                          then NorthPole
                          else if n' < -0.499
                               then SouthPole
                               else NoPole

  gimbalMultiplier : GimbalPole -> Double
  gimbalMultiplier NoPole    = 0
  gimbalMultiplier NorthPole = 1
  gimbalMultiplier SouthPole = -1

  -- conversion between euler angles and quaternions
  -- see https://en.wikipedia.org/wiki/Conversion_between_quaternions_and_Euler_angles

  ||| the roll = rotation around x-axis
  export
  roll : Quaternion -> Angle
  roll q = let q' = qnormalize q
               (Q w (x :: y :: z :: Nil)) = q'
           in case (gimbalPole q) of
                   NoPole    => Radians $ atan2 (2*(w*z + y*x)) (1 - 2*(x*x+z*z))
                   p@(_)     => Radians $ (2 * (atan2 y w)) * (gimbalMultiplier p)

  ||| rotation around y-axis
  export
  pitch : Quaternion -> Angle
  pitch q = let q' = qnormalize q
                (Q w (x :: y :: z :: Nil)) = q'
            in case (gimbalPole q) of
                    NoPole => Radians $ asin (2*(w*x - z*y)) -- might need clamping for asin
                    _      => Radians $ (pi / 2)

  ||| rotation around z-axis
  export
  yaw : Quaternion -> Angle
  yaw q = let q' = qnormalize q
              (Q w (x :: y :: z :: Nil)) = q'
          in case (gimbalPole q) of
                    NoPole => Radians $ atan2 (2*(y*w + x*z)) (1 - 2*(y*y + x*x))
                    _      => Radians $ 0

  ||| creates a quaternion from a vector of euler angles
  export
  fromEulerAngles : Vect 3 Angle -> Quaternion
  fromEulerAngles (yaw :: pitch :: roll :: Nil) =
    let yawR = (getRadians yaw) / 2; pitchR = (getRadians pitch) / 2; rollR = (getRadians roll) / 2
        w    = (cos yawR) * (cos pitchR) * (cos rollR) + (sin yawR) * (sin pitchR) * (sin rollR)
        x    = (cos yawR) * (sin pitchR) * (cos rollR) + (sin yawR) * (cos pitchR) * (sin rollR)
        y    = (sin yawR) * (cos pitchR) * (cos rollR) - (cos yawR) * (sin pitchR) * (sin rollR)
        z    = (cos yawR) * (cos pitchR) * (sin rollR) - (sin yawR) * (sin pitchR) * (cos rollR)
    in (Q w [x,y,z])

  export
  toEulerAngles : Quaternion -> Vect 3 Angle
  toEulerAngles q = [roll q, pitch q, yaw q]

  export
  fromCross : Vect 3 Double -> Vect 3 Double-> Quaternion
  fromCross v1 v2 = let theta = acos (dot (normalize v1) (normalize v2))
                        vec   = cross (normalize v1) (normalize v2)
                    in fromAxis (Radians theta) vec

  {--
  slerpBetween : Vect (S n) Quaternion -> Quaternion
  slerpBetween qs = ?slerpBetween

  slerpBetweenWeighted : Vect (S n) (Quaternion, Double) -> Quaternion
  slerpBetweenWeighted qs = ?slerpBetweenWeighted
  --}

  -- ----------------------------------------------------------------- [ Algenbraic Classes for Quaternions ]

  implementation Semigroup Quaternion where
    (<+>) = qsum

  implementation Monoid Quaternion where
    neutral = Q 0 [0, 0, 0]

  implementation Group Quaternion where
    inverse (Q s v) = Q (-1*s) (scalar (-1) v)

  implementation AbelianGroup Quaternion where {}

  implementation Ring Quaternion where
    (<.>) = qmultiply

  implementation RingWithUnity Quaternion where
    unity = Q 1 [0,0,0]

  implementation Num Quaternion where
    (+) = qsum
    (*) = qmultiply
    fromInteger x = Q (fromInteger x) [0,0,0]

  implementation Field Quaternion where
    inverseM q _ = qinverse q

  -- ----------------------------------------------------------------- [ Quaternion Rotation ]

  qrotate : Vect 3 Double -> Quaternion -> Vect 3 Double
  qrotate v q = let p  = Q 0 v        -- make the vector a quaternion
                    q' = qnormalize q -- normalize the rotation quaternion (until we have unit quaternions as a type)
                    in imagPart $ q' <.> p <.> (conjugate q')

  ||| linear interpolation of quaternions
  ||| TODO handle corner cases (sintheta < 0.00001)
  slerp : Quaternion -> Quaternion -> Double -> Quaternion
  slerp q0 q1 t = let n1 = qnormalize q0
                      n2 = qnormalize q1
                      theta = acos ((toVect n1) <:> (toVect n2))
                      sintheta = sin theta
                      weight1 = (sin (theta * (1-t))) / sintheta
                      weight2 = (sin (theta*t)) / sintheta
                  in ((qscalar weight1 n1) + (qscalar weight2 n2))

{--
// if theta = 180 degrees then result is not fully defined
	// we could rotate around any axis normal to qa or qb
	if (fabs(sinHalfTheta) < 0.001){ // fabs is floating point absolute
		qm.w = (qa.w * 0.5 + qb.w * 0.5);
		qm.x = (qa.x * 0.5 + qb.x * 0.5);
		qm.y = (qa.y * 0.5 + qb.y * 0.5);
		qm.z = (qa.z * 0.5 + qb.z * 0.5);
		return qm;
	}
--}

{--
#define SLERP_TO_LERP_SWITCH_THRESHOLD 0.01f

Quaternion Quaternion_slerp(Quaternion left, Quaternion right, float value) {
	float leftWeight, rightWeight, difference;
	Quaternion result;

	difference = left.x * right.x + left.y * right.y + left.z * right.z + left.w * right.w;
	if (1.0f - fabs(difference) > SLERP_TO_LERP_SWITCH_THRESHOLD) {
		float theta, oneOverSinTheta;

		theta = acos(fabs(difference));
		oneOverSinTheta = 1.0f / sin(theta);
		leftWeight = sin(theta * (1.0f - value)) * oneOverSinTheta;
		rightWeight = sin(theta * value) * oneOverSinTheta;
		if (difference < 0.0f) {
			leftWeight = -leftWeight;
		}
	} else {
		leftWeight = 1.0f - value;
		rightWeight = value;
	}
	result.x = left.x * leftWeight + right.x * rightWeight;
	result.y = left.y * leftWeight + right.y * rightWeight;
	result.z = left.z * leftWeight + right.z * rightWeight;
	result.w = left.w * leftWeight + right.w * rightWeight;
	Quaternion_normalize(&result);

	return result;
}
--}

max_stars_repo_name: spearman/gl-idris

max_issues_repo_name: spearman/gl-idris

max_forks_repo_name: spearman/gl-idris


text:
public export
interface Do (m : Type) where
  Next : (a : Type) -> (b : Type) -> m -> Type
  bind : (x : m) -> Next a b x

-- This won't actually achieve anything useful, but we're testing whether
-- it successfully typechecks and in the type of 'foo' we have the right 'a'
public export
Monad m => Do (m a) where
  Next a b x = (a -> m b) -> m b
  bind x = ?foo


text:
module Quantities.NonSIUnits

import Quantities.FreeAbelianGroup
import Quantities.Core
import Quantities.SIBaseQuantities
import Quantities.SIDerivedQuantities
import Quantities.SIPrefixes
import Quantities.SIBaseUnits
import Quantities.SIDerivedUnits

%default total
%access public export

-- Based on http://en.wikipedia.org/wiki/Non-SI_units_mentioned_in_the_SI

Minute : ElemUnit Time
Minute = < one "min" equals 60 Second >
Min : ElemUnit Time
Min = Minute

Hour : ElemUnit Time
Hour = < one "h" equals 60 Minute >
H : ElemUnit Time
H = Hour

Day : ElemUnit Time
Day = < one "d" equals 24 Hour >
D : ElemUnit Time
D = Day

Week : ElemUnit Time
Week = < one "week" equals 7 Day >

-- Julian year
Year : ElemUnit Time
Year = < one "a" equals 365.25 Day >
JulianYear : ElemUnit Time
JulianYear = Year
A : ElemUnit Time
A = Year

Century : Unit Time
Century = hecto Year

Millenium : Unit Time
Millenium = kilo Year

Tonne : ElemUnit Mass
Tonne = < one "t" equals 1000 Kg >
T : ElemUnit Mass
T = Tonne

Degree : ElemUnit PlaneAngle
Degree = < one "deg" equals (pi / 180) Rad >
Deg : ElemUnit PlaneAngle
Deg = Degree

Arcmin : ElemUnit PlaneAngle
Arcmin = < one "arcmin" equals (1/60) Degree >

Arcsec : ElemUnit PlaneAngle
Arcsec = < one "arcsec" equals (1/60) Arcmin >

-- Ångström (Å)
Angstrom : ElemUnit Length
Angstrom = < one "angstrom" equals 0.1 (nano Metre) >

AstronomicalUnit : ElemUnit Length
AstronomicalUnit = < one "au" equals 149597870700 Metre >
Au : ElemUnit Length
Au = AstronomicalUnit

StandardGravity : ElemUnit Acceleration
--StandardGravity = < one "g_0" equals 9.80665 (Metre <//> (Second ^^ 2)) >
StandardGravity = defineAsMultipleOf "g_0" 9.80665 (Metre <//> (Second ^^ 2))
G_0 : ElemUnit Acceleration
G_0 = StandardGravity

RotationsPerMinute : Unit Frequency
RotationsPerMinute = One <//> Minute
Rpm : Unit Frequency
Rpm = RotationsPerMinute

-- Use this only for relative temparature! Not suitable for conversions of
-- absolute temperature!

Fahrenheit : ElemUnit Temperature
Fahrenheit = < one "dF" equals (5/9) K > -- °F
DF : ElemUnit Temperature
DF = Fahrenheit

Are : ElemUnit Area
Are = < one "are" equals 100 (Metre ^^ 2) >

Hectare : ElemUnit Area
Hectare = < one "ha" equals 1 ((hecto Metre) ^^ 2) >
Ha : ElemUnit Area
Ha = Hectare

Barn : ElemUnit Area
Barn = < one "b" equals 100 ((femto Metre) ^^ 2) >
B : ElemUnit Area
B = Barn

Litre : ElemUnit Volume
Litre = < one "l" equals 1 (milli (Metre ^^ 3)) >
Liter : ElemUnit Volume
Liter = Litre
L : ElemUnit Volume
L = Litre

Bar : ElemUnit Pressure
Bar = < one "bar" equals 100 (kilo Pascal) >

MillimetreOfMercury : ElemUnit Pressure
MillimetreOfMercury = < one "mmHg" equals 133.322 Pascal >
MmHg : ElemUnit Pressure
MmHg = MillimetreOfMercury

Calorie : ElemUnit Energy
Calorie = < one "cal" equals 4.18400 Joule >
ThermochemicalCalorie : ElemUnit Energy
ThermochemicalCalorie = Calorie
Cal : ElemUnit Energy
Cal = Calorie

-- Non-SI units whose values in SI must be determined experimentally

Electronvolt : ElemUnit Energy
Electronvolt = < one "eV" equals 1.60217653 (Ten ^^ -19 <**> Joule) >
EV : ElemUnit Energy
EV = Electronvolt

Dalton : ElemUnit Mass
Dalton = < one "Da" equals 1.66053886 (Ten ^^ -27 <**> Kilogram) >
Da : ElemUnit Mass
Da = Dalton
UnifiedAtomicMassUnit : ElemUnit Mass
UnifiedAtomicMassUnit = Dalton
U : ElemUnit Mass
U = Dalton

-- Atomic and natural units

ElementaryCharge : ElemUnit ElectricCharge
ElementaryCharge = < one "e" equals 1.60217653 (Ten ^^ -19 <**> Coulomb) >
E : ElemUnit ElectricCharge
E = ElementaryCharge

MassOfElectron : ElemUnit Mass
MassOfElectron = < one "m_e" equals 9.1093826 (Ten ^^ -31 <**> Kilogram) >
ElectronMass : ElemUnit Mass
ElectronMass = MassOfElectron
M_e : ElemUnit Mass
M_e = MassOfElectron

BohrRadius : ElemUnit Length
BohrRadius = < one "a_0" equals 0.5291772108 (Ten ^^ -10 <**> Metre) >
Bohr : ElemUnit Length
Bohr = BohrRadius
A_0 : ElemUnit Length
A_0 = BohrRadius

HartreeEnergy : ElemUnit Energy
HartreeEnergy = < one "E_h" equals 4.35974417 (Ten ^^ -18 <**> Joule) >
Hartree : ElemUnit Energy
Hartree = HartreeEnergy
E_h : ElemUnit Energy
E_h = HartreeEnergy

PlanckConstant : ElemUnit (Energy <*> Time)
PlanckConstant = < one "h" equals 6.62606957 (Joule <**> Second) >
H_ : ElemUnit (Energy <*> Time)
H_ = PlanckConstant

ReducedPlanckConstant : ElemUnit (Energy <*> Time)
ReducedPlanckConstant = < one "hBar" equals (1 / (2*pi)) (Joule <**> Second) >
HBar : ElemUnit (Energy <*> Time)
HBar = ReducedPlanckConstant

AtomicUnitOfTime : ElemUnit Time
AtomicUnitOfTime = < one "auOfTime" equals 1 (HBar <//> Hartree) >
AuOfTime : ElemUnit Time
AuOfTime = AtomicUnitOfTime

SpeedOfLight : ElemUnit Speed
SpeedOfLight = < one "c_0" equals 299792458 (Metre <//> Second) >
C_0 : ElemUnit Speed
C_0 = SpeedOfLight

NaturalUnitOfTime : ElemUnit Time
NaturalUnitOfTime = < one "nuOfTime" equals 1 (HBar <//> (M_e <**> (C_0 ^^ 2))) >
NuOfTime : ElemUnit Time
NuOfTime = NaturalUnitOfTime

LightSecond : ElemUnit Length
LightSecond = < one "ls" equals 1 (Second <**> SpeedOfLight) >
Ls : ElemUnit Length
Ls = LightSecond

LightMinute : ElemUnit Length
LightMinute = < one "lmin" equals 1 (Minute <**> SpeedOfLight) >
Lmin : ElemUnit Length
Lmin = LightMinute

LightHour : ElemUnit Length
LightHour = < one "lh" equals 1 (Hour <**> SpeedOfLight) >
Lh : ElemUnit Length
Lh = LightHour

LightDay : ElemUnit Length
LightDay = < one "ld" equals 1 (Day <**> SpeedOfLight) >
Ld : ElemUnit Length
Ld = LightDay

LightWeek : ElemUnit Length
LightWeek = < one "ld" equals 1 (Week <**> SpeedOfLight) >
Lw : ElemUnit Length
Lw = LightWeek

LightYear : ElemUnit Length
LightYear = < one "ly" equals 1 (Year <**> SpeedOfLight) >
Ly : ElemUnit Length
Ly = LightYear

-- Non-SI units associated with the CGS and the CGS-Gaussian system of units

Erg : Unit Energy
Erg = Ten ^^ -7 <**> Joule

Dyne : Unit Force'
Dyne = Ten ^^ -5 <**> Newton
Dyn : Unit Force'
Dyn = Dyne

Poise : Unit DynamicViscosity
Poise = Dyne <**> Second <//> (Centimetre ^^ 2)
P : Unit DynamicViscosity
P = Poise

Stokes : Unit KinematicViscosity
Stokes = Centimetre ^^ 2 <//> Second
St : Unit KinematicViscosity
St = Stokes

Stilb : Unit Luminance
Stilb = Candela <//> (Centimetre ^^ 2)
Sb : Unit Luminance
Sb = Stilb

Phot : Unit Illuminance
Phot = Candela <**> Steradian <//> (Centimetre ^^ 2)
Ph : Unit Illuminance
Ph = Phot

Gal : Unit Acceleration
Gal = Centimetre <//> (Second ^^ 2)

Maxwell : Unit MagneticFlux
Maxwell = Ten ^^ -8 <**> Weber
Mx : Unit MagneticFlux
Mx = Maxwell

Gauss : Unit MagneticFluxDensity
Gauss = Maxwell <//> (Centimetre ^^ 2)
G : Unit MagneticFluxDensity
G = Gauss

Oersted : ElemUnit MagneticFieldStrength
Oersted = < one "oe" equals (250 / pi) (Ampere <//> Metre) >
Oe : ElemUnit MagneticFieldStrength
Oe = Oersted

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
> module Nat.GCDAlgorithm

> import Nat.GCD
> import Nat.GCDProperties
> import Nat.GCDEuclid
> import Pairs.Operations
> import Sigma.Sigma

> %default total

> %access public export

> %hide gcd

> ||| The GCD algorithm
> gcdAlg : Nat -> Nat -> Nat
> gcdAlg m n = getWitness (euclidGCD m n)

> gcdAlgLemma : (m : Nat) -> (n : Nat) -> GCD (gcdAlg m n) m n
> gcdAlgLemma m n = getProof (euclidGCD m n)

> gcdAlgCommutative : (m : Nat) -> (n : Nat) -> gcdAlg m n = gcdAlg n m
> gcdAlgCommutative m n =
>   let d1  :  Nat
>           =  gcdAlg m n in
>   let d2  :  Nat
>           =  gcdAlg n m in
>   let v1  :  GCD d1 m n
>           =  gcdAlgLemma m n in
>   let v2  :  GCD d2 m n
>           =  gcdCommutative (gcdAlgLemma n m) in
>   gcdUnique d1 d2 v1 v2

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Error.Data

import public Loc
import public Syntax.Tokens

public export
data ExpectType
  = ExpectTkn Tkn
  | ExpectKeyword String
  | ExpectId
  | ExpectInt
  | ExpectStr
  | Unknown
  | TknEOF

public export
data BetweenType
  = Parenthesis
  | CurlyBrackets
  | SquareBrackets

public export
data ReaderError
  = NotClosed BetweenType
  | Expected ExpectType Tkn

public export
data LexerError
  = UnterminatedString
  | UnexpectedChar

public export
data CapitalizedNameErr
  = CapitalModule
  | CapitalType
  | CapitalADTName
  | CapitalDataConstructor

public export
data ParserError
  = InvalidTopLevel String
  | InvalidIdName String
  | InvalidPath String
  | ExpectedDataField
  | ExpectedLiteral
  | ExpectedIdentifier
  | ExpectedIdButGotPath
  | ExpectedTypeDef
  | ImpossibleParsingError
  | NeedCapitalizedName CapitalizedNameErr
  | NeedMinusculeName
  | NotSupportEmptyList
  | NotAValidPattern
  | NotAValidType
  | NotAValidRecordField
  | InvalidExpr
  | Unreachable
  | NotAllCasesHaveCond
  | ArrowWithOneArg

public export
data ErrorType
  = LexicalError Range LexerError
  | ReadingError Range ReaderError
  | ParsingError Range ParserError
  | EOF
  | ExpectedEOF
  | UnexpectedInternalError

public export
record ErrorData where
  constructor MkErrorData
  fileName    : String
  sourceInput : String
  error       : ErrorType

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
module Data.Matrix.ZZVerified

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

import Data.Vect.Structural
import Data.Matrix.Structural

import Data.ZZ
import Control.Algebra.ZZVerifiedInstances

-- import Data.Matrix.LinearCombinations ( timesVectMatAsHeadTail_ByTransposeElimination )
import Data.Matrix.LinearCombinations

%default total

{-
Identities whose proof is particular to ZZ.
-}

{-
-- More instance collisions prevent a proof. (<:>) invokes a (neutral) for the ring which differs from (the a Algebra.neutral).

ringVecNeutralIsVecPtwiseProdZeroL : VerifiedRing a => (xs : Vect n a) -> xs <:> (the (Vect n a) Algebra.neutral) = the a Algebra.neutral
ringVecNeutralIsVecPtwiseProdZeroL [] {a} = Refl
ringVecNeutralIsVecPtwiseProdZeroL (x::xs) = vecHeadtailsEq (ringNeutralIsMultZeroL x) $ ringVecNeutralIsVecPtwiseProdZeroL xs

ringVecNeutralIsVecPtwiseProdZeroR : VerifiedRing a => (xs : Vect n a) -> (the (Vect n a) Algebra.neutral) <:> xs = the a Algebra.neutral
ringVecNeutralIsVecPtwiseProdZeroR [] {a} = Refl
ringVecNeutralIsVecPtwiseProdZeroR (x::xs) = vecHeadtailsEq (ringNeutralIsMultZeroR x) $ ringVecNeutralIsVecPtwiseProdZeroR xs

matVecMultIsVecTransposeMult : Ring a => (v : Vect n a) -> (xs : Matrix n m a) -> v <\> xs = (transpose xs) </> v

ringVecNeutralIsMatVecMultZero : VerifiedRing a => (xs : Matrix n m a) -> xs </> Algebra.neutral = Algebra.neutral
ringVecNeutralIsMatVecMultZero [] = Refl
ringVecNeutralIsMatVecMultZero (x::xs) = vecHeadtailsEq (ringVecNeutralIsVecPtwiseProdZeroR x) $ ringVecNeutralIsMatVecMultZero xs

ringVecNeutralIsVecMatMultZero : VerifiedRing a => (xs : Matrix n m a) -> Algebra.neutral <\> xs = Algebra.neutral
ringVecNeutralIsVecMatMultZero xs = trans (vecMatMultTransposeEq Algebra.neutral xs) $ ringVecNeutralIsMatVecMultZero $ transpose xs
-}

zzVecNeutralIsVecPtwiseProdZeroL :
	(xs : Vect n ZZ)
	-> xs <:> Algebra.neutral = Algebra.neutral
zzVecNeutralIsVecPtwiseProdZeroL [] = Refl
zzVecNeutralIsVecPtwiseProdZeroL (x::xs) =
	trans ( foldrImplRec (<+>) (Pos 0) id
		(x <.> Algebra.neutral)
		(zipWith (<.>) xs Algebra.neutral) )
	$ trans ( rewrite ringNeutralIsMultZeroR x in monoidNeutralIsNeutralR _ )
	$ zzVecNeutralIsVecPtwiseProdZeroL xs
{-
Couldn't do this:

> zzVecNeutralIsVecPtwiseProdZeroL (x::xs) = vecHeadtailsEq (ringNeutralIsMultZeroR x) $ zzVecNeutralIsVecPtwiseProdZeroL xs

Discovered this proof by ordered inspection following this proof script:

ZZVerified.zzVecNeutralIsVecPtwiseProdZeroL' = proof
  intros
  let pr' = zzVecNeutralIsVecPtwiseProdZeroL xs
  exact _ pr'
  compute
  intro computedPr
  exact trans _ computedPr
  -- The script thusfar makes it possible to identify the missing theorem.
  exact trans ( foldrImplRec (<+>) (Pos 0) id (x <.> Algebra.neutral) (zipWith (<.>) xs Algebra.neutral) ) $ _
  compute
  rewrite sym $ ringNeutralIsMultZeroR x
  exact monoidNeutralIsNeutralR _
-}

zzVecNeutralIsVecPtwiseProdZeroR : (xs : Vect n ZZ) -> Algebra.neutral <:> xs = Algebra.neutral
zzVecNeutralIsVecPtwiseProdZeroR [] = Refl
zzVecNeutralIsVecPtwiseProdZeroR (x::xs) =
	trans ( foldrImplRec (<+>) (Pos 0) id
		(Algebra.neutral <.> x)
		(zipWith (<.>) Algebra.neutral xs) )
	$ trans ( rewrite ringNeutralIsMultZeroL x in monoidNeutralIsNeutralR _ )
	$ zzVecNeutralIsVecPtwiseProdZeroR xs

zzVecNeutralIsVecMatMultZero : (xs : Matrix n m ZZ) -> Algebra.neutral <\> xs = Algebra.neutral
zzVecNeutralIsVecMatMultZero xs {m=Z} = zeroVecEq
zzVecNeutralIsVecMatMultZero xs {m=S predm} = trans timesVectMatAsHeadTail_ByTransposeElimination $ vecHeadtailsEq (zzVecNeutralIsVecPtwiseProdZeroR $ map Vect.head xs) $ zzVecNeutralIsVecMatMultZero $ map Vect.tail xs

zzVecNeutralIsMatVecMultZero : (xs : Matrix n m ZZ) -> xs </> Algebra.neutral = Algebra.neutral
zzVecNeutralIsMatVecMultZero xs = trans (matVecMultIsVecTransposeMult Algebra.neutral xs) $ zzVecNeutralIsVecMatMultZero (transpose xs)

zzVecNeutralIsNeutralL : (l : Vect n ZZ) -> l<+>Algebra.neutral=l
zzVecNeutralIsNeutralL = monoidNeutralIsNeutralL_Vect

zzVecNeutralIsNeutralR : (r : Vect n ZZ) -> Algebra.neutral<+>r=r
zzVecNeutralIsNeutralR = monoidNeutralIsNeutralR_Vect

zzVecScalarUnityIsUnity : (v : Vect n ZZ) -> (Algebra.unity {a=ZZ}) <#> v = v
zzVecScalarUnityIsUnity = moduleScalarUnityIsUnity_Vect


text:
> module Nat.Coprime

> import Nat.GCD
> import Nat.GCDAlgorithm
> import Unique.Predicates
> import Equality.Properties
> import Nat.GCDEuclid
> import Pairs.Operations
> import Sigma.Sigma

> %default total

> %access public export

> |||
> data Coprime : (m : Nat) -> (n : Nat) -> Type where
>   MkCoprime : {m, n : Nat} -> gcdAlg m n = S Z -> Coprime m n

> |||
> CoprimeUnique : {m, n : Nat} -> Unique (Coprime m n)
> CoprimeUnique {m} {n} (MkCoprime p) (MkCoprime q) = cong (uniqueEq (gcdAlg m n) (S Z) p q)


text:
module Signed

%access export
%default total

||| A signed binary number represented with `n` bits
data Signed : (n : Nat) -> Type where
  ||| Built from an underlying integer
  S : Integer -> Signed n

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

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

||| Eq instacne for equality of `Signed n`
Eq (Signed n) where
  (==) (S x) (S y) = x==y

||| Ord instance for ordering of `Signed n`
Ord (Signed n) where
  compare (S x) (S y) = compare x y

||| MinBound instance for generating extremes of `Signed n`
MinBound (Signed n) where
  minBound = S . negate . cast . power 2 $ n `minus` 1

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

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

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

||| Show instance for printing `Signed n`
Show (Signed n) where
  show (S x) = "S" ++ show n ++ " " ++ show x


text:
-- --------------------------------------------------------------- [ Utils.idr ]
-- Module    : Utils.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module GRL.Lang.Common.Utils

import GRL.Common
import GRL.Model

%access export

prettyResult : GoalNode -> String
prettyResult g = unwords
    [ "Result:"
    , show (fromMaybe NONE (getSValue g))
    , "\t<=="
    , getNodeTitle g]

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
import Control.Monad.State

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

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty) "Fred"
                      (Node Empty "Sheila" Empty)) "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

flatten : Tree a -> List a
flatten Empty = []
flatten (Node left val right) = flatten left ++ val :: flatten right

treeLabelWith : Tree a -> State (Stream labelType) (Tree (labelType, a))
treeLabelWith Empty = pure Empty
treeLabelWith (Node left val right)
     = do left_labelled <- treeLabelWith left
          (this :: rest) <- get
          put rest
          right_labelled <- treeLabelWith right
          pure (Node left_labelled (this, val) right_labelled)

treeLabel : Tree a -> Tree (Integer, a)
treeLabel tree = evalState [1..] (treeLabelWith tree)


text:
-- 4.1.5 Exercises

-- integer arithmetic expression
data Exp = Single Int
         | Add Exp Exp
         | Sub Exp Exp
         | Mul Exp Exp

-- more flexible syntax
-- data Exp : Type where
--      Single : Int -> Exp
--      Add : Exp -> Exp -> Exp
--      Sub : Exp -> Exp -> Exp
--      Mul : Exp -> Exp -> Exp

eval : Exp -> Int
eval (Single x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y

-- *Chap4> eval (Add (Single 1) (Single 2))
-- 3 : Int

data BSTree : Type -> Type where
      Empty : Ord e => BSTree e
      Node  : Ord e => (left : BSTree e) -> (val : e) -> (right : BSTree e) -> BSTree e

-- %name BSTree left, right
-- using a %name directive to give naming hints for building definitions interactively

insert : elem -> BSTree elem -> BSTree elem
insert x Empty = Node Empty x Empty
insert x orig@(Node left val right) = case compare x val of
                                    LT => Node (insert x left) val right
                                    EQ => orig -- same as as-patterns in Haskell
                                    GT => Node left val (insert x right)
-- match Ctrl-Alt-M

listToTree : Ord a => List a -> BSTree a
listToTree [] = Empty
listToTree (x :: xs) = insert x $ listToTree xs

-- *starting/Chap4> listToTree ['p', 'r', 'a', 't']
-- Node (Node Empty 'a' (Node (Node Empty 'p' Empty) 'r' Empty)) 't' Empty : BSTree Char

treeToList : BSTree a -> List a
treeToList Empty = []
treeToList (Node left val right) = treeToList left ++ [val] ++ treeToList right


text:
{-
a[0] = {foo: bar}
a[1] = {baz: qux}
-}
import CIL.FFI.Array
import Data.Vect

DictionaryEntryTy : CILTy
DictionaryEntryTy = corlibTyVal "System.Collections.DictionaryEntry"

||| System.Collections.DictionaryEntry value type.
DictionaryEntry : Type
DictionaryEntry = CIL DictionaryEntryTy

newDictionaryEntry : key -> value -> CIL_IO DictionaryEntry
newDictionaryEntry key value = new (Object -> Object -> CIL_IO DictionaryEntry)
                                   (believe_me key)
                                   (believe_me value)

Key : DictionaryEntry -> CIL_IO Object
Key = invoke (CILInstance "get_Key") (DictionaryEntry -> CIL_IO Object)

Value : DictionaryEntry -> CIL_IO Object
Value = invoke (CILInstance "get_Value") (DictionaryEntry -> CIL_IO Object)

main : CIL_IO ()
main = do
  a <- arrayOf DictionaryEntryTy [ !(newDictionaryEntry "foo" "bar")
                                 , !(newDictionaryEntry "baz" "qux") ]
  for_ [0..1] $ \i => do
    e <- get a i
    k <- Key e >>= ToString
    v <- Value e >>= ToString
    putStrLn ("a[" ++ show i ++ "] = {" ++ k ++ ": " ++ v ++ "}")

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

max_stars_repo_name: timjs/iris-clean

max_issues_repo_name: timjs/iris-clean

max_forks_repo_name: timjs/iris-clean


text:
module Main

import Control.IOExcept
import Control.ST
import Control.ST.File
import Control.ST.ImplicitCall

testFile : (ConsoleIO m, File m) => ST m () []
testFile = with ST do
              Right fileHandle <- open "writeTestFile" WriteTruncate
                    | Left ferr =>  do putStrLn (show ferr)
                                       pure ()
              Right _ <- writeLine fileHandle "HELLO!!"
                    | Left ferr =>  do putStrLn (show ferr)
                                       close fileHandle
                                       pure ()
              Right _ <- writeLine fileHandle "WORLD!!"
                    | Left ferr =>  do putStrLn (show ferr)
                                       close fileHandle
                                       pure ()
              close fileHandle
              pure ()

main : IO ()
main = do putStrLn "--test IO:"
          run testFile
          putStrLn "--test IOExcept:"
          ioe_run (run testFile)
                  (\err => putStrLn err)
                  (\ok  => printLn ok)

-- EOF -------------------------------------------------------------------------

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin