text:
--   Copyright 2017-2018 The Lathe Authors
--
--   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.

edgeLakeMedium : (d : Nat) -> Medium d -> Medium d
edgeLakeMedium d i = case d of
  0 => mediumZero ()
  1 + d' => mediumSucc d' (mediumEdge i) (\_ -> ())

edgeType : (d : Nat) -> Medium d -> Type
edgeType d i = Tower d i (edgeLakeMedium d i) refl

type Medium (d : Nat) where
  mediumZero : Type -> Medium 0
  mediumSucc :
    (d : Nat) -> (e : Medium d) -> (edgeType d e -> Type) ->
    Medium (1 + d)

mediumEdge : (d : Nat) -> Medium (1 + d) -> Medium d
mediumEdge d m = case m of
  mediumSucc d' edge contentTypes => edge

edgeEqType : (d : Nat) -> Medium d -> Medium d -> Type
edgeEqType d i l = case d in
  0 => () = ()
  1 + d' => mediumEdge d' i = mediumEdge d' l

towerMap :
  (d : Nat) ->
  (ix : Medium d) -> (lx : Medium d) -> (eqx : edgeEqType d ix lx) ->
  (iy : Medium d) -> (ly : Medium d) -> (eqy : edgeEqType d iy ly) ->
  (eqxy : edgeEqType d ix iy) ->
  (case (ix, iy) of
    (mediumZero tx, mediumZero ty) => () -> tx -> ty
    (mediumSucc dx ex cx, mediumSucc dy ey cy) =>
      (e : edgeType dx ex) -> cx e -> cy e) ->
  (case (lx, ly) of
    (mediumZero tx, mediumZero ty) => () -> tx -> ty
    (mediumSucc dx ex cx, mediumSucc dy ey cy) =>
      (e : edgeType dx ex) -> cx e -> cy e) ->
  Tower d ix lx eqx ->
  Tower d iy ly eqy
towerMap d ix lx eqx iy ly eqy eqxy ifunc lfunc tower = case tower of
  nil d' i l eq content =>
    nil d iy ly eqy
      (case d of
        0 => ifunc content
        1 + d' => case content of
          contentEdge * contentVal => contentEdge * ifunc contentVal)
  cons d' i l eq subtowers content =>
    cons d iy ly eqy
      (towerMap d'
        (mediumEdge ix)
        (subtowerMedium d' (mediumEdge lx) lx ix)
        refl
        (mediumEdge iy)
        (subtowerMedium d' (mediumEdge ly) ly iy)
        refl
        refl
        (\islandEdge island -> island)
        (\lakeEdge lake -> case lake of
          inl lake' => inl (lfunc lake')
          inr (subtowers * compatible) =>
            inr
              (towerMap d iy ly eqy ix lx eqx refl lfunc ifunc *
                compatible))
        subtowers)
      (case d of
        0 => ifunc content
        1 + d' => case content of
          contentEdge * contentVal => contentEdge * ifunc contentVal)

towerNullify :
  (d : Nat) -> (i : Medium d) -> (l : Medium d) ->
  (eqx : edgeEqType d i l) ->
  (eqy : edgeEqType d i (edgeLakeMedium d i)) ->
  Tower d i l eqx ->
  Tower d i (edgeLakeMedium d i) eqy
towerNullify d i l eqx eqy tower =
  towerMap d i l eqx i (edgeLakeMedium d i) eqy refl
    (\islandEdge island -> island)
    (\lakeEdge lake -> ())
    tower

merge : (x : a) -> (y : a) -> x = y -> a
merge x y eq = x

towerAllType :
  (d : Nat) -> (i : Medium d) -> (l : Medium d) ->
  (eq : edgeEqType d i l) ->
  (case i of
    mediumZero t => () -> t -> Type
    mediumSucc d e c => (edge : edgeType d e) -> c edge -> Type) ->
  (case l of
    mediumZero t => () -> t -> Type
    mediumSucc d e c => (edge : edgeType d e) -> c edge -> Type) ->
  Tower d i l eq ->
  Type
towerAllType d i l eq itype ltype tower = case tower of
  nil d' i' l' eq content => itype content
  cons d' i' l' eq subtowers content =>
    let im = merge i i' refl in
    let lm = merge l l' refl in
    let e = merge (mediumEdge im) (mediumEdge lm) eq in
    let sublake = (subtowerMedium d' e lm im) in
    itype (towerNullify d' e sublake refl refl subtowers) content *
    towerAllLakesType d' e sublake refl
      (\lakeEdge lake -> case lake of
        inl lakeVal => ()
        inr subtower => towerAllType d l i refl ltype itype subtower)
      subtowers

towerAllLakesType :
  (d : Nat) -> (i : Medium d) -> (l : Medium d) ->
  (eq : edgeEqType d i l) ->
  (case l of
    mediumZero t => () -> t -> Type
    mediumSucc d e c => (edge : edgeType d e) -> c edge -> Type) ->
  Tower d i l eq ->
  Type
towerAllLakesType d i l eq ltype tower =
  towerAllType d i l eq (\islandEdge island -> ()) ltype tower

type Medium (d : Nat) where
  mediumZero : Type -> Medium 0
  mediumSucc :
    (d : Nat) -> (e : Medium d) -> (edgeType d e -> Type) ->
    Medium (1 + d)

mediumCons :
  (d : Nat) -> (a : Medium d) -> (b : Medium d) ->
  (eq : edgeEqType d a b) ->
  Medium d
mediumCons d a b eq = case (a, b) of
  (mediumZero ca, mediumZero cb) => mediumZero (ca, cb)
  (mediumSucc da ea ca, mediumSucc db eb cb) =>
    mediumSucc (merge da db refl) (merge ea eb eq)
      (\content -> (ca content, cb content))

towerCons :
  (d : Nat) ->
  (ia : Medium d) -> (la : Medium d) -> (eqa : edgeEqType d ia la) ->
  (ib : Medium d) -> (lb : Medium d) -> (eqb : edgeEqType d ib lb) ->
  (eqi : edgeEqType d ia ib) ->
  (eql : edgeEqType d la lb) ->
  (eqy :
    edgeEqType d (mediumCons d ia ib eqi) (mediumCons d la lb eql)) ->
  Tower d ia la eqa ->
  Tower d ib lb eqb ->
  Tower d (mediumCons d ia ib eqi) (mediumCons d la lb eql) eqy
towerCons d ia la eqa ib lb eqb eqi eql eqy a b = case (a, b) of
  (nil da ia' la' eqa' contenta, nil db ib' lb' eqb' contentb) =>
    nil d (mediumCons d ia la eqa) (mediumCons d ib lb eqb) refl
      (contenta, contentb)
  (cons da ia' la' eqa' subtowersa contenta,
    cons db ib' lb' eqb' subtowersb contentb) =>
    let d' = merge da db refl in
    let e = merge (mediumEdge ia) (mediumEdge ib) eqi in
    cons d (mediumCons d ia la eqa) (mediumCons d ib lb eqb) refl
      (towerMap d'
        (mediumCons d' e e refl)
        (mediumCons d'
          (subtowerMedium d' e la ia)
          (subtowerMedium d' e lb ib)
          refl)
        refl
        e
        (subtowerMedium d e
          (mediumCons d la lb eql)
          (mediumCons d ia ib eqi))
        refl
        (\islandEdge island -> case island of
          -- TODO: See if there's some way we should be merging these.
          (ca, cb) => ca)
        (\lakeEdge lake -> case lake of
          (inl ca, inl cb) => inl (ca, cb)
          (inr subtowera, inr subtowerb) =>
            inr
              (towerCons d la ia refl lb ib refl refl refl refl
                subtowera subtowerb)
          _ => error "Expected towers a and b to be compatible")
        (towerCons d
          e (subtowerMedium d e la ia) refl
          e (subtowerMedium d e la ia) refl
          refl refl refl
          subtowersa subtowersb))
      (contenta, contentb)

towerEdge t = TODO

towerCompatibleType :
  (d : Nat) ->
  (ia : Medium d) -> (la : Medium d) -> (eqa : edgeEqType d ia la) ->
  Tower d ia la eqa ->
  (ib : Medium d) -> (lb : Medium d) -> (eqb : edgeEqType d ib lb) ->
  Tower d ib lb eqb ->
  edgeEqType d ia ib ->
  Type
towerCompatibleType d ia la eqa a ib lb eqb b eqi = case (a, b) of
  (nil da' ia' la' eqa' contenta, nil db' ib' lb' eqb' contentb) -> ()
  (cons da' ia' la' eqa' subtowersa contenta,
    cons db' ib' lb' eqb' subtowersb contentb) ->
    let d' = merge da' db' refl in
    let ea = merge (mediumEdge ia) (mediumEdge la) eqa in
    let eb = merge (mediumEdge ib) (mediumEdge lb) eqb in
    towerCompatibleType d'
      ea (subtowerMedium d' ea la ia) refl subtowersa
      eb (subtowerMedium d' eb lb ib) refl subtowersb
      refl *
    towerAllLakesType d
      (mediumCons d ia ib eqi)
      (mediumCons d la lb refl)
      refl
      (\lakeEdge lake -> case lake of
        (inl ca, inl cb) => ()
        (inr subtowera, inr subtowerb) =>
          towerCompatibleType d
            la ia refl subtowera lb ib refl subtowerb refl
        _ => Bot)
      (towerCons d'
        ea (subtowerMedium d' ea la ia) refl
        eb (subtowerMedium d' eb lb ib) refl
        refl refl refl
        subtowersa subtowersb)
  _ -> Bot

subtowerMedium :
  (d : Nat) ->
  Medium d ->
  (subtowerIsland : Medium (1 + d)) ->
  (subtowerLake : Medium (1 + d)) ->
  edgeEqType (1 + d) subtowerIsland subtowerLake ->
  Medium d
subtowerMedium d main subtowerIsland subtowerLake eq = case main of
  mediumZero t => mediumZero t
  mediumSucc d' thisMediumEdge contentTypes =>
    mediumSucc d' thisMediumEdge
      (\contentEdge ->
        contentTypes contentEdge +
        (
          (subtowers : Tower (1 + d) subtowerIsland subtowerLake eq) *
          towerCompatibleType d'
            TODO TODO refl contentEdge
            TODO TODO refl (towerEdge (towerEdge subtowers))
            refl))

type Tower (d : Nat) (i : Medium d) (l : Medium d)
  (eq : edgeEqType d i l)
where
  nil :
    (d : Nat) -> (i : Medium d) -> (l : Medium d) ->
    (eq : edgeEqType d i l) ->
    (case i of
      mediumZero contentType => contentType
      mediumSucc d' thisMediumEdge contentTypes =>
        (contentEdge : edgeType d' thisMediumEdge) *
        contentTypes contentEdge) ->
    Tower d i l eq
  cons :
    (d : Nat) -> (i : Medium (1 + d)) -> (l : Medium (1 + d)) ->
    (eq : edgeEqType (1 + d) i l) ->
    let e = merge (mediumEdge i) (mediumEdge l) eq in
    (subtowers : Tower d e (subtowerMedium d e l i) refl) ->
    (case i of
      mediumSucc d' thisMediumEdge contentTypes =>
        contentTypes
          (towerNullfiy d e (subtowerMedium d e l i) refl refl
            subtowers) ->
        Tower (1 + d) i l eq)

max_stars_repo_name: rocketnia/lexmeta

max_issues_repo_name: rocketnia/lexmeta

max_forks_repo_name: lathe/punctaffy-for-racket


text:
module Minecraft.Base.PreClassic.Air

%default total

public export
record Block where
  constructor MkBlock

ext: idr

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
module Http.Request

import public Data.SortedMap
import public Http.Uri

%access export

||| The HTTP Method which is either POST or GET
public export
data Method = POST | GET | HEAD

implementation Show Method where
  show POST = "POST"
  show GET  = "GET"
  show HEAD = "HEAD"

implementation Eq Method where
  x == y = show x == show y

implementation Cast String Method where
  cast "POST" = POST
  cast "HEAD" = HEAD
  cast _      = GET

||| A String-alias for Hosts.
public export
Host : Type
Host = String

||| A type alias for HTTP Versions.
||| HttpVersion shall have the value "HTTP/1.0" or "HTTP/1.1"
HttpVersion : Type
HttpVersion = String

httpVersion : HttpVersion
httpVersion = "HTTP/1.1"

||| A data type for requests.
||| A request consists out of a method,
||| a host, a port, a path, a query and a http version.
public export
record Request a where
  constructor MkRequest
  ||| The requests method. Either POST or GET.
  method : Method

  ||| The URI we're attempting to access.
  uri : URI

  requestBody : a

  ||| Headers to pass along.
  headers : SortedMap String String

||| This is the first line of a request line defined in RFC7230 Section 3.1.1.
|||
||| @ req The request to get the request line from.
private
requestLine : (req : Request a) -> String
requestLine req =
  show (method req) ++ " " ++ uriToString (uri req) ++ " " ++ httpVersion ++ "\r\n"

||| This is a CRLF seperated list of header-fields as defined in RFC7230 Section 3.2.
|||
||| @ req The request to get the header string from.
private
headerFields : (req : Request a) -> String
headerFields req = fields . toList $ headers req
  where
    fields : List (String, String) -> String
    fields [] = ""
    fields ((k,v) :: xs) = k ++ ": " ++ v ++ "\r\n" ++ fields xs

||| Convert a request into a string.
||| This follows RFC7230's definition of an HTTP-Message defined in Section 3.
|||
||| @ req The request to convert.
resolveRequest : (req : Request a) -> String
resolveRequest req =
  requestLine req ++ headerFields req ++ "\r\n"

max_stars_repo_name: unthingable/idris-https

max_issues_repo_name: unthingable/idris-https

max_forks_repo_name: unthingable/idris-https


text:
module xquant.Graph.Feynman

import xquant.Graph.Marked
import Control.Algebra

%default total

||| Fixed interaction order scalar particle graph
||| @ n number of line endpoints attached to each vertex (interaction order)
||| @ l number of lines
||| @ v number of vertices
||| @ m which line endpoints are attached to vertices
data ScalarGraph : (n : Nat) ->
                   (l : Nat) ->
                   (v : Nat) ->
                   (m : Marks (2*l) j) ->
                   Type where
  Grf : (n : Nat) ->
        (l : Nat) ->
        ScalarGraph n l Z allO
  vertex : (x : Marks (2*l) n) ->
           {y : Marks (2*l) j} ->
           (c : Compat x y) ->
           ScalarGraph n l v y ->
           ScalarGraph n l (S v) (markAdd c)

||| The number of external lines is the number of endpoints not connected to vertices
external : ScalarGraph n p v m -> Nat
external {n} {p} {v} g = 2*p `minus` n*v

-- example: the interaction vertex in phi^3 theory
phi3vertex : ScalarGraph 3 3 1 [O,X,O,X,O,X]
phi3vertex = vertex [O,X,O,X,O,X]
                    (ComOO $ ComXO $ ComOO $ ComXO $ ComOO $ ComXO ComZero)
                    (Grf 3 3)

||| Directed Graph with fixed number of line-endpoints per vertex
||| @ n number of line endpoints attached to each vertex (interaction order)
||| @ l number of lines
||| @ v number of vertices
||| @ m which line endpoints are attached to vertices
||| @ h which line arrows are reversed
data Digraph : (n : Nat) ->
               (l : Nat) ->
               (v : Nat) ->
               (m : Marks (2*l) j) ->
               (h : Marks l k) ->
               Type where
  DiGrf : (n : Nat) ->
          (l : Nat) ->
          Digraph n l Z empty (empty_ l)
  DiVrtx : (x : Marks (2*l) n) ->
           {y : Marks (2*l) j} ->
           (c : Compat x y) ->
           Digraph n l v y r ->
           Digraph n l (S v) (markAdd c) r

||| Very basic particle content. Should dramatically generalize from here
||| Here only takes number of scalars and fermions
data ParticleContent = Particles Nat Nat

data VertexType : Nat -> Type where
   VertType : (b : Nat) -> (f : Nat) -> VertexType (n + 2*m)

-- data SFPropagator : Nat -> Type where
-- SFProp : Marks 2

||| Directed Graph with fixed number of line-endpoints per vertex
||| @ s scalar lines
||| @ f fermion lines
||| @ v number of vertices
||| @ sm which scalar line endings are attached to vertices
||| @ fb which fermionic line _beginnings_ are attached to vertices
||| @ fe which fermionic line _end_points are attached to vertices
data SimpScalarFermion : (s : Nat) ->
                         (f : Nat) ->
                         (v : Nat) ->
                         (sm : Marks (2*s) i) ->
                         (fb : Marks f j) ->
                         (fe : Marks f j) -> Type where
  SFGrf : (s,f : Nat) ->
          SimpScalarFermion s f Z empty (empty_ _) (empty_ _)
  SFVrtx : SimpScalarFermion s f v sm fb fe ->
           {x : Marks (2*s) 1} ->
           {y : Marks f 1} ->
           {z : Marks f 1} ->
           (c : Compat x sm) ->
           (d : Compat y fb) ->
           (e : Compat z fe) ->
           SimpScalarFermion s f (S v) (markAdd c) (markAdd d) (markAdd e)

max_stars_repo_name: BlackBrane/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
-- @generated by 'make'/'make build'
module IdvPaths.Generated

export
idvLocation : String
idvLocation = "~/.idv"

export
defaultIdris2Location : String
defaultIdris2Location = "~/.idris2/bin/idris2"

max_stars_repo_name: memoryruins/idv

max_issues_repo_name: memoryruins/idv

max_forks_repo_name: memoryruins/idv


text:
module gcd

import NatUtils
import NatOrder

%default total
%access public export

|||Auxilliary proof for euclidDivide
--Proof to finish euclidDivide, couldn't add it as a where clause within euclidDivide. If someone knows how to do that, please do so.
extendedEqualityProof : (a : Nat) -> (b : Nat) -> (q : Nat) -> (r : Nat)->
					((S r) = b) -> (a = r + (q * b)) -> (S a = (S q) * b)
extendedEqualityProof a b q r proofSmlEq proofBigEq =
	trans (cong proofBigEq) (plusConstantRight (S r) b (q * b) proofSmlEq)

||| Given a, b, and a proof that b != 0, returns (q, r) and proofs that a = bq + r, r < b
--removed possible problems with Rohit's
euclidDivide : (a : Nat) -> (b : Nat) -> (Not (b = Z)) ->
			(q : Nat ** (r : Nat ** (a = r + (q * b), LNEQ r b)))
euclidDivide _ Z proofeq = void(proofeq Refl)
euclidDivide Z (S k) SIsNotZ = (Z ** (Z ** (Refl, (LEQZero, ZIsNotS))))
euclidDivide (S n) (S k) SIsNotZ =
	case (euclidDivide n (S k) SIsNotZ) of
		(q ** (r ** (proofEq, proofLNEQ))) =>
			case (lneqImpliesEqOrLNEQ r (S k) proofLNEQ) of
				(Right proofSrLNEQSk) => (q ** ((S r) ** ((cong proofEq), proofSrLNEQSk)))
				(Left proofSrEqSk) => ((S q)** (Z ** ((extendedEqualityProof n (S k) q r proofSrEqSk proofEq), (LEQZero, ZIsNotS))))

||| Given a, b, and a proof that b != 0, returns (q, r) and proofs that a = bq + r, r < b (Old Version)
--removed possible problems with Rohit's
eculidDivideAux : (a : Nat) -> (b : Nat) ->
  (b = Z -> Void) -> (q : Nat ** (r : Nat ** ((a = r + (q * b)), LT r b)))
eculidDivideAux a b pf =
	let
		res = euclidDivide a b pf
		q = DPair.fst res
		r = DPair.fst (DPair.snd res)
		eqn = fst (DPair.snd (DPair.snd res))
		ltpf = lneqToLT (snd (DPair.snd (DPair.snd res)))
	in
		(q ** (r ** (eqn , ltpf)))

|||Type of proof that d divides a
isDivisible : (a : Nat) -> (d : Nat) -> (Not (d = Z)) -> Type
isDivisible a d proofNotZ = (n : Nat ** a = n * d)

|||Proof that all natural numbers divide zero
zeroDivisible : {n : Nat} ->  isDivisible Z (S n) SIsNotZ
zeroDivisible {n} = (Z ** sym (multZeroLeftZero (S n)))

|||Proof that 1 divides all natural numbers
oneDivides : {n : Nat} -> isDivisible n (S Z) SIsNotZ
oneDivides {n} = (n ** rewrite multOneRightNeutral n in Refl)

|||Proof that all natural numbers divide themselves
divisionReflexive : {n : Nat} -> (isDivisible (S n) (S n) SIsNotZ)
divisionReflexive {n} = (S Z ** rewrite multOneLeftNeutral n in Refl)

|||Type of proof that d is a common divisor of a and b
isCommonDivisor : (a : Nat) -> (b : Nat) -> (d : Nat) -> (Not (d = Z)) -> Type
isCommonDivisor a b d proofNotZ = (isDivisible a d proofNotZ, isDivisible b d proofNotZ)

|||Type of proof that d is the GCD of a and b, where atleast one of a and b are non-zero
isGCD : (a : Nat) -> (b : Nat) -> Either (Not (a = Z)) (Not (b = Z)) -> (d : Nat) -> Type
isGCD a b notBothZ d = (dIsNotZ : Not (d = Z) ** ((isCommonDivisor a b d dIsNotZ), (n : Nat) -> (proofNotZ : Not (n = Z)) -> (isCommonDivisor a b n proofNotZ) -> (isDivisible d n proofNotZ)))

|||Proof that 1 is a common divisor of all pairs of natural numbers
oneCommonDivisor : {a : Nat} -> (b : Nat) -> (isCommonDivisor a b (S Z) SIsNotZ)
oneCommonDivisor {a} {b} = (oneDivides, oneDivides)

|||Proof that n is a common divisor of n and 0
zeroCommonDivisorRight : {n : Nat} -> (isCommonDivisor (S n) Z (S n) SIsNotZ)
zeroCommonDivisorRight {n} = (divisionReflexive, zeroDivisible)

|||Proof that n is a common divisor of 0 and n
zeroCommonDivisorLeft : {n : Nat} -> (isCommonDivisor Z (S n) (S n) SIsNotZ)
zeroCommonDivisorLeft {n} = (zeroDivisible, divisionReflexive)

|||Proof that a common divisor of (a, b) is a common divisor of (b, a)
commonDivisorSymmetric : {a : Nat} -> {b : Nat} -> {d : Nat} -> {proofNotZ : Not (d = Z)} ->
					(isCommonDivisor a b d proofNotZ) -> (isCommonDivisor b a d proofNotZ)
commonDivisorSymmetric {a} {b} {d} (proofDividesa, proofDividesb) = (proofDividesb, proofDividesa)

|||Proof d divides a and a = b implies d divides b
eqConservesDivisible : {a : Nat} -> {b : Nat} -> {d : Nat} -> {proofNotZ : Not (d = Z)} ->
					(isDivisible a d proofNotZ) -> (a = b) -> (isDivisible b d proofNotZ)
eqConservesDivisible {a} {d} (n ** proofDivides) Refl = (n ** proofDivides)

|||Proof that d divides a implies d divides c * a
dividesMultiple : {a : Nat} -> {d : Nat} -> {proofNotZ : Not (d = Z)} ->
				(isDivisible a d proofNotZ) -> (c : Nat)-> (isDivisible (c * a) d proofNotZ)
dividesMultiple {d} (n ** Refl) c = ((c * n) ** (rewrite (multAssociative c n d) in Refl))

|||Proof that d is a common divisor of a and b implies d divides a + b
dividesSum :  {a : Nat} -> {b : Nat} -> {d : Nat} -> {proofNotZ : Not (d = Z)} ->
			(isCommonDivisor a b d proofNotZ)-> (isDivisible (a + b) d proofNotZ)
dividesSum {a} {b} {d} ((m ** proofDividesa), (n ** proofDividesb)) =
	((m + n) ** (distributeProof a b d m n proofDividesa proofDividesb))

|||Proof that d is a common divisor of a and b implies d divides a * x + b * y
dividesLinearCombination :  {a : Nat} -> {b : Nat} -> {d : Nat} -> {proofNotZ : Not (d = Z)} ->
						(isCommonDivisor a b d proofNotZ) -> (x : Nat) -> (y : Nat) ->
						(isDivisible ((x * a) + (y * b)) d proofNotZ)
dividesLinearCombination {proofNotZ = prf} commonDivisorProof x y =
	dividesSum {proofNotZ = prf} ((dividesMultiple {proofNotZ = prf} (fst commonDivisorProof) x), (dividesMultiple {proofNotZ = prf} (snd commonDivisorProof) y))

|||Proof that d divides n and n != 0 implies n >= d
dividesImpliesGEQ : {n : Nat} -> {d : Nat} -> {proofNotZ : Not (d = Z)} -> (isDivisible n d proofNotZ) -> (Not (n = Z)) -> (LEQ d n)
dividesImpliesGEQ {n} {d} {proofNotZ} (k ** proofEq) nNotZ =
	case k of
		Z => void (nNotZ proofEq)
		(S l) =>  ((l * d) ** (sym proofEq))

|||Proof that d divides (a + b) and d divides b implies d divides a
dividesDifference : {a : Nat} -> {b : Nat} -> {d : Nat} -> {proofNotZ : Not (d = Z)} -> (isDivisible (a + b) d proofNotZ) -> (isDivisible b d proofNotZ) -> (isDivisible a d proofNotZ)
dividesDifference {a} {b} {d} {proofNotZ} (n ** proofDivSum) (m ** proofDivb) =
	case (leqDivConstantRight proofNotZ (eqPreservesLEQ (a ** (plusCommutative b a)) proofDivb proofDivSum)) of
	(l ** proofEq) =>
		(l ** sym (plusLeftCancel b (l * d) a (rewrite (plusCommutative b a) in (rewrite proofDivSum in (rewrite proofDivb in (trans (sym (multDistributesOverPlusLeft m l d)) (cong {f = (\n => n * d)} proofEq)))))))

|||Proof that if n = r + q * d, where r ! = 0 and r < d,  then n is not divisible by d
notDivisible : {n : Nat} -> {r : Nat} -> {q : Nat} -> {d : Nat} -> (dNotZ : Not (d = Z)) ->
			(Not (r = Z)) -> (LNEQ r d) -> (n = r + (q * d)) -> (Not (isDivisible n d dNotZ))
notDivisible {n} {r} {q} {d} dNotZ rNotZ proofLNEQ proofEq (k ** proofDiv) =
	(leqImpliesNotLNEQ dLEQr proofLNEQ) where
		dLEQr = (dividesImpliesGEQ {proofNotZ = dNotZ} dDividesr rNotZ) where
			dDividesr = dividesDifference {proofNotZ = dNotZ} (k ** (trans (sym proofEq) proofDiv)) (q ** Refl)

|||Decision procedure to check if n is divisible by d
decDivisible : (n : Nat) -> (d : Nat) -> (proofNotZ : Not (d = Z)) -> Dec (isDivisible n d proofNotZ)
decDivisible n d proofNotZ = case (euclidDivide n d proofNotZ) of
	(q ** (r ** ((proofEq, proofLNEQ)))) =>
	case r of
		Z => Yes (q ** proofEq)
		(S k) => No (notDivisible proofNotZ SIsNotZ proofLNEQ proofEq)

|||Proof that d divides a, d divides b and a = r + q * b implies d divides r
dividesDiffExtend : {a : Nat} -> {b : Nat} -> {q : Nat} -> {r : Nat} -> {proofNotZ : Not (d = Z)} ->
 				(isDivisible a d proofNotZ) -> (isDivisible b d proofNotZ) -> (a = r + (q * b)) -> (isDivisible r d proofNotZ)
dividesDiffExtend {a} {b} {q} {r} {proofNotZ = dNotZ} dDividesa dDividesb proofEq =
	dividesDifference {proofNotZ = dNotZ} (eqConservesDivisible dDividesa proofEq) (dividesMultiple dDividesb q)

|||Returns the GCD of a and b with proof that it is the GCD
euclidGCD : (bound : Nat) -> (a : Nat) -> (b : Nat) -> (LTE a bound) -> (LTE (S b) bound) -> (notBothZ : (Either (Not (a = Z)) (Not (b = Z)))) -> (d : Nat ** (isGCD a b notBothZ d))
euclidGCD bound Z Z _ _ notBothZ = case notBothZ of
				Left notZ => void (notZ Refl)
				Right notZ => void (notZ Refl)
euclidGCD bound (S a) Z _ _ _ = ((S a) ** (SIsNotZ ** (zeroCommonDivisorRight, (\n : Nat => (\proofNotZ => (\proofCommonDivisor => (fst proofCommonDivisor)))))))
euclidGCD bound Z (S b) _ _ _ = ((S b) ** (SIsNotZ ** (zeroCommonDivisorLeft, (\n : Nat => (\proofNotZ => (\proofCommonDivisor => (snd proofCommonDivisor)))))))
euclidGCD Z (S a) (S b) lteLeft lteRight _ = void (succNotLTEzero lteLeft)
euclidGCD (S bound) (S a) (S b) (LTESucc lteLeft) (LTESucc lteRight) notBothZ =
	case (euclidDivide (S a) (S b) SIsNotZ) of
	(q ** (r ** (proofEq, proofLNEQ))) =>
		case (euclidGCD bound (S b) r lteRight (lteTransitive (lneqToLT proofLNEQ) lteRight) (Left SIsNotZ)) of
		(d ** (dNotZ ** (commonDivisorProof,  largestDivisorProof))) =>
			(d ** (dNotZ ** (((eqConservesDivisible {proofNotZ = dNotZ} (dividesSum {proofNotZ = dNotZ} ((snd commonDivisorProof), dividesMultiple {proofNotZ = dNotZ} (fst commonDivisorProof) q)) (sym proofEq)), (fst commonDivisorProof)), (\n => (\nNotZ => (\commonDivisor => (largestDivisorProof n nNotZ ((snd commonDivisor), (dividesDiffExtend {proofNotZ = nNotZ} (fst commonDivisor) (snd commonDivisor) proofEq)))))))))


text:
module LightClick.Types.Sensitivity

import Decidable.Equality

import Toolkit.Decidable.Informative

%default total

||| Capture wire sensitivity
public export
data Sensitivity = High | Low | Rising | Falling | Insensitive

highNotLow : (High = Low) -> Void
highNotLow Refl impossible

highNotRising : (High = Rising) -> Void
highNotRising Refl impossible

highNotFalling : (High = Falling) -> Void
highNotFalling Refl impossible

highNotInsenitive : (High = Insensitive) -> Void
highNotInsenitive Refl impossible

lowNotRising : (Low = Rising) -> Void
lowNotRising Refl impossible

lowNotFalling : (Low = Falling) -> Void
lowNotFalling Refl impossible

lowNotInsensitive : (Low = Insensitive) -> Void
lowNotInsensitive Refl impossible

risingNotFalling : (Rising = Falling) -> Void
risingNotFalling Refl impossible

risingNotInsensitive : (Rising = Insensitive) -> Void
risingNotInsensitive Refl impossible

fallingNotInsensitive : (Falling = Insensitive) -> Void
fallingNotInsensitive Refl impossible

export
DecEq Sensitivity where
  decEq High High        = Yes Refl
  decEq High Low         = No highNotLow
  decEq High Rising      = No highNotRising
  decEq High Falling     = No highNotFalling
  decEq High Insensitive = No highNotInsenitive

  decEq Low High        = No (negEqSym highNotLow)
  decEq Low Low         = Yes Refl
  decEq Low Rising      = No lowNotRising
  decEq Low Falling     = No lowNotFalling
  decEq Low Insensitive = No lowNotInsensitive

  decEq Rising High        = No (negEqSym highNotRising)
  decEq Rising Low         = No (negEqSym lowNotRising)
  decEq Rising Rising      = Yes Refl
  decEq Rising Falling     = No risingNotFalling
  decEq Rising Insensitive = No risingNotInsensitive

  decEq Falling High        = No (negEqSym highNotFalling)
  decEq Falling Low         = No (negEqSym lowNotFalling)
  decEq Falling Rising      = No (negEqSym risingNotFalling)
  decEq Falling Falling     = Yes Refl
  decEq Falling Insensitive = No fallingNotInsensitive

  decEq Insensitive High        = No (negEqSym highNotInsenitive)
  decEq Insensitive Low         = No (negEqSym lowNotInsensitive)
  decEq Insensitive Rising      = No (negEqSym risingNotInsensitive)
  decEq Insensitive Falling     = No (negEqSym fallingNotInsensitive)
  decEq Insensitive Insensitive = Yes Refl

public export
data Compatible : (l,r : Sensitivity) -> Type
  where
    SameSense : Compatible a a
    ToInsense : Compatible a Insensitive
    FoInsense : Compatible Insensitive a

negCompatibleSym : (Compatible l r -> Void) -> Compatible r l -> Void
negCompatibleSym f SameSense = f SameSense
negCompatibleSym f ToInsense = f FoInsense
negCompatibleSym f FoInsense = f ToInsense

noHL : Compatible High Low -> Void
noHL SameSense impossible
noHL ToInsense impossible
noHL FoInsense impossible

noHF : Compatible High Falling -> Void
noHF SameSense impossible
noHF ToInsense impossible
noHF FoInsense impossible

noHR : Compatible High Rising -> Void
noHR SameSense impossible
noHR ToInsense impossible
noHR FoInsense impossible

noLR : Compatible Low Rising -> Void
noLR SameSense impossible
noLR ToInsense impossible
noLR FoInsense impossible

noLF : Compatible Low Falling -> Void
noLF SameSense impossible
noLF ToInsense impossible
noLF FoInsense impossible

noRF : Compatible Rising Falling -> Void
noRF SameSense impossible
noRF ToInsense impossible
noRF FoInsense impossible

namespace Compatibility
  namespace Sensitivity
    public export
    data Error = NoChangeFromHigh
               | NoChangeFromLow
               | NoChangeFromRising
               | NoChangeFromFalling
export
compatible : (l,r : Sensitivity) -> DecInfo Compatibility.Sensitivity.Error (Compatible l r)
compatible High High = Yes SameSense
compatible Low Low = Yes SameSense
compatible Rising Rising = Yes SameSense
compatible Falling Falling = Yes SameSense
compatible Insensitive Insensitive = Yes SameSense
compatible Insensitive b = Yes FoInsense
compatible a Insensitive = Yes ToInsense

compatible High Low     = No NoChangeFromHigh noHL
compatible High Rising  = No NoChangeFromHigh noHR
compatible High Falling = No NoChangeFromHigh noHF

compatible Low High     = No NoChangeFromLow (negCompatibleSym noHL)
compatible Low Rising   = No NoChangeFromLow noLR
compatible Low Falling  = No NoChangeFromLow noLF

compatible Rising High    = No NoChangeFromRising (negCompatibleSym noHR)
compatible Rising Low     = No NoChangeFromRising (negCompatibleSym noLR)
compatible Rising Falling = No NoChangeFromRising noRF

compatible Falling High   = No NoChangeFromFalling (negCompatibleSym noHF)
compatible Falling Low    = No NoChangeFromFalling (negCompatibleSym noLF)
compatible Falling Rising = No NoChangeFromFalling (negCompatibleSym noRF)

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Web.Internal.SvgPrim

import JS
import Web.Internal.Types

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

namespace SVGAElement

  export
  %foreign "browser:lambda:x=>x.download"
  prim__download : SVGAElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.download = v}"
  prim__setDownload : SVGAElement -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.hreflang"
  prim__hreflang : SVGAElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.hreflang = v}"
  prim__setHreflang : SVGAElement -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.ping"
  prim__ping : SVGAElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.ping = v}"
  prim__setPing : SVGAElement -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.referrerPolicy"
  prim__referrerPolicy : SVGAElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.referrerPolicy = v}"
  prim__setReferrerPolicy : SVGAElement -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.rel"
  prim__rel : SVGAElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.rel = v}"
  prim__setRel : SVGAElement -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.relList"
  prim__relList : SVGAElement -> PrimIO DOMTokenList

  export
  %foreign "browser:lambda:x=>x.target"
  prim__target : SVGAElement -> PrimIO SVGAnimatedString

  export
  %foreign "browser:lambda:x=>x.text"
  prim__text : SVGAElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.text = v}"
  prim__setText : SVGAElement -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : SVGAElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.type = v}"
  prim__setType : SVGAElement -> String -> PrimIO ()

namespace SVGAngle

  export
  %foreign "browser:lambda:x=>x.unitType"
  prim__unitType : SVGAngle -> PrimIO Bits16

  export
  %foreign "browser:lambda:x=>x.value"
  prim__value : SVGAngle -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.value = v}"
  prim__setValue : SVGAngle -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.valueAsString"
  prim__valueAsString : SVGAngle -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.valueAsString = v}"
  prim__setValueAsString : SVGAngle -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.valueInSpecifiedUnits"
  prim__valueInSpecifiedUnits : SVGAngle -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.valueInSpecifiedUnits = v}"
  prim__setValueInSpecifiedUnits : SVGAngle -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.convertToSpecifiedUnits(a)"
  prim__convertToSpecifiedUnits : SVGAngle -> Bits16 -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.newValueSpecifiedUnits(a,b)"
  prim__newValueSpecifiedUnits : SVGAngle -> Bits16 -> Double -> PrimIO ()

namespace SVGAnimatedAngle

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal : SVGAnimatedAngle -> PrimIO SVGAngle

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal : SVGAnimatedAngle -> PrimIO SVGAngle

namespace SVGAnimatedBoolean

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal : SVGAnimatedBoolean -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal : SVGAnimatedBoolean -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,v)=>{x.baseVal = v}"
  prim__setBaseVal : SVGAnimatedBoolean -> Boolean -> PrimIO ()

namespace SVGAnimatedEnumeration

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal : SVGAnimatedEnumeration -> PrimIO Bits16

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal : SVGAnimatedEnumeration -> PrimIO Bits16

  export
  %foreign "browser:lambda:(x,v)=>{x.baseVal = v}"
  prim__setBaseVal : SVGAnimatedEnumeration -> Bits16 -> PrimIO ()

namespace SVGAnimatedInteger

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal : SVGAnimatedInteger -> PrimIO Int32

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal : SVGAnimatedInteger -> PrimIO Int32

  export
  %foreign "browser:lambda:(x,v)=>{x.baseVal = v}"
  prim__setBaseVal : SVGAnimatedInteger -> Int32 -> PrimIO ()

namespace SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal : SVGAnimatedLength -> PrimIO SVGLength

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal : SVGAnimatedLength -> PrimIO SVGLength

namespace SVGAnimatedLengthList

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal : SVGAnimatedLengthList -> PrimIO SVGLengthList

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal : SVGAnimatedLengthList -> PrimIO SVGLengthList

namespace SVGAnimatedNumber

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal : SVGAnimatedNumber -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal : SVGAnimatedNumber -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.baseVal = v}"
  prim__setBaseVal : SVGAnimatedNumber -> Double -> PrimIO ()

namespace SVGAnimatedNumberList

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal : SVGAnimatedNumberList -> PrimIO SVGNumberList

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal : SVGAnimatedNumberList -> PrimIO SVGNumberList

namespace SVGAnimatedPreserveAspectRatio

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal :  SVGAnimatedPreserveAspectRatio
                -> PrimIO SVGPreserveAspectRatio

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal :  SVGAnimatedPreserveAspectRatio
                -> PrimIO SVGPreserveAspectRatio

namespace SVGAnimatedRect

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal : SVGAnimatedRect -> PrimIO DOMRectReadOnly

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal : SVGAnimatedRect -> PrimIO DOMRect

namespace SVGAnimatedString

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal : SVGAnimatedString -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal : SVGAnimatedString -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.baseVal = v}"
  prim__setBaseVal : SVGAnimatedString -> String -> PrimIO ()

namespace SVGAnimatedTransformList

  export
  %foreign "browser:lambda:x=>x.animVal"
  prim__animVal : SVGAnimatedTransformList -> PrimIO SVGTransformList

  export
  %foreign "browser:lambda:x=>x.baseVal"
  prim__baseVal : SVGAnimatedTransformList -> PrimIO SVGTransformList

namespace SVGCircleElement

  export
  %foreign "browser:lambda:x=>x.cx"
  prim__cx : SVGCircleElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.cy"
  prim__cy : SVGCircleElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.r"
  prim__r : SVGCircleElement -> PrimIO SVGAnimatedLength

namespace SVGElement

  export
  %foreign "browser:lambda:x=>x.className"
  prim__className : SVGElement -> PrimIO SVGAnimatedString

  export
  %foreign "browser:lambda:x=>x.ownerSVGElement"
  prim__ownerSVGElement : SVGElement -> PrimIO (Nullable SVGSVGElement)

  export
  %foreign "browser:lambda:x=>x.viewportElement"
  prim__viewportElement : SVGElement -> PrimIO (Nullable SVGElement)

namespace SVGEllipseElement

  export
  %foreign "browser:lambda:x=>x.cx"
  prim__cx : SVGEllipseElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.cy"
  prim__cy : SVGEllipseElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.rx"
  prim__rx : SVGEllipseElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.ry"
  prim__ry : SVGEllipseElement -> PrimIO SVGAnimatedLength

namespace SVGForeignObjectElement

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height : SVGForeignObjectElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width : SVGForeignObjectElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.x"
  prim__x : SVGForeignObjectElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.y"
  prim__y : SVGForeignObjectElement -> PrimIO SVGAnimatedLength

namespace SVGGeometryElement

  export
  %foreign "browser:lambda:x=>x.pathLength"
  prim__pathLength : SVGGeometryElement -> PrimIO SVGAnimatedNumber

  export
  %foreign "browser:lambda:(x,a)=>x.getPointAtLength(a)"
  prim__getPointAtLength : SVGGeometryElement -> Double -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:x=>x.getTotalLength()"
  prim__getTotalLength : SVGGeometryElement -> PrimIO Double

  export
  %foreign "browser:lambda:(x,a)=>x.isPointInFill(a)"
  prim__isPointInFill :  SVGGeometryElement
                      -> UndefOr DOMPointInit
                      -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,a)=>x.isPointInStroke(a)"
  prim__isPointInStroke :  SVGGeometryElement
                        -> UndefOr DOMPointInit
                        -> PrimIO Boolean

namespace SVGGradientElement

  export
  %foreign "browser:lambda:x=>x.gradientTransform"
  prim__gradientTransform :  SVGGradientElement
                          -> PrimIO SVGAnimatedTransformList

  export
  %foreign "browser:lambda:x=>x.gradientUnits"
  prim__gradientUnits : SVGGradientElement -> PrimIO SVGAnimatedEnumeration

  export
  %foreign "browser:lambda:x=>x.spreadMethod"
  prim__spreadMethod : SVGGradientElement -> PrimIO SVGAnimatedEnumeration

namespace SVGGraphicsElement

  export
  %foreign "browser:lambda:x=>x.transform"
  prim__transform : SVGGraphicsElement -> PrimIO SVGAnimatedTransformList

  export
  %foreign "browser:lambda:(x,a)=>x.getBBox(a)"
  prim__getBBox :  SVGGraphicsElement
                -> UndefOr SVGBoundingBoxOptions
                -> PrimIO DOMRect

  export
  %foreign "browser:lambda:x=>x.getCTM()"
  prim__getCTM : SVGGraphicsElement -> PrimIO (Nullable DOMMatrix)

  export
  %foreign "browser:lambda:x=>x.getScreenCTM()"
  prim__getScreenCTM : SVGGraphicsElement -> PrimIO (Nullable DOMMatrix)

namespace SVGImageElement

  export
  %foreign "browser:lambda:x=>x.crossOrigin"
  prim__crossOrigin : SVGImageElement -> PrimIO (Nullable String)

  export
  %foreign "browser:lambda:(x,v)=>{x.crossOrigin = v}"
  prim__setCrossOrigin : SVGImageElement -> Nullable String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height : SVGImageElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.preserveAspectRatio"
  prim__preserveAspectRatio :  SVGImageElement
                            -> PrimIO SVGAnimatedPreserveAspectRatio

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width : SVGImageElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.x"
  prim__x : SVGImageElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.y"
  prim__y : SVGImageElement -> PrimIO SVGAnimatedLength

namespace SVGLength

  export
  %foreign "browser:lambda:x=>x.unitType"
  prim__unitType : SVGLength -> PrimIO Bits16

  export
  %foreign "browser:lambda:x=>x.value"
  prim__value : SVGLength -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.value = v}"
  prim__setValue : SVGLength -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.valueAsString"
  prim__valueAsString : SVGLength -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.valueAsString = v}"
  prim__setValueAsString : SVGLength -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.valueInSpecifiedUnits"
  prim__valueInSpecifiedUnits : SVGLength -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.valueInSpecifiedUnits = v}"
  prim__setValueInSpecifiedUnits : SVGLength -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.convertToSpecifiedUnits(a)"
  prim__convertToSpecifiedUnits : SVGLength -> Bits16 -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.newValueSpecifiedUnits(a,b)"
  prim__newValueSpecifiedUnits : SVGLength -> Bits16 -> Double -> PrimIO ()

namespace SVGLengthList

  export
  %foreign "browser:lambda:(o,x,v)=>o[x] = v"
  prim__set : SVGLengthList -> Bits32 -> SVGLength -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : SVGLengthList -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.numberOfItems"
  prim__numberOfItems : SVGLengthList -> PrimIO Bits32

  export
  %foreign "browser:lambda:(x,a)=>x.appendItem(a)"
  prim__appendItem : SVGLengthList -> SVGLength -> PrimIO SVGLength

  export
  %foreign "browser:lambda:x=>x.clear()"
  prim__clear : SVGLengthList -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.getItem(a)"
  prim__getItem : SVGLengthList -> Bits32 -> PrimIO SVGLength

  export
  %foreign "browser:lambda:(x,a)=>x.initialize(a)"
  prim__initialize : SVGLengthList -> SVGLength -> PrimIO SVGLength

  export
  %foreign "browser:lambda:(x,a,b)=>x.insertItemBefore(a,b)"
  prim__insertItemBefore :  SVGLengthList
                         -> SVGLength
                         -> Bits32
                         -> PrimIO SVGLength

  export
  %foreign "browser:lambda:(x,a)=>x.removeItem(a)"
  prim__removeItem : SVGLengthList -> Bits32 -> PrimIO SVGLength

  export
  %foreign "browser:lambda:(x,a,b)=>x.replaceItem(a,b)"
  prim__replaceItem : SVGLengthList -> SVGLength -> Bits32 -> PrimIO SVGLength

namespace SVGLineElement

  export
  %foreign "browser:lambda:x=>x.x1"
  prim__x1 : SVGLineElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.x2"
  prim__x2 : SVGLineElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.y1"
  prim__y1 : SVGLineElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.y2"
  prim__y2 : SVGLineElement -> PrimIO SVGAnimatedLength

namespace SVGLinearGradientElement

  export
  %foreign "browser:lambda:x=>x.x1"
  prim__x1 : SVGLinearGradientElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.x2"
  prim__x2 : SVGLinearGradientElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.y1"
  prim__y1 : SVGLinearGradientElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.y2"
  prim__y2 : SVGLinearGradientElement -> PrimIO SVGAnimatedLength

namespace SVGMarkerElement

  export
  %foreign "browser:lambda:x=>x.markerHeight"
  prim__markerHeight : SVGMarkerElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.markerUnits"
  prim__markerUnits : SVGMarkerElement -> PrimIO SVGAnimatedEnumeration

  export
  %foreign "browser:lambda:x=>x.markerWidth"
  prim__markerWidth : SVGMarkerElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.orient"
  prim__orient : SVGMarkerElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.orient = v}"
  prim__setOrient : SVGMarkerElement -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.orientAngle"
  prim__orientAngle : SVGMarkerElement -> PrimIO SVGAnimatedAngle

  export
  %foreign "browser:lambda:x=>x.orientType"
  prim__orientType : SVGMarkerElement -> PrimIO SVGAnimatedEnumeration

  export
  %foreign "browser:lambda:x=>x.refX"
  prim__refX : SVGMarkerElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.refY"
  prim__refY : SVGMarkerElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:(x,a)=>x.setOrientToAngle(a)"
  prim__setOrientToAngle : SVGMarkerElement -> SVGAngle -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.setOrientToAuto()"
  prim__setOrientToAuto : SVGMarkerElement -> PrimIO ()

namespace SVGNumber

  export
  %foreign "browser:lambda:x=>x.value"
  prim__value : SVGNumber -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.value = v}"
  prim__setValue : SVGNumber -> Double -> PrimIO ()

namespace SVGNumberList

  export
  %foreign "browser:lambda:(o,x,v)=>o[x] = v"
  prim__set : SVGNumberList -> Bits32 -> SVGNumber -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : SVGNumberList -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.numberOfItems"
  prim__numberOfItems : SVGNumberList -> PrimIO Bits32

  export
  %foreign "browser:lambda:(x,a)=>x.appendItem(a)"
  prim__appendItem : SVGNumberList -> SVGNumber -> PrimIO SVGNumber

  export
  %foreign "browser:lambda:x=>x.clear()"
  prim__clear : SVGNumberList -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.getItem(a)"
  prim__getItem : SVGNumberList -> Bits32 -> PrimIO SVGNumber

  export
  %foreign "browser:lambda:(x,a)=>x.initialize(a)"
  prim__initialize : SVGNumberList -> SVGNumber -> PrimIO SVGNumber

  export
  %foreign "browser:lambda:(x,a,b)=>x.insertItemBefore(a,b)"
  prim__insertItemBefore :  SVGNumberList
                         -> SVGNumber
                         -> Bits32
                         -> PrimIO SVGNumber

  export
  %foreign "browser:lambda:(x,a)=>x.removeItem(a)"
  prim__removeItem : SVGNumberList -> Bits32 -> PrimIO SVGNumber

  export
  %foreign "browser:lambda:(x,a,b)=>x.replaceItem(a,b)"
  prim__replaceItem : SVGNumberList -> SVGNumber -> Bits32 -> PrimIO SVGNumber

namespace SVGPatternElement

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height : SVGPatternElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.patternContentUnits"
  prim__patternContentUnits : SVGPatternElement -> PrimIO SVGAnimatedEnumeration

  export
  %foreign "browser:lambda:x=>x.patternTransform"
  prim__patternTransform : SVGPatternElement -> PrimIO SVGAnimatedTransformList

  export
  %foreign "browser:lambda:x=>x.patternUnits"
  prim__patternUnits : SVGPatternElement -> PrimIO SVGAnimatedEnumeration

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width : SVGPatternElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.x"
  prim__x : SVGPatternElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.y"
  prim__y : SVGPatternElement -> PrimIO SVGAnimatedLength

namespace SVGPointList

  export
  %foreign "browser:lambda:(o,x,v)=>o[x] = v"
  prim__set : SVGPointList -> Bits32 -> DOMPoint -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : SVGPointList -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.numberOfItems"
  prim__numberOfItems : SVGPointList -> PrimIO Bits32

  export
  %foreign "browser:lambda:(x,a)=>x.appendItem(a)"
  prim__appendItem : SVGPointList -> DOMPoint -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:x=>x.clear()"
  prim__clear : SVGPointList -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.getItem(a)"
  prim__getItem : SVGPointList -> Bits32 -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:(x,a)=>x.initialize(a)"
  prim__initialize : SVGPointList -> DOMPoint -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:(x,a,b)=>x.insertItemBefore(a,b)"
  prim__insertItemBefore : SVGPointList -> DOMPoint -> Bits32 -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:(x,a)=>x.removeItem(a)"
  prim__removeItem : SVGPointList -> Bits32 -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:(x,a,b)=>x.replaceItem(a,b)"
  prim__replaceItem : SVGPointList -> DOMPoint -> Bits32 -> PrimIO DOMPoint

namespace SVGPreserveAspectRatio

  export
  %foreign "browser:lambda:x=>x.align"
  prim__align : SVGPreserveAspectRatio -> PrimIO Bits16

  export
  %foreign "browser:lambda:(x,v)=>{x.align = v}"
  prim__setAlign : SVGPreserveAspectRatio -> Bits16 -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.meetOrSlice"
  prim__meetOrSlice : SVGPreserveAspectRatio -> PrimIO Bits16

  export
  %foreign "browser:lambda:(x,v)=>{x.meetOrSlice = v}"
  prim__setMeetOrSlice : SVGPreserveAspectRatio -> Bits16 -> PrimIO ()

namespace SVGRadialGradientElement

  export
  %foreign "browser:lambda:x=>x.cx"
  prim__cx : SVGRadialGradientElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.cy"
  prim__cy : SVGRadialGradientElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.fr"
  prim__fr : SVGRadialGradientElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.fx"
  prim__fx : SVGRadialGradientElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.fy"
  prim__fy : SVGRadialGradientElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.r"
  prim__r : SVGRadialGradientElement -> PrimIO SVGAnimatedLength

namespace SVGRectElement

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height : SVGRectElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.rx"
  prim__rx : SVGRectElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.ry"
  prim__ry : SVGRectElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width : SVGRectElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.x"
  prim__x : SVGRectElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.y"
  prim__y : SVGRectElement -> PrimIO SVGAnimatedLength

namespace SVGSVGElement

  export
  %foreign "browser:lambda:x=>x.currentScale"
  prim__currentScale : SVGSVGElement -> PrimIO Double

  export
  %foreign "browser:lambda:(x,v)=>{x.currentScale = v}"
  prim__setCurrentScale : SVGSVGElement -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.currentTranslate"
  prim__currentTranslate : SVGSVGElement -> PrimIO DOMPointReadOnly

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height : SVGSVGElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width : SVGSVGElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.x"
  prim__x : SVGSVGElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.y"
  prim__y : SVGSVGElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:(x,a,b)=>x.checkEnclosure(a,b)"
  prim__checkEnclosure :  SVGSVGElement
                       -> SVGElement
                       -> DOMRectReadOnly
                       -> PrimIO Boolean

  export
  %foreign "browser:lambda:(x,a,b)=>x.checkIntersection(a,b)"
  prim__checkIntersection :  SVGSVGElement
                          -> SVGElement
                          -> DOMRectReadOnly
                          -> PrimIO Boolean

  export
  %foreign "browser:lambda:x=>x.createSVGAngle()"
  prim__createSVGAngle : SVGSVGElement -> PrimIO SVGAngle

  export
  %foreign "browser:lambda:x=>x.createSVGLength()"
  prim__createSVGLength : SVGSVGElement -> PrimIO SVGLength

  export
  %foreign "browser:lambda:x=>x.createSVGMatrix()"
  prim__createSVGMatrix : SVGSVGElement -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:x=>x.createSVGNumber()"
  prim__createSVGNumber : SVGSVGElement -> PrimIO SVGNumber

  export
  %foreign "browser:lambda:x=>x.createSVGPoint()"
  prim__createSVGPoint : SVGSVGElement -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:x=>x.createSVGRect()"
  prim__createSVGRect : SVGSVGElement -> PrimIO DOMRect

  export
  %foreign "browser:lambda:(x,a)=>x.createSVGTransformFromMatrix(a)"
  prim__createSVGTransformFromMatrix :  SVGSVGElement
                                     -> UndefOr DOMMatrix2DInit
                                     -> PrimIO SVGTransform

  export
  %foreign "browser:lambda:x=>x.createSVGTransform()"
  prim__createSVGTransform : SVGSVGElement -> PrimIO SVGTransform

  export
  %foreign "browser:lambda:x=>x.deselectAll()"
  prim__deselectAll : SVGSVGElement -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.forceRedraw()"
  prim__forceRedraw : SVGSVGElement -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.getElementById(a)"
  prim__getElementById : SVGSVGElement -> String -> PrimIO Element

  export
  %foreign "browser:lambda:(x,a,b)=>x.getEnclosureList(a,b)"
  prim__getEnclosureList :  SVGSVGElement
                         -> DOMRectReadOnly
                         -> Nullable SVGElement
                         -> PrimIO NodeList

  export
  %foreign "browser:lambda:(x,a,b)=>x.getIntersectionList(a,b)"
  prim__getIntersectionList :  SVGSVGElement
                            -> DOMRectReadOnly
                            -> Nullable SVGElement
                            -> PrimIO NodeList

  export
  %foreign "browser:lambda:(x,a)=>x.suspendRedraw(a)"
  prim__suspendRedraw : SVGSVGElement -> Bits32 -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.unsuspendRedrawAll()"
  prim__unsuspendRedrawAll : SVGSVGElement -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.unsuspendRedraw(a)"
  prim__unsuspendRedraw : SVGSVGElement -> Bits32 -> PrimIO ()

namespace SVGScriptElement

  export
  %foreign "browser:lambda:x=>x.crossOrigin"
  prim__crossOrigin : SVGScriptElement -> PrimIO (Nullable String)

  export
  %foreign "browser:lambda:(x,v)=>{x.crossOrigin = v}"
  prim__setCrossOrigin : SVGScriptElement -> Nullable String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : SVGScriptElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.type = v}"
  prim__setType : SVGScriptElement -> String -> PrimIO ()

namespace SVGStopElement

  export
  %foreign "browser:lambda:x=>x.offset"
  prim__offset : SVGStopElement -> PrimIO SVGAnimatedNumber

namespace SVGStringList

  export
  %foreign "browser:lambda:(o,x,v)=>o[x] = v"
  prim__set : SVGStringList -> Bits32 -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : SVGStringList -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.numberOfItems"
  prim__numberOfItems : SVGStringList -> PrimIO Bits32

  export
  %foreign "browser:lambda:(x,a)=>x.appendItem(a)"
  prim__appendItem : SVGStringList -> String -> PrimIO String

  export
  %foreign "browser:lambda:x=>x.clear()"
  prim__clear : SVGStringList -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.getItem(a)"
  prim__getItem : SVGStringList -> Bits32 -> PrimIO String

  export
  %foreign "browser:lambda:(x,a)=>x.initialize(a)"
  prim__initialize : SVGStringList -> String -> PrimIO String

  export
  %foreign "browser:lambda:(x,a,b)=>x.insertItemBefore(a,b)"
  prim__insertItemBefore : SVGStringList -> String -> Bits32 -> PrimIO String

  export
  %foreign "browser:lambda:(x,a)=>x.removeItem(a)"
  prim__removeItem : SVGStringList -> Bits32 -> PrimIO String

  export
  %foreign "browser:lambda:(x,a,b)=>x.replaceItem(a,b)"
  prim__replaceItem : SVGStringList -> String -> Bits32 -> PrimIO String

namespace SVGStyleElement

  export
  %foreign "browser:lambda:x=>x.media"
  prim__media : SVGStyleElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.media = v}"
  prim__setMedia : SVGStyleElement -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.title"
  prim__title : SVGStyleElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.title = v}"
  prim__setTitle : SVGStyleElement -> String -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : SVGStyleElement -> PrimIO String

  export
  %foreign "browser:lambda:(x,v)=>{x.type = v}"
  prim__setType : SVGStyleElement -> String -> PrimIO ()

namespace SVGTextContentElement

  export
  %foreign "browser:lambda:x=>x.lengthAdjust"
  prim__lengthAdjust : SVGTextContentElement -> PrimIO SVGAnimatedEnumeration

  export
  %foreign "browser:lambda:x=>x.textLength"
  prim__textLength : SVGTextContentElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:(x,a)=>x.getCharNumAtPosition(a)"
  prim__getCharNumAtPosition :  SVGTextContentElement
                             -> UndefOr DOMPointInit
                             -> PrimIO Int32

  export
  %foreign "browser:lambda:x=>x.getComputedTextLength()"
  prim__getComputedTextLength : SVGTextContentElement -> PrimIO Double

  export
  %foreign "browser:lambda:(x,a)=>x.getEndPositionOfChar(a)"
  prim__getEndPositionOfChar :  SVGTextContentElement
                             -> Bits32
                             -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:(x,a)=>x.getExtentOfChar(a)"
  prim__getExtentOfChar : SVGTextContentElement -> Bits32 -> PrimIO DOMRect

  export
  %foreign "browser:lambda:x=>x.getNumberOfChars()"
  prim__getNumberOfChars : SVGTextContentElement -> PrimIO Int32

  export
  %foreign "browser:lambda:(x,a)=>x.getRotationOfChar(a)"
  prim__getRotationOfChar : SVGTextContentElement -> Bits32 -> PrimIO Double

  export
  %foreign "browser:lambda:(x,a)=>x.getStartPositionOfChar(a)"
  prim__getStartPositionOfChar :  SVGTextContentElement
                               -> Bits32
                               -> PrimIO DOMPoint

  export
  %foreign "browser:lambda:(x,a,b)=>x.getSubStringLength(a,b)"
  prim__getSubStringLength :  SVGTextContentElement
                           -> Bits32
                           -> Bits32
                           -> PrimIO Double

  export
  %foreign "browser:lambda:(x,a,b)=>x.selectSubString(a,b)"
  prim__selectSubString : SVGTextContentElement -> Bits32 -> Bits32 -> PrimIO ()

namespace SVGTextPathElement

  export
  %foreign "browser:lambda:x=>x.method"
  prim__method : SVGTextPathElement -> PrimIO SVGAnimatedEnumeration

  export
  %foreign "browser:lambda:x=>x.spacing"
  prim__spacing : SVGTextPathElement -> PrimIO SVGAnimatedEnumeration

  export
  %foreign "browser:lambda:x=>x.startOffset"
  prim__startOffset : SVGTextPathElement -> PrimIO SVGAnimatedLength

namespace SVGTextPositioningElement

  export
  %foreign "browser:lambda:x=>x.dx"
  prim__dx : SVGTextPositioningElement -> PrimIO SVGAnimatedLengthList

  export
  %foreign "browser:lambda:x=>x.dy"
  prim__dy : SVGTextPositioningElement -> PrimIO SVGAnimatedLengthList

  export
  %foreign "browser:lambda:x=>x.rotate"
  prim__rotate : SVGTextPositioningElement -> PrimIO SVGAnimatedNumberList

  export
  %foreign "browser:lambda:x=>x.x"
  prim__x : SVGTextPositioningElement -> PrimIO SVGAnimatedLengthList

  export
  %foreign "browser:lambda:x=>x.y"
  prim__y : SVGTextPositioningElement -> PrimIO SVGAnimatedLengthList

namespace SVGTransform

  export
  %foreign "browser:lambda:x=>x.angle"
  prim__angle : SVGTransform -> PrimIO Double

  export
  %foreign "browser:lambda:x=>x.matrix"
  prim__matrix : SVGTransform -> PrimIO DOMMatrix

  export
  %foreign "browser:lambda:x=>x.type"
  prim__type : SVGTransform -> PrimIO Bits16

  export
  %foreign "browser:lambda:(x,a)=>x.setMatrix(a)"
  prim__setMatrix : SVGTransform -> UndefOr DOMMatrix2DInit -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b,c)=>x.setRotate(a,b,c)"
  prim__setRotate : SVGTransform -> Double -> Double -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.setScale(a,b)"
  prim__setScale : SVGTransform -> Double -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.setSkewX(a)"
  prim__setSkewX : SVGTransform -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a)=>x.setSkewY(a)"
  prim__setSkewY : SVGTransform -> Double -> PrimIO ()

  export
  %foreign "browser:lambda:(x,a,b)=>x.setTranslate(a,b)"
  prim__setTranslate : SVGTransform -> Double -> Double -> PrimIO ()

namespace SVGTransformList

  export
  %foreign "browser:lambda:(o,x,v)=>o[x] = v"
  prim__set : SVGTransformList -> Bits32 -> SVGTransform -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.length"
  prim__length : SVGTransformList -> PrimIO Bits32

  export
  %foreign "browser:lambda:x=>x.numberOfItems"
  prim__numberOfItems : SVGTransformList -> PrimIO Bits32

  export
  %foreign "browser:lambda:(x,a)=>x.appendItem(a)"
  prim__appendItem : SVGTransformList -> SVGTransform -> PrimIO SVGTransform

  export
  %foreign "browser:lambda:x=>x.clear()"
  prim__clear : SVGTransformList -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.consolidate()"
  prim__consolidate : SVGTransformList -> PrimIO (Nullable SVGTransform)

  export
  %foreign "browser:lambda:(x,a)=>x.createSVGTransformFromMatrix(a)"
  prim__createSVGTransformFromMatrix :  SVGTransformList
                                     -> UndefOr DOMMatrix2DInit
                                     -> PrimIO SVGTransform

  export
  %foreign "browser:lambda:(x,a)=>x.getItem(a)"
  prim__getItem : SVGTransformList -> Bits32 -> PrimIO SVGTransform

  export
  %foreign "browser:lambda:(x,a)=>x.initialize(a)"
  prim__initialize : SVGTransformList -> SVGTransform -> PrimIO SVGTransform

  export
  %foreign "browser:lambda:(x,a,b)=>x.insertItemBefore(a,b)"
  prim__insertItemBefore :  SVGTransformList
                         -> SVGTransform
                         -> Bits32
                         -> PrimIO SVGTransform

  export
  %foreign "browser:lambda:(x,a)=>x.removeItem(a)"
  prim__removeItem : SVGTransformList -> Bits32 -> PrimIO SVGTransform

  export
  %foreign "browser:lambda:(x,a,b)=>x.replaceItem(a,b)"
  prim__replaceItem :  SVGTransformList
                    -> SVGTransform
                    -> Bits32
                    -> PrimIO SVGTransform

namespace SVGUseElement

  export
  %foreign "browser:lambda:x=>x.animatedInstanceRoot"
  prim__animatedInstanceRoot : SVGUseElement -> PrimIO (Nullable SVGElement)

  export
  %foreign "browser:lambda:x=>x.height"
  prim__height : SVGUseElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.instanceRoot"
  prim__instanceRoot : SVGUseElement -> PrimIO (Nullable SVGElement)

  export
  %foreign "browser:lambda:x=>x.width"
  prim__width : SVGUseElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.x"
  prim__x : SVGUseElement -> PrimIO SVGAnimatedLength

  export
  %foreign "browser:lambda:x=>x.y"
  prim__y : SVGUseElement -> PrimIO SVGAnimatedLength

namespace ShadowAnimation

  export
  %foreign "browser:lambda:(a,b)=> new ShadowAnimation(a,b)"
  prim__new : Animation -> Animatable -> PrimIO ShadowAnimation

  export
  %foreign "browser:lambda:x=>x.sourceAnimation"
  prim__sourceAnimation : ShadowAnimation -> PrimIO Animation

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

namespace GetSVGDocument

  export
  %foreign "browser:lambda:x=>x.getSVGDocument()"
  prim__getSVGDocument : GetSVGDocument -> PrimIO Document

namespace SVGAnimatedPoints

  export
  %foreign "browser:lambda:x=>x.animatedPoints"
  prim__animatedPoints : SVGAnimatedPoints -> PrimIO SVGPointList

  export
  %foreign "browser:lambda:x=>x.points"
  prim__points : SVGAnimatedPoints -> PrimIO SVGPointList

namespace SVGElementInstance

  export
  %foreign "browser:lambda:x=>x.correspondingElement"
  prim__correspondingElement :  SVGElementInstance
                             -> PrimIO (Nullable SVGElement)

  export
  %foreign "browser:lambda:x=>x.correspondingUseElement"
  prim__correspondingUseElement :  SVGElementInstance
                                -> PrimIO (Nullable SVGUseElement)

namespace SVGFitToViewBox

  export
  %foreign "browser:lambda:x=>x.preserveAspectRatio"
  prim__preserveAspectRatio :  SVGFitToViewBox
                            -> PrimIO SVGAnimatedPreserveAspectRatio

  export
  %foreign "browser:lambda:x=>x.viewBox"
  prim__viewBox : SVGFitToViewBox -> PrimIO SVGAnimatedRect

namespace SVGTests

  export
  %foreign "browser:lambda:x=>x.requiredExtensions"
  prim__requiredExtensions : SVGTests -> PrimIO SVGStringList

  export
  %foreign "browser:lambda:x=>x.systemLanguage"
  prim__systemLanguage : SVGTests -> PrimIO SVGStringList

namespace SVGURIReference

  export
  %foreign "browser:lambda:x=>x.href"
  prim__href : SVGURIReference -> PrimIO SVGAnimatedString

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

namespace SVGBoundingBoxOptions

  export
  %foreign "browser:lambda:(a,b,c,d)=> {fill: a,stroke: b,markers: c,clipped: d}"
  prim__new :  UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> UndefOr Boolean
            -> PrimIO SVGBoundingBoxOptions

  export
  %foreign "browser:lambda:x=>x.clipped"
  prim__clipped : SVGBoundingBoxOptions -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.clipped = v}"
  prim__setClipped : SVGBoundingBoxOptions -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.fill"
  prim__fill : SVGBoundingBoxOptions -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.fill = v}"
  prim__setFill : SVGBoundingBoxOptions -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.markers"
  prim__markers : SVGBoundingBoxOptions -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.markers = v}"
  prim__setMarkers : SVGBoundingBoxOptions -> UndefOr Boolean -> PrimIO ()

  export
  %foreign "browser:lambda:x=>x.stroke"
  prim__stroke : SVGBoundingBoxOptions -> PrimIO (UndefOr Boolean)

  export
  %foreign "browser:lambda:(x,v)=>{x.stroke = v}"
  prim__setStroke : SVGBoundingBoxOptions -> UndefOr Boolean -> PrimIO ()


text:
||| Command-line options when starting up game server
module Bautzen.Options

import Network.Socket.Data

import Data.Strings.Extra

public export
data RunMode : Type where
  ClientMode : RunMode
  ServerMode : RunMode

public export
record Options where
  constructor MkOptions
  ||| The port to listen on for incoming connections
  ||| Can be 0 in which case the server listens on a random port
  port : Port

  ||| The host to bind server to
  ||| defaults to `localhost` which will only allow local connections
  host : String

  ||| The mode this instance runs in, either client or server
  ||| default mode is `ServerMode`
  runMode : RunMode

export
defaultOptions : Options
defaultOptions = MkOptions 34567 "localhost" ServerMode

doProcessOptions : List String -> Options -> Either String Options
doProcessOptions []                        opts = Right opts
doProcessOptions ("--host" :: arg :: args) opts =
  doProcessOptions args (record { host = arg } opts)
doProcessOptions ("--port" :: arg :: args) opts =
  case parseInteger (unpack arg) 0 of
    Nothing => Left $ "cannot parse " ++ arg ++ " as a port number"
    (Just x) => doProcessOptions args (record { port = fromInteger x } opts)
doProcessOptions ("client" :: args) opts =
  doProcessOptions args (record { runMode = ClientMode } opts)
doProcessOptions ("server" :: args) opts =
  doProcessOptions args (record { runMode = ServerMode } opts)
doProcessOptions (arg :: _) _ = Left $ "unknown argument " ++ arg

||| Process arguments from the command-line, turning them into
||| `Options`.
|||
||| Returns a `Left` if there's an error in the processing, or
||| a `Right` with the `Options` data filled in.
export
processOptions : List String -> Either String Options
processOptions args = doProcessOptions args defaultOptions

namespace OptionsTest

  can_parse_port_option :
    doProcessOptions [ "--port" , "123" ] Options.defaultOptions = Right (MkOptions 123 "localhost" ServerMode)
  can_parse_port_option = Refl

  can_parse_host_option :
    doProcessOptions [ "--host" , "foo" ] Options.defaultOptions = Right (MkOptions 34567 "foo" ServerMode)
  can_parse_host_option = Refl

  can_parse_run_mode_option :
    doProcessOptions [ "client" ] Options.defaultOptions = Right (MkOptions 34567 "localhost" ClientMode )
  can_parse_run_mode_option = Refl

  can_parse_client_mode_with_host_port :
    doProcessOptions [ "client" ,  "--host" , "foo",  "--port" , "123"  ] Options.defaultOptions
      = Right (MkOptions 123 "foo" ClientMode )
  can_parse_client_mode_with_host_port= Refl

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Maps

import Logic
import IndProp

%access public export

%default total

data Id : Type where
  MkId : String -> Id

beq_id : (x1, x2 : Id) -> Bool
beq_id (MkId x) (MkId y) = decAsBool $ decEq x y

mkIdInjective : MkId x = MkId y -> x = y
mkIdInjective Refl = Refl

implementation DecEq Id where
  decEq (MkId x) (MkId y) with (decEq x y)
    decEq _ _ | Yes prf = Yes $ cong {f=MkId} prf
    decEq _ _ | No contra = No $ \prf => contra $ mkIdInjective prf

beq_id_refl : (x : Id) -> True = beq_id x x
beq_id_refl (MkId x) with (decEq x x)
  beq_id_refl _ | Yes _ = Refl
  beq_id_refl _ | No contra = absurd $ contra Refl

beq_id_true_iff : (beq_id x y = True) ↔ x = y
beq_id_true_iff = (forward, backward)
where forward : beq_id x y = True -> x = y
      forward {x = (MkId x)} {y = (MkId y)} prf with (decEq x y)
        forward Refl | Yes eq = cong {f=MkId} eq
        forward Refl | No _ impossible
      backward : x = y -> beq_id x y = True
      backward {x = (MkId x)} {y = (MkId y)} prf with (decEq x y)
        backward Refl | Yes _ = Refl
        backward prf | No contra = absurd . contra $ mkIdInjective prf

beq_id_false_iff : (beq_id x y = False) ↔ Not (x = y)
beq_id_false_iff = (forward, backward)
where forward : beq_id x y = False -> Not (x = y)
      forward prf = (snd not_true_iff_false) prf . (snd beq_id_true_iff)
      backward : Not (x = y) -> beq_id x y = False
      backward not_eq = (fst not_true_iff_false) $ not_eq . (fst beq_id_true_iff)

beq_id_x_y_eq_beq_id_y_x : beq_id x y = beq_id y x
beq_id_x_y_eq_beq_id_y_x {x} {y} = case decEq x y of
  Yes prf => rewrite prf in Refl
  No contra => rewrite (snd beq_id_false_iff) contra
               in case decEq y x of
                    Yes prf => void . contra $ sym prf
                    No contra => rewrite (snd beq_id_false_iff) contra
                                 in Refl

TotalMap : Type -> Type
TotalMap a = Id -> a

t_empty : (v : a) -> TotalMap a
t_empty = const

t_update : (x : Id) -> (v : a) -> (m : TotalMap a) -> TotalMap a
t_update x v m = \y => if beq_id x y then v else m y

t_update_eq : (t_update x v m) x = v
t_update_eq {x} = rewrite sym $ beq_id_refl x in Refl

t_update_neq : Not (x = y) -> (t_update x v m) y = m y
t_update_neq not_eq = rewrite (snd beq_id_false_iff) not_eq
                      in Refl

function_extensionality : ((x : t) -> f x = g x) -> f = g
function_extensionality = really_believe_me

t_update_shadow : t_update x v2 $ t_update x v1 m = t_update x v2 m
t_update_shadow {x} = function_extensionality $ \y => case decEq x y of
  Yes prf => rewrite (snd beq_id_true_iff) prf in Refl
  No contra => rewrite (snd beq_id_false_iff) contra in Refl

beq_idP : {x, y : Id} -> Reflect (x = y) (beq_id x y)
beq_idP = iff_reflect $ iff_sym $ beq_id_true_iff

t_update_same : t_update x (m x) m = m
t_update_same {x} = function_extensionality $ \y => case decEq x y of
  Yes prf => rewrite (snd beq_id_true_iff) prf in cong prf
  No contra => rewrite (snd beq_id_false_iff) contra in Refl

t_update_permute : Not (x2 = x1) -> t_update x1 v1 $ t_update x2 v2 m
                                  = t_update x2 v2 $ t_update x1 v1 m
t_update_permute {x1} {x2} x2_neq_x1 = function_extensionality $ \y =>
  case decEq x1 y of
    Yes x1_eq_y => rewrite (snd beq_id_true_iff) x1_eq_y
                   in rewrite sym x1_eq_y
                   in rewrite (snd beq_id_false_iff) x2_neq_x1
                   in Refl
    No x1_neq_y => rewrite (snd beq_id_false_iff) x1_neq_y
                   in Refl

PartialMap : Type -> Type
PartialMap a = TotalMap (Maybe a)

empty : PartialMap a
empty = t_empty Nothing

update : (x : Id) -> (v : a) -> (m : PartialMap a) -> PartialMap a
update x v m = t_update x (Just v) m

apply_empty : empty {a} x = Nothing {a}
apply_empty = Refl

update_eq : (update x v m) x = Just v
update_eq {v} = t_update_eq {v=Just v}

update_neq : Not (x2 = x1) -> (update x2 v m) x1 = m x1
update_neq {x1} {x2} {v} = t_update_neq {x=x2} {y=x1} {v=Just v}

update_shadow : update x v2 $ update x v1 m = update x v2 m
update_shadow {v1} {v2} = t_update_shadow {v1=Just v1} {v2=Just v2}

update_same : m x = Just v -> update x v m = m
update_same prf = rewrite sym prf in t_update_same

update_permute : Not (x2 = x1) -> update x1 v1 $ update x2 v2 m
                                = update x2 v2 $ update x1 v1 m
update_permute {v1} {v2} = t_update_permute {v1=Just v1} {v2=Just v2}


text:
module QFT

import Data.Nat
import Data.Vect
import Decidable.Equality
import Unitary
import Injection
import Lemmas

%default total

|||Quantum circuit for the Quantum Fourier Transform

--CONTROLLED PHASE GATES FOR THE QFT

||| Phase gate with phase 2 pi / (2^m)
Rm : Nat -> Unitary 1
Rm m = PGate (2 * pi / (pow 2 (cast m)))

||| Controlled phase gate with phase 2 pi / (2^m)
cRm : Nat -> Unitary 2
cRm m = controlled (Rm m)

--A FEW LEMMAS FOR THE QFT

kLTSucc1 : (k : Nat) -> k < (k + 1) = True
kLTSucc1 0 = Refl
kLTSucc1 (S k) = kLTSucc1 k

lemmaInj1 : (k : Nat) -> isInjective (S (k + 1)) [S k, 0] = True
lemmaInj1 k =
  let p1 = kLTSucc1 k
  in lemmaAnd (lemmaAnd p1 Refl) Refl

--QFT

||| Auxiliary function for QFT : builds the recursive pattern
|||
||| n -- number of qubits
export
qftRec : (n : Nat) -> Unitary n
qftRec 0 = IdGate
qftRec 1 = HGate
qftRec (S (S k)) =
  let t1 = (qftRec (S k)) # IdGate
  in rewrite sym $ lemmaplusOneRight k in apply (cRm (S k)) t1 [S k, 0] {prf = lemmaInj1 k}

||| QFT unitary circuit for n qubits
|||
||| n -- number of qubits
export
qft : (n : Nat) -> Unitary n
qft 0 = IdGate
qft (S k) =
  let g = qftRec (S k)
      h = (IdGate {n = 1}) # (qft k)
  in h . g

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
module Main

main : IO ()
main = putStr "Hello world\n"

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Test.Parser

import Data.List
import Text.Show.Pretty
import Test.Mini
import Text.Lexer

--------------------------------------------------------------------------------
--          String Tokens
--------------------------------------------------------------------------------

nats : List String
nats = ["0","123","0xabc123","0b11011","0o77653", "0XAFC123"]

strings : List String
strings = map show ["0 foo","x y z", "    ", "\t\t"]

chars : List String
chars = map show ['a','z','A','Z','0','9','\t','ä','ü']

spaceStrs : List String
spaceStrs = ["   ","\r\n","\n","\t\t \n"]

ops : List String
ops = [">>=", "+", "-", ">=", ">", "<", "::", "::="]

idents : List String
idents = ["idents", "nat_token", "Nat_Token", "foo_bar__", "_any123"]

identOrOps : List String
identOrOps = idents ++ map (\o => "(" ++ o ++ ")") ops

symbols : List String
symbols = ["(",")","[","]","{","}",",","="]

doubles : List String
doubles = ["1.234", "12.0e-2", "0.334E+10", "0.1234E10"]

--------------------------------------------------------------------------------
--          Lexing
--------------------------------------------------------------------------------

testLex : String -> List (String, List ShowToken) -> IO Bool
testLex s ps = do putStrLn ("Lexing " ++ s)
                  report $ runEq lex_ (map (map Right) ps)

natTokens : List (String,List ShowToken)
natTokens = map (\s => (s, [NatLit s])) nats

stringTokens : List (String,List ShowToken)
stringTokens = map (\s => (s, [StringLit s])) strings

charTokens : List (String,List ShowToken)
charTokens = map (\s => (s, [CharLit s])) chars

doubleTokens : List (String,List ShowToken)
doubleTokens = map (\s => (s, [DblLit s])) doubles

spaceTokens : List (String,List ShowToken)
spaceTokens = map (\s => (s, [])) spaceStrs

identTokens : List (String,List ShowToken)
identTokens = map (\s => (s, [Ident s])) idents

opTokens : List (String,List ShowToken)
opTokens = map (\s => (s, [Op s])) ops

symbolTokens : List (String,List ShowToken)
symbolTokens = map (\s => (s, [Symbol s])) symbols

export
lexTest : IO Bool
lexTest = testAll [ testLex "nat literals" natTokens
                  , testLex "string literals" stringTokens
                  , testLex "char literals" charTokens
                  , testLex "float literals" doubleTokens
                  , testLex "spaces" spaceTokens
                  , testLex "identifiers" identTokens
                  , testLex "operators" opTokens
                  , testLex "symbols" symbolTokens
                  ]

--------------------------------------------------------------------------------
--          Parsing
--------------------------------------------------------------------------------

testParse : String -> List (String, Value) -> IO Bool
testParse s ps = do putStrLn ("Parsing " ++ s)
                    report $ runEq parseValueE (map (map Right) ps)

prims : List (String,Value)
prims =  map (\s => (s, Chr s)) chars
      ++ map (\s => (s, Natural s)) nats
      ++ map (\s => (s, Dbl s)) doubles
      ++ map (\s => (s, Str s)) strings
      ++ map (\s => (s, Con (MkName s) [])) identOrOps

negated : List (String,Value)
negated =  map (\s => ("-" ++ s, Neg $ Natural s)) nats
        ++ map (\s => ("-" ++ s, Neg $ Dbl s)) doubles

singleCons : List (String,Value)
singleCons = do (s,v) <- prims
                ident <- identOrOps
                pure ( ident ++ " " ++ s
                     , Con (MkName ident) [v]
                     )

doubleCons : List (String,Value)
doubleCons = do (ps,v)  <- prims
                ident   <- identOrOps
                (cs,sc) <- take 100 singleCons
                pure ( ident ++ " " ++ ps ++ "(" ++ cs ++ ")"
                     , Con (MkName ident) [v,sc]
                     )

emptyRecs : List (String,Value)
emptyRecs = do i <- identOrOps
               pure (i ++ " {}", Rec (MkName i) [])

primsOrCons : List (String,Value)
primsOrCons = prims ++ take 10 singleCons ++ take 20 doubleCons

recs1 : List (String,Value)
recs1 = do (ps,p)  <- primsOrCons
           ident1  <- identOrOps
           ident2  <- identOrOps
           pure  ( concat {t = List} [ ident1, " { "
                                     , ident2, " = ", ps
                                     , " } "
                                     ]
                 , Rec (MkName ident1) [(MkName ident2, p)]
                 )

recs2 : List (String,Value)
recs2 = do (ps,p)  <- take 20 primsOrCons
           ident1  <- take 2 identOrOps
           ident2  <- take 2 identOrOps
           ident3  <- take 2 identOrOps
           (cs,sc) <- take 5 doubleCons
           pure  ( concat {t = List} [ ident1, " { "
                                     , ident2, " = ", ps, ", "
                                     , ident3, " = ", cs
                                     , " } "
                                     ]
                 , Rec (MkName ident1) [ (MkName ident2, p)
                                       , (MkName ident3, sc)
                                       ]
                 )

export
parseTest : IO Bool
parseTest = testAll [ testParse "primities" prims
                    , testParse "negated" negated
                    , testParse "cons arity 1" singleCons
                    , testParse "cons arity 2" doubleCons
                    , testParse "empty records" emptyRecs
                    , testParse "records of arity 1" recs1
                    , testParse "records of arity 2" recs2
                    ]


text:
module Mrk.Tests
import Test.Unit
import Mrk.DSL

%default total

AttributeValue String where
  toAttr = id

fixture : Document Root
fixture = do
  html [] $ do
    head [] $ do
      meta (Charset UTF8) []
      title [] "Best site evah"
      stylesheet "foo.css"

    body [ClassNames ["hi"]] $ do
      ul [] $ do
        li [] $ do
          text "inside"
        li [] $ do
          p [] $ do
            a (Just "/contact") [Rel Nofollow] $ text "Contact"

      div [] $ do
        div [] $ do
          text "Yo"
        h1 [] $ do
          text "Main heading"

        h2 [] $ do
          text "Sub heading"

        h3 [] $ do
          text "Sub heading"

        h4 [] $ do
          text "Sub heading"

        h5 [] $ do
          text "Sub heading"

        h6 [] $ do
          text "Sub heading"

        p [] $ text "some paragraph text"
        img "/someimage.jpg" "another sentence" []

export
main : IO ()
main = runTests tests where
  tests : List (IO Bool)
  tests =
       assertEquals
         (show fixture)
         (
         "<!doctype html>" ++
         "" ++
         "" ++
         "<meta charset=\"utf-8\">" ++
         "<title>Best site evah</title>" ++
         "<link rel=\"stylesheet\" href=\"foo.css\" type=\"text/css\">" ++
         "" ++
         "" ++
         "
" ++
         "
inside
" ++
         "

Contact

" ++
         "
" ++
         "
" ++
         "
Yo
" ++
         "
Main heading
" ++
         "
Sub heading
" ++
         "
Sub heading
" ++
         "
Sub heading
" ++
         "
Sub heading
" ++
         "
Sub heading
" ++
         "
some paragraph text
" ++
         "" ++
         "
" ++
         "" ++
         ""
         )

    :: neutral

-- Local Variables:
-- idris-load-packages: ("contrib")
-- End:

max_stars_repo_name: camelpunch/mrk

max_issues_repo_name: camelpunch/mrk

max_forks_repo_name: camelpunch/mrk


text:
module Postgres.Utility

import System.FFI

public export
libpq : String -> String
libpq fn = "C:" ++ fn ++ ", libpq"

public export
helper : String -> String
helper fn = "C:" ++ fn ++ ", libpg-idris"

export
%foreign helper "string_value"
prim__string_value : Ptr String -> String

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
-- https://blog.cofree.coffee/2020-10-17-bounded-space-automata/

module Store

import Data.Vect
import Data.Fin

interface Comonad (w : Type -> Type) where
  extract : w a -> a
  extend  : (w a -> b) -> w a -> w b

interface Functor f => Representable (f : Type -> Type) (rep : Type) | f where
  tabulate : (rep -> a) -> f a
  index    : f a -> (rep -> a)

{n : Nat} -> Representable (Vect n) (Fin n) where
  tabulate f {n = Z}     = []
  tabulate f {n = (S k)} = f FZ :: tabulate (f . FS)
  index (x :: _) FZ {n = (S k)} = x
  index (_ :: xs) (FS x) {n = (S k)} = index xs x

data Store : (f : Type -> Type) -> (rep : Type) -> (a : Type) -> Type where
  MkStore : rep -> f a -> Store f rep a

pos : Store f r a -> r
pos (MkStore r f) = r

peek : Representable f r => r -> Store f r a -> a
peek r (MkStore _ f) = index f r

peeks : Representable f r => (r -> r) -> Store f r a -> a
peeks g (MkStore r f) = index f (g r)

seek : Representable f r => r -> Store f r a -> Store f r a
seek r (MkStore _ f) = MkStore r f

seeks : Representable f r => (r -> r) -> Store f r a -> Store f r a
seeks g (MkStore r f) = MkStore (g r) f

experiment : (Representable f r, Functor g) => (r -> g r) -> Store f r a -> g a
experiment f s = map (`peek` s) (f (pos s))

Representable f r => Comonad (Store f r) where
  extract (MkStore r f) = index f r
  extend g (MkStore r f) = MkStore r (tabulate (\r' => g (MkStore r' f)))

up : {k : Nat} -> Fin (S k) -> Fin (S k)
up = either (const FZ) FS . strengthen

down : {k : Nat} -> Fin (S k) -> Fin (S k)
down FZ     = last
down (FS k) = weaken k

indices : {k : Nat} -> Fin (3 + k) -> Vect 3 (Fin (3 + k))
indices x = [down x, x, up x]

neighbors : {k : Nat} -> Store (Vect (3 + k)) (Fin (3 + k)) Bool -> Vect 3 Bool
neighbors = experiment indices

max_stars_repo_name: andorp/IdrisExtSTGCodegen

max_issues_repo_name: andorp/IdrisExtSTGCodegen

max_forks_repo_name: andorp/IdrisExtSTGCodegen


text:
module Prelude.Ops

-- Numerical operators
infix 6 ==, /=, <, <=, >, >=
infixl 7 <<, >> -- unused
infixl 8 +, -
infixl 9 *, /

-- Boolean operators
infixr 5 &&
infixr 4 ||

-- List and String operators
infixr 7 ::, ++

-- Functor/Applicative/Monad/Algebra operators
infixl 1 >>=
infixr 2 <|>
infixl 3 <*>, *>, <*
infixr 4 <$>, $>, <$
infixl 6 <+>

-- Utility operators
infixr 9 .
infixr 0 $

infixl 9 `div`, `mod`


text:
module Vending

data DoorState = DoorClosed | DoorOpen

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

namespace DoorCmdDo
  (>>=) : DoorCmd a state1 state2 -> (a -> DoorCmd b state2 state3) -> DoorCmd a state1 state3
  (>>=) = Do1

  Pure: ty -> DoorCmd ty state state
  Pure = Pure1

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

data GuessCmd : Type -> Nat -> Nat -> Type where
  Try : Integer -> GuessCmd Ordering (S g) g
  Pure2 : ty -> GuessCmd ty state state
  BindGuess : GuessCmd a state1 state2 -> (a -> GuessCmd b state2 state3) ->  GuessCmd b state1 state3

namespace GuessCmdDo
  (>>=) : GuessCmd a state1 state2 -> (a -> GuessCmd b state2 state3) ->  GuessCmd b state1 state3
  (>>=) = BindGuess

  Pure : ty -> GuessCmd ty state state
  Pure = Pure2

threeGuess : GuessCmd () 0 0
threeGuess = do Try 10
                Pure ()

VendState : Type
VendState = (Nat, Nat)

data Input = COIN
     | VEND
     | CHANGE
     | REFILL Nat

data MachineCmd : Type ->
                  VendState ->
                  VendState -> Type where
     InsertCoin : MachineCmd () (pounds, chocs) (S pounds, chocs)
     Vend: MachineCmd () (S pounds, S chocs) (pounds, chocs)
     GetCoins : MachineCmd () (pounds, chocs) (Z, chocs)
     Refill : (bars: Nat) -> MachineCmd () (Z, chocs) (Z, bars + chocs)

     Display : String -> MachineCmd () state state
     GetInput : MachineCmd (Maybe Input) state state

     Pure: ty -> MachineCmd ty state state
     (>>=): MachineCmd a state1 state2 -> (a -> MachineCmd b state2 state3) -> MachineCmd a state1 state3

data MachineIO : VendState -> Type where
     Do : MachineCmd a state1 state2 -> (a -> Inf (MachineIO state2)) -> MachineIO state1

namespace MachineDo
  (>>=) : MachineCmd a state1 state2 -> (a -> Inf (MachineIO state2)) -> MachineIO state1
  (>>=) = Do

mutual
  vend: MachineIO (pounds, chocs)
  vend {chocs = Z} = Display "Out of stock" >>= (\_ => machineLoop)

  vend {pounds = Z} = do Display "InsertCoin"
                         machineLoop
  vend {pounds = (S j)} {chocs = (S k)} = do Vend
                                             Display "Enjoy!"
                                             machineLoop

  refill: (num: Nat) -> MachineIO (pounds, chocs)
  refill {pounds = Z} num = do Refill num
                               machineLoop
  refill _ = do Display "Can't refill"
                machineLoop

  machineLoop : MachineIO (pounds, chocs)
  machineLoop =
              do Just x <- GetInput
                      | Nothing => do Display "Invalid Input"
                                      machineLoop
                 case x of
                   COIN => do InsertCoin
                              machineLoop
                   VEND => vend
                   CHANGE => do GetCoins
                                Display "Change returned"
                                machineLoop
                   REFILL num => refill num

max_stars_repo_name: gdevanla/idris-learn

max_issues_repo_name: gdevanla/idris-learn

max_forks_repo_name: gdevanla/idris-learn


text:
module Again

%default total
%access public export

||| A "full" or non-empty list
FList : Type -> Type
FList a = (xs : List a ** NonEmpty xs)

infixr 5 :::

(:::) : a -> List a -> FList a
(:::) x xs = ((x :: xs) ** IsNonEmpty)

||| Proof that the first list is an improper prefix of the second list, with the
||| third list as the remainder.
data IsPrefixOf : FList a -> FList a -> List a -> Type where
  SingletonPrefix : IsPrefixOf (x ::: []) (x ::: rem) rem
  SuccPrefix : IsPrefixOf (xs ** _) (ys ** _) rem
             -> IsPrefixOf (x ::: xs) (x ::: ys) rem

prefixAntisym : (xs : FList a) -> (ys : FList a) -> (zs : List a)
              -> IsPrefixOf xs ys zs -> IsPrefixOf ys xs zs
              -> (xs = ys, zs = [])
prefixAntisym (xs ** xpf) (ys ** ypf) [] SingletonPrefix _ impossible
prefixAntisym (xs ** xpf) (ys ** ypf) [] (SuccPrefix _) _ impossible
prefixAntisym (xs ** xpf) (ys ** ypf) (_ :: _) SingletonPrefix _ impossible
prefixAntisym (xs ** xpf) (ys ** ypf) (_ :: _) (SuccPrefix _) _ impossible

prefixAntisym' : (xs : FList a) -> (ys : FList a) -> (zs : List a)
               -> IsPrefixOf xs ys zs -> IsPrefixOf ys xs zs
               -> (xs = ys, zs = [])
prefixAntisym' ((x :: []) ** IsNonEmpty) ((x :: []) ** IsNonEmpty) [] SingletonPrefix SingletonPrefix = (Refl, Refl)
prefixAntisym' ((x :: []) ** IsNonEmpty) ((y :: (y' :: ys)) ** IsNonEmpty) [] ipo1 ipo2 = ?prefixAntisym'_rhs_5
prefixAntisym' ((x :: (x' :: xs)) ** IsNonEmpty) ((y :: []) ** IsNonEmpty) [] ipo1 ipo2 = ?prefixAntisym'_rhs_1
prefixAntisym' ((x :: (x' :: xs)) ** IsNonEmpty) ((y :: (y' :: ys)) ** IsNonEmpty) [] ipo1 ipo2 = ?prefixAntisym'_rhs_6
prefixAntisym' ((x :: xs) ** IsNonEmpty) ((y :: ys) ** IsNonEmpty) (z :: zs) ipo1 ipo2 = ?prefixAntisym'_rhs_3

max_stars_repo_name: Kazark/fspp

max_issues_repo_name: Kazark/fspp

max_forks_repo_name: Kazark/fspp