text:
module Control.Monad.Dom.Interface

import Control.MonadRec
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Writer
import Control.WellFounded
import Data.Iterable
import Data.Nat
import Data.SOP
import JS
import Text.CSS
import Text.Html
import Web.Dom

%default total

--------------------------------------------------------------------------------
--          ElemRef
--------------------------------------------------------------------------------

||| A typed reference to an element or container in the DOM. Elements can
||| either be referenced by their ID string or their CSS class
||| (both of which must be unique), or by holding a value directly.
||| This can be used to access the element in question,
||| for instance by invoking `getElementByRef`.
|||
||| In addition, we provide (pseudo-)element references for
||| `body`, `document`, and `window`.
public export
data ElemRef : (t : Type) -> Type where
  Id :  {tag : String}
     -> (tpe : ElementType tag t)
     -> (id : String)
     -> ElemRef t

  Class :  {tag   : String}
        -> (tpe   : ElementType tag t)
        -> (class : String)
        -> ElemRef t

  Ref : (ref : t) -> ElemRef t

  Body : ElemRef HTMLElement

  Document : ElemRef Document

  Window : ElemRef Window

||| Predicate witnessing that a given `ElemRef` is a reference
||| by ID.
public export
data ById : ElemRef t -> Type where
  IsById : {0 tpe : _} -> {0 id : _} -> ById (Id tpe id)

||| Predicate witnessing that a given `ElemRef` is a reference
||| by Class.
public export
data ByClass : ElemRef t -> Type where
  IsByClass : {0 tpe : _} -> {0 id : _} -> ByClass (Class tpe id)

namespace Attribute
  ||| Uses an element ref as an ID attribute
  export
  ref : (r : ElemRef t) -> {auto 0 _ : ById r} -> Attribute ev
  ref (Id _ i) = id i

namespace CSS
  ||| Uses an element ref as an ID selector
  export
  idRef : (r : ElemRef t) -> {auto 0 _ : ById r} -> Selector 0 False False
  idRef (Id _ i) = Id i

  ||| Uses an element ref as a class selector
  export
  classRef : (r : ElemRef t) -> {auto 0 _ : ByClass r} -> Selector 0 False False
  classRef (Class _ i) = Class i

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

public export
data Position = BeforeBegin | AfterBegin | BeforeEnd | AfterEnd

export
positionStr : Position -> String
positionStr BeforeBegin = "beforebegin"
positionStr AfterBegin  = "afterbegin"
positionStr BeforeEnd   = "beforeend"
positionStr AfterEnd    = "afterend"

--------------------------------------------------------------------------------
--          Interface
--------------------------------------------------------------------------------

||| Interface for setting up interactions with the DOM
public export
interface Monad m => MonadDom (0 ev : Type) (0 m : Type -> Type) | m where
  ||| Generates a new unique ID
  uniqueId      : m String

  ||| Registers an event listener at the given DOM element,
  ||| acting on events provided by the given `DOMEvent` value.
  registerEvent : ElemRef t -> DOMEvent ev -> m ()

export
MonadDom ev m => MonadDom ev (ReaderT e m) where
  uniqueId          = lift uniqueId
  registerEvent r e = lift (registerEvent r e)

export
MonadDom ev m => MonadDom ev (StateT s m) where
  uniqueId          = lift uniqueId
  registerEvent r e = lift (registerEvent r e)

export
MonadDom ev m => MonadDom ev (WriterT w m) where
  uniqueId          = lift uniqueId
  registerEvent r e = lift (registerEvent r e)

--------------------------------------------------------------------------------
--          Node Preparation
--------------------------------------------------------------------------------

-- generates an `ElemRef` for the given HTMLElement type `t`,
-- either by using the ID already defined in the attribute list,
-- or by creating a new unique ID.
--
-- This ID will be used by `innerHtmlAt` to properly set up the
-- necessary event listeners.
getRef :  {str : String}
       -> MonadDom ev m
       => Attributes ev
       -> ElementType str t
       -> m (Attributes ev, ElemRef t)
getRef as tpe = case getId as of
  Just i  => pure (as, Id tpe i)
  Nothing => (\i => (Id i :: as, Id tpe i)) <$> uniqueId

PrepareRes : Type -> (Type -> Type) -> Type
PrepareRes ev m = (List (Node ev), List (m ()))

mutual
  -- tail-call optimized preparation of nodes
  -- the totality checker needs a wee bit of help for this
  prepareNodes :  MonadDom ev m
               => MonadRec m
               => List (Node ev)
               -> m (PrepareRes ev m)
  prepareNodes ns = trSized ns ([], []) go
    where go :  (vs : List (Node ev))
             -> PrepareRes ev m
             -> m (Step Smaller vs (PrepareRes ev m) (PrepareRes ev m))
          go [] (      ns2,ens) = pure $ Done (reverse ns2, ens)
          go (h :: t) (ns2,ens) = do
            (n2, en) <- assert_total $ prepareNode h
            pure $ Cont t (reflexive {rel = LTE}) (n2 :: ns2, en ++ ens)

  -- inserts unique IDs where necessary and extracts a list of
  -- actions, which will register the necessary event listeners
  -- after creating the nodes in the DOM
  prepareNode :  MonadDom ev m
              => MonadRec m
              => Node ev
              -> m (Node ev, List $ m ())
  prepareNode (El tpe as ns) = case getEvents as of
    Nil => do
      (ns2, ens) <- prepareNodes ns
      pure (El tpe as ns2, ens)
    es  => do
      (as2,r)    <- getRef as tpe
      (ns2, ens) <- prepareNodes ns
      pure $ (El tpe as2 ns2, map (registerEvent r) es ++ ens)

  prepareNode r@(Raw _)  = pure (r,[])
  prepareNode r@(Text _) = pure (r,[])

--------------------------------------------------------------------------------
--          Inserting Nodes
--------------------------------------------------------------------------------

||| Tries to retrieve an element of the given type by looking
||| up its ID in the DOM. Unlike `getElementById`, this will throw
||| an exception in the `JSIO` monad if the element is not found
||| or can't be safely cast to the desired type.
export
strictGetElementById : LiftJSIO m => SafeCast t => (tag,id : String) -> m t
strictGetElementById tag id = do
  Nothing <- castElementById t id | Just t => pure t
  liftJSIO $ throwError $
    Caught "Control.Monad.Dom.Interface.strictGetElementById: Could not find \{tag} with id \{id}"

||| Tries to retrieve a HTMLElement by looking
||| up its ID in the DOM. Unlike `getElementById`, this will throw
||| an exception in the `JSIO` monad if the element is not found
||| or can't be safely cast to the desired type.
export %inline
strictGetHTMLElementById : LiftJSIO m => (tag,id : String) -> m HTMLElement
strictGetHTMLElementById = strictGetElementById

||| Tries to retrieve an element of the given type by looking
||| up its ID in the DOM. Unlike `getElementById`, this will throw
||| an exception in the `JSIO` monad if the element is not found
||| or can't be safely cast to the desired type.
export
getElementByRef : LiftJSIO m => SafeCast t => ElemRef t -> m t
getElementByRef (Id {tag} _ id) = strictGetElementById tag id
getElementByRef (Class _ class) = getElementByClass class
getElementByRef (Ref t)         = pure t
getElementByRef Body            = liftJSIO body
getElementByRef Document        = liftJSIO document
getElementByRef Window          = liftJSIO window

err : String
err = "Control.Monad.Dom.Interface.castElementByRef"

||| Tries to retrieve an element of the given type by looking
||| up its ID in the DOM. Unlike `getElementById`, this will throw
||| an exception in the `JSIO` monad if the element is not found
||| or can't be safely cast to the desired type.
export
castElementByRef : LiftJSIO m => SafeCast t2 => ElemRef t -> m t2
castElementByRef (Id {tag} _ id) = strictGetElementById tag id
castElementByRef (Class _ class) = getElementByClass class
castElementByRef Body            = liftJSIO $ body >>= tryCast err
castElementByRef Document        = liftJSIO $ document >>= tryCast err
castElementByRef Window          = liftJSIO $ window >>= tryCast err
castElementByRef (Ref t)         = liftJSIO $ tryCast err t

||| Sets up the reactive behavior of the given `Node` and
||| inserts it as the only child of the given target.
|||
||| This adds unique IDs and event listeners to the generated
||| nodes as required in their attributes.
export
innerHtmlAtN :  LiftJSIO m
             => MonadRec m
             => MonadDom ev m
             => ElemRef t
             -> List (Node ev)
             -> m ()
innerHtmlAtN ref ns = do
  elem     <- castElementByRef {t2 = Element} ref
  (n2, es) <- prepareNodes ns
  liftJSIO $ innerHTML elem .= renderMany n2
  forM_ (\x => x) es

||| Sets up the reactive behavior of the given `Node` and
||| inserts it as the only child of the given target.
|||
||| This adds unique IDs and event listeners to the generated
||| nodes as required in their attributes.
export
innerHtmlAt :  LiftJSIO m
            => MonadRec m
            => MonadDom ev m
            => ElemRef t
            -> Node ev
            -> m ()
innerHtmlAt ref n = do
  elem     <- castElementByRef {t2 = Element} ref
  (n2, es) <- prepareNode n
  liftJSIO $ innerHTML elem .= render n2
  forM_ (\x => x) es

||| Replaces the `innerHTML` property of the target with the
||| given `String`. Warning: The string will not be escaped
||| before being inserted, so don't use this with text from
||| untrusted sources.
export
rawInnerHtmlAt :  LiftJSIO m
               => ElemRef t
               -> String
               -> m ()
rawInnerHtmlAt ref str = liftJSIO $ do
  elem <- castElementByRef {t2 = Element} ref
  liftJSIO $ innerHTML elem .= str


text:
module Flexidisc.Record.Transformation

import Flexidisc.Record
import Flexidisc.RecordContent
import Flexidisc.OrdList.Disjoint
import Flexidisc.OrdList.Nub
import public Flexidisc.Transformation.Type
import public Flexidisc.Transformation.TransHeader

import public Control.Monad.Identity

%default total
%access export

||| A list of transformation of tagged values.
||| Its purpose is to apply several transformation on different fields
||| simultaneously.
data TransformationM : (m : Type -> Type) -> (k : Type) ->
                       (header : TransHeader k) -> Type where
  Trans : (o : Ord k) =>
          (values : MapValuesM m k o header) ->
          (nubProof : Nub header) ->
          TransformationM m k (T header)

public export
Transformation : (k : Type) -> (header : TransHeader k) -> Type
Transformation = TransformationM id

||| Monomorphic `id` to help inference
transM : (m : Type -> Type) -> TransformationM m k header -> TransformationM m k header
transM _ = id

||| Monomorphic `id` to help inference
trans : TransformationM Identity k header -> TransformationM Identity k header
trans = id

||| The empty record
Nil : Ord k => TransformationM m k []
Nil = Trans [] []

||| Insert a new transformation function in a `Transformation`
(::) : (DecEq k, Ord k) => TaggedValue k' (s -> m t) -> TransformationM m k header ->
       {default SoTrue fresh : IsFresh k' header} ->
       TransformationM m k ((k', s :-> t) :: header)
(::) x (Trans xs isnub) {fresh} =
  Trans (insert x xs) (freshInsert (getProof fresh) isnub)

transPreservesFresh : Ord k => (xs : OrdList k o MapValue) -> (y : Fresh l (toSource xs)) -> Fresh l (toTarget xs)
transPreservesFresh [] y = y
transPreservesFresh ((k, s :-> t) :: xs) (f :: fresh) = f :: transPreservesFresh xs fresh

transPreservesNub : (header : OrdList k o MapValue) -> Nub (toSource header) -> Nub (toTarget header)
transPreservesNub [] xs = xs
transPreservesNub ((l, s :-> t) :: xs) (y::ys) = transPreservesFresh xs y :: transPreservesNub xs ys

||| Map all the field of a record
mapRecord : (trans : TransformationM m k mapper) ->
            (xs : Record k (toSource mapper)) ->
            RecordM m k (toTarget mapper)
mapRecord (Trans trans nubT) (Rec xs nubXS) {mapper = T mapper} =
  Rec (mapRecord trans xs) (transPreservesNub mapper nubXS)

||| Map all the field of a record, extract the effect
traverseRecord : Applicative m =>
                 (trans : TransformationM m k mapper) ->
                 (xs : Record k (toSource mapper)) ->
                 m (Record k (toTarget mapper))
traverseRecord (Trans trans nubT) (Rec xs nubXS) {mapper = T mapper} =
  map (flip Rec (transPreservesNub mapper nubXS)) (traverseRecord trans xs)

||| Map all the field of a record
traverseRecord' : (trans : Transformation k mapper) ->
                  (xs : Record k (toSource mapper)) ->
                  Record k (toTarget mapper)
traverseRecord' = mapRecord

||| Create a record of Maybe type, with the values of the initial record,
||| if defined, or with `Nothing` if the field is not defined.
optional : DecEq k =>
           (xs : Record k header) ->
           {auto prf : HereOrNot post header} ->
           {default SoTrue postNub : IsNub post} ->
           RecordM Maybe k post
optional (Rec xs nubXS) {prf = HN prf} {postNub} =
  Rec (optional xs prf) (getProof postNub)

||| Change the effect
hoist : (f: {a : _} -> m a -> n a) -> (xs : RecordM m k header) -> RecordM n k header
hoist f (Rec xs nubXS) = Rec (hoist f xs) nubXS

||| Perform a `Record` transformation under the `Identity` Monad
withIdentity : (RecordM Identity k pre -> RecordM Identity k post) ->
               Record k pre -> Record k post
withIdentity f = hoist runIdentity . f . hoist Id

||| lift fields of a Record
lift : (f: {a : _} -> a -> m a) -> (xs : Record k header) -> RecordM m k header
lift = hoist

||| extract an effect from a record
sequence : Applicative m => (xs : RecordM m k header) -> m (Record k header)
sequence (Rec xs nubXS) = flip Rec nubXS <$> sequence xs

||| embed the effect in the values, directly into the `Record`
unlift : RecordM m k header -> Record k (map m header)
unlift (Rec values nubProof) = Rec (unlift values) (mapValuesPreservesNub nubProof)

||| Map a subset of a record
patchRecord : (DecEq k, Applicative m) =>
              (trans : TransformationM m k mapper) ->
              (xs : Record k header) ->
              {auto prf : Sub (toSource mapper) header} ->
              m (Record k (patch (toTarget mapper) header))
patchRecord (Trans trans nubT) (Rec xs nubXS) {prf = S prf} {mapper = T mapper} = let
  nubProof = disjointNub diffIsDisjoint
                         (isNubFromSub diffIsSub nubXS)
                         (transPreservesNub mapper (isNubFromSub prf nubXS))
  in map (flip Rec nubProof) (patchRecord trans xs prf)

||| Map a subset of a record
patchRecord' : DecEq k =>
               (trans : Transformation k mapper) ->
               (xs : Record k header) ->
               {auto prf : Sub (toSource mapper) header} ->
               Record k (patch (toTarget mapper) header)
patchRecord' (Trans trans nubT) (Rec xs nubXS) {prf = S prf} {mapper = T mapper} = let
  nubProof = disjointNub diffIsDisjoint
                         (isNubFromSub diffIsSub nubXS)
                         (transPreservesNub mapper (isNubFromSub prf nubXS))
  in (flip Rec nubProof) (patchRecord' trans xs prf)

-- Foldmap

public export
data RecordFunc : (required : Header k) ->
                  (optional : Header k) ->
                  (result : Type) -> Type where
  Func : (Record k required -> RecordM Maybe k opt -> a) ->
         RecordFunc required opt a

||| Apply a function on a known set of data
foldRecord : (Ord k, DecEq k) =>
             RecordFunc required opt a ->
             Record k header ->
             {auto optNub : IsNub opt} ->
             {auto decomp : Decomp required opt header} ->
             a
foldRecord (Func f) xs {decomp = D sub op} {optNub} =
  f (project xs) (optional xs {postNub = optNub})

||| Apply a modifier Record to a record
(<**>) : RecordM (endoM m n) k header -> RecordM m k header -> RecordM n k header
(<**>) (Rec fs _) (Rec xs nubXS) = Rec (fs <**> xs) nubXS

-- Operators

keepIf : (Alternative m, Applicative m) => (a -> Bool) -> a -> m a
keepIf f x = map (const x) (guard (f x))

is : (Eq a, Alternative m, Applicative m) => a -> a -> m a
is expected = keepIf (== expected)

isnot : (Eq a, Alternative m, Applicative m) => a -> a -> m a
isnot expected = keepIf (/= expected)

ext: idr

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module PurelyFunctionalState

import Verified

||| The State Functor, abstracts all the combinators
||| We'll be using in this chapter
|||
data MyState s a =
    StateAction (s -> (a, s))

||| To fold MyState s a into (a, s) you need to give it an initial state
|||
runMyState : MyState s a -> s -> (a, s)
runMyState (StateAction action) = action

||| Like runMyState except that it drops the value and just returns the final state
|||
execMyState : MyState s a -> s -> s
execMyState ma st = snd (runMyState ma st)

-- Need to define the combinators, we're in a strict environment, so you have to start from the most
-- generic one and work your way down...

bindMyState : MyState s a -> (a -> MyState s b) -> MyState s b
bindMyState mx f = StateAction stateAction
    where
        stateAction : s -> (b, s)
        stateAction st = let (x, st1) = runMyState mx st in runMyState (f x) st1

pureMyState : a -> MyState s a
pureMyState x = StateAction (\st => (x, st))

mapMyState : (a -> b) -> MyState s a -> MyState s b
mapMyState f mx = bindMyState mx (pureMyState . f)

lift2MyState : (a -> b -> c) -> MyState s a -> MyState s b -> MyState s c
lift2MyState g mx my = bindMyState mx (\x => bindMyState my (\y => pureMyState (g x y)))

applyMyState : MyState s (a -> b) -> MyState s a -> MyState s b
applyMyState = lift2MyState id

-- instances

instance Functor (MyState s) where
    map = mapMyState

instance VerifiedFunctor (MyState s) where
    mapIdentity fa = ?mapIdentityMyState_rhs
    mapComposition fa k g = ?mapCompositionMyState_rhs

instance Applicative (MyState s) where
    pure = pureMyState
    (<*>) = applyMyState

||| a lot of these are hard to prove without a notion of extensional equality for functions,
||| since these proofs wont be used in programs,
||| I'm happy to cheat with believe_me.
|||
extensionalEquality : (f : a -> b) -> (g : a -> b) -> (x : a) -> (f x = g x )-> f = g
extensionalEquality f g x = believe_me

instance VerifiedApplicative (MyState s) where
    applicativePureId v = ?applicativePureIdMyState_rhs

    applicativeComposition (StateAction u) (StateAction v) (StateAction w) = ?applicativeCompositionMyState_rhs

    applicativeHomomorphism k x = ?applicativeHomomorphismMyState_rhs

    applicativeInterchange u y = ?applicativeInterchangeMyState_rhs

instance Monad (MyState s) where
    (>>=) = bindMyState

instance VerifiedMonad (MyState s) where
    monadPureIdentityL k x = ?monadPureIdentityLMyState_rhs

    monadPureIdentityR ma = ?monadPureIdentityLMyState_rhs

    monadBindAssociative k h ma = ?monadBindAssociativeMyState_rhs

    monadBindApplySame f mx my = ?monadBindApplySameMyState_rhs

-- exercises

-- I skipped the RNG related exercises as Idris' RNG and Int manipulation functions are sort of immature.

||| Exercise 6 : Implement map2 for MyState
|||
total
map2 : (a -> b -> c) -> MyState s a -> MyState s b -> MyState s c
map2 = lift2MyState

||| Exercise 6 : Implement map2 for MyState
|||
||| see map2
|||
total
exercise6 : (a -> b -> c) -> MyState s a -> MyState s b -> MyState s c
exercise6 = map2

total
traverseMyStateList : (a -> MyState s b) -> List a -> MyState s (List b)
traverseMyStateList f xs = foldr (foldFunc f) (pure (the (List b) Nil)) xs
    where
        foldFunc : (a -> MyState s b) -> a -> MyState s (List b) -> MyState s (List b)
        foldFunc g x mys = lift2MyState (::) (g x) mys
||| Exercise 7 : Implement SequenceList for a list of MyState
|||
total
sequenceMyStateList : List (MyState s a) -> MyState s (List a)
sequenceMyStateList = traverseMyStateList id

||| Exercise 7 : Implement SequenceList for a list of MyState.
|||
||| see sequenceMyStateList
|||
total
exercise7 : List (MyState s a) -> MyState s (List a)
exercise7 = sequenceMyStateList

||| Exercise 8 : Implement bindMyState
|||
||| see bindMyState
|||
total
exercise8 : MyState s a -> (a -> MyState s b) -> MyState s b
exercise8 = bindMyState

||| Exercise 9 : Reimplement map and map2 in terms of bindMyState,
||| (I already wrote map2 in terms of bindMyState).
|||
|||
total
mapMyState2 : (a -> b) -> MyState s a -> MyState s b
mapMyState2 f ma = bindMyState ma (pureMyState . f)

||| Exercise 9 : Reimplement map and map2 in terms of bindMyState,
||| (I already wrote map2 in terms of bindMyState).
|||
||| so see mapMyState2.
|||
total
exercise9 : (a -> b) -> MyState s a -> MyState s b
exercise9 = mapMyState2

-- Exercise 10 is all the Functor, Applicative and Monad functions for MyState.
-- which is already done, see the Functor, Applicative and Monad instances for
-- MyState,
--
-- Also see sequenceMyStateList

||| State type for Exercise 11
data CoinMachineState = CoinMachineS Bool Int Int

total
isLocked : CoinMachineState -> Bool
isLocked (CoinMachineS b x y) = b

total
candies : CoinMachineState -> Int
candies (CoinMachineS b x y) = x

total
coins : CoinMachineState -> Int
coins (CoinMachineS b x y) = y

data MachineAction = InsertCoin | TurnKnob

||| Common function for MyState, gets the value of the State
|||
total
getMyState : MyState s s
getMyState = StateAction (\x => (x, x))

||| applies a function to the state and returns the result
|||
total
getsMyState : (s -> a) -> MyState s a
getsMyState f = mapMyState f getMyState

||| This function allows you to write to the state
|||
total
putMyState : s -> MyState s ()
putMyState newState = StateAction (\oldState => ((), newState))

||| Given a conditional, will run the applicative action unless the conditional is False
|||
||| @ b The Conditional
||| @ action the action to run when the conditional is False
|||
total
unlessA : (Applicative f) => (b : Bool) -> (action : f ()) -> f ()
unlessA b action = if b then pure () else action

total
isOutOfCandy : MyState CoinMachineState Bool
isOutOfCandy = do
    candyCount <- getsMyState candies
    pure (candyCount == 0)

total
ifCandy : MyState CoinMachineState () -> MyState CoinMachineState ()
ifCandy action = do
    isOut <- isOutOfCandy
    unlessA isOut action

total
ifUnlocked : MyState CoinMachineState () -> MyState CoinMachineState ()
ifUnlocked action = do
    locked <- getsMyState isLocked
    unlessA locked action

total
ifLocked : MyState CoinMachineState () -> MyState CoinMachineState ()
ifLocked action = do
    locked <- getsMyState isLocked
    when locked action

total
runAction : MachineAction -> MyState CoinMachineState ()
runAction InsertCoin  = ifCandy (
    do
        coins' <- getsMyState coins
        candies' <- getsMyState candies
        putMyState (CoinMachineS False candies' (coins' + 1))
    )
runAction TurnKnob    = ifCandy (ifUnlocked (
    do
        coins' <- getsMyState coins
        candies' <- getsMyState candies
        putMyState (CoinMachineS True (candies' - 1) coins')
    ))

initialState : Int -> Int -> CoinMachineState
initialState = CoinMachineS True

||| Exercise 11 - simulateMachine
|||
total
simulationMachine : (candy : Int) -> (coin : Int) -> (actions : List MachineAction) -> CoinMachineState
simulationMachine candy coin = flip execMyState (initialState candy coin) . traverseMyStateList runAction

max_stars_repo_name: ajnavarro/language-dataset

max_issues_repo_name: ajnavarro/language-dataset

max_forks_repo_name: ajnavarro/language-dataset


text:
module Language.LSP.DocumentSymbol

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.Name
import Data.List
import Idris.Doc.String
import Language.LSP.Message
import Libraries.Data.NameMap
import Server.Configuration
import Server.Log
import Server.Utils

-- NOTE: Structured information should be rendereded from the actual Term of the expressions
-- in a file, that would give a better high-level overview. For now this is more like a placeholder
-- rather than a useful functionality.
-- NOTE: Global symbols considered as functions, meta symbols considered as Variables.

||| Check if the name is visible in the local namespaces, if yes return Just its full name, otherwise Nothing.
||| This function meant to be used with GlobalNames.
checkVisibleName : Ref Ctxt Defs => List Namespace -> Name -> Core (Maybe Name)
checkVisibleName namespaces name = do
  fullName <- toFullNames name
  let True = isUserName fullName
      | False => pure Nothing
  let (Just fullNamespace, _) = displayName fullName
      | _ => pure Nothing
  pure
    $ if elem fullNamespace namespaces
        then Just fullName
        else Nothing

||| Check if the name is visible and returns the associated NonEmpty location.
currentNSNameWithLoc : Ref Ctxt Defs => List Namespace -> Name -> Core (Maybe (Name, FilePos, FilePos))
currentNSNameWithLoc namespaces name = do
  Just visibleName <- checkVisibleName namespaces name
    | Nothing => pure Nothing
  defs <- get Ctxt
  Just gdef <- lookupCtxtExact visibleName defs.gamma
    | Nothing => pure Nothing
  pure $ case gdef.location of
    EmptyFC                 => Nothing
    MkFC        _ start end => Just (gdef.fullname, start, end)
    MkVirtualFC _ start end => Just (gdef.fullname, start, end)

||| Render all names form Meta and current namespace matching Global names as SymbolInformation.
||| The LSP client needs to handle the SymbolInformations correctly.
export
documentSymbol : Ref Ctxt Defs
              => Ref MD Metadata
              => Ref LSPConf LSPConfiguration
              => DocumentSymbolParams -> Core (List SymbolInformation)
documentSymbol params = do
  Just (uri, _) <- gets LSPConf openFile
    | Nothing => do
        logString Debug "documentSymbol: openFile returned Nothing. This shouldn't happen."
        pure []
  let True = uri == params.textDocument.uri
      | False => do
          logString Debug "documentSymbol: different URI than expected \{show (uri, params.textDocument.uri)}"
          pure []
  defs <- get Ctxt
  -- Get the current and visible namespaces from the context
  let currentNamespaces = defs.currentNS :: defs.nestedNS
  -- Get all resolved names, which are in the visible namesspaces
  let knownNames = NameMap.keys $ namesResolvedAs defs.gamma
  -- Render global and meta names as SymbolInformation
  visibleNames <- map catMaybes $ traverse (currentNSNameWithLoc currentNamespaces) knownNames
  let globalDocSymbols
        = map (\(n, (sline,scol), (eline, ecol)) =>
                let range = MkRange (MkPosition sline scol) (MkPosition eline ecol)
                    name = show $ dropNS n
                 in MkSymbolInformation
                    { name          = name
                    , kind          = Function
                    , tags          = Nothing
                    , deprecated    = Nothing
                    , location      = MkLocation params.textDocument.uri range
                    , containerName = Nothing
                    })
              visibleNames
  meta <- get MD
  let metaDocSymbols
        = map (\((_, (sline, scol), (eline, ecol)), (metaName, _, _)) =>
                let range = MkRange (MkPosition sline scol) (MkPosition eline ecol)
                    name = show $ dropNS metaName
                 in MkSymbolInformation
                    { name          = name
                    , kind          = Variable
                    , tags          = Nothing
                    , deprecated    = Nothing
                    , location      = MkLocation params.textDocument.uri range
                    , containerName = Nothing
                    })
              meta.names
  let docSymbols = globalDocSymbols ++ metaDocSymbols
  logString Debug "documentSymbol: Found \{show (length globalDocSymbols)} global and \{show (length metaDocSymbols)} meta document symbols."
  pure $ docSymbols


text:
module Data.Queue

import Data.SnocList

%default total

export
record Queue (a : Type) where
  constructor MkQueue
  front : List a
  back  : SnocList a

export
empty : Queue a
empty = MkQueue [] [<]

export
push : a -> Queue a -> Queue a
push x = { back $= (:< x) }

export
pop : Queue a -> Maybe (a, Queue a)
pop (MkQueue [] sx) = case sx <>> [] of
  [] => Nothing
  (x :: xs) => Just (x, MkQueue xs [<])
pop (MkQueue (x :: xs) ys) = Just (x, MkQueue xs ys)

export
Functor Queue where
  map f = { front $= map f, back $= map f }

export
Foldable Queue where
  foldr c n (MkQueue xs ys) = foldr c (foldr c n ys) xs

max_stars_repo_name: gallais/ncurses-idris

max_issues_repo_name: gallais/ncurses-idris

max_forks_repo_name: gallais/ncurses-idris


text:
module Main

import Syntax.Lexer
import Syntax.Tokens
import Error
import Loc

main : IO ()
main = case lex "(test \"test something\" 10)" of
          Right res => putStr (concatMap ((++ "\n") . show) res)
          Left _ => putStrLn "Error"

max_stars_repo_name: felipegchi/Yurei

max_issues_repo_name: felipegchi/Yurei

max_forks_repo_name: felipegchi/Yurei


text:
||| Implementation  of ordering relations for `Fin`ite numbers
module Data.Fin.Order

import Data.Fin
import Data.Fun
import Data.Rel
import Data.Nat
import Data.Nat.Order
import Decidable.Decidable
import Decidable.Order

using (k : Nat)
  data FinLTE : Fin k -> Fin k -> Type where
    FromNatPrf : {m : Fin k} -> {n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n

  implementation Preorder (Fin k) FinLTE where
    transitive m n o (FromNatPrf p1) (FromNatPrf p2) =
      FromNatPrf (LTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)
    reflexive n = FromNatPrf (LTEIsReflexive (finToNat n))

  implementation Poset (Fin k) FinLTE where
    antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =
      finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)

  implementation Decidable [Fin k, Fin k] FinLTE where
    decide m n with (decideLTE (finToNat m) (finToNat n))
      decide m n | Yes prf    = Yes (FromNatPrf prf)
      decide m n | No  disprf = No (\ (FromNatPrf prf) => disprf prf)

  implementation Ordered (Fin k) FinLTE where
    order m n =
      either (Left . FromNatPrf)
             (Right . FromNatPrf)
             (order (finToNat m) (finToNat n))


text:
module Remotelib2

import Remotelib1

export
rem2 : String
rem2 = rem1  ++ " - what a delight!"

max_stars_repo_name: idream-build/idream

max_issues_repo_name: idream-build/idream

max_forks_repo_name: idream-build/idream


text:
module EqNat

public export
data EqNat : (num1 : Nat) -> (num2 : Nat) -> Type where
     Same : (num : Nat) -> EqNat num num

-- sameS : (eq : EqNat k j) -> EqNat (S k) (S j)
-- sameS (Same j) = Same (S j)

public export
checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (EqNat num1 num2)
checkEqNat Z Z = Just $ Same Z
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                         Nothing => Nothing
                         Just (Same j) => Just $ Same (S j)


text:
infixr 6 -*
(-*) : Type -> Type -> Type
(-*) a b = (1 _ : a) -> b

-- Test that the types of holes are not overly generalised wrt the
-- multiplicities in the function type

foo1 : (((1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()) -> ()) -> ()
foo1 f = f ?foo1h

foo2 : (((1 _ : a) -> (1 _ : b) -> (1 _ : c) -> ()) -> ()) -> ()
foo2 f = f (id ?foo2h)

foo3 : ((a -* b -* c -* ()) -> ()) -> ()
foo3 f = f (id ?foo3h)


text:
module Common.Felt

-- Idris2 does not support pattern matching on [external] types.
-- Do not declare public since it allows to write pattern matching code which does not work
export
data Felt : Type where [external]

public export %extern
prim__mk_Felt : Integer -> Felt

public export %extern
prim__from_Felt : Felt -> Integer

public export %extern
prim__add_Felt : Felt -> Felt -> Felt

public export %extern
prim__mul_Felt : Felt -> Felt -> Felt

public export %extern
prim__sub_Felt : Felt -> Felt -> Felt

public export %extern
prim__div_Felt : Felt -> Felt -> Felt

public export %extern
prim__eq_Felt : Felt -> Felt -> Bool

public export %inline
Eq Felt where
  (==) = prim__eq_Felt

public export %inline
Num Felt where
  (+) = prim__add_Felt
  (*) = prim__mul_Felt
  fromInteger = prim__mk_Felt

public export %inline
Neg Felt where
  negate x = assert_total $ prim__sub_Felt (fromInteger 0) x
  a - b = prim__sub_Felt a b

public export %inline
Integral Felt where
  div = prim__div_Felt
  mod _ _ = prim__mk_Felt 0 -- In a primefield divisions do not have a rest

public export %inline
Show Felt where
  show = show . prim__from_Felt

public export %inline
[PlusFeltSemi] Semigroup Felt using Semigroup.Additive where
  (<+>) x y = x + y

public export %inline
[MultFeltSemi] Semigroup Felt using Semigroup.Multiplicative where
  (<+>) x y = x * y

public export %inline
[PlusFeltMonoid] Monoid Felt using Monoid.Additive PlusFeltSemi where
  neutral = 0

public export %inline
[MultFeltMonoid] Monoid Felt using Monoid.Multiplicative MultFeltSemi where
  neutral = 1

{-
TODO: How to treat partiallity?

%inline
partial
public export
Integral Felt where
  div x y
      = case y == 0 of
             False => prim__div_Felt x y
  mod x y
      = case y == 0 of
             False => prim__mod_Felt x y

-}

public export %inline
Cast Bool Felt where
  cast True = 1
  cast False = 0

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Compiler.LLVM.Rapid.Closure

import Core.Name

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

-- A "fat" closure is always invoked via its "closure entry" function
export
FAT_CLOSURE_LIMIT : Int
FAT_CLOSURE_LIMIT = 8

CLOSURE_MAX_ARGS : Int
CLOSURE_MAX_ARGS = 1024

export
mkClosure : Name -> Nat -> List (IRValue IRObjPtr) -> Codegen (IRValue IRObjPtr)
mkClosure n missingN [] =
  pure $ SSA IRObjPtr $ "bitcast ({i64, %FuncPtr} addrspace(1)* @\{safeName n}$$closureNoArgs to %ObjPtr)"

mkClosure n missingN args = do
  let missing = cast {to=Int} missingN
  let len = cast {to=Int} $ length args
  let totalArgsExpected = missing + len
  if totalArgsExpected > (cast CLOSURE_MAX_ARGS)
     then do
       addError $ "ERROR : too many closure arguments: " ++ show totalArgsExpected ++ " > " ++ show CLOSURE_MAX_ARGS
       pure nullPtr
     else do
  let header = constHeader OBJECT_TYPE_ID_CLOSURE (cast ((missing * 0x10000) + len))
  newObj <- dynamicAllocate (Const I64 $ cast (8 + 8 * len))
  putObjectHeader newObj header
  funcPtr <- (if (totalArgsExpected <= (cast FAT_CLOSURE_LIMIT))
             then
               assignSSA $ "bitcast %FuncPtrArgs" ++ show totalArgsExpected ++ " @" ++ (safeName n) ++ " to %FuncPtr"
             else do
               assignSSA $ "bitcast %FuncPtrClosureEntry @" ++ (safeName n) ++ "$$closureEntry to %FuncPtr"
               )

  putObjectSlot newObj (Const I64 0) (SSA FuncPtr funcPtr)
  for_ (enumerate args) (\iv => do
      let (i, argObj) = iv
      putObjectSlot newObj (Const I64 $ cast $ i+1) argObj
      pure ()
      )
  pure newObj


text:
module Cast

%default total

{-
  interface Cast from to where
    caset : (orig : from) -> to

-}

Cast (Maybe elem) (List elem) where
  cast Nothing = []
  cast (Just x) = [x]

foo : List Integer
foo = cast (Just 100)

bar : List Integer
bar = cast (the (Maybe Integer) Nothing)

Cast (List elem) (Maybe elem) where
  cast [] = Nothing
  cast (x :: xs) = Just x

baz : Maybe Int
baz = cast  (the (List Int) [99])

quux : Maybe Int
quux = cast (the (List Int) [])

-- there is nothing special about the Cast interface. We can define our own version

interface Mould from to where
  mould : (oig : from) -> to

Mould (Maybe elem) (List elem) where
  mould Nothing = []
  mould (Just x) = [x]

foofoo : List String
foofoo = mould (the (Maybe String) (Just "Hello"))

barbar : List String
barbar = mould (the (Maybe String) Nothing)

Mould (List elem) (Maybe elem) where
  mould [] = Nothing
  mould (x :: xs) = Just x

bazbaz : Maybe String
bazbaz = mould (the (List String) ["world"])

quuxquux : Maybe String
quuxquux = mould (the (List String) [])

max_stars_repo_name: timmyjose-study/tdd-with-idris

max_issues_repo_name: timmyjose-study/tdd-with-idris

max_forks_repo_name: timmyjose-study/tdd-with-idris


text:
module Compiler.LLVM.IR

import Core.Name

import Control.Codegen
import Data.Utils

isSafeChar : Char -> Bool
isSafeChar '.' = True
isSafeChar '_' = True
isSafeChar c = isAlphaNum c

fullShow : Name -> String
fullShow (NS ns n) = showNSWithSep "." ns ++ "." ++ fullShow n
fullShow (UN (Basic n)) = n
fullShow (UN (Field n)) = "_.(" ++ n ++ ")"
fullShow (UN Underscore) = "_"
fullShow (MN n i) = "_{" ++ n ++ ":" ++ show i ++ "}"
fullShow (PV n i) = "_{P:" ++ fullShow n ++ ":" ++ show i ++ "}"
fullShow (DN _ n) = fullShow n
fullShow (Nested (outer, idx) inner) = show outer ++ "/" ++ show idx ++ "/" ++ fullShow inner
fullShow (CaseBlock outer i) = "case/" ++ outer ++ "$" ++ show i
fullShow (WithBlock outer i) = "with/" ++ outer ++ "$" ++ show i
fullShow (Resolved i) = "resolved/" ++ show i

export
safeName : Name -> String
safeName s = concatMap okchar (unpack $ fullShow s)
  where
    okchar : Char -> String
    okchar c = if isSafeChar c
                  then cast c
                  else "$" ++ asHex (cast {to=Bits64} c)

public export
interface ToIR a where
  toIR : a -> String
  showWithoutType : a -> String

export
assignSSA : ToIR a => a -> Codegen String
assignSSA value = do
  i <- getUnique
  let varname = "%t" ++ show i
  appendCode ("  " ++ varname ++ " = " ++ (toIR value))
  pure varname

public export
data IRType = I1 | I8 | I16 | I32 | I64 | F64 | FuncPtr | IRObjPtr | Pointer Int IRType

export
Show IRType where
  show I1 = "i1"
  show I8 = "i8"
  show I16 = "i16"
  show I32 = "i32"
  show I64 = "i64"
  show F64 = "double"
  show FuncPtr = "%FuncPtr"
  show IRObjPtr = "%ObjPtr"
  show (Pointer i t) = (show t) ++ " addrspace(" ++ show i ++ ")*"

public export
data IRLabel = MkLabel String

public export
ToIR IRLabel where
  toIR (MkLabel l) = "label %" ++ l
  showWithoutType (MkLabel l) = "%" ++ l

export
beginLabel : IRLabel -> Codegen ()
beginLabel (MkLabel l) = appendCode (l ++ ":")

export
genLabel : String -> Codegen IRLabel
genLabel s = MkLabel <$> mkVarName ("glbl_" ++ s)

export
RuntimePtr : IRType
RuntimePtr = Pointer 0 I8

public export
data IRValue : IRType -> Type where
  Const : (t : IRType) -> Integer -> IRValue t
  ConstI64 : Integer -> IRValue I64
  ConstF64 : Double -> IRValue F64
  SSA : (t : IRType) ->  String -> IRValue t
  IRDiscard : IRValue (Pointer 0 IRObjPtr)

export
total
ToIR (IRValue t) where
  toIR {t} (SSA t s) = (show t) ++ " " ++ s
  toIR (Const t i) = (show t) ++ " " ++ (show i)
  toIR (ConstI64 i) = "i64 " ++ (show i)
  toIR (ConstF64 f) = "double 0x" ++ (assert_total $ doubleToHex f)
  toIR (IRDiscard) = "ERROR: trying to use DISCARD with type"

  showWithoutType (SSA _ n) = n
  showWithoutType (Const _ i) = show i
  showWithoutType (ConstI64 i) = show i
  showWithoutType (ConstF64 f) = "0x" ++ (assert_total $ doubleToHex f)
  showWithoutType (IRDiscard) = "ERROR: trying to use DISCARD without type"

export
nullPtr : IRValue IRObjPtr
nullPtr = SSA IRObjPtr "null"

export
pConst : Cast a Integer => {ty : IRType} -> a -> IRValue ty
pConst {ty} val = Const ty (cast {to=Integer} val)


text:
module Idris.REPL.Opts

import Compiler.Common
import Idris.Syntax
import Parser.Unlit
import TTImp.Interactive.ExprSearch
import TTImp.TTImp

import Data.List
import Data.List1
import Libraries.Data.List.Extra
import Data.String
import System.File
import Libraries.Data.String.Extra

%hide Data.String.lines
%hide Data.String.lines'
%hide Data.String.unlines
%hide Data.String.unlines'

%default total

namespace VerbosityLvl
  public export
  data VerbosityLvl =
   ||| Suppress all message output to `stdout`.
   NoneLvl |
   ||| Keep only errors.
   ErrorLvl |
   ||| Keep everything.
   InfoLvl

public export
data OutputMode
  = IDEMode Integer File File |
    ||| Given that we can divide elaboration messages into
    ||| two categories: informational message and error message,
    ||| `VerbosityLvl` applies a filter on the output,
    |||  suppressing writes to `stdout` if the level condition isn't met.
    REPL VerbosityLvl

public export
record REPLOpts where
  constructor MkREPLOpts
  showTypes : Bool
  evalMode : REPLEval
  mainfile : Maybe String
  literateStyle : Maybe LiterateStyle
  source : String
  editor : String
  errorLine : Maybe Int
  idemode : OutputMode
  currentElabSource : String
  psResult : Maybe (Name, Core (Search RawImp)) -- last proof search continuation (and name)
  gdResult : Maybe (Int, Core (Search (FC, List ImpClause))) -- last generate def continuation (and line number)
  evalResultName : Maybe Name
  -- TODO: Move extraCodegens from here, it doesn't belong, but there's nowhere
  -- better to stick it now.
  extraCodegens : List (String, Codegen)
  consoleWidth : Maybe Nat -- Nothing is auto
  color : Bool
  synHighlightOn : Bool

litStyle : Maybe String -> Maybe LiterateStyle
litStyle = join . map isLitFile

export
defaultOpts : Maybe String -> OutputMode -> List (String, Codegen) -> REPLOpts
defaultOpts fname outmode cgs
    = MkREPLOpts
        { showTypes = False
        , evalMode = NormaliseAll
        , mainfile = fname
        , literateStyle = litStyle fname
        , source = ""
        , editor = "vim"
        , errorLine = Nothing
        , idemode = outmode
        , currentElabSource = ""
        , psResult = Nothing
        , gdResult = Nothing
        , evalResultName = Nothing
        , extraCodegens = cgs
        , consoleWidth = Nothing
        , color = True
        , synHighlightOn = True
        }
  where
    litStyle : Maybe String -> Maybe LiterateStyle
    litStyle Nothing = Nothing
    litStyle (Just fn) = isLitFile fn

export
data ROpts : Type where

export
withROpts : {auto o : Ref ROpts REPLOpts} -> Core a -> Core a
withROpts = wrapRef ROpts (\_ => pure ())

export
setOutput : {auto o : Ref ROpts REPLOpts} ->
            OutputMode -> Core ()
setOutput m
    = do opts <- get ROpts
         put ROpts (record { idemode = m } opts)

export
getOutput : {auto o : Ref ROpts REPLOpts} -> Core OutputMode
getOutput = do opts <- get ROpts
               pure (idemode opts)

export
setMainFile : {auto o : Ref ROpts REPLOpts} ->
              Maybe String -> Core ()
setMainFile src
    = do opts <- get ROpts
         put ROpts (record { mainfile = src,
                             literateStyle = litStyle src } opts)

export
resetProofState : {auto o : Ref ROpts REPLOpts} ->
                  Core ()
resetProofState
    = do opts <- get ROpts
         put ROpts (record { psResult = Nothing,
                             gdResult = Nothing } opts)

export
setSource : {auto o : Ref ROpts REPLOpts} ->
            String -> Core ()
setSource src
    = do opts <- get ROpts
         put ROpts (record { source = src } opts)

export
getSource : {auto o : Ref ROpts REPLOpts} ->
            Core String
getSource
    = do opts <- get ROpts
         pure (source opts)

export
getSourceLine : {auto o : Ref ROpts REPLOpts} ->
                Int -> Core (Maybe String)
getSourceLine l
    = do src <- getSource
         pure $ elemAt (forget $ lines src) (integerToNat (cast (l-1)))

export
getLitStyle : {auto o : Ref ROpts REPLOpts} ->
              Core (Maybe LiterateStyle)
getLitStyle
    = do opts <- get ROpts
         pure (literateStyle opts)

export
setCurrentElabSource : {auto o : Ref ROpts REPLOpts} ->
                       String -> Core ()
setCurrentElabSource src
    = do opts <- get ROpts
         put ROpts (record { currentElabSource = src } opts)

export
getCurrentElabSource : {auto o : Ref ROpts REPLOpts} ->
                       Core String
getCurrentElabSource
     = do opts <- get ROpts
          pure (currentElabSource opts)

addCodegen : {auto o : Ref ROpts REPLOpts} ->
             String -> Codegen -> Core ()
addCodegen s cg = do opts <- get ROpts
                     put ROpts (record { extraCodegens $= ((s,cg)::) } opts)

export
getCodegen : {auto o : Ref ROpts REPLOpts} ->
             String -> Core (Maybe Codegen)
getCodegen s = do opts <- get ROpts
                  pure $ lookup s (extraCodegens opts)

export
getConsoleWidth : {auto o : Ref ROpts REPLOpts} -> Core (Maybe Nat)
getConsoleWidth = do opts <- get ROpts
                     pure $ opts.consoleWidth

export
setConsoleWidth : {auto o : Ref ROpts REPLOpts} -> Maybe Nat -> Core ()
setConsoleWidth n = do opts <- get ROpts
                       put ROpts (record { consoleWidth = n } opts)

export
getColor : {auto o : Ref ROpts REPLOpts} -> Core Bool
getColor = do opts <- get ROpts
              pure $ opts.color

export
setColor : {auto o : Ref ROpts REPLOpts} -> Bool -> Core ()
setColor b = do opts <- get ROpts
                put ROpts (record { color = b } opts)

export
getSynHighlightOn : {auto o : Ref ROpts REPLOpts} -> Core Bool
getSynHighlightOn = do opts <- get ROpts
                       pure $ opts.synHighlightOn

export
setSynHighlightOn : {auto o : Ref ROpts REPLOpts} -> Bool -> Core ()
setSynHighlightOn b = do opts <- get ROpts
                         put ROpts (record { synHighlightOn = b } opts)


text:
module Data.Bytes.Lazy

import public Data.Bytes.Lazy.Internal -- probably don't need this here
import public Data.Bytes.Lazy.API


text:
module Algebra.ZeroOneOmega

import Algebra.Semiring
import Algebra.Preorder

%default total

export
data ZeroOneOmega = Rig0 | Rig1 | RigW

export
Preorder ZeroOneOmega where
  Rig0 <=    _ = True
  Rig1 <= Rig1 = True
  _    <= RigW = True
  _    <=    _ = False
  preorderRefl {x = Rig0} = Refl
  preorderRefl {x = Rig1} = Refl
  preorderRefl {x = RigW} = Refl
  preorderTrans {x = Rig0} _ _ = Refl
  preorderTrans {x = Rig1} {y = Rig0} _ _ impossible
  preorderTrans {x = Rig1} {y = Rig1} _ yz = yz
  preorderTrans {x = Rig1} {y = RigW} {z = Rig0} _ _ impossible
  preorderTrans {x = Rig1} {y = RigW} {z = Rig1} _ _ = Refl
  preorderTrans {x = Rig1} {y = RigW} {z = RigW} _ _ = Refl
  preorderTrans {x = RigW} {y = Rig0} _ _ impossible
  preorderTrans {x = RigW} {y = Rig1} _ _ impossible
  preorderTrans {x = RigW} {y = RigW} _ yz = yz

public export
Eq ZeroOneOmega where
  (==) Rig0 Rig0 = True
  (==) Rig1 Rig1 = True
  (==) RigW RigW = True
  (==) _ _ = False

export
Show ZeroOneOmega where
  show Rig0 = "Rig0"
  show Rig1 = "Rig1"
  show RigW = "RigW"

export
rigPlus : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmega
rigPlus Rig0 a = a
rigPlus a Rig0 = a
rigPlus _ _ = RigW

export
rigMult : ZeroOneOmega -> ZeroOneOmega -> ZeroOneOmega
rigMult Rig0 _ = Rig0
rigMult _ Rig0 = Rig0
rigMult Rig1 a = a
rigMult a Rig1 = a
rigMult _ _ = RigW

public export
Semiring ZeroOneOmega where
  (|+|) = rigPlus
  (|*|) = rigMult
  plusNeutral = Rig0
  timesNeutral = Rig1

||| The top value of a lattice
export
Top ZeroOneOmega where
  top = RigW
  topAbs {x = Rig0} = Refl
  topAbs {x = Rig1} = Refl
  topAbs {x = RigW} = Refl

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

rigPlusAssociative : (x, y, z : ZeroOneOmega) ->
  rigPlus x (rigPlus y z) = rigPlus (rigPlus x y) z
rigPlusAssociative Rig0 _ _ = Refl
rigPlusAssociative Rig1 Rig0 _ = Refl
rigPlusAssociative Rig1 Rig1 Rig0 = Refl
rigPlusAssociative Rig1 Rig1 Rig1 = Refl
rigPlusAssociative Rig1 Rig1 RigW = Refl
rigPlusAssociative Rig1 RigW Rig0 = Refl
rigPlusAssociative Rig1 RigW Rig1 = Refl
rigPlusAssociative Rig1 RigW RigW = Refl
rigPlusAssociative RigW Rig0 _ = Refl
rigPlusAssociative RigW Rig1 Rig0 = Refl
rigPlusAssociative RigW Rig1 Rig1 = Refl
rigPlusAssociative RigW Rig1 RigW = Refl
rigPlusAssociative RigW RigW Rig0 = Refl
rigPlusAssociative RigW RigW Rig1 = Refl
rigPlusAssociative RigW RigW RigW = Refl

rigPlusCommutative : (x, y : ZeroOneOmega) ->
  rigPlus x y = rigPlus y x
rigPlusCommutative Rig0 Rig0 = Refl
rigPlusCommutative Rig0 Rig1 = Refl
rigPlusCommutative Rig0 RigW = Refl
rigPlusCommutative Rig1 Rig0 = Refl
rigPlusCommutative Rig1 Rig1 = Refl
rigPlusCommutative Rig1 RigW = Refl
rigPlusCommutative RigW Rig0 = Refl
rigPlusCommutative RigW Rig1 = Refl
rigPlusCommutative RigW RigW = Refl

rigMultAssociative : (x, y, z : ZeroOneOmega) ->
  rigMult x (rigMult y z) = rigMult (rigMult x y) z
rigMultAssociative Rig0 _ _ = Refl
rigMultAssociative Rig1 Rig0 _ = Refl
rigMultAssociative Rig1 Rig1 Rig0 = Refl
rigMultAssociative Rig1 Rig1 Rig1 = Refl
rigMultAssociative Rig1 Rig1 RigW = Refl
rigMultAssociative Rig1 RigW Rig0 = Refl
rigMultAssociative Rig1 RigW Rig1 = Refl
rigMultAssociative Rig1 RigW RigW = Refl
rigMultAssociative RigW Rig0 _ = Refl
rigMultAssociative RigW Rig1 Rig0 = Refl
rigMultAssociative RigW Rig1 Rig1 = Refl
rigMultAssociative RigW Rig1 RigW = Refl
rigMultAssociative RigW RigW Rig0 = Refl
rigMultAssociative RigW RigW Rig1 = Refl
rigMultAssociative RigW RigW RigW = Refl

rigMultCommutative : (x, y : ZeroOneOmega) ->
  rigMult x y = rigMult y x
rigMultCommutative Rig0 Rig0 = Refl
rigMultCommutative Rig0 Rig1 = Refl
rigMultCommutative Rig0 RigW = Refl
rigMultCommutative Rig1 Rig0 = Refl
rigMultCommutative Rig1 Rig1 = Refl
rigMultCommutative Rig1 RigW = Refl
rigMultCommutative RigW Rig0 = Refl
rigMultCommutative RigW Rig1 = Refl
rigMultCommutative RigW RigW = Refl


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

import public Config.Error
import public Config.YAML

%access export

-- ------------------------------------------------------------ [ YAML Parsing ]

{-
Schema is

file ::= pattern+
pattern ::= "pattern": {"problem":!!str, "solution": (vale::!!str)}

-}

private
getString : YAMLNode -> Maybe String
getString (YAMLString s) = Just s
getString _              = Nothing

private
isPatternMap : YAMLNode -> Bool
isPatternMap (YAMLString str) = toLower str == "pattern"
isPatternMap _ = False

private
getPatternKVPairs : YAMLNode -> List (YAMLNode)
getPatternKVPairs (YAMLDoc _ doc) with (doc)
  | (YAMLMap ps) = map snd $ filter (\(x,y) => isPatternMap x) ps
  | otherwise = Nil
getPatternKVPairs _ = Nil

private
getStringKey : (YAMLNode, YAMLNode) -> Maybe String
getStringKey (k,_) = getString k

private
getStringValue : (YAMLNode, YAMLNode) -> Maybe String
getStringValue (_,v) = getString v

private
getPSPair : YAMLNode -> Maybe (String, String)
getPSPair (YAMLMap [p,s]) =
    case (getStringKey p, getStringKey s) of
      (Just p', Just s') =>
        if toLower p' == "problem" && toLower s' == "solution"
          then case (getStringValue p, getStringValue s) of
            (Just p'', Just s'') => Just (p'', s'')
            otherwise            => Nothing
          else Nothing
      otherwise          => Nothing
getPSPair _  = Nothing

filterPreludeIDX : YAMLNode -> List (String, String)
filterPreludeIDX doc = mapMaybe (getPSPair) $ getPatternKVPairs doc

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

max_stars_repo_name: jfdm/sif-lang

max_issues_repo_name: jfdm/sif-lang

max_forks_repo_name: jfdm/sif-lang


text:
module Js.Object

import Control.Monad.Syntax
import Js

%default total
%access export

public export
interface Class c where
    ptr : (object : c) -> Ptr

public export
interface Member a where
    get : Class c => (member : String) -> (object : c) -> JS_IO a
    set : Class c => (member : String) -> (value : a) -> (object : c) -> JS_IO ()

%inline
jsGet : (ty : Type) -> {auto fty : FTy FFI_JS [] ty} -> ty
jsGet ty = js "%1[%0]" ty

%inline
jsSet : (ty : Type) -> {auto fty : FTy FFI_JS [] ty} -> ty
jsSet ty = js "%2[%0] = %1" ty

public export
data Object = MkObject Ptr

Class Object where
    ptr (MkObject p) = p

%inline
empty : JS_IO Object
empty = MkObject <$> js "{}" (JS_IO Ptr)

%inline
wrap : Member a => (member : String) -> (value : a) -> JS_IO Object
wrap member value = do object <- empty
                       set member value object
                       pure object

Member Bool where
    get member object = pure $ !(js "%1[%0] + 0" (String -> Ptr -> JS_IO Int) member $ ptr object) /= 0
    set member False = js "%1[%0] = false" (String -> Ptr -> JS_IO ()) member . ptr
    set member True = js "%1[%0] = true" (String -> Ptr -> JS_IO ()) member . ptr

Member Nat where
    get member = jsGet (String -> Ptr -> JS_IO Int) member . ptr >=> pure . cast
    set member value = jsSet (String -> Int -> Ptr -> JS_IO ()) member (cast value) . ptr

Member Int where
    get member = jsGet (String -> Ptr -> JS_IO Int) member . ptr
    set member value = jsSet (String -> Int -> Ptr -> JS_IO ()) member value . ptr

Member Double where
    get member = jsGet (String -> Ptr -> JS_IO Double) member . ptr
    set member value = jsSet (String -> Double -> Ptr -> JS_IO ()) member value . ptr

Member String where
    get member = jsGet (String -> Ptr -> JS_IO String) member . ptr
    set member value = jsSet (String -> String -> Ptr -> JS_IO ()) member value . ptr

Member Ptr where
    get member = jsGet (String -> Ptr -> JS_IO Ptr) member . ptr
    set member value = jsSet (String -> Ptr -> Ptr -> JS_IO ()) member value . ptr

Member Object where
    get member = jsGet (String -> Ptr -> JS_IO Ptr) member . ptr >=> pure . MkObject
    set member value = jsSet (String -> Ptr -> Ptr -> JS_IO ()) member (ptr value) . ptr

max_stars_repo_name: jheiling/idris-js

max_issues_repo_name: jheiling/idris-js

max_forks_repo_name: jheiling/idris-js


text:
module GRIN.GrinCG

import Core.Core
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Options
import Core.Options.Log
import Compiler.Common

import Data.String.Builder
import Data.String

import Libraries.Utils.Path

import System
import System.File
import System.Directory

import GRIN.ANFToGRIN
import GRIN.AST
import GRIN.Data
import GRIN.Error
import GRIN.PrettyCompatB
import GRIN.Pipeline
import GRIN.Name
import GRIN.GrinM

getSaveIR : List String -> Bool
getSaveIR [] = False
getSaveIR (d :: ds) = trim d == "save-ir" || getSaveIR ds

getDoOpts : List String -> Bool
getDoOpts [] = True
getDoOpts (d :: ds) = trim d /= "no-opts" && getDoOpts ds

getSkipCG : List String -> Bool
getSkipCG [] = False
getSkipCG (d :: ds) = trim d == "skip-cg" || getSkipCG ds

getDoStats : List String -> Bool
getDoStats [] = False
getDoStats (d :: ds) = trim d == "stats" || getDoStats ds

ShowB GName where
    showB = showB @{FromShow}

data PostPipeline
    = Eval
    | EvalWithStats
    | SaveLLVM

compileExpr :
    PostPipeline ->
    Ref Ctxt Defs ->
    (tmpDir : String) ->
    (outDir : String) ->
    ClosedTerm ->
    (outFile : String) ->
    Core (Maybe String)
compileExpr post d tmpDir outDir term outFile = do
    let appDir = outDir </> outFile ++ "_app"
        mkGrinFile = \f => appDir </> f <.> "grin"
        outGrinFile = mkGrinFile outFile
        outLLFile = outDir </> outFile

    ds <- getDirectives (Other "grin")
    let doOpts = getDoOpts ds
    let saveIR = getSaveIR ds
    let skipCG = getSkipCG ds

    Right _ <- coreLift $ mkdirAll appDir
        | Left err => throw $ FileErr appDir err

    cdata <- getCompileData True ANF term

    prog0 <- logTime "++ Compile ANF to GRIN" $ compileANF cdata.anf

    prog1 <- logTime "++ Resolve names" $ pure $ runResolveM $ traverseProg resolve prog0

    let pipeline : List (Transform (Resolved GName))
        pipeline =
            [ SaveGrin saveIR (mkGrinFile "000_ANF")
            , O NormaliseBind
            , SaveGrin saveIR (mkGrinFile "001_bind_normalise")
            , O CopyPropogation
            , SaveGrin saveIR (mkGrinFile "002_copy_prop")
            , O InlineSimpleDef
            , SaveGrin saveIR (mkGrinFile "003_inline_simple")
            , O $ Fix
                [ UnusedFunctionElim
                , UnusedConstructorElim
                ]
            , SaveGrin saveIR (mkGrinFile "004_unused_function_constructor")
            , O  $ InlineUsedOnce
            , SaveGrin saveIR (mkGrinFile "005_inline_used_once")
            , O $ Fix [ UnusedParamElim ]
            , SaveGrin saveIR (mkGrinFile "006_unused_parameter")
            , O CaseSimplify
            , SaveGrin saveIR (mkGrinFile "007_case_simplify")
            , O UnusedFunctionElim
            , O NormaliseBind
            , SaveCalls saveIR (appDir </> "calls_graph")
            , SaveCalledBy saveIR (appDir </> "called_by_graph")
            , SaveGrin True outGrinFile
            ]

    st <- logTime "++ Run optimisations" $ coreLift $ execGrinT' (runTransforms $
            if doOpts
                then pipeline
                else [ SaveGrin True outGrinFile ])
            (newGrinState prog1)

    let [] = getErrors st
        | errs => throw $ InternalError $ "Error running optimisations\n" ++ show errs

    doLog <- unverifiedLogging "grin" 10

    let grinc = "grinIdris2-exe"
    let grinCMD =
            grinc
            ++ " \"" ++ (outDir </> outFile ++ "_app")
            ++ "\" \""  ++ outGrinFile ++ "\""
            ++ (if doLog then " --logging" else "")
            ++ (if saveIR then " --save-ir" else "")
            ++ (case post of
                    Eval => " --eval"
                    EvalWithStats => " --eval-stats"
                    SaveLLVM => " --save-llvm \"" ++ (outDir </> outFile) ++ "\"")

    unverifiedLogC "grin" 10 $ pure grinCMD
    unless skipCG $ (coreLift $ system grinCMD) >>= \case
        0 => pure ()
        errno => throw $ InternalError $ "grinIdris2-exe returned error " ++ show errno

    pure $ Just outGrinFile

executeExpr :
    Ref Ctxt Defs ->
    (tmpDir : String) ->
    ClosedTerm -> Core ()
executeExpr d tmpDir term = do
    ds <- getDirectives (Other "grin")
    if getDoStats ds
        then ignore $ compileExpr EvalWithStats d tmpDir tmpDir term "execute"
        else ignore $ compileExpr Eval d tmpDir tmpDir term "execute"

export
grin : Codegen
grin = MkCG (compileExpr SaveLLVM) executeExpr Nothing Nothing


text:
module Main

import Depling
import Depling.TypeCheck
import Depling.PrettyPrint
import Depling.Incr
import Depling.Elevate
import Data.Vect
import Data.Fin
import Utils

lℕℂ : DCon 0
lℕℂ = DConV "ℕ" [] 𝕋

lℕ : DAST n
lℕ = ℂ lℕℂ []

lzℂ : DCon 0
lzℂ = DConV "z" [] lℕ

lz : DAST n
lz = ℂ lzℂ []

lsℂ : DCon 1
lsℂ = DConV "s" [lℕ] lℕ

ls : DAST n
ls = λ lℕ $ ℂ lsℂ [ʌ 0]

lp : DAST n
lp =
	𝔽 lℕ (λT lℕ lℕ) $
		ℙ (ʌ 0) lzℂ (λ lℕ $ ʌ 0) $
		ℙ (ʌ 0) lsℂ (λ lℕ $ ʌ 3 =!= ʌ 1 =!= (ls =!= ʌ 0)) $
		𝔹 (λT lℕ lℕ)

lco : DAST n
lco = λ 𝕋 $ λ (λT (ʌ 0) 𝕋) $ λ (λT (ʌ 1) (ʌ 1 =!= ʌ 0)) $ λ 𝕋 $ λ (λT (ʌ 0) (ʌ 4)) $ λ (ʌ 1) $ ʌ 3 =!= (ʌ 1 =!= ʌ 0)

llℂ : DCon 1
llℂ = DConV "l" [𝕋] 𝕋

ll : DAST n
ll = λ 𝕋 $ ℂ llℂ [ʌ 0]

lnℂ : DCon 1
lnℂ = DConV "n" [𝕋] $ ll =!= ʌ 0

ln : DAST n
ln = λ 𝕋 $ ℂ lnℂ [ʌ 0]

lcℂ : DCon 3
lcℂ = DConV "c" [𝕋, ʌ 0, ll =!= ʌ 1] $ ll =!= ʌ 2

lc : DAST n
lc = λ 𝕋 $ λ (ʌ 0) $ λ (ll =!= ʌ 1) $ ℂ lcℂ [ʌ 2, ʌ 1, ʌ 0]

lrepeat : DAST n
lrepeat = λ 𝕋 $ 𝔽 (ʌ 0) (ll =!= ʌ 1) $ lc =!= ʌ 2 =!= ʌ 0 =!= (ʌ 1 =!= ʌ 0)

lcycle : DAST n
lcycle =
	-- a : Type
	λ 𝕋 $
		-- orig : List a
		λ (ll =!= ʌ 0) $
			-- R : List a -> List a
			-- l : List a
			(𝔽 (ll =!= ʌ 1) (ll =!= ʌ 2) $
				-- a' : Type -- a' = a
				ℙ (ʌ 0) lnℂ (ʌ 2 =!= ʌ 3) $
				-- a' : Type -- a' = a
				-- h : a
				-- t : List a
				ℙ (ʌ 0) lcℂ (lc =!= ʌ 6 =!= ʌ 1 =!= (ʌ 4 =!= ʌ 0)) $
				𝔹 $ ll =!= ʌ 3
			) =!= ʌ 0

lhead : DAST n
lhead = λ 𝕋 $ λ (ll =!= ʌ 0) $ ℙ (ʌ 0) lcℂ (ʌ 1) $ 𝕌 "head of empty list" (ʌ 1)

ltail : DAST n
ltail = λ 𝕋 $ λ (ll =!= ʌ 0) $ ℙ (ʌ 0) lcℂ (ʌ 0) $ ʌ 0

leqℂ : DCon 4
leqℂ = DConV "=" [𝕋, ʌ 0, 𝕋, ʌ 0] 𝕋

leq : DAST n
leq = λ 𝕋 $ λ (ʌ 0) $ λ 𝕋 $ λ (ʌ 0) $ ℂ leqℂ [ʌ 3, ʌ 2, ʌ 1, ʌ 0]

lreflℂ : DCon 2
lreflℂ = DConV "Refl" [𝕋, ʌ 0] $ ℂ leqℂ [ʌ 1, ʌ 0, ʌ 1, ʌ 0]

lrefl : DAST n
lrefl = λ 𝕋 $ λ (ʌ 0) $ ℂ lreflℂ [ʌ 1, ʌ 0]

lThe : DAST n
lThe = λ 𝕋 $ λ (ʌ 0) $ ʌ 0

lPlusSuccRightSucc : DAST n
lPlusSuccRightSucc {n} =
	-- recurse : Nat -> Nat -> Nat
	-- left : Nat
	𝔽 lℕ (λT lℕ lℕ) $
		-- right : Nat
		λ lℕ $
			ℙ (ʌ 1) lzℂ (ℂ lreflℂ [lℕ, ℂ lsℂ [ʌ 0]]) $
			-- left : Nat
			-- ℙ (ʌ 1) lsℂ (
				-- lThe =!= t =!= ℂ lreflℂ [lℕ, ℂ lsℂ [ʌ 0]]
				𝕌 "wat" t
				-- ℙ (ʌ 3 =!= ʌ 0 =!= ʌ 1) lreflℂ (
					-- ℂ lreflℂ [lℕ, ℂ lsℂ [ʌ 0]]
				-- ) $
				-- 𝕌 "wat" $ elevate {gte=ltePlus'' {n=S$ S$ S$ n} {a=1}} t
			-- ) $
			-- 𝕌 "wat" t
	where
	t : DAST (S$ S$ S$ n)
	--  ℂ  =   [Nat, plus   left    ℂ succ [right], Nat, ℂ succ [plus   left    right]]
	t = ℂ leqℂ [lℕ , lp =!= ʌ 1 =!= ℂ lsℂ  [ʌ 0  ], lℕ , ℂ lsℂ  [lp =!= ʌ 1 =!= ʌ 0  ]]

ltest' : DAST n
ltest' = λ (ℂ leqℂ [lℕ, lz, lℕ, lz]) $ ʌ 0

ltest : DAST n
ltest = ltest' =!= ℂ lreflℂ [𝕋, 𝕋]

ppTypeError : DTypeError -> String
ppTypeError (DTypeErrorV e ts) =
	(pp_n DPOpen [] $ replace (sym $ plusZeroRightNeutral _) e) ++ ":\n"
	++ (unlines $ map (("  " ++) . pp_n DPOpen [] . replace (sym $ plusZeroRightNeutral _)) ts)

main : IO ()
main = putStrLn $ pp DPOpen [] $ lPlusSuccRightSucc

max_stars_repo_name: CoderPuppy/idris-depling

max_issues_repo_name: CoderPuppy/idris-depling

max_forks_repo_name: CoderPuppy/idris-depling


text:
module Main

import Data.Vect

%default total

insert :  Ord elem
       => (x : elem)
       -> (xsSorted : Vect len elem)
       -> Vect (S len) elem
insert x [] = [x]
insert x (y :: xs) =
  if x < y
    then x :: y :: xs
    else y :: insert x xs

insSort :  Ord elem
        => Vect n elem
        -> Vect n elem
insSort [] = []
insSort (x :: xs) =
  let xsSorted = insSort xs in insert x xsSorted

{-
insSort [1,3,2,9,7,6,4,5,8]
-}

max_stars_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_issues_repo_name: haroldcarr/learn-haskell-coq-ml-etc

max_forks_repo_name: haroldcarr/learn-haskell-coq-ml-etc


text:
> module Interfaces.Math

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

> interface (Num ty) => Math ty where
>   exp : ty -> ty
>   sin : ty -> ty
>   cos : ty -> ty

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Control.Monad.Codensity

import Control.Monad.Trans
import Control.Monad.Reader
import Control.Monad.State

import Control.Linear.LIO

public export
data Codensity : (m : Type -> Type) -> (a : Type) -> Type where
  MkCodensity : (1 _ : (forall b. (a -> m b) -> m b)) -> Codensity m a

runCodensity : Codensity m a -> (forall b. (a -> m b) -> m b)
runCodensity (MkCodensity x) = x

public export
implementation Functor (Codensity m) where
  map f g = MkCodensity $ \bmr => runCodensity g (\a => bmr (f a))

public export
implementation Applicative (Codensity m) where
  pure x = MkCodensity \amr => amr x
  f <*> x = MkCodensity \bmr =>
   runCodensity f (\ab => runCodensity x (\a => bmr (ab a)))

public export
implementation Alternative m => Alternative (Codensity m) where
  x <|> y = MkCodensity \k => runCodensity x k <|> runCodensity y k
  empty = MkCodensity \_ => empty

public export
implementation Monad (Codensity m) where
  x >>= k = MkCodensity \bmr => runCodensity x (\a => runCodensity (k a) bmr)

public export
implementation HasIO m => HasIO (Codensity m) where
  liftIO x = MkCodensity (liftIO x >>=)

public export
implementation MonadTrans Codensity where
  lift x = MkCodensity (Prelude.(>>=) x)

MonadReader r m => MonadReader r (Codensity m) where
  ask = MkCodensity (ask >>=)
  local f (MkCodensity co) = MkCodensity \amb => do
    r <- ask
    local f . co $ local (const r) . amb

MonadReader s m => MonadState s (Codensity m) where
  get = MkCodensity (ask >>=)
  put s = MkCodensity \amb => local (const s) (amb ())


text:
module Color

public export
data Color : Type where
  Black : Color
  Red : Color
  Green : Color
  Yellow : Color
  Blue : Color
  Magenta : Color
  Cyan : Color
  White : Color

public export
data Decorator : Type where
  Reset : Decorator
  Text : Color -> Decorator
  BG : Color -> Decorator
  Bold : Decorator
  Underline : Decorator
  Reversed : Decorator
  Both : Decorator -> Decorator -> Decorator

export %inline
(<&>) : Decorator -> Decorator -> Decorator
(<&>) = Both
infixr 5 <&>

ctrl : String -> String
ctrl =
  strCons (chr 27)

export
init : Decorator -> String
init Reset = ctrl "[0m"
init Bold = ctrl "[1m"
init Underline = ctrl "[4m"
init Reversed = ctrl "[7m"
init (Text Black) = ctrl "[30m"
init (Text Red) = ctrl "[31m"
init (Text Green) = ctrl "[32m"
init (Text Yellow) = ctrl "[33m"
init (Text Blue) = ctrl "[34m"
init (Text Magenta) = ctrl "[35m"
init (Text Cyan) = ctrl "[36m"
init (Text White) = ctrl "[37m"
init (BG Black) = ctrl "[40m"
init (BG Red) = ctrl "[41m"
init (BG Green) = ctrl "[42m"
init (BG Yellow) = ctrl "[43m"
init (BG Blue) = ctrl "[44m"
init (BG Magenta) = ctrl "[45m"
init (BG Cyan) = ctrl "[46m"
init (BG White) = ctrl "[47m"
init (Both a b) = init a ++ init b

export
fin : Decorator -> String
fin Reset = ""
fin (Both a b) = fin a ++ fin b
fin _ = init Reset

export
decorate : Decorator -> String -> String
decorate d str = (init d) ++ str ++ (fin d)

max_stars_repo_name: Z-snails/inigo

max_issues_repo_name: Z-snails/inigo

max_forks_repo_name: Z-snails/inigo


text:
module Compiler.ES.TailRec

import Compiler.ES.ImperativeAst

hasTailCall : Name -> ImperativeStatement -> Bool
hasTailCall n (SeqStatement x y) =
    hasTailCall n y
hasTailCall n (ReturnStatement x) =
    case x of
        IEApp (IEVar cn) _ => n == cn
        _ => False
hasTailCall n (SwitchStatement e alts d) =
    (any (\(_, w)=>hasTailCall n w) alts) || (maybe False (hasTailCall n) d)
hasTailCall n (ForEverLoop x) =
    hasTailCall n x
hasTailCall n o = False

argsName : Name
argsName = MN "tailRecOptimArgs" 0

stepFnName : Name
stepFnName = MN "tailRecOptimStep" 0

createNewArgs : List ImperativeExp -> ImperativeExp
createNewArgs values =
    IEConstructor (Left 0) values

createArgInit : List Name -> ImperativeStatement
createArgInit names =
    LetDecl argsName (Just $ IEConstructor (Left 0) (map IEVar names))

replaceTailCall : Name -> ImperativeStatement -> ImperativeStatement
replaceTailCall n (SeqStatement x y) = SeqStatement x (replaceTailCall n y)
replaceTailCall n (ReturnStatement x) =
    let defRet = ReturnStatement $ IEConstructor (Left 1) [x]
    in case x of
        IEApp (IEVar cn) arg_vals =>
            if n == cn then ReturnStatement $ createNewArgs arg_vals
                else defRet
        _ => defRet

replaceTailCall n (SwitchStatement e alts d) =
    SwitchStatement e (map (\(x,y) => (x, replaceTailCall n y)) alts) (map (replaceTailCall n) d)
replaceTailCall n (ForEverLoop x) =
    ForEverLoop $ replaceTailCall n x
replaceTailCall n o = o

makeTailOptimToBody : Name -> List Name -> ImperativeStatement -> ImperativeStatement
makeTailOptimToBody n argNames body =
    let lastArg = (length argNames) + 1
        newArgExp = map (\x => IEConstructorArg (cast x) (IEVar argsName)) [1..lastArg]
        bodyArgsReplaced = replaceNamesExpS (zip argNames newArgExp) body
        stepBody = replaceTailCall n bodyArgsReplaced
        stepFn = FunDecl EmptyFC stepFnName [argsName] stepBody
        loopRec = MutateStatement argsName (IEApp (IEVar stepFnName) [IEVar argsName])
        loopReturn = ReturnStatement (IEConstructorArg 1 $ IEVar argsName)
        loop = ForEverLoop $ SwitchStatement (IEConstructorHead $ IEVar argsName) [(IEConstructorTag $ Left 0, loopRec)] (Just loopReturn)
    in stepFn <+> createArgInit argNames <+> loop

export
tailRecOptim :  ImperativeStatement -> ImperativeStatement
tailRecOptim (SeqStatement x y) = SeqStatement (tailRecOptim x) (tailRecOptim y)
tailRecOptim (FunDecl fc n args body) =
    let new_body = if hasTailCall n body then makeTailOptimToBody n args body
                        else body
    in FunDecl fc n args new_body
tailRecOptim x = x


text:
||| Using single machine-word as Bitarray.
|||
||| Copyright 2021, HATTORI, Hiroki
||| This file is released under the MIT license, see LICENSE for more detail.
|||
module Data.Container.IntSet

import Data.Container.Interfaces

import Data.Bits
import Data.Maybe               -- fromMaybe
import Data.So
import Data.SortedMap as M      -- mergeWith, empty
import Decidable.Equality

%default total

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

-- 0 decideTiny : (n:Nat) -> Dec ((n <= 32) = True)
decideTiny : (n:Nat) -> Dec ((n <= 32) = True)
decideTiny n = decEq (n <= 32) True

export IntSet : (N:Nat) -> Type
IntSet n with (decideTiny n)
  IntSet _ | Yes _ = Bits32
  IntSet _ | No _  = M.SortedMap Integer Bits32

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

export
(n:Nat) => Semigroup (IntSet n) where
  x <+> y with (decideTiny n)
    x <+> y | Yes _ = prim__or_Bits32 x y
    x <+> y | No _  = M.mergeWith prim__or_Bits32 x y

export
(n:Nat) => Semigroup (IntSet n) => Monoid (IntSet n) where
  neutral with (decideTiny n)
    neutral | Yes _ = 0
    neutral | No _  = M.empty

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

keyix : Integer -> (Integer, Bits32)
keyix k =
  let i = if k >= 0 then (k `div` 32) else (negate $ (k - 1) `div` 32)
      b = fromInteger $ abs $ k `mod` 32
   in (i, b)

export
{n:Nat} -> Container (IntSet n) where
  KeyTy = Integer
  null xs with (decideTiny n)
    null xs | Yes _ = xs == 0
    null xs | No _  = null xs
  count xs with (decideTiny n)
    count xs | Yes _ = popCount xs
    count xs | No _  = foldl (\acc, b => acc + popCount b) 0 xs
  contains k xs with (decideTiny n)
    contains k xs | Yes _ =
      if k >= 0 && k < 32
        then 0 /= (prim__and_Bits32 xs $ prim__shl_Bits32 1 $ fromInteger k)
        else False
    contains k xs | No  _ =
      let (i, b) = keyix k
       in maybe False (\ys => 0 /= (prim__and_Bits32 ys $ prim__shl_Bits32 1 b))
                (M.lookup i xs)
  delete k xs with (decideTiny n)
    delete k xs | Yes _ =
      if k >= 0 && k < 32
         then prim__and_Bits32 xs $ prim__xor_Bits32 0xffffffff $ prim__shl_Bits32 1 $ fromInteger k
         else xs
    delete k xs | No _  =
      let (i, b) = keyix k
       in maybe xs (\ys => M.insert i (prim__and_Bits32 ys $ prim__xor_Bits32 0xffffffff $ prim__shl_Bits32 1 b) xs)
                (M.lookup i xs)

export
(n:Nat) => (Container (IntSet n)) => Set (IntSet n) where
  KeyTy = Integer
  insert k xs with (decideTiny n)
    insert k xs | Yes _ =
      if k >= 0 && k < 32
         then prim__or_Bits32 xs $ prim__shl_Bits32 1 $ fromInteger k
         else xs
    insert k xs | No  _ =
      let (i, b) = keyix k
       in M.insert i
                   (prim__or_Bits32 (fromMaybe 0 (M.lookup i xs)) $ prim__shl_Bits32 1 b)
                   xs

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


text:
-- ----------------------------------------------------------------- [ Org.idr ]
-- Module    : Org.idr
-- Copyright : (c) Jan de Muijnck-Hughes
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
module Text.Markup.Edda.Writer.CommonMark

import Data.AVL.Dict

import Effects
import Effect.File
import Effect.Exception

import Text.Markup.Edda.Model
import Text.Markup.Edda.Process.Utils

import Text.Markup.Edda.Writer.Common

-- -------------------------------------------------------------- [ Directives ]
%default total
%access private

-- @TODO Attributes...

-- ------------------------------------------------------------ [ Misc Writing ]
ntimes : Char -> Nat -> String
ntimes c n = concat $ ntimes' (S n)
  where
    ntimes' : Nat -> List String
    ntimes' Z     = Nil
    ntimes' (S k) = (cast c) :: ntimes' k

-- ----------------------------------------------------------- [ Write Inlines ]

mutual
  export
  inlines : List (Edda INLINE) -> String
  inlines xs = assert_total $ concatMap inline xs

  parens : String -> String -> Either String (List (Edda INLINE)) -> String
  parens l r (Left str) = concat [l, str,        r]
  parens l r (Right ts) = concat [l, inlines ts, r]

  markup : String -> Either String (List (Edda INLINE)) -> String
  markup t txt = parens t t txt

  link : String -> List (Edda INLINE) -> String
  link uri Nil  = concat ["<", uri, ">"]
  link uri desc = concat ["[", uri, "](", inlines desc, ")"]

  inline : Edda INLINE -> String
  inline (Text t)     = t
  inline (Sans t)     = t
  inline (Scap t)     = t
  inline (Mono t)     = t
  inline (Verb v)     = markup "`"  (Left v)
  inline (Code v)     = markup "`"  (Left v)
  inline (Math v)     = markup "`"  (Left v)
  inline (Emph t)     = markup "*"  (Right t)
  inline (Bold t)     = markup "**" (Right t)
  inline (Strike t)   = markup "~~" (Right t)
  inline (Uline t)    = markup "*"  (Right t)
  inline (Quote ty t) =
    case ty of
      SQuote => markup "'"  (Right t)
      DQuote => markup "\"" (Right t)
  inline (Parens ty t) =
    case ty of
      Parents  => parens "(" ")" (Right t)
      Brackets => parens "[" "]" (Right t)
      Braces   => parens "{" "}" (Right t)
  inline (Ref url)        = link url Nil
  inline (Hyper uri desc) = link uri desc
  inline (FNote l d) =
    case d of
      Nil => parens "`" "`" (Left (concat ["fn", ":", l, ":"]))
      x   => parens "`" "`" (Right ([Text ("fn:" ++ l ++ ":")] ++ x))
  inline (Cite ty uri) =
    case ty of
      ParenSty => ("`citep:" ++ uri ++ "`")
      TextSty  => ("`citet:" ++ uri ++ "`")
  inline (MiscPunc c) = (cast c)
  inline Space      = " "
  inline Newline    = "\n"
  inline Tab        = "\t"
  inline LBrace     = "{"
  inline RBrace     = "}"
  inline LParen     = "("
  inline RParen     = ")"
  inline LBrack     = "["
  inline RBrack     = "]"
  inline LAngle     = "<"
  inline RAngle     = ">"
  inline Dollar     = "$"
  inline Colon      = ":"
  inline Semi       = ";"
  inline EnDash     = "--"
  inline EmDash     = "---"
  inline FSlash     = "/"
  inline BSlash     = "\\"
  inline Apostrophe = "'"
  inline SMark      = "\""
  inline Comma      = ","
  inline Plus       = "+"
  inline Ellipsis   = "..."
  inline Hyphen     = "-"
  inline Bang       = "!"
  inline Period     = "."
  inline QMark      = "?"
  inline Hash       = "#"
  inline Equals     = "="
  inline Pipe       = "|"

-- ----------------------------------------------------- [ Write Generic Block ]

genblock : (a -> String)
        -> a
        -> String
genblock f b = unlines [ f b, "\n"]

textblock : List (Edda INLINE)
         -> String
textblock = genblock (inlines)

verbblock : String
         -> String
verbblock = genblock (\x => ">" ++ x)

-- ------------------------------------------------------------- [ Write Block ]

itemDef : (List (Edda INLINE), List (Edda INLINE)) -> String
itemDef (k,vs) =
    unwords ["+", markup "*" (Left $ inlines k), "::", inlines vs]

item : String -> List (Edda INLINE) -> String
item m b = unwords [m, inlines b]

export
block : Edda BLOCK -> String
block (HRule) = "-----"
block (Empty) = "\n"
block (Section lvl label title as body) =
   assert_total (unlines $ unwords [ntimes '#' lvl, inlines title, fromMaybe "" label] :: (map block body))
block (Figure l c as fig) = unlines [inline fig, "\n"]

block (DList kvs) = (unlines $ map itemDef kvs)
block (OList bs)        = (unlines $ map (item "1.") bs)
block (BList bs)        = (unlines $ map (item "*")  bs)
block (Para txt)        = inlines txt

block (Listing l c lang langopts as src) =
    unlines [ "\n```" ++ fromMaybe "" lang , src, "```"]

block (Comment ss)          = verbblock ss
block (Equation l eq)       = verbblock eq
block (Literal l c src)     = verbblock src

block (Quotation l txt)     = textblock txt

block (Theorem l c txt)     = textblock txt
block (Corollary l c txt)   = textblock txt
block (Lemma l c txt)       = textblock txt
block (Proposition l c txt) = textblock txt
block (Proof l c txt)       = textblock txt
block (Definition l c txt)  = textblock txt
block (Exercise l c txt)    = textblock txt
block (Note l c txt)        = textblock txt
block (Remark l c txt)      = textblock txt
block (Problem l c txt)     = textblock txt
block (Question l c txt)    = textblock txt
block (Solution l c txt)    = textblock txt
block (Example l c txt)     = textblock txt

blocks : List (Edda BLOCK) -> String
blocks = concatMap block

-- -------------------------------------------------------- [ Write List (String, String) ]

properties : List (Edda INLINE) -> Dict String String -> String
properties t ps =
  unlines [ "%YAML 1.2\n---"
          , concat ["title:",  inlines t]
          , concat ["author:", fromMaybe "author missing" (lookup "AUTHOR" ps)]
          , concat ["date:",   fromMaybe "date missing"   (lookup "DATE" ps)]
          , "...\n"
          ]

-- -------------------------------------------------------- [ Write CommonMark ]

namespace Doc
  ||| Convert edda document to markdown.
  export
  toCommonMark : Edda DOC -> String
  toCommonMark (Doc title attrs body) =
     let attrsStr = properties title attrs in
       unlines $ attrsStr :: map block body

namespace File
  ||| Write document to a markdown file.
  export
  toCommonMarkE : String
                 -> Edda DOC
                 -> Eff (FileOpSuccess) [FILE ()]
  toCommonMarkE fn doc = writeEddaFileE toCommonMark fn doc

  ||| Write document to a markdown file.
  export
  toCommonMark : String
                 -> Edda DOC
                 -> IO (Either FileError ())
  toCommonMark fn doc = writeEddaFile toCommonMark fn doc

namespace Snippet
  ||| Convert edda document to markdown.
  export
  toCommonMark : Edda SNIPPET -> String
  toCommonMark (Snippet snippet prf) with (prf)
    toCommonMark (Snippet snippet prf) | IsInLine = inlines snippet
    toCommonMark (Snippet snippet prf) | IsBlock = blocks snippet

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

max_stars_repo_name: jfdm/edda

max_issues_repo_name: jfdm/edda

max_forks_repo_name: jfdm/edda


text:
module CodeGen.InjectLinearImplicits

import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import Primitives.Externals
import Primitives.Primitives
import Data.SortedMap
import Data.SortedSet
import Core.Context
import CairoCode.Traversal.Base
import CairoCode.Traversal.Composition
import Utils.Lens
import Utils.Helpers

%hide Prelude.toList

extractImpls : (Name, CairoDef) -> (Name, SortedSet LinearImplicit)
extractImpls (n, FunDef _ impls _ _) = (n, fromList $ keys impls)
extractImpls (n, ForeignDef (MkForeignInfo _ _ impls _ _) _ _) = (n, fromList impls)

preloadLinearImplicitsDefs : List (Name, CairoDef) -> SortedMap Name (SortedSet LinearImplicit)
preloadLinearImplicitsDefs defs = fromList $ map extractImpls defs

collectApplyLinearImplicits : SortedMap Name (SortedSet LinearImplicit) -> List (Name, CairoDef) -> SortedSet LinearImplicit
collectApplyLinearImplicits implicitLookup defs = snd $ runVisitConcatCairoDefs (pureTraversal closureCollectTraversal) defs
    where closureCollectTraversal : InstVisit CairoReg -> SortedSet LinearImplicit
          closureCollectTraversal (VisitMkClosure _ name _ _ ) = fromMaybe empty (lookup name implicitLookup)
          closureCollectTraversal _ = empty

discoverNeededLinearImplicitsDef : SortedMap Name (SortedSet LinearImplicit) -> SortedSet LinearImplicit -> (Name, CairoDef) -> SortedSet LinearImplicit
discoverNeededLinearImplicitsDef implicitLookup applyLinearImplicits def = snd $ runVisitConcatCairoDef (pureTraversal neededLinearImplicits) def
      where exludeExisting : SortedSet LinearImplicit -> LinearImplicitArgs -> SortedSet LinearImplicit
            exludeExisting needed existing = difference needed (fromList $ keys existing)
            lookupLinearImplicits : Name -> SortedSet LinearImplicit
            lookupLinearImplicits name = fromMaybe empty (lookup name implicitLookup)
            definedImpls : List LinearImplicit
            definedImpls = toList $ snd $ extractImpls def
            neededLinearImplicits : InstVisit CairoReg -> SortedSet LinearImplicit
            neededLinearImplicits (VisitApply _ linImpls _ _) = exludeExisting applyLinearImplicits linImpls
            neededLinearImplicits (VisitCall _ linImpls name _) = exludeExisting (lookupLinearImplicits name) linImpls
            neededLinearImplicits (VisitExtprim _ linImpls name _) = exludeExisting (fromList $ externalLinearImplicits name) linImpls
            neededLinearImplicits (VisitOp  _ linImpls fn _) = exludeExisting (primFnLinearImplicits fn) linImpls
            -- This is just an integrity check
            neededLinearImplicits (VisitReturn _ linImpls) = if definedImpls /= (keys linImpls)
                 then assert_total $ idris_crash ("predefined implicits are not returned")
                 else empty
            neededLinearImplicits _ = empty

discoverNeededLinearImplicitsDefs : SortedMap Name (SortedSet LinearImplicit) -> SortedSet LinearImplicit -> List (Name, CairoDef) -> SortedMap Name (SortedSet LinearImplicit)
discoverNeededLinearImplicitsDefs implicitLookup applyLinearImplicits defs = foldl processCheckAndUpdateDef implicitLookup defs
    where processCheckAndUpdateDef : SortedMap Name (SortedSet LinearImplicit) -> (Name, CairoDef) -> SortedMap Name (SortedSet LinearImplicit)
          processCheckAndUpdateDef currentLookup def@(name,_) = updateDef $ discoverNeededLinearImplicitsDef currentLookup applyLinearImplicits def
                where definedImpls : SortedSet LinearImplicit
                      definedImpls = snd $ extractImpls def
                      checkedImpls : SortedSet LinearImplicit -> SortedSet LinearImplicit
                      checkedImpls discoveredLinearImplicits = if all (\i => not (contains i definedImpls)) discoveredLinearImplicits
                        then discoveredLinearImplicits
                        else assert_total $ idris_crash ("predefined implicits do not cover all instructions")
                      updateDef : SortedSet LinearImplicit -> SortedMap Name (SortedSet LinearImplicit)
                      updateDef discoveredLinearImplicits = insert name (union (checkedImpls discoveredLinearImplicits) (fromMaybe empty (lookup name currentLookup))) currentLookup

singleDiscoveryRun : SortedMap Name (SortedSet LinearImplicit) -> List (Name, CairoDef) -> (SortedSet LinearImplicit, SortedMap Name (SortedSet LinearImplicit))
singleDiscoveryRun implicitLookup defs = (appliedLinearImplicits, discoverNeededLinearImplicitsDefs implicitLookup appliedLinearImplicits defs)
    where appliedLinearImplicits : SortedSet LinearImplicit
          appliedLinearImplicits = collectApplyLinearImplicits implicitLookup defs

repeatedDiscoveryRun : SortedMap Name (SortedSet LinearImplicit) -> List (Name, CairoDef) -> (SortedSet LinearImplicit, SortedMap Name (SortedSet LinearImplicit))
repeatedDiscoveryRun implicitLookup defs = if (snd runResult) == implicitLookup
    then runResult
    else repeatedDiscoveryRun (snd runResult) defs
    where runResult : (SortedSet LinearImplicit, SortedMap Name (SortedSet LinearImplicit))
          runResult = singleDiscoveryRun implicitLookup defs

-- This does the discovery of all implicits needed per Name
executeLinearImplicitDiscovery : List (Name, CairoDef) -> (SortedSet LinearImplicit, SortedMap Name (SortedSet LinearImplicit))
executeLinearImplicitDiscovery defs = repeatedDiscoveryRun (preloadLinearImplicitsDefs defs) defs

-- Note: SortedMap CairoReg CairoReg only needed as Optimisation can not do forward substitution at branch border:
--          Meaning: "x = ...; y = x" is not translated to "y = ..." when y escapes the branch
--          If we ever do we can simplify this by just doing an ASSIGN at end of branch
--        Currently we record y = x in the map and use substituteRegs to make the translation
--       The List (CairoReg, RegGen) are the active register in each active branch
--        as well as the generator to generate the next register in that branch
record RegTrackerState where
    constructor MkRegTrackerState
    stack : List (CairoReg, RegisterGen)
    subst : SortedMap CairoReg CairoReg

-- Lenses for leaner and more readable main definitions
stackLens : Lens RegTrackerState (List (CairoReg, RegisterGen))
stackLens = MkLens stack (\ts,fn => {stack $= fn} ts)

substLens : Lens RegTrackerState (SortedMap CairoReg CairoReg)
substLens = MkLens subst (\ts,fn => {subst $= fn} ts)

headLens : Lens RegTrackerState (CairoReg, RegisterGen)
headLens = join stackLens headFailLens

activeRegLens : Lens RegTrackerState CairoReg
activeRegLens = join headLens leftLens

activeRegGenLens : Lens RegTrackerState RegisterGen
activeRegGenLens = join headLens rightLens

-- Accessors
getCurrentReg : Traversal RegTrackerState CairoReg
getCurrentReg = readStateL activeRegLens

getDepth : Traversal RegTrackerState Int
getDepth = map (\s => (cast $ length s) - 1) (readStateL stackLens)

advanceRegBinding : Traversal RegTrackerState (CairoReg, CairoReg)
advanceRegBinding = do
    beforeReg <- getCurrentReg
    depth <- getDepth
    _ <- updateStateL headLens (\(_,regGen) => nextRegister regGen depth)
    afterReg <- getCurrentReg
    pure (beforeReg, afterReg)

enterBranch : Show a => Maybe a -> Traversal RegTrackerState (CairoReg, CairoReg)
enterBranch tc = do
    beforeReg <- getCurrentReg
    depth <- getDepth
    regGen <- readStateL activeRegGenLens
    let nextRegAndGen = nextRegister (branchRegisterGen tc regGen) depth
    _ <- updateStateL stackLens (nextRegAndGen::)
    afterReg <- getCurrentReg
    pure (beforeReg, afterReg)

leaveBranch : Traversal RegTrackerState ()
leaveBranch = updateState update
    -- goes 2 elements deep on stack, so lenses do not improve the situation here
    where update : RegTrackerState -> RegTrackerState
          update (MkRegTrackerState ((branchReg, _)::(reg,regGen)::xs) subst) =
            MkRegTrackerState ((reg,regGen)::xs) (insert branchReg (fst $ nextRegister regGen (cast $ length xs)) subst)
          update _ = assert_total $ idris_crash "Illegal Active State"

implicitRegTransformer : SortedSet Name -> Bool -> LinearImplicit -> (InstVisit CairoReg -> Traversal RegTrackerState (List (InstVisit CairoReg)))
implicitRegTransformer neededByCall neededByApply impl = implicitRegInjector
    where implicitRegInjector : InstVisit CairoReg -> Traversal RegTrackerState (List (InstVisit CairoReg))
          implicitRegInjector (VisitFunction name params linImpls rets) = map (\r => [VisitFunction name params (insert impl r linImpls) rets]) getCurrentReg
          implicitRegInjector inst@(VisitApply res linImpls clo arg) = if neededByApply
              then map (\bind => [VisitApply res (insert impl bind linImpls) clo arg]) advanceRegBinding
              else pure [inst]
          implicitRegInjector inst@(VisitCall res linImpls name args) = if contains name neededByCall
              then map (\bind => [VisitCall res (insert impl bind linImpls) name args]) advanceRegBinding
              else pure [inst]
          implicitRegInjector inst@(VisitOp res linImpls fn args) = if contains impl (primFnLinearImplicits fn)
              then map (\bind => [VisitOp res (insert impl bind linImpls) fn args]) advanceRegBinding
              else pure [inst]
          implicitRegInjector inst@(VisitExtprim res linImpls name args) = if contains impl (fromList $ externalLinearImplicits name)
              then map (\bind => [VisitExtprim res (insert impl bind linImpls) name args]) advanceRegBinding
              else pure [inst]
          implicitRegInjector (VisitReturn res linImpls) = map (\(reg,_) => [VisitReturn res (insert impl reg linImpls)]) advanceRegBinding
          implicitRegInjector (VisitConBranch tag) = map (\(curReg, brReg) => [VisitConBranch tag, VisitAssign brReg curReg]) (enterBranch tag)
          implicitRegInjector (VisitConstBranch const) = map (\(curReg, brReg) => [VisitConstBranch const, VisitAssign brReg curReg]) (enterBranch const)
          implicitRegInjector (VisitBranchEnd) = map (\_ => [VisitBranchEnd]) leaveBranch
          implicitRegInjector (VisitCaseEnd) = map (\_ => [VisitCaseEnd]) advanceRegBinding
          implicitRegInjector inst = pure [inst]

areAppliesAffected : LinearImplicit -> SortedSet LinearImplicit -> Bool
areAppliesAffected = contains

transformLinearImplicitDef : LinearImplicit -> SortedMap Name (SortedSet LinearImplicit) -> SortedSet LinearImplicit -> (Name, CairoDef) -> (Name, CairoDef)
transformLinearImplicitDef impl functionImpls applyImpls def@(name, FunDef _ linImpls _ _) = if isJust (lookup impl linImpls)
    then def -- is already present no need to inject
    else substituteDefRegisters substituteReg (snd result)
    where affectedCalls : SortedSet Name
          affectedCalls = fromList ((toList functionImpls) >>= (\(n,linImpls) => if contains impl linImpls then [n] else []))
          areAppliesAffected : Bool
          areAppliesAffected = contains impl applyImpls
          transformer : InstVisit CairoReg -> Traversal RegTrackerState (List (InstVisit CairoReg))
          transformer = implicitRegTransformer affectedCalls areAppliesAffected impl
          initialState : RegTrackerState
          initialState = MkRegTrackerState ((NamedParam (implicitName impl), ("implicit_" ++ (implicitName impl), 0))::Nil) empty
          result : (RegTrackerState, (Name, CairoDef))
          result = runVisitTransformCairoDef (rawTraversal transformer initialState) def
          substituteReg : CairoReg -> Maybe CairoReg
          -- call recursively to ensure we end up with the final substitution
          substituteReg reg = maybeMap (\r => fromMaybe r (substituteReg r)) (lookup reg (subst (fst result)))
transformLinearImplicitDef _ _ _ def = def

transformDef : SortedMap Name (SortedSet LinearImplicit) -> SortedSet LinearImplicit -> (Name, CairoDef) -> (Name, CairoDef)
transformDef functionImpls applyImpls def@(name,_) = foldl (\d,impl => transformLinearImplicitDef impl functionImpls applyImpls d) def requiredImpls
    where requiredImpls : SortedSet LinearImplicit
          requiredImpls = fromMaybe empty (lookup name functionImpls)

transformDefs : SortedMap Name (SortedSet LinearImplicit) -> SortedSet LinearImplicit -> List (Name, CairoDef) -> List (Name, CairoDef)
transformDefs functionImpls applyImpls defs = map (transformDef functionImpls applyImpls) defs

export
injectLinearImplicitsDefs : List (Name, CairoDef) -> List (Name, CairoDef)
injectLinearImplicitsDefs defs = transformDefs (snd discoveryResult) (fst discoveryResult) defs
    where discoveryResult : (SortedSet LinearImplicit, SortedMap Name (SortedSet LinearImplicit))
          discoveryResult = executeLinearImplicitDiscovery defs


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

import public GRL.Lang.GLang

import Sif.Types

import public Sif.Pattern.Model
import public Sif.Pattern.API
import public Sif.Pattern.Convert

%default partial
%access export

-- --------------------------------------------------- [ Public Data Structure ]

Show (PATTERN impl d) where
  show x =
    case showConvPattern STRING x of
      Nothing => show $ "Internal Err"
      Just r  => r

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


text:
module Printf

import Data.Vect

data Format = Number Format
            | Chr Format
            | Float Format
            | Str Format
            | Lit String Format
            | End

Matrix : Nat -> Nat -> Type
Matrix Z Z = Vect 0 (Vect 0 Nat)
Matrix Z h = Vect 0 (Vect h Nat)
Matrix h j = Vect h (Vect j Nat)

TupleVect : (size : Nat) -> Type -> Type
TupleVect Z ty = ()
TupleVect (S k) ty = (ty, TupleVect k ty)

-- Ex. 1
testMatrix : Matrix 2 3
testMatrix = [[0, 0, 0], [0, 0, 0]]

-- Ex. 3
test : TupleVect 4 Nat
test = (1,2,3,4,())

PrintfType : Format -> Type
PrintfType (Number fmt) = (i : Int) -> PrintfType fmt
PrintfType (Chr fmt) = (c : Char) -> PrintfType fmt
PrintfType (Float fmt) = (f : Double) -> PrintfType fmt
PrintfType (Str fmt) = (str : String) -> PrintfType fmt
PrintfType (Lit str fmt) = PrintfType fmt
PrintfType End = String

printfFmt : (fmt : Format) -> (acc : String) -> PrintfType fmt
printfFmt (Number fmt) acc = \i => printfFmt fmt (acc ++ show i)
printfFmt (Chr fmt) acc = \c => printfFmt fmt (acc ++ show c)
printfFmt (Float fmt) acc = \f => printfFmt fmt (acc ++ show f)
printfFmt (Str fmt) acc = \str => printfFmt fmt (acc ++ str)
printfFmt (Lit str fmt) acc = printfFmt fmt (acc ++ str)
printfFmt End acc = acc

toFormat : (xs : List Char) -> Format
toFormat [] = End
toFormat ('%' :: 'd' :: chars) = Number $ toFormat chars
toFormat ('%' :: 'c' :: chars) = Chr $ toFormat chars
toFormat ('%' :: 'f' :: chars) = Float $ toFormat chars
toFormat ('%' :: 's' :: chars) = Str $ toFormat chars
toFormat ('%' :: chars) = Lit "%" $ toFormat chars
toFormat (c :: chars) = case toFormat chars of
                             Lit str chars' => Lit (strCons c str) chars'
                             fmt => Lit (strCons c "") fmt

printf : (fmt : String) -> PrintfType (toFormat (unpack fmt))
printf fmt = printfFmt _ ""


text:
module Data.HList

import Data.Vect

%access public export
%default total

data HList: (n :Nat) -> Vect n Type -> Type where
  Nil : HList 0 []
  (::) : t -> (HList n tps) -> HList (S n) (t :: tps)

get : (fin:Fin n1) -> HList n1 tps -> (index fin tps)
get FZ (y :: z) = y
get (FS x) (y :: z) = get x z

setWith : (fin:Fin n1) -> HList n1 tps -> ((index fin tps) -> (index fin tps)) -> HList n1 tps
setWith FZ (x :: z) f = (f x) :: z
setWith (FS s) (x :: w) y = x :: (setWith s w y)

set : (fin:Fin n1) -> HList n1 tps -> (index fin tps) -> HList n1 tps
set fin x y = setWith fin x (\a => y)

head : HList (S len) (h :: tps) -> h
head (x :: y) = x

LastType : HList (S n) (a :: tps) -> Type
LastType {a} (x :: []) = a
LastType {a} (x :: l1 @ (t :: ts)) = LastType l1

last : ( l : HList (S n) (t :: ts) ) -> LastType l
last (x :: []) = x
last (x :: l1 @ (y :: z)) = last l1

ZipTypeVect : HList n ts1 -> HList n ts2 -> Vect n Type
ZipTypeVect {ts1 = []} {ts2 = []} [] [] = []
ZipTypeVect {ts1 = (t :: tps)} {ts2 = (y :: xs)} (x :: z) (w :: s) = (t, y) :: ZipTypeVect z s

ZipType : HList n ts1 -> HList n ts2 -> Type
ZipType {n} x y = HList n (ZipTypeVect x y)

zip : (l1 : HList n ts1) -> ( l2 : HList n ts2) -> ZipType l1 l2
zip [] [] = []
zip (x :: y) (z :: w) = (x, z) :: zip y w

hlength : HList n ts1 -> Nat
hlength {n} x = n

take : (n : Nat) -> ( l : HList (n + m) ts ) -> HList n (take n ts)
take Z l = []
take (S k) (x :: y) = x :: take k y

drop : (n : Nat) -> ( l : HList (n + m) ts ) -> HList m (drop n ts)
drop Z l = l
drop (S k) (x :: y) = drop k y

init : HList (S len) (x :: ts) -> HList len (init (x :: ts))
init (x :: []) = []
init (x :: l @ (y :: z)) = x :: (init l)

tail : HList (S len) (x :: ts) -> HList len ts
tail (x :: y) = y

(++) : ( xs : HList m tms ) -> (ys : HList n tns ) -> HList (m + n) (tms ++ tns)
(++) [] ys = ys
(++) (x :: y) ys = x :: (y ++ ys)

updateTypeVect : (fin:Fin n) -> (HList n tps) -> Type -> Vect n Type
updateTypeVect {n = (S k)} {tps = (t :: xs)} FZ (x :: z) y = y :: xs
updateTypeVect {n = (S k)} {tps = (t :: xs)} (FS z) (x :: w) y = t :: (updateTypeVect z w y)

UpdateType : (fin:Fin n) -> (HList n tps) -> Type -> Type
UpdateType fin x y = HList _ $ updateTypeVect fin x y

update : (fin:Fin n) -> (l : HList n tps) -> t -> (UpdateType fin l t)
update FZ (y :: z) x = x :: z
update (FS y) (z :: w) x = z :: (update y w x)

insertAtTypeVect : (fin:Fin (S n)) -> (HList n tps) -> Type -> Vect (S n) Type
insertAtTypeVect {n = n} {tps = tps} FZ x y = y :: tps
insertAtTypeVect {n = Z} {tps = []} (FS z) [] y = [y]
insertAtTypeVect {n = (S k)} {tps = (t :: xs)} (FS z) (x :: w) y = t :: (insertAtTypeVect z w y)

InsertAtType : (fin:Fin (S n)) -> (HList n tps) -> Type -> Type
InsertAtType fin x y = HList _ $ insertAtTypeVect fin x y

insertAt : (fin:Fin (S n)) -> (l : HList n tps) -> t -> InsertAtType fin l t
insertAt FZ l x = x :: l
insertAt (FS y) [] x = [x]
insertAt (FS y) (z :: w) x = z :: insertAt y w x

deleteAtTypeVect : (fin:Fin (S n)) -> (HList (S n) tps) -> Vect n Type
deleteAtTypeVect {tps = (t :: xs)} FZ (x :: y) = xs
deleteAtTypeVect {tps = (t :: (y :: tps))} (FS FZ) (x :: (z :: w)) = t :: tps
deleteAtTypeVect {tps = (t :: xs)} (FS (FS y)) (x :: z) = t :: (deleteAtTypeVect (FS y) z)

DeleteAtType : (fin:Fin (S n)) -> (HList (S n) tps) -> Type
DeleteAtType fin x = HList _ $ deleteAtTypeVect fin x

deleteAt : (fin:Fin (S n)) -> (l : HList (S n) tps) -> (DeleteAtType fin l)
deleteAt FZ (x :: y) = y
deleteAt (FS FZ) (y :: (x :: z)) = y :: z
deleteAt (FS (FS x)) (y :: z) = y :: deleteAt (FS x) z

implementation Eq (HList 0 []) where
  (==) []      []      = True

implementation (Eq a, Eq (HList len elems)) => Eq (HList (S len) (a :: elems)) where
  (==) (x::xs) (y::ys) = x == y && xs == ys

implementation Ord (HList 0 []) where
  compare []      []      = EQ

implementation (Ord a, Ord (HList len elems)) => Ord (HList (S len) (a :: elems)) where
  compare (x::xs) (y::ys) = compare x y `thenCompare` compare xs ys

interface Hap (n:Nat) (tps : Vect n Type) (wts : Vect n Type) where
  hapTypeVect : HList n tps -> HList n wts -> Vect n Type
  hap : (l1:HList n tps) -> (l2:HList n wts) -> HList n $ hapTypeVect l1 l2

implementation Hap Z [] [] where
  hapTypeVect [] [] = []
  hap [] [] = []

implementation (hap:Hap n tps wts) => Hap (S n) (a :: tps) ((a -> b) :: wts) where
  hapTypeVect {b} (a1 :: tps) (f :: wts) = b :: hapTypeVect tps wts
  hap {b} {tps} {wts} (a1 :: tps1) (f :: wts1) = (f a1) :: hap tps1 wts1

max_stars_repo_name: gdefacci/idris-hlist

max_issues_repo_name: gdefacci/idris-hlist

max_forks_repo_name: gdefacci/idris-hlist


text:
foo : ? -> Int
foo x = 42


text:
module Node

import Data.Buffer

%foreign "node:lambda: (ty, a) => JSON.stringify(a, null, 2)"
ffi_toJsonString : a -> String

export
toJsonString : a -> String
toJsonString a = ffi_toJsonString a

%foreign "node:lambda: (ty, a) => console.log(a)"
ffi_debugJsValue : a -> PrimIO ()

export
debugJsValue : a -> IO ()
debugJsValue a = primIO $ ffi_debugJsValue a

%foreign "node:lambda: cb => setTimeout(() => cb(), 0)"
ffi_defer : PrimIO () -> PrimIO ()

export
defer : HasIO io => IO () -> io ()
defer action = primIO $ ffi_defer $ toPrim action

max_stars_repo_name: kbertalan/tyttp

max_issues_repo_name: kbertalan/tyttp

max_forks_repo_name: kbertalan/tyttp