text:
module Idrlisp

import CIO
import Data.SortedMap
import public Idrlisp.Value
import Idrlisp.Parser
import Idrlisp.Env
import Idrlisp.Syntax

%default covering

export
parseExpr : String -> Either String Value
parseExpr = Parser.parseToEnd

export
parseProgram : String -> Either String (List Value)
parseProgram = Parser.parseToEnd

export
newContext : List (String, Builtin) -> IO Context
newContext builtins =
  do
    env <- Env.new Nothing
    traverse_ (uncurry (install env)) Syntax.syntaxList
    pure $ MkContext env (fromList builtins)
  where
    install : Env Value -> String -> Syntax -> IO ()
    install env name syn = Env.define name (Pure (NSyntax syn)) env

export
runCompile : Context -> Compile a -> CIO String (a, Code Value)
runCompile ctx = run
  where
    run : Compile a -> CIO String (a, Code Value)
    run (Do inst) = pure ((), singleton inst)
    run (Refer sym) = do
      value <- lift $ Env.lookup sym (topLevel ctx)
      pure (eitherToMaybe value, empty)
    run (Block x) = do
      (_, code) <- run x
      pure (code, empty)
    run (Pure x) = pure (x, empty)
    run (Bind x f) = do
      (a, code) <- run x
      (b, code') <- run (f a)
      pure (b, code ++ code')
    run (Fail x) = throw x

export
runVM : Context -> VM a -> Cont -> CIO String (a, Cont)
runVM ctx = run
  where
    run : VM a -> Cont -> CIO String (a, Cont)
    run (Push value) cont = pure ((), record { stack $= (value ::) } cont)
    run Pop cont =
      case stack cont of
        x :: xs => pure (Just x, record { stack = xs } cont)
        _ => pure (Nothing, cont)
    run (Get name) cont = do
      value <- lift $ Env.lookup name (env cont)
      pure (value, cont)
    run (Define name value) cont = do
      r <- lift $ Env.define name value (env cont)
      pure (Right r, cont)
    run (Set name value) cont = do
      r <- lift $ Env.set name value (env cont)
      pure (r, cont)
    run CaptureEnv cont = pure (env cont, cont)
    run Next cont =
      case next (code cont) of
        Just (x, xs) => pure (Just x, record { code = xs } cont)
        Nothing => pure (Nothing, cont)
    run (Enter nenv ncode) (MkCont stack env code dump) = do
      nenv <- lift $ Env.new $ Just nenv
      if tailPosition code
         then pure ((), MkCont stack nenv ncode dump)
         else pure ((), MkCont stack nenv ncode ((env, code) :: dump))
    run Leave cont@(MkCont stack env code dump) =
      case dump of
        [] => pure (Left (), cont)
        (penv, pcode) :: rest => pure (Right (env, code), MkCont stack penv pcode rest)
    run DropCont cont = pure ((), MkCont [] (env cont) (singleton Leave) [])
    run (RestoreCont cont) _ = pure ((), cont)
    run CaptureCont cont = pure (cont, cont)
    run CaptureContext cont = pure (ctx, cont)
    run (LoadBuiltin name) cont = pure (lookup name (builtins ctx), cont)
    run (Action action) cont = pure (!(lift action), cont)
    run (Pure x) cont = pure (x, cont)
    run (Bind x f) cont = do
      (x, cont) <- run x cont
      run (f x) cont
    run (Fail err) cont = throw err

export
runMacroExpand : Context -> MacroExpand a -> CIO String a
runMacroExpand ctx = run
  where
    run : MacroExpand a -> CIO String a
    run (Refer sym) = do
      value <- lift $ Env.lookup sym (topLevel ctx)
      pure $ eitherToMaybe value
    run (Execute op) = fst <$> runVM ctx op (MkCont [] (topLevel ctx) empty [])
    run (Pure x) = pure x
    run (Bind x f) = do
      x <- run x
      run (f x)
    run (Fail err) = throw err

export
compileExpr : Context -> Value -> IO (Either String (Code Value))
compileExpr ctx expr = runCIO $ snd <$> runCompile ctx (load expr)

export
macroExpandExpr : Context -> Bool -> Value -> IO (Either String Value)
macroExpandExpr ctx recurse expr = runCIO $ runMacroExpand ctx (expand recurse expr)

export
execCode : Context -> Env Value -> Code Value -> IO (Either String Value)
execCode ctx env code = runCIO $ fst <$> runVM ctx instCycle (MkCont [] env code [])

export
evalExpr : Context -> Value -> IO (Either String Value)
evalExpr ctx expr = runCIO $ do
  expr <- runMacroExpand ctx (expand True expr)
  (_, code) <- runCompile ctx (load expr)
  (r, _) <- runVM ctx instCycle (MkCont [] (topLevel ctx) code [])
  pure r

export
evalProgram : Context -> List Value -> IO (Either (Nat, String) Value)
evalProgram ctx = go 0 Nil
  where
    go : Nat -> Value -> List Value -> IO (Either (Nat, String) Value)
    go index last [] = pure $ Right last
    go index last (x :: xs) =
      case !(evalExpr ctx x) of
        Left err => pure $ Left (index, err)
        Right last' => go (S index) last' xs

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

s150 : PrintString m => CanSleep m => (offset : Time) => m String
s150 = do
  printTime offset "s150 proc, first"
  for 5 $ do
    printTime offset "s150 proc, before 1000"
    sleepFor 1.seconds
    printTime offset "s150 proc, before 2000"
    sleepFor 2.seconds
  "long" <$ printTime offset "s150 proc, last"

s55 : PrintString m => CanSleep m => (offset : Time) => m String
s55 = do
  printTime offset "                         s55 proc, first"
  for 5 $ do
    printTime offset "                         s55 proc, before 350"
    sleepFor 350.millis
    printTime offset "                         s55 proc, before 750"
    sleepFor 750.millis
  "mid 1" <$ printTime offset "                         s55 proc, last"

s35 : PrintString m => CanSleep m => (offset : Time) => m String
s35 = do
  printTime offset "                                               s35 proc, first"
  for 5 $ do
    printTime offset "                                               s35 proc, before 700"
    sleepFor 700.millis
  "short" <$ printTime offset "                                               s35 proc, last"

s77 : PrintString m => CanSleep m => (offset : Time) => m String
s77 = do
  printTime offset "                                                                      s77 proc, first"
  for 5 $ do
    printTime offset "                                                                      s77 proc, before 1350"
    sleepFor 1350.millis
  sleepFor 950.millis
  "mid 2" <$ printTime offset "                                                                      s77 proc, last"

export
program : PrintString m => CanSleep m => Zippable m => Alternative m => m Unit
program = do
  offset <- currentTime
  printTime offset "start"

  res <- choice [s150, s55, s35, s77]
  printTime offset "top: \{res}"

  printTime offset "end"

ext: idr


text:
||| A class to store canonical pretty-printers. This is a separate
||| module to allow users to define their own Pretty class or to have
||| different instances for base types.
module Text.PrettyPrint.Leijen.Class

import Text.PrettyPrint.Leijen

-----------------------------------------------------------
-- overloading "pretty"
-----------------------------------------------------------

||| The member `prettyList` is only used to define the `Pretty
||| a => Pretty [a]`. In normal circumstances only the `pretty` function
||| is used.
interface Pretty a where
  ||| The canonical pretty-printer for a type
  pretty        : a -> Doc
  prettyList    : List a -> Doc
  prettyList    = list . map pretty

Pretty a => Pretty (List a) where
  pretty        = prettyList

Pretty Doc where
  pretty        = id

Pretty () where
  pretty ()     = text "()"

Pretty Bool where
  pretty b      = bool b

Pretty Char where
  pretty c      = char c
  prettyList s  = string (pack s)

Pretty Int where
  pretty i      = int i

Pretty Integer where
  pretty i      = integer i

-- Pretty Float where
--   pretty f      = float f

Pretty Double where
  pretty d      = double d

--Pretty Rational where
--  pretty r      = rational r

(Pretty a,Pretty b) => Pretty (a,b) where
  pretty (x,y)  = tupled [pretty x, pretty y]

-- (Pretty a,Pretty b,Pretty c) => Pretty (a,b,c) where
--   pretty (x,y,z)= tupled [pretty x, pretty y, pretty z]

Pretty a => Pretty (Maybe a) where
  pretty Nothing        = empty
  pretty (Just x)       = pretty x


text:
module ReadWrite

import System
import System.Info
import System.File

abc : String
abc = "abc"
abcLF : String
abcLF = "abc\n"
abcCRLF : String
abcCRLF = "abc\r\n"

showInt : String -> String
showInt f = show . map (cast {to=Int}) . unpack $ f

writeFile : String -> IO()
writeFile f = do
         Right h <- openFile f ReadWriteTruncate
           | Left _ => exitFailure
         Right _ <- fPutStr h abc
           | Left _ => exitFailure
         Right _ <- fPutStrLn h abc
           | Left _ => exitFailure
         Right _ <- fPutStr h abcLF
           | Left _ => exitFailure
         Right _ <- fPutStr h abcCRLF
           | Left _ => exitFailure
         _ <- closeFile h
         pure ()

readFile: String -> IO()
readFile f = do
         Right h <- openFile f Read
           | Left _ => exitFailure
         showFile h
  where
    showFile : ?f -> IO ()
    showFile h = do
      if !(fEOF h)
        then pure ()
        else do
          Right l <- fGetLine h
            | Left _ => exitFailure
          putStrLn . showInt $ l
          showFile h

main : IO ()
main = do
  writeFile "abc.txt"
  readFile "abc.txt"


text:
||| Borrowed From Idris2 and improved with Test.Unit
module Main

import Data.List

import Test.Golden

%default total

tests : TestPool
tests
  = MkTestPool "Tests"
        []
        Nothing
        [ "000-mux-check"
        , "001-nice-exempler"
        , "002-unused-port"
        , "003-linear-check"
        , "004-malformed-file"
        , "005-locallink"
        , "006-unused-port"
        , "007-firewall"
        , "008-core-alliance-swerv-eh1"
        , "009-scrubbing"
        , "010-gates"
        , "011-paper"
        , "012-tutorial"
        ]

covering
main : IO ()
main
  = runner [ tests ]

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Calc

%default total

public export
addInts : Int -> Int -> Int
addInts x y = x + y

public export
subInts : Int -> Int -> Int
subInts x y = x - y

public export
mulInts : Int -> Int -> Int
mulInts x y = x * y

public export
divInts : Int -> Int -> Int
divInts x y = x `div` y

max_stars_repo_name: timmyjose-study/idris-from-the-docs

max_issues_repo_name: timmyjose-study/idris-from-the-docs

max_forks_repo_name: timmyjose-study/idris-from-the-docs


text:
module Data.Late

%default total

------------------------------------------------------------------------
-- Type

public export
data Late : Type -> Type where
  Now : a -> Late a
  Later : Inf (Late a) -> Late a

------------------------------------------------------------------------
-- Creating late values

||| Never return
never : Late a
never = Later never

||| Run a small state machine until it reaches a final state and yields a value.
public export
unfold : (seed -> Either seed value) -> seed -> Late value
unfold f s = case f s of
  Left s' => Later (unfold f s')
  Right v => Now v

||| It's easier to define map and (<*>) in terms of bind so let's start
||| by defining it.
public export
bind : Late a -> (a -> Late b) -> Late b
bind (Now v) f = f v
bind (Later d) f = Later (bind d f)

------------------------------------------------------------------------
-- Inspecting late values

||| Check whether we already have a value.
public export
isNow : Late a -> Maybe a
isNow (Now v) = Just v
isNow (Later d) = Nothing

||| Wait for one tick, hoping to get a value.
public export
wait : Late a -> Late a
wait (Later d) = d
wait d = d

||| Wait for a set number of ticks.
public export
engine : Nat -> Late a -> Late a
engine Z = id
engine (S n) = engine n . wait

||| Wait for a set number of ticks, hoping to get a value.
public export
petrol : Nat -> Late a -> Maybe a
petrol n = isNow . engine n

||| Accelerate makes things happen twice as fast.
public export
accelerate : Late a -> Late a
accelerate (Later (Later d)) = Later (accelerate d)
accelerate (Later (Now v)) = Now v
accelerate d = d

------------------------------------------------------------------------
-- Instances

public export
Functor Late where
  map f d = bind d (Now . f)

public export
Applicative Late where
  pure = Now
  df <*> dx = bind df (\ f => map (f $) dx)

public export
Monad Late where
  (>>=) = bind


text:
-- -------------------------------------------------------------- [ Lens.idr ]
-- Description : Idris port of Control.Lens
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Data.Curried

import Data.Morphisms

%access public export

data Curried : ( g : Type -> Type ) -> ( h : Type -> Type ) -> ( a : Type ) -> Type where
  MkCurried : ({r : Type} -> g (a -> r) -> h r) -> Curried g h a

Functor g => Functor (Curried g h) where
  map f (MkCurried g) = MkCurried (g . map (.f))

Functor g => Applicative (Curried g g) where
  pure a = MkCurried (map (\f => f a))
  (MkCurried mf) <*> (MkCurried ma) = MkCurried (ma . mf . map (.))

liftCurried : Applicative f => f a -> Curried f f a
liftCurried fa = MkCurried (<*> fa)

lowerCurried : Applicative f => Curried f g a -> g a
lowerCurried (MkCurried f) = f (pure id)

max_stars_repo_name: andrevidela/idris-lens

max_issues_repo_name: andrevidela/idris-lens

max_forks_repo_name: andrevidela/idris-lens


text:
module Core.Abstraction

import General
import Core.Variable
import Core.Term
import Core.ConSig

%access export

--  o8o  8888. oYYYo YY8YY 8YYYo  o8o   oYYo YY8YY Y8Y _YYY_ 8o  0 oYYYo
-- 8   8 8___Y %___    0   8___P 8   8 0   "   0    0  0   0 8Yo 8 %___
-- 8YYY8 8"""o `"""p   0   8""Yo 8YYY8 0   ,   0    0  0   0 8 Yo8 `"""p
-- 0   0 8ooo" YoooY   0   0   0 0   0  YooY   0   o8o "ooo" 0   8 YoooY

implementation Abstract a b c => Abstract a b (Plict,c) where
	abstr (plic,x) = MkPair plic <$> abstr x

implementation (Abstract a b Pattern, Abstract a b Term) => Abstract a b Clause where
	abstr (NewClause psc sc) = NewClause <$> abstractScope psc <*> abstractScope sc

implementation Abstract a b Term => Abstract a b CaseMotive where
	abstr (CaseMotiveNil a) = CaseMotiveNil <$> abstr a
	abstr (CaseMotiveCons a sc) = CaseMotiveCons <$> abstr a <*> abstractScope sc

implementation Abstract a b Term => Abstract a b Telescope where
	abstr TelescopeNil = pure TelescopeNil
	abstr (TelescopeCons t sc) = TelescopeCons <$> abstr t <*> abstractScope sc

mutual
	implementation Abstract String Term Term where
		abstr (Meta i) = pure $ Meta i
		abstr (Var (Name x)) = asks $ \e => case SortedMap.lookup x e of
			Nothing => Var (Name x)
			Just m  => m
		abstr (Var (Generated x i)) = pure $ Var (Generated x i)
		abstr (DottedVar m var) = pure $ DottedVar m var
		abstr (AbsoluteDottedVar m var) = pure $ AbsoluteDottedVar m var
		abstr (Ann m ty) = Ann <$> abstr m <*> pure ty
		abstr Star = pure Star
		abstr (Pi plic a sc) = Pi plic <$> abstr a <*> abstractScope sc
		abstr (Lam plic sc) = Lam plic <$> abstractScope sc
		abstr (App plic f a) = App plic <$> abstr f <*> abstr a
		abstr (Con c as) = Con c <$> Traversable.for as (\(plic, a) => do a' <- abstr a ; pure (plic,a'))
		abstr (Case as t cs) = Case <$> traverse abstr as <*> abstr t <*> traverse abstr cs
		abstr (RecordType tele) = RecordType <$> abstr tele
		abstr (RecordCon fields) = RecordCon <$> (sequence [ MkPair x <$> abstr m | (x,m) <- fields ])
		abstr (Project m x) = Project <$> abstr m <*> pure x

	implementation Abstract String Term Pattern where
		abstr (VarPat x) = pure $ VarPat x
		abstr (ConPat c ps) = ConPat c <$> traverse abstr ps
		abstr (AssertionPat m) = AssertionPat <$> abstr m
		abstr MakeMeta = pure MakeMeta

mutual
	implementation Abstract Int Term Term where
		abstr (Meta i) = pure $ Meta i
		abstr (Var (Name x)) = pure $ Var (Name x)
		abstr (Var (Generated x i)) = asks $ \e => case SortedMap.lookup i e of
			Nothing => Var (Generated x i)
			Just m  => m
		abstr (DottedVar m var) = pure $ DottedVar m var
		abstr (AbsoluteDottedVar m var) = pure $ AbsoluteDottedVar m var
		abstr (Ann m ty) = Ann <$> abstr m <*> pure ty
		abstr Star = pure Star
		abstr (Pi plic a sc) = Pi plic <$> abstr a <*> abstractScope sc
		abstr (Lam plic sc) = Lam plic <$> abstractScope sc
		abstr (App plic f a) = App plic <$> abstr f <*> abstr a
		abstr (Con c as) = Con c <$> Traversable.for as (\(plic,a) => do a' <- abstr a ; pure (plic,a'))
		abstr (Case as t cs) = Case <$> traverse abstr as <*> abstr t <*> traverse abstr cs
		abstr (RecordType tele) = RecordType <$> abstr tele
		abstr (RecordCon fields) = RecordCon <$> (sequence [ MkPair x <$> abstr m | (x,m) <- fields ])
		abstr (Project m x) = Project <$> abstr m <*> pure x

	implementation Abstract Int Term Pattern where
		abstr (VarPat x) = pure $ VarPat x
		abstr (ConPat c ps) = ConPat c <$> traverse abstr ps
		abstr (AssertionPat m) = AssertionPat <$> abstr m
		abstr MakeMeta = pure MakeMeta

mutual
	implementation Abstract String Variable Term where
		abstr (Meta i) = pure $ Meta i
		abstr (Var (Name x)) = asks $ \e => case SortedMap.lookup x e of
			Nothing => Var (Name x)
			Just y  => Var y
		abstr (Var (Generated x i)) = pure $ Var (Generated x i)
		abstr (DottedVar m var) = pure $ DottedVar m var
		abstr (AbsoluteDottedVar m var) = pure $ AbsoluteDottedVar m var
		abstr (Ann m ty) = Ann <$> abstr m <*> pure ty
		abstr Star = pure Star
		abstr (Pi plic a sc) = Pi plic <$> abstr a <*> abstractScope sc
		abstr (Lam plic sc) = Lam plic <$> abstractScope sc
		abstr (App plic f a) = App plic <$> abstr f <*> abstr a
		abstr (Con c as) = Con c <$> Traversable.for as (\(plic,a) => do a' <- abstr a ; pure (plic,a'))
		abstr (Case as t cs) = Case <$> traverse abstr as <*> abstr t <*> traverse abstr cs
		abstr (RecordType tele) = RecordType <$> abstr tele
		abstr (RecordCon fields) = RecordCon <$> (sequence [ MkPair x <$> abstr m | (x,m) <- fields ])
		abstr (Project m x) = Project <$> abstr m <*> pure x

	implementation Abstract String Variable Pattern where
		abstr (VarPat (Name x)) = asks $ \e => case SortedMap.lookup x e of
			Nothing => VarPat (Name x)
			Just y  => VarPat y
		abstr (VarPat (Generated x i)) = pure $ VarPat (Generated x i)
		abstr (ConPat c ps) = ConPat c <$> traverse abstr ps
		abstr (AssertionPat m) = AssertionPat <$> abstr m
		abstr MakeMeta = pure MakeMeta

mutual
	implementation Abstract Int Variable Term where
		abstr (Meta i) = pure $ Meta i
		abstr (Var (Name x)) = pure $ Var (Name x)
		abstr (Var (Generated x i)) = asks $ \e => case SortedMap.lookup i e of
			Nothing => Var (Generated x i)
			Just y  => Var y
		abstr (DottedVar m var) = pure $ DottedVar m var
		abstr (AbsoluteDottedVar m var) = pure $ AbsoluteDottedVar m var
		abstr (Ann m ty) = Ann <$> abstr m <*> pure ty
		abstr Star = pure Star
		abstr (Pi plic a sc) = Pi plic <$> abstr a <*> abstractScope sc
		abstr (Lam plic sc) = Lam plic <$> abstractScope sc
		abstr (App plic f a) = App plic <$> abstr f <*> abstr a
		abstr (Con c as) = Con c <$> Traversable.for as (\(plic,a) => do a' <- abstr a ; pure (plic,a'))
		abstr (Case as t cs) = Case <$> traverse abstr as <*> abstr t <*> traverse abstr cs
		abstr (RecordType tele) = RecordType <$> abstr tele
		abstr (RecordCon fields) = RecordCon <$> (sequence [ MkPair x <$> abstr m | (x,m) <- fields ])
		abstr (Project m x) = Project <$> abstr m <*> pure x

	implementation Abstract Int Variable Pattern where
		abstr (VarPat (Name x)) = pure $ VarPat (Name x)
		abstr (VarPat (Generated x i)) = asks $ \e => case SortedMap.lookup i e of
			Nothing => VarPat (Generated x i)
			Just y  => VarPat y
		abstr (ConPat c ps) = ConPat c <$> traverse abstr ps
		abstr (AssertionPat m) = AssertionPat <$> abstr m
		abstr MakeMeta = pure MakeMeta

-- 0   0 8YYYY 0    8YYYo 8YYYY 8YYYo oYYYo
-- 8___8 8___  0    8___P 8___  8___P %___
-- 8"""8 8"""  0    8"""  8"""  8""Yo `"""p
-- 0   0 8oooo 8ooo 0     8oooo 0   0 YoooY

piHelper : Plict -> String -> Term -> Term -> Term
piHelper plic x a b = Pi plic a (scope [x] b)

lamHelper : Plict -> String -> Term -> Term
lamHelper plic x b = Lam plic (scope [x] b)

clauseHelper : List Pattern -> List String -> Term -> Clause
clauseHelper ps xs b = do
	let cleanedXs = fst $ runState (traverse cleanXs xs) 0
	let cleanedPs = fst $ runState (traverse cleanPs ps) 0
	NewClause (scope2 xs cleanedXs cleanedPs) (scope (filter isVar xs) b)
where
	cleanXs : String -> State Integer String
	cleanXs "_" = do
		i <- get
		put (i + 1)
		pure $ "$" ++ show i
	cleanXs x = pure x

	cleanPs : Pattern -> State Integer Pattern
	cleanPs (VarPat (Name "_")) = do
		i <- get
		put (i + 1)
		pure $ VarPat (Name ("$" ++ show i))
	cleanPs (VarPat (Name n)) = pure $ VarPat (Name n)
	cleanPs (VarPat (Generated n i)) = pure $ VarPat (Generated n i)
	cleanPs (ConPat c ps') = ConPat c <$> traverse (\(plic,p) => do { p' <- cleanPs p ; pure (plic,p') }) ps'
	cleanPs (AssertionPat m) = pure $ AssertionPat m
	cleanPs MakeMeta = pure MakeMeta

consMotiveHelper : String -> Term -> CaseMotive -> CaseMotive
consMotiveHelper x a b = CaseMotiveCons a (scope [x] b)

telescopeHelper : List (String, Term) -> Telescope
telescopeHelper [] = TelescopeNil
telescopeHelper ((x,t)::xts) = let tele = telescopeHelper xts in TelescopeCons t (scope [x] tele)

implementation Abstract a Term Term => Abstract a Term (ConSig Term) where
	abstr (ConSigNil a) = ConSigNil <$> abstr a
	abstr (ConSigCons plic a sc) = ConSigCons plic <$> abstr a <*> abstractScope sc

conSigHelper : List DeclArg -> Term -> ConSig Term
conSigHelper [] b = ConSigNil b
conSigHelper (NewDeclArg plic x a :: as) b = ConSigCons plic a (scope [x] (conSigHelper as b))

max_stars_repo_name: totalscript/totalscript

max_issues_repo_name: totalscript/totalscript

max_forks_repo_name: totalscript/totalscript


text:
module Text.PrettyPrint.Prettyprinter.Util

import Data.List
import Data.String
import Text.PrettyPrint.Prettyprinter.Doc
import Text.PrettyPrint.Prettyprinter.Render.String

%default total

||| Split an input into word-sized `Doc`.
export
words : String -> List (Doc ann)
words s = map pretty $ map pack (helper (unpack s))
  where
    helper : List Char -> List (List Char)
    helper s =
      case dropWhile isSpace s of
           [] => []
           s' => let (w, s'') = break isSpace s' in
                     w :: helper (assert_smaller s s'')

||| Insert soft linebreaks between words, so that text is broken into multiple
||| lines when it exceeds the available width.
export
reflow : String -> Doc ann
reflow = fillSep . words

||| Renders a document with a certain width.
export
putDocW : Nat -> Doc ann -> IO ()
putDocW w = renderIO . layoutPretty (record { layoutPageWidth = AvailablePerLine (cast w) 1 } defaultLayoutOptions)


text:
module Progress

-- Pseudo-progress theorem for the 'Step' relation
-- in the untyped lambda calculus.

import Step
import Subst
import Term

%access export

-------------------------
-- Begin: PSEUDO-PROGRESS

-- Function 'progress' looks like the usual progress theorem
-- but notice that 'progress' is not a total function.
--
-- (It is therefore not consistent to interpret the
--  definition of the function 'progress' as a proof.)
--
progress : (e : Term 0) -> Either (Value e) (e' : Term 0 ** (Step e e'))
-- Expressions that are variables cannot occur in an empty context:
-- (In other words, variables are not closed expressions.)
progress (TVar i) = absurd $ FinZAbsurd i
-- Abstractions are values already:
progress (TAbs _) = Left VAbs
-- Applications can reduce in three different ways, the most
-- interesting of which occurs when both arguments of 'App'
-- are values already: in this case, the function 'subst'
-- is required:
progress (TApp e1 e2) = case progress e1 of
  Right (e' ** st) => Right (TApp e' e2 ** StApp1 st)
  Left  v1         =>
    case progress e2 of
         Right (e' ** st) => Right (TApp e1 e' ** StApp2 v1 st)
         Left  v2         => case e1 of
                                  TAbs f => let e'' = subst e2 FZ f
                                            in Right (e'' ** StBeta v2)
-- The constant 'Zero' is a value already:
progress TZero = Left VZero
--
progress (TSucc e) = case progress e of
  Right (e' ** st) => Right (TSucc e' ** StSucc st)
  Left  v          => Left (VSucc v)
progress (TPred e) = case progress e of
  Right (e' ** st) => Right (TPred e' ** StPred st)
  Left v           =>
    case e of
         TZero    => Right (TZero ** StPredZero)
         TSucc e' => case v of
                          VAbs     impossible
                          VZero    impossible
                          VSucc v' => Right (e' ** StPredSucc v')
--
progress (TIfz e1 e2 e3) = case progress e1 of
  Right (e' ** st) => Right $ (TIfz e' e2 e3 ** StIfz st)
  Left v           => case v of
                           VZero    => Right (e2 ** StIfzZero)
                           VSucc v' => Right (e3 ** StIfzSucc v')

-- End: PSEUDO-PROGRESS
-----------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Network.TLS.Handshake

import Data.Either
import Data.List1
import Data.Vect
import Network.TLS.HelloExtension
import Network.TLS.Magic
import Network.TLS.Parsing
import Utils.Bytes
import Utils.Misc
import Utils.Show

namespace Message
  public export
  record ClientHello where
    constructor MkClientHello
    version : TLSVersion
    random : Vect 32 Bits8
    session_id : List Bits8
    cipher_suites : List1 CipherSuite
    compression_levels : List1 CompressionLevel
    extensions : List (DPair _ ClientExtension)

  public export
  Show ClientHello where
    show x = show_record "ClientHello"
      [ ("version", show x.version)
      , ("random", xxd $ toList x.random)
      , ("session_id", xxd x.session_id)
      , ("cipher_suites", show x.cipher_suites)
      , ("compression_levels", show x.compression_levels)
      , ("extensions", show $ map (\x => show x.snd) x.extensions)
      ]

  public export
  record ServerHello where
    constructor MkServerHello
    version : TLSVersion
    random : Vect 32 Bits8
    session_id : List Bits8
    cipher_suite : CipherSuite
    compression_level : CompressionLevel
    extensions : List (DPair _ ServerExtension)

  public export
  Show ServerHello where
    show x = show_record "ClientHello"
      [ ("version", show x.version)
      , ("random", xxd $ toList x.random)
      , ("session_id", xxd x.session_id)
      , ("cipher_suite", show x.cipher_suite)
      , ("compression_level", show x.compression_level)
      , ("extensions", show $ map (\x => show x.snd) x.extensions)
      ]

  public export
  record EncryptedExtensions where
    constructor MkEncryptedExtensions
    get : List Bits8 -- TODO: how would it work?

  public export
  Show EncryptedExtensions where
    show x = show_record "EncryptedExtensions"
      [ ("get", xxd x.get)
      ]

  public export
  record CertificateEntry where
    constructor MkCertificateEntry
    body : List Bits8
    extensions : List Bits8

  public export
  Show CertificateEntry where
    show x = show_record "CertificateEntry"
      [ ("certificate", show $ xxd $ x.body)
      , ("certificate_extension", xxd x.extensions)
      ]

  public export
  record Certificate where
    constructor MkCertificate
    request_context : List Bits8
    certificates : List CertificateEntry

  public export
  Show Certificate where
    show x = show_record "Certificate"
      [ ("request_context", xxd x.request_context)
      , ("certificates", foldl (<+>) "" $ map show $ x.certificates)
      ]

  public export
  record CertificateVerify where
    constructor MkCertificateVerify
    signature_algorithm : SignatureAlgorithm
    signature : List Bits8

  public export
  Show CertificateVerify where
    show x = show_record "CertificateVerify"
      [ ("signature_algorithm", show x.signature_algorithm)
      , ("signature", xxd x.signature)
      ]

  public export
  record Finished where
    constructor MkFinished
    verify_data : List Bits8

  public export
  Show Finished where
    show x = show_record "Finished"
      [ ("verify_data", show x.verify_data)
      ]

  public export
  record NewSessionTicket where
    constructor MkNewSessionTicket
    lifetime_seconds : Nat
    age_add_milliseconds : Nat
    nonce : List Bits8
    session_ticket : List Bits8
    extensions : List ((Bits8, Bits8), List Bits8)

  public export
  Show NewSessionTicket where
    show x = show_record "NewSesssionTicket"
      [ ("lifetime_seconds", show x.lifetime_seconds)
      , ("age_add_milliseconds", show x.age_add_milliseconds)
      , ("nonce", show x.nonce)
      , ("session_ticket", show x.session_ticket)
      , ("extensions", show x.extensions)
      ]

  public export
  record ServerKeyExchange where
    constructor MkServerKeyExchange
    server_pk_group : SupportedGroup
    server_pk_body : List Bits8
    signature_algo : SignatureAlgorithm
    signature_body : List Bits8

  public export
  Show ServerKeyExchange where
    show x = show_record "ServerKeyExchange"
      [ ("server_pk_group", show x.server_pk_group)
      , ("server_pk_body", xxd x.server_pk_body)
      , ("signature_algo", show x.signature_algo)
      , ("signature_body", xxd x.signature_body)
      ]

  public export
  record ServerHelloDone where
    constructor MkServerHelloDone

  public export
  Show ServerHelloDone where
    show x = show_record "ServerHelloDone" []

  public export
  record ClientKeyExchange where
    constructor MkClientKeyExchange
    public_key : List Bits8

  Show ClientKeyExchange where
    show x = show_record "ClientKeyExchange"
      [ ("public_key", show x.public_key)
      ]

public export
data Handshake : HandshakeType -> Type where
  ClientHello : ClientHello -> Handshake ClientHello
  ServerHello : ServerHello -> Handshake ServerHello
  EncryptedExtensions : EncryptedExtensions -> Handshake EncryptedExtensions
  Certificate : Certificate -> Handshake Certificate
  CertificateVerify : CertificateVerify -> Handshake CertificateVerify
  Finished : Finished -> Handshake Finished
  NewSessionTicket : NewSessionTicket -> Handshake NewSessionTicket
  ServerKeyExchange : ServerKeyExchange -> Handshake ServerKeyExchange
  ServerHelloDone : ServerHelloDone -> Handshake ServerHelloDone
  ClientKeyExchange : ClientKeyExchange -> Handshake ClientKeyExchange

public export
Show (Handshake type) where
  show (ClientHello x) = show x
  show (ServerHello x) = show x
  show (EncryptedExtensions x) = show x
  show (Certificate x) = show x
  show (CertificateVerify x) = show x
  show (Finished x) = show x
  show (NewSessionTicket x) = show x
  show (ServerKeyExchange x) = show x
  show (ServerHelloDone x) = show x
  show (ClientKeyExchange x) = show x

XHandshake : Type
XHandshake = Eithers
  [ Handshake ClientHello
  , Handshake ServerHello
  , Handshake EncryptedExtensions
  , Handshake Certificate
  , Handshake CertificateVerify
  , Handshake Finished
  , Handshake NewSessionTicket
  , Handshake ServerKeyExchange
  , Handshake ServerHelloDone
  , Handshake ClientKeyExchange
  ]

hack_handshake : DPair _ Handshake -> XHandshake
hack_handshake (ClientHello ** x)         = Left x
hack_handshake (ServerHello ** x)         = Right (Left x)
hack_handshake (EncryptedExtensions ** x) = Right (Right (Left x))
hack_handshake (Certificate ** x)         = Right (Right (Right (Left x)))
hack_handshake (CertificateVerify ** x)   = Right (Right (Right (Right (Left x))))
hack_handshake (Finished ** x)            = Right (Right (Right (Right (Right (Left x)))))
hack_handshake (NewSessionTicket ** x)    = Right (Right (Right (Right (Right (Right (Left x))))))
hack_handshake (ServerKeyExchange ** x)   = Right (Right (Right (Right (Right (Right (Right (Left x)))))))
hack_handshake (ServerHelloDone ** x)     = Right (Right (Right (Right (Right (Right (Right (Right (Left x))))))))
hack_handshake (ClientKeyExchange ** x)   = Right (Right (Right (Right (Right (Right (Right (Right (Right x))))))))

fix_handshake : XHandshake -> DPair _ Handshake
fix_handshake (Left x)                                                                  = (ClientHello ** x)
fix_handshake (Right (Left x))                                                          = (ServerHello ** x)
fix_handshake (Right (Right (Left x)))                                                  = (EncryptedExtensions ** x)
fix_handshake (Right (Right (Right (Left x))))                                          = (Certificate ** x)
fix_handshake (Right (Right (Right (Right (Left x)))))                                  = (CertificateVerify ** x)
fix_handshake (Right (Right (Right (Right (Right (Left x))))))                          = (Finished ** x)
fix_handshake (Right (Right (Right (Right (Right (Right (Left x)))))))                  = (NewSessionTicket ** x)
fix_handshake (Right (Right (Right (Right (Right (Right (Right (Left x))))))))          = (ServerKeyExchange ** x)
fix_handshake (Right (Right (Right (Right (Right (Right (Right (Right (Left x)))))))))  = (ServerHelloDone ** x)
fix_handshake (Right (Right (Right (Right (Right (Right (Right (Right (Right x))))))))) = (ClientKeyExchange ** x)

namespace Parsing
  export
  handshake_id_with_length : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (HandshakeType, Nat)
  handshake_id_with_length = handshake_type <*>> nat 3

  export
  no_id_client_hello : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ClientHello)
  no_id_client_hello = map (\(a,b,c,d,e,f) => ClientHello (MkClientHello a b c d e f)) (\(ClientHello (MkClientHello a b c d e f)) => (a,b,c,d,e,f))
    $ lengthed 3
    $ under "client version" tls_version
    <*>> (under "client random" $ ntokens 32)
    <*>> (under "session id" $ lengthed_list 1 token)
    <*>> (under "client proposed cipher suites" $ lengthed_list1 2 cipher_suite)
    <*>> (under "client proposed compression levels" $ lengthed_list1 1 compression_level)
    <*>> (under "client extensions" $ lengthed_list 2 extension)

  export
  no_id_server_hello : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ServerHello)
  no_id_server_hello = map
    ((\(a,b,c,d,e,f) => ServerHello (MkServerHello a b c d e f)) . fromEither) -- (\(a,b,c,d,e,f) => ServerHello (MkServerHello a b c d e f))
    (\(ServerHello (MkServerHello a b c d e f)) => Left (a,b,c,d,e,f))
    $ ( lengthed 3
    $ (under "server version" tls_version)
    <*>> (under "server random" $ ntokens 32)
    <*>> (under "session id" $ lengthed_list 1 token)
    <*>> (under "server chosen cipher suite" $ cipher_suite)
    <*>> (under "server chosen compression level" $ compression_level)
    <*>> (under "server extensions" $ lengthed_list 2 Server.extension)
    )
    <|> ( lengthed 3
    $ (under "server version" tls_version)
    <*>> (under "server random" $ ntokens 32)
    <*>> (under "session id" $ lengthed_list 1 token)
    <*>> (under "server chosen cipher suite" $ cipher_suite)
    <*>> (under "server chosen compression level" $ compression_level)
    <*>> (under "server extensions" $ MkParserializer (const []) (pure []))
    )

  export
  no_id_encrypted_extensions : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake EncryptedExtensions)
  no_id_encrypted_extensions = map (\a => EncryptedExtensions (MkEncryptedExtensions a)) (\(EncryptedExtensions (MkEncryptedExtensions a)) => a)
    $ lengthed 3
    $ (under "encrypted extensions body" $ lengthed_list 2 token)

  export
  no_id_certificate : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake Certificate)
  no_id_certificate =
    map
    (\(a,b) => Certificate (MkCertificate a $ map (uncurry MkCertificateEntry) b))
    (\(Certificate (MkCertificate a d)) => (a, map (\b => (b.body, b.extensions)) d))
    $ lengthed 3
    $ (under "request context" $ lengthed_list 1 token)
    <*>> (under "certificates"
         $ under "certificate list"
         $ lengthed_list 3
         $ under "certificate entry"
         $ (lengthed_list 3 token <*>> (under "certificate extensions" $ lengthed_list 2 token)))

  export
  no_id_certificate2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake Certificate)
  no_id_certificate2 = map
    (\b => Certificate (MkCertificate [] $ map (\x => MkCertificateEntry x []) b))
    (\(Certificate (MkCertificate a b)) => map body b)
    $ lengthed 3
    $ (under "certificate list 1.2" $ lengthed_list 3 $ under "certificate entry 1.2" $ lengthed_list 3 token)

  export
  no_id_certificate_verify : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake CertificateVerify)
  no_id_certificate_verify = map (\(a,b) => CertificateVerify (MkCertificateVerify a b)) (\(CertificateVerify (MkCertificateVerify a b)) => (a,b))
    $ lengthed 3
    $ signature_algorithm
    <*>> (under "signature" $ lengthed_list 2 token)

  export
  no_id_finished : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake Finished)
  no_id_finished = map (\a => Finished (MkFinished a)) (\(Finished (MkFinished a)) => a)
    $ lengthed_list 3 token

  export
  no_id_new_session_ticket : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake NewSessionTicket)
  no_id_new_session_ticket = map
    (\(a,b,c,d,e) => NewSessionTicket (MkNewSessionTicket a b c d e))
    (\(NewSessionTicket (MkNewSessionTicket a b c d e)) => (a,b,c,d,e))
    $ lengthed 3
    $ (under "ticket lifetime seconds" $ nat 4)
    <*>> (under "ticket age add milliseconds" $ nat 4)
    <*>> (under "ticket nonce" $ lengthed_list 1 token)
    <*>> (under "session ticket" $ lengthed_list 2 token)
    <*>> (under "extensions" $ lengthed_list 2 ((token <*>> token) <*>> lengthed_list 2 token))

  export
  no_id_server_key_exchange : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ServerKeyExchange)
  no_id_server_key_exchange = map
    (\(a,b,c,d) => ServerKeyExchange (MkServerKeyExchange a b c d))
    (\(ServerKeyExchange (MkServerKeyExchange a b c d)) => (a,b,c,d))
    $ lengthed 3
    $ (under "curve info" $ (is [0x03]) *> supported_group)
    <*>> (under "public key" $ lengthed_list 1 token)
    <*>> (under "signature algo" signature_algorithm)
    <*>> (under "signature body" $ lengthed_list 2 token)

  export
  no_id_server_hello_done : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ServerHelloDone)
  no_id_server_hello_done = map
    (const (ServerHelloDone MkServerHelloDone))
    (const ())
    $ is [0x00, 0x00, 0x00]

  export
  no_id_client_key_exchange : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (Handshake ClientKeyExchange)
  no_id_client_key_exchange = map
    (ClientKeyExchange . MkClientKeyExchange)
    (\(ClientKeyExchange (MkClientKeyExchange x)) => x)
    $ lengthed 3
    $ (under "public key" $ lengthed_list 1 token)

  export
  with_id : (Cons (Posed Bits8) i, Monoid i) => {type : HandshakeType} -> Parserializer Bits8 i (SimpleError String) (Handshake type) -> Parserializer Bits8 i (SimpleError String) (Handshake type)
  with_id pser = under (show type <+> " handshake") $ is (to_vect $ handshake_type_to_id type) *> pser

  export
  handshake : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (DPair _ Handshake)
  handshake = map fix_handshake hack_handshake
    $ (with_id no_id_client_hello)
    <|> (with_id no_id_server_hello)
    <|> (with_id no_id_encrypted_extensions)
    <|> (with_id no_id_certificate)
    <|> (with_id no_id_certificate_verify)
    <|> (with_id no_id_finished)
    <|> (with_id no_id_new_session_ticket)
    <|> (with_id no_id_server_key_exchange)
    <|> (with_id no_id_server_hello_done)
    <|> (with_id no_id_client_key_exchange)

  export
  handshake2 : (Cons (Posed Bits8) i, Monoid i) => Parserializer Bits8 i (SimpleError String) (DPair _ Handshake)
  handshake2 = map fix_handshake hack_handshake
    $ (with_id no_id_client_hello)
    <|> (with_id no_id_server_hello)
    <|> (with_id no_id_encrypted_extensions)
    <|> (with_id no_id_certificate2)
    <|> (with_id no_id_certificate_verify)
    <|> (with_id no_id_finished)
    <|> (with_id no_id_new_session_ticket)
    <|> (with_id no_id_server_key_exchange)
    <|> (with_id no_id_server_hello_done)
    <|> (with_id no_id_client_key_exchange)


text:
||| Various tests of automatically-generated eliminators, to show that
||| the compiler doesn't barf and that they can be used for proving
||| things.
module ElimTest

import Data.Vect
import Data.So
import Control.WellFounded
import Data.Nat.DivMod.IteratedSubtraction

import Pruviloj.Core
import Pruviloj.Derive.Eliminators
import Derive.TestDefs

%default total

mkName : String -> TTName
mkName n = NS (UN n) ["ElimTest"]

mutual
  data U : Type where
    UNIT : U
    PI : (t : U) -> (el t -> U) -> U

  el : U -> Type
  el UNIT = ()
  el (PI ty ret) = (x : el ty) -> (el $ ret x)

mutual
  data Even : Nat -> Type where
    EvenZ : Even Z
    EvenS : Odd n -> Even (S n)
  data Odd : Nat -> Type where
    OddN : Even n -> Odd (S n)

forEffect : ()
forEffect = %runElab (do deriveElim `{Vect} (mkName "vectElim")
                         deriveElim `{Bool} (mkName "boolElim")
                         deriveElim `{List} (mkName "listElim")
                         deriveElim `{So} (mkName "soElim")
                         deriveElim `{Void} (mkName "voidElim")
                         deriveElim `{Nat} (mkName "natElim")
                         deriveElim `{LTE} (mkName "lteElim")
                         deriveElim `{LT'} (mkName "ltElim")
                         deriveElim `{(=)} (mkName "wrongEqElim")
                         deriveElim `{U} (mkName "uElim")
                         deriveElim `{W} (mkName "wElim")
                         deriveElim `{Unit} (mkName "unitElim")
                         deriveElim `{Even} (mkName "evenElim")
                         deriveElim `{Odd} (mkName "oddElim")
                         deriveElim `{Accessible} (mkName "accElim")
                         search)

||| Simple function computed using an eliminator
rev : List a -> List a
rev {a} xs = listElim a xs (const $ List a) [] (\y, _, ys => ys ++ [y])

||| Simple proof by induction using a generated eliminator
total
plusIsAssociative : (x,y,z : Nat) -> plus x (plus y z) = plus (plus x y) z
plusIsAssociative = \x,y,z => natElim x (\n => plus n (plus y z) = plus (plus n y) z) Refl (\n, ih => cong ih)

||| The "shape" of the underlying tree for Nat encoded as a W-type
WNatStep : Bool -> Type
WNatStep b = if b then () else Void

||| Nats, as a W-type
WNat : Type
WNat = W Bool WNatStep

||| Zero (it has no predecessors!)
WZ : WNat
WZ = Sup False void

||| Succ (it has a single predecessor, thus ()!)
wS : WNat -> WNat
wS n = Sup True (const n)

||| The induction principle for Nat, here expressed on Nat encoded as W-types.
|||
||| Note that this only works for this particular encoding of the
||| Nat. A separate, equivalent encoding would not work due to W-types
||| being basically useless in intensional type theory. Nevertheless,
||| it demonstrates that the generated eliminators can be used.
indWNat : (P : WNat -> Type) -> P WZ -> ((n : WNat) -> P n -> P (wS n)) -> (n : WNat) -> P n
indWNat P z s n = wElim Bool WNatStep n P
                    (\b => boolElim b
                            (\b' => (f : WNatStep b' -> WNat) ->
                                    ((x : WNatStep b') -> P (f x)) ->
                                    P (Sup b' f))
                            (\f, _ => rewrite voidFunext f void in z)
                            (\f, ih => rewrite unitFunext f in s (f ()) (ih ())))
  where
    ||| Functional extensionality that uses unsafe features to get it
    ||| to actually compute. This is evil and perhaps even inconsistent:
    ||| replace with a postulate for sanity. But it lets addition of WNat go.
    funext : (f, g : a -> b) -> ((x : a) -> f x = g x) -> f = g
    funext {a} {b} f g fun = really_believe_me (Refl {A=a->b} {x=f})
    voidFunext : (f, g : Void -> a) -> f = g
    voidFunext = \f,g => funext f g (\x => voidElim x (const (f x = g x)))
    unitEta : (x : ()) -> x = ()
    unitEta () = Refl
    unitFunext : (f : () -> a) -> f = \x => f ()
    unitFunext = \f => funext f (\x => f ()) (\x => cong (unitEta x))

addWNat : WNat -> WNat -> WNat
addWNat x y = indWNat (const WNat) y (\_, m => wS m) x

||| Recover the induction principle over well-founded relations from the generated one
accInd' : {rel : a -> a -> Type} -> {P : a -> Type} ->
          (step : (x : a) -> ((y : a) -> rel y x -> P y) -> P x) ->
          (z : a) -> Accessible rel z -> P z
accInd' {a} {rel} {P} step z acc =
  accElim a rel z acc (\x, _ => P x) (\y, acc', ih => step y ih)

max_stars_repo_name: Garnasha/derive-all-the-instances

max_issues_repo_name: Garnasha/derive-all-the-instances

max_forks_repo_name: Garnasha/derive-all-the-instances


text:
module Language.LSP.CodeAction.MakeWith

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List
import Data.List1
import Data.String
import Idris.IDEMode.MakeClause
import Idris.REPL.Opts
import Idris.Syntax
import Idris.Resugar
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.Message
import Libraries.Data.List.Extra
import Libraries.Data.PosMap
import Parser.Unlit
import Server.Configuration
import Server.Log
import Server.Utils
import TTImp.TTImp

buildCodeAction : Name -> URI -> List TextEdit -> CodeAction
buildCodeAction name uri edits =
  let workspaceEdit = MkWorkspaceEdit { changes           = Just (singleton uri edits)
                                      , documentChanges   = Nothing
                                      , changeAnnotations = Nothing
                                      }
   in MkCodeAction { title       = "Make with of \{show name}"
                   , kind        = Just RefactorRewrite
                   , diagnostics = Just []
                   , isPreferred = Just False
                   , disabled    = Nothing
                   , edit        = Just workspaceEdit
                   , command     = Nothing
                   , data_       = Nothing
                   }

export
makeWith : Ref LSPConf LSPConfiguration
        => Ref MD Metadata
        => Ref Ctxt Defs
        => Ref UST UState
        => Ref Syn SyntaxInfo
        => Ref ROpts REPLOpts
        => CodeActionParams -> Core (Maybe CodeAction)
makeWith params = do
  let True = params.range.start.line == params.range.end.line
    | _ => do logString Debug "makeWith: start and end line were different"
              pure Nothing

  [] <- searchCache params.range MakeWith
    | action :: _ => do logString Debug "makeWith: found cached action"
                        pure (Just action)

  nameLocs <- gets MD nameLocMap
  let line = params.range.start.line
  let col = params.range.start.character
  let Just (loc@(_, nstart, nend), name) = findPointInTreeLoc (line, col) nameLocs
    | Nothing => do logString Debug "makeWith: couldn't find name at \{show (line, col)}"
                    pure Nothing

  context <- gets Ctxt gamma
  [(_, _, Hole locs _, _)] <- lookupNameBy (\g => (definition g, type g)) name context
    | _ => do logString Debug $ "makeWith: \{show name} is not a metavariable"
              pure Nothing

  litStyle <- getLitStyle
  Just src <- getSourceLine (line + 1)
    | Nothing => do logString Debug $ "makeWith: error while fetching the referenced line"
                    pure Nothing
  let Right l = unlit litStyle src
    | Left err => do logString Debug $ "makeWith: invalid literate Idris"
                     pure Nothing
  let (markM, _) = isLitLine src
  let with_ = makeWith name l
  let range = MkRange (MkPosition line 0) (MkPosition line (cast (length src) - 1))
  let edit = MkTextEdit range with_
  let action = buildCodeAction name params.textDocument.uri [edit]

  modify LSPConf (record { cachedActions $= insert (cast loc, MakeWith, [action]) })
  pure $ Just action


text:
module BioFasta.Helpers

import Data.List
import Data.Maybe
import Data.Strings
import BioCore.Sequence
import BioFasta.Common

%default total

public export
||| Convert SeqData to String.
toStr : SeqData -> String
toStr (UnSD seqdata) = seqdata

public export
notLast : (l :(List (List Char))) -> {auto ok : NonEmpty l} -> List (List Char)
notLast l = init l

public export
splitsAt : Offset -> List Char -> List Char -> List (List Char)
splitsAt _ _ []       = []
splitsAt n s (_::ss') = let (s1,s2) = splitAt (integerToNat
                                              (prim__cast_IntInteger
                                              (extractUnOff n))) s
                          in if isNil s2
                               then [s1]
                               else s1 :: splitsAt n s2 ss'

public export
smallBlocks : List Char -> List (List Char)
smallBlocks blist = groupBy (const (/= '>'))
                    (filter (\x => x /= '#')
                    (dropWhile (\x => x /= '>') blist))


text:
module MaybeFin

import Data.Fin

%default total
%access public

data MaybeFin : Nat -> Type where
  NoFin : MaybeFin Z
  SomeFin : Fin (S k) -> MaybeFin (S k)

instance Cast (MaybeFin n) (Maybe (Fin n)) where
  cast NoFin = Nothing
  cast (SomeFin x) = Just x


text:
{- Another feature of the Idris2 type system, which comes from the underlying
 - Quantitative Type Theory, are quantities. Each value in a type can be annotated
 - as follows:
 -   0 - Argument erased at runtime, i.e. is only available at type-checking
 -   1 - Argument must be used exactly once each time the function is called.
       - No annotation means the argument can be used any number of times
 - The full inferred type of `id` below is shown in `id2`. -}

id : a -> a
id x = x

id2 : {0 a : Type} -> (1 x : a) -> a -- implicit eraced argument,
id2 x = x

{- We can see the effect of quantities (although not yet why they are useful)
 - through the following example. Consider the following definition. -}

duplicate : (1 x : a) -> (a, a)
duplicate x = ?hole

{- Inspecting ?hole above yields

 0 a : Type
 1 x : a
 -------------------------------------
 hole : (a, a)

 - Thus, idris is telling us we cannot use `a` in a term (only a type) and
 - we can use `x` exactly once. Say we do use it once:

-}

duplicate2 : (1 x : a) -> (a, a)
duplicate2 x = (?hole2, x)

{- On the hole `?hole2` above, we get the following. Note how the quantity of `x`
 - has changed from 1 to 0, since it has been used once.

 0 a : Type
 0 x : a
 -------------------------------------
 hole2 : a

 - Thus, this function is impossible to write without removing the quanity
 - constraint. We cannot use `x` twice.
 -}

duplicate3 : (x : a) -> (a, a)
duplicate3 x = (x, x)

{- Watch the following talk by the creator of Idris, starting at 26:15 for an
 - example of how quantities could be useful in practice. Or watch the whole
 - video, it gives a bunch of cool examples and should be accessible after
 - reading these notes.

 - https://www.youtube.com/watch?v=DRq2NgeFcO0}


text:
module CH09

%default total

data Elem : a -> List a -> Type where
  InCons : Elem value (value :: xs)
  InList : (prf : Elem value xs) -> Elem value (x :: xs)

elemNotInNil : Elem value [] -> Void
elemNotInNil _ impossible

elemNotInTail : (notInTail : Elem y xs -> Void) -> (notInCons : (x = y) -> Void) -> Elem y (x :: xs) -> Void
elemNotInTail _ notInCons InCons               = notInCons Refl
elemNotInTail notInTail notInCons (InList prf) = notInTail prf

isElem : DecEq a => (value : a) -> (xs : List a) -> Dec (Elem value xs)
isElem _ []        = No elemNotInNil
isElem y (x :: xs) = case decEq x y of
                       Yes Refl     => Yes InCons
                       No notInCons => case isElem y xs of
                                         Yes prf      => Yes (InList prf)
                                         No notInTail => No (elemNotInTail notInTail notInCons)

data Last : List a -> a -> Type where
  LastOne : Last [value] value
  LastCons : (prf : Last xs value) -> Last (x :: xs) value

notInLast : (contra : (x = y) -> Void) -> Last [x] y -> Void
notInLast contra LastOne = contra Refl

notInNil : Last [] value -> Void
notInNil _ impossible

notInTail : (notNil : (xs = []) -> Void) -> (notInList : Last xs y -> Void) -> Last (x :: xs) y -> Void
notInTail notNil _ LastOne           = notNil Refl
notInTail _ notInList (LastCons prf) = notInList prf

isLast : DecEq a => (xs : List a) -> (value : a) -> Dec (Last xs value)
isLast [] _        = No notInNil
isLast (x :: xs) y = case decEq xs [] of
                       Yes Refl  => case decEq x y of
                                      Yes Refl => Yes LastOne
                                      No notEq => No (notInLast notEq)
                       No notNil => case isLast xs y of
                                      Yes prf    => Yes (LastCons prf)
                                      No notLast => No (notInTail notNil notLast)


text:
module Arduino.Time

-------------
--- Types ---
-------------

-- TODO to make this type be nicer
public export
Time : Type
Time = Int

-----------------
--- Functions ---
-----------------

-- TODO to make something with, well, the fact that `Bits32` leaks out from the implementation

export
toMilliseconds : Time -> Bits32
toMilliseconds = cast

export
fromMilliseconds : Bits32 -> Time
fromMilliseconds = fromInteger . cast

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

public export
interface Timed m where
  currentTime : m Time

public export
interface Monad m => DelayableTill m where
  sleepTill : Time -> m Unit

public export
interface Monad m => DelayableFor m where
  sleepFor : Time -> m Unit

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
module Compiler.LLVM.Rapid.String

import Data.Vect

import Compiler.LLVM.IR
import Compiler.LLVM.Instruction
import Compiler.LLVM.Rapid.Object
import Control.Codegen
import Data.Utils

public export
data CompareOp = LT | LTE | EQ | GTE | GT

export
getStringLength : IRValue IRObjPtr -> Codegen (IRValue I32)
getStringLength strObj = do
  strLenBytes <- getStringByteLength strObj
  call {t=I32} "ccc" "@utf8_bytes_to_codepoints" [toIR !(getObjectPayloadAddr {t=I8} strObj), toIR strLenBytes]

export
stringCompare : CompareOp -> IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
stringCompare op o1 o2 = do
  l1 <- getObjectSize o1
  l2 <- getObjectSize o2

  minLength <- mkZext {to=I64} !(mkMin l1 l2)

  lblSizeCompare <- genLabel "strcompare_size"
  lblCmpStart <- genLabel "strcompare_start"
  lblPrefixEq <- genLabel "strcompare_prefix_eq"
  lblPrefixNotEq <- genLabel "strcompare_prefix_neq"
  lblEnd <- genLabel "strcompare_end"

  jump lblSizeCompare
  beginLabel lblSizeCompare
  lengthsEqual <- icmp "eq" l1 l2

  let startCommand = case op of
                          EQ => (branch lengthsEqual lblCmpStart lblEnd)
                          _ => (branch (Const I1 1) lblCmpStart lblEnd)

  startCommand
  beginLabel lblCmpStart

  str1 <- getObjectPayloadAddr {t=I8} o1
  str2 <- getObjectPayloadAddr {t=I8} o2
  cmpResult32 <- call {t=I32} "fastcc" "@rapid.memcmp" [toIR str1, toIR str2, toIR minLength]
  cmpResult <- mkSext cmpResult32
  cmpResultIsEq <- icmp "eq" cmpResult (ConstI64 0)
  branch cmpResultIsEq lblPrefixEq lblPrefixNotEq

  beginLabel lblPrefixEq
  string1Shorter <- icmp "slt" l1 l2
  string1ShorterOrEqual <- icmp "sle" l1 l2
  string2Shorter <- icmp "slt" l2 l1
  string2ShorterOrEqual <- icmp "sle" l2 l1
  let result : IRValue I1
      result =  case op of
                     LT  => string1Shorter
                     LTE => string1ShorterOrEqual
                     EQ  => lengthsEqual
                     GTE => string2ShorterOrEqual
                     GT  => string2Shorter
  jump lblEnd

  beginLabel lblPrefixNotEq
  cmpResultIsLt <- icmp "slt" cmpResult (Const I64 0)
  cmpResultIsGt <- icmp "sgt" cmpResult (Const I64 0)
  let result2 =  case op of
                      LT  => cmpResultIsLt
                      LTE => cmpResultIsLt
                      EQ  => Const I1 0
                      GT  => cmpResultIsGt
                      GTE => cmpResultIsGt
  jump lblEnd
  beginLabel lblEnd

  finalResult <- phi [(result, lblPrefixEq), (result2, lblPrefixNotEq), (Const I1 0, lblSizeCompare)]
  cgMkInt !(mkZext finalResult)

export
stringEqual : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue I1)
stringEqual obj1 obj2 = do
  lblStart <- genLabel "strcompare_hdr"
  lblEnd <- genLabel "strcompare_end"
  lblCompareContents <- genLabel "strcompare_content"
  appendCode $ "br " ++ toIR lblStart
  beginLabel lblStart
  h1 <- getObjectHeader obj1
  h2 <- getObjectHeader obj2
  headersEqual <- icmp "eq" h1 h2
  appendCode $ "br " ++ toIR headersEqual ++ ", " ++ toIR lblCompareContents ++ ", " ++ toIR lblEnd
  beginLabel lblCompareContents
  str1 <- getObjectPayloadAddr {t=I8} obj1
  str2 <- getObjectPayloadAddr {t=I8} obj2
  length <- mkAnd h1 (ConstI64 0xffffffff)
  contentsEqual <- (SSA I1) <$> assignSSA ("call fastcc i1 @mem_eq(" ++ (showSep ", " ([toIR str1, toIR str2, toIR length])) ++ ")")
  appendCode $ "br " ++ toIR lblEnd
  beginLabel lblEnd
  phi [(headersEqual, lblStart), (contentsEqual, lblCompareContents)]

export
mkSubstring : IRValue IRObjPtr -> IRValue I64 -> IRValue I64 -> Codegen (IRValue IRObjPtr)
mkSubstring strObj startIndexRaw length = do
  length32 <- mkTrunc {to=I32} !(mkMax length (Const I64 0))
  strLenBytes <- getStringByteLength strObj

  startIndex <- mkTrunc {to=I32} !(mkMax startIndexRaw (Const I64 0))
  strPayloadStart <- getObjectPayloadAddr {t=I8} strObj

  startOffset <- call {t=I32} "ccc" "@utf8_codepoints_bytelen" [toIR strPayloadStart, toIR startIndex, toIR strLenBytes]
  startAddr <- getElementPtr strPayloadStart startOffset
  maxLengthBytes <- mkMax !(mkSub strLenBytes startOffset) (Const I32 0)
  resultLength <- call {t=I32} "ccc" "@utf8_codepoints_bytelen" [toIR startAddr, toIR length32, toIR maxLengthBytes]

  newStr <- dynamicAllocate !(mkZext resultLength)
  newHeader <- mkHeader OBJECT_TYPE_ID_STR resultLength
  putObjectHeader newStr newHeader
  newStrPayload <- getObjectPayloadAddr {t=I8} newStr

  voidCall "ccc" "@llvm.memcpy.p1i8.p1i8.i64" [toIR newStrPayload, toIR startAddr, toIR !(mkZext {to=I64} resultLength), toIR (Const I1 0)]
  pure newStr

export
stringHead : IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
stringHead o1 = do
  strLength <- getStringByteLength o1
  strIsZero <- unlikely !(icmp "eq" (Const I32 0) strLength)

  mkIf (pure strIsZero) (do
        appendCode $ "call ccc void @idris_rts_crash(i64 1) noreturn"
        appendCode $ "unreachable"
        pure nullPtr
        ) (do
        payload <- getObjectPayloadAddr {t=I8} o1
        firstChar <- call {t=I32} "ccc" "@utf8_decode1" [toIR payload]
        cgMkChar firstChar
        )

export
stringTail : IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
stringTail o1 = do
  strLength <- getStringLength o1
  strIsZero <- unlikely !(icmp "eq" strLength (Const I32 0))

  mkIf (pure strIsZero) (do
    appendCode $ "call ccc void @idris_rts_crash(i64 17) noreturn"
    appendCode $ "unreachable"
    pure nullPtr
    ) (do
    mkSubstring o1 (Const I64 1) !(mkSub !(mkZext strLength) (Const I64 1))
    )

export
stringAppend : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
stringAppend o1 o2 = do
  l1 <- getObjectSize o1
  l2 <- getObjectSize o2
  newLength <- mkAddNoWrap l1 l2
  newStr <- dynamicAllocate !(mkZext newLength)
  newHeader <- mkHeader OBJECT_TYPE_ID_STR newLength

  str1 <- getObjectPayloadAddr {t=I8} o1
  str2 <- getObjectPayloadAddr {t=I8} o2

  l1_64 <- mkZext {to=I64} l1
  l2_64 <- mkZext {to=I64} l2
  newStrPayload1 <- getObjectPayloadAddr {t=I8} newStr
  newStrPayload2 <- getElementPtr newStrPayload1 l1_64

  appendCode $ "  call void @llvm.memcpy.p1i8.p1i8.i64(" ++ toIR newStrPayload1 ++ ", " ++ toIR str1 ++ ", " ++ toIR l1_64 ++ ", i1 false)"
  appendCode $ "  call void @llvm.memcpy.p1i8.p1i8.i64(" ++ toIR newStrPayload2 ++ ", " ++ toIR str2 ++ ", " ++ toIR l2_64 ++ ", i1 false)"

  putObjectHeader newStr newHeader
  pure newStr

export
stringReverse : IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
stringReverse strObj = do
  length <- getObjectSize strObj
  newStr <- dynamicAllocate !(mkZext length)
  newHeader <- mkHeader OBJECT_TYPE_ID_STR length

  origPayload <- getObjectPayloadAddr {t=I8} strObj
  newStrPayload <- getObjectPayloadAddr {t=I8} newStr

  length64 <- mkZext {to=I64} length
  appendCode $ "  call ccc void @rapid_strreverse(" ++ toIR newStrPayload ++ ", " ++ toIR origPayload ++ ", " ++ toIR length64 ++ ")"

  putObjectHeader newStr newHeader
  pure newStr

export
stringCons : IRValue IRObjPtr -> IRValue IRObjPtr -> Codegen (IRValue IRObjPtr)
stringCons charObj strObj = do
  charVal32 <- unboxChar' charObj
  l32 <- getStringByteLength strObj
  -- maximum length of one codepoint in UTF-8 is 4 bytes
  newLength <- mkAddNoWrap (Const I32 4) l32
  newStr <- dynamicAllocate !(mkZext newLength)
  putObjectHeader newStr !(mkHeader OBJECT_TYPE_ID_STR newLength)

  str2 <- getObjectPayloadAddr {t=I8} strObj

  newStrPayload1 <- getObjectPayloadAddr {t=I8} newStr

  charLength <- call {t=I32} "ccc" "@utf8_encode1" [toIR newStrPayload1, toIR charVal32]

  newStrPayload2 <- getElementPtr newStrPayload1 charLength
  appendCode $ "  call void @llvm.memcpy.p1i8.p1i8.i64(" ++ toIR newStrPayload2 ++ ", " ++ toIR str2 ++ ", " ++ toIR !(mkZext {to=I64} l32) ++ ", i1 false)"
  realNewLength <- mkAddNoWrap charLength l32
  putObjectHeader newStr !(mkHeader OBJECT_TYPE_ID_STR realNewLength)
  pure newStr


text:
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

%name Vect xs, ys, zs

replicate : {m : Nat} -> a -> Vect m a

transpose : {m : Nat} -> Vect n (Vect m a) -> Vect m (Vect n a)
transpose [] = ?transpose_rhs_1
transpose (x :: xs) = ?transpose_rhs_2


text:
module Frontend.Kotlin.AST

import Tools.AstF
import Tools.FullList
import Tools.Annotation
import Data.So
import Data.Vect

%access public export

--     _    ____ _____   _____                 _
--    / \  / ___|_   _| |  ___|   _ _ __   ___| |_ ___  _ __
--   / _ \ \___ \ | |   | |_ | | | | '_ \ / __| __/ _ \| '__|
--  / ___ \ ___) || |   |  _|| |_| | | | | (__| || (_) | |
-- /_/   \_\____/ |_|   |_|   \__,_|_| |_|\___|\__\___/|_|
--

data Operator = RefEq | RefNeq
              | StructEq | StructNeq
              | Lt | Le | Gt | Ge
              | Plus | Subs | Mult | Div | Modulo
              | And | Or

operatorLvl : Operator -> Nat
operatorLvl RefEq     = 6
operatorLvl RefNeq    = 6
operatorLvl StructEq  = 6
operatorLvl StructNeq = 6
operatorLvl Lt        = 5
operatorLvl Le        = 5
operatorLvl Gt        = 5
operatorLvl Ge        = 5
operatorLvl Plus      = 4
operatorLvl Subs      = 4
operatorLvl Mult      = 3
operatorLvl Div       = 3
operatorLvl Modulo    = 3
operatorLvl And       = 7
operatorLvl Or        = 8

Show Operator where
  show RefEq     = "==="
  show RefNeq    = "!=="
  show StructEq  = "=="
  show StructNeq = "!="
  show Lt        = "<"
  show Le        = "<="
  show Gt        = ">"
  show Ge        = ">="
  show Plus      = "+"
  show Subs      = "-"
  show Mult      = "*"
  show Div       = "/"
  show Modulo    = "%"
  show And       = "&&"
  show Or        = "||"

Ident : Type
Ident = String

data SyntaxType = TypeTy | VarTy | ParamTy | ParamCTy
                | ClassTy | FunTy | DeclTy | FileTy
                | ExprTy | BlockTy | BlockExprTy | AccessTy

data SyntaxF : (k : SyntaxType -> Type) -> (i : SyntaxType) -> Type where
  TParam  : Ident -> List (k TypeTy) -> SyntaxF k TypeTy
  TNull   : k TypeTy -> SyntaxF k TypeTy
  TFun    : List (k TypeTy) -> k TypeTy -> SyntaxF k TypeTy

  VVar    : Ident -> Maybe (k TypeTy) -> k ExprTy -> SyntaxF k VarTy
  VVal    : Ident -> Maybe (k TypeTy) -> k ExprTy -> SyntaxF k VarTy

  Param   : Ident -> k TypeTy -> SyntaxF k ParamTy

  PCVar   : Ident -> k TypeTy -> SyntaxF k ParamCTy
  PCVal   : Ident -> k TypeTy -> SyntaxF k ParamCTy

  Class   : Ident -> List Ident -> List (k ParamCTy)
         -> List (k VarTy) -> SyntaxF k ClassTy

  Fun     : List Ident -> Ident -> List (k ParamTy)
         -> k TypeTy -> k BlockTy -> SyntaxF k FunTy

  DVar    : k VarTy -> SyntaxF k DeclTy
  DClass  : k ClassTy -> SyntaxF k DeclTy
  DFun    : k FunTy -> SyntaxF k DeclTy

  File    : List (k DeclTy) -> SyntaxF k FileTy

  EInt    : Integer -> SyntaxF k ExprTy
  EStr    : String  -> SyntaxF k ExprTy
  ETrue   : SyntaxF k ExprTy
  EFalse  : SyntaxF k ExprTy
  EThis   : SyntaxF k ExprTy
  ENull   : SyntaxF k ExprTy
  EAccess : k AccessTy -> SyntaxF k ExprTy
  EAss    : k AccessTy -> k ExprTy -> SyntaxF k ExprTy
  ECall   : Ident -> List (k ExprTy) -> SyntaxF k ExprTy
  ENot    : k ExprTy -> SyntaxF k ExprTy
  EMinus  : k ExprTy -> SyntaxF k ExprTy
  EOp     : Operator -> k ExprTy -> k ExprTy -> SyntaxF k ExprTy
  EIfElse : k ExprTy -> k BlockExprTy -> k BlockExprTy -> SyntaxF k ExprTy
  EWhile  : k ExprTy -> k BlockExprTy -> SyntaxF k ExprTy
  EReturn : Maybe (k ExprTy) -> SyntaxF k ExprTy
  EFun    : List (k ParamTy) -> k TypeTy -> k BlockTy -> SyntaxF k ExprTy

  BEmpty  : SyntaxF k BlockTy
  BVar    : k VarTy -> k BlockTy -> SyntaxF k BlockTy
  BExpr   : k ExprTy -> k BlockTy -> SyntaxF k BlockTy

  BEBlock : k BlockTy -> SyntaxF k BlockExprTy
  BEExpr  : k ExprTy -> SyntaxF k BlockExprTy

  AIdent  : Ident -> SyntaxF k AccessTy
  ASub    : k ExprTy -> Ident -> SyntaxF k AccessTy
  ANSub   : k ExprTy -> Ident -> SyntaxF k AccessTy

--     _        _   _____   _           _
--    / \   ___| |_|  ___| (_)_ __  ___| |_ __ _ _ __   ___ ___
--   / _ \ / __| __| |_    | | '_ \/ __| __/ _` | '_ \ / __/ _ \
--  / ___ \\__ \ |_|  _|   | | | | \__ \ || (_| | | | | (_|  __/
-- /_/   \_\___/\__|_|     |_|_| |_|___/\__\__,_|_| |_|\___\___|
--
AstF SyntaxType SyntaxF where
  --  _              _ __  __
  -- | |___  __ __ _| |  \/  |__ _ _ __
  -- | / _ \/ _/ _` | | |\/| / _` | '_ \
  -- |_\___/\__\__,_|_|_|  |_\__,_| .__/
  --                              |_|
  localMap _ _ fn TypeTy (TParam x y) = TParam x $ map (fn TypeTy) y
  localMap _ _ fn TypeTy (TNull x)    = TNull $ fn TypeTy x
  localMap _ _ fn TypeTy (TFun xs x)  = TFun (map (fn TypeTy) xs) $ fn TypeTy x

  localMap _ _ fn VarTy (VVar x y z) = VVar x (map (fn TypeTy) y) $ fn ExprTy z
  localMap _ _ fn VarTy (VVal x y z) = VVal x (map (fn TypeTy) y) $ fn ExprTy z

  localMap _ _ fn ParamTy (Param x y) = Param x $ fn TypeTy y

  localMap _ _ fn ParamCTy (PCVar x y) = PCVar x $ (fn TypeTy) y
  localMap _ _ fn ParamCTy (PCVal x y) = PCVal x $ (fn TypeTy) y

  localMap _ _ fn ClassTy (Class x xs y ys) = Class x xs
                                                    (map (fn ParamCTy) y)
                                                    (map (fn VarTy) ys)

  localMap _ _ fn FunTy (Fun xs x ys y z) = Fun xs x (map (fn ParamTy) ys)
                                                (fn TypeTy y)
                                                (fn BlockTy z)

  localMap _ _ fn DeclTy (DVar x)   = DVar $ fn VarTy x
  localMap _ _ fn DeclTy (DClass x) = DClass $ fn ClassTy x
  localMap _ _ fn DeclTy (DFun x)   = DFun $ fn FunTy x

  localMap _ _ fn FileTy (File xs) = File $ map (fn DeclTy) xs

  localMap _ _ fn ExprTy (EInt x)        = EInt x
  localMap _ _ fn ExprTy (EStr x)        = EStr x
  localMap _ _ fn ExprTy ETrue           = ETrue
  localMap _ _ fn ExprTy EFalse          = EFalse
  localMap _ _ fn ExprTy EThis           = EThis
  localMap _ _ fn ExprTy ENull           = ENull
  localMap _ _ fn ExprTy (EAccess x)     = EAccess $ fn AccessTy x
  localMap _ _ fn ExprTy (EAss x y)      = EAss (fn AccessTy x) (fn ExprTy y)
  localMap _ _ fn ExprTy (ECall x xs)    = ECall x (map (fn ExprTy) xs)
  localMap _ _ fn ExprTy (ENot x)        = ENot $ fn ExprTy x
  localMap _ _ fn ExprTy (EMinus x)      = EMinus $ fn ExprTy x
  localMap _ _ fn ExprTy (EOp x y z)     = EOp x (fn ExprTy y) (fn ExprTy z)
  localMap _ _ fn ExprTy (EIfElse x y z) = EIfElse (fn ExprTy x)
                                                   (fn BlockExprTy y)
                                                   (fn BlockExprTy z)
  localMap _ _ fn ExprTy (EWhile x y)    = EWhile (fn ExprTy x) (fn BlockExprTy y)
  localMap _ _ fn ExprTy (EReturn x)     = EReturn $ map (fn ExprTy) x
  localMap _ _ fn ExprTy (EFun xs x y)   = EFun (map (fn ParamTy) xs)
                                                (fn TypeTy x)
                                                (fn BlockTy y)

  localMap _ _ fn BlockTy BEmpty      = BEmpty
  localMap _ _ fn BlockTy (BVar x y)  = BVar (fn VarTy x) (fn BlockTy y)
  localMap _ _ fn BlockTy (BExpr x y) = BExpr (fn ExprTy x) (fn BlockTy y)

  localMap _ _ fn BlockExprTy (BEBlock x) = BEBlock $ fn BlockTy x
  localMap _ _ fn BlockExprTy (BEExpr x)  = BEExpr  $ fn ExprTy  x

  localMap _ _ fn AccessTy (AIdent x)  = AIdent x
  localMap _ _ fn AccessTy (ASub x y)  = ASub  (fn ExprTy x) y
  localMap _ _ fn AccessTy (ANSub x y) = ANSub (fn ExprTy x) y

--     _                      _        _   _
--    / \   _ __  _ __   ___ | |_ __ _| |_(_) ___  _ __
--   / _ \ | '_ \| '_ \ / _ \| __/ _` | __| |/ _ \| '_ \
--  / ___ \| | | | | | | (_) | || (_| | |_| | (_) | | | |
-- /_/   \_\_| |_|_| |_|\___/ \__\__,_|\__|_|\___/|_| |_|
--

SyntaxAnn : SyntaxType -> Type -> Type
SyntaxAnn = Annotated SyntaxType SyntaxF

--  _____
-- |_   _|   _ _ __   ___
--   | || | | | '_ \ / _ \
--   | || |_| | |_) |  __/
--   |_| \__, | .__/ \___|
--       |___/|_|

--  _  _  ___   _   ___
-- | || |/ _ \ /_\ / __|
-- | __ | (_) / _ \\__ \
-- |_||_|\___/_/ \_\___/
--
mutual
  record KClass where
    constructor MkClass
    name    : String
    argc    : Nat
    members : List $ Pair String $ (Vect argc KType) -> KType

  record KFun where
    constructor MkFun
    name : String
    argc : Nat
    args : List $ Pair String $ Vect argc KType -> KType
    ret  : Vect argc KType -> KType

  data KType : Type where
    KTFun   : (f : KFun) -> Vect (argc f) KType -> KType
    KTNull  : KType
    KTOpt   : KType -> KType
    KTClass : (c : KClass) -> Vect (argc c) KType -> KType

record Var where
  constructor MkVar
  name  : String
  type  : KType
  scope : Nat

-- TODO replace lists by SortedMap
record Environment where
  constructor MkEnv
  classes   : List KClass
  functions : List KFun
  variables : List (List Var)

interface Named a where
  name : a -> String

Named KClass where
  name = KClass.name

Named KFun where
  name = KFun.name

Named Var where
  name = Var.name

--  _                 _                _
-- | |   _____ __ __ | |   _____ _____| |
-- | |__/ _ \ V  V / | |__/ -_) V / -_) |
-- |____\___/\_/\_/  |____\___|\_/\___|_|
--
interface Named a => Lookable t a | t where
  total lookupDef  : t -> String -> Bool
  total lookupObj  : (objs : t) -> (c : String) -> (So $ lookupDef objs c) -> a
  total insertable : Bool
  total subset     : t -> t -> Type
  total propagate  : (c : String) -> (objs1 : t) -> (objs2 : t)
                  -> subset objs1 objs -> (So $ lookupDef objs1 c)
                  -> (So $ lookupDef objs2 c)
  total insert     : So insertable -> (objs : t) -> (obj : a)
                  -> (result : t ** (Pair (So $ lookupDef result $ name obj) (subset objs result)))

total namedLookupDef : Named a => a -> String -> Bool
namedLookupDef obj nm = case decEq (name obj) nm of
                             Yes _ => True
                             No _  => False

total namedLookupObj : Named a => (obj : a) -> (nm : String) -> (So $ namedLookupDef obj nm) -> a
namedLookupObj obj nm prf with (name obj == nm)
  | True  = obj
  | False = void $ uninhabited prf

total namedSubset : Named a => a -> a -> Type
namedSubset obj1 obj2 = name obj1 = name obj2

total namedPropagate : Named a => (c : String) -> (obj1 : a) -> (obj2 : a)
                    -> namedSubset obj1 obj2 -> (So $ namedLookupDef obj1 c)
                    -> (So $ namedLookupDef obj2 c)
namedPropagate c obj1 obj2 sub prf with (name obj1 == name obj2)
  | True with (name obj1 == c) proof eqC
    | True  = ?hole
    | False = void $ uninhabited prf
  | False = ?hole2

Lookable KClass KClass where
  lookupDef  = namedLookupDef
  lookupObj  = namedLookupObj
  insertable = False
  subset     = namedSubset
Lookable KFun KFun where
  lookupDef  = namedLookupDef
  lookupObj  = namedLookupObj
  insertable = False
  subset     = namedSubset
Lookable Var Var where
  lookupDef  = namedLookupDef
  lookupObj  = namedLookupObj
  insertable = False
  subset     = namedSubset

total listLookupDef : Lookable t a => List t -> String -> Bool
listLookupDef []       _ = False
listLookupDef (h :: t) c = lookupDef h c || listLookupDef t c

Lookable t a => Lookable (List t) a where
  lookupDef = listLookupDef
  lookupObj (h :: t) c prf with (lookupDef h c) proof eq
    | True  = lookupObj h c $ replace eq prf
    | False = lookupObj t c prf
  insertable = True

--  _   _ _   _ _ _ _   _
-- | | | | |_(_) (_) |_(_)___ ___
-- | |_| |  _| | | |  _| / -_|_-<
--  \___/ \__|_|_|_|\__|_\___/__/
--
total hasClass : Environment -> String -> Type
hasClass env c = So $ lookupDef (classes env) c

total hasFun : Environment -> String -> Type
hasFun env c = So $ lookupDef (functions env) c

total hasVar : Environment -> String -> Type
hasVar env c = So $ lookupDef (variables env) c

total envClass : (e : Environment) -> (c : String) -> hasClass e c -> KClass
envClass env c prf = lookupObj (classes env) c prf

total envFun : (e : Environment) -> (c : String) -> hasFun e c -> KFun
envFun env c prf = lookupObj (functions env) c prf

total envVar : (e : Environment) -> (c : String) -> hasVar e c -> Var
envVar env c prf = lookupObj (variables env) c prf


text:
||| Vim for Idris Cheatcodes
|||
||| Ctrl-wv split window vertically
||| Ctrl-ww switch windows
|||
||| Ref : http://www.worldtimzone.com/res/vi.html
|||
||| :VimShell -> start a shell
||| idris  -> Start a REPL
|||
||| From the other windows (Idris vim mode)
|||
||| \d adds a template definition for the name declared on the current line (using :addclause).
||| \c case splits the variable at the cursor (using :casesplit).
||| \m adds the missing cases for the name at the cursor (using :addmissing).
||| \w adds a with clause (using :makewith).
||| \o invokes a proof search to solve the hole under the cursor (using :proofsearch).
||| \p invokes a proof search with additional hints to solve the hole under the cursor (using :proofsearch).
|||
||| There are also commands to invoke the type checker and evaluator:
|||
||| \t displays the type of the (globally visible) name under the cursor. In the case of a hole, this displays the context and the expected type.
||| \e prompts for an expression to evaluate.
||| \r reloads and type checks the buffer.
|||
||| Ref : http://docs.idris-lang.org/en/latest/tutorial/interactive.html#interactive-editing-in-vim
|||
||| Idris syntax : https://github.com/idris-lang/Idris-dev/blob/master/docs/reference/syntax-guide.rst
|||

|||
||| Kleene logic
||| inspied from Bool.idr
|||
module Fool

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 Undecided | F False

-- useful aliases for lazy people
T : Bool
T = True

F : Bool
F = False

||| Fuzzy Bool Representation
Fool : Type
Fool = Maybe Bool  -- Fuzzy Logic | Quantum Logic | Category Theory | Map Theory

||| 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))

||| OR operator
or : Fool -> Fool -> Fool
or (Just True)  _       = (Just True)
or (Just False) b       = b
or Nothing (Just True) = (Just True)
or Nothing _            = Nothing

||| AND operator
and : Fool -> Fool -> Fool
and (Just False) _       = (Just False)
and (Just True) b        = b
and Nothing (Just False) = (Just False)
and Nothing _            = Nothing

-- Foolean Operator Precedence
infixl 4 &&, ||, ~=>

(||) : Fool -> Fool -> Fool
(||) = or

(&&) : Fool -> Fool -> Fool
(&&) = and

||| Implication
imp : Fool -> Fool -> Fool
imp x y = (not x) || y

(~=>) : Fool -> Fool -> Fool
(~=>) = imp

-- TODO : proof
-- TODO : runnable tests (we can test all values !

-- more research :
-- Cohn algebra
-- Pradhan algebra
-- Dubrova and Muzio algebra

max_stars_repo_name: asmodehn/idris-playground

max_issues_repo_name: asmodehn/idris-playground

max_forks_repo_name: asmodehn/idris-playground


text:
||| Format decimal number into string.
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Text.Format.Digits

import Data.Nat
import Data.Fin
import Data.Primitives.Views

%default total

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

public export Digits : (base:Nat) -> Type
Digits base = (n:Int) -> {auto ok:n >= 0 && n < (cast base) = True} -> Char

upperHexdigit : Digits 16
upperHexdigit 0 = '0'
upperHexdigit 1 = '1'
upperHexdigit 2 = '2'
upperHexdigit 3 = '3'
upperHexdigit 4 = '4'
upperHexdigit 5 = '5'
upperHexdigit 6 = '6'
upperHexdigit 7 = '7'
upperHexdigit 8 = '8'
upperHexdigit 9 = '9'
upperHexdigit 10 = 'A'
upperHexdigit 11 = 'B'
upperHexdigit 12 = 'C'
upperHexdigit 13 = 'D'
upperHexdigit 14 = 'E'
upperHexdigit 15 = 'F'
upperHexdigit _ = '_' -- why i need this?

lowerHexdigit : Digits 16
lowerHexdigit 0 = '0'
lowerHexdigit 1 = '1'
lowerHexdigit 2 = '2'
lowerHexdigit 3 = '3'
lowerHexdigit 4 = '4'
lowerHexdigit 5 = '5'
lowerHexdigit 6 = '6'
lowerHexdigit 7 = '7'
lowerHexdigit 8 = '8'
lowerHexdigit 9 = '9'
lowerHexdigit 10 = 'a'
lowerHexdigit 11 = 'b'
lowerHexdigit 12 = 'c'
lowerHexdigit 13 = 'd'
lowerHexdigit 14 = 'e'
lowerHexdigit 15 = 'f'
lowerHexdigit _ = '_'  -- also this

intToDigits : (base:Nat)
            -> {base':Nat} -> {auto ok:base <= base' = True} -> Digits base'
            -> Int -> String
intToDigits base digits n = if n < 0 then pack $ go n [] else "0"
  where
    base_i : Int
    base_i = cast base

    go : Int -> List Char -> List Char
    go 0 xs = xs
    go m xs with (m `divides` base_i)
      go (_ * d + r) xs | DivBy d r prf =
        let prf' = believe_me prf
            in go (assert_smaller n d) (digits {ok=prf'} r :: xs)

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

public export DigitNum : (base:Nat) -> Type
DigitNum base = Char -> Maybe Int

hexNum : DigitNum 16
hexNum '0' = Just 0
hexNum '1' = Just 1
hexNum '2' = Just 2
hexNum '3' = Just 3
hexNum '4' = Just 4
hexNum '5' = Just 5
hexNum '6' = Just 6
hexNum '7' = Just 7
hexNum '8' = Just 8
hexNum '9' = Just 9
hexNum 'a' = Just 10
hexNum 'A' = Just 10
hexNum 'b' = Just 11
hexNum 'B' = Just 11
hexNum 'c' = Just 12
hexNum 'C' = Just 12
hexNum 'd' = Just 13
hexNum 'D' = Just 13
hexNum 'e' = Just 14
hexNum 'E' = Just 14
hexNum 'f' = Just 15
hexNum 'F' = Just 15
hexNum _ = Nothing

digitsToInt : (base:Nat)
           -> {base':Nat} -> {auto ok:base <= base' = True} -> Digits base'
           -> String -> Maybe Int
digitsToInt base digits str = go 0 $ unpack str where
  base_i : Int
  base_i = cast base

  go : Int -> List Char -> Maybe Int
  go ans [] = Just ans
  go ans (x::xs) with (hexNum x)
    go ans (x::xs) | Just x' = go (ans * base_i + x') xs
    go ans (x::xs) | Nothing = Nothing

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


text:
module OptimiseUnitary

import Data.Vect
import Data.Nat
import Unitary

simplify : Unitary n -> Unitary n -> (Unitary n, Bool)
simplify IdGate _ = (IdGate, False)
simplify _ IdGate = (IdGate, False)
simplify (H j x) (H k y) =
  if j == k then (y,True)
  else let (g,b) = simplify (H j x) y in (H k g, b)
simplify (H j x) (P p k y) =
  if j == k then (P p k y, False)
  else let (g,b) = simplify (H j x) y in (P p k g, b)
simplify (H j x) (CNOT c t y) =
  if j == c || j == t then (CNOT c t y, False)
  else let (g,b) = simplify (H j x) y in (CNOT c t g, b)
simplify (P p j x) (H k y) =
  if j == k then (H k y, False)
  else let (g,b) = simplify (P p j x) y in (H k g, b)
simplify (P p j x) (P p1 k y) =
  if j == k then (P (p + p1) k y, True)
  else let (g,b) = simplify (P p j x) y in (P p1 k g, b)
simplify (P p j x) (CNOT c t y) =
  if j == c || j == t then (CNOT c t y, False)
  else let (g,b) = simplify (P p j x) y in (CNOT c t g, b)
simplify (CNOT c t x) (H j y) =
  if j == c || j == t then (H j y, False)
  else let (g,b) = simplify (CNOT c t x) y in (H j g, b)
simplify (CNOT c t x) (P p j y) =
  if j == c || j == t then (P p j y, False)
  else let (g,b) = simplify (CNOT c t x) y in (P p j g, b)
simplify (CNOT c t x) (CNOT c1 t1 y) =
  if c == c1 && t == t1 then (y, True)
  else if c == c1 || t == t1 || c == t1 || t == c1
          then (CNOT c1 t1 y, False)
       else let (g,b) = simplify (CNOT c t x) y in (CNOT c1 t1 g, b)

optimise' : Unitary n -> (Unitary n, Bool)
optimise' IdGate = (IdGate, False)
optimise' (H j x) =
  let (g, b) = simplify (H j x) x
      (g1, b1) = optimise' g
  in if b then (g1, True)
     else (H j g1, b1)
optimise' (P p j x) =
  let (g, b) = simplify (P p j x) x
      (g1, b1) = optimise' g
  in if b then (g1, True)
     else (P p j g1, b1)
optimise' (CNOT c t x) =
  let (g, b) = simplify (CNOT c t x) x
      (g1, b1) = optimise' g
  in if b then (g1, True)
     else (CNOT c t g1, b1)

export
optimise : Unitary n -> Unitary n
optimise g =
  let (g1, b1) = optimise' g
  in if b1 then optimise g1
           else g1

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera