text:
module Cordial.EDSL.Specification.API

import Data.Vect
import Data.List.Quantifiers
import Data.Ranged

import Text.Markup.Edda

import Language.EDSL.SingleStateVar

import Cordial.Model.Specification

import Cordial.EDSL.Specification.Lang

%default total
%access public export

namespace Signals

  defSig : (label  : Var)
        -> (kind   : PortShape)
        -> (wirety : WireTy)
        -> (width  : PortWidthDesc kind)

        -> (idx : InContext (CanUseVar labelTy label) old)

        -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)

  defSig var k' k w idx =
    signal var k' k PC w High IsRequired IP NoValue Empty idx

  replicate : (n : Nat)
           -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
           -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  replicate n (Expr (DeclareSignal label kind wirety flow width sense required origin vorigin doc prf)) =
    Expr (Replicate n label kind wirety flow width sense required origin vorigin doc prf)
  replicate n (Expr (Replicate k var kind wirety flow width sense required origin vorigin doc prf)) =
    Expr (Replicate n var kind wirety flow width sense required origin vorigin doc prf)

  namespace Generic

    general : (label : Var)
           -> (kind : PortShape)
           -> {auto idx : InContext (CanUseVar labelTy label) old}
           -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)
    general var kind {idx} = defSig var kind General UserDefined idx

    clock : (label  : Var)
         -> (edge   : Maybe ClockEdge)
         -> (delay  : Maybe Delay)
         -> (tcons  : Maybe (RangedNat 0 100))

         -> {auto idx : InContext (CanUseVar labelTy label) old}

         -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)
    clock var e d t {idx} =
      defSig var WIRE (Clock e d t) One idx

    control : (label : Var)
           -> {auto idx : InContext (CanUseVar labelTy label) old}
           -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)
    control var {idx} = defSig var WIRE Control One idx

    interrupt : (label    : Var)
             -> {auto idx : InContext (CanUseVar labelTy label) old}
             -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)
    interrupt var {idx} = defSig var WIRE Interrupt One idx

    reset : (label : Var)
         -> {auto idx : InContext (CanUseVar labelTy label) old}
         -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)
    reset var {idx} = defSig var WIRE Reset One  idx

    info : (label : Var)
        -> (width : PortWidthDesc ARRAY)
        -> {auto idx : InContext (CanUseVar labelTy label) old}
        -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)
    info var width {idx} = defSig var ARRAY Information width idx

    bus : (label : Var)
       -> (width : PortWidthDesc ARRAY)
       -> {auto idx : InContext (CanUseVar labelTy label) old}
       -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)
    bus var width {idx} = defSig var ARRAY DataWire width idx

    address : (label : Var)
           -> (width  : PortWidthDesc ARRAY)
           -> {auto idx : InContext (CanUseVar labelTy label) old}
           -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)
    address var width {idx} = defSig var ARRAY AddressWire width idx

  namespace Unrestricted

    info : (label  : Var)
        -> {auto idx : InContext (CanUseVar labelTy label) old}
        -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)
    info var {idx} = Generic.info var UserDefined {idx=idx}

    bus : (label : Var)
       -> {auto idx : InContext (CanUseVar labelTy label) old}
       -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)
    bus var {idx} = Generic.bus var UserDefined {idx=idx}

    address : (label : Var)
           -> {auto idx : InContext (CanUseVar labelTy label) old}
           -> LangM m () (LangIDL labelTy) (TyExpr DECL) old (const $ update Consume old idx)
    address var {idx} = Generic.address var UserDefined {idx=idx}

namespace Accessor

  setDoc : (d   : String -> Either String (Edda SNIPPET))
        -> (src : String)
        -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
        -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  setDoc d src (Expr (DeclareSignal label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (DeclareSignal label kind wirety flow width sense required origin defaultValue (newDocString src d) idx)
  setDoc d src (Expr (Replicate n label kind wirety flow width sense required origin defaultValue doc idx)) = Expr (Replicate n label kind wirety flow width sense required origin defaultValue (newDocString src d) idx)

namespace Modifier

  system : String
        -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
        -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  system n (Expr (DeclareSignal label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (DeclareSignal label kind wirety flow width sense required (SYSTEM n) defaultValue doc idx)

  system m (Expr (Replicate n label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (Replicate n label kind wirety flow width sense required (SYSTEM m) defaultValue doc idx)

  fromEither : LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
            -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  fromEither (Expr (DeclareSignal label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (DeclareSignal label kind wirety PCCP width sense required origin defaultValue doc idx)
  fromEither (Expr (Replicate n label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (Replicate n label kind wirety PCCP width sense required origin defaultValue doc idx)

  fromInitiator : LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
               -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  fromInitiator (Expr (DeclareSignal label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (DeclareSignal label kind wirety PC width sense required origin defaultValue doc idx)
  fromInitiator (Expr (Replicate n label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (Replicate n label kind wirety PC width sense required origin defaultValue doc idx)

  fromTarget : LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
            -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  fromTarget (Expr (DeclareSignal label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (DeclareSignal label kind wirety CP width sense required origin defaultValue doc idx)
  fromTarget (Expr (Replicate n label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (Replicate n label kind wirety CP width sense required origin defaultValue doc idx)

  fromInitiatorAlways : LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
                     -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  fromInitiatorAlways (Expr (DeclareSignal label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (DeclareSignal label kind wirety ConstP width sense required origin defaultValue doc idx)
  fromInitiatorAlways (Expr (Replicate n label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (Replicate n label kind wirety ConstP width sense required origin defaultValue doc idx)

  fromTargetAlways : LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
                  -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  fromTargetAlways (Expr (DeclareSignal label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (DeclareSignal label kind wirety ConstC width sense required origin defaultValue doc idx)
  fromTargetAlways (Expr (Replicate n label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (Replicate n label kind wirety ConstC width sense required origin defaultValue doc idx)

  opt : LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
     -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  opt (Expr (DeclareSignal label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (DeclareSignal label kind wirety flow width sense CompletelyOptional origin defaultValue doc idx)
  opt (Expr (Replicate n label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (Replicate n label kind wirety flow width sense CompletelyOptional origin defaultValue doc idx)

  targetOpt : LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
           -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  targetOpt (Expr (DeclareSignal label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (DeclareSignal label kind wirety flow width sense ConsumerOptional origin defaultValue doc idx)
  targetOpt (Expr (Replicate n label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (Replicate n label kind wirety flow width sense ConsumerOptional origin defaultValue doc idx)

  initiatorOpt : LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
              -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  initiatorOpt (Expr (DeclareSignal label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (DeclareSignal label kind wirety flow width sense ProducerOptional origin defaultValue doc idx)
  initiatorOpt (Expr (Replicate n label kind wirety flow width sense required origin defaultValue doc idx)) =
    Expr (Replicate n label kind wirety flow width sense ProducerOptional origin defaultValue doc idx)

  setSensitivity : (s : Sensitivity)
                -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
                -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  setSensitivity s (Expr (DeclareSignal label kind wirety flow width _ required origin vorigin doc idx)) =
    Expr (DeclareSignal label kind wirety flow width s required origin vorigin doc idx)
  setSensitivity s (Expr (Replicate n label kind wirety flow width _ required origin vorigin doc idx)) =
    Expr (Replicate n label kind wirety flow width s required origin vorigin doc idx)

namespace Metadata

  setVendor : String -> LangM m () (LangIDL labelTy) (TyExpr MDATA) old (const old)
  setVendor v = setMetadata (\mdata => record {mvendor = Just v} mdata)

  setLibrary : String -> LangM m () (LangIDL labelTy) (TyExpr MDATA) old (const old)
  setLibrary v = setMetadata (\mdata => record {mlibrary = Just v} mdata)

  setName : String -> LangM m () (LangIDL labelTy) (TyExpr MDATA) old (const old)
  setName v = setMetadata (\mdata => record {mname = Just v} mdata)

  setVersion : String -> LangM m () (LangIDL labelTy) (TyExpr MDATA) old (const old)
  setVersion v = setMetadata (\mdata => record {mversion = Just v} mdata)

  setMaxInitiators : (maxp : Whole) -> LangM m () (LangIDL labelTy) (TyExpr MDATA) old (const old)
  setMaxInitiators m = setMetadata (\mdata => record {mmaxp = Just m} mdata)

  setMaxTargets : (maxc : Whole) -> LangM m () (LangIDL labelTy) (TyExpr MDATA) old (const old)
  setMaxTargets m = setMetadata (\mdata => record {mmaxc = Just m} mdata)

  setCommunicationStyle : CommStyle -> LangM m () (LangIDL labelTy) (TyExpr MDATA) old (const old)
  setCommunicationStyle v = setMetadata (\mdata => record {mcstyle = Just v} mdata)

  setDoc : (d   : String -> Either String (Edda SNIPPET))
        -> (src : String)
        -> LangM m () (LangIDL labelTy) (TyExpr MDATA) old (const old)
  setDoc d src = setMetadata (\mdata => record {mdoc = Just (newDocString src d)} mdata)

  (#) : LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
     -> (LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
       -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK)
     -> LangM m () (LangIDL labelTy) (TyExpr DECL) old newK
  (#) a f = f a

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Data.HVect

import Decidable.Equality
import Data.List
import public Data.Vect
import Data.Vect.Elem

%default total

||| Heterogeneous vectors where the type index gives, element-wise,
||| the types of the contents.
public export
data HVect : Vect k Type -> Type where
  Nil : HVect []
  (::) : t -> HVect ts -> HVect (t :: ts)

||| Extract an element from an HVect.
|||
||| ```idris example
||| > index 0 (the (HVect _) [1, "string"])
||| 1
||| ```
public export
index : (1 i : Fin k) -> (1 _ : HVect ts) -> index i ts
index FZ (x :: xs) = x
index (FS j) (x :: xs) = index j xs

||| Delete an element from an HVect.
|||
||| ```idris example
||| > deleteAt 0 (the (HVect _) [1, "string"])
||| ["string"]
||| ```
public export
deleteAt : (1 i : Fin (S l)) -> (1 _ : HVect ts) -> HVect (deleteAt i ts)
deleteAt FZ (x :: xs) = xs
deleteAt (FS FZ) (x :: (y :: xs)) = x :: xs
deleteAt (FS (FS j)) (x :: (y :: xs)) = x :: deleteAt (FS j) (y :: xs)

||| Replace an element in an HVect.
|||
||| ```idris example
||| > replaceAt 0 "firstString" (the (HVect _) [1, "string"])
||| ["firstString", "string"]
||| ```
public export
replaceAt : (1 i : Fin k) -> t -> (1 _ : HVect ts) -> HVect (replaceAt i t ts)
replaceAt FZ y (x :: xs) = y :: xs
replaceAt (FS j) y (x :: xs) = x :: replaceAt j y xs

||| Update an element in an HVect.
|||
||| ```idris example
||| > updateAt 0 (const True) (the (HVect _) [1, "string"])
||| [True, "string"]
||| ```
public export
updateAt : (1 i : Fin k) -> (index i ts -> t) -> (1 _ : HVect ts) -> HVect (replaceAt i t ts)
updateAt FZ f (x :: xs) = f x :: xs
updateAt (FS j) f (x :: xs) = x :: updateAt j f xs

||| Append two `HVect`s.
|||
||| ```idris example
||| > (the (HVect _) [1]) ++ (the (HVect _) ["string"])
||| [1, "string"]
||| ```
public export
(++) : (1 _ : HVect ts) -> HVect us -> HVect (ts ++ us)
(++) [] ys = ys
(++) (x :: xs) ys = x :: (xs ++ ys)

public export
Eq (HVect []) where
  [] == [] = True

public export
(Eq t, Eq (HVect ts)) => Eq (HVect (t :: ts)) where
  (x :: xs) == (y :: ys) = x == y && xs == ys

public export
consInjective1 : {0 xs, ys: HVect ts} -> {0 x, y: a} -> (1 _ : x :: xs = y :: ys) -> x = y
consInjective1 Refl = Refl

public export
consInjective2 : {0 xs, ys: HVect ts} -> {0 x, y: a} -> (1 _ : x :: xs = y :: ys) -> xs = ys
consInjective2 Refl = Refl

public export
DecEq (HVect []) where
  decEq [] [] = Yes Refl

public export
(DecEq t, DecEq (HVect ts)) => DecEq (HVect (t :: ts)) where
  decEq (x :: xs) (y :: ys) with (decEq x y)
    decEq (z :: xs) (z :: ys) | Yes Refl with (decEq xs ys)
      decEq (z :: zs) (z :: zs) | Yes Refl | Yes Refl = Yes Refl
      decEq (z :: xs) (z :: ys) | Yes Refl | No contra = No (contra . consInjective2)
    decEq (x :: xs) (y :: ys) | No contra = No (contra . consInjective1)

public export
interface Shows (k : Nat) (ts : Vect k Type) where
  shows : HVect ts -> Vect k String

public export
Shows Z [] where
  shows [] = []

public export
(Show t, Shows len ts) => Shows (S len) (t :: ts) where
  shows (x :: xs) = show x :: shows xs

public export
(Shows len ts) => Show (HVect ts) where
  show xs = "[" ++ (pack . intercalate [','] . map unpack . toList $ shows xs) ++ "]"

||| Extract an arbitrary element of the correct type.
|||
||| ```idris example
||| > get [1, "string"] {p = Here}
||| 1
||| ```
public export
get : (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> t
get (x :: xs) {p = Here} = x
get (x :: xs) {p = (There p')} = get xs

||| Replace an element with the correct type. (Homogeneous)
|||
||| ```idris example
||| > put 2 [1, "string"]
||| [2, "string"]
||| ```
public export
put : t -> (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> HVect ts
put y (x :: xs) {p = Here} = y :: xs
put y (x :: xs) {p = (There p')} = x :: put y xs

||| Replace an element with the correct type. (Heterogeneous)
|||
||| ```idris example
||| > htPut True [1, "string"] {p = Here}
||| [True, "string"]
||| ```
public export
htPut : u -> (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> HVect (replaceByElem ts p u)
htPut y (x :: xs) {p = Here} = y :: xs
htPut y (x :: xs) {p = There p'} = x :: htPut y xs

||| Update an element with the correct type. (Homogeneous)
|||
||| ```idris example
||| > update (const "hello world!") [1, "string"]
||| [1, "hello world!"]
||| ```
public export
update : (t -> t) -> (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> HVect ts
update f (x :: xs) {p = Here} = f x :: xs
update f (x :: xs) {p = There p'} = x :: update f xs

||| Update an element with the correct type. (Heterogeneous)
|||
||| ```idris example
||| > htUpdate (\_ : String => 2) [1, "string"]
||| [1, 2]
||| ```
public export
htUpdate : (t -> u) -> (1 _ : HVect ts) -> {auto 1 p : Elem t ts} -> HVect (replaceByElem ts p u)
htUpdate f (x :: xs) {p = Here} = f x :: xs
htUpdate f (x :: xs) {p = (There p')} = x :: htUpdate f xs

ext: idr


text:
||| Module for serialising and deserialising Inigo packages
module Inigo.Package.JSON

import Data.List
import Data.Maybe
import Inigo.Package.Package
import Language.JSON
import SemVar

extraDepToJSON : ExtraDep -> JSON
extraDepToJSON (MkExtraDep Git commit url subDirs) = JObject
    [ ("download", JString "git")
    , ("commit", JString commit)
    , ("url", JString url)
    , ("subDirs", JArray (JString <$> subDirs))
    ]
extraDepToJSON (MkExtraDep SubDir _ url subDirs) = JObject
    [ ("download", JString "folder")
    , ("url", JString url)
    , ("subDirs", JArray (JString <$> subDirs))
    ]

nullable : Lazy (a -> JSON) -> Maybe a -> JSON
nullable = maybe JNull

export
encodePackage : Package -> JSON
encodePackage pkg = JObject
    [ ("ns", JString pkg.ns)
    , ("package", JString pkg.package)
    , ("version", JString (show pkg.version))
    , ("description", nullable JString pkg.description)
    , ("link", nullable JString pkg.link)
    , ("readme", nullable JString pkg.readme)
    , ("modules", JArray (JString <$> pkg.modules))
    , ("depends", JArray (JString <$> pkg.depends))
    , ("license", nullable JString pkg.license)
    , ("sourcedir", JString pkg.sourcedir)
    , ("main", nullable JString pkg.main)
    , ("executable", nullable JString pkg.executable)
    , ("deps", JArray (mkDep <$> pkg.deps))
    , ("dev-deps", JArray (mkDep <$> pkg.devDeps))
    , ("extra-deps", JArray (extraDepToJSON <$> pkg.extraDeps))
    ]
  where
    mkDep : (List String, Requirement) -> JSON
    mkDep (ns, semvar) = JObject
        [ ("name", JArray (JString <$> ns))
        , ("semvar", JString (show semvar))
        ]

export
encodeAsJSON : Package -> String
encodeAsJSON = show . JSON.encodePackage

namespace Parse

    key : String -> JSON -> Maybe JSON
    key k (JObject kvs) = lookup k kvs
    key _ _ = Nothing

    string : JSON -> Maybe String
    string (JString str) = Just str
    string _ = Nothing

    stringKey : String -> JSON -> Maybe String
    stringKey k json = key k json >>= \case
        JString str => Just str
        _ => Nothing

    arrayKey : String -> JSON -> Maybe (List JSON)
    arrayKey k json = key k json >>= \case
        JArray arr => Just arr
        _ => Nothing

    nullable : Maybe a -> Maybe (Maybe a)
    nullable (Just x) = Just (Just x)
    nullable Nothing = Just Nothing

    parseExtraDep : JSON -> Maybe ExtraDep
    parseExtraDep json = do
        url <- stringKey "url" json
        subDirs <- arrayKey "subDirs" json >>= traverse string
        download <- stringKey "download" json
        case download of
            "git" => do
                commit <- stringKey "commit" json
                Just $ MkExtraDep Git commit url subDirs
            "folder" => Just $ MkExtraDep SubDir () url subDirs
            _ => Nothing

    export
    parsePackage : JSON -> Maybe Package
    parsePackage json = do
        ns <- stringKey "ns" json
        package <- stringKey "package" json
        version <- stringKey "version" json >>= parseVersion
        description <- nullable $ stringKey "description" json
        link <- nullable $ stringKey "link" json
        readme <- nullable $ stringKey "readme" json
        modules <- arrayKey "modules" json >>= traverse string
        depends <- arrayKey "depends" json >>= traverse string
        license <- nullable $ stringKey "license" json
        sourcedir <- stringKey "sourcedir" json
        main <- nullable $ stringKey "main" json
        executable <- nullable $ stringKey "executable" json
        deps <- arrayKey "deps" json >>= traverse parseDep
        devDeps <- arrayKey "dev-deps" json >>= traverse parseDep
        extraDeps <- arrayKey "extra-deps" json >>= traverse parseExtraDep
        Just $ MkPackage
            { ns, package, version, description, link, readme
            , modules, depends, license, sourcedir
            , main, executable, deps, devDeps, extraDeps
            }
      where
        parseDep : JSON -> Maybe (List String, Requirement)
        parseDep json = do
            ns <- arrayKey "name" json >>= traverse string
            var <- stringKey "semvar" json >>= parseRequirement
            Just (ns, var)

export
decodeJSON : String -> Maybe Package
decodeJSON = parse >=> parsePackage

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
||| Spec: https://webassembly.github.io/spec/core/valid/types.html#block-types
module WebAssembly.Validation.Types.BlockTypes

import WebAssembly.Structure
import WebAssembly.Validation.Conventions

-------------------------------------------------------------------------------
-- Validation Rules
-------------------------------------------------------------------------------

||| Valid blocks
public export
data ValidBlockType : Context -> BlockType -> FuncType -> Type where
  ||| Proof that a BlockType is valid for some given type-index
  |||
  |||   C.types[typeidx] = functype
  |||-----------------------------------
  |||      C ⊢ typeidx : functype
  |||
  MkValidTypeIdxBlock : (c : Context) -> (i : TypeIdx)
    -> {auto in_bounds: InBounds i (types c)}
    -> ValidBlockType c (BlockTypeTypeIdx i) (index i (types c))
  ||| Proof that a BlockType without result-type is valid
  |||
  |||-------------------------------------
  |||   C ⊢ [] : [] -> []
  |||
  MkValidBlockWithoutResult : (c : Context) -> ValidBlockType c BlockTypeEmpty ([] ->> [])
  ||| Proof that a BlockType with some result-type is valid
  |||
  |||-------------------------------------
  |||   C ⊢ [valtype] : [] -> [valtype]
  |||
  MkValidBlockWithResult : (c : Context) -> (t : ValType) -> ValidBlockType c (BlockTypeSingelton t) ([] ->> [t])

-------------------------------------------------------------------------------
-- Type Inference
-------------------------------------------------------------------------------

||| If the typeIndex is not present in the context, the block is invalid
total
typeidx_out_of_bounds : (c : Context) -> (i : TypeIdx)
  -> (out_of_bounds: InBounds i (types c) -> Void)
  -> ValidBlockType c (BlockTypeTypeIdx i) ft
  -> Void
typeidx_out_of_bounds c i out_of_bounds (MkValidTypeIdxBlock c i {in_bounds}) = out_of_bounds in_bounds

||| If the typeIndex is not present in the context, no type can be inferred
total
typeidx_out_of_bounds2 : (c : Context) -> (i : TypeIdx)
  -> (out_of_bounds: InBounds i (types c) -> Void)
  -> (ft ** ValidBlockType c (BlockTypeTypeIdx i) ft)
  -> Void
typeidx_out_of_bounds2 c i out_of_bounds (x ** pf) = typeidx_out_of_bounds c i out_of_bounds pf

||| Infer the FuncType of some BlockType
total public export
inferBlockType : (c : Context)
              -> (bt : BlockType)
              -> Dec (ft ** ValidBlockType c bt ft)
inferBlockType c BlockTypeEmpty = Yes $ ([] ->> [] ** MkValidBlockWithoutResult c)
inferBlockType c (BlockTypeSingelton vt) = Yes $ ([] ->> [vt] ** MkValidBlockWithResult c vt)
inferBlockType c (BlockTypeTypeIdx i) = case inBounds i (types c) of
  No out_of_bounds => No $ typeidx_out_of_bounds2 c i out_of_bounds
  Yes in_bounds    => Yes $ ((index i (types c)) ** MkValidTypeIdxBlock c i)

-------------------------------------------------------------------------------
-- Type Checking
-------------------------------------------------------------------------------

||| The bounds-proof does not affect the result of the index-function
total
index_proof_irrelevant : {i : TypeIdx, a : Type, xs : List a}
  -> (prfA : InBounds i xs)
  -> (prfB: InBounds i xs)
  -> (index i xs {ok = prfA}) = (index i xs {ok = prfB})
index_proof_irrelevant InFirst InFirst = Refl
index_proof_irrelevant (InLater prfA') (InLater prfB') = index_proof_irrelevant prfA' prfB'

||| If the FuncType in the context does not match the expected FuncType,
||| the block is invalid.
total
check_failed : (c : Context) -> (i : TypeIdx)
            -> {auto prfA : InBounds i (types c)}
            -> ((ft = index i (types c)) -> Void)
            -> ValidBlockType c (BlockTypeTypeIdx i) ft -> Void
check_failed {prfA} c i contra (MkValidTypeIdxBlock c i {in_bounds=prfB}) = contra (rewrite index_proof_irrelevant prfA prfB in Refl)

||| If the expected type does not match the actual type, the check fails
total
valtype_without_result_check_failed : (contra : (ft = ([] ->> [])) -> Void) -> ValidBlockType c BlockTypeEmpty ft -> Void
valtype_without_result_check_failed contra (MkValidBlockWithoutResult c) = contra Refl

||| If the expected type does not match the actual type, the check fails
total
valtype_with_result_check_failed : (contra : (ft = ([] ->> [vt])) -> Void) -> ValidBlockType c (BlockTypeSingelton vt) ft -> Void
valtype_with_result_check_failed contra (MkValidBlockWithResult c vt) = contra Refl

||| Typecheck a BlockType
total public export
checkBlockType :  (c : Context)
              -> (bt : BlockType)
              -> (ft : FuncType)
              -> Dec (ValidBlockType c bt ft)
checkBlockType c BlockTypeEmpty ft = case decEq ft ([] ->> []) of
  No contra => No (valtype_without_result_check_failed contra)
  Yes Refl  => Yes $ MkValidBlockWithoutResult c
checkBlockType c (BlockTypeSingelton vt) ft = case decEq ft ([] ->> [vt]) of
  No contra => No (valtype_with_result_check_failed contra)
  Yes Refl  => Yes $ MkValidBlockWithResult c vt
checkBlockType c (BlockTypeTypeIdx i) ft = case inBounds i (types c) of
  No out_of_bounds => No $ typeidx_out_of_bounds c i out_of_bounds
  Yes in_bounds    => case decEq ft (index i (types c)) of
    No contra => No (check_failed c i contra)
    Yes Refl  => Yes $ MkValidTypeIdxBlock c i

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Main

import Postgres
import Data.Strings
import Data.String.Extra
import Data.List
import Data.HVect

error : Show a => {default "" ctx: String} -> a -> String
error {ctx} diag = let ctxStr = if (strLength ctx) == 0
                                   then ""
                                   else " (" ++ ctx ++ ")" in
                                     "Error" ++ ctxStr ++ ": " ++ (show diag)

putErr : Show a => {default "" ctx: String} -> a -> IO ()
putErr {ctx} diag = putStrLn $ error {ctx=ctx} diag

putNotif : IO Notification -> IO ()
putNotif n = putStrLn $ "Notification on channel " ++ (show (!n).channel)

notificationLoop : Stream (IO Notification) -> IO ()
notificationLoop (n :: ns) = do putNotif n
                                notificationLoop ns

jsonStatement : Connection -> IO ()
jsonStatement conn = do
  cmd <- getLine
  Just json <- jsonQuery cmd conn
   | Nothing => putErr "command failed."
  putStrLn $ show json

describe : String -> Connection -> IO ()
describe query conn = do
  Right (_ ** _ ** (headers, _)) <- stringQuery True query conn
    | Left err => putStrLn err
  putStrLn (join ", " $ show <$> headers)

describeResult : Connection -> IO ()
describeResult conn = do
  query <- getLine
  describe query conn

showResult : Connection -> IO ()
showResult conn = do
  query <- getLine
  Right (_ ** _ ** rows) <- stringQuery False query conn
    | Left err => putStrLn err
  for_ rows $ \row => do
    putStrLn (join ", " $ (\case Just s => s; Nothing => "null") <$> row)

showTables : Connection -> IO ()
showTables conn = do
  Right (_ ** rows) <- expectedQuery [String, String, Bool] "select schemaname, tablename, hasindexes from pg_tables limit 10" conn
    | Left err => putStrLn err
  for_ rows $ \(schema :: table :: hasIndices :: []) => do
    putStrLn $ schema ++ "." ++ table ++ (if hasIndices then " (has indices)" else " (doesn't have indices)")

showFunctions : Connection -> IO ()
showFunctions conn = do
  Right (_ ** rows) <- expectedQuery [String, List String] "select proname, proargnames from pg_proc where proargnames != '{}' limit 10" conn
    | Left err => putStrLn err
  for_ rows $ \(name :: args :: []) => do
    putStrLn $ name ++ "(" ++ (join ", " args) ++ ")"

describeFnTable : Connection -> IO ()
describeFnTable conn = do
  describe "select * from pg_proc limit 1" conn

run : Connection -> IO ()
run conn = do
  putStrLn "Connected"

  COMMAND_OK <- listen "test_channel" conn
   | x => putErr {ctx="Listening"} x

  putStrLn "Choose One:"
  putStrLn "1 => Arbitrary JSON Statement"
  putStrLn "2 => Notification Loop"
  putStrLn "3 => Describe Arbitrary Result"
  putStrLn "4 => Describe pg_proc table."
  putStrLn "5 => Show Arbitrary SELECT Result Rows"
  putStrLn "6 => Show 10 tables."
  putStrLn "7 => Show 10 functions."
  opt <- getLine
  case (stringToNatOrZ opt) of
       1 => do putStrLn "Enter SQL: "
               jsonStatement conn
       2 => do putStrLn "Entering notification loop..."
               notificationLoop $ notificationStream conn
       3 => do putStrLn "Enter SQL: "
               describeResult conn
       4 => describeFnTable conn
       5 => do putStrLn "Enter SQL: "
               showResult conn
       6 => do putStrLn "Showing 10 tables..."
               showTables conn
       7 => do putStrLn "Showing 10 functions..."
               showFunctions conn
       _ => pure ()

public export
main : IO ()
main = do
  putStrLn "postgres url:"
  url <- getLine
  putStrLn "starting up..."

  Right _ <- withDB url (exec run)
    | Left err => putErr {ctx="Connection"} err

  putStrLn "shutting down..."

--
-- As seen in README
--

-- Just an example of opening and closing; it's easier to use
-- `withDB`.
openAndClose : (url : String) -> Database () Closed (const Closed)
openAndClose url =
  do initDatabase
     OK <- openDatabase url
       | Failed err => pure () -- connection error!
     closeDatabase

-- Again, an example used in the Readme
runRoutine : HasIO io => (url : String) -> io (Either String ())
runRoutine url =
  withDB url $ pure ()

-- more example
execCommand : Database () Open (const Open)
execCommand = do liftIO' $ putStrLn "Woo! Running a command!"
                 exec $ (\c => pure ())

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
module Idrlisp.Pattern

import Idrlisp.Sexp

%default total

public export
record Pattern where
  constructor MkPattern
  fixed : List String
  rest : Maybe String

export
Eq Pattern where
  (==) x y = fixed x == fixed y && rest x == rest y

export
Show Pattern where
  show x =
    let fixed = map Sym (fixed x) in
    let rest = map Sym (rest x) in
    assert_total $ show $ the (Sexp ()) $ foldr (::) (fromMaybe Nil rest) fixed

export
build : Sexp a -> Either (Sexp a) Pattern
build (Sym x) = Right $ MkPattern [] (Just x)
build Nil = Right $ MkPattern [] Nothing
build (Sym x :: s) = record { fixed $= (x::) } <$> build s
build (x :: s) = Left x
build s = Left s

export
bind : Pattern -> List (Sexp a) -> Either String (List (String, Sexp a))
bind pat xs = go (fixed pat) (rest pat) xs
  where
    go : List String -> Maybe String -> List (Sexp a) -> Either String (List (String, Sexp a))
    go (p :: ps) rest [] = Left "not enough arguments"
    go (p :: ps) rest (a :: args) = ((p, a) ::) <$> go ps rest args
    go [] Nothing [] = Right []
    go [] Nothing (a :: args) = Left "too much arguments"
    go [] (Just rest) args = Right [(rest, foldr (::) Nil args)]

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Ipkg.Types

import Data.List1

public export
data PkgVersion = PV (List1 Nat)

public export
record PkgVersionBounds where
  constructor PVB
  lowerBound : Maybe PkgVersion
  lowerInclusive : Bool
  upperBound : Maybe PkgVersion
  upperInclusive : Bool

export
anyBounds : PkgVersionBounds
anyBounds = PVB Nothing True Nothing True

public export
record Depends where
  constructor D
  name : String
  bounds : PkgVersionBounds

public export
record Package where
  constructor P
  name : String
  version : Maybe PkgVersion
  strFields : List (String, String)
  depends : List Depends
  modules : List String

export
def : String -> Package
def s = P s Nothing [] [] []

public export
Show PkgVersion where
  show (PV v) = foldl1By (\acc, next => "\{acc}.\{show next}") show v

public export
Show Depends where
  show (D n b) = n

public export
Show Package where
  show (P n v s d m) =
    "package \{n}\n" ++
    (maybe "" (\x => "version \{show x}\n") v) ++
    "modules: \{show m}\n" ++
    "depends: \{show d}\n" ++
    "strings:\n" ++ show s ++ "\n"

max_stars_repo_name: claymager/ipkg-to-json

max_issues_repo_name: claymager/ipkg-to-json

max_forks_repo_name: claymager/ipkg-to-json


text:
-- ------------------------------------------------------- [ Effs.idr<Process> ]
-- Module    : Effs.idr<Process>
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Readability.Process.Effs

import Effects
import Effect.State

import Readability.Stats

%access export

public export
ReadEffs : List EFFECT
ReadEffs = ['readST ::: STATE RStats]

getReadState : Eff RStats ['readST ::: STATE RStats]
getReadState = 'readST :- get

putReadState : RStats -> Eff () ['readST ::: STATE RStats]
putReadState r = 'readST :- put r

updateReadState : (RStats -> RStats) -> Eff () ['readST ::: STATE RStats]
updateReadState f = 'readST :- update f

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

max_stars_repo_name: jfdm/idris-read

max_issues_repo_name: jfdm/idris-read

max_forks_repo_name: jfdm/idris-read


text:
module Typing.Common

import public General

import public Core.Variable
import public Core.Term
import public Core.Abstraction
import public Core.ConSig
import public Core.Evaluation

export
extract : (a -> Bool) -> List a -> Maybe (a, List a)
extract _ [] = Nothing
extract p (x::xs) with (p x)
	| True  = Just (x,xs)
	| False = do
		(y,xs') <- extract p xs
		pure (y,x::xs')

public export
Definitions : Type
Definitions = Environment FullName (Term >< Term)

public export
ContextEntry : Type
ContextEntry = Int >< String >< Term

public export
Context : Type
Context = List ContextEntry

public export
MetaVar : Type
MetaVar = Int

public export
Substitution : Type
Substitution = List $ MetaVar >< Term

public export
ModuleAliases : Type
ModuleAliases = List $ (String \/ FullName) >< FullName

-- YY8YY  oYYo oYYYo YY8YY  o8o  YY8YY 8YYYY
--   0   0   " %___    0   8   8   0   8___
--   0   0   , `"""p   0   8YYY8   0   8"""
--   0    YooY YoooY   0   0   0   0   8oooo

public export
record TCState where
	constructor NewTCState
	tcSig : Signature Term
	tcDefs : Definitions
	tcCtx : Context
	tcNextName : Int
	tcNextMeta : MetaVar
	tcSubs : Substitution
	tcAliases : ModuleAliases
	tcModuleNames : List String

public export
TypeCheckerState TCState (Signature Term) Definitions Context where
	typeCheckerSig = tcSig
	putTypeCheckerSig s sig = record { tcSig = sig } s
	typeCheckerDefs = tcDefs
	putTypeCheckerDefs s defs = record { tcDefs = defs } s
	addTypeCheckerDefs s edefs = record { tcDefs = fromList(toList edefs ++ toList (tcDefs s)) } s
	typeCheckerCtx = tcCtx
	putTypeCheckerCtx s ctx = record { tcCtx = ctx } s
	addTypeCheckerCtx s ectx = record { tcCtx = ectx ++ tcCtx s } s
	typeCheckerNextName = tcNextName
	putTypeCheckerNextName s n = record { tcNextName = n } s

public export
TypeCheckerMetas TCState Substitution where
	typeCheckerNextMeta = tcNextMeta
	putTypeCheckerNextMeta s n = record { tcNextMeta = n } s
	typeCheckerSubs = tcSubs
	putTypeCheckerSubs s subs = record { tcSubs = subs } s

-- YY8YY 0   0 8YYYo 8YYYY  oYYo 0   0 8YYYY  oYYo 0  oY 8YYYY 8YYYo
--   0   "o o" 8___P 8___  0   " 8___8 8___  0   " 8_oY  8___  8___P
--   0     0   8"""  8"""  0   , 8"""8 8"""  0   , 8"Yo  8"""  8""Yo
--   0     0   0     8oooo  YooY 0   0 8oooo  YooY 0  Yo 8oooo 0   0

public export
TypeChecker : Type -> Type
TypeChecker = StateT TCState (Either String)

public export
TCMonad TypeChecker TCState (Signature Term) Definitions Context where {}

public export
TCPolyMonad TypeChecker TCState (Signature Term) Definitions Context Substitution where {}

export
runTypeChecker : TypeChecker a ->
	Signature Term ->
	Definitions ->
	Context ->
	Int ->
	ModuleAliases ->
	List String ->
	String \/ (a >< TCState)
runTypeChecker checker sig defs ctx i als mods = runStateT checker (NewTCState sig defs ctx i 0 [] als mods)

export
aliases : TypeChecker ModuleAliases
aliases = map tcAliases get

export
putAliases : ModuleAliases -> TypeChecker ()
putAliases als = do
	s <- get
	put $ record { tcAliases = als } s

export
moduleNames : TypeChecker (List String)
moduleNames = map tcModuleNames get

-- Y8Y 8o  0 8YYYY 8YYYY 8YYYo 8YYYo 8YYYY 8888_
--  0  8Yo 8 8___  8___  8___P 8___P 8___  0   0
--  0  8 Yo8 8"""  8"""  8""Yo 8""Yo 8"""  0   0
-- o8o 0   8 0     8oooo 0   0 0   0 8oooo 8oooY

infix 4 <:>
||| Inferred and elaborated type
public export
data InferredF a b = (<:>) a b

public export
Inferred : Type
Inferred = InferredF Term Term

export
termHalf : Inferred -> Term
termHalf (x <:> t) = x

export
typeHalf : Inferred -> Term
typeHalf (x <:> t) = t

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
module Eval

-- Evaluators for terms in the simply-typed
-- lambda calculus.

import BigStep
import Equivalence
import Determinism
import Progress
import Step
import Subst
import Term

%access export

------------------------------------------------------------
-- Begin: EVALUATOR (FORMALLY) BASED ON SMALL-STEP SEMANTICS

eval : (e : Term [] t) -> (e' : Term [] t ** (Value e', TransStep e e'))
eval e = case progress e of
  Left v           => (e ** (v, TStRefl e))
  Right (e' ** s') => let (e'' ** (v'', s'')) = eval e'
                      in (e'' ** (v'', TStTrans s' s''))

-- End: EVALUATOR (FORMALLY) BASED ON SMALL-STEP SEMANTICS
----------------------------------------------------------

----------------------------------------------------------
-- Begin: EVALUATOR INFORMALLY BASED ON BIG-STEP SEMANTICS

eval' : Term [] t -> Term [] t
eval' (TVar _)     impossible
eval' (TAbs e)     = TAbs e
eval' (TApp e1 e2) = let (TAbs e1v) = eval' e1
                         e2v        = eval' e2
                     in eval' $ subst e2v First e1v
eval' (TFix e)     = let (TAbs ev) = eval' e
                        in eval' $ subst (TFix (TAbs ev)) First ev
eval' TZero        = TZero
eval' (TSucc e)    = TSucc (eval' e)
eval' (TPred e)    = case eval' e of
                          TZero     => TZero
                          TSucc ev' => ev'
eval' (TIfz e1 e2 e3) = case eval' e1 of
                             TZero   => eval' e2
                             TSucc _ => eval' e3

-- End: EVALUATOR INFORMALLY BASED ON BIG-STEP SEMANTICS
--------------------------------------------------------

--------------------------------------------------------
-- Begin: EVALUATOR FORMALLY BASED ON BIG-STEP SEMANTICS

evalBigStep : (e : Term [] t) -> (e' : Term [] t ** (Value e', BigStep e e'))
evalBigStep (TVar _)   impossible
evalBigStep (TAbs x)   = (TAbs x ** (VAbs, BStValue VAbs))
evalBigStep (TApp x y) = case evalBigStep x of
  (_ ** (VZero, _))         impossible
  (_ ** (VSucc _, _))       impossible
  (TAbs ex ** (VAbs, bStx)) => let (ey ** (_ , bSty)) = evalBigStep y
                                   (er ** (vr, bStr)) = evalBigStep (subst ey First ex)
                               in (er ** (vr, BStApp bStx bSty bStr))
evalBigStep (TFix x)   = case evalBigStep x of
  (_ ** (VZero, _))         impossible
  (_ ** (VSucc _, _))       impossible
  (TAbs ex ** (VAbs, bStx)) => let (er ** (vr, bStr)) = evalBigStep (subst (TFix (TAbs ex)) First ex)
                               in (er ** (vr, BStFix bStx bStr))
evalBigStep TZero      = (TZero ** (VZero, BStValue VZero))
evalBigStep (TSucc x)  = let (ex ** (vx, bStx)) = evalBigStep x
                         in (TSucc ex ** (VSucc vx, BStSucc bStx))
evalBigStep (TPred x)  = case evalBigStep x of
  (TZero    ** (_,        bStx)) => (TZero ** (VZero, BStPredZero bStx))
  (TSucc ex ** (VSucc vx, bStx)) => (ex    ** (vx, BStPredSucc bStx))
  (_        ** (VAbs, _))        impossible
evalBigStep (TIfz x y z) = case evalBigStep x of
  (TZero    ** (_,        bStx)) => let (ey ** (vy, bSty)) = evalBigStep y
                                    in (ey ** (vy, BStIfzZero bStx bSty))
  (TSucc ex ** (VSucc vx, bStx)) => let (ez ** (vz, bStz)) = evalBigStep z
                                    in (ez ** (vz, BStIfzSucc bStx bStz))
  (_ ** (VAbs, _))               impossible

-- End: EVALUATOR FORMALLY BASED ON BIG-STEP SEMANTICS
------------------------------------------------------

-----------------------------------
-- Begin: EQUIVALENCE OF EVALUATORS

total equivEval : (eval e1) = (e2 ** (v2, tst2)) ->
                  (evalBigStep e1) = (e3 ** (v3, bSt3)) ->
                  e2 = e3
equivEval {v2 = v2} {tst2 = tst2} {bSt3 = bSt3} _ _ =
  let (tst3, v3) = bigStepToTransStep bSt3
  in transStepDeterministic v2 tst2 v3 tst3

-- End: EQUIVALENCE OF EVALUATORS
---------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Yet.Another.Path

%default total

public export
val : Nat
val = 5


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 4

-- check that all functions are total
%default total

--
-- Binary Search Trees
--

||| A binary search tree.
data BST : Type -> Type where
  ||| An empty tree.
  Empty : Ord elem =>
          BST elem
  ||| A node with a value, a left subtree, and a right subtree.
  ||| Elements in the left subtree must be strictly lower than the value.
  ||| Elements in the right subtree must be strictly greater than the value.
  Node : Ord elem =>
         (left : BST elem) ->
         (val : elem) ->
         (right : BST elem) ->
         BST elem

||| insert a value in a binary search tree
insert : elem -> BST elem -> BST elem
insert x Empty = Node Empty x Empty
insert x orig@(Node left val right)
  = case compare x val of
      LT => Node (insert x left) val right
      EQ => orig
      GT => Node left val (insert x right)

listToTree : Ord a => List a -> BST a
listToTree [] = Empty
listToTree (x :: xs) = insert x $ listToTree xs

treeToList : BST a -> List a
treeToList Empty = []
treeToList (Node left val right) = treeToList left ++ [val] ++ treeToList right

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module hangman

import Effects

-- State

data GState = Running Nat Nat | NotRunning
data Hangman : GState -> Type

-- Rules

data GRules : Effect where
  Guess : (c : Char) ->
          sig GRules Bool
              (Hangman (Running (S g) (S w)))
              (\inword => if inword
                          then Hangman (Running (S g) w)
                          else Hangman (Running g (S w)))
  Won  : sig GRules () (Hangman (Running g 0))
                       (Hangman NotRunning)
  Lost : sig GRules () (Hangman (Running 0 g))
                       (Hangman NotRunning)
  Get : sig GRules String (Hangman h)


text:
module Idris.IDEMode.SyntaxHighlight

import Core.Context
import Core.Context.Log
import Core.Directory
import Core.InitPrimitives
import Core.Metadata
import Core.TT

import Idris.REPL
import Idris.Syntax
import Idris.Doc.String
import Idris.IDEMode.Commands

import Data.List
import Data.Maybe

import Libraries.Data.PosMap

%default total

SExpable Decoration where
  toSExp Typ      = SExpList [ SymbolAtom "decor", SymbolAtom "type"]
  toSExp Function = SExpList [ SymbolAtom "decor", SymbolAtom "function"]
  toSExp Data     = SExpList [ SymbolAtom "decor", SymbolAtom "data"]
  toSExp Keyword  = SExpList [ SymbolAtom "decor", SymbolAtom "keyword"]
  toSExp Bound    = SExpList [ SymbolAtom "decor", SymbolAtom "bound"]

record Highlight where
  constructor MkHighlight
  location : NonEmptyFC
  filename : String
  name : String
  isImplicit : Bool
  key : String
  decor : Decoration
  docOverview : String
  typ : String
  ns : String

SExpable (FileName, FC) where
  toSExp (fname, fc) = case isNonEmptyFC fc of
    Just (origin, (startLine, startCol), (endLine, endCol)) =>
      SExpList [ SExpList [ SymbolAtom "filename", StringAtom fname ]
               , SExpList [ SymbolAtom "start"
                          , IntegerAtom (cast startLine + 1)
                          , IntegerAtom (cast startCol + 1)
                          ]
               , SExpList [ SymbolAtom "end"
                          , IntegerAtom (cast endLine + 1)
                          , IntegerAtom (cast endCol)
                          ]
               ]
    Nothing => SExpList []

SExpable Highlight where
  toSExp (MkHighlight loc fname nam impl k dec doc t ns)
    = SExpList [ toSExp $ (fname, justFC loc)
               , SExpList [ SExpList [ SymbolAtom "name", StringAtom nam ]
                          , SExpList [ SymbolAtom "namespace", StringAtom ns ]
                          , toSExp dec
                          , SExpList [ SymbolAtom "implicit", toSExp impl ]
                          , SExpList [ SymbolAtom "key", StringAtom k ]
                          , SExpList [ SymbolAtom "doc-overview", StringAtom doc ]
                          , SExpList [ SymbolAtom "type", StringAtom t ]
                          ]
               ]

||| Output some data using current dialog index
export
printOutput : {auto c : Ref Ctxt Defs} ->
              {auto o : Ref ROpts REPLOpts} ->
              SExp -> Core ()
printOutput msg
  =  do opts <- get ROpts
        case idemode opts of
          REPL _ => pure ()
          IDEMode i _ f =>
            send f (SExpList [SymbolAtom "output",
                              msg, toSExp i])

outputHighlight : {auto c : Ref Ctxt Defs} ->
                  {auto opts : Ref ROpts REPLOpts} ->
                  Highlight -> Core ()
outputHighlight h =
  printOutput $ SExpList [ SymbolAtom "ok"
                         , SExpList [ SymbolAtom "highlight-source"
                                    , toSExp hlt
                                    ]
                         ]
  where
    hlt : List Highlight
    hlt = [h]

lwOutputHighlight :
  {auto c : Ref Ctxt Defs} ->
  {auto opts : Ref ROpts REPLOpts} ->
  (FileName, NonEmptyFC, Decoration) -> Core ()
lwOutputHighlight (fname, nfc, decor) =
  printOutput $ SExpList [ SymbolAtom "ok"
                         , SExpList [ SymbolAtom "highlight-source"
                                    , toSExp $ the (List _) [
                                    SExpList [ toSExp $ (fname, justFC nfc)
               , SExpList [ toSExp decor]
               ]]]]

outputNameSyntax : {auto c : Ref Ctxt Defs} ->
                   {auto s : Ref Syn SyntaxInfo} ->
                   {auto opts : Ref ROpts REPLOpts} ->
                   (FileName, NonEmptyFC, Decoration, Name) -> Core ()
outputNameSyntax (fname, nfc, decor, nm) = do
      defs <- get Ctxt
      log "ide-mode.highlight" 20 $ "highlighting at " ++ show nfc
                                 ++ ": " ++ show nm
                                 ++ "\nAs: " ++ show decor
      let fc = justFC nfc
      let (mns, name) = displayName nm
      outputHighlight $ MkHighlight
         { location = nfc
         , name
         , filename = fname
         , isImplicit = False
         , key = ""
         , decor
         , docOverview = "" --!(getDocsForName fc nm)
         , typ = "" -- TODO: extract type maybe "" show !(lookupTyExact nm (gamma defs))
         , ns = maybe "" show mns
         }

export
outputSyntaxHighlighting : {auto c : Ref Ctxt Defs} ->
                           {auto m : Ref MD Metadata} ->
                           {auto s : Ref Syn SyntaxInfo} ->
                           {auto opts : Ref ROpts REPLOpts} ->
                           String ->
                           REPLResult ->
                           Core REPLResult
outputSyntaxHighlighting fname loadResult = do
  opts <- get ROpts
  when (opts.synHighlightOn) $ do
    meta <- get MD
    modIdent <- ctxtPathToNS fname

    let allNames = filter ((PhysicalIdrSrc modIdent ==) . fst . fst)
                     $ toList meta.nameLocMap
    --decls <- filter (inFile fname) . tydecls <$> get MD
    --_ <- traverse outputNameSyntax allNames -- ++ decls)

    let semHigh = meta.semanticHighlighting
    log "ide-mode.highlight" 19 $
      "Semantic metadata is: " ++ show semHigh

    let aliases
          : List ASemanticDecoration
          = flip foldMap meta.semanticAliases $ \ (from, to) =>
              let decors = uncurry exactRange (snd to) semHigh in
              map (\ ((fnm, loc), rest) => ((fnm, snd from), rest)) decors
    log "ide-mode.highlight.alias" 19 $
      "Semantic metadata from aliases is: " ++ show aliases

    let defaults
         : List ASemanticDecoration
         = flip foldMap meta.semanticDefaults $ \ decor@((_, range), _) =>
             case uncurry exactRange range semHigh of
               [] => [decor]
               _ => []

    traverse_ {b = Unit}
         (\(nfc, decor, mn) =>
           case mn of
             Nothing => lwOutputHighlight (fname, nfc, decor)
             Just n  => outputNameSyntax  (fname, nfc, decor, n))
         (defaults ++ aliases ++ toList semHigh)

  pure loadResult

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
-- --------------------------------------------------------------- [ DVect.idr ]
-- Module    : DVect.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| A `list` construct to create lists of dependent types.
|||
||| One of the problems with using dependent types is that types
||| depend on values. This affects the ability to construct lists of
||| values that have a dependent type. The existing `List` type cannot
||| be used as it requires all elements to have the same type.
module Toolkit.Data.DVect

import Data.Nat
import Data.String

import public Data.Vect
import public Data.Vect.Elem

import public Toolkit.Decidable.Equality.Indexed

%default total

||| A list construct for dependent types.
|||
||| @aTy    The type of the value contained within the list element type.
||| @len    The length of the list.
||| @elemTy The type of the elements within the list
||| @as     The List used to contain the different values within the type.
public export
data DVect : (aTy : Type)
          -> (elemTy : aTy -> Type)
          -> (len : Nat)
          -> (as : Vect len aTy)
          -> Type where
  ||| Create an empty List
  Nil  : DVect aTy elemTy Z Nil
  ||| Cons
  |||
  ||| @ex The element to add
  ||| @rest The list for `elem` to be added to.
  (::) : {x : aTy}
      -> (ex : elemTy x)
      -> (rest : DVect aTy elemTy n xs)
      -> DVect aTy elemTy (S n) (x::xs)

public export
size : DVect a e l as -> Nat
size Nil = Z
size (x::xs) = 1 + size xs

public export
mapToVect : (forall x . e x -> b)
         -> DVect a e n xs
         -> Vect n b
mapToVect _ Nil = Nil
mapToVect f (x::xs) = f x :: mapToVect f xs

toList : Vect q a -> List a
toList Nil = Nil
toList (x::xs) = x :: DVect.toList xs

||| Function to show a `DList`.
|||
||| Due to limitations in idris wrt to class instances on dependent
||| types a generic show instance cannot be defined for
||| sigmalist. This will cause minor annoyances in its use.
|||
||| @showFunc A function to show the elements
||| @l       The list to be Shown.
public export
showDVect : (showFunc : forall a . elemTy a -> String)
         -> (l : DVect aTy elemTy n as)
         -> String
showDVect f xs = "[" ++ unwords asList ++ "]"
  where
    asList : List String
    asList = DVect.toList $ intersperse "," (mapToVect f xs)

namespace Alternative
  public export
  index : DVect aTy elemTy n as
       -> Elem a as
       -> elemTy a
  index (x::xs) Here = x
  index (x::xs) (There later) = index xs later

  public export
  update : (vs  : DVect iTy eTy l is)
        -> (idx : Elem i is)
        -> (new : eTy i)
        -> DVect iTy eTy l is
  update (ex :: rest) Here new = new :: rest
  update (ex :: rest) (There later) new = ex :: update rest later new

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

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Void

%default total

{-
  data Void : Type where

-}

twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible

valueNotSucc : (x : Nat) -> x = S x -> Void
valueNotSucc _ Refl impossible

{-
  data Dec : (prop : Type) -> Type where
    Yes : (prf : prop) -> Dec prop
    No : (contra : prop -> Void) -> Dec prop
-}

-- more precise implementation of checkEqNat

zeroNotSucc : Z = S k -> Void
zeroNotSucc Refl impossible

succNotZero : S k = Z -> Void
succNotZero Refl impossible

noRec : (k = j -> Void) -> S k = S j -> Void
noRec contra Refl = contra Refl

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Dec (num1 = num2)
checkEqNat Z Z = Yes Refl
checkEqNat Z (S k) = No zeroNotSucc
checkEqNat (S k) Z = No succNotZero
checkEqNat (S k) (S j) = case checkEqNat k j of
                              Yes prf => Yes (cong S prf)
                              No contra => No (noRec contra)

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
-- SPDX-FileCopyrightText: 2022 The toml-idr developers
--
-- SPDX-License-Identifier: MPL-2.0

module Language.TOML.Processing

import Data.List.Elem
import Decidable.Equality
import Language.TOML.Value

infixr 2 `And`

mutual
    public export
    data ValueTy
        = TString
        | TInteger
        | TFloat
        | TBoolean
        | TEnum (List String)
        | TArray ValueTy
        | TTable TableTy

    public export
    record FieldTy where
        constructor MkFieldTy
        name : String
        optional : Bool
        ty : ValueTy

    public export
    data TableTy : Type where
        Emp : TableTy
        Ext : (ft : FieldTy) -> (FieldOf ft -> TableTy) -> TableTy

    public export
    And : FieldTy -> TableTy -> TableTy
    And x y = Ext x (const y)

    public export
    ValueOf : ValueTy -> Type
    ValueOf TString    = String
    ValueOf TInteger   = Integer
    ValueOf TFloat     = Double
    ValueOf TBoolean   = Bool
    ValueOf (TEnum names) = (name ** Elem name names)
    ValueOf (TArray t) = List (ValueOf t)
    ValueOf (TTable x) = TableOf x

    public export
    FieldOf : FieldTy -> Type
    FieldOf x = (if x.optional then Maybe else id) (ValueOf x.ty)

    public export
    data TableOf : TableTy -> Type where
        Nil : TableOf Emp
        (::) : (x : FieldOf ft) -> TableOf (f x) -> TableOf (Ext ft f)

mutual
    public export
    data ValueError
        = ExpectedType ValueTy
        | InsideArray ValueError
        | InsideTable TableError
        | BadEnumVal String

    public export
    data TableError
        = FieldError String ValueError
        | ExpectedField String
        | UnexpectedFields (List String)

mutual
    public export
    processTable : (ty : TableTy) -> Table -> Either TableError (TableOf ty)
    processTable Emp x with (keys x)
      _ | [] = Right []
      _ | ks = Left $ UnexpectedFields ks
    processTable (Ext (MkFieldTy name optional ty) fields) x with (lookup name x)
      _ | Nothing = case optional of
                         True => Right $ Nothing :: !(processTable (fields Nothing) x)
                         False => Left $ ExpectedField name
      _ | Just val = do
              val' <- bimap (FieldError name) id $ processValue ty val
              let val'' = case optional of
                               True => Just val'
                               False => val'
              fields' <- processTable (fields val'') (delete name x)
              Right (val'' :: fields')

    public export
    processValue : (ty : ValueTy) -> Value -> Either ValueError (ValueOf ty)
    processValue (TEnum xs) (VString x) with (isElem x xs)
      _ | Yes el = Right (x ** el)
      _ | No nel = Left $ BadEnumVal x
    processValue TString    (VString x)  = Right x
    processValue TInteger   (VInteger x) = Right x
    processValue TFloat     (VFloat x)   = Right x
    processValue TBoolean   (VBoolean x) = Right x
    processValue (TArray t) (VArray xs)  = traverse (bimap InsideArray id . processValue t) xs
    processValue (TTable t) (VTable x)   = bimap InsideTable id $ processTable t x
    processValue t          v            = Left $ ExpectedType t

max_stars_repo_name: sepiina/toml-idr

max_issues_repo_name: sepiina/toml-idr

max_forks_repo_name: sepiina/toml-idr


text:
import Control.Monad.State

update : (stateType -> stateType) -> State stateType ()
update func =
  do
    currState <- get
    put (func currState)

increase : Nat -> State Nat ()
increase diff = update (+diff)

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
||| An approach to intrinsically-typed STLC with types as terms.
|||
||| We use this razor to demonstrate succintly how Type universes are
||| used to separate descriptions of how types are formed and their
||| use to type values.
|||
||| Standard constructions are used to represent the language as an
||| EDSL, together with proof of progress taken from PLFA Part 2.
|||
||| This module compliments Appendix 2 of the Functional Pearl.
|||
||| Although the code appears to be total, there is a known issues
||| with Idris2 totality checker that causes it to slow down when
||| dealing with mutually defined terms.
|||
module Razor.STLC

import Razor.Common

%default covering

namespace Types

  ||| Levels at which types and their types are defined in our type
  ||| universes.
  public export
  data Level = TYPE -- Build types here
             | VALUE -- Use types here.

  ||| Our types are meta types...
  public export
  data MTy : Level -> Type where

    BoolTyDesc : MTy TYPE
    BoolTy     : MTy VALUE

    FuncTy : MTy level -> MTy level -> MTy level

  ||| A predicate to type check types against type formers.
  public export
  data TyCheck : (type : MTy TYPE)
              -> (value : MTy VALUE)
              -> Type
    where
      ChkBool : TyCheck BoolTyDesc BoolTy

      ChkFunc : TyCheck paramTy  paramValue
             -> TyCheck returnTy returnValue
             -> TyCheck (FuncTy paramTy    returnTy)
                        (FuncTy paramValue returnValue)

  ||| A context is a list of types in different universes.
  public export
  Context : List Level -> Type
  Context = DList Level MTy

  public export
  Elem : Context lvls -> MTy level -> Type
  Elem g ty = Elem Level MTy ty g

namespace Terms

    public export
    data STLC : Context lvls -> MTy level -> Type where
      -- STLC

      Var : Elem Level MTy type ctxt -> STLC ctxt type

      Func : {paramTyType     : MTy TYPE}
          -> {paramTy, bodyTy : MTy VALUE}
          -> (type : STLC ctxt paramTyType)
          -> (term : STLC (ctxt +=         paramTy) bodyTy)
          -> (prf  : TyCheck paramTyType paramTy)
                  -> STLC  ctxt    (FuncTy paramTy  bodyTy)

      App : {paramTy, bodyTy : MTy VALUE}
         -> (func  : STLC ctxt (FuncTy paramTy bodyTy))
         -> (value : STLC ctxt         paramTy)
                  -> STLC ctxt                 bodyTy

      -- Type Constructors
      TyBool : STLC ctxt BoolTyDesc
      TyFunc : {paramMTy, returnMTy : MTy TYPE}
            -> (paramTy  : STLC ctxt paramMTy)
            -> (returnTy : STLC ctxt returnMTy)
                        -> STLC ctxt (FuncTy paramMTy returnMTy)

      -- Base Values
      True  : STLC ctxt BoolTy
      False : STLC ctxt BoolTy

namespace Renaming

  public export
  weaken : (func : Types.Elem old type
                -> Types.Elem new type)
        -> (Elem (old += type') type
         -> Types.Elem (new += type') type)

  weaken func Here = Here
  weaken func (There rest) = There (func rest)

  public export
  rename : (f : {level : Level}
             -> {type  : MTy level}
                      -> Types.Elem old type
                      -> Types.Elem new type)
        -> ({level : Level}
         -> {type : MTy level}
         -> STLC old type
         -> STLC new type)

  -- STLC
  rename f (Var idx) = Var (f idx)

  rename f (Func ty body prf)
    = Func (rename f ty) (rename (weaken f) body) prf

  rename f (App func param)
    = App (rename f func) (rename f param)

  -- Type Constructors
  rename f TyBool = TyBool
  rename f (TyFunc param body)
    = TyFunc (rename f param) (rename f body)

  -- Base Values
  rename f True  = True
  rename f False = False

namespace Substitution
  public export
  weakens : (f : {level : Level}
              -> {type  : MTy level}
                       -> Types.Elem old type
                       -> STLC new type)
         -> ({level : Level}
          -> {type  : MTy level}
                   -> Types.Elem (old += type') type
                   -> STLC (new += type') type)
  weakens f Here = Var Here
  weakens f (There rest) = rename There (f rest)

  -- general substitute
  namespace General
    public export
    subst : (f : {level : Level}
              -> {type  : MTy level}
                       -> Types.Elem old type
                       -> STLC new type)
         -> ({level : Level}
          -> {type  : MTy level}
                   -> STLC old type
                   -> STLC new type)

    -- STLC
    subst f (Var idx) = f idx

    subst f (Func type body prf)
      = Func (subst f type)
             (subst (weakens f) body)
             prf

    subst f (App func var)
      = App (subst f func) (subst f var)

    -- Types
    subst f TyBool = TyBool
    subst f (TyFunc param return)
      = TyFunc (subst f param) (subst f return)

    -- Base Values
    subst f True  = True
    subst f False = False

  namespace Single
    public export
    apply : {levelA : Level}
         -> {typeA  : MTy levelA}
         -> (this   : STLC ctxt typeB)
         -> (idx    : Elem (ctxt += typeB) typeA)
                   -> STLC ctxt typeA
    apply this Here = this
    apply this (There rest) = Var rest

    public export
    subst : {levelA,levelB : Level}
         -> {typeA         : MTy levelA}
         -> {typeB         : MTy levelB}
         -> (this          : STLC  ctxt           typeB)
         -> (inThis        : STLC (ctxt += typeB) typeA)
                          -> STLC  ctxt           typeA
    subst {ctxt} {typeA} {typeB} {levelA} {levelB} this inThis
      = General.subst (apply this) inThis

namespace Values

  public export
  data Value : STLC ctxt type -> Type where
    TrueV  : Value True
    FalseV : Value False
    FuncV : {body : STLC (ctxt += paramTy) bodyTy}
                 -> Value (Func type body prf)

    TyBoolV : Value TyBool
    TyFuncV : {param : STLC ctxt pty}
           -> {return : STLC ctxt rty}
           -> Value param
           -> Value return
           -> Value (TyFunc param return)

namespace Reduction

  public export
  data Redux : (this : STLC ctxt type)
            -> (that : STLC ctxt type)
            -> Type
    where
      -- Functions reduce
      SimplifyFuncAppFunc : (func : Redux this that)
                                 -> Redux (App this var)
                                          (App that var)

      SimplifyFuncAppVar : {this, that : STLC ctxt type}
                        -> {func       : STLC ctxt (FuncTy type return)}
                        -> (value      : Value func)
                        -> (var        : Redux this that)
                                      -> Redux (App func this)
                                               (App func that)

      ReduceFuncApp : (value : Value var)
                            -> Redux (App (Func type body prf) var)
                                     (subst var body)

      -- Simplify Function Types
      SimplifyTyFuncParam : (param : Redux this that)
                                  -> Redux (TyFunc this body)
                                           (TyFunc that body)

      SimplifyTyFuncBody : {this, that : STLC ctxt type}
                        -> {param      : STLC ctxt paramTy}
                        -> (value      : Value param)
                        -> (body       : Redux this that)
                                      -> Redux (TyFunc param this)
                                               (TyFunc param that)

namespace Progress
  public export
  data Progress : (term : STLC Nil type)
                       -> Type
    where
      Done : forall mty . {term : STLC Nil mty}
                        -> Value term
                        -> Progress term
      Step : {this, that : STLC Nil type}
          -> (prf        : Redux this that)
                        -> Progress this

  public export
  progress : (term : STLC Nil type)
          -> Progress term
  -- STLC
  progress {type} (Var _) impossible

  progress (Func type body prf) = Done FuncV

  progress (App func var) with (progress func)
    progress (App func var) | (Done prfF) with (progress var)
      progress (App (Func ty b prf) var) | (Done prfF) | (Done prfV)
        = Step (ReduceFuncApp prfV {body=b})
      progress (App func var) | (Done prfF) | (Step prfV)
        = Step (SimplifyFuncAppVar prfF prfV)
    progress (App func var) | (Step prfF)
      = Step (SimplifyFuncAppFunc prfF)

  -- Type Constructors
  progress TyBool = Done TyBoolV

  progress (TyFunc param return) with (progress param)
    progress (TyFunc param return) | (Done valueP) with (progress return)
      progress (TyFunc param return) | (Done valueP) | (Done valueR)
        = Done (TyFuncV valueP valueR)
      progress (TyFunc param return) | (Done valueP) | (Step prfR)
        = Step (SimplifyTyFuncBody valueP prfR)
    progress (TyFunc param return) | (Step prfP)
      = Step (SimplifyTyFuncParam prfP)

  -- Base Values
  progress True  = Done TrueV
  progress False = Done FalseV

namespace Evaluation

  public export
  data Reduces : (this : STLC ctxt type)
              -> (that : STLC ctxt type)
              -> Type
    where
      Refl  : {this : STLC ctxt type}
                   -> Reduces this this
      Trans : {this, that, end : STLC ctxt type}
           -> Redux this that
           -> Reduces that end
           -> Reduces this end

  public export
  data Finished : (term : STLC ctxt type)
                       -> Type
    where
      Normalised : {term : STLC ctxt type}
                        -> Value term
                        -> Finished term
      OOF : Finished term

  public export
  data Evaluate : (term : STLC Nil type) -> Type where
    RunEval : {this, that : STLC Nil type}
           -> (steps      : Inf (Reduces this that))
           -> (result     : Finished that)
                         -> Evaluate this

  public export
  data Fuel = Empty | More (Lazy Fuel)

  public export
  covering
  forever : Fuel
  forever = More forever

  public export
  compute : forall type
          . (fuel : Fuel)
         -> (term : STLC Nil type)
         -> Evaluate term
  compute Empty term = RunEval Refl OOF
  compute (More fuel) term with (progress term)
    compute (More fuel) term | (Done value) = RunEval Refl (Normalised value)
    compute (More fuel) term | (Step step {that}) with (compute fuel that)
      compute (More fuel) term | (Step step {that = that}) | (RunEval steps result)
        = RunEval (Trans step steps) result

public export
covering
run : forall type
    . (this : STLC Nil type)
           -> Maybe (Subset (STLC Nil type) (Reduces this))
run this with (compute forever this)
  run this | (RunEval steps (Normalised {term} x))
    = Just (Element term steps)
  run this | (RunEval steps OOF) = Nothing

namespace Example

  export
  example0 : STLC Nil BoolTy
  example0 = App (Func TyBool (Var Here) ChkBool) True

  export
  example1 : STLC Nil (FuncTy BoolTy BoolTy)
  example1 = (Func TyBool True ChkBool)

  export
  id : STLC Nil (FuncTy BoolTy BoolTy)
  id = (Func TyBool (Var Here) ChkBool)

  public export
  CBool : MTy VALUE
  CBool = FuncTy (FuncTy BoolTy BoolTy)
                 (FuncTy BoolTy BoolTy)

  public export
  TyCBool : STLC ctxt (FuncTy (FuncTy BoolTyDesc BoolTyDesc)
                              (FuncTy BoolTyDesc BoolTyDesc))
  TyCBool = TyFunc (TyFunc TyBool TyBool) (TyFunc TyBool TyBool)

  export
  zero : STLC ctxt CBool
  zero = Func (TyFunc TyBool TyBool)
              (Func TyBool
                    (Var Here)
                    ChkBool)
              (ChkFunc ChkBool ChkBool)

  export
  one : STLC ctxt CBool
  one = Func (TyFunc TyBool TyBool)
              (Func TyBool
                    (App (Var (There Here)) (Var Here))
                    ChkBool)
              (ChkFunc ChkBool ChkBool)

  export
  two : STLC ctxt CBool
  two = Func (TyFunc TyBool TyBool)
             (Func TyBool
                   (App (Var (There Here))
                        (App (Var (There Here)) (Var Here)))
                   ChkBool)
             (ChkFunc ChkBool ChkBool)

  export
  succ : STLC ctxt (FuncTy CBool CBool)
  succ = Func TyCBool
              (Func (TyFunc TyBool TyBool)
                    (Func TyBool
                          ((Var (There Here)) `App`
                               (((Var (There (There Here))) `App`
                                         (Var (There Here))) `App`
                                    (Var Here)))
                          ChkBool)
                    (ChkFunc ChkBool ChkBool))
              (ChkFunc (ChkFunc ChkBool ChkBool)
                       (ChkFunc ChkBool ChkBool))

  export
  plus : STLC Nil (CBool `FuncTy` (CBool `FuncTy` CBool))
  plus = Func TyCBool
              (Func TyCBool
                    (Func (TyFunc TyBool TyBool)
                          (Func TyBool
                                (App (App (Var (There (There (There Here))))
                                          (Var (There Here)))
                                     (App (App (Var (There (There Here))) (Var (There Here)))
                                          (Var Here)))
                                ChkBool
                          )
                          (ChkFunc ChkBool ChkBool)
                    )

                    (ChkFunc (ChkFunc ChkBool ChkBool)
                             (ChkFunc ChkBool ChkBool))
              )
              (ChkFunc (ChkFunc ChkBool ChkBool)
                       (ChkFunc ChkBool ChkBool))

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

max_stars_repo_name: border-patrol/pearly-razors

max_issues_repo_name: border-patrol/pearly-razors

max_forks_repo_name: border-patrol/pearly-razors


text:
module Main
import Data.Vect

myVectAdd : Num elem => Vect len elem -> Vect len elem -> Vect len elem
myVectAdd  [] [] = []
myVectAdd (x::xs) (y::ys) = (x+y) :: myVectAdd xs ys

v1 : Vect 3 Int
v1 = [1, 2, 3]

v2: Vect 3 Int
v2 = [4, 5, 6]

main : IO ()
main = printLn $ myVectAdd v1 v2


text:
module Main

import System.REPL

main : IO ()
main = repl "> " reverse


text:
module Common

%default total

BoolQ : Type
BoolQ = (A : Type) -> A -> A -> A

unBoolQ : {A : Type} -> A -> A -> BoolQ -> A
unBoolQ a a' q = q _ a a'

trueQ : BoolQ
trueQ = \_, a, a' => a

falseQ : BoolQ
falseQ = \_, a, a' => a'

fromBoolQ : BoolQ -> Bool
fromBoolQ q = unBoolQ True False q

toBoolQ : Bool -> BoolQ
toBoolQ True  = trueQ
toBoolQ False = falseQ

test_unBoolTrueQ : unBoolQ a a' trueQ = a
test_unBoolTrueQ = Refl

test_unBoolFalseQ : unBoolQ a a' falseQ = a'
test_unBoolFalseQ = Refl

test_fromTrueQ : fromBoolQ trueQ = True
test_fromTrueQ = Refl

test_fromFalseQ : fromBoolQ falseQ = False
test_fromFalseQ = Refl

test_toTrueQ : toBoolQ True = trueQ
test_toTrueQ = Refl

test_toFalseQ : toBoolQ False = falseQ
test_toFalseQ = Refl

MaybeQ : Type -> Type
MaybeQ A = (B : Type) -> (A -> B) -> B -> B

unMaybeQ : {A, B : Type} -> (A -> B) -> B -> MaybeQ A -> B
unMaybeQ f b q = q _ f b

justQ : {A : Type} -> A -> MaybeQ A
justQ a = \_, f, b => f a

nothingQ : {A : Type} -> MaybeQ A
nothingQ = \_, f, b => b

fromMaybeQ : {A : Type} -> MaybeQ A -> Maybe A
fromMaybeQ q = unMaybeQ Just Nothing q

toMaybeQ : {A : Type} -> Maybe A -> MaybeQ A
toMaybeQ (Just a) = justQ a
toMaybeQ Nothing  = nothingQ

test_unMaybeJustQ : unMaybeQ f b (justQ a) = f a
test_unMaybeJustQ = Refl

test_unMaybeNothingQ : unMaybeQ f b nothingQ = b
test_unMaybeNothingQ = Refl

test_fromJustQ : fromMaybeQ (justQ a) = Just a
test_fromJustQ = Refl

test_fromNothingQ : fromMaybeQ nothingQ = Nothing
test_fromNothingQ = Refl

test_toJustQ : toMaybeQ (Just a) = justQ a
test_toJustQ = Refl

test_toNothingQ : toMaybeQ Nothing = nothingQ
test_toNothingQ = Refl

EitherQ : Type -> Type -> Type
EitherQ A B = (C : Type) -> (A -> C) -> (B -> C) -> C

unEitherQ : {A, B, C : Type} -> (A -> C) -> (B -> C) -> EitherQ A B -> C
unEitherQ f g q = q _ f g

leftQ : {A, B : Type} -> A -> EitherQ A B
leftQ a = \_, f, g => f a

rightQ : {A, B : Type} -> B -> EitherQ A B
rightQ b = \_, f, g => g b

fromEitherQ : {A, B : Type} -> EitherQ A B -> Either A B
fromEitherQ q = unEitherQ Left Right q

toEitherQ : {A, B : Type} -> Either A B -> EitherQ A B
toEitherQ (Left a)  = leftQ a
toEitherQ (Right b) = rightQ b

test_unEitherLeftQ : unEitherQ f g (leftQ a) = f a
test_unEitherLeftQ = Refl

test_unEitherRightQ : unEitherQ f g (rightQ b) = g b
test_unEitherRightQ = Refl

test_fromLeftQ : fromEitherQ (leftQ a) = Left a
test_fromLeftQ = Refl

test_fromRightQ : fromEitherQ (rightQ b) = Right b
test_fromRightQ = Refl

test_toLeftQ : toEitherQ (Left a) = leftQ a
test_toLeftQ = Refl

test_toRightQ : toEitherQ (Right b) = rightQ b
test_toRightQ = Refl

PairQ : Type -> Type -> Type
PairQ A B = (C : Type) -> (A -> B -> C) -> C

unPairQ : {A, B, C : Type} -> (A -> B -> C) -> PairQ A B -> C
unPairQ f q = q _ f

pairQ : {A, B : Type} -> A -> B -> PairQ A B
pairQ a b = \_, f => f a b

fromPairQ : {A, B : Type} -> PairQ A B -> (A, B)
fromPairQ q = unPairQ (\a, b => (a, b)) q

toPairQ : {A, B : Type} -> (A, B) -> PairQ A B
toPairQ (a, b) = pairQ a b

fstQ : {A, B : Type} -> PairQ A B -> A
fstQ q = unPairQ (\a, b => a) q

sndQ : {A, B : Type} -> PairQ A B -> B
sndQ q = unPairQ (\a, b => b) q

test_unPairPairQ : unPairQ (\a, b => (a, b)) (pairQ a b) = (a, b)
test_unPairPairQ = Refl

test_fromPairQ : fromPairQ (pairQ a b) = (a, b)
test_fromPairQ = Refl

test_toPairQ : toPairQ (a, b) = pairQ a b
test_toPairQ = Refl

test_fstPairQ : fstQ (pairQ a b) = a
test_fstPairQ = Refl

test_sndPairQ : sndQ (pairQ a b) = b
test_sndPairQ = Refl

max_stars_repo_name: mietek/scott-encoding

max_issues_repo_name: mietek/scott-encoding

max_forks_repo_name: mietek/scott-encoding


text:
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 : Nat -> Bool
    odd Z     = False
    odd (S k) = even k

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


text:
module Language.JSON.Tokens

import Language.JSON.String
import Text.Token
import Text.Bounded

%default total

public export
strTrue : String
strTrue = "true"

public export
strFalse : String
strFalse = "false"

public export
data Bracket = Open | Close

public export
Eq Bracket where
  (==) Open Open = True
  (==) Close Close = True
  (==) _ _ = False

public export
data Punctuation
  = Comma
  | Colon
  | Square Bracket
  | Curly Bracket

public export
Eq Punctuation where
  (==) Comma Comma = True
  (==) Colon Colon = True
  (==) (Square b1) (Square b2) = b1 == b2
  (==) (Curly b1) (Curly b2) = b1 == b2
  (==) _ _ = False

public export
data JSONTokenKind
  = JTBoolean
  | JTNumber
  | JTString
  | JTNull
  | JTPunct Punctuation
  | JTIgnore

public export
JSONToken : Type
JSONToken = Token JSONTokenKind

public export
Eq JSONTokenKind where
  (==) JTBoolean JTBoolean = True
  (==) JTNumber JTNumber = True
  (==) JTString JTString = True
  (==) JTNull JTNull = True
  (==) (JTPunct p1) (JTPunct p2) = p1 == p2
  (==) _ _ = False

public export
TokenKind JSONTokenKind where
  TokType JTBoolean = Bool
  TokType JTNumber = Double
  TokType JTString = Maybe String
  TokType JTNull = ()
  TokType (JTPunct _) = ()
  TokType JTIgnore = ()

  tokValue JTBoolean x = x == strTrue
  tokValue JTNumber x = cast x
  tokValue JTString x = stringValue x
  tokValue JTNull _ = ()
  tokValue (JTPunct _) _ = ()
  tokValue JTIgnore _ = ()

export
ignored : WithBounds JSONToken -> Bool
ignored (MkBounded (Tok JTIgnore _) _ _) = True
ignored _ = False


text:
module Data.String.Extras

import Data.Vect

%default total
%access export

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

max_stars_repo_name: jheiling/idris-extras

max_issues_repo_name: jheiling/idris-extras

max_forks_repo_name: jheiling/idris-extras


text:
|||
module Toolkit.Data.Graph.EdgeBounded.HasMinDegree

import Decidable.Equality

import Data.String
import Data.List.Elem
import Data.List.Quantifiers

import Toolkit.Decidable.Do
import Toolkit.Decidable.Informative

import Toolkit.Data.Nat
import Toolkit.Data.Pair
import Toolkit.Data.List.Size
import Toolkit.Data.List.Occurs.Does

import Toolkit.Data.Graph.EdgeBounded

import public Toolkit.Data.Graph.EdgeBounded.DegreeCommon

%default total

namespace Out

  public export
  HasMinDegreeOut : (v  : Nat)
                 -> (es : Edges)
                 -> (d  : Nat)
                       -> Type
  HasMinDegreeOut v
    = AtLeast.Occurs (Pair Nat Nat) (IsFirst v)

  export
  hasMinDegreeOut : (v  : Nat)
                 -> (es : Edges)
                 -> (d  : Nat)
                       -> DecInfo (Maybe HasDegree.Error)
                                  (HasMinDegreeOut v es d)

  hasMinDegreeOut v es d
    = embed (maybe Nothing (\x => Just $ MkError v O x))
            (AtLeast.occurs (isFirst v) es d)

namespace In

  public export
  HasMinDegreeIn : (v  : Nat)
                -> (es : Edges)
                -> (d  : Nat)
                      -> Type
  HasMinDegreeIn v
    = AtLeast.Occurs (Pair Nat Nat) (IsSecond v)

  export
  hasMinDegreeIn : (v  : Nat)
                -> (es : Edges)
                -> (d  : Nat)
                      -> DecInfo (Maybe HasDegree.Error)
                                 (HasMinDegreeIn v es d)
  hasMinDegreeIn v es d
    = embed (maybe Nothing (\x => Just $ MkError v I x))
            (AtLeast.occurs (isSecond v) es d)

namespace Error
  public export
  data Kind = WrongIN
            | WrongOUT
            | WrongLeafSrcIN
            | WrongLeafSrcOUT
            | WrongLeafSnkIN
            | WrongLeafSnkOUT

public export
record Error type where
  constructor MkError
  vertex : Vertex type
  kind   : Error.Kind
  error  : Maybe HasDegree.Error

namespace Raw

  public export
  data ExpDegrees : (v : Vertex type) -> (i,o : Nat) -> Type where
    Node : ExpDegrees (Node d     k j i) j i
    Src  : ExpDegrees (Leaf d SRC k j)   0 j
    Bsrc : ExpDegrees (Leaf d BI  k j)   0 j
    Snk  : ExpDegrees (Leaf d SNK k j)   j 0
    Bsnk : ExpDegrees (Leaf d BI  k j)   j 0

  public export
  data HasExactDegree : (v   : Vertex type)
                     -> (es  : Edges)
                     -> (i,o : Nat)
                     -> (exp : ExpDegrees v i o)
                            -> Type
    where
      HDN : (din  : HasExactDegreeIn  v es i)
         -> (dout : HasExactDegreeOut v es o)
                 -> HasExactDegree (Node d v i o) es i o Node

      HDLS : (din  : HasExactDegreeIn  v es 0)
          -> (dout : HasExactDegreeOut v es o)
                  -> HasExactDegree (Leaf d SRC v o) es 0 o Src

      HDLT : (din  : HasExactDegreeIn  v es i)
          -> (dout : HasExactDegreeOut v es 0)
                  -> HasExactDegree (Leaf d SNK v i) es i 0 Snk

      HDLBS : (din  : HasExactDegreeIn  v es 0)
           -> (dout : HasExactDegreeOut v es k)
                   -> HasExactDegree (Leaf d BI v k) es 0 k Bsrc

      HDLBT : (din  : HasExactDegreeIn  v es k)
           -> (dout : HasExactDegreeOut v es 0)
                   -> HasExactDegree (Leaf d BI v k) es k 0 Bsnk

{-

  leafBiAsSrcOutWrong : (HasExactDegreeOut       k    es   o      -> Void)
                      -> HasExactDegree (Leaf d BI k o) es 0 o Bsrc -> Void
  leafBiAsSrcOutWrong f (HDLBS din dout) = f dout

  leafBiAsSrcInWrong : (HasExactDegreeIn        k    es 0        -> Void)
                    ->  HasExactDegree (Leaf d BI k o) es 0 o Bsrc -> Void
  leafBiAsSrcInWrong f (HDLBS din dout) = f din

  leafBiAsSnkOutWrong : (HasExactDegreeOut       k    es   0      -> Void)
                     ->  HasExactDegree (Leaf d BI k o) es o 0 Bsnk -> Void
  leafBiAsSnkOutWrong f (HDLBT din dout) = f dout

  leafBiAsSnkInWrong : (HasExactDegreeIn        k    es o        -> Void)
                    ->  HasExactDegree (Leaf d BI k o) es o 0 Bsnk -> Void
  leafBiAsSnkInWrong f (HDLBT din dout) = f din
-}
  export
  hasExactDegree : (v   : Vertex type)
           -> (exp : ExpDegrees v i o)
           -> (es  : Edges)
                  -> DecInfo (HasExactDegree.Error type)
                             (HasExactDegree v es i o exp)
{-
  hasExactDegree (Node d k i o) Node es with (hasExactDegreeIn k es i)
    hasExactDegree (Node d k i o) Node es | (Yes pI) with (hasExactDegreeOut k es o)
      hasExactDegree (Node d k i o) Node es | (Yes pI) | (Yes pO)
        = Yes (HDN pI pO)
      hasExactDegree (Node d k i o) Node es | (Yes pI) | (No msg contra)
        = No (MkError (Node d k i o) WrongOUT msg)
             (\(HDN pI pO) => contra pO)

    hasExactDegree (Node d k i o) Node es | (No msg contra)
      = No (MkError (Node d k i o) WrongIN msg)
           (\(HDN pI pO) => contra pI)

  hasExactDegree (Leaf d SRC k o) Src es with (hasExactDegreeIn k es 0)
    hasExactDegree (Leaf d SRC k o) Src es | (Yes pI) with (hasExactDegreeOut k es o)
      hasExactDegree (Leaf d SRC k o) Src es | (Yes pI) | (Yes pO)
        = Yes (HDLS pI pO)
      hasExactDegree (Leaf d SRC k o) Src es | (Yes pI) | (No msg contra)
        = No (MkError (Leaf d SRC k o) WrongOUT msg)
             (\(HDLS pI pO) => contra pO)

    hasExactDegree (Leaf d SRC k o) Src es | (No msg contra)
      = No (MkError (Leaf d SRC k o) WrongIN msg)
           (\(HDLS pI pO) => contra pI)

  hasExactDegree (Leaf d BI k o) Bsrc es with (hasExactDegreeIn k es 0)
    hasExactDegree (Leaf d BI k o) Bsrc es | (Yes pI) with (hasExactDegreeOut k es o)
      hasExactDegree (Leaf d BI k o) Bsrc es | (Yes pI) | (Yes pO)
        = Yes (HDLBS pI pO)
      hasExactDegree (Leaf d BI k o) Bsrc es | (Yes pI) | (No msg contra)
        = No (MkError (Leaf d BI k o) WrongLeafSrcOUT msg)
             (leafBiAsSrcOutWrong contra)

    hasExactDegree (Leaf d BI k o) Bsrc es | (No msg contra)
      = No (MkError (Leaf d BI k o) WrongLeafSrcIN msg)
           (leafBiAsSrcInWrong contra)

  hasExactDegree (Leaf d SNK k i) Snk es with (hasExactDegreeIn k es i)
    hasExactDegree (Leaf d SNK k i) Snk es | (Yes pI) with (hasExactDegreeOut k es 0)
      hasExactDegree (Leaf d SNK k i) Snk es | (Yes pI) | (Yes pO)
        = Yes (HDLT pI pO)
      hasExactDegree (Leaf d SNK k i) Snk es | (Yes pI) | (No msg contra)
        = No (MkError (Leaf d SNK k i) WrongLeafSnkOUT msg)
             (\(HDLT pI pO) => contra pO)

    hasExactDegree (Leaf d SNK k i) Snk es | (No msg contra)
      = No (MkError (Leaf d SNK k i) WrongLeafSnkIN msg)
           (\(HDLT pI pO) => contra pI)

  hasExactDegree (Leaf d BI k i) Bsnk es with (hasExactDegreeIn k es i)
    hasExactDegree (Leaf d BI k i) Bsnk es | (Yes pO) with (hasExactDegreeOut k es 0)
      hasExactDegree (Leaf d BI k i) Bsnk es | (Yes pO) | (Yes pI)
        = Yes (HDLBT pO pI)
      hasExactDegree (Leaf d BI k i) Bsnk es | (Yes pO) | (No msg contra)
        = No (MkError (Leaf d SNK k i) WrongLeafSnkOUT msg)
             (leafBiAsSnkOutWrong contra)

    hasExactDegree (Leaf d BI k i) Bsnk es | (No msg contra)
      = No (MkError (Leaf d SNK k i) WrongLeafSnkIN msg)
           (leafBiAsSnkInWrong contra)
-}
{-
public export
data HasExactDegree : (v : Vertex type) -> (es : Edges) -> Type where
  R : (exp : ExpDegrees v i o)
   -> (prf : HasExactDegree v es i o exp)
          -> HasExactDegree v es

biLeafWrong : (HasExactDegree (Leaf d BI k j) es j 0 Bsnk -> Void)
           -> (HasExactDegree (Leaf d BI k j) es 0 j Bsrc -> Void)
           ->  HasExactDegree (Leaf d BI k j) es          -> Void
biLeafWrong f g (R Bsrc prf) = g prf
biLeafWrong f g (R Bsnk prf) = f prf

export
hasExactDegree : (v  : Vertex type)
              -> (es : Edges)
                    -> DecInfo (HasExactDegree.Error type)
                               (HasExactDegree v es)

hasExactDegree (Node d k j i) es with (hasExactDegree (Node d k j i) Node es)
  hasExactDegree (Node d k j i) es | (Yes prf)
    = Yes (R Node prf)
  hasExactDegree (Node d k j i) es | (No msg contra)
    = No msg
         (\(R Node prf) => contra prf)

hasExactDegree (Leaf d SRC k j) es with (hasExactDegree (Leaf d SRC k j) Src es)
  hasExactDegree (Leaf d SRC k j) es | (Yes prf)
    = Yes (R Src prf)
  hasExactDegree (Leaf d SRC k j) es | (No msg contra)
    = No msg
         (\(R Src prf) => contra prf)

hasExactDegree (Leaf d SNK k j) es with (hasExactDegree (Leaf d SNK k j) Snk es)
  hasExactDegree (Leaf d SNK k j) es | (Yes prf)
    = Yes (R Snk prf)
  hasExactDegree (Leaf d SNK k j) es | (No msg contra)
    = No msg (\(R Snk prf) => contra prf)

hasExactDegree (Leaf d BI k j) es with (hasExactDegree (Leaf d BI k j) Bsrc es)
  hasExactDegree (Leaf d BI k j) es | (Yes prf)
    = Yes (R Bsrc prf)

  hasExactDegree (Leaf d BI k j) es | (No msgi contra) with (hasExactDegree (Leaf d BI k j) Bsnk es)
    hasExactDegree (Leaf d BI k j) es | (No msgi contra) | (Yes prf)
      = Yes (R Bsnk prf)

    hasExactDegree (Leaf d BI k j) es | (No msgi contra) | (No msg f)
      = No msg (biLeafWrong f contra)
-}
-- [ EOF ]


text:
module Language.LSP.Message.TextDocument

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.URI
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentIdentifier
public export
record TextDocumentIdentifier where
  constructor MkTextDocumentIdentifier
  uri : DocumentURI
%runElab deriveJSON defaultOpts `{{TextDocumentIdentifier}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#versionedTextDocumentIdentifier
public export
record VersionedTextDocumentIdentifier where
  constructor MkVersionedTextDocumentIdentifier
  uri     : DocumentURI
  version : Int
%runElab deriveJSON defaultOpts `{{VersionedTextDocumentIdentifier}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#versionedTextDocumentIdentifier
public export
record OptionalVersionedTextDocumentIdentifier where
  constructor MkOptionalVersionedTextDocumentIdentifier
  uri     : DocumentURI
  version : Maybe Int
%runElab deriveJSON defaultOpts `{{OptionalVersionedTextDocumentIdentifier}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentItem
public export
record TextDocumentItem where
  constructor MkTextDocumentItem
  uri        : DocumentURI
  languageId : String
  version    : Int
  text       : String
%runElab deriveJSON defaultOpts `{{TextDocumentItem}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentPositionParams
public export
record TextDocumentPositionParams where
  constructor MkTextDocumentPositionParams
  textDocument : TextDocumentIdentifier
  position     : Position
%runElab deriveJSON defaultOpts `{{TextDocumentPositionParams}}

namespace TextDocumentSyncKind
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_synchronization
  public export
  data TextDocumentSyncKind = None | Full | Incremental

export
ToJSON TextDocumentSyncKind where
  toJSON None        = JNumber 0
  toJSON Full        = JNumber 1
  toJSON Incremental = JNumber 2

export
FromJSON TextDocumentSyncKind where
  fromJSON (JNumber 0) = pure None
  fromJSON (JNumber 1) = pure Full
  fromJSON (JNumber 2) = pure Incremental
  fromJSON _ = Nothing

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didOpen
public export
record DidOpenTextDocumentParams where
  constructor MkDidOpenTextDocumentParams
  textDocument : TextDocumentItem
%runElab deriveJSON defaultOpts `{{DidOpenTextDocumentParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#documentFilter
public export
record DocumentFilter where
  constructor MkDocumentFilter
  language : Maybe String
  scheme   : Maybe String
  pattern  : Maybe String
%runElab deriveJSON defaultOpts `{{DocumentFilter}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#documentFilter
public export
DocumentSelector : Type
DocumentSelector = List DocumentFilter

public export
record TextDocumentRegistrationOptions where
  constructor MkTextDocumentRegistrationOptions
  documentSelector : OneOf [DocumentSelector, Null]
%runElab deriveJSON defaultOpts `{{TextDocumentRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocumentRegistrationOptions
public export
record TextDocumentChangeRegistrationOptions where
  constructor MkTextDocumentChangeRegistrationOptions
  syncKind : TextDocumentSyncKind
%runElab deriveJSON defaultOpts `{{TextDocumentChangeRegistrationOptions}}

namespace DidChangeTextDocumentParams
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange
  public export
  record TextDocumentContentChangeEvent where
    constructor MkTextDocumentContentChangeEvent
    text : String
  %runElab deriveJSON defaultOpts `{{TextDocumentContentChangeEvent}}

  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange
  public export
  record TextDocumentContentChangeEventWithRange where
    constructor MkTextDocumentContentChangeEventWithRange
    range       : Range
    rangeLength : Maybe Int
    text        : String
  %runElab deriveJSON defaultOpts `{{TextDocumentContentChangeEventWithRange}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didChange
public export
record DidChangeTextDocumentParams where
  constructor MkDidChangeTextDocumentParams
  textDocument   : VersionedTextDocumentIdentifier
  contentChanges : List (OneOf [TextDocumentContentChangeEvent, TextDocumentContentChangeEventWithRange])
%runElab deriveJSON defaultOpts `{{DidChangeTextDocumentParams}}

namespace TextDocumentSaveReason
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_willSave
  public export
  data TextDocumentSaveReason = Manual | AfterDelay | FocusOut

export
ToJSON TextDocumentSaveReason where
  toJSON Manual     = JNumber 1
  toJSON AfterDelay = JNumber 2
  toJSON FocusOut   = JNumber 3

export
FromJSON TextDocumentSaveReason where
  fromJSON (JNumber 1) = pure Manual
  fromJSON (JNumber 2) = pure AfterDelay
  fromJSON (JNumber 3) = pure FocusOut
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_willSave
public export
record WillSaveTextDocumentParams where
  constructor MkWillSaveTextDocumentParams
  textDocument : TextDocumentIdentifier
  reason       : TextDocumentSaveReason
%runElab deriveJSON defaultOpts `{{WillSaveTextDocumentParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave
public export
record SaveOptions where
  constructor MkSaveOptions
  includeText : Maybe Bool
%runElab deriveJSON defaultOpts `{{SaveOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave
public export
record TextDocumentSaveRegistrationOptions where
  constructor MkTextDocumentSaveRegistrationOptions
  documentSelector : OneOf [DocumentSelector, Null]
  includeText      : Maybe Bool
%runElab deriveJSON defaultOpts `{{TextDocumentSaveRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didSave
public export
record DidSaveTextDocumentParams where
  constructor MkDidSaveTextDocumentParams
  textDocument : TextDocumentIdentifier
  text         : Maybe String
%runElab deriveJSON defaultOpts `{{DidSaveTextDocumentParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose
public export
record DidCloseTextDocumentParams where
  constructor MkDidCloseTextDocumentParams
  textDocument : TextDocumentIdentifier
%runElab deriveJSON defaultOpts `{{DidCloseTextDocumentParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose
public export
record TextDocumentSyncClientCapabilities where
  constructor MkTextDocumentSyncClientCapabilities
  dynamicRegistration : Maybe Bool
  willSave            : Maybe Bool
  willSaveWaitUntil   : Maybe Bool
  didSave             : Maybe Bool
%runElab deriveJSON defaultOpts `{{TextDocumentSyncClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_didClose
public export
record TextDocumentSyncOptions where
  constructor MkTextDocumentSyncOptions
  openClose         : Maybe Bool
  change            : Maybe TextDocumentSyncKind
  willSave          : Maybe Bool
  willSaveWaitUntil : Maybe Bool
  save              : Maybe (OneOf [Bool, SaveOptions])
%runElab deriveJSON defaultOpts `{{TextDocumentSyncOptions}}


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

import Data.AVL.Dict

import Readability
import Readability.Process.XML

import Config.INI

import XML.DOM
import XML.XPath
import XML.XPath.Query

import Freyja.Utils

import Frigg.Options
import Frigg.Error
import Frigg.Effs
import Frigg.Config

-- -------------------------------------------------------------- [ Directives ]

%access private

-- ------------------------------------------------------------------- [ Begin ]

-- @TODO Make nicers
getScore : (heading  : String)
        -> (gradings : Dict String Double)
        -> (doc      : XMLDoc)
        -> Either FriggError Double
getScore t gsc doc = do
    case query (concat ["//", toLower t, "/@score"]) doc of
      Left err => Left $ ExtractionError err
      Right xs => case getText xs of
        Nil     => Left $ EvalError $ unwords ["Node Not Found for:", show t]
        (x::xs) => case getNodeValue x of
          Nothing => Left $ EvalError $ unwords ["Score Not Given for:", show t]
          Just v => case Dict.lookup (toLower v) gsc of
            Nothing => Left $ EvalError $ unwords ["Weighting not found for:", show v]
            Just s  => Right s

calcTemplateAdherence : Dict String Double
                     -> Dict String Double
                     -> Document DOCUMENT
                     -> Either FriggError Double
calcTemplateAdherence ws gsc doc = do
    ss <- mapEither (\(k,v) => doCalc k v) $ Dict.toList ws
    pure $ foldl (+) 0.0 ss
  where
    doCalc : String -> Double -> Either FriggError Double
    doCalc t weight = do
        res <- getScore t gsc doc
        pure (weight * res)

export
evalTemplate : Frigg (Either FriggError Double)
evalTemplate = do
    doc <- getXMLDoc
    scale <- getGradingScale
    weight <- getTemplateWeightings
    case (isEmpty scale, isEmpty weight) of
        (False, False) => pure $ calcTemplateAdherence weight scale doc
        otherwise      => pure $ Left InvalidMapping

export
evalTemplateAndReport : Frigg ()
evalTemplateAndReport = do
  (Right res) <- evalTemplate | Left err => printLn err
  printLn res

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

max_stars_repo_name: jfdm/frigg-tool

max_issues_repo_name: jfdm/frigg-tool

max_forks_repo_name: jfdm/frigg-tool


text:
||| ===========================================================================
||| Universal algebra
||| ===========================================================================

||| A general n-ary operation on terms of a common type.
data Op n a = List a n -> Maybe a
||| A general algebraic structure on terms of type a.
data Algebraic a = List Op n a

data Formula a Algebraic a = {x:a} |

data SLP a {gens:List a} = gens

== : {x:type} -> {y:type} -> type where
    Same x = Refl

record Group a {gens:List a} {==:a->a->type} where
    constructor MkGroup
    * : Op 2 a
    - : Op 1 a
    id : Op 0 a
    gens : List a
    == : {x:type} -> {y:type} -> type where
        Same x = Refl
    ascLaw : (x:SLP gens) -> (y:SLP gens) -> (z:SLP gens) -> x*(y*z) == (x*y)*z
    invLaw : (x:SLP a) -> (x*(-x)) == id
    idLaw : (x:SLP a) -> x*id == x

max_stars_repo_name: algeboy/BlackBoxType

max_issues_repo_name: algeboy/BlackBoxType

max_forks_repo_name: algeboy/BlackBoxType