text:
module Web.Raw.Svg

import JS
import Web.Internal.SvgPrim
import Web.Internal.Types

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

namespace SVGAElement

  export
  download : SVGAElement -> Attribute True I String
  download v = fromPrim "SVGAElement.getdownload"
                        prim__download
                        prim__setDownload
                        v

  export
  hreflang : SVGAElement -> Attribute True I String
  hreflang v = fromPrim "SVGAElement.gethreflang"
                        prim__hreflang
                        prim__setHreflang
                        v

  export
  ping : SVGAElement -> Attribute True I String
  ping v = fromPrim "SVGAElement.getping" prim__ping prim__setPing v

  export
  referrerPolicy : SVGAElement -> Attribute True I String
  referrerPolicy v = fromPrim "SVGAElement.getreferrerPolicy"
                              prim__referrerPolicy
                              prim__setReferrerPolicy
                              v

  export
  rel : SVGAElement -> Attribute True I String
  rel v = fromPrim "SVGAElement.getrel" prim__rel prim__setRel v

  export
  relList : (obj : SVGAElement) -> JSIO DOMTokenList
  relList a = primJS $ SVGAElement.prim__relList a

  export
  target : (obj : SVGAElement) -> JSIO SVGAnimatedString
  target a = primJS $ SVGAElement.prim__target a

  export
  text : SVGAElement -> Attribute True I String
  text v = fromPrim "SVGAElement.gettext" prim__text prim__setText v

  export
  type : SVGAElement -> Attribute True I String
  type v = fromPrim "SVGAElement.gettype" prim__type prim__setType v

namespace SVGAngle

  public export
  SVG_ANGLETYPE_DEG : Bits16
  SVG_ANGLETYPE_DEG = 2

  public export
  SVG_ANGLETYPE_GRAD : Bits16
  SVG_ANGLETYPE_GRAD = 4

  public export
  SVG_ANGLETYPE_RAD : Bits16
  SVG_ANGLETYPE_RAD = 3

  public export
  SVG_ANGLETYPE_UNKNOWN : Bits16
  SVG_ANGLETYPE_UNKNOWN = 0

  public export
  SVG_ANGLETYPE_UNSPECIFIED : Bits16
  SVG_ANGLETYPE_UNSPECIFIED = 1

  export
  unitType : (obj : SVGAngle) -> JSIO Bits16
  unitType a = primJS $ SVGAngle.prim__unitType a

  export
  value : SVGAngle -> Attribute True I Double
  value v = fromPrim "SVGAngle.getvalue" prim__value prim__setValue v

  export
  valueAsString : SVGAngle -> Attribute True I String
  valueAsString v = fromPrim "SVGAngle.getvalueAsString"
                             prim__valueAsString
                             prim__setValueAsString
                             v

  export
  valueInSpecifiedUnits : SVGAngle -> Attribute True I Double
  valueInSpecifiedUnits v = fromPrim "SVGAngle.getvalueInSpecifiedUnits"
                                     prim__valueInSpecifiedUnits
                                     prim__setValueInSpecifiedUnits
                                     v

  export
  convertToSpecifiedUnits : (obj : SVGAngle) -> (unitType : Bits16) -> JSIO ()
  convertToSpecifiedUnits a b = primJS
                              $ SVGAngle.prim__convertToSpecifiedUnits a b

  export
  newValueSpecifiedUnits :  (obj : SVGAngle)
                         -> (unitType : Bits16)
                         -> (valueInSpecifiedUnits : Double)
                         -> JSIO ()
  newValueSpecifiedUnits a b c = primJS
                               $ SVGAngle.prim__newValueSpecifiedUnits a b c

namespace SVGAnimatedAngle

  export
  animVal : (obj : SVGAnimatedAngle) -> JSIO SVGAngle
  animVal a = primJS $ SVGAnimatedAngle.prim__animVal a

  export
  baseVal : (obj : SVGAnimatedAngle) -> JSIO SVGAngle
  baseVal a = primJS $ SVGAnimatedAngle.prim__baseVal a

namespace SVGAnimatedBoolean

  export
  animVal : (obj : SVGAnimatedBoolean) -> JSIO Bool
  animVal a = tryJS "SVGAnimatedBoolean.animVal"
            $ SVGAnimatedBoolean.prim__animVal a

  export
  baseVal : SVGAnimatedBoolean -> Attribute True I Bool
  baseVal v = fromPrim "SVGAnimatedBoolean.getbaseVal"
                       prim__baseVal
                       prim__setBaseVal
                       v

namespace SVGAnimatedEnumeration

  export
  animVal : (obj : SVGAnimatedEnumeration) -> JSIO Bits16
  animVal a = primJS $ SVGAnimatedEnumeration.prim__animVal a

  export
  baseVal : SVGAnimatedEnumeration -> Attribute True I Bits16
  baseVal v = fromPrim "SVGAnimatedEnumeration.getbaseVal"
                       prim__baseVal
                       prim__setBaseVal
                       v

namespace SVGAnimatedInteger

  export
  animVal : (obj : SVGAnimatedInteger) -> JSIO Int32
  animVal a = primJS $ SVGAnimatedInteger.prim__animVal a

  export
  baseVal : SVGAnimatedInteger -> Attribute True I Int32
  baseVal v = fromPrim "SVGAnimatedInteger.getbaseVal"
                       prim__baseVal
                       prim__setBaseVal
                       v

namespace SVGAnimatedLength

  export
  animVal : (obj : SVGAnimatedLength) -> JSIO SVGLength
  animVal a = primJS $ SVGAnimatedLength.prim__animVal a

  export
  baseVal : (obj : SVGAnimatedLength) -> JSIO SVGLength
  baseVal a = primJS $ SVGAnimatedLength.prim__baseVal a

namespace SVGAnimatedLengthList

  export
  animVal : (obj : SVGAnimatedLengthList) -> JSIO SVGLengthList
  animVal a = primJS $ SVGAnimatedLengthList.prim__animVal a

  export
  baseVal : (obj : SVGAnimatedLengthList) -> JSIO SVGLengthList
  baseVal a = primJS $ SVGAnimatedLengthList.prim__baseVal a

namespace SVGAnimatedNumber

  export
  animVal : (obj : SVGAnimatedNumber) -> JSIO Double
  animVal a = primJS $ SVGAnimatedNumber.prim__animVal a

  export
  baseVal : SVGAnimatedNumber -> Attribute True I Double
  baseVal v = fromPrim "SVGAnimatedNumber.getbaseVal"
                       prim__baseVal
                       prim__setBaseVal
                       v

namespace SVGAnimatedNumberList

  export
  animVal : (obj : SVGAnimatedNumberList) -> JSIO SVGNumberList
  animVal a = primJS $ SVGAnimatedNumberList.prim__animVal a

  export
  baseVal : (obj : SVGAnimatedNumberList) -> JSIO SVGNumberList
  baseVal a = primJS $ SVGAnimatedNumberList.prim__baseVal a

namespace SVGAnimatedPreserveAspectRatio

  export
  animVal :  (obj : SVGAnimatedPreserveAspectRatio)
          -> JSIO SVGPreserveAspectRatio
  animVal a = primJS $ SVGAnimatedPreserveAspectRatio.prim__animVal a

  export
  baseVal :  (obj : SVGAnimatedPreserveAspectRatio)
          -> JSIO SVGPreserveAspectRatio
  baseVal a = primJS $ SVGAnimatedPreserveAspectRatio.prim__baseVal a

namespace SVGAnimatedRect

  export
  animVal : (obj : SVGAnimatedRect) -> JSIO DOMRectReadOnly
  animVal a = primJS $ SVGAnimatedRect.prim__animVal a

  export
  baseVal : (obj : SVGAnimatedRect) -> JSIO DOMRect
  baseVal a = primJS $ SVGAnimatedRect.prim__baseVal a

namespace SVGAnimatedString

  export
  animVal : (obj : SVGAnimatedString) -> JSIO String
  animVal a = primJS $ SVGAnimatedString.prim__animVal a

  export
  baseVal : SVGAnimatedString -> Attribute True I String
  baseVal v = fromPrim "SVGAnimatedString.getbaseVal"
                       prim__baseVal
                       prim__setBaseVal
                       v

namespace SVGAnimatedTransformList

  export
  animVal : (obj : SVGAnimatedTransformList) -> JSIO SVGTransformList
  animVal a = primJS $ SVGAnimatedTransformList.prim__animVal a

  export
  baseVal : (obj : SVGAnimatedTransformList) -> JSIO SVGTransformList
  baseVal a = primJS $ SVGAnimatedTransformList.prim__baseVal a

namespace SVGCircleElement

  export
  cx : (obj : SVGCircleElement) -> JSIO SVGAnimatedLength
  cx a = primJS $ SVGCircleElement.prim__cx a

  export
  cy : (obj : SVGCircleElement) -> JSIO SVGAnimatedLength
  cy a = primJS $ SVGCircleElement.prim__cy a

  export
  r : (obj : SVGCircleElement) -> JSIO SVGAnimatedLength
  r a = primJS $ SVGCircleElement.prim__r a

namespace SVGElement

  export
  className :  (0 _ : JSType t1)
            => {auto 0 _ : Elem SVGElement (Types t1)}
            -> (obj : t1)
            -> JSIO SVGAnimatedString
  className a = primJS $ SVGElement.prim__className (up a)

  export
  ownerSVGElement :  (0 _ : JSType t1)
                  => {auto 0 _ : Elem SVGElement (Types t1)}
                  -> (obj : t1)
                  -> JSIO (Maybe SVGSVGElement)
  ownerSVGElement a = tryJS "SVGElement.ownerSVGElement"
                    $ SVGElement.prim__ownerSVGElement (up a)

  export
  viewportElement :  (0 _ : JSType t1)
                  => {auto 0 _ : Elem SVGElement (Types t1)}
                  -> (obj : t1)
                  -> JSIO (Maybe SVGElement)
  viewportElement a = tryJS "SVGElement.viewportElement"
                    $ SVGElement.prim__viewportElement (up a)

namespace SVGEllipseElement

  export
  cx : (obj : SVGEllipseElement) -> JSIO SVGAnimatedLength
  cx a = primJS $ SVGEllipseElement.prim__cx a

  export
  cy : (obj : SVGEllipseElement) -> JSIO SVGAnimatedLength
  cy a = primJS $ SVGEllipseElement.prim__cy a

  export
  rx : (obj : SVGEllipseElement) -> JSIO SVGAnimatedLength
  rx a = primJS $ SVGEllipseElement.prim__rx a

  export
  ry : (obj : SVGEllipseElement) -> JSIO SVGAnimatedLength
  ry a = primJS $ SVGEllipseElement.prim__ry a

namespace SVGForeignObjectElement

  export
  height : (obj : SVGForeignObjectElement) -> JSIO SVGAnimatedLength
  height a = primJS $ SVGForeignObjectElement.prim__height a

  export
  width : (obj : SVGForeignObjectElement) -> JSIO SVGAnimatedLength
  width a = primJS $ SVGForeignObjectElement.prim__width a

  export
  x : (obj : SVGForeignObjectElement) -> JSIO SVGAnimatedLength
  x a = primJS $ SVGForeignObjectElement.prim__x a

  export
  y : (obj : SVGForeignObjectElement) -> JSIO SVGAnimatedLength
  y a = primJS $ SVGForeignObjectElement.prim__y a

namespace SVGGeometryElement

  export
  pathLength :  (0 _ : JSType t1)
             => {auto 0 _ : Elem SVGGeometryElement (Types t1)}
             -> (obj : t1)
             -> JSIO SVGAnimatedNumber
  pathLength a = primJS $ SVGGeometryElement.prim__pathLength (up a)

  export
  getPointAtLength :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem SVGGeometryElement (Types t1)}
                   -> (obj : t1)
                   -> (distance : Double)
                   -> JSIO DOMPoint
  getPointAtLength a b = primJS
                       $ SVGGeometryElement.prim__getPointAtLength (up a) b

  export
  getTotalLength :  (0 _ : JSType t1)
                 => {auto 0 _ : Elem SVGGeometryElement (Types t1)}
                 -> (obj : t1)
                 -> JSIO Double
  getTotalLength a = primJS $ SVGGeometryElement.prim__getTotalLength (up a)

  export
  isPointInFill :  (0 _ : JSType t1)
                => (0 _ : JSType t2)
                => {auto 0 _ : Elem SVGGeometryElement (Types t1)}
                -> {auto 0 _ : Elem DOMPointInit (Types t2)}
                -> (obj : t1)
                -> (point : Optional t2)
                -> JSIO Bool
  isPointInFill a b = tryJS "SVGGeometryElement.isPointInFill"
                    $ SVGGeometryElement.prim__isPointInFill (up a) (optUp b)

  export
  isPointInFill' :  (0 _ : JSType t1)
                 => {auto 0 _ : Elem SVGGeometryElement (Types t1)}
                 -> (obj : t1)
                 -> JSIO Bool
  isPointInFill' a = tryJS "SVGGeometryElement.isPointInFill'"
                   $ SVGGeometryElement.prim__isPointInFill (up a) undef

  export
  isPointInStroke :  (0 _ : JSType t1)
                  => (0 _ : JSType t2)
                  => {auto 0 _ : Elem SVGGeometryElement (Types t1)}
                  -> {auto 0 _ : Elem DOMPointInit (Types t2)}
                  -> (obj : t1)
                  -> (point : Optional t2)
                  -> JSIO Bool
  isPointInStroke a b = tryJS "SVGGeometryElement.isPointInStroke"
                      $ SVGGeometryElement.prim__isPointInStroke (up a)
                                                                 (optUp b)

  export
  isPointInStroke' :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem SVGGeometryElement (Types t1)}
                   -> (obj : t1)
                   -> JSIO Bool
  isPointInStroke' a = tryJS "SVGGeometryElement.isPointInStroke'"
                     $ SVGGeometryElement.prim__isPointInStroke (up a) undef

namespace SVGGradientElement

  public export
  SVG_SPREADMETHOD_PAD : Bits16
  SVG_SPREADMETHOD_PAD = 1

  public export
  SVG_SPREADMETHOD_REFLECT : Bits16
  SVG_SPREADMETHOD_REFLECT = 2

  public export
  SVG_SPREADMETHOD_REPEAT : Bits16
  SVG_SPREADMETHOD_REPEAT = 3

  public export
  SVG_SPREADMETHOD_UNKNOWN : Bits16
  SVG_SPREADMETHOD_UNKNOWN = 0

  export
  gradientTransform :  (0 _ : JSType t1)
                    => {auto 0 _ : Elem SVGGradientElement (Types t1)}
                    -> (obj : t1)
                    -> JSIO SVGAnimatedTransformList
  gradientTransform a = primJS
                      $ SVGGradientElement.prim__gradientTransform (up a)

  export
  gradientUnits :  (0 _ : JSType t1)
                => {auto 0 _ : Elem SVGGradientElement (Types t1)}
                -> (obj : t1)
                -> JSIO SVGAnimatedEnumeration
  gradientUnits a = primJS $ SVGGradientElement.prim__gradientUnits (up a)

  export
  spreadMethod :  (0 _ : JSType t1)
               => {auto 0 _ : Elem SVGGradientElement (Types t1)}
               -> (obj : t1)
               -> JSIO SVGAnimatedEnumeration
  spreadMethod a = primJS $ SVGGradientElement.prim__spreadMethod (up a)

namespace SVGGraphicsElement

  export
  transform :  (0 _ : JSType t1)
            => {auto 0 _ : Elem SVGGraphicsElement (Types t1)}
            -> (obj : t1)
            -> JSIO SVGAnimatedTransformList
  transform a = primJS $ SVGGraphicsElement.prim__transform (up a)

  export
  getBBox :  (0 _ : JSType t1)
          => (0 _ : JSType t2)
          => {auto 0 _ : Elem SVGGraphicsElement (Types t1)}
          -> {auto 0 _ : Elem SVGBoundingBoxOptions (Types t2)}
          -> (obj : t1)
          -> (options : Optional t2)
          -> JSIO DOMRect
  getBBox a b = primJS $ SVGGraphicsElement.prim__getBBox (up a) (optUp b)

  export
  getBBox' :  (0 _ : JSType t1)
           => {auto 0 _ : Elem SVGGraphicsElement (Types t1)}
           -> (obj : t1)
           -> JSIO DOMRect
  getBBox' a = primJS $ SVGGraphicsElement.prim__getBBox (up a) undef

  export
  getCTM :  (0 _ : JSType t1)
         => {auto 0 _ : Elem SVGGraphicsElement (Types t1)}
         -> (obj : t1)
         -> JSIO (Maybe DOMMatrix)
  getCTM a = tryJS "SVGGraphicsElement.getCTM"
           $ SVGGraphicsElement.prim__getCTM (up a)

  export
  getScreenCTM :  (0 _ : JSType t1)
               => {auto 0 _ : Elem SVGGraphicsElement (Types t1)}
               -> (obj : t1)
               -> JSIO (Maybe DOMMatrix)
  getScreenCTM a = tryJS "SVGGraphicsElement.getScreenCTM"
                 $ SVGGraphicsElement.prim__getScreenCTM (up a)

namespace SVGImageElement

  export
  crossOrigin : SVGImageElement -> Attribute False Maybe String
  crossOrigin v = fromNullablePrim "SVGImageElement.getcrossOrigin"
                                   prim__crossOrigin
                                   prim__setCrossOrigin
                                   v

  export
  height : (obj : SVGImageElement) -> JSIO SVGAnimatedLength
  height a = primJS $ SVGImageElement.prim__height a

  export
  preserveAspectRatio :  (obj : SVGImageElement)
                      -> JSIO SVGAnimatedPreserveAspectRatio
  preserveAspectRatio a = primJS $ SVGImageElement.prim__preserveAspectRatio a

  export
  width : (obj : SVGImageElement) -> JSIO SVGAnimatedLength
  width a = primJS $ SVGImageElement.prim__width a

  export
  x : (obj : SVGImageElement) -> JSIO SVGAnimatedLength
  x a = primJS $ SVGImageElement.prim__x a

  export
  y : (obj : SVGImageElement) -> JSIO SVGAnimatedLength
  y a = primJS $ SVGImageElement.prim__y a

namespace SVGLength

  public export
  SVG_LENGTHTYPE_CM : Bits16
  SVG_LENGTHTYPE_CM = 6

  public export
  SVG_LENGTHTYPE_EMS : Bits16
  SVG_LENGTHTYPE_EMS = 3

  public export
  SVG_LENGTHTYPE_EXS : Bits16
  SVG_LENGTHTYPE_EXS = 4

  public export
  SVG_LENGTHTYPE_IN : Bits16
  SVG_LENGTHTYPE_IN = 8

  public export
  SVG_LENGTHTYPE_MM : Bits16
  SVG_LENGTHTYPE_MM = 7

  public export
  SVG_LENGTHTYPE_NUMBER : Bits16
  SVG_LENGTHTYPE_NUMBER = 1

  public export
  SVG_LENGTHTYPE_PC : Bits16
  SVG_LENGTHTYPE_PC = 10

  public export
  SVG_LENGTHTYPE_PERCENTAGE : Bits16
  SVG_LENGTHTYPE_PERCENTAGE = 2

  public export
  SVG_LENGTHTYPE_PT : Bits16
  SVG_LENGTHTYPE_PT = 9

  public export
  SVG_LENGTHTYPE_PX : Bits16
  SVG_LENGTHTYPE_PX = 5

  public export
  SVG_LENGTHTYPE_UNKNOWN : Bits16
  SVG_LENGTHTYPE_UNKNOWN = 0

  export
  unitType : (obj : SVGLength) -> JSIO Bits16
  unitType a = primJS $ SVGLength.prim__unitType a

  export
  value : SVGLength -> Attribute True I Double
  value v = fromPrim "SVGLength.getvalue" prim__value prim__setValue v

  export
  valueAsString : SVGLength -> Attribute True I String
  valueAsString v = fromPrim "SVGLength.getvalueAsString"
                             prim__valueAsString
                             prim__setValueAsString
                             v

  export
  valueInSpecifiedUnits : SVGLength -> Attribute True I Double
  valueInSpecifiedUnits v = fromPrim "SVGLength.getvalueInSpecifiedUnits"
                                     prim__valueInSpecifiedUnits
                                     prim__setValueInSpecifiedUnits
                                     v

  export
  convertToSpecifiedUnits : (obj : SVGLength) -> (unitType : Bits16) -> JSIO ()
  convertToSpecifiedUnits a b = primJS
                              $ SVGLength.prim__convertToSpecifiedUnits a b

  export
  newValueSpecifiedUnits :  (obj : SVGLength)
                         -> (unitType : Bits16)
                         -> (valueInSpecifiedUnits : Double)
                         -> JSIO ()
  newValueSpecifiedUnits a b c = primJS
                               $ SVGLength.prim__newValueSpecifiedUnits a b c

namespace SVGLengthList

  export
  set :  (obj : SVGLengthList)
      -> (index : Bits32)
      -> (newItem : SVGLength)
      -> JSIO ()
  set a b c = primJS $ SVGLengthList.prim__set a b c

  export
  length : (obj : SVGLengthList) -> JSIO Bits32
  length a = primJS $ SVGLengthList.prim__length a

  export
  numberOfItems : (obj : SVGLengthList) -> JSIO Bits32
  numberOfItems a = primJS $ SVGLengthList.prim__numberOfItems a

  export
  appendItem : (obj : SVGLengthList) -> (newItem : SVGLength) -> JSIO SVGLength
  appendItem a b = primJS $ SVGLengthList.prim__appendItem a b

  export
  clear : (obj : SVGLengthList) -> JSIO ()
  clear a = primJS $ SVGLengthList.prim__clear a

  export
  getItem : (obj : SVGLengthList) -> (index : Bits32) -> JSIO SVGLength
  getItem a b = primJS $ SVGLengthList.prim__getItem a b

  export
  initialize : (obj : SVGLengthList) -> (newItem : SVGLength) -> JSIO SVGLength
  initialize a b = primJS $ SVGLengthList.prim__initialize a b

  export
  insertItemBefore :  (obj : SVGLengthList)
                   -> (newItem : SVGLength)
                   -> (index : Bits32)
                   -> JSIO SVGLength
  insertItemBefore a b c = primJS $ SVGLengthList.prim__insertItemBefore a b c

  export
  removeItem : (obj : SVGLengthList) -> (index : Bits32) -> JSIO SVGLength
  removeItem a b = primJS $ SVGLengthList.prim__removeItem a b

  export
  replaceItem :  (obj : SVGLengthList)
              -> (newItem : SVGLength)
              -> (index : Bits32)
              -> JSIO SVGLength
  replaceItem a b c = primJS $ SVGLengthList.prim__replaceItem a b c

namespace SVGLineElement

  export
  x1 : (obj : SVGLineElement) -> JSIO SVGAnimatedLength
  x1 a = primJS $ SVGLineElement.prim__x1 a

  export
  x2 : (obj : SVGLineElement) -> JSIO SVGAnimatedLength
  x2 a = primJS $ SVGLineElement.prim__x2 a

  export
  y1 : (obj : SVGLineElement) -> JSIO SVGAnimatedLength
  y1 a = primJS $ SVGLineElement.prim__y1 a

  export
  y2 : (obj : SVGLineElement) -> JSIO SVGAnimatedLength
  y2 a = primJS $ SVGLineElement.prim__y2 a

namespace SVGLinearGradientElement

  export
  x1 : (obj : SVGLinearGradientElement) -> JSIO SVGAnimatedLength
  x1 a = primJS $ SVGLinearGradientElement.prim__x1 a

  export
  x2 : (obj : SVGLinearGradientElement) -> JSIO SVGAnimatedLength
  x2 a = primJS $ SVGLinearGradientElement.prim__x2 a

  export
  y1 : (obj : SVGLinearGradientElement) -> JSIO SVGAnimatedLength
  y1 a = primJS $ SVGLinearGradientElement.prim__y1 a

  export
  y2 : (obj : SVGLinearGradientElement) -> JSIO SVGAnimatedLength
  y2 a = primJS $ SVGLinearGradientElement.prim__y2 a

namespace SVGMarkerElement

  public export
  SVG_MARKERUNITS_STROKEWIDTH : Bits16
  SVG_MARKERUNITS_STROKEWIDTH = 2

  public export
  SVG_MARKERUNITS_UNKNOWN : Bits16
  SVG_MARKERUNITS_UNKNOWN = 0

  public export
  SVG_MARKERUNITS_USERSPACEONUSE : Bits16
  SVG_MARKERUNITS_USERSPACEONUSE = 1

  public export
  SVG_MARKER_ORIENT_ANGLE : Bits16
  SVG_MARKER_ORIENT_ANGLE = 2

  public export
  SVG_MARKER_ORIENT_AUTO : Bits16
  SVG_MARKER_ORIENT_AUTO = 1

  public export
  SVG_MARKER_ORIENT_UNKNOWN : Bits16
  SVG_MARKER_ORIENT_UNKNOWN = 0

  export
  markerHeight : (obj : SVGMarkerElement) -> JSIO SVGAnimatedLength
  markerHeight a = primJS $ SVGMarkerElement.prim__markerHeight a

  export
  markerUnits : (obj : SVGMarkerElement) -> JSIO SVGAnimatedEnumeration
  markerUnits a = primJS $ SVGMarkerElement.prim__markerUnits a

  export
  markerWidth : (obj : SVGMarkerElement) -> JSIO SVGAnimatedLength
  markerWidth a = primJS $ SVGMarkerElement.prim__markerWidth a

  export
  orient : SVGMarkerElement -> Attribute True I String
  orient v = fromPrim "SVGMarkerElement.getorient"
                      prim__orient
                      prim__setOrient
                      v

  export
  orientAngle : (obj : SVGMarkerElement) -> JSIO SVGAnimatedAngle
  orientAngle a = primJS $ SVGMarkerElement.prim__orientAngle a

  export
  orientType : (obj : SVGMarkerElement) -> JSIO SVGAnimatedEnumeration
  orientType a = primJS $ SVGMarkerElement.prim__orientType a

  export
  refX : (obj : SVGMarkerElement) -> JSIO SVGAnimatedLength
  refX a = primJS $ SVGMarkerElement.prim__refX a

  export
  refY : (obj : SVGMarkerElement) -> JSIO SVGAnimatedLength
  refY a = primJS $ SVGMarkerElement.prim__refY a

  export
  setOrientToAngle : (obj : SVGMarkerElement) -> (angle : SVGAngle) -> JSIO ()
  setOrientToAngle a b = primJS $ SVGMarkerElement.prim__setOrientToAngle a b

  export
  setOrientToAuto : (obj : SVGMarkerElement) -> JSIO ()
  setOrientToAuto a = primJS $ SVGMarkerElement.prim__setOrientToAuto a

namespace SVGNumber

  export
  value : SVGNumber -> Attribute True I Double
  value v = fromPrim "SVGNumber.getvalue" prim__value prim__setValue v

namespace SVGNumberList

  export
  set :  (obj : SVGNumberList)
      -> (index : Bits32)
      -> (newItem : SVGNumber)
      -> JSIO ()
  set a b c = primJS $ SVGNumberList.prim__set a b c

  export
  length : (obj : SVGNumberList) -> JSIO Bits32
  length a = primJS $ SVGNumberList.prim__length a

  export
  numberOfItems : (obj : SVGNumberList) -> JSIO Bits32
  numberOfItems a = primJS $ SVGNumberList.prim__numberOfItems a

  export
  appendItem : (obj : SVGNumberList) -> (newItem : SVGNumber) -> JSIO SVGNumber
  appendItem a b = primJS $ SVGNumberList.prim__appendItem a b

  export
  clear : (obj : SVGNumberList) -> JSIO ()
  clear a = primJS $ SVGNumberList.prim__clear a

  export
  getItem : (obj : SVGNumberList) -> (index : Bits32) -> JSIO SVGNumber
  getItem a b = primJS $ SVGNumberList.prim__getItem a b

  export
  initialize : (obj : SVGNumberList) -> (newItem : SVGNumber) -> JSIO SVGNumber
  initialize a b = primJS $ SVGNumberList.prim__initialize a b

  export
  insertItemBefore :  (obj : SVGNumberList)
                   -> (newItem : SVGNumber)
                   -> (index : Bits32)
                   -> JSIO SVGNumber
  insertItemBefore a b c = primJS $ SVGNumberList.prim__insertItemBefore a b c

  export
  removeItem : (obj : SVGNumberList) -> (index : Bits32) -> JSIO SVGNumber
  removeItem a b = primJS $ SVGNumberList.prim__removeItem a b

  export
  replaceItem :  (obj : SVGNumberList)
              -> (newItem : SVGNumber)
              -> (index : Bits32)
              -> JSIO SVGNumber
  replaceItem a b c = primJS $ SVGNumberList.prim__replaceItem a b c

namespace SVGPatternElement

  export
  height : (obj : SVGPatternElement) -> JSIO SVGAnimatedLength
  height a = primJS $ SVGPatternElement.prim__height a

  export
  patternContentUnits : (obj : SVGPatternElement) -> JSIO SVGAnimatedEnumeration
  patternContentUnits a = primJS $ SVGPatternElement.prim__patternContentUnits a

  export
  patternTransform : (obj : SVGPatternElement) -> JSIO SVGAnimatedTransformList
  patternTransform a = primJS $ SVGPatternElement.prim__patternTransform a

  export
  patternUnits : (obj : SVGPatternElement) -> JSIO SVGAnimatedEnumeration
  patternUnits a = primJS $ SVGPatternElement.prim__patternUnits a

  export
  width : (obj : SVGPatternElement) -> JSIO SVGAnimatedLength
  width a = primJS $ SVGPatternElement.prim__width a

  export
  x : (obj : SVGPatternElement) -> JSIO SVGAnimatedLength
  x a = primJS $ SVGPatternElement.prim__x a

  export
  y : (obj : SVGPatternElement) -> JSIO SVGAnimatedLength
  y a = primJS $ SVGPatternElement.prim__y a

namespace SVGPointList

  export
  set :  (obj : SVGPointList)
      -> (index : Bits32)
      -> (newItem : DOMPoint)
      -> JSIO ()
  set a b c = primJS $ SVGPointList.prim__set a b c

  export
  length : (obj : SVGPointList) -> JSIO Bits32
  length a = primJS $ SVGPointList.prim__length a

  export
  numberOfItems : (obj : SVGPointList) -> JSIO Bits32
  numberOfItems a = primJS $ SVGPointList.prim__numberOfItems a

  export
  appendItem : (obj : SVGPointList) -> (newItem : DOMPoint) -> JSIO DOMPoint
  appendItem a b = primJS $ SVGPointList.prim__appendItem a b

  export
  clear : (obj : SVGPointList) -> JSIO ()
  clear a = primJS $ SVGPointList.prim__clear a

  export
  getItem : (obj : SVGPointList) -> (index : Bits32) -> JSIO DOMPoint
  getItem a b = primJS $ SVGPointList.prim__getItem a b

  export
  initialize : (obj : SVGPointList) -> (newItem : DOMPoint) -> JSIO DOMPoint
  initialize a b = primJS $ SVGPointList.prim__initialize a b

  export
  insertItemBefore :  (obj : SVGPointList)
                   -> (newItem : DOMPoint)
                   -> (index : Bits32)
                   -> JSIO DOMPoint
  insertItemBefore a b c = primJS $ SVGPointList.prim__insertItemBefore a b c

  export
  removeItem : (obj : SVGPointList) -> (index : Bits32) -> JSIO DOMPoint
  removeItem a b = primJS $ SVGPointList.prim__removeItem a b

  export
  replaceItem :  (obj : SVGPointList)
              -> (newItem : DOMPoint)
              -> (index : Bits32)
              -> JSIO DOMPoint
  replaceItem a b c = primJS $ SVGPointList.prim__replaceItem a b c

namespace SVGPreserveAspectRatio

  public export
  SVG_MEETORSLICE_MEET : Bits16
  SVG_MEETORSLICE_MEET = 1

  public export
  SVG_MEETORSLICE_SLICE : Bits16
  SVG_MEETORSLICE_SLICE = 2

  public export
  SVG_MEETORSLICE_UNKNOWN : Bits16
  SVG_MEETORSLICE_UNKNOWN = 0

  public export
  SVG_PRESERVEASPECTRATIO_NONE : Bits16
  SVG_PRESERVEASPECTRATIO_NONE = 1

  public export
  SVG_PRESERVEASPECTRATIO_UNKNOWN : Bits16
  SVG_PRESERVEASPECTRATIO_UNKNOWN = 0

  public export
  SVG_PRESERVEASPECTRATIO_XMAXYMAX : Bits16
  SVG_PRESERVEASPECTRATIO_XMAXYMAX = 10

  public export
  SVG_PRESERVEASPECTRATIO_XMAXYMID : Bits16
  SVG_PRESERVEASPECTRATIO_XMAXYMID = 7

  public export
  SVG_PRESERVEASPECTRATIO_XMAXYMIN : Bits16
  SVG_PRESERVEASPECTRATIO_XMAXYMIN = 4

  public export
  SVG_PRESERVEASPECTRATIO_XMIDYMAX : Bits16
  SVG_PRESERVEASPECTRATIO_XMIDYMAX = 9

  public export
  SVG_PRESERVEASPECTRATIO_XMIDYMID : Bits16
  SVG_PRESERVEASPECTRATIO_XMIDYMID = 6

  public export
  SVG_PRESERVEASPECTRATIO_XMIDYMIN : Bits16
  SVG_PRESERVEASPECTRATIO_XMIDYMIN = 3

  public export
  SVG_PRESERVEASPECTRATIO_XMINYMAX : Bits16
  SVG_PRESERVEASPECTRATIO_XMINYMAX = 8

  public export
  SVG_PRESERVEASPECTRATIO_XMINYMID : Bits16
  SVG_PRESERVEASPECTRATIO_XMINYMID = 5

  public export
  SVG_PRESERVEASPECTRATIO_XMINYMIN : Bits16
  SVG_PRESERVEASPECTRATIO_XMINYMIN = 2

  export
  align : SVGPreserveAspectRatio -> Attribute True I Bits16
  align v = fromPrim "SVGPreserveAspectRatio.getalign"
                     prim__align
                     prim__setAlign
                     v

  export
  meetOrSlice : SVGPreserveAspectRatio -> Attribute True I Bits16
  meetOrSlice v = fromPrim "SVGPreserveAspectRatio.getmeetOrSlice"
                           prim__meetOrSlice
                           prim__setMeetOrSlice
                           v

namespace SVGRadialGradientElement

  export
  cx : (obj : SVGRadialGradientElement) -> JSIO SVGAnimatedLength
  cx a = primJS $ SVGRadialGradientElement.prim__cx a

  export
  cy : (obj : SVGRadialGradientElement) -> JSIO SVGAnimatedLength
  cy a = primJS $ SVGRadialGradientElement.prim__cy a

  export
  fr : (obj : SVGRadialGradientElement) -> JSIO SVGAnimatedLength
  fr a = primJS $ SVGRadialGradientElement.prim__fr a

  export
  fx : (obj : SVGRadialGradientElement) -> JSIO SVGAnimatedLength
  fx a = primJS $ SVGRadialGradientElement.prim__fx a

  export
  fy : (obj : SVGRadialGradientElement) -> JSIO SVGAnimatedLength
  fy a = primJS $ SVGRadialGradientElement.prim__fy a

  export
  r : (obj : SVGRadialGradientElement) -> JSIO SVGAnimatedLength
  r a = primJS $ SVGRadialGradientElement.prim__r a

namespace SVGRectElement

  export
  height : (obj : SVGRectElement) -> JSIO SVGAnimatedLength
  height a = primJS $ SVGRectElement.prim__height a

  export
  rx : (obj : SVGRectElement) -> JSIO SVGAnimatedLength
  rx a = primJS $ SVGRectElement.prim__rx a

  export
  ry : (obj : SVGRectElement) -> JSIO SVGAnimatedLength
  ry a = primJS $ SVGRectElement.prim__ry a

  export
  width : (obj : SVGRectElement) -> JSIO SVGAnimatedLength
  width a = primJS $ SVGRectElement.prim__width a

  export
  x : (obj : SVGRectElement) -> JSIO SVGAnimatedLength
  x a = primJS $ SVGRectElement.prim__x a

  export
  y : (obj : SVGRectElement) -> JSIO SVGAnimatedLength
  y a = primJS $ SVGRectElement.prim__y a

namespace SVGSVGElement

  export
  currentScale : SVGSVGElement -> Attribute True I Double
  currentScale v = fromPrim "SVGSVGElement.getcurrentScale"
                            prim__currentScale
                            prim__setCurrentScale
                            v

  export
  currentTranslate : (obj : SVGSVGElement) -> JSIO DOMPointReadOnly
  currentTranslate a = primJS $ SVGSVGElement.prim__currentTranslate a

  export
  height : (obj : SVGSVGElement) -> JSIO SVGAnimatedLength
  height a = primJS $ SVGSVGElement.prim__height a

  export
  width : (obj : SVGSVGElement) -> JSIO SVGAnimatedLength
  width a = primJS $ SVGSVGElement.prim__width a

  export
  x : (obj : SVGSVGElement) -> JSIO SVGAnimatedLength
  x a = primJS $ SVGSVGElement.prim__x a

  export
  y : (obj : SVGSVGElement) -> JSIO SVGAnimatedLength
  y a = primJS $ SVGSVGElement.prim__y a

  export
  checkEnclosure :  (0 _ : JSType t1)
                 => (0 _ : JSType t2)
                 => {auto 0 _ : Elem SVGElement (Types t1)}
                 -> {auto 0 _ : Elem DOMRectReadOnly (Types t2)}
                 -> (obj : SVGSVGElement)
                 -> (element : t1)
                 -> (rect : t2)
                 -> JSIO Bool
  checkEnclosure a b c = tryJS "SVGSVGElement.checkEnclosure"
                       $ SVGSVGElement.prim__checkEnclosure a (up b) (up c)

  export
  checkIntersection :  (0 _ : JSType t1)
                    => (0 _ : JSType t2)
                    => {auto 0 _ : Elem SVGElement (Types t1)}
                    -> {auto 0 _ : Elem DOMRectReadOnly (Types t2)}
                    -> (obj : SVGSVGElement)
                    -> (element : t1)
                    -> (rect : t2)
                    -> JSIO Bool
  checkIntersection a b c = tryJS "SVGSVGElement.checkIntersection"
                          $ SVGSVGElement.prim__checkIntersection a
                                                                  (up b)
                                                                  (up c)

  export
  createSVGAngle : (obj : SVGSVGElement) -> JSIO SVGAngle
  createSVGAngle a = primJS $ SVGSVGElement.prim__createSVGAngle a

  export
  createSVGLength : (obj : SVGSVGElement) -> JSIO SVGLength
  createSVGLength a = primJS $ SVGSVGElement.prim__createSVGLength a

  export
  createSVGMatrix : (obj : SVGSVGElement) -> JSIO DOMMatrix
  createSVGMatrix a = primJS $ SVGSVGElement.prim__createSVGMatrix a

  export
  createSVGNumber : (obj : SVGSVGElement) -> JSIO SVGNumber
  createSVGNumber a = primJS $ SVGSVGElement.prim__createSVGNumber a

  export
  createSVGPoint : (obj : SVGSVGElement) -> JSIO DOMPoint
  createSVGPoint a = primJS $ SVGSVGElement.prim__createSVGPoint a

  export
  createSVGRect : (obj : SVGSVGElement) -> JSIO DOMRect
  createSVGRect a = primJS $ SVGSVGElement.prim__createSVGRect a

  export
  createSVGTransformFromMatrix :  (0 _ : JSType t1)
                               => {auto 0 _ : Elem DOMMatrix2DInit (Types t1)}
                               -> (obj : SVGSVGElement)
                               -> (matrix : Optional t1)
                               -> JSIO SVGTransform
  createSVGTransformFromMatrix a b = primJS
                                   $ SVGSVGElement.prim__createSVGTransformFromMatrix a
                                                                                (optUp b)

  export
  createSVGTransformFromMatrix' : (obj : SVGSVGElement) -> JSIO SVGTransform
  createSVGTransformFromMatrix' a = primJS
                                  $ SVGSVGElement.prim__createSVGTransformFromMatrix a
                                                                                undef

  export
  createSVGTransform : (obj : SVGSVGElement) -> JSIO SVGTransform
  createSVGTransform a = primJS $ SVGSVGElement.prim__createSVGTransform a

  export
  deselectAll : (obj : SVGSVGElement) -> JSIO ()
  deselectAll a = primJS $ SVGSVGElement.prim__deselectAll a

  export
  forceRedraw : (obj : SVGSVGElement) -> JSIO ()
  forceRedraw a = primJS $ SVGSVGElement.prim__forceRedraw a

  export
  getElementById : (obj : SVGSVGElement) -> (elementId : String) -> JSIO Element
  getElementById a b = primJS $ SVGSVGElement.prim__getElementById a b

  export
  getEnclosureList :  (0 _ : JSType t1)
                   => (0 _ : JSType t2)
                   => {auto 0 _ : Elem DOMRectReadOnly (Types t1)}
                   -> {auto 0 _ : Elem SVGElement (Types t2)}
                   -> (obj : SVGSVGElement)
                   -> (rect : t1)
                   -> (referenceElement : Maybe t2)
                   -> JSIO NodeList
  getEnclosureList a b c = primJS
                         $ SVGSVGElement.prim__getEnclosureList a
                                                                (up b)
                                                                (mayUp c)

  export
  getIntersectionList :  (0 _ : JSType t1)
                      => (0 _ : JSType t2)
                      => {auto 0 _ : Elem DOMRectReadOnly (Types t1)}
                      -> {auto 0 _ : Elem SVGElement (Types t2)}
                      -> (obj : SVGSVGElement)
                      -> (rect : t1)
                      -> (referenceElement : Maybe t2)
                      -> JSIO NodeList
  getIntersectionList a b c = primJS
                            $ SVGSVGElement.prim__getIntersectionList a
                                                                      (up b)
                                                                      (mayUp c)

  export
  suspendRedraw :  (obj : SVGSVGElement)
                -> (maxWaitMilliseconds : Bits32)
                -> JSIO Bits32
  suspendRedraw a b = primJS $ SVGSVGElement.prim__suspendRedraw a b

  export
  unsuspendRedrawAll : (obj : SVGSVGElement) -> JSIO ()
  unsuspendRedrawAll a = primJS $ SVGSVGElement.prim__unsuspendRedrawAll a

  export
  unsuspendRedraw :  (obj : SVGSVGElement)
                  -> (suspendHandleID : Bits32)
                  -> JSIO ()
  unsuspendRedraw a b = primJS $ SVGSVGElement.prim__unsuspendRedraw a b

namespace SVGScriptElement

  export
  crossOrigin : SVGScriptElement -> Attribute False Maybe String
  crossOrigin v = fromNullablePrim "SVGScriptElement.getcrossOrigin"
                                   prim__crossOrigin
                                   prim__setCrossOrigin
                                   v

  export
  type : SVGScriptElement -> Attribute True I String
  type v = fromPrim "SVGScriptElement.gettype" prim__type prim__setType v

namespace SVGStopElement

  export
  offset : (obj : SVGStopElement) -> JSIO SVGAnimatedNumber
  offset a = primJS $ SVGStopElement.prim__offset a

namespace SVGStringList

  export
  set :  (obj : SVGStringList)
      -> (index : Bits32)
      -> (newItem : String)
      -> JSIO ()
  set a b c = primJS $ SVGStringList.prim__set a b c

  export
  length : (obj : SVGStringList) -> JSIO Bits32
  length a = primJS $ SVGStringList.prim__length a

  export
  numberOfItems : (obj : SVGStringList) -> JSIO Bits32
  numberOfItems a = primJS $ SVGStringList.prim__numberOfItems a

  export
  appendItem : (obj : SVGStringList) -> (newItem : String) -> JSIO String
  appendItem a b = primJS $ SVGStringList.prim__appendItem a b

  export
  clear : (obj : SVGStringList) -> JSIO ()
  clear a = primJS $ SVGStringList.prim__clear a

  export
  getItem : (obj : SVGStringList) -> (index : Bits32) -> JSIO String
  getItem a b = primJS $ SVGStringList.prim__getItem a b

  export
  initialize : (obj : SVGStringList) -> (newItem : String) -> JSIO String
  initialize a b = primJS $ SVGStringList.prim__initialize a b

  export
  insertItemBefore :  (obj : SVGStringList)
                   -> (newItem : String)
                   -> (index : Bits32)
                   -> JSIO String
  insertItemBefore a b c = primJS $ SVGStringList.prim__insertItemBefore a b c

  export
  removeItem : (obj : SVGStringList) -> (index : Bits32) -> JSIO String
  removeItem a b = primJS $ SVGStringList.prim__removeItem a b

  export
  replaceItem :  (obj : SVGStringList)
              -> (newItem : String)
              -> (index : Bits32)
              -> JSIO String
  replaceItem a b c = primJS $ SVGStringList.prim__replaceItem a b c

namespace SVGStyleElement

  export
  media : SVGStyleElement -> Attribute True I String
  media v = fromPrim "SVGStyleElement.getmedia" prim__media prim__setMedia v

  export
  title : SVGStyleElement -> Attribute True I String
  title v = fromPrim "SVGStyleElement.gettitle" prim__title prim__setTitle v

  export
  type : SVGStyleElement -> Attribute True I String
  type v = fromPrim "SVGStyleElement.gettype" prim__type prim__setType v

namespace SVGTextContentElement

  public export
  LENGTHADJUST_SPACING : Bits16
  LENGTHADJUST_SPACING = 1

  public export
  LENGTHADJUST_SPACINGANDGLYPHS : Bits16
  LENGTHADJUST_SPACINGANDGLYPHS = 2

  public export
  LENGTHADJUST_UNKNOWN : Bits16
  LENGTHADJUST_UNKNOWN = 0

  export
  lengthAdjust :  (0 _ : JSType t1)
               => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
               -> (obj : t1)
               -> JSIO SVGAnimatedEnumeration
  lengthAdjust a = primJS $ SVGTextContentElement.prim__lengthAdjust (up a)

  export
  textLength :  (0 _ : JSType t1)
             => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
             -> (obj : t1)
             -> JSIO SVGAnimatedLength
  textLength a = primJS $ SVGTextContentElement.prim__textLength (up a)

  export
  getCharNumAtPosition :  (0 _ : JSType t1)
                       => (0 _ : JSType t2)
                       => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
                       -> {auto 0 _ : Elem DOMPointInit (Types t2)}
                       -> (obj : t1)
                       -> (point : Optional t2)
                       -> JSIO Int32
  getCharNumAtPosition a b = primJS
                           $ SVGTextContentElement.prim__getCharNumAtPosition (up a)
                                                                              (optUp b)

  export
  getCharNumAtPosition' :  (0 _ : JSType t1)
                        => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
                        -> (obj : t1)
                        -> JSIO Int32
  getCharNumAtPosition' a = primJS
                          $ SVGTextContentElement.prim__getCharNumAtPosition (up a)
                                                                             undef

  export
  getComputedTextLength :  (0 _ : JSType t1)
                        => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
                        -> (obj : t1)
                        -> JSIO Double
  getComputedTextLength a = primJS
                          $ SVGTextContentElement.prim__getComputedTextLength (up a)

  export
  getEndPositionOfChar :  (0 _ : JSType t1)
                       => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
                       -> (obj : t1)
                       -> (charnum : Bits32)
                       -> JSIO DOMPoint
  getEndPositionOfChar a b = primJS
                           $ SVGTextContentElement.prim__getEndPositionOfChar (up a)
                                                                              b

  export
  getExtentOfChar :  (0 _ : JSType t1)
                  => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
                  -> (obj : t1)
                  -> (charnum : Bits32)
                  -> JSIO DOMRect
  getExtentOfChar a b = primJS
                      $ SVGTextContentElement.prim__getExtentOfChar (up a) b

  export
  getNumberOfChars :  (0 _ : JSType t1)
                   => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
                   -> (obj : t1)
                   -> JSIO Int32
  getNumberOfChars a = primJS
                     $ SVGTextContentElement.prim__getNumberOfChars (up a)

  export
  getRotationOfChar :  (0 _ : JSType t1)
                    => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
                    -> (obj : t1)
                    -> (charnum : Bits32)
                    -> JSIO Double
  getRotationOfChar a b = primJS
                        $ SVGTextContentElement.prim__getRotationOfChar (up a) b

  export
  getStartPositionOfChar :  (0 _ : JSType t1)
                         => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
                         -> (obj : t1)
                         -> (charnum : Bits32)
                         -> JSIO DOMPoint
  getStartPositionOfChar a b = primJS
                             $ SVGTextContentElement.prim__getStartPositionOfChar (up a)
                                                                                b

  export
  getSubStringLength :  (0 _ : JSType t1)
                     => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
                     -> (obj : t1)
                     -> (charnum : Bits32)
                     -> (nchars : Bits32)
                     -> JSIO Double
  getSubStringLength a b c = primJS
                           $ SVGTextContentElement.prim__getSubStringLength (up a)
                                                                            b
                                                                            c

  export
  selectSubString :  (0 _ : JSType t1)
                  => {auto 0 _ : Elem SVGTextContentElement (Types t1)}
                  -> (obj : t1)
                  -> (charnum : Bits32)
                  -> (nchars : Bits32)
                  -> JSIO ()
  selectSubString a b c = primJS
                        $ SVGTextContentElement.prim__selectSubString (up a) b c

namespace SVGTextPathElement

  public export
  TEXTPATH_METHODTYPE_ALIGN : Bits16
  TEXTPATH_METHODTYPE_ALIGN = 1

  public export
  TEXTPATH_METHODTYPE_STRETCH : Bits16
  TEXTPATH_METHODTYPE_STRETCH = 2

  public export
  TEXTPATH_METHODTYPE_UNKNOWN : Bits16
  TEXTPATH_METHODTYPE_UNKNOWN = 0

  public export
  TEXTPATH_SPACINGTYPE_AUTO : Bits16
  TEXTPATH_SPACINGTYPE_AUTO = 1

  public export
  TEXTPATH_SPACINGTYPE_EXACT : Bits16
  TEXTPATH_SPACINGTYPE_EXACT = 2

  public export
  TEXTPATH_SPACINGTYPE_UNKNOWN : Bits16
  TEXTPATH_SPACINGTYPE_UNKNOWN = 0

  export
  method : (obj : SVGTextPathElement) -> JSIO SVGAnimatedEnumeration
  method a = primJS $ SVGTextPathElement.prim__method a

  export
  spacing : (obj : SVGTextPathElement) -> JSIO SVGAnimatedEnumeration
  spacing a = primJS $ SVGTextPathElement.prim__spacing a

  export
  startOffset : (obj : SVGTextPathElement) -> JSIO SVGAnimatedLength
  startOffset a = primJS $ SVGTextPathElement.prim__startOffset a

namespace SVGTextPositioningElement

  export
  dx :  (0 _ : JSType t1)
     => {auto 0 _ : Elem SVGTextPositioningElement (Types t1)}
     -> (obj : t1)
     -> JSIO SVGAnimatedLengthList
  dx a = primJS $ SVGTextPositioningElement.prim__dx (up a)

  export
  dy :  (0 _ : JSType t1)
     => {auto 0 _ : Elem SVGTextPositioningElement (Types t1)}
     -> (obj : t1)
     -> JSIO SVGAnimatedLengthList
  dy a = primJS $ SVGTextPositioningElement.prim__dy (up a)

  export
  rotate :  (0 _ : JSType t1)
         => {auto 0 _ : Elem SVGTextPositioningElement (Types t1)}
         -> (obj : t1)
         -> JSIO SVGAnimatedNumberList
  rotate a = primJS $ SVGTextPositioningElement.prim__rotate (up a)

  export
  x :  (0 _ : JSType t1)
    => {auto 0 _ : Elem SVGTextPositioningElement (Types t1)}
    -> (obj : t1)
    -> JSIO SVGAnimatedLengthList
  x a = primJS $ SVGTextPositioningElement.prim__x (up a)

  export
  y :  (0 _ : JSType t1)
    => {auto 0 _ : Elem SVGTextPositioningElement (Types t1)}
    -> (obj : t1)
    -> JSIO SVGAnimatedLengthList
  y a = primJS $ SVGTextPositioningElement.prim__y (up a)

namespace SVGTransform

  public export
  SVG_TRANSFORM_MATRIX : Bits16
  SVG_TRANSFORM_MATRIX = 1

  public export
  SVG_TRANSFORM_ROTATE : Bits16
  SVG_TRANSFORM_ROTATE = 4

  public export
  SVG_TRANSFORM_SCALE : Bits16
  SVG_TRANSFORM_SCALE = 3

  public export
  SVG_TRANSFORM_SKEWX : Bits16
  SVG_TRANSFORM_SKEWX = 5

  public export
  SVG_TRANSFORM_SKEWY : Bits16
  SVG_TRANSFORM_SKEWY = 6

  public export
  SVG_TRANSFORM_TRANSLATE : Bits16
  SVG_TRANSFORM_TRANSLATE = 2

  public export
  SVG_TRANSFORM_UNKNOWN : Bits16
  SVG_TRANSFORM_UNKNOWN = 0

  export
  angle : (obj : SVGTransform) -> JSIO Double
  angle a = primJS $ SVGTransform.prim__angle a

  export
  matrix : (obj : SVGTransform) -> JSIO DOMMatrix
  matrix a = primJS $ SVGTransform.prim__matrix a

  export
  type : (obj : SVGTransform) -> JSIO Bits16
  type a = primJS $ SVGTransform.prim__type a

  export
  setMatrix :  (0 _ : JSType t1)
            => {auto 0 _ : Elem DOMMatrix2DInit (Types t1)}
            -> (obj : SVGTransform)
            -> (matrix : Optional t1)
            -> JSIO ()
  setMatrix a b = primJS $ SVGTransform.prim__setMatrix a (optUp b)

  export
  setMatrix' : (obj : SVGTransform) -> JSIO ()
  setMatrix' a = primJS $ SVGTransform.prim__setMatrix a undef

  export
  setRotate :  (obj : SVGTransform)
            -> (angle : Double)
            -> (cx : Double)
            -> (cy : Double)
            -> JSIO ()
  setRotate a b c d = primJS $ SVGTransform.prim__setRotate a b c d

  export
  setScale : (obj : SVGTransform) -> (sx : Double) -> (sy : Double) -> JSIO ()
  setScale a b c = primJS $ SVGTransform.prim__setScale a b c

  export
  setSkewX : (obj : SVGTransform) -> (angle : Double) -> JSIO ()
  setSkewX a b = primJS $ SVGTransform.prim__setSkewX a b

  export
  setSkewY : (obj : SVGTransform) -> (angle : Double) -> JSIO ()
  setSkewY a b = primJS $ SVGTransform.prim__setSkewY a b

  export
  setTranslate :  (obj : SVGTransform)
               -> (tx : Double)
               -> (ty : Double)
               -> JSIO ()
  setTranslate a b c = primJS $ SVGTransform.prim__setTranslate a b c

namespace SVGTransformList

  export
  set :  (obj : SVGTransformList)
      -> (index : Bits32)
      -> (newItem : SVGTransform)
      -> JSIO ()
  set a b c = primJS $ SVGTransformList.prim__set a b c

  export
  length : (obj : SVGTransformList) -> JSIO Bits32
  length a = primJS $ SVGTransformList.prim__length a

  export
  numberOfItems : (obj : SVGTransformList) -> JSIO Bits32
  numberOfItems a = primJS $ SVGTransformList.prim__numberOfItems a

  export
  appendItem :  (obj : SVGTransformList)
             -> (newItem : SVGTransform)
             -> JSIO SVGTransform
  appendItem a b = primJS $ SVGTransformList.prim__appendItem a b

  export
  clear : (obj : SVGTransformList) -> JSIO ()
  clear a = primJS $ SVGTransformList.prim__clear a

  export
  consolidate : (obj : SVGTransformList) -> JSIO (Maybe SVGTransform)
  consolidate a = tryJS "SVGTransformList.consolidate"
                $ SVGTransformList.prim__consolidate a

  export
  createSVGTransformFromMatrix :  (0 _ : JSType t1)
                               => {auto 0 _ : Elem DOMMatrix2DInit (Types t1)}
                               -> (obj : SVGTransformList)
                               -> (matrix : Optional t1)
                               -> JSIO SVGTransform
  createSVGTransformFromMatrix a b = primJS
                                   $ SVGTransformList.prim__createSVGTransformFromMatrix a
                                                                                (optUp b)

  export
  createSVGTransformFromMatrix' : (obj : SVGTransformList) -> JSIO SVGTransform
  createSVGTransformFromMatrix' a = primJS
                                  $ SVGTransformList.prim__createSVGTransformFromMatrix a
                                                                                undef

  export
  getItem : (obj : SVGTransformList) -> (index : Bits32) -> JSIO SVGTransform
  getItem a b = primJS $ SVGTransformList.prim__getItem a b

  export
  initialize :  (obj : SVGTransformList)
             -> (newItem : SVGTransform)
             -> JSIO SVGTransform
  initialize a b = primJS $ SVGTransformList.prim__initialize a b

  export
  insertItemBefore :  (obj : SVGTransformList)
                   -> (newItem : SVGTransform)
                   -> (index : Bits32)
                   -> JSIO SVGTransform
  insertItemBefore a b c = primJS
                         $ SVGTransformList.prim__insertItemBefore a b c

  export
  removeItem : (obj : SVGTransformList) -> (index : Bits32) -> JSIO SVGTransform
  removeItem a b = primJS $ SVGTransformList.prim__removeItem a b

  export
  replaceItem :  (obj : SVGTransformList)
              -> (newItem : SVGTransform)
              -> (index : Bits32)
              -> JSIO SVGTransform
  replaceItem a b c = primJS $ SVGTransformList.prim__replaceItem a b c

namespace SVGUnitTypes

  public export
  SVG_UNIT_TYPE_OBJECTBOUNDINGBOX : Bits16
  SVG_UNIT_TYPE_OBJECTBOUNDINGBOX = 2

  public export
  SVG_UNIT_TYPE_UNKNOWN : Bits16
  SVG_UNIT_TYPE_UNKNOWN = 0

  public export
  SVG_UNIT_TYPE_USERSPACEONUSE : Bits16
  SVG_UNIT_TYPE_USERSPACEONUSE = 1

namespace SVGUseElement

  export
  animatedInstanceRoot : (obj : SVGUseElement) -> JSIO (Maybe SVGElement)
  animatedInstanceRoot a = tryJS "SVGUseElement.animatedInstanceRoot"
                         $ SVGUseElement.prim__animatedInstanceRoot a

  export
  height : (obj : SVGUseElement) -> JSIO SVGAnimatedLength
  height a = primJS $ SVGUseElement.prim__height a

  export
  instanceRoot : (obj : SVGUseElement) -> JSIO (Maybe SVGElement)
  instanceRoot a = tryJS "SVGUseElement.instanceRoot"
                 $ SVGUseElement.prim__instanceRoot a

  export
  width : (obj : SVGUseElement) -> JSIO SVGAnimatedLength
  width a = primJS $ SVGUseElement.prim__width a

  export
  x : (obj : SVGUseElement) -> JSIO SVGAnimatedLength
  x a = primJS $ SVGUseElement.prim__x a

  export
  y : (obj : SVGUseElement) -> JSIO SVGAnimatedLength
  y a = primJS $ SVGUseElement.prim__y a

namespace ShadowAnimation

  export
  new :  (0 _ : JSType t1)
      => (0 _ : JSType t2)
      => {auto 0 _ : Elem Animation (Types t1)}
      -> {auto 0 _ : Elem Animatable (Types t2)}
      -> (source : t1)
      -> (newTarget : t2)
      -> JSIO ShadowAnimation
  new a b = primJS $ ShadowAnimation.prim__new (up a) (up b)

  export
  sourceAnimation : (obj : ShadowAnimation) -> JSIO Animation
  sourceAnimation a = primJS $ ShadowAnimation.prim__sourceAnimation a

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

namespace GetSVGDocument

  export
  getSVGDocument :  (0 _ : JSType t1)
                 => {auto 0 _ : Elem GetSVGDocument (Types t1)}
                 -> (obj : t1)
                 -> JSIO Document
  getSVGDocument a = primJS $ GetSVGDocument.prim__getSVGDocument (up a)

namespace SVGAnimatedPoints

  export
  animatedPoints :  (0 _ : JSType t1)
                 => {auto 0 _ : Elem SVGAnimatedPoints (Types t1)}
                 -> (obj : t1)
                 -> JSIO SVGPointList
  animatedPoints a = primJS $ SVGAnimatedPoints.prim__animatedPoints (up a)

  export
  points :  (0 _ : JSType t1)
         => {auto 0 _ : Elem SVGAnimatedPoints (Types t1)}
         -> (obj : t1)
         -> JSIO SVGPointList
  points a = primJS $ SVGAnimatedPoints.prim__points (up a)

namespace SVGElementInstance

  export
  correspondingElement :  (0 _ : JSType t1)
                       => {auto 0 _ : Elem SVGElementInstance (Types t1)}
                       -> (obj : t1)
                       -> JSIO (Maybe SVGElement)
  correspondingElement a = tryJS "SVGElementInstance.correspondingElement"
                         $ SVGElementInstance.prim__correspondingElement (up a)

  export
  correspondingUseElement :  (0 _ : JSType t1)
                          => {auto 0 _ : Elem SVGElementInstance (Types t1)}
                          -> (obj : t1)
                          -> JSIO (Maybe SVGUseElement)
  correspondingUseElement a = tryJS "SVGElementInstance.correspondingUseElement"
                            $ SVGElementInstance.prim__correspondingUseElement (up a)

namespace SVGFitToViewBox

  export
  preserveAspectRatio :  (0 _ : JSType t1)
                      => {auto 0 _ : Elem SVGFitToViewBox (Types t1)}
                      -> (obj : t1)
                      -> JSIO SVGAnimatedPreserveAspectRatio
  preserveAspectRatio a = primJS
                        $ SVGFitToViewBox.prim__preserveAspectRatio (up a)

  export
  viewBox :  (0 _ : JSType t1)
          => {auto 0 _ : Elem SVGFitToViewBox (Types t1)}
          -> (obj : t1)
          -> JSIO SVGAnimatedRect
  viewBox a = primJS $ SVGFitToViewBox.prim__viewBox (up a)

namespace SVGTests

  export
  requiredExtensions :  (0 _ : JSType t1)
                     => {auto 0 _ : Elem SVGTests (Types t1)}
                     -> (obj : t1)
                     -> JSIO SVGStringList
  requiredExtensions a = primJS $ SVGTests.prim__requiredExtensions (up a)

  export
  systemLanguage :  (0 _ : JSType t1)
                 => {auto 0 _ : Elem SVGTests (Types t1)}
                 -> (obj : t1)
                 -> JSIO SVGStringList
  systemLanguage a = primJS $ SVGTests.prim__systemLanguage (up a)

namespace SVGURIReference

  export
  href :  (0 _ : JSType t1)
       => {auto 0 _ : Elem SVGURIReference (Types t1)}
       -> (obj : t1)
       -> JSIO SVGAnimatedString
  href a = primJS $ SVGURIReference.prim__href (up a)

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

namespace SVGBoundingBoxOptions

  export
  new :  (fill : Optional Bool)
      -> (stroke : Optional Bool)
      -> (markers : Optional Bool)
      -> (clipped : Optional Bool)
      -> JSIO SVGBoundingBoxOptions
  new a b c d = primJS
              $ SVGBoundingBoxOptions.prim__new (toFFI a)
                                                (toFFI b)
                                                (toFFI c)
                                                (toFFI d)

  export
  new' : JSIO SVGBoundingBoxOptions
  new' = primJS $ SVGBoundingBoxOptions.prim__new undef undef undef undef

  export
  clipped :  (0 _ : JSType t)
          => {auto 0 _ : Elem SVGBoundingBoxOptions (Types t)}
          -> t
          -> Attribute True Optional Bool
  clipped v = fromUndefOrPrim "SVGBoundingBoxOptions.getclipped"
                              prim__clipped
                              prim__setClipped
                              False
                              (v :> SVGBoundingBoxOptions)

  export
  fill :  (0 _ : JSType t)
       => {auto 0 _ : Elem SVGBoundingBoxOptions (Types t)}
       -> t
       -> Attribute True Optional Bool
  fill v = fromUndefOrPrim "SVGBoundingBoxOptions.getfill"
                           prim__fill
                           prim__setFill
                           True
                           (v :> SVGBoundingBoxOptions)

  export
  markers :  (0 _ : JSType t)
          => {auto 0 _ : Elem SVGBoundingBoxOptions (Types t)}
          -> t
          -> Attribute True Optional Bool
  markers v = fromUndefOrPrim "SVGBoundingBoxOptions.getmarkers"
                              prim__markers
                              prim__setMarkers
                              False
                              (v :> SVGBoundingBoxOptions)

  export
  stroke :  (0 _ : JSType t)
         => {auto 0 _ : Elem SVGBoundingBoxOptions (Types t)}
         -> t
         -> Attribute True Optional Bool
  stroke v = fromUndefOrPrim "SVGBoundingBoxOptions.getstroke"
                             prim__stroke
                             prim__setStroke
                             False
                             (v :> SVGBoundingBoxOptions)


text:
import Data.String

subtract : Neg a => a -> a -> a
subtract x y = y - x

parse : List Char -> Integer -> Integer
parse (x::xs) =
  case parseInteger (pack xs) of
    Nothing => id
    Just num =>
      case x of
        '+' => (+num)
        '-' => subtract num

loop : Integer -> List (List Char) -> Integer
loop acc lst = foldl (\x, f => f x) acc (map parse lst)

main : IO ()
main = do
  args <- getArgs
  case args of
    (_::arg::_) => do
      file <- readFile arg
      case file of
        Right res => print $ loop 0 $ map unpack (lines res)
        Left _ => putStrLn "File not found"
    _ => putStrLn "Usage: ./appositum input.txt"

ext: idr

max_stars_repo_name: unleashed-coding/advent-of-code

max_issues_repo_name: unleashed-coding/advent-of-code

max_forks_repo_name: unleashed-coding/advent-of-code


text:
module IntegerProofs

%access public export
%default total

||| A decision procedure for `DecEq Integer`
||| @ m the first number
||| @ n the second number
isEq : (m : Integer) -> (n : Integer) -> Dec (m = n)
isEq m n = decEq m n

||| Proofs that `m` is not equal to `n`
||| @ m the first number
||| @ n the second number
NotEq : (m, n : Integer) -> Type
NotEq m n = Not (m=n)

||| Not (m = n) implies m /= n
notEqImpliesNotEq : (contra : (m = n) -> Void) -> ((m = n) -> Void)
notEqImpliesNotEq contra Refl = contra Refl

||| (m = n) implies Not (m /= n)
eqImpliesNotNotEq : (prf : m = n) -> (((m = n) -> Void) -> Void)
eqImpliesNotNotEq Refl f = f Refl

||| A decision procedure for `NotEq`
isNotEq : (m : Integer) -> (n : Integer) -> Dec (NotEq m n)
isNotEq m n = case (isEq m n) of
                   (Yes prf) => No (eqImpliesNotNotEq prf)
                   (No contra) => Yes (notEqImpliesNotEq contra)

smaller : (m : Integer) -> (n : Integer) -> Integer
smaller m n = case m <= n of
                   False => n
                   True => m

sameIntegerCheckPrf : (prf : m = n) -> (n : Integer) -> Integer
sameIntegerCheckPrf Refl n = n

sameInteger : (m : Integer) -> (n : Integer) -> (m=n) -> Integer
sameInteger m n prf = sameIntegerCheckPrf prf n

isTrue : (b : Bool) -> Dec (b = True)
isTrue b = decEq b True

isFalse : (b : Bool) -> Dec (b = False)
isFalse b = decEq b False

max_stars_repo_name: zenntenn/Idris-NumericProofs

max_issues_repo_name: zenntenn/Idris-NumericProofs

max_forks_repo_name: zenntenn/Idris-NumericProofs


text:
import Data.Vect

-- Defining functions by pattern matching
invert : Bool -> Bool
invert True = False
invert False = True

describeList : List Int -> String
describeList [] = "Empty"
describeList (x :: xs) = "Non-empty, tail = " ++ show xs

-- Given just the type declaration below, can use Ctrl-Alt-A in Atom to add a
-- definition.
allLengths_list : List String -> List Nat
-- allLengths_list list = ?rhs -- put the cursor on list and do ctrl-alt-c in
-- Atom to expand the cases as below:
-- allLengths_list [] = ?rhs_1
-- allLengths_list (x :: xs) = ?rhs_2
allLengths_list [] = []
allLengths_list (x :: xs) = length x :: allLengths_list xs
-- Check if allLengths_list is total
-- :total allLengths_list -> Main.allLengths_list is Total

allLengths : Vect len String -> Vect len Nat
allLengths [] = []
allLengths (word :: words) = 0 :: allLengths words

-- :doc List pulls up the documentation for List.
-- In Atom, ctrl-alt-D

-- Data types are defined in terms of their constructors, a bit like Java enum
-- members but often with parameters.

-- mutual lets you define functions that call each other, otherwise Idris
-- requires everything to be top-down.

mutual
  isEven : Nat -> Bool
  isEven Z = True
  isEven (S k) = not $ isOdd k

  isOdd : Nat -> Bool
  isOdd Z = False
  isOdd (S k) = not $ isEven k

fourInts : Vect 4 Int
fourInts = [0, 1, 2, 3]

sixInts : Vect 6 Int
sixInts = [4, 5, 6, 7, 8, 9]

tenInts : Vect 10 Int
tenInts = fourInts ++ sixInts

insert : Ord elem => (x : elem) -> (xs : Vect len elem) -> Vect (S len) elem
insert x [] = [x]
insert x (y :: ys) = if (x < y) then (x :: y :: ys) else (y :: insert x ys)

insertSort : (Ord elem) => Vect n elem -> Vect n elem
insertSort [] = []
insertSort (x :: xs) = insert x (insertSort xs)

my_length : List a -> Nat
my_length [] = Z
my_length (x :: xs) = S (my_length xs)

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

my_map : (a -> b) -> List a -> List b
my_map f [] = []
my_map f (x :: xs) = f x :: my_map f xs

my_vect_map : (a -> b) -> Vect n a -> Vect n b
my_vect_map f [] = []
my_vect_map f (x :: xs) = f x :: my_vect_map f xs

-- total makes sure it won't compile if it's not total, total meaning every
-- scenario is accounted for.

-- I struggled with this, something about two-dimensional arrays seems to cause
-- me problems. Transposing means taking the top row, transposing the rest
-- recursively, then prefixing each transposed row with the values from the top
-- row to form a new column.

-- Ctrl-Alt-T in Atom to find types, only works on the right hand side.
-- Ctrl-Alt-A to add missing cases
-- Ctrl-Alt-C to split out a case by destructuring a particular variable
-- Ctrl-Alt-S to do an expression search, if the type is specific enough it
-- can fill in a right hand side.

createEmpties : Vect n (Vect 0 elem)
createEmpties = replicate _ []

prefixEach : (x : Vect n elem) -> Vect n (Vect k elem) -> Vect n (Vect (S k) elem)
prefixEach [] [] = []
prefixEach (x :: xs) (y :: ys) = (x :: y) :: prefixEach xs ys

total transposeMat : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat [] = createEmpties
transposeMat (x :: xs) = prefixEach x (transposeMat xs)

-- Exercise 1 - reimplement using zipWith

total transposeMat_zipWith : Vect m (Vect n elem) -> Vect n (Vect m elem)
transposeMat_zipWith [] = replicate _ []
transposeMat_zipWith (x :: xs) = zipWith (::) x (transposeMat_zipWith xs)

-- Exercise 2

addMatrix : Num a => Vect n (Vect m a) -> Vect n (Vect m a) -> Vect n (Vect m a)
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = zipWith (+) x y :: addMatrix xs ys

-- Exercise 3

-- [1 2]     [ 7  8  9 10]   [1*7 + 2*11 = 29] -- sum(row 1 * column 1)
-- [3 4]  x  [11 12 13 14] =
-- [5 6]

-- Transposing:
-- [1 2]     [ 7 11]   [1*7 + 2*11, 1*8 + 2*12, 1*9 + 2*13, 1*10 + 2*14]
-- [3 4]  x  [ 8 12] = [3*7 + 4*11, 3*8 + 4*12, 3*9 + 4*13, 3*10 + 4*14]
-- [5 6]     [ 9 13]   [5*7 + 6*11, 5*8 + 6*12, 5*9 + 6*13, 5*10 + 6*14]
--           [10 14]

multMatrix : Num a => Vect n (Vect m a) -> Vect m (Vect p a) -> Vect n (Vect p a)
multMatrix xs ys = multHelper xs (transposeMat_zipWith ys)
  where
    sumOneRow : Num a => Vect m a -> Vect m a -> a
    sumOneRow xs ys = sum (zipWith (*) xs ys)

    multHelper : Num a => Vect n (Vect m a) -> Vect p (Vect m a) -> Vect n (Vect p a)
    multHelper [] _ = []
    multHelper (x :: xs) ys = map (sumOneRow x) ys :: multHelper xs ys

-- Implicit values: _ means infer the value.
-- Implicit parameters: {param: Type} means infer the parameter.

vect_length : Vect n elem -> Nat
vect_length {n} xs = n -- {n} brings the argument into scope

createEmpties_inferred : Vect n (Vect 0 a)
createEmpties_inferred {n = Z} = []
createEmpties_inferred {n = (S k)} = [] :: createEmpties

max_stars_repo_name: rickyclarkson/idris-playground

max_issues_repo_name: rickyclarkson/idris-playground

max_forks_repo_name: rickyclarkson/idris-playground


text:
module Core.Value

import Core.Context
import Core.Core
import Core.Env
import Core.TT

import Libraries.Data.IntMap
import Libraries.Data.NameMap

%default covering

public export
data EvalOrder = CBV | CBN

public export
record EvalOpts where
  constructor MkEvalOpts
  holesOnly : Bool -- only evaluate hole solutions
  argHolesOnly : Bool -- only evaluate holes which are relevant arguments
  removeAs : Bool -- reduce 'as' patterns (don't do this on LHS)
  evalAll : Bool -- evaluate everything, including private names
  tcInline : Bool -- inline for totality checking
  fuel : Maybe Nat -- Limit for recursion depth
  reduceLimit : List (Name, Nat) -- reduction limits for given names. If not
                     -- present, no limit
  strategy : EvalOrder

export
defaultOpts : EvalOpts
defaultOpts = MkEvalOpts False False True False False Nothing [] CBN

export
withHoles : EvalOpts
withHoles = MkEvalOpts True True False False False Nothing [] CBN

export
withAll : EvalOpts
withAll = MkEvalOpts False False True True False Nothing [] CBN

export
withArgHoles : EvalOpts
withArgHoles = MkEvalOpts False True False False False Nothing [] CBN

export
tcOnly : EvalOpts
tcOnly = record { tcInline = True } withArgHoles

export
onLHS : EvalOpts
onLHS = record { removeAs = False } defaultOpts

export
cbn : EvalOpts
cbn = defaultOpts

export
cbv : EvalOpts
cbv = record { strategy = CBV } defaultOpts

mutual
  public export
  data LocalEnv : List Name -> List Name -> Type where
       Nil  : LocalEnv free []
       (::) : Closure free -> LocalEnv free vars -> LocalEnv free (x :: vars)

  public export
  data Closure : List Name -> Type where
       MkClosure : {vars : _} ->
                   (opts : EvalOpts) ->
                   LocalEnv free vars ->
                   Env Term free ->
                   Term (vars ++ free) -> Closure free
       MkNFClosure : EvalOpts -> Env Term free -> NF free -> Closure free

  -- The head of a value: things you can apply arguments to
  public export
  data NHead : List Name -> Type where
       NLocal : Maybe Bool -> (idx : Nat) -> (0 p : IsVar nm idx vars) ->
                NHead vars
       NRef   : NameType -> Name -> NHead vars
       NMeta  : Name -> Int -> List (Closure vars) -> NHead vars

  -- Values themselves. 'Closure' is an unevaluated thunk, which means
  -- we can wait until necessary to reduce constructor arguments
  public export
  data NF : List Name -> Type where
       NBind    : FC -> (x : Name) -> Binder (Closure vars) ->
                  (Defs -> Closure vars -> Core (NF vars)) -> NF vars
       -- Each closure is associated with the file context of the App node that
       -- had it as an argument. It's necessary so as to not lose file context
       -- information when creating the normal form.
       NApp     : FC -> NHead vars -> List (FC, Closure vars) -> NF vars
       NDCon    : FC -> Name -> (tag : Int) -> (arity : Nat) ->
                  List (FC, Closure vars) -> NF vars
       NTCon    : FC -> Name -> (tag : Int) -> (arity : Nat) ->
                  List (FC, Closure vars) -> NF vars
       NAs      : FC -> UseSide -> NF vars -> NF vars -> NF vars
       NDelayed : FC -> LazyReason -> NF vars -> NF vars
       NDelay   : FC -> LazyReason -> Closure vars -> Closure vars -> NF vars
       NForce   : FC -> LazyReason -> NF vars -> List (FC, Closure vars) -> NF vars
       NPrimVal : FC -> Constant -> NF vars
       NErased  : FC -> (imp : Bool) -> NF vars
       NType    : FC -> NF vars

export
ntCon : FC -> Name -> Int -> Nat -> List (FC, Closure vars) -> NF vars
ntCon fc (UN (Basic "Type")) tag Z [] = NType fc
ntCon fc n tag Z [] = case isConstantType n of
  Just c => NPrimVal fc c
  Nothing => NTCon fc n tag Z []
ntCon fc n tag arity args = NTCon fc n tag arity args

export
getLoc : NF vars -> FC
getLoc (NBind fc _ _ _) = fc
getLoc (NApp fc _ _) = fc
getLoc (NDCon fc _ _ _ _) = fc
getLoc (NTCon fc _ _ _ _) = fc
getLoc (NAs fc _ _ _) = fc
getLoc (NDelayed fc _ _) = fc
getLoc (NDelay fc _ _ _) = fc
getLoc (NForce fc _ _ _) = fc
getLoc (NPrimVal fc _) = fc
getLoc (NErased fc i) = fc
getLoc (NType fc) = fc

export
{free : _} -> Show (NHead free) where
  show (NLocal _ idx p) = show (nameAt p) ++ "[" ++ show idx ++ "]"
  show (NRef _ n) = show n
  show (NMeta n _ args) = "?" ++ show n ++ "_[" ++ show (length args) ++ " closures]"

Show (Closure free) where
  show _ = "[closure]"

export
{free : _} -> Show (NF free) where
  show (NBind _ x (Lam _ c info ty) _)
    = "\\" ++ withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++
      " => [closure]"
  show (NBind _ x (Let _ c val ty) _)
    = "let " ++ showCount c ++ show x ++ " : " ++ show ty ++
      " = " ++ show val ++ " in [closure]"
  show (NBind _ x (Pi _ c info ty) _)
    = withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++
      " -> [closure]"
  show (NBind _ x (PVar _ c info ty) _)
    = withPiInfo info ("pat " ++ showCount c ++ show x ++ " : " ++ show ty) ++
      " => [closure]"
  show (NBind _ x (PLet _ c val ty) _)
    = "plet " ++ showCount c ++ show x ++ " : " ++ show ty ++
      " = " ++ show val ++ " in [closure]"
  show (NBind _ x (PVTy _ c ty) _)
    = "pty " ++ showCount c ++ show x ++ " : " ++ show ty ++
      " => [closure]"
  show (NApp _ hd args) = show hd ++ " [" ++ show (length args) ++ " closures]"
  show (NDCon _ n _ _ args) = show n ++ " [" ++ show (length args) ++ " closures]"
  show (NTCon _ n _ _ args) = show n ++ " [" ++ show (length args) ++ " closures]"
  show (NAs _ _ n tm) = show n ++ "@" ++ show tm
  show (NDelayed _ _ tm) = "%Delayed " ++ show tm
  show (NDelay _ _ _ _) = "%Delay [closure]"
  show (NForce _ _ tm args) = "%Force " ++ show tm ++ " [" ++ show (length args) ++ " closures]"
  show (NPrimVal _ c) = show c
  show (NErased _ _) = "[__]"
  show (NType _) = "Type"


text:
module PacketStruct
import IdrisNet.PacketLang
import Data.So

%access public

simpleStruct : PacketLang
simpleStruct = do
  cstring
  lstring 5
  p_either (bits 32) (lstring 4)
  listn 3 cstring
  b1 <- bool
  b2 <- bool
  prop (prop_or (prop_bool b2)
                (prop_bool b1))

myBoundedInt : Bounded 32
myBoundedInt = BInt 9001 Oh

simpleStructInstance : (mkTy simpleStruct)
simpleStructInstance = ("hello" ##
                        "world" ##
                        (Left myBoundedInt) ##
                        ["hello", "you", "dears"] ##
                        True ##
                        False ##
                        (Right Oh))

simpleResponse : PacketLang
simpleResponse = do
  cstring
  cstring

simpleResponseInstance : (mkTy simpleResponse)
simpleResponseInstance = "Got" ## "It!"


text:
||| The \"Main\" module of 'algebra'.
module Main

-- The interface to the 'algebra' project.
import Algebra

||| The \"main\" function of 'algebra'.
main : IO ()
main = putStrLn $ show Answer

max_stars_repo_name: greatBigDot/algebra

max_issues_repo_name: greatBigDot/algebra

max_forks_repo_name: greatBigDot/algebra


text: module LLVM.AST


text:
module Main

StringOrInt : Bool -> Type
StringOrInt x = case x of
  True  => Int
  False => String

getStringOrInt : (x : Bool) -> StringOrInt x
getStringOrInt x = case x of
  True  => 94
  False => "Ninety four"

valToString : (x : Bool) -> StringOrInt x -> String
valToString x val = case x of
  True  => cast val
  False => val

main : IO ()
main = do
  putStrLn (valToString True (getStringOrInt True))
  putStrLn (valToString False (getStringOrInt False))

max_stars_repo_name: pdani/idris-grin

max_issues_repo_name: pdani/idris-grin

max_forks_repo_name: pdani/idris-grin


text:
module System.File.Support

%default total

public export
support : String -> String
support fn = "C:" ++ fn ++ ", libidris2_support, idris_file.h"

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


text:
module Main

import Replica
import Replica.Options
import Replica.RunEnv

import System

%default total

usage : String
usage = "Usage: replica <test path> [<test path>*]"

optionsToRunargs : Options -> List RunEnv
optionsToRunargs (MkOptions interactive tests) = MkRunEnv interactive <$> tests

covering
main : IO ()
main = do
  (_ :: args) <- getArgs
    | other => putStrLn usage
  let opts = options args
  for_ (optionsToRunargs opts) \env => do
    result <- runTest env
    displayTestResult env.path result

max_stars_repo_name: xvw/REPLica

max_issues_repo_name: xvw/REPLica

max_forks_repo_name: xvw/REPLica


text:
module Main

import VirtualDOM
import VirtualDOM.DOM

listStyle : String
listStyle = "color: green; background-color: pink"

appRoot : JS_IO Node
appRoot = getElementById "app-root"

mutual
  html1 : Html
  html1 =
    node "div" [] []
      [ node "button" [ on "click" (const main1) noOptions ] [] [ text "Toggle list" ]
      ]

  html2 : Html
  html2 =
    node "div" [] []
      [ node "span" [] []
        [ node "button" [ on "click" (const main2) noOptions ]
          [] [ text "Toggle list" ]
        ]
      , node "ol" [] [("style", "display:none"), ("style", listStyle)]
        [ node "li" [] [] [text "Wash the dishes"]
        , node "li" [] [] [text "Grate the carrots"]
        , node "li" [] [] [text "Investigate new extensions to Hindley-Milner"]
        ]
      ]

  main1 : JS_IO ()
  main1 = do
    root <- appRoot
    render root (Just html1) (Just html2)

  main2 : JS_IO ()
  main2 = do
    root <- appRoot
    render root (Just html2) (Just html1)

main : JS_IO ()
main = do
  root <- appRoot
  render root Nothing (Just html1)

max_stars_repo_name: concert/idris-vdom

max_issues_repo_name: concert/idris-vdom

max_forks_repo_name: concert/idris-vdom


text:
module Replica.App.Log

import Control.App
import Control.App.Console

import Replica.App.Replica
import Replica.Option.Global
import Replica.Other.Decorated

%default total

export
interface Log e where
  logWithLevel : (lvl : LogLevel) -> (content : String) -> App e ()

export
log : Log e => String -> App e ()
log = logWithLevel Info

export
debug : Log e => String -> App e ()
debug = logWithLevel Debug

export
warning : Log e => String -> App e ()
warning = logWithLevel Warning

export
critical : Log e => String -> App e ()
critical = logWithLevel Critical

export
Console e => State GlobalConfig Global e => Log e where
  logWithLevel lvl content = do
    Just threshold <- map logLevel $ get GlobalConfig
      | Nothing => pure ()
    if lvl >= threshold
       then putStrLn content
       else pure ()

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
||| Drawing a pumpkin for Halloween

module Pumpkin

import Data.Nat
import Data.Vect
import NCurses

%default covering

||| We'll need color, don't care about the keypad and want to block
||| until users either toggle ('t') or quit ('q')
CFG : Config
CFG = MkConfig
  { noDelayEnabled = False
  , keypadEnabled  = False
  , colorEnabled   = True
  }

main : IO ()
main = runNCurses $ NCurses.do
  -- Initialise curses
  cBreak
  noEcho
  clear
  -- we need start color for initColorPair to make sense
  startColor
  setCursorVisibility CInvisible

  -- Initialise colours
  orange <- initColorPair 1 Black Yellow
  green  <- initColorPair 2 Green Green
  black  <- initColorPair 3 Black Black
  red    <- initColorPair 4 Red   Red

  -- Draw the stalk (parts will be overwritten by the body)
  nSetAttr (CP green)
  mvHLine (MkPosition { row = 0, col = 18 }) ' ' 4
  mvHLine (MkPosition { row = 1, col = 20 }) ' ' 4
  mvHLine (MkPosition { row = 2, col = 20 }) ' ' 4
  mvHLine (MkPosition { row = 3, col = 20 }) ' ' 6
  mvHLine (MkPosition { row = 4, col = 18 }) ' ' 10
  mvHLine (MkPosition { row = 5, col = 18 }) ' ' 10

  -- Draw the pumpkin's body (parts will be overriden by the holes)
  nSetAttr (CP orange)
  mvHLine (MkPosition { row = 3,  col = 8  }) ' ' 8
  mvHLine (MkPosition { row = 3,  col = 28 }) ' ' 8
  mvHLine (MkPosition { row = 4,  col = 6  }) ' ' 12
  mvHLine (MkPosition { row = 4,  col = 28 }) ' ' 10
  mvHLine (MkPosition { row = 5,  col = 4  }) ' ' 14
  mvHLine (MkPosition { row = 5,  col = 20 }) ' ' 2
  mvHLine (MkPosition { row = 5,  col = 24 }) ' ' 2
  mvHLine (MkPosition { row = 5,  col = 28 }) ' ' 12
  mvHLine (MkPosition { row = 6,  col = 2  }) ' ' 40
  mvHLine (MkPosition { row = 7,  col = 2  }) ' ' 40
  mvHLine (MkPosition { row = 8,  col = 0  }) ' ' 44
  mvHLine (MkPosition { row = 9,  col = 0  }) ' ' 44
  mvHLine (MkPosition { row = 10, col = 0  }) ' ' 44
  mvHLine (MkPosition { row = 11, col = 0  }) ' ' 44
  mvHLine (MkPosition { row = 12, col = 0  }) ' ' 44
  mvHLine (MkPosition { row = 13, col = 0  }) ' ' 44
  mvHLine (MkPosition { row = 14, col = 2  }) ' ' 40
  mvHLine (MkPosition { row = 15, col = 2  }) ' ' 40
  mvHLine (MkPosition { row = 16, col = 4  }) ' ' 36
  mvHLine (MkPosition { row = 17, col = 6  }) ' ' 30
  mvHLine (MkPosition { row = 18, col = 10 }) ' ' 10
  mvHLine (MkPosition { row = 18, col = 24 }) ' ' 10

  -- Draw the holes
  nSetAttr (CP black)
  mvHLine (MkPosition { row = 7,  col = 14 }) ' ' 2
  mvHLine (MkPosition { row = 7,  col = 30 }) ' ' 2
  mvHLine (MkPosition { row = 8,  col = 12 }) ' ' 6
  mvHLine (MkPosition { row = 8,  col = 28 }) ' ' 6
  mvHLine (MkPosition { row = 9,  col = 10 }) ' ' 10
  mvHLine (MkPosition { row = 9,  col = 22 }) ' ' 2
  mvHLine (MkPosition { row = 9,  col = 26 }) ' ' 10
  mvHLine (MkPosition { row = 10, col = 20 }) ' ' 6
  mvHLine (MkPosition { row = 11, col = 18 }) ' ' 10
  mvHLine (MkPosition { row = 13, col = 10 }) ' ' 6
  mvHLine (MkPosition { row = 13, col = 20 }) ' ' 8
  mvHLine (MkPosition { row = 13, col = 32 }) ' ' 6
  mvHLine (MkPosition { row = 14, col = 12 }) ' ' 24
  mvHLine (MkPosition { row = 15, col = 14 }) ' ' 20
  mvHLine (MkPosition { row = 16, col = 16 }) ' ' 6
  mvHLine (MkPosition { row = 16, col = 26 }) ' ' 4

  react red black

  where

    eyes : ColorPair -> NCurses CFG CFG ()
    eyes col = do
      nSetAttr (CP col)
      mvHLine (MkPosition { row = 8, col = 14 }) ' ' 2
      mvHLine (MkPosition { row = 8, col = 30 }) ' ' 2

    react : (red, black : ColorPair) -> NCurses CFG CFG ()
    react red black
      = do c <- getCh
           -- swapping red for black means turning the eyes on/off
           let p = ifThenElse (c == 't') (black, red) (red, black)
           eyes (snd p)
           when (c /= 'q') $ uncurry react p

max_stars_repo_name: gallais/ncurses-idris

max_issues_repo_name: gallais/ncurses-idris

max_forks_repo_name: gallais/ncurses-idris


text:
module Product_Type_Eq

%access public export
%default total

||| A proof that equality for product types are generate by the equalities of the componenets

Product_Eq_property_1 : (ty1, ty2 : Type) -> (a, b : (ty1, ty2)) ->
                        ( (fst a) = (fst b) ) -> ( (snd a) = (snd b) ) ->
                        ( a = b )

Product_Eq_property_1 ty1 ty2 (x, y) (x, y) Refl Refl = Refl


text:
module LightClick.Types.WireType

import Decidable.Equality

import Toolkit.Decidable.Informative

%default total

public export
data Wire : Type where
   Data      : Wire
   Address   : Wire
   Clock     : Wire
   Reset     : Wire
   Info      : Wire
   Interrupt : Wire
   Control   : Wire
   General   : Wire

dataNotAddress : (Data = Address) -> Void
dataNotAddress Refl impossible

dataNotClock : (Data = Clock) -> Void
dataNotClock Refl impossible

dataNotReset : (Data = Reset) -> Void
dataNotReset Refl impossible

dataNotInfo : (Data = Info) -> Void
dataNotInfo Refl impossible

dataNotInterrupt : (Data = Interrupt) -> Void
dataNotInterrupt Refl impossible

dataNotControl : (Data = Control) -> Void
dataNotControl Refl impossible

dataNotGeneral : (Data = General) -> Void
dataNotGeneral Refl impossible

addressNotClock : (Address = Clock) -> Void
addressNotClock Refl impossible

addressNotReset : (Address = Reset) -> Void
addressNotReset Refl impossible

addressNotInfo : (Address = Info) -> Void
addressNotInfo Refl impossible

addressNotInterrupt : (Address = Interrupt) -> Void
addressNotInterrupt Refl impossible

addressNotControl : (Address = Control) -> Void
addressNotControl Refl impossible

addressNotGeneral : (Address = General) -> Void
addressNotGeneral Refl impossible

clockNotReset : (Clock = Reset) -> Void
clockNotReset Refl impossible

clockNotInfo : (Clock = Info) -> Void
clockNotInfo Refl impossible

clockNotInterrupt : (Clock = Interrupt) -> Void
clockNotInterrupt Refl impossible

clockNotControl : (Clock = Control) -> Void
clockNotControl Refl impossible

clockNotGeneral : (Clock = General) -> Void
clockNotGeneral Refl impossible

resetNotInfo : (Reset = Info) -> Void
resetNotInfo Refl impossible

resetNotInterrupt : (Reset = Interrupt) -> Void
resetNotInterrupt Refl impossible

resetNotControl : (Reset = Control) -> Void
resetNotControl Refl impossible

resetNotGeneral : (Reset = General) -> Void
resetNotGeneral Refl impossible

infoNotInterrupt : (Info = Interrupt) -> Void
infoNotInterrupt Refl impossible

infoNotControl : (Info = Control) -> Void
infoNotControl Refl impossible

infoNotGeneral : (Info = General) -> Void
infoNotGeneral Refl impossible

interruptNotControl : (Interrupt = Control) -> Void
interruptNotControl Refl impossible

interruptNotGeneral : (Interrupt = General) -> Void
interruptNotGeneral Refl impossible

controlNotGeneral : (Control = General) -> Void
controlNotGeneral Refl impossible

export
DecEq Wire where
  decEq Data Data = Yes Refl
  decEq Data Address = No dataNotAddress
  decEq Data Clock = No dataNotClock
  decEq Data Reset = No dataNotReset
  decEq Data Info = No dataNotInfo
  decEq Data Interrupt = No dataNotInterrupt
  decEq Data Control = No dataNotControl
  decEq Data General = No dataNotGeneral

  decEq Address Data = No (negEqSym dataNotAddress)
  decEq Address Address = Yes Refl
  decEq Address Clock = (No addressNotClock)
  decEq Address Reset = (No addressNotReset)
  decEq Address Info = (No addressNotInfo)
  decEq Address Interrupt = (No addressNotInterrupt)
  decEq Address Control = (No addressNotControl)
  decEq Address General = (No addressNotGeneral)

  decEq Clock Data = No (negEqSym dataNotClock)
  decEq Clock Address = No (negEqSym addressNotClock)
  decEq Clock Clock = Yes Refl
  decEq Clock Reset = No clockNotReset
  decEq Clock Info = No clockNotInfo
  decEq Clock Interrupt = No clockNotInterrupt
  decEq Clock Control = No clockNotControl
  decEq Clock General = No clockNotGeneral

  decEq Reset Data = No (negEqSym dataNotReset)
  decEq Reset Address = No (negEqSym addressNotReset)
  decEq Reset Clock = No (negEqSym clockNotReset)
  decEq Reset Reset = Yes Refl
  decEq Reset Info = No resetNotInfo
  decEq Reset Interrupt = No resetNotInterrupt
  decEq Reset Control = No resetNotControl
  decEq Reset General = No resetNotGeneral

  decEq Info Data = No (negEqSym dataNotInfo)
  decEq Info Address = No (negEqSym addressNotInfo)
  decEq Info Clock = No (negEqSym clockNotInfo)
  decEq Info Reset = No (negEqSym resetNotInfo)
  decEq Info Info = Yes Refl
  decEq Info Interrupt = No infoNotInterrupt
  decEq Info Control = No infoNotControl
  decEq Info General = No infoNotGeneral

  decEq Interrupt Data = No (negEqSym dataNotInterrupt)
  decEq Interrupt Address = No (negEqSym addressNotInterrupt)
  decEq Interrupt Clock = No (negEqSym clockNotInterrupt)
  decEq Interrupt Reset = No (negEqSym resetNotInterrupt)
  decEq Interrupt Info = No (negEqSym infoNotInterrupt)
  decEq Interrupt Interrupt = Yes Refl
  decEq Interrupt Control = No interruptNotControl
  decEq Interrupt General = No interruptNotGeneral

  decEq Control Data = No (negEqSym dataNotControl)
  decEq Control Address = No (negEqSym addressNotControl)
  decEq Control Clock = No (negEqSym clockNotControl)
  decEq Control Reset = No (negEqSym resetNotControl)
  decEq Control Info = No (negEqSym infoNotControl)
  decEq Control Interrupt = No (negEqSym interruptNotControl)
  decEq Control Control = Yes Refl
  decEq Control General = No controlNotGeneral

  decEq General Data = No (negEqSym dataNotGeneral)
  decEq General Address = No (negEqSym addressNotGeneral)
  decEq General Clock = No (negEqSym clockNotGeneral)
  decEq General Reset = No (negEqSym resetNotGeneral)
  decEq General Info = No (negEqSym infoNotGeneral)
  decEq General Interrupt = No (negEqSym interruptNotGeneral)
  decEq General Control = No (negEqSym controlNotGeneral)
  decEq General General = Yes Refl

public export
data Compatible : (l,r : Wire) -> Type
  where
    SameWire : Compatible w       w
    GAny     : Compatible General a
    AnyG     : Compatible a       General

negCompatibleSym : (Compatible l r -> Void) -> Compatible r l -> Void
negCompatibleSym f SameWire = f SameWire
negCompatibleSym f GAny = f AnyG
negCompatibleSym f AnyG = f GAny

daNotCompat : Compatible Data Address -> Void
daNotCompat SameWire impossible
daNotCompat GAny impossible
daNotCompat AnyG impossible

dcNotCompat : Compatible Data Clock -> Void
dcNotCompat SameWire impossible
dcNotCompat GAny impossible
dcNotCompat AnyG impossible

drNotCompat : Compatible Data Reset -> Void
drNotCompat SameWire impossible
drNotCompat GAny impossible
drNotCompat AnyG impossible

ddNotCompat : Compatible Data Info -> Void
ddNotCompat SameWire impossible
ddNotCompat GAny impossible
ddNotCompat AnyG impossible

diNotCompat : Compatible Data Interrupt -> Void
diNotCompat SameWire impossible
diNotCompat GAny impossible
diNotCompat AnyG impossible

dctrlNotCompat : Compatible Data Control -> Void
dctrlNotCompat SameWire impossible
dctrlNotCompat GAny impossible
dctrlNotCompat AnyG impossible

acNotCompat : Compatible Address Clock -> Void
acNotCompat SameWire impossible
acNotCompat GAny impossible
acNotCompat AnyG impossible

arNotCompat : Compatible Address Reset -> Void
arNotCompat SameWire impossible
arNotCompat GAny impossible
arNotCompat AnyG impossible

aiNotCompat : Compatible Address Info -> Void
aiNotCompat SameWire impossible
aiNotCompat GAny impossible
aiNotCompat AnyG impossible

aitNotCompat : Compatible Address Interrupt -> Void
aitNotCompat SameWire impossible
aitNotCompat GAny impossible
aitNotCompat AnyG impossible

actrlNotCompat : Compatible Address Control -> Void
actrlNotCompat SameWire impossible
actrlNotCompat GAny impossible
actrlNotCompat AnyG impossible

crNotCompat : Compatible Clock Reset -> Void
crNotCompat SameWire impossible
crNotCompat GAny impossible
crNotCompat AnyG impossible

ciNotCompat : Compatible Clock Info -> Void
ciNotCompat SameWire impossible
ciNotCompat GAny impossible
ciNotCompat AnyG impossible

cintNotCompat : Compatible Clock Interrupt -> Void
cintNotCompat SameWire impossible
cintNotCompat GAny impossible
cintNotCompat AnyG impossible

ccNotCompatc : Compatible Clock Control -> Void
ccNotCompatc SameWire impossible
ccNotCompatc GAny impossible
ccNotCompatc AnyG impossible

riNotCompat : Compatible Reset Info -> Void
riNotCompat SameWire impossible
riNotCompat GAny impossible
riNotCompat AnyG impossible

rintNotCompat : Compatible Reset Interrupt -> Void
rintNotCompat SameWire impossible
rintNotCompat GAny impossible
rintNotCompat AnyG impossible

rcNotCompat : Compatible Reset Control -> Void
rcNotCompat SameWire impossible
rcNotCompat GAny impossible
rcNotCompat AnyG impossible

infoINotCompat : Compatible Info Interrupt -> Void
infoINotCompat SameWire impossible
infoINotCompat GAny impossible
infoINotCompat AnyG impossible

infoCNotCompat : Compatible Info Control -> Void
infoCNotCompat SameWire impossible
infoCNotCompat GAny impossible
infoCNotCompat AnyG impossible

interCNotCompat : Compatible Interrupt Control -> Void
interCNotCompat SameWire impossible
interCNotCompat GAny impossible
interCNotCompat AnyG impossible

namespace Compatibility
  namespace Wire
    public export
    data Error = TypesDiffer Wire Wire

export
compatible : (l,r : Wire) -> DecInfo Compatibility.Wire.Error (Compatible l r)
compatible a@Data      b@Data      = Yes SameWire
compatible a@Data      b@Address   = No (TypesDiffer a b) daNotCompat
compatible a@Data      b@Clock     = No (TypesDiffer a b) dcNotCompat
compatible a@Data      b@Reset     = No (TypesDiffer a b) drNotCompat
compatible a@Data      b@Info      = No (TypesDiffer a b) ddNotCompat
compatible a@Data      b@Interrupt = No (TypesDiffer a b) diNotCompat
compatible a@Data      b@Control   = No (TypesDiffer a b) dctrlNotCompat
compatible a@Data      b@General   = Yes AnyG
compatible a@Address   b@Data      = No (TypesDiffer a b) $ negCompatibleSym daNotCompat
compatible a@Address   b@Address   = Yes SameWire
compatible a@Address   b@Clock     = No (TypesDiffer a b) acNotCompat
compatible a@Address   b@Reset     = No (TypesDiffer a b) arNotCompat
compatible a@Address   b@Info      = No (TypesDiffer a b) aiNotCompat
compatible a@Address   b@Interrupt = No (TypesDiffer a b) aitNotCompat
compatible a@Address   b@Control   = No (TypesDiffer a b) actrlNotCompat
compatible a@Address   b@General   = Yes AnyG
compatible a@Clock     b@Data      = No (TypesDiffer a b) (negCompatibleSym dcNotCompat)
compatible a@Clock     b@Address   = No (TypesDiffer a b) (negCompatibleSym acNotCompat)
compatible a@Clock     b@Clock     = Yes SameWire
compatible a@Clock     b@Reset     = No (TypesDiffer a b) crNotCompat
compatible a@Clock     b@Info      = No (TypesDiffer a b) ciNotCompat
compatible a@Clock     b@Interrupt = No (TypesDiffer a b) cintNotCompat
compatible a@Clock     b@Control   = No (TypesDiffer a b) ccNotCompatc
compatible a@Clock     b@General   = Yes AnyG
compatible a@Reset     b@Data      = No (TypesDiffer a b) (negCompatibleSym drNotCompat)
compatible a@Reset     b@Address   = No (TypesDiffer a b) (negCompatibleSym arNotCompat)
compatible a@Reset     b@Clock     = No (TypesDiffer a b) (negCompatibleSym crNotCompat)
compatible a@Reset     b@Reset     = Yes SameWire
compatible a@Reset     b@Info      = No (TypesDiffer a b) riNotCompat
compatible a@Reset     b@Interrupt = No (TypesDiffer a b) rintNotCompat
compatible a@Reset     b@Control   = No (TypesDiffer a b) rcNotCompat
compatible a@Reset     b@General   = Yes AnyG
compatible a@Info      b@Data      = No (TypesDiffer a b) (negCompatibleSym ddNotCompat)
compatible a@Info      b@Address   = No (TypesDiffer a b) (negCompatibleSym aiNotCompat)
compatible a@Info      b@Clock     = No (TypesDiffer a b) (negCompatibleSym ciNotCompat)
compatible a@Info      b@Reset     = No (TypesDiffer a b) (negCompatibleSym riNotCompat)
compatible a@Info      b@Info      = Yes SameWire
compatible a@Info      b@Interrupt = No (TypesDiffer a b) infoINotCompat
compatible a@Info      b@Control   = No (TypesDiffer a b) infoCNotCompat
compatible a@Info      b@General   = Yes AnyG
compatible a@Interrupt b@Data      = No (TypesDiffer a b) (negCompatibleSym diNotCompat)
compatible a@Interrupt b@Address   = No (TypesDiffer a b) (negCompatibleSym aitNotCompat)
compatible a@Interrupt b@Clock     = No (TypesDiffer a b) (negCompatibleSym cintNotCompat)
compatible a@Interrupt b@Reset     = No (TypesDiffer a b) (negCompatibleSym rintNotCompat)
compatible a@Interrupt b@Info      = No (TypesDiffer a b) (negCompatibleSym infoINotCompat)
compatible a@Interrupt b@Interrupt = Yes SameWire
compatible a@Interrupt b@Control   = No (TypesDiffer a b) interCNotCompat
compatible a@Interrupt b@General   = Yes AnyG
compatible a@Control   b@Data      = No (TypesDiffer a b) (negCompatibleSym dctrlNotCompat)
compatible a@Control   b@Address   = No (TypesDiffer a b) (negCompatibleSym actrlNotCompat)
compatible a@Control   b@Clock     = No (TypesDiffer a b) (negCompatibleSym ccNotCompatc)
compatible a@Control   b@Reset     = No (TypesDiffer a b) (negCompatibleSym rcNotCompat)
compatible a@Control   b@Info      = No (TypesDiffer a b) (negCompatibleSym infoCNotCompat)
compatible a@Control   b@Interrupt = No (TypesDiffer a b) (negCompatibleSym interCNotCompat)

compatible Control Control = Yes SameWire
compatible Control General = Yes AnyG
compatible General r = Yes GAny

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Circuits.Common.Lexer

import public Text.Lexer

import public Toolkit.Text.Lexer.Run

%default total

public export
record LangSpec where
  constructor W
  symbols : List String
  keywords : List String
  commentLine : String
  commentBlock : Pair String String
  docLine      : Maybe String
  docBlock     : Maybe (Pair String String)

public export
data Identifier = MkIdentifier String

export
Eq Identifier where
  (==) (MkIdentifier x) (MkIdentifier y) = x == y

public export
data Token = ID String
             | Keyword String
             | LineComment String
             | BlockComment String
             | Documentation String
             | LitNat Nat
             | Symbol String
             | WS String
             | NotRecognised String
             | EndInput

export
Eq Token where
  (==) (ID x) (ID y) = x == y
  (==) (LineComment x) (LineComment y) = x == y
  (==) (BlockComment x) (BlockComment y) = x == y
  (==) (LitNat x) (LitNat y) = x == y
  (==) (Documentation x) (Documentation y) = x == y
  (==) (Keyword x) (Keyword y) = x == y
  (==) (Symbol x) (Symbol y) = x == y
  (==) (WS x) (WS y) = x == y
  (==) (NotRecognised x) (NotRecognised y) = x == y
  (==) EndInput EndInput = True
  (==) _ _ = False

showToken : Show a => String -> a -> String
showToken n a = "(" <+> n <+> " " <+> show a <+> ")"

export
Show Token where
  show (ID id)             = showToken "ID" id
  show (Keyword str)       = showToken "Keyword" str
  show (LineComment str)   = showToken "LineComment" str
  show (BlockComment str)  = showToken "BlockComment" str
  show (Documentation str) = showToken "Documentation" str

  show (LitNat n) = showToken "Nat" n

  show (Symbol s) = showToken "Symbol" s
  show (WS ws) = "WS"
  show (NotRecognised s) = showToken "Urgh" s
  show EndInput          = "EndInput"

identifier : Lexer
identifier = pred startIdent <+> many (pred validIdent)
  where
    startIdent : Char -> Bool
    startIdent x = isAlpha x

    validIdent : Char -> Bool
    validIdent '_' = True
    validIdent x = isAlphaNum x

tokenMap : LangSpec -> TokenMap Token
tokenMap (W symbols keywords comL (comBL, comBR) docLM docBM)
    = with List
        [
          (space, WS)
        , (lineComment (exact comL), LineComment)
        , (blockComment (exact comBL) (exact comBR), BlockComment)
        ]
        ++
          maybe [] (\dL => [(lineComment (exact dL), Documentation)])
                   docLM
        ++
          maybe [] (\dB
                     => [
                          (blockComment (exact (fst dB)) (exact (snd dB)), Documentation)
                        ])
                   docBM
        ++
        [
          (digits, \x => LitNat (integerToNat $ cast {to=Integer} x))
        ]
        ++
           map (\x => (exact x, Symbol)) symbols
        ++
        [
          (identifier, (\x => if elem x keywords then Keyword x else ID x))
        , (any, NotRecognised)
        ]

keep : WithBounds Token -> Bool
keep (MkBounded t _ _) = case t of
    BlockComment _ => False
    LineComment  _ => False
    WS           _ => False
    _              => True

namespace Circuits
  namespace Common

    export
    langSpec : List String -> List String -> LangSpec
    langSpec symbols keywords
      = W symbols
          keywords
          "//"
          ("/*", "*/")
          Nothing
          (Just ("/**", "**/"))

    export
    Lexer : LangSpec -> Lexer Token
    Lexer spec = MkLexer (Common.Lexer.tokenMap spec) (keep) EndInput

    export
    lexString : LangSpec -> String -> Either LexError (List (WithBounds Token))
    lexString spec = lexString (Lexer spec)

    export
    lexFile : LangSpec -> String -> IO $ Either LexFail (List (WithBounds Token))
    lexFile spec = lexFile (Lexer spec)

-- [ EOF ]

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
module Conway

import Control.Comonad
import Control.Comonad.Store.Representable
import Data.Fuel
import Data.Functor.Representable
import Data.List
import Data.String
import Data.Vect
import System

%default total

public export
Grid : Nat -> Nat -> Type -> Type
Grid n m = Store (Vect n . Vect m) {rep = Compose}

public export
Coord : Nat -> Nat -> Type
Coord n m = (Fin n, Fin m)

public export
Rule : Nat -> Nat -> Type
Rule n m = Grid n m Bool -> Bool

public export
mkGrid : {n : Nat} -> {m : Nat} -> List (Coord (S n) (S m)) -> Grid (S n) (S m) Bool
mkGrid coords = store @{Compose} (`elem` coords) (0, 0)

public export
showGrid : Grid n m Bool -> String
showGrid (MkStore xss _) = unlines . map (foldMap (bool "  " "██")) . toList $ xss
  where
    bool : a -> a -> Bool -> a
    bool x y = \case
      True => y
      False => x

public export
conway : {n : Nat} -> {m : Nat} -> Rule n m
conway g =
  (alive && (aliveCount == 2 || aliveCount == 3)) || (not alive && aliveCount == 3)
  where
    alive : Bool
    alive = extract g

    incWrap : {n : Nat} -> Fin n -> Fin n
    incWrap {n = S _} x = fromMaybe FZ . strengthen $ FS x

    sucWrap : {n : Nat} -> Fin n -> Fin n
    sucWrap {n = 0} _ impossible
    sucWrap FZ = last
    sucWrap (FS x) = weaken x

    neighbors : (Fin n, Fin m) -> List (Fin n, Fin m)
    neighbors (x, y) =
      [ (incWrap x, sucWrap y), (incWrap x, y), (incWrap x, incWrap y)
      , (x,         sucWrap y),                 (x,         incWrap y)
      , (sucWrap x, sucWrap y), (sucWrap x, y), (sucWrap x, incWrap y)
      ]

    aliveCount : Nat
    aliveCount = length . filter id . experiment neighbors $ g

public export
runLife : {n : Nat} -> {m : Nat} -> Rule n m -> Grid n m Bool -> Fuel -> IO ()
runLife _ _ Dry = pure ()
runLife r g (More fuel) = do
  putStr "\ESC[2J"
  putStr $ showGrid g
  usleep 500000
  runLife r (g =>> r) fuel

max_stars_repo_name: pnotequalnp/game-of-life

max_issues_repo_name: pnotequalnp/game-of-life

max_forks_repo_name: pnotequalnp/game-of-life