text:
module Light

import public Lightyear

import Data.String

import Effects
import Effect.Exception
import Effect.State

import MiniParser
import Types

isBound : String -> Eff Bool [STATE Env]
isBound var = case (lookup var !get) of
                   Nothing => pure False
                   Just _  => pure True

getVar : String -> Eff Val [STATE Env, EXCEPTION Error]
getVar var = case lookup var !get of
                  Nothing => raise $ UnboundVar "unbound variable" var
                  Just val => pure val

-- update var `n` with v
updateList : String -> Val -> List (String, Val) -> List (String, Val)
updateList n v ls = map set ls
                   where
                    set : (String, Val) -> (String, Val)
                    set (a, b) = if a == n
                                 then (a, v)
                                 else (a, b)

addToList : String -> Val -> List (String, Val) -> List (String, Val)
addToList n v ls = (n, v) :: ls

setVar : String -> Val -> Eff Val [STATE Env, EXCEPTION Error]
setVar var val = case lookup var !get of
                      Nothing => raise $ UnboundVar "unbound variable" var
                      Just v => do update (updateList var v)
                                   pure val

defineVar : String -> Val -> Eff Val [STATE Env, EXCEPTION Error]
defineVar var val = do case !(isBound var) of
                            True => pure !(setVar var val)
                            False => do update (addToList var val)
                                        pure val

bindVars : List (String, Val) -> Eff Env [STATE Env]
bindVars bindings = do update (++ bindings)
                       pure !get

readExpr : String -> Eff Val [EXCEPTION Error]
readExpr str = case parse parseExpr str of
                   Left err => raise $ ParserE err
                   Right v  => pure v

toVect2' : List Val -> Maybe (Vect 2 Val)
toVect2' [x, y] = Just (fromList [x, y])
toVect2' _      = Nothing

toVect2 : List Val -> ThrowsError (Vect 2 Val)
toVect2 ls = maybeToEither (NumArgs 2 ls) (toVect2' ls)

unpackNum : Val -> ThrowsError Integer
-- unpackNum (A x)    = ?unpackNum_rhs_1
unpackNum (L [n])  = unpackNum n
-- unpackNum (D xs x) = ?unpackNum_rhs_3
unpackNum (N n)    = Right $ n
unpackNum (S n)    = maybeToEither (TypeMismatch "number" (S n)) $ parseInteger n -- todo
-- unpackNum (B x)    = ?unpackNum_rhs_6
unpackNum notNum   = Left $ TypeMismatch "number" notNum

unpackStr : Val -> ThrowsError String
unpackStr (S s)      = Right s
unpackStr (N s)      = Right $ show s
unpackStr (B s)      = Right $ show s
unpackStr notString  = Left $ TypeMismatch "string" notString

unpackBool : Val -> ThrowsError Bool
unpackBool (B b) = Right b
unpackBool notBool  = Left $ TypeMismatch "boolean" notBool

boolBinop : (unpacker : Val -> ThrowsError a) -> (a -> a -> Bool) -> Vect 2 Val -> ThrowsError Val
boolBinop unpacker op args = do left <- unpacker $ head args
                                right <- unpacker $ last args
                                pure $ B $ left `op` right

numBoolBinop : (Integer -> Integer -> Bool) -> List Val -> ThrowsError Val
numBoolBinop op ls = toVect2 ls >>= boolBinop unpackNum op

strBoolBinop : (String -> String -> Bool) -> List Val -> ThrowsError Val
strBoolBinop op ls = toVect2 ls >>= boolBinop unpackStr op

boolBoolBinop : (Bool -> Bool -> Bool) -> List Val -> ThrowsError Val
boolBoolBinop op ls = toVect2 ls >>= boolBinop unpackBool op

numericBinop : (Integer -> Integer -> Integer) -> List Val -> ThrowsError Val
numericBinop op params = (liftA N) $ foldl1 (liftA2 op) $ map unpackNum params

car : List Val -> ThrowsError Val
car [L (x :: xs)]   = pure x
car [D (x :: xs) _] = pure x
car [badArg]        = Left $ TypeMismatch "pair" badArg
car badArgList      = Left $ NumArgs 1 badArgList

cdr : List Val -> ThrowsError Val
cdr [L (x :: xs)]   = pure $ L xs
cdr [D [_] x]       = pure x
cdr [D (_ :: xs) x] = pure $ D xs x
cdr [badArg]        = Left $ TypeMismatch "pair" badArg
cdr badArgList      = Left $ NumArgs 1 badArgList

cons : Vect 2 Val -> ThrowsError Val
cons [x1, L []]      = pure $ L [x1]
cons [x, L xs]       = pure $ L $ x :: xs
cons [x, D xs xlast] = pure $ D (x :: xs) xlast
cons [x1, x2]        = pure $ D [x1] x2

eqv : Vect 2 Val -> ThrowsError Val
eqv [(B arg1), (B arg2)] = pure $ B $ arg1 == arg2
eqv [(N arg1), (N arg2)] = pure $ B $ arg1 == arg2
eqv [(S arg1), (S arg2)] = pure $ B $ arg1 == arg2
eqv [(A arg1), (A arg2)] = pure $ B $ arg1 == arg2
eqv [(D xs x), (D ys y)] = eqv [L $ xs ++ [x], L $ ys ++ [y]]
eqv [(L arg1), (L arg2)] = pure $ B $ (length arg1 == length arg2) && (all eqvPair $ zip arg1 arg2)
                           where eqvPair (x1, x2) = case eqv [x1, x2] of
                                                         Left err => False
                                                         Right (B v) => v
eqv [_, _]               = pure $ B False

-- equal? and Weak Typing: Heterogenous Lists[edit]
-- equal : List Val -> ThrowsError Val

-- non-lazy version of (&&)
and : Bool -> Bool -> Bool
and True x  = x
and False _ = False

-- non-lazy version of (||)
or : Bool -> Bool -> Bool
or False x = x
or True _  = True

infixr 1 >=>
(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
(>=>) f g = \x => f x >>= g

primitives : List (String, List Val -> ThrowsError Val)
primitives = [("+", numericBinop (+)),
              ("-", numericBinop (-)),
              ("*", numericBinop (*)),
              ("/", numericBinop div),
              ("mod", numericBinop mod),
              ("quotient", numericBinop divBigInt),
              ("remainder", numericBinop modBigInt),
              ("=", numBoolBinop (==)),
              ("<", numBoolBinop (<)),
              (">", numBoolBinop (>)),
              ("/=", numBoolBinop (/=)),
              (">=", numBoolBinop (>=)),
              ("<=", numBoolBinop (<=)),
              ("&&", boolBoolBinop and),
              ("||", boolBoolBinop or),
              ("string=?", strBoolBinop (==)),
              ("string<?", strBoolBinop (<)),
              ("string>?", strBoolBinop (>)),
              ("string<=?", strBoolBinop (<=)),
              ("string>=?", strBoolBinop (>=)),
              ("car", car),
              ("cdr", cdr),
              ("cons", toVect2 >=> cons),
              ("eqv?", toVect2 >=> eqv),
              ("eq?", toVect2 >=> eqv)]

applyFunc : (func : String) -> (args : List Val) -> Eff Val [EXCEPTION Error]
applyFunc func args = maybe (raise $ NotFunction "Unrecognized primitive function" func)
                            (\op => case op args of
                                         Right v => pure v
                                         Left e => raise e)
                            $ List.lookup func primitives

eval' : Val -> Eff Val [STATE Env, EXCEPTION Error]
eval' val@(S x) = pure $ val
eval' val@(N x) = pure $ val
eval' val@(B x) = pure $ val
eval' (A id)    = getVar id
eval' (L [A "if", pred, conseq, alt]) = do result <- eval' pred
                                           case result of
                                                B False   => eval' alt
                                                otherwise => eval' conseq
eval' (L [A "set!", A var, form]) = setVar var !(eval' form)
eval' (L [A "define", A var, form]) = defineVar var !(eval' form)
eval' (L (A func :: args)) = do args' <- mapEff eval' args
                                applyFunc func args'
                             where mapEff : (f : Val -> Eff Val [STATE Env, EXCEPTION Error]) -> List Val -> Eff (List Val) [STATE Env, EXCEPTION Error]
                                   mapEff f []        = pure []
                                   mapEff f (x :: xs) = do x' <- f x
                                                           pure $ x' :: !(mapEff f xs)
eval' badForm = raise $ BadSpecialForm "Unrecognized special form" badForm

eval : Val -> Eff Val [EXCEPTION Error]
eval (L [A "if", pred, conseq, alt]) = do
                                         result <- eval pred
                                         case result of
                                              B False   => eval alt
                                              otherwise => eval conseq
-- eval (A x) = ?eval_rhs_1 -- todo
eval (L [A "quote", val]) = pure val
eval (L (A func :: args)) = do
                              args' <- mapEff eval args
                              applyFunc func args'
                            where
                              mapEff : (eval : Val -> Eff Val [EXCEPTION Error]) -> List Val -> Eff (List Val) [EXCEPTION Error]
                              mapEff eval []        = pure []
                              mapEff eval (x :: xs) = do x' <- eval x
                                                         pure $ x' :: !(mapEff eval xs)
-- eval (D xs x) = ?eval_rhs_3 -- todo
eval val@(N x) = pure $ val
eval val@(S x) = pure $ val
eval val@(B x) = pure $ val
eval badForm   = raise $ BadSpecialForm "Unrecognized special form" badForm

export
evaluate : String -> Eff Val [STATE Env, EXCEPTION Error]
evaluate expr = eval' !(readExpr expr)


text:
data Vect : Nat -> Type -> Type where
     Nil  : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case m == len of
                                 False => Nothing
                                 True => Just ?input

data EqNat : Nat -> Nat -> Type where
     Same : (x : Nat) -> EqNat x x

sameS : (k : Nat) -> (j : Nat) -> (eq : EqNat k j) -> EqNat (S k) (S j)
sameS k k (Same k) = Same (S k)

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just (Same Z)
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Nothing => Nothing
                              Just eq => Just (sameS _ _ eq)

{-
exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case checkEqNat m len of
                                 Nothing => Nothing
                                 Just (Same _) => Just ?input
--                                 Just (Same m) => Just input

-}

ext: idr

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


text:
module Web.Raw.Visibility

import JS
import Web.Internal.VisibilityPrim
import Web.Internal.Types

%default total


text:
module Main

import Data.Vect

-- foldr (::) [] converts to lists
foldToList : (Foldable t) => t a -> List a
foldToList = foldr (::) []

showTestLine : List Int -> Vect n Int -> IO ()
showTestLine xs ys =
  putStrLn $ "(" ++
    show xs ++ ", " ++
    show ys ++ ") " ++
    "-> (" ++
    show (foldToList xs) ++ ", " ++
    show (foldToList ys) ++ ")"

main : IO ()
main = do
  showTestLine [] []
  showTestLine [1] [1]
  showTestLine [1, 2, 3] [1, 2, 3]
  showTestLine [3, 2, 1] [3, 2, 1]

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
module xquant.Spinor.BKS

import Data.Vect
import xquant.Spinor.Sigmas
import xquant.Spinor.SigKets

%default total

-----------------------------------------------------------------------
--                           Commutation
-----------------------------------------------------------------------

||| Individual Pauli operators commute iff they are identical up to a phase,
||| or if one of them is the identity
data PauliComm : Pauli -> Pauli -> Type where
  PSame    : (p : Pauli) -> PauliComm p  p
  PIdRight : (p : Pauli) -> PauliComm p  SI
  PIdLeft  : (p : Pauli) -> PauliComm SI p

||| Pauli operators do not commute iff they are not identical up to a phase,
||| and one of them isn't the identity
data PauliNonComm : Pauli -> Pauli -> Type where
  NonCommXY : PauliNonComm SX SY
  NonCommYZ : PauliNonComm SY SZ
  NonCommZX : PauliNonComm SZ SX
  NonCommSwap : PauliNonComm q w -> PauliNonComm w q

||| Decide whether two Pauli operators commute or not
decCommPauli : (x : Pauli) -> (y : Pauli) -> Either (PauliComm x y) (PauliNonComm x y)
decCommPauli SI p  = Left $ PIdLeft p
decCommPauli p  SI = Left $ PIdRight p
decCommPauli SX SX = Left $ PSame SX
decCommPauli SY SY = Left $ PSame SY
decCommPauli SZ SZ = Left $ PSame SZ
decCommPauli SX SY = Right $ NonCommXY
decCommPauli SY SX = Right $ NonCommSwap NonCommXY
decCommPauli SY SZ = Right $ NonCommYZ
decCommPauli SZ SY = Right $ NonCommSwap NonCommYZ
decCommPauli SZ SX = Right $ NonCommZX
decCommPauli SX SZ = Right $ NonCommSwap NonCommZX

mutual
  ||| A pair of commuting Sigma operators is formed by prepending a pair of commuting Paulis
  ||| onto a pair of commuting Sigmas, or by prepending a pair of non-commuting Paulis onto
  ||| a pair of non-commuting Sigmas. Sigmas of level zero (pure numbers) trivially commute.
  data Commuting : Sigma n -> Sigma n -> Type where
    CommPhase : {s1,s2 : Sigma Z} -> Commuting s1 s2
    CommSame  : PauliComm    j k -> Commuting    g h -> Commuting (Sig j g) (Sig k h)
    CommDiff  : PauliNonComm j k -> NonCommuting g h -> Commuting (Sig j g) (Sig k h)

  ||| A pair of non-commuting Sigma operators is formed by prepending a pair of commuting Paulis
  ||| onto a pair of non-commuting Sigmas, or by prepending a pair of non-commuting Paulis onto
  ||| a pair of commuting Sigmas.
  data NonCommuting : Sigma n -> Sigma n -> Type where
    NoCommSame : PauliNonComm j k -> Commuting    g h -> NonCommuting (Sig j g) (Sig k h)
    NoCommDiff : PauliComm    j k -> NonCommuting g h -> NonCommuting (Sig j g) (Sig k h)

||| Decide whether two Sigma operators commute or not
decComm : (x : Sigma n) -> (y : Sigma n) -> Either (Commuting x y) (NonCommuting x y)
decComm (sPhase p1) (sPhase p2) = Left CommPhase
decComm (Sig p1 s1) (Sig p2 s2) with (decComm s1 s2)
  decComm (Sig p1 s1) (Sig p2 s2) | commPrf with (decCommPauli p1 p2)
    decComm (Sig p1 s1) (Sig p2 s2) | Left cm  | Left  cmp = Left  $ CommSame cmp cm
    decComm (Sig p1 s1) (Sig p2 s2) | Left cm  | Right ncp = Right $ NoCommSame ncp cm
    decComm (Sig p1 s1) (Sig p2 s2) | Right nc | Left  cmp = Right $ NoCommDiff cmp nc
    decComm (Sig p1 s1) (Sig p2 s2) | Right nc | Right ncp = Left  $ CommDiff ncp nc

commTest : Vect n (Sigma m) -> Bool
commTest []        = True
commTest (x :: xs) = all (commute x) xs && (commTest xs)

data MutuallyCommuting : Vect n (Sigma m) -> Type where
  IsMutuallyCommuting : (v : Vect n $ Sigma m) ->
                        commTest v = True ->
                        MutuallyCommuting v

data CommStatus : (x : Sigma n) -> (y : Sigma n) -> Type where
  Status_Comm   : Commuting    x y -> CommStatus x y
  Status_NoComm : NonCommuting x y -> CommStatus x y

-----------------------------------------------------------------------
--        Even Parity (for each subspace & generator) datatype
-----------------------------------------------------------------------

data Parity = Even | Odd

data PauliParity = PParity Parity Parity Parity

swap : Parity -> Parity
swap Even = Odd
swap Odd  = Even

updateP : Pauli -> PauliParity -> PauliParity
updateP SX (PParity x y z) = PParity (swap x) y z
updateP SY (PParity x y z) = PParity x (swap y) z
updateP SZ (PParity x y z) = PParity x y (swap z)
updateP SI p               = p

updateParity : Sigma n -> Vect n PauliParity -> Vect n PauliParity
updateParity (sPhase ph) []      = []
updateParity (Sig pl s)  (p::ps) = (updateP pl p) :: (updateParity s ps)

||| Sets of Sigma n operators can be classified by whether each Sigma occurs
||| an even or odd number of times in each single-qubit Hilbert Space
data SigmaParity : Vect n (Sigma m) -> Vect m PauliParity -> Type where
  ParityZero : {m : Nat} -> SigmaParity [] (replicate m $ PParity Even Even Even)
  ParityNext : {v : Vect n (Sigma m)} ->
               (s : Sigma m) ->
               SigmaParity v p ->
               SigmaParity (s::v) (updateParity s p)

data EvenParity : Vect n (Sigma m) -> Type where
  IsEven : {v : Vect n (Sigma m)} ->
           SigmaParity v (replicate m $ PParity Even Even Even) ->
           EvenParity v

evenParity : (n : Nat) -> Vect n PauliParity
evenParity n = replicate n $ PParity Even Even Even

-----------------------------------------------------------------------
--               Multiply-to-Negative-Identity datatype
-----------------------------------------------------------------------

data NegId : Vect n (Sigma m) -> Type where
  IsNegId : (v : Vect (S n) (Sigma m)) ->
            foldr1 (<>) v = negId m ->
            NegId v

-----------------------------------------------------------------------
--                      BKS Theorem datatype
-----------------------------------------------------------------------

data BKS : Vect n (Sigma m) -> Type where
  MkBKS : MutuallyCommuting v ->
          NegId v ->
          EvenParity v ->
          BKS v

-----------------------------------------------------------------------
--      5-qubit BKS proof of David DiVincenzo & Asher Peres
-----------------------------------------------------------------------

zzzzz : Sigma 5
zzzzz = sZ <&> sZ <&> sZ <&> sZ <&> sZ

zxIIx : Sigma 5
zxIIx = sZ <&> sX <&> sI <&> sI <&> sX

xzxII : Sigma 5
xzxII = sX <&> sZ <&> sX <&> sI <&> sI

IxzxI : Sigma 5
IxzxI = sI <&> sX <&> sZ <&> sX <&> sI

IIxzx : Sigma 5
IIxzx = sI <&> sI <&> sX <&> sZ <&> sX

xIIxz : Sigma 5
xIIxz = sX <&> sI <&> sI <&> sX <&> sZ

Asher_David : Vect 6 (Sigma 5)
Asher_David = [zzzzz,
               zxIIx,
               xzxII,
               IxzxI,
               IIxzx,
               xIIxz]

Asher_David_Commuting : MutuallyCommuting Asher_David
Asher_David_Commuting = IsMutuallyCommuting Asher_David Refl

Asher_David_NegId : NegId Asher_David
Asher_David_NegId = IsNegId Asher_David Refl

Asher_David_Parity : SigmaParity Asher_David $ evenParity 5
Asher_David_Parity = ParityNext zzzzz $
                     ParityNext zxIIx $
                     ParityNext xzxII $
                     ParityNext IxzxI $
                     ParityNext IIxzx $
                     ParityNext xIIxz ParityZero

Asher_David_EvenParity : EvenParity Asher_David
Asher_David_EvenParity = IsEven Asher_David_Parity

Asher_David_BKS : BKS Asher_David
Asher_David_BKS = MkBKS Asher_David_Commuting Asher_David_NegId Asher_David_EvenParity

-----------------------------------------------------------------------
--       4-qubit BKS proof of Aravind-Chryssanthacopoulos-Harvey
-----------------------------------------------------------------------

xxxx : Sigma 4
xxxx = sX <&> sX <&> sX <&> sX

xxzz : Sigma 4
xxzz = sX <&> sX <&> sZ <&> sZ

zxxz : Sigma 4
zxxz = sZ <&> sX <&> sX <&> sZ

zxzx : Sigma 4
zxzx = sZ <&> sX <&> sZ <&> sX

Aravind : Vect 4 (Sigma 4)
Aravind = [xxxx,
           xxzz,
           zxxz,
           zxzx]

Aravind_Commuting : MutuallyCommuting Aravind
Aravind_Commuting = IsMutuallyCommuting Aravind Refl

Aravind_NegId : NegId Aravind
Aravind_NegId = IsNegId Aravind Refl

Aravind_Parity : SigmaParity Aravind $ evenParity 4
Aravind_Parity = ParityNext xxxx $
                 ParityNext xxzz $
                 ParityNext zxxz $
                 ParityNext zxzx ParityZero

Aravind_Even_Parity : EvenParity Aravind
Aravind_Even_Parity = IsEven Aravind_Parity

Aravind_BKS : BKS Aravind
Aravind_BKS = MkBKS Aravind_Commuting Aravind_NegId Aravind_Even_Parity

max_stars_repo_name: fieldstrength/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module Protocol.IDE.Decoration

import Protocol.SExp

%default total

public export
data Decoration : Type where
  Comment   : Decoration
  Typ       : Decoration
  Function  : Decoration
  Data      : Decoration
  Keyword   : Decoration
  Bound     : Decoration
  Namespace : Decoration
  Postulate : Decoration
  Module    : Decoration

public export
Eq Decoration where
  Comment   == Comment   = True
  Typ       == Typ       = True
  Function  == Function  = True
  Data      == Data      = True
  Keyword   == Keyword   = True
  Bound     == Bound     = True
  Namespace == Namespace = True
  Postulate == Postulate = True
  Module    == Module    = True
  _         == _         = False

public export
Show Decoration where
  show Comment   = "comment"
  show Typ       = "type"
  show Function  = "function"
  show Data      = "data"
  show Keyword   = "keyword"
  show Bound     = "bound"
  show Namespace = "namespace"
  show Postulate = "postulate"
  show Module    = "module"

export
SExpable Decoration where
  toSExp decor = SExpList [ SymbolAtom "decor"
                          , SymbolAtom (show decor)
                          ]
  where
    {- This definition looks like it repeats `Show`, but `display` is part
       of the IDE protocol, whereas the `Show` instance doesn't have to be.
    -}
    display : Decoration -> String
    display Comment   = "comment"
    display Typ       = "type"
    display Function  = "function"
    display Data      = "data"
    display Keyword   = "keyword"
    display Bound     = "bound"
    display Namespace = "namespace"
    display Postulate = "postulate"
    display Module    = "module"

export
FromSExpable Decoration where
  fromSExp (SExpList [SymbolAtom "decor", SymbolAtom decor]) =
    case decor of
      "comment"   => Just Comment
      "type"      => Just Typ
      "function"  => Just Function
      "data"      => Just Data
      "keyword"   => Just Keyword
      "bound"     => Just Bound
      "namespace" => Just Namespace
      "postulate" => Just Postulate
      "module"    => Just Module
      _ => Nothing
  fromSExp _ = Nothing


text:
module Quantities

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

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
module SmallStep

import Logic

%access public export

%default total

data Tm : Type where
  C : Nat -> Tm
  P : Tm -> Tm -> Tm

Uninhabited (C _ = P _ _) where
  uninhabited Refl impossible

Uninhabited (P _ _ = C _) where
  uninhabited Refl impossible

evalF : (t : Tm) -> Nat
evalF (C n) = n
evalF (P n m) = evalF n + evalF m

data Eval : Tm -> Nat -> Type where
  E_Const : Eval (C n) n
  E_Plus : Eval t1 n1 -> Eval t2 n2 -> Eval (P t1 t2) (n1 + n2)

infixl 5 =+>

(=+>) : (t : Tm) -> (n : Nat) -> Type
(=+>) = Eval

infix 4 -+>

data Value : Tm -> Type where
  V_Const : (n : Nat) -> Value (C n)

Uninhabited (Value (P _ _)) where
  uninhabited (V_Const _) impossible

data Step : Tm -> Tm -> Type where
  ST_PlusConstConst : Step (P (C n1) (C n2)) (C (n1 + n2))
  ST_Plus1 : Step t1 t1' -> Step (P t1 t2) (P t1' t2)
  ST_Plus2 : Value v1 -> Step t2 t2' -> Step (P v1 t2) (P v1 t2')

(-+>) : Tm -> Tm -> Type
(-+>) = Step

test_step_1 : P (P (C 0) (C 3)) (P (C 2) (C 4)) -+>
              P (C (0 + 3)) (P (C 2) (C 4))
test_step_1 = ST_Plus1 ST_PlusConstConst

test_step_2 : P (C 0) (P (C 2) (P (C 0) (C 3))) -+>
              P (C 0) (P (C 2) (C (0 + 3)))
test_step_2 = ST_Plus2 (V_Const 0) (ST_Plus2 (V_Const 2) ST_PlusConstConst)

step_deterministic : Deterministic Step
step_deterministic ST_PlusConstConst ST_PlusConstConst =
  Refl
step_deterministic (ST_Plus1 s1) (ST_Plus1 s2) =
  rewrite step_deterministic s1 s2 in Refl
step_deterministic (ST_Plus2 _ s1) (ST_Plus2 _ s2) =
  rewrite step_deterministic s1 s2 in Refl

strong_progress : (t : Tm) -> Either (Value t) (t' : Tm ** t -+> t')
strong_progress (C n) = Left (V_Const n)
strong_progress (P (C n) (C m)) = Right (C (n + m) ** ST_PlusConstConst)
strong_progress (P (C n) (P t1 t2)) = case strong_progress (P t1 t2) of
  Left _ impossible
  Right (t' ** s) => Right (P (C n) t' ** ST_Plus2 (V_Const n) s)
strong_progress (P (P t1 t2) t3) = case strong_progress (P t1 t2) of
  Left _ impossible
  Right (t' ** s) => Right (P t' t3 ** ST_Plus1 s)

value_is_nf : Value v -> NormalForm Step v
value_is_nf (V_Const _) (_ ** _) impossible

nf_is_value : NormalForm Step v -> Value v
nf_is_value {v = (C k)} _ = V_Const k
nf_is_value {v = (P (C k) (C j))} contra =
  absurd (contra (C (k + j) ** ST_PlusConstConst))
nf_is_value {v = (P (C k) (P t1 t2))} contra = case strong_progress (P t1 t2) of
  Left _ impossible
  Right (x' ** s) => absurd (contra (P (C k) x' ** ST_Plus2 (V_Const k) s))
nf_is_value {v = (P (P t1 t2) t3)} contra = case strong_progress (P t1 t2) of
  Left _ impossible
  Right (x' ** s) => absurd (contra (P x' t3 ** ST_Plus1 s))

nf_same_as_value : (NormalForm Step v) ↔ (Value v)
nf_same_as_value = (nf_is_value, value_is_nf)

namespace Temp1
  data Value1 : Tm -> Type where
    V_Const1 : (n : Nat) -> Value1 (C n)
    V_Funny1 : Value1 (P t1 (C n2))

  data Step1 : Tm -> Tm -> Type where
    ST_PlusConstConst1 : Step1 (P (C n1) (C n2)) (C (n1 + n2))
    ST_Plus11 : Step1 t1 t1' -> Step1 (P t1 t2) (P t1' t2)
    ST_Plus21 : Value1 v1 -> Step1 t2 t2' -> Step1 (P v1 t2) (P v1 t2')

  value1_not_same_as_normal_form : (v : Tm ** ( Value1 v
                                              , Not (NormalForm Step1 v) ))
  value1_not_same_as_normal_form =
    (P (C 0) (C 0) ** (V_Funny1, \contra => contra (C 0 ** ST_PlusConstConst1)))

namespace Temp2
  data Value2 : Tm -> Type where
    V_Const2 : (n : Nat) -> Value2 (C n)

  data Step2 : Tm -> Tm -> Type where
    ST_Funny2 : Step2 (C n) (P (C n) (C 0))
    ST_PlusConstConst2 : Step2 (P (C n1) (C n2)) (C (n1 + n2))
    ST_Plus12 : Step2 t1 t1' -> Step2 (P t1 t2) (P t1' t2)
    ST_Plus22 : Value2 v1 -> Step2 t1 t2' -> Step2 (P v1 t2) (P v1 t2')

  value2_not_same_as_normal_form : (v : Tm ** ( Value2 v
                                              , Not (NormalForm Step2 v) ))
  value2_not_same_as_normal_form =
    (C 0 ** (V_Const2 0, \contra => contra (P (C 0) (C 0) ** ST_Funny2)))

namespace Temp3
  data Value3 : Tm -> Type where
    V_Const3 : (n : Nat) -> Value3 (C n)

  data Step3 : Tm -> Tm -> Type where
    ST_PlusConstConst3 : Step3 (P (C n1) (C n2)) (C (n1 + n2))
    ST_Plus13 : Step3 t1 t1' -> Step3 (P t1 t2) (P t1' t2)

  value3_not_same_as_normal_form : (v : Tm ** ( Not (Value3 v)
                                              , NormalForm Step3 v ))
  value3_not_same_as_normal_form =
    (P (C 0) (P (C 0) (C 0)) ** ( \v => case v of
                                    V_Const3 _ impossible
                                , \(x' ** s) => case s of
                                    ST_Plus13 ST_PlusConstConst3 impossible
                                    ST_Plus13 (ST_Plus13 _) impossible ))

namespace Temp4
  data Tm4 : Type where
    Tru4 : Tm4
    Fls4 : Tm4
    Test4 : Tm4 -> Tm4 -> Tm4 -> Tm4

  data Value4 : Tm4 -> Type where
    V_Tru4 : Value4 Tru4
    V_Fls4 : Value4 Fls4

  data Step4 : Tm4 -> Tm4 -> Type where
    ST_IfTrue4 : Step4 (Test4 Tru4 t1 t2) t1
    ST_IfFalse4 : Step4 (Test4 Fls4 t1 t2) t2
    ST_If4 : Step4 t1 t1' -> Step4 (Test4 t1 t2 t3) (Test4 t1' t2 t3)

  bool_step_prop1 : Not (Step4 Fls4 Fls4)
  bool_step_prop1 ST_IfTrue4 impossible
  bool_step_prop1 ST_IfFalse4 impossible
  bool_step_prop1 (ST_If4 _) impossible

  bool_step_prop2 : Not (Step4 (Test4 Tru4
                                      (Test4 Tru4 Tru4 Tru4)
                                      (Test4 Fls4 Fls4 Fls4))
                               Tru4)
  bool_step_prop2 ST_IfTrue4 impossible
  bool_step_prop2 ST_IfFalse4 impossible
  bool_step_prop2 (ST_If4 _) impossible

  bool_step_prop3 : Step4 (Test4 (Test4 Tru4 Tru4 Tru4)
                                 (Test4 Tru4 Tru4 Tru4)
                                 Fls4)
                          (Test4 Tru4
                                 (Test4 Tru4 Tru4 Tru4)
                                 Fls4)
  bool_step_prop3 = ST_If4 ST_IfTrue4

  strong_progress_bool : (t : Tm4) -> Either (Value4 t) (t' : Tm4 ** Step4 t t')
  strong_progress_bool Tru4 = Left V_Tru4
  strong_progress_bool Fls4 = Left V_Fls4
  strong_progress_bool (Test4 Tru4 t2 _) = Right (t2 ** ST_IfTrue4)
  strong_progress_bool (Test4 Fls4 _ t3) = Right (t3 ** ST_IfFalse4)
  strong_progress_bool (Test4 (Test4 t1 t2 t3) t4 t5) =
    case strong_progress_bool (Test4 t1 t2 t3) of
      Left _ impossible
      Right (t' ** s) => Right (Test4 t' t4 t5 ** ST_If4 s)

  step_deterministic_bool : Step4 x y1 -> Step4 x y2 -> y1 = y2
  step_deterministic_bool ST_IfTrue4 ST_IfTrue4 = Refl
  step_deterministic_bool ST_IfFalse4 ST_IfFalse4 = Refl
  step_deterministic_bool (ST_If4 s1) (ST_If4 s2) =
    rewrite step_deterministic_bool s1 s2 in Refl

infix 4 -+>*

(-+>*) : Relation Tm
(-+>*) = Multi Step

test_multistep_1 : P (P (C 0) (C 3)) (P (C 2) (C 4)) -+>* C 9
test_multistep_1 = MultiStep (ST_Plus1 ST_PlusConstConst) $
                   MultiStep (ST_Plus2 (V_Const 3) ST_PlusConstConst) $
                   MultiStep ST_PlusConstConst $
                   MultiRefl

test_multistep_2 : C 3 -+>* C 3
test_multistep_2 = MultiRefl

test_multistep_3 : P (C 0) (C 3) -+>* P (C 0) (C 3)
test_multistep_3 = MultiRefl

test_multistep_4 : P (C 0) (P (C 2) (P (C 0) (C 3))) -+>* P (C 0) (C 5)
test_multistep_4 = MultiStep (ST_Plus2 (V_Const 0)
                                       (ST_Plus2 (V_Const 2)
                                                 ST_PlusConstConst)) $
                   MultiStep (ST_Plus2 (V_Const 0) ST_PlusConstConst) $
                   MultiRefl

NormalFormOf : (t, t' : Tm) -> Type
NormalFormOf t t' = (t -+>* t', NormalForm Step t')

normal_forms_unique : Deterministic NormalFormOf
normal_forms_unique (MultiRefl, _) (MultiRefl, _) = Refl
normal_forms_unique (MultiRefl, contra) (MultiStep {y} x_step_y _, _) =
  absurd (contra (y ** x_step_y))
normal_forms_unique (MultiStep {y} x_step_y _, _) (MultiRefl, contra) =
  absurd (contra (y ** x_step_y))
normal_forms_unique {y2}
                    p@(MultiStep x_step_y y_step_y1, contra1)
                    (MultiStep x_step_y3 y3_step_y2, contra2) =
  let y3_eq_y = sym (step_deterministic x_step_y x_step_y3)
      y_step_y2 = replace {P=\x => Multi Step x y2} y3_eq_y y3_step_y2
  in normal_forms_unique (assert_smaller p (y_step_y1, contra1))
                         (y_step_y2, contra2)

Normalizing : (r : Relation t) -> Type
Normalizing {t} r = (x : t) -> (y : t ** (Multi r x y, NormalForm r y))

multistep_congr_1 : t1 -+>* t1' -> P t1 t2 -+>* P t1' t2
multistep_congr_1 MultiRefl = MultiRefl
multistep_congr_1 (MultiStep once next) =
  MultiStep (ST_Plus1 once) (multistep_congr_1 next)

multistep_congr_2 : Value t1 -> t2 -+>* t2' -> P t1 t2 -+>* P t1 t2'
multistep_congr_2 _ MultiRefl = MultiRefl
multistep_congr_2 v (MultiStep once next) =
  MultiStep (ST_Plus2 v once) (multistep_congr_2 v next)

step_normalizing : Normalizing Step
step_normalizing (C n) =
  (C n ** (MultiRefl, \(_ ** s) => case s of
                        ST_PlusConstConst impossible
                        ST_Plus1 _ impossible
                        ST_Plus2 _ _ impossible))
step_normalizing (P t1 t2) =
  let (_ ** (s1, nf1)) = step_normalizing t1
      (_ ** (s2, nf2)) = step_normalizing t2
      v1@(V_Const n1) = nf_is_value nf1
      V_Const n2 = nf_is_value nf2
      steps = multi_trans (multistep_congr_1 {t2=t2} s1) $
              multi_trans (multistep_congr_2 v1 s2) $
              MultiStep ST_PlusConstConst MultiRefl
  in (C (n1 + n2) ** (steps, \(_ ** s) => case s of
                               ST_PlusConstConst impossible
                               ST_Plus1 _ impossible
                               ST_Plus2 _ _ impossible))

eval__multistep : t =+> n -> t -+>* C n
eval__multistep E_Const = MultiRefl
eval__multistep (E_Plus {n1} e1 e2) =
  multi_trans (multistep_congr_1 (eval__multistep e1)) $
  multi_trans (multistep_congr_2 (V_Const n1) (eval__multistep e2)) $
  MultiStep ST_PlusConstConst MultiRefl

step__eval : t -+> t' -> t' =+> n -> t =+> n
step__eval ST_PlusConstConst E_Const = E_Plus E_Const E_Const
step__eval (ST_Plus1 s1) (E_Plus e1 e2) = E_Plus (step__eval s1 e1) e2
step__eval (ST_Plus2 _ s2) (E_Plus e1 e2) = E_Plus e1 (step__eval s2 e2)

multistep__eval : NormalFormOf t t' -> (n : Nat ** (t' = C n, t =+> n))
multistep__eval (MultiRefl, nf) =
  let V_Const n = nf_is_value nf
  in (n ** (Refl, E_Const))
multistep__eval p@(MultiStep {y} once next, nf) =
  let (n ** (prf, e)) = multistep__eval (assert_smaller p (next, nf))
  in (n ** (prf, step__eval once e))

evalF_eval : (evalF t = n) ↔ (t =+> n)
evalF_eval = (forward, backward)
where forward : evalF t = n -> t =+> n
      forward {t = (C _)} prf = rewrite prf in E_Const
      forward {t = (P t1 t2)} prf with (evalF t1) proof prf1
        forward {t = (P t1 t2)} prf | _ with (evalF t2) proof prf2
          forward {t = (P t1 t2)} prf | _ | _ =
            rewrite sym prf
            in E_Plus (forward (sym prf1)) (forward (sym prf2))
      backward : t =+> n -> evalF t = n
      backward E_Const = Refl
      backward (E_Plus e1 e2) =
        rewrite backward e1
        in rewrite backward e2
        in Refl


text:
import Effects
import Effect.Logging.Category

func : Nat -> Eff () [LOG String]
func x = do
  warn Nil $ unwords ["I do nothing with", show x]
  pure ()

doubleFunc : Nat -> Eff Nat [LOG String]
doubleFunc x = do
  logN 40 ["NumOPS"] $ unwords ["Doing the double with", show x ]
  func x
  pure (x+x)

eMain : Eff Nat [LOG String]
eMain = do
  initLogger ALL ["NumOPS"]
  doubleFunc 3

main : IO ()
main = do
   x <- run eMain
   printLn x


text:
import Language.Reflection

%language ElabReflection

fc : FC
fc = EmptyFC

mkEnum : (name : String) -> (cons : List String) -> Elab ()
mkEnum name cons =
  let enumDecl = IData EmptyFC Public Nothing dat
   in declare [enumDecl]
  where enumName : Name
        enumName = UN $ Basic name

        mkCon : String -> ITy
        mkCon n = MkTy EmptyFC EmptyFC (UN $ Basic n) (IVar EmptyFC enumName)

        dat : Data
        dat = MkData EmptyFC enumName (IType EmptyFC) [] (map mkCon cons)

%runElab mkEnum "FooBar" ["Foo","Bar"]

eqFooBar : FooBar -> FooBar -> Bool
eqFooBar Foo Foo = True
eqFooBar Bar Bar = True
eqFooBar _   _   = False

main : IO ()
main =  printLn (eqFooBar Foo Foo)
     >> printLn (eqFooBar Bar Foo)


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

import public GRL.Common
import public GRL.IR
import public GRL.Model

%access public export
%default total

data GLangAST : GTy -> Type where
    MkNode   : String -> GElemTy -> String -> Maybe SValue -> GLangAST ELEM
    MkIntent : GIntentTy -> CValue -> String -> String -> GLangAST INTENT
    MkStruct : GStructTy -> String -> List (String) -> GLangAST STRUCT

showSValue : Maybe SValue -> String
showSValue Nothing     = ""
showSValue (Just sval) = unwords ["is", show sval]

listIDs : List String -> String
listIDs is = unwords $ intersperse "," is

showIntent : String -> CValue -> String -> String -> String
showIntent op cval x y = unwords [x, op, y, "|", show cval]

showStruct : String -> String -> List String -> String
showStruct op x ys = unwords [x, op, "[", listIDs ys, "]" ]

Show (GLangAST ty) where
  show (MkNode id ty t sval) = unwords [id, "<-", show ty, show t, showSValue sval]
  show (MkIntent ty cval x y) =
      case ty of
        IMPACTSty => showIntent "==>" cval x y
        AFFECTSty => showIntent "~~>" cval x y
  show (MkStruct ty x ys) =
      case ty of
        ANDty => showStruct "&=" x ys
        XORty => showStruct "X=" x ys
        IORty => showStruct "|=" x ys

-- ----------------------------------------------------------- [ The FUnctions ]

private
mkPrefix : GElemTy -> String
mkPrefix GOALty = "g"
mkPrefix SOFTty = "s"
mkPrefix TASKty = "t"
mkPrefix RESty  = "r"

private
mkStructOp : GStructTy -> String
mkStructOp ANDty = "&="
mkStructOp XORty = "X="
mkStructOp IORty = "|="

private
prettyElem : NodeID -> GoalNode -> String
prettyElem id n = with List show (MkNode
    (concat [mkPrefix (getNodeTy n), show id])
    (getNodeTy n)
    (getNodeTitle n)
    (getSValue n))

private
genIDs : List (GoalNode, NodeID) -> Dict NodeID String
genIDs is = foldl doInsert empty is
  where
    doInsert : Dict NodeID String -> (GoalNode, NodeID) -> Dict NodeID String
    doInsert dict (g,id) = with List
        insert id (concat [mkPrefix (getNodeTy g), show id]) dict

private
fetchID : NodeID -> Dict NodeID String -> String
fetchID n dict =
    case lookup n dict of
      Nothing  => "No ID this will fail"
      Just val => val

private
prettyStruct : String -> GStructTy -> List String -> String
prettyStruct x ty ys = show $ MkStruct ty x ys

private
prettyStructs : NodeID -> Dict NodeID String -> GModel -> Maybe String
prettyStructs n dict m =
    case getValueByID n m of
      Nothing   => Nothing
      Just nVal =>
        case getStructTy nVal of
          Nothing => Nothing
          Just s  => Just $ prettyStruct (fetchID n dict) s ys'

  where
    ys : List NodeID
    ys = map fst $ filter (\(y,l) => isDeCompEdge l) (getEdgesByID n m)

    ys' : List String
    ys' = map (\x => fetchID x dict) ys

private
prettyIntents : NodeID -> Dict NodeID String -> GModel -> String
prettyIntents n dict m = unlines $ map prettyIntent ys'
  where
    x : String
    x = fetchID n dict

    ys' : List (DemiEdge GoalEdge)
    ys' = filter (\(y,l) => not $ isDeCompEdge l) (getEdgesByID n m)

    prettyIntent : DemiEdge GoalEdge -> String
    prettyIntent (yID, Just (Correlation cval))  =
        show $ MkIntent AFFECTSty cval (fetchID yID dict) x
    prettyIntent (yID, Just (Contribution cval)) =
        show $ MkIntent IMPACTSty cval (fetchID yID dict) x
    prettyIntent _  = "-- err"

namespace GLang
  toString : GModel -> String
  toString m = unlines
      [ "grl model\n"
      , unlines es, "\n"
      , unlines (catMaybes ss), "\n"
      , unlines is, "\n"
      , "\n"
      ]
    where
      ids : Dict NodeID String
      ids = genIDs (legend m)

      es : List String
      es = foldr (\(k,v),res => prettyElem v k :: res) Nil (legend m)

      is : List String
      is = map (\n => prettyIntents n ids m) (verticesID m)

      ss : List (Maybe String)
      ss = map (\n => prettyStructs n ids m) (verticesID m)

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Config

import Data.Config
import Data.Either
import Data.List
import Data.List.PrefixSuffix
import Data.List1
import Data.Promise
import Data.String
import Decidable.Equality
import FFI.Git
import FFI.GitHub
import Language.JSON
import System
import System.File

%default total

writeConfig : Config -> Promise Config
writeConfig config =
  do res <- writeFile config.filepath (format 2 $ json config)
     case res of
          Right () => pure config
          Left err => reject "Failed to write updated config file to \{config.filepath}: \{show err}."

export
syncConfig : Config => Octokit => (echo : Bool) -> Promise Config
syncConfig @{config} echo =
 do teamSlugs  <- listTeams config.org
    orgMembers <- listOrgMembers config.org
    updatedAt  <- cast {to=Timestamp} <$> time
    let config' = { updatedAt  := updatedAt
                  , teamSlugs  := teamSlugs
                  , orgMembers := orgMembers
                  } config
    ignore $ writeConfig config'
    when echo $
      do putStrLn "Your updated configuration is:"
         printLn config
    pure config'

export
syncIfOld : Octokit => Config -> Promise Config
syncIfOld config =
  if config.updatedAt < !oneDayAgo
     then do -- putStrLn "Syncing config file..."
             syncConfig False
     else pure config
  where
    oneDayAgo : HasIO io => io Timestamp
    oneDayAgo =
      do let oneDay = 86_400
         now <- time
         pure $ cast (now - oneDay)

record GitRemote where
  constructor Remote
  org, repo : String

dropPrefix' : (prefx : String) -> String -> Maybe String
dropPrefix' prefx = map pack . drop' . unpack
  where
    drop' : List Char -> Maybe (List Char)
    drop' xs with (dropPrefix (unpack prefx) xs)
      drop' xs | (Yes (suffix ** _)) = Just suffix
      drop' xs | (No contra)         = Nothing

parseGitHubURI : String -> Maybe GitRemote
parseGitHubURI str = parseHTTPS str <|> parseSSH str
  where
    parseSuffix : String -> Maybe GitRemote
    parseSuffix suffix =
      do let (orgAndRepo, _) = break (== '.') suffix
         (org ::: repo :: []) <- pure $ split (== '/') orgAndRepo
           | _ => Nothing
         pure $ Remote org repo

    parseHTTPS : String -> Maybe GitRemote
    parseHTTPS = dropPrefix' "https://github/com/" >=> parseSuffix

    parseSSH : String -> Maybe GitRemote
    parseSSH = dropPrefix' "git@github.com:" >=> parseSuffix

propSetters : List (String, (Config -> String -> Maybe Config))
propSetters = [
    ("assignTeams"    , update parseBool (\b => { assignTeams := b }))
  , ("commentOnAssign", update parseBool (\b => { commentOnAssign := b }))
  ]
  where
    parseBool : String -> Maybe Bool
    parseBool x with (toLower x)
      _ | "yes"   = Just True
      _ | "true"  = Just True
      _ | "no"    = Just False
      _ | "false" = Just False
      _ | _ = Nothing

    update : Functor f => (String -> f a) -> (a -> b -> b) -> b -> String -> f b
    update f g c = map (flip g c) . f

namespace PropSettersProperties
  propSettersCoveragePrf : Data.Config.settableProps = Builtin.fst <$> Config.propSetters
  propSettersCoveragePrf = Refl

||| Attempt to set a property and value given String representations.
||| After setting, write the config and return the updated result.
export
setConfig : Config =>
            (prop : String)
         -> (value : String)
         -> Promise Config
setConfig @{config} prop value with (lookup prop propSetters)
  _ | Nothing  = reject "\{prop} cannot be set via `config` command."
  _ | (Just set) with (set config value)
    _ | Nothing  = reject "\{value} is not a valid value for \{prop}."
    _ | (Just config') = writeConfig config'

propGetters : List (String, (Config -> String))
propGetters = [
    ("assignTeams"    , show . assignTeams)
  , ("commentOnAssign", show . commentOnAssign)
  ]

namespace PropGettersProperties
  propGetterCoveragePrf : Data.Config.settableProps = Builtin.fst <$> Config.propGetters
  propGetterCoveragePrf = Refl

export
getConfig : Config =>
            (prop : String)
         -> Promise String
getConfig @{config} prop with (lookup prop propGetters)
  getConfig prop | Nothing    = reject "\{prop} cannot get read via `config` command."
  getConfig prop | (Just get) = pure $ get config

createConfig : Git => Octokit =>
               (terminalColors : Bool)
            -> Promise Config
createConfig terminalColors =
  do putStrLn "Creating a new configuration (storing in \{Config.filename})..."
     -- TODO: don't assume remote name ("origin"), get it from git or ask for it.
     defaultOrgAndRepo <- (parseGitHubURI <$> remoteURI "origin") <|> pure Nothing
     let orgDefaultStr = defaultStr (.org) defaultOrgAndRepo
     putStrLn "What GitHub org would you like to use harmony for\{orgDefaultStr}?"
     org  <- orIfEmpty (org defaultOrgAndRepo)  . trim <$> getLine
     let repoDefaultStr = defaultStr (.repo) defaultOrgAndRepo
     putStrLn "What repository would you like to use harmony for\{repoDefaultStr}?"
     repo <- orIfEmpty (repo defaultOrgAndRepo) . trim <$> getLine
     putStr "Would you like harmony to comment when it assigns reviewers? [Y/n] "
     commentOnAssign <- yesUnlessNo . trim <$> getLine
     putStr "Would you like harmony to assign teams in addition to individuals when it assigns reviewers? [Y/n] "
     assignTeams <- yesUnlessNo . trim <$> getLine
     putStrLn "Creating config..."
     mainBranch <- getRepoDefaultBranch org repo
     updatedAt  <- cast <$> time
     let ephemeral = MkEphem {
         filepath = "./\{Config.filename}"
       , colors   = terminalColors
       }
     do teamSlugs  <- listTeams org
        orgMembers <- listOrgMembers org
        let config = MkConfig {
            updatedAt
          , org
          , repo
          , mainBranch
          , assignTeams
          , commentOnAssign
          , teamSlugs
          , orgMembers
          , ephemeral
          }
        ignore $ writeConfig config
        putStrLn "Your new configuration is:"
        printLn config
        pure config
  where
    orIfEmpty : Maybe String -> String -> String
    orIfEmpty Nothing  x  = x
    orIfEmpty (Just y) "" = y
    orIfEmpty (Just _) x  = x

    yesUnlessNo : String -> Bool
    yesUnlessNo "n" = False
    yesUnlessNo "N" = False
    yesUnlessNo _   = True

    org : Maybe GitRemote -> Maybe String
    org = map (.org)

    repo : Maybe GitRemote -> Maybe String
    repo = map (.repo)

    enterForDefaultStr : String -> String
    enterForDefaultStr str = " (ENTER for default: \{str})"

    defaultStr : (GitRemote -> String) -> Maybe GitRemote -> String
    defaultStr f = fromMaybe "" . map (enterForDefaultStr . f)

data ConfigError = File FileError
                 | Parse String

Show ConfigError where
  show (File e)  = show e
  show (Parse e) = show e

findConfig : HasIO io => (startDir : String) -> Fuel -> io (Maybe String)
findConfig startDir Dry = pure Nothing
findConfig startDir (More fuel) =
  let location = "\{startDir}/\{Config.filename}"
  in if !(exists location)
       then pure (Just location)
       else findConfig "\{startDir}/.." fuel

export
covering
loadConfig : HasIO io =>
             (terminalColors : Bool)
          -> io (Either ConfigError Config)
loadConfig terminalColors = let (>>=) = (>>=) @{Monad.Compose} in
  do location   <- mapFst File . maybeToEither FileNotFound <$>
                     findConfig "." (limit 10)
     configFile <- mapFst File <$>
                     readFile location
     pure . mapFst Parse $ parseConfig (MkEphem location terminalColors) configFile

export
covering
loadOrCreateConfig : Git => Octokit =>
                     (terminalColors : Bool)
                  -> Promise Config
loadOrCreateConfig terminalColors =
  do Right config <- loadConfig terminalColors
       | Left (File FileNotFound) => createConfig terminalColors
       | Left err => reject "Error loading \{Config.filename}: \{show err}."
     pure config

max_stars_repo_name: mattpolzin/harmony

max_issues_repo_name: mattpolzin/harmony

max_forks_repo_name: mattpolzin/harmony


text:
interface Natty (n : Nat) where

fromNatty : Type -> Nat
fromNatty (Natty Z) = Z
fromNatty (Natty (S n)) = S (fromNatty (Natty n))
fromNatty _ = Z

main : IO ()
main = ignore $ traverse printLn
  [ fromNatty (Natty 3)
  , fromNatty (Natty (2 + 6))
  , fromNatty (List (Natty 1))
  ]


text:
module LightClick.IR.Channel.MicroSV.Intermediate

import Data.List
import Data.Vect
import Data.String

import Data.Vect.Sort

import Toolkit.Data.DList
import Toolkit.Data.DList.DeBruijn
import Toolkit.Data.DVect

import public Language.SystemVerilog.MetaTypes
import public Language.SystemVerilog.Gates
import public Language.SystemVerilog.Direction

import LightClick.Error

import LightClick.Types.Direction

import LightClick.IR.ModuleCentric
import LightClick.IR.ChannelCentric
import LightClick.IR.Channel.MicroSV.InterpTy
import LightClick.IR.Channel.MicroSV.Error

%default total

public export
data MicroSvIR : (lctxt : Context)
              -> (type : Ty)
              -> Type
  where
    End : MicroSvIR ctxt UNIT

    Local  : (label : String)
                   -> Index ctxt (label, type)
                   -> MicroSvIR ctxt type

    Global : (label : String)
          -> (ty    : Ty)
                   -> MicroSvIR ctxt ty

    Let : {typeE, ty : Ty}
       -> (this     : String)
       -> (beThis   : MicroSvIR ctxt typeE)
       -> (withType : MicroSvIR ctxt ty)
       -> (inThis   : MicroSvIR ((this,typeE)::ctxt) typeB)
       -> MicroSvIR ctxt typeB

    Seq : {typeA, typeB : Ty}
       -> MicroSvIR ctxt typeA
       -> MicroSvIR ctxt typeB
       -> MicroSvIR ctxt typeB

    TYPE : MicroSvIR ctxt TYPE
    GATE : MicroSvIR ctxt GATE

    -- Decls
    DataLogic : MicroSvIR ctxt DATA

    DataArray : (type : MicroSvIR ctxt DATA) -> (size : Nat) -> MicroSvIR ctxt DATA

    DataStruct : {n : Nat} -> (xs : Vect (S n) (Pair String (MicroSvIR ctxt DATA)))
              -> MicroSvIR ctxt DATA

    DataUnion : {n : Nat} -> (xs : Vect (S n) (Pair String (MicroSvIR ctxt DATA)))
             -> MicroSvIR ctxt DATA

    Port : (label : String)
        -> (dir   : SystemVerilog.Direction.Direction)
        -> (type  : MicroSvIR ctxt DATA)
        -> MicroSvIR ctxt (PORT label)

    MDecl : DList String (\s => MicroSvIR ctxt (PORT s)) names
         -> MicroSvIR ctxt (MODULE names)

    -- Ctors
    NewChan : MicroSvIR ctxt CHAN
    NewModule : List (Pair String (MicroSvIR ctxt CHAN))
             -> MicroSvIR ctxt (MINST names)

    -- Gates
    Not : (out : MicroSvIR ctxt CHAN)
       -> (ins : MicroSvIR ctxt CHAN)
              -> MicroSvIR ctxt GINST

    Gate : {n    : Nat}
        -> (type : TyGateComb)
        -> (out  : MicroSvIR ctxt CHAN)
        -> (ins  : Vect (S (S n)) (MicroSvIR ctxt CHAN))
                -> MicroSvIR ctxt GINST

export
getType : {type : Ty} -> MicroSvIR ctxt type -> Ty
getType {type} _ = type

public export
data Decl : Ty -> Type where
  MkDecl : {type : Ty} -> String -> MicroSvIR Nil type -> Decl type

public export
Decls : List Ty -> Type
Decls = DList Ty Decl
-- Could turn into a triple/custom data type to collect proof that the `type` is valid for a declaration

export
lookup : String -> Decls ty -> Maybe Ty
lookup x [] = Nothing
lookup x (MkDecl y expr :: rest) with (decEq x y)
  lookup x (MkDecl x expr :: rest) | (Yes Refl) = Just $ getType expr
  lookup x (MkDecl y expr :: rest) | (No contra) = lookup x rest

public export
data MicroSvIrSpec : Type where
  MkMSVIRSpec : (decls : Decls types)
             -> (expr  : MicroSvIR Nil UNIT)
             -> MicroSvIrSpec

data TEnv : (local : context) -> Type where
  MkTEnv : {types : List Ty}
        -> (decls : Decls types)
        -> (local : Context)
        -> TEnv local

data TRes : (local : Context) -> (type : TyIR) -> Type where
  MkTRes : {type : Ty}
        -> {types : List Ty}
        -> {tyIR : TyIR}
        -> (decls : Decls types)
        -> (expr  : MicroSvIR ctxt type)
        -> (prf   : InterpTy tyIR type)
        -> TRes ctxt tyIR

TFuncSig : (local : Context) -> TyIR -> Type
TFuncSig local type =
      (env  : TEnv local)
   -> (expr : ChannelIR type)
   -> Either TError (TRes local type)

%inline
port : (f : TFuncSig local PORT)
    -> (e : TEnv local)
    -> (p : ChannelIR PORT)
    -> Either TError (s ** MicroSvIR local (PORT s))
port f e p with (f e p)
  port f e p | (Left l) = Left l
  port f e p | (Right (MkTRes decls (Port l dir type) (PP l))) = Right (_ ** Port l dir type)
  port f e p | (Right (MkTRes decls _                 (PP l))) = Left (General $ "Port Expected")

ports : (f  : TFuncSig local PORT)
     -> (e  : TEnv local)
     -> (ps : Vect (S n) (ChannelIR PORT))
     -> Either TError (ns ** DList String (\s => MicroSvIR local (PORT s)) ns)
ports f e (x :: xs)
    = do x' <- port f e x
         xs' <- ports' f e xs
         pure (_ ** (snd x') :: (snd xs'))
  where
    ports' : (f  : TFuncSig local PORT)
        -> (e  : TEnv local)
        -> (ps : Vect y (ChannelIR PORT))
        -> Either TError (ns ** DList String (\s => MicroSvIR local (PORT s)) ns)
    ports' f e [] = pure (_ ** Nil)
    ports' f e (x :: xs) =
      do x' <- port f e x
         xs' <- ports' f e xs
         pure (_ ** (snd x') :: (snd xs'))

%inline
chan : (f : TFuncSig local CHAN)
    -> (e : TEnv local)
    -> (c : (String, ChannelIR CHAN))
    -> Either TError (String, MicroSvIR local CHAN)
chan f e (l,c) with (f e c)
  chan f e (l,c) | (Left err) = Left $ Nested "Attempted to convert chan" err
  chan f e (l,c) | (Right (MkTRes decls expr CC)) = Right (l,expr)

chans : (f  : TFuncSig local CHAN)
     -> (e  : TEnv local)
     -> (cs : Vect (S n) (String, ChannelIR CHAN))
     -> Either TError (List (String, (MicroSvIR local CHAN)))
chans f e (x :: xs)
    = do x' <- chan f e x
         xs' <- chans' f e xs
         pure (x'::xs')
  where

    chans' : (f  : TFuncSig local CHAN)
          -> (e  : TEnv local)
          -> (cs : Vect y (String, ChannelIR CHAN))
                -> Either TError (List (String, (MicroSvIR local CHAN)))
    chans' f e [] = pure Nil
    chans' f e (x :: xs) =
      do x' <- chan f e x
         xs' <- chans' f e xs
         pure (x'::xs')

%inline
chan' : (f : TFuncSig local CHAN)
     -> (e : TEnv local)
     -> (c : ChannelIR CHAN)
          -> Either TError (MicroSvIR local CHAN)
chan' f e c with (f e c)
  chan' f e c | (Left err) = Left $ Nested "Attempted to convert chan" err
  chan' f e c | (Right (MkTRes decls expr CC)) = Right expr

%inline
kvpair : (f : TFuncSig local DATA)
      -> (e : TEnv local)
      -> (c : (String, ChannelIR DATA))
      -> Either TError (String, MicroSvIR local DATA)
kvpair f e (l,c) with (f e c)
  kvpair f e (l,c) | (Left err) = Left $ Nested "Attempted to convert KVPair" err
  kvpair f e (l,c) | (Right (MkTRes decls expr DD)) = Right (l,expr)

Eq (ChannelIR PORT) where
  (==) (CPort x f d) (CPort y g e) = x == y
  (==) _ _ = False

Ord (ChannelIR PORT) where
  compare (CPort x f d) (CPort y g e) = compare x y
  compare _ _ = LT

covering
convert : {type : TyIR}
       -> {local : Context}
       -> (e : TEnv local)
       -> (c : ChannelIR type)
       -> Either TError (TRes local type)
-- [ References ]
convert e (CRef x type) with (e)
  convert e (CRef x type) | (MkTEnv decls local) with (isIndex x local)
    convert e (CRef x type) | (MkTEnv decls local) | (Yes (ty ** idx)) with (interpTy type ty)
      convert e (CRef x type) | (MkTEnv decls local) | (Yes (ty ** idx)) | (Yes prf) =
        pure (MkTRes decls (Local x idx) prf)
      convert e (CRef x type) | (MkTEnv decls local) | (Yes (ty ** idx)) | (No contra) =
        Left $ General (unwords ["Attempting to construct Local", show x])

    convert e (CRef x type) | (MkTEnv decls local) | (No contra) with (lookup x decls)
      convert e (CRef x type) | (MkTEnv decls local) | (No contra) | Nothing
        = Left $ General (unwords ["Attempting to construct global, identifier not found", show x])
      convert e (CRef x type) | (MkTEnv decls local) | (No contra) | Just ty with (interpTy type ty)
        convert e (CRef x type) | (MkTEnv decls local) | (No contra) | Just ty | (Yes prf)
          = pure (MkTRes decls (Global x ty) prf)
        convert e (CRef x type) | (MkTEnv decls local) | (No contra) | Just ty | (No contra')
          = Left $ General (unwords ["Attempting to construct Global type issue", show x])

-- [ NOTE ] traverse decls and extra ty to do proof. will formalise later.

-- [ Structural Statements ]

---- [ Let Bindings ]

---- Is `this` bindable and if so then how
convert e (CLet bind this {term} inThis) with (isBindable term)

  {- [ Translate the Global Bindings]

    - Extend global declarations with result, assume that the expr is closed
    - Translate `inThis`
  -}

  convert e (CLet bind this {term = term} inThis) | (IsDecl prfDecl) with (e)
    convert e (CLet bind this {term = term} inThis) | (IsDecl prfDecl) | (MkTEnv decls local) with (convert (MkTEnv decls Nil) this)
      convert e (CLet bind this {term = term} inThis) | (IsDecl prfDecl) | (MkTEnv decls local) | (Left l)
        = Left $ Nested "Attempting to construct global declaration" l
      convert e (CLet bind this {term = term} inThis) | (IsDecl prfDecl) | (MkTEnv decls local) | (Right (MkTRes rest expr prf))
        = convert (MkTEnv (MkDecl bind expr::rest) local) inThis

  {- [ Translate the local bindings ]

    Convert the `this` and `inThis` before constructing the type of `this`.
  -}
  convert e (CLet bind this {term = term} inThis) | (IsLet x) with (e)
    convert e (CLet bind this {term = term} inThis) | (IsLet x) | (MkTEnv decls local) with (convert (MkTEnv decls local) this)
      convert e (CLet bind this {term = term} inThis) | (IsLet x) | (MkTEnv decls local) | (Left l)
        = Left $ Nested "Attempting to this of local let" l
      convert e (CLet bind this {term = term} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) with (Intermediate.convert (MkTEnv decls ((bind, getType expr)::local)) inThis)
        convert e (CLet bind this {term = term} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Left l) = Left $ Nested "Attempting to construct body of Local Let" l

        -- MicroSV is typed, we need to introspect `this` again because we need to get the type.
        convert e (CLet bind this {term = term} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) with (x)

          {- [ Translating Module instantiations ]

            When MINST
              - the type is the name/ref to the module
              - the value is the result of translating `this`
          -}
          convert e (CLet bind this {term = CONN} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstM with (this)
            convert e (CLet bind this {term = CONN} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstM | (CModuleInst mtype _) with (Intermediate.convert e mtype)
              convert e (CLet bind this {term = CONN} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstM | (CModuleInst mtype _) | Left l
                = Left $ Nested "Cannot construct type for local let module" l
              convert e (CLet bind this {term = CONN} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstM | (CModuleInst mtype _) | Right (MkTRes _ newMType prfType)
                = pure (MkTRes y (Let bind expr newMType z) w)

            convert e (CLet bind this {term = CONN} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstM | _
              = Left $ General "Expected local let `this` to be CModuleInst, it wasn't"

          {- [ Translating Channel terms ]

            When CHAN
              - the type is var or inline data type
              - the value is `NewChan`
          -}
          convert e (CLet bind this {term = CHAN} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstC with (this)
            convert e (CLet bind this {term = CHAN} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstC | (CChan dtype) with (convert e dtype)
              convert e (CLet bind this {term = CHAN} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstC | (CChan dtype) | Left l
                = Left $ Nested "Attempting to construct this from local let chan" l
              convert e (CLet bind this {term = CHAN} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstC | (CChan dtype) | (Right (MkTRes _ newDType prfType))
                = pure (MkTRes y (Let bind expr newDType z) w)

            convert e (CLet bind this {term = CHAN} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstC | _
              = Left $ General "Expected local let `this` to be CChan, it wasn't"

          {- [ Translating Gate terms ]

            When GATE
              - the type is var or inline data type
              - the value is another gate.
          -}
          convert e (CLet bind this {term = GATE} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstG with (this)
            convert e (CLet bind this {term = GATE} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstG | (CNot o i) with (convert e (CNot o i))
              convert e (CLet bind this {term = GATE} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstG | (CNot o i) | Left l
                = Left $ Nested "Attempting to construct this from local let not gate" l
              convert e (CLet bind this {term = GATE} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstG | (CNot o i) | Right (MkTRes _ newNot prfType)
                = Right (MkTRes y (Let bind expr GATE z) w)

            convert e (CLet bind this {term = GATE} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstG | (CGate ty o ins) with (convert e (CGate ty o ins))
              convert e (CLet bind this {term = GATE} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstG | (CGate ty o ins) | Left l
                = Left $ Nested "Attempting to construct this from local let gate gate" l
              convert e (CLet bind this {term = GATE} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstG | (CGate ty o ins) | Right (MkTRes _ newNot prfType)
                = Right (MkTRes y (Let bind expr GATE z) w)

            convert e (CLet bind this {term = GATE} inThis) | (IsLet x) | (MkTEnv decls local) | (Right (MkTRes rest expr prf)) | (Right (MkTRes y z w)) | IsInstG | _
              = Left $ General "Expected local let `this` to be a Gate, it wasn't"                                                                                --

  -- Any other pattern here is unexpected.
  convert e (CLet bind this {term = term} inThis) | Unbindable = Left $ General "We were given something unbindable"

---- [ Sequencing ]
convert (MkTEnv decls local) (CSeq x y) with (convert (MkTEnv decls local) x)
  convert (MkTEnv decls local) (CSeq x y) | Left err = Left $ Nested "Left Sequent failed" err
  convert (MkTEnv decls local) (CSeq x y) | Right (MkTRes declsX x' prfX) with (convert (MkTEnv declsX local) y)
    convert (MkTEnv decls local) (CSeq x y) | Right (MkTRes declsX x' prfX) | Left err
      = Left $ Nested "Right  sequant failed" err
    convert (MkTEnv decls local) (CSeq x y) | Right (MkTRes declsX x' prfX) | Right (MkTRes declsY y' prfY) =
      pure (MkTRes declsY (Seq x' y') prfY)

---- [ This is the End ]
convert e CEnd with (e)
  convert e CEnd | (MkTEnv decls local) = pure (MkTRes decls End UU)

-- [ Module Declarations ]

convert e (CPort l d type) with (convert e type)
  convert e (CPort l d type) | Left err
    = Left $ Nested "Attempting to construct type for Port" err
  convert e (CPort l d type) | (Right (MkTRes decls t' DD))
    = pure (MkTRes decls (Port l (interpDir d) t') (PP l))

convert e (CModule {n} xs) with (ports convert e (sort xs))
  convert e (CModule {n} xs) | (Left l)
    = Left $ Nested "Attempting to construct ports for Module Declaration" l
  convert e (CModule {n} xs) | (Right (ns ** ps)) with (e)
    convert e (CModule {n} xs) | (Right (ns ** ps)) | (MkTEnv decls local)
      = pure (MkTRes decls (MDecl ps) (MM ns))

-- [ Data Declarations ]

convert (MkTEnv decls local) CDataLogic = pure (MkTRes decls DataLogic DD)

convert e (CDataArray type k) with (convert e type)
  convert e (CDataArray type k) | Left l
    = Left $ Nested "Attempting to construct Data Type for array" l
  convert e (CDataArray type k) | Right res with (res)
    convert e (CDataArray type k) | Right res | (MkTRes decls type' DD)
      = pure (MkTRes decls (DataArray type' k) DD)

convert e (CDataStruct xs) with (e)
  convert e (CDataStruct xs) | (MkTEnv decls local)
    = do xs' <- traverse (kvpair convert e) xs
         pure (MkTRes decls (DataStruct xs') DD)

convert e (CDataUnion xs) with (e)
  convert e (CDataUnion xs) | (MkTEnv decls local)
    = do xs' <- traverse (kvpair convert e) xs
         pure (MkTRes decls (DataUnion xs') DD)

-- [ A Thing that should not exist in 'Our Normal Form' ]

convert e (CIDX label x y)
  = Left $ Nested "IDX Not expected" MalformedExpr

-- [ Constructors for Channels and Modules ]
convert e (CChan _) with (e)
  convert e (CChan _) | (MkTEnv decls local)
    = pure $ MkTRes decls NewChan CC

convert e (CModuleInst _ kvs) with (e)
  convert e (CModuleInst _ kvs) | (MkTEnv decls local)
    = do xs' <- chans convert e kvs
         let ns = map fst xs'
         pure (MkTRes decls (NewModule xs') (CM (sort ns)))

-- [ Gates ]
convert e (CNot o i) with (e)
  convert e (CNot o i) | (MkTEnv decls local)
    = do o' <- chan' convert e o
         i' <- chan' convert e i
         pure (MkTRes decls (Not o' i') GG)

convert e (CGate ty o ins) with (e)
  convert e (CGate ty o ins) | (MkTEnv decls local)
    = do o'  <- chan'  convert e o
         is' <- traverse (chan' convert e) ins
         pure (MkTRes decls (Gate ty o' is') GG)

export
covering
runConvert : (c : ChannelIR UNIT)
               -> Either TError MicroSvIrSpec
runConvert expr with (convert (MkTEnv Nil Nil) expr)
  runConvert expr | Left l
    = Left $ Nested "Cannot consruct spec" l
  runConvert expr | Right (MkTRes decls expr' UU)
    = Right (MkMSVIRSpec decls expr')

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

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Main

import Cairo
import Data.Bits

-- The following functions are required to avoid that the constantfolder
-- evaluates the expressions at compile time.
-- Maybe we should disable the constantfolder and write the tests more direct.

%foreign
  """
  code:
  func Main_f_100() -> (r):
      return (100)
  end
  """
f_100 : Felt

%foreign
  """
  code:
  func Main_f_50() -> (r):
      return (50)
  end
  """
f_50 : Felt

i8_100 : Int8
i8_100 = cast {to=Int8} f_100

i8_50 : Int8
i8_50 = cast {to=Int8} f_50

out : Cast a Felt => a -> Cairo ()
out = output . cast

%noinline
main : Cairo ()
main = do
  out $ i8_100 + i8_50
  out $ i8_100 - i8_50
  out $ i8_100 * i8_50
  -- BUG, this returns 0!!!
  -- Patternmachting on felt famously does not work.
  -- Best would be to make it work - otherwise throw an error at compile time or at least crash at runtime.
  -- out $ case b of 0 => 0 ; x => (cast {to=Bits8} a) `div` (cast {to=Bits8} x)
  out $ assert_total $ i8_100 `div` (the Int8 7)
  out $ assert_total $ i8_100 `mod` (the Int8 7)
  out $ - i8_50
  out $ i8_100 .&. i8_50
  out $ i8_100 .|. i8_50
  out $ i8_100 `xor` i8_50
  out $ i8_100 < i8_50
  out $ i8_100 <= i8_50
  out $ i8_100 == i8_50
  out $ i8_100 >= i8_50
  out $ i8_100 > i8_50
  -- out $ i8_50 `shiftL` 1 -- Index is of type Nat. Not implemented yet
  -- out $ i8_100 `shiftR` 1

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module TypedContainers.RBTree.Base

import Data.List
import TypedContainers.In
import TypedContainers.LawfulOrd

%default total

public export
data Color = Red | Black

public export
data GoodTree :
  {height : Nat} ->
  {color : Color} ->
  {kt : Type} ->
  {kord : LawfulOrd kt} ->
  {keys : List kt} ->
  {vt : kt -> Type} -> Type
  where
  Empty : (0 _ : keys = []) -> GoodTree {height = 0, color = Black, keys}
  RedNode :
    {0 kord : LawfulOrd kt} ->
    (k : kt) ->
    {0 kp : In (k ==) keys} ->
    vt k ->
    GoodTree {height, color = Black, kt, kord, keys = filter (k >) keys, vt} ->
    GoodTree {height, color = Black, kt, kord, keys = filter (k <) keys, vt} ->
    GoodTree {height, color = Red, kt, kord, keys, vt}
  BlackNode :
    {0 kord : LawfulOrd kt} ->
    (k : kt) ->
    {0 kp : In (k ==) keys} ->
    vt k ->
    GoodTree {height, color = colorLeft, kt, kord, keys = filter (k >) keys, vt} ->
    GoodTree {height, color = colorRight, kt, kord, keys = filter (k <) keys, vt} ->
    GoodTree {height = S height, color = Black, kt, kord, keys, vt}

-- Like GoodTree but BadRedNode can have red children
public export
data BadTree :
  {height : Nat} ->
  {kt : Type} ->
  {kord : LawfulOrd kt} ->
  {keys : List kt} ->
  {vt : kt -> Type} -> Type
  where
  BadRedNode :
    {0 kord : LawfulOrd kt} ->
    (k : kt) ->
    {0 kp : In (k ==) keys} ->
    vt k ->
    GoodTree {height, kt, kord, keys = filter (k >) keys, vt} ->
    GoodTree {height, kt, kord, keys = filter (k <) keys, vt} ->
    BadTree {height, kt, kord, keys, vt}

max_stars_repo_name: L-as/idris-rbtree

max_issues_repo_name: L-as/idris-rbtree

max_forks_repo_name: L-as/idris-rbtree


text:
import Data.Vect

import Data.List.Views
import Data.Vect.Views
import Data.Nat.Views

{- 1 -}

total
equalSuffix : Eq a => List a -> List a -> List a
equalSuffix input1 input2 with (snocList input1)
  equalSuffix [] input2 | Empty = []
  equalSuffix (xs ++ [x]) input2 | (Snoc xsrec) with (snocList input2)
    equalSuffix (xs ++ [x]) [] | (Snoc xsrec) | Empty = []
    equalSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xsrec) | (Snoc ysrec)
         = if x == y
              then equalSuffix xs ys | xsrec | ysrec ++ [y]
              else []

{- 2 -}

total
mergeSort : Ord a => Vect n a -> Vect n a
mergeSort xs with (splitRec xs)
  mergeSort [] | SplitRecNil = []
  mergeSort [x] | SplitRecOne = [x]
  mergeSort (ys ++ zs) | (SplitRecPair lrec rrec)
      = merge (mergeSort ys | lrec) (mergeSort zs | rrec)

{- 3 -}

total
toBinary : Nat -> String
toBinary k with (halfRec k)
  toBinary Z | HalfRecZ = ""
  toBinary (n + n) | (HalfRecEven rec) = toBinary n | rec ++ "0"
  toBinary (S (n + n)) | (HalfRecOdd rec) = toBinary n | rec ++ "1"

{- 4 -}

palindrome : Eq a => List a -> Bool
palindrome input with (vList input)
  palindrome [] | VNil = True
  palindrome [x] | VOne = True
  palindrome (x :: (xs ++ [y])) | (VCons rec)
      = x == y && palindrome xs

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
||| Provides a data type for Monadic Stream Functions (MSFs)
||| together with associated interface implementations and
||| some core functionality.
|||
||| An MSF is an effectful computation from an input of type `i`
||| to an output of type `o`, that can be described using a rich
||| library of combinators and evaluated using function
||| `Data.MSF.Running.step`,
||| which not only produces an output for every input value
||| but also a new MSF to be used in the next evaluation step.
module Data.MSF.Core

import Data.MSF.Event
import Data.SOP

%default total

mutual
  ||| A heterogeneous list of MSFs. This is used both
  ||| for running several unrelated MSFs in parallel, in
  ||| which case it takes an n-ary product as input
  ||| and produces an n-ary product as output (see
  ||| function `par`), as well as for selecting a single
  ||| MSF to run based on an n-ary sum as input, in which
  ||| case a value of an n-ary sum is produced as output
  ||| (see function `choice` for this use case).
  public export
  data MSFList :  (m : Type -> Type)
               -> (is : List Type)
               -> (os : List Type)
               -> Type where
    Nil  : MSFList m [] []
    (::) :  (sf : MSF m i o)
         -> (sfs : MSFList m is os)
         -> MSFList m (i :: is) (o :: os)

  namespace FanList
    ||| A heterogeneous list of MSFs all of which
    ||| accept the same input type. This is used for
    ||| broadcasting a input value across several MSFs,
    ||| collecting the result as an n-ary product.
    ||| See also function `fan`.
    public export
    data FanList :  (m : Type -> Type)
                 -> (i : Type)
                 -> (os : List Type)
                 -> Type where
      Nil  : FanList m i Nil
      (::) :  (sf : MSF m i o)
           -> (sfs : FanList m i os)
           -> FanList m i (o :: os)

  namespace CollectList
    ||| A heterogeneous list of MSFs all of which
    ||| produce the same type of outup. This is used for
    ||| choosing a single MSF for producing a result based
    ||| on an n-ary sum as input. See also function `collect`.
    public export
    data CollectList :  (m  : Type -> Type)
                     -> (is : List Type)
                     -> (o  : Type)
                 -> Type where
      Nil  : CollectList m Nil o
      (::) :  (sf : MSF m i o)
           -> (sfs : CollectList m is o)
           -> CollectList m (i :: is) o

  ||| A monadic stream function (`MSF`) is used to
  ||| convert streams of input values of type `i` to
  ||| output values of type `o` in a monadic context `m`.
  |||
  ||| The [dunai](https://hackage.haskell.org/package/dunai)
  ||| library implements them as
  ||| `data MSF m i o = MSF (i -> m (o, MSF m i o))`
  ||| but this most general form does not go well with
  ||| the Idris totality checker.
  |||
  ||| It is therefore implemented as a set of primitive
  ||| constructors, some of which are truly primitives,
  ||| some of which are there for reasons of efficiency.
  ||| In later versions of this library, `MSF` might
  ||| no longer be publicly exported, so client code should
  ||| use the provided combinators instead of accessing the
  ||| data constructors directly.
  |||
  ||| `MSF` objects can be stepwise evaluated by invoking
  ||| function `Data.MSF.Running.step`.
  public export
  data MSF : (m : Type -> Type) -> (i : Type) -> (o : Type) -> Type where

    ||| The identity MSF
    Id        :  MSF m i i

    ||| The constant MSF
    Const     :  o -> MSF m i o

    ||| Lifts a pure function to an MSF
    Arr       :  (i -> o) -> MSF m i o

    ||| Lifts an effectful computation to an MSF
    Lifted    :  (i -> m o) -> MSF m i o

    ||| Sequencing of MSFs
    Seq       :  MSF m i x -> MSF m x o -> MSF m i o

    ||| Parallelising MSFs
    Par       :  MSFList m is os -> MSF m (NP I is) (NP I os)

    ||| Broadcasting a value to a list of MSFs
    ||| all taking the same input
    Fan       :  FanList m i os -> MSF m i (NP I os)

    ||| Choosing an MSF based on an n-ary sum as input
    Choice    :  MSFList m is os -> MSF m (NS I is) (NS I os)

    ||| Choosing an MSF (all of which produce the same output)
    ||| based on an n-ary sum as input
    Collect   :  CollectList m is o -> MSF m (NS I is) o

    ||| Feedback loops (stateful computations)
    Loop      :  s -> MSF m (NP I [s, i]) (NP I [s, o]) -> MSF m i o

    ||| Single time switching: Upon the first event,
    ||| the second stream function is calculated,
    ||| evaluated immediately and used henceforth.
    Switch    :  MSF m i (Either e o) -> (e -> MSF m i o) -> MSF m i o

--------------------------------------------------------------------------------
--          Lifting Primitives
--------------------------------------------------------------------------------

||| The identity MSF
export %inline
id : MSF m i i
id = Id

||| A constant MSF
export %inline
const : o -> MSF m i o
const = Const

||| Lifting a pure function to an MSF
export %inline
arr : (i -> o) -> MSF m i o
arr = Arr

||| Lifting an effectful computation to an MSF
export %inline
arrM : (i -> m o) -> MSF m i o
arrM = Lifted

||| Lifting a value in a context to an MSF
export %inline
constM : m o -> MSF m i o
constM = Lifted . const

--------------------------------------------------------------------------------
--          Sequencing MSFs
--------------------------------------------------------------------------------

infixr 1 >>>

||| Sequencing of MSFs
export %inline
(>>>) : MSF m i x -> MSF m x o -> MSF m i o
(>>>) = Seq

--------------------------------------------------------------------------------
--          Paralellising MSFs
--------------------------------------------------------------------------------

||| Runs a bundle of MSFs in parallel. This is
||| a generalization of `(***)` from `Control.Arrow`.
export %inline
par : MSFList m is os -> MSF m (NP I is) (NP I os)
par = Par

||| Broadcasts an input value across a list of MSFs,
||| all of which must accept the same type of input.
||| This is a generalization of `(&&&)` from `Control.Arrow`.
export %inline
fan : FanList m i os -> MSF m i (NP I os)
fan = Fan

||| Apply a binary function to the result of running
||| two MSFs in parallel.
export %inline
elementwise2 : (o1 -> o2 -> o3) -> MSF m i o1 -> MSF m i o2 -> MSF m i o3
elementwise2 f x y = fan [x,y] >>> arr (\[a,b] => f a b)

--------------------------------------------------------------------------------
--          Selecting MSFs
--------------------------------------------------------------------------------

||| Choose an MSF to run depending the input value
||| This is a generalization of `(+++)` from `Control.Arrow`.
export %inline
choice : MSFList m is os -> MSF m (NS I is) (NS I os)
choice = Choice

||| Choose an MSF all of which produce the same output.
||| This is a generalization of `(\|/)` from `Control.Arrow`.
export %inline
collect : CollectList m is o -> MSF m (NS I is) o
collect = Collect

--------------------------------------------------------------------------------
--          Loops and Stateful computations
--------------------------------------------------------------------------------

||| Feedback loops: Given an initial state value,
||| we can feedback the result of each evaluation
||| step and us it as the new state for the next step.
export %inline
feedback : s -> MSF m (NP I [s,i]) (NP I [s,o]) -> MSF m i o
feedback = Loop

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

export %inline
Functor (MSF m i) where
  map f = (>>> arr f)

export %inline
Applicative (MSF m i) where
  pure = Const
  (<*>) = elementwise2 apply

export %inline
Semigroup o => Semigroup (MSF m i o) where
  (<+>) = elementwise2 (<+>)

export %inline
Monoid o => Monoid (MSF m i o) where
  neutral = Const neutral

export %inline
Num o => Num (MSF m i o) where
  fromInteger = Const . fromInteger
  (+) = elementwise2 (+)
  (*) = elementwise2 (*)

export %inline
Neg o => Neg (MSF m i o) where
  (-)    = elementwise2 (-)
  negate = map negate

export %inline
Integral o => Integral (MSF m i o) where
  mod = elementwise2 mod
  div = elementwise2 div

export %inline
Fractional o => Fractional (MSF m i o) where
  (/)  = elementwise2 (/)

export %inline
FromString o => FromString (MSF m i o) where
  fromString = const . fromString


text:
module Web.Internal.WebidlTypes

import JS

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

export data DOMException : Type where [external]

export
ToFFI DOMException DOMException where toFFI = id

export
FromFFI DOMException DOMException where fromFFI = Just

export
SafeCast DOMException where
  safeCast = unsafeCastOnPrototypeName "DOMException"

--------------------------------------------------------------------------------
--          Callbacks
--------------------------------------------------------------------------------

export data Function : Type where [external]

export
ToFFI Function Function where toFFI = id

export
FromFFI Function Function where fromFFI = Just

export data VoidFunction : Type where [external]

export
ToFFI VoidFunction VoidFunction where toFFI = id

export
FromFFI VoidFunction VoidFunction where fromFFI = Just


text:
module MiddleLang

--------------------------------------------------
--               verifyable chunks
data Chunk : Type where
  ||| loop count, start location
  FORLOOP : Int -> Int -> Chunk

max_stars_repo_name: nickgeoca/QVM

max_issues_repo_name: nickgeoca/QVM

max_forks_repo_name: nickgeoca/QVM


text:
module Main

-- Using :di we can see the internal structure. MkFoo should be a newtype,
-- MkBar not
data Foo : Type where
  MkFoo : String -> Foo

data Bar : Type where
  [noNewtype]
  MkBar : String -> Bar


text:
module Web.Internal.PermissionsPrim

import JS
import Web.Internal.Types

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

namespace PermissionStatus

  export
  %foreign "browser:lambda:x=>x.onchange"
  prim__onchange : PermissionStatus -> PrimIO (Nullable EventHandlerNonNull)

  export
  %foreign "browser:lambda:(x,v)=>{x.onchange = v}"
  prim__setOnchange :  PermissionStatus
                    -> Nullable EventHandlerNonNull
                    -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.state"
  prim__state : PermissionStatus -> PrimIO String

namespace Permissions

  export
  %foreign "browser:lambda:(x,a)=>x.query(a)"
  prim__query : Permissions -> Object -> PrimIO (Promise PermissionStatus)

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

namespace CameraDevicePermissionDescriptor

  export
  %foreign "browser:lambda:(a)=> {panTiltZoom: a}"
  prim__new : UndefOr Boolean -> PrimIO CameraDevicePermissionDescriptor

  export
  %foreign "browser:lambda:x=>x.panTiltZoom"
  prim__panTiltZoom :  CameraDevicePermissionDescriptor
                    -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.panTiltZoom = v}"
  prim__setPanTiltZoom :  CameraDevicePermissionDescriptor
                       -> UndefOr Boolean
                       -> PrimIO ()

namespace DevicePermissionDescriptor

  export
  %foreign "browser:lambda:(a)=> {deviceId: a}"
  prim__new : UndefOr String -> PrimIO DevicePermissionDescriptor

  export
  %foreign "browser:lambda:x=>x.deviceId"
  prim__deviceId : DevicePermissionDescriptor -> PrimIO (UndefOr String)

  export
  %foreign "browser:lambda:(x,v)=>{x.deviceId = v}"
  prim__setDeviceId : DevicePermissionDescriptor -> UndefOr String -> PrimIO ()

namespace MidiPermissionDescriptor

  export
  %foreign "browser:lambda:(a)=> {sysex: a}"
  prim__new : UndefOr Boolean -> PrimIO MidiPermissionDescriptor

  export
  %foreign "browser:lambda:x=>x.sysex"
  prim__sysex : MidiPermissionDescriptor -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.sysex = v}"
  prim__setSysex : MidiPermissionDescriptor -> UndefOr Boolean -> PrimIO ()

namespace PermissionDescriptor

  export
  %foreign "browser:lambda:(a)=> {name: a}"
  prim__new : String -> PrimIO PermissionDescriptor

  export
  %foreign "browser:lambda:x=>x.name"
  prim__name : PermissionDescriptor -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.name = v}"
  prim__setName : PermissionDescriptor -> String -> PrimIO ()

namespace PermissionSetParameters

  export
  %foreign "browser:lambda:(a,b,c)=> {descriptor: a,state: b,oneRealm: c}"
  prim__new :  PermissionDescriptor
            -> String
            -> UndefOr Boolean
            -> PrimIO PermissionSetParameters

  export
  %foreign "browser:lambda:x=>x.descriptor"
  prim__descriptor : PermissionSetParameters -> PrimIO PermissionDescriptor

  export
  %foreign "browser:lambda:(x,v)=>{x.descriptor = v}"
  prim__setDescriptor :  PermissionSetParameters
                      -> PermissionDescriptor
                      -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.oneRealm"
  prim__oneRealm : PermissionSetParameters -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.oneRealm = v}"
  prim__setOneRealm : PermissionSetParameters -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.state"
  prim__state : PermissionSetParameters -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.state = v}"
  prim__setState : PermissionSetParameters -> String -> PrimIO ()

namespace PushPermissionDescriptor

  export
  %foreign "browser:lambda:(a)=> {userVisibleOnly: a}"
  prim__new : UndefOr Boolean -> PrimIO PushPermissionDescriptor

  export
  %foreign "browser:lambda:x=>x.userVisibleOnly"
  prim__userVisibleOnly : PushPermissionDescriptor -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.userVisibleOnly = v}"
  prim__setUserVisibleOnly :  PushPermissionDescriptor
                           -> UndefOr Boolean
                           -> PrimIO ()


text:
module Utils.Helpers

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

%hide Prelude.toList

export
setMap : Ord b => (a -> b) -> SortedSet a -> SortedSet b
setMap fn setv = fromList $ map fn (toList setv)

export
mapMap : Ord k2 => ((k1,a) -> (k2, b)) -> SortedMap k1 a -> SortedMap k2 b
mapMap fn mapv = fromList $ map fn (toList mapv)

export
mapValueMap : Ord k => (a -> b) -> SortedMap k a -> SortedMap k b
mapValueMap fn mapv = mapMap (\(k,v) => (k, fn v)) mapv

export
mapFilter : Ord k => ((k,a) -> Bool) -> SortedMap k a -> SortedMap k a
mapFilter fn mapv = fromList $ filter fn (toList mapv)

export
keyFilter : Ord k => (k -> Bool) -> SortedMap k a -> SortedMap k a
keyFilter fn mapv = mapFilter (fn . fst) mapv

export
maybeMap : (a -> b) -> Maybe a -> Maybe b
maybeMap _ Nothing = Nothing
maybeMap f (Just av) = Just (f av)

export
[dropDuplicateKeysSemigroup] Semigroup (SortedMap k v) where
  (<+>) = mergeLeft

export
[dropDuplicateKeysMonoid] (Ord k) => Monoid (SortedMap k v) using dropDuplicateKeysSemigroup where
  neutral = empty


text:
module Main

import BoundAst

%default total

max_stars_repo_name: Kazark/tyclgen

max_issues_repo_name: Kazark/tyclgen

max_forks_repo_name: Kazark/tyclgen


text:
module mmhelloworld.idrisjvmautoffisample.importer.JvmImporter

import IdrisJvm.IO
import IdrisJvm.JvmImport
import Java.Lang
import Java.Util

%access public export
%language TypeProviders

objectMapperClass : String
objectMapperClass = "com/fasterxml/jackson/databind/ObjectMapper"

jsonNodeClass : String
jsonNodeClass = "com/fasterxml/jackson/databind/JsonNode"

javaimport "mvn -f ../pom.xml exec:java@jvm-import-idris -Dexec.arguments=" [
    (objectMapperClass, ["<init>", "readTree"]),
    (jsonNodeClass, ["at", "asDouble"]),
    (integerClass, ["parseInt"])
]

max_stars_repo_name: mmhelloworld/idris-jvm-auto-ffi-sample

max_issues_repo_name: mmhelloworld/idris-jvm-auto-ffi-sample

max_forks_repo_name: mmhelloworld/idris-jvm-auto-ffi-sample


text:
module Demo.Other

%access public export
%default total

hello : String
hello = "hello"

max_stars_repo_name: roycrippen/scratch

max_issues_repo_name: roycrippen/scratch

max_forks_repo_name: roycrippen/scratch


text:
module Derive.Show

import Data.Vect

import Language.Reflection.Elab
import Language.Reflection.Utils
import Pruviloj.Core
import Pruviloj.Internals.TyConInfo
import Pruviloj.Internals

%access public export

isRType : Raw -> Bool
isRType RType = True
isRType _ = False

declareShow : (fam, sh : TTName) -> TyConInfo -> Elab TyDecl
declareShow fam eq info =
  do let paramArgs = map (\(n, t) => MkFunArg n t Implicit NotErased) (getParams info)
     constrs <- traverse
                     (\(n, t) =>
                        do n' <- gensym "constrarg"
                           pure $ MkFunArg n' `(Show ~(Var n)) Constraint NotErased) $
                     List.filter (isRType . snd) $
                     getParams info
     precn <- gensym "d"
     let precArg = with List [MkFunArg precn `(Prec) Explicit NotErased]
     arg <- applyTyCon (args info) (Var fam)
     pure $ Declare eq (paramArgs ++ constrs ++ precArg ++ arg) `(String)
  where
    makeImplicit : FunArg -> FunArg
    makeImplicit arg = record {plicity = Implicit} arg

    applyTyCon : List TyConArg -> Raw -> Elab (List FunArg)
    applyTyCon [] acc = pure $ [MkFunArg !(gensym "arg") acc Explicit NotErased]
    applyTyCon (TyConIndex arg :: args) acc =
        (\tl => makeImplicit arg :: tl) <$> applyTyCon args (RApp acc (Var (name arg)))
    applyTyCon (TyConParameter arg :: args) acc =
        applyTyCon args (RApp acc (Var (name arg)))

    getFunArg : TyConArg -> FunArg
    getFunArg (TyConParameter x) = makeImplicit x
    getFunArg (TyConIndex x)     = makeImplicit x

    mkArg : TTName -> Raw -> FunArg
    mkArg n t = MkFunArg n t Explicit NotErased

||| Compute the constructor name's representation in user output
strName : TTName -> String
strName (UN n) = case unpack n of
                   [] => ""
                   (c :: cs) => if isAlpha c then n else "(" ++ n ++ ")"
strName (NS n _) = strName n
strName (MN x y) = y
strName (SN x) = "**SN**" -- won't happen with user-declared types
strName nErased = "**Erased**" -- won't happen with user-declared types

||| Make the show clause for a single constructor
ctorClause : (fam, sh : TTName) -> (info : TyConInfo) ->
             (c : (TTName, List CtorArg, Raw)) -> Elab (FunClause Raw)
ctorClause fam sh info ctor =
  do -- Begin by making non-param names unique (so we can use them for holes as well)
    (cn, ctorArgs, resTy) <- processCtorArgs info ctor
    elabPatternClause
      (do -- First give consistent bindings to the parameters
          traverse {b=()} (\(n, ty) => do claim n ty ; unfocus n) (getParams info)
          -- Next create holes for arguments - do indices, then a hole for each actual arg
          -- Now make holes for non-param args
          traverse mkArgHole ctorArgs

          -- Now make a hole for the argument itself
          arg <- newHole "arg" resTy

          -- Now apply show, with holes for its args that we will fill
          -- with these ones. Most will be solved through unification,
          -- but not all.
          holes' <- apply (mkApp (Var sh) (map (Var . fst) (getParams info)))
                          (replicate (length (getParams info) +
                                      length (getIndices info) + 2)
                                     True)
          solve
          -- We can find the argument positions by counting
          -- holes. Drop the constraints and indices, then take
          -- an arg
          focus !(unsafeNth (1 + length (getParams info) + (length (getIndices info))) holes')
          apply (Var arg) []; solve

          -- Now we get the actual arguments in place
          focus arg
          apply (mkApp (Var cn) (map (Var . name . ctorFunArg) ctorArgs)) []
          solve)
      (if hasArgsToShow ctorArgs
         then do d <- newHole "d" `(Prec)
                 shownArgs <- newHole "args" `(String)
                 fill `(showCon ~(Var d) ~(RConstant (Str (strName cn))) ~(Var shownArgs)); solve
                 focus d; search
                 focus shownArgs
                 traverse_ showCtorArg ctorArgs
                 -- leaves behind a hole waiting for the last arg string - we just fill with ""
                 fill `(""); solve
         else do fill (RConstant (Str (strName cn))); solve)

  where mkArgHole : CtorArg -> Elab ()
        mkArgHole (CtorParameter _) = pure ()
        mkArgHole (CtorField arg) = do claim (name arg) (type arg)
                                       unfocus (name arg)

        ctorFunArg : CtorArg -> FunArg
        ctorFunArg (CtorParameter a) = a
        ctorFunArg (CtorField a) = a

        showOneArg : FunArg -> Elab ()
        showOneArg thisArg =
            do argHere <- newHole "thisArg" `(String)
               rest <- newHole "next" `(String)
               fill `(~(Var argHere) ++ ~(Var rest) : String)
               solve
               focus argHere
               if headName (type thisArg) == Just fam
                 then recursiveCall
                 else useShow
               focus rest
          where
            recursiveCall : Elab ()
            recursiveCall =
                do -- recursive call to self with initial space
                   afterSpace <- newHole "afterSpace" `(String)
                   fill `(" " ++ ~(Var afterSpace)); solve
                   focus afterSpace

                   hs <- apply (mkApp (Var sh) (map (Var . fst) (getParams info)))
                               (replicate (length (getParams info) +
                                           length (getIndices info)
                                           + 2)
                                          True)
                   solve
                   -- TC dict arguments to recursive call should be threaded through
                   traverse_
                     (\h => do ignore $ inHole h (resolveTC sh))
                     (List.take (length (getParams info)) hs)
                   prec <- unsafeNth (length (getParams info)) hs
                   focus prec; apply `(App : Prec) []; solve
                   field <- unsafeNth (1 + length (args info)) hs
                   ignore $ inHole field (apply (Var (name thisArg)) [] *> solve)

            useShow : Elab ()
            useShow =
                do -- call the real showArg
                   [tyH, dictH, xH] <- apply (Var `{showArg}) [True, True, True]
                   solve
                   focus xH; apply (Var (name thisArg)) []; solve
                   focus dictH; resolveTC sh

        hasArgsToShow : List CtorArg -> Bool
        hasArgsToShow [] = False
        hasArgsToShow (CtorParameter (MkFunArg _ _ Explicit _) :: _) = True
        hasArgsToShow (CtorField (MkFunArg _ _ Explicit _) :: _) = True
        hasArgsToShow (_ :: args) = hasArgsToShow args

        showCtorArg : CtorArg -> Elab ()
        showCtorArg ca = case ca of
                           CtorParameter a => showCtorArg' a
                           CtorField a => showCtorArg' a
          where showCtorArg' : FunArg -> Elab ()
                showCtorArg' (MkFunArg _ RType Explicit _) =
                    do h <- newHole "next" `(String)
                       fill `(" _" ++ ~(Var h) : String); solve
                       focus h
                showCtorArg' (MkFunArg _ _ Explicit Erased) =
                    do h <- newHole "next" `(String)
                       fill `(" _" ++ ~(Var h) : String); solve
                       focus h
                showCtorArg' thisArg@(MkFunArg name _ Explicit NotErased) =
                    showOneArg thisArg
                showCtorArg' _ = skip

instClause : (sh, instn : TTName) ->
             (info : TyConInfo) ->
             (instArgs, instConstrs : List FunArg) ->
             Elab (List (FunClause Raw))
instClause sh instn info instArgs instConstrs =
  do let baseCtorN = SN (ImplementationCtorN `{Show})
     (ctorN, _, _) <- lookupTyExact baseCtorN
     clause <- elabPatternClause
                 (do apply (Var instn)
                           (replicate (length instArgs +
                                       length instConstrs)
                                      True)
                     solve)
                 (do [ty, showImpl, showPrecImpl] <-
                        apply (Var ctorN) [True, False, False]
                     solve

                     -- ty was solved by unification, if things are going right
                     focus showImpl
                     shArg <- gensym "x"
                     attack; intro shArg
                     shPArgs <- apply (Var sh)
                                      (replicate (2 * length (getParams info) +
                                                  length (getIndices info) + 2)
                                                 True)
                     focus !(last shPArgs); apply (Var shArg) []; solve
                     traverse_ (\h => inHole h (exact `(Open : Prec) <|> resolveTC instn))
                               shPArgs
                     solve -- attack
                     solve -- the hole in the instance constructor

                     focus showPrecImpl
                     shPArgP <- gensym "d"
                     shPArgX <- gensym "x"
                     attack; intro shPArgP
                     attack; intro shPArgX
                     shPArgs' <- apply (Var sh)
                                       (replicate (2 * length (getParams info) +
                                                   length (getIndices info) + 2)
                                                  True)
                     focus !(last shPArgs'); apply (Var shPArgX) []; solve

                     focus !(unsafeNth (2 * length (getParams info) )
                                            shPArgs')
                     apply (Var shPArgP) []; solve
                     traverse_ (\h => inHole h (resolveTC instn)) shPArgs'
                     solve; solve -- attacks
                     solve) -- constructor hole

     pure [clause]

export
deriveShow : (fam : TTName) -> Elab ()
deriveShow fam =
    do sh <- flip NS !currentNamespace . SN . MetaN fam <$> gensym "showImpl"
       datatype <- lookupDatatypeExact fam
       info <- getTyConInfo (tyConArgs datatype) (tyConRes datatype)
       decl <- declareShow fam sh info
       declareType decl
       let instn = NS (SN $ ImplementationN `{Show} [show fam]) !currentNamespace
       instConstrs <- Foldable.concat <$>
                      traverse (\ param =>
                                  case param of
                                    (n, RType) => do constrn <- gensym "instarg"
                                                     pure [MkFunArg constrn
                                                                      `(Show ~(Var n) : Type)
                                                                      Constraint
                                                                      NotErased]
                                    _ => pure [])
                               (getParams info)
       let instArgs = map tcFunArg (args info)
       let instRes = RApp (Var `{Show})
                          (mkApp (Var fam)
                                 (map (Var . tcArgName) (args info)))
       declareType $ Declare instn (instArgs ++ instConstrs) instRes
       clauses <- traverse (ctorClause fam sh info) (constructors datatype)
       defineFunction $ DefineFun sh clauses
       defineFunction $
         DefineFun instn !(instClause sh instn info instArgs instConstrs)
       addImplementation `{Show} instn
       pure ()
  where tcArgName : TyConArg -> TTName
        tcArgName (TyConParameter x) = name x
        tcArgName (TyConIndex x) = name x

        tcFunArg : TyConArg -> FunArg
        tcFunArg (TyConParameter x) = record {plicity = Implicit} x
        tcFunArg (TyConIndex x) = record {plicity = Implicit} x

max_stars_repo_name: idris-industry/derive

max_issues_repo_name: idris-industry/derive

max_forks_repo_name: idris-industry/derive


text: module Meriv.Core.ExternRelation

max_stars_repo_name: Sintrastes/meriv-idr-prototype

max_issues_repo_name: Sintrastes/meriv-idr-prototype

max_forks_repo_name: Sintrastes/meriv-idr-prototype