text:
||| Lambductive core calculus
module Lambductive.Core

%default total

data Context : Type

data TypeTerm : Context -> Type

infixl 7 :::

||| De Bruijn variable context
data Context : Type where
  Nil : Context
  ||| Add a variable to a context
  ||| @type The type of the variable
  (:::) : (context : Context) -> (type : TypeTerm context) -> Context

||| Judgment of whether the interpretation of a term as a type code is reducible
data InterpretReducibility : Type where
  InterpretReducible : InterpretReducibility
  InterpretIrreducible : InterpretReducibility

data ValueTerm : (context : Context) -> TypeTerm context -> InterpretReducibility -> Type

||| Types of the calculus
data TypeTerm : Context -> Type where
  ||| A universe of type codes
  U : (level : Nat) -> TypeTerm context
  ||| Dependent function type
  Pi : (domain : TypeTerm context) -> (codomain : TypeTerm (context ::: domain)) -> TypeTerm context
  ||| An irreducible application of the type code interpretation operator
  |||
  ||| Use the `interpret` function to interpret type codes without any concern for reducibility
  IrreducibleInterpret : ValueTerm context (U level) InterpretIrreducible -> TypeTerm context

||| Bring a type into a context with an extra variable at the head
addVarToType : TypeTerm context -> TypeTerm (context ::: type)

||| An index into a context
||| @type The type of the variable at that index
data ContextIndex : (context : Context) -> (type : TypeTerm context) -> Type where
  Z : ContextIndex (_ ::: type) (addVarToType type)
  S : ContextIndex context type -> ContextIndex (context ::: type') (addVarToType type)

||| Interpret a type code to a type
interpret : ValueTerm context (U _) _ -> TypeTerm context

||| Values of the calculus
data ValueTerm : (context : Context) -> TypeTerm context -> InterpretReducibility -> Type where
  Var : ContextIndex context type -> ValueTerm context type InterpretIrreducible

interpret (Var idx) = IrreducibleInterpret (Var idx)

||| An offset into a context
data ContextOffset : Context -> Type where
  OffZ : ContextOffset context
  OffS : ContextOffset context -> ContextOffset (context ::: type)

||| Drop some variables from a context
drop : (context : Context) -> ContextOffset context -> Context
drop context OffZ = context
drop (context ::: _) (OffS off) = drop context off

||| Insert a variable into a context at a given offset
||| @type The type of the variable
insertAt : (context : Context) -> (off : ContextOffset context) -> (type : TypeTerm (drop context off)) -> Context

||| Bring a type into a context with an extra variable at a given offset
addVarToTypeAtOffset : (off : ContextOffset context) -> TypeTerm context -> TypeTerm (insertAt context off type)

insertAt context OffZ type = context ::: type
insertAt (context ::: type) (OffS off) type' = insertAt context off type' ::: addVarToTypeAtOffset off type

||| Bring a type code into a context with an extra variable at a given offset
addVarToCodeAtOffset : (off : ContextOffset context) -> ValueTerm context (U level) interpretReducible -> ValueTerm (insertAt context off type') (U level) interpretReducible

addVarToTypeAtOffset _ (U level) = U level
addVarToTypeAtOffset off (Pi domain codomain) = Pi (addVarToTypeAtOffset off domain) (addVarToTypeAtOffset (OffS off) codomain)
addVarToTypeAtOffset off (IrreducibleInterpret code) = IrreducibleInterpret (addVarToCodeAtOffset off code)

addVarToType type = addVarToTypeAtOffset OffZ type

||| Bring a value into a context with an extra variable at a given offset
addVarToValueAtOffset : (off : ContextOffset context) -> ValueTerm context type interpretReducible -> ValueTerm (insertAt context off type') (addVarToTypeAtOffset off type) interpretReducible
addVarToValueAtOffset OffZ (Var idx) = Var (S idx)
addVarToValueAtOffset (OffS off) (Var idx) = ?hole

addVarToCodeAtOffset off code = addVarToValueAtOffset off code

max_stars_repo_name: shlevy/lambductive

max_issues_repo_name: shlevy/lambductive

max_forks_repo_name: shlevy/lambductive


text:
module TTImp.WithClause

import Core.Context
import Core.Context.Log
import Core.TT
import TTImp.BindImplicits
import TTImp.TTImp

import Data.List

%default covering

matchFail : FC -> Core a
matchFail loc = throw (GenericMsg loc "With clause does not match parent")

mutual
  export
  getMatch : (lhs : Bool) -> RawImp -> RawImp ->
             Core (List (String, RawImp))
  getMatch lhs (IBindVar _ n) tm = pure [(n, tm)]
  getMatch lhs (Implicit _ _) tm = pure []

  getMatch lhs (IVar _ (NS ns n)) (IVar loc (NS ns' n'))
      = if n == n' && isParentOf ns' ns then pure [] else matchFail loc
  getMatch lhs (IVar _ (NS ns n)) (IVar loc n')
      = if n == n' then pure [] else matchFail loc
  getMatch lhs (IVar _ n) (IVar loc n')
      = if n == n' then pure [] else matchFail loc
  getMatch lhs (IPi _ c p n arg ret) (IPi loc c' p' n' arg' ret')
      = if c == c' && samePiInfo p p' && n == n'
           then matchAll lhs [(arg, arg'), (ret, ret')]
           else matchFail loc
    where
      samePiInfo : PiInfo RawImp -> PiInfo RawImp -> Bool
      samePiInfo Explicit Explicit = True
      samePiInfo Implicit Implicit = True
      samePiInfo AutoImplicit AutoImplicit = True
      samePiInfo (DefImplicit _) (DefImplicit _) = True
      samePiInfo _ _ = False
  -- TODO: Lam, Let, Case, Local, Update
  getMatch lhs (IApp _ f a) (IApp loc f' a')
      = matchAll lhs [(f, f'), (a, a')]
  getMatch lhs (IImplicitApp _ f n a) (IImplicitApp loc f' n' a')
      = if n == n'
           then matchAll lhs [(f, f'), (a, a')]
           else matchFail loc
  getMatch lhs (IWithApp _ f a) (IWithApp loc f' a')
      = matchAll lhs [(f, f'), (a, a')]
  -- On LHS: If there's an implicit in the parent, but not the clause, add the
  -- implicit to the clause. This will propagate the implicit through to the
  -- body
  getMatch True (IImplicitApp fc f n a) f'
      = matchAll True [(f, f'), (a, a)]
  -- On RHS: Rely on unification to fill in the implicit
  getMatch False (IImplicitApp fc f n a) f'
      = getMatch False f f
  -- Can't have an implicit in the clause if there wasn't a matching
  -- implicit in the parent
  getMatch lhs f (IImplicitApp fc f' n a)
      = matchFail fc
  -- Alternatives are okay as long as the alternatives correspond, and
  -- one of them is okay
  getMatch lhs (IAlternative fc _ as) (IAlternative _ _ as')
      = matchAny fc lhs (zip as as')
  getMatch lhs (IAs _ _ (UN n) p) (IAs fc _ (UN n') p')
      = do ms <- getMatch lhs p p'
           mergeMatches lhs ((n, IBindVar fc n') :: ms)
  getMatch lhs (IAs _ _ (UN n) p) p'
      = do ms <- getMatch lhs p p'
           mergeMatches lhs ((n, p') :: ms)
  getMatch lhs (IAs _ _ _ p) p' = getMatch lhs p p'
  getMatch lhs p (IAs _ _ _ p') = getMatch lhs p p'
  getMatch lhs (IType _) (IType _) = pure []
  getMatch lhs (IPrimVal fc c) (IPrimVal fc' c') =
    if c == c'
    then pure []
    else matchFail fc
  getMatch lhs pat spec = matchFail (getFC pat)

  matchAny : FC -> (lhs : Bool) -> List (RawImp, RawImp) ->
             Core (List (String, RawImp))
  matchAny fc lhs [] = matchFail fc
  matchAny fc lhs ((x, y) :: ms)
      = catch (getMatch lhs x y)
              (\err => matchAny fc lhs ms)

  matchAll : (lhs : Bool) -> List (RawImp, RawImp) ->
             Core (List (String, RawImp))
  matchAll lhs [] = pure []
  matchAll lhs ((x, y) :: ms)
      = do matches <- matchAll lhs ms
           mxy <- getMatch lhs x y
           mergeMatches lhs (mxy ++ matches)

  mergeMatches : (lhs : Bool) -> List (String, RawImp) ->
                 Core (List (String, RawImp))
  mergeMatches lhs [] = pure []
  mergeMatches lhs ((n, tm) :: rest)
      = do rest' <- mergeMatches lhs rest
           case lookup n rest' of
                Nothing => pure ((n, tm) :: rest')
                Just tm' =>
                   do getMatch lhs tm tm' -- just need to know it succeeds
                      mergeMatches lhs rest

-- Get the arguments for the rewritten pattern clause of a with by looking
-- up how the argument names matched
getArgMatch : FC -> Bool -> RawImp -> List (String, RawImp) ->
              Maybe (PiInfo RawImp, Name) -> RawImp
getArgMatch ploc search warg ms Nothing = warg
getArgMatch ploc True warg ms (Just (AutoImplicit, UN n))
    = case lookup n ms of
           Nothing => ISearch ploc 500
           Just tm => tm
getArgMatch ploc True warg ms (Just (AutoImplicit, _))
    = ISearch ploc 500
getArgMatch ploc search warg ms (Just (_, UN n))
    = case lookup n ms of
           Nothing => Implicit ploc True
           Just tm => tm
getArgMatch ploc search warg ms _ = Implicit ploc True

export
getNewLHS : {auto c : Ref Ctxt Defs} ->
            FC -> (drop : Nat) -> NestedNames vars ->
            Name -> List (Maybe (PiInfo RawImp, Name)) ->
            RawImp -> RawImp -> Core RawImp
getNewLHS ploc drop nest wname wargnames lhs_raw patlhs
    = do (mlhs_raw, wrest) <- dropWithArgs drop patlhs
         autoimp <- isUnboundImplicits
         setUnboundImplicits True
         (_, lhs) <- bindNames False lhs_raw
         (_, mlhs) <- bindNames False mlhs_raw
         setUnboundImplicits autoimp

         let (warg :: rest) = reverse wrest
             | _ => throw (GenericMsg ploc "Badly formed 'with' clause")
         log "with" 5 $ show lhs ++ " against " ++ show mlhs ++
                 " dropping " ++ show (warg :: rest)
         ms <- getMatch True lhs mlhs
         log "with" 5 $ "Matches: " ++ show ms
         let newlhs = apply (IVar ploc wname)
                            (map (getArgMatch ploc False warg ms) wargnames ++ rest)
         log "with" 5 $ "New LHS: " ++ show newlhs
         pure newlhs
  where
    dropWithArgs : Nat -> RawImp ->
                   Core (RawImp, List RawImp)
    dropWithArgs Z tm = pure (tm, [])
    dropWithArgs (S k) (IApp _ f arg)
        = do (tm, rest) <- dropWithArgs k f
             pure (tm, arg :: rest)
    -- Shouldn't happen if parsed correctly, but there's no guarantee that
    -- inputs come from parsed source so throw an error.
    dropWithArgs _ _ = throw (GenericMsg ploc "Badly formed 'with' clause")

-- Find a 'with' application on the RHS and update it
export
withRHS : {auto c : Ref Ctxt Defs} ->
          FC -> (drop : Nat) -> Name -> List (Maybe (PiInfo RawImp, Name)) ->
          RawImp -> RawImp ->
          Core RawImp
withRHS fc drop wname wargnames tm toplhs
    = wrhs tm
  where
    withApply : FC -> RawImp -> List RawImp -> RawImp
    withApply fc f [] = f
    withApply fc f (a :: as) = withApply fc (IWithApp fc f a) as

    updateWith : FC -> RawImp -> List RawImp -> Core RawImp
    updateWith fc (IWithApp _ f a) ws = updateWith fc f (a :: ws)
    updateWith fc tm []
        = throw (GenericMsg fc "Badly formed 'with' application")
    updateWith fc tm (arg :: args)
        = do log "with" 10 $ "With-app: Matching " ++ show toplhs ++ " against " ++ show tm
             ms <- getMatch False toplhs tm
             log "with" 10 $ "Result: " ++ show ms
             let newrhs = apply (IVar fc wname)
                                (map (getArgMatch fc True arg ms) wargnames)
             log "with" 10 $ "With args for RHS: " ++ show wargnames
             log "with" 10 $ "New RHS: " ++ show newrhs
             pure (withApply fc newrhs args)

    mutual
      wrhs : RawImp -> Core RawImp
      wrhs (IPi fc c p n ty sc)
          = pure $ IPi fc c p n !(wrhs ty) !(wrhs sc)
      wrhs (ILam fc c p n ty sc)
          = pure $ ILam fc c p n !(wrhs ty) !(wrhs sc)
      wrhs (ILet fc c n ty val sc)
          = pure $ ILet fc c n !(wrhs ty) !(wrhs val) !(wrhs sc)
      wrhs (ICase fc sc ty clauses)
          = pure $ ICase fc !(wrhs sc) !(wrhs ty) !(traverse wrhsC clauses)
      wrhs (ILocal fc decls sc)
          = pure $ ILocal fc decls !(wrhs sc) -- TODO!
      wrhs (IUpdate fc upds tm)
          = pure $ IUpdate fc upds !(wrhs tm) -- TODO!
      wrhs (IApp fc f a)
          = pure $ IApp fc !(wrhs f) !(wrhs a)
      wrhs (IImplicitApp fc f n a)
          = pure $ IImplicitApp fc !(wrhs f) n !(wrhs a)
      wrhs (IWithApp fc f a) = updateWith fc f [a]
      wrhs (IRewrite fc rule tm) = pure $ IRewrite fc !(wrhs rule) !(wrhs tm)
      wrhs (IDelayed fc r tm) = pure $ IDelayed fc r !(wrhs tm)
      wrhs (IDelay fc tm) = pure $ IDelay fc !(wrhs tm)
      wrhs (IForce fc tm) = pure $ IForce fc !(wrhs tm)
      wrhs tm = pure tm

      wrhsC : ImpClause -> Core ImpClause
      wrhsC (PatClause fc lhs rhs) = pure $ PatClause fc lhs !(wrhs rhs)
      wrhsC c = pure c

ext: idr


text:
module ATM

import Data.Vect

PIN: Type
PIN = Vect 4 Integer

data ATMState = Ready | CardInserted | Session

data HasCard : ATMState -> Type where
  HasCI : HasCard CardInserted
  HasSession : HasCard Session

data PINCheck = CorrectPIN | IncorrectPIN

data ATMCmd : (ty: Type) -> ATMState -> (ty -> ATMState) -> Type where
  InsertCard: ATMCmd () Ready (const CardInserted)
  EjectCard: {auto prf: HasCard state} -> ATMCmd () state (const Ready)
  GetPIN: ATMCmd PIN CardInserted (const CardInserted)
  CheckPIN: PIN -> ATMCmd PINCheck CardInserted (\check => case check of
                                                              CorrectPIN => Session
                                                              IncorrectPIN => CardInserted)

  GetAmount: ATMCmd Nat state (const state)
  Dispense: (amount: Nat) -> ATMCmd () Session (const Session)

  Message: String -> ATMCmd () state (const state)

  Pure: (res: ty) -> ATMCmd ty (state_fn res) state_fn

  (>>=): ATMCmd a state1 state2_fn -> ((res: a) -> ATMCmd b (state2_fn res) state3_fn) -> ATMCmd b state1 state3_fn

insertEject : ATMCmd () Ready (const Ready)
insertEject = do InsertCard
                 EjectCard

-- atm: ATMCmd () Ready (const Ready)
-- atm = do InsertCard
--          pin <- GetPIN
--          pinOK <- CheckPIN pin
--          case pinOK of
--               CorrectPIN => do cash <- GetAmount
--                                Dispense cash
--                                EjectCard
--               IncorrectPIN => EjectCard

-- runATM: ATMCmd res inState outState_fn -> IO res
-- runATM InsertCard = do putStrLn "Please insert your card"
--                        x <- getLine
--                        pure()
-- runATM EjectCard = putStrLn "Thank you"
-- runATM GetPIN = do putStr "Enter Pin"
--                    pure (the (Vect _ Integer) [1, 2, 3, 4])
-- runATM (CheckPIN pin) = if pin == [1, 2, 3, 4]
--                           then pure CorrectPIN
--                           else pure IncorrectPIN
-- runATM GetAmount = do putStr "How much would you like"
--                       x <- getLine
--                       pure (cast x)
-- runATM (Dispense amount) = putStrLn "Here is the amount"
-- runATM (Message msg) = putStrLn msg
-- runATM (Pure res) = pure res
-- runATM (x >>= f) = do res <- runATM x
--                       runATM (f res)

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module Main

import System

readNumber : IO (Maybe Nat)
readNumber = do
  input <- getLine
  if all isDigit (unpack input)
     then pure (Just (cast input))
     else pure Nothing

guess : (target : Nat) -> (guesses: Nat) -> IO ()
guess target k = do putStrLn ("Number of tries: " ++ show k)
                    putStr "Guess number: "
                    Just input <- readNumber
                        | Nothing => do putStrLn "NaN"
                                        guess target (S k)
                    case compare input target of
                         LT => do putStrLn "Number too small"
                                  guess target (S k)
                         GT => do putStrLn "Number too big"
                                  guess target (S k)
                         EQ => putStrLn "Congrats! That's the number."

generateNrToGuess : IO (Nat)
generateNrToGuess = do timeValue <- time
                       let nrToGuess = mod timeValue 100
                       putStrLn ("Number to guess: " ++ show nrToGuess)
                       pure (fromIntegerNat nrToGuess)

main : IO()
main = do target <- generateNrToGuess
          guess target 0

repl2 : (prompt : String) -> (onInput : String -> String) -> IO ()
repl2 prompt onInput = do putStr prompt
                          input <- getLine
                          putStrLn (onInput input)
                          repl2 prompt onInput

replWith2 : (state : a) -> (prompt : String) ->
    (onInput : a -> String -> Maybe (String, a)) -> IO ()
replWith2 state prompt onInput =
        do putStr prompt
           input <- getLine
           case onInput state input of
                Just (output, newState) => do putStr output
                                              replWith2 newState prompt onInput
                Nothing => pure ()

testRepl2 : IO ()
testRepl2 = repl2 "Put string: " (\x => "Input string was: " ++ show x)

func : Integer -> String -> Maybe (String, Integer)
func sum input = if all isDigit (unpack input)
                    then let result = (cast input) + sum in
                         Just ("Sum: " ++ show result ++ "\n", result)
                    else Nothing

testReplWith : IO ()
testReplWith =
  replWith 0 "Add number: " func

testReplWith2 : IO()
testReplWith2 =
  replWith2 0 "Add number: " func


text:
import Data.Vect

total insert : Ord type => (x : type) -> (xsSorted : Vect len type) -> Vect (S len) type
insert x [] = [x]
insert x (y :: xs) = case x < y of
                          False => y :: insert x xs
                          True => x :: y :: xs

total insSort : Ord type => Vect length type -> Vect length type
insSort [] = []
insSort (x :: xs) = let xsSorted = insSort xs in
                              insert x xsSorted

total len : List a -> Nat
len [] = 0
len (x :: xs) = 1 + len xs

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

total map' : (a -> b) -> List a -> List b
map' f [] = []
map' f (x :: xs) = f x :: map' f xs

total map'' : (a -> b) -> Vect n a -> Vect n b
map'' f [] = []
map'' f (x :: xs) = f x :: map'' f xs

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Render

import Data.String

import VNode
import Attributes

-- Creates an empty node an returns a pointer to it
%foreign "browser:lambda: node => document.createElement(node)"
prim__makeNode : String -> PrimIO AnyPtr

-- Returns undefined
%foreign "browser:lambda: (node, attr, value) => node.setAttribute(attr, value)"
prim__setAttr : AnyPtr -> String -> String -> PrimIO AnyPtr

%foreign "browser:lambda: (parent, child) => parent.appendChild(child)"
prim__addNode : AnyPtr -> AnyPtr -> PrimIO AnyPtr

%foreign "browser:lambda: id => document.getElementById(id)"
prim__getRoot : String -> PrimIO AnyPtr

%foreign "browser:lambda: text => document.createTextNode(text)"
prim__madeText : String -> PrimIO AnyPtr

%foreign "browser:lambda: value => console.log(value)"
prim__consoleLog : AnyPtr -> PrimIO AnyPtr

%foreign "browser:lambda: value => console.log(value)"
prim__consoleString : String -> PrimIO AnyPtr

%foreign "browser:lambda: node => node.innerHTML = ''"
prim__clearNode : AnyPtr -> PrimIO AnyPtr

export
getRoot : String -> IO AnyPtr
getRoot id = primIO $ prim__getRoot id

export
consoleLog : Show a => a -> IO ()
consoleLog x = do
  _ <- primIO $ prim__consoleString (show x)
  pure ()

export
setAttributes : NodeRef -> List Attribute -> IO NodeRef
setAttributes node attrs = do
  _ <- traverse (setAttribute node) attrs
  pure node
  where
    setAttribute : NodeRef -> Attribute -> IO NodeRef
    setAttribute node (Class xs) = primIO $ prim__setAttr node "class" (unwords xs)
    setAttribute node (Accept x) = primIO $ prim__setAttr node "accept" x
    setAttribute node (AcceptCharSet x) = primIO $ prim__setAttr node "accept-charset" x
    setAttribute node (AcessKey x) = primIO $ prim__setAttr node "accesskey" x
    setAttribute node (Action x) = primIO $ prim__setAttr node "action" x
    setAttribute node Async = primIO $ prim__setAttr node "async" ""   -- TODO Fix this
    setAttribute node (Cols x) = primIO $ prim__setAttr node "cols" (show x)
    setAttribute node (Attr x y) = primIO $ prim__setAttr node x y
    setAttribute node (Id x) = primIO $ prim__setAttr node "id" x

makeNode : (Node V tagType) -> IO NodeRef
makeNode (Tag name attrs children) = do
  node <- primIO $ prim__makeNode name
  _ <- setAttributes node attrs
  pure node

makeNode (Void name attrs) = do
  node <- primIO $ prim__makeNode name
  _ <- setAttributes node attrs
  pure node

makeNode (Text text) = primIO $ prim__madeText text

attachNode : (parent : NodeRef) -> (child : NodeRef) -> IO ()
attachNode parent child = do
  _ <- primIO $ prim__addNode parent child
  pure ()

render' : (root : NodeRef) -> (vdom : DOM V) -> IO (DOM L)
render' root (VDOM meta node) = do
  ref <- makeNode node
  _ <-  attachNode root ref
  case node of
    (Tag name attr children) => do
      children <- traverse (render' ref) children
      let liveNode = Tag name attr children
      pure (LiveDOM meta liveNode ref)
    (Text string) => pure (LiveDOM meta (Text string) ref)
    (Void name attr) => pure (LiveDOM meta (Void name attr) ref)

export
render : (root : NodeRef) -> (vdom : DOM V) -> IO (DOM L)
render root vdom = do
  _ <- primIO $ prim__clearNode root
  render' root vdom

max_stars_repo_name: Stinners/alder

max_issues_repo_name: Stinners/alder

max_forks_repo_name: Stinners/alder


text:
module Control.Permutation.Mod

import Prelude.Nat
import Data.List
import Data.Vect
import Control.Permutation.Types
import Data.Vect

%default total

%access public export

mutual
  even : Nat -> Bool
  even Z = True
  even (S k) = odd k

  odd : Nat -> Bool
  odd Z = False
  odd (S k) = even k

private
natToFin : (n : Nat) -> Fin (S n)
natToFin Z = FZ
natToFin (S k) = FS k' where k' = natToFin k

||| This permutation reverses a vector completely
reverse : Permutation n
reverse {n=Z} = []
reverse {n=S _} = last :: reverse

private
finiteL : (n : Nat) -> Vect (S n) (Fin (S n))
finiteL Z = FZ :: Nil
finiteL n@(S m) = natToFin n :: (map weaken $ finiteL m)

factorial : Nat -> Nat
factorial Z = S Z
factorial (S k) = (S k) * factorial k

combine : Vect m (a -> b) -> Vect n a -> Vect (m * n) b
combine {m} {n} fs xs = rewrite multCommutative m n in
                                concat $ map (g fs) xs
  where
    g : Vect m (a -> b) -> a -> Vect m b
    g fs x = fs <*> pure x

||| All permutations of a certain order.
export
enumerateStrict : Vect (factorial n) (Permutation n)
enumerateStrict {n=Z} = Nil :: Nil
enumerateStrict {n=S Z} = ((FZ :: Nil) :: Nil)
enumerateStrict {n=n@(S m)} = combine (map (::) (finiteL m)) enumerateStrict

||| Show where an integer is sent.
||| @p A permutation
||| @m The integer
fixNat : (p : Permutation n) -> (m : Fin n) -> Fin n
fixNat p m = index m $ (toVector p)
  where
    index : Fin l -> Lazy (Vect l e) -> e
    index FZ     (x::xs) = x
    index (FS k) (x::xs) = index k xs

||| Orbit generated by a given element.
||| @p A permutation
||| @i The starting point
orbit : (p : Permutation (S n)) -> (i : Fin (S n)) -> Stream (Fin (S n))
orbit p {n} i = i :: go i where
  go : Fin (S n) -> Stream (Fin (S n))
  go j = next :: go next where
    next : Fin (S n)
    next = fixNat p j

||| Return the orbit of some permutation.
finOrbit : Permutation (S n) -> Fin (S n) -> List (Fin (S n))
finOrbit p {n} i = nub $ take (S n) (orbit p i)

||| Return a list of disjoint cycles given a permutation. We use this for our
||| pretty-printer.
export
cycles : Permutation (S n) -> List (List (Fin (S n)))
cycles p {n} = nubBy g . map (finOrbit p) . enumFromTo 0 $ (natToFin n)
  where
    g : List (Fin (S n)) -> List (Fin (S n)) -> Bool
    g x y = and $ map (Delay . flip elem y) x

export
order : Permutation (S n) -> Nat
order = foldr lcm 1 . map length . cycles

private
checkId : String -> String
checkId "" = "id"
checkId x = x

implementation Show (Permutation (S n)) where
  show {n} p = checkId (concatMap (go n) (cycles p))
    where
      go : (Show a) => Nat -> List a -> String
      go _ l@(_::_::_) = if n <= 9
        then "(" ++ concatMap show l ++ ")"
        else "(" ++ concat ((intersperse "," . map show) l) ++ ")"
      go _ _ = ""

private
fill : Fin n -> Permutation n
fill FZ = neutral
fill (FS k) = FS (zeros k) :: fill k
  where zeros : Fin m -> Fin m
        zeros FZ = FZ
        zeros (FS _) = FZ

||| The permutation π_ij
export
pi : Fin n -> Fin n -> Permutation n
pi (FS j) (FS k) = FZ :: pi j k
pi (FS j) FZ = FS j :: fill j
pi FZ (FS k) = FS k :: fill k
pi FZ FZ = neutral

||| For S_4, (1234)
export
circulate : Permutation n
circulate {n=Z} = Nil
circulate {n=S Z} = FZ :: Nil
circulate {n=S (S m)} = foldl (<+>) neutral pis
  where
    pis : List (Permutation (S (S m)))
    pis = zipWith pi (enumFromTo 0 (weaken $ natToFin m)) (enumFromTo 1 (natToFin (S m)))

||| Factors a permutation into a product of swaps.
export
swaps : Permutation n -> List (Permutation n)
swaps {n=Z} _ = []
swaps {n=n@(S _)} p = go overlaps p
  where
    go : (List (Fin (S n)) -> List (Permutation (S n))) -> Permutation (S n) -> List (Permutation (S n))
    go f p = (>>= f) $ cycles p
    overlaps (x::xs@(y::ys)) = pi x y :: overlaps xs
    overlaps x = []

||| Test whether a permutation is even.
export
isEven : Permutation n -> Bool
isEven = even . length . swaps

max_stars_repo_name: marcosh/permutations

max_issues_repo_name: marcosh/permutations

max_forks_repo_name: marcosh/permutations


text:
import Data.Either
import Data.List
import Data.Maybe
import Data.String

import System.File

data Command = Forward Int | Up Int | Down Int

parseCommand : String -> Maybe Command
parseCommand s = do (c, i) <- pure $ break (== ' ') s
                    i <- parseInteger {a=Int} i
                    case c of
                         "forward" => Just $ Forward $ i
                         "up" => Just $ Up $ i
                         "down" => Just $ Down $ i
                         _ => Nothing

parseLines : (String -> Maybe a) -> String -> List a
parseLines f s = catMaybes $ f <$> lines s

doCommand : (Int, Int, Int) -> Command -> (Int, Int, Int)
doCommand (p, d, a) (Forward x) = (p + x, d + a * x, a)
doCommand (p, d, a) (Up x) = (p, d, a - x)
doCommand (p, d, a) (Down x) = (p, d, a + x)

run : String -> IO ()
run s = do let (p, d, _) = foldl doCommand (0, 0, 0) $ parseLines parseCommand s
           putStrLn $ show $ p * d

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


text:
module Main

import Data.Nat
import Data.Vect
import Data.List
import LinearTypes
import Control.Linear.LIO
import Unitary
import QStateT
import Teleportation
import System.Random
import Injection
import QFT
import Grover
import AlterningBitsOracle
import VQE
import Complex
import QuantumOp
import CoinToss
import QAOA
import Graph
import Examples
import RUS

-- %default total

||| Perform 1000 fair coin tosses and count the number of heads
||| (via simulating the quantum dynamics).
testCoins : IO ()
testCoins = do
  let f = coin {t = SimulatedOp}
  s <- sequence (Data.List.replicate 1000 f)
  let heads = filter (== True) s
  putStrLn $ "Number of heads: " ++ (show (length heads))

||| Call the drawTeleportation function (using the SimulatedOp implementation)
||| then execute the runTeleportation function 1000 times and report on the
||| observed measurement results on the third qubit
||| (which is in state |+> at the end of the teleportation protocol).
export
testTeleport : IO ()
testTeleport = do
  drawTeleportation {t = SimulatedOp}
  l <- sequence (Data.List.replicate 1000 (runTeleportation {t = SimulatedOp}))
  let nbT = length $ filter (\x => (last x) == True) l
  putStrLn "\n\nFor 1000 measurements"
  putStrLn ("Number of True measurements : " ++ show nbT)

||| Test graph for the QAOA problem
export
graph1 : Graph 5
graph1 = AddVertex (AddVertex (AddVertex (AddVertex (AddVertex Empty []) [True]) [True, True]) [False, True, False]) [False, False, True, True]

||| Execute QAOA with 100 samples on the previous graph to solve the MAXCUT problem
export
testQAOA : IO (Cut 5)
testQAOA = do
  QAOA {t = SimulatedOp} 100 1 graph1

||| Small test for the VQE algorithm
export
testVQE : IO Double
testVQE = do
  putStrLn "Test VQE"
  let hamiltonian = [(2, [PauliX, PauliY]),(3,[PauliZ, PauliI])]
  VQE {t = SimulatedOp} 2 hamiltonian 5 10 5

export
main : IO ()
main = do

  -- Execute the example file and draw the circuit examples
  drawExamples

  -- Draw the Quantum Fourier Transform for n = 3
--  putStrLn "\n\n\nQuantum Fourier Transform for n = 3"
--  draw (qft 3)

  -- Execute the coin toss example
  putStrLn "\nTest coin toss by performing 1000 coin tosses."
  testCoins

  -- Teleportation protocol
--  putStrLn "\nTest Teleportation protocol"
--  testTeleport

  -- Repeat until success
  putStrLn "\nTest 'Repeat Until Success'. Probability to measure '1' is 2/3 for this example."
  testMultipleRUS 10000

  -- VQE
--  putStrLn "\nSmall test with VQE"
--  r <- testVQE
--  putStrLn $ "result from VQE : " ++ show r

  -- QAOA
--  putStrLn "\nSmall test with QAOA"
--  cut <- testQAOA
--  putStrLn $ "result from QAOA : " ++ show cut

  pure ()

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module Graphics.Rendering.Gl.Types

%access public export

GLenum : Type
GLenum = Int

GLbitfield : Type
GLbitfield = Int

GLboolean : Type
GLboolean = Int

GLbyte : Type
GLbyte = Char

GLubyte : Type
GLubyte = Char

GLshort : Type
GLshort = Int

GLushort : Type
GLushort = Int

GLint : Type
GLint = Int

GLuint : Type
GLuint = Int

GLsizei : Type
GLsizei = Int

GLchar : Type
GLchar = Char

GLdouble : Type
GLdouble = Double

GLclampd : Type
GLclampd = Double

-- only temporary
GLfloat : Type
GLfloat = Double

GLclampf : Type
GLclampf = Double

-- the pointer size of the data len*sizeof(whatever)
GLsizeiptr : Type
GLsizeiptr = Int

class GlEnum a where
  toGlInt   : a -> Int

max_stars_repo_name: spearman/gl-idris

max_issues_repo_name: spearman/gl-idris

max_forks_repo_name: spearman/gl-idris


text:
module Sub02LTE72t45

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total

-- 6(12t+7)+3 --E[2,-4]--> 6t+3
export
lte72t45 : (l : Nat) -> LTE (S l)
  (S (((S (l+l))+(S (l+l))) + ((S (l+l))+(S (l+l))) + ((S (l+l))+(S (l+l)))))
lte72t45 Z     = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc) LTEZero
lte72t45 (S l) =
  let lemma = lte72t45 l in
  rewrite (sym (plusSuccRightSucc l l)) in

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

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

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


text:
||| A channel built on top of System.Concurrency.Queue. It is MTSafe thanks to
||| Queues being MTSafe, and buffered as it operates using a Queue of things.
module System.Concurrency.BufferedChannel

import public Data.List
import System.Concurrency

import public System.Concurrency.Queue

%default total

||| A channel for inter-process communication where one side is the sender, and
||| the other is the receiver.
||| See also:
||| - @makeBufferedChannel@
||| - @becomeSender@
||| - @becomeReceiver@
export
data BufferedChannel : Type -> Type where
  MkBufferedChannel : (condLock : Mutex)
                    -> (condVar : Condition)
                    -> (qRef    : IORef (Queue a))
                    -> BufferedChannel a

||| Create a new BufferedChannel. Since BufferedChannels are shared resources,
||| they can only be obtained in an IORef.
||| See also
||| - @becomeSender@
||| - @becomeReceiver@
export
makeBufferedChannel : IO (IORef (BufferedChannel a))
makeBufferedChannel =
  do cl <- makeMutex
     cv <- makeCondition
     q  <- makeQueue
     newIORef (MkBufferedChannel cl cv q)

-- Sending --

||| The type of a sender function is something which takes a channel and a thing
||| to send, and produces an empty IO action, i.e. the sending of the thing.
public export
SenderFunc : Type -> Type
SenderFunc a = BufferedChannel a -> a -> IO ()

||| What sending should do to the BufferedChannel's internal Condition Variable:
||| - Signalling wakes 1 thread waiting to receive, if there are any.
||| - Broadcasting wakes all the threads waiting to receive, if there are any.
public export
data SendEffect = Signal
                | Broadcast

||| Send a thing on the BufferedChannel and signal its internal condition
||| variable.
|||
||| MTSafe: YES
sendAndSignal : SenderFunc a
sendAndSignal (MkBufferedChannel _ condVar qRef) thing =
  do enqueue qRef thing
     conditionSignal condVar

||| Send a thing on the BufferedChannel and broadcast its internal condition
||| variable.
|||
||| MTSafe: YES
sendAndBroadcast : SenderFunc a
sendAndBroadcast (MkBufferedChannel _ condVar qRef) thing =
  do enqueue qRef thing
     conditionBroadcast condVar

||| Send a thing on the BC, affecting the internal CV in the specified way.
send : SendEffect -> SenderFunc a
send Signal = sendAndSignal
send Broadcast = sendAndBroadcast

||| The type of a buffer function is something which takes a channel and
||| non-empty list of things to send, and produces an empty IO action, i.e. the
||| sending of the things.
public export
BufferFunc : Type -> Type
BufferFunc a =
  BufferedChannel a -> (items : List a) -> {auto 0 ok : NonEmpty items} -> IO ()

||| Send some things in bulk on the BufferedChannel and signal its internal
||| condition variable.
bufferAndSignal : BufferFunc a
bufferAndSignal (MkBufferedChannel _ condVar qRef) things =
  do ignore $ traverse (\thing => enqueue qRef thing) things
     conditionSignal condVar

||| Send some things in bulk on the BufferedChannel and broadcast its internal
||| condition variable.
bufferAndBroadcast : BufferFunc a
bufferAndBroadcast (MkBufferedChannel _ condVar qRef) things =
  do ignore $ traverse (\thing => enqueue qRef thing) things
     conditionBroadcast condVar

||| Buffer a list of things on the BC, affecting the internal CV in the
||| specified way.
buffer : SendEffect -> BufferFunc a
buffer Signal = bufferAndSignal
buffer Broadcast = bufferAndBroadcast

-- Obtaining send access --

||| Given a reference to a BufferedChannel obtain the channel and the ability to
||| send on the channel given the desired effect sending should have on any
||| potentially waiting receiver-threads.
export
becomeSender : (bcRef : IORef (BufferedChannel a))
             -> IO (dc : BufferedChannel a ** (SendEffect -> SenderFunc a))
becomeSender bcRef =
  do bc <- readIORef bcRef
     pure (MkDPair bc send)

||| Given a reference to a BufferedChannel obtain the channel and the ability to
||| buffer a list of items on the channel given the desired effect sending
||| should have on any potentially waiting receiver-threads.
export
becomeBuffer : (bcRef : IORef (BufferedChannel a))
             -> IO (dc : BufferedChannel a ** (SendEffect -> BufferFunc a))
becomeBuffer bcRef =
  do bc <- readIORef bcRef
     pure (MkDPair bc buffer)

-- Receiving --

||| The type of a receiver function which takes a channel and produces an IO
||| action containing the next thing on the channel if there is one, and Nothing
||| otherwise.
public export
NonBlockingReceiver : Type -> Type
NonBlockingReceiver a = BufferedChannel a -> IO (Maybe a)

||| The type of a receiver function which takes a channel and produces an
||| IO action which is guaranteed to contain the next thing on the channel.
public export
BlockingReceiver : Type -> Type
BlockingReceiver a = BufferedChannel a -> IO a

||| Crash Idris with a message signalling that something went wrong in terms of
||| the fundamental guarantees of condition variables.
|||
||| Essentially, the point of waiting on a CV is to wait until something is
||| available for consumption. So as soon as the CV lets us past, there will be
||| something to retrieve. However, Idris doesn't know this.
await_crash : IO a
await_crash =
  assert_total $ idris_crash "Await somehow got Nothing despite waiting on a CV"

||| Try to receive a thing on the channel without blocking until something
||| appears.
|||
||| MTSafe: YES
receive : NonBlockingReceiver a
receive (MkBufferedChannel condLock condVar qRef) = dequeue qRef

||| Try to receive the next thing and if there is Nothing, block on the
||| BufferedChannel's internal condition variable until something arrives, and
||| at that point, retrieve that thing.
|||
||| MTSafe: YES
await : BlockingReceiver a
await (MkBufferedChannel condLock condVar qRef) =
  do (Just thing) <- dequeue qRef
          -- if there wasn't anything in the queue, wait until something appears
        | Nothing => do mutexAcquire condLock
                        conditionWait condVar condLock
                        (Just thing') <- dequeue qRef
                           | Nothing => await_crash
                        mutexRelease condLock
                        pure thing'
     pure thing

-- Obtaining receive access --

||| How receiving on a channel should behave:
||| - A non-blocking receiver is not guaranteed to always get a thing when it
|||   receives, but never blocks the receiving thread.
||| - A blocking receiver is guaranteed to always get a thing when it receives,
|||   but may block the receiving thread until something arrives.
public export
data ReceiveType = NonBlocking
                 | Blocking

||| Given a reference to a BufferedChannel and a choice between weather the
||| receive operation should block the thread until something arrives or not,
||| obtain the channel and the ability to receive on it in the desired manner.
export
becomeReceiver : (1 recvType : ReceiveType)
               -> (bcRef : IORef (BufferedChannel a))
               -> case recvType of
                       NonBlocking => IO (dc : BufferedChannel a
                                               ** (NonBlockingReceiver a))
                       Blocking => IO (dc : BufferedChannel a
                                            ** (BlockingReceiver a))
becomeReceiver NonBlocking bcRef = do bc <- readIORef bcRef
                                      pure (MkDPair bc receive)
becomeReceiver Blocking bcRef = do bc <- readIORef bcRef
                                   pure (MkDPair bc await)


text:
||| A Idris port of the prettyprinter library [1] and
||| the ANSI terminal backend [2].
|||
||| [1] https://hackage.haskell.org/package/prettyprinter
||| [2] https://hackage.haskell.org/package/prettyprinter-ansi-terminal

module Text.PrettyPrint.Prettyprinter

import public Text.PrettyPrint.Prettyprinter.Doc
import public Text.PrettyPrint.Prettyprinter.Symbols

%default total


text:
module Fronted.Kotlin.PrettyPrinter

import Frontend.Kotlin.AST
import Tools.Annotation

%access public export

--  _   _ _   _ _      ---------------------------------------------------------
-- | | | | |_(_) |___  ---------------------------------------------------------
-- | | | | __| | / __| ---------------------------------------------------------
-- | |_| | |_| | \__ \ ---------------------------------------------------------
--  \___/ \__|_|_|___/ ---------------------------------------------------------
--                     ---------------------------------------------------------
exprLvl : (k : SyntaxType -> Type)
       -> (k ExprTy -> Nat)
       -> SyntaxF k ExprTy
       -> Nat
exprLvl _ lvl (EInt x)        = 0
exprLvl _ lvl (EStr x)        = 0
exprLvl _ lvl ETrue           = 0
exprLvl _ lvl EFalse          = 0
exprLvl _ lvl EThis           = 0
exprLvl _ lvl ENull           = 0
exprLvl _ lvl (EAccess x)     = 0
exprLvl _ lvl (EAss x y)      = 8
exprLvl _ lvl (ECall x xs)    = 0
exprLvl _ lvl (ENot x)        = 1
exprLvl _ lvl (EMinus x)      = 1
exprLvl _ lvl (EOp x y z)     = operatorLvl x
exprLvl _ lvl (EIfElse x y z) = 10
exprLvl _ lvl (EWhile x y)    = 9
exprLvl _ lvl (EReturn x)     = 9
exprLvl _ lvl (EFun xs x y)   = 0

intersperse : String -> List String -> String
intersperse sep [] = ""
intersperse sep xs = foldl1 (\a1 => \a2 => a1 ++ sep ++ a2) xs

parens : String -> String
parens str = "(" ++ str ++ ")"

--                 _   _         ____       _       _    ____             ------
--  _ __  _ __ ___| |_| |_ _   _|  _ \ _ __(_)_ __ | |_ / ___| ___ _ __   ------
-- | '_ \| '__/ _ \ __| __| | | | |_) | '__| | '_ \| __| |  _ / _ \ '_ \  ------
-- | |_) | | |  __/ |_| |_| |_| |  __/| |  | | | | | |_| |_| |  __/ | | | ------
-- | .__/|_|  \___|\__|\__|\__, |_|   |_|  |_|_| |_|\__|\____|\___|_| |_| ------
-- |_|                     |___/                                          ------
--

prettyPrintGen : (k : SyntaxType -> Type)
              -> ((tp : SyntaxType) -> Nat -> k tp -> String)
              -> (k ExprTy -> Nat)
              -> (tp : SyntaxType)
              -> Nat
              -> SyntaxF k tp
              -> String

--  _____              _____
-- |_   _|  _ _ __  __|_   _|  _
--   | || || | '_ \/ -_)| || || |
--   |_| \_, | .__/\___||_| \_, |
--       |__/|_|            |__/
prettyPrintGen _ shower lvl _ tbs (TParam x [])  = x
prettyPrintGen _ shower lvl _ tbs (TParam x xs)  = x ++ "<"
                                                ++ ( intersperse ", "
                                                   $ map (shower TypeTy tbs) xs)
                                                ++ ">"
prettyPrintGen _ shower lvl _ tbs (TNull x)      = shower TypeTy tbs x ++ "?"
prettyPrintGen _ shower lvl _ tbs (TFun xs x)    = ( parens  $ intersperse ", "
                                                   $ map (shower TypeTy tbs) xs)
                                                ++ " -> " ++ shower TypeTy tbs x

-- __   __       _____
-- \ \ / /_ _ _ |_   _|  _
--  \ V / _` | '_|| || || |
--   \_/\__,_|_|  |_| \_, |
--                    |__/
prettyPrintGen _ shower lvl _ tbs (VVar x Nothing z)  = concat (take tbs (repeat "\t"))
                                                     ++ "var " ++ x ++ " = "
                                                     ++ shower ExprTy (tbs + 1) z
prettyPrintGen _ shower lvl _ tbs (VVar x (Just t) z) = concat (take tbs (repeat "\t"))
                                                     ++ "var " ++ x ++ " : " ++ shower TypeTy 0 t
                                                     ++ " = " ++ shower ExprTy (tbs + 1) z
prettyPrintGen _ shower lvl _ tbs (VVal x Nothing z)  = concat (take tbs (repeat "\t"))
                                                     ++ "val " ++ x ++ " = "
                                                     ++ shower ExprTy (tbs + 1) z
prettyPrintGen _ shower lvl _ tbs (VVal x (Just t) z) = concat (take tbs (repeat "\t"))
                                                     ++ "val " ++ x ++ " : " ++ shower TypeTy 0 t
                                                     ++ " = " ++ shower ExprTy (tbs + 1) z

--  ___                   _____       ___                     ___ _____
-- | _ \__ _ _ _ __ _ _ _|_   _|  _  | _ \__ _ _ _ __ _ _ __ / __|_   _|  _
-- |  _/ _` | '_/ _` | '  \| || || | |  _/ _` | '_/ _` | '  \ (__  | || || |
-- |_| \__,_|_| \__,_|_|_|_|_| \_, | |_| \__,_|_| \__,_|_|_|_\___| |_| \_, |
--                             |__/                                    |__/
prettyPrintGen _ shower lvl _ tbs (Param x y) =           x ++ " : " ++ shower TypeTy 0 y
prettyPrintGen _ shower lvl _ tbs (PCVar x y) = "var " ++ x ++ " : " ++ shower TypeTy 0 y
prettyPrintGen _ shower lvl _ tbs (PCVal x y) = "val " ++ x ++ " : " ++ shower TypeTy 0 y

--   ___ _            _____
--  / __| |__ _ _____|_   _|  _
-- | (__| / _` (_-<_-< | || || |
--  \___|_\__,_/__/__/ |_| \_, |
--                         |__/
prettyPrintGen _ shower lvl _ tbs (Class x xs ys zs) = concat (take tbs (repeat "\t"))
                                                    ++ "data class " ++ x ++ "<"
                                                    ++ intersperse ", " xs ++ ">("
                                                    ++ ( intersperse ", "
                                                       $ map (shower ParamCTy (tbs + 1)) ys)
                                                    ++ ") {"
                                                    ++ ( intersperse ";\n"
                                                       $ map (shower VarTy (tbs + 1)) zs)
                                                    ++ " }"

--  ___        _____
-- | __|  _ _ |_   _|  _
-- | _| || | ' \| || || |
-- |_| \_,_|_||_|_| \_, |
--                  |__/
prettyPrintGen _ shower lvl _ tbs (Fun xs x ys y z) = concat (take tbs (repeat "\t"))
                                                   ++ "fun<" ++ intersperse ", " xs ++ "> "
                                                   ++ x ++ "("
                                                   ++ ( intersperse ", "
                                                      $ map (shower ParamTy 0) ys)
                                                   ++ ")"
                                                   ++ " : " ++ shower TypeTy 0 y
                                                   ++ " {\n" ++ shower BlockTy (tbs + 1) z

--  ___         _ _____
-- |   \ ___ __| |_   _|  _
-- | |) / -_) _| | | || || |
-- |___/\___\__|_| |_| \_, |
--                     |__/
prettyPrintGen _ shower lvl _ tbs (DVar x)   = shower VarTy   tbs x
prettyPrintGen _ shower lvl _ tbs (DClass x) = shower ClassTy tbs x
prettyPrintGen _ shower lvl _ tbs (DFun x)   = shower FunTy   tbs x

--  ___ _ _    _____
-- | __(_) |__|_   _|  _
-- | _|| | / -_)| || || |
-- |_| |_|_\___||_| \_, |
--                  |__/
prettyPrintGen _ shower lvl _ tbs (File xs) = intersperse "\n\n"
                                            $ map (shower DeclTy tbs) xs

--  ___             _____
-- | __|_ ___ __ _ |_   _|  _
-- | _|\ \ / '_ \ '_|| || || |
-- |___/_\_\ .__/_|  |_| \_, |
--         |_|           |__/
prettyPrintGen _ shower lvl _ tbs (EInt x)        = show x
prettyPrintGen _ shower lvl _ tbs (EStr x)        = show x
prettyPrintGen _ shower lvl _ tbs ETrue           = "true"
prettyPrintGen _ shower lvl _ tbs EFalse          = "false"
prettyPrintGen _ shower lvl _ tbs EThis           = "this"
prettyPrintGen _ shower lvl _ tbs ENull           = "null"
prettyPrintGen _ shower lvl _ tbs (EAccess x)     = shower AccessTy tbs x
prettyPrintGen _ shower lvl _ tbs (EAss x y)      = shower AccessTy tbs x ++ " = "
                                                 ++ shower ExprTy   tbs y
prettyPrintGen _ shower lvl _ tbs (ECall x xs)    = x ++ "("
                                                 ++ ( intersperse ", "
                                                    $ map (shower ExprTy tbs) xs)
                                                 ++ ")"
prettyPrintGen _ shower lvl _ tbs (ENot x)        = "!"
                                                 ++ ( (if lvl x > 1 then parens else id)
                                                    $ shower ExprTy tbs x)
prettyPrintGen _ shower lvl _ tbs (EMinus x)      = "-"
                                                 ++ ( (if lvl x > 1 then parens else id)
                                                    $ shower ExprTy tbs x)
prettyPrintGen _ shower lvl _ tbs (EOp x y z)     = ( (if lvl y > operatorLvl x then parens else id)
                                                    $ shower ExprTy tbs y)
                                                 ++ " " ++ show x ++ " "
                                                 ++ ( (if lvl z > operatorLvl x then parens else id)
                                                    $ shower ExprTy tbs z)
prettyPrintGen _ shower lvl _ tbs (EIfElse x y z) = "if(" ++ shower ExprTy tbs x ++ ") "
                                                 ++ shower BlockExprTy tbs y
                                                 ++ " else " ++ shower BlockExprTy tbs z
prettyPrintGen _ shower lvl _ tbs (EWhile x y)    = "while(" ++ shower ExprTy tbs x ++ ") "
                                                 ++ shower BlockExprTy tbs y
prettyPrintGen _ shower lvl _ tbs (EReturn x)     = "return "
                                                 ++ case x of
                                                      Nothing => ""
                                                      Just x' => shower ExprTy tbs x'
prettyPrintGen _ shower lvl _ tbs (EFun xs x y)   = "fun("
                                                 ++ ( intersperse ", "
                                                    $ map (shower ParamTy tbs) xs)
                                                 ++ ") "
                                                 ++ " : " ++ shower TypeTy tbs x ++ " "
                                                 ++ "{" ++ shower BlockTy (tbs + 1) y

--  ___ _         _   _____
-- | _ ) |___  __| |_|_   _|  _
-- | _ \ / _ \/ _| / / | || || |
-- |___/_\___/\__|_\_\ |_| \_, |
--                         |__/
prettyPrintGen _ shower lvl _ tbs BEmpty      = concat (take tbs (repeat "\t")) ++ "}"
prettyPrintGen _ shower lvl _ tbs (BVar x y)  = shower VarTy   (tbs + 1) x ++ "\n"
                                             ++ shower BlockTy tbs       y
prettyPrintGen _ shower lvl _ tbs (BExpr x y) = concat (take (tbs + 1) (repeat "\t"))
                                             ++ shower ExprTy  (tbs + 1) x ++ "\n"
                                             ++ shower BlockTy tbs       y

--  ___ _         _   ___             _____
-- | _ ) |___  __| |_| __|_ ___ __ _ |_   _|  _
-- | _ \ / _ \/ _| / / _|\ \ / '_ \ '_|| || || |
-- |___/_\___/\__|_\_\___/_\_\ .__/_|  |_| \_, |
--                           |_|           |__/
prettyPrintGen _ shower lvl _ tbs (BEBlock x) = concat (take tbs (repeat "\t")) ++ "{"
                                             ++ shower BlockTy tbs x
prettyPrintGen _ shower lvl _ tbs (BEExpr x)  = shower ExprTy tbs x

--    _                   _____
--   /_\  __ __ ___ _____|_   _|  _
--  / _ \/ _/ _/ -_|_-<_-< | || || |
-- /_/ \_\__\__\___/__/__/ |_| \_, |
--                             |__/
prettyPrintGen _ shower lvl _ tbs (AIdent x)  = x
prettyPrintGen _ shower lvl _ tbs (ASub x y)  = ( (if lvl x > 0 then parens else id)
                                                $ shower ExprTy tbs x)
                                               ++ "." ++ y
prettyPrintGen _ shower lvl _ tbs (ANSub x y) = ( (if lvl x > 0 then parens else id)
                                                $ shower ExprTy tbs x)
                                               ++ "?." ++ y

--     _                      _        _   _              ----------------------
--    / \   _ __  _ __   ___ | |_ __ _| |_(_) ___  _ __   ----------------------
--   / _ \ | '_ \| '_ \ / _ \| __/ _` | __| |/ _ \| '_ \  ----------------------
--  / ___ \| | | | | | | (_) | || (_| | |_| | (_) | | | | ----------------------
-- /_/   \_\_| |_|_| |_|\___/ \__\__,_|\__|_|\___/|_| |_| ----------------------
--                                                        ----------------------

prettyPrintLvl : SyntaxAnn ExprTy a -> Nat
prettyPrintLvl (Ann _ syn) = exprLvl (\id => SyntaxAnn id a) prettyPrintLvl syn

prettyPrintAST : (tp : SyntaxType) -> Nat -> SyntaxAnn tp a -> String
prettyPrintAST _ tbs (Ann _ syn) = prettyPrintGen (\id => SyntaxAnn id a)
                                                  prettyPrintAST
                                                  prettyPrintLvl
                                                  tp tbs syn

prettyPrintAnn : Show a => (tp : SyntaxType) -> Nat -> SyntaxAnn tp a -> String
prettyPrintAnn _ tbs (Ann ann syn) = "[" ++ show ann ++ "]"
                                  ++ prettyPrintGen (\id => SyntaxAnn id a)
                                                    prettyPrintAnn
                                                    prettyPrintLvl
                                                    tp tbs syn

Show (SyntaxAnn tp a) where
  show syn = prettyPrintAST tp 0 syn


text:
module Bezout
import Divisors
import ZZ
import Data.Vect
import Data.Fin
%access public export

{-Copied from Chinmaya's code. Gives quotient and remainder on divison-}
{-This just computes the qoutient and the remainder, but it doesn't prove that they indeed satisfy the conditions a = b*q + r and r < b -}
Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat)
Eucl Z b = (Z,Z)
Eucl (S k) b = case (lte (S (S k)) b) of
                    False => (S(fst(Eucl (minus (S k) b) b)), snd(Eucl (minus (S k) b) b))
                    True => (Z, S k)
{-Just a slight modification of the Euclid's division function to give the remainder -}
rem : (a : Nat) -> (b : Nat) -> Nat
rem Z b = Z
rem (S k) b = case (lte (S (S k)) b) of
                    False => (rem (minus (S k) b) b)
                    True => (S k)
{-Let rk be the remainder in the Euclidean algorithm at the k-2th step.
Let rk = ak*r0 + bk*r1 where r0 and r1 are the original inputs.Correspondingly  rsk = ask*r0 + bsk*r1 where sk = k+1
Then the I am going to the next step in the Euclid algorithm and changing the coefficients.
These formulas can be easily derived.-}
Euclnos: (Integer,Integer,Integer,Integer,Integer,Integer)->(Integer,Integer,Integer,Integer,Integer,Integer)
Euclnos (rk, rsk ,ak ,ask, bk ,bsk) = (rsk,rssk,ask,assk,bsk,bssk) where
  rssk = cast(snd (Eucl (cast rk) (cast rsk)))
  bssk =bk-bsk* (cast(fst (Eucl (cast rk) (cast rsk))))
  assk =ak-ask* (cast(fst (Eucl (cast rk) (cast rsk))))
{-Does the Euclnos repeatedy until the remainder is zero. Then the previous remainder is the GCD.-}
Bezouttuple: (Integer,Integer,Integer,Integer,Integer,Integer)->(Integer,Integer,Integer,Integer,Integer,Integer)
Bezouttuple (rk, rsk ,ak ,ask, bk, bsk) = case rsk of
                                        0 => (rk, rsk, ak, ask, bk, bsk)
                                        _ => (Bezouttuple (Euclnos (rk ,rsk, ak ,ask ,bk ,bsk)))
{-Returns 2 particular Integers out of a 6 tuple-}
returnab: (Integer,Integer,Integer,Integer,Integer,Integer)->(ZZ,ZZ)
returnab (a ,b ,c ,d, e ,f)  = (cast c,cast e)
{-Returns the Bezout coefficients-}
Bezout : Nat ->Nat ->(ZZ,ZZ)
Bezout k j =  (returnab(Bezouttuple((cast k) , (cast j),1, 0 ,0 ,1)))

|||Same as Euclnos wxcept that it stores the quotient and remainder in a list
MEuclnos:((Integer,Integer,Integer,Integer,Integer,Integer),(List (Integer,Integer)))->((Integer,Integer,Integer,Integer,Integer,Integer),(List (Integer,Integer)))
MEuclnos ((rk, rsk ,ak ,ask, bk ,bsk),xs) = ((Euclnos (rk, rsk ,ak ,ask, bk ,bsk)),((q,r)::xs)) where
  q = (cast(fst (Eucl (cast rk) (cast rsk))))
  r = (cast(snd (Eucl(cast rk) (cast rsk))))
|||Same as Bezouttuple except that it stores the quotient and remainder in a list
MBezout:((Integer,Integer,Integer,Integer,Integer,Integer),(List (Integer,Integer)))->((Integer,Integer,Integer,Integer,Integer,Integer),(List (Integer,Integer)))
MBezout ((rk, rsk ,ak ,ask, bk ,bsk),xs) = case rsk of
                                                0 =>  ((rk, rsk ,ak ,ask, bk ,bsk),xs)
                                                _ =>MBezout (MEuclnos ((rk, rsk ,ak ,ask, bk ,bsk),xs))

|||Gives a list of quotients and remainders in Euclid's Algorithm
EuclList:(a:Nat)->(b:Nat)->List (Integer,Integer)
EuclList a b = (snd (MBezout (((cast a)  ,(cast b), 1,0,0,1),[])))

gcd2 : Nat -> Nat -> ZZ
gcd2 a b = ( (((cast a)*(snd (Bezout a b))) + ((cast b)*(fst (Bezout a b)))))

{-}
just the functions to compute the GCD in two different ways.
{-}
{-
gcd2 : Nat -> Nat -> ZZ
gcd2 a b = ( (((cast a)*(snd (Bezout a b))) + ((cast b)*(fst (Bezout a b)))))

gcdab : Nat -> Nat -> Nat
gcdab b Z = b
gcdab a b = gcdab b (snd (Eucl a b))

{-}

{-proof of existence of remainders and quotients is necessary to define the concept of divisibilty -}
{-The next step ahead might be to proof the uniqueness of these remainders and quotients probably -}

-- defining divisibilty as b | a if there exists q such that a = b*q + Z
-- if b | a and c | b, then c | a.
-- if c | a and c | b, then c | (a + b)

-- auxplusDiv 1 to 4 are just auxilary proofs.
auxtransDiv : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (b = c*q)
auxtransDiv a b c d = ?auxtransDiv_rhs

auxplusDiv1 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (a = b) -> (c = d) -> (a + c = b + d)
auxplusDiv1 b b d d Refl Refl = Refl

auxplusDiv2 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat) -> (p : Nat) -> (a = c*q) -> (b = c*p) -> (a + b = c*(q + p))
auxplusDiv2 a b c q p pf1 pf2 = (trans (auxplusDiv1 a (c*q) b (c*p) pf1 pf2) (sym(multDistributesOverPlusRight c q p)))

auxplusDiv3 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (d : Nat) -> (a = c) -> (b = d) -> ((minus a b) = (minus c d))
auxplusDiv3 c d c d Refl Refl = Refl

-- Holes !!
auxplusDiv4 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat) -> (p : Nat) -> (a + b = c*q) -> (b = c*p) -> (a = c*(minus q p))
auxplusDiv4 a b c q p pf1 pf2 = ?auxplusDiv3_rhs

--These statements are the two main facts we might be Integererested in.
plusDiv1 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat ** a = c*q) -> (p : Nat ** b = c*p) -> (f : Nat ** a + b = c*f)
plusDiv1 a b c (q ** pf1) (p ** pf2) = ((q + p) ** (auxplusDiv2 a b c q p pf1 pf2))

plusDiv2 : (a : Nat) -> (b : Nat) -> (c : Nat) -> (q : Nat ** a + b = c*q) -> (p : Nat ** b = c*p) -> (f : Nat ** a = c*f)
plusDiv2 a b c (q ** pf1) (p ** pf2) = ((minus q p) ** (auxplusDiv4 a b c q p pf1 pf2))

-- I'll try and prove some (possibly useful) facts about the gcd.
-- weak definition of the gcd : d | a, d | b and if c | a and c | b, then c <= d.
--This is the common Factor Type

isCommonFactor : Nat -> Nat -> Nat -> Type
isCommonFactor a b c = ((q : Nat ** a = c*q),(p : Nat ** b = c*p))

--This is the GCD type
-- d is "a" gcd of a and b if isGCD a b d type is inhabited.
-- Uniqueness of GCD not assumed !!
-- the gcd is just assumed to be bigger than any other common divisor, not a multiple of it.

isGCD : Nat -> Nat -> Nat -> Type
isGCD a b d = ((isCommonFactor a b d) , ((c : Nat) -> (isCommonFactor a b c) -> (LTE c d)))

-- try to prove that if d is "a" gcd of (a,b) then it is "a" gcd of (a+b,a)

gcdfact1 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (isCommonFactor (a + b) b d)
gcdfact1 a b d (((q ** pf1),(p ** pf2)),f) = ((plusDiv1 a b d (q ** pf1) (p ** pf2)),(p ** pf2))

gcdfact2 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (c : Nat) -> (isCommonFactor (a + b) b c) -> (LTE c d)
gcdfact2 a b d (pf , f) c ((q ** pf1),(p ** pf2)) = (f c ((plusDiv2 a b c (q ** pf1) (p ** pf2)),(p ** pf2)))

maingcdfact1 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (isGCD (a + b) b d)
maingcdfact1 a b d pf = ((gcdfact1 a b d pf),(gcdfact2 a b d pf))

-- now the proof that if d is "a" gcd of (a+b,b), then it is "a" gcd of (a,b)

gcdfact3 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD (a + b) b d) -> (isCommonFactor a b d)
gcdfact3 a b d (((q ** pf1),(p ** pf2)),f) = ((plusDiv2 a b d (q ** pf1) (p ** pf2)),(p ** pf2))

gcdfact4 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD (a + b) b d) -> (c : Nat) -> (isCommonFactor a b c) -> (LTE c d)
gcdfact4 a b d (pf, f) c ((q ** pf1),(p ** pf2)) = (f c ((plusDiv1 a b c (q ** pf1) (p ** pf2)),(p ** pf2)))

maingcdFact2 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD (a + b) b d) -> (isGCD a b d)
maingcdFact2 a b d pf = ((gcdfact3 a b d pf),(gcdfact4 a b d pf))

-- now the proof that if d is "a" gcd of (a,b), it is also "a" gcd of (b,a)

symCommonFactor : (a : Nat) -> (b : Nat) -> (c : Nat) -> (isCommonFactor a b c) -> (isCommonFactor b a c)
symCommonFactor a b c ((p ** pf1),(q ** pf2)) = ((q ** pf2),(p ** pf1))

symGCD1 : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> ((c : Nat) -> (isCommonFactor b a c) -> (LTE c d))
symGCD1 a b d (pf, f) = g where
                          g c ((p ** pf1),(q ** pf2)) = f c ((q ** pf2),(p ** pf1))

symGCD : (a : Nat) -> (b : Nat) -> (d : Nat) -> (isGCD a b d) -> (isGCD b a d)
symGCD a b d (pf , f) = ((symCommonFactor a b d pf) , (symGCD1 a b d (pf , f)))

-- I'll list the types and functions that might be useful
-- The GCD type : isGCD : Nat -> Nat -> Nat -> Type
--                isGCD a b d = ((isCommonFactor a b d) , ((c : Nat) -> (isCommonFactor a b c) -> (LTE c d)))
-- maingcdfact1 , maingcdfact2 , symGCD.

-- The next step might be to show that the natural number that the euclidian algorithm gives us is indeed a gcd
-- also uniqueness of gcd.


text:
module Solutions.DataTypes

-- If all or almost all functions in a module are provably
-- total, it is convenient to add the following pragma
-- at the top of the module. It is then no longer necessary
-- to annotate each function with the `total` keyword.
%default total

--------------------------------------------------------------------------------
--          Enumerations
--------------------------------------------------------------------------------

-- 1
and : Bool -> Bool -> Bool
and True  b = b
and False _ = False

or : Bool -> Bool -> Bool
or True  _ = True
or False b = b

--2
data UnitOfTime = Second | Minute | Hour | Day | Week

toSeconds : UnitOfTime -> Integer -> Integer
toSeconds Second y = y
toSeconds Minute y = 60 * y
toSeconds Hour y   = 60 * 60 * y
toSeconds Day y    = 24 * 60 * 60 * y
toSeconds Week y   = 7 * 24 * 60 * 60 * y

fromSeconds : UnitOfTime -> Integer -> Integer
fromSeconds u s = s `div` toSeconds u 1

convert : UnitOfTime -> Integer -> UnitOfTime -> Integer
convert u1 n u2 = fromSeconds u2 (toSeconds u1 n)

--------------------------------------------------------------------------------
--          Sum Types
--------------------------------------------------------------------------------

data Title = Mr | Mrs | Other String

eqTitle : Title -> Title -> Bool
eqTitle Mr        Mr        = True
eqTitle Mrs       Mrs       = True
eqTitle (Other x) (Other y) = x == y
eqTitle _         _         = False

isOther : Title -> Bool
isOther (Other _) = True
isOther _         = False

data LoginError = UnknownUser String | InvalidPassword | InvalidKey

showError : LoginError -> String
showError (UnknownUser x) = "Unknown user: " ++ x
showError InvalidPassword = "Invalid password"
showError InvalidKey      = "Invalid key"

--------------------------------------------------------------------------------
--          Records
--------------------------------------------------------------------------------

-- 1
record TimeSpan where
  constructor MkTimeSpan
  unit  : UnitOfTime
  value : Integer

timeSpanToSeconds : TimeSpan -> Integer
timeSpanToSeconds (MkTimeSpan unit value) = toSeconds unit value

-- 2
eqTimeSpan : TimeSpan -> TimeSpan -> Bool
eqTimeSpan x y = timeSpanToSeconds x == timeSpanToSeconds y

-- alternative equality check using `on` from the Idris Prelude
eqTimeSpan' : TimeSpan -> TimeSpan -> Bool
eqTimeSpan' = (==) `on` timeSpanToSeconds

-- 3
showUnit : UnitOfTime -> String
showUnit Second = "s"
showUnit Minute = "min"
showUnit Hour   = "h"
showUnit Day    = "d"
showUnit Week   = "w"

prettyTimeSpan : TimeSpan -> String
prettyTimeSpan (MkTimeSpan Second v) = show v ++ " s"
prettyTimeSpan (MkTimeSpan u v)      =
  show v ++ " " ++ showUnit u ++ "(" ++ show (toSeconds u v) ++ " s)"

-- 4
compareUnit : UnitOfTime -> UnitOfTime -> Ordering
compareUnit = compare `on` (\x => toSeconds x 1)

minUnit : UnitOfTime -> UnitOfTime -> UnitOfTime
minUnit x y = case compareUnit x y of
  LT => y
  _  => x

addTimeSpan : TimeSpan -> TimeSpan -> TimeSpan
addTimeSpan (MkTimeSpan u1 v1) (MkTimeSpan u2 v2) =
  case minUnit u1 u2 of
    u => MkTimeSpan u (convert u1 v1 u + convert u2 v2 u)

--------------------------------------------------------------------------------
--          Generic Data Types
--------------------------------------------------------------------------------

-- 1
mapMaybe : (a -> b) -> Maybe a -> Maybe b
mapMaybe _ Nothing  = Nothing
mapMaybe f (Just x) = Just (f x)

appMaybe : Maybe (a -> b) -> Maybe a -> Maybe b
appMaybe (Just f) (Just v) = Just (f v)
appMaybe _        _        = Nothing

bindMaybe : Maybe a -> (a -> Maybe b) -> Maybe b
bindMaybe Nothing  _ = Nothing
bindMaybe (Just x) f = f x

filterMaybe : (a -> Bool) -> Maybe a -> Maybe a
filterMaybe f Nothing  = Nothing
filterMaybe f (Just x) = if (f x) then Just x else Nothing

first : Maybe a -> Maybe a -> Maybe a
first Nothing  y = y
first (Just x) _ = Just x

last : Maybe a -> Maybe a -> Maybe a
last x y = first y x

foldMaybe : (acc -> elem -> acc) -> acc -> Maybe elem -> acc
foldMaybe f x = maybe x (f x)

-- 2
mapEither : (a -> b) -> Either e a -> Either e b
mapEither _ (Left x)  = Left x
mapEither f (Right x) = Right (f x)

appEither : Either e (a -> b) -> Either e a -> Either e b
appEither (Left x)  _         = Left x
appEither (Right _) (Left x)  = Left x
appEither (Right f) (Right v) = Right (f v)

bindEither : Either e a -> (a -> Either e b) -> Either e b
bindEither (Left x)  _ = Left x
bindEither (Right x) f = f x

firstEither : (e -> e -> e) -> Either e a -> Either e a -> Either e a
firstEither fun (Left e1) (Left e2) = Left (fun e1 e2)
firstEither _   (Left e1) y         = y
firstEither _   (Right x) _         = Right x

-- instead of implementing this via pattern matching, we use
-- firstEither and swap the arguments. Since this would mean that
-- in the case of two `Left`s the errors would be in the wrong
-- order, we have to swap the arguments of `fun` as well.
-- Function `flip` from the prelude does this for us.
lastEither : (e -> e -> e) -> Either e a -> Either e a -> Either e a
lastEither fun x y = firstEither (flip fun) y x

fromEither : (e -> c) -> (a -> c) -> Either e a -> c
fromEither f _ (Left x)  = f x
fromEither _ g (Right x) = g x

-- 3
mapList : (a -> b) -> List a -> List b
mapList f Nil       = Nil
mapList f (x :: xs) = f x :: mapList f xs

filterList : (a -> Bool) -> List a -> List a
filterList f Nil       = Nil
filterList f (x :: xs) =
  if f x then x :: filterList f xs else filterList f xs

headMaybe : List a -> Maybe a
headMaybe Nil      = Nothing
headMaybe (x :: _) = Just x

tailMaybe : List a -> Maybe (List a)
tailMaybe Nil       = Nothing
tailMaybe (x :: xs) = Just xs

lastMaybe : List a -> Maybe a
lastMaybe Nil        = Nothing
lastMaybe (x :: Nil) = Just x
lastMaybe (_ :: xs)  = lastMaybe xs

initMaybe : List a -> Maybe (List a)
initMaybe Nil        = Nothing
initMaybe (x :: Nil) = Just Nil
initMaybe (x :: xs)  = mapMaybe (x ::) (initMaybe xs)

foldList : (acc -> elem -> acc) -> acc -> List elem -> acc
foldList fun vacc Nil       = vacc
foldList fun vacc (x :: xs) = foldList fun (fun vacc x) xs

-- 4
record Client where
  constructor MkClient
  name     : String
  title    : Title
  age      : Bits8
  password : Either Bits64 String

data Credentials = Password String Bits64 | Key String

login1 : Client -> Credentials -> Either LoginError Client
login1 c (Password u y) =
  if c.name == u then
    if c.password == Left y then Right c else Left InvalidPassword
  else Left (UnknownUser u)

login1 c (Key x) =
  if c.password == Right x then Right c else Left InvalidKey

login : List Client -> Credentials -> Either LoginError Client
login Nil       (Password u _) = Left (UnknownUser u)
login Nil       (Key x)        = Left InvalidKey
login (x :: xs) cs             = case login1 x cs of
  Right c               => Right c
  Left  InvalidPassword => Left InvalidPassword
  Left _                => login xs cs


text:
module Bisim

%default total

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

ssucc : Stream' Nat -> Stream' Nat
ssucc s = (S (hd s)) :: (ssucc (tl s))

zeros : Stream' Nat
zeros = 0 :: zeros

ones : Stream' Nat
ones = 1 :: ones

twos : Stream' Nat
twos = 2 :: twos

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

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

bisimsucconestwos : BisimStream' Nat (ssucc ones) twos
bisimsucconestwos = MkBisimStream' Refl bisimsucconestwos

bisim_eq : BisimStream' a s s' -> s = s'
bisim_eq = believe_me

-- repeat : Vect (S n) a -> Stream' a
-- repeat xs = repeat' xs xs
--   where
--   repeat' : Vect (S n) a -> Vect (S m) a -> Stream' a
--   repeat' xs (x :: []) = x :: (repeat' xs xs)
--   repeat' xs (x :: (y :: ys)) = x :: (repeat' xs (y :: ys))

-- zeroone : Vect 2 Nat
-- zeroone = [0, 1]

-- onetwo : Vect 2 Nat
-- onetwo = [1, 2]

-- bisim_succ_repeat_zeroone__repeat_onetwo : BisimStream' Nat (ssucc (repeat zeroone)) (repeat onetwo)
-- bisim_succ_repeat_zeroone__repeat_onetwo = MkBisimStream' Refl help
--   where
--   help : BisimStream' Nat (tl (ssucc (repeat (zeroone)))) (tl (repeat onetwo))
--   help = MkBisimStream' Refl bisim_succ_repeat_zeroone__repeat_onetwo

-- bisim_succ_repeat_zeroone__repeat_onetwo' : BisimStream (ssucc (repeat zeroone)) (repeat onetwo)
-- bisim_succ_repeat_zeroone__repeat_onetwo' = MkBisimStream Refl (MkBisimStream Refl bisim_succ_repeat_zeroone__repeat_onetwo')

max_stars_repo_name: sualitu/thesis

max_issues_repo_name: sualitu/thesis

max_forks_repo_name: sualitu/thesis


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

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

-- Hint: Use Strings.isInfixOf
filterStr : String -> Vect n String -> (p ** Vect p String)
filterStr s xs = filter (\str => s `isInfixOf` str) xs

filterStr' : String -> List String -> List String
filterStr' s xs = filter (\str => s `isInfixOf` str) xs

search : DataStore -> String -> Maybe (String, DataStore)
search (MkData Z items) str = Nothing
search store@(MkData (S k) items) str = Just (unwords (filterStr' str (toList items)) ++ "\n", store)

-- Just (unwords (toList (filterStr str items)), store)

addToStore : DataStore -> String -> DataStore
addToStore (MkData size items) y =
              MkData _ (addToData items) where
                addToData : Vect old String -> Vect (S old) String
                addToData [] = [y]
                addToData (x :: xs) = x :: addToData xs

sumInputs : Integer -> String -> Maybe (String, Integer)
sumInputs t input =
  let val = cast input in
            if val < 0
            then Nothing
            else let newVal = t + val in Just ("Subtotal: " ++ show newVal ++ "\n", newVal)

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

parseCommand : (cmd : String) -> (args : 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 "search" str = Just (Search str)
parseCommand "size" "" = Just Size
parseCommand "quit" "" = Just Quit
parseCommand _ _ = Nothing

parse : (input : String) -> Maybe Command
parse input = case span (/= ' ') input of
                   (cmd, args) => parseCommand cmd $ ltrim args -- remove leading spaces with the ltrim

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

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store inp
            = case parse inp 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 (show (size store) ++ "\n", store)
                    Just (Search str) => search store str
                    Just Quit => Nothing

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

-- *datastore> :exec
-- Command: add LOL
-- ID 0
-- Command: ad haha
-- Invalid command
-- Command: add haha
-- ID 1
-- Command: get 1
-- haha
-- Command: get 0
-- LOL

-- replWith : a -> String -> (a -> String -> Maybe (String, a)) -> IO ()
-- replWith initial data, a prompt, and a function

-- main : IO ()
-- main = replWith 0 "Value: " sumInputs
-- replWith : a -> String -> (a -> String -> Maybe (String, a)) -> IO ()

-- *datastore> :exec
-- Command: add heyPrat
-- ID 0
-- Command: add hello
-- ID 1
-- Command: search ell
-- hello
-- Command: search he
-- heyPrat hello
-- Command: quit


text:
module Algebra.Monoid

import Data.List

%default total

||| This interface is a witness that for a
||| type `a` the axioms of a monoid hold: `(<+>)` is associative
||| with `neutral` being the neutral element.
public export
interface Monoid a => LMonoid a where
  0 appendAssociative : {x,y,z : a} -> x <+> (y <+> z) === (x <+> y) <+> z

  0 appendLeftNeutral : {x : a} -> Prelude.neutral <+> x === x

  0 appendRightNeutral : {x : a} -> x <+> Prelude.neutral === x

export
LMonoid (List a) where
  appendAssociative = Data.List.appendAssociative _ _ _
  appendRightNeutral = appendNilRightNeutral _
  appendLeftNeutral = Refl

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

export
LMonoid String where
  appendAssociative = unsafeRefl
  appendRightNeutral = unsafeRefl
  appendLeftNeutral = unsafeRefl

||| This interface is a witness that for a
||| type `a` the axioms of a commutative monoid hold:
||| `(<+>)` is commutative.
public export
interface LMonoid a => CommutativeMonoid a where
  0 appendCommutative : {x,y : a} -> x <+> y === y <+> x


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

long : PrintString m => CanSleep m => (offset : Time) => m String
long = do
  printTime offset "long proc, first"
  for 5 $ do
    printTime offset "long proc, before 1000"
    sleepFor 1.seconds
    printTime offset "long proc, before 2000"
    sleepFor 2.seconds
  "long" <$ printTime offset "long proc, last"

short : PrintString m => CanSleep m => (offset : Time) => m String
short = do
  printTime offset "short proc, first"
  for 5 $ do
    printTime offset "short proc, before 350"
    sleepFor 350.millis
    printTime offset "short proc, before 750"
    sleepFor 750.millis
  "short" <$ printTime offset "short proc, last"

zipped : PrintString m => CanSleep m => Zippable m => (offset : Time) => m String
zipped = zipWith (\x, y => "\{x}: \{show y}") a b where
  a : m String
  a = do
    printTime offset "                       zipped a, first"
    sleepFor 3500.millis
    printTime offset "                       zipped a, mid"
    sleepFor 3.seconds
    "zipped" <$ printTime offset "                       zipped a, last"

  b : m Nat
  b = do
    printTime offset "                       zipped b, first"
    6 <$ printTime offset "                       zipped b, last"

export
program : PrintString m => CanSleep m => Zippable m => Alternative m => m Unit
program = do
  offset <- currentTime
  printTime offset "start"

  res <- zipped <|> short
  printTime offset "top: \{res}"

  sleepFor 1.seconds
  printTime offset "------"

  res <- zipped <|> long
  printTime offset "top: \{res}"

  printTime offset "end"


text:
module TTImp.Elab.Hole

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

import TTImp.Elab.Check
import TTImp.TTImp

%default covering

-- If the hole type is itself a hole, mark it as to be solved without
-- generalising multiplicities so that we get as precise as possible a type
-- for the hole
mkPrecise : {auto c : Ref Ctxt Defs} ->
            NF vars -> Core ()
mkPrecise (NApp _ (NMeta n i _) _)
    = updateDef (Resolved i)
                (\case
                    Hole i p => Just (Hole i (record { precisetype = True} p))
                    d => Nothing)
mkPrecise _ = pure ()

export
checkHole : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto m : Ref MD Metadata} ->
            {auto u : Ref UST UState} ->
            {auto e : Ref EST (EState vars)} ->
            RigCount -> ElabInfo ->
            NestedNames vars -> Env Term vars ->
            FC -> UserName -> Maybe (Glued vars) ->
            Core (Term vars, Glued vars)
checkHole rig elabinfo nest env fc n_in (Just gexpty)
    = do nm <- inCurrentNS (UN n_in)
         defs <- get Ctxt
         Nothing <- lookupCtxtExact nm (gamma defs)
             | _ => do log "elab.hole" 1 $ show nm ++ " already defined"
                       throw (AlreadyDefined fc nm)
         expty <- getTerm gexpty
         -- Turn lets into lambda before making the hole so that they
         -- get abstracted over in the hole (it's fine here, unlike other
         -- holes, because we're not trying to unify it so it's okay if
         -- applying the metavariable isn't a pattern form)
         let env' = letToLam env
         (idx, metaval) <- metaVarI fc rig env' nm expty
         mkPrecise !(getNF gexpty)
         -- Record the LHS for this hole in the metadata
         withCurrentLHS (Resolved idx)
         addNameLoc fc nm
         addUserHole False nm
         saveHole nm
         pure (metaval, gexpty)
checkHole rig elabinfo nest env fc n_in exp
    = do nmty <- genName ("type_of_" ++ show n_in)
         let env' = letToLam env
         ty <- metaVar fc erased env' nmty (TType fc)
         nm <- inCurrentNS (UN n_in)
         defs <- get Ctxt
         mkPrecise !(nf defs env' ty)

         Nothing <- lookupCtxtExact nm (gamma defs)
             | _ => do log "elab.hole" 1 $ show nm ++ " already defined"
                       throw (AlreadyDefined fc nm)
         (idx, metaval) <- metaVarI fc rig env' nm ty
         withCurrentLHS (Resolved idx)
         addNameLoc fc nm
         addUserHole False nm
         saveHole nm
         pure (metaval, gnf env ty)


text:
-- Idris implementation of a type-correct, stack-safe
-- compiler including exception handling.
--
-- Morten S. Knudsen, Jeppe Vinberg, Francisco M. Lasaca

import Data.List

%default total

data TyExp = NatTy | BoolTy

VariableId : Type
VariableId = String

mutual
  StackType : Type
  StackType = List Ty

  HeapType : Type
  HeapType = List (VariableId, TyExp)

  data Ty = Han StackType StackType HeapType HeapType | Val TyExp

data V : TyExp -> Type where
  VNat : Nat -> V NatTy
  VBool : Bool -> V BoolTy

data Exp : Bool -> TyExp -> List (VariableId, TyExp) -> Type where
  VarExp : (vId : VariableId) -> {auto p : Elem (vId, ty) env} -> Exp False ty env
  SingleExp : (v : V t) -> Exp False t env
  PlusExp : (x : Exp a NatTy env) -> (y : Exp b NatTy env) -> Exp (a || b) NatTy env
  IfExp : (cond : Exp a BoolTy env) -> (x : Exp b t env) -> (y : Exp c t env) -> Exp (a || b || c) t env
  ThrowExp : Exp True t env
  CatchExp : (x : Exp a t env) -> (h : Exp b t env) -> Exp (a && b) t env

data Program : List (VariableId, TyExp) -> List (VariableId, TyExp) -> Type where
  EmptyProgram : Program env env
  Declaration : (vId : VariableId) ->
                (exp : Exp b t env) ->
                {auto expExecutable : b = False} ->
                (continuing : Program ((vId, t) :: env) env') ->
                (Program env env')
  Assignment : (vId : VariableId) ->
               (exp : Exp b t env) ->
               {auto expExecutable : b = False} ->
               (continuing : Program ((vId, t) :: env) env') ->
               {auto prf' : Elem (vId, t) env} ->
               (Program env env')

data ValuesEnv : List (VariableId, TyExp) -> Type where
  EmptyValuesEnv : ValuesEnv []
  MoreValuesEnv : (vId: VariableId) -> V ty -> ValuesEnv envTy
                  -> ValuesEnv ((vId, ty) :: envTy)

mutual
  evalVarExp : (x : ValuesEnv tEnv) -> (p : Elem (vId, ty) tEnv)  -> V ty
  evalVarExp (MoreValuesEnv _ val _) Here = val
  evalVarExp (MoreValuesEnv _ _ valueEnv) (There later) = evalVarExp valueEnv later

  evalPlusExp : (x : Exp a NatTy tEnv) -> (y : Exp b NatTy tEnv) -> (valuesEnv : ValuesEnv tEnv) -> (prf : (a || (Delay b)) = False) -> V NatTy
  evalPlusExp x y valuesEnv prf {a = False} {b = False} =
    case eval x valuesEnv of
          (VNat x') => case eval y valuesEnv of
                             (VNat y') => VNat (x' + y')
  evalPlusExp _ _ _ Refl {a = False} {b = True} impossible
  evalPlusExp _ _ _ Refl {a = True} {b = _} impossible

  evalIfExp : (cond : Exp a BoolTy tEnv) -> (x : Exp b t tEnv) -> (y : Exp c t tEnv) -> (valuesEnv : ValuesEnv tEnv) -> (prf : (a || (Delay (b || (Delay c)))) = False) -> V t
  evalIfExp cond x y valuesEnv prf {a = False} {b = False} {c = False} =
    case eval cond valuesEnv of
          VBool True => eval x valuesEnv
          VBool False => eval y valuesEnv
  evalIfExp _ _ _ _ Refl {a = False} {b = False} {c = True} impossible
  evalIfExp _ _ _ _ Refl {a = False} {b = False} {c = True} impossible
  evalIfExp _ _ _ _ Refl {a = True} {b = _} {c = _} impossible

  evalCatchExp : (x : Exp a t tEnv) -> (h : Exp b t tEnv) -> (valuesEnv : ValuesEnv tEnv) ->(prf : (a && (Delay b)) = False) -> V t
  evalCatchExp x h valuesEnv prf {a = False} = eval x valuesEnv
  evalCatchExp x h valuesEnv prf {a = True} {b = False} = eval h valuesEnv
  evalCatchExp _ _ _ Refl {a = True} {b = True} impossible

  eval : (e : Exp b t tEnv) -> (valuesEnv : ValuesEnv tEnv) -> {auto prf : b = False} -> V t
  eval (VarExp vId {p}) valuesEnv = evalVarExp valuesEnv p
  eval (SingleExp v) valuesEnv = v
  eval (PlusExp x y) valuesEnv {prf} = evalPlusExp x y valuesEnv prf
  eval (IfExp cond x y) valuesEnv {prf} = evalIfExp cond x y valuesEnv prf
  eval ThrowExp _ {prf = Refl} impossible
  eval (CatchExp x h) valuesEnv {prf}= evalCatchExp x h valuesEnv prf

evPro : (p : Program env env') -> (valueEnv : ValuesEnv env) -> ValuesEnv env'
evPro EmptyProgram valueEnv = valueEnv
evPro (Declaration vId exp continuing) valueEnv =
  let evaluated = eval exp valueEnv in
  evPro continuing (MoreValuesEnv vId evaluated valueEnv)
evPro (Assignment vId exp continuing) valueEnv =
  let evaluated = eval exp valueEnv in
  evPro continuing (MoreValuesEnv vId evaluated valueEnv)
evalProgram : (p : Program [] env') -> ValuesEnv env'
evalProgram p = evPro p EmptyValuesEnv

mutual
  El : Ty -> Type
  El (Han t t' h h') = Code t t' h h'
  El (Val NatTy) = Nat
  El (Val BoolTy) = Bool

  data Code : (s : StackType) -> (s' : StackType) -> (h: HeapType) -> (h': HeapType) -> Type where
    STORE : (vId: VariableId) -> (c: Code s s' ((vId, ty)::h) h') -> Code ((Val ty)::s) s' h h'
    LOAD : (vId: VariableId) -> {auto prf: Elem (vId, ty) h} -> (c: Code ((Val ty)::s) s' h h') -> Code s s' h h'
    PUSH : V tyExp -> Code (Val tyExp :: s) s' h h' -> Code s s' h h'
    ADD : Code (Val NatTy :: s) s' h h' -> Code (Val NatTy :: Val NatTy :: s) s' h h'
    IF : (c1 : Code s s' h h') -> (c2 : Code s s' h h') -> Code (Val BoolTy :: s) s' h h'
    THROW : Code (s'' ++ (Han s s' h h') :: s) s' h h'
    MARK : (han : Code s s' h h') -> (c : Code ((Han s s' h h') :: s) s' h h') -> Code s s' h h'
    UNMARK : Code (t :: s) s' h h' -> Code (t :: (Han s s' h h') :: s) s' h h'
    HALT : Code s s h h

mutual
  compCatch : Exp b ty tenv -> Code (Val ty :: (s'' ++ (Han s s' tenv h') :: s)) s' tenv h' -> Code (s'' ++ (Han s s' tenv h') :: s) s' tenv h'
  compCatch (VarExp vId) c = LOAD vId c
  compCatch (SingleExp v) c = PUSH v c
  compCatch (PlusExp x y) c = compCatch x (compCatch {s'' = Val NatTy :: _} y (ADD c))
  compCatch {s} {s''} (IfExp cond x y) c = compCatch cond (IF (compCatch x c) (compCatch y c))
  compCatch ThrowExp c = THROW
  compCatch (CatchExp x h) c = MARK (compCatch h c) (compCatch {s'' = []} x (UNMARK c))

  compPlusExp : (p : (a || b) = False) -> (x : Exp a NatTy tenv) ->  (y : Exp b NatTy tenv) -> (c : Code ((Val NatTy) :: s) s' tenv h') -> Code s s' tenv h'
  compPlusExp {a = False} {b = False} Refl x y c = comp Refl x (comp Refl y (ADD c))
  compPlusExp {a = False} {b = True} Refl _ _ _ impossible
  compPlusExp {a = True} {b = _} Refl _ _ _ impossible

  compCatchExp : (p : (a && b) = False) -> (x : Exp a ty tenv) -> (handler : Exp b ty tenv) -> (c : Code ((Val ty) :: s) s' tenv h') -> Code s s' tenv h'
  compCatchExp {a = False} Refl x handler c = comp Refl x c
  compCatchExp {a = True} {b = False} p x handler c = MARK (comp Refl handler c) (compCatch {s'' = []} x (UNMARK c))
  compCatchExp {a = True} {b = True} Refl _ _ _ impossible

  compIfExp : (p : (a || b || c) = False) -> (cond : Exp a BoolTy tenv) ->(x : Exp b ty tenv) -> (y : Exp c ty tenv) -> (co : Code ((Val ty) :: s) s' tenv h') -> Code s s' tenv h'
  compIfExp {a = False} {b = False} {c = False} Refl cond x y co = comp Refl cond (IF (comp Refl x co) (comp Refl y co))
  compIfExp {a = False} {b = False} {c = True} Refl _ _ _ _ impossible
  compIfExp {a = False} {b = False} {c = True} Refl _ _ _ _ impossible
  compIfExp {a = True} Refl _ _ _ _ impossible

  comp : (b = False) -> Exp b ty tenv -> Code (Val ty :: s) s' tenv h' -> Code s s' tenv h'
  comp _ (VarExp {p} vId) {tenv} c = LOAD vId c
  comp p (SingleExp v) c = PUSH v c
  comp p (PlusExp x y) c = compPlusExp p x y c
  comp p (IfExp cond x y) co = compIfExp p cond x y co
  comp p (CatchExp x h) c = compCatchExp p x h c
  comp Refl ThrowExp _ impossible

  partial
  compile : (prog: Program tenv tenv') -> Code [] [] tenv tenv'
  compile (Declaration vId exp {expExecutable} continuing) =
    comp expExecutable exp (STORE vId (compile continuing))
  compile (Assignment vId exp {expExecutable} continuing) =
    comp expExecutable exp (STORE vId (compile continuing))
  compile EmptyProgram = HALT

data Stack : (s : StackType) -> Type where
  Nil : Stack []
  (::) : El t -> Stack s -> Stack (t :: s)

data Heap : (h : HeapType) -> Type where
  HeapNil : Heap []
  HeapCons : (vId: VariableId) -> V t -> Heap h -> Heap ((vId, t) :: h)

mutual

  lookup: Heap h -> (p: Elem (vId, ty) h) -> V ty
  lookup (HeapCons vId val tl) Here = val
  lookup (HeapCons _ _ tl) (There later) = lookup tl later

  partial
  exec : Code s s' h h' -> Stack s -> Heap h -> (Stack s', Heap h')
  exec (LOAD {prf} vId c) s h = case lookup h prf of
    (VNat v) => exec c (v :: s) h
    (VBool v) => exec c (v :: s) h
  exec (STORE vId c) {s=(Val NatTy)::_} (x :: tl) h = exec c tl (HeapCons vId (VNat x) h)
  exec (STORE vId c) {s=(Val BoolTy)::_} (x :: tl) h = exec c tl (HeapCons vId (VBool x) h)
  exec (PUSH (VNat x) c) s h = exec c (x :: s) h
  exec (PUSH (VBool x) c) s h = exec c (x :: s) h
  exec (ADD c) (m :: n :: s) h = exec c ((n + m) :: s) h
  exec (IF c1 c2) (True :: s) h = exec c1 s h
  exec (IF c1 c2) (False :: s) h = exec c2 s h
  exec THROW s h = fail s h
  exec (MARK handler c) s h = exec c (handler :: s) h
  exec (UNMARK c) (x :: handler :: s) h = exec c (x :: s) h
  exec HALT s h = (s, h)

  partial
  fail : Stack (s'' ++ Han s s' h h' :: s) -> Heap h -> (Stack s', Heap h')
  fail {s'' = []} (handler' :: s) h = exec handler' s h
  fail {s'' = (_ :: _)} (_ :: s) h = fail s h

-- Example of an entire program
-- `entireProgram`

-- x <- 3           -- []
-- x <- x + 1       -- [x <- 3]
-- y <- x + 2       -- [x <- 4]
-- emptyProgram     -- [y <- 6, x <- 4]

myEmpty : Program [("y", NatTy), ("x", NatTy), ("x", NatTy)] [("y", NatTy), ("x", NatTy), ("x", NatTy)]
myEmpty = EmptyProgram

yEqualsXPlusTwo : Program [("x", NatTy), ("x", NatTy)] [("y", NatTy), ("x", NatTy), ("x", NatTy)]
yEqualsXPlusTwo = Declaration "y" (PlusExp (VarExp "x") (SingleExp (VNat 2))) myEmpty

xEqualsXPlusOne : Program [("x", NatTy)] [("y", NatTy), ("x", NatTy), ("x", NatTy)]
xEqualsXPlusOne = Assignment "x" (PlusExp (VarExp "x") (SingleExp (VNat 1))) yEqualsXPlusTwo

entireProgram : Program [] [("y", NatTy), ("x", NatTy), ("x", NatTy)]
entireProgram = Declaration "x" (SingleExp (VNat 3)) xEqualsXPlusOne

evaluatedProgram : ValuesEnv [("y", NatTy), ("x", NatTy), ("x", NatTy)]
evaluatedProgram = evalProgram entireProgram

compiledProgram :  Code [] [] [] [("y", NatTy), ("x", NatTy), ("x", NatTy)]
compiledProgram = compile entireProgram

partial
executedProgram : (Stack [], Heap [("y", NatTy), ("x", NatTy), ("x", NatTy)])
executedProgram = exec (compiledProgram) [] HeapNil

max_stars_repo_name: JnxF/idris-epigram

max_issues_repo_name: JnxF/idris-epigram

max_forks_repo_name: JnxF/idris-epigram


text:
module Minecraft.Core

%default total

-- Forward declaractions for potential recursive interfaces
namespace Block
  public export data Block : (self : Type) -> Type
namespace Entity
  public export data Entity : (self : Type) -> Type
  namespace Pickup
    public export data Pickup : (self : Type) -> Type
namespace Item
  public export data Item : (self : Type) -> Type
  namespace Put
    public export data Put : (self : Type) -> Type
namespace Tangible
  public export data Tangible : (self : Type) -> Type

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Test.Sodium

import Crypto.Sodium

key : IO Key
key = do k <- newSymmKey
         setKeyChars k 0 [1..26]
         pure k
   where setKeyChars : Key -> Int -> List Int -> IO ()
         setKeyChars k i [] = pure ()
         setKeyChars k i (c :: cs) = do setKeyIdx k i ((c * 42) `mod` 255)
                                        setKeyChars k (i + 1) cs

nonce : IO Nonce
nonce = newNonceFromString "sdlfkjsdlkfjacvbnm,vbnmvhghjvbnasdasdm"

export
test : IO ()
test = do -- first, symmetric key hello world

          encrypted <- cryptoSecretBox "Hello world!" !nonce !key
          print (getBytes encrypted)
          decrypted <- cryptoSecretBoxOpen encrypted !nonce !key

          putStrLn (readBox decrypted)

          --- Now some public/private key stuff

          (alice_pub, alice_sec) <- newKeyPair -- generated by libsodium
          (bob_pub, bob_sec) <- newKeyPair -- generated by libsodium

          encrypted <- cryptoBox "Hello Bob!" !nonce alice_pub bob_sec
          print (getBytes encrypted)
          decrypted <- cryptoBoxOpen encrypted !nonce bob_pub alice_sec

          if (validOpenBox decrypted)
          then putStrLn (readBox decrypted)
          else putStrLn "Error"


text:
-- check dequeuing removes things

import System.Concurrency.Queue

main : IO ()
main = do q <- makeQueue {a=Nat}
          enqueue q 3
          (Just theVal) <- dequeue q
            | Nothing => putStrLn "ERROR: Value disappeared from queue."
          Nothing <- dequeue q
            | (Just huh) => putStrLn "ERROR: Dequeue didn't remove the item."
          putStrLn "Success!"


text:
module Data.BoundedInt

import Data.Bits

trim : Bits (1 + n) -> Bits n
trim b = truncate b

||| An integer in the range [lower, upper). BoundedInt 0 ~= Fin, but using
||| Integers instead of Peano arithmetic, for efficiency.
BoundedInt : Integer -> Nat -> Type
BoundedInt lower upper =
  (x : Integer ** so (lower <= x && x < toIntegerNat upper))

postulate bounds : (x : Integer)
                   -> so (lower <= x && x < toIntegerNat upper)
                   -> so (lower <= x && 1+2*x < pow 2 upper)

bitsToBI : Bits n -> BoundedInt 0 (pow 2 n)
bitsToBI {n=Z}   _ = (0 ** oh)
bitsToBI {n=S _} b = let (x ** meh) = bitsToBI (trim b)
                     in if (b `and` (intToBits 1)) /= (intToBits 0)
                        then (1 + 2 * x ** flip bounds meh)
                        else (2 * x ** flip bounds meh)

(+) : BoundedInt m n -> BoundedInt o p -> BoundedInt (m + o) ((n + p) - 1)
(+) {n=S n} {p=p} (x ** _) (y ** _) = (x + y ** oh)

(-) : BoundedInt m n -> BoundedInt o p -> BoundedInt (m - toIntegerNat p + 1) (fromInteger (toIntegerNat n - o))
(-) (x ** _) (y ** _) = (x - y ** oh)

BIToInteger : BoundedInt m n -> Integer
BIToInteger (x ** _) = x

offByOne : Vect m (BoundedInt (1 + n) (S p)) -> Vect m (BoundedInt n p)
offByOne = map (\x => x - (1 ** oh))

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto