text:
module VISD.Common

import Control.Isomorphism
import Data.BoundedList

%logging 1
%default total
%hide Prelude.Algebra.(<*>)
%hide Prelude.Applicative.(<|>)
%hide Prelude.Vect.reverse

-- http://www.informatik.uni-marburg.de/~rendel/unparse/

-- core definitions

data PartIso : Type -> Type -> Type where
  MkPartIso : (to : a -> Maybe b) ->
              (from : b -> Maybe a) ->
              (toFrom : (y : b) -> maybe () (\x => to x = Just y) (from y)) ->
              (fromTo : (x : a) -> maybe () (\y => from y = Just x) (to x)) ->
              PartIso a b

class PartIsoFunctor (f : Type -> Type -> Type) where
  (<$>) : PartIso a b -> f a c -> f b c

class PFunctor (f : Type -> Type -> Type) where
  (<*>) : f a c -> Lazy (f b c) -> f (a, b) c

class PAlternative (f : Type -> Type -> Type) where
  (<|>) : f a c -> Lazy (f a c) -> f a c
  empty : f a c

class (PartIsoFunctor d, PFunctor d, PAlternative d) => Syntax (d : Type -> Type -> Type) c where
  pure : Eq a => a -> d a c
  item : d c c

-- helper functions

ipc_inverse : PartIso a b -> PartIso b a
ipc_inverse (MkPartIso f g tf ft) = MkPartIso g f ft tf

ipc_apply : PartIso a b -> a -> Maybe b
ipc_apply (MkPartIso f g ft ft) = f

ipc_unapply : PartIso a b -> b -> Maybe a
ipc_unapply = ipc_apply . ipc_inverse

-- Inspect and other stuff

data Inspect : a -> Type where
  wi : {A : Type} -> (x : A) -> (y : A) -> (eq: x = y) -> Inspect x

inspect : {A : Type} -> (x : A) -> Inspect x
inspect x = wi x _ Refl

match : {A : Type} -> {x : A} -> (y : A) -> {eq : x = y} -> Inspect x
match y {eq} = wi _ y eq

maybe_assoc : (x : Maybe a) -> (f : a -> Maybe b) -> (g : b -> Maybe c) -> (x >>= (\y => f y >>= g)) = (x >>= f >>= g)
maybe_assoc Nothing f g = Refl
maybe_assoc (Just x) f g = Refl

maybe_unbind : (f : a -> Maybe b) -> (g : b -> Maybe c) -> (x : a) -> {y : b} ->
  (f x = Just y) -> g y = Just x >>= f >>= g
maybe_unbind f g x eq = rewrite eq in Refl

-- Algebra

infixr 1 >=>
(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
f >=> g = \x => f x >>= g

pId : PartIso a a
pId = MkPartIso (\x => Just x) (\x => Just x) (\x => Refl) (\x => Refl)

infixl 9 ..
(..) : PartIso b c -> PartIso a b -> PartIso a c
(MkPartIso gTo gFrom gTF gFT) .. (MkPartIso fTo fFrom fTF fFT) =
  MkPartIso
    (ipc_apply (MkPartIso fTo fFrom fTF fFT) >=> ipc_apply (MkPartIso gTo gFrom gTF gFT))
    (ipc_unapply (MkPartIso gTo gFrom gTF gFT) >=> ipc_unapply (MkPartIso fTo fFrom fTF fFT))
    tf ft
  where
    tf y with (inspect $ (gFrom y))
      | match Nothing {eq} = rewrite eq in ()
      | match (Just z) {eq} = rewrite eq in case (inspect $ fFrom z) of
        match Nothing {eq=eq1} => rewrite eq1 in ()
        match (Just n) {eq=eq1} => rewrite eq1 in
          rewrite (replace eq1 {P=(\pz => maybe () (\x => fTo x = Just z) pz)} (fTF z)) in
            (replace eq {P=(\py => maybe () (\x => gTo x = Just y) py)} (gTF y))
    ft x with (inspect $ (fTo x))
      | match Nothing {eq} = rewrite eq in ()
      | match (Just z) {eq} = rewrite eq in case (inspect $ gTo z) of
        match Nothing {eq=eq1} => rewrite eq1 in ()
        match (Just n) {eq=eq1} => rewrite eq1 in
          rewrite (replace eq1 {P=(\pz => maybe () (\x => gFrom x = Just z) pz)} (gFT z)) in
            (replace eq {P=(\py => maybe () (\y => fFrom y = Just x) py)} (fFT x))

commute : PartIso (a, b) (b, a)
commute = MkPartIso f f (\(a,b) => Refl) (\(a,b) => Refl) where
  f : (c, d) -> Maybe (d, c)
  f (a, b) = Just (b, a)

unit : {a : Type} -> PartIso a (a, ())
unit = MkPartIso f g tf ft where
  f : {a : Type} -> a -> Maybe (a, ())
  f a = Just (a, ())
  g : {a : Type} -> (a, ()) -> Maybe a
  g (a, ()) = Just a
  tf (a, ()) = Refl
  ft a = Refl

-- *>, <*

infixl 3 *>
(*>) : Syntax d c => d () c -> d a c -> d a c
p *> q = ipc_inverse unit .. commute <$> p <*> q

infixl 3 <*
(<*) : Syntax d c => d a c -> d () c -> d a c
p <* q = ipc_inverse unit <$> p <*> q

-- the following function can't be verified: there's no isomorphism
-- when we are ignoring input; neither can it be changed, because it's
-- quite important to be able to ignore input

ignore : a -> PartIso a ()
ignore x = MkPartIso f g tf ft where
  f : a -> Maybe ()
  f y = Just ()
  g : () -> Maybe a
  g () = Just x
  tf () = Refl
  ft y = believe_me (Just x = Just y)

-- Parser

data Parser a c = MkParser (List c -> Maybe (a, List c))

parse : Parser a c -> List c -> Maybe a
parse (MkParser p) s = p s >>= pure . fst

instance PartIsoFunctor Parser where
  iso <$> (MkParser p) = MkParser pf
  where
    pf l = do
      (x, rest) <- p l
      y <- ipc_apply iso x
      return (y, rest)

instance PFunctor Parser where
  (MkParser p) <*> mkpq = MkParser pf
  where
    pf l = do
      (x, rest) <- p l
      case mkpq of
        (MkParser q) => do
          (y, ret) <- q rest
          return ((x, y), ret)

instance PAlternative Parser where
  (MkParser p) <|> mkpq = MkParser pf
  where
    pf l = case p l of
      Just x => Just x
      Nothing => case mkpq of
        (MkParser q) => q l
  empty = MkParser (\s => Nothing)

instance Syntax Parser c where
  pure x = MkParser (\s => Just (x, s))
  item = MkParser f
  where
    f [] = Nothing
    f (x :: xs) = Just (x, xs)

-- Printer

data Printer a c = MkPrinter (a -> Maybe (List c))

compose : Printer a c -> a -> Maybe (List c)
compose (MkPrinter p) x = p x

instance PartIsoFunctor Printer where
  iso <$> (MkPrinter p) = MkPrinter (\b => ipc_unapply iso b >>= p)

instance PFunctor Printer where
  (MkPrinter p) <*> mkpq = MkPrinter pf
  where
    pf (x, y) = do
      x' <- p x
      case mkpq of
        (MkPrinter q) => do
          y' <- q y
          return (x' ++ y')

instance PAlternative Printer where
  (MkPrinter p) <|> mkpq = MkPrinter $ \s =>
    case (p s) of
      Nothing => case mkpq of
        (MkPrinter q) => q s
      x => x
  empty = MkPrinter (\s => Nothing)

instance Syntax Printer c where
  pure x = MkPrinter (\y =>
    if x == y
    then Just []
    else Nothing)
  item = MkPrinter (\t => Just [t])

-- Basic parsers/composers

sat : Syntax d a => (a -> Bool) -> d a a
sat {a} p = (MkPartIso check check verify verify) <$> item
  where
    check : a -> Maybe a
    check x = if p x then Just x else Nothing
    verify y with (inspect $ p y)
      | match False {eq=eq} = rewrite eq in ()
      | match True {eq=eq} = rewrite eq in
        rewrite eq in Refl

val : (Syntax d a, Eq a) => a -> d a a
val x = sat (== x)

-- rep

nilv : PartIso () (Vect 0 a)
nilv = MkPartIso to from tf ft
  where
    to : () -> Maybe (Vect 0 a)
    to () = Just $ Vect.Nil {a=a}
    from : (Vect 0 a) -> Maybe ()
    from [] = Just ()
    from _ = Nothing
    tf [] = Refl
    ft () = Refl

consv : PartIso (a, Vect n a) (Vect (S n) a)
consv = MkPartIso c1 c2 tf ft
  where
    c1 : (a, Vect n a) -> Maybe (Vect (S n) a)
    c1 (x, xs) = Just (x :: xs)
    c2 : (Vect (S n) a) -> Maybe (a, Vect n a)
    c2 (x :: xs) = Just (x, xs)
    tf (x :: xs) = Refl
    ft (a, b) = Refl

rep : Syntax d c => (n : Nat) -> d a c -> d (Vect n a) c
rep Z p = nilv <$> pure ()
rep (S k) p = consv <$> p <*> rep k p

-- up to

bNil : PartIso () (BoundedList n a)
bNil = MkPartIso to from tf ft
  where
    to : () -> Maybe (BoundedList n a)
    to () = Just []
    from : BoundedList n a -> Maybe ()
    from [] = Just ()
    from _ = Nothing
    tf [] = Refl
    tf (x::xs) impossible
    ft () = Refl

bCons : PartIso (a, BoundedList n a) (BoundedList (S n) a)
bCons = MkPartIso to from tf ft
  where
    to : (a, BoundedList n a) -> Maybe (BoundedList (S n) a)
    to (x, l) = Just $ x :: l
    from : BoundedList (S n) a -> Maybe (a, BoundedList n a)
    from [] = Nothing
    from (x :: xs) = Just (x, xs)
    tf [] = ()
    tf (x :: xs) = Refl
    ft (x, l) = Refl

upTo : Syntax d c => (n: Nat) -> d a c -> d (BoundedList n a) c
upTo Z _ = (bNil <$> pure ())
upTo (S n) p = (bCons <$> (p <*> (upTo n p)))
           <|> (bNil <$> pure ())

bounded : Syntax d c => (min,add: Nat) -> d a c -> d (Vect min a, BoundedList add a) c
bounded min add p = rep min p <*> upTo add p

-- maybe

just : PartIso a (Maybe a)
just = MkPartIso (Just . Just) id tf ft
  where
    tf Nothing = ()
    tf (Just x) = Refl
    ft _ = Refl

nothing : PartIso () (Maybe a)
nothing = MkPartIso to from tf ft
  where
    to : () -> Maybe (Maybe a)
    to x = Just Nothing
    from : Maybe a -> Maybe ()
    from (Just x) = Nothing
    from Nothing = Just ()
    tf (Just x) = ()
    tf Nothing = Refl
    ft () = Refl

maybe : Syntax d c => d a c -> d (Maybe a) c
maybe p = (just <$> p)
      <|> (nothing <$> pure ())

-- many

nil : PartIso () (List a)
nil = MkPartIso c1 c2 tf ft
  where
    c1 : () -> Maybe (List a)
    c1 () = Just []
    c2 : List a -> Maybe ()
    c2 [] = Just ()
    c2 (x :: xs) = Nothing
    tf [] = Refl
    tf (x :: xs) = ()
    ft () = Refl

cons : PartIso (a, List a) (List a)
cons = MkPartIso c1 c2 tf ft
  where
    c1 : (a, List a) -> Maybe (List a)
    c1 (x, l) = Just $ x :: l
    c2 : List a -> Maybe (a, List a)
    c2 [] = Nothing
    c2 (x :: xs) = Just (x, xs)
    tf [] = ()
    tf (x :: xs) = Refl
    ft (x, l) = Refl

partial many : Syntax d c => d a c -> d (List a) c
many p = (cons <$> (p <*> (many p)))
     <|> (nil <$> pure ())

-- sepBy1

partial sepBy1 : Syntax d c => d a c -> d b c -> b -> d (List a) c
sepBy1 p s x = cons <$> (p <*> (many ((ignore x <$> s) *> p)))

max_stars_repo_name: defanor/parcomb

max_issues_repo_name: defanor/parcomb

max_forks_repo_name: defanor/parcomb


text:
module Server.QuickFix

import Core.Context
import Core.Core
import Core.Env
import Core.FC
import Core.Metadata
import Data.List
import Data.List1
import Data.String
import Idris.Pretty
import Idris.REPL.Opts
import Idris.Resugar
import Idris.Syntax
import Language.LSP.Message
import Language.JSON
import Server.Configuration
import Server.Diagnostics
import Server.Utils
import Server.Log

pShowMN : {vars : _} -> Term vars -> Env t vars -> Doc IdrisAnn -> Doc IdrisAnn
pShowMN (Local _ _ _ p) env acc =
  case dropAllNS (nameAt p) of
       MN _ _ => acc <++> parens ("implicitly bound at" <++> pretty (getBinderLoc p env))
       _      => acc
pShowMN _ _ acc = acc

pshow : {vars : _}
     -> Ref Ctxt Defs
     => Ref Syn SyntaxInfo
     => Env Term vars
     -> Term vars
     -> Core String
pshow env tm
    = do defs <- get Ctxt
         ntm <- normaliseHoles defs env tm
         itm <- resugar env ntm
         pure $ show (pShowMN ntm env $ prettyTerm itm)

addMissingCases : Ref Ctxt Defs
               => Ref Syn SyntaxInfo
               => String -> List ClosedTerm -> Nat -> Core String
addMissingCases n [] k = pure ""
addMissingCases n (x :: xs) k =
  [| pure "\{!(pshow [] x)} = ?\{n}_missing_case_\{show k}\n" ++ addMissingCases n xs (S k) |]

findBlankLine : List String -> Int -> Int
findBlankLine [] acc = acc
findBlankLine (x :: xs) acc = if trim x == "" then acc else findBlankLine xs (acc + 1)

export
findQuickfix : Ref LSPConf LSPConfiguration
            => Ref Ctxt Defs
            => Ref Syn SyntaxInfo
            => Ref ROpts REPLOpts
            => Ref MD Metadata
            => (caps : Maybe PublishDiagnosticsClientCapabilities)
            -> (uri : URI)
            -> Error
            -> Core ()
findQuickfix caps uri (WhenUnifying fc _ x y err) = findQuickfix caps uri err
findQuickfix caps uri (InType _ _ err) = findQuickfix caps uri err
findQuickfix caps uri (InCon _ _ err) = findQuickfix caps uri err
findQuickfix caps uri (InLHS _ _ err) = findQuickfix caps uri err
findQuickfix caps uri (InRHS _ _ err) = findQuickfix caps uri err
findQuickfix caps uri (MaybeMisspelling err _) = findQuickfix caps uri err
findQuickfix caps uri err@(PatternVariableUnifies fc env n tm) = do
  whenJust (isNonEmptyFC (getLoc tm)) $ \fc => do
    diagnostic <- toDiagnostic caps uri err
    let textEdit = MkTextEdit (cast fc) (nameRoot n)
    let workspaceEdit = MkWorkspaceEdit { changes           = Just (singleton uri [textEdit])
                                        , documentChanges   = Nothing
                                        , changeAnnotations = Nothing
                                        }
    let codeAction = MkCodeAction { title       = "QuickFix: unify pattern names"
                                  , kind        = Just QuickFix
                                  , diagnostics = Just [diagnostic]
                                  , isPreferred = Just True
                                  , disabled    = Nothing
                                  , edit        = Just workspaceEdit
                                  , command     = Nothing
                                  , data_       = Nothing
                                  }
    modify LSPConf (record { quickfixes $= (codeAction ::) })
findQuickfix caps uri err@(ValidCase fc _ (Left tm)) =
  whenJust (isNonEmptyFC fc) $ \fc => do
    Just (f, args) <- (uncons' <=< init' <=< map words) <$> (getSourceLine (startLine fc + 1))
      | Nothing => do logString Debug "findQuickfix: error while fetching source line"
                      pure ()
    let line = unwords $ f :: args ++ ["=", "?\{f}_rhs_not_impossible"]
    diagnostic <- toDiagnostic caps uri err
    let textEdit = MkTextEdit (cast fc) line
    let workspaceEdit = MkWorkspaceEdit { changes           = Just (singleton uri [textEdit])
                                        , documentChanges   = Nothing
                                        , changeAnnotations = Nothing
                                        }
    let codeAction = MkCodeAction { title       = "QuickFix: remove impossible keyword"
                                  , kind        = Just QuickFix
                                  , diagnostics = Just [diagnostic]
                                  , isPreferred = Just True
                                  , disabled    = Nothing
                                  , edit        = Just workspaceEdit
                                  , command     = Nothing
                                  , data_       = Nothing
                                  }
    modify LSPConf (record { quickfixes $= (codeAction ::) })
findQuickfix caps uri err@(NotCovering fc n (MissingCases cs)) = do
  whenJust (isNonEmptyFC fc) $ \fc => do
    cases <- addMissingCases !(prettyName n) cs 1
    let startline = startLine fc
    let endline = endLine fc
    src <- String.lines <$> getSource
    let blank = findBlankLine (drop (integerToNat (cast endline)) src) endline
    diagnostic <- toDiagnostic caps uri err
    let range = MkRange (MkPosition blank 0) (MkPosition blank 0)
    let textEdit = MkTextEdit range cases
    let workspaceEdit = MkWorkspaceEdit { changes           = Just (singleton uri [textEdit])
                                        , documentChanges   = Nothing
                                        , changeAnnotations = Nothing
                                        }
    let missingCodeAction = MkCodeAction { title       = "QuickFix: add missing cases"
                                         , kind        = Just QuickFix
                                         , diagnostics = Just [diagnostic]
                                         , isPreferred = Just True
                                         , disabled    = Nothing
                                         , edit        = Just workspaceEdit
                                         , command     = Nothing
                                         , data_       = Nothing
                                         }
    let range = MkRange (MkPosition startline 0) (MkPosition startline 0)
    let textEdit = MkTextEdit range "partial\n"
    let workspaceEdit = MkWorkspaceEdit { changes           = Just (singleton uri [textEdit])
                                        , documentChanges   = Nothing
                                        , changeAnnotations = Nothing
                                        }
    let partialCodeAction = MkCodeAction { title       = "QuickFix: add partial annotation"
                                         , kind        = Just QuickFix
                                         , diagnostics = Just [diagnostic]
                                         , isPreferred = Just False
                                         , disabled    = Nothing
                                         , edit        = Just workspaceEdit
                                         , command     = Nothing
                                         , data_       = Nothing
                                         }
    modify LSPConf (record { quickfixes $= (\qf => missingCodeAction :: partialCodeAction :: qf) })
findQuickfix caps uri err@(NotCovering fc n _) = do
  whenJust (isNonEmptyFC fc) $ \fc => do
    diagnostic <- toDiagnostic caps uri err
    let startline = startLine fc
    let range = MkRange (MkPosition startline 0) (MkPosition startline 0)
    let textEdit = MkTextEdit range "partial\n"
    let workspaceEdit = MkWorkspaceEdit { changes           = Just (singleton uri [textEdit])
                                        , documentChanges   = Nothing
                                        , changeAnnotations = Nothing
                                        }
    let codeAction = MkCodeAction { title       = "QuickFix: add partial annotation"
                                  , kind        = Just QuickFix
                                  , diagnostics = Just [diagnostic]
                                  , isPreferred = Just False
                                  , disabled    = Nothing
                                  , edit        = Just workspaceEdit
                                  , command     = Nothing
                                  , data_       = Nothing
                                  }
    modify LSPConf (record { quickfixes $= (codeAction ::) })
findQuickfix caps uri err@(NotTotal fc n _) = do
  whenJust (isNonEmptyFC fc) $ \fc => do
    diagnostic <- toDiagnostic caps uri err
    let startline = startLine fc
    let range = MkRange (MkPosition startline 0) (MkPosition startline 0)
    let textEdit = MkTextEdit range "covering\n"
    let workspaceEdit = MkWorkspaceEdit { changes           = Just (singleton uri [textEdit])
                                        , documentChanges   = Nothing
                                        , changeAnnotations = Nothing
                                        }
    let codeAction = MkCodeAction { title       = "QuickFix: add covering annotation"
                                  , kind        = Just QuickFix
                                  , diagnostics = Just [diagnostic]
                                  , isPreferred = Just False
                                  , disabled    = Nothing
                                  , edit        = Just workspaceEdit
                                  , command     = Nothing
                                  , data_       = Nothing
                                  }
    modify LSPConf (record { quickfixes $= (codeAction ::) })
findQuickfix _ _ _ = pure ()

ext: idr


text:
------------- Example 1 ----------------
natInjective : (x, y : Nat) -> S x === S y -> x === y
natInjective x x Refl = Refl

succNotZero : (x : Nat) -> Not (S x === Z)
succNotZero x Refl impossible

peanoNat : (a  : Type
        ** n0  : a
        ** ns  : a -> a
        ** inj : ((x, y : a) -> ns x === ns y -> x === y)
        **       (x : a) -> Not (ns x === n0))
peanoNat = MkDPair
             Nat
         $ MkDPair
             Z
         $ MkDPair -- {a = Nat -> Nat}
             S
         $ MkDPair
             natInjective
             succNotZero

------------- Example 2 ----------------
ac : forall r. ((x : a) -> (y : b ** r x y)) -> (f : a -> b ** (x : a) -> r x (f x))
ac g = (\x => fst (g x) ** \x => snd (g x))

------------- Example 3 ----------------
idid1 : forall A. (f : A -> A ** (x : A) -> f x = x)
idid1 = MkDPair id (\x => Refl)


text:
module Replica.Option.Global

import Data.List
import Data.String

import Replica.Help
import Replica.Option.Types
import Replica.Other.Decorated

public export
data LogLevel = Debug | Info | Warning | Critical

export
Show LogLevel where
  show Debug = "Debug"
  show Info = "Info"
  show Warning = "Warning"
  show Critical = "Critical"

levelToNat : LogLevel -> Nat
levelToNat Debug = 0
levelToNat Info = 1
levelToNat Warning = 2
levelToNat Critical = 3

public export
data DiffCommand
  = Native
  | Diff
  | GitDiff
  | Custom String

export
Show DiffCommand where
  show Native = "Native"
  show Diff = "Diff"
  show GitDiff = "GitDiff"
  show (Custom x) = "Custom \{show x}"

export
Eq LogLevel where
  (==) = (==) `on` levelToNat

export
Ord LogLevel where
  compare = compare `on` levelToNat

public export
record Global' (f : Type -> Type) where
  constructor MkGlobal
  replicaDir : f String
  colour : f Bool
  ascii : f Bool
  logLevel : f (Maybe LogLevel)
  diff : f DiffCommand
  file : f String

public export
Global : Type
Global = Done Global'

export
Show Global where
  show x = unwords
    [ "MkGlobal"
    , show x.replicaDir
    , show x.colour
    , show x.ascii
    , show x.logLevel
    , show x.diff
    , show x.file
    ]

export
TyMap Global' where
  tyMap func x = MkGlobal
    (func x.replicaDir) (func x.colour)
    (func x.ascii) (func x.logLevel)
    (func x.diff) (func x.file)

export
TyTraversable Global' where
  tyTraverse func x =
    [| MkGlobal
    (func x.replicaDir) (func x.colour)
    (func x.ascii) (func x.logLevel)
    (func x.diff) (func x.file)
    |]

replicaDirPart : Part (Builder Global') String
replicaDirPart = inj $ MkOption
  (singleton $ MkMod (singleton "replica-dir") []
      (Right $ MkValue "DIR" Just)
      "set the location of replica store (default: \".replica\")")
  ".replica"
  go
  where
    go : String -> Builder Global' -> Either String (Builder Global')
    go = one replicaDir (\x => record {replicaDir = Right x})
                 (\x, y => "More than one replica dir were given: \{y}, \{x}")

logLevelPart : Part (Builder Global') (Maybe LogLevel)
logLevelPart = inj $ MkOption
  (toList1
    [ MkMod (singleton "log") [] (Right logLevelValue)
        #"""
        define the log level of the application
        available values: <none, debug, info, warning, critical> (default: none)
        """#
    , MkMod (singleton "verbose") ['v'] (Left $ Just Info)
        "similar to --log info"
    ])
  Nothing
  go
  where
    logLevelValue : Value (Maybe LogLevel)
    logLevelValue = MkValue "logLevel" (go . toLower)
      where
        go : String -> Maybe (Maybe LogLevel)
        go "none" = Just Nothing
        go "debug" = Just $ Just Debug
        go "info" = Just $ Just Info
        go "warning" = Just $ Just Warning
        go "critical" = Just $ Just Critical
        go _ = Nothing
    go : Maybe LogLevel -> Builder Global' -> Either String (Builder Global')
    go = ifSame logLevel (\x => record {logLevel = Right $ x})
                         (const $ const "Contradictory log level")

colourPart : Part (Builder Global') Bool
colourPart = inj $ MkOption
      (toList1
        [ MkMod (toList1 ["color", "colour"]) ['c'] (Left True)
            "activate colour in output (default)"
        , MkMod (toList1 ["no-color", "no-colour"]) [] (Left False)
            "desactivate colour in output"
        ])
      True
      go
    where
    go : Bool -> Builder Global' -> Either String (Builder Global')
    go = ifSame colour (\x => record {colour = Right $ x})
                       (const $ const "Contradictory colour settings")

asciiPart : Part (Builder Global') Bool
asciiPart = inj $ MkOption
      (toList1
        [ MkMod (singleton "utf8") [] (Left False)
            "allow emojis in reports (default)"
        , MkMod (singleton "ascii") [] (Left True)
             "use only ascii in reports (unless there are some in your test file)"
        ])
      False
      go
      where
      go : Bool -> Builder Global' -> Either String (Builder Global')
      go = ifSame ascii (\x => record {ascii = Right $ x})
                        (const $ const "Contradictory ascii settings")

diffPart : Part (Builder Global') DiffCommand
diffPart = inj $ MkOption
  (toList1 [ MkMod (singleton "diff") ['d'] (Right parseDiff)
     #"""
     diff command use to display difference between the given and the golden one
     available values: <git|diff|native|custom_command> (default : native)
     """#])
  Native
  compose
  where
    go : String -> DiffCommand
    go "native" = Native
    go "git" = GitDiff
    go "diff" = Diff
    go x = Custom x
    parseDiff : Value DiffCommand
    parseDiff = MkValue "CMD" (Just . go . toLower)
    compose : DiffCommand -> Builder Global' -> Either String (Builder Global')
    compose = one diff (\x => record {diff = Right x})
                  (\x, y => "More than one diff command were given: \{show y}, \{show x}")

export
fileParamPart : Part (Builder Global') String
fileParamPart = inj $ MkParam "JSON_FILE" Just go
  where
    go : String -> Builder Global' -> Either String (Builder Global')
    go = one file
             (\x => record {file = Right x})
             (\x, y => "More than one test file were given: \{y}, \{x}")

export
optParseGlobal : OptParse (Builder Global') Global
optParseGlobal =
  [| MkGlobal
    (liftAp replicaDirPart)
    (liftAp colourPart)
    (liftAp asciiPart)
    (liftAp logLevelPart)
    (liftAp diffPart)
    (liftAp fileParamPart)
  |]

export
defaultGlobal : Default Global'
defaultGlobal =
  MkGlobal
    (defaultPart replicaDirPart)
    (defaultPart colourPart)
    (defaultPart asciiPart)
    (defaultPart logLevelPart)
    (defaultPart diffPart)
    (defaultPart fileParamPart)

export
globalOptionsHelp : List1 Help
globalOptionsHelp = toList1 {ok = ?trustMe}
  $ runApM (\p => partHelp p) optParseGlobal

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
-----------------------------------------------------------------------------
  -- -
  -- Module    : Core.Types
  -- Copyright : (c) Jeffrey Young
  -- License   : BSD3
  -- Maintainer: youngjef@oregonstate.edu
  -- Stability : experimental
  --
  -- Internal types for the fgli library in Idris
  -- TODO: Make this description much much better
  -----------------------------------------------------------------------------

module Types where

interface Graph gr where

max_stars_repo_name: doyougnu/fgli

max_issues_repo_name: doyougnu/fgli

max_forks_repo_name: doyougnu/fgli


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

||| Qualitative evaluations for
module GRL.Eval.Qualitative

import GRL.Common
import GRL.Model

%access public export

implementation [andSN] Cast SValue Nat where
  cast DENIED    = cast 0
  cast CONFLICT  = cast 1
  cast UNDECIDED = cast 1
  cast WEAKDEN   = cast 2
  cast NONE      = cast 3
  cast WEAKSATIS = cast 4
  cast SATISFIED = cast 5

implementation [andNS] Cast Nat SValue where
  cast Z                     = DENIED
  cast (S Z)                 = UNDECIDED
  cast (S (S Z))             = WEAKDEN
  cast (S (S (S Z)))         = NONE
  cast (S (S (S (S Z))))     = WEAKSATIS
  cast (S (S (S (S (S Z))))) = SATISFIED
  cast _                     = UNDECIDED

||| Calculate AND decomposition
getDecompAnd : List SValue -> SValue
getDecompAnd ss = cast @{andNS} $ foldl (\olds,s => min (toNat s) olds) (cast 5) ss
  where
    toNat : SValue -> Nat
    toNat sv = cast @{andSN} sv

implementation [orSN] Cast SValue Nat where
  cast DENIED    = cast 0
  cast WEAKDEN   = cast 1
  cast NONE      = cast 2
  cast WEAKSATIS = cast 3
  cast CONFLICT  = cast 4
  cast UNDECIDED = cast 4
  cast SATISFIED = cast 5

implementation [orNS] Cast Nat SValue where
  cast Z                     = DENIED
  cast (S Z)                 = WEAKDEN
  cast (S (S Z))             = NONE
  cast (S (S (S Z)))         = WEAKSATIS
  cast (S (S (S (S Z))))     = UNDECIDED
  cast (S (S (S (S (S Z))))) = SATISFIED
  cast _                     = UNDECIDED

||| Calculate IOR decomposition.
getDecompIOR : List SValue -> SValue
getDecompIOR ss = cast @{orNS} $ foldl (\olds,s => max (toNat s) olds) (cast 0) ss
  where
    toNat : SValue -> Nat
    toNat sv = cast @{orSN} sv

||| Calculate XOR decomposition.
getDecompXOR : List SValue -> SValue
getDecompXOR ss = cast @{orNS} $ foldl (\olds,s => min (toNat s) olds) (cast 5) ss
  where
    toNat : SValue -> Nat
    toNat sv = cast @{orSN} sv

||| Record to keep track of contribution valeu counts.
record ContribCount where
  constructor MkCCount
  noSatis  : Nat
  noWeakS  : Nat
  noWeakD  : Nat
  noDenied : Nat
  noUndec  : Nat

||| Default constructor for `ContribCount`
defCCount : ContribCount
defCCount = MkCCount Z Z Z Z Z

||| Implementation of `AdjustContributionCounters`
adJustCount : SValue -> ContribCount -> ContribCount
adJustCount SATISFIED cnt = record {noSatis  = (S (noSatis cnt))} cnt
adJustCount DENIED    cnt = record {noDenied = (S (noDenied cnt))} cnt
adJustCount WEAKSATIS cnt = record {noWeakS  = (S (noWeakS cnt))} cnt
adJustCount WEAKDEN   cnt = record {noWeakD  = (S (noWeakD cnt))} cnt
adJustCount UNDECIDED cnt = record {noUndec  = (S (noUndec cnt))} cnt
adJustCount _         cnt = cnt

||| Implementation of `AdjustContributionCounters` for a list of values.
adjustCounts : List SValue -> ContribCount
adjustCounts es = foldl (flip $ adJustCount) defCCount es

||| Implementation of the `WeightedContribution` look up table.
weightedContrib : SValue -> CValue -> SValue
weightedContrib x y = foldl (\res,(x',y',r') => if x == x' && y == y' then r' else res) NONE table
  where
    table : List (SValue, CValue, SValue)
    table = [ (DENIED   , MAKES  ,  DENIED   )
            , (DENIED   , HELPS  ,  WEAKDEN  )
            , (DENIED   , SOMEPOS,  WEAKDEN  )
            , (DENIED   , UNKNOWN,  NONE     )
            , (DENIED   , SOMENEG,  WEAKSATIS)
            , (DENIED   , HURTS  ,  WEAKSATIS)
            , (DENIED   , BREAK  ,  SATISFIED)
            , (WEAKDEN  , MAKES  ,  WEAKDEN  )
            , (WEAKDEN  , HELPS  ,  WEAKDEN  )
            , (WEAKDEN  , SOMEPOS,  WEAKDEN  )
            , (WEAKDEN  , UNKNOWN,  NONE     )
            , (WEAKDEN  , SOMENEG,  WEAKSATIS)
            , (WEAKDEN  , HURTS  ,  WEAKSATIS)
            , (WEAKDEN  , BREAK  ,  WEAKSATIS)
            , (WEAKSATIS, MAKES  ,  WEAKSATIS)
            , (WEAKSATIS, HELPS  ,  WEAKSATIS)
            , (WEAKSATIS, SOMEPOS,  WEAKSATIS)
            , (WEAKSATIS, UNKNOWN,  NONE     )
            , (WEAKSATIS, SOMENEG,  WEAKDEN  )
            , (WEAKSATIS, HURTS  ,  WEAKDEN  )
            , (WEAKSATIS, BREAK  ,  WEAKDEN  )
            , (SATISFIED, MAKES  ,  SATISFIED)
            , (SATISFIED, HELPS  ,  WEAKSATIS)
            , (SATISFIED, SOMEPOS,  WEAKSATIS)
            , (SATISFIED, UNKNOWN,  NONE     )
            , (SATISFIED, SOMENEG,  WEAKDEN  )
            , (SATISFIED, HURTS  ,  WEAKDEN  )
            , (SATISFIED, BREAK  ,  DENIED   )
            , (CONFLICT , MAKES  ,  UNDECIDED)
            , (CONFLICT , HELPS  ,  UNDECIDED)
            , (CONFLICT , SOMEPOS,  UNDECIDED)
            , (CONFLICT , UNKNOWN,  UNDECIDED)
            , (CONFLICT , SOMENEG,  UNDECIDED)
            , (CONFLICT , HURTS  ,  UNDECIDED)
            , (CONFLICT , BREAK  ,  UNDECIDED)
            , (UNDECIDED, MAKES  ,  UNDECIDED)
            , (UNDECIDED, HELPS  ,  UNDECIDED)
            , (UNDECIDED, SOMEPOS,  UNDECIDED)
            , (UNDECIDED, UNKNOWN,  UNDECIDED)
            , (UNDECIDED, SOMENEG,  UNDECIDED)
            , (UNDECIDED, HURTS  ,  UNDECIDED)
            , (UNDECIDED, BREAK  ,  UNDECIDED)
            , (NONE     , MAKES  ,  NONE     )
            , (NONE     , HELPS  ,  NONE     )
            , (NONE     , SOMEPOS,  NONE     )
            , (NONE     , UNKNOWN,  NONE     )
            , (NONE     , SOMENEG,  NONE     )
            , (NONE     , HURTS  ,  NONE     )
            , (NONE     , BREAK  ,  NONE     )]

||| Implementation of the `CompareSatisfiedAndDenied`  resolution
cmpSatAndDen : ContribCount -> SValue
cmpSatAndDen cnt =
  if noSatis cnt > 0 && noDenied cnt > 0
    then CONFLICT
    else if noSatis cnt > 0 && noDenied cnt == 0
      then SATISFIED
      else if noDenied cnt > 0 && noSatis cnt == 0
        then DENIED
        else if noSatis cnt == 0 && noDenied cnt == 0
          then NONE
          else NONE

||| Implementation of the `CompareWSandWD` function
cmpWSandWD : ContribCount -> SValue
cmpWSandWD cnt =
  if noWeakS cnt > noWeakD cnt
    then WEAKSATIS
    else if noWeakD cnt > noWeakS cnt
      then WEAKDEN
      else if noWeakD cnt == noWeakS cnt
        then NONE
        else NONE

||| Implementation of the `CombineContributionutions` function
combineContribs : ContribCount -> SValue
combineContribs c = doCombine (cmpWSandWD c) (cmpSatAndDen c)
  where
    table : List (SValue, SValue, SValue)
    table =[ (WEAKDEN  , DENIED   , DENIED   )
           , (WEAKDEN  , SATISFIED, WEAKSATIS)
           , (WEAKDEN  , CONFLICT , CONFLICT )
           , (WEAKDEN  , NONE     , WEAKDEN  )
           , (WEAKSATIS, DENIED   , WEAKDEN  )
           , (WEAKSATIS, SATISFIED, SATISFIED)
           , (WEAKSATIS, CONFLICT , CONFLICT )
           , (WEAKSATIS, NONE     , WEAKSATIS)
           , (NONE     , DENIED   , DENIED   )
           , (NONE     , SATISFIED, SATISFIED)
           , (NONE     , CONFLICT , CONFLICT )
           , (NONE     , NONE     , NONE     )]

    doCombine : SValue -> SValue -> SValue
    doCombine x y = foldl (\res,(x',y',r') => if x == x' && y == y' then r' else res) NONE table

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module CodeGen.CodeGenHelper

import Protocol.Hex
import CairoCode.CairoCode
import Core.Context
import CairoCode.CairoCodeUtils
import Data.SortedMap

export
-- Constant Operations
constToInteger : CairoConst -> Maybe Integer
constToInteger (I x) = Just $ cast x
constToInteger (I8 x) = Just $ cast x
constToInteger (I16 x) = Just $ cast x
constToInteger (I32 x) = Just $ cast x
constToInteger (I64 x) = Just $ cast x
constToInteger (F x) = Just  x
constToInteger (BI x) = Just  x
constToInteger (Ch x) = Just $ cast x
constToInteger (B8 x) = Just $ cast x
constToInteger (B16 x) = Just $ cast x
constToInteger (B32 x) = Just $ cast x
constToInteger (B64 x) = Just $ cast x
-- Todo: is this correct? How are non primitive types represented? conflict?
-- Negative numbers in case it is incorrect to reduce conflict potential.
constToInteger IntType = Just (-1)
constToInteger Int8Type = Just (-2)
constToInteger Int16Type = Just (-3)
constToInteger Int32Type = Just (-4)
constToInteger Int64Type = Just (-5)
constToInteger FeltType = Just (-6)
constToInteger IntegerType = Just (-7)
constToInteger StringType = Just (-8)
constToInteger CharType = Just (-9)
constToInteger Bits8Type = Just (-10)
constToInteger Bits16Type = Just (-11)
constToInteger Bits32Type = Just (-12)
constToInteger Bits64Type = Just (-13)
constToInteger _ = Nothing

export
compileConst: CairoConst -> String
compileConst (I x) = show x
compileConst (I8 x) = show x
compileConst (I16 x) = show x
compileConst (I32 x) = show x
compileConst (I64 x) = show x
compileConst (F x) = show x
compileConst (BI x) = show x  -- Todo: We don't have BigInteger. Temporary hack until we have.
compileConst (Ch x) = assert_total $ idris_crash "Char is not supported yet."
compileConst (Str x) = assert_total $ idris_crash "String is not supported yet."
compileConst (B8 x) = show x
compileConst (B16 x) = show x
compileConst (B32 x) = show x
compileConst (B64 x) = show x
compileConst typ = show $ constToInteger typ

export
regName : CairoReg -> String
regName (Unassigned Nothing n d) = "u_" ++ show n ++ "_" ++ show d
regName (Unassigned (Just p) n d) = "_" ++ p ++ "_" ++ show n ++ "_" ++ show d
regName (NamedParam n) = n
regName (Param i) = "p_" ++ show i
regName (Local i _) = "l_" ++ show i
regName (Let i _) = "b_" ++ show i
regName (Temp i _) = "t_" ++ show i
regName (Const v) = "inlined_constant"
regName Eliminated = "discarded_register"

export
compileReg : CairoReg -> String
compileReg (Const v) = compileConst v
compileReg Eliminated = "0"
compileReg reg = regName reg

export
compileRegDeclCommon : CairoReg -> String -> String -> String
compileRegDeclCommon (Unassigned Nothing i d) _ _ = "u_" ++ show i ++ "_" ++ show d
compileRegDeclCommon (Unassigned (Just p) i d) _ _ = "_" ++ p ++ "_" ++ show i ++ "_" ++ show d
compileRegDeclCommon (Local i _) _ _ = "l_" ++ show i
compileRegDeclCommon (Let i _) _ letS = letS ++ " b_" ++ show i
compileRegDeclCommon (Temp i _) tempS _ = tempS ++ " t_" ++ show i
compileRegDeclCommon (Const v) _ letS = letS ++ " inlined_constant"
compileRegDeclCommon Eliminated _ letS = letS ++ " discarded_register"
compileRegDeclCommon _ _ _ = ""

export
compileRegDecl : CairoReg -> String
compileRegDecl r = compileRegDeclCommon r "tempvar" "let"

export
compileNestRegDecl : CairoReg -> String
compileNestRegDecl r = compileRegDeclCommon r "tempvar" "tempvar"

export
compileConstRegDecl : CairoReg -> String
compileConstRegDecl r = compileRegDeclCommon r "const" "const"

export
compileRegDeclRef : CairoReg -> String
compileRegDeclRef r = compileRegDeclCommon r "let" "let"

export
compileRegManifest : CairoReg -> String
compileRegManifest r = if isLocal r then "" else compileRegDeclCommon r "tempvar" "tempvar"

export
ensureManifested : CairoReg -> String -> (String, String)
ensureManifested reg@(Let _ _) tempName = ("tempvar \{tempName} = \{compileReg reg}\n", tempName)
ensureManifested reg tempName = ("", compileReg reg)

-- records do not have tags
export
tagToString : Maybe Int -> String
tagToString (Just tag) = show tag
tagToString Nothing = "0"

export
impossibleCase : CairoReg -> String -> String
impossibleCase reg msg = """
    %{ assert False, '\{ msg }' %}
    assert 1 = 0
    \{ compileRegDecl reg } = 0

    """

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Core.UnifyState

import Core.CaseTree
import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.FC
import Core.Normalise
import Core.Options
import Core.TT
import Core.TTC
import Utils.Binary

import Data.IntMap
import Data.List
import Data.NameMap
import Data.StringMap

%default covering

public export
data Constraint : Type where
     -- An unsolved constraint, noting two terms which need to be convertible
     -- in a particular environment
     MkConstraint : {vars : _} ->
                    FC ->
                    (withLazy : Bool) ->
                    (blockedOn : List Name) ->
                    (env : Env Term vars) ->
                    (x : Term vars) -> (y : Term vars) ->
                    Constraint
     -- An unsolved sequence of constraints, arising from arguments in an
     -- application where solving later constraints relies on solving earlier
     -- ones
     MkSeqConstraint : {vars : _} ->
                       FC ->
                       (env : Env Term vars) ->
                       (xs : List (Term vars)) ->
                       (ys : List (Term vars)) ->
                       Constraint
     -- A resolved constraint
     Resolved : Constraint

export
TTC Constraint where
  toBuf b (MkConstraint {vars} fc l block env x y)
     = do tag 0; toBuf b vars; toBuf b l
          toBuf b block
          toBuf b fc; toBuf b env; toBuf b x; toBuf b y
  toBuf b (MkSeqConstraint {vars} fc env xs ys)
     = do tag 1; toBuf b vars; toBuf b fc; toBuf b env; toBuf b xs; toBuf b ys
  toBuf b Resolved = tag 2

  fromBuf b
      = case !getTag of
             0 => do vars <- fromBuf b
                     fc <- fromBuf b; l <- fromBuf b
                     block <- fromBuf b
                     env <- fromBuf b
                     x <- fromBuf b; y <- fromBuf b
                     pure (MkConstraint {vars} fc l block env x y)
             1 => do vars <- fromBuf b
                     fc <- fromBuf b; env <- fromBuf b
                     xs <- fromBuf b; ys <- fromBuf b
                     pure (MkSeqConstraint {vars} fc env xs ys)
             2 => pure Resolved
             _ => corrupt "Constraint"

public export
record UState where
  constructor MkUState
  holes : IntMap (FC, Name) -- All metavariables with no definition yet.
                            -- 'Int' is the 'Resolved' name
  guesses : IntMap (FC, Name) -- Names which will be defined when constraints solved
                              -- (also includes auto implicit searches)
  currentHoles : IntMap (FC, Name) -- Holes introduced this elaboration session
  delayedHoles : IntMap (FC, Name) -- Holes left unsolved after an elaboration,
                                   -- so we need to check again at the end whether
                                   -- they have been solved later. Doesn't include
                                   -- user defined hole names, which don't need
                                   -- to have been solved
  constraints : IntMap Constraint -- map for finding constraints by ID
  dotConstraints : List (Name, DotReason, Constraint) -- dot pattern constraints
  nextName : Int
  nextConstraint : Int
  delayedElab : List (Nat, Int, Core ClosedTerm)
                -- Elaborators which we need to try again later, because
                -- we didn't have enough type information to elaborate
                -- successfully yet.
                -- 'Nat' is the priority (lowest first)
                -- The 'Int' is the resolved name. Delays can't be nested,
                -- so we just process them in order.
  logging : Bool

export
initUState : UState
initUState = MkUState empty empty empty empty empty [] 0 0 [] False

export
data UST : Type where

export
resetNextVar : {auto u : Ref UST UState} ->
               Core ()
resetNextVar
    = do ust <- get UST
         put UST (record { nextName = 0 } ust)

-- Generate a global name based on the given root, in the current namespace
export
genName : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          String -> Core Name
genName str
    = do ust <- get UST
         put UST (record { nextName $= (+1) } ust)
         n <- inCurrentNS (MN str (nextName ust))
         pure n

-- Generate a global name based on the given name, in the current namespace
export
genMVName : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            Name -> Core Name
genMVName (UN str) = genName str
genMVName (MN str _) = genName str
genMVName n
    = do ust <- get UST
         put UST (record { nextName $= (+1) } ust)
         mn <- inCurrentNS (MN (show n) (nextName ust))
         pure mn

-- Generate a unique variable name based on the given root
export
genVarName : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             String -> Core Name
genVarName str
    = do ust <- get UST
         put UST (record { nextName $= (+1) } ust)
         pure (MN str (nextName ust))

-- Again, for case names
export
genCaseName : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              String -> Core Name
genCaseName root
    = do ust <- get UST
         put UST (record { nextName $= (+1) } ust)
         inCurrentNS (CaseBlock root (nextName ust))

export
genWithName : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              String -> Core Name
genWithName root
    = do ust <- get UST
         put UST (record { nextName $= (+1) } ust)
         inCurrentNS (WithBlock root (nextName ust))

addHoleName : {auto u : Ref UST UState} ->
              FC -> Name -> Int -> Core ()
addHoleName fc n i
    = do ust <- get UST
         put UST (record { holes $= insert i (fc, n),
                           currentHoles $= insert i (fc, n) } ust)

addGuessName : {auto u : Ref UST UState} ->
               FC -> Name -> Int -> Core ()
addGuessName fc n i
    = do ust <- get UST
         put UST (record { guesses $= insert i (fc, n)  } ust)

export
removeHole : {auto u : Ref UST UState} ->
             Int -> Core ()
removeHole n
    = do ust <- get UST
         put UST (record { holes $= delete n,
                           currentHoles $= delete n,
                           delayedHoles $= delete n } ust)

export
removeHoleName : {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 Name -> Core ()
removeHoleName n
    = do defs <- get Ctxt
         let Just i = getNameID n (gamma defs)
             | Nothing => pure ()
         removeHole i

export
saveHoles : {auto u : Ref UST UState} ->
            Core (IntMap (FC, Name))
saveHoles
    = do ust <- get UST
         put UST (record { currentHoles = empty } ust)
         pure (currentHoles ust)

export
restoreHoles : {auto u : Ref UST UState} ->
               IntMap (FC, Name) -> Core ()
restoreHoles hs
    = do ust <- get UST
         put UST (record { currentHoles = hs } ust)

export
removeGuess : {auto u : Ref UST UState} ->
              Int -> Core ()
removeGuess n
    = do ust <- get UST
         put UST (record { guesses $= delete n } ust)

-- Get all of the hole data
export
getHoles : {auto u : Ref UST UState} ->
           Core (IntMap (FC, Name))
getHoles
    = do ust <- get UST
         pure (holes ust)

-- Get all of the guess data
export
getGuesses : {auto u : Ref UST UState} ->
           Core (IntMap (FC, Name))
getGuesses
    = do ust <- get UST
         pure (guesses ust)

-- Get the hole data for holes in the current elaboration session
-- (i.e. since the last 'saveHoles')
export
getCurrentHoles : {auto u : Ref UST UState} ->
                  Core (IntMap (FC, Name))
getCurrentHoles
    = do ust <- get UST
         pure (currentHoles ust)

export
isHole : {auto u : Ref UST UState} ->
         Int -> Core Bool
isHole i
    = do ust <- get UST
         pure (maybe False (const True) (lookup i (holes ust)))

export
isCurrentHole : {auto u : Ref UST UState} ->
                Int -> Core Bool
isCurrentHole i
    = do ust <- get UST
         pure (maybe False (const True) (lookup i (currentHoles ust)))

export
setConstraint : {auto u : Ref UST UState} ->
                Int -> Constraint -> Core ()
setConstraint cid c
    = do ust <- get UST
         put UST (record { constraints $= insert cid c } ust)

export
deleteConstraint : {auto u : Ref UST UState} ->
                Int -> Core ()
deleteConstraint cid
    = do ust <- get UST
         put UST (record { constraints $= delete cid } ust)

export
addConstraint : {auto u : Ref UST UState} ->
                {auto c : Ref Ctxt Defs} ->
                Constraint -> Core Int
addConstraint constr
    = do ust <- get UST
         let cid = nextConstraint ust
         put UST (record { constraints $= insert cid constr,
                           nextConstraint = cid+1 } ust)
         pure cid

export
addDot : {vars : _} ->
         {auto u : Ref UST UState} ->
         FC -> Env Term vars -> Name -> Term vars -> DotReason -> Term vars ->
         Core ()
addDot fc env dotarg x reason y
    = do ust <- get UST
         put UST (record { dotConstraints $=
                             ((dotarg, reason, MkConstraint fc False [] env x y) ::)
                         } ust)

mkConstantAppArgs : {vars : _} ->
                    Bool -> FC -> Env Term vars ->
                    (wkns : List Name) ->
                    List (Term (wkns ++ (vars ++ done)))
mkConstantAppArgs lets fc [] wkns = []
mkConstantAppArgs {done} {vars = x :: xs} lets fc (b :: env) wkns
    = let rec = mkConstantAppArgs {done} lets fc env (wkns ++ [x]) in
          if lets || not (isLet b)
             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
                  rewrite (appendAssociative wkns [x] (xs ++ done)) in rec
             else rewrite (appendAssociative wkns [x] (xs ++ done)) in rec
  where
    mkVar : (wkns : List Name) ->
            IsVar name (length wkns) (wkns ++ name :: vars ++ done)
    mkVar [] = First
    mkVar (w :: ws) = Later (mkVar ws)

mkConstantAppArgsSub : {vars : _} ->
                       Bool -> FC -> Env Term vars ->
                       SubVars smaller vars ->
                       (wkns : List Name) ->
                       List (Term (wkns ++ (vars ++ done)))
mkConstantAppArgsSub lets fc [] p wkns = []
mkConstantAppArgsSub {done} {vars = x :: xs}
                        lets fc (b :: env) SubRefl wkns
    = rewrite appendAssociative wkns [x] (xs ++ done) in
              mkConstantAppArgs lets fc env (wkns ++ [x])
mkConstantAppArgsSub {done} {vars = x :: xs}
                        lets fc (b :: env) (DropCons p) wkns
    = rewrite appendAssociative wkns [x] (xs ++ done) in
              mkConstantAppArgsSub lets fc env p (wkns ++ [x])
mkConstantAppArgsSub {done} {vars = x :: xs}
                        lets fc (b :: env) (KeepCons p) wkns
    = let rec = mkConstantAppArgsSub {done} lets fc env p (wkns ++ [x]) in
          if lets || not (isLet b)
             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
                  rewrite appendAssociative wkns [x] (xs ++ done) in rec
             else rewrite appendAssociative wkns [x] (xs ++ done) in rec
  where
    mkVar : (wkns : List Name) ->
            IsVar name (length wkns) (wkns ++ name :: vars ++ done)
    mkVar [] = First
    mkVar (w :: ws) = Later (mkVar ws)

mkConstantAppArgsOthers : {vars : _} ->
                          Bool -> FC -> Env Term vars ->
                          SubVars smaller vars ->
                          (wkns : List Name) ->
                          List (Term (wkns ++ (vars ++ done)))
mkConstantAppArgsOthers lets fc [] p wkns = []
mkConstantAppArgsOthers {done} {vars = x :: xs}
                        lets fc (b :: env) SubRefl wkns
    = rewrite appendAssociative wkns [x] (xs ++ done) in
              mkConstantAppArgsOthers lets fc env SubRefl (wkns ++ [x])
mkConstantAppArgsOthers {done} {vars = x :: xs}
                        lets fc (b :: env) (KeepCons p) wkns
    = rewrite appendAssociative wkns [x] (xs ++ done) in
              mkConstantAppArgsOthers lets fc env p (wkns ++ [x])
mkConstantAppArgsOthers {done} {vars = x :: xs}
                        lets fc (b :: env) (DropCons p) wkns
    = let rec = mkConstantAppArgsOthers {done} lets fc env p (wkns ++ [x]) in
          if lets || not (isLet b)
             then Local fc (Just (isLet b)) (length wkns) (mkVar wkns) ::
                  rewrite appendAssociative wkns [x] (xs ++ done) in rec
             else rewrite appendAssociative wkns [x] (xs ++ done) in rec
  where
    mkVar : (wkns : List Name) ->
            IsVar name (length wkns) (wkns ++ name :: vars ++ done)
    mkVar [] = First
    mkVar (w :: ws) = Later (mkVar ws)

export
applyTo : {vars : _} ->
          FC -> Term vars -> Env Term vars -> Term vars
applyTo fc tm env
  = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

export
applyToFull : {vars : _} ->
              FC -> Term vars -> Env Term vars -> Term vars
applyToFull fc tm env
  = let args = reverse (mkConstantAppArgs {done = []} True fc env []) in
        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

export
applyToSub : {vars : _} ->
             FC -> Term vars -> Env Term vars ->
             SubVars smaller vars -> Term vars
applyToSub fc tm env sub
  = let args = reverse (mkConstantAppArgsSub {done = []} True fc env sub []) in
        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

export
applyToOthers : {vars : _} ->
                FC -> Term vars -> Env Term vars ->
                SubVars smaller vars -> Term vars
applyToOthers fc tm env sub
  = let args = reverse (mkConstantAppArgsOthers {done = []} True fc env sub []) in
        apply fc tm (rewrite sym (appendNilRightNeutral vars) in args)

-- Create a new metavariable with the given name and return type,
-- and return a term which is the metavariable applied to the environment
-- (and which has the given type)
-- Flag whether cycles are allowed in the result, and whether to abstract
-- over lets
export
newMetaLets : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              FC -> RigCount ->
              Env Term vars -> Name -> Term vars -> Def ->
              Bool -> Bool ->
              Core (Int, Term vars)
newMetaLets {vars} fc rig env n ty def nocyc lets
    = do let hty = if lets then abstractFullEnvType fc env ty
                           else abstractEnvType fc env ty
         let hole = record { noCycles = nocyc }
                           (newDef fc n rig [] hty Public def)
         log "unify.meta" 5 $ "Adding new meta " ++ show (n, fc, rig)
         logTerm "unify.meta" 10 ("New meta type " ++ show n) hty
         defs <- get Ctxt
         idx <- addDef n hole
         addHoleName fc n idx
         pure (idx, Meta fc n idx envArgs)
  where
    envArgs : List (Term vars)
    envArgs = let args = reverse (mkConstantAppArgs {done = []} lets fc env []) in
                  rewrite sym (appendNilRightNeutral vars) in args

export
newMeta : {vars : _} ->
          {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          FC -> RigCount ->
          Env Term vars -> Name -> Term vars -> Def ->
          Bool ->
          Core (Int, Term vars)
newMeta fc r env n ty def cyc = newMetaLets fc r env n ty def cyc False

mkConstant : {vars : _} ->
             FC -> Env Term vars -> Term vars -> ClosedTerm
mkConstant fc [] tm = tm
-- mkConstant {vars = x :: _} fc (Let c val ty :: env) tm
--     = mkConstant fc env (Bind fc x (Let c val ty) tm)
mkConstant {vars = x :: _} fc (b :: env) tm
    = let ty = binderType b in
          mkConstant fc env (Bind fc x (Lam fc (multiplicity b) Explicit ty) tm)

-- Given a term and a type, add a new guarded constant to the global context
-- by applying the term to the current environment
-- Return the replacement term (the name applied to the environment)
export
newConstant : {vars : _} ->
              {auto u : Ref UST UState} ->
              {auto c : Ref Ctxt Defs} ->
              FC -> RigCount -> Env Term vars ->
              (tm : Term vars) -> (ty : Term vars) ->
              (constrs : List Int) ->
              Core (Term vars)
newConstant {vars} fc rig env tm ty constrs
    = do let def = mkConstant fc env tm
         let defty = abstractFullEnvType fc env ty
         cn <- genName "postpone"
         let guess = newDef fc cn rig [] defty Public
                            (Guess def (length env) constrs)
         log "unify.constant" 5 $ "Adding new constant " ++ show (cn, fc, rig)
         logTerm "unify.constant" 10 ("New constant type " ++ show cn) defty
         idx <- addDef cn guess
         addGuessName fc cn idx
         pure (Meta fc cn idx envArgs)
  where
    envArgs : List (Term vars)
    envArgs = let args = reverse (mkConstantAppArgs {done = []} True fc env []) in
                  rewrite sym (appendNilRightNeutral vars) in args

-- Create a new search with the given name and return type,
-- and return a term which is the name applied to the environment
-- (and which has the given type)
export
newSearch : {vars : _} ->
            {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            FC -> RigCount -> Nat -> Name ->
            Env Term vars -> Name -> Term vars -> Core (Int, Term vars)
newSearch {vars} fc rig depth def env n ty
    = do let hty = abstractEnvType fc env ty
         let hole = newDef fc n rig [] hty Public (BySearch rig depth def)
         log "unify.search" 10 $ "Adding new search " ++ show fc ++ " " ++ show n
         logTermNF "unify.search" 10 "New search type" env ty
         idx <- addDef n hole
         addGuessName fc n idx
         pure (idx, Meta fc n idx envArgs)
  where
    envArgs : List (Term vars)
    envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
                  rewrite sym (appendNilRightNeutral vars) in args

-- Add a hole which stands for a delayed elaborator
export
newDelayed : {vars : _} ->
             {auto u : Ref UST UState} ->
             {auto c : Ref Ctxt Defs} ->
             FC -> RigCount ->
             Env Term vars -> Name ->
             (ty : Term vars) -> Core (Int, Term vars)
newDelayed {vars} fc rig env n ty
    = do let hty = abstractEnvType fc env ty
         let hole = newDef fc n rig [] hty Public Delayed
         idx <- addDef n hole
         log "unify.delay" 10 $ "Added delayed elaborator " ++ show (n, idx)
         addHoleName fc n idx
         pure (idx, Meta fc n idx envArgs)
  where
    envArgs : List (Term vars)
    envArgs = let args = reverse (mkConstantAppArgs {done = []} False fc env []) in
                  rewrite sym (appendNilRightNeutral vars) in args

export
tryErrorUnify : {auto c : Ref Ctxt Defs} ->
                {auto u : Ref UST UState} ->
                Core a -> Core (Either Error a)
tryErrorUnify elab
    = do ust <- get UST
         defs <- branch
         catch (do res <- elab
                   commit
                   pure (Right res))
               (\err => do put UST ust
                           defs' <- get Ctxt
                           put Ctxt (record { timings = timings defs' } defs)
                           pure (Left err))

export
tryUnify : {auto c : Ref Ctxt Defs} ->
           {auto u : Ref UST UState} ->
           Core a -> Core a -> Core a
tryUnify elab1 elab2
    = do Right ok <- tryErrorUnify elab1
               | Left err => elab2
         pure ok

export
handleUnify : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              Core a -> (Error -> Core a) -> Core a
handleUnify elab1 elab2
    = do Right ok <- tryErrorUnify elab1
               | Left err => elab2 err
         pure ok

-- Note that the given hole name arises from a type declaration, so needs
-- to be resolved later
export
addDelayedHoleName : {auto u : Ref UST UState} ->
                     (Int, (FC, Name)) -> Core ()
addDelayedHoleName (idx, h)
    = do ust <- get UST
         put UST (record { delayedHoles $= insert idx h } ust)

export
checkDelayedHoles : {auto u : Ref UST UState} ->
                    {auto c : Ref Ctxt Defs} ->
                    Core (Maybe Error)
checkDelayedHoles
    = do ust <- get UST
         let hs = toList (delayedHoles ust)
         if (not (isNil hs))
            then do pure (Just (UnsolvedHoles (map snd hs)))
            else pure Nothing

-- A hole is 'valid' - i.e. okay to leave unsolved for later - as long as it's
-- not guarded by a unification problem (in which case, report that the unification
-- problem is unsolved) and it doesn't depend on an implicit pattern variable
-- (in which case, perhaps suggest binding it explicitly)
export
checkValidHole : {auto c : Ref Ctxt Defs} ->
                 {auto u : Ref UST UState} ->
                 (Int, (FC, Name)) -> Core ()
checkValidHole (idx, (fc, n))
    = do defs <- get Ctxt
         ust <- get UST
         Just gdef <- lookupCtxtExact (Resolved idx) (gamma defs)
              | Nothing => pure ()
         case definition gdef of
              BySearch _ _ _ =>
                  do defs <- get Ctxt
                     Just ty <- lookupTyExact n (gamma defs)
                          | Nothing => pure ()
                     throw (CantSolveGoal fc [] ty)
              Guess tm envb (con :: _) =>
                  do ust <- get UST
                     let Just c = lookup con (constraints ust)
                          | Nothing => pure ()
                     case c of
                          MkConstraint fc l blocked env x y =>
                             do put UST (record { guesses = empty } ust)
                                xnf <- normaliseHoles defs env x
                                ynf <- normaliseHoles defs env y
                                throw (CantSolveEq fc env xnf ynf)
                          MkSeqConstraint fc env (x :: _) (y :: _) =>
                             do put UST (record { guesses = empty } ust)
                                xnf <- normaliseHoles defs env x
                                ynf <- normaliseHoles defs env y
                                throw (CantSolveEq fc env xnf ynf)
                          _ => pure ()
              _ => traverse_ checkRef !(traverse getFullName
                                        ((keys (getRefs (Resolved (-1)) (type gdef)))))
  where
    checkRef : Name -> Core ()
    checkRef (PV n f)
        = throw (GenericMsg fc
                   ("Hole cannot depend on an unbound implicit " ++ show n))
    checkRef _ = pure ()

-- Bool flag says whether it's an error for there to have been holes left
-- in the last session. Usually we can leave them to the end, but it's not
-- valid for there to be holes remaining when checking a LHS.
-- Also throw an error if there are unresolved guarded constants or
-- unsolved searches
export
checkUserHoles : {auto u : Ref UST UState} ->
                 {auto c : Ref Ctxt Defs} ->
                 Bool -> Core ()
checkUserHoles now
    = do gs_map <- getGuesses
         let gs = toList gs_map
         log "unify.unsolved" 10 $ "Unsolved guesses " ++ show gs
         traverse_ checkValidHole gs
         hs_map <- getCurrentHoles
         let hs = toList hs_map
         let hs' = if any isUserName (map (snd . snd) hs)
                      then [] else hs
         when (now && not (isNil hs')) $
              throw (UnsolvedHoles (map snd (nubBy nameEq hs)))
         -- Note the hole names, to ensure they are resolved
         -- by the end of elaborating the current source file
         traverse_ addDelayedHoleName hs'
  where
    nameEq : (a, b, Name) -> (a, b, Name) -> Bool
    nameEq (_, _, x) (_, _, y) = x == y

export
checkNoGuards : {auto u : Ref UST UState} ->
                {auto c : Ref Ctxt Defs} ->
                Core ()
checkNoGuards = checkUserHoles False

export
dumpHole' : {auto u : Ref UST UState} ->
            {auto c : Ref Ctxt Defs} ->
            LogLevel -> (hole : Int) -> Core ()
dumpHole' lvl hole
    = do ust <- get UST
         defs <- get Ctxt
         if keepLog lvl (logLevel $ session $ options defs)
            then pure ()
            else do
               defs <- get Ctxt
               case !(lookupCtxtExact (Resolved hole) (gamma defs)) of
                 Nothing => pure ()
                 Just gdef => case (definition gdef, type gdef) of
                    (Guess tm envb constraints, ty) =>
                         do log' lvl $ "!" ++ show !(getFullName (Resolved hole)) ++ " : " ++
                                              show !(toFullNames !(normaliseHoles defs [] ty))
                            log' lvl $ "\t  = " ++ show !(normaliseHoles defs [] tm)
                                            ++ "\n\twhen"
                            traverse dumpConstraint constraints
                            pure ()
                    (Hole _ p, ty) =>
                         log' lvl $ "?" ++ show (fullname gdef) ++ " : " ++
                                           show !(normaliseHoles defs [] ty)
                                           ++ if implbind p then " (ImplBind)" else ""
                                           ++ if invertible gdef then " (Invertible)" else ""
                    (BySearch _ _ _, ty) =>
                         log' lvl $ "Search " ++ show hole ++ " : " ++
                                           show !(toFullNames !(normaliseHoles defs [] ty))
                    (PMDef _ args t _ _, ty) =>
                         log' (withVerbosity 4 lvl) $
                            "Solved: " ++ show hole ++ " : " ++
                            show !(normalise defs [] ty) ++
                            " = " ++ show !(normalise defs [] (Ref emptyFC Func (Resolved hole)))
                    (ImpBind, ty) =>
                         log' (withVerbosity 4 lvl) $
                             "Bound: " ++ show hole ++ " : " ++
                             show !(normalise defs [] ty)
                    (Delayed, ty) =>
                         log' (withVerbosity 4 lvl) $
                            "Delayed elaborator : " ++
                            show !(normalise defs [] ty)
                    _ => pure ()
  where
    dumpConstraint : Int -> Core ()
    dumpConstraint n
        = do ust <- get UST
             defs <- get Ctxt
             case lookup n (constraints ust) of
                  Nothing => pure ()
                  Just Resolved => log' lvl "\tResolved"
                  Just (MkConstraint _ lazy _ env x y) =>
                    do log' lvl $ "\t  " ++ show !(toFullNames !(normalise defs env x))
                                       ++ " =?= " ++ show !(toFullNames !(normalise defs env y))
                       log' (withVerbosity 5 lvl)
                                $ "\t    from " ++ show !(toFullNames x)
                                      ++ " =?= " ++ show !(toFullNames y) ++
                               if lazy then "\n\t(lazy allowed)" else ""
                  Just (MkSeqConstraint _ _ xs ys) =>
                       log' lvl $ "\t\t" ++ show xs ++ " =?= " ++ show ys

export
dumpConstraints : {auto u : Ref UST UState} ->
                  {auto c : Ref Ctxt Defs} ->
                  (topics : String) -> (verbosity : Nat) ->
                  (all : Bool) ->
                  Core ()
dumpConstraints str n all
    = do ust <- get UST
         defs <- get Ctxt
         let lvl = mkLogLevel str n
         if keepLog lvl (logLevel $ session $ options defs) then
            do let hs = toList (guesses ust) ++
                        toList (if all then holes ust else currentHoles ust)
               case hs of
                    [] => pure ()
                    _ => do log' lvl "--- CONSTRAINTS AND HOLES ---"
                            traverse (dumpHole' lvl) (map fst hs)
                            pure ()
            else pure ()


text:
module Main

import Internal.CTimespec
import Data.DateTime
import Data.Time.Calendar.Gregorian
import Data.Time.LocalTime.Internal.TimeOfDay
import Data.Time.Clock.Internal.UTCTime
import Data.Time.Clock.Internal.DiffTime

import Data.Time.Clock.Internal.Fixed

main : IO ()
main = do
  putStrLn $ show !clock_gettime
  x <- today
  let y = addDays x 20
  putStrLn $ show x
  putStrLn $ show y
  --putStrLn $ show !clock_getres
  utcTime <- getUTCTime
  putStrLn $ show (utctDayTime utcTime)
  let timeofday = timeToTimeOfDay (utctDayTime utcTime)
  putStrLn $ show (diffTimeToPicoseconds (utctDayTime utcTime))
  putStrLn $ "Time of day is = (fixed min) " ++ show timeofday
  pure ()
  -- mem <- alloc time_spec
  --   v <- get_time !ClockRealTime mem
  -- putStrLn $ show v
  -- let (CPt x1 y) = field time_spec 0 mem
  -- let (CPt x2 y) = field time_spec 1 mem
  --   putStrLn $ show $ prim__zextB64_BigInt !(peek I64 x1)
  -- putStrLn $ show !(peek I64 x2)
  -- pure ()

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

max_stars_repo_name: gdevanla/idris-time

max_issues_repo_name: gdevanla/idris-time

max_forks_repo_name: gdevanla/idris-time


text:
module Compiler.Jvm.Foreign

import Compiler.Common
import Compiler.CompileExpr
import Compiler.Inline

import Core.Context
import Core.Name
import Core.TT

import Libraries.Data.SortedMap
import Data.List
import Data.List1
import Data.Vect
import Data.String

import Compiler.Jvm.InferredType
import Compiler.Jvm.Jname
import Compiler.Jvm.Asm
import Compiler.Jvm.ExtPrim
import Compiler.Jvm.ShowUtil

namespace ForeignType
    public export
    data ForeignType
        = AtomicForeignType InferredType
        | FunctionForeignType
            String -- (interfaceName: String)
            String -- (methodName: String)
            InferredFunctionType -- (interfaceMethodType: InferredFunctionType)
            InferredFunctionType -- (implementationMethodType: InferredFunctionType)

    public export
    getInferredType : ForeignType -> InferredType
    getInferredType (FunctionForeignType interfaceName _ _ _) = IRef interfaceName
    getInferredType (AtomicForeignType ty) = ty

export
Show ForeignType where
    show (AtomicForeignType ty) = show ty
    show (FunctionForeignType interfaceName methodName interfaceMethodType implementationMethodType) =
        interfaceName ++ "." ++ methodName ++ "#" ++ show interfaceMethodType ++ "#" ++ show implementationMethodType

namespace ForeignImplementationType
    public export
    data ForeignImplementationType
        = AtomicForeignImplementationType InferredType
        | FunctionForeignImplementationType InferredFunctionType

    export
    getInferredType : FC -> ForeignImplementationType -> Asm InferredType
    getInferredType fc (AtomicForeignImplementationType ty) = Pure ty
    getInferredType fc _ = Throw fc "Callback functions cannot be higher order"

    mutual
        parseCallbackType : FC -> List CFType -> CFType -> Asm ForeignImplementationType
        parseCallbackType fc arguments (CFFun CFWorld returnType) = parseCallbackType fc arguments returnType
        parseCallbackType fc arguments (CFFun nextArgument returnType) =
            parseCallbackType fc (nextArgument :: arguments) returnType
        parseCallbackType fc arguments returnType = do
                argumentForeignTypes <- traverse parseInferredType (List.reverse arguments)
                returnForeignType <- parseInferredType returnType
                Pure $ FunctionForeignImplementationType (MkInferredFunctionType returnForeignType argumentForeignTypes)
            where
                parseInferredType : CFType -> Asm InferredType
                parseInferredType ty = do
                    foreignType <- parse fc ty
                    inferredType <- getInferredType fc foreignType
                    Pure inferredType

        export
        parse : FC -> CFType -> Asm ForeignImplementationType
        parse _ CFUnit = Pure $ AtomicForeignImplementationType IVoid
        parse _ CFInt = Pure $ AtomicForeignImplementationType IInt
        parse _ CFUnsigned8 = Pure $ AtomicForeignImplementationType IInt
        parse _ CFUnsigned16 = Pure $ AtomicForeignImplementationType IInt
        parse _ CFUnsigned32 = Pure $ AtomicForeignImplementationType IInt
        parse _ CFUnsigned64 = Pure $ AtomicForeignImplementationType ILong
        parse _ CFString = Pure $ AtomicForeignImplementationType inferredStringType
        parse _ CFDouble = Pure $ AtomicForeignImplementationType IDouble
        parse _ CFChar = Pure $ AtomicForeignImplementationType IChar
        parse _ CFWorld = Pure $ AtomicForeignImplementationType IInt
        parse fc (CFIORes returnType) = parse fc returnType
        parse fc (CFFun argument returnType) = parseCallbackType fc [argument] returnType
        parse _ _ = Pure $ AtomicForeignImplementationType inferredObjectType

export
Show ForeignImplementationType where
    show (AtomicForeignImplementationType ty) = show ty
    show (FunctionForeignImplementationType functionType) = show functionType

export
throwExplicitFunctionDescriptorRequired : FC -> Asm a
throwExplicitFunctionDescriptorRequired fc = Throw fc ("Explicit function descriptor must be provided while " ++
                                                        "passing idris functions to JVM functions")

export
parseForeignCallbackDeclarationType : FC -> (descriptorParts : List String) -> Asm InferredFunctionType
parseForeignCallbackDeclarationType fc [] = throwExplicitFunctionDescriptorRequired fc
parseForeignCallbackDeclarationType _ [returnDescriptor] = Pure $ MkInferredFunctionType (parse returnDescriptor) []
parseForeignCallbackDeclarationType _ (arg :: next) =
    let (argumentTypesReversed, returnType) = go [] arg next
    in Pure $ MkInferredFunctionType returnType (List.reverse argumentTypesReversed)
  where
    go : List InferredType -> String -> List String -> (List InferredType, InferredType)
    go acc descriptor (nextArgument :: rest) = go (parse descriptor :: acc) nextArgument rest
    go acc descriptor [] = (acc, parse descriptor)

export
getForeignCallbackDeclarationType : FC -> ForeignImplementationType -> Asm ForeignType
getForeignCallbackDeclarationType fc (AtomicForeignImplementationType ty) = Pure $ AtomicForeignType ty
getForeignCallbackDeclarationType fc _ = throwExplicitFunctionDescriptorRequired fc

{-
 - Callbacks are represented as JVM functional interface types. For example, a foreign descriptor
 - might have a callback like "jvm:foo:String java/util/function/ToIntFunction#applyAsInt#Object#Int Int".
 - This descriptor provides the underlying functional interface method type for the second argument with the
 - interface name, interface abstract method name, input and output types, all separated by "#".
 -}
export
parseForeignType : FC -> String -> ForeignImplementationType -> Asm ForeignType
parseForeignType fc descriptor implementationType = case toList $ String.split (== '#') descriptor of
    [] => Throw fc $ "Invalid descriptor: " ++ descriptor
    (interfaceName :: interfaceMethodName :: signatureParts) =>
        case implementationType of
            AtomicForeignImplementationType _ => Throw fc ("Cannot pass non function argument as a JVM function")
            FunctionForeignImplementationType implementationType => do
                declarationType <- parseForeignCallbackDeclarationType fc signatureParts
                Pure $ FunctionForeignType interfaceName interfaceMethodName declarationType implementationType
    [_] => case implementationType of
        FunctionForeignImplementationType _ => throwExplicitFunctionDescriptorRequired fc
        _ => Pure $ AtomicForeignType $ parse descriptor

export
parseForeignFunctionDescriptor : FC -> List String -> List ForeignImplementationType ->
    InferredType -> Asm (String, String, InferredType, List ForeignType)
parseForeignFunctionDescriptor fc (functionDescriptor :: className :: _) argumentTypes returnType =
    case String.break (== '(') functionDescriptor of
        (fn, "") => do
            argumentDeclarationTypes <- traverse (getForeignCallbackDeclarationType fc) argumentTypes
            Pure (className, fn, returnType, argumentDeclarationTypes)
        (fn, signature) => do
            let descriptorsWithIdrisTypes =
                zip
                    (toList $ String.split (== ' ') (assert_total $ strTail . fst $ break (== ')') signature))
                    (argumentTypes ++ [AtomicForeignImplementationType returnType])
            (argumentTypesReversed, returnType) <- go [] descriptorsWithIdrisTypes
            Pure (className, fn, returnType, List.reverse argumentTypesReversed)
  where
    go : List ForeignType -> List (String, ForeignImplementationType) -> Asm (List ForeignType, InferredType)
    go acc [] = Pure (acc, IUnknown)
    go acc ((returnTypeDesc, _) :: []) = Pure (acc, parse returnTypeDesc)
    go acc ((argument, ty) :: rest) = do
        foreignType <- parseForeignType fc argument ty
        go (foreignType :: acc) rest
parseForeignFunctionDescriptor fc descriptors _ _ = Throw fc $ "Invalid foreign descriptor: " ++ show descriptors

export
findJvmDescriptor : FC -> Name -> List String -> Asm (List String)
findJvmDescriptor fc name descriptors = case parseCC ["jvm"] descriptors of
    Just ("jvm", descriptorParts) => Pure descriptorParts
    _ => Throw fc $ "Cannot compile foreign function " ++ show name ++ " to JVM as JVM foreign descriptor is missing"

export
getArgumentIndices : (arity: Int) -> List String -> IO (Map String Int)
getArgumentIndices 0 _ = Map.newTreeMap {key=String} {value=Int}
getArgumentIndices argIndex args = Map.fromList $ zip args [0 .. argIndex - 1]

getPrimMethodName : String -> String
getPrimMethodName "" = "prim__jvmStatic"
getPrimMethodName name =
    assert_total $ if prim__strHead name == '.' then "prim__jvmInstance" else "prim__jvmStatic"

export
inferForeign : String -> Name -> FC -> List String -> List CFType -> CFType -> Asm ()
inferForeign programName idrisName fc foreignDescriptors argumentTypes returnType = do
    resetScope
    let jname = jvmName idrisName
    let jvmClassAndMethodName = getIdrisFunctionName programName (className jname) (methodName jname)
    jvmArgumentTypes <- traverse (parse fc) argumentTypes
    let arityNat = length jvmArgumentTypes
    let isNilArity = arityNat == 0
    jvmDescriptor <- findJvmDescriptor fc idrisName foreignDescriptors
    jvmReturnType <- getInferredType fc !(parse fc returnType)
    (foreignFunctionClassName, foreignFunctionName, jvmReturnType, jvmArgumentTypes) <-
        parseForeignFunctionDescriptor fc jvmDescriptor jvmArgumentTypes jvmReturnType
    let jvmArgumentTypes = getInferredType <$> jvmArgumentTypes -- TODO: Do not discard Java lambda type descriptor
    scopeIndex <- newScopeIndex
    let arity = the Int $ cast arityNat
    let argumentNames =
       if isNilArity then [] else (\argumentIndex => "arg" ++ show argumentIndex) <$> [0 .. arity - 1]
    let argumentTypesByName = SortedMap.fromList $ zip argumentNames jvmArgumentTypes
    let methodReturnType = if isNilArity then delayedType else inferredObjectType
    let inferredFunctionType = MkInferredFunctionType methodReturnType (replicate arityNat inferredObjectType)
    scopes <- LiftIo $ JList.new {a=Scope}
    let externalFunctionBody =
        NmExtPrim fc (NS (mkNamespace "") $ UN $ Basic $ getPrimMethodName foreignFunctionName) [
           NmCon fc (UN $ Basic $ createExtPrimTypeSpec jvmReturnType) DATACON Nothing [],
           NmPrimVal fc (Str $ foreignFunctionClassName ++ "." ++ foreignFunctionName),
           getJvmExtPrimArguments $ zip argumentTypes $ SortedMap.toList argumentTypesByName,
           NmPrimVal fc WorldVal]
    let functionBody = if isNilArity then NmDelay fc LLazy externalFunctionBody else externalFunctionBody
    let function = MkFunction jname inferredFunctionType scopes 0 jvmClassAndMethodName functionBody
    setCurrentFunction function
    LiftIo $ AsmGlobalState.addFunction !getGlobalState jname function
    let parameterTypes = parameterTypes inferredFunctionType
    argumentTypesByIndex <- LiftIo $
        if isNilArity
            then Map.newTreeMap {key=Int} {value=InferredType}
            else Map.fromList $ zip [0 .. arity - 1] parameterTypes
    argumentTypesByName <- LiftIo $ Map.fromList $ zip argumentNames parameterTypes
    argIndices <- LiftIo $ getArgumentIndices arity argumentNames
    let functionScope = MkScope scopeIndex Nothing argumentTypesByName argumentTypesByIndex argIndices argIndices
                            methodReturnType arity (0, 0) ("", "") []
    saveScope functionScope
    when isNilArity $ do
        let parentScopeIndex = scopeIndex
        scopeIndex <- newScopeIndex
        variableTypes <- LiftIo $ Map.newTreeMap {key=String} {value=InferredType}
        allVariableTypes <- LiftIo $ Map.newTreeMap {key=Int} {value=InferredType}
        variableIndices <- LiftIo $ Map.newTreeMap {key=String} {value=Int}
        allVariableIndices <- LiftIo $ Map.newTreeMap {key=String} {value=Int}
        let delayLambdaScope =
            MkScope scopeIndex (Just parentScopeIndex) variableTypes allVariableTypes
                variableIndices allVariableIndices IUnknown 0 (0, 0) ("", "") []
        saveScope delayLambdaScope
    updateScopeVariableTypes arityNat
  where
    getJvmExtPrimArguments : List (CFType, String, InferredType) -> NamedCExp
    getJvmExtPrimArguments [] = NmCon fc (UN $ Basic "emptyForeignArg") DATACON (Just 0) []
    getJvmExtPrimArguments ((CFWorld, _, _) :: rest) = getJvmExtPrimArguments rest
    getJvmExtPrimArguments ((_, name, ty) :: rest) = NmCon fc (UN $ Basic "foreignArg") DATACON (Just 1) [
        NmCon fc (UN . Basic $ createExtPrimTypeSpec ty) DATACON (Just 0) [],
        NmLocal fc (UN $ Basic name),
        getJvmExtPrimArguments rest ]


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

--
-- Examples of interactions available with these Lenses
--

Ex1 : Maybe Int
Ex1 = over mapped (+1) (Just 2)

Ex1Proof : Ex1 = Just 3
Ex1Proof = Refl

Ex2 : (Int, Int)
Ex2 = (2,3) & over both (+1)

Ex2Proof : Ex2 = (3, 4)
Ex2Proof = Refl

Ex3 : (String, String)
Ex3 = ("Hello",2) & _2 .~ "World!"

Ex3Proof : Ex3 = ("Hello","World!")
Ex3Proof = Refl

Ex4 : Either String Int
Ex4 = f (Left "hi")
  where f : Either String Int -> Either String Int
        f = over _Right (+1)

Ex4Proof : Ex4 = (Left "hi")
Ex4Proof = Refl

Ex5 : Either String Int
Ex5 = f (Right 4)
  where f : Either String Int -> Either String Int
        f = over _Right (+1)

Ex5Proof : Ex5 = (Right 5)
Ex5Proof = Refl

Ex6 : Either (String, Int) Int
Ex6 = f (Left ("hi", 2))
  where f : Either (String,Int) Int -> Either (String,Int) Int
        f = over (_Left . _2) (+1)

Ex6Proof : Ex6 = Left ("hi", 3)
Ex6Proof = Refl

Ex7 : Additive
Ex7 = f (Left ("hi", GetAdditive 2)) where
  f : Either (String, Additive) Int -> Additive
  f = view (_Left . _2)

Ex7Proof : Ex7 = (GetAdditive 2)
Ex7Proof = Refl

Ex8 : Additive
Ex8 = f (Right 2) where
  f : Either (String, Additive) Int -> Additive
  f = view (_Left . _2)

Ex8Proof : Ex8 = (GetAdditive 0)
Ex8Proof = Refl

Ex9 : Maybe String
Ex9 = g ^? _Right . _1 where
 g : Either String (String, Int)
 g = Right ("x",2)

Ex9Proof : Ex9 = Just "x"
Ex9Proof = Refl

Ex10 : Maybe ()
Ex10 = Just "x" ^? _Nothing

Ex10Proof : Ex10 = Nothing
Ex10Proof = Refl

Ex11 : Maybe ()
Ex11 = n ^? _Nothing where
  n : Maybe String
  n = Nothing

Ex11Proof : Ex11 = Just ()
Ex11Proof = Refl

Ex12 : Int
Ex12 = view (to fst) (1,2)

Ex12Proof : Ex12 = 1
Ex12Proof = Refl

Ex13 : Either Int String
Ex13 = the (Either Int String) $ _Left # 4

Ex13Proof : Ex13 = Left 4
Ex13Proof = Refl

Ex14 : Either Int String
Ex14 = the (Either Int String) $ 5 ^.re _Left

Ex14Proof : Ex14 = Left 5
Ex14Proof = Refl

sansExample : Maybe Int
sansExample = sans () (Just 4)

fusingExample : Maybe (Int, Int)
fusingExample = Just (2,3) & over ( fusing (_Just . both)) (+1)

confusingExample : Maybe (Int, Int)
confusingExample = Just (2,3) & over ( confusing (_Just . both)) (+1)

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

max_stars_repo_name: andrevidela/idris-lens

max_issues_repo_name: andrevidela/idris-lens

max_forks_repo_name: andrevidela/idris-lens


text:
import System.Signal
import System

main : IO ()
main = do
  Right () <- ignoreSignal SigABRT
    | Left (Error code) => putStrLn $ "error " ++ (show code)
  Right () <- defaultSignal SigABRT
    | Left (Error code) => putStrLn $ "error " ++ (show code)
  Right () <- raiseSignal SigABRT
    | Left (Error code) => putStrLn $ "received non-zero exit from system call: " ++ (show code)
  sleep 1
  putStrLn "(should not get here)."


text:
module Sleep

import Effects
import System
import Control.IOExcept
import public Data.So

%access public export

data Sleep : Effect where
     Usleep : (i : Int) -> {auto prf : So (i >= fromInteger 0 && Delay (i <= fromInteger 1000000))} -> sig Sleep ()

implementation Handler Sleep IO where
    handle () (Usleep i) k = do usleep i; k () ()

implementation Handler Sleep (IOExcept a) where
    handle () (Usleep i) k = do ioe_lift $ usleep i; k () ()

SLEEP : EFFECT
SLEEP = MkEff () Sleep

sleep : (i : Int) -> {auto prf : So (i >= fromInteger 0 && Delay (i <= fromInteger 1000000))} -> Eff () [SLEEP]
sleep i = call $ Usleep i

max_stars_repo_name: artemohanjanyan/game-of-life

max_issues_repo_name: artemohanjanyan/game-of-life

max_forks_repo_name: artemohanjanyan/game-of-life


text:
module CLaSH.Signal

import Data.HVect

%access public

infixr 5 :-
abstract codata Signal a = (:-) a (Signal a)

namespace Signal
  abstract
  head : (sig : Signal a) -> a
  head (h :- _) = h

  abstract
  tail : (sig : Signal a) -> Signal a
  tail (_ :- tl) = tl

  abstract
  mapS : (a -> b) -> Signal a -> Signal b
  mapS f (a :- as) = f a :- mapS f as

  abstract
  pureS : a -> Signal a
  pureS a = a :- pureS a

  abstract
  appS : Signal (a -> b) -> Signal a -> Signal b
  appS (f :- fs) as = f (head as) :- (appS fs (tail as))

  abstract
  register : (initS : a) -> (sig : Signal a) -> Signal a
  register i s = i :- s

sample : (i : Nat) -> (s : Signal a) -> List a
sample Z     inp = []
sample (S n) inp = head inp :: sample n (tail inp)

fromList : (l : List a) -> Signal a
fromList (x::xs) = x :- fromList xs

simulate : (Signal a -> Signal b) -> List a -> List b
simulate f is = sample (length is) (f (fromList is))

instance Functor Signal where
  map = Signal.mapS

instance Applicative Signal where
  pure  = Signal.pureS
  (<$>) = Signal.appS

namespace HVect
  head : {ts : Vect n Type} -> (hs : HVect (t::ts)) -> t
  head (x::xs) = x

  tail : {ts : Vect n Type} -> (hs : HVect (t::ts)) -> HVect ts
  tail (x::xs) = xs

  abstract
  pack : {ts : Vect n Type} -> (hs : HVect (map Signal ts)) -> Signal (HVect ts)
  pack {ts=[]}     []      = pure HVect.Nil
  pack {ts=t::ts'} (x::xs) = [| HVect.(::) x (pack xs) |]

  abstract
  unpack : {ts : Vect n Type} -> (phs : Signal (HVect ts)) -> HVect (map Signal ts)
  unpack {ts=[]}      nils = []
  unpack {ts=t::ts'}  hvs  = map HVect.head hvs :: unpack (map HVect.tail hvs)

lift : {is : Vect m Type} -> {ts : Vect n Type} ->
       (mealy : s -> HVect is -> HVect [s,HVect ts]) -> (ini : s) ->
       (inpt : HVect (map Signal is)) -> HVect (map Signal ts)
lift {s} {ts} fun initS inp = unpack (head (tail res))
  where
    res   : HVect [Signal s, Signal (HVect ts)]
    prevS : Signal s
    res   = unpack [| fun prevS (pack inp) |]
    prevS = register initS (head res)

namespace Vect
  abstract
  pack : (vs : Vect n (Signal a)) -> Signal (Vect n a)
  pack vs = map Signal.head vs :- pack (map Signal.tail vs)

  abstract
  unpack : (pvs : Signal (Vect n a)) -> Vect n (Signal a)
  unpack {n=Z}   vs = []
  unpack {n=S k} vs = map Vect.head vs :: unpack (map Vect.tail vs)

instance Num a => Num (Signal a) where
  (+) a b     = [| (+) a b |]
  (-) a b     = [| (-) a b |]
  (*) a b     = [| (*) a b |]
  abs         = map abs
  fromInteger = pure . fromInteger

max_stars_repo_name: christiaanb/clash-prelude-idris

max_issues_repo_name: christiaanb/clash-prelude-idris

max_forks_repo_name: christiaanb/clash-prelude-idris


text:
--    Copyright 2017, the blau.io contributors
--
--    Licensed under the Apache License, Version 2.0 (the "License");
--    you may not use this file except in compliance with the License.
--    You may obtain a copy of the License at
--
--        http://www.apache.org/licenses/LICENSE-2.0
--
--    Unless required by applicable law or agreed to in writing, software
--    distributed under the License is distributed on an "AS IS" BASIS,
--    WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
--    See the License for the specific language governing permissions and
--    limitations under the License.

module API.Web.XHR.XMLHttpRequest

import IdrisScript

%access public export
%default total

record XMLHttpRequest where
  constructor NewXMLRequest
  ||| self is a non-standard field to faciliate integration with JavaScript
  self : JSRef

open : XMLHttpRequest -> (method : String) -> (url : String) -> JS_IO ()
open xhr = jscall "%0.open(%1, %2)" (JSRef -> String -> String -> JS_IO ()) $
           self xhr

send : XMLHttpRequest -> JS_IO ()
send xhr = jscall "%0.send()" (JSRef -> JS_IO ()) $ self xhr

-- TODO: No options yet, callback is missing event, etc. This should really live
-- somewhere else, but I'm under time pressure for LD38.
partial
addEventListener : XMLHttpRequest -> (type : String) ->
                   (cb : (XMLHttpRequest -> JS_IO ())) -> JS_IO ()
addEventListener (NewXMLRequest self) type cb = addEventListener' where
  callback : () -> JS_IO ()
  callback _ = cb $ NewXMLRequest self

  partial
  addEventListener' : JS_IO ()
  addEventListener' = jscall "%0.addEventListener(%1, %2)"
    (JSRef -> String -> JsFn (() -> JS_IO ()) -> JS_IO ()) self type $
    MkJsFn callback

max_stars_repo_name: blau-io/idris-xhr

max_issues_repo_name: blau-io/idris-xhr

max_forks_repo_name: blau-io/idris-xhr


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

import Effects

%access export

public export
record RStats where
  constructor MkRStats
  chars      : Int
  sylls      : Int
  nowords    : Int
  shortwords : Int
  longwords  : Int
  bigwords   : Int
  sentances  : Int

Default (RStats) where
    default = MkRStats 0 0 0 0 0 0 0

Show RStats where
  show st = "No. of chars: " ++ show (chars st) ++
       "\nNo. of syllables: " ++ show (sylls st) ++
       "\nNo. of words: " ++ show (nowords st) ++
       "\nNo. of short words: " ++ show (shortwords st) ++
       "\nNo. of long words: "  ++ show (longwords st) ++
       "\nNo. of big words: "   ++ show (bigwords st) ++
       "\nNo. of sentances: "   ++ show (sentances st)

updateRStats : Int -> Int -> Int -> Int -> Int -> RStats -> RStats
updateRStats cs ss sws lws bws st =
  record { chars      = (chars st)      + cs
         , sylls      = (sylls st)      + ss
         , nowords    = (nowords st)    + 1
         , shortwords = (shortwords st) + sws
         , longwords  = (longwords st)  + lws
         , bigwords   = (bigwords st)   + bws
    } st

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

max_stars_repo_name: jfdm/idris-read

max_issues_repo_name: jfdm/idris-read

max_forks_repo_name: jfdm/idris-read


text:
module Data.Nat.Parity

import Data.Nat

%default total

--------------------------------------------------------------------------------
-- Parity
--------------------------------------------------------------------------------

mutual
  public export
  even : Nat -> Bool
  even Z = True
  even (S k) = odd k

  public export
  odd : Nat -> Bool
  odd Z = False
  odd (S k) = even k

||| A nat is Even when it is twice some other nat.
public export
Even : Nat -> Type
Even n = (half : Nat ** n = half * 2)

||| A nat is Odd when it is one more than twice some other nat.
public export
Odd : Nat -> Type
Odd n = (haf : Nat ** n = S (haf * 2))

||| Two more than an Even is Even.
public export
add2Even : Even n -> Even (2 + n)
add2Even (half ** pf) = (S half ** cong ((+) 2) pf)

||| Two more than an Odd is Odd.
public export
add2Odd : Odd n -> Odd (2 + n)
add2Odd (haf ** pf) = (S haf ** cong ((+) 2) pf)

||| One more than an Even is Odd.
public export
succEvenOdd : Even n -> Odd (S n)
succEvenOdd (half ** pf) = (half ** cong S pf)

||| One more than an Odd is Even.
public export
succOddEven : Odd n -> Even (S n)
succOddEven (haf ** pf) = (S haf ** cong S pf)

||| One less than an Odd is Even.
public export
predOddEven : Odd (S n) -> Even n
predOddEven (haf ** pf) = (haf ** cong Nat.pred pf)

||| A helper fact.
public export
succDoublePredPred : {k : Nat} -> S n = k * 2 -> n = S ((pred k) * 2)
succDoublePredPred {k = Z} prf = absurd prf
succDoublePredPred {k = S _} prf = cong Nat.pred prf

||| One less than an Even is Odd.
public export
predEvenOdd : Even (S n) -> Odd n
predEvenOdd (half ** pf) = (pred half ** succDoublePredPred pf)

||| Every nat is either Even or Odd.
public export
evenOrOdd : (n : Nat) -> Either (Even n) (Odd n)
evenOrOdd Z = Left (0 ** Refl)
evenOrOdd (S k) = case evenOrOdd k of
  Left (half ** pf) => Right (half ** cong S pf)
  Right (haf ** pf) => Left (S haf ** cong S pf)

||| No nat is both Even and Odd.
public export
notEvenAndOdd : {n : Nat} -> Even n -> Odd n -> Void
notEvenAndOdd {n = Z} _ (_ ** odd) = absurd odd
notEvenAndOdd {n = (S k)} (half ** even) (haf ** odd) =
  notEvenAndOdd {n = k}
   (haf ** cong Nat.pred odd)
   (pred half ** succDoublePredPred even)

||| Evenness is decidable.
public export
evenDec : (n : Nat) -> Dec (Even n)
evenDec n = case evenOrOdd n of
  Left even => Yes even
  Right odd => No $ \even => notEvenAndOdd even odd

||| Oddness is decidable.
public export
oddDec : (n : Nat) -> Dec (Odd n)
oddDec n = case evenOrOdd n of
  Left even => No $ notEvenAndOdd even
  Right odd => Yes odd

mutual
  ||| Evens are even.
  public export
  evenEven : {n : Nat} -> Even n -> even n = True
  evenEven {n = Z} _ = Refl
  evenEven {n = S _} pf = oddOdd $ predEvenOdd pf

  ||| Odds are odd.
  public export
  oddOdd : {n: Nat} -> Odd n -> odd n = True
  oddOdd {n = Z} (_ ** pf) = absurd pf
  oddOdd {n = S _} pf = evenEven $ predOddEven pf

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
module RnaTranscription

import Data.Vect

%access export
%default total

namespace DnaStrand
  public export
  data DnaStrand

namespace RnaStrand
  public export
  data RnaStrand

toRna : Vect n DnaStrand -> Vect n RnaStrand
toRna = ?toRna_rhs