text:
import SimpleFFI

dartUI : Lib
dartUI = MkLib "dartUI" "dart:ui"

gestures : Lib
gestures = MkLib "gestures" "package:flutter/gestures.dart"

painting : Lib
painting = MkLib "gestures" "package:flutter/painting.dart"

widgets : Lib
widgets = MkLib "widgets" "package:flutter/widgets.dart"

material : Lib
material = MkLib "material" "package:flutter/material.dart"

foundation : Lib
foundation = MkLib "foundation" "package:flutter/foundation.dart"

flutter : Module
flutter = defModule "Flutter.FFI" [
  defLib foundation [
    defClass "Key" [
    ]
  ],
  defLib painting [
    defClass "TextStyle" [
      defConstructor "" [
          named "Color" "backgroundColor",
          named "Color" "color",
          named double "fontSize"
      ],
      final "TextAlign" "textAlign"
    ],
    defClass "AlignmentGeometry" [
    ],
    defClass "Alignment" [
      extends "AlignmentGeometry",
      defConst "Alignment" "centerLeft",
      defConst "Alignment" "centerRight"
    ],

    defClass "NetworkImage" [
      defConstructor "" [
        positional string "src"
      ]
    ]

  ],
  defLib material [
    defClass "MaterialColor" [
    ],
    defClass "Colors" [
      defConst "MaterialColor" "black",
      defConst "MaterialColor" "blue",
      defConst "MaterialColor" "brown",
      defConst "MaterialColor" "cyan",
      defConst "MaterialColor" "green",
      defConst "MaterialColor" "grey",
      defConst "MaterialColor" "purple",
      defConst "MaterialColor" "red",
      defConst "MaterialColor" "transparent",
      defConst "MaterialColor" "white",
      defConst "MaterialColor" "yellow"
    ],
    defClass "VisualDensity" [
      defConst "VisualDensity" "adaptivePlatformDensity"
    ],
    defClass "TextTheme" [
      final "TextStyle" "headline1",
      final "TextStyle" "headline2",
      final "TextStyle" "headline3",
      final "TextStyle" "headline4"
    ],
    defClass "Theme" [
      defStatic "of" [positional "BuildContext" "context"] "ThemeData"
    ],
    defClass "ThemeData" [
      defConstructor "" [
        named "MaterialColor" "primarySwatch",
        named "VisualDensity" "visualDensity"
      ],
      final "TextTheme" "textTheme"
    ],
    defClass "ButtonStyle" [
      defConstructor "" [
          named "Color" "backgroundColor"
      ],
      final "TextAlign" "textAlign"
    ],
    defClass "Scaffold" [
      extends "Widget",
      defConstructor "" [
        named "Widget" "appBar",
        named "Widget" "body",
        named "Widget" "floatingActionButton",
        named "Color" "backgroundColor",
        named bool "resizeToAvoidBottomPadding"
      ]
    ],
    defClass "AppBar" [
      extends "Widget",
      defConstructor "" [
        named "Widget" "title"
      ]
    ],
    defClass "Icons" [
      defConst "IconData" "add",
      defConst "IconData" "add_circle_outline",
      defConst "IconData" "remove",
      defConst "IconData" "remove_circle_outline",
      defConst "IconData" "play_arrow",
      defConst "IconData" "stop",
      defConst "IconData" "stop_circle",
      defConst "IconData" "stop_circle_outlined",
      defConst "IconData" "stop_circle_rounded",
      defConst "IconData" "stop_circle_sharp",
      defConst "IconData" "stop_outlined",
      defConst "IconData" "stop_rounded"
    ],
    defClass "IconButton" [
      extends "Widget",
      defConstructor "" [
        named (function [] void) "onPressed",
        named string "tooltip",
        named "Widget" "icon",
        named "AlignmentGeometry" "alignment"
      ]
    ],
    defClass "FloatingActionButton" [
      extends "Widget",
      defConstructor "" [
        named (function [] void) "onPressed",
        named string "tooltip",
        named "Widget" "child"
      ]
    ],

    defClass "TextButton" [
      extends "Widget",
      defConstructor "" [
        named (function [] void) "onPressed",
        named "ButtonStyle" "style",
        named "Widget" "child"
        ],
      defStatic "styleFrom" [
        named "Color" "primary",
        named "Color" "backgroundColor"
      ] "ButtonStyle"
    ],

    defClass "InputDecoration" [
      defConstructor "" [
        named string "labelText",
        named "TextStyle" "labelStyle",
        named "Color" "fillColor",
        named bool "filled"
      ]
    ],

    defClass "TextField" [
      extends "Widget",
      defConstructor "" [
        named "InputDecoration" "decoration",
        named "TextStyle" "style",
        named bool "obscureText",
        named (function [string] void) "onChanged"
      ]
    ],

    defClass "Slider" [
      extends "Widget",
      defConstructor "" [
        named double "value",
        named (function [double] void) "onChanged",
        named (function [double] void) "onChangeStart",
        named (function [double] void) "onChangeEnd",
        named double "min",
        named double "max",
        named int "divisions",
        named string "label"
      ]
    ],

    defClass "MaterialPageRoute" [
      extends "Widget",
      defConstructor "" [
        named (function ["WidgetBuilder"] "Widget") "builder"
      ]
    ],

    defClass "MaterialApp" [
      extends "Widget",
      defConstructor "" [
        named string "title",
        named "Widget" "home",
        named "ThemeData" "theme"
      ]
    ]
  ],
  defLib widgets [
    defEnum "MainAxisAlignment" [
      "start", "end", "center", "spaceBetween", "spaceAround", "spaceEvenly"
    ],
    defClass "IconData" [
    ],
    defClass "Icon" [
      extends "Widget",
      defConstructor "" [
        positional "IconData" "icon",
        named "Key" "key"
      ]
    ],
    defClass "Widget" [
    ],
    defClass "BuildContext" [
    ],
    defClass "WidgetBuilder" [
      defConstructor "" [
        positional "BuildContext" "context"
      ]
    ],

    defClass "Container" [
      extends "Widget",
      defConstructor "" [
        named "Widget" "child"
      ]
    ],

    defClass "SizedBox" [
      extends "Widget",
      defConstructor "" [
        named double "width",
        named double "height"
      ]
    ],

    defClass "Center" [
      extends "Widget",
      defConstructor "" [
        named "Widget" "child"
      ]
    ],
    defClass "Column" [
      extends "Widget",
      defConstructor "" [
        named (listOf "Widget") "children",
        named "MainAxisAlignment" "mainAxisAlignment"
      ]
    ],
    defClass "Expanded" [
      extends "Widget",
      defConstructor "" [
        named "Widget" "child"
      ]
    ],
    defClass "Row" [
      extends "Widget",
      defConstructor "" [
        named (listOf "Widget") "children",
        named "MainAxisAlignment" "mainAxisAlignment"
      ]
    ],

    defClass "Route" [
      extends "Widget",
      defConstructor "" [
      ]
    ],

    defClass "Navigator" [
      extends "Widget",
      defStatic "push" [
        positional "BuildContext" "context",
        positional "MaterialPageRoute" "materialPageRoute"
      ] void
    ],

    defClass "Text" [
      extends "Widget",
      defConstructor "" [
        positional string "text",
        named double "textScaleFactor",
        named "TextStyle" "style",
        named "TextAlign" "textAlign"
      ]
    ],

    defClass "Image" [
      extends "Widget",
      defConstructor "" [
        named "NetworkImage" "image"
      ]
    ],

    defClass "GestureDetector" [
      extends "Widget",
      defConstructor "" [
        named "Key" "key",
        named "Widget" "child",
        named (function ["TapDownDetails"] void) "onTapDown",
        named (function ["TapUpDetails"] void) "onTapUp",
        named (function [] void) "onTap",
        named (function [] void) "onTapCancel",
        named (function [] void) "onSecondaryTap",
        named (function [] void) "onSecondaryTapCancel",
        named (function [] void) "onDoubleTap",
        named (function [] void) "onDoubleTapCancel",
        named (function ["TapDownDetails"] void) "onSecondaryTapDown",
        named (function ["TapUpDetails"] void) "onSecondaryTapUp",
        named (function [] void) "onLongPress",
        named (function ["LongPressStartDetails"] void) "onLongPressStart",
        named (function ["LongPressMoveUpdateDetails"] void) "onLongPressMoveUpdate",
        named (function ["LongPressEndDetails"] void) "onLongPressEnd"
      ]
    ],
    defClass "CustomPaint" [
      extends "Widget",
      defConstructor "" [
        named "Key" "key",
        named "Widget" "child",
        named "CustomPainter" "painter",
        named "CustomPainter" "foregroundPainter",
        named "Size" "size",
        named bool "isComplex",
        named bool "willChange"
      ]
    ],
    defClass "CustomPainter" [
    ]
  ],
  defLib dartUI [
    defEnum "AppLifecycleState" [
      "detached",
      "inactive",
      "paused",
      "resumed"
    ],
    defClass "Color" [
      defConstructor "" [
        positional int "value"
      ]
    ],
    defClass "Canvas" [
      defIO "drawPath" [
        positional "Path" "path",
        positional "Paint" "paint"
      ] void
    ],
    defEnum "PaintingStyle" [
      "stroke"
    ],
    defClass "Paint" [
      defConstructor "" [],
      var "PaintingStyle" "style",
      var double "strokeWidth"
    ],
    defClass "Offset" [
      defConstructor "" [positional double "dx", positional double "dy"],
      final double "dx",
      final double "dy"
    ],
    defClass "Size" [
      final double "width",
      final double "height"
    ],
    defClass "Path" [
      defConstructor "" [],
      defIO "moveTo" [positional double "x", positional double "y"] void,
      defIO "lineTo" [positional double "x", positional double "y"] void
    ],
    defClass "Velocity" [
      final "Offset" "pixelsPerSecond"
    ],
    defEnum "TextAlign" ["left", "right", "center", "start", "end", "justify"]
  ],
  defLib gestures [
    defClass "TapDownDetails" [
      final "Offset" "globalPosition",
      final "Offset" "localPosition"
    ],
    defClass "TapUpDetails" [
      final "Offset" "globalPosition",
      final "Offset" "localPosition"
    ],
    defClass "LongPressStartDetails" [
      final "Offset" "globalPosition",
      final "Offset" "localPosition"
    ],
    defClass "LongPressMoveUpdateDetails" [
      final "Offset" "localOffsetFromOrigin",
      final "Offset" "localPosition"
    ],
    defClass "LongPressEndDetails" [
      final "Offset" "globalPosition",
      final "Offset" "localPosition"
    ]
  ]
]

main : IO ()
main = renderModule flutter


text:
module Dbcritic.Config

import Control.IOExcept
import Dbcritic.Check
import Dbcritic.Interface

public export
record Silence where
    constructor MkSilence

    silenceCheck : String
    silenceIssue : List String

public export
record Config where
    constructor MkConfig

    ||| For a check any issue that matches the issue prefix will not be
    ||| reported. These issues are called silenced issues.
    silences : List Silence

export
getSilences : Config -> Check -> List Silence
getSilences config check =
    filter ((==) (identifier check) . silenceCheck)
        (silences config)

silences : Silence -> Issue -> Bool
silences silence issue =
    (silenceIssue silence) `isPrefixOf` (identifier issue)

export
isSilenced : List Silence -> Issue -> Bool
isSilenced allSilences issue = any (`silences` issue) allSilences

export
silencesIssue : List Issue -> Silence -> Bool
silencesIssue allIssues silence = any (silence `silences`) allIssues

export
formatSilence : Int -> Silence -> String
formatSilence index silence =
    formatMessage index description problems solutions
    where
    description = "Unneeded silence directive"
    problems = ["You may reintroduce the resolved issue."]
    solutions = ["Unsilence this issue or check by removing: ‘silence " ++
        unwords (silenceCheck silence :: silenceIssue silence) ++ "’."]

||| Parse configuration that was already read from a file.
||| See README.md for a description of the configuration file format.
export
parseConfig : String -> Either String Config
parseConfig = foldlM parseLine emptyConfig . map words . lines
    where

    emptyConfig : Config
    emptyConfig = MkConfig []

    parseLine : Config -> List String -> Either String Config

    -- Skip empty lines and comment lines.
    parseLine config []         = Right config
    parseLine config ("#" :: _) = Right config

    -- Parse silence directives.
    parseLine config ("silence" :: check :: issue) =
        let
            silence = MkSilence check issue
        in
            Right $ record { silences $= (silence ::) } config
    parseLine config ("silence" :: []) =
        Left "Empty silence directive"

    -- Anything else is an error.
    parseLine config (directive :: _) =
        Left ("Unknown directive: ‘" ++ directive ++ "’")

||| Read configuration from a file and then parse it.
||| See README.md for a description of the configuration file format.
export
readConfig : String -> IOExcept String Config
readConfig path = IOM $ do
    let context = path ++ ": "
    let handle  = either (Left . (context ++) . show) Right
    contents <- handle <$> readFile path
    pure $ contents >>= parseConfig

ext: idr

max_stars_repo_name: channable/dbcritic

max_issues_repo_name: channable/dbcritic

max_forks_repo_name: channable/dbcritic


text:
> module SequentialDecisionProblems.examples.LeftAheadRight

> import Data.Fin
> import Control.Isomorphism

> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Sigma.Sigma

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

> ||| Left, Ahead or Right
> data LeftAheadRight = Left | Ahead | Right

> implementation Eq LeftAheadRight where
>   (==) Left   Left = True
>   (==) Left      _ = False
>   (==) Ahead Ahead = True
>   (==) Ahead     _ = False
>   (==) Right Right = True
>   (==) Right     _ = False

> implementation Show LeftAheadRight where
>   show Left  = "L"
>   show Ahead = "A"
>   show Right = "R"

LeftAheadRight is finite:

> to : LeftAheadRight -> Fin 3
> to Left  =        FZ
> to Ahead =     FS FZ
> to Right = FS (FS FZ)

> from : Fin 3 -> LeftAheadRight
> from             FZ   = Left
> from         (FS FZ)  = Ahead
> from     (FS (FS FZ)) = Right
> from (FS (FS (FS k))) = absurd k

> toFrom : (k : Fin 3) -> to (from k) = k
> toFrom             FZ   = Refl
> toFrom         (FS FZ)  = Refl
> toFrom     (FS (FS FZ)) = Refl
> toFrom (FS (FS (FS k))) = absurd k

> fromTo : (a : LeftAheadRight) -> from (to a) = a
> fromTo Left  = Refl
> fromTo Ahead = Refl
> fromTo Right = Refl

> finiteLeftAheadRight : Finite LeftAheadRight
> finiteLeftAheadRight = MkSigma 3 (MkIso to from toFrom fromTo)
> %freeze finiteLeftAheadRight

LeftAheadRight is non empty:

> cardNotZLeftAheadRight : CardNotZ finiteLeftAheadRight
> cardNotZLeftAheadRight = cardNotZLemma finiteLeftAheadRight Left
> %freeze cardNotZLeftAheadRight

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
> module Double.Postulates

> import Data.So

> import Double.Predicates

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

* Arithmetic

> |||
> postulate
> plusZeroLeftNeutral : {x : Double} -> 0.0 + x = x

> |||
> postulate
> plusZeroRightNeutral : {x : Double} -> x + 0.0 = x

> |||
> postulate
> multZeroLeftZero : {x : Double} -> 0.0 * x = 0.0

> |||
> postulate
> multZeroRightZero : {x : Double} -> x * 0.0 = 0.0

> |||
> postulate
> minusSelfZero : {x : Double} -> x - x = 0.0

> |||
> postulate
> plusAssociative : (x : Double) -> (y : Double) -> (z : Double) ->
>                   x + (y + z) = (x + y) + z

* |LTE|:

> ||| LTE is reflexive
> postulate
> reflexiveLTE : (x : Double) -> x `LTE` x

> ||| LTE is transitive
> postulate
> transitiveLTE : (x, y, z : Double) -> x `LTE` y -> y `LTE` z -> x `LTE` z

> ||| LTE is monotone w.r.t. addition
> postulate
> monotonePlusLTE : {a, b, c, d : Double} ->
>                   a `LTE` b -> c `LTE` d -> a + c `LTE` b + d

> ||| LTE is monotone w.r.t. multiplication
> postulate
> monotoneMultLTE : {a, b, c, d : Double} ->
>                   a `LTE` b -> c `LTE` d -> a * c `LTE` b * d

> ||| LTE is monotone w.r.t. "subtraction of a const"
> postulate
> monotoneMinusConstLTE : {a, b, c : Double} ->
>                         a `LTE` b -> a - c `LTE` b - c

> ||| LTE is monotone w.r.t. "division by a const"
> postulate
> monotoneDivConstLTE : {a, b, c : Double} ->
>                       a `LTE` b -> Positive c -> a / c `LTE` b / c

> ||| LTE is unique
> postulate
> uniqueLTE : {x, y : Double} -> (p : x `LTE` y) -> (q : x `LTE` y) -> p = q

* |LT|:

> ||| LT is unique
> postulate
> uniqueLT : {x, y : Double} -> (p : x `LT` y) -> (q : x `LT` y) -> p = q

* Non-negative double precision floating point numbers:

> ||| Non-negative |Double|s are closed w.r.t. "subtraction"
> postulate
> minusPreservesNonNegativity : {x, y : Double} ->
>                               NonNegative x -> NonNegative y -> y `LTE` x -> NonNegative (x - y)

> ||| Non-negative |Double|s are closed w.r.t. division
> postulate
> divPreservesNonNegativity : {x, y : Double} ->
>                             NonNegative x -> NonNegative y -> NonNegative (x / y)

* Positive double precision floating point numbers:

> |||
> postulate
> positivePlusAnyPositive : {x, y : Double} ->
>                           Positive x -> NonNegative y -> Positive (x + y)

> ||| Positive |Double|s are closed w.r.t. division
> postulate
> divPreservesPositivity : {x, y : Double} ->
>                          Positive x -> Positive y -> Positive (x / y)

> |||
> postulate
> divPositiveSelfOne : {x : Double} -> Positive x -> x / x = 1.0

> |||
> postulate
> divZeroPositiveZero : {x : Double} -> Positive x -> 0.0 / x = 0.0

* Ord methods:

> |||
> postulate
> gtLT : {x, y : Double} -> So (x > y) -> So (y < x)

> postulate
> notCompareEQ : {x, y : Double} -> Not (So (x == y)) -> Not (EQ = compare x y)


text:
import Data.String

main : IO ()
main = do printLn (lines "")
          printLn (lines "ab")
          printLn (lines "ab\n")
          printLn (lines "ab\ncd")
          printLn (lines "ab\ncd\n")
          printLn (lines "a\rb")
          printLn (lines "a\r\nb")
          printLn (lines "\n\r\n\n")


text:
module Test.Lexer

import Test.Generators
import Text.Lexer
import Text.WebIDL.Lexer
import Text.WebIDL.Encoder

lex : String -> Either String (List IdlToken)
lex s = map (map val) $ lexIdl s

prop_identifier : Property
prop_identifier = property $ do
                    i <- forAll identifier
                    lex i.value === Right [Ident i]

prop_space : Property
prop_space = property $ do
               s <- forAll space
               lex s === Right [Space]

prop_stringLit : Property
prop_stringLit = property $ do
                   v <- forAll stringLit
                   lex v.value === Right [SLit v]

prop_intLit : Property
prop_intLit = property $ do
                n <- forAll intLit
                footnote ("Encoded: " ++ intLit n)
                lex (intLit n) === Right [ILit n]

prop_floatLit : Property
prop_floatLit = property $ do
                  n <- forAll floatLit
                  lex (floatLit n) === Right [FLit n]

prop_comment : Property
prop_comment = property $ do
                 s <- forAll comment
                 lex s === Right [Comment s]

prop_other : Property
prop_other = property $ do
               v <- forAll symbol
               lex (symbol v) === Right [Other v]

export
props : Group
props = MkGroup "Lexer Properties"
          [ ("prop_identifier", prop_identifier)
          , ("prop_space", prop_space)
          , ("prop_stringLit", prop_stringLit)
          , ("prop_intLit", prop_intLit)
          , ("prop_floatLit", prop_floatLit)
          , ("prop_comment", prop_comment)
          , ("prop_other", prop_other)
          ]


text:
module Cordial.Model.Common.Source

import Cordial.Model.Common.Essential

%default total
%access public export

{-

p -Always-> p
c <-Always- p
p -> c
c <- p
p/c <-> c/p

SRC SRC
SRC IP
IP  SRC
IP  IP

-}

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Mrk.Elements

import public Data.List

import public Mrk.Attributes
import public Mrk.NodeNames

%default total
%access public export

mutual
  data Element : (parent : NodeName) -> Type where
    Generic : (el : NodeName) ->
              (attrs : List Attribute) ->
              (children : Element el) ->
              {auto prf : el `HasParent` parent} ->
              {auto prfAttrsAllowed : disallowedAttrs el attrs = []} ->
              Element parent
    Link : (rel : LinkType) ->
           (href : URI) ->
           (optionalAttrs : List Attribute) ->
           {auto placement : Link `HasParent` parent} ->
           {auto attrsAllowed : disallowedAttrs Link optionalAttrs = []} ->
           Element parent
    Img : (src : URI) ->
          (alt : String) ->
          (optionalAttrs : List Attribute) ->
          {auto placement : Img `HasParent` parent} ->
          {auto attrsAllowed : disallowedAttrs Img optionalAttrs = []} ->
          Element parent
    Head : List Attribute ->
           (children : Element Head) ->
           {auto oneTitle : numTitles children = 1} ->
           {auto metaPositionValid : ValidMetaPosition children} ->
           Element Html
    Meta : (firstAttr : Attribute) ->
           (attrs : List Attribute) ->
           {auto prf : isValidMetaFirstAttr firstAttr = True} ->
           {auto attrsAllowed : disallowedAttrs Meta attrs = []} ->
           Element parent
    AnchorHyperlink : (href : URI) ->
                      (attrs : List Attribute) ->
                      (children : Element A) ->
                      {auto placement : A `HasParent` parent} ->
                      {auto attrsAllowed : disallowedAttrs A attrs = []} ->
                      Element parent
    AnchorPlaceholder : (children : Element A) ->
                        {auto placement : A `HasParent` parent} ->
                        Element parent
    Text : String -> Element parent
    Collection : (existing : Element parent) ->
                 (new : Element parent) ->
                 Element parent

  isValidMetaFirstAttr : (attr : Attribute) -> Bool
  isValidMetaFirstAttr (Charset _) = True
  isValidMetaFirstAttr _ = False

  firstChildMetaCharset : Element el -> Bool
  firstChildMetaCharset (Meta (Charset _) _) = True
  firstChildMetaCharset (Collection (Meta (Charset _) _) _) = True
  firstChildMetaCharset _ = False

  metaCharsetCount : (children : Element el) -> Nat
  metaCharsetCount (Meta (Charset _) _) = 1
  metaCharsetCount (Collection (Meta (Charset _) _) rest) = 1 + metaCharsetCount rest
  metaCharsetCount (Collection _ rest) = metaCharsetCount rest
  metaCharsetCount _ = 0

  data ValidMetaPosition : (children : Element el) -> Type where
    FirstChildIsMetaCharset : {auto prf : firstChildMetaCharset children = True} ->
                              ValidMetaPosition children
    NoMetaCharset : {auto prf : metaCharsetCount children = 0} ->
                    ValidMetaPosition children

  disallowedAttrs : NodeName -> List Attribute -> List Attribute
  disallowedAttrs nodeName attrs = filter (not . attrPermitted nodeName) attrs where
    attrPermitted : NodeName -> Attribute -> Bool
    attrPermitted Html (Lang _) = True
    attrPermitted Link (Href _) = True
    attrPermitted Link (MimeType _) = True
    attrPermitted _ (ClassNames _) = True
    attrPermitted A (Rel _) = True
    attrPermitted _ _ = False

  numTitles : Element Head -> Nat
  numTitles (Generic Title xs children) = 1
  numTitles (Collection existing new) = numTitles existing + numTitles new
  numTitles _ = 0

  flowContent : List NodeName
  flowContent =
    [ H 1
    , H 2
    , H 3
    , H 4
    , H 5
    , H 6
    , Div
    , Ul
    , P
    , Img
    ] ++ phrasingContent

  phrasingContent : List NodeName
  phrasingContent =
    interactivePhrasingContent ++ nonInteractivePhrasingContent

  interactivePhrasingContent : List NodeName
  interactivePhrasingContent =
    [ A
    ]

  nonInteractivePhrasingContent : List NodeName
  nonInteractivePhrasingContent =
    [
    ]

  HasParent : (child : NodeName) -> (parent : NodeName) -> Type
  HasParent child parent = child `Elem` childrenOf parent where
    childrenOf : NodeName -> List NodeName
    childrenOf Root = [Html]
    childrenOf Html = [Head, Body]
    childrenOf Head = [Link, Meta, Title]
    childrenOf Meta = []
    childrenOf Title = []
    childrenOf Link = []
    childrenOf (H n) = phrasingContent
    childrenOf Img = []
    childrenOf Body = flowContent
    childrenOf Div = flowContent
    childrenOf P = phrasingContent
    childrenOf Ul = [Li]
    childrenOf Li = flowContent
    childrenOf A = nonInteractivePhrasingContent

Semigroup (Element parent) where
  (<+>) = Collection

Monoid (Element parent) where
  neutral = Text ""

showAttrs : List Attribute -> String
showAttrs [] = ""
showAttrs xs = " " ++ unwords (map show xs)

openTag : NodeName -> List Attribute -> String
openTag name attrs = "<" ++ show name ++ showAttrs attrs ++ ">"

closeTag : NodeName -> String
closeTag name = "</" ++ show name ++ ">"

mutual
  openCloseTag : NodeName -> List Attribute -> Element _ -> String
  openCloseTag name attrs children =
    openTag name attrs ++ show children ++ closeTag name

  Show (Element parent) where
    show (Generic el attrs (Text "")) =
      openTag el attrs
    show (Generic Html attrs children) =
      "<!doctype html>" ++
      openCloseTag Html attrs children
    show (Generic el attrs children) =
      openCloseTag el attrs children
    show (Head attrs children) =
      openCloseTag Head attrs children
    show (Meta attr attrs) =
      openTag Meta (attr :: attrs)
    show (Link rel href attrs) =
      openTag Link (Rel rel :: Href href :: attrs)
    show (Img src alt attrs) =
      openTag Img (Src src :: Alt alt :: attrs)
    show (AnchorHyperlink href attrs children) =
      openCloseTag A (Href href :: attrs) children
    show (AnchorPlaceholder children) =
      openCloseTag A [] children
    show (Text s) =
      s
    show (Collection x y) =
      show x ++ show y

max_stars_repo_name: camelpunch/mrk

max_issues_repo_name: camelpunch/mrk

max_forks_repo_name: camelpunch/mrk


text:
module Main

import Data.Fin
import Data.Vect

--------------------------------------------------------------------------------
-- Player

data Player = X | O | N  -- N means nobody
instance Eq Player where
    X == X = True
    O == O = True
    N == N = True
    _ == _ = False
instance Show Player where
    show X = "X"
    show O = "O"
    show N = " "

otherPlayer : Player -> Player
otherPlayer p = case p of
    X => O
    O => X
    N => N

--------------------------------------------------------------------------------
-- BoardSquares (and accessors)

BoardSquares : Type
BoardSquares = Vect 9 Player

blankBoardSquares : BoardSquares
blankBoardSquares = [N,N,N,N,N,N,N,N,N]

rows : BoardSquares -> Vect 3 (Vect 3 Player)
rows [a,b,c,d,e,f,g,h,i] = [[a,b,c],[d,e,f],[g,h,i]]

cols : BoardSquares -> Vect 3 (Vect 3 Player)
cols sqs = transpose (rows sqs)

--------------------------------------------------------------------------------
-- Board (and Accessors)

record Board : Type where
    MkBoard : (squares : BoardSquares) ->
              (whoseTurn : Player) -> Board

initialBoard : Board
initialBoard = MkBoard blankBoardSquares X

BoardLocation : Type
BoardLocation = Fin 9

{-
-- TODO: Need to fix type of (+) in the standard library first.
--       Should be:      (Fin n) -> (Fin m) -> (Fin (n + m - 1))
--       But is instead: (Fin n) -> (Fin m) -> (Fin (n + m))
mkBoardLocation : Fin 3 -> Fin 3 -> BoardLocation
mkBoardLocation x y =
    (y + y + y) + x
     3   5   7    9
 -}

square : Board -> BoardLocation -> Player
square b loc =
    index loc (squares b)

isPositionOccupied : Board -> BoardLocation -> Bool
isPositionOccupied b loc =
    (square b loc) /= N

--------------------------------------------------------------------------------
-- winner : BoardSquares -> Maybe Player

allEqTo : Eq t => t -> Vect n t -> Bool
allEqTo e Nil       = True
allEqTo e (x :: xs) = if x == e then (allEqTo e xs)
                                else False

allEq : Eq t => Vect n t -> Bool
allEq Nil       = True
allEq (x :: xs) = allEqTo x xs

winnerInList : Vect (S n') Player -> Maybe Player
winnerInList (x :: xs) =
    let isWinner = allEq (x :: xs) in
    if isWinner then if x /= N then Just x
                               else Nothing
                else Nothing

-- TODO: Surely this is in the standard library...
firstJust : Vect n (Maybe t) -> Maybe t
firstJust Nil       = Nothing
firstJust (m :: ms) =
    case m of
        Nothing => firstJust ms
        Just x  => Just x

-- TODO: Surely this is in the standard library...
firstJust' : List (Maybe t) -> Maybe t
firstJust' Nil       = Nothing
firstJust' (m :: ms) =
    case m of
        Nothing => firstJust' ms
        Just x  => Just x

winnerRowCol : BoardSquares -> Maybe Player
winnerRowCol sqs = firstJust' [firstJust (map winnerInList (rows sqs)),
                               firstJust (map winnerInList (cols sqs))]

winnerDiag : BoardSquares -> Maybe Player
winnerDiag [a,b,c,d,e,f,g,h,i] =
    if      a == e && e == i && a /= N then Just a
    else if c == e && e == g && c /= N then Just c
                                       else Nothing

{-
-- TODO: Surely this is in the standard library...
-- TODO: Figure out why I can't match on Nil. Compile error.
-- TODO: Rename "eType" to "E" without confusing the compiler.
-- TODO: Reorder arguments to be: Vect n eType -> eType -> Maybe (Fin n)
indexOf : Eq eType => {n:Nat} -> eType -> Vect n eType -> Maybe (Fin n)
indexOf {n} e v =
    case v of
        Nil =>
            Nothing
        x::xs =>
            case (x == e) of
                True =>
                    Just (the (Fin n) 0)
                False =>
                    case (indexOf e xs) of
                        Just index => index + 1  -- NOTE: requires linear memory
                        Nothing    => Nothing
-}

-- TODO: Surely this is in the standard library...
contains : Eq eType => Vect n eType -> eType -> Bool
contains Nil e =
    False
contains (x::xs) e =
    (e == x) || (contains xs e)

winnerTie : BoardSquares -> Maybe Player
winnerTie sqs =
    if (contains sqs N) then Nothing
                        else Just N

winner : BoardSquares -> Maybe Player
winner sqs = firstJust' [winnerRowCol sqs, winnerDiag sqs, winnerTie sqs]

--------------------------------------------------------------------------------
-- Board Mutators

-- TODO: Exercise: Refuse to play at an occupied location at *compile* time
-- TODO: Exercise: Refuse to play if there is a winner at *compile* time
move : Board -> BoardLocation -> Maybe Board
move b loc =
    if (not (isJust (winner (squares b)))) &&
       (not (isPositionOccupied b loc)) then
        Just (MkBoard (replaceAt loc (whoseTurn b) (squares b))
                                  (otherPlayer (whoseTurn b)))
    else
        Nothing

-- TODO: Implement a takeMoveBack method
-- TODO: Exercise: Refuse to take back a move on an empty board at *compile* time

--------------------------------------------------------------------------------
-- Main

-- NOTE: Implementation is probably quadratic time unless recursive string
--       appends are specially optimized. Unlikely.
--
-- TODO: Figure out how to make this work with (List String)
--       in addition to (Vect n String). Probably some kind of
--       type generalization is required.
intercalateAcc : String -> Vect n String -> String -> String
intercalateAcc separator Nil result =
    result
intercalateAcc separator (x::xs) result =
    intercalateAcc separator xs (result ++ separator ++ x)

intercalate : String -> Vect n String -> String
intercalate separator Nil =
    ""
intercalate separator (x::xs) =
    intercalateAcc separator xs x

formatCell : Player -> String
formatCell cell =
    " " ++ (show cell) ++ " "

formatBoardRow : Vect 3 Player -> String
formatBoardRow row =
    intercalate "|" (map formatCell row)

formatBoardSquares : BoardSquares -> String
formatBoardSquares sqs =
    intercalate "\n---|---|---\n" (map formatBoardRow (rows sqs))

formatBoard : Board -> String
formatBoard board =
    formatBoardSquares (squares board)

inputFin : (n:Nat) -> IO (Fin n)
inputFin n = do
    line <- getLine
    -- TODO: Detect and reject non-integer input
    let int = the Integer (cast line)
    case (integerToFin int n) of
        Just int' => return int'
        Nothing   => inputFin n  -- out of bounds; try again

runGame : Board -> IO ()
runGame board = do
    putStrLn (formatBoard board)
    putStrLn ""
    case (winner (squares board)) of
        Just theWinner =>
            case theWinner of
                N => putStrLn "Tie!"
                _ => putStrLn ((show theWinner) ++ " wins!")
        Nothing => do
            putStr "Next move? (0-8) "
            loc' <- inputFin 9
            putStrLn ""
            let loc = the BoardLocation loc'
            case (move board loc) of
                Just newBoard => runGame newBoard
                Nothing       => runGame board    -- illegal move; try again

main : IO ()
main = do
    runGame initialBoard

max_stars_repo_name: davidfstr/tic-tac-idris

max_issues_repo_name: davidfstr/tic-tac-idris

max_forks_repo_name: davidfstr/tic-tac-idris


text:
module Corecursive

import Control.Isomorphism

mutual
  data A = MkA B
  data B = MkB A

interface Isomorphism a b where

  iso : Either a b -> Either a b

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
module Derive.Newtype

import public Derive.Common
import        Util
%language ElabReflection

-- Derivaton of newtypes, datatypes with a single constructor and single field.
-- Currently just supporting simple types without parameteres and indexes.

-- Some common typeclass methods are provided as well. Technically newtype could
-- derive any typeclass its constituent has but that is a little more involved.

newtypeName : TTImp -> Maybe Name
newtypeName (IVar _ n) = Just n
newtypeName (IApp _ (IVar _ n) r) = Just n
newtypeName _ = Nothing

isNewtype : Name -> Elab Bool
isNewtype n0 = do
    [(ncon,ty)] <- constructors n0
      | _ => pure False
    pure $ fieldCount ty == 1
  where
    fieldCount : TTImp -> Int
    fieldCount (IPi _ _ ExplicitArg _ _ retty) = 1 + fieldCount retty
    fieldCount (IPi _ _ _ _ _ retty) = fieldCount retty
    fieldCount _ = 0

-- combine our checks into one spot:
-- 1. is a given TTImp possibly representing a type
-- 2. does it have exactly one constructor and one explicit field
||| Given a TTImp name it possibly a Name of some newtype and the single data
||| constructor of that newtype.
checkNewtype : TTImp -> Elab (Name, (Name, TTImp))
checkNewtype ttimp = do
  Just typename <- pure $ newtypeName ttimp
    | _ => fail "Failed to resolve type name"
  guard !(isNewtype typename) $ show typename ++ " is not a newtype."
  [onlyconstructor] <- constructors typename
    | _ => fail "Error in checkNewtype"
  pure (typename,onlyconstructor)

-------------------------------------------------

-- We use TTImp instead of Name because in name quotation on primtypes `{{Int}}
-- is not parsed as a name, in fact prims are specifically excluded from this.
||| Generate a very basic newtype, no params just wrapping.
||| newtype "Foo" `(Int) ~~> data Foo : Type where
|||                            MkFoo : Int -> Foo
export
newtype : String -> Visibility -> TTImp -> Elab ()
newtype name0 vis ty = do
    name <- inCurrentNS (UN name0)
    let con = MkTy eFC (getTTImpFC ty) (mapName ("Mk" ++) name) `(~ty -> ~(IVar eFC name))
    let decl = IData eFC vis $ MkData eFC name (IType eFC) [] [con]
    declare [decl]
-- e.g `[  ~foo : Type where
--           ~mkfoo : ~ty -> ~foo ]

-------------------------------------------------

export
%macro
showNewtype : Elab (x -> String)
showNewtype = do
    Just (IPi _ _ _ _ ty1 `(String)) <- goal
      | _ => fail "Required type is not: x -> String"
    (n1,(conname,_)) <- checkNewtype ty1
    let con = IVar eFC conname
    check `(\a => case a of ~con x => ~(IPrimVal eFC (Str (nameStr conname)))
                                          ++ " " ++ show x)

export
%macro
eqNewtype : Elab (x -> x -> Bool)
eqNewtype = do
    Just (IPi _ _ _ _ ty1 (IPi _ _ _ _ ty2 `(Prelude.Basics.Bool))) <- goal
      | _ => fail "Required type is not: x -> x -> Bool"
    (n1,(conname,_)) <- checkNewtype ty1
    (n2,_) <- checkNewtype ty2
    let con = IVar eFC conname
    guard (nameStr n1 == nameStr n2) "Required type is not: x -> x -> Bool"
    check `(\a,b => case a of ~con x => case b of ~con y => x == y)

export
%macro
ordNewtype : Elab (x -> x -> Ordering)
ordNewtype = do
    Just (IPi _ _ _ _ ty1 (IPi _ _ _ _ ty2 `(Prelude.EqOrd.Ordering))) <- goal
      | _ => fail "Required type is not: x -> x -> Ordering"
    (n1,(conname,_)) <- checkNewtype ty1
    (n2,_) <- checkNewtype ty2
    let con = IVar eFC conname
    guard (nameStr n1 == nameStr n2) "Required type is not: x -> x -> Ordering"
    check `(\a,b => case a of ~con x => case b of ~con y => compare x y)

data FooPtr : Type where

data Fraf : Nat -> Type where
  Geb : Fraf Z

%runElab newtype "Foo1" Private `(Int) -- is a primtype
%runElab newtype "Foo2" Private `(FooPtr) -- has no cons
-- %runElab newtype "Foo3" Private `(Fraf) -- needs params, not handled yet

caseFoo1 : Foo1 -> Int
caseFoo1 (MkFoo1 x) = x

caseFoo2 : Foo2 -> FooPtr
caseFoo2 (MkFoo2 x) = x

Show Foo1 where
  show = showNewtype

Eq Foo1 where
  (==) = eqNewtype

Ord Foo1 where
  compare = ordNewtype

showTest1 : show (MkFoo1 3) == "MkFoo1 3" = True
showTest1 = ?good -- append is keeping this from reducing, but it checks out

eqTest1 : MkFoo1 3 == MkFoo1 3 = True
eqTest1 = Refl

ordTest1 : MkFoo1 3 > MkFoo1 3 = False
ordTest1 = Refl


text:
module DB.SQLite.Effect
import Effects
import DB.SQLite.SQLiteCodes

%default total

%link C "sqlite3api.o"
%include C "sqlite3api.h"
%lib C "sqlite3"

%dynamic "libsqlite3"
%dynamic "sqlite3api.so"
%access public export

data ConnectionPtr = ConnPtr Ptr
data StmtPtr = PSPtr Ptr

data DBVal = DBInt Int
           | DBText String
           | DBFloat Double
           | DBNull

implementation Show DBVal where
  show (DBInt i) = "DBInt " ++ show i
  show (DBText t) = "DBText " ++ show t
  show (DBFloat f) = "DBFloat " ++ show f
  show DBNull = "DBNull"

-- Type synonym for a table
ResultSet : Type
ResultSet = List (List DBVal)

DBName : Type
DBName = String

QueryString : Type
QueryString = String

Column : Type
Column = Int

ArgPos : Type
ArgPos = Int
data BindError = BE ArgPos SQLiteCode

{- Connection-stage resources -}
data SQLiteConnected : Type where
  SQLConnection : ConnectionPtr -> SQLiteConnected

{- PreparedStatement resources -}
data BindStep = Binding | Bound

data SQLitePSSuccess : BindStep -> Type where
  -- We record potential bind failures within the resource,
  -- and branch on the finishBind step. This prevents us from
  -- having to branch on every bind, which would be impractical.
  SQLitePS : ConnectionPtr -> StmtPtr -> SQLitePSSuccess a
  SQLiteBindFail : ConnectionPtr -> StmtPtr -> BindError -> SQLitePSSuccess a

data SQLitePSFail : Type where
  PSFail : ConnectionPtr -> SQLitePSFail

data SQLiteFinishBindFail : Type where
  SQLiteFBFail : ConnectionPtr -> StmtPtr -> SQLiteFinishBindFail

{- Executing Resources -}
-- Tag used to indicate whether another row may be fetched
data ExecutionResult = ValidRow
                     | InvalidRow

data SQLiteExecuting : ExecutionResult -> Type where
  SQLiteE : ConnectionPtr -> StmtPtr -> SQLiteExecuting a

data QueryError = ConnectionError SQLiteCode
                | BindingError BindError
                | StatementError SQLiteCode
                | ExecError String
                | InternalError

implementation Show QueryError where
  show (ConnectionError code) = "Error connecting to database, code: " ++ (show code)
  show (BindingError (BE ap code)) = "Error binding variable, pos: " ++ (show ap) ++ ", code: " ++ (show code)
  show (StatementError code) = "Error creating prepared statement, code: " ++ (show code)
  show (ExecError err) = err
  show (InternalError) = "Internal Error."

data Sqlite : Effect where
  -- Opens a connection to the database
  OpenDB : DBName -> sig Sqlite (Either QueryError ()) () (\result => (either (const ()) (const SQLiteConnected) result))
  -- Closes the database handle
  CloseDB : sig Sqlite () SQLiteConnected ()
  -- Prepares a statement, given a basic query string
  PrepareStatement : QueryString -> sig Sqlite (Either QueryError ())
                      (SQLiteConnected)
                       (\result => either (const SQLitePSFail)
                              (const $ SQLitePSSuccess Binding) result)
  -- Binds arguments to the given argument position
  BindInt : ArgPos -> Int -> sig  Sqlite () (SQLitePSSuccess Binding)
  BindFloat : ArgPos -> Double -> sig Sqlite () (SQLitePSSuccess Binding)
  BindText : ArgPos -> String -> Int -> sig Sqlite () (SQLitePSSuccess Binding)
  BindNull : ArgPos -> sig Sqlite () (SQLitePSSuccess Binding)

  -- Checks to see whether all the binds were successful, if not then fails with the bind error
  FinishBind : sig Sqlite (Maybe QueryError) (SQLitePSSuccess Binding) (\result => maybe (SQLitePSSuccess Bound) (const SQLiteFinishBindFail) result)

  -- Executes the statement, and fetches the first row
  ExecuteStatement : sig Sqlite (StepResult) (SQLitePSSuccess Bound)
                       (\result => if hasMoreRows result
                         then SQLiteExecuting ValidRow
                         else SQLiteExecuting InvalidRow)

  RowStep : sig Sqlite (StepResult) (SQLiteExecuting ValidRow)
              (\result => if hasMoreRows result
                then SQLiteExecuting ValidRow
                else SQLiteExecuting InvalidRow)

  -- We need two separate effects, but this is entirely non-user-facing due to
  -- if_valid in the wrapper function
  Reset : sig Sqlite (StepResult) (SQLiteExecuting state)
            (\result => if hasMoreRows result
              then SQLiteExecuting ValidRow
              else SQLiteExecuting InvalidRow)

  -- Column access functions
  GetColumnName : Column -> sig  Sqlite String (SQLiteExecuting ValidRow)
  GetColumnDataSize : Column -> sig  Sqlite Int (SQLiteExecuting ValidRow)
  GetColumnText : Column -> sig  Sqlite String (SQLiteExecuting ValidRow)
  GetColumnInt : Column -> sig Sqlite Int (SQLiteExecuting ValidRow)
  GetColumnFloat : Column -> sig Sqlite Double (SQLiteExecuting ValidRow)
  IsColumnNull : Column -> sig Sqlite Bool (SQLiteExecuting ValidRow)

  -- Finalisation Functions
  Finalise : sig Sqlite () (SQLiteExecuting s) SQLiteConnected

  -- Cleanup functions to handle error states
  CleanupPSFail : sig Sqlite () SQLitePSFail  ()
  CleanupBindFail : sig  Sqlite () SQLiteFinishBindFail ()

private
foreignGetError : ConnectionPtr -> IO Int
foreignGetError (ConnPtr ptr) = foreign FFI_C "idr_errcode" (Ptr -> IO Int) ptr

private
foreignNextRow : ConnectionPtr -> IO StepResult
foreignNextRow (ConnPtr ptr) =
  map stepResult (foreign FFI_C "sqlite3_step_idr" (Ptr -> IO Int) ptr)

private
foreignFinalise : ConnectionPtr -> IO ()
foreignFinalise (ConnPtr c) = do foreign FFI_C "sqlite3_finalize_idr" (Ptr -> IO Int) c
                                 return ()

private
foreignClose : ConnectionPtr -> IO ()
foreignClose (ConnPtr c) = do foreign FFI_C "sqlite3_close_idr" (Ptr -> IO Int) c
                              return ()

-- That's the painful bit done, since exception branching will allow us to not have to do
-- the ugliness of pass-through handlers
implementation Handler Sqlite IO where
  handle () (OpenDB file) k = do
    ff <- foreign FFI_C "sqlite3_open_idr" (String -> IO Ptr) file
    is_null <- nullPtr ff
    if (not is_null) then k (Right ()) (SQLConnection (ConnPtr ff))
                     else k (Left (ConnectionError sqlite_ERROR)) ()

  handle (SQLConnection (ConnPtr conn)) CloseDB k = do
    foreign FFI_C "sqlite3_close_idr" (Ptr -> IO Int) conn
    k () ()

  handle (SQLConnection (ConnPtr conn)) (PrepareStatement str) k = do
    res <- foreign FFI_C "sqlite3_prepare_idr" (Ptr -> String -> IO Ptr) conn str
    is_null <- nullPtr res
    if (not is_null) then k (Right ()) (SQLitePS (ConnPtr conn) (PSPtr res))
                     else do err <- foreignGetError (ConnPtr conn)
                             k (Left (StatementError err)) (PSFail (ConnPtr conn))

  handle (SQLitePS (ConnPtr conn) (PSPtr res)) (BindInt pos i) k = do
    res <- foreign FFI_C "sqlite3_bind_int_idr" (Ptr -> Int -> Int -> IO Ptr) conn pos i
    is_null <- nullPtr res
    if (not is_null) then k () (SQLitePS (ConnPtr conn) (PSPtr res))
                     else do err <- foreignGetError (ConnPtr conn)
             -- putStrLn $ "BindInt error: " ++ (show err)
                             k () (SQLiteBindFail (ConnPtr conn) (PSPtr res) (BE pos err))

  handle (SQLitePS (ConnPtr conn) (PSPtr res)) (BindFloat pos f) k = do
    res <- foreign FFI_C "sqlite3_bind_double_idr" (Ptr -> Int -> Double -> IO Ptr) conn pos f
    is_null <- nullPtr res
    if (not is_null) then k () (SQLitePS (ConnPtr conn) (PSPtr res))
                     else do err <- foreignGetError (ConnPtr conn)
                             k () (SQLiteBindFail (ConnPtr conn) (PSPtr res) (BE pos err))

  handle (SQLitePS (ConnPtr conn) (PSPtr res)) (BindText pos str str_len) k = do
    res <- foreign FFI_C "sqlite3_bind_text_idr"
                   (Ptr -> String -> Int -> Int -> IO Ptr)
                   conn str pos str_len
    is_null <- nullPtr res
    if (not is_null) then k () (SQLitePS (ConnPtr conn) (PSPtr res))
                     else do err <- foreignGetError (ConnPtr conn)
               -- putStrLn $ "BindStr error: " ++ (show err)
                             k () (SQLiteBindFail (ConnPtr conn) (PSPtr res) (BE pos err))

  handle (SQLitePS (ConnPtr conn) (PSPtr res)) (BindNull pos) k = do
    res <- foreign FFI_C "sqlite3_bind_null_idr" (Ptr -> Int -> IO Ptr) conn pos
    is_null <- nullPtr res
    if (not is_null) then k () (SQLitePS (ConnPtr conn) (PSPtr res))
                     else do err <- foreignGetError (ConnPtr conn)
                             k () (SQLiteBindFail (ConnPtr conn) (PSPtr res) (BE pos err))

  -- Ok, I lied, we have to do *some* pass-throughs. But they're not terrible.
  handle (SQLiteBindFail conn ps be) (BindInt _ _) k = k () (SQLiteBindFail conn ps be)
  handle (SQLiteBindFail conn ps be) (BindText _ _ _) k = k () (SQLiteBindFail conn ps be)
  handle (SQLiteBindFail conn ps be) (BindFloat _ _) k = k () (SQLiteBindFail conn ps be)
  handle (SQLiteBindFail conn ps be) (BindNull _) k = k () (SQLiteBindFail conn ps be)

  -- Finishing binding, reporting any bind errors if they occurred
  handle (SQLitePS c p) (FinishBind) k =
    k Nothing (SQLitePS c p)

  handle (SQLiteBindFail c ps be) (FinishBind) k =
    k (Just (BindingError be)) (SQLiteFBFail c ps)

  handle (SQLitePS (ConnPtr c) (PSPtr p)) (ExecuteStatement) k = do
    step <- foreignNextRow (ConnPtr c)
    case step of
      Unstarted    => k Unstarted    (SQLiteE (ConnPtr c) (PSPtr p))
      StepComplete => k StepComplete (SQLiteE (ConnPtr c) (PSPtr p))
      StepFail     => k StepFail     (SQLiteE (ConnPtr c) (PSPtr p))
      NoMoreRows   => k NoMoreRows   (SQLiteE (ConnPtr c) (PSPtr p))

  handle (SQLiteE (ConnPtr c) (PSPtr p)) (RowStep) k = do
    step <- foreignNextRow (ConnPtr c)
    case step of
      Unstarted    => k Unstarted    (SQLiteE (ConnPtr c) (PSPtr p))
      StepComplete => k StepComplete (SQLiteE (ConnPtr c) (PSPtr p))
      StepFail     => k StepFail     (SQLiteE (ConnPtr c) (PSPtr p))
      NoMoreRows   => k NoMoreRows   (SQLiteE (ConnPtr c) (PSPtr p))

  -- Getting values from the current row
  handle (SQLiteE (ConnPtr c) (PSPtr p)) (GetColumnName i) k = do
    res <- foreign FFI_C "sqlite3_column_name_idr" (Ptr -> Int -> IO String) c i
    k res (SQLiteE (ConnPtr c) (PSPtr p))

  handle (SQLiteE (ConnPtr c) (PSPtr p)) (GetColumnDataSize i) k = do
    res <- foreign FFI_C "sqlite3_column_bytes_idr" (Ptr -> Int -> IO Int) c i
    k res (SQLiteE (ConnPtr c) (PSPtr p))

  handle (SQLiteE (ConnPtr c) (PSPtr p)) (GetColumnInt i) k = do
    res <- foreign FFI_C "sqlite3_column_int_idr" (Ptr -> Int -> IO Int) c i
    k res (SQLiteE (ConnPtr c) (PSPtr p))

  handle (SQLiteE (ConnPtr c) (PSPtr p)) (GetColumnFloat i) k = do
    res <- foreign FFI_C "sqlite3_column_double_idr" (Ptr -> Int -> IO Double) c i
    k res (SQLiteE (ConnPtr c) (PSPtr p))

  handle (SQLiteE (ConnPtr c) (PSPtr p)) (GetColumnText i) k = do
    res <- foreign FFI_C "sqlite3_column_text_idr" (Ptr -> Int -> IO String) c i
    k res (SQLiteE (ConnPtr c) (PSPtr p))

  handle (SQLiteE (ConnPtr c) (PSPtr p)) (IsColumnNull i) k = do
    res <- foreign FFI_C "sqlite3_column_null_idr" (Ptr -> Int -> IO Int) c i
    k (res /= 0) (SQLiteE (ConnPtr c) (PSPtr p))

  -- Resetting our position
  handle (SQLiteE (ConnPtr c) (PSPtr p)) (Reset) k = do
    foreign FFI_C "sqlite3_reset_idr" (Ptr -> IO Int) c
    step <- foreignNextRow (ConnPtr c)
    case step of
      Unstarted    => k Unstarted    (SQLiteE (ConnPtr c) (PSPtr p))
      StepComplete => k StepComplete (SQLiteE (ConnPtr c) (PSPtr p))
      StepFail     => k StepFail     (SQLiteE (ConnPtr c) (PSPtr p))
      NoMoreRows   => k NoMoreRows   (SQLiteE (ConnPtr c) (PSPtr p))

{-  handle (SQLiteE (ConnPtr c) (PSPtr p)) (ResetFromEnd) k = do
    foreign FFI_C (FFun "sqlite3_reset_idr" [FPtr] FInt) c
    step <- foreignNextRow (ConnPtr c)
    case step of
      StepComplete => k StepComplete (SQLiteE (ConnPtr c) (PSPtr p))
      StepFail     => k StepFail     (SQLiteE (ConnPtr c) (PSPtr p))
      NoMoreRows   => k NoMoreRows   (SQLiteE (ConnPtr c) (PSPtr p))
-}
      -- Finalising the SQL Statement
  handle (SQLiteE c p) (Finalise) k = do
    foreignFinalise c
    k () (SQLConnection c)

  handle (PSFail c) CleanupPSFail k = do
    foreignClose c
    k () ()

  handle (SQLiteFBFail c p) CleanupBindFail k = do
    foreignFinalise c
    foreignClose c
    k () ()
  --hack
  handle _ _ k = believe_me ()

SQLITE : Type -> EFFECT
SQLITE t = MkEff t Sqlite
{- User-facing functions -}
openDB : DBName ->  Eff (Either QueryError ()) [SQLITE ()]
                     (\result => [SQLITE (either (const ()) (const SQLiteConnected) result)])
openDB name = call $ OpenDB name

closeDB : Eff () [SQLITE (SQLiteConnected)] [SQLITE ()]
closeDB = call CloseDB

prepareStatement : QueryString -> Eff (Either QueryError ())
                    [SQLITE SQLiteConnected]
                    (\result => [SQLITE ( either (const SQLitePSFail)
                                      (const $ SQLitePSSuccess Binding) result)])
prepareStatement stmt = call $ PrepareStatement stmt

bindInt : ArgPos -> Int -> Eff () [SQLITE (SQLitePSSuccess Binding)]
bindInt pos i = call $ BindInt pos i

bindFloat : ArgPos -> Double -> Eff () [SQLITE (SQLitePSSuccess Binding)]
bindFloat pos f = call $ BindFloat pos f

bindText : ArgPos -> String -> Eff () [SQLITE (SQLitePSSuccess Binding)]
bindText pos str = call $ BindText pos str str_len
  where natToInt : Nat -> Int
        natToInt Z = 0
        natToInt (S k) = 1 + (natToInt k)

        str_len : Int
        str_len = natToInt (length str)

bindNull : ArgPos -> Eff () [SQLITE (SQLitePSSuccess Binding)]
bindNull pos = call $ BindNull pos

finishBind : Eff (Maybe QueryError) [SQLITE (SQLitePSSuccess Binding)]
               (\result => [SQLITE (maybe (SQLitePSSuccess Bound) (const SQLiteFinishBindFail) result)])
finishBind = call FinishBind

nextRow : Eff StepResult [SQLITE (SQLiteExecuting ValidRow)]
            (\result => [SQLITE (if hasMoreRows result
                       then SQLiteExecuting ValidRow
                       else SQLiteExecuting InvalidRow)])
nextRow = call RowStep

reset : Eff StepResult [SQLITE (SQLiteExecuting state)]
          (\result => [SQLITE (if hasMoreRows result
                     then SQLiteExecuting ValidRow
                     else SQLiteExecuting InvalidRow)])
reset = call Reset

getColumnName : Column -> Eff String [SQLITE (SQLiteExecuting ValidRow)]
getColumnName col = call $ GetColumnName col

getColumnText : Column -> Eff String [SQLITE (SQLiteExecuting ValidRow)]
getColumnText col = call $ GetColumnText col

getColumnInt : Column -> Eff Int [SQLITE (SQLiteExecuting ValidRow)]
getColumnInt col = call $ GetColumnInt col

getColumnFloat : Column -> Eff Double [SQLITE (SQLiteExecuting ValidRow)]
getColumnFloat col = call $ GetColumnFloat col

isColumnNull : Column -> Eff Bool [SQLITE (SQLiteExecuting ValidRow)]
isColumnNull col = call $ IsColumnNull col

getColumnDataSize : Column -> Eff Int [SQLITE (SQLiteExecuting ValidRow)]
getColumnDataSize col = call $ GetColumnDataSize col

finalise : Eff () [SQLITE (SQLiteExecuting s)] [SQLITE SQLiteConnected]
finalise = call Finalise

cleanupPSFail : Eff () [SQLITE (SQLitePSFail)] [SQLITE ()]
cleanupPSFail = call CleanupPSFail

cleanupBindFail :  Eff () [SQLITE (SQLiteFinishBindFail)] [SQLITE ()]
cleanupBindFail = call CleanupBindFail

-- Just makes it a tad nicer to write
executeStatement : Eff StepResult [SQLITE (SQLitePSSuccess Bound)]
                     (\result => [SQLITE (if hasMoreRows result
                                then SQLiteExecuting ValidRow
                                else SQLiteExecuting InvalidRow)])
executeStatement = call ExecuteStatement

getQueryError : Either QueryError b -> QueryError
getQueryError (Left qe) = qe
getQueryError _ = InternalError

total
multiBind' : List (Int, DBVal) -> Eff () [SQLITE (SQLitePSSuccess Binding)]
multiBind' [] = Effects.pure ()
multiBind' ((pos, (DBInt i)) :: xs) = do bindInt pos i
                                         multiBind' xs
multiBind' ((pos, (DBFloat f)) :: xs) = do bindFloat pos f
                                           multiBind' xs
multiBind' ((pos, (DBText t)) :: xs) = do bindText pos t
                                          multiBind' xs
multiBind' ((pos, DBNull) :: xs) = do bindNull pos
                                      multiBind' xs
-- Binds multiple values within a query

multiBind : List (Int, DBVal) -> Eff (Maybe QueryError)
                 [SQLITE (SQLitePSSuccess Binding)]
                 (\result => [SQLITE (maybe (SQLitePSSuccess Bound) (const SQLiteFinishBindFail) result)])

multiBind vals = do
  multiBind' vals
  finishBind

getRowCount' : StepResult -> Eff (Either QueryError Int) [SQLITE (SQLiteExecuting s)] [SQLITE ()]

getRowCount' NoMoreRows   = do finalise
                               closeDB
                               return $ Left (ExecError "Unable to get row count")
getRowCount' StepFail     = do finalise
                               closeDB
                               return $ Left (ExecError "Error whilst getting row count")
getRowCount' {s=ValidRow} StepComplete = do last_insert_id <- getColumnInt 0
                                            finalise
                                            closeDB
                                            return $ Right last_insert_id
getRowCount' {s=InvalidRow} StepComplete = do finalise
                                              closeDB
                                              return $ Left (ExecError "Invalid row")
getRowCount' Unstarted    = do finalise
                               closeDB
                               return $ Left (ExecError "Not started")

getBindError : Maybe QueryError -> QueryError
getBindError (Just (BindingError be)) = (BindingError be)
getBindError _ = InternalError

getRowCount : Eff (Either QueryError Int) [SQLITE SQLiteConnected] [SQLITE ()]
getRowCount = do
  let insert_id_sql = "SELECT last_insert_rowid()"
  sql_prep_res <- prepareStatement insert_id_sql
  case sql_prep_res of
    Left err => do cleanupPSFail
                   return (Left err)
    Right () =>
      do bind_res_2 <- finishBind
         case bind_res_2 of
           Just err => do let be = getBindError bind_res_2
                          cleanupBindFail
                          return $ Left be
           Nothing =>
             do exec_res <- executeStatement
                case exec_res of
                  NoMoreRows => getRowCount' NoMoreRows
                  StepComplete => getRowCount' StepComplete
                  StepFail => getRowCount' StepFail
                  Unstarted => getRowCount' Unstarted

executeInsert : String ->
                String ->
                List (Int, DBVal) ->
                Eff (Either QueryError Int) [SQLITE ()]
executeInsert db_name query bind_vals =
  do db_res <- openDB db_name
     case db_res of
       Left err => return (Left err)
       Right () =>
         do ps_res <- prepareStatement query
            case ps_res of
              Left err => do cleanupPSFail
                             return (Left err)
              Right () =>
                do bind_res <- multiBind bind_vals
                   case bind_res of
                     Just err => do cleanupBindFail
                                    return (Left err)
                     Nothing  => executeIt
  -- split out to make typechecking faster
  where executeIt : Eff (Either QueryError Int) [SQLITE (SQLitePSSuccess Bound)] [SQLITE ()]

        executeIt =
          do er_1 <- executeStatement
             case er_1 of
               StepFail => do finalise {s=ValidRow}
                              closeDB
                              return $ Left (ExecError "Error inserting")
               Unstarted => do finalise {s=ValidRow}
                               closeDB
                               return $ Left (ExecError "Internal error: 'unstarted' after execution")
               NoMoreRows => do finalise {s=InvalidRow}
                                getRowCount
               StepComplete => do finalise {s=ValidRow}
                                  getRowCount

-- Helper functions for selection from a DB
partial
collectResults : (Eff (List DBVal) [SQLITE (SQLiteExecuting ValidRow)]) ->
                 Eff ResultSet [SQLITE (SQLiteExecuting ValidRow)] [SQLITE (SQLiteExecuting InvalidRow)]
collectResults fn =
  do results <- fn
     case !nextRow of
       Unstarted => return $ results :: !(collectResults fn)
       StepFail => return $ results :: !(collectResults fn)
       StepComplete => return $ results :: !(collectResults fn)
       NoMoreRows => return [results]

-- Convenience function to abstract around some of the boilerplate code.
-- Takes in the DB name, query, a list of (position, variable value) tuples,
-- a function to process the returned data,
partial
executeSelect : (db_name : String) -> (q : String) -> List (Int, DBVal) ->
                (Eff (List DBVal) [SQLITE (SQLiteExecuting ValidRow)]) ->
                Eff (Either QueryError ResultSet) [SQLITE ()]
executeSelect db_name q bind_vals fn =
  do Right () <- openDB db_name | Left err => return (Left err)
     Right () <- prepareStatement q | Left err => do cleanupPSFail
                                                     return $ Left err
     Nothing <- multiBind bind_vals | Just err => do cleanupBindFail
                                                     return $ Left err
     case !executeStatement of
       Unstarted => do res <- collectResults fn
                       finalise
                       closeDB
                       return $ Right res
       StepFail => do res <- collectResults fn
                      finalise
                      closeDB
                      return $ Right res
       StepComplete => do res <- collectResults fn
                          finalise
                          closeDB
                          return $ Right res
       NoMoreRows => do finalise
                        closeDB
                        return $ Right []

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
{-
null
is Nothing
is not Just
not null
is not Nothing
is Just
==
/=
==
Just 42
Nothing
-}

import CIL.FFI
import CIL.System.Reflection

putMaybeString : Maybe String -> CIL_IO ()
putMaybeString s =
  putStrLn (maybe "null" id s)

putIsNothing : Maybe String -> CIL_IO ()
putIsNothing Nothing = putStrLn "is Nothing"
putIsNothing _       = putStrLn "is not Nothing"

putIsJust : Maybe String -> CIL_IO ()
putIsJust (Just _) = putStrLn "is Just"
putIsJust _        = putStrLn "is not Just"

TheExportsTy : CILTy
TheExportsTy = CILTyRef "" "TheExports"

%inline
invokeMaybeString : String -> Maybe String -> CIL_IO ()
invokeMaybeString fn s =
  invokeStatic TheExportsTy fn (Maybe String -> CIL_IO ()) s

testFFI : Maybe String -> CIL_IO ()
testFFI s = do
  invokeMaybeString "putMaybeString" s
  invokeMaybeString "putIsNothing" s
  invokeMaybeString "putIsJust" s

valueOf : Bool -> Maybe String
valueOf False = Nothing
valueOf True  = Just "True"

testMaybeEq : Bool -> Maybe String -> CIL_IO ()
testMaybeEq b m = putStrLn (if valueOf b == m then "==" else "/=")

maybeInt : Bool -> Maybe Int
maybeInt True  = Just 42
maybeInt False = Nothing

testMaybeInt : Bool -> CIL_IO ()
testMaybeInt b = printLn (maybeInt b)

%inline
invokeTestMaybeInt : Bool -> CIL_IO ()
invokeTestMaybeInt =
  invokeStatic TheExportsTy "testMaybeInt" (Bool -> CIL_IO ())

main : CIL_IO ()
main = do
  testFFI Nothing
  testFFI (Just "not null")
  testMaybeEq False Nothing
  testMaybeEq False (Just "True")
  testMaybeEq True  (Just "True")
  invokeTestMaybeInt True
  invokeTestMaybeInt False

exports : FFI_Export FFI_CIL "TheExports" []
exports =
  Fun putMaybeString CILDefault $
  Fun putIsNothing CILDefault $
  Fun putIsJust CILDefault $
  Fun testMaybeInt CILDefault $
  End

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

max_stars_repo_name: alaendle/idris-cil

max_issues_repo_name: alaendle/idris-cil

max_forks_repo_name: alaendle/idris-cil


text:
module Language.LSP.CodeAction.RefineHole

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Unify
import Core.UnifyState
import Core.Value
import Data.Nat
import Data.String
import Idris.REPL.Common
import Idris.REPL.Opts
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.Message
import Libraries.Data.NameMap
import Libraries.Data.PosMap
import TTImp.Elab.App
import TTImp.Elab.Check
import TTImp.TTImp
import TTImp.Unelab
import Server.Configuration
import Server.Log
import Server.Response
import Server.Utils

-- CodeAction for filling holes, not necessarily type correct constructions.
-- This code action does three things:
-- * Tries to determine the type of the hole and offers valid constructors with new holes for parameters.
--   Poor man's hole refining.
-- * Tries to find similar names from the context.
--   In many cases I find myself writing out the hole name somewhat similar to final function I want to
--   call later on, in the given hole.
-- * Tries to find names which are safely fit to the hole.

||| Tries to resolve a type where Like Nat, Maybe
||| It ignores the type parameters
resolveTypeName
  :  Ref Ctxt Defs
  => Ref LSPConf LSPConfiguration
  => {vars : _}
  -> Term vars
  -> Core (Maybe Name)
resolveTypeName (Ref fc x name)     = Just <$> toFullNames name
resolveTypeName (Bind fc x b scope) = resolveTypeName scope -- ignores explicit/implicit parameters: {a} -> DataType
resolveTypeName (App fc fn arg)     = resolveTypeName fn    -- ignores type parameters: DataType a
resolveTypeName other = do
  logString Debug "resolveTypeName: \{show other}"
  pure Nothing

||| Checks if the the Term represents an explicit function
isFunctionType : Term vars -> Bool
isFunctionType (Bind fc x (Lam fc1 y Implicit ty)         scope) = isFunctionType scope
isFunctionType (Bind fc x (Lam fc1 y Explicit ty)         scope) = True
isFunctionType (Bind fc x (Lam fc1 y AutoImplicit ty)     scope) = isFunctionType scope
isFunctionType (Bind fc x (Lam fc1 y (DefImplicit z) ty)  scope) = isFunctionType scope
isFunctionType (Bind fc x (Pi  fc1 y Implicit ty)         scope) = isFunctionType scope
isFunctionType (Bind fc x (Pi  fc1 y Explicit ty)         scope) = True
isFunctionType (Bind fc x (Pi  fc1 y AutoImplicit ty)     scope) = isFunctionType scope
isFunctionType (Bind fc x (Pi  fc1 y (DefImplicit z) ty)  scope) = isFunctionType scope
isFunctionType other               = False

||| Checks if the name is visible in the namespace of the hole.
checkVisibleName : Ref Ctxt Defs => Name -> Name -> GlobalDef -> Core Bool
checkVisibleName h n g = do
  fn <- toFullNames n
  fh <- toFullNames h
  let (Just namespc, _) = displayName fn
      | _ => pure False
  let (Just hnamespc, _) = displayName fh
      | _ => pure False
  case namespc == hnamespc of
    -- Same namespace everything is visible.
    True  => pure True
    -- Different namespace, Private members are hidden.
    False => do
      vs <- isVisible namespc
      pure $ vs && g.visibility /= Private

||| Learn the user defined name of the explicit paramenters for a type of the constructor, of the length
||| of the names matches the arity, then these names are the names for the field with
||| a high probability.
constructorParameters : Term vars -> List (Maybe Name)
constructorParameters (Bind fc x (Lam fc1 y Explicit ty) scope) =
  case isUserName x of
    True  => Just x :: constructorParameters scope
    False => Nothing :: constructorParameters scope
constructorParameters (Bind fc x (Lam fc1 y z ty) scope) =
  constructorParameters scope
constructorParameters (Bind fc x (Pi fc1 y Explicit ty) scope) =
  case isUserName x of
    True  => Just x :: constructorParameters scope
    False => Nothing :: constructorParameters scope
constructorParameters (Bind fc x (Pi fc1 y z ty) scope) =
  constructorParameters scope
constructorParameters other = []

data ConstructorInfo
  = UnnamedFieldsCon Name Nat
  | NamedFieldsCon   Name (List (Maybe Name))

||| Generate a list of constructors for the given type.
constructors : Ref LSPConf LSPConfiguration => Ref Ctxt Defs => Name -> Name -> Core (Maybe (List ConstructorInfo))
constructors holeName typeName = do
  defs <- get Ctxt
  Just gdef <- lookupCtxtExact !(toFullNames typeName) defs.gamma
    | Nothing => do
        pure Nothing
  let (TCon tag arity parampos detpos flags mutwith datacons detagabbleBy) = gdef.definition
    | _ => do
        pure Nothing
  -- Possible constructor informations, if something is not a constructor (for some reason)
  -- it is marked as Nothing
  mConsInfo
    <- traverse
        (\consName => do
          rConName <- toFullNames consName
          gConDef <- lookupCtxtExact rConName defs.gamma
          case gConDef of
            Nothing => pure Nothing
            Just gd => case (!(checkVisibleName holeName rConName gd), gd.definition) of
              (False, _) => pure Nothing
              (_, DCon tag arity newtypeArg) => do
                let arity' = minus arity (length gd.eraseArgs)
                possibleFieldNames <- constructorParameters <$> toFullNames gd.type
                pure
                  $ Just
                  $ if arity' == length possibleFieldNames
                      then NamedFieldsCon   rConName possibleFieldNames
                      else UnnamedFieldsCon rConName arity'
              other => pure Nothing)
        datacons
  -- If all are constructors we are OK
  pure $ sequence mConsInfo

generateHoleName : Ref Ctxt Defs => String -> Nat -> Core (String, Nat)
generateHoleName holeName k = do
  defs <- get Ctxt
  let n = holeName ++ "_" ++ show k
  case !(lookupCtxtName (UN n) defs.gamma) of
    [] => pure (n, k+1)
    _ => generateHoleName holeName (k + 1)

||| Generate hole names if we only have arity information
generateHoleNames : Ref Ctxt Defs => String -> Nat -> Core (Nat, List String)
generateHoleNames baseName 0     = pure (0, [])
generateHoleNames baseName (S k) = do
  (n, rest) <- generateHoleNames baseName k
  (holeName, n') <- generateHoleName baseName n
  pure (n',("?" ++ holeName) :: rest)

||| Generate hole names if we have mixed information, names an unknown names in the arguments
genereateFieldHoleNames : Ref Ctxt Defs => String -> List (Maybe Name) -> Core (Nat, List String)
genereateFieldHoleNames baseName [] = pure (0, [])
genereateFieldHoleNames baseName (f :: fs) = do
  (n, rest) <- genereateFieldHoleNames baseName fs
  (holeName, n') <- generateHoleName (maybe baseName (show . dropAllNS) f) n
  pure (n', ("?" ++ holeName) :: rest)

renderConstructor : Ref Ctxt Defs => Name -> ConstructorInfo -> Core (Maybe String)
renderConstructor holeName conInfo = do
  case conInfo of
    UnnamedFieldsCon fullName 0 => pure $ Just $ show $ dropAllNS fullName
    UnnamedFieldsCon fullName n => do
      let Just holeName' = userNameRoot holeName
          | Nothing => pure Nothing
      (_, newHoles) <- generateHoleNames holeName' n
      pure $ Just $ "(" ++ show (dropAllNS fullName) ++ " " ++ unwords newHoles ++ ")"
    NamedFieldsCon fullName [] => pure $ Just $ show $ dropAllNS fullName
    NamedFieldsCon fullName fieldNames => do
      let Just holeName' = userNameRoot holeName
          | Nothing => pure Nothing
      (_, newHoles) <- genereateFieldHoleNames holeName' fieldNames
      pure $ Just $ "(" ++ show (dropAllNS fullName) ++ " " ++ unwords newHoles ++ ")"

fcToRange : FC -> Maybe Range
fcToRange (MkFC x (sline,scol) (eline, ecol))
  = Just (MkRange (MkPosition sline scol)
                  (MkPosition eline ecol))
fcToRange (MkVirtualFC x (sline,scol) (eline, ecol))
  = Just (MkRange (MkPosition sline scol)
                  (MkPosition eline ecol))
fcToRange EmptyFC = Nothing

||| Create a CodeAction with string to replace the hole, insert (!) if the substituition possibly non-well-typed.
refineHoleWith : Bool -> FC -> CodeActionParams -> String -> CodeAction
refineHoleWith maybeNonTypesafe holeLoc params nameString =
  MkCodeAction
    { title       = "Fill Hole ~ \{strSubstr 0 50 nameString}" ++ if maybeNonTypesafe then " (!)" else ""
    , kind        = Just RefactorRewrite
    , diagnostics = Just []
    , isPreferred = Just False -- not a quickfix
    , disabled    = Nothing
    , edit        = Just $ MkWorkspaceEdit
        { changes           = Just (singleton params.textDocument.uri
            [ MkTextEdit range nameString ])
        , documentChanges   = Nothing
        , changeAnnotations = Nothing
        }
    , command     = Nothing
    , data_       = Nothing
    }
  where
    range : Range
    range = fromMaybe params.range $ fcToRange holeLoc

isHole : Defs -> Name -> Core Bool
isHole defs n = do
  Just def <- lookupCtxtExact n (gamma defs)
    | Nothing => do pure False
  pure $ case definition def of
    Hole _ _ => True
    _        => False

||| Check if the name has the exact type
nameHasType : Ref LSPConf LSPConfiguration
  => Ref Ctxt Defs
  => Ref MD Metadata
  => Ref UST UState
  => Name -> Name -> Term [] -> Core Bool
nameHasType holeName nameRef expected = do
  defs <- get Ctxt
  fullName <- toFullNames nameRef
  Just def <- lookupCtxtExact fullName defs.gamma
    | Nothing => pure False
  True <- checkVisibleName holeName fullName def
    | False => pure False
  nt <- normaliseAll defs [] (GlobalDef.type def)
  ex <- normaliseAll defs [] expected
  equivTypes nt ex

findFirstN : Nat -> (a -> Core (Maybe b)) -> List a -> Core (List b)
findFirstN Z f xs = pure []
findFirstN (S k) f [] = pure []
findFirstN (S k) f (x :: xs) = case !(f x) of
  Nothing => findFirstN (S k) f xs
  Just y  => map (y ::) (findFirstN k f xs)

||| Keeps the name with same preffix as the hole, ignoring namespaces.
typeMatchingNames
  :  Ref LSPConf LSPConfiguration
  => Ref Ctxt Defs
  => Ref MD Metadata
  => Ref UST UState
  => Name -> Term [] -> Nat -> Core (List String)
typeMatchingNames holeName ty limit = do
  defs <- get Ctxt
  let hn = userNameRoot holeName
  findFirstN limit
      (\funcName =>
        let sn = userNameRoot funcName
        in if hn /= sn && !(nameHasType holeName funcName ty)
              then pure (userNameRoot funcName)
              else pure Nothing)
    $ keys
    $ namesResolvedAs defs.gamma

keepNonHoleNames : Ref Ctxt Defs => List String -> Core (List String)
keepNonHoleNames = map catMaybes . traverse nonHoleName
  where
    -- If the name is uniquely determines a hole filter out from the list
    -- if the name is not unique keep it around.
    nonHoleName : String -> Core (Maybe String)
    nonHoleName name = do
      -- Find the type information at this hole
      defs <- get Ctxt
      [(_, (_, holeGlobalDef))] <- lookupCtxtName (UN name) (gamma defs)
        | _ => do
          pure $ Just name
      pure $ case holeGlobalDef.definition of
        Hole{} => Nothing
        _      => Just name

export
refineHole
  :  Ref LSPConf LSPConfiguration
  => Ref MD Metadata
  => Ref Ctxt Defs
  => Ref UST UState
  => Ref Syn SyntaxInfo
  => Ref ROpts REPLOpts
  => CodeActionParams -> Core (List CodeAction)
refineHole params = do
  let True = params.range.start.line == params.range.end.line
    | _ => pure []

  [] <- searchCache params.range RefineHole
    | actions => do logString Debug "refineHole: found cached action"
                    pure actions

  meta <- get MD
  let line = params.range.start.line
  let col = params.range.start.character
  let Just (loc, name) = findPointInTreeLoc (line, col) (nameLocMap meta)
    | Nothing =>
        do logString Debug $
             "refineHole: couldn't find name in tree for position (\{show line},\{show col})"
           pure []

  -- The name is a hole
  defs <- get Ctxt
  True <- (isHole defs name) -- should only work on holes
    | _ => do logString Debug $ "refineHole: \(show name) is not a hole"
              pure []

  -- Find the type information at this hole
  [(holeName, (x, holeGlobalDef))] <- lookupCtxtName name (gamma defs)
    | _ => do
      logString Debug "refineHole: Non-unique context entries for \{show name}"
      pure []

  -- Try to find some constructors
  constructorStrings <-
    -- If the type is a datatype find its definition
    case !(resolveTypeName holeGlobalDef.type) of
      Nothing => pure []
      Just dataTypeName =>
        if isFunctionType holeGlobalDef.type
          -- If a hole represents a function, we shouldn't offer constructors
          then pure []
          -- Find its constructors
          else case !(constructors holeName dataTypeName) of
                Nothing => pure []
                Just [] => pure []
                Just cns => do
                  -- Render the (Constructor ?field1 ?field2) like fields
                  someNameStrings <- traverse (renderConstructor name) cns
                  case the (Maybe (List String)) (sequence someNameStrings) of
                    Nothing => pure []
                    Just cs => pure cs

  -- Limit the results
  cfg <- get LSPConf
  let limit = cfg.searchLimit

  typesafeNames <- keepNonHoleNames !(typeMatchingNames holeName holeGlobalDef.type 1000)
  similarNames <- keepNonHoleNames (filter (\n => not (elem n typesafeNames)) !(getSimilarNames name))

  -- Render code actions that inject constructors or similar names
  let fillerStrings = nub (constructorStrings ++ typesafeNames)
  let safeFillers = map (refineHoleWith False holeGlobalDef.location params) fillerStrings
  let nonSafeFillerStrings = take limit $ filter (\x => elemBy (/=) x fillerStrings) similarNames
  let nonSafeFillers = map (refineHoleWith True holeGlobalDef.location params) nonSafeFillerStrings
  let fillers = safeFillers ++ nonSafeFillers

  -- Cache the fillers
  modify LSPConf (record { cachedActions $= insert (cast loc, RefineHole, fillers) })

  pure fillers


text:
module Data.Profunctor

import Data.Morphisms

public export
interface Profunctor (0 f : Type -> Type -> Type) where
  dimap : (a -> a') -> (b -> b') -> f a' b -> f a b'
  lmap : (a -> a') -> f a' b -> f a b
  rmap : (b -> b') -> f a b -> f a b'

  dimap pre post = rmap post . lmap pre
  lmap pre = dimap pre id
  rmap post = dimap id post


text:
module Main

import Terminal

partial
loop : IO ()
loop = do
  c <- getChar
  putStrLn $ show (ord c)
  if c=='q' then pure () else loop

partial
main : IO ()
main = do
  setRaw
  loop

max_stars_repo_name: PeterHajdu/peti

max_issues_repo_name: PeterHajdu/peti

max_forks_repo_name: PeterHajdu/peti


text:
-- ----------------------------------------------------------- [ SimpleDot.idr ]
-- Module    : SimpleDot.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]

||| A Simple Graph representation for Dot.
module Commons.Data.Graphviz.SimpleDot

import Data.AVL.Graph

%access export

-- ------------------------------------------------------------------- [ Utils ]

toKVString : List (String, String) -> List String
toKVString Nil         = Nil
toKVString ((x,y)::xs) = (x ++ "=" ++ show y) :: toKVString xs

compact : List String -> String
compact Nil = ""
compact (x::xs) = x ++ compact xs

showAttrs : List (String, String) -> String
showAttrs Nil = ";"
showAttrs xs  = unwords
    [ "["
    , compact $ intersperse "," (toKVString xs)
    , "];"]

-- -------------------------------------------------------------------- [ ADTs ]

public export
data SDTy = NODE | GRAPH | EDGE

||| A simple dot file with no sub-graphs.
public export
data SimpleDot : SDTy -> Type where
  Node    : NodeID -> List (String, String)                -> SimpleDot NODE
  Edge    : NodeID -> NodeID -> List (String, String)      -> SimpleDot EDGE
  Digraph : List (SimpleDot NODE) -> List (SimpleDot EDGE) -> SimpleDot GRAPH
  Graph   : List (SimpleDot NODE) -> List (SimpleDot EDGE) -> SimpleDot GRAPH

-- -------------------------------------------------------------------- [ Show ]

Show (SimpleDot x) where
  show (Node i as) = unwords [ show i, showAttrs as]
  show (Edge x y as) = unwords
      [ show x
      , "->"
      , show y
      , showAttrs as
      ]
  show (Digraph ns es) = unlines ["digraph g ", unlines ["{" , unlines $ map show ns, "\n\n", unlines $ map show es, "}\n"]]
  show (Graph   ns es) = unlines [show "graph g ", unlines ["{" , unlines $ map show ns, "\n\n", unlines $ map show es, "}\n"]]

-- --------------------------------------------------------------- [ Transform ]

||| Convert a Graph to a simple dot node.
|||
||| @mkNodeLabel How to make a node label.
||| @mkEdgeLabel How to make a edge label.
toDot : Graph v e
     -> (mkNodeLabel : v -> String)
     -> (mkEdgeLabel : Edge e -> SimpleDot EDGE)
     -> SimpleDot GRAPH
toDot g mkNodeLabel mkEdgeLabel = Digraph ns es
  where
    getNodeLabel : NodeID -> String
    getNodeLabel n = case getValueByID n g of
        Nothing => ""
        Just u  => mkNodeLabel u

    ns : List (SimpleDot NODE)
    ns = map (\x => Node x [("label", getNodeLabel x)]) (verticesID g)

    es : List (SimpleDot EDGE)
    es = map mkEdgeLabel (edges g)

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

max_stars_repo_name: jfdm/idris-common

max_issues_repo_name: jfdm/idris-common

max_forks_repo_name: jfdm/idris-common


text:
module xquant.Core.Spectrum

import public xquant.Core.Types
import public xquant.Core.NonZero
import Data.Matrix.Algebraic

%default total

data SysType = Finite Nat | Infinite

||| Spectrum – list of energies – for
||| a finite-dimensional system
data FSpectrum : Nat -> Type where
  FSpect : Vect n Fl -> FSpectrum n

||| Finite system degeneracy, i.e.,
||| state multiplicity by energy level
data FDegen : Nat -> Type where
  FDeg : {v : Vect n Nat} -> NVect v -> FDegen n

size : FDegen n -> Nat
size (FDeg {v} _) = sum v

rep : FDegen n -> Type
rep fd = StateSpace (size fd) Amp

data FSystem : Nat -> Type where
  FSys : (fd : FDegen n) ->
         FSpectrum n ->
         rep fd ->
         FSystem n

||| Infinite system spectrum
data ISpectrum = ISpect (Nat -> Fl)

||| Infinite system degeneracy
||| (state multiplicity by energy level)
data IDegen : Type where
  IDeg : (Nat -> NonZ) -> IDegen

max_stars_repo_name: BlackBrane/xquant

max_issues_repo_name: fieldstrength/xquant

max_forks_repo_name: fieldstrength/xquant


text:
module Void

import Basic

%default total

public export
data Void : Type where

public export
VoidInduction : (0 p : Void -> Type) -> (0 x : Void) -> p x
VoidInduction _ x impossible

public export
VoidRecursion : (0 p : Type) -> (0 x : Void) -> p
VoidRecursion p = VoidInduction (const p)

public export
VoidInitial : (0 p : Type) -> (0 x : Void) -> p
VoidInitial = VoidRecursion

public export
IsEmpty : Type -> Type
IsEmpty a = a -> Void

public export
Neg : Type -> Type
Neg = IsEmpty


text:
module Main
import QB.FFI

-- helper functions
assert : a -> a -> IO Unsafe
assert x1 x2 = callff2 "assert2" (unsafe x1) (unsafe x2)

annInt : Integer -> Integer
annInt x = x

showInt : Integer -> String
showInt = show

-- http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#primitive-types
x : Int
x = 42

foo : String
foo = "Sausage machine"

bar : Char
bar = 'Z'

quux : Bool
quux = False

-- http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#functions
plus' : Nat -> Nat -> Nat
plus' Z     y = y
plus' (S k) y = S (plus' k y)

-- Unary multiplication
mult' : Nat -> Nat -> Nat
mult' Z     y = Z
mult' (S k) y = plus' y (mult' k y)

%hide reverse
-- http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#where-clauses
reverse : List a -> List a
reverse xs = revAcc [] xs where
  revAcc : List a -> List a -> List a
  revAcc acc [] = acc
  revAcc acc (x :: xs) = revAcc (x :: acc) xs

foo' : Int -> Int
foo' x = case isLT of
            Yes => x*2
            No => x*4
    where
       data MyLT = Yes | No

       isLT : MyLT
       isLT = if x < 20 then Yes else No

even : Nat -> Bool
even Z = True
even (S k) = odd k where
  odd Z = False
  odd (S k) = even k

test : List Nat
test = [c (S 1), c Z, d (S Z)]
  where c x = 42 + x
        d y = c (y + 1 + z y)
              where z w = y + w

-- http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#first-class-types
isSingleton : Bool -> Type
isSingleton True = Nat
isSingleton False = List Nat

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs

main : IO ()
main = do
    -- http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#functions
    assert (plus' (S (S Z)) (S (S Z))) 4
    assert (mult' (S (S (S Z))) (plus' (S (S Z)) (S (S Z)))) 12
    putStrLn' $ show $ reverse [1, 2, 3]
    assert (reverse [1, 2, 3]) ([3, 2, 1])

    putStrLn' $ "sum False [1, 2, 3] = " ++ show (sum False [1, 2, 3])
    putStrLn' $ "sum True 5 = " ++ show (sum True 5)

    putStrLn' $ if x == 6 * 6 + 6 then "The answer!" else "Not the answer"
    putStrLn' $
        showInt $ case (annInt 12, annInt 2) of
             (a, b) => a + b


text:
module NoDeclaration

identity : (a : Type) -> a -> a
identity _ x = x

idNat = identity Nat

double = (S 1 *)

test : idNat (double 3) === 6
test = Refl

unwords : List String -> String
unwords [] = ""
unwords [x] = x
unwords (x::xs) = x ++ " " ++ unwords xs

helloWorld = unwords ["hello", "world"]

test' : NoDeclaration.helloWorld === "hello world"
test' = Refl

cat x y = unwords [x, show {ty = Nat} y]


text:
module StringLiteral

Str : String
Str = """
  First line

  Third line
  """

Str2NL : String
Str2NL = "First line\n\nThird line"

sss : Str === Str2NL
sss = Refl

Str1NL : String
Str1NL = "First line\nThird line"

sss' : (Str == Str1NL) === False
sss' = Refl