text:
module Compiler.Scheme.Gambit

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Generated
import Compiler.Inline
import Compiler.Scheme.Common

import Core.Context
import Core.Directory
import Core.Name
import Core.Options
import Core.TT
import Libraries.Utils.Hex
import Libraries.Utils.Path

import Data.List
import Data.Maybe
import Libraries.Data.NameMap
import Data.String
import Data.Vect

import Idris.Env

import System
import System.Directory
import System.File
import System.Info

%default covering

-- TODO Look for gsi-script, then gsi
findGSI : IO String
findGSI =
  do env <- idrisGetEnv "GAMBIT_GSI"
     pure $ fromMaybe "/usr/bin/env gsi" env

-- TODO Look for gsc-script, then gsc
findGSC : IO String
findGSC =
  do env <- idrisGetEnv "GAMBIT_GSC"
     pure $ fromMaybe "/usr/bin/env gsc" env

findGSCBackend : IO String
findGSCBackend =
  do env <- idrisGetEnv "GAMBIT_GSC_BACKEND"
     pure $ case env of
              Nothing => ""
              Just e => " -cc " ++ e

schHeader : String
schHeader =
    "; " ++ (generatedString "Gambit") ++ "\n" ++
    "(declare (block)\n" ++
    "(inlining-limit 450)\n" ++
    "(standard-bindings)\n" ++
    "(extended-bindings)\n" ++
    "(not safe)\n" ++
    "(optimize-dead-definitions))\n"

showGambitChar : Char -> String -> String
showGambitChar '\\' = ("\\\\" ++)
showGambitChar c
   = if c < chr 32 -- XXX
        then (("\\x" ++ asHex (cast c) ++ ";") ++)
        else strCons c

showGambitString : List Char -> String -> String
showGambitString [] = id
showGambitString ('"'::cs) = ("\\\"" ++) . showGambitString cs
showGambitString (c::cs) = (showGambitChar c) . showGambitString cs

gambitString : String -> String
gambitString cs = strCons '"' (showGambitString (unpack cs) "\"")

mutual
  handleRet : String -> String -> String
  handleRet "void" op = op ++ " " ++ mkWorld (schConstructor gambitString (UN $ Basic "") (Just 0) [])
  handleRet _ op = mkWorld op

  getFArgs : NamedCExp -> Core (List (NamedCExp, NamedCExp))
  getFArgs (NmCon fc _ _ (Just 0) _) = pure []
  getFArgs (NmCon fc _ _ (Just 1) [ty, val, rest]) = pure $ (ty, val) :: !(getFArgs rest)
  getFArgs arg = throw (GenericMsg (getFC arg) ("Badly formed c call argument list " ++ show arg))

  gambitPrim : Int -> ExtPrim -> List NamedCExp -> Core String
  gambitPrim i GetField [NmPrimVal _ (Str s), _, _, struct,
                         NmPrimVal _ (Str fld), _]
      = do structsc <- schExp gambitPrim gambitString 0 struct
           pure $ "(" ++ s ++ "-" ++ fld ++ " " ++ structsc ++ ")"
  gambitPrim i GetField [_,_,_,_,_,_]
      = pure "(error \"bad getField\")"
  gambitPrim i SetField [NmPrimVal _ (Str s), _, _, struct,
                         NmPrimVal _ (Str fld), _, val, world]
      = do structsc <- schExp gambitPrim gambitString 0 struct
           valsc <- schExp gambitPrim gambitString 0 val
           pure $ mkWorld $
                "(" ++ s ++ "-" ++ fld ++ "-set! " ++ structsc ++ " " ++ valsc ++ ")"
  gambitPrim i SetField [_,_,_,_,_,_,_,_]
      = pure "(error \"bad setField\")"
  gambitPrim i SysCodegen []
      = pure $ "\"gambit\""
  gambitPrim i prim args
      = schExtCommon gambitPrim gambitString i prim args

-- Reference label for keeping track of loaded external libraries
data Loaded : Type where

-- Label for noting which struct types are declared
data Structs : Type where

notWorld : CFType -> Bool
notWorld CFWorld = False
notWorld _ = True

cType : FC -> CFType -> Core String
cType fc CFUnit = pure "void"
cType fc CFInt = pure "int"
cType fc CFString = pure "char *"
cType fc CFDouble = pure "double"
cType fc CFChar = pure "char"
cType fc CFPtr = pure "void *"
cType fc (CFIORes t) = cType fc t
cType fc (CFStruct n t) = pure $ "struct " ++ n
cType fc (CFFun s t) = funTySpec [s] t
  where
    funTySpec : List CFType -> CFType -> Core String
    funTySpec args (CFFun CFWorld t) = funTySpec args t
    funTySpec args (CFFun s t) = funTySpec (s :: args) t
    funTySpec args retty
        = do rtyspec <- cType fc retty
             argspecs <- traverse (cType fc) (reverse . filter notWorld $ args)
             pure $ rtyspec ++ " (*)(" ++ showSep ", " argspecs ++ ")"
cType fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
                       " to foreign function"))

cftySpec : FC -> CFType -> Core String
cftySpec fc CFUnit = pure "void"
cftySpec fc CFInt = pure "int"
cftySpec fc CFInt8 = pure "char"
cftySpec fc CFInt16 = pure "short"
cftySpec fc CFInt32 = pure "int"
cftySpec fc CFInt64 = pure "long"
cftySpec fc CFUnsigned8 = pure "unsigned-char"
cftySpec fc CFUnsigned16 = pure "unsigned-short"
cftySpec fc CFUnsigned32 = pure "unsigned-int"
cftySpec fc CFUnsigned64 = pure "unsigned-long"
cftySpec fc CFString = pure "UTF-8-string"
cftySpec fc CFDouble = pure "double"
cftySpec fc CFChar = pure "char"
cftySpec fc CFPtr = pure "(pointer void)"
cftySpec fc (CFIORes t) = cftySpec fc t
cftySpec fc (CFStruct n t) = pure $ n ++ "*/nonnull"
cftySpec fc (CFFun s t) = funTySpec [s] t
  where
    funTySpec : List CFType -> CFType -> Core String
    funTySpec args (CFFun CFWorld t) = funTySpec args t
    funTySpec args (CFFun s t) = funTySpec (s :: args) t
    funTySpec args retty
        = do rtyspec <- cftySpec fc retty
             argspecs <- traverse (cftySpec fc) (reverse . filter notWorld $ args)
             pure $ "(function (" ++ showSep " " argspecs ++ ") " ++ rtyspec ++ ")"
cftySpec fc t = throw (GenericMsg fc ("Can't pass argument of type " ++ show t ++
                         " to foreign function"))

record CCallbackInfo where
  constructor MkCCallbackInfo
  schemeArgName : String
  schemeWrapName : String
  callbackBody : String
  argTypes : List String
  retType : String

record CWrapperDefs where
  constructor MkCWrapperDefs
  setBox : String
  boxDef : String
  cWrapDef : String

cCall : {auto c : Ref Ctxt Defs} ->
        {auto l : Ref Loaded (List String)} ->
        FC -> (cfn : String) -> (fnWrapName : String -> String) -> (clib : String) ->
        List (Name, CFType) -> CFType -> Core (String, String)
cCall fc cfn fnWrapName clib args ret
    = do -- loaded <- get Loaded
         -- lib <- if clib `elem` loaded
         --           then pure ""
         --           else do (fname, fullname) <- locate clib
         --                   copyLib (fname, fullname)
         --                   put Loaded (clib :: loaded)
         --                   pure ""
         argTypes <- traverse (cftySpec fc . snd) args
         retType <- cftySpec fc ret

         argsInfo <- traverse buildArg args
         argCTypes <- traverse (cType fc . snd) args
         retCType <- cType fc ret

         let cWrapperDefs = map buildCWrapperDefs $ mapMaybe snd argsInfo
         let cFunWrapDeclaration = buildCFunWrapDeclaration cfn retCType argCTypes
         let wrapDeclarations = cFunWrapDeclaration
                                ++ concatMap (.boxDef) cWrapperDefs
                                ++ concatMap (.cWrapDef) cWrapperDefs

         let setBoxes = concatMap (.setBox) cWrapperDefs
         let call = " ((c-lambda (" ++ showSep " " argTypes ++ ") "
                      ++ retType ++ " " ++ show cfn ++ ") "
                      ++ showSep " " (map fst argsInfo) ++ ")"
         let body = setBoxes ++ "\n" ++ call

         pure $ case ret of -- XXX
                     CFIORes _ => (handleRet retType body, wrapDeclarations)
                     _ => (body, wrapDeclarations)
  where
    mkNs : Int -> List CFType -> List (Maybe String)
    mkNs i [] = []
    mkNs i (CFWorld :: xs) = Nothing :: mkNs i xs
    mkNs i (x :: xs) = Just ("cb" ++ show i) :: mkNs (i + 1) xs

    applyLams : String -> List (Maybe String) -> String
    applyLams n [] = n
    applyLams n (Nothing :: as) = applyLams ("(" ++ n ++ " #f)") as
    applyLams n (Just a :: as) = applyLams ("(" ++ n ++ " " ++ a ++ ")") as

    replaceChar : Char -> Char -> String -> String
    replaceChar old new = pack . replaceOn old new . unpack

    buildCWrapperDefs : CCallbackInfo -> CWrapperDefs
    buildCWrapperDefs (MkCCallbackInfo arg schemeWrap callbackStr argTypes retType) =
      let box = schemeWrap ++ "-box"
          setBox = "\n (set-box! " ++ box ++ " " ++ callbackStr ++ ")"
          cWrapName = replaceChar '-' '_' schemeWrap
          boxDef = "\n(define " ++ box ++ " (box #f))\n"

          args =
            if length argTypes > 0
              then " " ++ (showSep " " $ map (\i => "farg-" ++ show i) [0 .. (natToInteger $ length argTypes) - 1])
              else ""

          cWrapDef =
            "\n(c-define " ++
            "(" ++ schemeWrap ++ args ++ ")" ++
            " (" ++ showSep " " argTypes ++ ")" ++
            " " ++ retType ++
            " \"" ++ cWrapName ++ "\"" ++ " \"\"" ++
            "\n ((unbox " ++ box ++ ")" ++ args ++ ")" ++
            "\n)\n"
      in MkCWrapperDefs setBox boxDef cWrapDef

    buildCFunWrapDeclaration : String -> String -> List String -> String
    buildCFunWrapDeclaration name ret args =
      "\n(c-declare #<<c-declare-end\n" ++
      ret ++ " " ++ name ++ "(" ++ showSep ", " args ++ ");" ++
      "\nc-declare-end\n)\n"

    mkFun : List CFType -> CFType -> String -> String
    mkFun args ret n
        = let argns = mkNs 0 args in
              "(lambda (" ++ showSep " " (mapMaybe id argns) ++ ") "
              ++ (applyLams n argns ++ ")")

    callback : String -> List CFType -> CFType -> Core (String, List String, String)
    callback n args (CFFun s t) = callback n (s :: args) t
    callback n args_rev retty
        = do let args = reverse args_rev
             argTypes <- traverse (cftySpec fc) (filter notWorld args)
             retType <- cftySpec fc retty
             pure (mkFun args retty n, argTypes, retType)

    buildArg : (Name, CFType) -> Core (String, Maybe CCallbackInfo)
    buildArg (n, CFFun s t) = do
      let arg = schName n
      let schemeWrap = fnWrapName arg
      (callbackBody, argTypes, retType) <- callback arg [s] t
      pure (schemeWrap, Just $ MkCCallbackInfo arg schemeWrap callbackBody argTypes retType)
    buildArg (n, _) = pure (schName n, Nothing)

schemeCall : FC -> (sfn : String) ->
             List Name -> CFType -> Core String
schemeCall fc sfn argns ret
    = let call = "(" ++ sfn ++ " " ++ showSep " " (map schName argns) ++ ")" in
          case ret of
               CFIORes _ => pure $ mkWorld call
               _ => pure call

-- Use a calling convention to compile a foreign def.
-- Returns the name of the static library to link and the body
-- of the function call.
useCC : {auto c : Ref Ctxt Defs} ->
        {auto l : Ref Loaded (List String)} ->
        FC -> List String -> List (Name, CFType) -> CFType -> Core (Maybe String, (String, String))
useCC fc ccs args ret
    = case parseCC ["scheme,gambit", "scheme", "C"] ccs of
           Nothing => throw (NoForeignCC fc ccs)
           Just ("scheme,gambit", [sfn]) => pure (Nothing, (!(schemeCall fc sfn (map fst args) ret), ""))
           Just ("scheme", [sfn]) => pure (Nothing, (!(schemeCall fc sfn (map fst args) ret), ""))
           Just ("C", [cfn, clib]) => pure (Just clib, !(cCall fc cfn (fnWrapName cfn) clib args ret))
           Just ("C", [cfn, clib, chdr]) => pure (Just clib, !(cCall fc cfn (fnWrapName cfn) clib args ret))
           _ => throw (NoForeignCC fc ccs)
  where
    fnWrapName : String -> String -> String
    fnWrapName cfn schemeArgName = schemeArgName ++ "-" ++ cfn ++ "-cFunWrap"

-- For every foreign arg type, return a name, and whether to pass it to the
-- foreign call (we don't pass '%World')
mkArgs : Int -> List CFType -> List (Name, Bool)
mkArgs i [] = []
mkArgs i (CFWorld :: cs) = (MN "farg" i, False) :: mkArgs i cs
mkArgs i (c :: cs) = (MN "farg" i, True) :: mkArgs (i + 1) cs

mkStruct : {auto s : Ref Structs (List String)} ->
           CFType -> Core String
mkStruct (CFStruct n flds)
    = do defs <- traverse mkStruct (map snd flds)
         strs <- get Structs
         if n `elem` strs
            then pure (concat defs)
            else do put Structs (n :: strs)
                    pure $ concat defs ++ "(define-c-struct " ++ n ++ " "
                           ++ showSep " " !(traverse showFld flds) ++ ")\n"
  where
    showFld : (String, CFType) -> Core String
    showFld (n, ty) = pure $ "(" ++ n ++ " " ++ !(cftySpec emptyFC ty) ++ ")"
mkStruct (CFIORes t) = mkStruct t
mkStruct (CFFun a b) = do ignore (mkStruct a); mkStruct b
mkStruct _ = pure ""

schFgnDef : {auto c : Ref Ctxt Defs} ->
            {auto l : Ref Loaded (List String)} ->
            {auto s : Ref Structs (List String)} ->
            FC -> Name -> NamedDef -> Core (Maybe String, String)
schFgnDef fc n (MkNmForeign cs args ret)
    = do let argns = mkArgs 0 args
         let allargns = map fst argns
         let useargns = map fst (filter snd argns)
         argStrs <- traverse mkStruct args
         retStr <- mkStruct ret
         (lib, (body, wrapDeclarations)) <- useCC fc cs (zip useargns args) ret
         defs <- get Ctxt
         pure (lib,
                concat argStrs ++ retStr ++
                wrapDeclarations ++
                "(define " ++ schName !(full (gamma defs) n) ++
                " (lambda (" ++ showSep " " (map schName allargns) ++ ") " ++
                body ++ "))\n")
schFgnDef _ _ _ = pure (Nothing, "")

getFgnCall : {auto c : Ref Ctxt Defs} ->
             {auto l : Ref Loaded (List String)} ->
             {auto s : Ref Structs (List String)} ->
             (Name, FC, NamedDef) -> Core (Maybe String, String)
getFgnCall (n, fc, d) = schFgnDef fc n d

compileToSCM : Ref Ctxt Defs ->
               ClosedTerm -> (outfile : String) -> Core (List String)
compileToSCM c tm outfile
    = do cdata <- getCompileData False Cases tm
         let ndefs = namedDefs cdata
         -- let tags = nameTags cdata
         let ctm = forget (mainExpr cdata)

         defs <- get Ctxt
         l <- newRef {t = List String} Loaded []
         s <- newRef {t = List String} Structs []
         fgndefs <- traverse getFgnCall ndefs
         compdefs <- traverse (getScheme gambitPrim gambitString) ndefs
         let code = fastAppend (map snd fgndefs ++ compdefs)
         main <- schExp gambitPrim gambitString 0 ctm
         support <- readDataFile "gambit/support.scm"
         ds <- getDirectives Gambit
         extraRuntime <- getExtraRuntime ds
         foreign <- readDataFile "gambit/foreign.scm"
         let scm = showSep "\n" [schHeader, support, extraRuntime, foreign, code, main]
         Right () <- coreLift $ writeFile outfile scm
            | Left err => throw (FileErr outfile err)
         pure $ mapMaybe fst fgndefs

compileExpr : Ref Ctxt Defs -> (tmpDir : String) -> (outputDir : String) ->
              ClosedTerm -> (outfile : String) -> Core (Maybe String)
compileExpr c tmpDir outputDir tm outfile
    = do let srcPath = tmpDir </> outfile <.> "scm"
         let execPath = outputDir </> outfile
         libsname <- compileToSCM c tm srcPath
         libsfile <- traverse findLibraryFile $ map (<.> "a") (nub libsname)
         gsc <- coreLift findGSC
         gscBackend <- coreLift findGSCBackend
         ds <- getDirectives Gambit
         let gscCompileOpts =
             case find (== "C") ds of
                 Nothing => gscBackend ++ " -exe -cc-options \"-Wno-implicit-function-declaration\" -ld-options \"" ++
                   (showSep " " libsfile) ++ "\""
                 Just _ => " -c"
         let cmd =
             gsc ++ gscCompileOpts ++ " -o \"" ++ execPath ++ "\" \"" ++ srcPath ++ "\""
         ok <- coreLift $ system cmd
         if ok == 0
            then pure (Just execPath)
            else pure Nothing

executeExpr : Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
executeExpr c tmpDir tm
    = do Just sh <- compileExpr c tmpDir tmpDir tm "_tmpgambit"
           | Nothing => throw (InternalError "compileExpr returned Nothing")
         coreLift_ $ system sh -- TODO: on windows, should add exe extension
         pure ()

export
codegenGambit : Codegen
codegenGambit = MkCG compileExpr executeExpr Nothing Nothing


text:
module Weaken

import Data.Fin

weaken1 : (fn : Fin n) -> (fsn : Fin (S n) ** finToNat fn = finToNat fsn)
weaken1 FZ = (FZ ** Refl)
weaken1 (FS n) with (weaken1 n)
  | (nw ** nat_n_eq_nat_nw) = (FS nw ** eqSucc (finToNat n) (finToNat nw) nat_n_eq_nat_nw)

ext: idr

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
parameters (X : Nat)
  foo : Bool -> ()
  foo n = ?help


text:
module TyTTP.URL

import Control.Monad.Either
import Data.List
import Data.String
import TyTTP

public export
data Scheme
  = HTTP
  | HTTPS
  | OtherScheme String

namespace Scheme
  export
  parse : String -> Scheme
  parse "http" = HTTP
  parse "https" = HTTPS
  parse str = OtherScheme str

public export
record URL a p s where
  constructor MkURL
  scheme : Maybe Scheme
  authority : Maybe a
  path : p
  search : s

namespace Simple

  public export
  SimpleURL : Type
  SimpleURL = URL String String String

  public export
  data URLParserError
    = EmptyString
    | MissingAuthorityOrPath

  export -- visible for testing
  parse : String -> Either URLParserError SimpleURL
  parse str = scheme (unpack $ trim str) $ MkURL Nothing Nothing "" ""
    where
      search : List Char -> SimpleURL -> Either URLParserError SimpleURL
      search [] url = Right url
      search xs url = Right $ { search := pack xs } url

      path : List Char -> SimpleURL -> Either URLParserError SimpleURL
      path [] url = Right $ { path := "/" } url
      path xs url =
        let (p, rest) = List.break (== '?') xs
        in search rest $ { path := pack p } url

      authority : List Char -> SimpleURL -> Either URLParserError SimpleURL
      authority ('/' :: '/' :: xs) url =
        let (auth, rest) = List.break (== '/') xs
        in path rest $ { authority := Just $ pack auth } url
      authority [] _ = Left MissingAuthorityOrPath
      authority x url = path x url

      scheme : List Char -> SimpleURL -> Either URLParserError SimpleURL
      scheme ('h' :: 't' :: 't' :: 'p' :: xs) url =
        case xs of
           ('s' :: ':' :: ys) => authority ys $ { scheme := Just HTTPS } url
           (':' :: ys) => authority ys $ { scheme := Just HTTP } url
           xs => path ('h' :: 't' :: 't' :: 'p' :: xs) url
      scheme [] _ = Left EmptyString
      scheme xs url = authority xs url

  export
  url : MonadError URLParserError m
    => (
      Step me SimpleURL h1 s h2 a b
      -> m $ Step me' SimpleURL h1' s' h2' a' b'
    )
    -> Step me String h1 s h2 a b
    -> m $ Step me' String h1' s' h2' a' b'
  url handler step = case parse step.request.url of
    Right u => do
      result <- handler $ { request.url := u } step
      pure $ { request.url := step.request.url } result
    Left err => throwError err

  export
  url' : Monad m
    => (
      URLParserError
      -> Step me String h1 s h2 a b
      -> m $ Step me' String h1' s' h2' a' b'
    )
    -> (
      Step me SimpleURL h1 s h2 a b
      -> EitherT URLParserError m $ Step me' SimpleURL h1' s' h2' a' b'
    )
    -> Step me String h1 s h2 a b
    -> m $ Step me' String h1' s' h2' a' b'
  url' errHandler handler step = do
    Right result <- runEitherT $ Simple.url handler step
      | Left err => errHandler err step
    pure result

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp


text:
module Bautzen.ZoC

import Bautzen.GameUnit
import Bautzen.Pos

import Data.List.Extra

import Data.List
import Data.Nat
import Data.Vect

-- section 3
-- zones of control

public export
data ZoC : Type where
  InZoC : (side : Side) -> ZoC
  Free : ZoC

public export
Eq ZoC where
  Free == Free = True
  (InZoC s) == (InZoC s') = s == s'
  _ == _ = False

||| Test if given position for given `side` is in the ZoC of the unit.
public export
inZocOf : (pos : Pos) -> (side : Side) -> (GameUnit, Pos) -> Bool
inZocOf pos curSide (unit, location) with (curSide == side (nation unit))
  inZocOf pos curSide (unit, location) | False = pos `elem` neighbours location
  inZocOf pos curSide (unit, location) | True = False

||| Is the given `Pos`ition in an enemy ZoC?
||| This assumes the current `side` is playing and checking ZoCs
public export
inZoC : Side -> List (GameUnit, Pos) -> Pos -> ZoC
inZoC curSide units pos =
  case find' (inZocOf pos curSide) units of
    Nothing => Free
    (Just (unit, _)) => InZoC (side $ nation unit)

-- ZoC tests

-- inZoCTrue : inZocOf (Hex 3 3) Axis (Bautzen.GameUnit.p13_5dp, Hex 3 4) = True
-- inZoCTrue = Refl

-- inZoCTrue2 : inZocOf (Hex 4 3) Axis (Bautzen.GameUnit.p13_5dp, Hex 3 4) = False
-- inZoCTrue2 = Refl

-- inZoCFalsePolish : inZocOf (Hex 3 3) Allies (Bautzen.GameUnit.p13_5dp, Hex 3 4) = False
-- inZoCFalsePolish = Refl

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module Transducers.Utils

import Transducers.Core

--------------------------------------------------------------------------------
-- Utils to conjoin elements to a container
--------------------------------------------------------------------------------

public export
interface Conj xs x where
  conj : xs -> x -> xs

export
implementation Conj (List a) a where
  conj xs x = x :: xs

export
implementation Conj String Char where
  conj xs x = xs ++ singleton x

--------------------------------------------------------------------------------
-- Utils to conjoin the result of a transduce into a container
--------------------------------------------------------------------------------

export
into : (Foldable t, Conj acc a) => acc -> Transducer acc () s b a -> t b -> acc
into acc xf = transduce xf conj acc

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
> module NonNegDouble.Measures

> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import NonNegDouble.Operations
> import NonNegDouble.Properties

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

> using implementation FractionalNonNegDouble
>   |||
>   average : List NonNegDouble -> NonNegDouble
>   average xs = (sum xs) * ( one / fromNat (length xs))

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
||| mutable stack
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Container.Mutable.Stack

import Data.Container.Mutable.Array

import Data.Fin
import Data.List1
import Data.IORef
import Data.So
import System.Info

%default total

-- --------------------------------------------------------------------------
-- Backend specific mutable stack

namespace Prim

  data PrimIOStack : Type -> Type where [external]

  %foreign "javascript:lambda:() => new Array()"
  prim__iostack_new : PrimIO (PrimIOStack t)

  %foreign "javascript:lambda:(x, xs) => xs.push(x)"
  prim__iostack_push : t -> PrimIOStack t -> PrimIO ()

  %foreign "javascript:lambda:(d, f, xs) => { const x = xs.pop(); return (x === undefined)? d : f(x); }"
  prim__iostack_pop : a -> (t -> a) -> PrimIOStack t -> PrimIO a

  %foreign "javascript:lambda:(xs) => xs.length == 0"
  prim__iostack_null : PrimIOStack t -> PrimIO Bool

  %foreign "javascript:lambda:(xs) => xs.length"
  prim__iostack_length : PrimIOStack t -> PrimIO Int

  %inline export newPrimIOStack : HasIO io => io (PrimIOStack t)
  newPrimIOStack = primIO $ prim__iostack_new

  export null : HasIO io => PrimIOStack t -> io Bool
  null xs   = primIO $ prim__iostack_null xs

  export length : HasIO io => PrimIOStack t -> io Nat
  length xs  = (primIO $ prim__iostack_length xs) >>= pure . fromInteger . cast

  export push : HasIO io => t -> PrimIOStack t -> io ()
  push x xs = primIO $ prim__iostack_push x xs

  export pop : HasIO io => PrimIOStack t -> io (Maybe t)
  pop xs    = primIO $ prim__iostack_pop Nothing Just xs

  {-
  export
  HasIO io => MutableStack io PrimIOStack where
    null xs   = primIO $ prim__iostack_null xs
    length xs  = (primIO $ prim__iostack_length xs) >>= pure . fromInteger . cast
    push x xs = primIO $ prim__iostack_push x xs
    pop xs    = primIO $ prim__iostack_pop Nothing Just xs
  -}

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

%inline public export
HasNativeIOStack : Bool
HasNativeIOStack with (codegen)
  HasNativeIOStack | "javascript" = True
  HasNativeIOStack | _            = False

-- --------------------------------------------------------------------------
-- Generic IOArray based mutable stack
namespace Generic

  export
  record IOArrayStack t where
    constructor MkIOArrayStack
    allocsize : IORef Nat
    pages : IORef (Nat, List1 (IOArray (Maybe t)))

  export newIOArrayStack : HasIO io => io (IOArrayStack t)
  newIOArrayStack = do
    let s = 511
    xs <- newIOArray (S s) Nothing
    pure $ MkIOArrayStack !(newIORef s) !(newIORef (0, (xs:::[])))

  export null : HasIO io => IOArrayStack t -> io Bool
  null xs   = do
    (n, (y:::ys)) <- readIORef xs.pages
    pure $ n == 0 && null ys

  export length : HasIO io => IOArrayStack t -> io Nat
  length xs  = do
    (n, (y:::ys)) <- readIORef xs.pages
    pure $ fromInteger $ cast $ sum (map capacity ys) + (cast n)

  export push : HasIO io => t -> IOArrayStack t -> io ()
  push x xs = do
    (n, ys'@(y:::ys)) <- readIORef xs.pages
    case natToFin n (S $ ubound y) of
         Just n' => writeIOArray y n' (Just x) >> writeIORef xs.pages (S n, ys')
         Nothing => do
           -- update acclocation unit size.
           ac <- readIORef xs.allocsize
           let newac = if capacity y < S ac then ac else S (ac + ac)
           writeIORef xs.allocsize newac

           -- allocate new page
           newpage <- newIOArray (S newac) Nothing
           writeIOArray newpage 0 (Just x)
           writeIORef xs.pages (1, (newpage:::(y::ys)))

  export pop : HasIO io => IOArrayStack t -> io (Maybe t)
  pop xs    = do
    (n, ys'@(y:::ys)) <- readIORef xs.pages
    case n of
         S n' => do
           writeIORef xs.pages (n', ys')
           let n'' = restrict y (cast n')
           r <- readIOArray y n''
           writeIOArray y n'' Nothing
           pure r

         Z => case ys of
                   [] => pure Nothing
                   (y'::ys'') => do
                     writeIORef xs.pages (ubound y', y':::ys'')
                     let l = restrict y' $ cast $ ubound y'
                     r <- readIOArray y' l
                     writeIOArray y' l Nothing
                     pure r

{-
export
HasIO io => MutableStack io IOArrayStack where
  null xs   = do
    (n, (y:::ys)) <- readIORef xs.pages
    pure $ n == 0 && null ys

  length xs  = do
    (n, (y:::ys)) <- readIORef xs.pages
    pure $ fromInteger $ cast $ sum (map capacity ys) + (cast n)

  push x xs = do
    (n, ys'@(y:::ys)) <- readIORef xs.pages
    case natToFin n (S $ ubound y) of
         Just n' => writeIOArray y n' (Just x) >> writeIORef xs.pages (S n, ys')
         Nothing => do
           -- update acclocation unit size.
           ac <- readIORef xs.allocsize
           let newac = if capacity y < S ac then ac else S (ac + ac)
           writeIORef xs.allocsize newac

           -- allocate new page
           newpage <- newIOArray (S newac) Nothing
           writeIOArray newpage 0 (Just x)
           writeIORef xs.pages (1, (newpage:::(y::ys)))

  pop xs    = do
    (n, ys'@(y:::ys)) <- readIORef xs.pages
    case n of
         S n' => do
           writeIORef xs.pages (n', ys')
           let n'' = restrict y (cast n')
           r <- readIOArray y n''
           writeIOArray y n'' Nothing
           pure r

         Z => case ys of
                   [] => pure Nothing
                   (y'::ys'') => do
                     writeIORef xs.pages (ubound y', y':::ys'')
                     let l = restrict y' $ cast $ ubound y'
                     r <- readIOArray y' l
                     writeIOArray y' l Nothing
                     pure r
-}

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

{- WONN'T WORK!!!!

public export %inline IOStack : Type -> Type
IOStack t with (HasNativeIOStack)
  IOStack t | True  = PrimIOStack t
  IOStack t | False = IOArrayStack t

public export %inline
newIOStack : HasIO io => io (IOStack t)
newIOStack with (HasNativeIOStack)
  newIOStack | True  = newPrimIOStack
  newIOStack | False = newIOArrayStack
{-
export
IOStackMutableStack : HasIO io => MutableStack io IOStack t
IOStackMutableStack with (hasNativeIOStack)
  IOStackMutableStack | True  = PrimIOStackMutableStack
  IOStackMutableStack | False = IOArrayStackMutableStack
  -}
-- public export
-- HasIO io => MutableStack io IOStack t using IOStackMutableStack where

-}
-- --------------------------------------------------------------------------
-- vim: tw=80 sw=2 expandtab :


text:
module Lukasiewicz

import Prelude.Bool

%access public export

%default total

-- ||| Three values for Kleene logic as type
-- ||| Also interpretable as a Fuzzy Boolean
-- ||| Also intrepretable in the context of Map Theory
-- data Fool = T True | U Unknown | F False

||| Fuzzy Bool Representation
Fool : Type
Fool = Maybe Bool  -- Fuzzy Logic | Quantum Logic | Category Theory | Map Theory
-- TODO : -> Lazy Bool ?

-- useful aliases for lazy people
T : Fool
T = Just True

F : Fool
F = Just False

U : Fool
U = Nothing

||| Kleene NOT
||| Ref https://en.wikipedia.org/wiki/Three-valued_logic#Kleene_and_Priest_logics
not : Fool -> Fool
not Nothing = Nothing
not (Just b) = (Just (not b))

imp: Fool -> Fool -> Fool
imp (Just False) _ = (Just True)
imp Nothing False = Nothing
imp Nothing _ = (Just True)
imp (Just True) b = b

max_stars_repo_name: asmodehn/idris-playground

max_issues_repo_name: asmodehn/idris-playground

max_forks_repo_name: asmodehn/idris-playground


text:
||| An expression language with mechanical proof of type-safety.
|||
||| `Recorded` is an expression language supporting Let-bindings, and
||| Records i.e. Named Tuples.  Standard constructions are used to
||| represent the language as an EDSL, together with proof of progress
||| taken from PLFA Part 2.
|||
||| This module represents Section 3 of the Functional Pearl.
|||
module Razor.Recorded

import Razor.Common

%default total

namespace Types

  public export
  data Ty = TyInt
          | TyChar
          | TyRecord (Vect (S n) Ty)

namespace Terms

  mutual
    ||| Field in a record.
    public export
    data Field : (g : List Ty)
              -> (type  : Ty)
              -> Type
      where
        MkField : (value : Recorded g type)
                        -> Field    g type

    ||| Record Fields.
    public export
    data Fields : (g : List Ty)
               -> (types : Vect (S n) Ty)
               -> Type
      where
        Singleton : (first : Field  g  ty)
                          -> Fields g (ty::Nil)

        Extend : (next : Field  g  ty)
              -> (rest : Fields g      tys)
                      -> Fields g (ty::tys)

    public export
    data Recorded : List Ty -> Ty -> Type where
          -- Let-Bindings & Variables
          Var : Elem ty g -> Recorded g ty

          Let : {expr, body : Ty}
             -> (this     : Recorded        g  expr)
             -> (beInThis : Recorded (expr::g) body)
                         -> Recorded        g  body

          -- Base Values
          I : Int  -> Recorded g TyInt
          C : Char -> Recorded g TyChar

          -- Records & Accessors
          MkRecord : {types  : Vect (S n) Ty}
                  -> (values : Fields   g           types)
                            -> Recorded g (TyRecord types)

          Proj : {type : Ty}
              -> {types : Vect (S n) Ty}
              -> (rec   : Recorded g (TyRecord types))
              -> (idx   : Elem type types)
                       -> Recorded g type

  public export
  index : (idx    : Elem type types)
       -> (fields : Fields g types)
       -> Recorded g type
  index Here (Singleton (MkField value)) = value
  index Here (Extend (MkField value) rest) = value
  index (There later) (Extend next rest) = index later rest

namespace Renaming

  public export
  weaken : (Contains  old           type -> Contains  new           type)
        -> (Contains (old += type') type -> Contains (new += type') type)

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

  mutual
    namespace Fields
      public export
      rename : (forall type  . Contains old type  -> Contains new type)
            -> (forall types . Fields   old types -> Fields   new types)
      rename f (Singleton (MkField first))
        = Singleton (MkField (rename f first))
      rename f (Extend (MkField next) rest)
        = Extend (MkField (rename f next)) (rename f rest)

    public export
    rename : (forall type . Contains old type -> Contains new type)
          -> (forall type . Recorded old type -> Recorded new type)
    -- Let-Bindings & Variables
    rename f (Var x) = Var (f x)
    rename f (Let this beInThis)
      = Let (rename f this)
            (rename (weaken f) beInThis)

    -- Base Values
    rename f (I x) = I x
    rename f (C x) = C x

    -- Records & Accessors
    rename f (MkRecord values) = MkRecord (rename f values)
    rename f (Proj rec idx) = Proj (rename f rec) idx

namespace Substitution
  public export
  weakens : (forall type . Contains  old type
                        -> Recorded  new type)
         -> (forall type . Contains (old += type') type
                        -> Recorded (new += type') type)
  weakens f Here         = Var Here
  weakens f (There rest) = rename There (f rest)

  namespace General
    mutual
      namespace Fields
        public export
        subst : (f : forall type  . Contains old type  -> Recorded new type)
                 -> (forall types . Fields   old types -> Fields   new types)
        subst f (Singleton (MkField first))
          = Singleton (MkField (subst f first))
        subst f (Extend (MkField next) rest)
          = Extend (MkField (subst f next)) (subst f rest)

      public export
      subst : (forall type . Contains old type -> Recorded new type)
           -> (forall type . Recorded old type -> Recorded new type)
      -- Let-Bindings & Variables
      subst f (Var x) =  f x
      subst f (Let this beInThis)
        = Let (subst f this)
              (subst (weakens f) beInThis)

      -- Base Values
      subst f (I x) = I x
      subst f (C x) = C x

      -- Records & Accesors
      subst f (MkRecord values) = MkRecord (subst f values)
      subst f (Proj rec idx)    = Proj (subst f rec) idx

  namespace Single
    public export
    apply : (this : Recorded  ctxt           typeB)
         -> (idx  : Contains (ctxt += typeB) typeA)
                 -> Recorded  ctxt           typeA
    apply this Here         = this
    apply this (There rest) = Var rest

    public export
    subst : (this   : Recorded  ctxt           typeB)
         -> (inThis : Recorded (ctxt += typeB) typeA)
                   -> Recorded  ctxt           typeA
    subst {ctxt} {typeA} {typeB} this inThis
      = General.subst (apply this) inThis

namespace Values
  mutual
    namespace Field
      public export
      data Value : (field  : Field g type) -> Type
        where
          MkField : (prf : Value v)
                        -> Value (MkField v)

    namespace Fields
      public export
      data Value : (fields : Fields g types) -> Type
        where
          Singleton : (field : Value value)
                            -> Value (Singleton value)

          Extend : {value  : Field g type}
                -> {values : Fields g types}
                -> (next   : Value value)
                -> (rest   : Value values)
                          -> Value (Extend value values)

    public export
    data Value : Recorded ctxt type -> Type where
      -- Base Values
      I : Value (I i)
      C : Value (C c)

      -- Records
      MkRecord : Value fields -> Value (MkRecord fields)

namespace Reduction

  mutual
    namespace Field
      public export
      data Redux : (this, that : Field ctxt type) -> Type
        where
          SimplifyField : {this, that : Recorded g type}
                       -> (prf        : Redux this that)
                                     -> Redux (MkField this)
                                              (MkField that)

    namespace Fields
      public export
      data Redux : (this, that : Terms.Fields g types) -> Type
        where
          SimplifySingleton : (prf : Redux this that)
                                  -> Redux (Singleton this)
                                           (Singleton that)

          SimplifyExtend : {this, that : Field g type}
                        -> {rest       : Fields g types}
                        -> (prf        : Redux this that)
                                      -> Redux (Extend this rest)
                                               (Extend that rest)

          SimplifyExtendV : {this, that : Fields ctxt types}
                         -> {v          : Field ctxt type}
                         -> (value      : Value v)
                         -> (rest       : Redux this that)
                                       -> Redux (Extend v this)
                                                (Extend v that)

    public export
    data Redux : (this, that : Recorded ctxt type) -> Type where
      -- Let Bindings
      SimplifyLetValue : Redux this that
                      -> Redux (Let this body)
                               (Let that body)
      ReduceLetBody : Value value
                   -> Redux (Let value body)
                            (subst value body)

      SimplifyRecord : Redux this that
                    -> Redux (MkRecord this) (MkRecord that)

      -- Accessors
      SimplifyProj : {type       : Ty}
                  -> {labels     : Vect (S n) Ty}
                  -> {this, that : Recorded g (TyRecord labels)}
                  -> {idx        : Elem type labels}
                                -> Redux this that
                                -> Redux (Proj this idx) (Proj that idx)

      ReduceProj : {type   : Ty}
                -> {types  : Vect (S n) Ty}
                -> {fields : Fields g types}
                -> {idx    : Elem type types}
                -> (values : Value fields)
                          -> Redux (Proj (MkRecord fields) idx)
                                   (index idx fields)

namespace Progress

  public export
  data Progress : (term : Recorded Nil type)
                       -> Type
    where
      Done : {term : Recorded Nil type} -> Value term -> Progress term
      Step : {type : Ty}
          -> {this, that : Recorded Nil type}
          -> (step  : Redux this that)
                   -> Progress this

  namespace Field
    public export
    data Progress : (field : Field Nil type) -> Type where
      Done : Value field -> Progress field
      Step : {this, that : Field Nil type}
          -> (step       : Redux this that)
                        -> Progress this

  namespace Fields
    public export
    data Progress : (fields : Fields Nil types) -> Type where
      Done :  (value : Value fields) -> Progress fields

      Step : {this, that : Fields Nil types}
          -> (step       : Redux this that)
                        -> Progress this

  mutual
    namespace Field
      public export
      progress : (field : Field Nil type)
              -> Progress field
      progress (MkField value) with (progress value)
        progress(MkField value) | (Done v)
          = Done (MkField v)
        progress(MkField value) | (Step step)
          = Step (SimplifyField step)

    namespace Fields
      public export
      progress : (fields : Fields Nil types)
              -> Progress fields
      progress (Singleton first) with (Field.progress first)
        progress (Singleton first) | (Done x)
          = Done (Singleton x)
        progress (Singleton first) | (Step prf)
          = Step (SimplifySingleton prf)

      progress (Extend next rest) with (progress next)
        progress (Extend next rest) | (Done x) with (progress rest)
          progress (Extend next rest) | (Done x) | (Done xs)
            = Done (Extend x xs)
          progress (Extend next rest) | (Done x) | (Step prf)
            = Step (SimplifyExtendV x prf)

        progress (Extend next rest) | (Step prf)
          = Step (SimplifyExtend prf)

    public export
    progress : forall type . (term : Recorded Nil type) -> Progress term
    -- Let-Bindings & Variables
    progress (Var _) impossible
    progress (Let this beInThis) with (progress this)
      progress (Let this beInThis) | (Done x)
        = Step (ReduceLetBody x)
      progress (Let this beInThis) | (Step prf)
        = Step (SimplifyLetValue prf)

    -- Base Values
    progress (I x) = Done I
    progress (C x) = Done C

    -- Records & Accessors
    progress (MkRecord values) with (progress values)
      progress (MkRecord values) | (Done v)   = Done (MkRecord v)
      progress (MkRecord values) | (Step prf) = Step (SimplifyRecord prf)

    progress (Proj rec idx) with (progress rec)
      progress (Proj (MkRecord fields) idx) | (Done (MkRecord fieldsV))
        = Step (ReduceProj fieldsV)
      progress (Proj rec idx) | (Step prf)
        = Step (SimplifyProj prf)

namespace Evaluation

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

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

  public export
  data Evaluate : (term : Recorded Nil type) -> Type where
    RunEval : {this, that : Recorded 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 : (fuel : Fuel)
         -> (term : Recorded 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 : (this : Recorded Nil type)
           -> Maybe (Subset (Recorded 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 Examples

  public export
  pairIC : Recorded Nil (TyRecord [TyInt, (TyChar)])
  pairIC = MkRecord (Extend    (MkField (I 1))
                    (Singleton (MkField (C 'c'))))

  public export
  i : Recorded Nil TyInt
  i = Proj pairIC Here

  public export
  c : Recorded Nil TyChar
  c = Proj pairIC (There Here)

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 SequentialDecisionProblems.applications.Main

> import Data.Fin
> import Data.List
> import Data.List.Quantifiers
> import Data.So
> import Effects
> import Effect.Exception
> import Effect.StdIO

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.FullTheory
> import SequentialDecisionProblems.TabBackwardsInduction
> import SequentialDecisionProblems.Utils
> import SequentialDecisionProblems.FastStochasticDefaults
> import SequentialDecisionProblems.CoreTheoryOptDefaults
> import SequentialDecisionProblems.FullTheoryOptDefaults
> import SequentialDecisionProblems.TabBackwardsInductionOptDefaults

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.BasicProperties
> import FastSimpleProb.MonadicOperations
> import FastSimpleProb.MonadicProperties
> import FastSimpleProb.Measures
> import FastSimpleProb.MeasuresProperties
> import FastSimpleProb.Operations
> import Sigma.Sigma
> import Sigma.Operations
> import Sigma.Properties
> import Nat.LTProperties
> import Double.Predicates
> import Double.Postulates
> import Double.Operations
> import Double.Properties
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import NonNegDouble.Predicates
> import NonNegDouble.LTEProperties
> import NonNegDouble.Measures
> import NonNegDouble.MeasureProperties
> import Finite.Predicates
> import Finite.Operations
> import Finite.Properties
> import Unique.Predicates
> import Decidable.Predicates
> import Decidable.Properties
> import LocalEffect.Exception
> import LocalEffect.StdIO
> import Fin.Operations
> import Fraction.Fraction
> import Fraction.Normal
> import Nat.Positive
> import List.Operations
> import Unit.Properties

> -- %default total
> %auto_implicits off
> -- %logging 5

> computation : { [STDIO] } Eff ()
> computation =
>   do putStrLn "done!"

> main : IO ()
> main = run computation

> {-

> ---}

-- Local Variables:
-- idris-packages: ("effects")
-- End:


text:
module lib.Library2

import lib.Library3

export
salute2 : String
salute2 = "Hello, this is Library 2, friend of Library 3 who salutes:\n    " ++ salute3


text:
module Database

import Schema

import Decidable.Equality

public export data DB : String -> Type where
  MkDB : (dbFile : String) ->
         (dbTables : List (String, Schema)) -> DB dbFile

%name DB db

public export data HasTable : List (String, Schema) -> String -> Schema -> Type where
  Here : HasTable ((name, s)::ts) name s
  There : HasTable ts name s ->
          HasTable ((name',s')::ts) name s

max_stars_repo_name: ethansr/IdrisSqlite

max_issues_repo_name: ethansr/IdrisSqlite

max_forks_repo_name: ethansr/IdrisSqlite


text:
module ParsingTest

import System

import Effects
import Effect.StdIO
import Effect.Exception
import Effect.System

import public Lightyear
import public Lightyear.Strings

import TestRunner

-- ----------------------------------------------------------- [ Parsing Tests ]

||| Expect a parsing test to pass.
parseTestGood : Parser a -> String -> Test
parseTestGood p s = case parse p s of
    Left err => raise $ "Expected passing test failed " ++ err
    Right re => pure ()

||| Expect a test to fail
parseTestBad : Parser a -> String -> Test
parseTestBad p s = case parse p s of
    Left err => pure ()
    Right re => raise "Expected failing test passed..."
-- --------------------------------------------------------------------- [ EPF ]

max_stars_repo_name: jfdm/idris-uml

max_issues_repo_name: jfdm/idris-uml

max_forks_repo_name: jfdm/idris-uml


text:
module Proofs.GroupCancelMisc

import public Common.Abbrev
import Specifications.Group
import Symmetry.Opposite
import Proofs.GroupCancelationLemmas
import Proofs.GroupTheory

%default total
%access export

infixl 8 #

groupCancelMisc1 : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b,c : s) ->
  a # (b # inv c) # c = a # b
groupCancelMisc1 spec a b c = o1 @== cong o2 where
  o1 : a # ((b # inv c) # c) = a # (b # inv c) # c
  o1 = associative (monoid spec) _ _ _
  o2 : (b # inv c) # c = b
  o2 = groupCancel2bis spec b c

groupCancelMisc2 : {(#) : Binop s} -> GroupSpec (#) e inv -> (a,b,c : s) ->
  a # b # inv (c # b) = a # inv c
groupCancelMisc2 spec a b c = o4 @== cong o3 where
  o1 : b # inv (c # b) = b # (inv b # inv c)
  o1 = cong (groupInverseAnti spec c b)
  o2 : b # (inv b # inv c) = inv c
  o2 = groupCancel2bis (opposite spec) _ b
  o3 : b # inv (c # b) = inv c
  o3 = o1 === o2
  o4 : a # (b # inv (c # b)) = a # b # inv (c # b)
  o4 = associative (monoid spec) _ _ _

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
-- ------------------------------------------------------------- [ Strings.idr ]
-- Module      : Lightyear.Strings
-- Description : String-related parsers.
--
-- This code is distributed under the BSD 2-clause license.
-- See the file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Lightyear.Strings

import public Data.Vect
import public Data.Fin

import public Control.Monad.Identity

import Lightyear.Position
import Lightyear.Core
import Lightyear.Combinators

import Lightyear.Char

%access export

-- --------------------------------------------------------- [ A String Parser ]
||| Parsers, specialised to Strings
public export
Parser : Type -> Type
Parser = ParserT String Identity

||| Run a parser against an input string
parseGeneric : (src_ident : Maybe String)
            -> (tab_width : Nat)
            -> (parser    : Parser a)
            -> (source    : String)
            -> Either String a
parseGeneric src tw f s = let Id r = execParserT f (initialState src s tw)
                           in case r of
                               MkReply _ (Success x)  => Right x
                               MkReply _ (Failure es) => Left $ concat $ intersperse "\n" $ map display es

||| Run a parser against an input string with a custom tab-width.
parseCustom : (tab_width : Nat)
           -> (parser    : Parser a)
           -> (source    : String)
           -> Either String a
parseCustom = parseGeneric Nothing

||| Run a parser against an input string assuming that tab-widths are
||| eight characters in length.
parse : (parser : Parser a)
     -> (source : String)
     -> Either String a
parse = parseGeneric Nothing 8

namespace File

  ||| Run a parser against an input string taken from the named file
  ||| with a custom tab-width.
  parseCustom : (fname     : String)
             -> (tab_width : Nat)
             -> (parser    : Parser a)
             -> (source    : String)
             -> Either String a
  parseCustom fname = parseGeneric (Just fname)

  ||| Run a parser against an input string taken from the named file,
  ||| such that tab-widths are assumed to be eight characters in
  ||| length.
  parse : (fname  : String)
       -> (parser : Parser a)
       -> (source : String)
       -> Either String a
  parse fname = parseGeneric (Just fname) 8

implementation Stream Char String where
  uncons s with (strM s)
    uncons ""             | StrNil       = Nothing
    uncons (strCons x xs) | StrCons x xs = Just (x, xs)
  updatePos tw pos tk = (increment tw pos tk, pos)

-- ---------------------------------------------------------- [ Reserved Stuff ]

||| A parser that matches a particular string
string : Monad m => String -> ParserT String m String
string s = pack <$> (traverse char $ unpack s) <?> "string " ++ show s

-- ------------------------------------------------------------------- [ Space ]

||| A simple lexer that strips white space from tokens
lexeme : Monad m => ParserT String m a -> ParserT String m a
lexeme p = p <* spaces

-- ------------------------------------------------------------------ [ Tokens ]

||| A parser that matches a specific string, then skips following whitespace
token : Monad m => String -> ParserT String m ()
token s = lexeme (skip (string s)) <?> "token " ++ show s

||| Parses ',' and trailing whitespace.
comma : Monad m => ParserT String m ()
comma = token "," <?> "Comma"

||| Parses '=' and trailing whitespace.
equals : Monad m => ParserT String m ()
equals = token "=" <?> "equals"

||| Parses '.' and trailing whitespace.
dot : Monad m => ParserT String m ()
dot = token "." <?> "dot"

||| Parses ':' and trailing whitespace.
colon : Monad m => ParserT String m ()
colon = token ":" <?> "colon"

||| Parses ';' and trailing whitespace.
semi : Monad m => ParserT String m ()
semi = token ";" <?> "semi colon"

-- -------------------------------------------------- [ Delineated Expressions ]

||| Parses `p` enclosed in parentheses and returns result of `p`.
parens : Monad m => ParserT String m a -> ParserT String m a
parens p = between (token "(") (token ")") p

||| Parses `p` enclosed in brackets and returns result of `p`.
brackets : Monad m => ParserT String m a -> ParserT String m a
brackets p = between (token "[") (token "]") p

||| Parses `p` enclosed in braces and returns the result of `p`.
braces : Monad m => ParserT String m a -> ParserT String m a
braces p = between (token "{") (token "}") p

||| Parses `p` enclosed in angles and returns the result of `p`.
angles : Monad m => ParserT String m a -> ParserT String m a
angles p = between (token "<") (token ">") p

||| Parses `p` enclosed in single quotes and returns the result of `p`.
||| Not to be used for charLiterals.
squote : Monad m => ParserT String m a -> ParserT String m a
squote p = between (char '\'') (lexeme $ char '\'') p

||| Parses `p` enclosed in double quotes and returns the result of `p`.
||| Not to be used for `stringLiterals`.
dquote : Monad m => ParserT String m a -> ParserT String m a
dquote p = between (char '\"') (lexeme $ char '\"') p

||| Collect the literal string contained between two characters
quoted' : Monad m => Char -> Char -> ParserT String m String
quoted' l r = map pack $ between (char l) (lexeme $ char r) (some (satisfy (/= r)))

||| Literal string between two identical characters
quoted : Monad m => Char -> ParserT String m String
quoted c = quoted' c c

-- --------------------------------------------------- [ Separated Expressions ]
||| Parses /one/ or more occurrences of `p` separated by `comma`.
commaSep1 : Monad m => ParserT String m a -> ParserT String m (List a)
commaSep1 p = p `sepBy1` comma

||| Parses /zero/ or more occurrences of `p` separated by `comma`.
commaSep : Monad m => ParserT String m a -> ParserT String m (List a)
commaSep p = p `sepBy` comma

||| Parses /one/ or more occurrences of `p` separated by `semi`.
semiSep1 : Monad m => ParserT String m a -> ParserT String m (List a)
semiSep1 p = p `sepBy1` semi

||| Parses /zero/ or more occurrences of `p` separated by `semi`.
semiSep : Monad m => ParserT String m a -> ParserT String m (List a)
semiSep p = p `sepBy` semi

||| Run some parser `p` until the second parser is encountered,
||| collecting a list of success for `p`, and the result of the second
||| parser is dropped.
|||
||| Primarily useful for collecting single line comments and other
||| similar verbatim environments.
manyUntil : Monad m => ParserT String m a
                    -> ParserT String m b
                    -> ParserT String m (List a)
manyUntil p end = ( end *> pure Nil ) <|> do { x <- p; xs <- manyUntil p end; pure ( x :: xs ) }

-- -------------------------------------------------------- [ Testing Function ]
testParser : Parser a -> String -> IO (Maybe a)
testParser p s = case parse p s of
  Left  e => putStrLn e *> pure Nothing
  Right x => pure (Just x)
-- --------------------------------------------------------------------- [ EOF ]


text:
module Language.LSP.Definition

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Data.List
import Data.String
import Data.String.Parser
import Data.URI
import Language.LSP.Message
import Server.Configuration
import Server.Log
import Server.Utils
import System.File

mkLocation : Ref Ctxt Defs
          => Ref LSPConf LSPConfiguration
          => String -> (Int, Int) -> (Int, Int) -> Core (Maybe Location)
mkLocation fname (sline, scol) (eline, ecol) = do
  Just (Just (Here path)) <- map rootPath <$> gets LSPConf initialized
    | _ => do
        logString Debug "gotoDefinition: Root path was not set."
        pure Nothing

  -- URIs can refer relative or absolute paths, also they can refer modules
  -- out of the current project.
  mSourceStr <-
    if path `isPrefixOf` fname
       then pure $ Just $ "file://" ++ fname
       else do
         let concatedName = path ++ "/" ++ fname
         if !(coreLift $ exists concatedName)
            then pure $ Just $ "file://" ++ concatedName
            else pure Nothing

  let Just sourceStr = mSourceStr
      | Nothing => do
          logString Debug "gotoDefinition: \{fname} referring module out of project."
          pure Nothing

  let Right (uri, _) = parse uriReferenceParser sourceStr
      | Left err => do
          logString Debug "gotoDefinition: URI parse error: \{err} \{show (sourceStr, sline, scol)}"
          pure Nothing

  pure $ Just $ MkLocation uri (MkRange (MkPosition sline scol) (MkPosition eline ecol))

export
gotoDefinition : Ref Ctxt Defs
              => Ref MD Metadata
              => Ref LSPConf LSPConfiguration
              => DefinitionParams -> Core (Maybe Location)
gotoDefinition params = do
  -- Check actual doc
  Just (actualUri, _) <- gets LSPConf openFile
    | Nothing => do
        logString Debug "gotoDefinition: openFile returned Nothing."
        pure Nothing
  let True = actualUri == params.textDocument.uri
      | False => do
          logString Debug "gotoDefinition: different URI than expected \{show (actualUri, params.textDocument.uri)}"
          pure Nothing

  let line = params.position.line
  let col  = params.position.character

  nameLocs <- gets MD nameLocMap
  let Just (_, name) = findPointInTreeLoc (line, col) nameLocs
    | Nothing => do
        logString Debug "gotoDefinition: Couldn't find a name at \{show (line, col)}"
        pure Nothing

  Nothing <- findTypeAt $ anyWithName name $ within (line, col)
    | Just _ => do
        logString Debug "gotoDefinition: \{show name} was a local name."
        pure Nothing

  Just globalDef <- lookupCtxtExact name !(gets Ctxt gamma)
    | Nothing => do
        logString Debug "gotoDefinition: \{show name} didn't have a GlobalDef."
        pure Nothing

  case globalDef.location of
    EmptyFC => do
      logString Debug "gotoDefinition: \{show name} didn't have location information."
      pure Nothing
    MkFC f s e => mkLocation f s e


text:
module Specdris.OutputTest

import Specdris.Spec
import Specdris.TestUtil

expected : List String
expected = ["\ESC[37m  context 1\ESC[0m",
            "\ESC[37m    context 1.1\ESC[0m",
            "\ESC[37m      + context 1.1.1\ESC[0m",
            "\ESC[31m         [x] not equal\n             actual:   1\n             expected: 2\ESC[0m",
            "\ESC[37m    + context 1.2\ESC[0m",
            "\ESC[31m       [x] not equal\n           actual:   1\n           expected: 2\ESC[0m",
            "\ESC[37m    + context 1.3\ESC[0m",
            "\ESC[33m       [] pending: for some reason\ESC[0m"]

testCase : IO ()
testCase
  = do state <- specWithState {storeOutput = True} $ do
             describe "context 1" $ do
               describe "context 1.1" $ do
                 it "context 1.1.1" $ do
                   1 === 2
               it "context 1.2" $ do
                 1 `shouldBe` 2
               it "context 1.3" $ do
                 pendingWith "for some reason"

       testAndPrint "spec output" (output state) (Just expected) (==)

export
specSuite : IO ()
specSuite = do putStrLn "\n  output:"
               testCase

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
||| Relationship between sum-types and the monoidal operation on wires
module SumWire

import Data.Vect
import ProcessLib
import Proto
import Primitives
import VertComp

%default total

-- TODO: move these to a util
pi1: (a,b,c) -> a
pi1 (x,y,z) = x
pi2: (a,b,c) -> b
pi2 (x,y,z) = y
pi3: (a,b,c) -> c
pi3 (x,y,z) = z

--------------------------------
--  Split Eithers
--------------------------------

normal: (msg : Req (MkNiche [Down (Either a b)] [Down a, Down b])) ->
        SubProc (MkNiche [Down (Either a b)] [Down a, Down b]) (ProcIF (MkNiche [Down (Either a b)] [Down a, Down b]) msg)
normal (Val (TopInWire Here) x) = Pure Accepted
normal (Conn _ _ _) = Pure Taken
normal (Val (TopInWire (There _)) _) impossible
normal (Val (BotInWire (There (There _))) _) impossible

forward : MessagePID (ProcIF niche_a) ->
          InWire niche_a a ->
          MessagePID (ProcIF niche_b) ->
          InWire niche_b b ->
          Maybe (Req (MkNiche [Down (Either a b)] [Down a, Down b])) ->
          Process (ProcIF (MkNiche [Down (Either a b)] [Down a, Down b]))
                  ()
                  Sent
                  Sent
forward pid_a tar_a pid_b tar_b Nothing = Pure ()
forward pid_a tar_a pid_b tar_b (Just (Conn _ _ _)) = Pure ()
forward pid_a tar_a pid_b tar_b (Just (Val (TopInWire Here) x)) = case x of
  Left l  => do { Request pid_a (Val tar_a l); Pure () }
  Right r => do { Request pid_b (Val tar_b r); Pure () }
forward pid_a tar_a pid_b tar_b (Just (Val (TopInWire (There _)) _))         impossible
forward pid_a tar_a pid_b tar_b (Just (Val (BotInWire (There (There _))) _)) impossible

initResp : Slot a ->
           Slot b ->
           (msg : Req (MkNiche [Down (Either a b)] [Down a, Down b])) ->
           ( SubProc (MkNiche [Down (Either a b)] [Down a, Down b])
                     (ProcIF (MkNiche [Down (Either a b)] [Down a, Down b]) msg)
           , Slot a
           , Slot b )
initResp EmptySlot slot_b    (Conn (BotOutWire Here) pid tar)         = ( Pure ConnAccepted, FullSlot pid tar, slot_b           )
initResp slot_a    EmptySlot (Conn (BotOutWire (There Here)) pid tar) = ( Pure ConnAccepted, slot_a          , FullSlot pid tar )
initResp slot_a    slot_b    (Conn (BotOutWire _) _   _  )            = ( Pure Taken       , slot_a          , slot_b           )
initResp slot_a    slot_b    (Val _ _)                                = ( Pure Error       , slot_a          , slot_b           )
initResp _         _         (Conn (BotOutWire (There (There _))) _ _) impossible
initResp _         _         (Conn (TopOutWire (There _)) _ _)         impossible

splitEither': Slot a -> Slot b -> Hom [Down (Either a b)] [Down a, Down b]
splitEither' sl1@(FullSlot pid_a tar_a) sl2@(FullSlot pid_b tar_b) = do
  r <- Respond normal
  forward pid_a tar_a pid_b tar_b r
  Loop $ splitEither' sl1 sl2
splitEither' {a} {b} slot_a slot_b = do
  Just msg <- Respond $ (\msg => pi1 (initResp slot_a slot_b msg)) | _ => Loop (splitEither' slot_a slot_b)
  Loop $ splitEither' (pi2 $ initResp slot_a slot_b msg) (pi3 $ initResp slot_a slot_b msg)

export splitEither: Hom [Down (Either a b)] [Down a, Down b]
splitEither = splitEither' EmptySlot EmptySlot

------------------------------
--  Join Eithers
------------------------------

respJ : (msg : Req (MkNiche [Down a, Down b] [Down (Either a b)])) ->
        ( SubProc (MkNiche [Down a, Down b] [Down (Either a b)])
                  (ProcIF (MkNiche [Down a, Down b] [Down (Either a b)]) msg)
        , Slot (Either a b) )
respJ (Conn (BotOutWire Here) pid tar) = ( Pure ConnAccepted, FullSlot pid tar )
respJ (Val inWire x)                   = ( Pure Error       , EmptySlot        )
respJ (Conn (BotOutWire (There Here)) _ _)      impossible
respJ (Conn (BotOutWire (There (There _))) _ _) impossible
respJ (Conn (TopOutWire (There (There _))) _ _) impossible

normalJ: MessagePID (ProcIF niche) ->
         InWire niche (Either a b) ->
         (msg : Req (MkNiche [Down a, Down b] [Down (Either a b)])) ->
         ( ProcIF (MkNiche [Down a, Down b] [Down (Either a b)]) msg
         , Process (ProcIF (MkNiche [Down a, Down b] [Down (Either a b)])) () Sent Sent )
normalJ pid tar (Conn _ _ _)                          = ( Taken   , Pure ()                                         )
normalJ pid tar (Val (TopInWire Here) x)              = ( Accepted, do { Request pid (Val tar (Left  x)); Pure () } )
normalJ pid tar (Val (TopInWire (There Here)) x)      = ( Accepted, do { Request pid (Val tar (Right x)); Pure () } )
normalJ pid tar (Val (TopInWire (There (There _))) _) impossible
normalJ pid tar (Val (BotInWire (There _)) _)         impossible

joinEither': Slot (Either a b) -> Hom [Down a, Down b] [Down (Either a b)]
joinEither' slot@(FullSlot pid tar) = do Just msg <- Respond (\msg => Pure $ fst $ normalJ pid tar msg) | _ => Loop (joinEither' slot)
                                         snd $ normalJ pid tar msg
                                         Loop (joinEither' slot)
joinEither' EmptySlot = do Just msg <- Respond (\msg => fst (respJ msg)) | _ => Loop (joinEither' EmptySlot)
                           Loop $ joinEither' $ snd (respJ msg)

export joinEither: Hom [Down a, Down b] [Down (Either a b)]
joinEither = joinEither' EmptySlot

-----------------------------------
--  Symetric monoidal structure
-----------------------------------

-- we get this for free by using {join,split}Either, but would be better to make a primitive

symEither: Either a b -> Either b a
symEither (Left x)  = Right x
symEither (Right x) = Left x

export partial sym: (Show a, Show b) => Hom [Down a, Down b] [Down b, Down a]
sym = joinEither -*- (mkPure "sym: " symEither) -*- splitEither

--------------------------------------
--  Splicing
--------------------------------------

spliceEither: Either a a -> a
spliceEither (Left x)  = x
spliceEither (Right x) = x

export partial splice: Show a => Hom [Down a, Down a] [Down a]
splice = joinEither -*- (mkPure "splice: " spliceEither)

max_stars_repo_name: jameshaydon/smproc

max_issues_repo_name: jameshaydon/smproc

max_forks_repo_name: jameshaydon/smproc


text:
module Replica.Core.Parse

import Replica.Core.Types
import Replica.Other.Validation

import Data.List
import Language.JSON

%default total

allString : List JSON -> Validation (List String) (List String)
allString =  traverse \j => case j of
  JString str => Valid str
  _ => Error ["Invalid expectation part: \{show j}"]

validatePending : Maybe JSON -> Validation (List String) Bool
validatePending Nothing = Valid False
validatePending (Just (JBoolean x)) = Valid x
validatePending x = Error ["Pending must be a boolean, found: \{show x}"]

validateDesc : Maybe JSON -> Validation (List String) (Maybe String)
validateDesc Nothing = Valid empty
validateDesc (Just JNull) = Valid empty
validateDesc (Just (JString x)) = Valid $ Just $ x
validateDesc (Just x)
  = Error ["Test description should be a string, found: \{show x}"]

validateRequire : JSON -> Validation (List String) String
validateRequire (JString x) = Valid x
validateRequire x = Error ["A requirement must be a testname, found: \{show x}"]

validatOrderSensitive : Maybe JSON -> Validation (List String) OrderSensitive
validatOrderSensitive Nothing = Valid Ordered
validatOrderSensitive (Just (JBoolean x)) = Valid $ if x then Ordered else Whatever
validatOrderSensitive (Just x) = Error
  ["OrderSensitive must be a boolean, found \{show x}"]

validateExpectation : Maybe JSON -> Validation (List String) Expectation
validateExpectation Nothing = Valid Generated
validateExpectation (Just (JString x)) = Valid (Exact x)
validateExpectation (Just (JArray xs)) = Partial Ordered <$> allString xs
validateExpectation (Just (JObject o)) =
  let Just (JArray parts) = lookup "parts" o
      | other => Error $ maybe ["missing parts"] (const ["invalid parts"]) other
  in [| Partial
     (validatOrderSensitive $ lookup "ordered" o)
     (allString parts)
     |]
validateExpectation x = Error ["An expectation must be an expectation, found: \{show x}"]

validateRequireList : Maybe JSON -> Validation (List String) (List String)
validateRequireList Nothing = Valid empty
validateRequireList (Just JNull) = Valid empty
validateRequireList (Just (JString x)) = Valid $ pure x
validateRequireList (Just (JArray ys)) = traverse validateRequire ys
validateRequireList (Just x) = Error
  ["Require must contain a test name or an array of test names, found \{show x}"]

validateWD : Maybe JSON -> Validation (List String) (Maybe String)
validateWD Nothing = Valid empty
validateWD (Just JNull) = Valid empty
validateWD (Just (JString x)) = Valid $ Just $ x
validateWD (Just x)
  = Error ["Test working directory should be a string, found: \{show x}"]

validateTag : JSON -> Validation (List String) String
validateTag (JString x) = Valid x
validateTag x = Error ["A tag must be a string, found: \{show x}"]

validateTagList : Maybe JSON -> Validation (List String) (List String)
validateTagList Nothing = Valid empty
validateTagList (Just JNull) = Valid empty
validateTagList (Just (JString x)) = Valid $ pure x
validateTagList (Just (JArray ys)) = traverse validateTag ys
validateTagList (Just x) = Error
  ["Tags must contain a tag (string) or an array of tags, found \{show x}"]

validateCommandItem : JSON -> Validation (List String) String
validateCommandItem (JString x) = Valid x
validateCommandItem x = Error ["An item must be a string, found \{show x}"]

validateCommandList : (commandName : String) -> Maybe JSON -> Validation (List String) (List String)
validateCommandList _ Nothing = Valid empty
validateCommandList _ (Just JNull) = Valid empty
validateCommandList _ (Just (JString x)) = Valid $ pure x
validateCommandList _ (Just (JArray ys)) = traverse validateCommandItem ys
validateCommandList cmd (Just x) = Error
  ["\{cmd} must contain a command (string) or an array of commands, found \{show x}"]

validateBefore : Maybe JSON -> Validation (List String) (List String)
validateBefore = validateCommandList "beforeTest"

validateAfter : Maybe JSON -> Validation (List String) (List String)
validateAfter = validateCommandList "afterTest"

validateCommand : Maybe JSON -> Validation (List String) String
validateCommand (Just (JString str)) = Valid str
validateCommand Nothing = Error ["command is missing"]
validateCommand (Just x) = Error ["Command must be a string, found \{show x}"]

validateInput : JSON -> Validation (List String) String
validateInput (JString str) = Valid str
validateInput x = Error ["input must be a string, found \{show x}"]

validateStatus : Maybe JSON -> Validation (List String) (Maybe Bool)
validateStatus Nothing = Valid empty
validateStatus (Just JNull) = Valid empty
validateStatus (Just (JBoolean x)) = Valid $ Just x
validateStatus (Just x) = Error ["Status should be a boolean, found: \{show x}"]

validateSpaceSensitive : Maybe JSON -> Validation (List String) Bool
validateSpaceSensitive Nothing = Valid True
validateSpaceSensitive (Just (JBoolean x)) = Valid x
validateSpaceSensitive x = Error ["Pending must be a boolean, found: \{show x}"]

isString : JSON -> Validation (List String) String
isString (JString str) = Valid str
isString x = Error ["oututFiles content should be a list of string, found: \{show x}"]

validateFile : Maybe JSON -> Validation (List String) (Maybe String)
validateFile Nothing = Valid empty
validateFile (Just json) = Just <$> isString json

jsonToTest : String -> JSON -> Validation (List String) Test
jsonToTest str (JObject xs) =
  [| MkTest
  (pure str)
  (validatePending $ lookup "pending" xs)
  (validateDesc $ lookup "description" xs)
  (validateRequireList $ lookup "require" xs)
  (validateWD $ lookup "workingDir" xs)
  (validateTagList $ lookup "tags" xs)
  (validateBefore $ lookup "beforeTest" xs)
  (validateAfter $ lookup "afterTest" xs)
  (validateCommand $ lookup "command" xs)
  (traverse validateInput $ lookup "input" xs)
  (validateStatus $ lookup "succeed" xs)
  (validateSpaceSensitive $ lookup "spaceSensitive" xs)
  (validateExpectation $ lookup "expectation" xs)
  (validateFile $ lookup "outputFile" xs)
  |]
jsonToTest str json =
  Error ["Expecting a JSON object for test '\{str}' and got: \{show json}"]

export
jsonToReplica : JSON -> Validation (List String) Replica
jsonToReplica (JObject xs) = [| MkReplica $ traverse (uncurry jsonToTest) xs |]
jsonToReplica _ = Error ["Replica test file must be a JSON object"]

parseMissingGolden : Maybe String -> List (String, JSON) -> Maybe FailReason
parseMissingGolden src xs = do
  JString "Missing" <- lookup "reason" xs
    | _ => Nothing
  JString given <- lookup "given" xs
    | _ => Nothing
  pure $ WrongOutput src $ GoldenIsMissing given

parseWrongOutput : Maybe String -> List (String, JSON) -> Lazy (Maybe FailReason)
parseWrongOutput src xs = do
  JString exp <- lookup "expected" xs
    | _ => Nothing
  JString given <- lookup "given" xs
    | _ => Nothing
  pure $ WrongOutput src $ DifferentOutput exp given

parsePartialOutputMsimatch : Maybe String -> List (String, JSON) -> Maybe FailReason
parsePartialOutputMsimatch src xs = do
  JBoolean o<- lookup "ordered" xs
    | _ => Nothing
  JArray missing <- lookup "missingParts" xs
    | _ => Nothing
  let Just m = the (Maybe (List String)) $ traverse go missing
    | _ => Nothing
  JString given <- lookup "given" xs
    | _ => Nothing
  pure $ WrongOutput src $ PartialOutputMismatch (if o then Ordered else Whatever) m given
  where
    go : JSON -> Maybe String
    go (JString str) = Just str
    go _ = Nothing

parseWrongStatus : List (String, JSON) -> Maybe FailReason
parseWrongStatus xs = do
  JBoolean exp <- lookup "expected" xs
    | _ => Nothing
  pure $ WrongStatus exp

parseExpectedNotFound : List (String, JSON) -> Maybe FailReason
parseExpectedNotFound xs = do
  JString exp <- lookup "expected" xs
    | _ => Nothing
  pure $ ExpectedFileNotFound exp

parseFailReason : JSON -> Validation (List String) FailReason
parseFailReason (JObject xs) = do
  let Just src = case lookup "file" xs of
                 Nothing => Just Nothing
                 Just (JString str) => Just $ Just str
                 _ => Nothing
    | _ => Error ["Unexpected file value"]
  case lookup "type" xs of
    Just (JString "output") => maybe
      (Error ["Invalid Wrong output content"])
      Valid
      (parseMissingGolden src xs <|> parseWrongOutput src xs <|> parsePartialOutputMsimatch src xs)
    Just (JString "status") => maybe
      (Error ["Invalid Wrong output content"])
      Valid
      (parseWrongStatus xs)
    Just (JString "missing") => maybe
      (Error ["Invalid Wrong expected file not found content"])
      Valid
      (parseExpectedNotFound xs)
    pat => Error ["Invalid object content for a fail reason: \{show xs}"]
parseFailReason json =
  Error ["Expecting a JSON object for a fail reason, got: \{show json}"]

parseTestResult : JSON -> Validation (List String) TestResult
parseTestResult (JObject [("Fail", JArray cause)]) = map Fail $ traverse parseFailReason cause
parseTestResult (JString "Success") = Valid Success
parseTestResult (JString "Scekipped") = Valid Skipped
parseTestResult x = Error ["\{show x} can't be a valid result"]

parseTestError : JSON -> Validation (List String) TestError
parseTestError (JObject json) = case lookup "type" json of
  Just (JString "FileSystemError") => map
    FileSystemError
    $ case lookup "content" json of
           Just (JString str) => Valid str
           _ => Error ["No content found for a FileSystemError"]
  Just (JString "InitializationFailed") => map
    InitializationFailed
    $ case lookup "content" json of
           Just (JString str) => Valid str
           _ => Error ["No content found for a InitializationFailed"]
  Just (JString "RequirementsFailed") => map
    RequirementsFailed
    $ case lookup "content" json of
           Just (JString str) => Valid str
           _ => Error ["No content found for a RequirementsFailed"]
  Just (JString "WrapUpFailed") => map
    (uncurry WrapUpFailed)
    $ case (lookup "result" json, lookup "content" json) of
           (Just result, Just (JString content)) => map (flip MkPair content) $ parseTestResult result
           _ => Error ["No result and/or content found for a WrapUpFailed"]
  pat => Error ["Can't pares TestError content"]
parseTestError json =
  Error ["Expecting a JSON object for a test error and got: \{show json}"]

parseResult : JSON -> Validation (List String) (Either TestError TestResult)
parseResult (JObject [("Error", cause)]) = map Left $ parseTestError cause
parseResult (JObject [("Fail", JArray cause)]) = map (Right . Fail) $ traverse parseFailReason cause
parseResult (JString "Success") = Valid $ Right Success
parseResult x = Error ["\{show x} can't be a valid result"]

export
parseReport : JSON -> Validation (List String) (List (String, Either TestError TestResult))
parseReport (JObject xs) = traverse (\(str, res) => map (MkPair str) (parseResult res)) xs
parseReport x = Error ["A report must be an object. Found : \{show x}"]

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
||| This module presents the Xilinx LocalLink protocol encoded within
||| out abstract interfact description language.
module Example.Specification.LocalLink

import Text.Markup.Edda
import Text.Markup.Edda.Org

import Cordial.EDSL.Specification

%access public export
%default total

||| Concrete labels for port descriptions.
data LLRTy = CLOCK | RESET | DATA | SRC_RDY | DST_RDY | SOF | EOF
           | SOP | EOP
           | REM | REM_SOF | REM_SOP | REM_EOP
           | SRC_DSC | DST_DSC
           | CH | CH_RDY | CH_SWAP
           | PARITY | PARITY_ERR

||| Equality type is required to differentiate labels.
Eq LLRTy where
  (==) CLOCK      CLOCK      = True
  (==) RESET      RESET      = True
  (==) DATA       DATA       = True
  (==) SRC_RDY    SRC_RDY    = True
  (==) DST_RDY    DST_RDY    = True
  (==) SOF        SOF        = True
  (==) EOF        EOF        = True
  (==) SOP        SOP        = True
  (==) EOP        EOP        = True
  (==) REM        REM        = True
  (==) REM_SOF    REM_SOF    = True
  (==) REM_SOP    REM_SOP    = True
  (==) REM_EOP    REM_EOP    = True
  (==) SRC_DSC    SRC_DSC    = True
  (==) DST_DSC    DST_DSC    = True
  (==) CH         CH         = True
  (==) CH_RDY     CH_RDY     = True
  (==) CH_SWAP    CH_SWAP    = True
  (==) PARITY     PARITY     = True
  (==) PARITY_ERR PARITY_ERR = True
  (==) _          _          = False

||| ENcodes the remainder kind.
data TyRemainder = ENCODED | MASK

||| This function represents the 'generic' specification for the
||| LocalLink protocol.
|||
||| We diverge from the formal specification presented by embracing
||| Cordial's EDSL nature to allow more value dependencies than
||| presented in the paper.
|||
||| *Note* For several busses it is not clear what the width should
||| be. This is a result of calculations resulting in an array of $1 -
||| 1$ length, coupled with loose specification, or widths that
||| require floating point arithemetic.  The latter is something that
||| the formalism does not support natively w.r.t. Widths.
|||
||| We have left those widths 'undefined'.
|||
||| @dWidth The width of the data bus must be one of [32,16,8].
||| @noChans The number of channels supported.
||| @rTy     The kind of remainder.
LocalLink_Gen : (dWidth, noChans : Nat)
             -> (rTy  : TyRemainder)
             -> (prfD : ValidArraySpec dWidth [32,16,8])
             -> (prfC : GTE noChans 1)
             -> IDL LLRTy
LocalLink_Gen dWidth noChans rTy prfD prfC = do
  setVendor "XILINX"
  setLibrary "examples"
  setName ("LocalLink")
  setVersion "0.1"
  setCommunicationStyle Unicast

  c                 <- label CLOCK
  r                 <- label RESET
  d                 <- label DATA
  rdy_src           <- label SRC_RDY
  rdy_dst           <- label DST_RDY
  frame_start       <- label SOF
  frame_end         <- label EOF
  payload_start     <- label SOP
  payload_end       <- label EOP
  rem               <- label REM
  rem_frame_start   <- label REM_SOF
  rem_payload_start <- label REM_SOP
  rem_payload_end   <- label REM_EOP
  disco_src         <- label SRC_DSC
  disco_dst         <- label DST_DSC
  chan              <- label CH
  chan_rdy          <- label CH_RDY
  chan_swp          <- label CH_SWAP
  parity            <- label PARITY
  perr              <- label PARITY_ERR

  clock c Nothing Nothing Nothing
    # fromTargetAlways
    # system "sys"

  reset r
    # fromTargetAlways
    # system "sys"
    # setSensitivity Low

  bus d (fromNat dWidth prfD)
  control rdy_src # setSensitivity Low
  control rdy_dst # setSensitivity Low # fromTarget

  control frame_start # opt # setSensitivity Low
  control frame_end   # opt # setSensitivity Low

  control payload_start # opt
  control payload_end   # opt

  let d_dbl = cast {to=Double} dWidth
  let remsize = case rTy of
      ENCODED => calcBits d_dbl
      MASK    => (d_dbl / 8) - 1

  let p_width = FromDouble.fromDouble remsize

  bus rem               # opt
  bus rem_frame_start   # opt
  bus rem_payload_start # opt
  bus rem_payload_end   # opt
  -- Ideally specify bus with width p_width but no proof that `p_wdith >= 2`

  -- [ NOTE]

  control disco_src              # opt
  control disco_dst # fromTarget # opt

  control perr
    # opt
    # fromTarget
    # setSensitivity Low

  let paritysize = assert_total $ minus (div dWidth 8) 1
  -- nat division is not total

  bus parity # opt
  -- Ideally specify bus with width paritysize but no proof that `paritysize >= 2`

  let csize = calcBits (cast {to=Double} noChans)

  bus chan # opt
    -- Ideally specify bus with width csize but no proof that `csize >= 2`

  bus chan_rdy  # opt # setSensitivity Low
  bus chan_swp  # opt
  -- Ideally specify bus with a bus width of noChans but no proof that `noChans >= 2` must hold.
  stop

||| Transform the specification into a model.
LocalLink : (dWidth, noChans : Nat)
         -> (rTy : TyRemainder)
         -> {auto prfD : ValidArraySpec dWidth [32,16,8]}
         -> {auto prfC : GTE noChans 1}
         -> InterfaceTy () LLRTy
LocalLink d c r {prfD} {prfC} =
  buildSpec (LocalLink_Gen d c r prfD prfC)

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

max_stars_repo_name: border-patrol/cordial

max_issues_repo_name: border-patrol/cordial

max_forks_repo_name: border-patrol/cordial


text:
module Prelude.Cast

import Builtin
import Prelude.Basics
import Prelude.Num
import Prelude.Types

%default total

-----------
-- CASTS --
-----------

-- Casts between primitives only here.  They might be lossy.

||| Interface for transforming an instance of a data type to another type.
public export
interface Cast from to where
  constructor MkCast
  ||| Perform a (potentially lossy!) cast operation.
  ||| @ orig The original type
  cast : (orig : from) -> to

export
Cast a a where
  cast = id

-- To String

export
Cast Int String where
  cast = prim__cast_IntString

export
Cast Integer String where
  cast = prim__cast_IntegerString

export
Cast Char String where
  cast = prim__cast_CharString

export
Cast Double String where
  cast = prim__cast_DoubleString

-- To Integer

export
Cast Int Integer where
  cast = prim__cast_IntInteger

export
Cast Char Integer where
  cast = prim__cast_CharInteger

export
Cast Double Integer where
  cast = prim__cast_DoubleInteger

export
Cast String Integer where
  cast = prim__cast_StringInteger

export
Cast Nat Integer where
  cast = natToInteger

export
Cast Bits8 Integer where
  cast = prim__cast_Bits8Integer

export
Cast Bits16 Integer where
  cast = prim__cast_Bits16Integer

export
Cast Bits32 Integer where
  cast = prim__cast_Bits32Integer

export
Cast Bits64 Integer where
  cast = prim__cast_Bits64Integer

-- To Int

export
Cast Integer Int where
  cast = prim__cast_IntegerInt

export
Cast Char Int where
  cast = prim__cast_CharInt

export
Cast Double Int where
  cast = prim__cast_DoubleInt

export
Cast String Int where
  cast = prim__cast_StringInt

export
Cast Nat Int where
  cast = fromInteger . natToInteger

export
Cast Bits8 Int where
  cast = prim__cast_Bits8Int

export
Cast Bits16 Int where
  cast = prim__cast_Bits16Int

export
Cast Bits32 Int where
  cast = prim__cast_Bits32Int

export
Cast Bits64 Int where
  cast = prim__cast_Bits64Int

-- To Char

export
Cast Int Char where
  cast = prim__cast_IntChar

-- To Double

export
Cast Int Double where
  cast = prim__cast_IntDouble

export
Cast Integer Double where
  cast = prim__cast_IntegerDouble

export
Cast String Double where
  cast = prim__cast_StringDouble

export
Cast Nat Double where
  cast = prim__cast_IntegerDouble . natToInteger

-- To Bits8

export
Cast Int Bits8 where
  cast = prim__cast_IntBits8

export
Cast Integer Bits8 where
  cast = prim__cast_IntegerBits8

export
Cast Bits16 Bits8 where
  cast = prim__cast_Bits16Bits8

export
Cast Bits32 Bits8 where
  cast = prim__cast_Bits32Bits8

export
Cast Bits64 Bits8 where
  cast = prim__cast_Bits64Bits8

-- To Bits16

export
Cast Int Bits16 where
  cast = prim__cast_IntBits16

export
Cast Integer Bits16 where
  cast = prim__cast_IntegerBits16

export
Cast Bits8 Bits16 where
  cast = prim__cast_Bits8Bits16

export
Cast Bits32 Bits16 where
  cast = prim__cast_Bits32Bits16

export
Cast Bits64 Bits16 where
  cast = prim__cast_Bits64Bits16

-- To Bits32

export
Cast Int Bits32 where
  cast = prim__cast_IntBits32

export
Cast Integer Bits32 where
  cast = prim__cast_IntegerBits32

export
Cast Bits8 Bits32 where
  cast = prim__cast_Bits8Bits32

export
Cast Bits16 Bits32 where
  cast = prim__cast_Bits16Bits32

export
Cast Bits64 Bits32 where
  cast = prim__cast_Bits64Bits32

-- To Bits64

export
Cast Int Bits64 where
  cast = prim__cast_IntBits64

export
Cast Integer Bits64 where
  cast = prim__cast_IntegerBits64

export
Cast Bits8 Bits64 where
  cast = prim__cast_Bits8Bits64

export
Cast Bits16 Bits64 where
  cast = prim__cast_Bits16Bits64

export
Cast Bits32 Bits64 where
  cast = prim__cast_Bits32Bits64

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Main

import ContriverText.Tests

main : JS_IO ()
main = do
  testMain {f=FFI_JS}
  runJsTests

max_stars_repo_name: rocketnia/contrivertext

max_issues_repo_name: rocketnia/contrivertext

max_forks_repo_name: rocketnia/contrivertext


text:
module PLFI.Part1.Negation

import Control.Function.FunExt
import Data.DPair

import PLFI.Part1.Relations
import PLFI.Part1.Naturals

-- ¬_ : Set → Set
-- ¬ A = A → ⊥

%default total

%hide Prelude.Not

Not : Type -> Type
Not a = a -> Void

-- ¬-elim : ∀ {A : Set}
--   → ¬ A
--   → A
--     ---
--   → ⊥
-- ¬-elim ¬x x = ¬x x

notElim : (Not a) -> a -> Void
notElim = ($)
-- notElim not_x x = not_x $ x
-- notElim not_x x = not_x x

-- ¬¬-intro : ∀ {A : Set}
--   → A
--     -----
--   → ¬ ¬ A
-- ¬¬-intro x  =  λ{¬x → ¬x x}

notNotIntro : a -> (Not (Not a))
notNotIntro = flip ($)
-- notNotIntro x = \notX => notX x
-- notNotIntro x notX = notX x

-- ¬¬¬-elim : ∀ {A : Set}
--   → ¬ ¬ ¬ A
--     -------
--   → ¬ A
-- ¬¬¬-elim ¬¬¬x  =  λ x → ¬¬¬x (¬¬-intro x)

notNotNotElim : (Not (Not (Not a))) -> Not a
notNotNotElim = flip (.) notNotIntro
-- notNotNotElim nnnx = nnnx . notNotIntro
-- notNotNotElim nnnx x = nnnx (notNotIntro x) -- (\f => f x)

nnnnElim : (Not (Not (Not (Not a)))) -> (Not (Not a))
nnnnElim = notNotNotElim

-- contraposition : ∀ {A B : Set}
--   → (A → B)
--     -----------
--   → (¬ B → ¬ A)
-- contraposition f ¬y x = ¬y (f x)

contraposition : (a -> b) -> (Not b -> Not a)
contraposition = flip (.)
-- contraposition f ny = ny (f x)

-- _≢_ : ∀ {A : Set} → A → A → Set
-- x ≢ y  =  ¬ (x ≡ y)

-- inequality
-- unequality
Neq : a -> a -> Type
Neq x y = Not (x === y)
-- Neq = (Not .) . (===)

-- _ : 1 ≢ 2
-- _ = λ()

-- PLFI.Part1.Negation.h1 : 1 = 2 -> Void
ex1 : Neq (S Z) (S (S Z))
-- ex1 = ?h1 -- x impossible
-- ex1 Refl impossible
ex1 x impossible

-- PLFI.Part1.Negation.h2 : () = Nat -> Void
ex2 : Neq Unit Nat
-- ex2 = ?h2 -- Refl impossible -- wat?
ex2 Refl impossible
-- ex2 x impossible -- ex2 x is not a valid impossible case.

Neq2 : a -> b -> Type
Neq2 x y = Not (x ~=~ y)

-- PLFI.Part1.Negation.h3 : () = 0 -> Void
ex3 : Neq2 Unit Z
ex3 x impossible

-- peano : ∀ {m : ℕ} → zero ≢ suc m
-- peano = λ()

peano : {m : Nat} -> Neq Z (S m)
peano Refl impossible

-- id : ⊥ → ⊥
-- id x = x
--
-- id′ : ⊥ → ⊥
-- id′ ()

id1 : Void -> Void
id1 x = x

id2 : Void -> Void
id2 x impossible

0
id1_id2 : FunExt => Negation.id1 === Negation.id2
-- id1_id2 = funExt (\x => case x of {})
id1_id2 = funExt (\x => absurd x)
-- id1_id2 = funExt absurd

0
h : FunExt => (f : Void -> a) -> (g : Void -> a) -> f === g
h f g = funExt (\x => absurd x)

-- assimilation : ∀ {A : Set} (¬x ¬x′ : ¬ A) → ¬x ≡ ¬x′
-- assimilation ¬x ¬x′ = extensionality (λ x → ⊥-elim (¬x x))

0
assimilation : FunExt => (f, g : Not a) -> f === g
assimilation f g = funExt (\x => absurd (g x))

-- <-irreflexive
-- Using negation, show that strict inequality is irreflexive, that is, n < n holds for no n.

total
ltIrreflexive0 : (n : N) -> Not (n < n)
ltIrreflexive0 (Suc _) (SucLT x) = ltIrreflexive0 _ x

ltIrreflexive1 : (n : N) -> Not (n < n)
ltIrreflexive1 Zero    ZeroLT    impossible
ltIrreflexive1 Zero    (SucLT x) impossible
ltIrreflexive1 (Suc m) (SucLT x) = ltIrreflexive1 m x

-- Exercise trichotomy (practice)
-- Show that strict inequality satisfies trichotomy, that is, for any naturals m and n exactly one of the following holds:

data Trichotomy : N -> N -> Type where
  LT : m < n -> Trichotomy m n
  EQ : m = n -> Trichotomy m n
  GT : n < m -> Trichotomy m n

uniquenessOfEq : {a : Type} -> (n,m : a) -> (x,y : n === m) -> x === y
uniquenessOfEq n n Refl Refl = Refl

uniquenessOfLT : (n,m : N) -> (x,y : n < m) -> x === y
uniquenessOfLT Zero    (Suc n) ZeroLT    ZeroLT    = Refl
uniquenessOfLT (Suc m) (Suc n) (SucLT x) (SucLT y) = cong SucLT (uniquenessOfLT m n x y)

lessNotEqualLemma : (m < n) -> (m = n) -> Void
lessNotEqualLemma ZeroLT    Refl impossible
lessNotEqualLemma (SucLT x) Refl = lessNotEqualLemma x Refl

lessNotGreaterLemma : (m < n) -> (n < m) -> Void
lessNotGreaterLemma ZeroLT    ZeroLT    impossible
lessNotGreaterLemma ZeroLT    (SucLT x) impossible
lessNotGreaterLemma (SucLT x) (SucLT y) = lessNotGreaterLemma x y

trichotomy : (m, n : N) -> (t1, t2 : Trichotomy m n) -> t1 === t2
trichotomy m n (LT x) (LT y) = cong LT (uniquenessOfLT m n x y)
trichotomy m n (LT x) (EQ p) = absurd (lessNotEqualLemma x p)
trichotomy m n (LT x) (GT y) = absurd (lessNotGreaterLemma x y)
trichotomy m n (EQ p) (LT x) = absurd (lessNotEqualLemma x p)
trichotomy m n (EQ p) (EQ q) = cong EQ (uniquenessOfEq m n p q)
trichotomy m n (EQ p) (GT x) = absurd (lessNotEqualLemma x (sym p))
trichotomy m n (GT x) (LT y) = absurd (lessNotGreaterLemma x y)
trichotomy m n (GT x) (EQ p) = absurd (lessNotEqualLemma x (sym p))
trichotomy m n (GT x) (GT y) = cong GT (uniquenessOfLT n m x y)

data Trichotomy1 : N -> N -> Type where
  LT1 :      (m < n)  -> (Not (m = n)) -> (Not (n < m)) -> Trichotomy1 m n
  EQ1 : (Not (m < n)) ->      (m = n)  -> (Not (n < m)) -> Trichotomy1 m n
  GT1 : (Not (n < m)) -> (Not (m = n)) ->      (n < m)  -> Trichotomy1 m n

lemma1 : (n < m) -> (Not (n = m), Not (m < n))
lemma2 : (m = n) -> (Not (n < m), Not (m < n))

max_stars_repo_name: andorp/PLFI

max_issues_repo_name: andorp/PLFI

max_forks_repo_name: andorp/PLFI


text:
module System.File.Process

import public System.File.Error
import public System.File.Mode
import System.File.Support
import public System.File.Types
import System.FFI

fileClass : String
fileClass = "io/github/mmhelloworld/idrisjvm/runtime/ChannelIo"

%foreign "C:fflush,libc 6"
         jvm' fileClass "flush" fileClass "int"
prim__flush : FilePtr -> PrimIO Int
%foreign support "idris2_popen"
         jvm' fileClass "popen" "String String" fileClass
prim__popen : String -> String -> PrimIO FilePtr
%foreign support "idris2_pclose"
         jvm' fileClass "close" fileClass "void"
prim__pclose : FilePtr -> PrimIO ()

export
fflush : HasIO io => (h : File) -> io ()
fflush (FHandle f)
    = ignore $ primIO (prim__flush f)

export
popen : HasIO io => String -> Mode -> io (Either FileError File)
popen f m = do
    ptr <- primIO (prim__popen f (modeStr m))
    if prim__nullAnyPtr ptr /= 0
        then returnError
        else pure (Right (FHandle ptr))

export
pclose : HasIO io => File -> io ()
pclose (FHandle h) = primIO (prim__pclose h)