text:
module piAutomata

import tipos
import Data.SortedMap

%access public export

calcAExp : AExp -> Int
calcAExp (Sum (N n1) (N n2)) = n1 + n2
calcAExp (Sub (N n1) (N n2)) = n1 - n2
calcAExp (Div (N n1) (N n2)) = n1 `div` n2
calcAExp (Mul (N n1) (N n2)) = n1 * n2

calcBExp : BExp -> Bool
calcBExp (Not (Boo b)) = not b
calcBExp (Equal (N n1) (N n2)) = n1 == n2
calcBExp (GE (N n1) (N n2)) = n1 >= n2
calcBExp (LE (N n1) (N n2)) = n1 <= n2
calcBExp (LT (N n1) (N n2)) = n1 < n2
calcBExp (GT (N n1) (N n2)) = n1 > n2
calcBExp (And (Boo b1) (Boo b2)) = (&&) b1 b2
calcBExp (OR (Boo b1) (Boo b2)) = (||) b1 b2

transforma:Maybe a -> a
transforma (Just v) = v

-- retorna o maior Loc da lista de Locs
maxList: List Loc -> Int
maxList [] = 0
maxList (x :: xs) = auxiliar x xs where
  auxiliar: Loc -> List Loc -> Int
  auxiliar (L x) [] = x
  auxiliar x  (l :: ls) = if x > l then auxiliar x ls  else auxiliar l ls

-- retorna o maior Loc do mapa + 1
getLocPlus1FromMap: SortedMap Loc Val -> Loc
getLocPlus1FromMap map = L ((maxList (keys map)) + 1)

-- Retorna um stored com a adição de uma nova location como chave e um valor v
extendStored: SortedMap Loc Val -> Val -> SortedMap Loc Val
extendStored map v = insert (getLocPlus1FromMap map) (v) map

getLocFromValBindable: Bindable -> Val
getLocFromValBindable (BindLoc x) = ValLoc x

-- Atualiza segundo ambiente com os valores do primeiro, e cria novas chave-valor caso nao exista
-- ex: addIntersectionNewEnv ([ (ValId "k", L 3) , (ValId "y", L 4) , (ValId "z", L 5)]) ([ (ValId "x", L 1) , (ValId "y", L 2) , (ValId "z", L 3)])
addIntersectionNewEnv: List (Id,Bindable)-> List (Id,Bindable) -> SortedMap Id Bindable
addIntersectionNewEnv [] env = fromList env
addIntersectionNewEnv ( (key,value) :: e) env = addIntersectionNewEnv e (toList (insert key value (fromList env)))

-- deleta todos as chave-valor da memoria dada uma lista de chaves (Loc)
deleteLocsStore: List Loc -> SortedMap Loc Val -> SortedMap Loc Val
deleteLocsStore [] store = store
deleteLocsStore (x :: xs) store = deleteLocsStore xs (delete x store)

pushExpsInCtrl : Actuals -> List Ctrl -> List Ctrl
pushExpsInCtrl (Act []) list = list
pushExpsInCtrl (Act (x::xs)) list =  pushExpsInCtrl (Act xs) ((CtExp x)::list)

getCmdFromClosure : Id -> (SortedMap Id Bindable) ->  Ctrl
getCmdFromClosure id env = let (bindClosure) = lookup id env in case bindClosure of
  Just (BindClos (Clos (f, b, e))) => CtCmd b

getFormalsFromClosure : Id -> (SortedMap Id Bindable) -> Formals
getFormalsFromClosure id env = let (bindClosure) = lookup id env in case bindClosure of
  Just (BindClos (Clos (f, b, e))) => f

getEnvFromClosure : Id -> (SortedMap Id Bindable) -> (SortedMap Id Bindable)
getEnvFromClosure id env = let (bindClosure) = lookup id env in case bindClosure of
  Just (BindClos (Clos (f, b, e))) => e

getExpsFromListVal: List Val -> Nat -> List Val -> List Val
getExpsFromListVal list Z l = reverse l
getExpsFromListVal (x::xs) (S tam) l = getExpsFromListVal xs (tam) (x::l)

removeActuals: Nat -> List Val -> List Val
removeActuals Z list = list
removeActuals (S tam) (x::xs) = removeActuals tam xs

getLocFromValLoc: Val -> Loc
getLocFromValLoc (ValLoc l) = l

match: Formals -> List Val -> SortedMap Id Bindable -> SortedMap Id Bindable
match (Form []) (val::vals) e = empty
match (Form (id::ids)) [] e = empty
match (Form []) [] e = e
match (Form (id::ids)) (val::vals) e = case val of
  ValInt x => let env = insert id (BindInt x) e in match (Form ids) (vals) env
  ValLoc l => let env = insert id (BindLoc l) e in match (Form ids) (vals) env

lookup': Maybe Bindable -> SortedMap Loc Val -> Val
lookup' (Just (BindLoc loc)) sto =  transforma (lookup loc sto)
lookup' Nothing sto = ValNop

inserir : Maybe Bindable -> Val -> SortedMap Loc Val -> SortedMap Loc Val
inserir (Just (BindLoc loc)) v stored = insert loc v stored
inserir Nothing v stored = stored

getCmdFromRec : Id -> (SortedMap Id Bindable) ->  Ctrl
getCmdFromRec id env = let (bindRec) = lookup id env in case bindRec of
  Just (BindRec (Rec (f, b, e, e'))) => CtCmd b

getFormalsFromRec : Id -> (SortedMap Id Bindable) -> Formals
getFormalsFromRec id env = let (bindRec) = lookup id env in case bindRec of
  Just (BindRec (Rec (f, b, e, e'))) => f

getEnv1FromRec : Id -> (SortedMap Id Bindable) -> (SortedMap Id Bindable)
getEnv1FromRec id env = let (bindRec) = lookup id env in case bindRec of
  Just (BindRec (Rec (f, b, e, e'))) => e

getEnv2FromRec : Id -> (SortedMap Id Bindable) -> (SortedMap Id Bindable)
getEnv2FromRec id env = let (bindRec) = lookup id env in case bindRec of
  Just (BindRec (Rec (f, b, e, e'))) => e'

reclose : SortedMap Id Bindable -> SortedMap Id Bindable
reclose env = let list = toList env in recloseAux list where
  recloseAux : List (Id, Bindable) -> SortedMap Id Bindable
  recloseAux [] = empty
  recloseAux (x::[]) = case x of
    ((ValID w), (BindClos (Clos (f, b, e)))) => let env' = insert (ValID w) (BindClos (Clos (f, b, e))) empty in insert (ValID w) (BindRec (Rec (f,b,e, env'))) empty
    ((ValID w), (BindRec (Rec (f,b,e', e'')))) => let env' = insert (ValID w) (BindRec (Rec (f,b,e', e''))) empty in insert (ValID w) (BindRec (Rec (f,b,e', env'))) empty
    (id, b) => insert id b empty
  recloseAux (x::xs) = Data.SortedMap.fromList ((Data.SortedMap.toList (reclose (Data.SortedMap.fromList [x]))) ++ (Data.SortedMap.toList (reclose (Data.SortedMap.fromList xs))))

unfold : SortedMap Id Bindable -> SortedMap Id Bindable
unfold e = reclose(e)

process: (List Ctrl, List Val, SortedMap Id Bindable , SortedMap Loc Val, List Loc) -> List (List Ctrl, List Val, SortedMap Id Bindable , SortedMap Loc Val, List Loc) -> ((List Ctrl, List Val, SortedMap Id Bindable , SortedMap Loc Val, List Loc), List (List Ctrl, List Val, SortedMap Id Bindable , SortedMap Loc Val, List Loc))

-- Stop Case
process ([],[], env, stored, listLoc) list = (([],[], env, stored, listLoc), ([],[], env, stored, listLoc)::list)

-- Aritmetic Expression
process ( (CtExp (AExpR (Sum n1 n2))) ::xs , listVal, env, stored, listLoc) (list) = process ((CtExp (AExpR n1) :: (CtExp (AExpR n2) :: (CtExpOp CtrlSum :: xs)) ), listVal, env, stored, listLoc) (( (CtExp (AExpR (Sum n1 n2))) ::xs , listVal, env, stored, listLoc)::list)

process ( (CtExp (AExpR (Sub n1 n2))) ::xs , listVal, env, stored, listLoc) (list) = process ((CtExp (AExpR n1) :: (CtExp (AExpR n2) :: (CtExpOp CtrlSub :: xs)) ), listVal, env, stored, listLoc) (( (CtExp (AExpR (Sub n1 n2))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (AExpR (Mul n1 n2))) ::xs , listVal, env, stored, listLoc) (list) = process ((CtExp (AExpR n1) :: (CtExp (AExpR n2) :: (CtExpOp CtrlMul :: xs)) ), listVal, env, stored, listLoc) (( (CtExp (AExpR (Mul n1 n2))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (AExpR (Div n1 n2))) ::xs , listVal, env, stored, listLoc) (list) = process ((CtExp (AExpR n1) :: (CtExp (AExpR n2) :: (CtExpOp CtrlDiv :: xs)) ), listVal, env, stored, listLoc) (( (CtExp (AExpR (Div n1 n2))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (AExpR (N     n  ))) ::xs , listVal, env, stored, listLoc) (list) = process (xs , ValInt n :: listVal, env, stored, listLoc) (( (CtExp (AExpR (N     n  ))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExpOp CtrlSum)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc) (list) = process (xs, (ValInt (calcAExp (Sum (N val2) (N val1)))) ::restoLista, env, stored, listLoc) (( (CtExpOp CtrlSum)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc)::list)
process ( (CtExpOp CtrlSub)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc) (list) = process (xs, (ValInt (calcAExp (Sub (N val2) (N val1)))) ::restoLista, env, stored, listLoc) (( (CtExpOp CtrlSub)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc)::list)
process ( (CtExpOp CtrlMul)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc) (list) = process (xs, (ValInt (calcAExp (Mul (N val2) (N val1)))) ::restoLista, env, stored, listLoc) (( (CtExpOp CtrlMul)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc)::list)
process ( (CtExpOp CtrlDiv)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc) (list) = process (xs, (ValInt (calcAExp (Div (N val2) (N val1)))) ::restoLista, env, stored, listLoc) (( (CtExpOp CtrlDiv)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc)::list)

-- Boolean Expression
process ( (CtExp (BExpR (Not b))) ::xs , listVal, env, stored, listLoc) (list) = process ( (CtExp (BExpR b)) :: (CtExpOp CtrlNot :: xs) , listVal, env, stored, listLoc) (( (CtExp (BExpR (Not b))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (BExpR (Equal n1 n2))) ::xs , listVal, env, stored, listLoc) (list) = process ((CtExp (AExpR n1) :: (CtExp (AExpR n2) :: (CtExpOp CtrlEq :: xs)) ), listVal, env, stored, listLoc) (( (CtExp (BExpR (Equal n1 n2))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (BExpR (GE n1 n2))) ::xs , listVal, env, stored, listLoc) (list) = process ((CtExp (AExpR n1) :: (CtExp (AExpR n2) :: (CtExpOp CtrlGE :: xs)) ), listVal, env, stored, listLoc) (( (CtExp (BExpR (GE n1 n2))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (BExpR (LE n1 n2))) ::xs , listVal, env, stored, listLoc) (list) = process ((CtExp (AExpR n1) :: (CtExp (AExpR n2) :: (CtExpOp CtrlLE :: xs)) ), listVal, env, stored, listLoc) (( (CtExp (BExpR (LE n1 n2))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (BExpR (LT n1 n2))) ::xs , listVal, env, stored, listLoc) (list) = process ((CtExp (AExpR n1) :: (CtExp (AExpR n2) :: (CtExpOp CtrlLT :: xs)) ), listVal, env, stored, listLoc) (( (CtExp (BExpR (LT n1 n2))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (BExpR (GT n1 n2))) ::xs , listVal, env, stored, listLoc) (list) = process ((CtExp (AExpR n1) :: (CtExp (AExpR n2) :: (CtExpOp CtrlGT :: xs)) ), listVal, env, stored, listLoc) (( (CtExp (BExpR (GT n1 n2))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (BExpR (And b1 b2))) ::xs , listVal, env, stored, listLoc) (list) = process ((CtExp (BExpR b1) :: (CtExp (BExpR b2) :: (CtExpOp CtrlAnd :: xs)) ), listVal, env, stored, listLoc) (( (CtExp (BExpR (And b1 b2))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (BExpR (OR b1 b2))) ::xs , listVal, env, stored, listLoc) (list) = process ((CtExp (BExpR b1) :: (CtExp (BExpR b2) :: (CtExpOp CtrlOR :: xs)) ), listVal, env, stored, listLoc) (( (CtExp (BExpR (OR b1 b2))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (BExpR (Boo b))) ::xs , listVal, env, stored, listLoc) (list) = process (xs , ValBool b :: listVal, env, stored, listLoc) (( (CtExp (BExpR (Boo b))) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExpOp CtrlNot) :: xs , (ValBool b) :: restoLista, env, stored, listLoc) (list) = process (xs , ValBool (calcBExp (Not (Boo b))) :: restoLista , env, stored, listLoc) (( (CtExpOp CtrlNot) :: xs , (ValBool b) :: restoLista, env, stored, listLoc)::list)
process ( (CtExpOp CtrlEq)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc) (list) = process (xs, (ValBool (calcBExp (Equal (N val2) (N val1)))) ::restoLista, env, stored, listLoc) (( (CtExpOp CtrlEq)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc)::list)
process ( (CtExpOp CtrlGE)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc) (list) = process (xs, (ValBool (calcBExp (GE (N val2) (N val1)))) ::restoLista, env, stored, listLoc) (( (CtExpOp CtrlGE)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc)::list)
process ( (CtExpOp CtrlLE)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc) (list) = process (xs, (ValBool (calcBExp (LE (N val2) (N val1)))) ::restoLista, env, stored, listLoc) (( (CtExpOp CtrlLE)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc)::list)
process ( (CtExpOp CtrlLT)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc) (list) = process (xs, (ValBool (calcBExp (LT (N val2) (N val1)))) ::restoLista, env, stored, listLoc) (( (CtExpOp CtrlLT)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc)::list)
process ( (CtExpOp CtrlGT)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc) (list) = process (xs, (ValBool (calcBExp (GT (N val2) (N val1)))) ::restoLista, env, stored, listLoc) (( (CtExpOp CtrlGT)::xs , (ValInt val1) :: (ValInt val2 :: restoLista), env, stored, listLoc)::list)
process ( (CtExpOp CtrlAnd)::xs , (ValBool val1) :: (ValBool val2 :: restoLista), env, stored, listLoc) (list) = process (xs, (ValBool (calcBExp (And (Boo val2) (Boo val1)))) ::restoLista, env, stored, listLoc) (( (CtExpOp CtrlAnd)::xs , (ValBool val1) :: (ValBool val2 :: restoLista), env, stored, listLoc)::list)
process ( (CtExpOp CtrlOR)::xs , (ValBool val1) :: (ValBool val2 :: restoLista), env, stored, listLoc) (list) = process (xs, (ValBool (calcBExp (OR (Boo val2) (Boo val1)))) ::restoLista, env, stored, listLoc) (( (CtExpOp CtrlOR)::xs , (ValBool val1) :: (ValBool val2 :: restoLista), env, stored, listLoc)::list)

--Commands
process ( (CtCmd (Assign (ValID c1) c2)) ::xs , listVal, env, stored, listLoc) (list) = process (CtExp c2 ::(CtCmdOp CtrlAssign::xs), ValId c1::listVal, env, stored, listLoc) (( (CtCmd (Assign (ValID c1) c2)) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtExp (AExpR (IdA (ValID c1)) )) ::xs , listVal, env, stored, listLoc) (list) = let loc = lookup (ValID c1) env in case loc of
  Nothing => process ([], listVal, env, stored, listLoc) (list)
  Just (BindLoc l) => process (xs, (lookup' (Just (BindLoc l)) (stored))::listVal, env, stored, listLoc) (( (CtExp (AExpR (IdA (ValID c1)) )) ::xs , listVal, env, stored, listLoc)::list)
  Just (BindInt k) => process (xs, (ValInt k)::listVal, env, stored, listLoc) (( (CtExp (AExpR (IdA (ValID c1)) )) ::xs , listVal, env, stored, listLoc)::list)

process ( (CtExp (BExpR (IdB (ValID c1)) )) ::xs , listVal, env, stored, listLoc) (list) = let loc = lookup (ValID c1) env in case loc of
  Nothing => process ([], listVal, env, stored, listLoc) (list)
  Just (BindLoc l) => process (xs, (lookup' (Just (BindLoc l)) (stored))::listVal, env, stored, listLoc) (( (CtExp (BExpR (IdB (ValID c1)) )) ::xs , listVal, env, stored, listLoc)::list)
  Just (BindInt k) => process (xs, (ValInt k)::listVal, env, stored, listLoc) (( (CtExp (BExpR (IdB (ValID c1)) )) ::xs , listVal, env, stored, listLoc)::list)

process ( (CtCmd (Loop b c)) ::xs , listVal, env, stored, listLoc) (list) = process (CtExp (BExpR b) ::(CtCmdOp CtrlLoop::xs), ValCmd (Loop b c)::listVal, env, stored, listLoc) (( (CtCmd (Loop b c)) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtCmd (Cond b c1 c2)) ::xs , listVal, env, stored, listLoc) (list) = process (CtExp (BExpR b) ::(CtCmdOp CtrlCond::xs), ValCmd (Cond b c1 c2)::listVal, env, stored, listLoc) (( (CtCmd (Cond b c1 c2)) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtCmd (CSeq c1 c2)) ::xs , listVal, env, stored, listLoc) (list) = process (CtCmd c1::(CtCmd c2::xs), listVal, env, stored, listLoc) (( (CtCmd (CSeq c1 c2)) ::xs , listVal, env, stored, listLoc)::list)
process ( (CtCmd NOP) ::xs, listVal, env, stored, listLoc) (list) = process ( xs, listVal, env, stored, listLoc) (list)

process ( (CtCmdOp CtrlAssign :: xs ,  v1 :: (ValId v2 ::listVal), env, stored, listLoc)) (list) = process (xs, listVal, env, (inserir (lookup (ValID v2) env) (v1) stored), listLoc) (( (CtCmdOp CtrlAssign :: xs ,  v1 :: (ValId v2 ::listVal), env, stored, listLoc))::list)
process ( (CtCmdOp CtrlLoop :: xs , ValBool True :: (ValCmd (Loop b2 c) :: listVal), env, stored, listLoc)) (list) = process (CtCmd c ::(CtCmd (Loop b2 c)::xs), listVal, env, stored, listLoc) (( (CtCmdOp CtrlLoop :: xs , ValBool True :: (ValCmd (Loop b2 c) :: listVal), env, stored, listLoc))::list)
process ( (CtCmdOp CtrlLoop :: xs , ValBool False :: (ValCmd (Loop b2 c) :: listVal), env, stored, listLoc)) (list) = process (xs, listVal, env, stored, listLoc) (( (CtCmdOp CtrlLoop :: xs , ValBool False :: (ValCmd (Loop b2 c) :: listVal), env, stored, listLoc))::list)
process ( (CtCmdOp CtrlCond :: xs , ValBool True :: (ValCmd (Cond b2 c1 c2) :: listVal), env, stored, listLoc)) (list) = process (CtCmd c1 ::xs, listVal, env, stored, listLoc) (( (CtCmdOp CtrlCond :: xs , ValBool True :: (ValCmd (Cond b2 c1 c2) :: listVal), env, stored, listLoc))::list)
process ( (CtCmdOp CtrlCond :: xs , ValBool False :: (ValCmd (Cond b2 c1 c2) :: listVal), env, stored, listLoc)) (list) = process (CtCmd c2 ::xs, listVal, env, stored, listLoc) (( (CtCmdOp CtrlCond :: xs , ValBool False :: (ValCmd (Cond b2 c1 c2) :: listVal), env, stored, listLoc))::list)

--Declarations
process ( CtExp (Ref exp) :: xs , listVal, env, stored, listLoc) (list) = process (CtExp exp ::(CtExpOp CtrlRef::xs), listVal, env, stored, listLoc) (( CtExp (Ref exp) :: xs , listVal, env, stored, listLoc)::list)
process ( CtCmd (Blk d c) :: xs , listVal, env, stored, listLoc) (list) = process ( CtDec d :: (CtCmdOp CtrlBlkDec :: (CtCmd c :: (CtCmdOp CtrlBlkCmd::xs))), ValListLoc listLoc :: listVal, env, stored, []) (( CtCmd (Blk d c) :: xs , listVal, env, stored, listLoc)::list)
process ( CtDec (Bind (ValID x) exp) :: xs , listVal, env, stored, listLoc) (list) = process ( CtExp exp :: (CtDecOp CtrlBind::xs), ValId x ::listVal, env, stored, listLoc) (( CtDec (Bind (ValID x) exp) :: xs , listVal, env, stored, listLoc)::list)
process ( CtExp (DeRef (ValID x)) :: xs , listVal, env, stored, listLoc) (list) = process ( xs, ( getLocFromValBindable (transforma (lookup (ValID x) env)))::listVal, env, stored, listLoc) (( CtExp (DeRef (ValID x)) :: xs , listVal, env, stored, listLoc)::list)
process ( CtExp (ValRef (ValID x)) :: xs , listVal, env, stored, listLoc) (list) = process ( xs, (lookup' (Just (BindLoc (getLocFromValLoc (lookup' (lookup (ValID x) env) stored))) ) stored)::listVal, env, stored, listLoc) (( CtExp (ValRef (ValID x)) :: xs , listVal, env, stored, listLoc)::list)
process ( CtDec (DSeq a b) :: xs , listVal, env, stored, listLoc) (list) = process (CtDec a :: (CtDec b :: xs), listVal, env, stored, listLoc) (( CtDec (DSeq a b) :: xs , listVal, env, stored, listLoc)::list)

process ( CtExpOp CtrlRef :: xs , v :: listVal, env, stored, listLoc) (list) = process (xs, ValLoc (getLocPlus1FromMap stored) ::listVal, env, extendStored stored v, getLocPlus1FromMap stored ::listLoc) (( CtExpOp CtrlRef :: xs , v :: listVal, env, stored, listLoc)::list)
process ( CtCmdOp CtrlBlkDec :: xs , ValEnv e :: listVal, env, stored, listLoc) (list) = process (xs, ValEnv env ::listVal, addIntersectionNewEnv (toList e) (toList env), stored, listLoc) (( CtCmdOp CtrlBlkDec :: xs , ValEnv e :: listVal, env, stored, listLoc)::list)
process ( CtCmdOp CtrlBlkCmd :: xs , ValEnv e :: (ValListLoc l :: listVal), env, stored, listLoc) (list) = process (xs, listVal, e, deleteLocsStore listLoc stored, l) (( CtCmdOp CtrlBlkCmd :: xs , ValEnv e :: (ValListLoc l :: listVal), env, stored, listLoc)::list)
process ( CtDecOp CtrlBind :: xs , ValLoc l :: (ValId w :: (ValEnv e :: listVal)), env, stored, listLoc) (list) = process (xs, ValEnv (insert (ValID w) (BindLoc l) (e)) ::listVal, env, stored, listLoc) (( CtDecOp CtrlBind :: xs , ValLoc l :: (ValId w :: (ValEnv e :: listVal)), env, stored, listLoc)::list)
process ( CtDecOp CtrlBind :: xs , ValLoc l :: (ValId w :: listVal), env, stored, listLoc) (list) = process (xs, ValEnv (insert (ValID w) (BindLoc l) (empty)) ::listVal, env, stored, listLoc) (( CtDecOp CtrlBind :: xs , ValLoc l :: (ValId w :: listVal), env, stored, listLoc)::list)
process ( CtDecOp CtrlBind :: xs , ValInt n :: (ValId w :: (ValEnv e :: listVal)), env, stored, listLoc) (list) = process (xs, ValEnv (insert (ValID w) (BindInt n) (e)) ::listVal, env, stored, listLoc) (( CtDecOp CtrlBind :: xs , ValInt n :: (ValId w :: (ValEnv e :: listVal)), env, stored, listLoc)::list)
process ( CtDecOp CtrlBind :: xs , ValInt n :: (ValId w :: listVal), env, stored, listLoc) (list) = process (xs, ValEnv (insert (ValID w) (BindInt n) (empty)) ::listVal, env, stored, listLoc) (( CtDecOp CtrlBind :: xs , ValInt n :: (ValId w :: listVal), env, stored, listLoc)::list)

--Abstractions
process ( CtDec (BindF (ValID x) abs) :: xs , listVal, env, stored, listLoc) (list) = process ( CtAbs abs :: (CtDecOp CtrlBindF::xs), ValId x ::listVal, env, stored, listLoc) (( CtDec (BindF (ValID x) abs) :: xs , listVal, env, stored, listLoc)::list)
process ( CtAbs (Abstr f c) :: xs , listVal, env, stored, listLoc) (list) = process (xs, ValClos (Clos (f,c, env))::listVal, env, stored, listLoc) (( CtAbs (Abstr f c) :: xs , listVal, env, stored, listLoc)::list)
process ( CtCmd (Call id (Act listExp)) :: xs , listVal, env, stored, listLoc) (list) = process ((pushExpsInCtrl (Act listExp) ((CtCmdOp (CtrlCall id (Prelude.List.length listExp)))::xs)), listVal, env, stored, listLoc) (( CtCmd (Call id (Act listExp)) :: xs , listVal, env, stored, listLoc)::list)

process ( CtDecOp CtrlBindF :: xs , ValClos cls :: (ValId w :: listVal), env, stored, listLoc) (list) = process (xs, ValEnv (insert (ValID w) (BindClos cls) (empty)) ::listVal, env, stored, listLoc) (( CtDecOp CtrlBindF :: xs , ValClos cls :: (ValId w :: listVal), env, stored, listLoc)::list)
process ( CtCmdOp (CtrlCall id tam)::xs , listVal, env, stored, listLoc) (list) = let e = toList env in case e of
  (((ValID w), (BindClos (Clos (f, b, e))))::l) => process ((getCmdFromClosure id env)::((CtCmdOp CtrlBlkCmd)::xs), ValEnv env :: (ValListLoc listLoc:: (removeActuals tam listVal) ), addIntersectionNewEnv ( Data.SortedMap.toList (match (getFormalsFromClosure id env) (getExpsFromListVal (listVal) (tam) ([]) ) empty) ) ( Data.SortedMap.toList (addIntersectionNewEnv (Data.SortedMap.toList (getEnvFromClosure id env)) (Data.SortedMap.toList env)) ) , stored, []) (( CtCmdOp (CtrlCall id tam)::xs , listVal, env, stored, listLoc)::list)
  (((ValID w), (BindRec (Rec (f,b,e', e''))))::l) => process ((getCmdFromRec id env)::((CtCmdOp CtrlBlkCmd)::xs), ValEnv env :: (ValListLoc listLoc:: (removeActuals tam listVal) ), addIntersectionNewEnv ( Data.SortedMap.toList (match (getFormalsFromRec id env) (getExpsFromListVal (listVal) (tam) ([]) ) empty) ) (Data.SortedMap.toList (addIntersectionNewEnv (Data.SortedMap.toList (unfold (getEnv2FromRec id env))) ( Data.SortedMap.toList (addIntersectionNewEnv (Data.SortedMap.toList (getEnv1FromRec id env)) (Data.SortedMap.toList env)) ))) , stored, []) (( CtCmdOp (CtrlCall id tam)::xs , listVal, env, stored, listLoc)::list)

process ( CtDec (Rbnd (ValID x) (Abstr f c)) :: xs , listVal, env, stored, listLoc) (list) = process ( xs, ValEnv (unfold (insert (ValID x) (BindClos (Clos (f, c, env))) empty)) ::listVal, env, stored, listLoc) (( CtDec (Rbnd (ValID x) (Abstr f c)) :: xs , listVal, env, stored, listLoc)::list)

max_stars_repo_name: RonaldCamp/ImpCompiler

max_issues_repo_name: RonaldCamp/ImpCompiler

max_forks_repo_name: RonaldCamp/ImpCompiler


text:
module System.Directory

import System.Errno
import public System.File
import System.FFI

%default total

public export
DirPtr : Type
DirPtr = AnyPtr

support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support, idris_directory.h"

directoriesClass : String
directoriesClass = "io/github/mmhelloworld/idrisjvm/runtime/Directories"

ok : HasIO io => a -> io (Either FileError a)
ok x = pure (Right x)

%foreign support "idris2_currentDirectory"
         "node:lambda:()=>process.cwd()"
         jvm directoriesClass "getWorkingDirectory"
prim__currentDir : PrimIO (Ptr String)

%foreign support "idris2_changeDir"
         "node:support:changeDir,support_system_directory"
         jvm directoriesClass "changeDirectory"
prim__changeDir : String -> PrimIO Int

%foreign support "idris2_createDir"
         "node:support:createDir,support_system_directory"
         jvm directoriesClass "createDirectory"
prim__createDir : String -> PrimIO Int

%foreign support "idris2_openDir"
         jvm directoriesClass "openDirectory"
prim__openDir : String -> PrimIO DirPtr

%foreign support "idris2_closeDir"
         jvm directoriesClass "closeDirectory"
prim__closeDir : DirPtr -> PrimIO ()

%foreign support "idris2_removeDir"
         jvm directoriesClass "delete"
prim__removeDir : String -> PrimIO ()

%foreign support "idris2_nextDirEntry"
         jvm directoriesClass "getNextDirectoryEntry"
prim__dirEntry : DirPtr -> PrimIO (Ptr String)

export
data Directory : Type where
     MkDir : DirPtr -> Directory

export
createDir : HasIO io => String -> io (Either FileError ())
createDir dir
    = do res <- primIO (prim__createDir dir)
         if res == 0
            then ok ()
            else returnError

export
changeDir : HasIO io => String -> io Bool
changeDir dir
    = do ok <- primIO (prim__changeDir dir)
         pure (ok == 0)

export
currentDir : HasIO io => io (Maybe String)
currentDir
    = do res <- primIO prim__currentDir
         if prim__nullPtr res /= 0
            then pure Nothing
            else pure (Just (prim__getString res))

export
openDir : HasIO io => String -> io (Either FileError Directory)
openDir d
    = do res <- primIO (prim__openDir d)
         if prim__nullAnyPtr res /= 0
            then returnError
            else ok (MkDir res)

export
closeDir : HasIO io => Directory -> io ()
closeDir (MkDir d) = primIO (prim__closeDir d)

export
removeDir : HasIO io => String -> io ()
removeDir dirName = primIO (prim__removeDir dirName)

export
nextDirEntry : HasIO io => Directory -> io (Either FileError (Maybe String))
nextDirEntry (MkDir d)
    = do res <- primIO (prim__dirEntry d)
         if prim__nullPtr res /= 0
            then if !(getErrno) /= 0
                    then returnError
                    else pure $ Right Nothing
            else do let n = prim__getString res
                    if n == "." || n == ".."
                       then assert_total $ nextDirEntry (MkDir d)
                       else pure $ Right (Just n)

-- This function is deprecated; to be removed after the next version bump
export
dirEntry : HasIO io => Directory -> io (Either FileError String)
dirEntry d = do r <- nextDirEntry d
                pure $ case r of
                         Left e         => Left e
                         Right (Just n) => Right n
                         Right Nothing  => Left FileNotFound

collectDir : HasIO io => Directory -> io (Either FileError (List String))
collectDir d
    = liftIO $ do let (>>=) : (IO . Either e) a -> (a -> (IO . Either e) b) -> (IO . Either e) b
                      (>>=) = Prelude.(>>=) @{Monad.Compose {m = IO} {t = Either e}}
                  Just n <- nextDirEntry d
                    | Nothing => pure $ Right []
                  ns <- assert_total $ collectDir d
                  pure $ Right (n :: ns)

export
listDir : HasIO io => String -> io (Either FileError (List String))
listDir name = do Right d <- openDir name
                    | Left e => pure $ Left e
                  ns <- collectDir d
                  ignore <- closeDir d
                  pure $ ns

ext: idr


text:
module Evens

public export
data IsEven : Nat -> Type where
  ZEven : IsEven 0
  SSEven : (n: Nat) -> IsEven n -> IsEven (S (S n))

twoEven : IsEven 2
twoEven = SSEven 0 ZEven

fourEven : IsEven 4
fourEven = SSEven 2 twoEven

half : (n: Nat) -> IsEven n -> Nat
half Z ZEven = 0
half (S (S k)) (SSEven k x) = S (half k x)

public export
double: Nat -> Nat
double Z = Z
double (S k) = S (S (double k))

doubleEven : (n: Nat) -> IsEven (double n)
doubleEven Z = ZEven
doubleEven (S k) = SSEven (double k) (doubleEven k)

halfDouble: Nat -> Nat
halfDouble n = half (double n) (doubleEven n)

oneOdd: IsEven 1 -> Void
oneOdd ZEven impossible
oneOdd (SSEven _ _) impossible

threeOdd : IsEven 3 -> Void
threeOdd (SSEven (S Z) ZEven) impossible
threeOdd (SSEven (S Z) (SSEven _ _)) impossible

nOrSnEven: (n: Nat) -> Either (IsEven n) (IsEven (S n))
nOrSnEven Z = Left ZEven
nOrSnEven (S k) = case (nOrSnEven k) of
                       (Left l) => Right (SSEven k l)
                       (Right r) => Left r

halfRoof: Nat -> Nat
halfRoof n = case (nOrSnEven n) of
                  (Left nEven) => half n nEven
                  (Right snEven) => half (S n) snEven

nSnNotBothEven: (n: Nat) -> (IsEven n) -> IsEven (S n) -> Void
nSnNotBothEven Z ZEven ZEven impossible
nSnNotBothEven Z ZEven (SSEven _ _) impossible
nSnNotBothEven (S (S k)) (SSEven k x) (SSEven (S k) y) = nSnNotBothEven k x y

notNandSnEven : (n: Nat) -> (IsEven n , IsEven (S n)) -> Void
notNandSnEven n (a, b) = nSnNotBothEven n a b

apNat : (f: Nat -> Nat) -> (n: Nat) -> (m: Nat) -> n = m -> f n = f m
apNat f m m Refl = Refl

byTwo : (n: Nat) -> IsEven n -> (k: Nat ** double k = n)
byTwo Z ZEven = (0 ** Refl)
byTwo (S (S k)) (SSEven k x) = step where
  step = case (byTwo k x) of
            (m ** pf) => ((S m) ** apNat (\l => S (S l)) (double m) k pf)

oneOddFamily : Nat -> Type
oneOddFamily Z = ()
oneOddFamily (S Z) = Void
oneOddFamily (S (S k)) = ()

oneOddProof : (n : Nat) -> IsEven n -> oneOddFamily n
oneOddProof Z ZEven = ()
oneOddProof (S (S k)) (SSEven k x) = ()


text:
module Collections.BSTree.Set.Core

import Collections.Util.Bnd
import Collections.BSTree.Map.Core as M
import Decidable.Order.Strict

||| A verified binary search tree with erased proofs.
|||
||| The keys in the tree are constrained by min/max bounds, which make use of `Bnd` to extend the
||| tree key type with `Top` and `Bot` values. This allows for a natural way to leave bounds
||| unconstrained (by having a minimum of `Bot` or a maximum of `Top`).
|||
||| @ ord The ordering implementations used in the tree. Since these are w.r.t. a type `kTy`, the
|||       type of tree keys is defined implicitly by `ord`.
||| @ min The minimum value constraint, proving that `sto min (Mid x)` for all values `x` in the
|||       tree.
||| @ max The maximum value constraint, proving that `sto (Mid x) max` for all values `x` in the
|||       tree.
public export
BST : {0 sto : kTy -> kTy -> Type} ->
      (pre : StrictPreorder kTy sto) ->
      (tot : StrictOrdered kTy sto) ->
      (0 min,max : Bnd kTy) ->
      Type
BST pre tot min max = M.BST pre tot () min max
%name Collections.BSTree.Set.Core.BST t,u,v

||| A verified binary search tree with erased proofs.
|||
||| This is an alias for the more generic `BST` (which accepts min/max bounds for its contents).
||| The bounds are necessary for verifying the structure of a tree, but the root node of any
||| `BST` will always be unconstrained. So generally, `BST` can be considered an implementation
||| detail.
|||
||| @ ord The strict total ordering used in the tree. Since a `StrictOrdered` impl is w.r.t. a type
|||       `kTy`, the type of tree values is defined implicitly by `ord`.
public export
BSTree : {0 kTy : Type} ->
         (0 sto : kTy -> kTy -> Type) ->
         {auto pre : StrictPreorder kTy sto} ->
         {auto tot : StrictOrdered kTy sto} ->
         Type
BSTree sto {pre} {tot} = M.BST pre tot () Bot Top
%name Collections.BSTree.Set.Core.BSTree t,u,v

max_stars_repo_name: polendri/idris-collections

max_issues_repo_name: polendri/idris-collections

max_forks_repo_name: polendri/idris-collections


text:
||| An Idris port of the Wadler-Leijen pretty-printer.
module Text.PrettyPrint.Leijen

import Data.List
import Data.Stream

%default total

||| Zip a Stream and a List together.
private
zipWithStreamL : (f : a -> b -> c) -> Stream a -> (r : List b) -> List c
zipWithStreamL _ _         []        = []
zipWithStreamL f (x :: xs) (y :: ys) = f x y :: zipWithStreamL f xs ys

||| Create a string from a specified number of spaces.
|||
||| @ n how many spaces to use
private
spaces : (n : Nat) -> String
spaces Z = ""
spaces n = pack (replicate n ' ')

private
indentation : Nat -> String
indentation n = spaces n

infixr 5 |/|, |//|, |$|, |$$|
infixr 6 |+|, |++|

||| The abstract data type `Doc` represents pretty documents.
|||
||| Doc is an instance of the `Show` class. `(show doc)` pretty prints
||| document `doc` with a page width of 100 characters and a ribbon
||| width of 40 characters.
|||
|||     > show (text "hello" |$| text "world")
|||
||| Which would return the string "hello\nworld", i.e.
|||
|||
|||     hello
|||     world
|||
export
data Doc : Type where
  Empty : Doc

  ||| A single character document with the invariant that the
  ||| character is not a newline.
  Char' : Char -> Doc

  ||| A document containing a string (plus its length). Invariant:
  ||| the string doesn't contain a newline.
  Text : Nat -> String -> Doc

  ||| A newline document.
  |||
  ||| @ nospace If True, then when this newline is undone by group, do
  ||| not insert a space
  Line : (nospace : Bool) -> Doc

  Cat : Doc -> Doc -> Doc
  Nest : Int -> Doc -> Doc

  ||| One document or another.
  |||
  ||| Invariant: first lines of first doc longer than the first lines
  ||| of the second doc
  |||
  ||| @ d1 the document with the longer first lines
  ||| @ d2 the document with the shorter first lines
  Union : (d1, d2 : Doc) -> Doc

  Column  : (Nat -> Doc) -> Doc
  Nesting : (Int -> Doc) -> Doc

||| The data type `SimpleDoc` represents rendered documents and is
||| used by the display functions.
|||
||| The `Nat` in `SText` contains the length of the string. The `Nat`
||| in `SLine` contains the indentation for that line. The library
||| provides two default display functions 'displayS' and
||| 'displayIO'. You can provide your own display function by writing a
||| function from a `SimpleDoc` to your own output format.
public export
data SimpleDoc  = SEmpty
                | SChar Char SimpleDoc
                | SText Nat String SimpleDoc
                | SLine Nat SimpleDoc

||| List of indentation/document pairs; saves an indirection over `List (Nat,Doc)`
public export
data Docs   = Nil
            | Cons Nat Doc Docs

-----------------------------------------------------------
-- Primitives
-----------------------------------------------------------

||| The empty document is, indeed, empty. Although `empty` has no
||| content, it does have a 'height' of 1 and behaves exactly like
||| `(text "")` (and is therefore not a unit of `|$|`).
public export
empty : Doc
empty           = Empty

||| The `line` document advances to the next line and indents to the
||| current nesting level. Document `line` behaves like `(text " ")`
||| if the line break is undone by 'group'.
public export
line : Doc
line            = Line False

||| The document `(char c)` contains the literal character `c`. The
||| character shouldn't be a newline (`'\n'`), the function 'line'
||| should be used for line breaks.
public export
char : Char -> Doc
char '\n'       = line
char c          = Char' c

||| The document `(text s)` contains the literal string `s`. The
||| string shouldn't contain any newline (`'\n'`) characters. If the
||| string contains newline characters, the function 'string' should be
||| used.
public export
text : String -> Doc
text ""         = Empty
text s          = Text (length s) s

||| The `linebreak` document advances to the next line and indents to
||| the current nesting level. Document `linebreak` behaves like
||| 'empty' if the line break is undone by 'group'.
public export
linebreak : Doc
linebreak       = Line True

||| Horizontal concatenation of documents
public export
beside : Doc -> Doc -> Doc
beside x y      = Cat x y

||| The document `(nest i x)` renders document `x` with the current
||| indentation level increased by i (See also 'hang', 'align' and
||| 'indent').
|||
||| > nest 2 (text "hello" |$| text "world") |$| text "!"
|||
||| outputs as:
|||
||| `
||| hello
|||   world
||| !
||| `
public export
nest : Int -> Doc -> Doc
nest i x        = Nest i x

public export
column : (Nat -> Doc) -> Doc
column f        = Column f

public export
nesting : (Int -> Doc) -> Doc
nesting f       = Nesting f

||| The `group` combinator is used to specify alternative
||| layouts. The document `(group x)` undoes all line breaks in
||| document `x`. The resulting line is added to the current line if
||| that fits the page. Otherwise, the document `x` is rendered without
||| any changes.
public export
group : Doc -> Doc
group x         = Union (flatten x) x
  where flatten : Doc -> Doc
        flatten (Cat x y)       = Cat (flatten x) (flatten y)
        flatten (Nest i x)      = Nest i (flatten x)
        flatten (Line break)    = if break then Empty else Text 1 " "
        flatten (Union x _)     = flatten x
        flatten (Column f)      = Column (\n => flatten (f n))
        flatten (Nesting f)     = Nesting (\n => flatten (f n))
        flatten other           = other                     --Empty,Char,Text

-----------------------------------------------------------
-- semi primitive: Alignment and indentation
-----------------------------------------------------------

-- The combinators in this section can not be described by Wadler's
-- original combinators. They align their output relative to the
-- current output position - in contrast to `nest` which always
-- aligns to the current nesting level. This deprives these
-- combinators from being `optimal'. In practice however they
-- prove to be very useful. The combinators in this section should
-- be used with care, since they are more expensive than the other
-- combinators. For example, `align` shouldn't be used to pretty
-- print all top-level declarations of a language, but using `hang`
-- for let expressions is fine.

||| The document `(align x)` renders document `x` with the nesting
||| level set to the current column. It is used for example to
||| implement 'hang'.
|||
||| As an example, we will put a document right above another one,
||| regardless of the current nesting level:
|||
||| > x $$ y  = align (x |$| y)
|||
||| > test    = text "hi" |++| (text "nice" $$ text "world")
|||
||| which will be layed out as:
|||
||| `
||| hi nice
|||    world
||| `
public export
align : Doc -> Doc
align d         = column (\k =>
                  nesting (\i => nest (cast k - i) d))   --nesting might be negative :-)

||| The hang combinator implements hanging indentation. The document
||| `(hang i x)` renders document `x` with a nesting level set to the
||| current column plus `i`. The following example uses hanging
||| indentation for some text:
|||
||| > test  = hang 4 (fillSep (map text
||| >         (words "the hang combinator indents these words !")))
|||
||| Which lays out on a page with a width of 20 characters as:
|||
||| `
||| the hang combinator
|||     indents these
|||     words !
||| `
|||
||| The `hang` combinator is implemented as:
|||
||| > hang i x  = align (nest i x)
public export
hang : Nat -> Doc -> Doc
hang i d        = align (nest (cast i) d)

||| The document `(indent i x)` indents document `x` with `i` spaces.
|||
||| > test  = indent 4 (fillSep (map text
||| >         (words "the indent combinator indents these words !")))
|||
||| Which lays out with a page width of 20 as:
|||
||| `
|||     the indent
|||     combinator
|||     indents these
|||     words !
||| `
public export
indent : Nat -> Doc -> Doc
indent i d      = hang i (text (spaces i) `beside` d)

-----------------------------------------------------------
-- Character documents
-----------------------------------------------------------

||| The document `lparen` contains a left parenthesis, "(".
public export
lparen : Doc
lparen          = char '('

||| The document `rparen` contains a right parenthesis, ")".
public export
rparen : Doc
rparen          = char ')'

||| The document `langle` contains a left angle, "<".
public export
langle : Doc
langle          = char '<'

||| The document `rangle` contains a right angle, ">".
public export
rangle : Doc
rangle          = char '>'

||| The document `lbrace` contains a left brace, "{".
public export
lbrace : Doc
lbrace          = char '{'

||| The document `rbrace` contains a right brace, "}".
public export
rbrace : Doc
rbrace          = char '}'

||| The document `lbracket` contains a left square bracket, "[".
public export
lbracket : Doc
lbracket        = char '['

||| The document `rbracket` contains a right square bracket, "]".
public export
rbracket : Doc
rbracket        = char ']'

||| The document `squote` contains a single quote, "'".
public export
squote : Doc
squote          = char '\''

||| The document `dquote` contains a double quote, '"'.
public export
dquote : Doc
dquote          = char '"'

||| The document `semi` contains a semi colon, ";".
public export
semi : Doc
semi            = char ';'

||| The document `colon` contains a colon, ":".
public export
colon : Doc
colon           = char ':'

||| The document `comma` contains a comma, ",".
public export
comma : Doc
comma           = char ','

||| The document `space` contains a single space, " ".
|||
||| > x |++| y   = x |+| space |+| y
public export
space : Doc
space           = char ' '

||| The document `dot` contains a single dot, ".".
public export
dot : Doc
dot             = char '.'

||| The document `backslash` contains a backslash, "\\".
public export
backslash : Doc
backslash       = char '\\'

||| The document `equals` contains an equal sign, "=".
public export
equals : Doc
equals          = char '='

-----------------------------------------------------------
-- high-level combinators
-----------------------------------------------------------

||| The document `softline` behaves like `space` if the resulting
||| output fits the page, otherwise it behaves like `line`.
|||
||| ```
||| softline = group line
||| ```
public export
softline : Doc
softline        = group line

||| The document `softbreak` behaves like `empty` if the resulting
||| output fits the page, otherwise it behaves like 'line'.
|||
||| ```
||| softbreak  = group linebreak
||| ```
public export
softbreak : Doc
softbreak       = group linebreak

||| The document `(x |+| y)` concatenates document `x` and document
||| `y`. It is an associative operation having 'empty' as a left and
||| right unit.
public export
(|+|) : Doc -> Doc -> Doc
x |+| y          = x `beside` y

||| The document `(x |++| y)` concatenates document `x` and `y` with a
||| `space` in between.
public export
(|++|) : Doc -> Doc -> Doc
x |++| y         = x |+| space |+| y

||| The document `(x |/| y)` concatenates document `x` and `y` with a
||| 'softline' in between. This effectively puts `x` and `y` either
||| next to each other (with a `space` in between) or underneath each
||| other.
public export
(|/|) : Doc -> Doc -> Doc
x |/| y         = x |+| softline |+| y

||| The document `(x |//| y)` concatenates document `x` and `y` with
||| a 'softbreak' in between. This effectively puts `x` and `y` either
||| right next to each other or underneath each other.
public export
(|//|) : Doc -> Doc -> Doc
x |//| y        = x |+| softbreak |+| y

||| The document `(x |$| y)` concatenates document `x` and `y` with a
||| `line` in between.
public export
(|$|) : Doc -> Doc -> Doc
x |$| y         = x |+| line |+| y

||| The document `(x |$$| y)` concatenates document `x` and `y` with
||| a `linebreak` in between.
public export
(|$$|) : Doc -> Doc -> Doc
x |$$| y        = x |+| linebreak |+| y

||| Fold a list of documents using some combining operator.
|||
||| @ f how to combine the documents
||| @ ds the documents to combine
public export
fold : (f : Doc -> Doc -> Doc) -> (ds : List Doc) -> Doc
fold _ []       = empty
fold f (d::ds)  = f d (fold f ds)

||| The document `(vsep xs)` concatenates all documents `xs`
||| vertically with `(|$|)`. If a 'group' undoes the line breaks
||| inserted by `vsep`, all documents are separated with a space.
|||
||| ```
||| someText = map text (words ("text to lay out"))
|||
||| test     = text "some" |++| vsep someText
||| ```
|||
||| This is layed out as:
|||
||| ```
||| some text
||| to
||| lay
||| out
||| ```
|||
||| The 'align' combinator can be used to align the documents under
||| their first element
|||
||| ```
||| test     = text "some" |++| align (vsep someText)
||| ```
|||
||| Which is printed as:
|||
||| ```
||| some text
|||      to
|||      lay
|||      out
||| ```
public export
vsep : List Doc -> Doc
vsep            = fold (|$|)

||| The document `(sep xs)` concatenates all documents `xs` either
||| horizontally with `(|++|)`, if it fits the page, or vertically with
||| `(|$|)`.
|||
||| ```
||| sep xs  = group (vsep xs)
||| ```
public export
sep : List Doc -> Doc
sep             = group . vsep

||| The document `(fillSep xs)` concatenates documents `xs`
||| horizontally with `(|++|)` as long as its fits the page, than
||| inserts a `line` and continues doing that for all documents in
||| `xs`.
|||
||| ```
||| fillSep xs  = foldr (|/|) empty xs
||| ```
public export
fillSep : List Doc -> Doc
fillSep         = fold (|/|)

||| The document `(hsep xs)` concatenates all documents `xs`
||| horizontally with `(|++|)`.
public export
hsep : List Doc -> Doc
hsep            = fold (Text.PrettyPrint.Leijen.(|++|))

||| The document `(hcat xs)` concatenates all documents `xs`
||| horizontally with `(|+|)`.
public export
hcat : List Doc -> Doc
hcat            = fold (|+|)

||| The document `(vcat xs)` concatenates all documents `xs`
||| vertically with `(|$$|)`. If a `group` undoes the line breaks
||| inserted by `vcat`, all documents are directly concatenated.
public export
vcat : List Doc -> Doc
vcat            = fold (|$$|)

||| The document `(cat xs)` concatenates all documents `xs` either
||| horizontally with `(|+|)`, if it fits the page, or vertically with
||| `(|$$|)`.
|||
||| ```
||| cat xs  = group (vcat xs)
||| ```
public export
cat : List Doc -> Doc
cat             = group . vcat

||| The document `(fillCat xs)` concatenates documents `xs`
||| horizontally with `(|+|)` as long as its fits the page, than inserts
||| a `linebreak` and continues doing that for all documents in `xs`.
|||
||| ```
||| fillCat xs  = foldr (|//|) empty xs
||| ```
public export
fillCat : List Doc -> Doc
fillCat         = fold (|//|)

||| The document `(enclose l r x)` encloses document `x` between
||| documents `l` and `r` using `(|+|)`.
|||
||| ```
||| enclose l r x   = l |+| x |+| r
||| ```
public export
enclose : Doc -> Doc -> Doc -> Doc
enclose l r x   = l |+| x |+| r

||| Document `(squotes x)` encloses document `x` with single quotes
||| "\'".
public export
squotes : Doc -> Doc
squotes         = enclose squote squote

||| Document `(dquotes x)` encloses document `x` with double quotes
||| '\"'.
public export
dquotes : Doc -> Doc
dquotes         = enclose dquote dquote

||| Document `(braces x)` encloses document `x` in braces, "{" and
||| "}".
public export
braces : Doc -> Doc
braces          = enclose lbrace rbrace

||| Document `(parens x)` encloses document `x` in parenthesis, "("
||| and ")".
public export
parens : Doc -> Doc
parens          = enclose lparen rparen

||| Document `(angles x)` encloses document `x` in angles, "<" and
||| ">".
public export
angles : Doc -> Doc
angles          = enclose langle rangle

||| Document `(brackets x)` encloses document `x` in square brackets,
||| "[" and "]".
public export
brackets : Doc -> Doc
brackets        = enclose lbracket rbracket

-----------------------------------------------------------
-- list, tupled and semiBraces pretty print a list of
-- documents either horizontally or vertically aligned.
-----------------------------------------------------------

||| The document `(encloseSep l r sep xs)` concatenates the documents
||| `xs` separated by `sep` and encloses the resulting document by `l`
||| and `r`. The documents are rendered horizontally if that fits the
||| page. Otherwise they are aligned vertically. All separators are put
||| in front of the elements. For example, the combinator 'list' can be
||| defined with `encloseSep`:
|||
||| > list xs = encloseSep lbracket rbracket comma xs
||| > test    = text "list" |++| (list (map int [10,200,3000]))
|||
||| Which is layed out with a page width of 20 as:
|||
||| ``
||| list [10,200,3000]
||| ``
|||
||| But when the page width is 15, it is layed out as:
|||
||| ``
||| list [10
|||      ,200
|||      ,3000]
||| ``
public export
encloseSep : Doc -> Doc -> Doc -> List Doc -> Doc
encloseSep left right sep ds
    = case ds of
        []  => left `beside` right
        [d] => left `beside` (d `beside` right)
        _   => align (cat (zipWithStreamL (beside) (left :: repeat sep) ds) `beside` right)

||| The document `(list xs)` comma separates the documents `xs` and
||| encloses them in square brackets. The documents are rendered
||| horizontally if that fits the page. Otherwise they are aligned
||| vertically. All comma separators are put in front of the
||| elements.
public export
list : List Doc -> Doc
list            = encloseSep lbracket rbracket comma

||| The document `(tupled xs)` comma separates the documents `xs`
||| and encloses them in parenthesis. The documents are rendered
||| horizontally if that fits the page. Otherwise they are aligned
||| vertically. All comma separators are put in front of the
||| elements.
public export
tupled : List Doc -> Doc
tupled          = encloseSep lparen   rparen  comma

||| The document `(semiBraces xs)` separates the documents `xs` with
||| semicolons and encloses them in braces. The documents are
||| rendered horizontally if that fits the page. Otherwise they are
||| aligned vertically. All semi colons are put in front of the
||| elements.
public export
semiBraces : List Doc -> Doc
semiBraces      = encloseSep lbrace   rbrace  semi

-----------------------------------------------------------
-- punctuate p [d1,d2,...,dn] => [d1 |+| p,d2 |+| p, ... ,dn]
-----------------------------------------------------------

||| `(punctuate p xs)` concatenates all documents in `xs` with
||| document `p` except for the last document.
|||
||| ```
||| > someText = map text ["words","in","a","tuple"]
||| > test     = parens (align (cat (punctuate comma someText)))
||| ```
|||
||| This is layed out on a page width of 20 as:
|||
||| ```
||| (words,in,a,tuple)
||| ```
|||
||| But when the page width is 15, it is layed out as:
|||
||| ```
||| (words,
|||  in,
|||  a,
|||  tuple)
||| ```
|||
||| (If you want put the commas in front of their elements instead of
||| at the end, you should use `tupled` or, in general, `encloseSep`.)
public export
punctuate : Doc -> List Doc -> List Doc
punctuate _ []      = []
punctuate _ [d]     = [d]
punctuate p (d::ds)  = (d |+| p) :: punctuate p ds

-----------------------------------------------------------
-- Combinators for prelude types
-----------------------------------------------------------

private
string' : List Char -> Doc
string' []        = empty
string' ('\n'::s) = line |+| string' s
string' (c::s)    = char c |+| string' s

||| The document `(string s)` concatenates all characters in `s`
||| using `line` for newline characters and `char` for all other
||| characters. It is used instead of 'text' whenever the text contains
||| newline characters.
public export
string : String -> Doc
string str = string' (unpack str)

public export
bool : Bool -> Doc
bool b          = text (show b)

||| The document `(int i)` shows the literal integer `i` using
||| 'text'.
public export
int : Int -> Doc
int i           = text (show i)

||| The document `(integer i)` shows the literal integer `i` using
||| 'text'.
public export
integer : Integer -> Doc
integer i       = text (show i)

public export
nat : Nat -> Doc
nat n = text (show n)

||| The document `(double d)` shows the literal double `d` using
||| 'text'.
public export
double : Double -> Doc
double d        = text (show d)

{-
-- | The document @(rational r)@ shows the literal rational @r@ using
-- 'text'.
rational : Rational -> Doc
rational r      = text (show r)
-}

-----------------------------------------------------------
-- Useful instances
-----------------------------------------------------------

||| Note that this operator is not associative with respect to
||| propositional equality of the underlying Doc syntax tree, but
||| rather with respect to the equality of the result of rendering. So
||| it's "morally" a `Semigroup`.
public export
Semigroup Doc where
  (<+>) = beside

||| Note that the neutral element is not a left and right unit with
||| respect to propositional equality of the underlying Doc syntax
||| tree, but rather with respect to the equality of the result of
||| rendering. So it's "morally" a `Monoid`.
public export
Monoid Doc where
  neutral = empty

-----------------------------------------------------------
-- semi primitive: fill and fillBreak
-----------------------------------------------------------

public export
width : Doc -> (Nat -> Doc) -> Doc
width d f       = column (\k1 => d |+| column (\k2 => f (minus k2 k1)))

||| The document `(fillBreak i x)` first renders document `x`. It
||| than appends `space`s until the width is equal to `i`. If the
||| width of `x` is already larger than `i`, the nesting level is
||| increased by `i` and a `line` is appended. When we redefine `ptype`
||| in the previous example to use `fillBreak`, we get a useful
||| variation of the previous output:
|||
||| > ptype (name,tp)
||| >        = fillBreak 6 (text name) |++| text ":" |++| text tp
|||
||| The output will now be:
|||
||| `
||| let empty  : Doc
|||     nest   : Int -> Doc -> Doc
|||     linebreak
|||            : Doc
||| `
public export
fillBreak : Int -> Doc -> Doc
fillBreak f x   = width x (\w =>
                  if (cast w > f) then nest f linebreak
                                  else text "")

||| The document `(fill i x)` renders document `x`. It than appends
||| `space`s until the width is equal to `i`. If the width of `x` is
||| already larger, nothing is appended. This combinator is quite
||| useful in practice to output a list of bindings. The following
||| example demonstrates this.
|||
||| > types  = [("empty","Doc")
||| >          ,("nest","Int -> Doc -> Doc")
||| >          ,("linebreak","Doc")]
||| >
||| > ptype (name,tp)
||| >        = fill 6 (text name) |++| text ":" |++| text tp
||| >
||| > test   = text "let" |++| align (vcat (map ptype types))
|||
||| Which is layed out as:
|||
||| `
||| let empty  : Doc
|||     nest   : Int -> Doc -> Doc
|||     linebreak : Doc
||| `
public export
fill : Nat -> Doc -> Doc
fill f d        = width d (\w =>
                  if (w >= f) then empty
                              else text (spaces (minus f w)))

-----------------------------------------------------------
-- Renderers
-----------------------------------------------------------

private
fits : Nat -> SimpleDoc -> Bool
fits w SEmpty                   = True
fits Z (SChar _ x)              = False
fits w (SChar _ x)              = fits (minus w 1) x
fits Z (SText l _ x)            = False
fits w (SText l _ x)            = fits (minus w l) x
fits w (SLine _ _)              = True

-----------------------------------------------------------
-- renderPretty: the default pretty printing algorithm
-----------------------------------------------------------

||| This is the default pretty printer which is used by 'show',
||| 'putDoc' and 'hPutDoc'. `(renderPretty ribbonfrac width x)` renders
||| document `x` with a page width of `width` and a ribbon width of
||| `(ribbonfrac * width)` characters. The ribbon width is the maximal
||| amount of non-indentation characters on a line. The parameter
||| `ribbonfrac` should be between `0.0` and `1.0`. If it is lower or
||| higher, the ribbon width will be 0 or `width` respectively.
public export
renderPretty : Double -> Nat -> Doc -> SimpleDoc
renderPretty rfrac w x
    = assert_total $ best 0 0 (Cons 0 x Nil)
    where
     ||| the ribbon width in characters
     r : Nat
     r  = let rDouble = cast w * rfrac
              rNat = integerToNat (cast rDouble)
          in max 0 (min w rNat)

     --nicest : r = ribbon width, w = page width,
     --          n = indentation of current line, k = current column
     --          x and y, the (simple) documents to chose from.
     --          precondition: first lines of x are longer than the first lines of y.
     nicest : Nat -> Nat -> SimpleDoc -> SimpleDoc -> SimpleDoc
     nicest n k x y =
       let width = min (minus w k) ((minus r k) + n) in
       if fits width x then x else y

     -- best : n = indentation of current line
     --         k = current column
     --        (ie. (k >= n) && (k - n == count of inserted characters)
     covering
     best : Nat -> Nat -> Docs -> SimpleDoc
     best _ _ Nil      = SEmpty
     best n k (Cons i d ds)
       = case d of
           Empty       => best n k ds
           Char' c     => let k' = k+1 in SChar c (best n k' ds)
           Text l s    => let k' = k+l in SText l s (best n k' ds)
           Line _      => SLine i (best i i ds)
           Cat x y     => best n k (Cons i x (Cons i y ds))
           Nest j x    => let i' = integerToNat (cast (cast i + j)) in best n k (Cons i' x ds)
           Union x y   => nicest n k (best n k (Cons i x ds))
                                     (best n k (Cons i y ds))

           Column f    => best n k (Cons i (f k) ds)
           Nesting f   => best n k (Cons i (f (cast i)) ds)

-----------------------------------------------------------
-- renderCompact: renders documents without indentation
--  fast and fewer characters output, good for machines
-----------------------------------------------------------

||| `(renderCompact x)` renders document `x` without adding any
||| indentation. Since no 'pretty' printing is involved, this
||| renderer is very fast. The resulting output contains fewer
||| characters than a pretty printed version and can be used for output
||| that is read by other programs.
covering
renderCompact : Doc -> SimpleDoc
renderCompact x
    = scan 0 [x]
    where
      covering
      scan : Nat -> List Doc -> SimpleDoc
      scan _ []     = SEmpty
      scan k (d::ds) = case d of
                        Empty       => scan k ds
                        Char' c     => let k' = k+1 in SChar c (scan k' ds)
                        Text l s    => let k' = k+l in SText l s (scan k' ds)
                        Line _      => SLine 0 (scan 0 ds)
                        Cat x y     => scan k (x::y::ds)
                        Nest _ x    => scan k (x::ds)
                        Union _ y   => scan k (y::ds)
                        Column f    => scan k (f k::ds)
                        Nesting f   => scan k (f 0::ds)

-----------------------------------------------------------
-- Displayers:  displayS and displayIO
-----------------------------------------------------------

||| `(displayS simpleDoc)` takes the output `simpleDoc` from a
||| rendering function and transforms it to a 'ShowS' type (for use in
||| the 'Show' class).
|||
||| > showWidth : Nat -> Doc -> String
||| > showWidth w x   = displayS (renderPretty 0.4 w x) ""
public export
displayS : SimpleDoc -> String -> String
displayS SEmpty             = id
displayS (SChar c x)        = strCons c . displayS x
displayS (SText _ s x)      = (s ++) . displayS x
displayS (SLine i x)        = (('\n' `strCons` indentation i) ++) . displayS x

{-
-- | `(displayIO handle simpleDoc)` writes `simpleDoc` to the file
-- handle `handle`. This function is used for example by 'hPutDoc':
--
-- > hPutDoc handle doc  = displayIO handle (renderPretty 0.4 100 doc)
displayIO : Handle -> SimpleDoc -> IO ()
displayIO handle simpleDoc
    = display simpleDoc
    where
      display SEmpty        = return ()
      display (SChar c x)   = do{ hPutChar handle c; display x}
      display (SText _ s x) = do{ hPutStr handle s; display x}
      display (SLine i x)   = do{ hPutStr handle ('\n'::indentation i); display x}
-}

-----------------------------------------------------------
-- default pretty printers: show, putDoc and hPutDoc
-----------------------------------------------------------
public export
Show Doc where
  show doc       = displayS (renderPretty 0.4 80 doc) ""

{-
||| The action `(putDoc doc)` pretty prints document `doc` to the
||| standard output, with a page width of 100 characters and a ribbon
||| width of 40 characters.
|||
||| > main : IO ()
||| > main = do{ putDoc (text "hello" |++| text "world") }
|||
||| Which would output
|||
||| `
||| hello world
||| `
putDoc : Doc -> IO ()
putDoc doc              = hPutDoc stdout doc

||| `(hPutDoc handle doc)` pretty prints document `doc` to the file
||| handle `handle` with a page width of 100 characters and a ribbon
||| width of 40 characters.
|||
||| > main = do{ handle <- openFile "MyFile" WriteMode
||| >          ; hPutDoc handle (vcat (map text
||| >                            ["vertical","text"]))
||| >          ; hClose handle
||| >          }
hPutDoc : Handle -> Doc -> IO ()
hPutDoc handle doc      = displayIO handle (renderPretty 0.4 80 doc)
-}

 --  LocalWords:  PPrint combinators Wadler Wadler's encloseSep
-- -}


text:
-- Originally developed at a solution to the kata at codewars:
-- https://www.codewars.com/kata/5c7fe5c859036f142eccaabb

module Sprintf

%access export
%default total

namespace SideThought

  public export total
  SprintfType : List Char -> Type
  SprintfType []                   =            String
  SprintfType ('%' :: '%' :: rest) =            SprintfType rest
  SprintfType ('%' :: 'd' :: rest) = Integer -> SprintfType rest
  SprintfType ('%' :: 'f' :: rest) = Double  -> SprintfType rest
  SprintfType ('%' :: 'c' :: rest) = Char    -> SprintfType rest
  SprintfType ('%' :: rest)        = Void    -> SprintfType rest
  SprintfType (_   :: rest)        =            SprintfType rest

public export
strToSty : (curr : String) -> (str : List Char) -> (t : Type ** t)
strToSty c []             = (_ ** c)
strToSty c ('%'::'%'::ks) = strToSty (c ++ "%") ks
strToSty c ('%'::'d'::ks) = (_ ** \n : Integer => snd $ strToSty (c ++ show n) ks)
strToSty c ('%'::'f'::ks) = (_ ** \x : Double  => snd $ strToSty (c ++ show x) ks)
strToSty c ('%'::'c'::ks) = (_ ** \k : Char    => snd $ strToSty (c ++ singleton k) ks)
strToSty c ('%':: ks)     = (_ ** \v : Void    => snd $ strToSty c ks)
strToSty c ( k :: ks)     = strToSty (c ++ singleton k) ks

sprintf : (str : String) -> fst $ strToSty "" $ unpack str
sprintf str = snd $ strToSty "" $ unpack str

max_stars_repo_name: buzden/code-in-lectures

max_issues_repo_name: buzden/code-in-lectures

max_forks_repo_name: buzden/code-in-lectures


text:
module Test.Lexer

import Test.Assertions
import Idrlisp.Lexer

%default covering

export
test : IO ()
test = describe "Idrlisp.Lexer" $ do
  describe "lex" $ do
    lex ""
      `shouldBe` Right []
    lex "    ; hello  \n\n  "
      `shouldBe` Right []
    lex "()"
      `shouldBe` Right [LPAREN, RPAREN]
    lex ")[(]"
      `shouldBe` Right [RPAREN, LBRACK, LPAREN, RBRACK]
    lex "#t.#f"
      `shouldBe` Right [TRUE, DOT, FALSE]
    lex "123"
      `shouldBe` Right [NUM 123]
    lex "3.14"
      `shouldBe` Right [NUM 3.14]
    lex "-16.5"
      `shouldBe` Right [NUM (-16.5)]
    lex "64e+3"
      `shouldBe` Right [NUM 64000]
    lex "foo"
      `shouldBe` Right [SYM "foo"]
    lex "hello-1world*"
      `shouldBe` Right [SYM "hello-1world*"]
    lex (show "Hello, World!")
      `shouldBe` Right [STR "Hello, World!"]
    lex (show "Escape\nsequence\tEscape\"sequence\\")
      `shouldBe` Right [STR "Escape\nsequence\tEscape\"sequence\\"]
    lex "`(foo ,bar ,@(hoge 'fuga))"
      `shouldBe` Right [QUASIQUOTE, LPAREN, SYM "foo", UNQUOTE, SYM "bar", UNQUOTE_SPLICING, LPAREN, SYM "hoge", QUOTE, SYM "fuga", RPAREN, RPAREN]

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
import Lightyear.Strings
import Network.Socket
import System
import Control.Monad.State
import Control.Monad.Trans
import System.Concurrency.Process

import HydraBot.Types
import HydraBot.IRCParsers
import HydraBot.NetworkUtils

||| Message processor out of a pure function
pureProc : (ProcID Message) -> (Message -> List Message) -> Process Message ()
pureProc w f = do
  m <- recv
  traverse (send w) (f m)
  pureProc w f

||| Message processor, IO and State included
sioProc : (ProcID Message) -> (x:s) -> (Message -> StateT s IO (List Message)) -> Process Message ()
sioProc w s f = do
  m <- recv
  (ml, s') <- Lift $ runStateT (f m) s
  traverse (send w) ml
  sioProc w s' f

||| Channel messages processor
sioChannel : (String -> String -> String -> StateT s IO (List String)) ->
           Message -> StateT s IO (List Message)
sioChannel f (Msg (Just (User u)) (Left "PRIVMSG") [c,msg]) = map (map (cmsg c)) $ f u c msg
sioChannel _ _ = pure []

||| Run sioChannel for prefixed commands
||| @w Writer process
||| @x Initial state
||| @p Command prefix
||| @f A function to wrap
sioCommand : (w: ProcID Message) -> (x:s) -> (p: String) ->
           (f: String -> String -> List String -> StateT s IO (List String)) ->
           IO (ProcID Message)
sioCommand w st p f = run . create $ sioProc w st (sioChannel f')
where
  f' : String -> String -> String -> StateT s IO (List String)
  f' u c m = if isPrefixOf p m
             then f u c (words $ pack $ unpack m \\ unpack p)
             else pure []

||| Writer process
||| @s A connected socket
writerProc : (s: Socket) -> Process Message ()
writerProc s = do
  m <- recv
  Lift . putStrLn $ "> " ++ show m
  Lift . sendLine s $ show m
  writerProc s

||| Reader process
||| @pl A list of processes for broadcast
||| @s A connected socket
readerProc : (pl: List (ProcID Message)) -> (s: Socket) -> Process Message ()
readerProc pl s = do
  line <- Lift $ recvTill s "\r\n"
  case line of
    Left err => Lift $ putStrLn $ "Socket error on recv: " ++ show err
    Right str => do
      Lift $ putStr $ "< " ++ str
      broadcast (parse message str)
      readerProc pl s
where
  broadcast : (Either String Message) -> Process Message ()
  broadcast (Left err) = Lift (putStrLn err)
  broadcast (Right msg) = do
    traverse (flip send msg) pl
    return ()

max_stars_repo_name: defanor/hydra-bot

max_issues_repo_name: defanor/hydra-bot

max_forks_repo_name: defanor/hydra-bot


text:
module Introduction

-- This is a simple comment

-- Import statements
import Data.Vect
import public Syntax.PreorderReasoning

-- All the functions/definitions in this module must be total.
-- Total definitions can be safely used in proofs and type level programming
-- %default total

data Day
  = Monday
  | Tuesday
  | Wednesday
  | Thursday
  | Friday
  | Saturday
  | Sunday

data Workday : Day -> Type where
  MondayW : Workday Monday
  TuesdayW : Workday Tuesday
  WednesdayW : Workday Wednesday
  ThursdayW : Workday Thursday
  FridayW : Workday Friday

-- test : Workday Monday
-- test = MondayW

-- test2 : Workday Tuesday
-- test2 = TuesdayW

total
printWorkday : (d : Day) -> {auto _ : Workday d} -> String
printWorkday Monday = ?printWorkday_rhs_1
printWorkday Tuesday = ?printWorkday_rhs_2
printWorkday Wednesday = ?printWorkday_rhs_3
printWorkday Thursday = ?printWorkday_rhs_4
printWorkday Friday = ?printWorkday_rhs_5

-- printWorkday Monday MondayW = "Monday"
-- printWorkday Tuesday TuesdayW = "Tuesday"
-- printWorkday Wednesday WednesdayW = "Wednesday"
-- printWorkday Thursday ThursdayW = "Thursday"
-- printWorkday Friday FridayW = "Friday"

max_stars_repo_name: andorp/PLFI

max_issues_repo_name: andorp/PLFI

max_forks_repo_name: andorp/PLFI


text:
module Main

import IdrisScript
import IdrisScript.Date

main : JS_IO ()
main = do
  current <- now
  if !(getDay current) == Friday
     then putStrLn' "It's Friday! I'm in love!"
     else putStrLn' "Meh!"

max_stars_repo_name: jimmyhmiller/IdrisScript

max_issues_repo_name: jimmyhmiller/IdrisScript

max_forks_repo_name: jimmyhmiller/IdrisScript


text:
module Primitives.Common

import Core.Context
import CairoCode.CairoCode
import CommonDef
import Data.SortedSet
import Data.SortedMap
import CodeGen.CodeGenHelper

-- This is a separate module to avoid cyclic dependencies

-- Currently simplified we may add information if necessary but I have the feeling this is enough
public export
data ValueInfo : Type where
     UnknownValue : ValueInfo
     ConstValue : CairoConst -> ValueInfo
     CompositeValue : (tag:Int) -> List ValueInfo -> ValueInfo
     ClosureValue : Name -> (missing:Nat) -> List ValueInfo -> ValueInfo

public export
data EvalRes : Type where
     Failure : String -> EvalRes
     NewValue : ValueInfo -> EvalRes
     ArgValue : Nat -> EvalRes

public export
data PrimFnCode = Instructions (List CairoInst) | Raw String

public export
interface PrimFn where
    apStable : Bool
    apStable = True

    implicits : SortedSet LinearImplicit
    implicits = empty

    imports : SortedSet Import
    imports = empty

    eval: List ValueInfo -> Maybe EvalRes

    dependencies : SortedMap Name (Lazy CairoDef)
    dependencies = empty

    generateCode : (res:CairoReg) -> (args:List CairoReg) -> LinearImplicitArgs -> PrimFnCode

export
makeBuiltinName : String -> Name
makeBuiltinName fnName = makeName "Builtin" fnName

export
generateMissingCodeError : String -> a
generateMissingCodeError name = assert_total $ idris_crash $ "Missing primop: " ++ name

export
pow2 : Nat -> Integer
pow2 nBits = product $ replicate nBits 2

-- Helpers
public export
toInt : Bool -> CairoConst
toInt True = I 1
toInt False = I 0

export
bitwiseBuiltinImport : Import
bitwiseBuiltinImport = MkImport "starkware.cairo.common.cairo_builtins" "BitwiseBuiltin"

-- This currently is ugly for things like if a == b then ... as it gens two ifs
--  But while eliminating it would be possible its not worth the trouble yet
--   For the record it would be over introducing (IF res function args ifcase elsecase) as Opcode
-- compileCairoInst _ (OP r linImpls (EQ _) [a,b]) = compileEqOp a b linImpls r
export
compileEqOp : String -> CairoReg -> List CairoReg -> LinearImplicitArgs -> String
compileEqOp primFnName reg [a,b] linImpls =
  if linImpls == empty
    then """
      if \{ compileReg a } == \{ compileReg b }:
        \{compileNestRegDecl reg} = 1
      else:
        \{compileNestRegDecl reg} = 0
      end

    """
    else assert_total $ idris_crash "no implicits expected for Eq \{primFnName}"
compileEqOp primFnName _ _ _ = assert_total $ idris_crash "Bad arguments to generateCode compileEqOp \{primFnName}"

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Numbers

%default total

data MyNat : Type where
     MyZ : MyNat
     MyS : MyNat -> MyNat

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

minDos : Nat -> Nat
minDos Z = Z
minDos (S k) = Z
minDos (S (S k)) = k

evenb : Nat -> Bool
evenb Z = True
evenb (S (S k)) = evenb k
evenb (S k) = False
-- can also pattern match on (and have it as the 1st or 2nd option):
-- evenb (S Z) = False

oddb : Nat -> Bool
oddb = not . evenb

todd1 : oddb 1 = True
todd1 = Refl
todd2 : oddb 4 = False
todd2 = Refl

myPlus : Nat -> Nat -> Nat
myPlus Z b = b
myPlus (S k) b = S (myPlus k b)

myMult : Nat -> Nat -> Nat
myMult Z b = Z
myMult (S k) b = myPlus b (myMult k b)

tM1 : (mult 3 3) = 9
tM1 = Refl

myMinus : (uno, dos : Nat) -> Nat
myMinus Z _ = Z
myMinus a Z = a
myMinus (S k) (S j) = myMinus k j

tmi1 : (myMinus 5 3) = 2
tmi1 = Refl
tmi2 : (myMinus 0 2352) = 0
tmi2 = Refl

myExp : Nat -> Nat -> Nat
myExp _ Z = 1
myExp b (S j) = myMult b (myExp b j)

tme1 : (myExp 2 3) = 8
tme1 = Refl
tme2 : (myExp 5 2) = 25
tme2 = Refl


text:
data PowerSource = Petrol | Pedal | Electric

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

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

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

bmw : Vehicle Petrol
bmw = Car 20

cube : Vehicle Pedal
cube = Bicycle

let x = refuel bmw
let y = refuel cube

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Data.Hashable.Lifted

import Data.Vect

import Data.Hashable

infixl 10 `hashWithSalt1`

||| Interface for higher-kinded types that can be hashed, if the element they contain can be hashed.
public export
interface Hashable1 t where
    hashWithSalt1 : (Bits64 -> a -> Bits64) -> Bits64 -> t a -> Bits64

export
Hashable a => Hashable1 t => Hashable (t a) where
    hashWithSalt = hashWithSalt1 hashWithSalt

||| Hashable implementation for any foldable.
export
[Hashable1Foldable] Foldable t => Hashable1 t where
    hashWithSalt1 hws s xs = finalise (foldl step (s, 0) xs)
      where
        step : (Bits64, Bits64) -> a -> (Bits64, Bits64)
        step (s, l) x = (hws s x, l + 1)
        finalise : (Bits64, Bits64) -> Bits64
        finalise (s, l) = hashWithSalt s l

export
Hashable1 Maybe where
    hashWithSalt1 hws s Nothing = s
    hashWithSalt1 hws s (Just x) = 1 `hashWithSalt` s `hws` x

export
Hashable1 List where
    hashWithSalt1 = hashWithSalt1 @{Hashable1Foldable}

export
Hashable1 (Vect len) where
    hashWithSalt1 = hashWithSalt1 @{Hashable1Foldable}


text:
module OrderDefs

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

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

import LuaCommon

-- Borrowed from the Node backend
mutual
  ||| Returns all names referenced within the given expression.
  ||| Names are not chased down transitivily.
  export
  usedNames : NamedCExp -> SortedSet Name
  usedNames (NmLocal fc n) = empty
  usedNames (NmRef fc n) = insert n empty
  usedNames (NmLam fc n e) = usedNames e
  usedNames (NmApp fc x args) = usedNames x `union` concat (usedNames <$> args)
  usedNames (NmPrimVal fc c) = empty
  usedNames (NmOp fc op args) = concat $ usedNames <$> args
  usedNames (NmConCase fc sc alts def) = (usedNames sc `union` concat (usedNamesConAlt <$> alts)) `union` maybe empty usedNames def
  usedNames (NmConstCase fc sc alts def) = (usedNames sc `union` concat (usedNamesConstAlt <$> alts)) `union` maybe empty usedNames def
  usedNames (NmExtPrim fc p args) = concat $ usedNames <$> args
  usedNames (NmCon fc x _ t args) = concat $ usedNames <$> args
  usedNames (NmDelay fc _ t) = usedNames t
  usedNames (NmForce fc _ t) = usedNames t
  usedNames (NmLet fc x val sc) = usedNames val `union` usedNames sc
  usedNames (NmErased fc) = empty
  usedNames (NmCrash fc msg) = empty

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

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

||| Returns all names referenced within the given definition.
||| Names are not chased down transitivily.
usedNamesDef : NamedDef -> SortedSet Name
usedNamesDef (MkNmFun args exp) = usedNames exp
usedNamesDef (MkNmError exp) = usedNames exp
usedNamesDef (MkNmForeign cs args ret) = empty
usedNamesDef (MkNmCon _ _ _) = empty

||| For each definition finds names referenced within it.
export
defsToUsedMap : List (Name, NamedDef) -> SortedMap Name (NamedDef, SortedSet Name)
defsToUsedMap defs =
  fromList $ (\(n, d) => (n, (d, usedNamesDef d))) <$> defs

||| The first argument is for local storage. Initialized with the empty set.
||| The second argument is a map from names to their dependencies.
||| The third argument is a set of names
||| Returns a set of names that the given names depend on.
calcUsed : SortedSet Name -> SortedMap Name (NamedDef, SortedSet Name) -> List Name -> SortedSet Name
calcUsed done d [] = done
calcUsed done d xs =
  let used_in_xs = foldl (\x, y => union x (fromMaybe empty (snd <$> y))) empty $ (\z => lookup z d) <$> xs
      new_done   = union done (fromList xs)
  in calcUsed (new_done) d (SortedSet.toList $ difference used_in_xs new_done)

calcUsedDefs : List Name -> SortedMap Name (NamedDef, SortedSet Name) -> List (Name, (NamedDef, SortedSet Name))
calcUsedDefs names usedMap =
  let usedNames = calcUsed empty usedMap names
  in List.filter (\(n, _) => contains n usedNames) (toList usedMap)

export
defsUsedByNamedCExp : NamedCExp -> SortedMap Name (NamedDef, SortedSet Name) -> List (Name, NamedDef)
defsUsedByNamedCExp exp usedMap = map (mapSnd fst) $ calcUsedDefs (SortedSet.toList $ usedNames exp) usedMap

export
used : (Name, NamedDef) -> SortedMap Name (NamedDef, SortedSet Name) -> SortedSet Name
used (n, _) usedMap = fromList $ map fst $ calcUsedDefs [n] usedMap

public export
interface MaybeRelated t r where
  mbRelated : (a : t) -> (b : t) -> Maybe (a `r` b)

contains : SortedSet a -> a -> Bool
contains = flip SortedSet.contains

%hide SortedSet.contains

-- `x` <= `y`: ?reflexive, transitive, antisymmetric relation. Forms a total order
public export
data Lte : (defs : SortedMap Name (NamedDef, SortedSet Name)) -> (x : (Name, NamedDef)) -> (y : (Name, NamedDef)) -> Type where
  MkLte : {x, y, defs : _} ->
          let a = contains (used y defs) (fst x)
              b = contains (used x defs) (fst y)
          in  (0 prf : Either (So a, So $ not b) $ Either (So a, So b) (So $ not a, So $ not b))
           -> Lte defs x y

public export
{defs : _} -> MaybeRelated _ (Lte defs) where
  mbRelated x y
   = let
       a : Bool
       a = contains (used y defs) (fst x)
       b : Bool
       b = contains (used x defs) (fst y)
     in
       case (choose a, choose b) of
         (Left isA, Right notB) => Just $ MkLte (Left (isA, notB))
         (Left isA, Left isB) => Just $ MkLte (Right $ Left (isA, isB))
         (Right notA, Right notB) => Just $ MkLte (Right $ Right (notA, notB))
         _ => Nothing

public export
quicksort : {defs : SortedMap Name (NamedDef, SortedSet Name)} -> List (Name, NamedDef) -> List (Name, NamedDef)
quicksort (y :: xs)
 = let (lte, gt) = partition (\x => isJust $ mbRelated {r = Lte defs} x y) xs in
    quicksort {defs} lte ++ (y :: quicksort {defs} gt)
quicksort [] = []


text:
||| Simple GADTs for F#
module Sg4f

%default total
%access public export

mutual
  ||| A term in the language
  ||| universe 0 - values
  ||| universe 1 - types
  ||| universe 2 - kinds
  ||| universe 2 - sorts
  data Term : (universe : Nat) -> Type where
    ||| A named term
    NamedTerm : Name u -> Term u
    ||| Function application
    Appl : (f : Func u t) -> (a : TypedTerm u t) -> Term u
    ||| Type constructor operator. Its terms cannot be values.
    Arrow : Term (S u) -> Term (S u) -> Term (S u)

  ||| A function term
  ||| Func is parameterized by the type of its input; thus, we must go down a
  ||| universe from its input to get its universe
  data Func : (universe : Nat) -> Term (S universe) -> Type where
    ||| The input and output type of the constructor
    Ctr : String -> (t : Term (S u)) -> Term (S u) -> Func u t

  data TypedTerm : (universe : Nat) -> Term (S universe) -> Type where
    TermWithType : (t : Term u) -> TypedTerm u (GetType t)

  ||| An actual name of a term
  data Name : (universe : Nat) -> Type where
    ||| The name of Type in any universe starting with 2 (since the lowest Type
    ||| has as its type Kind).
    Tau : Name (S (S n))
    ||| A primitive type or type constructor in universe one, opaque to the
    ||| source language because taken for granted as existing in the target
    ||| language. Syntax:
    |||   primitive string : Type
    |||   primitive Maybe : Type -> Type
    |||   primitive Either : Type -> Type -> Type
    ||| The term in universe two is the type of the primitive: all primitives
    ||| have a type of Type or of some type constructor, which are kinds, so it
    ||| is in universe two.
    PrimType : String -> Term 2 -> Name 1
    NamedFun : Func u t -> Name u

  ||| Get the type of some term. Returns a term in the next unvierse up.
  GetType : Term u -> Term (S u)
  GetType (NamedTerm Tau) = NamedTerm Tau
  GetType (NamedTerm (PrimType _ t)) = t
  GetType (NamedTerm (NamedFun (Ctr _ t x))) = Arrow t x
  GetType (Appl (Ctr _ _ z) _) = z
  GetType (Arrow x y) = NamedTerm Tau

funcName : Func u t -> String
funcName (Ctr x _ _) = x

||| Get the name of the type or type constructor
typeName : Name u -> String
typeName {u = (S (S Z))} Tau = "Type"
typeName {u = (S (S (S Z)))} Tau = "Kind"
typeName {u = (S (S (S (S Z))))} Tau = "Sort"
typeName {u = (S (S (S (S (S _)))))} Tau = "Why asketh thou such things?"
typeName (PrimType x _) = x
typeName (NamedFun f) = funcName f

Show (Term u) where
  show (NamedTerm x) = typeName x
  show (Appl f (TermWithType t)) = funcName f ++ " " ++ show t
  show (Arrow x y) = show x ++ " -> " ++ show y

showWithType : Term u -> String
showWithType t = show t ++ " : " ++ show (GetType t)


text:
module Mod

export
fn : Nat -> Nat
fn x = S x