text:
module Idris.IDEMode.SyntaxHighlight

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

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

import Data.List
import Data.Maybe

import Libraries.Data.PosMap

%default total

------------------------------------------------------------------------
-- Text properties supported by the IDE mode
------------------------------------------------------------------------

data Formatting : Type where
  Bold      : Formatting
  Italic    : Formatting
  Underline : Formatting

-- CAREFUL: this instance is used in SExpable Formatting. If you change
-- it then you need to fix the SExpable implementation in order not to
-- break the IDE mode.
Show Formatting where
  show Bold = "bold"
  show Italic = "italic"
  show Underline = "underline"

-- At most one decoration & one formatting
-- (We could use `These` to guarantee non-emptiness but I am not
-- convinced this will stay being just 2 fields e.g. the emacs mode
-- has support for tagging things as errors, adding links, etc.)
public export
record Properties where
  constructor MkProperties
  decor  : Maybe Decoration
  format : Maybe Formatting

export
mkDecor : Decoration -> Properties
mkDecor dec = MkProperties (Just dec) Nothing

export
mkFormat : Formatting -> Properties
mkFormat = MkProperties Nothing . Just

export
syntaxToProperties : IdrisSyntax -> Maybe Properties
syntaxToProperties syn = mkDecor <$> syntaxToDecoration syn

export
annToProperties : IdrisAnn -> Maybe Properties
annToProperties Warning      = Nothing
annToProperties Error        = Nothing
annToProperties ErrorDesc    = Nothing
annToProperties FileCtxt     = Nothing
annToProperties Code         = Nothing
annToProperties Meta         = Nothing
annToProperties (Syntax syn) = syntaxToProperties syn

export
docToProperties : IdrisDocAnn -> Maybe Properties
docToProperties Header        = pure $ mkFormat Underline
docToProperties Declarations  = Nothing
docToProperties (Decl _)      = Nothing
docToProperties DocStringBody = Nothing
docToProperties UserDocString = Nothing
docToProperties (Syntax syn)  = syntaxToProperties syn

SExpable Decoration where
  toSExp decor = SExpList [ SymbolAtom "decor"
                          , SymbolAtom (show decor)
                          ]

SExpable Formatting where
  toSExp format = SExpList [ SymbolAtom "text-formatting"
                           , SymbolAtom (show format)
                           ]

export
SExpable Properties where
  toSExp (MkProperties dec form)  = SExpList $ catMaybes
    [ toSExp <$> form
    , toSExp <$> dec
    ]

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

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

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

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

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

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

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

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

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

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

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

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

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

  pure loadResult


text:
module Data.Crypto.MAC

import Data.Bits

%default total
%access public export

interface Signer s (blockLength : Nat) (outputLength : Nat) | s where
  signMessage : s -> List (Bits blockLength) -> Bits outputLength

interface Verifier v (blockLength : Nat) (outputLength : Nat) | v where
  verifyMessage : v -> List (Bits blockLength) -> Bits n -> Bool

interface (Signer m b o, Verifier m b o) => MAC m (b : Nat) (o : Nat) | m where
  -- TODO: This default implementation _should_ work.
  -- implementation Verifier m b o where
  --   verifyMessage key message digest = digest == signMessage key message

ext: idr

max_stars_repo_name: idris-hackers/idris-crypto

max_issues_repo_name: idris-hackers/idris-crypto

max_forks_repo_name: idris-hackers/idris-crypto


text:
module GRIN.Opts.CopyPropogation

import Data.SortedMap

import GRIN.AST
import GRIN.GrinM

0 CopyMap : Type
CopyMap = SortedMap Var Var

isValVar : (Val name) -> Maybe Var
isValVar (SimpleVal (SVar var)) = Just var
isValVar _ = Nothing

isPureVar : SExp name -> Maybe Var
isPureVar (Pure val) = isValVar val
isPureVar _ = Nothing

copyPropVar : CopyMap -> Var -> Var
copyPropVar cm var = case lookup var cm of
    Nothing => var
    Just var' => var'

copyPropSVal : CopyMap -> SVal -> SVal
copyPropSVal _ (SLit lit) = SLit lit
copyPropSVal cm (SVar var) = SVar (copyPropVar cm var)

copyPropVal : CopyMap -> Val name -> Val name
copyPropVal cm (SimpleVal val) = SimpleVal (copyPropSVal cm val)
copyPropVal cm (ConstTagNode tag args) = ConstTagNode tag (copyPropSVal cm <$> args)
copyPropVal _ (ConstTag tag) = ConstTag tag
copyPropVal cm (VarTagNode var args) = VarTagNode var (copyPropSVal cm <$> args)
copyPropVal _ VUnit = VUnit

mutual
    copyPropSExp : CopyMap -> SExp name -> SExp name
    copyPropSExp cm (Do exp) = Do (copyPropExp cm exp)
    copyPropSExp cm (App fn vars) = App fn (copyPropVar cm <$> vars)
    copyPropSExp cm (Pure val) = Pure (copyPropVal cm val)
    copyPropSExp cm (Store val) = Store (copyPropVal cm val)
    copyPropSExp cm (Fetch i var) = Fetch i (copyPropVar cm var)
    copyPropSExp cm (FetchI i n var) = FetchI i n (copyPropVar cm var)
    copyPropSExp cm (Update var val) = Update (copyPropVar cm var) (copyPropVal cm val)

    copyPropExp : CopyMap -> Exp name -> Exp name
    copyPropExp cm (Bind val rhs rest) =
        let rhs' = copyPropSExp cm rhs in
        case isValVar val of
            Nothing => Bind val rhs' (copyPropExp cm rest)
            Just copy => case isPureVar rhs of
                Nothing => Bind val rhs' (copyPropExp cm rest)
                Just var => copyPropExp (insert copy var cm) rest
    copyPropExp cm (Case val alts) = Case (copyPropVal cm val) (copyPropAlt cm <$> alts)
    copyPropExp cm (SimpleExp exp) = SimpleExp (copyPropSExp cm exp)

    copyPropAlt : CopyMap -> Alt name -> Alt name
    copyPropAlt cm (MkAlt pat exp) = MkAlt pat (copyPropExp cm exp)

export
copyProp : Monad m => GrinT name m ()
copyProp = mapProg $ mapExpProg (copyPropExp empty)


text:
module Control.Comonad

import Control.Monad.Identity

%access public export

--------------------------------------------------------------------------------
-- | Interfaces
--------------------------------------------------------------------------------

-- | `Comonad` extends the `Extend` class with the `extract` function
-- | which extracts a value, discarding the comonadic context.
-- |
-- | dual of |
-- | --------+----------
-- | Monad   | Comonad
-- | bind    | extend
-- | pure    | extract
-- | join    | duplicate

interface Functor w => Comonad (w : Type -> Type) where
  extract : w a -> a

  extend : (w a -> b) -> w a -> w b
  extend f = map f . duplicate

  duplicate : w a -> w (w a)
  duplicate = extend id

interface Comonad w => VerifiedComonad (w : Type -> Type) where
  comonadLeftIdentity : (wx : w a) -> Control.Comonad.extract `extend` wx = wx
  comonadRightIdentity : (wx : w a) -> (f : w a -> b) -> extract (f `extend` wx) = f wx
  comonadAssociative : (wx : w a) -> (f : w b -> c) -> (g : w a -> b) ->
                       (extend f . extend g) wx = extend (f . extend g) wx

infixl 1 <<=
(<<=) : Comonad w => (w a -> b) -> w a -> w b
(<<=) = extend

-- | Forwards co-Kleisli composition
composeCoKleisli : Comonad w => (w a -> b) -> (w b -> c) -> w a -> c
composeCoKleisli f g w = g (f <<= w)

infixl 1 =>=
(=>=) : Comonad w => (w a -> b) -> (w b -> c) -> w a -> c
(=>=) = composeCoKleisli

--------------------------------------------------------------------------------
-- | Functions
--------------------------------------------------------------------------------

liftW : Comonad w => (a -> b) -> w a -> w b
liftW f = extend (f . extract)

--------------------------------------------------------------------------------
-- | Implementations
--------------------------------------------------------------------------------

Comonad Identity where
  duplicate = Id
  extract = runIdentity

VerifiedComonad Identity where
  comonadLeftIdentity (Id runIdentity) = Refl
  comonadRightIdentity (Id runIdentity) f = Refl
  comonadAssociative (Id runIdentity) f g = Refl

max_stars_repo_name: Risto-Stevcev/idris-comonad

max_issues_repo_name: Risto-Stevcev/idris-comonad

max_forks_repo_name: Risto-Stevcev/idris-comonad


text:
module Group_property

import Monoid
import Group
import congruence

%access public export

||| Property 1 - Identity is unique for groups
total
Group_property_1 : (grp : Type) -> ((*) : grp -> grp -> grp) ->
                   (IsGroup grp (*)) -> (e1 : grp) -> (e2 :grp) ->
                   (IsIdentity grp (*) e1) -> (IsIdentity grp (*) e2) ->
                   (e1 = e2)

Group_property_1 grp (*) pf_grp e1 e2 pf1 pf2 = trans (sym(snd (pf2 e1))) (fst (pf1 e2))

||| Property 2 - Inverse of an element is unique
total
Group_property_2 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a : grp) -> (b : grp) -> (c : grp) ->
                   (IsInverse grp (*) (fst(snd pfgrp)) a b) ->
                   (IsInverse grp (*) (fst(snd pfgrp)) a c) -> (b = c)

Group_property_2 grp (*) pfgrp a b c pfb pfc = let
                                               pfAss = fst pfgrp
                                               pfid = (fst (snd pfgrp))
                                               in
                                               rewrite (sym (fst ((snd pfid) b))) in
                                              (rewrite (sym (fst pfc)) in
                                              (rewrite (sym (pfAss b a c)) in
                                              (rewrite (snd pfb) in
                                              (rewrite (snd ((snd pfid) c)) in Refl))))

||| Property 3 - b = c implies a*b = a*c
total
Group_property_3 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a : grp) -> (b : grp) -> (c : grp) -> (b = c) -> (a*b = a*c)
Group_property_3 grp (*) pfgrp a b c pfEq = cong pfEq

||| Property 4 - a*b = a*c implies b = c
total
Group_property_4 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a : grp) -> (b : grp) -> (c : grp) -> (a*b = a*c) -> (b = c)
Group_property_4 grp (*) pfgrp a b c pfEq = let pfid = (fst (snd (snd pfgrp)))
                                                a_inv = fst(Inv_with_pf grp (*) pfgrp a)
                                                pf_inv = snd(Inv_with_pf grp (*) pfgrp a)
                                                pfAss = fst pfgrp
                                                in
                                                (rewrite (sym (snd ((snd pfid) b))) in
                                                (rewrite (sym (snd ((snd pfid) c))) in
                                                (rewrite (sym (snd pf_inv)) in
                                                (rewrite (pfAss a_inv a b) in
                                                (rewrite (pfAss a_inv a c) in
                                                (Group_property_3 grp (*) pfgrp a_inv (a*b) (a*c) pfEq))))))

||| Property 5 - b = c implies b*a = c*a
total
Group_property_5 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a : grp) -> (b : grp) -> (c : grp) -> (b = c) -> ( (b*a) = (c*a) )
Group_property_5 grp (*) pfgrp a b c pfEq = (congruence grp grp b c (\x : grp => x*a) pfEq)

||| Property 6 - b*a = c*a implies b = c
total
Group_property_6 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : IsGroup grp (*)) ->
                   (a : grp) -> (b : grp) -> (c : grp) -> (b*a = c*a) -> (b = c)
Group_property_6 grp (*) pfgrp a b c pfEq = let pfid = (fst (snd (snd pfgrp)))
                                                a_inv = fst(Inv_with_pf grp (*) pfgrp a)
                                                pf_inv = snd(Inv_with_pf grp (*) pfgrp a)
                                                pfAss = fst pfgrp
                                                in
                                                (rewrite (sym (fst ((snd pfid) b))) in
                                                (rewrite (sym (fst ((snd pfid) c))) in
                                                (rewrite (sym (fst pf_inv)) in
                                                (rewrite (sym (pfAss b a a_inv)) in
                                                (rewrite (sym (pfAss c a a_inv)) in
                                                (Group_property_5 grp (*) pfgrp a_inv (b*a) (c*a) pfEq))))))

||| Auxilliary proof 1 - Two idenitities mentioned in the definition of the group
||| (one in (fst (snd pfgrp)) another in (fst (snd (snd pfgrp))) are equal.
total
Group_aux_pf_1 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : (IsGroup grp (*))) ->
                 ( (fst (Group_id grp (*) pfgrp)) = (fst (fst (snd (snd pfgrp)))) )

Group_aux_pf_1 grp (*) pfgrp = let
                               pfid1 = (Group_id grp (*) pfgrp)
                               e1 = (fst pfid1)
                               pf1 = (snd pfid1)
                               pfid2 = (fst (snd (snd pfgrp)))
                               e2 = (fst pfid2)
                               pf2 = (snd pfid2)
                               in
                               (Group_property_1 grp (*) pfgrp e1 e2 pf1 pf2)

||| Property 7 - One sided inverse is two sided inverse
total
Group_property_7 : (grp : Type) -> ((*) : grp -> grp -> grp) -> (pfgrp : (IsGroup grp (*))) -> (a : grp)
                   -> (b : grp) -> ( (a*b) = (fst (Group_id grp (*) pfgrp)) )
                   -> (IsInverse grp (*) (Group_id grp (*) pfgrp) a b)

Group_property_7 grp (*) pfgrp a b pfEq = let
                                          pfid1 = Group_id grp (*) pfgrp -- Identity in IdentityExists
                                          pfid2 = fst (snd (snd pfgrp)) -- Identity in InverseExists
                                          e1 = (fst pfid1)
                                          e2 = (fst pfid2)
                                          a_inv = Inv grp (*) pfgrp a
                                          a_inv_pf = snd (Inv_with_pf grp (*) pfgrp a)
                                          a_inv_pf1 = (fst a_inv_pf) -- Proof that a*a_inv = e2
                                          a_inv_pf2 = (snd a_inv_pf) -- Proof that a_inv*a = e2
                                          pfId_eq = Group_aux_pf_1 grp (*) pfgrp -- proof that e1 = e2
                                          pf1 = trans a_inv_pf1 (sym pfId_eq) -- proof that a*a_inv = e1
                                          pf2 = trans pf1 (sym pfEq) -- proof that a*a_inv = a*b
                                          pf3 = Group_property_4 grp (*) pfgrp a a_inv b pf2 -- proof that a_inv b
                                          pf4 = trans a_inv_pf2 (sym pfId_eq) -- proof that a_inv*a = e1
                                          pf5 = Group_property_5 grp (*) pfgrp a a_inv b pf3 -- proof that a_inv*a = b*a
                                          pf6 = trans (sym pf5) pf4
                                          in
                                          (pfEq, pf6)


text:
import CommonTestingStuff

-------------------------------
--- Preparation for testing ---
-------------------------------

Timed (State $ SnocList String) where
  currentTime = (.millis) <$> length <$> get

CanSleep (State $ SnocList String) where
  sleepFor  _ = pure ()
  sleepTill _ = pure ()

append : MonadState (SnocList a) m => a -> m ()
append x = modify (:< x)

exec : Coop (State $ SnocList String) Unit -> SnocList String
exec = execState [<] . runCoop

-----------------------
--- Unit test cases ---
-----------------------

main : HasIO io => io ()
main = do
  putStrLn "test: do nothing"
  (exec $ pure ()) === [<]

  putStrLn "test: return time at the start"
  (exec $ currentTime >>= append . show) === [<"0"]

  putStrLn "test: return time at the start and then just a string"
  (exec $ currentTime >>= append . show >> append "test") === [<"0", "test"]

  putStrLn "test: consequent appends"
  (exec $ append "test1" *> append "test2") === [<"test1", "test2"]

  putStrLn "test: return time after some message"
  (exec $ append "before time" *> currentTime >>= append . show) === [<"before time", "1"]


text:
module Flexidisc.OrdList.Nub

import Flexidisc.Dec.IsYes
import Flexidisc.OrdList.Fresh
import Flexidisc.OrdList.Type
import Flexidisc.OrdList.Label

%default total
%access public export

||| A proof that each value in the list has a different label
data Nub : (OrdList label value o) -> Type where
  ||| in an empty list, all the values are different indeed
  Nil  : Nub []
  ||| If we add a fresh value, it still holds
  (::) : Fresh l xs -> Nub xs -> Nub ((l,ty) :: xs)

%name Nub nub, isnub, prf

||| Decide whether a list is made of different labelents or not
decNub : DecEq label => (xs : OrdList label value o) -> Dec (Nub xs)
decNub [] = Yes []
decNub ((l, ty) :: xs) with (decFresh l xs)
  | (Yes headFresh) with (decNub xs)
    | (Yes tailFresh) = Yes (headFresh :: tailFresh)
    | (No contra) = No (\ (_ :: tailFresh) => contra tailFresh)
  | (No contra) = No (\ (headFresh :: _) => contra headFresh)

||| Proof that the decision procedure `decNub` gives a `Yes`
IsNub : DecEq label => (xs : OrdList label value o) -> Type
IsNub xs = IsYes (decNub xs)

||| If we remove a labelt from a `Nub` list, this label is `Fresh` for the
||| resulting list.
export
removeFromNubIsFresh : {k : key} ->
                       Nub xs -> (ePre : OrdLabel k xs) -> Fresh k (dropLabel xs ePre)
removeFromNubIsFresh (yes :: isnub) Here = yes
removeFromNubIsFresh (yes :: isnub) (There later) =
  (\p => freshCantBeLabel yes (rewrite (sym p) in later))
  :: removeFromNubIsFresh isnub later

||| `Nub` still hols if we change a value
changeValuePreservesNub : Nub xs -> Nub (changeValue xs loc new)
changeValuePreservesNub [] {loc} = absurd loc
changeValuePreservesNub (p :: pf) {loc = Here} = p :: pf
changeValuePreservesNub (p :: pf) {loc = (There later)} =
  freshOnValueChange p :: changeValuePreservesNub pf

||| If `Nub` holds for a list, it holds if we drop one element from the list
export
dropPreservesNub : Nub xs -> (loc : OrdLabel l xs) -> Nub (dropLabel xs loc)
dropPreservesNub (_   :: x) Here = x
dropPreservesNub (yes :: x) (There later) =
  dropPreservesFresh yes :: dropPreservesNub x later

mapValuesPreservesNub : Nub xs -> Nub (f <$> xs)
mapValuesPreservesNub [] = []
mapValuesPreservesNub (fresh :: nub) = freshOnMapValues fresh :: mapValuesPreservesNub nub

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module FinUtils
import Data.Fin

%access public export

--Fin to Nat
tonatFin: (n: Nat) -> Fin(n) -> Nat
tonatFin (S k) FZ = Z
tonatFin (S k) (FS x) = S (tonatFin k x)

--Euclid's div
Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat)
Eucl Z b = (0,0)
Eucl (S k) b = case (lte (S (S k)) b) of
                    False => (S(fst(Eucl (minus (S k) b) b)), snd(Eucl (minus (S k) b) b))
                    True => (0, S k)
--Nat to Fin (NOT modular values; if it overflows, the result is 0)
tofinNat: (a: Nat) -> (n: Nat) -> Fin n
tofinNat a Z = assert_unreachable
tofinNat Z (S k) = FZ
tofinNat (S j) (S k) = case (lte (S j) (S k)) of
                             False => FS (tofinNat j k)
                             True => FZ

--adding two Fin n's
-- addfin: (n: Nat) -> Fin (S n) -> Fin (S n) -> Fin (S n) -> (Fin (S n), Fin (S n))
-- addfin n x y z = case (tofin ((tonatFin (S n) x)+ (tonatFin (S n) y) + (tonatFin (S n) z)) (S n)) of
--                     [l] => (FZ, l)
--                     [k, l] => (k,l)

-- embedding Fin n in Fin S n vertically
embn: (n: Nat) -> Fin n -> Fin (S n)
embn (S k) FZ = FZ
embn (S k) (FS x) = FS (embn k x)

--Unused mulfinNat - multiplies two Fin n's
-- mulfinNat: (n: Nat) -> Fin (n) -> Fin (n) -> (Fin (n), Fin (n))
-- mulfinNat (S n) x y =  case tofin ((tonatFin (S n) x)*(tonatFin (S n) y)) (S n) of
--                     [l] => (FZ, l)
--                     [k,l] => (k,l)


text:
||| A simple module to process 'literate' documents.
|||
||| The module uses a lexer to split the document into code blocks,
||| delineated by user-defined markers, and code lines that are
||| indicated be a line marker. The lexer returns a document stripped
||| of non-code elements but preserving the original document's line
||| count. Column numbering of code lines are not preserved.
|||
||| The underlying tokeniser is greedy.
|||
||| Once it identifies a line marker it reads a prettifying space then
||| consumes until the end of line. Once identifies a starting code
||| block marker, the lexer will consume input until the next
||| identifiable end block is encountered. Any other content is
||| treated as part of the original document.
|||
||| Thus, the input literate files *must* be well-formed w.r.t
||| to code line markers and code blocks.
|||
||| A further restriction is that literate documents cannot contain
||| the markers within the document's main text: This will confuse the
||| lexer.
|||
module Text.Literate

import Text.Lexer

import Data.List
import Data.List1
import Data.List.Views
import Data.String
import Data.String.Extra

%default total

untilEOL : Recognise False
untilEOL = manyUntil newline any

line : String -> Lexer
line s = exact s <+> (newline <|> space <+> untilEOL)

block : String -> String -> Lexer
block s e = surround (exact s <+> untilEOL) (exact e <+> untilEOL) any

notCodeLine : Lexer
notCodeLine = newline
           <|> any <+> untilEOL

data Token = CodeBlock String String String
           | Any String
           | CodeLine String String

Show Token where
  showPrec d (CodeBlock l r x) = showCon d "CodeBlock" $ showArg l ++ showArg r ++ showArg x
  showPrec d (Any x)           = showCon d "Any" $ showArg x
  showPrec d (CodeLine m x)    = showCon d "CodeLine" $ showArg m ++ showArg x

rawTokens : (delims  : List (String, String))
         -> (markers : List String)
         -> TokenMap (Token)
rawTokens delims ls =
          map (\(l,r) => (block l r, CodeBlock (trim l) (trim r))) delims
       ++ map (\m => (line m, CodeLine (trim m))) ls
       ++ [(notCodeLine, Any)]

namespace Compat
  -- `reduce` below was depending on the old behaviour of `lines` before #1585
  -- was merged. That old `lines` function is added here to preserve behaviour
  -- of `reduce`.
  lines' : List Char -> List1 (List Char)
  lines' [] = singleton []
  lines' s  = case break isNL s of
                   (l, s') => l ::: case s' of
                                         [] => []
                                         _ :: s'' => forget $ lines' (assert_smaller s s'')
  export
  lines : String -> List1 String
  lines s = map pack (lines' (unpack s))

||| Merge the tokens into a single source file.
reduce : List (WithBounds Token) -> List String -> String
reduce [] acc = fastAppend (reverse acc)
reduce (MkBounded (Any x) _ _ :: rest) acc =
  -- newline will always be tokenized as a single token
  if x == "\n"
  then reduce rest ("\n"::acc)
  else reduce rest acc

reduce (MkBounded (CodeLine m src) _ _ :: rest) acc =
    if m == trim src
    then reduce rest ("\n"::acc)
    else reduce rest ((substr (length m + 1) -- remove space to right of marker.
                              (length src)
                              src
                      )::acc)

reduce (MkBounded (CodeBlock l r src) _ _ :: rest) acc with (Compat.lines src) -- Strip the deliminators surrounding the block.
  reduce (MkBounded (CodeBlock l r src) _ _ :: rest) acc | (s ::: ys) with (snocList ys)
    reduce (MkBounded (CodeBlock l r src) _ _ :: rest) acc | (s ::: []) | Empty = reduce rest acc -- 2
    reduce (MkBounded (CodeBlock l r src) _ _ :: rest) acc | (s ::: (srcs ++ [f])) | (Snoc f srcs rec) =
        -- the "\n" counts for the open deliminator; the closing deliminator should always be followed by a (Any "\n"), so we don't add a newline
        reduce rest (((unlines srcs) ++ "\n") :: "\n" :: acc)

-- [ NOTE ] 1 & 2 shouldn't happen as code blocks are well formed i.e. have two deliminators.

public export
record LiterateError where
  constructor MkLitErr
  line   : Int
  column : Int
  input  : String

||| Description of literate styles.
|||
||| A 'literate' style comprises of
|||
||| + a list of code block deliminators (`deliminators`);
||| + a list of code line markers (`line_markers`); and
||| + a list of known file extensions `file_extensions`.
|||
||| Some example specifications:
|||
||| + Bird Style
|||
|||```
|||MkLitStyle Nil [">"] [".lidr"]
|||```
|||
||| + Literate Haskell (for LaTeX)
|||
|||```
|||MkLitStyle [("\\begin{code}", "\\end{code}"),("\\begin{spec}","\\end{spec}")]
|||           Nil
|||           [".lhs", ".tex"]
|||```
|||
||| + OrgMode
|||
|||```
|||MkLitStyle [("#+BEGIN_SRC idris","#+END_SRC"), ("#+COMMENT idris","#+END_COMMENT")]
|||           ["#+IDRIS:"]
|||           [".org"]
|||```
|||
||| + Common Mark
|||
|||```
|||MkLitStyle [("```idris","```"), ("<!-- idris","--!>")]
|||           Nil
|||           [".md", ".markdown"]
|||```
|||
public export
record LiterateStyle where
  constructor MkLitStyle
  ||| The pairs of start and end tags for code blocks.
  deliminators : List (String, String)

  ||| Line markers that indicate a line contains code.
  line_markers : List String

  ||| Recognised file extensions. Not used by the module, but will be
  ||| of use when connecting to code that reads in the original source
  ||| files.
  file_extensions : List String

||| Given a 'literate specification' extract the code from the
||| literate source file (`litStr`) that follows the presented style.
|||
||| @specification The literate specification to use.
||| @litStr  The literate source file.
|||
||| Returns a `LiterateError` if the literate file contains malformed
||| code blocks or code lines.
|||
export
extractCode : (specification : LiterateStyle)
           -> (litStr        : String)
           -> Either LiterateError String
extractCode (MkLitStyle delims markers exts) str =
      case lex (rawTokens delims markers) str of
        (toks, (_,_,"")) => Right (reduce toks Nil)
        (_, (l,c,i))     => Left (MkLitErr l c i)

||| Synonym for `extractCode`.
export
unlit : (specification : LiterateStyle)
     -> (litStr        : String)
     -> Either LiterateError String
unlit = extractCode

||| Is the provided line marked up using a line marker?
|||
||| If the line is suffixed by any one of the style's set of line
||| markers then return length of literate line marker, and the code stripped from the line
||| marker. Otherwise, return Nothing and the unmarked line.
export
isLiterateLine : (specification : LiterateStyle)
              -> (str : String)
              -> Pair (Maybe String) String
isLiterateLine (MkLitStyle delims markers _) str with (lex (rawTokens delims markers) str)
  isLiterateLine (MkLitStyle delims markers _) str | ([MkBounded (CodeLine m str') _ _], (_,_, "")) = (Just m, str')
  isLiterateLine (MkLitStyle delims markers _) str | (_, _) = (Nothing, str)

||| Given a 'literate specification' embed the given code using the
||| literate style provided.
|||
||| If the style uses deliminators to denote code blocks use the first
||| pair of deliminators in the style. Otherwise use first linemarker
||| in the style. If there is **no style** return the presented code
||| string unembedded.
|||
|||
||| @specification The literate specification to use.
||| @code  The code to embed,
|||
|||
export
embedCode : (specification : LiterateStyle)
         -> (code : String)
         -> String
embedCode (MkLitStyle ((s,e)::delims) _            _) str = unlines [s,str,e]
embedCode (MkLitStyle Nil             (m::markers) _) str = unwords [m, str]
embedCode (MkLitStyle _               _            _) str = str

||| Synonm for `embedCode`
export
relit : (specification : LiterateStyle)
     -> (code : String)
     -> String
relit = embedCode

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


text:
module Another.One.Third

import A.Path.Of.Dires.First

%default total

export
map : (a -> b) -> Tree a -> Tree b
map f (Leaf a) = Leaf (f a)
map f (Node l r) = Node (map f l) (map f r)


text:
module Misc

smallOdds : List Integer
smallOdds = [x | x <- [1..20], Builtins.mod x 2 == 0 ]

greeter : String -> String
greeter whom = "Hello to " ++ whom

max_stars_repo_name: harrisi/on-being-better

max_issues_repo_name: harrisi/on-being-better

max_forks_repo_name: harrisi/on-being-better


text:
import Data.Vect

strange : (n : Nat) -> if n == 0 then Int else String
strange Z = 0
strange (S k) = "positive"

strangeLength : (s : String) -> if length s == 0 then Int else String
strangeLength s = strange (length s)

{-
-- Doesn't compile, because Idris enforces parametricity.
replicateWithWart : (n : Nat) -> a -> Vect n a
replicateWithWart {a} n x =
  case a of
    Int => replicate n 0
    _   => replicate n x
-}

useTortured : a -> b -> (Type, a, b)
useTortured {a} {b} x y = tortured [a, b] x y

-- Doesn't compile
useTorturedBroken : a -> b -> (Type, a, b)
useTorturedBroken {a} {b} x y = tortured [a, b] x x

{-
-- Doesn't compile
useTorturedBroken : (x : a) -> (y : b) -> (Type, a, b)
useTorturedBroken {a} {b} x y = tortured [a, b] x x
-}

{-
-- Doesn't compile
strangeLengthBroken : (s : String) -> if length s == 0 then Int else String
strangeLengthBroken s = strange (length s + 1)
-}

{-
zipReplicasBroken : (numAs : Nat) -> a -> (numBs : Nat) -> b -> Vect numAs (a, b)
zipReplicasBroken numAs valA numBs valB =
  let aVec = replicate numAs valA
      bVec = replicate numBs valB
  in Vect.zip aVec bVec
-}
zipReplicas : (n : Nat) -> a -> b -> Vect n (a, b)
zipReplicas n valA valB =
  let aVec = replicate n valA
      bVec = replicate n valB
  in Vect.zip aVec bVec

{-
zipReplicasSuccessorBroken : (n : Nat) -> a -> b -> Vect (n + 1) (a, b)
zipReplicasSuccessorBroken n valA valB =
  let aVec = replicate (n + 1) valA
      bVec = valB :: replicate n valB
  in Vect.zip aVec bVec
~-}
zipReplicasSuccessor : (n : Nat) -> a -> b -> Vect (1 + n) (a, b)
zipReplicasSuccessor n valA valB =
  let aVec = replicate (1 + n) valA
      bVec = valB :: replicate n valB
  in Vect.zip aVec bVec

zipReplicasSuccessor2 : (n : Nat) -> a -> b -> Vect (n + 1) (a, b)
zipReplicasSuccessor2 n valA valB =
  let aVec = replicate (n + 1) valA
      bVec = valB :: replicate n valB
  in Vect.zip aVec (rewrite plusCommutative n 1 in bVec)