text:
import Data.Vect

-- Chapter 3.2 Exercises

my_length : List a -> Nat
my_length [] = Z
my_length (x :: xs) = S (my_length xs)

my_reverse : List a -> List a
my_reverse [] = []
my_reverse [x] = [x]
my_reverse (x :: xs) = my_reverse xs ++ [x]

my_map : (a -> b) -> List a -> List b
my_map _ [] = []
my_map f (x :: xs) = f x :: my_map f xs

my_vect_map : (a -> b) -> Vect n a -> Vect n b
my_vect_map _ [] = []
my_vect_map f (x :: xs) = f x :: my_vect_map f xs


text:
module Step

-- Relation 'Step' for reducing terms
-- in the simply-typed lambda calculus.

import Term
import Subst

%default total
%access public export

-------------------------------------------------------------------------
-- Begin: SMALL-STEP EVALUATION RELATION FOR TERMS IN THE LAMBDA CALCULUS

data Step : (x : Term) -> (y : Term) -> Type where
  StApp1     : Step t1 t1' ->
               Step (TApp t1 t2) (TApp t1' t2)
  --
  StApp2     : Value v -> Step t2 t2' ->
               Step (TApp v t2) (TApp v t2')
  --
  StBeta     : Value v ->
               Step (TApp (TAbs t) v) (subst v Z t)
  --
  StRec      : Step t t' ->
               Step (TRec t t0 t1) (TRec t' t0 t1)
  --
  StRecZero  : Step (TRec TZero t0 t1) t0
  --
  StRecSucc  : Value (TSucc n) ->
               Step (TRec (TSucc n) t0 t1)
                    (TApp ((TApp t1) n) (TRec n t0 t1))
  --
  StSucc     : Step t t' ->
               Step (TSucc t) (TSucc t')
  --
  StPred     : Step t t' ->
               Step (TPred t) (TPred t')
  --
  StPredZero : Step (TPred TZero) TZero
  --
  StPredSucc : Value v ->
               Step (TPred (TSucc v)) v
  --
  StIfz      : Step t1 t1' ->
               Step (TIfz t1 t2 t3) (TIfz t1' t2 t3)
  --
  StIfzZero  : Step (TIfz TZero t1 t2) t1
  --
  StIfzSucc  : Value v ->
               Step (TIfz (TSucc v) t1 t2) t2

-- End: SMALL-STEP EVALUATION RELATION FOR TERMS IN THE LAMBDA CALCULUS
-----------------------------------------------------------------------

--------------------------------
-- Begin: VALUES ARE IRREDUCIBLE

valueIrreducible : (e : Term) ->
                   Value e ->
                   (Step e e' -> Void)
valueIrreducible TZero     VZero     step impossible
valueIrreducible (TSucc e) (VSucc v) (StSucc step) =
  valueIrreducible e v step
valueIrreducible (TAbs e)  VAbs      step impossible

-- End: VALUES ARE IRREDUCIBLE
------------------------------

----------------------------
-- Begin: TRANSITIVE CLOSURE

-- Data type for representing the transistive closure
-- of an arbitrary relation 'rel : a -> a -> Type'.
using (a : Type, rel : a -> a -> Type)
  data TransCl : {a : Type} -> (a -> a -> Type) -> (a -> a -> Type) where
    TClRefl   : (x : a) -> TransCl rel x x
    TClSingle : rel x y  -> TransCl rel x y
    TClTrans  : TransCl rel x y -> TransCl rel y z -> TransCl rel x z

-- Data type specifically for representing the
-- transitive closure of the 'Step' relation.
data TransStep : Term -> Term -> Type where
   TStRefl   : (e : Term) -> TransStep e e
   TStTrans  : {e : Term} -> {e' : Term} -> {e'' : Term} ->
               Step e e' -> TransStep e' e'' -> TransStep e e''

-- 'TransStep' is indeed transitive.
transStepTransitive : TransStep e1 e2 -> TransStep e2 e3 -> TransStep e1 e3
transStepTransitive (TStRefl _) y    = y
transStepTransitive (TStTrans x y) z = TStTrans x (transStepTransitive y z)

-- Correctness proof for 'TransStep', i.e.: TransStep => (TransCl Step).
transStepCorrect : TransStep e e' -> TransCl Step e e'
transStepCorrect (TStRefl e)    = TClRefl e
transStepCorrect (TStTrans x y) = TClTrans (TClSingle x) (transStepCorrect y)

-- Completeness proof for 'TransStep', i.e.: (TransCl Step) => TransStep.
transStepComplete : TransCl Step e e' -> TransStep e e'
transStepComplete (TClRefl e)    = TStRefl e
transStepComplete (TClSingle x)  = TStTrans x (TStRefl _)
transStepComplete (TClTrans x z) = transStepTransitive (transStepComplete x)
                                                       (transStepComplete z)

-- Operators for compact notation:
infixl 10 .++.
(.++.) : TransStep e1 e2 -> TransStep e2 e3 -> TransStep e1 e3
(.++.) = transStepTransitive

infixl 10 .+.
(.+.) : TransStep e1 e2 -> Step e2 e3 -> TransStep e1 e3
(.+.) x y = x .++. (TStTrans y (TStRefl _))

-- End: TRANSITIVE CLOSURE
--------------------------

--------------------
-- Begin: CONGRUENCE

-- Construction of terms is a congruence
-- for the transitive closure of 'Step'.

-- Congruence lemma for '(TApp _ e)':
congApp1 : TransStep e1 e2 -> TransStep (TApp e1 e) (TApp e2 e)
congApp1 (TStRefl e1)   = TStRefl (TApp e1 _)
congApp1 (TStTrans x y) = TStTrans (StApp1 x) (congApp1 y)

-- Congruence lemma for '(TApp e _)':
congApp2 : {v : Value e} ->
           TransStep e1 e2 -> TransStep (TApp e e1) (TApp e e2)
congApp2         (TStRefl e1)   = TStRefl (TApp _ e1)
congApp2 {v = v} (TStTrans x y) = TStTrans (StApp2 v x) (congApp2 {v = v} y)

-- Congruence lemma for '(Succ _)':
congSucc : TransStep e1 e2 -> TransStep (TSucc e1) (TSucc e2)
congSucc (TStRefl e1)   = TStRefl (TSucc e1)
congSucc (TStTrans x y) = TStTrans (StSucc x) (congSucc y)

-- Congruence lemma for '(Pred _)':
congPred : TransStep e1 e2 -> TransStep (TPred e1) (TPred e2)
congPred (TStRefl e1)   = TStRefl (TPred e1)
congPred (TStTrans x y) = TStTrans (StPred x) (congPred y)

-- Congruence lemma for '(Ifz _ ez es)':
congIfz : TransStep e1 e2 -> TransStep (TIfz e1 ez es) (TIfz e2 ez es)
congIfz (TStRefl e1)   = TStRefl (TIfz e1 _ _)
congIfz (TStTrans x y) = TStTrans (StIfz x) (congIfz y)

-- Congruence lemma for '(TRec _ e0 e1)':
congRec : TransStep e e' -> TransStep (TRec e e0 e1) (TRec e' e0 e1)
congRec (TStRefl e)    = TStRefl (TRec e _ _)
congRec (TStTrans x y) = TStTrans (StRec x) (congRec y)

-- End: CONGRUENCE
------------------

ext: idr

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module STLC
import Data.Fin
import Data.Vect

data Ty = TyInt | TyBool | TyFun Ty Ty

interpTy : Ty -> Type
interpTy TyInt       = Int
interpTy TyBool      = Bool
interpTy (TyFun A T) = interpTy A -> interpTy T

using (G:Vect n Ty)
  data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
    Stop : HasType FZ (t :: G) t
    Pop  : HasType k G t -> HasType (FS k) (u :: G) t

  data Expr : Vect n Ty -> Ty -> Type where
    Var : HasType i G t -> Expr G t
    Val : (x : Int) -> Expr G TyInt
    Lam : Expr (a :: G) t -> Expr G (TyFun a t)
    App : Expr G (TyFun a t) -> Expr G a -> Expr G t
    Op  : (interpTy a -> interpTy b -> interpTy c) ->
             Expr G a -> Expr G b -> Expr G c
    If  : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a

  data Env : Vect n Ty -> Type where
    Nil  : Env Nil
    (::) : interpTy a -> Env G -> Env (a :: G)

  lookup : HasType i G t -> Env G -> interpTy t
  lookup Stop    (x :: xs) = x
  lookup (Pop k) (x :: xs) = lookup k xs

  interp : Env G -> Expr G t -> interpTy t
  interp env (Var i)     = lookup i env
  interp env (Val x)     = x
  interp env (Lam sc)    = \x => interp (x :: env) sc
  interp env (App f s)   = interp env f (interp env s)
  interp env (Op op x y) = op (interp env x) (interp env y)
  interp env (If x t e)  = if interp env x then interp env t
                                           else interp env e

-- Unit Tests
  sub1 : Expr G (TyFun TyInt TyInt)
  sub1 = Lam (Op (-) (Var Stop) (Val 1))

  sub2 : Expr G (TyFun TyInt TyInt)
  sub2 = Lam (App sub1 (App sub1 (Var Stop)))

  add : Expr G (TyFun TyInt (TyFun TyInt TyInt))
  add = Lam (Lam (Op (+) (Var Stop) (Var (Pop Stop))))

  fact : Expr G (TyFun TyInt TyInt)
  fact = Lam (If (Op (==) (Var Stop) (Val 0))
               (Val 1)
               (Op (*) (App fact (Op (-) (Var Stop) (Val 1)))
                       (Var Stop)))

  fib : Expr G (TyFun TyInt TyInt)
  fib = Lam (If (Op (==) (Var Stop) (Val 0))
                (Val 1)
                (If (Op (==) (Var Stop) (Val 1))
                    (Val 1)
                    (Op (*) (App fib (App sub1 (Var Stop)))
                            (App fib (App sub2 (Var Stop))))))

max_stars_repo_name: akuhlens/metaprogramming

max_issues_repo_name: akuhlens/metaprogramming

max_forks_repo_name: akuhlens/metaprogramming


text:
data Format = Number Format
            | NumDouble Format
            | Str Format
            | Ch Format
            | Lit String Format
            | End
%name Format fmt

||| Takes a Format and converts it to a Type that
||| includes the variable length arguments to the format string
||| ex.
|||    PrintfType (toFormat (unpack "this is a literal of %d words"))
||| will return Int -> String : Type
PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (NumDouble fmt) =(d : Double) -> PrintfType fmt
PrintfType (Str fmt) = (s : String) -> PrintfType fmt
PrintfType (Ch fmt) = (c : Char) -> PrintfType fmt
PrintfType (Lit s fmt) = PrintfType fmt
PrintfType End = String

||| Builds String from a Format
||| Basically recursively parses the given Format into final PrintfType to return from printf
printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt)  acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (NumDouble fmt) acc = \d => printfFmt fmt (acc ++ show d)
printfFmt (Str fmt) acc = \s => printfFmt fmt (acc ++ s)
printfFmt (Ch fmt) acc = \c => printfFmt fmt (acc ++ cast c)
printfFmt (Lit lit fmt) acc = printfFmt fmt (acc ++ lit)
printfFmt End acc = acc

||| Converts format string (with %d or %s) to Format
||| ex. toFormat (unpack "this is a literal of %d words")
|||  => Lit "this is a literal of " (Number (Lit " words" End)) : Format
toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number (toFormat chars)
toFormat ('%' :: 'f' :: chars) = NumDouble (toFormat chars)
toFormat ('%' :: 's' :: chars) = Str (toFormat chars)
toFormat ('%' :: 'c' :: chars) = Ch (toFormat chars)
toFormat ('%' :: chars) = Lit "%" (toFormat chars)
toFormat (c :: chars) = case toFormat chars of
                             Lit lit chars' => Lit (strCons c lit) chars'
                             fmt => Lit (strCons c "") fmt

||| PrintfType will generate a Type based on the input string `fmt`
||| which consists of all the arguments that need to be present
||| to interpolate the string.
||| > :t printf "the %s is %d years old" : String -> Int -> String
||| > printf "the %s is %d years old" "man" 55 : String
||| => "the man is 55 years old" : String
printf : (fmtStr : String) -> PrintfType (toFormat (unpack fmtStr))
printf _ = printfFmt _ "" -- full Format type inferred from above definition


text:
module Tree

import Data.List

%default total

{-
  interface Functor (f : Type -> Type) where
    map : (func : a -> b) -> f a -> f b

  Functor List where
    map func [] = []
    map func (x :: xs) = f x :: map func xs

-}

interface MyFunctor f where
  myMap : (a -> b) -> f a -> f b

MyFunctor List where
  myMap func [] = []
  myMap func (x :: xs) = func x :: myMap func xs

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

Functor Tree where
  map func Empty = Empty
  map func (Node l v r) = Node (map func l) (func v) (map func r)

partial
fromList : List a -> Tree a
fromList [] = Empty
fromList (x :: xs) = Node (fromList left) x (fromList right)
  where
    len : Nat
    len = fromInteger $ natToInteger (length xs) `div` 2

    left : List a
    left = take len xs

    right : List a
    right = drop len xs

{-
  Functor (Vect n) where
    map func [] = []
    map func (x :: xs) = func x :: map func xs

-}

{-
  foldr : Foldable t => (a -> b -> b) -> b -> t a -> b
  foldl : Foldable t => (b -> a -> b) -> b -> t a -> b

-}

sampleTree : Tree Int
sampleTree = Node (Node (Node Empty 1 Empty) 2 (Node Empty 3 Empty)) 4 (Node (Node Empty 5 Empty) 6 (Node Empty 7 Empty))

Foldable Tree where
  foldr func acc Empty = acc
  foldr func acc (Node l v r) = let rightFold = foldr func acc r
                                    leftFold = foldr func rightFold l in
                                    func v leftFold

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Web.Internal.XhrPrim

import JS
import Web.Internal.Types

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

namespace FormData

  export
  %foreign "browser:lambda:(a)=> new FormData(a)"
  prim__new : UndefOr HTMLFormElement -> PrimIO FormData

  export
  %foreign "browser:lambda:(x,a,b)=>x.append(a,b)"
  prim__append : FormData -> String -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.append(a,b,c)"
  prim__append1 : FormData -> String -> Blob -> UndefOr String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.delete(a)"
  prim__delete : FormData -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.getAll(a)"
  prim__getAll : FormData -> String -> PrimIO (Array (Union2 File String))

  export
  %foreign "browser:lambda:(x,a)=>x.get(a)"
  prim__get : FormData -> String -> PrimIO (Nullable (Union2 File String))

  export
  %foreign "browser:lambda:(x,a)=>x.has(a)"
  prim__has : FormData -> String -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,a,b)=>x.set(a,b)"
  prim__set : FormData -> String -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.set(a,b,c)"
  prim__set1 : FormData -> String -> Blob -> UndefOr String -> PrimIO ()

namespace ProgressEvent

  export
  %foreign "browser:lambda:(a,b)=> new ProgressEvent(a,b)"
  prim__new : String -> UndefOr ProgressEventInit -> PrimIO ProgressEvent

  export
  %foreign "browser:lambda:x=>x.lengthComputable"
  prim__lengthComputable : ProgressEvent -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.loaded"
  prim__loaded : ProgressEvent -> PrimIO JSBits64

  export
  %foreign "browser:lambda:x=>x.total"
  prim__total : ProgressEvent -> PrimIO JSBits64

namespace XMLHttpRequest

  export
  %foreign "browser:lambda:()=> new XMLHttpRequest()"
  prim__new : PrimIO XMLHttpRequest

  export
  %foreign "browser:lambda:x=>x.onreadystatechange"
  prim__onreadystatechange :  XMLHttpRequest
                           -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onreadystatechange = v}"
  prim__setOnreadystatechange :  XMLHttpRequest
                              -> Nullable EventHandlerNonNull
                              -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.readyState"
  prim__readyState : XMLHttpRequest -> PrimIO Bits16

  export
  %foreign "browser:lambda:x=>x.response"
  prim__response : XMLHttpRequest -> PrimIO AnyPtr

  export
  %foreign "browser:lambda:x=>x.responseText"
  prim__responseText : XMLHttpRequest -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.responseType"
  prim__responseType : XMLHttpRequest -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.responseType = v}"
  prim__setResponseType : XMLHttpRequest -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.responseURL"
  prim__responseURL : XMLHttpRequest -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.responseXML"
  prim__responseXML : XMLHttpRequest -> PrimIO (Nullable Document)

  export
  %foreign "browser:lambda:x=>x.status"
  prim__status : XMLHttpRequest -> PrimIO Bits16

  export
  %foreign "browser:lambda:x=>x.statusText"
  prim__statusText : XMLHttpRequest -> PrimIO ByteString

  export
  %foreign "browser:lambda:x=>x.timeout"
  prim__timeout : XMLHttpRequest -> PrimIO Bits32

  export
  %foreign "browser:lambda:(x,v)=>{x.timeout = v}"
  prim__setTimeout : XMLHttpRequest -> Bits32 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.upload"
  prim__upload : XMLHttpRequest -> PrimIO XMLHttpRequestUpload

  export
  %foreign "browser:lambda:x=>x.withCredentials"
  prim__withCredentials : XMLHttpRequest -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,v)=>{x.withCredentials = v}"
  prim__setWithCredentials : XMLHttpRequest -> Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.abort()"
  prim__abort : XMLHttpRequest -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.getAllResponseHeaders()"
  prim__getAllResponseHeaders : XMLHttpRequest -> PrimIO ByteString

  export
  %foreign "browser:lambda:(x,a)=>x.getResponseHeader(a)"
  prim__getResponseHeader :  XMLHttpRequest
                          -> ByteString
                          -> PrimIO (Nullable ByteString)

  export
  %foreign "browser:lambda:(x,a,b)=>x.open(a,b)"
  prim__open : XMLHttpRequest -> ByteString -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b,c,d,e)=>x.open(a,b,c,d,e)"
  prim__open1 :  XMLHttpRequest
              -> ByteString
              -> String
              -> Boolean
              -> UndefOr (Nullable String)
              -> UndefOr (Nullable String)
              -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.overrideMimeType(a)"
  prim__overrideMimeType : XMLHttpRequest -> String -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.send(a)"
  prim__send :  XMLHttpRequest
             -> UndefOr (Nullable (Union16 Document
                                           Blob
                                           Int8Array
                                           Int16Array
                                           Int32Array
                                           UInt8Array
                                           UInt8Array
                                           UInt8Array
                                           UInt8ClampedArray
                                           Float32Array
                                           Float64Array
                                           DataView
                                           ArrayBuffer
                                           FormData
                                           URLSearchParams
                                           String))
             -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.setRequestHeader(a,b)"
  prim__setRequestHeader :  XMLHttpRequest
                         -> ByteString
                         -> ByteString
                         -> PrimIO ()

namespace XMLHttpRequestEventTarget

  export
  %foreign "browser:lambda:x=>x.onabort"
  prim__onabort :  XMLHttpRequestEventTarget
                -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onabort = v}"
  prim__setOnabort :  XMLHttpRequestEventTarget
                   -> Nullable EventHandlerNonNull
                   -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onerror"
  prim__onerror :  XMLHttpRequestEventTarget
                -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onerror = v}"
  prim__setOnerror :  XMLHttpRequestEventTarget
                   -> Nullable EventHandlerNonNull
                   -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onload"
  prim__onload :  XMLHttpRequestEventTarget
               -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onload = v}"
  prim__setOnload :  XMLHttpRequestEventTarget
                  -> Nullable EventHandlerNonNull
                  -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onloadend"
  prim__onloadend :  XMLHttpRequestEventTarget
                  -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onloadend = v}"
  prim__setOnloadend :  XMLHttpRequestEventTarget
                     -> Nullable EventHandlerNonNull
                     -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onloadstart"
  prim__onloadstart :  XMLHttpRequestEventTarget
                    -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onloadstart = v}"
  prim__setOnloadstart :  XMLHttpRequestEventTarget
                       -> Nullable EventHandlerNonNull
                       -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.onprogress"
  prim__onprogress :  XMLHttpRequestEventTarget
                   -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onprogress = v}"
  prim__setOnprogress :  XMLHttpRequestEventTarget
                      -> Nullable EventHandlerNonNull
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.ontimeout"
  prim__ontimeout :  XMLHttpRequestEventTarget
                  -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.ontimeout = v}"
  prim__setOntimeout :  XMLHttpRequestEventTarget
                     -> Nullable EventHandlerNonNull
                     -> PrimIO ()

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

namespace ProgressEventInit

  export
  %foreign "browser:lambda:(a,b,c)=> {lengthComputable: a,loaded: b,total: c}"
  prim__new :  UndefOr Boolean
            -> UndefOr JSBits64
            -> UndefOr JSBits64
            -> PrimIO ProgressEventInit

  export
  %foreign "browser:lambda:x=>x.lengthComputable"
  prim__lengthComputable : ProgressEventInit -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.lengthComputable = v}"
  prim__setLengthComputable : ProgressEventInit -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.loaded"
  prim__loaded : ProgressEventInit -> PrimIO (UndefOr JSBits64)

  export
  %foreign "browser:lambda:(x,v)=>{x.loaded = v}"
  prim__setLoaded : ProgressEventInit -> UndefOr JSBits64 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.total"
  prim__total : ProgressEventInit -> PrimIO (UndefOr JSBits64)

  export
  %foreign "browser:lambda:(x,v)=>{x.total = v}"
  prim__setTotal : ProgressEventInit -> UndefOr JSBits64 -> PrimIO ()


text:
module TheoremProving

%default total

-- equality
{-
  data Equal : a -> b -> Type where
    Refl : Equal x x

  Equal x y is also written as x = y
-}

fiveIsFive : Equal 5 5
fiveIsFive = Refl

twoPlusTwoIsFour : 2 + 2 = 4
twoPlusTwoIsFour = Refl

-- the Empty type - Void, useful for
-- proving impossible cases in theorem proving.
-- Essentially, proof by contradiction

-- proof that zero can never be equal to a successor
disjoint : (n : Nat) -> Z = S n -> Void
disjoint n prf = replace { p = disjointTy } prf () where
  disjointTy : Nat -> Type
  disjointTy Z = ()
  disjointTy (S k) = Void

-- proving theorems
-- a proof in Idris is basically a program with a precise enough type to guarantee a special property of interest
-- Hence we write proofs the same way as other programs.

plusReduces : (n : Nat) -> plus Z n = n
plusReduces n = Refl

plusReducesZ : (n : Nat) -> n = plus n Z
plusReducesZ Z = Refl
plusReducesZ (S k) = cong S (plusReducesZ k)

plusReducesS : (n : Nat) -> (m : Nat) -> S (plus n m) = plus n (S m)
plusReducesS Z m = Refl
plusReducesS (S k) m = cong S (plusReducesS k m)

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 Web.Internal.VisibilityTypes

import JS

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

namespace VisibilityState

  public export
  data VisibilityState = Hidden | Visible

  public export
  Show VisibilityState where
    show Hidden = "hidden"
    show Visible = "visible"

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

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

  public export
  read : String -> Maybe VisibilityState
  read "hidden" = Just Hidden
  read "visible" = Just Visible
  read _ = Nothing

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

  export
  ToFFI VisibilityState String where
    toFFI = show

  export
  FromFFI VisibilityState String where
    fromFFI = read


text:
> module Rel.Preorder

> %default total
> %access public export

> ||| Preorder
> data Preorder : Type -> Type where
>   MkPreorder : {A : Type} ->
>                (R : A -> A -> Type) ->
>                (reflexive : (x : A) -> R x x) ->
>                (transitive : (x : A) -> (y : A) -> (z : A) -> R x y -> R y z -> R x z) ->
>                Preorder A

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Main
import Data.Vect

data DataStore : Type where
     MkData : (size : Nat) -> (items : Vect size String) -> DataStore

size : DataStore -> Nat
size (MkData size' items') = size'

items : (store : DataStore) -> Vect (size store) String
items (MkData size' items') = items'

addToStore : DataStore -> String -> DataStore
addToStore (MkData size store) newitem = MkData _ (addToData store)
  where
    addToData : Vect oldsize String -> Vect (S oldsize) String
    addToData [] = [newitem]
    addToData (x :: xs) = x :: addToData xs

data Command = Add String
             | Get Integer
             | Size
             | Search String
             | Quit

parseCommand : String -> String -> Maybe Command
parseCommand "add" str = Just (Add str)
parseCommand "get" val = case all isDigit (unpack val) of
                              False => Nothing
                              True => Just (Get (cast val))
parseCommand "size" _ = Just Size
parseCommand "search" val = Just (Search val)
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

parse : (input : String) -> Maybe Command
parse input = case span (/= ' ') input of
                   (cmd, args) => parseCommand cmd (ltrim args)

getEntry : (pos : Integer) -> (store : DataStore) ->
           Maybe (String, DataStore)
getEntry pos store
    = let store_items = items store in
          case integerToFin pos (size store) of
               Nothing => Just ("Out of range\n", store)
               Just id => Just (index id (items store) ++ "\n", store)

displayItems : String -> Vect n String -> String
displayItems {n = Z} x [] = ""
displayItems {n = (S len)} substr (str :: strs) =
  if isInfixOf substr str then
    (show len) ++ ": " ++ str ++ "\n" ++ (displayItems substr strs) else
    displayItems substr strs

getMatchingItems : (val : String) -> (store : DataStore) -> Maybe (String, DataStore)
getMatchingItems val store = Just (displayItems val (reverse (items store)), store)

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
    = case parse input of
           Nothing => Just ("Invalid command\n", store)
           Just (Add item) =>
              Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
           Just (Get pos) => getEntry pos store
           Just Size => Just ("Size: " ++ show (size store) ++ "\n", store)
           Just (Search val) => getMatchingItems val store
           Just Quit => Nothing

main : IO ()
main = replWith (MkData _ []) "Command: " processInput


text:
-- ---------------------------------------------------------- [ Properties.idr ]
-- Description : Properties files.
-- Copyright   : (c) Jan de Muijnck-Hughes
-- License     : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Config.Properties

import Effects
import Effect.File

import Lightyear
import Lightyear.Char
import Lightyear.Strings

import public Config.Error

import Config.Parse.Utils
import Config.Parse.Common

%access private

-- ------------------------------------------------------------------- [ Model ]
public export
data Property = PropFile (List Property)
              | PropEntry String String

-- ------------------------------------------------------------------ [ Parser ]
propComment : Parser ()
propComment = comment "#" <|> comment "!" <?> "Property Comments"

propSpace : Parser ()
propSpace = langSpace propComment <?> "Prop Space"

genKVpair : String -> Parser Property
genKVpair s = do
    (k,v) <- keyvalue s (map pack $ manyTill anyChar (skip endOfLine <|> propComment))
    pure $ PropEntry k v
  <?> "Proeprty KVPair"

kvpair : Parser Property
kvpair = genKVpair "=" <|> genKVpair ":"

export
parseProperties : Parser Property
parseProperties = do
    es <- some (propSpace *> kvpair)
    pure $ PropFile es
  <?> "Properties File"

-- -------------------------------------------------------------------- [ Read ]
export
readPropertiesConfig : String -> Eff (Either ConfigError Property) [FILE ()]
readPropertiesConfig = readConfigFile parseProperties

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

max_stars_repo_name: jfdm/idris-config

max_issues_repo_name: jfdm/idris-config

max_forks_repo_name: jfdm/idris-config


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

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

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

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


text:
-- | The core type system.
module Ethambda.System

import Ethambda.Common using ((<.>), (<.))

public export
data Tp : Type -> Type where
  Var : a -> Tp a
  Fun : Tp a -> Tp a -> Tp a

Show a => Show (Tp a) where
  show t = case t of
    -- Var a => ?foo
    Var a => show a
    Fun a0 b0 => mbrackets a0 <+> "→" <+> show b0
  where
    brackets : String -> String
    brackets s = "(" <+> s <+> ")"
    mbrackets : Show a => Tp a -> String
    mbrackets a = case a of
      Var _   => neutral
      Fun _ _ => brackets (show a)

max_stars_repo_name: fredefox/ethambda-idr

max_issues_repo_name: fredefox/ethambda-idr

max_forks_repo_name: fredefox/ethambda-idr


text:
module Replica.App.Replica

import Control.App
import Control.App.Console

import Data.List
import Data.Maybe
import Data.String

import Language.JSON

import System.Path

import Replica.App.FileSystem
import Replica.App.System
import Replica.Command.Run
import Replica.Core.Parse
import Replica.Core.Types
import Replica.Option.Global
import Replica.Other.Decorated
import Replica.Other.String
import Replica.Other.Validation

%default total

export
data CurrentTest : Type where

export
data GlobalConfig : Type where

public export
data ReplicaError
  = CantAccessTestFile String
  | InvalidJSON (List String)

export
Show ReplicaError where
  show (CantAccessTestFile x) = "Can't access file \{x}"
  show (InvalidJSON xs) = unlines $ "Can't parse JSON:" ::xs

export
testDir : String -> String
testDir = (</> "test")

export
logDir : String -> String
logDir = (</> "log")

export
lastRunLog : String -> String
lastRunLog rdir = logDir rdir </> "last.json"

export
getReplicaDir : State GlobalConfig Global e => App e String
getReplicaDir = map replicaDir $ get GlobalConfig

export
setAbsoluteReplicaDir : Has [State GlobalConfig Global, FileSystem] e => App e ()
setAbsoluteReplicaDir = do
  rdir <- getReplicaDir
  if isAbsolute rdir
     then pure ()
     else do
       pwd <- getCurrentDir
       modify GlobalConfig (record {replicaDir = pwd </> rdir})

export
getSingleTestDir : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getSingleTestDir = do
  d <- map replicaDir $ get GlobalConfig
  t <- get CurrentTest
  pure $ testDir d </> t.name

export
getInputFile : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getInputFile = do
  d <- map replicaDir $ get GlobalConfig
  t <- getSingleTestDir
  pure $ t </> defaultInput

export
getOutputFile : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getOutputFile = do
  d <- map replicaDir $ get GlobalConfig
  t <- getSingleTestDir
  pure $ t </> defaultOutput

export
getExpectedOutput : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getExpectedOutput = do
  d <- map replicaDir $ get GlobalConfig
  t <- getSingleTestDir
  pure $ t </> defaultExpected

export
getExpectedFile : Has
  [ State CurrentTest Test
  , State GlobalConfig Global ] e => App e String
getExpectedFile = do
  d <- map replicaDir $ get GlobalConfig
  t <- getSingleTestDir
  pure $ t </> defaultFile

export
getReplica :
  FileSystem (FSError :: e) =>
  Has [ State GlobalConfig Global
      , Exception ReplicaError ] e => App e Replica
getReplica = do
  ctx <- get GlobalConfig
  let f = ctx.file
  content <- handle (readFile f)
                    pure
                    (\err : FSError => throw $ CantAccessTestFile f)
  let Just json = parse content
        | Nothing => throw $ InvalidJSON []
  let Valid repl = jsonToReplica json
        | Error xs => throw $ InvalidJSON xs
  pure repl

export
when : Bool -> App e () -> App e ()
when cond x = if cond then x else pure ()

export
catchNew : App (err :: e) a -> (err -> App e a) -> App e a
catchNew x f = handle x pure (\er : err => f er)

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module Main

import System

import TestRunner
import ParsingTest

import UML
import UML.Reader

-- --------------------------------------------------------------------- [ XML ]

classTest : Test
classTest = parseTestGood classModel "Class Bob {\n + ad : String\n}\n\n Class Alice\n\n Bob --> Alice"

seqTest : Test
seqTest = parseTestGood sequenceModel "data TCPMsg\n A -> B : (syn : TCPMsg)\n B -> A : (ack : TCPMsg)\n A -> B : (syn : TCPMsg, ack : TCPMsg)\n"

depTest : Test
depTest = parseTestGood deploymentModel "device server presentation {\n    env appserver presentation {\n        artifact exe policyAdminUIwar with spec specxml {\n            a : \"asas\",\n            b : \"asas\"\n        }\n    }\n    properties {\n        a : \"sdsd\",\n        b : \"asas\"\n    }\n}\n\ndevice server policy {\n    env appserver policy {\n        artifact exe policyServerjar with spec specxml\n        properties {\n            a : \"sdsd\",\n            b : \"asas\"\n        }\n    }\n}\n\ndevice server product {\n    env appserver product {\n        artifact exe productServerjar\n    }\n    env engine rules {\n        artifact doc rules\n    }\n}\n\ndevice workstation user {\n    env os workstation {\n        artifact exe productServerUIexe\n    }\n}\n\ndevice server documents {\n    env os server {\n        artifact exe docMngmntSystem\n    }\n}\n\ndevice server dbServer {\n    env engine dbms {\n        artifact doc schemaproduct\n        artifact doc schemapolicy\n    }\n}\n\ndevice server dirServer {\n    env app ldapServer {\n        artifact doc GrpUsrheirarchy\n    }\n}\n\ndevice server uWriteRating {\n    env engine rules {\n        artifact doc ratingrules\n        artifact doc underwritingrules\n    }\n    env appserver apps {\n        artifact exe underwritingenginejar\n        artifact exe ratingenginejar\n    }\n}\n\npresentation commsWith policy via http\npolicy commsWith uWriteRating via http\npolicy commsWith dirServer via http\npolicy commsWith dbServer via http\npolicy commsWith documents via http\ndbServer commsWith product via http\nproduct commsWith documents via http\nuser commsWith product via http\n"

compTest : Test
compTest = parseTestGood componentModel "data Int\ndata String\n\ndata User {\n  id : String,\n  name : String\n}\n\ndata Item {\n  id : String,\n  name : String,\n  desc : String\n}\n\ndata Order {\n  id : String,\n  item : Items\n}\n\ncomponent Accounting {\n  provides ManageOrders from Orders\n  provides ManageCustomers from Customers\n  requires ManageInventory from Warehouses\n\n  component Customers {\n    interface ManageCustomers {\n      addCustomer : (c : Customer) -> Bool\n      removeCustomer : (c : Customer) -> Bool\n    }\n  }\n\n  component Orders {\n    interface ManageOrders {\n      createOrder : Int\n      addToOrder : (p : Product) -> (orderID : Int) -> Bool\n      removeFromOrder : (p : Product) -> (orderID : Int) -> Bool\n    }\n    requires ManageCustomers from Customers\n    requires ManageInventory from Warehouses\n  }\n}\n\ncomponent Warehouses {\n  provides SearchInventory from Inventory\n  provides ManageInventory from Inventory\n\n  component Inventory {\n    interface SearchInventory {\n      createOrder : Int\n      addToOrder : (p : Product) -> (orderID : Int) -> Bool\n      removeFromOrder : (p : Product) -> (orderID : Int) -> Bool\n    }\n    interface ManageInventory {\n      createOrder : Int\n      addToOrder : (p : Product) -> (orderID : Int) -> Bool\n      removeFromOrder : (p : Product) -> (orderID : Int) -> Bool\n    }\n  }\n}\n\ncomponent WebStore {\n  provides ProductSearch from SearchEngine\n  provides OnlineShopping from ShoppingCart\n  provides UserSession from Authentication\n\n  requires SearchInventory from Warehouses\n  requires ManageOrders from Accounting\n  requires ManageCustomers from Accounting\n\n  component Authentication {\n    interface UserSession {\n      createOrder : Int\n      addToOrder : (p : Product) -> (orderID : Int) -> Bool\n      removeFromOrder : (p : Product) -> (orderID : Int) -> Bool\n    }\n    requires ManageCustomers from Accounting\n  }\n\n  component ShoppingCart {\n    interface OnlineShopping {\n      createOrder : Int\n      addToOrder : (p : Product) -> (orderID : Int) -> Bool\n      removeFromOrder : (p : Product) -> (orderID : Int) -> Bool\n    }\n    requires UserSession from Authentication\n    requires ManageOrders from Accounting\n  }\n\n  component SearchEngine {\n    interface ProductSearch {\n      createOrder : Int\n      addToOrder : (p : Product) -> (orderID : Int) -> Bool\n      removeFromOrder : (p : Product) -> (orderID : Int) -> Bool\n\n    }\n    requires SearchInventory from Warehouses\n  }\n\n}\n"

-- -------------------------------------------------------------------- [ Main ]
main : IO ()
main = do
    run $ tests (Z) [classTest, seqTest, depTest, compTest]
    exit 0

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

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module Main

import Erlang.System

main : IO ()
main = do
    ok <- setEnv "HELLO" "HI" True
    printLn ok
    Just str <- getEnv "HELLO"
        | Nothing => pure ()
    putStrLn str
    ok <- setEnv "HELLO" "HO" False
    printLn ok
    Just str <- getEnv "HELLO"
        | Nothing => pure ()
    putStrLn str
    ok <- setEnv "HELLO" "EH" True
    printLn ok
    Just str <- getEnv "HELLO"
        | Nothing => pure ()
    putStrLn str
    ok <- unsetEnv "HELLO"
    printLn ok
    Just str <- getEnv "HELLO"
        | Nothing => putStrLn "Nothing there"
    pure ()


text:
module Web.Raw.Css

import JS
import Web.Internal.CssPrim
import Web.Internal.Types

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

namespace CSSGroupingRule

  export
  cssRules :  (0 _ : JSType t1)
           => {auto 0 _ : Elem CSSGroupingRule (Types t1)}
           -> (obj : t1)
           -> JSIO CSSRuleList
  cssRules a = primJS $ CSSGroupingRule.prim__cssRules (up a)

  export
  deleteRule :  (0 _ : JSType t1)
             => {auto 0 _ : Elem CSSGroupingRule (Types t1)}
             -> (obj : t1)
             -> (index : Bits32)
             -> JSIO ()
  deleteRule a b = primJS $ CSSGroupingRule.prim__deleteRule (up a) b

  export
  insertRule :  (0 _ : JSType t1)
             => {auto 0 _ : Elem CSSGroupingRule (Types t1)}
             -> (obj : t1)
             -> (rule : String)
             -> (index : Optional Bits32)
             -> JSIO Bits32
  insertRule a b c = primJS
                   $ CSSGroupingRule.prim__insertRule (up a) b (toFFI c)

  export
  insertRule' :  (0 _ : JSType t1)
              => {auto 0 _ : Elem CSSGroupingRule (Types t1)}
              -> (obj : t1)
              -> (rule : String)
              -> JSIO Bits32
  insertRule' a b = primJS $ CSSGroupingRule.prim__insertRule (up a) b undef

namespace CSSImportRule

  export
  href : (obj : CSSImportRule) -> JSIO String
  href a = primJS $ CSSImportRule.prim__href a

  export
  media : (obj : CSSImportRule) -> JSIO MediaList
  media a = primJS $ CSSImportRule.prim__media a

  export
  styleSheet : (obj : CSSImportRule) -> JSIO CSSStyleSheet
  styleSheet a = primJS $ CSSImportRule.prim__styleSheet a

namespace CSSMarginRule

  export
  name : (obj : CSSMarginRule) -> JSIO String
  name a = primJS $ CSSMarginRule.prim__name a

  export
  style : (obj : CSSMarginRule) -> JSIO CSSStyleDeclaration
  style a = primJS $ CSSMarginRule.prim__style a

namespace CSSNamespaceRule

  export
  namespaceURI : (obj : CSSNamespaceRule) -> JSIO String
  namespaceURI a = primJS $ CSSNamespaceRule.prim__namespaceURI a

  export
  prefix_ : (obj : CSSNamespaceRule) -> JSIO String
  prefix_ a = primJS $ CSSNamespaceRule.prim__prefix a

namespace CSSPageRule

  export
  selectorText : CSSPageRule -> Attribute True I String
  selectorText v = fromPrim "CSSPageRule.getselectorText"
                            prim__selectorText
                            prim__setSelectorText
                            v

  export
  style : (obj : CSSPageRule) -> JSIO CSSStyleDeclaration
  style a = primJS $ CSSPageRule.prim__style a

namespace CSSPseudoElement

  export
  element : (obj : CSSPseudoElement) -> JSIO Element
  element a = primJS $ CSSPseudoElement.prim__element a

  export
  type : (obj : CSSPseudoElement) -> JSIO String
  type a = primJS $ CSSPseudoElement.prim__type a

namespace CSSRule

  public export
  CHARSET_RULE : Bits16
  CHARSET_RULE = 2

  public export
  FONT_FACE_RULE : Bits16
  FONT_FACE_RULE = 5

  public export
  IMPORT_RULE : Bits16
  IMPORT_RULE = 3

  public export
  MARGIN_RULE : Bits16
  MARGIN_RULE = 9

  public export
  MEDIA_RULE : Bits16
  MEDIA_RULE = 4

  public export
  NAMESPACE_RULE : Bits16
  NAMESPACE_RULE = 10

  public export
  PAGE_RULE : Bits16
  PAGE_RULE = 6

  public export
  STYLE_RULE : Bits16
  STYLE_RULE = 1

  export
  cssText :  (0 _ : JSType t)
          => {auto 0 _ : Elem CSSRule (Types t)}
          -> t
          -> Attribute True I String
  cssText v = fromPrim "CSSRule.getcssText"
                       prim__cssText
                       prim__setCssText
                       (v :> CSSRule)

  export
  parentRule :  (0 _ : JSType t1)
             => {auto 0 _ : Elem CSSRule (Types t1)}
             -> (obj : t1)
             -> JSIO (Maybe CSSRule)
  parentRule a = tryJS "CSSRule.parentRule" $ CSSRule.prim__parentRule (up a)

  export
  parentStyleSheet :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem CSSRule (Types t1)}
                   -> (obj : t1)
                   -> JSIO (Maybe CSSStyleSheet)
  parentStyleSheet a = tryJS "CSSRule.parentStyleSheet"
                     $ CSSRule.prim__parentStyleSheet (up a)

  export
  type :  (0 _ : JSType t1)
       => {auto 0 _ : Elem CSSRule (Types t1)}
       -> (obj : t1)
       -> JSIO Bits16
  type a = primJS $ CSSRule.prim__type (up a)

namespace CSSRuleList

  export
  length : (obj : CSSRuleList) -> JSIO Bits32
  length a = primJS $ CSSRuleList.prim__length a

  export
  item : (obj : CSSRuleList) -> (index : Bits32) -> JSIO (Maybe CSSRule)
  item a b = tryJS "CSSRuleList.item" $ CSSRuleList.prim__item a b

namespace CSSStyleDeclaration

  export
  cssFloat : CSSStyleDeclaration -> Attribute True I String
  cssFloat v = fromPrim "CSSStyleDeclaration.getcssFloat"
                        prim__cssFloat
                        prim__setCssFloat
                        v

  export
  cssText : CSSStyleDeclaration -> Attribute True I String
  cssText v = fromPrim "CSSStyleDeclaration.getcssText"
                       prim__cssText
                       prim__setCssText
                       v

  export
  length : (obj : CSSStyleDeclaration) -> JSIO Bits32
  length a = primJS $ CSSStyleDeclaration.prim__length a

  export
  parentRule : (obj : CSSStyleDeclaration) -> JSIO (Maybe CSSRule)
  parentRule a = tryJS "CSSStyleDeclaration.parentRule"
               $ CSSStyleDeclaration.prim__parentRule a

  export
  getPropertyPriority :  (obj : CSSStyleDeclaration)
                      -> (property : String)
                      -> JSIO String
  getPropertyPriority a b = primJS
                          $ CSSStyleDeclaration.prim__getPropertyPriority a b

  export
  getPropertyValue :  (obj : CSSStyleDeclaration)
                   -> (property : String)
                   -> JSIO String
  getPropertyValue a b = primJS $ CSSStyleDeclaration.prim__getPropertyValue a b

  export
  item : (obj : CSSStyleDeclaration) -> (index : Bits32) -> JSIO String
  item a b = primJS $ CSSStyleDeclaration.prim__item a b

  export
  removeProperty :  (obj : CSSStyleDeclaration)
                 -> (property : String)
                 -> JSIO String
  removeProperty a b = primJS $ CSSStyleDeclaration.prim__removeProperty a b

  export
  setProperty :  (obj : CSSStyleDeclaration)
              -> (property : String)
              -> (value : String)
              -> (priority : Optional String)
              -> JSIO ()
  setProperty a b c d = primJS
                      $ CSSStyleDeclaration.prim__setProperty a b c (toFFI d)

  export
  setProperty' :  (obj : CSSStyleDeclaration)
               -> (property : String)
               -> (value : String)
               -> JSIO ()
  setProperty' a b c = primJS
                     $ CSSStyleDeclaration.prim__setProperty a b c undef

namespace CSSStyleRule

  export
  selectorText : CSSStyleRule -> Attribute True I String
  selectorText v = fromPrim "CSSStyleRule.getselectorText"
                            prim__selectorText
                            prim__setSelectorText
                            v

  export
  style : (obj : CSSStyleRule) -> JSIO CSSStyleDeclaration
  style a = primJS $ CSSStyleRule.prim__style a

namespace CSSStyleSheet

  export
  cssRules : (obj : CSSStyleSheet) -> JSIO CSSRuleList
  cssRules a = primJS $ CSSStyleSheet.prim__cssRules a

  export
  ownerRule : (obj : CSSStyleSheet) -> JSIO (Maybe CSSRule)
  ownerRule a = tryJS "CSSStyleSheet.ownerRule"
              $ CSSStyleSheet.prim__ownerRule a

  export
  rules : (obj : CSSStyleSheet) -> JSIO CSSRuleList
  rules a = primJS $ CSSStyleSheet.prim__rules a

  export
  addRule :  (obj : CSSStyleSheet)
          -> (selector : Optional String)
          -> (style : Optional String)
          -> (index : Optional Bits32)
          -> JSIO Int32
  addRule a b c d = primJS
                  $ CSSStyleSheet.prim__addRule a (toFFI b) (toFFI c) (toFFI d)

  export
  addRule' : (obj : CSSStyleSheet) -> JSIO Int32
  addRule' a = primJS $ CSSStyleSheet.prim__addRule a undef undef undef

  export
  deleteRule : (obj : CSSStyleSheet) -> (index : Bits32) -> JSIO ()
  deleteRule a b = primJS $ CSSStyleSheet.prim__deleteRule a b

  export
  insertRule :  (obj : CSSStyleSheet)
             -> (rule : String)
             -> (index : Optional Bits32)
             -> JSIO Bits32
  insertRule a b c = primJS $ CSSStyleSheet.prim__insertRule a b (toFFI c)

  export
  insertRule' : (obj : CSSStyleSheet) -> (rule : String) -> JSIO Bits32
  insertRule' a b = primJS $ CSSStyleSheet.prim__insertRule a b undef

  export
  removeRule : (obj : CSSStyleSheet) -> (index : Optional Bits32) -> JSIO ()
  removeRule a b = primJS $ CSSStyleSheet.prim__removeRule a (toFFI b)

  export
  removeRule' : (obj : CSSStyleSheet) -> JSIO ()
  removeRule' a = primJS $ CSSStyleSheet.prim__removeRule a undef

namespace MediaList

  export
  length : (obj : MediaList) -> JSIO Bits32
  length a = primJS $ MediaList.prim__length a

  export
  mediaText : MediaList -> Attribute True I String
  mediaText v = fromPrim "MediaList.getmediaText"
                         prim__mediaText
                         prim__setMediaText
                         v

  export
  appendMedium : (obj : MediaList) -> (medium : String) -> JSIO ()
  appendMedium a b = primJS $ MediaList.prim__appendMedium a b

  export
  deleteMedium : (obj : MediaList) -> (medium : String) -> JSIO ()
  deleteMedium a b = primJS $ MediaList.prim__deleteMedium a b

  export
  item : (obj : MediaList) -> (index : Bits32) -> JSIO (Maybe String)
  item a b = tryJS "MediaList.item" $ MediaList.prim__item a b

namespace StyleSheet

  export
  disabled :  (0 _ : JSType t)
           => {auto 0 _ : Elem StyleSheet (Types t)}
           -> t
           -> Attribute True I Bool
  disabled v = fromPrim "StyleSheet.getdisabled"
                        prim__disabled
                        prim__setDisabled
                        (v :> StyleSheet)

  export
  href :  (0 _ : JSType t1)
       => {auto 0 _ : Elem StyleSheet (Types t1)}
       -> (obj : t1)
       -> JSIO (Maybe String)
  href a = tryJS "StyleSheet.href" $ StyleSheet.prim__href (up a)

  export
  media :  (0 _ : JSType t1)
        => {auto 0 _ : Elem StyleSheet (Types t1)}
        -> (obj : t1)
        -> JSIO MediaList
  media a = primJS $ StyleSheet.prim__media (up a)

  export
  ownerNode :  (0 _ : JSType t1)
            => {auto 0 _ : Elem StyleSheet (Types t1)}
            -> (obj : t1)
            -> JSIO (Maybe (NS I [ Element , ProcessingInstruction ]))
  ownerNode a = tryJS "StyleSheet.ownerNode" $ StyleSheet.prim__ownerNode (up a)

  export
  parentStyleSheet :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem StyleSheet (Types t1)}
                   -> (obj : t1)
                   -> JSIO (Maybe CSSStyleSheet)
  parentStyleSheet a = tryJS "StyleSheet.parentStyleSheet"
                     $ StyleSheet.prim__parentStyleSheet (up a)

  export
  title :  (0 _ : JSType t1)
        => {auto 0 _ : Elem StyleSheet (Types t1)}
        -> (obj : t1)
        -> JSIO (Maybe String)
  title a = tryJS "StyleSheet.title" $ StyleSheet.prim__title (up a)

  export
  type :  (0 _ : JSType t1)
       => {auto 0 _ : Elem StyleSheet (Types t1)}
       -> (obj : t1)
       -> JSIO String
  type a = primJS $ StyleSheet.prim__type (up a)

namespace StyleSheetList

  export
  length : (obj : StyleSheetList) -> JSIO Bits32
  length a = primJS $ StyleSheetList.prim__length a

  export
  item :  (obj : StyleSheetList)
       -> (index : Bits32)
       -> JSIO (Maybe CSSStyleSheet)
  item a b = tryJS "StyleSheetList.item" $ StyleSheetList.prim__item a b

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

namespace ElementCSSInlineStyle

  export
  style :  (0 _ : JSType t1)
        => {auto 0 _ : Elem ElementCSSInlineStyle (Types t1)}
        -> (obj : t1)
        -> JSIO CSSStyleDeclaration
  style a = primJS $ ElementCSSInlineStyle.prim__style (up a)

namespace LinkStyle

  export
  sheet :  (0 _ : JSType t1)
        => {auto 0 _ : Elem LinkStyle (Types t1)}
        -> (obj : t1)
        -> JSIO (Maybe CSSStyleSheet)
  sheet a = tryJS "LinkStyle.sheet" $ LinkStyle.prim__sheet (up a)


text:
module Flexidisc.OrdList.Diff

import public Flexidisc.OrdList.Disjoint
import public Flexidisc.OrdList.Fresh
import public Flexidisc.OrdList.Label
import public Flexidisc.OrdList.Sub
import public Flexidisc.OrdList.Type

%default total
%access public export

||| compute the difference between the first and the second list.
diffKeys : DecEq k => (xs, ys : OrdList k v o) -> OrdList k v o
diffKeys [] ys = []
diffKeys ((lx, vx) :: xs) ys with (decFresh lx ys)
  | Yes prf   = (lx, vx) :: diffKeys xs ys
  | No contra = diffKeys xs ys

||| Apply a patch `xs` to an `OrdList` `ys`.
||| The label of `ys` that are in `xs` are updated,
||| and the fresh element of `xs` are added
patch : DecEq k => (xs, ys : OrdList k v o) -> OrdList k v o
patch xs ys = merge (diffKeys ys xs) xs

diffIsSub : DecEq k => {xs : OrdList k v o} -> Sub (diffKeys xs ys) xs
diffIsSub {xs = []} = Empty
diffIsSub {xs = (lx, vx) :: xs} {ys} with (decFresh lx ys)
  | Yes prf   = Keep diffIsSub
  | No contra = Skip diffIsSub

diffIsDisjoint : DecEq k => {xs : OrdList k v o} ->
                 Disjoint (diffKeys xs ys) ys
diffIsDisjoint {xs = []} = []
diffIsDisjoint {xs = (kx, vx) :: xs} {ys} with (decFresh kx ys)
  | Yes prf  = isFreshFromEvidence prf :: diffIsDisjoint
  | No contra = diffIsDisjoint

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
> module Lit
>
> %default total

a > b

a < b

> data V a = Empty | Extend a (V a)

> isCons : V a -> Bool
> isCons Empty = False
> isCons (Extend _ _) = True

< namespace Hidden
<   data U a = Empty | Extend a (U a)


text:
module Compiler.ES.RemoveUnused

import Data.SortedSet
import Data.SortedMap
import Data.Vect
import Data.List

import Core.CompileExpr
import Core.Name
import Core.FC

import Debug.Trace

mutual
  usedNames : NamedCExp -> SortedSet Name
  usedNames (NmLocal fc n) = empty
  usedNames (NmRef fc n) = insert n empty
  usedNames (NmLam fc n e) = usedNames e
  usedNames (NmApp fc x args) = usedNames x `union` concat (usedNames <$> args)
  usedNames (NmPrimVal fc c) = empty
  usedNames (NmOp fc op args) = concat $ usedNames <$> args
  usedNames (NmConCase fc sc alts def) = (usedNames sc `union` concat (usedNamesConAlt <$> alts)) `union` maybe empty usedNames def
  usedNames (NmConstCase fc sc alts def) = (usedNames sc `union` concat (usedNamesConstAlt <$> alts)) `union` maybe empty usedNames def
  usedNames (NmExtPrim fc p args) = concat $ usedNames <$> args
  usedNames (NmCon fc x t args) = concat $ usedNames <$> args
  usedNames (NmDelay fc t) = usedNames t
  usedNames (NmForce fc t) = usedNames t
  usedNames (NmLet fc x val sc) = usedNames val `union` usedNames sc
  usedNames (NmErased fc) = empty
  usedNames (NmCrash fc msg) = empty

  usedNamesConAlt : NamedConAlt -> SortedSet Name
  usedNamesConAlt (MkNConAlt n t args exp) = usedNames exp

  usedNamesConstAlt : NamedConstAlt -> SortedSet Name
  usedNamesConstAlt (MkNConstAlt c exp) = usedNames exp

usedNamesDef : NamedDef -> SortedSet Name
usedNamesDef (MkNmFun args exp) = usedNames exp
usedNamesDef (MkNmError exp) = usedNames exp
usedNamesDef (MkNmForeign cs args ret) = empty
usedNamesDef (MkNmCon _ _ _) = empty

defsToUsedMap : List (Name, FC, NamedDef) -> SortedMap Name (SortedSet Name)
defsToUsedMap defs =
  fromList $ (\(n,_,d)=> (n, usedNamesDef d)) <$> defs

calcUsed : SortedSet Name -> SortedMap Name (SortedSet Name) -> List Name -> SortedSet Name
calcUsed done d [] = done
calcUsed done d xs =
  let used_in_xs = foldl f empty $ (\z => lookup z d) <$> xs
      new_done   = union done (fromList xs)
  in calcUsed (new_done) d (SortedSet.toList $ difference used_in_xs new_done)
  where
    f : SortedSet Name -> Maybe (SortedSet Name) -> SortedSet Name
    f x Nothing = x
    f x (Just y) = union x y

calcUsedDefs : List Name -> List (Name, FC, NamedDef) -> List (Name, FC, NamedDef)
calcUsedDefs names defs =
  let usedNames = calcUsed empty (defsToUsedMap defs) names
  in List.filter (\(n, fc, d) => contains n usedNames) defs

export
defsUsedByNamedCExp : NamedCExp -> List (Name, FC, NamedDef) -> List (Name, FC, NamedDef)
defsUsedByNamedCExp exp defs = calcUsedDefs (SortedSet.toList $ usedNames exp) defs


text:
module Ch04.Eval

import Ch03.Arith
import Ch04.NaturalInduction
import Data.Fin

%default total

mutual
  namespace IsBadBool
    ||| Propositional type describing that a term is a "bad boolean".
    data IsBadBool : Term -> Type where
      IsStuckTerm : {pf : IsStuck t} -> IsBadBool t
      IsNat : {pf : IsNumValue t} -> IsBadBool t

  namespace IsBadNat
    ||| Propositional type describing that a term is a "bad nat".
    data IsBadNat : Term -> Type where
      IsStuckTerm : {pf : IsStuck t} -> IsBadNat t
      IsBool : {pf : IsBoolValue t} -> IsBadNat t

  ||| Propositional type describing that a term is stuck.
  data IsStuck : Term -> Type where
    EIfWrong : {t1,t2,t3 : Term} ->
               {pf : IsBadBool t1} ->
               IsStuck (IfThenElse t1 t2 t3)
    ESuccWrong : {t : Term} ->
                 {pf : IsBadNat t} ->
                 IsStuck (Succ t)
    EPredWrong : {t : Term} ->
                 {pf : IsBadNat t} ->
                 IsStuck (Pred t)
    EIsZeroWrong : {t : Term} ->
                   {pf : IsBadNat t} ->
                   IsStuck (IsZero t)

-- We are using an ad hoc definition of what it means to be stuck,
-- which is not exactly the one used in the book (normal but not a value).
-- This is for convenience. (TODO: Fix this maybe.)
||| Propositional type describing that a term is fully evaluated.
FullyEvaluated : Term -> Type
FullyEvaluated t = Either (IsStuck t) (IsValue t)

||| Propositional type describing that a term is normal.
Normal : Term -> Type
Normal t = (t' : Term) -> EvalsTo t t' -> Void

--------------------------------------------------------------------------------
-- Helper lemmas for `fully_evaluated_is_normal`.
--------------------------------------------------------------------------------

true_is_normal : Normal True
true_is_normal = \_, r => case r of
                               EIfTrue impossible
                               EIfFalse impossible
                               (EIf _) impossible
                               (ESucc _) impossible
                               EPredZero impossible
                               EPredSucc impossible
                               (EPred _) impossible
                               EIsZeroZero impossible
                               EIsZeroSucc impossible
                               (EIsZero _) impossible

false_is_normal : Normal False
false_is_normal = \_, r => case r of
                                EIfTrue impossible
                                EIfFalse impossible
                                (EIf _) impossible
                                (ESucc _) impossible
                                EPredZero impossible
                                EPredSucc impossible
                                (EPred _) impossible
                                EIsZeroZero impossible
                                EIsZeroSucc impossible
                                (EIsZero _) impossible

zero_is_normal : Normal Zero
zero_is_normal = \_, r => case r of
                               EIfTrue impossible
                               EIfFalse impossible
                               (EIf _) impossible
                               (ESucc _) impossible
                               EPredZero impossible
                               EPredSucc impossible
                               (EPred _) impossible
                               EIsZeroZero impossible
                               EIsZeroSucc impossible
                               (EIsZero _) impossible

num_values_are_normal_helper : (nv : NumValue) -> Normal (nv2t nv)
num_values_are_normal_helper nv = case nv of
                                       Zero => zero_is_normal
                                       (Succ nv') => \_, r => case r of
                                                                    (ESucc r') => (num_values_are_normal_helper nv') _ r'

num_values_are_normal : (t : Term) -> {pf : IsNumValue t} -> Normal t
num_values_are_normal (nv2t nv) {pf=ConvertedFrom nv} = num_values_are_normal_helper nv

values_are_normal : (t : Term) -> {pf : IsValue t} -> Normal t
values_are_normal (bv2t bv) {pf=ConvertedFrom (Left bv)} = case bv of
                                                                True => true_is_normal
                                                                False => false_is_normal
values_are_normal (nv2t nv) {pf=ConvertedFrom (Right nv)} = num_values_are_normal (nv2t nv) {pf=ConvertedFrom nv}

num_value_not_bool_value : (nv : NumValue) -> Not (IsBoolValue (nv2t nv))
num_value_not_bool_value Zero = \pf_bv => case pf_bv of
                                               ConvertedFrom True impossible
                                               ConvertedFrom False impossible
num_value_not_bool_value (Succ nv) = \pf_bv => case pf_bv of
                                                    (ConvertedFrom True) impossible
                                                    (ConvertedFrom False) impossible

num_value_not_stuck : (nv : NumValue) -> Not (IsStuck (nv2t nv))
num_value_not_stuck Zero = \pf_bad => case pf_bad of
                                           EIfWrong impossible
                                           ESuccWrong impossible
                                           EPredWrong impossible
                                           EIsZeroWrong impossible
num_value_not_stuck (Succ nv) = \pf_bad => case pf_bad of
                                                ESuccWrong {pf=pf_succ_wrong} => case pf_succ_wrong of
                                                                                IsStuckTerm {pf=pf_stuck} => absurd ((num_value_not_stuck nv) pf_stuck)
                                                                                IsBool {pf=pf_bool} => absurd ((num_value_not_bool_value nv) pf_bool)

num_value_not_bad_nat : (nv : NumValue) -> Not (IsBadNat (nv2t nv))
num_value_not_bad_nat nv = \pf_bad => case pf_bad of
                                           IsStuckTerm {pf=pf_stuck} => absurd ((num_value_not_stuck nv) pf_stuck)
                                           IsBool {pf=pf_bool} => absurd ((num_value_not_bool_value nv) pf_bool)

values_not_stuck : {t : Term} -> {pf : IsValue t} -> Not (IsStuck t)
values_not_stuck {t = (bv2t bv)} {pf = (ConvertedFrom (Left bv))} = \pf_stuck => case bv of
                                                                                True => case pf_stuck of
                                                                                EIfWrong impossible
                                                                                ESuccWrong impossible
                                                                                EPredWrong impossible
                                                                                EIsZeroWrong impossible
                                                                                False => case pf_stuck of
                                                                                EIfWrong impossible
                                                                                ESuccWrong impossible
                                                                                EPredWrong impossible
                                                                                EIsZeroWrong impossible
values_not_stuck {t = (nv2t nv)} {pf = (ConvertedFrom (Right nv))} = num_value_not_stuck nv

bool_not_bad_bool : {t : Term} -> {pf : IsBoolValue t} -> Not (IsBadBool t)
bool_not_bad_bool {pf} = \x => case x of
                                    IsStuckTerm {pf=pf_stuck} => (values_not_stuck {pf=boolValueIsValue pf}) pf_stuck
                                    IsNat {pf=pf_nat} => numNotBool pf_nat pf

nat_not_bad_nat : {t : Term} -> {pf : IsNumValue t} -> Not (IsBadNat t)
nat_not_bad_nat {pf} = \x => case x of
                                  IsStuckTerm {pf=pf_stuck} => (values_not_stuck {pf=numValueIsValue pf}) pf_stuck
                                  IsBool {pf=pf_bool} => numNotBool pf pf_bool

stuck_is_normal : IsStuck t -> Normal t
stuck_is_normal (EIfWrong {pf}) = \_, r => case r of
                                                EIfTrue => (bool_not_bad_bool {pf=ConvertedFrom True}) pf
                                                EIfFalse => (bool_not_bad_bool {pf=ConvertedFrom False}) pf
                                                (EIf {t1} r') => case pf of
                                                                      IsStuckTerm {pf=pf_stuck} => stuck_is_normal pf_stuck _ r'
                                                                      IsNat {pf=pf_num} => values_are_normal t1 {pf=numValueIsValue pf_num} _ r'
stuck_is_normal (ESuccWrong {t} {pf}) = \_, r => case r of
                                                      (ESucc r') => case pf of
                                                                         IsStuckTerm {pf=pf_stuck} => stuck_is_normal pf_stuck _ r'
                                                                         IsBool {pf=pf_bool} => values_are_normal t {pf=boolValueIsValue pf_bool} _ r'
stuck_is_normal (EPredWrong {t} {pf}) = \_, r => case r of
                                                      EPredZero => nat_not_bad_nat {pf=ConvertedFrom Zero} pf
                                                      EPredSucc {nv1=nv} {pf=pf_num} => nat_not_bad_nat {pf=succNumValueIsNumValue pf_num} pf
                                                      (EPred r') => case pf of
                                                                         IsStuckTerm {pf=pf_stuck} => stuck_is_normal pf_stuck _ r'
                                                                         IsBool {pf=pf_bool} => values_are_normal t {pf=boolValueIsValue pf_bool} _ r'
stuck_is_normal (EIsZeroWrong {t} {pf}) = \_, r => case r of
                                                        EIsZeroZero => nat_not_bad_nat {pf=ConvertedFrom Zero} pf
                                                        EIsZeroSucc {nv1=nv} {pf=pf_num} => nat_not_bad_nat {pf=succNumValueIsNumValue pf_num} pf
                                                        (EIsZero r') => case pf of
                                                                             IsStuckTerm {pf=pf_stuck} => stuck_is_normal pf_stuck _ r'
                                                                             IsBool {pf=pf_bool} => values_are_normal t {pf=boolValueIsValue pf_bool} _ r'

||| Proof that a fully evaluated term is also normal.
fully_evaluated_is_normal : FullyEvaluated t -> Normal t
fully_evaluated_is_normal (Left pf_stuck) = stuck_is_normal pf_stuck
fully_evaluated_is_normal {t} (Right pf_value) = values_are_normal t {pf=pf_value}

-----------------------------------------------------------------------
-- Helper lemmas for `normal_is_fully_evaluated`.
-----------------------------------------------------------------------

if_subterm_of_normal_is_normal : {x,y,z : Term} -> Normal (IfThenElse x y z) -> Normal x
if_subterm_of_normal_is_normal pf = \_, r => absurd (pf _ (EIf r))

succ_subterm_of_normal_is_normal : {t : Term} -> Normal (Succ t) -> Normal t
succ_subterm_of_normal_is_normal pf = \_, r => absurd (pf _ (ESucc r))

pred_subterm_of_normal_is_normal : {t : Term} -> Normal (Pred t) -> Normal t
pred_subterm_of_normal_is_normal pf = \_, r => absurd (pf _ (EPred r))

is_zero_subterm_of_normal_is_normal : {t : Term} -> Normal (IsZero t) -> Normal t
is_zero_subterm_of_normal_is_normal pf = \_, r => absurd (pf _ (EIsZero r))

succ_of_fully_evaluated_is_fully_evaluated : {t : Term} -> FullyEvaluated t -> FullyEvaluated (Succ t)
succ_of_fully_evaluated_is_fully_evaluated {t} (Left pf_stuck) = Left (ESuccWrong {pf=IsStuckTerm {pf=pf_stuck}})
succ_of_fully_evaluated_is_fully_evaluated {t} (Right pf_val) = case pf_val of
                                                                     ConvertedFrom (Left bv) => Left (ESuccWrong {pf=IsBool {pf=ConvertedFrom bv}})
                                                                     ConvertedFrom (Right nv) => Right (numValueIsValue $ succNumValueIsNumValue (ConvertedFrom nv))

||| Proof that a normal term is also fully evaluated.
normal_is_fully_evaluated : Normal t -> FullyEvaluated t
normal_is_fully_evaluated {t=True} _ = Right (ConvertedFrom (Left True))
normal_is_fully_evaluated {t=False} _ = Right (ConvertedFrom (Left False))
normal_is_fully_evaluated {t=IfThenElse t1 t2 t3} pf_normal = case normal_is_fully_evaluated (if_subterm_of_normal_is_normal pf_normal) of
                                                                   (Left pf_stuck) => Left (EIfWrong {pf=IsStuckTerm {pf=pf_stuck}})
                                                                   (Right pf_val) => case pf_val of
                                                                                (ConvertedFrom (Left bv)) => case bv of
                                                                                True => absurd (pf_normal _ EIfTrue)
                                                                                False => absurd (pf_normal _ EIfFalse)
                                                                                (ConvertedFrom (Right nv)) => Left (EIfWrong {pf=IsNat {pf=ConvertedFrom nv}})
normal_is_fully_evaluated {t=Zero} _ = Right (ConvertedFrom (Right Zero))
normal_is_fully_evaluated {t=Succ t'} pf_normal = succ_of_fully_evaluated_is_fully_evaluated $
                                                  normal_is_fully_evaluated $
                                                  succ_subterm_of_normal_is_normal pf_normal
normal_is_fully_evaluated {t=Pred t'} pf_normal = case normal_is_fully_evaluated $ pred_subterm_of_normal_is_normal pf_normal of
                                                       Left pf_stuck => Left (EPredWrong {pf=IsStuckTerm {pf=pf_stuck}})
                                                       Right pf_val => case pf_val of
                                                                            (ConvertedFrom (Left bv)) => Left (EPredWrong {pf=IsBool {pf=ConvertedFrom bv}})
                                                                            (ConvertedFrom (Right Zero)) => absurd (pf_normal _ EPredZero)
                                                                            (ConvertedFrom (Right (Succ nv))) => absurd (pf_normal _ (EPredSucc {pf=ConvertedFrom nv}))
normal_is_fully_evaluated {t=IsZero t'} pf_normal = case normal_is_fully_evaluated $ is_zero_subterm_of_normal_is_normal pf_normal of
                                                         Left pf_stuck => Left (EIsZeroWrong {pf=IsStuckTerm {pf=pf_stuck}})
                                                         Right pf_val => case pf_val of
                                                                              (ConvertedFrom (Left bv)) => Left (EIsZeroWrong {pf=IsBool {pf=ConvertedFrom bv}})
                                                                              (ConvertedFrom (Right Zero)) => absurd (pf_normal _ EIsZeroZero)
                                                                              (ConvertedFrom (Right (Succ nv))) => absurd (pf_normal _ (EIsZeroSucc {pf=ConvertedFrom nv}))

--------------------------------------------------------------------------------
-- Definition of the evaluation function.
--------------------------------------------------------------------------------

eval_reduces_size_lemma1 : {n,m : Nat} ->
                           LTE (S n) (S ((n + m) + 1))
eval_reduces_size_lemma1 {n = Z} = LTESucc LTEZero
eval_reduces_size_lemma1 {n = (S k)} = LTESucc (eval_reduces_size_lemma1 {n=k})

eval_reduces_size_lemma2 : {n,m : Nat} ->
                           LTE (S m) (S ((n + m) + 1))
eval_reduces_size_lemma2 {n} {m} = rewrite plusCommutative n m in
                                           eval_reduces_size_lemma1

eval_reduces_size_lemma3 : {n,m,l : Nat} ->
                           LTE n m ->
                           LTE (l+n) (l+m)
eval_reduces_size_lemma3 {l = Z} pf = pf
eval_reduces_size_lemma3 {l = (S k)} pf = LTESucc (eval_reduces_size_lemma3 pf)

eval_reduces_size_lemma3' : {n,m,l : Nat} ->
                            LTE n m ->
                            LTE (n+l) (m+l)
eval_reduces_size_lemma3' {n} {m} {l} pf = rewrite plusCommutative n l in
                                                   rewrite plusCommutative m l in
                                                           eval_reduces_size_lemma3 pf

data ElementaryMonotoneFunction : (Nat -> Nat) -> Type where
  IsConstant : {c : Nat} -> ElementaryMonotoneFunction (const c)
  IsIdentity : ElementaryMonotoneFunction (\n => n) --TODO: Figure out why using `id {a=Nat}` fails to type check
  IsSum : {f,g : Nat -> Nat} ->
          ElementaryMonotoneFunction f ->
          ElementaryMonotoneFunction g ->
          ElementaryMonotoneFunction (\n => (f n) + (g n))

namespace ElementaryStrictlyMonotoneFunction
  data ElementaryStrictlyMonotoneFunction : (Nat -> Nat) -> Type where
    IsIdentity : ElementaryStrictlyMonotoneFunction (\n => n)
    IsSumLeft : {f,g : Nat -> Nat} ->
                ElementaryStrictlyMonotoneFunction f ->
                ElementaryMonotoneFunction g ->
                ElementaryStrictlyMonotoneFunction (\n => (f n) + (g n))
    IsSumRight : {f,g : Nat -> Nat} ->
                 ElementaryMonotoneFunction f ->
                 ElementaryStrictlyMonotoneFunction g ->
                 ElementaryStrictlyMonotoneFunction (\n => (f n) + (g n))

interface Monotone (P : (Nat -> Nat) -> Type) where
  monotone : (x, y : Nat) ->
             {f : Nat -> Nat} ->
             {pf : P f} ->
             LTE x y ->
             LTE (f x) (f y)

interface StrictlyMonotone (P : (Nat -> Nat) -> Type) where
  strictly_monotone : (x, y : Nat) ->
                      {f : Nat -> Nat} ->
                      {pf : P f} ->
                      LT x y ->
                      LT (f x) (f y)

Monotone ElementaryMonotoneFunction where
  monotone x y {f = (const c)} {pf = (IsConstant {c=c})} pf_assum = lteRefl
  monotone x y {f = (\n => n)} {pf = IsIdentity} pf_assum = pf_assum
  monotone x y {f = (\n => ((f n) + (g n)))} {pf = (IsSum {f} {g} pf_f pf_g)} pf_assum = let pf_assum_f = monotone x y {f=f} {pf=pf_f} pf_assum
                                                                                pf_assum_g = monotone x y {f=g} {pf=pf_g} pf_assum
                                                                                temp1 = eval_reduces_size_lemma3 {l=f x} pf_assum_g
                                                                                temp2 = eval_reduces_size_lemma3' {l=g y} pf_assum_f in
                                                                                lteTransitive temp1 temp2

StrictlyMonotone ElementaryStrictlyMonotoneFunction where
  strictly_monotone x y {f = (\n => n)} {pf = IsIdentity} pf_assum = pf_assum
  strictly_monotone x y {f = (\n => ((f n) + (g n)))} {pf = (IsSumLeft {f} {g} pf_f pf_g)} pf_assum = let pf_assum_f = strictly_monotone x y {f=f} {pf=pf_f} pf_assum
                                                                                pf_assum' = lteTransitive (lteSuccRight lteRefl) pf_assum
                                                                                pf_assum_g = monotone x y {f=g} {pf=pf_g} pf_assum'
                                                                                temp1 = eval_reduces_size_lemma3 {l=f y} pf_assum_g
                                                                                temp2 = eval_reduces_size_lemma3' {l=g x} pf_assum_f in
                                                                                lteTransitive temp2 temp1
  strictly_monotone x y {f = (\n => ((f n) + (g n)))} {pf = (IsSumRight {f} {g} pf_f pf_g)} pf_assum = let pf_assum_g = strictly_monotone x y {f=g} {pf=pf_g} pf_assum
                                                                                pf_assum' = lteTransitive (lteSuccRight lteRefl) pf_assum
                                                                                pf_assum_f = monotone x y {f=f} {pf=pf_f} pf_assum'
                                                                                temp1 = eval_reduces_size_lemma3 {l=f x} pf_assum_g
                                                                                temp2 = eval_reduces_size_lemma3' {l=g y} pf_assum_f in
                                                                                rewrite plusSuccRightSucc (f x) (g x) in
                                                                                lteTransitive temp1 temp2

-- Note: We need to define `if_then_else_size_f` explicitly using a lambda expression
-- (instead of pattern matching) because otherwise `pf_if_then_else_size_f` below will
-- fail to type check.
if_then_else_size_f : {n2, n3 : Nat} -> Nat -> Nat
if_then_else_size_f {n2} {n3} = \n => ((n + n2) + n3) + 1

pf_if_then_else_size_f : {n2, n3 : Nat} ->
                         ElementaryStrictlyMonotoneFunction (if_then_else_size_f {n2=n2} {n3=n3})
pf_if_then_else_size_f {n2} {n3} = IsSumLeft (IsSumLeft (IsSumLeft IsIdentity (IsConstant {c=n2})) (IsConstant {c=n3})) (IsConstant {c=1})

succ_size_f : Nat -> Nat
succ_size_f = \n => S n

pf_succ_size_f : ElementaryStrictlyMonotoneFunction Ch04.Eval.succ_size_f
pf_succ_size_f = IsSumRight (IsConstant {c=1}) IsIdentity

pred_size_f : Nat -> Nat
pred_size_f = \n => S n

pf_pred_size_f : ElementaryStrictlyMonotoneFunction Ch04.Eval.pred_size_f
pf_pred_size_f = IsSumRight (IsConstant {c=1}) IsIdentity

is_zero_size_f : Nat -> Nat
is_zero_size_f = \n => S n

pf_is_zero_size_f : ElementaryStrictlyMonotoneFunction Ch04.Eval.is_zero_size_f
pf_is_zero_size_f = IsSumRight (IsConstant {c=1}) IsIdentity

||| Proof that evaluation reduces size.
eval_reduces_size : {t,t' : Term} -> EvalsTo t t' -> LT (size t') (size t)
eval_reduces_size {t = (IfThenElse True t2 t3)} {t' = t2} EIfTrue = eval_reduces_size_lemma1
eval_reduces_size {t = (IfThenElse False t2 t3)} {t' = t3} EIfFalse = eval_reduces_size_lemma2
eval_reduces_size {t = (IfThenElse t1 t2 t3)} {t' = (IfThenElse t1' t2 t3)} (EIf x) = let pf = eval_reduces_size x in
                                                                                strictly_monotone (size t1') (size t1) {pf=pf_if_then_else_size_f} pf
eval_reduces_size {t = (Succ t1)} {t' = (Succ t2)} (ESucc x) = let pf = eval_reduces_size x in
                                                                   strictly_monotone (size t2) (size t1) {pf=pf_succ_size_f} pf
eval_reduces_size {t = (Pred Zero)} {t' = Zero} EPredZero = lteRefl
eval_reduces_size {t = (Pred (Succ t'))} {t' = t'} EPredSucc = LTESucc (lteSuccRight lteRefl)
eval_reduces_size {t = (Pred t1)} {t' = (Pred t2)} (EPred x) = let pf = eval_reduces_size x in
                                                                   strictly_monotone (size t2) (size t1) {pf=pf_pred_size_f} pf
eval_reduces_size {t = (IsZero Zero)} {t' = True} EIsZeroZero = lteRefl
eval_reduces_size {t = (IsZero (Succ nv1))} {t' = False} EIsZeroSucc = LTESucc (LTESucc LTEZero)
eval_reduces_size {t = (IsZero t1)} {t' = (IsZero t2)} (EIsZero x) = let pf = eval_reduces_size x in
                                                                         strictly_monotone (size t2) (size t1) {pf=pf_is_zero_size_f} pf

||| Proof that a term is either normal or evaluates to something. Note that this would be
||| a triviality if we were to assume the law of the excluded middle.
either_normal_or_evals : (t : Term) -> Either (Normal t) (t' : Term ** EvalsTo t t')
either_normal_or_evals True = Left true_is_normal
either_normal_or_evals False = Left false_is_normal
either_normal_or_evals (IfThenElse t1 t2 t3) = case either_normal_or_evals t1 of
                                                    Left pf_normal => case normal_is_fully_evaluated pf_normal of
                                                                           Left pf_stuck => Left (fully_evaluated_is_normal $
                                                                                Left (EIfWrong {pf=IsStuckTerm {pf=pf_stuck}}))
                                                                           Right pf_val => case pf_val of
                                                                                (ConvertedFrom (Left True)) => Right (t2 ** EIfTrue)
                                                                                (ConvertedFrom (Left False)) => Right (t3 ** EIfFalse)
                                                                                (ConvertedFrom (Right nv)) => Left (fully_evaluated_is_normal $
                                                                                Left (EIfWrong {pf=IsNat {pf=ConvertedFrom nv}}))
                                                    Right (t1' ** r) => Right ((IfThenElse t1' t2 t3) ** EIf r)
either_normal_or_evals Zero = Left zero_is_normal
either_normal_or_evals (Succ t) = case either_normal_or_evals t of
                                       Left pf_normal => Left (fully_evaluated_is_normal $
                                                        succ_of_fully_evaluated_is_fully_evaluated $
                                                        normal_is_fully_evaluated pf_normal)
                                       Right (t' ** r) => Right ((Succ t') ** (ESucc r))
either_normal_or_evals (Pred t) = case either_normal_or_evals t of
                                       Left pf_normal => case normal_is_fully_evaluated pf_normal of
                                                              Left pf_stuck => Left (fully_evaluated_is_normal $
                                                                              Left (EPredWrong {pf=IsStuckTerm {pf=pf_stuck}}))
                                                              Right pf_val => case pf_val of
                                                                                (ConvertedFrom (Left bv)) => Left (fully_evaluated_is_normal $
                                                                                Left (EPredWrong {pf=IsBool {pf=ConvertedFrom bv}}))
                                                                                (ConvertedFrom (Right Zero)) => Right (Zero ** EPredZero)
                                                                                (ConvertedFrom (Right (Succ nv))) => Right ((nv2t nv) ** EPredSucc {pf=ConvertedFrom nv})
                                       Right (t' ** r) => Right (_ ** (EPred r))
either_normal_or_evals (IsZero t) = case either_normal_or_evals t of
                                         Left pf_normal => case normal_is_fully_evaluated pf_normal of
                                                                Left pf_stuck => Left (fully_evaluated_is_normal $
                                                                                Left (EIsZeroWrong {pf=IsStuckTerm {pf=pf_stuck}}))
                                                                Right pf_val => case pf_val of
                                                                                (ConvertedFrom (Left bv)) => Left (fully_evaluated_is_normal $
                                                                                Left (EIsZeroWrong {pf=IsBool {pf=ConvertedFrom bv}}))
                                                                                (ConvertedFrom (Right Zero)) => Right (True ** EIsZeroZero)
                                                                                (ConvertedFrom (Right (Succ nv))) => Right (False ** EIsZeroSucc {pf=ConvertedFrom nv})
                                         Right (t' ** r) => Right (_ ** (EIsZero r))

||| Given a term, returns its value.
smallStep_eval : (t : Term) -> (v : Term ** (EvalsToStar t v, FullyEvaluated v))
smallStep_eval t = (inductive_construction size' f) (t ** Refl) where
  a : Type
  a = (t' : Term ** EvalsToStar t t')

  b : Type
  b = (t' : Term ** (EvalsToStar t t', FullyEvaluated t'))

  size' : a -> Nat
  size' (t' ** _) = size t'

  f : (x : a) -> Either b (x' : a ** LT (size' x') (size' x))
  f (t' ** p) = case either_normal_or_evals t' of
                     Left pf_normal => Left (t' ** (p, normal_is_fully_evaluated pf_normal))
                     Right (t'' ** p') => Right ((t'' ** (snoc p p')) ** eval_reduces_size p')

max_stars_repo_name: mr-infty/tapl

max_issues_repo_name: mr-infty/tapl

max_forks_repo_name: mr-infty/tapl


text:
module Main

import System

countdown : (secs : Nat) -> IO ()
countdown Z = putStrLn "Lift Off!"
countdown t@(S s) = do
  putStrLn (show t)
  usleep 1000000
  countdown s

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module IdrisScript.Date.Types

import IdrisScript.Date.Months
import IdrisScript.Date.Days

%access public export

record Year where
  constructor MkYear
  unYear : Int

implementation Eq Year where
  year == year' = unYear year == unYear year'

record Date where
  constructor MkDate
  unDate : Int

implementation Eq Date where
  date == date' = unDate date == unDate date'

record Hours where
  constructor MkHours
  unHours : Int

implementation Eq Hours where
  hours == hours' = unHours hours == unHours hours'

record Minutes where
  constructor MkMinutes
  unMinutes : Int

implementation Eq Minutes where
  mins == mins' = unMinutes mins == unMinutes mins'

record Seconds where
  constructor MkSeconds
  unSeconds : Int

implementation Eq Seconds where
  secs == secs' = unSeconds secs == unSeconds secs'

record Milliseconds where
  constructor MkMilliseconds
  unMilliseconds : Int

implementation Eq Milliseconds where
  millis == millis' = unMilliseconds millis == unMilliseconds millis'

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module xquant.Graph.Marked

-- import Pruviloj
import xquant.Math.Set

%default total

||| Marks are used to signify sets of sites that are either
||| occupied (X) or not (O)
data Mark = X | O

||| Increment a Nat if X, do nothing if O.
||| Used to count total number of marks that are X.
mS : Mark -> Nat -> Nat
mS X = S
mS O = id

||| Representation of a set of sites
||| @ n total number of sites
||| @ k numer that are occupied with X
data Marks : (n : Nat) -> (k : Nat) -> Type where
  Nil  : Marks Z Z
  (::) : (m : Mark) -> Marks n k -> Marks (S n) (mS m k)

empty_ : (n : Nat) -> Marks n Z
empty_ Z     = []
empty_ (S k) = O :: empty_ k

empty : {n : Nat} -> Marks n Z
empty = empty_ _

insertMk : Fin n -> (y : Mark) -> Marks n j -> Marks (S n) (mS y j)
insertMk FZ     y m        = y :: m
insertMk (FS i) X (X :: m) = X :: insertMk i X m
insertMk (FS i) O (X :: m) = X :: insertMk i O m
insertMk (FS i) X (O :: m) = O :: insertMk i X m
insertMk (FS i) O (O :: m) = O :: insertMk i O m

--countMZero : (n : Nat) -> Set [empty_ n]

data Compat : Marks n k -> Marks n j -> Type where
  ComZero : Compat [] []
  ComOO   : Compat q w -> Compat (O :: q) (O :: w)
  ComXO   : Compat q w -> Compat (X :: q) (O :: w)
  ComOX   : Compat q w -> Compat (O :: q) (X :: w)

pL : {x : Marks n k} -> {y : Marks n j} -> Compat x y -> Marks n k
pL {x} c = x

pR : {x : Marks n k} -> {y : Marks n j} -> Compat x y -> Marks n j
pR {y} c = y

||| Add two compatible marked sets together
markAdd : {q : Marks n m} -> {w : Marks n j} -> Compat q w -> Marks n (m + j)
markAdd ComZero    = []
markAdd (ComOO c)  = O :: (markAdd c)
markAdd (ComOX c) ?= X :: (markAdd c)
markAdd (ComXO c)  = X :: (markAdd c)

markAdd_lemma_1 = proof
  intros
  rewrite plusSuccRightSucc m j
  trivial

{-
markLem : Elab ()
markLem = do ns <- intros
             rewriteWith `(plusSuccRightSucc ~(Var m1) ~(Var j))
             hypothesis

mlem = %runElab markLem
-}

Marks_ : Nat -> Type
Marks_ n = (m ** Marks n m)

shift : LTE n m -> LTE n (S m)
shift LTEZero     = LTEZero
shift (LTESucc l) = LTESucc (shift l)

markBound : Marks n m -> LTE m n
markBound [] = LTEZero
markBound (X :: q) with (markBound q)
  | w = LTESucc w
markBound (O :: q) with (markBound q)
  | LTEZero   = LTEZero
  | LTESucc x = LTESucc $ shift x

XXnotCompat : Compat (X :: ys) (X :: zs) -> Void
XXnotCompat ComZero impossible

XOunfold : Compat (X :: ys) (O :: zs) -> Compat ys zs
XOunfold (ComXO c) = c

OXunfold : Compat (O :: ys) (X :: zs) -> Compat ys zs
OXunfold (ComOX c) = c

OOunfold : Compat (O :: ys) (O :: zs) -> Compat ys zs
OOunfold (ComOO c) = c

antiCom : Not (Compat xs ys) -> Not $ Compat (q::xs) (w::ys)
antiCom contra ComZero impossible

decer : (m1 : Marks n i) -> (m2 : Marks n j) -> Dec (Compat m1 m2)
decer []        []        = Yes ComZero
decer (X :: ys) (X :: zs) = No  XXnotCompat
decer (X :: ys) (O :: zs) with (decer ys zs)
  decer (X :: ys) (O :: zs) | Yes prf = Yes $ ComXO prf
  decer (X :: ys) (O :: zs) | No contra = No $ antiCom contra
decer (O :: ys) (X :: zs) with (decer ys zs)
  decer (O :: ys) (X :: zs) | Yes prf = Yes $ ComOX prf
  decer (O :: ys) (X :: zs) | No contra = No $ antiCom contra
decer (O :: ys) (O :: zs) with (decer ys zs)
  decer (O :: ys) (O :: zs) | Yes prf = Yes $ ComOO prf
  decer (O :: ys) (O :: zs) | No contra = No $ antiCom contra

partial
add' : (m1 : Marks n i) -> (m2 : Marks n j) -> Compat m1 m2
add' m1 m2 with (decer m1 m2)
  | Yes c = c

data Compatible : List (Marks_ n) -> Marks_ n -> Type where
  OneCom : (m : Marks_ n) -> Compatible [m] m
  NextCom : (m : Marks_ n)
         -> Compatible l m0
         -> {c : Compat (getProof m) (getProof m0)}
         -> Compatible (m::l) (_ ** markAdd c)

data CompatSet : Nat -> Type where
  CompSet : {m : Marks_ n} -> (Compatible l m) -> CompatSet n

mkComp : Marks n j -> CompatSet n
mkComp m = CompSet $ OneCom (_ ** m)

partial comp' : (x : Marks_ n) -> Compatible l m -> (j ** Compatible (x::l) j)
comp' {m} x allc with (decer (getProof x) (getProof m))
  | Yes c = (_ ** NextCom {c} x allc)

partial comp : (x : Marks_ n) -> CompatSet n -> CompatSet n
comp x (CompSet c) = CompSet $ getProof $ comp' x c

||| A partition of a set of sites into subsets
data Partition : (x : Marks n m) -> Type where
  POne  : (y : Marks n m) -> Partition y
  PNext : (y : Marks n m) -> (c : Compat y z) -> Partition z -> Partition (markAdd c)

||| A complete partition of a set of sites into subsets
data PartitionOfUnity : Nat -> Type where
  PUnity : {m : Marks n n} -> (p : Partition m) -> PartitionOfUnity n

||| A partition of a set of sites into subsets of a particular size
||| @ i the size of the subsets
||| @ x which sites are included in the partition
data PartitionBy : (i : Nat) -> (x : Marks n m) -> Type where
  PBZero : PartitionBy i (empty_ n)
  PBNext : {y : Marks n i} -> (c : Compat y z) -> PartitionBy i z -> PartitionBy i (markAdd c)

||| A complete partition of a set of sites into subsets of a fixed size
||| @ i the size of the subsets
||| @ n the size of the partitioned set
data PartitionOfUnityBy : (i : Nat) -> (n : Nat) -> Type where
  PUnityBy : {x : Marks n n} -> (p : PartitionBy i x) -> PartitionOfUnityBy i n

||| The dual of a marked set, status of every site switched
dual : Marks n m -> Marks n (n `minus` m)
dual []      = []
dual (X :: q)  = O :: dual q
dual (O :: q) ?= X :: dual q

test1 : Partition [X,O]
test1 = POne [X,O]

test2 : Partition [X,X]
test2 = PNext [O,X] (ComOX (ComXO ComZero)) test1

---------- Proofs ----------

minusSuccLeft : (n,m : Nat) -> LTE m n -> (S n) `minus` m = S (n `minus` m)
minusSuccLeft n     Z     LTEZero = ?minusSuccLeft_rhs_1
minusSuccLeft (S n) (S m) (LTESucc l) with (minusSuccLeft n m l)
  | eqn = ?minusSuccLeft_rhs_2

minusSuccLeft_rhs_1 = proof
  intros
  rewrite sym $ minusZeroRight n
  trivial

minusSuccLeft_rhs_2 = proof
  intros
  trivial

dual_lemma_1 = proof
  intros
  let prf = markBound q
  let msl = minusSuccLeft n k prf
  rewrite sym msl
  trivial

max_stars_repo_name: BlackBrane/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module Main

main : IO ()
main = do
  putStr "Enter your name: "
  x <- getLine
  putStrLn("Hello " ++ x ++ "!")


text:
module Utils.Num

import Data.Vect

alphabets : Vect 36 Char
alphabets = fromList $ unpack "0123456789abcdefghijklmnopqrstuvwxyz"

-- Use integer for performance reason
export
stringToNat' : Fin 36 -> String -> Maybe Integer
stringToNat' base str = if str == "" then Nothing else go (finToInteger base) 1 0 $ reverse $ unpack str
  where
    go : Integer -> Integer -> Integer -> List Char -> Maybe Integer
    go base' yoyo acc [] = Just acc
    go base' yoyo acc (chr :: xs) = do
      i <- elemIndex chr alphabets
      if i < base then go base' (base' * yoyo) (acc + finToInteger i * yoyo) xs else Nothing

export
stringToNat : Fin 36 -> String -> Maybe Nat
stringToNat base string = integerToNat <$> stringToNat' base string

export
stringToInteger : Fin 36 -> String -> Maybe Integer
stringToInteger base str =
  case strUncons str of
    Just ('-', num) => negate <$> stringToNat' base num
    Just ('+', num) => stringToNat' base num
    _ => stringToNat' base str


text:
module xquant.Core.NonZero

import Data.Vect

%default total

data NonZero : Nat -> Type where
  NZ : {k : Nat} -> NonZero (S k)

||| works but takes a while when N > ~1000
partial nonzero : (n : Nat) -> NonZero n
nonzero (S k) = NZ

NonZ : Type
NonZ = (n : Nat ** NonZero n)

||| Vector of Non-zero naturals
data NVect : (v : Vect n Nat) -> Type where
  Nil  : NVect []
  (::) : (n : Nat) -> NVect v -> {auto nz : NonZero n} -> NVect (n :: v)

partial
vtov : (v : Vect n Nat) -> NVect v
vtov [] = []
vtov ((S k)::ns) = S k :: (vtov ns)

max_stars_repo_name: fieldstrength/xquant


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

import Data.AVL.Dict

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

%access private
%default total

-- Rewrite with views

-- ----------------------------------------------------------- [ Double Squash ]
scanSquash2 : (a -> a -> Maybe a) -> List a -> List a
scanSquash2 _     Nil          = Nil
scanSquash2 squaFunc (x::xs) with (xs)
    | (y::ys) = case squaFunc x y of
                  Just yes => yes :: scanSquash2 squaFunc ys
                  Nothing  => x :: scanSquash2 squaFunc xs
    | Nil = x :: xs

partial
doSquash2 : (a -> a -> Maybe a) -> Nat -> List a -> List a
doSquash2 squaFunc oldLen bs =
  case scanSquash2 squaFunc bs of
    xs => if length xs == oldLen
             then xs
             else doSquash2 squaFunc (length xs) xs

export
squash2By : (a -> a -> Maybe a) -> List a -> List a
squash2By squaFunc xs = assert_total $ doSquash2 squaFunc (length xs) xs

squashEddaPair : Edda ty -> Edda ty -> Maybe (Edda ty)
squashEddaPair HRule     HRule     = Just $ HRule
squashEddaPair (Para xs) (Para ys) = Just $ Para (xs ++ ys)
squashEddaPair Empty     Empty     = Just $ Empty
squashEddaPair Space     Space     = Just Space
squashEddaPair Hyphen    Hyphen    = Just EnDash
squashEddaPair _         _         = Nothing

export
squash2 : List (Edda ty) -> List (Edda ty)
squash2 = squash2By (squashEddaPair)

-- --------------------------------------------------- [ Triple Punc Squashing ]

export
squash3By : (a -> a -> a -> Maybe a) -> List a -> List a
squash3By _        Nil     = Nil
squash3By squaFunc (x::xs) with (xs)
  | (y::z::zs) = case squaFunc x y z of
                  Just yes => yes :: squash3By squaFunc zs
                  Nothing  => x :: squash3By squaFunc xs
  | (y::ys)    = x :: xs
  | Nil        = x :: xs

squashEddaTriples : Edda ty -> Edda ty -> Edda ty -> Maybe (Edda ty)
squashEddaTriples Period Period Period = Just Ellipsis
squashEddaTriples Hyphen Hyphen Hyphen = Just EmDash
squashEddaTriples _      _      _      = Nothing

export
covering
squash3 : List (Edda ty) -> List (Edda ty)
squash3 = squash3By (squashEddaTriples)

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module Labelling

import Control.Monad.State

-- 12.1.4 Exercises
update : (stateType -> stateType) -> State stateType ()
update f = do state <- get
              put $ f state

increase' : Nat -> State Nat ()
increase' inc = update (+inc)

-- *Labelling> runState (increase' 5) 89
-- ((), 94) : ((), Nat)

-- Tree Labelling

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

countEmpty : Tree a -> State Nat ()
countEmpty Empty = do update (+ 1)
countEmpty (Node l v r) = do countEmpty l
                             countEmpty r

countEmptyNode : Tree a -> State (Nat, Nat) ()
countEmptyNode Empty = do update (\p => (fst p, snd p + 1))
countEmptyNode (Node l v r) = do update (\p => (fst p + 1, snd p))
                                 countEmptyNode l
                                 countEmptyNode r

 -- *Labelling> execState (countEmpty testTree) 0
 -- 7 : Nat

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 : Stream labelType ->
                Tree a ->
                (Stream labelType, Tree (labelType, a))
treeLabelWith lbls Empty = (lbls, Empty)
treeLabelWith lbls (Node left val right)
    = let (this :: lblsLeft, left_labelled) = treeLabelWith lbls left
          (lblsRight, right_labelled)       = treeLabelWith lblsLeft right
      in
          (lblsRight, Node left_labelled (this, val) right_labelled)

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

increase : Nat -> State Nat ()
increase inc = do current <- get
                  put (current + inc)

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