text:
module SmallStepExpr

import Expr
import Maps

%access public export

%default total

data AVal : AExp -> Type where
  AV_Num : (n : Nat) -> AVal (ANum n)

data AStep : State -> AExp -> AExp -> Type where
  AS_Id : AStep st (AId i) (ANum (st i))
  AS_Plus1 : AStep st a1 a1' -> AStep st (APlus a1 a2) (APlus a1' a2)
  AS_Plus2 : AVal v1 -> AStep st a2 a2' -> AStep st (APlus v1 a2) (APlus v1 a2')
  AS_Plus : AStep st (APlus (ANum n1) (ANum n2)) (ANum (n1 + n2))
  AS_Minus1 : AStep st a1 a1' -> AStep st (AMinus a1 a2) (AMinus a1' a2)
  AS_Minus2 : AVal v1 -> AStep st a2 a2' ->
              AStep st (AMinus v1 a2) (AMinus v1 a2')
  AS_Minus : AStep st (AMinus (ANum n1) (ANum n2)) (ANum (minus n1 n2))
  AS_Mult1 : AStep st a1 a1' -> AStep st (AMult a1 a2) (AMult a1' a2)
  AS_Mult2 : AVal v1 -> AStep st a2 a2' -> AStep st (AMult v1 a2) (AMult v1 a2')
  AS_Mult : AStep st (AMult (ANum n1) (ANum n2)) (ANum (n1 * n2))

syntax [t] "/" [st] "-+>a" [t'] = AStep st t t'

data BStep : State -> BExp -> BExp -> Type where
  BS_Eq1 : AStep st a1 a1' -> BStep st (BEq a1 a2) (BEq a1' a2)
  BS_Eq2 : AVal v1 -> AStep st a2 a2' -> BStep st (BEq v1 a2) (BEq v1 a2')
  BS_Eq : BStep st
                (BEq (ANum n1) (ANum n2))
                (if n1 == n2 then BTrue else BFalse)
  BS_Le1 : AStep st a1 a1' -> BStep st (BLe a1 a2) (BLe a1' a2)
  BS_Le2 : AVal v1 -> AStep st a2 a2' -> BStep st (BLe v1 a2) (BLe v1 a2')
  BS_Le : BStep st
                (BLe (ANum n1) (ANum n2))
                (if lte n1 n2 then BTrue else BFalse)
  BS_NotStep : BStep st b b' -> BStep st (BNot b) (BNot b')
  BS_NotTrue : BStep st (BNot BTrue) BFalse
  BS_NotFalse : BStep st (BNot BFalse) BTrue
  BS_AndStep : BStep st b1 b1' -> BStep st (BAnd b1 b2) (BAnd b1' b2)
  BS_AndTrueStep : BStep st b2 b2' -> BStep st (BAnd BTrue b2) (BAnd BTrue b2')
  BS_AndTrueTrue : BStep st (BAnd BTrue BTrue) BTrue
  BS_AndTrueFalse : BStep st (BAnd BTrue BFalse) BFalse
  BS_AndFalse : BStep st (BAnd BFalse b2) BFalse

syntax [t] "/" [st] "-+>b" [t'] = BStep st t t'


text:
a1 : Char
a1 = 'a'

a2 : Char
a2 = 'a'

whyNot : a1 = a2
whyNot = ?hole

ext: idr


text:
module MyPkg

main : IO ()
main =
  putStrLn "Hello from MyPkg"

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Chapter.Concurrency.ProcessLib

import System.Concurrency.Channels

export
data MessagePID : (iface : reqType -> Type) -> Type where
     MkMessage : PID -> MessagePID iface

%access public export

NoRecv : Void -> Type
NoRecv = const Void

data ProcState = Ready
               | Sent
               | Looping

data Process : (iface : reqType -> Type) ->
               Type ->
               (in_state  : ProcState) ->
               (out_state : ProcState) ->
               Type where
     Request : MessagePID service_iface ->
               (msg : service_reqType) ->
               Process ifae (service_iface msg) st st
     Respond : ((msg : reqType) -> Process iface (iface msg) Ready Ready) ->
               Process iface (Maybe reqType) st Sent
     Spawn   : Process service_iface () Ready Looping ->
               Process iface (Maybe (MessagePID service_iface)) st st

     Loop    : Inf (Process iface a Ready Looping) ->
               Process iface a Sent Looping
     Action  : IO a -> Process iface a st st
     Pure    : a -> Process iface a st st
     (>>=)   : Process iface a st1 st2 ->
               (a -> Process iface b st2 st3) ->
               Process iface b st1 st3

data Fuel = Dry
          | More (Lazy Fuel)

%access export

partial
forever : Fuel
forever = More forever

run : Fuel -> Process iface t in_state out_state -> IO (Maybe t)
run fuel (Request {service_iface} (MkMessage proc) msg) =
    do Just chan <- connect proc
         | Nothing => pure Nothing
       if !(unsafeSend chan msg)
          then do Just x <- unsafeRecv (service_iface msg) chan
                    | Nothing => pure Nothing
                  pure (Just x)
          else pure Nothing
-- TODO: encapsulate timeout
run fuel (Respond {reqType} calc) =
    do Just sender <- listen 1
         | Nothing => pure (Just Nothing)
       Just msg <- unsafeRecv reqType sender
         | Nothing => pure (Just Nothing)
       Just res <- run fuel (calc msg)
         | Nothing => pure Nothing
       unsafeSend sender res
       pure (Just (Just msg))
run fuel (Spawn proc)       = do Just pid <- spawn (run fuel proc *> pure ())
                                   | Nothing => pure (Just Nothing)
                                 pure (Just (Just (MkMessage pid)))
run (More fuel) (Loop proc) = run fuel proc
run fuel (Action act)       = pure (Just !act)
run fuel (Pure val)         = pure (Just val)
run fuel (act >>= next)     = do Just x <- run fuel act
                                   | Nothing => pure Nothing
                                 run fuel (next x)
run Dry _                   = pure Nothing

%access public export

Service : (iface : reqType -> Type) -> Type -> Type
Service iface a = Process iface a Ready Looping

Client : Type -> Type
Client a = Process NoRecv a Ready Ready

partial export
runProc : Process iface () in_state out_state -> IO ()
runProc proc = run forever proc *> pure ()

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
||| An implementation of `Data.Heap` based on binomial trees.
||| This implementation is an adaptation of Okasaki's `BinomialHeap`
||| found on pp.20-25 of his book.
||| SEe also:
||| * [BinomialHeap in Agda](https://github.com/ericpony/FLOLAC-2014/blob/master/Analysis%20and%20synthesis%20of%20inductive%20families/Examples/BinomialHeap.agda)
||| *  [BinomialHeap in Haskell](https://jaspervdj.be/posts/2018-09-04-binomial-heaps-101.html#binomial-heaps-lets-build-it-up)
module Data.Heap.BinomialHeap

import Data.Vect

import public Data.Binary

%access public export
%default total

mutual
  ||| A Binomial Tree
  ||| quoting Okasaki:
  ||| A binomial tree is inductively defined as:
  ||| * a binomial tree of rank 0 is a singleton node
  ||| * a binomial tree of rank (n+1) is formed by linking 2 binomial trees
  |||   of rank n, making one tree the leftmost child of the other
  |||
  ||| Equivalently, a binomial tree of rank `r` is a tree with
  ||| `r` children `t_1 .. t_r` where each `t_i` has rank `r - i`.
  data BinTree : (rank : Nat) -> Type -> Type where
    MkTree : (elem : a) -> (subs : Children rank a) -> BinTree rank a

  ||| A helper type for children of a binomial tree, ensuring
  ||| subtrees are stored in increasing rank order.
  data Children : (rank : Nat) -> Type -> Type where
    CNil : Children 0 a
    CCons : BinTree k a -> Children k a -> Children (S k) a

||| A singleton binomial tree
Singleton : a -> BinTree 0 a
Singleton x = MkTree x CNil

||| Basic operation to _grow_ binomial trees
||| Takes 2 trees of equal rank `r` and forms a new tree of rank `S r`
link : (Ord a) => (left : BinTree r a) -> (right : BinTree r a) -> BinTree (S r) a
link left@(MkTree elem subs) right@(MkTree elem' subs') =
  if elem <= elem'
  then MkTree elem (CCons right subs)
  else MkTree elem' (CCons left subs')

||| A `Forest` is a list of `BinTree` with rank at most `rank`
||| @rank The rank of the largest `BinTree` contained in the Forest
||| @bin the `Binary` encoding of the occupied positions in this `Forest`. There
|||      is a tree at index `i` if the corresponding bit is `B1`
||| @a the type of elements contained in this forest
data Forest : (rank : Nat) -> (bin : Binary v) -> (a : Type) -> Type where
  FEnd : Forest rank BEnd a
  F0   :                   Forest (S rank) b a -> Forest rank (B0 b) a
  F1   : BinTree rank a -> Forest (S rank) b a -> Forest rank (B1 b) a

emptyForest : Forest rank BEnd a
emptyForest = FEnd

insertTree : (Ord a) => BinTree rank a -> Forest rank b a -> Forest rank (inc b) a
insertTree tree FEnd              = F1 tree FEnd
insertTree tree (F0 forest)       = F1 tree forest
insertTree tree (F1 tree' forest) = F0 (insertTree (link tree tree') forest)

mergeForests : (Ord a) => Forest rank b a -> Forest rank b' a
             -> Forest rank (add b b') a
mergeForests FEnd right {b'}   = rewrite sym (natIsBinary b') in right
mergeForests left FEnd {b} = ?hole
mergeForests _  _  = ?hole

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
import SnocList

total
isSuffix : Eq a => List a -> List a -> Bool
isSuffix input1 input2 with (snocList input1)
  isSuffix [] input2 | Empty = True
  isSuffix (xs ++ [x]) input2 | (Snoc xs_rec) with (snocList input2)
    isSuffix (xs ++ [x]) [] | (Snoc xs_rec) | Empty = False
    isSuffix (xs ++ [x]) (ys ++ [y]) | (Snoc xs_rec) | (Snoc ys_rec)
      = if x == y then isSuffix xs ys | xs_rec | ys_rec
                  else False

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module Compiler.Jvm.Jname

import Core.Name
import Data.List

public export
data Jname = Jqualified String String
           | Jsimple String

export
className : Jname -> String
className (Jqualified cname _) = cname
className (Jsimple _) = "main/Main"

export
methodName : Jname -> String
methodName (Jqualified _ mname) = mname
methodName (Jsimple mname) = mname

%inline
export
assemblerClass : String -> String
assemblerClass name = "io/github/mmhelloworld/idrisjvm/assembler/" ++ name

%foreign "jvm:transformCharacters,io/github/mmhelloworld/idrisjvm/assembler/IdrisName"
export
cleanupIdentifier : String -> String

%foreign "jvm:.replace,java/lang/String"
replace : String -> Char -> Char -> String

getSimpleNameWithSep : String -> Jname -> String
getSimpleNameWithSep _ (Jsimple n) = n
getSimpleNameWithSep sep (Jqualified q n) = q ++ sep ++ n

export
getSimpleName : Jname -> String
getSimpleName = getSimpleNameWithSep "/"

export
implementation Eq Jname where
    name1 == name2 = getSimpleName name1 == getSimpleName name2

export
implementation Ord Jname where
  compare name1 name2 = compare (getSimpleName name1) (getSimpleName name2)

export
implementation Show Jname where
    show = getSimpleName

export
jvmName : Name -> Jname
jvmName (NS ns n) =
  Jqualified (replace (cleanupIdentifier $ showNSWithSep "$" ns) '$' '/') $ getSimpleNameWithSep "$" (jvmName n)
jvmName (UN n) = Jsimple $ cleanupIdentifier (displayUserName n)
jvmName (MN n i) = Jsimple $ cleanupIdentifier n ++ "$" ++ show i
jvmName (PV n d) = Jsimple $ "$p" ++ getSimpleNameWithSep "$" (jvmName n)
jvmName (DN str n) = Jsimple $ cleanupIdentifier str ++ "$" ++ getSimpleNameWithSep "$" (jvmName n)
jvmName (Nested (i, x) n) = Jsimple $ "$n" ++ show i ++ "$" ++ show x ++ "$" ++ getSimpleNameWithSep "$" (jvmName n)
jvmName (CaseBlock x y) = Jsimple $ "$c" ++ cleanupIdentifier (show x) ++ "$" ++ show y
jvmName (WithBlock x y) = Jsimple $ "$w" ++ cleanupIdentifier (show x) ++ "$" ++ show y
jvmName (Resolved i) = Jsimple $ "$r" ++ show i

export
jvmSimpleName : Name -> String
jvmSimpleName = getSimpleName . jvmName

%inline
jvmIdrisMainMethodName : String
jvmIdrisMainMethodName = "jvm$idrisMain"

jvmIdrisMainClass : String -> String
jvmIdrisMainClass rootPackage = rootPackage ++ "/Main"

export
idrisMainFunctionName : String -> Name
idrisMainFunctionName rootPackage = NS (mkNamespace $ rootPackage ++ ".Main") (UN $ Basic jvmIdrisMainMethodName)


text:
module Main

import Data.Vect
import Data.Fin

%language DSLNotation

data Ty = TyInt | TyBool| TyFun Ty Ty

interpTy : Ty -> Type
interpTy TyInt       = Int
interpTy TyBool      = Bool
interpTy (TyFun s t) = interpTy s -> interpTy t

using (G : Vect n Ty)

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

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

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

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

  %static
  lam_ : TTName -> Expr (a :: G) t -> Expr G (TyFun a t)
  lam_ _ = Lam

  dsl expr
      lambda = lam_
      variable = Var
      index_first = Stop
      index_next = Pop

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

  eId : Expr G (TyFun TyInt TyInt)
  eId = expr (\x => x)

  eTEST : Expr G (TyFun TyInt (TyFun TyInt TyInt))
  eTEST = expr (\x, y => y)

  eAdd : Expr G (TyFun TyInt (TyFun TyInt TyInt))
  eAdd = expr (\x, y => Op (+) x y)

--   eDouble : Expr G (TyFun TyInt TyInt)
--   eDouble = Lam (App (App (Lam (Lam (Op' (+) (Var FZ) (Var (FS FZ))))) (Var FZ)) (Var FZ))

  eDouble : Expr G (TyFun TyInt TyInt)
  eDouble = expr (\x => App (App eAdd x) (Var Stop))

--   app : Lazy (Expr G (TyFun a t)) -> Expr G a -> Expr G t
--   app = \f, a => App (Force f) a

  eFac : Expr G (TyFun TyInt TyInt)
  eFac = expr (\x => If (Op (==) x (Val 0))
                 (Val 1)
                 (Op (*) (App eFac (Op (-) x (Val 1))) x))

  -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

  eProg : Expr G (TyFun TyInt (TyFun TyInt TyInt))
  eProg = Lam (Lam
                    (Bind (App eDouble (Var (Pop Stop)))
              (\x => Bind (App eDouble (Var Stop))
              (\y => Bind (App eDouble (Val x))
              (\z => App (App eAdd (Val y)) (Val z))))))

test : Int
test = interp [] eProg 2 2

testFac : Int
testFac = interp [] eFac 4

testEnv : Int -> Env [TyInt,TyInt]
testEnv x = [x,x]

main : IO ()
main = do { printLn testFac
            printLn test }

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:
import Aoc
import Data.Nat
import Data.Strings

Point : Type
Point = (Integer, Integer)

||| Add two points.
(+~) : Point -> Point -> Point
(+~) (x,y) (x',y') = (x+x',y+y')
infixl 5 +~

||| Scale a point.
(*~) : Integer -> Point -> Point
(*~) n (x,y) = (n*x,n*y)
infixl 6 *~

||| Turn a vector 90° to the left. (+x is >, +y is ^)
turnLeft : Point -> Point
turnLeft (x,y) = (-y,x)

||| Turn a vector 90° to the right. (+x is >, +y is ^)
turnRight : Point -> Point
turnRight (x,y) = (y,-x)

manhattanNorm : Point -> Integer
manhattanNorm (x,y) = abs x + abs y

record Ship where
  constructor MkShip
  position : Point
  direction : Point

data Instruction
  = North Integer
  | South Integer
  | East Integer
  | West Integer
  | Left90 Nat
  | Right90 Nat
  | Forward Integer

||| Move a ship's position.
move : Point -> Ship -> Ship
move d s = record { position $= (+~ d) } s

||| Move a ship's waypoint (direction vector).
moveWaypoint : Point -> Ship -> Ship
moveWaypoint d s = record { direction $= (+~ d) } s

||| Follow an instruction, * style.
step1 : Ship -> Instruction -> Ship
step1 s (North n) = move (0, n) s
step1 s (South n) = move (0, -n) s
step1 s (East n) = move (n, 0) s
step1 s (West n) = move (-n, 0) s
step1 s (Left90 n) = record { direction $= times n turnLeft } s
step1 s (Right90 n) = record { direction $= times n turnRight } s
step1 s (Forward n) = move (n *~ s.direction) s

||| Follow an instruction, ** style.
step2 : Ship -> Instruction -> Ship
step2 s (North n) = moveWaypoint (0, n) s
step2 s (South n) = moveWaypoint (0, -n) s
step2 s (East n) = moveWaypoint (n, 0) s
step2 s (West n) = moveWaypoint (-n, 0) s
step2 s (Left90 n) = record { direction $= times n turnLeft } s
step2 s (Right90 n) = record { direction $= times n turnRight } s
step2 s (Forward n) = move (n *~ s.direction) s

||| Try to divide a natural number by 90.
div90 : Nat -> Maybe Nat
div90 n =
  case divmodNatNZ n 90 SIsNotZ of
    (k, 0) => Just k
    _ => Nothing

||| Try to parse an instruciton.
parseInstruction : String -> Maybe Instruction
parseInstruction s =
  case break isDigit s of
    ("N", n) => North <$> parsePositive n
    ("S", n) => South <$> parsePositive n
    ("E", n) => East <$> parsePositive n
    ("W", n) => West <$> parsePositive n
    ("L", n) => Left90 <$> (parsePositive n >>= div90)
    ("R", n) => Right90 <$> (parsePositive n >>= div90)
    ("F", n) => Forward <$> parsePositive n
    _ => Nothing

main : IO ()
main = do
  xs <- parseLines parseInstruction
  let ship1 = foldl step1 (MkShip (0, 0) (1, 0)) xs
  putStr "*   "; printLn (manhattanNorm ship1.position)
  let ship2 = foldl step2 (MkShip (0, 0) (10, 1)) xs
  putStr "**  "; printLn (manhattanNorm ship2.position)


text:
module Quantities.SIDerivedQuantities

import Quantities.Core
import Quantities.SIBaseQuantities

%default total
%access public export

-- Examples of coherent derived units in the SI expressed in terms of base
-- units

Area : Quantity
Area = Length ^ 2

Volume : Quantity
Volume = Length ^ 3

Speed : Quantity
Speed = Length </> Time

Velocity : Quantity
Velocity = Speed

Acceleration : Quantity
Acceleration = Speed </> Time

Wavenumber : Quantity
Wavenumber = Length ^ (-1)

Density : Quantity
Density = Mass </> Volume

MassDensity : Quantity
MassDensity = Density

SurfaceDensity : Quantity
SurfaceDensity = Mass </> Area

SpecificVolume : Quantity
SpecificVolume = Volume </> Mass

CurrentDensity : Quantity
CurrentDensity = ElectricCurrent </> Area

MagneticFieldStrength : Quantity
MagneticFieldStrength = ElectricCurrent </> Length

AmountConcentration : Quantity
AmountConcentration = AmountOfSubstance </> Volume

Concentration : Quantity
Concentration = AmountConcentration

MassConcentration : Quantity
MassConcentration = Mass </> Volume

Luminance : Quantity
Luminance = LuminousIntensity </> Area

RefractiveIndex : Quantity
RefractiveIndex = Scalar

RelativePermeability : Quantity
RelativePermeability = Scalar

-- Coherent derived units in the SI with special names and symbols

PlaneAngle : Quantity
PlaneAngle = Scalar

SolidAngle : Quantity
SolidAngle = Scalar

Frequency : Quantity
Frequency = Time ^ (-1)

Force' : Quantity
Force' = Acceleration <*> Mass

Pressure : Quantity
Pressure = Force' </> Area

Stress : Quantity
Stress = Pressure

Energy : Quantity
Energy = Force' <*> Length

Work : Quantity
Work = Energy

AmountOfHeat : Quantity
AmountOfHeat = Energy

Power : Quantity
Power = Energy </> Time

RadiantFlux : Quantity
RadiantFlux = Power

ElectricCharge : Quantity
ElectricCharge = Time <*> ElectricCurrent

AmountOfElectricity : Quantity
AmountOfElectricity = ElectricCharge

ElectricPotentialDifference : Quantity
ElectricPotentialDifference = Power </> ElectricCurrent

ElectromotiveForce : Quantity
ElectromotiveForce = ElectricPotentialDifference

Capacitance : Quantity
Capacitance = ElectricCharge </> ElectricPotentialDifference

ElectricResistance : Quantity
ElectricResistance = ElectricPotentialDifference </> ElectricCurrent

ElectricConductance : Quantity
ElectricConductance = ElectricCurrent </> ElectricPotentialDifference

MagneticFlux : Quantity
MagneticFlux = Time <*> ElectricPotentialDifference

MagneticFluxDensity : Quantity
MagneticFluxDensity = MagneticFlux </> Area

Inductance : Quantity
Inductance = MagneticFlux </> ElectricCurrent

-- Celsius temperature

LuminousFlux : Quantity
LuminousFlux = LuminousIntensity <*> SolidAngle

Illuminance : Quantity
Illuminance = LuminousFlux </> Area

ActivityReferredToARadionuclide : Quantity
ActivityReferredToARadionuclide = Time ^ (-1)

-- ... sometimes incorrectly called
Radioactivity : Quantity
Radioactivity = ActivityReferredToARadionuclide

AbsorbedDose : Quantity
AbsorbedDose = Energy </> Mass

SpecificEnergy : Quantity
SpecificEnergy = AbsorbedDose

Kerma : Quantity
Kerma = AbsorbedDose

DoseEquivalent : Quantity
DoseEquivalent = Energy </> Mass

AmbientDoseEquivalent : Quantity
AmbientDoseEquivalent = DoseEquivalent

DirectionalDoseEquivalent : Quantity
DirectionalDoseEquivalent = DoseEquivalent

PersonalDoseEquivalent : Quantity
PersonalDoseEquivalent = DoseEquivalent

CatalyticActivity : Quantity
CatalyticActivity = AmountOfSubstance </> Time

-- Examples of SI coherent derived units whose names and symbols include SI
-- coherent derived units with special names and symbols

DynamicViscosity : Quantity
DynamicViscosity = Stress <*> Time

KinematicViscosity : Quantity
KinematicViscosity = Area </> Time

MomentOfForce : Quantity
MomentOfForce = Force' <*> Length

Moment : Quantity
Moment = MomentOfForce

Torque : Quantity
Torque = MomentOfForce

SurfaceTension : Quantity
SurfaceTension = Force' </> Length

AngularVelocity : Quantity
AngularVelocity = PlaneAngle </> Time

AngularAcceleration : Quantity
AngularAcceleration = AngularVelocity </> Time

HeatFluxDensity : Quantity
HeatFluxDensity = Power </> Area

Irradiance : Quantity
Irradiance = HeatFluxDensity

HeatCapacity : Quantity
HeatCapacity = Energy </> Temperature

Entropy : Quantity
Entropy = HeatCapacity

SpecificHeatCapacity : Quantity
SpecificHeatCapacity = HeatCapacity </> Mass

SpecificEntropy : Quantity
SpecificEntropy = Entropy </> Mass

ThermalConductivity : Quantity
ThermalConductivity = Power </> (Length <*> Temperature)

EnergyDensity : Quantity
EnergyDensity = Energy </> Volume

ElectricFieldStrength : Quantity
ElectricFieldStrength = ElectricPotentialDifference </> Length

ElectricChargeDensity : Quantity
ElectricChargeDensity = ElectricCharge </> Volume

SurfaceChargeDensity : Quantity
SurfaceChargeDensity = ElectricCharge </> Area

ElectricFluxDensity : Quantity
ElectricFluxDensity = SurfaceChargeDensity

ElectricDisplacement : Quantity
ElectricDisplacement = SurfaceChargeDensity

Permettivity : Quantity
Permettivity = Capacitance </> Length

Permeability : Quantity
Permeability = Inductance </> Length

MolarEnergy : Quantity
MolarEnergy = Energy </> AmountOfSubstance

MolarHeatCapacity : Quantity
MolarHeatCapacity = MolarEnergy

Exposure : Quantity
Exposure = ElectricCharge </> Mass

AbsorbedDoseRate : Quantity
AbsorbedDoseRate = AbsorbedDose </> Time

RadiantIntensity : Quantity
RadiantIntensity = Power </> SolidAngle

Radiance : Quantity
Radiance = RadiantIntensity </> Area

CatalyticActivityConcentration : Quantity
CatalyticActivityConcentration = CatalyticActivity </> Volume

max_stars_repo_name: timjb/quantities

max_issues_repo_name: timjb/quantities

max_forks_repo_name: timjb/quantities


text:
module Minecraft.Base.PreClassic.Dirt.ItemEntity.Export

import public Minecraft.Core.Entity.Export
import public Minecraft.Base.PreClassic.Dirt.Item
import public Minecraft.Base.PreClassic.Dirt.ItemEntity

%default total

[dirtItemEntity']
Pickup Dirt.ItemEntity where
  collect self = new Dirt.Item self.base.item

[dirtVtbl']
Vtbl Dirt.ItemEntity where
  vtable (Pickup   Dirt.ItemEntity) = Just dirtItemEntity
  vtable (Entity   Dirt.ItemEntity) = Just %search
  vtable (Tangible Dirt.ItemEntity) = Just %search
  vtable _ = Nothing

dirtItemEntity = dirtItemEntity'
dirtVtbl = dirtVtbl'

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
||| Spec: https://webassembly.github.io/spec/core/syntax/types.html#table-types
module WebAssembly.Structure.Types.TableTypes

import WebAssembly.Structure.Types.Limits

import Decidable.Equality

-- Definition

public export
data ElemType : Type where
  FuncRef : ElemType

public export
TableType : Type
TableType = (Limits, ElemType)

-- Equality

-- Decidable Equality

public export
implementation DecEq ElemType where
  decEq FuncRef FuncRef = Yes Refl

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
--    Copyright 2017, the blau.io contributors
--
--    Licensed under the Apache License, Version 2.0 (the "License");
--    you may not use this file except in compliance with the License.
--    You may obtain a copy of the License at
--
--        http://www.apache.org/licenses/LICENSE-2.0
--
--    Unless required by applicable law or agreed to in writing, software
--    distributed under the License is distributed on an "AS IS" BASIS,
--    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--    See the License for the specific language governing permissions and
--    limitations under the License.

module API.Web.DOM.Event

import IdrisScript

%access public export
%default total

||| An Event is an object used for signaling that something has occured, e.g.,
||| that an image has completed downloading.
|||
||| The original interface specification can be found at
||| https://dom.spec.whatwg.org/#interface-event
record Event where
  constructor New
  ||| The type of *Event*, e.g. "`click`", "`hashchange`", or "`submit`"
  type : String
  ||| Non standard field for easier JS integration
  self : JSRef

max_stars_repo_name: blau-io/idris-web

max_issues_repo_name: pierrebeaucamp/idris-dom

max_forks_repo_name: pierrebeaucamp/idris-dom


text:
module DNSCodes
import IdrisNet.Socket
import IdrisNet.PacketLang

%access public

{- A module specifying the relations between codes and higher-level
 - data types. There is nothing of remotely any interest in here.

-}
%default total

data DNSHdrOpcode = QUERY | IQUERY | STATUS

instance Show DNSHdrOpcode where
  show QUERY = "QUERY"
  show IQUERY = "IQUERY"
  show STATUS = "STATUS"

dnsCodeToOpcode : Bounded 4 -> Maybe DNSHdrOpcode
dnsCodeToOpcode (BInt 0 oh) = Just QUERY
dnsCodeToOpcode (BInt 1 oh) = Just IQUERY
dnsCodeToOpcode (BInt 2 oh) = Just STATUS
dnsCodeToOpcode _ = Nothing

dnsOpcodeToCode : DNSHdrOpcode -> Bounded 4
dnsOpcodeToCode QUERY = BInt 0 oh
dnsOpcodeToCode IQUERY = BInt 1 oh
dnsOpcodeToCode STATUS = BInt 2 oh

data DNSClass = DNSClassIN -- Internet
  -- None of the following are used, anyway...
{-
              | DNSClassCS  -- CSNET
              | DNSClassCH -- CHAOS
              | DNSClassHS -- Hesiod
-}

instance Show DNSClass where
  show DNSClassIN = "IN"

data DNSClassRel : Int -> DNSClass -> Type where
  DNSClassRelIN : DNSClassRel 1 DNSClassIN
{-
  DNSClassRelCS : DNSClassRel 2 DNSClassCS
  DNSClassRelCH : DNSClassRel 3 DNSClassCH
  DNSClassRelHS : DNSClassRel 4 DNSClassHS
-}
dnsClassRel : (code : Int) -> (cls : DNSClass) -> Maybe (DNSClassRel code cls)
dnsClassRel 1 DNSClassIN = Just DNSClassRelIN
dnsClassRel _ _ = Nothing
{-
dnsClassToRel {code = 2} DNSClassCS = DNSClassRelCS
dnsClassToRel {code = 3} DNSClassCH = DNSClassRelCH
dnsClassToRel {code = 4} DNSClassHS = DNSClassRelHS
-}
dnsCodeToClass : (code : Int) -> Maybe DNSClass
dnsCodeToClass 1 = Just DNSClassIN
dnsCodeToClass _ = Nothing

dnsClassToCode : DNSClass -> Int
dnsClassToCode DNSClassIN = 1

dnsCodeToClass' : Bounded 16 -> Maybe DNSClass
dnsCodeToClass' (BInt 1 oh) = Just DNSClassIN
dnsCodeToClass' _ = Nothing

dnsClassToCode' : DNSClass -> Bounded 16
dnsClassToCode' DNSClassIN = BInt 1 oh

{-
dnsCodeToClass {cls = DNSClassCS} 2 = Just DNSClassRelCS
dnsCodeToClass {cls = DNSClassCH} 3 = Just DNSClassRelCH
dnsCodeToClass {cls = DNSClassHS} 4 = Just DNSClassRelHS
-}

data DNSQClass = DNSQClassIN -- Internet
               | DNSQClassANY -- Any class
               | DNSQClassCS  -- CSNET
               | DNSQClassCH -- CHAOS
               | DNSQClassHS -- Hesiod

instance Show DNSQClass where
  show DNSQClassIN = "IN"
  show DNSQClassANY = "ANY"
  show DNSQClassCS = "CS"
  show DNSQClassCH = "CH"
  show DNSQClassHS = "HS"

dnsCodeToQClass : (Bounded 16) -> Maybe DNSQClass
dnsCodeToQClass (BInt 1 oh) = Just DNSQClassIN
dnsCodeToQClass (BInt 2 oh) = Just DNSQClassCS
dnsCodeToQClass (BInt 3 oh) = Just DNSQClassCH
dnsCodeToQClass (BInt 4 oh) = Just DNSQClassHS
dnsCodeToQClass (BInt 255 oh) = Just DNSQClassANY
dnsCodeToQClass _ = Nothing

dnsQClassToCode : DNSQClass -> Bounded 16
dnsQClassToCode DNSQClassIN = BInt 1 oh
dnsQClassToCode DNSQClassCS = BInt 2 oh
dnsQClassToCode DNSQClassCH = BInt 3 oh
dnsQClassToCode DNSQClassHS = BInt 4 oh
dnsQClassToCode DNSQClassANY = BInt 255 oh

-- A few constants... Might change this
A_VAL : Int
A_VAL = 1

NS_VAL : Int
NS_VAL = 2

CNAME_VAL : Int
CNAME_VAL = 5

AAAA_VAL : Int
AAAA_VAL = 28

IN_VAL : Int
IN_VAL = 1

SOA_VAL : Int
SOA_VAL = 6
-- Type descriptions taken from RFC1035
           -- s | DNSTypeMD -- A mail destination (obsolete, use MX)
           -- s | DNSTypeMF -- A mail forwarder (obsolete, use MX)
           -- s | DNSTypeSOA -- Start of authority
           -- s | DNSTypeMB -- Mailbox domain name
           -- s | DNSTypeMG -- Mail group member
           -- s | DNSTypeMR -- Mail rename domain name
           -- s | DNSTypeWKS -- Well-known service description
           -- s | DNSTypeHINFO -- Host information
           -- s | DNSTypeMINFO -- Mailbox or mail list informatio n

data DNSType = DNSTypeA -- A host address
             | DNSTypeNS -- An authoritative name server
             | DNSTypeCNAME -- Canonical name for an alias
             | DNSTypeNULL -- Null RR
             | DNSTypePTR -- A domain name pointer
             | DNSTypeMX -- Mail exchange
             | DNSTypeTXT -- Text record
             | DNSTypeAAAA -- IPv6 Host Address
             | DNSTypeSOA

instance Show DNSType where
  show DNSTypeA = "A"
  show DNSTypeNS = "NA"
  show DNSTypeCNAME = "CNAME"
  show DNSTypeNULL = "NULL"
  show DNSTypePTR = "MX"
  show DNSTypeTXT = "TXT"
  show DNSTypeAAAA = "AAAA"
  show DNSTypeSOA = "SOA"

-- Question types
data DNSQType = DNSQTypeAXFR -- Request for transfer of entire zone
              | DNSQTypeMAILB -- Request for mailbox-related records
              | DNSQTypeMAILA -- Request for mail agent RRs (obsolete, use MX)
              | DNSQTypeALL -- Request for all records
              | DNSQTypeA -- A host address
              | DNSQTypeNS -- An authoritative name server
              | DNSQTypeCNAME -- Canonical name for an alias
              | DNSQTypeNULL -- Null RR
              | DNSQTypePTR -- A domain name pointer
              | DNSQTypeMX -- Mail exchange
              | DNSQTypeTXT -- Text record
              | DNSQTypeAAAA -- IPv6 Host Address
              | DNSQTypeSOA

instance Show DNSQType where
  show DNSQTypeAXFR = "AXFR"
  show DNSQTypeMAILA = "MAILA"
  show DNSQTypeMAILB = "MAILB"
  show DNSQTypeALL = "ALL"
  show DNSQTypeA = "A"
  show DNSQTypeNS = "NA"
  show DNSQTypeCNAME = "CNAME"
  show DNSQTypeNULL = "NULL"
  show DNSQTypePTR = "MX"
  show DNSQTypeTXT = "TXT"
  show DNSQTypeAAAA = "AAAA"
  show DNSQTypeSOA = "SOA"

-- stop parsing comments
            -- s | DNSQTypeMD -- A mail destination (obsolete, use MX)
            -- s | DNSQTypeMF -- A mail forwarder (obsolete, use MX)
            -- s | DNSQTypeSOA -- Start of authority
            -- s | DNSQTypeMB -- Mailbox domain name
            -- s | DNSQTypeMG -- Mail group member
            -- s | DNSQTypeMR -- Mail rename domain name
            -- s | DNSQTypeWKS -- Well-known service description
            -- s | DNSQTypeHINFO -- Host information
            -- s | DNSQTypeMINFO -- Mailbox or mail list informatio n

{- TODO (possibly?): make this a tad cleaner -}

data DNSTypeRel : Int -> DNSType -> Type where
  DNSTypeRelA : DNSTypeRel 1 DNSTypeA
  DNSTypeRelNS : DNSTypeRel NS_VAL DNSTypeNS
  DNSTypeRelCNAME : DNSTypeRel CNAME_VAL DNSTypeCNAME
  DNSTypeRelNULL : DNSTypeRel 10 DNSTypeNULL
  DNSTypeRelPTR : DNSTypeRel 12 DNSTypePTR
  DNSTypeRelMX : DNSTypeRel 15 DNSTypeMX
  DNSTypeRelTXT : DNSTypeRel 16 DNSTypeTXT
  DNSTypeRelAAAA : DNSTypeRel AAAA_VAL DNSTypeAAAA
 -- DNSTypeRelMD : DNSTypeRel 3 DNSTypeMD
 -- DNSTypeRelMF : DNSTypeRel 4 DNSTypeMF
 -- DNSTypeRelSOA : DNSTypeRel 6 DNSTypeSOA
 -- DNSTypeRelMB : DNSTypeRel 7 DNSTypeMB
 -- DNSTypeRelMG : DNSTypeRel 8 DNSTypeMG
 -- DNSTypeRelMR : DNSTypeRel 9 DNSTypeMR
  -- DNSTypeRelWKS : DNSTypeRel 11 DNSTypeWKS
  -- DNSTypeRelHINFO : DNSTypeRel 13 DNSTypeHINFO
  -- DNSTypeRelMINFO : DNSTypeRel 14 DNSTypeMINFO

data DNSQTypeRel : Int -> DNSQType -> Type where
  DNSQTypeRelA : DNSQTypeRel 1 DNSQTypeA
  DNSQTypeRelNS : DNSQTypeRel NS_VAL DNSQTypeNS
  DNSQTypeRelCNAME : DNSQTypeRel CNAME_VAL DNSQTypeCNAME
  DNSQTypeRelNULL : DNSQTypeRel 10 DNSQTypeNULL
  DNSQTypeRelPTR : DNSQTypeRel 12 DNSQTypePTR
  DNSQTypeRelMX : DNSQTypeRel 15 DNSQTypeMX
  DNSQTypeRelTXT : DNSQTypeRel 16 DNSQTypeTXT
  DNSQTypeRelAAAA : DNSQTypeRel AAAA_VAL DNSQTypeAAAA
  DNSQTypeRelAXFR : DNSQTypeRel 252 DNSQTypeAXFR
  DNSQTypeRelMAILB : DNSQTypeRel 253 DNSQTypeMAILB
  DNSQTypeRelMAILA : DNSQTypeRel 254 DNSQTypeMAILA
  DNSQTypeRelALL : DNSQTypeRel 255 DNSQTypeALL
--  DNSQTypeRelMD : DNSQTypeRel 3 DNSQTypeMD
--  DNSQTypeRelMF : DNSQTypeRel 4 DNSQTypeMF
--  DNSQTypeRelSOA : DNSQTypeRel 6 DNSQTypeSOA
--  DNSQTypeRelMB : DNSQTypeRel 7 DNSQTypeMB
--  DNSQTypeRelMG : DNSQTypeRel 8 DNSQTypeMG
--  DNSQTypeRelMR : DNSQTypeRel 9 DNSQTypeMR
--  DNSQTypeRelWKS : DNSQTypeRel 11 DNSQTypeWKS
--  DNSQTypeRelHINFO : DNSQTypeRel 13 DNSQTypeHINFO
--  DNSQTypeRelMINFO : DNSQTypeRel 14 DNSQTypeMINFO

dnsTypeToCode' : DNSType -> Bounded 16
dnsTypeToCode' DNSTypeA = (BInt 1 oh)
dnsTypeToCode' DNSTypeNS = (BInt 2 oh)
dnsTypeToCode' DNSTypeCNAME = (BInt 5 oh)
dnsTypeToCode' DNSTypeNULL = (BInt 10 oh)
dnsTypeToCode' DNSTypePTR = (BInt 12 oh)
dnsTypeToCode' DNSTypeMX = (BInt 15 oh)
dnsTypeToCode' DNSTypeTXT = (BInt 16 oh)
dnsTypeToCode' DNSTypeAAAA = (BInt 28 oh)
dnsTypeToCode' DNSTypeSOA = (BInt 6 oh)

dnsTypeToCode : DNSType -> Int
dnsTypeToCode DNSTypeA = 1
dnsTypeToCode DNSTypeNS = 2
dnsTypeToCode DNSTypeCNAME = 5
dnsTypeToCode DNSTypeNULL = 10
dnsTypeToCode DNSTypePTR = 12
dnsTypeToCode DNSTypeMX = 15
dnsTypeToCode DNSTypeTXT = 16
dnsTypeToCode DNSTypeAAAA = 28
dnsTypeToCode DNSTypeSOA = 6

dnsCodeToType' : (Bounded 16) -> Maybe DNSType
dnsCodeToType' (BInt 1 oh) = Just DNSTypeA
dnsCodeToType' (BInt 2 oh) = Just DNSTypeNS
dnsCodeToType' (BInt 5 oh) = Just DNSTypeCNAME
dnsCodeToType' (BInt 6 oh) = Just DNSTypeSOA
dnsCodeToType' (BInt 10 oh) = Just DNSTypeNULL
dnsCodeToType' (BInt 12 oh) = Just DNSTypePTR
dnsCodeToType' (BInt 15 oh) = Just DNSTypeMX
dnsCodeToType' (BInt 16 oh) = Just DNSTypeTXT
dnsCodeToType' (BInt 28 oh) = Just DNSTypeAAAA
dnsCodeToType' (BInt _ oh) = Nothing

dnsCodeToType : (code : Int) -> Maybe DNSType
dnsCodeToType 1 = Just DNSTypeA
dnsCodeToType 2 = Just DNSTypeNS
dnsCodeToType 5 = Just DNSTypeCNAME
dnsCodeToType 10 = Just DNSTypeNULL
dnsCodeToType 12 = Just DNSTypePTR
dnsCodeToType 15 = Just DNSTypeMX
dnsCodeToType 16 = Just DNSTypeTXT
dnsCodeToType 28 = Just DNSTypeAAAA
dnsCodeToType _ = Nothing

--dnsCodeToType {ty = DNSTypeMD} 3 = Just DNSTypeRelMD
--dnsCodeToType {ty = DNSTypeMF} 4 = Just DNSTypeRelMF
--dnsCodeToType {ty = DNSTypeSOA} 6 = Just DNSTypeRelSOA
--dnsCodeToType {ty = DNSTypeMB} 7 = Just DNSTypeRelMB
--dnsCodeToType {ty = DNSTypeMG} 8 = Just DNSTypeRelMG
--dnsCodeToType {ty = DNSTypeMR} 9 = Just DNSTypeRelMR
--dnsCodeToType {ty = DNSTypeWKS} 11 = Just DNSTypeRelWKS
--dnsCodeToType {ty = DNSTypeHINFO} 13 = Just DNSTypeRelHINFO
--dnsCodeToType {ty = DNSTypeMINFO} 14 = Just DNSTypeRelMINFO

dnsCodeToQType : Bounded 16 -> Maybe DNSQType
dnsCodeToQType (BInt 1 oh) = Just DNSQTypeA
dnsCodeToQType (BInt 2 oh) = Just DNSQTypeNS
dnsCodeToQType (BInt 5 oh) = Just DNSQTypeCNAME
dnsCodeToQType (BInt 10 oh) = Just DNSQTypeNULL
dnsCodeToQType (BInt 12 oh) = Just DNSQTypePTR
dnsCodeToQType (BInt 15 oh) = Just DNSQTypeMX
dnsCodeToQType (BInt 16 oh) = Just DNSQTypeTXT
dnsCodeToQType (BInt 28 oh) = Just DNSQTypeAAAA
dnsCodeToQType (BInt 252 oh) = Just DNSQTypeAXFR
dnsCodeToQType (BInt 253 oh) = Just DNSQTypeMAILB
dnsCodeToQType (BInt 254 oh) = Just DNSQTypeMAILA
dnsCodeToQType (BInt 255 oh) = Just DNSQTypeALL
dnsCodeToQType _ = Nothing

dnsQTypeToCode : DNSQType -> Bounded 16
dnsQTypeToCode DNSQTypeA = (BInt 1 oh)
dnsQTypeToCode DNSQTypeNS = (BInt 2 oh)
dnsQTypeToCode DNSQTypeCNAME = (BInt 5 oh)
dnsQTypeToCode DNSQTypeNULL = (BInt 10 oh)
dnsQTypeToCode DNSQTypePTR = (BInt 12 oh)
dnsQTypeToCode DNSQTypeMX = (BInt 15 oh)
dnsQTypeToCode DNSQTypeTXT = (BInt 16 oh)
dnsQTypeToCode DNSQTypeAAAA = (BInt 28 oh)
dnsQTypeToCode DNSQTypeAXFR = (BInt 252 oh)
dnsQTypeToCode DNSQTypeMAILB = (BInt 253 oh)
dnsQTypeToCode DNSQTypeMAILA = (BInt 254 oh)
dnsQTypeToCode DNSQTypeALL = (BInt 255 oh)
dnsQTypeToCode DNSQTypeSOA = (BInt 6 oh)

data DNSResponse = DNSResponseNoError
                 | DNSResponseFormatError
                 | DNSResponseServerError
                 | DNSResponseNameError
                 | DNSResponseNotImplementedError
                 | DNSResponseRefusedError

instance Show DNSResponse where
  show DNSResponseNoError = "No error"
  show DNSResponseFormatError = "Format error"
  show DNSResponseServerError = "Server error"
  show DNSResponseNameError = "Name error"
  show DNSResponseNotImplementedError = "Not implemented error"
  show DNSResponseRefusedError = "Refused error"

dnsCodeToResponse : Bounded 4 -> Maybe DNSResponse
dnsCodeToResponse (BInt 0 oh) = Just DNSResponseNoError
dnsCodeToResponse (BInt 1 oh) = Just DNSResponseFormatError
dnsCodeToResponse (BInt 2 oh) = Just DNSResponseServerError
dnsCodeToResponse (BInt 3 oh) = Just DNSResponseNameError
dnsCodeToResponse (BInt 4 oh) = Just DNSResponseNotImplementedError
dnsCodeToResponse (BInt 5 oh) = Just DNSResponseRefusedError
dnsCodeToResponse _ = Nothing

dnsResponseToCode : DNSResponse -> Bounded 4
dnsResponseToCode DNSResponseNoError = BInt 0 oh
dnsResponseToCode DNSResponseFormatError = BInt 1 oh
dnsResponseToCode DNSResponseServerError = BInt 2 oh
dnsResponseToCode DNSResponseNameError = BInt 3 oh
dnsResponseToCode DNSResponseNotImplementedError = BInt 4 oh
dnsResponseToCode DNSResponseRefusedError = BInt 5 oh

DomainFragment : Type
DomainFragment = String

record DNSSoA : Type where
  MkSOA : (dnsSOAMName : List DomainFragment) ->
          (dnsSOARName : List DomainFragment) ->
          (dnsSOASerial : Int) ->
          (dnsSOARefresh : Int) ->
          (dnsSOARetry : Int) ->
          (dnsSOAExpire : Int) ->
          (dnsSOAMinimum : Int) ->
          DNSSoA

instance Show DNSSoA where
  show soa =
    "DNS Start of Authority: \n" ++
    "MName: " ++ (show $ dnsSOAMName soa) ++ "\n" ++
    "RName: " ++ (show $ dnsSOARName soa) ++ "\n" ++
    "Serial: " ++ (show $ dnsSOASerial soa) ++ "\n" ++
    "Refresh: " ++ (show $ dnsSOARefresh soa) ++ "\n" ++
    "Retry: " ++ (show $ dnsSOARetry soa) ++ "\n" ++
    "Expire: " ++ (show $ dnsSOAExpire soa) ++ "\n" ++
    "Minimum: " ++ (show $ dnsSOAMinimum soa) ++ "\n"

data DNSPayloadType = DNSIPv4 | DNSIPv6 | DNSDomain | DNSSOA

data DNSPayload : DNSPayloadType -> Type where
  DNSIPv4Payload : SocketAddress -> DNSPayload DNSIPv4
  DNSIPv6Payload : SocketAddress -> DNSPayload DNSIPv6
  DNSDomainPayload : List DomainFragment -> DNSPayload DNSDomain
  DNSSOAPayload : DNSSoA -> DNSPayload DNSSOA

data DNSPayloadRel : DNSType -> DNSClass -> DNSPayloadType -> Type where
  DNSPayloadRelIP : DNSPayloadRel DNSTypeA DNSClassIN DNSIPv4
  DNSPayloadRelIP6 : DNSPayloadRel DNSTypeAAAA DNSClassIN DNSIPv6
  DNSPayloadRelCNAME : DNSPayloadRel DNSTypeCNAME DNSClassIN DNSDomain
  DNSPayloadRelNS : DNSPayloadRel DNSTypeNS DNSClassIN DNSDomain
  DNSPayloadRelSOA : DNSPayloadRel DNSTypeSOA DNSClassIN DNSSOA

showPayload : (DNSPayloadRel rrt rrc pl_ty) -> DNSPayload pl_ty -> String
showPayload DNSPayloadRelIP (DNSIPv4Payload addr) = "IPv4: " ++ (show addr)
showPayload DNSPayloadRelIP6 (DNSIPv6Payload addr) = "IPv6 " ++ (show addr)
showPayload DNSPayloadRelCNAME (DNSDomainPayload dom) = "Domain: " ++ show dom
showPayload DNSPayloadRelNS (DNSDomainPayload dom) = "Domain: " ++ show dom
showPayload DNSPayloadRelSOA (DNSSOAPayload soa) = "SOA: " ++ show soa


text:
import Js.ASync

p : Int -> Int
p x = x + 1

call_fn : (Int -> Int) -> Int -> JS_IO Int
call_fn f x =
  jscall
    "%0(%1)"
    ((JsFn (Int -> Int)) -> Int -> JS_IO Int)
    (MkJsFn f)
    x

main : JS_IO ()
main = do
  v <- call_fn p 1
  putStrLn' $ show v

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
||| Switching Combinators
|||
||| Switches allow us to dynamically change the structure
||| (wiring) of a running network of stream functions.
||| Semantically, the react on discrete events, but
||| some of the switching primitives in this module use
||| the `Either` data type if it allows us to more exactly
||| describe the semantics of a switch.
module Data.MSF.Switch

import Data.MSF.Core
import Data.MSF.Event
import Data.MSF.Running
import Data.MSF.Util
import Data.SOP

%default total

--------------------------------------------------------------------------------
--          Immediate Switches
--------------------------------------------------------------------------------

||| Produces output of the first MSF until it produces
||| a `Left`, in which case the event will be used to
||| create a new MSF, which will be immediately evaluated
||| and used henceforth.
|||
||| This is a one-time switch, which is often used to
||| run an MSF a fixed number of times or until a certain
||| event occurs, after which the replacement will be used.
|||
||| Note: It is unsafe to use this in a recursive setting,
|||       as it would allow us to create an infinite loop
|||       of streaming functions, all of which return `Left`s
|||       forever. Luckily, the totality checker will prevent us
|||       from doing this.
export %inline
switchE : MSF m i (Either e o) -> (e -> MSF m i o) -> MSF m i o
switchE = Switch

||| Produces output of the given MSF until it fires an event,
||| in which case a new MSF is created,
||| which will be evaluated immediately and used henceforth.
|||
||| This uses `switchE` internally, so all restrictions mentioned
||| there apply.
export
switch :  MSF m i (NP I [o, Event e])
       -> (e -> MSF m i o)
       -> MSF m i o
switch sf = switchE $ sf >>^ (\[vo,ve] => event (Right vo) Left ve)

--------------------------------------------------------------------------------
--          Delayed Switches
--------------------------------------------------------------------------------

rswUtil : NP I [o,Event x] -> Either (x,o) o
rswUtil [vo,Ev vx] = Left (vx,vo)
rswUtil [vo,NoEv]  = Right vo

||| Produces output of the given MSF until it fires an event,
||| in which case a new MSF is created,
||| which will be used in all further evaluation steps.
export
dSwitch : MSF m i (NP I [o, Event e]) -> (e -> MSF m i o) -> MSF m i o
dSwitch sf = switch (sf >>> par [id, iPre NoEv])

--------------------------------------------------------------------------------
--          Recurring Switches
--------------------------------------------------------------------------------

export %inline
rSwitch : Monad m => MSF m i o -> MSF m (NP I [Event $ MSF m i o,i]) o
rSwitch sf =
  feedback sf . arrM $
    \[sf,[ev,vi]] => do
      (vo,sf2) <- step (fromEvent sf ev) vi
      pure [sf2,vo]

export %inline
drSwitch : Monad m => MSF m i o -> MSF m (NP I [Event $ MSF m i o,i]) o
drSwitch sf =
  feedback sf . arrM $
    \[sf,[ev,vi]] => do
      (vo,sf2) <- step sf vi
      pure [fromEvent sf2 ev,vo]

||| Produces output of the first MSF until the second
||| fires an event, in which case a new MSF is created,
||| which will be used in all futre evaluation cycles.
export
drswitchWhen :  Monad m
             => MSF m i o
             -> MSF m i (Event e)
             -> (e -> MSF m i o)
             -> MSF m i o
drswitchWhen ini es f = fan [es >>^ map f,id] >>> drSwitch ini


text:
module Erlang.System.Concurrency

import Erlang.Decode
import Erlang.IO
import Erlang.Types

%default total

%extern prim__erlReceive : (ms : Int) -> (1 x : %World) -> IORes (Maybe ErlTerm)

export
erlSelf : HasIO io => io ErlPid
erlSelf = pure $ erlUnsafeCall ErlPid "erlang" "self" []

export
erlSpawn : HasIO io => IO () -> io ErlPid
erlSpawn action = pure $ erlUnsafeCall ErlPid "erlang" "spawn" [MkIOFun0 (map MkRaw action)]

export
erlSpawnLink : HasIO io => IO () -> io ErlPid
erlSpawnLink action = pure $ erlUnsafeCall ErlPid "erlang" "spawn_link" [MkIOFun0 (map MkRaw action)]

-- TODO: Support more receivers than just `ErlPid`
export
erlSend : (HasIO io, ErlType a) => ErlPid -> a -> io ()
erlSend receiver value = do
  pure $ erlUnsafeCall ErlTerm "erlang" "send" [receiver, value]
  pure ()

-- TODO: Add proof that `ms` is in proper range: 0 - 16#FFFFFFFF (http://erlang.org/doc/reference_manual/expressions.html#receive)
export %inline
erlReceive : HasIO io => (ms : Int) -> a -> ErlDecoder a -> io a
erlReceive ms def decoder = do
  Just term <- primIO (prim__erlReceive ms)
    | Nothing => pure def
  pure (erlDecodeDef def decoder term)


text:
module Divisors

import ZZ
%access public export
%default total
|||isDivisible a b can be constucted if b divides a
isDivisible : ZZ -> ZZ -> Type
isDivisible a b = (n : ZZ ** a = b * n)

|||1 divides everything
oneDiv : (a : ZZ) -> isDivisible a 1
oneDiv a = (a ** rewrite sym (multOneLeftNeutralZ a) in Refl)

|||Genetes a proof of (a+b) = d*(n+m) from (a=d*n)and (b=d*m)
DistributeProof: (a:ZZ)->(b:ZZ)->(d:ZZ)->(n:ZZ)->(m:ZZ)->(a=d*n)->(b=d*m)->((a+b) = d*(n+m))
DistributeProof a b d n m pf1 pf2 = rewrite  (multDistributesOverPlusRightZ d n m) in(trans (the (a+b=(d*n)+b) (v1)) v2) where
  v1 =plusConstantRightZ a (d*n) b pf1
  v2 =plusConstantLeftZ b (d*m) (d*n) pf2

|||The theorem d|a =>d|ac
MultDiv:(isDivisible a d) ->(c:ZZ)->(isDivisible (a*c) d)
MultDiv {d} (n**Refl) c =((n*c)** (rewrite sym (multAssociativeZ d n c) in (Refl)))

|||The theorem d|a and d|b =>d|(a+b)
PlusDiv : (isDivisible a d)->(isDivisible b d)->(isDivisible (a+b) d)
PlusDiv {d}{a}{b} (n**prf1) (m**prf2) = ((n+m)**(DistributeProof a b d n m prf1 prf2))
|||The theorem b|a and c|b =>c|a
TransDivide : (isDivisible a b)->(isDivisible b c)->(isDivisible a c)
TransDivide {c} (x ** pf1) (y ** pf2) = (y*x ** (rewrite  multAssociativeZ c y x in  (rewrite pf1 in (rewrite pf2 in Refl))))

|||If d divides a and b it divides a linear combination of a and b
LinCombDiv:(m:ZZ)->(n:ZZ)->(isDivisible a d)->(isDivisible b d)->(isDivisible ((a*m)+(b*n)) d)
LinCombDiv m n dDiva dDivb = PlusDiv (MultDiv  dDiva m) (MultDiv  dDivb n)

EuclidConservesDivisor:(m:ZZ)->(isDivisible a d)->(isDivisible b d)->(isDivisible (a+(b*(-m))) d)
EuclidConservesDivisor m dDiva dDivb = PlusDiv dDiva (MultDiv dDivb (-m) )

|||Any integer divides zero
ZZDividesZero:(a:ZZ)->(isDivisible 0 a )
ZZDividesZero a = (0**(sym (multZeroRightZeroZ a)))
|||A type that is occupied iff c is a common factor of a and b
isCommonFactorZ : (a:ZZ) -> (b:ZZ) -> (c:ZZ) -> Type
isCommonFactorZ a b c = ((isDivisible a c),(isDivisible b c))
|||The GCD type that is occupied iff d = gcd (a,b). Here GCD is defined as that positive integer such that any common factor of a and b divides it
GCDZ : (a:ZZ) -> (b:ZZ) -> (d:ZZ) -> Type
GCDZ a b d = ((IsPositive d),(isCommonFactorZ a b d),({c:ZZ}->(isCommonFactorZ a b c)->(isDivisible d c)))
|||Anything divides itself
SelfDivide:(a:ZZ)->(isDivisible a a)
SelfDivide a = (1**sym (multOneRightNeutralZ a))

|||Generates the proof that if c is a common factor of a and 0 then c divides a
GCDCondition : (a:ZZ) -> ({c:ZZ}->(isCommonFactorZ a 0 c)->(isDivisible a c))
GCDCondition  a {c} (cDiva,cDiv0) = cDiva
|||Proves that the GCD of a and 0 is a
gcdOfZeroAndInteger:(a:ZZ)->IsPositive a ->GCDZ a 0 a
gcdOfZeroAndInteger a pf = (pf,((SelfDivide a),(ZZDividesZero a)),((GCDCondition a)))
|||The theorem, d|a =>d|(-a)
dDividesNegative:(isDivisible a d)->(isDivisible  (-a) d)
dDividesNegative{a}{d} (x ** pf) = ((-x)**(multNegateRightIsNegateZ a d x pf))
|||The theorem c|b and c|(a+bp) then c|a
cDiva :{p:ZZ} ->(cDIvb :(isDivisible b c))->(cDIvExp:isDivisible (a+(b*p)) c)->(isDivisible a c)
cDiva {p}{b}{a}{c} cDivb cDivExp = rewrite (sym (addAndSubNeutralZ a (b*p))) in (PlusDiv cDivExp (dDividesNegative(MultDiv cDivb (p))))
|||A helper function for euclidConservesGcd function
genFunctionForGcd :(f:({c:ZZ}->(isCommonFactorZ a b c)->(isDivisible d c)))->(({c:ZZ}->(isCommonFactorZ b (a+(b*(-m)))  c)->(isDivisible d c)))
genFunctionForGcd f (cDivb,cDivExp) = f((cDiva cDivb cDivExp,cDivb))

|||The theorem, gcd(a,b)=d => gcd (b, a+ b(-m))=d
euclidConservesGcd :(m:ZZ)->(GCDZ a b d)->(GCDZ b  (a+(b*(-m))) d)
euclidConservesGcd m  (posProof, (dDiva,dDivb), f) = (posProof,(dDivb,(EuclidConservesDivisor m  dDiva dDivb)),genFunctionForGcd f)
|||The theorem that if c and d are positive d|c => (d is less than or equal to c)
posDivPosImpliesLte:(isDivisible c d)->(IsPositive c)->(IsPositive d)->LTEZ d c
posDivPosImpliesLte {d}{c}(x ** pf) cPos dPos = posLteMultPosPosEqZ {q=x} d c dPos cPos pf

|||The Theorem that if c and d are positive, d|c and c|d =>(c=d)
PosDivAndDivByImpliesEqual: (isDivisible c d)->(isDivisible d c)->(IsPositive c)->(IsPositive d) -> (c=d)
PosDivAndDivByImpliesEqual x y z x1 =lteAndGteImpliesEqualZ dLtec cLted where
  dLtec =posDivPosImpliesLte x z x1
  cLted =posDivPosImpliesLte y x1 z


text:
module Data.Group

import Data.Stream

||| This extends 'Monoid' by defining an inverse for every element.
public export
interface (Monoid t) => Group t where
  inverse : t -> t

||| Stream of elements starting at some given element.
public export
generate : (Monoid g) => g -> Stream g
generate g1 = neutral :: map (<+> g1) (generate g1)

||| (Positive) integer exponentiation.
public export
exp : (Monoid g) => (n : Nat) -> g -> g
exp n g = Prelude.head (drop n (generate g))

||| Whether a group element is idempotent
public export
total
idempotent : (Eq g, Semigroup g) => g -> Bool
idempotent x = x == (x <+> x)

||| Commutator of two elements.
public export
total
commutator : (Group g) => g -> g -> g
commutator a b = inverse a <+> inverse b <+> a <+> b

max_stars_repo_name: vmchale/permutations

max_issues_repo_name: vmchale/permutation

max_forks_repo_name: vmchale/permutation


text:
-- Exercise_5_2.idr

-- Implement a guessing game fro numbers

module Main

import System
import ReadNum

||| Guessing game: Interactive dialogs to guess a given number.
||| @target the number to be guessed
||| @guesses the number of trials
guess : (target : Nat) -> (guesses : Nat) -> IO ()
guess target guesses =
  do putStr ("Guess my number " ++ "(" ++ (show guesses) ++ " trial): ")
     Just trial <- readNumber | Nothing => (putStrLn "Invalid input! Try again.." >>= \_ =>
                                          guess target guesses)
     case compare trial target of
          EQ => putStrLn "Correct!"
          LT => putStrLn "Too small, try again.." >>= \_ => guess target (S guesses)
          GT => putStrLn "Too large, try again.." >>= \_ => guess target (S guesses)

||| Mimic replWith function from Prelude module
myReplWith : (state : a) -> (prompt : String) -> (onInput : a -> String -> Maybe (String, a)) -> IO ()
myReplWith state prompt onInput = do
  putStr prompt
  input <- getLine
  let Just (output, newState) = onInput state input | Nothing => pure ()
  putStr output
  myReplWith newState prompt onInput

||| Mimic repl function from Prelude module
myRepl : (prompt : String) -> (onInput : String -> String) -> IO ()
myRepl prompt onInput = myReplWith () prompt (\(), input => Just (onInput input, ()))

main : IO ()
main = do
  tsecs <- time
  let target = tsecs `mod` 100
  guess (cast target) 1

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
%default partial

foo : (Nat, Nat) -> Nat
foo (Z, Z) = Z

bar : {a : _} -> a -> Nat
bar Z = Z
bar (S _) = S Z

cty : (a : Type) -> a -> Nat
cty Nat Z = Z
cty Nat (S _) = S Z
cty _ x = S (S Z)

badBar : a -> Nat
badBar Z = Z
badBar (S _) = S Z


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 13, section 1

-- check that all functions are total
%default total

namespace exercise1

  data DoorState = DoorClosed | DoorOpen

  data DoorCmd : Type ->
                 DoorState ->
                 DoorState ->
                 Type where
    Open :     DoorCmd ()       DoorClosed DoorOpen
    Close :    DoorCmd ()       DoorOpen   DoorClosed
    RingBell : DoorCmd ()       state      state
    Pure :     ty -> DoorCmd ty state      state
    (>>=) :    DoorCmd a        state1     state2 ->
               (a -> DoorCmd b  state2     state3) ->
               DoorCmd b        state1     state3

  doorProg : DoorCmd () DoorClosed DoorClosed
  doorProg = do RingBell
                Open
                RingBell
                Close

namespace exercise2

  data GuessCmd : Type -> Nat -> Nat -> Type where
    Try : Integer -> GuessCmd Ordering (S k) (k)
    Pure : ty -> GuessCmd ty state state
    (>>=) : GuessCmd a state1 state2 ->
            (a -> GuessCmd b state2 state3) ->
            GuessCmd b state1 state3

  threeGuesses : GuessCmd () 3 0
  threeGuesses = do Try 10
                    Try 20
                    Try 15
                    Pure ()

  -- noGuesses : GuessCmd () 0 0
  -- noGuesses = do Try 10
  --                Pure ()

namespace exercise3

  data Matter = Solid | Liquid | Gas

  data MatterCmd : Type -> Matter -> Matter -> Type where
    Melt :     MatterCmd () Solid Liquid
    Boil :     MatterCmd () Liquid Gas
    Condense : MatterCmd () Gas Liquid
    Freeze :   MatterCmd () Liquid Solid
    Pure : ty -> MatterCmd ty state state
    (>>=) : MatterCmd a state1 state2 ->
            (a -> MatterCmd b state2 state3) ->
            MatterCmd b state1 state3

  iceSteam : MatterCmd () Solid Gas
  iceSteam = do Melt
                Boil

  steamIce : MatterCmd () Gas Solid
  steamIce = do Condense
                Freeze

  -- overMelt : MatterCmd () Solid Gas
  -- overMelt = do Melt
  --               Melt

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
namespace L0
  public export
  data List0 : Type

namespace L1
  public export
  data List1 : Type where
    Nil : List1
    Cons1 : Nat -> List0 -> List1

  public export
  (::) : Nat -> List0 -> List1
  (::) = Cons1

namespace L2
  public export
  data (::) : Nat -> List0 -> Type where

namespace L0
  public export
  data List0 : Type where
    Nil : List0
    (::) : Nat ->Type -> List0

m : Nat
m = believe_me %MkWorld

Rainbow : Nat -> Type
Rainbow n =  [ n , m , n ]


text:
module Flexidisc.OrdList.Sub

import Flexidisc.Dec.IsYes
import Flexidisc.OrdList.Fresh
import Flexidisc.OrdList.Label
import Flexidisc.OrdList.Nub
import Flexidisc.OrdList.Row
import Flexidisc.OrdList.Type

%default total
%access public export

||| Proof that an `OrdList` is a sublist of another vect
public export
data Sub : (xs, ys : OrdList k v o) -> Type where
  ||| The empty `Ordlist` is a sublist of the empty `OrdList`
  Empty : Sub [] []
  ||| Making the second list larger don't change the property
  Skip  : Sub xs ys -> Sub xs (y::ys)
  ||| To add an element to the first list, we need to add it to the second one
  Keep  : Sub xs ys -> Sub (x::xs) (x::ys)

%name Sub sub, issub, ss

||| An empty `OrdList` is an ordered subset of any `Any`
subEmpty' : (xs : OrdList k v o) -> Sub [] xs
subEmpty' [] = Empty
subEmpty' (_ :: xs) = Skip (subEmpty' xs)

||| An empty `OrdList` is an ordered subset of any `OrdList`
subEmpty : Sub [] xs
subEmpty {xs} = subEmpty' xs

implementation Uninhabited (Sub (x::xs) []) where
  uninhabited Empty impossible
  uninhabited (Skip _) impossible
  uninhabited (Keep _) impossible

||| A `OrdList` is an ordered subset of itself
subRefl' : (xs : OrdList k v o) -> Sub xs xs
subRefl' [] = Empty
subRefl' (x :: xs) = Keep (subRefl' xs)

||| A `OrdList` is an ordered subset of itself
subRefl : Sub xs xs
subRefl {xs} = subRefl' xs

freshInSub : Sub xs ys -> Fresh l ys -> Fresh l xs
freshInSub Empty fresh = fresh
freshInSub (Skip sub) (f :: fresh) = freshInSub sub fresh
freshInSub (Keep sub) (f :: fresh) = f :: freshInSub sub fresh

||| If the original vector doesn't contain any duplicate,
||| an orderred subset doesn't contain duplicate as well
isNubFromSub : Sub xs ys -> Nub ys -> Nub xs
isNubFromSub Empty y = y
isNubFromSub (Skip sub) (yes :: prf) = isNubFromSub sub prf
isNubFromSub (Keep sub) (yes :: prf) =
  freshInSub sub yes :: isNubFromSub sub prf

%hint
rowFromSub : Sub xs ys -> OrdRow key ty xs -> OrdRow key ty ys
rowFromSub Empty lbl = lbl
rowFromSub (Skip sub) loc = There (rowFromSub sub loc)
rowFromSub (Keep sub) Here = Here
rowFromSub (Keep sub) (There later) = There (rowFromSub sub later)

||| Given the proof that a Label is in an subset of a vect
||| provide a proof that this label is in the initial vect
%hint
labelFromSub : Sub xs ys -> OrdLabel x xs -> OrdLabel x ys
labelFromSub Empty y = y
labelFromSub (Skip z) loc = There (labelFromSub z loc)
labelFromSub (Keep _) Here = Here
labelFromSub (Keep sub) (There later) = There (labelFromSub sub later)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
main : IO ()
main = putStrLn "Hello, World!"

max_stars_repo_name: heyLu/qst

max_issues_repo_name: heyLu/qst

max_forks_repo_name: heyLu/qst


text:
ex : {n : Nat} -> String
ex {n} = "hello" ++ show n

main : IO ()
main = putStrLn ex


text:
module A.B

import A.B


text:
module LightClick.DSL.Convert

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

import Toolkit.Data.Location

import LightClick.Types
import LightClick.Terms
import LightClick.Error

import LightClick.DSL.AST

%default covering

public export
MetaTyCheck : Type -> Type
MetaTyCheck = Either LightClick.Error

convert : (ctxt : Context)
       -> (expr : AST)
       -> MetaTyCheck (type ** Term ctxt type)

expectPort : (ctxt : Context)
          -> (term : AST)
          -> MetaTyCheck (n ** Term ctxt (PORT n))
expectPort ctxt expr with (convert ctxt expr)
  expectPort ctxt expr | (Left l) = Left l
  expectPort ctxt expr | (Right (PORT n ** term)) = Right (n ** term)
  expectPort ctxt expr | (Right (type ** term)) = do
    loc <- getFC term
    Left (MetaTypeMismatch loc (PORT "") type)

checkType : (ctxt : Context)
         -> (type : MTy)
         -> AST
         -> MetaTyCheck (Term ctxt type)
checkType ctxt typeE ast with (convert ctxt ast)
  checkType ctxt typeE ast | (Left l) = Left l
  checkType ctxt typeE ast | (Right (typeG ** term)) with (decEq typeG typeE)
    checkType ctxt typeE ast | (Right (typeE ** term)) | (Yes Refl) = Right term
    checkType ctxt typeE ast | (Right (typeG ** term)) | (No contra) = do
        l <- getFC term
        Left (MetaTypeMismatch l typeE typeG)

doKVConvert : (ctxt : Context)
           -> (type : MTy)
           -> Pair String AST
           -> MetaTyCheck (Pair String (Term ctxt type))
doKVConvert ctxt type (k,v) = do
    v' <- checkType ctxt type v
    Right (k,v')

convertListPort : (ctxt : Context)
               -> (ps : Vect n AST)
               -> MetaTyCheck (ss : Vect n String
                                 **
                                DVect String
                                      (\s => Term ctxt (PORT s))
                                      n
                                      ss)

convertListPort ctxt [] = Right (_ ** Nil)
convertListPort ctxt (x :: xs) with (convert ctxt x)
  convertListPort ctxt (x :: xs) | (Left l) = Left l
  convertListPort ctxt (x :: xs) | (Right (PORT s ** term)) with (convertListPort ctxt xs)
    convertListPort ctxt (x :: xs) | (Right (PORT s ** term)) | (Left l) = Left l
    convertListPort ctxt (x :: xs) | (Right (PORT s ** term)) | (Right (ss ** ports)) = Right (s::ss ** term::ports)

  convertListPort ctxt (x :: xs) | (Right (type ** term)) = do
      loc <- getFC term
      Left (MetaTypeConstructionError loc (PORT "") type)

convertListPortM : (ctxt : Context)
                -> (ps : Vect (S n) AST)
                -> MetaTyCheck (ss : Vect (S n) String
                                 **
                                 DVect String
                                       (\s => Term ctxt (PORT s)) (S n)
                                       ss)
convertListPortM = convertListPort

convertListPortF : (ctxt : Context)
                -> (ps : Vect (S (S n)) AST)
                -> MetaTyCheck (ss : Vect (S (S n)) String
                                 **
                                 DVect String
                                       (\s => Term ctxt (PORT s)) (S (S n))
                                       ss)
convertListPortF = convertListPort

genIndex : (fc : FileContext)
        -> (ctxt : Context)
        -> (label : String)
        -> MetaTyCheck (type ** Index ctxt (label,type))
genIndex fc [] label =
  Left (IdentifierNotFound fc label)
genIndex fc ((x,t) :: xs) label with (decEq label x)
  genIndex fc ((x,t) :: xs) x | (Yes Refl) = Right (t ** Here)
  genIndex fc ((x,t) :: xs) label | (No contra) with (genIndex fc xs label)
    genIndex fc ((x,t) :: xs) label | (No contra) | (Left l) = Left l
    genIndex fc ((x,t) :: xs) label | (No contra) | (Right (type ** prf)) = Right (type ** There prf)

convert ctxt (Ref fc x) with (genIndex fc ctxt x)
  convert ctxt (Ref fc x) | (Left l) = Left l
  convert ctxt (Ref fc x) | (Right (type ** idx)) =
      Right (type ** Ref fc idx)

convert ctxt (Bind fc name expr body) with (genIndex fc ctxt name)
  convert ctxt (Bind fc name expr body) | (Left l) = do
    expr' <- convert ctxt expr
    body' <- convert ((name, fst expr')::ctxt) body
    Right (fst body' ** Let fc name (snd expr') (snd body'))
  convert ctxt (Bind fc name expr body) | (Right r) =
    Left (IdentifierAlreadyExists fc name)

convert ctxt (Seq exprA exprB) = do
   exprA' <- convert ctxt exprA
   exprB' <- convert ctxt exprB
   Right (fst exprB' ** Seq (snd exprA') (snd exprB'))

convert ctxt (DataLogic fc)      = Right (DATA ** DataLogic fc)

convert ctxt (DataArray fc ty l) = do
  term <- checkType ctxt DATA ty
  Right (DATA ** DataArray fc term l)

convert ctxt (DataStruct fc kvs) = do
    kvs' <- traverse (doKVConvert ctxt DATA) kvs
    Right (DATA ** DataStruct fc kvs')

convert ctxt (DataUnion fc kvs) = do
    kvs' <- traverse (doKVConvert ctxt DATA) kvs
    Right (DATA ** DataUnion fc kvs')

convert ctxt (Port fc l d s w t) = do
  dataType <- checkType ctxt DATA t
  Right (PORT l ** Port fc l d s w dataType)

convert ctxt (ModuleDef fc ps) = do
  ps' <- convertListPortM ctxt ps
  Right (MODULE (fst ps') ** Module fc $ snd ps')

convert ctxt (Index fc x b) with (convert ctxt x)
  convert ctxt (Index fc x b) | (Left l) = Left l
  convert ctxt (Index fc x b) | (Right (MODULE ns ** term)) with (isElem b ns)
    convert ctxt (Index fc x b) | (Right (MODULE ns ** term)) | (Yes prf) = Right (_ ** Index fc term prf)
    convert ctxt (Index fc x b) | (Right (MODULE ns ** term)) | (No contra) = do
      Left (InvalidModuleIndex fc b ns)

  convert ctxt (Index fc x b) | (Right (type ** term)) =
     Left (MetaTypeConstructionError fc (MODULE [""]) type)

convert ctxt (Connect fc x y) = do
  x' <- expectPort ctxt x
  y' <- expectPort ctxt y
  Right (CONN ** Connect fc (snd x') (snd y'))

convert ctxt (FanOut fc w ws) = do
   w'  <- expectPort ctxt w
   ws' <- convertListPortF ctxt ws
   Right (CONN ** FanOut fc (snd w') (snd ws'))

convert ctxt (Mux fc fan ctrl out) = do
  fan' <- convertListPortF ctxt fan
  ctrl' <- expectPort ctxt ctrl
  out'  <- expectPort ctxt out
  Right (CONN ** Mux fc (snd fan') (snd ctrl') (snd out'))

convert ctxt (NOT fc i o)
  = do x' <- expectPort ctxt i
       y' <- expectPort ctxt o
       Right (GATE ** NOT fc (snd x') (snd y'))

convert ctxt (GATE fc ty is o)
  = do is' <- convertListPortF ctxt is
       o'  <- expectPort ctxt o
       Right (GATE ** GATE fc ty (snd is') (snd o'))

convert ctxt End = Right (UNIT ** End)

export
runConvert : AST -> MetaTyCheck (Term Nil UNIT)
runConvert ast with (convert Nil ast)
  runConvert ast | (Left l) = Left l
  runConvert ast | (Right (UNIT ** term)) = Right term
  runConvert ast | (Right (type ** term)) = Left (NotSupposedToHappen $ Just "runConvert")

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Tools.NatUtils

%access public export

-- Proof of the type that an implication implies its contrapositive
impliesContrapositive : (A : Type) -> (B : Type) -> (A -> B) -> (B -> Void) -> (A -> Void)
impliesContrapositive typeA typeB proofAimpliesB proofBfalse a = proofBfalse (proofAimpliesB a)

-- Proof that S m = S n implies m = n
meqnSmeqSn : (m : Nat) -> (n : Nat) -> (S m = S n) -> (m = n)
meqnSmeqSn Z Z Refl = Refl
meqnSmeqSn (S k) (S k) Refl = Refl

-- Proof that m = n implies f(m) = f(n), taken from Lecture.intro (apNat)
functionExtendEquality : (f : Nat -> Nat) -> (n : Nat) -> (m : Nat) -> (n = m) -> (f n = f m)
functionExtendEquality f m m Refl = Refl

-- Proof that m != n implies S m != S n
proofSmneqSn : (m : Nat) -> (n : Nat) -> ((m = n) -> Void) -> ((S m = S n) -> Void)
proofSmneqSn m n proofmneqn = impliesContrapositive (S m = S n) (m = n) (meqnSmeqSn m n) proofmneqn

-- Proof that m<n implies S m = n or S m < n
proofLTimplieseqorLT : (m : Nat) -> (n : Nat) -> (LT m n) -> Either (S m = n) (LT (S m) n)
proofLTimplieseqorLT Z (S Z) (LTESucc LTEZero) = Left Refl
proofLTimplieseqorLT Z (S (S n)) (LTESucc LTEZero) = Right (LTESucc (LTESucc LTEZero))
proofLTimplieseqorLT (S m) (S n) proofSmLTSn = case (proofLTimplieseqorLT m n (fromLteSucc proofSmLTSn)) of
										(Left proofSmeqn) => Left (functionExtendEquality S (S m) n proofSmeqn)
										(Right proofSmLTn) => Right (LTESucc proofSmLTn)

|||The theorem that (m<=n) and (n<=m) implies n=m
lteAndGteImpliesEqual:{m:Nat}-> {n:Nat}->(LTE m n)-> (LTE n m)->(n=m)
lteAndGteImpliesEqual LTEZero LTEZero = Refl
lteAndGteImpliesEqual (LTESucc x) (LTESucc y) = cong (lteAndGteImpliesEqual x y)
|||The theorem (m<=n) implies (m<=(c+n))
plusConstantLeftSide:{m:Nat}->{n:Nat}->(c:Nat)->LTE m n ->LTE m (c+n)
plusConstantLeftSide Z x = x
plusConstantLeftSide (S k) x = lteSuccRight (plusConstantLeftSide k x)

plusConstantLeftPreservesLte:{m:Nat}-> {n:Nat}->(c:Nat)->(LTE m n)->(LTE (c+m) (c+n))
plusConstantLeftPreservesLte Z x = x
plusConstantLeftPreservesLte (S k) x = LTESucc (plusConstantLeftPreservesLte k x)

plusConstantRightPreservesLte:{m:Nat}-> {n:Nat}->(c:Nat)->(LTE m n)->(LTE (m+c) (n+c))
plusConstantRightPreservesLte {m}{n}c x = rewrite (plusCommutative m c)  in (rewrite (plusCommutative n c) in (plusConstantLeftPreservesLte c x))

|||The theorem that for any natural numbers k and m (m<= (S k)*m)
natLteMultNatNat: (k:Nat)->(m:Nat)->(LTE m ((S k)*m))
natLteMultNatNat Z m = rewrite (multOneLeftNeutral m) in (lteRefl)
natLteMultNatNat (S k) m =     plusConstantLeftSide m (natLteMultNatNat  k m)


text:
> module EscardoOliva.TestSelectionFunction

> import EscardoOliva.SelectionFunction

> %default total
> %access public export
> %auto_implicits off

> xs : List Int
> xs = [0,3,2,-1,0,9,-7]

> min : Int
> min = arginf xs id

> max : Int
> max = argsup xs id

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Test.Sexp

import Test.Assertions
import Idrlisp.Sexp

%default covering

sexpAndSSynTestcases : List (Sexp (), SSyn ())
sexpAndSSynTestcases =
  [ (Num 123, Num 123)
  , (Sym "foo", Sym "foo")
  , (Str "hello", Str "hello")
  , (Bool True, Bool True)
  , (Bool True :: Bool False, [Bool True] :.: Bool False)
  , (Bool True :: Bool False :: Num 0 :: Num 1, [Bool True, Bool False, Num 0] :.: Num 1)
  , ([Sym "id"], App [Sym "id"])
  , ([Sym "f", Sym "a", Sym "b"], App [Sym "f", Sym "a", Sym "b"])
  , ([Sym "quote", Sym "foo"], Quote (Sym "foo"))
  , (
      [Sym "quasiquote", [
        Sym "bar",
        [Sym "unquote", Sym "baz"],
        [Sym "unquote-splicing", [Sym "hoge", Sym "fuga"]]
      ]],
      Quasiquote (App [
        Sym "bar",
        Unquote (Sym "baz"),
        UnquoteSplicing (App [Sym "hoge", Sym "fuga"])
      ])
    )
  , (Nil, Nil)
  , (Pure (), Pure ())
  ]

sexpAndSListTestcases : List (Sexp (), SList ())
sexpAndSListTestcases =
  [ (Num 123, Improper (Num 123))
  , ([], Proper [])
  , ([Num 1, Num 2], Proper [Num 1, Num 2])
  , (Num 1 :: Num 2 :: Num 3, Improper (Num 1 :: Num 2 :: Num 3))
  ]

showTestCases : List (String, SSyn ())
showTestCases =
  [ ("123", Num 123)
  , ("3.14", Num 3.14)
  , ("foo", Sym "foo")
  , ("unquote-splicing", Sym "unquote-splicing")
  , ("\"Text\"", Str "Text")
  , ("\"Hello, World!\\n\"", Str "Hello, World!\n")
  , ("#t", Bool True)
  , ("()", Nil)
  , ("'foo", Quote (Sym "foo"))
  , ("`(bar ,baz ,@(hoge fuga))", Quasiquote (App [Sym "bar", Unquote (Sym "baz"), UnquoteSplicing (App [Sym "hoge", Sym "fuga"])]))
  , ("(f)", App [Sym "f"])
  , ("(f a b)", App [Sym "f", Sym "a", Sym "b"])
  , ("(#t . #f)", [Bool True] :.: Bool False)
  , ("(#t #f 0 . 1)", [Bool True, Bool False, Num 0] :.: Num 1)
  , ("()", Pure ())
  ]

export
test : IO ()
test = describe "Idrlisp.Sexp" $ do
  describe "cast" $ do
    for_ sexpAndSSynTestcases (`shouldSatisfy` castIdentical)
    for_ sexpAndSListTestcases (`shouldSatisfy` castIdentical)
  describe "show" $ do
    for_ showTestCases (\t => snd t `shouldShow` fst t)

  let testSexp : Sexp Integer = [Pure 1, Pure 2 :: Pure 3]

  describe "map" $
    map succ testSexp
      `shouldBe` [Pure 2, Pure 3 :: Pure 4]
  describe "foldr" $
    foldr (::) Nil testSexp
      `shouldBe` [1, 2, 3]
  describe "traverse" $
    traverse (const (the (List Int) [0])) testSexp
      `shouldBe` [[Pure 0, Pure 0 :: Pure 0]]

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
Gnu : Type
Gnu = Int

Foo : Type
Foo = Bool

A : Foo
A = True

mkFoo : Gnu -> Foo
mkFoo gnu = A

gnat : {auto startHere : (a : Foo ** a = A)} -> Unit
gnat = ()

pathology : (gnu : Gnu) -> Unit
pathology gnu =
  let %hint foo : Foo
      foo = mkFoo gnu
      %hint bar : Foo -> (ford : arg = A)
                      -> (a : Foo ** a = A)
      bar _ Refl = (A ** Refl)
  in gnat


text:
module Data.SOP.NP

import Data.List.Elem
import Data.SOP.Utils
import Data.SOP.Interfaces

import Decidable.Equality

%default total

||| An n-ary product.
|||
||| The product is parameterized by a type constructor f and indexed by a
||| type-level list ks. The length of the list determines the number of
||| elements in the product, and if the i-th element of the list is of type k,
||| then the i-th element of the product is of type f k.
|||
||| Two common instantiations of f are the identity functor I and the constant
||| functor K. For I, the product becomes a heterogeneous list, where the
||| type-level list describes the types of its components.  For K a, the product
||| becomes a homogeneous list, where the contents of the type-level list are
||| ignored, but its length still specifies the number of elements.
|||
||| In the context of the SOP approach to generic programming, an n-ary product
||| describes the structure of the arguments of a single data constructor.
|||
||| Note: `NP_` takes an additional type parameter `k` to simulate
|||       Haskell's kind polymorphism. In theory, this could be left
|||       as an implicit argument. However, type-inference when calling
|||       interface functions like `hpure` was rather poor with `k`
|||       being implicit.
|||
|||       We therefore made `k` explicit and added a type alias `NP`
|||       to be used in those occasions when `k` can be inferred.
|||
||| Examples:
|||
||| ```idris example
||| ex1 : NP I [Char,Bool]
||| ex1 = ['c',False]
|||
||| ex2 : NP (K String) [Char,Bool,Int]
||| ex2 = ["Hello","World","!"]
|||
||| ex3 : NP Maybe [Char,Bool,Int]
||| ex3 = [Just 'x', Nothing, Just 1]
||| ```
public export
data NP_ : (k : Type) -> (f : k -> Type) -> (ks : List k) -> Type where
  Nil  : NP_ k f []
  (::) : (v : f t) -> (vs : NP_ k f ks) -> NP_ k f (t :: ks)

||| Type alias for `NP_` with type parameter `k` being
||| implicit. This reflects the kind-polymorphic data type
||| in Haskell.
public export
NP : {k : Type} -> (f : k -> Type) -> (ks : List k) -> Type
NP = NP_ k

||| Changes an n-ary product to the identity context `I`
||| by adjusting the types of stored values accordingly.
public export
toI : NP_ k f ks -> NP I (map f ks)
toI []       = []
toI (h :: t) = h :: toI t

--------------------------------------------------------------------------------
--          Specialized Interface Functions
--------------------------------------------------------------------------------

||| Specialiced version of `hmap`
public export
mapNP : (fun : forall a . f a -> g a) -> NP f ks -> NP g ks
mapNP fun []        = []
mapNP fun (v :: vs) = fun v :: mapNP fun vs

||| Specialization of `hpure`.
public export
pureNP : {ks : _} -> (forall a . f a) -> NP f ks
pureNP {ks = []}     _ = []
pureNP {ks = _ :: _} f = f :: pureNP f

||| Specialization of `hap`.
public export
hapNP : NP (\a => f a -> g a) ks -> NP f ks -> NP g ks
hapNP []        []        = []
hapNP (f :: fs) (v :: vs) = f v :: hapNP fs vs

||| Specialization of `hfoldl`
public export
foldlNP : (fun : acc -> el -> acc) -> acc -> NP (K el) ks -> acc
foldlNP _   acc []        = acc
foldlNP fun acc (v :: vs) = foldlNP fun (fun acc v) vs

||| Specialization of `hfoldr`
public export
foldrNP : (fun : el -> Lazy acc -> acc) -> Lazy acc -> NP (K el) ks -> acc
foldrNP _   acc []        = acc
foldrNP fun acc (v :: vs) = fun v (foldrNP fun acc vs)

||| Specialization of `hsequence`
public export
sequenceNP : Applicative g => NP (\a => g (f a)) ks -> g (NP f ks)
sequenceNP []        = pure []
sequenceNP (v :: vs) = [| v :: sequenceNP vs |]

||| Specialization of `hcollapse`
public export
collapseNP : NP (K a) ks -> List a
collapseNP []        = []
collapseNP (v :: vs) = v :: collapseNP vs

--------------------------------------------------------------------------------
--          Core Functions
--------------------------------------------------------------------------------

||| Returns the head of a non-empty n-ary product
public export
hd : NP f (k :: ks) -> f k
hd (v :: _) = v

||| Returns the tail of a non-empty n-ary product
public export
tl : NP f (k :: ks) -> NP f ks
tl (_ :: vs) = vs

||| Tries to creates a homogeneous n-ary product of the given
||| shape from a list of values.
public export
fromListNP : NP f ks -> List a -> Maybe (NP (K a) ks)
fromListNP []       []        = Just []
fromListNP []       (_ :: _)  = Nothing
fromListNP (_ :: _) []        = Nothing
fromListNP (_ :: t) (x :: xs) = (x ::) <$> fromListNP t xs

||| Like `fromListNP` but takes the shape from the implicit
||| list of types.
public export
fromList : {ks : _} -> List a -> Maybe (NP (K a) ks)
fromList = fromListNP (pureNP ())

||| Creates a homogeneous n-ary product of the given
||| shape by repeatedly applying a function to a seed value.
public export
unfoldNP : NP f ks -> (s -> (s,a)) -> s -> NP (K a) ks
unfoldNP []       _ _ = []
unfoldNP (_ :: t) g s = let (s2,v) = g s
                         in v :: unfoldNP t g s2

||| Like `unfoldNP` but takes the shape from the implicit
||| list of types.
public export
unfold : {ks : _} -> (s -> (s,a)) -> s -> NP (K a) ks
unfold = unfoldNP (pureNP ())

||| Creates a homogeneous n-ary product of the given
||| shape using an initial value and a function for
||| generating the next value.
public export
iterateNP : NP f ks -> (a -> a) -> a -> NP (K a) ks
iterateNP np f = unfoldNP np (\v => (f v, v))

||| Like `iterate` but takes the shape from the implicit
||| list of types.
public export
iterate : {ks : _} -> (a -> a) -> a -> NP (K a) ks
iterate = iterateNP (pureNP ())

||| A projection of an n-ary product p extracts the
||| value of p at a certain position.
public export
0 Projection : (f : k -> Type) -> (ks : List k) -> (v : k) -> Type
Projection f ks v = NP f ks -> f v

||| The set of projections of an n-ary product `NP f ks` can
||| itself be wrapped in an n-ary product of the same shape.
public export
projections : {ks : _} -> NP (Projection f ks) ks
projections {ks = []}       = []
projections {ks = (_ :: _)} = hd :: mapNP (. tl) projections

--------------------------------------------------------------------------------
--          Accessing Values
--------------------------------------------------------------------------------

||| Access the first element of the given type in
||| an n-ary product
public export
get : (0 t : k) -> {auto prf : Elem t ks} -> NP_ k f ks -> f t
get t {prf = Here}    (v :: _) = v
get t {prf = There _} (_ :: vs) = get t vs

--------------------------------------------------------------------------------
--          Modifying Values
--------------------------------------------------------------------------------

||| Modify a single element of the given type
||| in an n-ary product, thereby possibly changing the
||| types of stored values.
public export
modify :  (fun : f t -> f t')
       -> {auto prf : UpdateOnce t t' ks ks'}
       -> NP_ k f ks
       -> NP_ k f ks'
modify fun {prf = UpdateHere}    (v :: vs) = fun v :: vs
modify fun {prf = UpdateThere _} (v :: vs) = v :: modify fun vs

||| Modify a single element of the given type
||| in an n-ary product by applying an effectful
||| function.
|||
||| This is the effectful version of `modify`.
public export
modifyF :  Functor g
        => (fun : f t -> g (f t'))
        -> {auto prf : UpdateOnce t t' ks ks'}
        -> NP_ k f ks
        -> g (NP_ k f ks')
modifyF fun {prf = UpdateHere}    (v :: vs) = (:: vs) <$> fun v
modifyF fun {prf = UpdateThere _} (v :: vs) = (v ::)  <$> modifyF fun vs

||| Modify several elements of the given type
||| in an n-ary product, thereby possibly changing the
||| types of stored values.
public export
modifyMany :  (fun : f t -> f t')
           -> {auto prf : UpdateMany t t' ks ks'}
           -> NP_ k f ks
           -> NP_ k f ks'
modifyMany f {prf = UMNil}        []      = []
modifyMany f {prf = UMConsSame x} (v::vs) = f v :: modifyMany f vs
modifyMany f {prf = UMConsDiff x} (v::vs) = v   :: modifyMany f vs

||| Modify several elements of the given type
||| in an n-ary product by applying an effectful function.
|||
||| This is the effectful version of `modifyMany`.
public export
modifyManyF :  Applicative g
            => (fun : f t -> g (f t'))
            -> {auto prf : UpdateMany t t' ks ks'}
            -> NP_ k f ks
            -> g (NP_ k f ks')
modifyManyF f {prf = UMNil}        []      = pure []
modifyManyF f {prf = UMConsSame x} (v::vs) = [| f v :: modifyManyF f vs |]
modifyManyF f {prf = UMConsDiff x} (v::vs) = (v ::) <$> modifyManyF f vs

||| Replaces the first element of the given type
||| in an n-ary product, thereby possibly changing the
||| types of stored values.
public export %inline
setAt :  (0 t : k)
      -> (v' : f t')
      -> {auto prf : UpdateOnce t t' ks ks'}
      -> NP_ k f ks
      -> NP_ k f ks'
setAt t v' = modify {t = t} (const v')

||| Replaces several elements of the given type
||| in an n-ary product, thereby possibly changing the
||| types of stored values.
public export %inline
setAtMany :  (0 t : k)
          -> (v' : f t')
          -> {auto prf : UpdateMany t t' ks ks'}
          -> NP_ k f ks
          -> NP_ k f ks'
setAtMany t v' = modifyMany {t = t} (const v')

||| Alias for `setAt` for those occasions when
||| Idris cannot infer the type of the new value.
public export %inline
setAt' :  (0 t  : k)
       -> (0 t' : k)
       -> (v' : f t')
       -> {auto prf : UpdateOnce t t' ks ks'}
       -> NP_ k f ks
       -> NP_ k f ks'
setAt' t _ v' np = setAt t v' np

||| Alias for `setAtMany` for those occasions when
||| Idris cannot infer the type of the new value.
public export %inline
setAtMany' :  (0 t  : k)
           -> (0 t' : k)
           -> (v' : f t')
           -> {auto prf : UpdateMany t t' ks ks'}
           -> NP_ k f ks
           -> NP_ k f ks'
setAtMany' t _ v' np = setAtMany t v' np

--------------------------------------------------------------------------------
--          Narrowing and expanding products
--------------------------------------------------------------------------------

||| Extracts a subset of values from an n-ary product.
||| The values must appear in the same order in both lists.
public export
narrow : NP f ks -> {auto prf: Sublist ks' ks} -> NP f ks'
narrow x         {prf = SLNil}    = []
narrow (v :: vs) {prf = SLSame y} = v :: narrow vs
narrow (_ :: vs) {prf = SLDiff y} = narrow vs

||| Appends two n-ary products.
public export
append : NP f ks -> NP f ks' -> NP f (ks ++ ks')
append []        y = y
append (v :: vs) y = v :: append vs y

||| Expands an n-ary product by filling missing
||| values with the given default-generating function.
public export
expand :  {ks' : List k}
       -> (forall k . f k)
       -> NP f ks
       -> {auto prf : Sublist ks ks'}
       -> NP f ks'
expand f []                         = pureNP f
expand f (v :: vs) {prf = SLSame x} = v :: expand f vs
expand f vs        {prf = SLDiff x} = f :: expand f vs

||| Expands an n-ary product by filling missing
||| values with the given default-generating function.
|||
||| This is the constrained version of `expand`.
public export
cexpand :  (0 c : k -> Type)
        -> (cs : NP c ks')
        => (forall k . c k => f k)
        -> {auto prf : Sublist ks ks'}
        -> NP_ k f ks
        -> NP_ k f ks'
cexpand c {cs = []}   f []                         = []
cexpand c {cs = _::_} f []                         = f :: cexpand c f []
cexpand c {cs = _::_} f (v :: vs) {prf = SLSame x} = v :: cexpand c f vs
cexpand c {cs = _::_} f vs        {prf = SLDiff x} = f :: cexpand c f vs

--------------------------------------------------------------------------------
--          Interface Conversions
--------------------------------------------------------------------------------

||| This is needed to implement `Ord` below.
public export %hint
ordToEqNP : NP (Ord . f) ks -> NP (Eq . f) ks
ordToEqNP = mapNP (\_ => materialize Eq)

||| This is needed to implement `Monoid` below.
public export %hint
monoidToSemigroupNP : NP (Monoid . f) ks -> NP (Semigroup . f) ks
monoidToSemigroupNP = mapNP (\_ => materialize Semigroup)

--------------------------------------------------------------------------------
--          Implementations
--------------------------------------------------------------------------------

public export %inline
HPure k (List k) (NP_ k) where hpure  = pureNP

public export %inline
HFunctor k (List k) (NP_ k) where hmap  = mapNP

public export %inline
HAp k (List k) (NP_ k) (NP_ k) where hap = hapNP

public export %inline
HFold k (List k) (NP_ k) where
  hfoldl = foldlNP
  hfoldr = foldrNP

public export %inline
HCollapse k (List k) (NP_ k) List where hcollapse = collapseNP

public export %inline
HSequence k (List k) (NP_ k) where hsequence = sequenceNP

public export
(all : NP (Eq . f) ks) => Eq (NP_ k f ks) where
  (==) {all = []}     [] []               = True
  (==) {all = _ :: _} (v :: vs) (w :: ws) = v == w && vs == ws

public export
(all : NP (Ord . f) ks) => Ord (NP_ k f ks) where
  compare {all = []}     [] []               = EQ
  compare {all = _ :: _} (v :: vs) (w :: ws) = compare v w <+> compare vs ws

public export
(all : NP (Semigroup . f) ks) => Semigroup (NP_ k f ks) where
  (<+>) {all = []}     [] []               = []
  (<+>) {all = _ :: _} (v :: vs) (w :: ws) = (v <+> w) :: (vs <+> ws)

public export
(all : NP (Monoid . f) ks) => Monoid (NP_ k f ks) where
  neutral {all = []}     = []
  neutral {all = _ :: _} = neutral :: neutral

public export
(all : NP (Show . f) ks) => Show (NP_ k f ks) where
  show =  dispStringList . hcollapse . hcmap (Show . f) show

private
consInjective : Data.SOP.NP.(::) a b = Data.SOP.NP.(::) c d -> (a = c, b = d)
consInjective Refl = (Refl, Refl)

public export
(all : NP (DecEq . f) ks) => DecEq (NP_ k f ks) where
  decEq {all = []}     []        []        = Yes Refl
  decEq {all = _::_} (v::vs) (w::ws) with (decEq v w)
    decEq {all = _::_} (v::vs) (w::ws) | (No contra) =
      No $ contra . fst . consInjective
    decEq {all = _::_} (v::vs) (v::ws) | (Yes Refl) with (decEq vs ws)
      decEq {all = _::_} (v::vs) (v::vs) | (Yes Refl) | (Yes Refl) = Yes Refl
      decEq {all = _::_} (v::vs) (v::ws) | (Yes Refl) | (No contra) =
        No $ contra . snd . consInjective

--------------------------------------------------------------------------------
--          Examples and Tests
--------------------------------------------------------------------------------

Ex1 : NP I [Char,Bool]
Ex1 = ['c',True]

Ex2 : NP Maybe [Int,Int,Int]
Ex2 = [Nothing,Nothing,Just 2]

Ex3 : NP (K String) [Char,Bool,Int]
Ex3 = ["Hello","World","!"]

EqTest1 : Ex1 == Ex1 = True
EqTest1 = Refl

EqTest2 : Ex1 == ['x',False] = False
EqTest2 = Refl

OrdTest1 : compare Ex1 Ex1 = EQ
OrdTest1 = Refl

OrdTest2 : compare Ex1 ['x',False] = LT
OrdTest2 = Refl

HdTest : hd Ex1 = 'c'
HdTest = Refl

TlTest : tl Ex1 = [True]
TlTest = Refl

SemiTest : the (NP I [String]) ["hello"] <+> ["world"] = ["helloworld"]
SemiTest = Refl

NeutralTest : the (NP I [String,List Int]) Prelude.neutral = ["",[]]
NeutralTest = Refl

HMapTest : hmap Just Ex1 = [Just 'c', Just True]
HMapTest = Refl

HCMapRes : NP (K String) [Char,Bool]
HCMapRes = hcmap Show show Ex1

HPureTest : NP Maybe [String,Int]
HPureTest = hpure Nothing

CPureNeutralTest : NP I [String,String]
CPureNeutralTest = hcpure Monoid neutral

Person : (f : Type -> Type) -> Type
Person f = NP f [String,Int]

toPersonMaybe : Person I -> Person Maybe
toPersonMaybe = hmap Just

personShowValues : Person I -> Person (K String)
personShowValues = hcmap Show show

emptyPerson : Person Maybe
emptyPerson = hpure Nothing

fooPerson : Person (K String)
fooPerson = hconst "foo"

Foo : (f : Type -> Type) -> Type
Foo f = NP f [String,String,List Int]

neutralFoo : Foo I
neutralFoo = hcpure Monoid neutral

update : forall a . Maybe a -> I a -> I a
update (Just a) _ = a
update Nothing  a = a

updatePerson : Person (\a => a -> a)
updatePerson = hmap update [Just "foo", Nothing]

updatedPerson : Person I
updatedPerson = hap updatePerson ["bar",12]

seqMaybe : NP Maybe [Int,String] -> Maybe (NP I [Int,String])
seqMaybe = hsequence

htraverseEx : NP (Either String) [Int,String] -> Maybe (NP I [Int,String])
htraverseEx = htraverse (either (const Nothing) Just)

interface Read a where
  read : String -> Maybe a

hctraverseEx : NP Read [Int,String] => NP (K String) [Int,String] -> Maybe (NP I [Int,String])
hctraverseEx = hctraverse Read read

subproductEx : NP I [Int,String,Bool,Maybe Bool] -> NP I [Int,Bool]
subproductEx np = narrow np


text:
           module UninhIndent

           data MyElem : a -> List a -> Type where
             MyHere : MyElem x (x :: xs)
             MyThere : (later : MyElem x xs) -> MyElem x (y :: xs)

           Uninhabited (MyElem a []) where
             uninhabited c = ?uninhabited_rhs


text:
module Js.ServiceTypes
{-
import public Js.Json
import public Data.List

public export
data ServiceTy = RPCServiceTy Type Type
               | FeedServiceTy Type Type

public export
data EncoderDecoder a = MkEncoderDecoder (a -> String) (String -> Either String a)

public export
data Service : String -> ServiceTy -> Type where
  RPCService : (s:String) -> EncoderDecoder a -> EncoderDecoder b -> Service s (RPCServiceTy a b)
  FeedService : (s:String) -> EncoderDecoder a -> EncoderDecoder b -> Service s (FeedServiceTy a b)

public export
data ServiceGroup : List (String, ServiceTy) -> Type where
  Nil : ServiceGroup []
  (::) : Service s t -> ServiceGroup ts -> ServiceGroup ((s,t)::ts)

export
decode : EncoderDecoder a -> String -> Either String a
decode (MkEncoderDecoder _ d) x = d x

export
encode : EncoderDecoder a -> a -> String
encode (MkEncoderDecoder e _) x = e x

public export
getService : (name:String) -> ServiceGroup ts -> Elem (name, s) ts -> Service name s
getService name (x :: xs) Here = x
getService name (x :: xs) (There p') = getService name xs p'

export
jsonEncoderDecoder : BothJson a => EncoderDecoder a
jsonEncoderDecoder = MkEncoderDecoder encode decode
-}


text:
module Language.LSP.Message.SignatureHelp

import Language.JSON
import Language.LSP.Message.Location
import Language.LSP.Message.Derive
import Language.LSP.Message.URI
import Language.LSP.Message.Utils
import Language.LSP.Message.Markup
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Progress
import Language.Reflection

%language ElabReflection
%default total

namespace SignatureHelpClientCapabilities
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
  public export
  record SignatureHelpParameterInformation where
    constructor MkSignatureHelpParameterInformation
    labelOffsetSupport : Maybe Bool
  %runElab deriveJSON defaultOpts `{{SignatureHelpParameterInformation}}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
  public export
  record SignatureHelpInformation where
    constructor MkSignatureHelpInformation
    documentationFormat    : Maybe (List MarkupKind)
    parameterInformation   : Maybe SignatureHelpParameterInformation
    activeParameterSupport : Maybe Bool
  %runElab deriveJSON defaultOpts `{{SignatureHelpInformation}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
public export
record SignatureHelpClientCapabilities where
  constructor MkSignatureHelpClientCapabilities
  dynamicRegistration  : Maybe Bool
  signatureInformation : Maybe SignatureHelpInformation
  contextSupport       : Maybe Bool
%runElab deriveJSON defaultOpts `{{SignatureHelpClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
public export
record SignatureHelpOptions where
  constructor MkSignatureHelpOptions
  workDoneProgress    : Maybe Bool
  triggerCharacters   : Maybe (List Char)
  retriggerCharacters : Maybe (List Char)
%runElab deriveJSON defaultOpts `{{SignatureHelpOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
public export
record SignatureHelpRegistrationOptions where
  constructor MkSignatureHelpRegistrationOptions
  workDoneProgress    : Maybe Bool
  triggerCharacters   : Maybe (List Char)
  retriggerCharacters : Maybe (List Char)
  documentSelector    : OneOf [DocumentSelector, Null]
%runElab deriveJSON defaultOpts `{{SignatureHelpRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
namespace SignatureHelpTriggerKind
  public export
  data SignatureHelpTriggerKind = Invoked | TriggerCharacter | ContentChange

export
ToJSON SignatureHelpTriggerKind where
  toJSON Invoked          = JNumber 1
  toJSON TriggerCharacter = JNumber 2
  toJSON ContentChange    = JNumber 3

export
FromJSON SignatureHelpTriggerKind where
  fromJSON (JNumber 1) = pure Invoked
  fromJSON (JNumber 2) = pure TriggerCharacter
  fromJSON (JNumber 3) = pure ContentChange
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
public export
record ParameterInformation where
  constructor MkParameterInformation
  label         : OneOf [String, (Int, Int)]
  documentation : Maybe (OneOf [String, MarkupContent])
%runElab deriveJSON defaultOpts `{{ParameterInformation}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
public export
record SignatureInformation where
  constructor MkSignatureInformation
  label           : String
  documentation   : Maybe (OneOf [String, MarkupContent])
  parameters_     : Maybe (List ParameterInformation)
  activeParameter : Maybe Int
%runElab deriveJSON (record {renames = [("parameters_", "parameters")]} defaultOpts) `{{SignatureInformation}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
public export
record SignatureHelp where
  constructor MkSignatureHelp
  signatures      : List SignatureInformation
  activeSignature : Maybe Int
  activeParameter : Maybe Int
%runElab deriveJSON defaultOpts `{{SignatureHelp}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
public export
record SignatureHelpContext where
  constructor MkSignatureHelpContext
  triggerKind         : SignatureHelpTriggerKind
  triggerCharacter    : Maybe Char
  isRetrigger         : Bool
  activeSignatureHelp : Maybe SignatureHelp
%runElab deriveJSON defaultOpts `{{SignatureHelpContext}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_signatureHelp
public export
record SignatureHelpParams where
  constructor MkSignatureHelpParams
  workDoneToken : Maybe ProgressToken
  textDocument  : TextDocumentIdentifier
  position      : Position
  context       : Maybe SignatureHelpContext
%runElab deriveJSON defaultOpts `{{SignatureHelpParams}}