text:
module Language.LSP.Message.DocumentHighlight

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
public export
record DocumentHighlightClientCapabilities where
  constructor MkDocumentHighlightClientCapabilities
  dynamicRegistration : Maybe Bool
%runElab deriveJSON defaultOpts `{{DocumentHighlightClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
public export
record DocumentHighlightOptions where
  constructor MkDocumentHighlightOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{{DocumentHighlightOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
public export
record DocumentHighlightRegistrationOptions where
  constructor MkDocumentHighlightRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
%runElab deriveJSON defaultOpts `{{DocumentHighlightRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
public export
record DocumentHighlightParams where
  constructor MkDocumentHighlightParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
  position           : Position
%runElab deriveJSON defaultOpts `{{DocumentHighlightParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
namespace DocumentHighlightKind
  public export
  data DocumentHighlightKind = Text | Read | Write

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
export
ToJSON DocumentHighlightKind where
  toJSON Text  = JNumber 1
  toJSON Read  = JNumber 2
  toJSON Write = JNumber 3

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
export
FromJSON DocumentHighlightKind where
  fromJSON (JNumber 1) = pure Text
  fromJSON (JNumber 2) = pure Read
  fromJSON (JNumber 3) = pure Write
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_documentHighlight
public export
record DocumentHighlight where
  constructor MkDocumentHighlight
  range : Range
  kind  : Maybe DocumentHighlightKind
%runElab deriveJSON defaultOpts `{{DocumentHighlight}}


text:
import Text.Readline

echoLoop : IO ()
echoLoop
    = do Just x <- readline "> "
              | Nothing => putStrLn "EOF"
         putStrLn ("Read: " ++ x)
         when (x /= "") $ addHistory x
         if x /= "quit"
            then echoLoop
            else putStrLn "Done"

main : IO ()
main = echoLoop

ext: idr


text:
-- $ chcp 65001
-- $ idris
-- > :l G1UpperProverNewyear
module G1UpperProverNewyear

import G4LowerFormalPSpring
import G3MiddleFunctionsWinter
import G2Postulate

%default total

gx1 : GNat
gx1 = 17

-- 46
data IsProvable : GNat -> Type where
  Yes : (p ** True = proves p x) -> IsProvable x

postulate p315 : (c, d : GNat) -> True = proves c (forall d (r d)) -> IsProvable (r c)

||| Double negation elimination
--DNE : Type -> Type
--DNE p = Not $ Not p -> p
-- 二重否定除去
postulate dne : ((a -> Void) -> Void) -> a
dne2 : a -> ((a -> Void) -> Void)
dne2 x f = f x

||| The converse of contraposition: (p -> q) -> Not q -> Not p
Transposition : Type -> Type -> Type
Transposition p q = (Not q -> Not p) -> p -> q

-- E1
fuga2 : Transposition ((Not . IsProvable) 17) ((t:GNat) -> False = proves t 17)
fuga2 prf p = let ans1 = flip prf p in let ans2 = dne ans1 in ans2
fuga4 : (((t : Nat) -> False = proves t 17) -> Void) -> IsProvable 17
fuga3 : (((t : Nat) -> False = proves t 17) -> Void) -> (IsProvable 17 -> Void) -> Void
fuga3 = dne2 . fuga4
fuga5 : (IsProvable 17 -> Void) -> (t : Nat) -> False = proves t 17
fuga5 = fuga2 fuga3

hoge : IsProvable (forall 17 (r 17)) -> GNat
hoge (Yes dep) -- = ?rhs1
  = let s = fst dep in let prf = snd dep in
    let d5 = p315 s gx1 prf in ?rhs1

namespace a
  -- 46_2
  data IsProvable2 : Bool -> GNat -> Type where
    Yes : (p ** True = proves p x) -> IsProvable2 True x
    No : ((t : GNat) -> False = proves t x) -> IsProvable2 False x

  huga : IsProvable2 True (forall 17 (r 17)) -> GNat
  huga (Yes dep) = 3


text:
module A

public export
-- interface AInt x where
interface BFromInteger x where
  foo : Integer -> x


text:
-- ------------------------------------------------------------ [ Position.idr ]
-- Module    : Lightyear.Position
-- Description : Positioning in source files.
--
-- This code is distributed under the BSD 2-clause license.
-- See the file LICENSE in the root directory for its full text.
-- --------------------------------------------------------------------- [ EOH ]
module Lightyear.Position

import Data.Nat
import Data.Strings

%default total
-- %access export

||| Generic representation of a position.
public export
record Position where
  constructor MkPos
  fname   : Maybe String
  lineNo  : Nat
  colNo   : Nat

export
defaultPos : Maybe String -> Position
defaultPos fname = MkPos fname 1 1

namespace Generic
  ||| Increment the position one character.
  export
  increment : (tabwidth  : Nat)
           -> (curr_pos  : Position)
           -> (character : Char)
           -> Position
  increment _      (MkPos f l _) '\n' = MkPos f (S l) 1
  increment twidth (MkPos f l c) '\t' = MkPos f l     (nextTab twidth)
    where
      nextTab : Nat -> Nat
      nextTab Z              = c
      nextTab twidth@(S ptw) = (divNatNZ ((minus c 1) + twidth) twidth SIsNotZ) * twidth + 1

  increment _ (MkPos f l c) _ = MkPos f l (S c)

  ||| Increment the position one character.
  export
  inc : Nat -> Position -> Char -> Position
  inc = Generic.increment

||| Increment the position one character with a default tab width of eight.
export
increment : Position -> Char -> Position
increment = Generic.increment 8

||| Increment the position one character with a default tab width of eight.
export
inc : Position -> Char -> Position
inc = Generic.increment 8

-- [ NOTE ]
--
-- When comparing ASTs it would be nice to ignore positioning information.

Eq Position where
  (==) _ _ = True

Ord Position where
  compare _ _ = EQ

export
display : Position -> String
display (MkPos (Just fname) l c) = concat [show fname, ":", show l, ":", show c]
display (MkPos Nothing      l c) = concat ["At ", show l, ":", show c]

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

max_stars_repo_name: Mr-Andersen/lightyear

max_issues_repo_name: Mr-Andersen/lightyear

max_forks_repo_name: Mr-Andersen/lightyear


text:
module Web.Raw.Animation

import JS
import Web.Internal.AnimationPrim
import Web.Internal.Types

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

namespace Animation

  export
  currentTime :  (0 _ : JSType t)
              => {auto 0 _ : Elem Animation (Types t)}
              -> t
              -> Attribute False Maybe Double
  currentTime v = fromNullablePrim "Animation.getcurrentTime"
                                   prim__currentTime
                                   prim__setCurrentTime
                                   (v :> Animation)

  export
  effect :  (0 _ : JSType t)
         => {auto 0 _ : Elem Animation (Types t)}
         -> t
         -> Attribute False Maybe AnimationEffect
  effect v = fromNullablePrim "Animation.geteffect"
                              prim__effect
                              prim__setEffect
                              (v :> Animation)

  export
  finished :  (0 _ : JSType t1)
           => {auto 0 _ : Elem Animation (Types t1)}
           -> (obj : t1)
           -> JSIO (Promise Animation)
  finished a = primJS $ Animation.prim__finished (up a)

  export
  id :  (0 _ : JSType t)
     => {auto 0 _ : Elem Animation (Types t)}
     -> t
     -> Attribute True I String
  id v = fromPrim "Animation.getid" prim__id prim__setId (v :> Animation)

  export
  oncancel :  (0 _ : JSType t)
           => {auto 0 _ : Elem Animation (Types t)}
           -> t
           -> Attribute False Maybe EventHandlerNonNull
  oncancel v = fromNullablePrim "Animation.getoncancel"
                                prim__oncancel
                                prim__setOncancel
                                (v :> Animation)

  export
  onfinish :  (0 _ : JSType t)
           => {auto 0 _ : Elem Animation (Types t)}
           -> t
           -> Attribute False Maybe EventHandlerNonNull
  onfinish v = fromNullablePrim "Animation.getonfinish"
                                prim__onfinish
                                prim__setOnfinish
                                (v :> Animation)

  export
  pending :  (0 _ : JSType t1)
          => {auto 0 _ : Elem Animation (Types t1)}
          -> (obj : t1)
          -> JSIO Bool
  pending a = tryJS "Animation.pending" $ Animation.prim__pending (up a)

  export
  playState :  (0 _ : JSType t1)
            => {auto 0 _ : Elem Animation (Types t1)}
            -> (obj : t1)
            -> JSIO AnimationPlayState
  playState a = tryJS "Animation.playState" $ Animation.prim__playState (up a)

  export
  playbackRate :  (0 _ : JSType t)
               => {auto 0 _ : Elem Animation (Types t)}
               -> t
               -> Attribute True I Double
  playbackRate v = fromPrim "Animation.getplaybackRate"
                            prim__playbackRate
                            prim__setPlaybackRate
                            (v :> Animation)

  export
  ready :  (0 _ : JSType t1)
        => {auto 0 _ : Elem Animation (Types t1)}
        -> (obj : t1)
        -> JSIO (Promise Animation)
  ready a = primJS $ Animation.prim__ready (up a)

  export
  startTime :  (0 _ : JSType t)
            => {auto 0 _ : Elem Animation (Types t)}
            -> t
            -> Attribute False Maybe Double
  startTime v = fromNullablePrim "Animation.getstartTime"
                                 prim__startTime
                                 prim__setStartTime
                                 (v :> Animation)

  export
  timeline :  (0 _ : JSType t)
           => {auto 0 _ : Elem Animation (Types t)}
           -> t
           -> Attribute False Maybe AnimationTimeline
  timeline v = fromNullablePrim "Animation.gettimeline"
                                prim__timeline
                                prim__setTimeline
                                (v :> Animation)

  export
  cancel :  (0 _ : JSType t1)
         => {auto 0 _ : Elem Animation (Types t1)}
         -> (obj : t1)
         -> JSIO ()
  cancel a = primJS $ Animation.prim__cancel (up a)

  export
  finish :  (0 _ : JSType t1)
         => {auto 0 _ : Elem Animation (Types t1)}
         -> (obj : t1)
         -> JSIO ()
  finish a = primJS $ Animation.prim__finish (up a)

  export
  pause :  (0 _ : JSType t1)
        => {auto 0 _ : Elem Animation (Types t1)}
        -> (obj : t1)
        -> JSIO ()
  pause a = primJS $ Animation.prim__pause (up a)

  export
  play :  (0 _ : JSType t1)
       => {auto 0 _ : Elem Animation (Types t1)}
       -> (obj : t1)
       -> JSIO ()
  play a = primJS $ Animation.prim__play (up a)

  export
  reverse :  (0 _ : JSType t1)
          => {auto 0 _ : Elem Animation (Types t1)}
          -> (obj : t1)
          -> JSIO ()
  reverse a = primJS $ Animation.prim__reverse (up a)

  export
  updatePlaybackRate :  (0 _ : JSType t1)
                     => {auto 0 _ : Elem Animation (Types t1)}
                     -> (obj : t1)
                     -> (playbackRate : Double)
                     -> JSIO ()
  updatePlaybackRate a b = primJS $ Animation.prim__updatePlaybackRate (up a) b

namespace AnimationEffect

  export
  getComputedTiming :  (0 _ : JSType t1)
                    => {auto 0 _ : Elem AnimationEffect (Types t1)}
                    -> (obj : t1)
                    -> JSIO ComputedEffectTiming
  getComputedTiming a = primJS $ AnimationEffect.prim__getComputedTiming (up a)

  export
  getTiming :  (0 _ : JSType t1)
            => {auto 0 _ : Elem AnimationEffect (Types t1)}
            -> (obj : t1)
            -> JSIO EffectTiming
  getTiming a = primJS $ AnimationEffect.prim__getTiming (up a)

  export
  updateTiming :  (0 _ : JSType t1)
               => (0 _ : JSType t2)
               => {auto 0 _ : Elem AnimationEffect (Types t1)}
               -> {auto 0 _ : Elem OptionalEffectTiming (Types t2)}
               -> (obj : t1)
               -> (timing : Optional t2)
               -> JSIO ()
  updateTiming a b = primJS
                   $ AnimationEffect.prim__updateTiming (up a) (optUp b)

  export
  updateTiming' :  (0 _ : JSType t1)
                => {auto 0 _ : Elem AnimationEffect (Types t1)}
                -> (obj : t1)
                -> JSIO ()
  updateTiming' a = primJS $ AnimationEffect.prim__updateTiming (up a) undef

namespace AnimationPlaybackEvent

  export
  currentTime : (obj : AnimationPlaybackEvent) -> JSIO (Maybe Double)
  currentTime a = tryJS "AnimationPlaybackEvent.currentTime"
                $ AnimationPlaybackEvent.prim__currentTime a

  export
  timelineTime : (obj : AnimationPlaybackEvent) -> JSIO (Maybe Double)
  timelineTime a = tryJS "AnimationPlaybackEvent.timelineTime"
                 $ AnimationPlaybackEvent.prim__timelineTime a

namespace AnimationTimeline

  export
  currentTime :  (0 _ : JSType t1)
              => {auto 0 _ : Elem AnimationTimeline (Types t1)}
              -> (obj : t1)
              -> JSIO (Maybe Double)
  currentTime a = tryJS "AnimationTimeline.currentTime"
                $ AnimationTimeline.prim__currentTime (up a)

namespace KeyframeEffect

  export
  composite : KeyframeEffect -> Attribute True I CompositeOperation
  composite v = fromPrim "KeyframeEffect.getcomposite"
                         prim__composite
                         prim__setComposite
                         v

  export
  iterationComposite :  KeyframeEffect
                     -> Attribute True I IterationCompositeOperation
  iterationComposite v = fromPrim "KeyframeEffect.getiterationComposite"
                                  prim__iterationComposite
                                  prim__setIterationComposite
                                  v

  export
  target :  KeyframeEffect
         -> Attribute False Maybe (NS I [ Element , CSSPseudoElement ])
  target v = fromNullablePrim "KeyframeEffect.gettarget"
                              prim__target
                              prim__setTarget
                              v

  export
  getKeyframes : (obj : KeyframeEffect) -> JSIO (Array Object)
  getKeyframes a = primJS $ KeyframeEffect.prim__getKeyframes a

  export
  setKeyframes :  (0 _ : JSType t1)
               => {auto 0 _ : Elem Object (Types t1)}
               -> (obj : KeyframeEffect)
               -> (keyframes : Maybe t1)
               -> JSIO ()
  setKeyframes a b = primJS $ KeyframeEffect.prim__setKeyframes a (mayUp b)

--------------------------------------------------------------------------------
--          Mixins
--------------------------------------------------------------------------------

namespace Animatable

  export
  animate :  (0 _ : JSType t1)
          => (0 _ : JSType t2)
          => {auto 0 _ : Elem Animatable (Types t1)}
          -> {auto 0 _ : Elem Object (Types t2)}
          -> (obj : t1)
          -> (keyframes : Maybe t2)
          -> (options : Optional (NS I [ Double , KeyframeAnimationOptions ]))
          -> JSIO Animation
  animate a b c = primJS $ Animatable.prim__animate (up a) (mayUp b) (toFFI c)

  export
  animate' :  (0 _ : JSType t1)
           => (0 _ : JSType t2)
           => {auto 0 _ : Elem Animatable (Types t1)}
           -> {auto 0 _ : Elem Object (Types t2)}
           -> (obj : t1)
           -> (keyframes : Maybe t2)
           -> JSIO Animation
  animate' a b = primJS $ Animatable.prim__animate (up a) (mayUp b) undef

  export
  getAnimations :  (0 _ : JSType t1)
                => {auto 0 _ : Elem Animatable (Types t1)}
                -> (obj : t1)
                -> JSIO (Array Animation)
  getAnimations a = primJS $ Animatable.prim__getAnimations (up a)

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

namespace AnimationPlaybackEventInit

  export
  new :  (currentTime : Optional (Maybe Double))
      -> (timelineTime : Optional (Maybe Double))
      -> JSIO AnimationPlaybackEventInit
  new a b = primJS $ AnimationPlaybackEventInit.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO AnimationPlaybackEventInit
  new' = primJS $ AnimationPlaybackEventInit.prim__new undef undef

  export
  currentTime :  (0 _ : JSType t)
              => {auto 0 _ : Elem AnimationPlaybackEventInit (Types t)}
              -> t
              -> Attribute True Optional (Maybe Double)
  currentTime v = fromUndefOrPrim "AnimationPlaybackEventInit.getcurrentTime"
                                  prim__currentTime
                                  prim__setCurrentTime
                                  Nothing
                                  (v :> AnimationPlaybackEventInit)

  export
  timelineTime :  (0 _ : JSType t)
               => {auto 0 _ : Elem AnimationPlaybackEventInit (Types t)}
               -> t
               -> Attribute True Optional (Maybe Double)
  timelineTime v = fromUndefOrPrim "AnimationPlaybackEventInit.gettimelineTime"
                                   prim__timelineTime
                                   prim__setTimelineTime
                                   Nothing
                                   (v :> AnimationPlaybackEventInit)

namespace BaseComputedKeyframe

  export
  new :  (offset : Optional (Maybe Double))
      -> (computedOffset : Optional Double)
      -> (easing : Optional String)
      -> (composite : Optional CompositeOperationOrAuto)
      -> JSIO BaseComputedKeyframe
  new a b c d = primJS
              $ BaseComputedKeyframe.prim__new (toFFI a)
                                               (toFFI b)
                                               (toFFI c)
                                               (toFFI d)

  export
  new' : JSIO BaseComputedKeyframe
  new' = primJS $ BaseComputedKeyframe.prim__new undef undef undef undef

  export
  composite :  (0 _ : JSType t)
            => {auto 0 _ : Elem BaseComputedKeyframe (Types t)}
            -> t
            -> Attribute False Optional CompositeOperationOrAuto
  composite v = fromUndefOrPrimNoDefault "BaseComputedKeyframe.getcomposite"
                                         prim__composite
                                         prim__setComposite
                                         (v :> BaseComputedKeyframe)

  export
  computedOffset :  (0 _ : JSType t)
                 => {auto 0 _ : Elem BaseComputedKeyframe (Types t)}
                 -> t
                 -> Attribute False Optional Double
  computedOffset v = fromUndefOrPrimNoDefault "BaseComputedKeyframe.getcomputedOffset"
                                              prim__computedOffset
                                              prim__setComputedOffset
                                              (v :> BaseComputedKeyframe)

  export
  easing :  (0 _ : JSType t)
         => {auto 0 _ : Elem BaseComputedKeyframe (Types t)}
         -> t
         -> Attribute True Optional String
  easing v = fromUndefOrPrim "BaseComputedKeyframe.geteasing"
                             prim__easing
                             prim__setEasing
                             "linear"
                             (v :> BaseComputedKeyframe)

  export
  offset :  (0 _ : JSType t)
         => {auto 0 _ : Elem BaseComputedKeyframe (Types t)}
         -> t
         -> Attribute True Optional (Maybe Double)
  offset v = fromUndefOrPrim "BaseComputedKeyframe.getoffset"
                             prim__offset
                             prim__setOffset
                             Nothing
                             (v :> BaseComputedKeyframe)

namespace BaseKeyframe

  export
  new :  (offset : Optional (Maybe Double))
      -> (easing : Optional String)
      -> (composite : Optional CompositeOperationOrAuto)
      -> JSIO BaseKeyframe
  new a b c = primJS $ BaseKeyframe.prim__new (toFFI a) (toFFI b) (toFFI c)

  export
  new' : JSIO BaseKeyframe
  new' = primJS $ BaseKeyframe.prim__new undef undef undef

  export
  composite :  (0 _ : JSType t)
            => {auto 0 _ : Elem BaseKeyframe (Types t)}
            -> t
            -> Attribute False Optional CompositeOperationOrAuto
  composite v = fromUndefOrPrimNoDefault "BaseKeyframe.getcomposite"
                                         prim__composite
                                         prim__setComposite
                                         (v :> BaseKeyframe)

  export
  easing :  (0 _ : JSType t)
         => {auto 0 _ : Elem BaseKeyframe (Types t)}
         -> t
         -> Attribute True Optional String
  easing v = fromUndefOrPrim "BaseKeyframe.geteasing"
                             prim__easing
                             prim__setEasing
                             "linear"
                             (v :> BaseKeyframe)

  export
  offset :  (0 _ : JSType t)
         => {auto 0 _ : Elem BaseKeyframe (Types t)}
         -> t
         -> Attribute True Optional (Maybe Double)
  offset v = fromUndefOrPrim "BaseKeyframe.getoffset"
                             prim__offset
                             prim__setOffset
                             Nothing
                             (v :> BaseKeyframe)

namespace BasePropertyIndexedKeyframe

  export
  new :  (offset : Optional (Maybe (NS I [ Double , Array (Nullable Double) ])))
      -> (easing : Optional (NS I [ String , Array String ]))
      -> (composite : Optional (NS I [ CompositeOperationOrAuto
                                     , Array String
                                     ]))
      -> JSIO BasePropertyIndexedKeyframe
  new a b c = primJS
            $ BasePropertyIndexedKeyframe.prim__new (toFFI a)
                                                    (toFFI b)
                                                    (toFFI c)

  export
  new' : JSIO BasePropertyIndexedKeyframe
  new' = primJS $ BasePropertyIndexedKeyframe.prim__new undef undef undef

  export
  composite :  (0 _ : JSType t)
            => {auto 0 _ : Elem BasePropertyIndexedKeyframe (Types t)}
            -> t
            -> Attribute False Optional (Union2 String (Array String))
  composite v = fromUndefOrPrimNoDefault "BasePropertyIndexedKeyframe.getcomposite"
                                         prim__composite
                                         prim__setComposite
                                         (v :> BasePropertyIndexedKeyframe)

  export
  easing :  (0 _ : JSType t)
         => {auto 0 _ : Elem BasePropertyIndexedKeyframe (Types t)}
         -> t
         -> Attribute False Optional (Union2 String (Array String))
  easing v = fromUndefOrPrimNoDefault "BasePropertyIndexedKeyframe.geteasing"
                                      prim__easing
                                      prim__setEasing
                                      (v :> BasePropertyIndexedKeyframe)

  export
  offset :  (0 _ : JSType t)
         => {auto 0 _ : Elem BasePropertyIndexedKeyframe (Types t)}
         -> t
         -> Attribute False Optional (Maybe (Union2 Double
                                                    (Array (Nullable Double))))
  offset v = fromUndefOrPrimNoDefault "BasePropertyIndexedKeyframe.getoffset"
                                      prim__offset
                                      prim__setOffset
                                      (v :> BasePropertyIndexedKeyframe)

namespace ComputedEffectTiming

  export
  new :  (endTime : Optional Double)
      -> (activeDuration : Optional Double)
      -> (localTime : Optional (Maybe Double))
      -> (progress : Optional (Maybe Double))
      -> (currentIteration : Optional (Maybe Double))
      -> JSIO ComputedEffectTiming
  new a b c d e = primJS
                $ ComputedEffectTiming.prim__new (toFFI a)
                                                 (toFFI b)
                                                 (toFFI c)
                                                 (toFFI d)
                                                 (toFFI e)

  export
  new' : JSIO ComputedEffectTiming
  new' = primJS $ ComputedEffectTiming.prim__new undef undef undef undef undef

  export
  activeDuration :  (0 _ : JSType t)
                 => {auto 0 _ : Elem ComputedEffectTiming (Types t)}
                 -> t
                 -> Attribute False Optional Double
  activeDuration v = fromUndefOrPrimNoDefault "ComputedEffectTiming.getactiveDuration"
                                              prim__activeDuration
                                              prim__setActiveDuration
                                              (v :> ComputedEffectTiming)

  export
  currentIteration :  (0 _ : JSType t)
                   => {auto 0 _ : Elem ComputedEffectTiming (Types t)}
                   -> t
                   -> Attribute False Optional (Maybe Double)
  currentIteration v = fromUndefOrPrimNoDefault "ComputedEffectTiming.getcurrentIteration"
                                                prim__currentIteration
                                                prim__setCurrentIteration
                                                (v :> ComputedEffectTiming)

  export
  endTime :  (0 _ : JSType t)
          => {auto 0 _ : Elem ComputedEffectTiming (Types t)}
          -> t
          -> Attribute False Optional Double
  endTime v = fromUndefOrPrimNoDefault "ComputedEffectTiming.getendTime"
                                       prim__endTime
                                       prim__setEndTime
                                       (v :> ComputedEffectTiming)

  export
  localTime :  (0 _ : JSType t)
            => {auto 0 _ : Elem ComputedEffectTiming (Types t)}
            -> t
            -> Attribute False Optional (Maybe Double)
  localTime v = fromUndefOrPrimNoDefault "ComputedEffectTiming.getlocalTime"
                                         prim__localTime
                                         prim__setLocalTime
                                         (v :> ComputedEffectTiming)

  export
  progress :  (0 _ : JSType t)
           => {auto 0 _ : Elem ComputedEffectTiming (Types t)}
           -> t
           -> Attribute False Optional (Maybe Double)
  progress v = fromUndefOrPrimNoDefault "ComputedEffectTiming.getprogress"
                                        prim__progress
                                        prim__setProgress
                                        (v :> ComputedEffectTiming)

namespace DocumentTimelineOptions

  export
  new : (originTime : Optional Double) -> JSIO DocumentTimelineOptions
  new a = primJS $ DocumentTimelineOptions.prim__new (toFFI a)

  export
  new' : JSIO DocumentTimelineOptions
  new' = primJS $ DocumentTimelineOptions.prim__new undef

  export
  originTime :  (0 _ : JSType t)
             => {auto 0 _ : Elem DocumentTimelineOptions (Types t)}
             -> t
             -> Attribute True Optional Double
  originTime v = fromUndefOrPrim "DocumentTimelineOptions.getoriginTime"
                                 prim__originTime
                                 prim__setOriginTime
                                 0
                                 (v :> DocumentTimelineOptions)

namespace EffectTiming

  export
  new :  (delay : Optional Double)
      -> (endDelay : Optional Double)
      -> (fill : Optional FillMode)
      -> (iterationStart : Optional Double)
      -> (iterations : Optional Double)
      -> (duration : Optional (NS I [ Double , String ]))
      -> (direction : Optional PlaybackDirection)
      -> (easing : Optional String)
      -> JSIO EffectTiming
  new a b c d e f g h = primJS
                      $ EffectTiming.prim__new (toFFI a)
                                               (toFFI b)
                                               (toFFI c)
                                               (toFFI d)
                                               (toFFI e)
                                               (toFFI f)
                                               (toFFI g)
                                               (toFFI h)

  export
  new' : JSIO EffectTiming
  new' = primJS
       $ EffectTiming.prim__new undef undef undef undef undef undef undef undef

  export
  delay :  (0 _ : JSType t)
        => {auto 0 _ : Elem EffectTiming (Types t)}
        -> t
        -> Attribute True Optional Double
  delay v = fromUndefOrPrim "EffectTiming.getdelay"
                            prim__delay
                            prim__setDelay
                            0
                            (v :> EffectTiming)

  export
  direction :  (0 _ : JSType t)
            => {auto 0 _ : Elem EffectTiming (Types t)}
            -> t
            -> Attribute False Optional PlaybackDirection
  direction v = fromUndefOrPrimNoDefault "EffectTiming.getdirection"
                                         prim__direction
                                         prim__setDirection
                                         (v :> EffectTiming)

  export
  duration :  (0 _ : JSType t)
           => {auto 0 _ : Elem EffectTiming (Types t)}
           -> t
           -> Attribute False Optional (NS I [ Double , String ])
  duration v = fromUndefOrPrimNoDefault "EffectTiming.getduration"
                                        prim__duration
                                        prim__setDuration
                                        (v :> EffectTiming)

  export
  easing :  (0 _ : JSType t)
         => {auto 0 _ : Elem EffectTiming (Types t)}
         -> t
         -> Attribute True Optional String
  easing v = fromUndefOrPrim "EffectTiming.geteasing"
                             prim__easing
                             prim__setEasing
                             "linear"
                             (v :> EffectTiming)

  export
  endDelay :  (0 _ : JSType t)
           => {auto 0 _ : Elem EffectTiming (Types t)}
           -> t
           -> Attribute True Optional Double
  endDelay v = fromUndefOrPrim "EffectTiming.getendDelay"
                               prim__endDelay
                               prim__setEndDelay
                               0
                               (v :> EffectTiming)

  export
  fill :  (0 _ : JSType t)
       => {auto 0 _ : Elem EffectTiming (Types t)}
       -> t
       -> Attribute False Optional FillMode
  fill v = fromUndefOrPrimNoDefault "EffectTiming.getfill"
                                    prim__fill
                                    prim__setFill
                                    (v :> EffectTiming)

  export
  iterationStart :  (0 _ : JSType t)
                 => {auto 0 _ : Elem EffectTiming (Types t)}
                 -> t
                 -> Attribute True Optional Double
  iterationStart v = fromUndefOrPrim "EffectTiming.getiterationStart"
                                     prim__iterationStart
                                     prim__setIterationStart
                                     0.0
                                     (v :> EffectTiming)

  export
  iterations :  (0 _ : JSType t)
             => {auto 0 _ : Elem EffectTiming (Types t)}
             -> t
             -> Attribute True Optional Double
  iterations v = fromUndefOrPrim "EffectTiming.getiterations"
                                 prim__iterations
                                 prim__setIterations
                                 1.0
                                 (v :> EffectTiming)

namespace KeyframeAnimationOptions

  export
  new : (id : Optional String) -> JSIO KeyframeAnimationOptions
  new a = primJS $ KeyframeAnimationOptions.prim__new (toFFI a)

  export
  new' : JSIO KeyframeAnimationOptions
  new' = primJS $ KeyframeAnimationOptions.prim__new undef

  export
  id :  (0 _ : JSType t)
     => {auto 0 _ : Elem KeyframeAnimationOptions (Types t)}
     -> t
     -> Attribute True Optional String
  id v = fromUndefOrPrim "KeyframeAnimationOptions.getid"
                         prim__id
                         prim__setId
                         ""
                         (v :> KeyframeAnimationOptions)

namespace KeyframeEffectOptions

  export
  new :  (iterationComposite : Optional IterationCompositeOperation)
      -> (composite : Optional CompositeOperation)
      -> JSIO KeyframeEffectOptions
  new a b = primJS $ KeyframeEffectOptions.prim__new (toFFI a) (toFFI b)

  export
  new' : JSIO KeyframeEffectOptions
  new' = primJS $ KeyframeEffectOptions.prim__new undef undef

  export
  composite :  (0 _ : JSType t)
            => {auto 0 _ : Elem KeyframeEffectOptions (Types t)}
            -> t
            -> Attribute False Optional CompositeOperation
  composite v = fromUndefOrPrimNoDefault "KeyframeEffectOptions.getcomposite"
                                         prim__composite
                                         prim__setComposite
                                         (v :> KeyframeEffectOptions)

  export
  iterationComposite :  (0 _ : JSType t)
                     => {auto 0 _ : Elem KeyframeEffectOptions (Types t)}
                     -> t
                     -> Attribute False Optional IterationCompositeOperation
  iterationComposite v = fromUndefOrPrimNoDefault "KeyframeEffectOptions.getiterationComposite"
                                                  prim__iterationComposite
                                                  prim__setIterationComposite
                                                  (v :> KeyframeEffectOptions)

namespace OptionalEffectTiming

  export
  new :  (delay : Optional Double)
      -> (endDelay : Optional Double)
      -> (fill : Optional FillMode)
      -> (iterationStart : Optional Double)
      -> (iterations : Optional Double)
      -> (duration : Optional (NS I [ Double , String ]))
      -> (direction : Optional PlaybackDirection)
      -> (easing : Optional String)
      -> JSIO OptionalEffectTiming
  new a b c d e f g h = primJS
                      $ OptionalEffectTiming.prim__new (toFFI a)
                                                       (toFFI b)
                                                       (toFFI c)
                                                       (toFFI d)
                                                       (toFFI e)
                                                       (toFFI f)
                                                       (toFFI g)
                                                       (toFFI h)

  export
  new' : JSIO OptionalEffectTiming
  new' = primJS
       $ OptionalEffectTiming.prim__new undef
                                        undef
                                        undef
                                        undef
                                        undef
                                        undef
                                        undef
                                        undef

  export
  delay :  (0 _ : JSType t)
        => {auto 0 _ : Elem OptionalEffectTiming (Types t)}
        -> t
        -> Attribute False Optional Double
  delay v = fromUndefOrPrimNoDefault "OptionalEffectTiming.getdelay"
                                     prim__delay
                                     prim__setDelay
                                     (v :> OptionalEffectTiming)

  export
  direction :  (0 _ : JSType t)
            => {auto 0 _ : Elem OptionalEffectTiming (Types t)}
            -> t
            -> Attribute False Optional PlaybackDirection
  direction v = fromUndefOrPrimNoDefault "OptionalEffectTiming.getdirection"
                                         prim__direction
                                         prim__setDirection
                                         (v :> OptionalEffectTiming)

  export
  duration :  (0 _ : JSType t)
           => {auto 0 _ : Elem OptionalEffectTiming (Types t)}
           -> t
           -> Attribute False Optional (NS I [ Double , String ])
  duration v = fromUndefOrPrimNoDefault "OptionalEffectTiming.getduration"
                                        prim__duration
                                        prim__setDuration
                                        (v :> OptionalEffectTiming)

  export
  easing :  (0 _ : JSType t)
         => {auto 0 _ : Elem OptionalEffectTiming (Types t)}
         -> t
         -> Attribute False Optional String
  easing v = fromUndefOrPrimNoDefault "OptionalEffectTiming.geteasing"
                                      prim__easing
                                      prim__setEasing
                                      (v :> OptionalEffectTiming)

  export
  endDelay :  (0 _ : JSType t)
           => {auto 0 _ : Elem OptionalEffectTiming (Types t)}
           -> t
           -> Attribute False Optional Double
  endDelay v = fromUndefOrPrimNoDefault "OptionalEffectTiming.getendDelay"
                                        prim__endDelay
                                        prim__setEndDelay
                                        (v :> OptionalEffectTiming)

  export
  fill :  (0 _ : JSType t)
       => {auto 0 _ : Elem OptionalEffectTiming (Types t)}
       -> t
       -> Attribute False Optional FillMode
  fill v = fromUndefOrPrimNoDefault "OptionalEffectTiming.getfill"
                                    prim__fill
                                    prim__setFill
                                    (v :> OptionalEffectTiming)

  export
  iterationStart :  (0 _ : JSType t)
                 => {auto 0 _ : Elem OptionalEffectTiming (Types t)}
                 -> t
                 -> Attribute False Optional Double
  iterationStart v = fromUndefOrPrimNoDefault "OptionalEffectTiming.getiterationStart"
                                              prim__iterationStart
                                              prim__setIterationStart
                                              (v :> OptionalEffectTiming)

  export
  iterations :  (0 _ : JSType t)
             => {auto 0 _ : Elem OptionalEffectTiming (Types t)}
             -> t
             -> Attribute False Optional Double
  iterations v = fromUndefOrPrimNoDefault "OptionalEffectTiming.getiterations"
                                          prim__iterations
                                          prim__setIterations
                                          (v :> OptionalEffectTiming)


text:
-- f1 : (a:Type) -> (x:a) -> (y:x) -> x
-- f1 a x y = y

hej : (tyOp : List Type -> Type) -> Type
hej tyOp = tyOp [Int, Bool]

hej2 : List Type -> Type
hej2 (t :: ts) = t

test21 : Type
test21 = hej2 [Type]  -- test21 == Type

test22 : Type
test22 = hej2 [Int]   -- test22 == Int

max_stars_repo_name: hjorthjort/IdrisToAgda

max_issues_repo_name: hjorthjort/IdrisToAgda

max_forks_repo_name: hjorthjort/IdrisToAgda


text:
module Control.TransitionIndexed

import public Control.Monad.TransitionIndexed
import public Control.Monad.TransitionIndexed.Do

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
module Compiler.ES.Doc

import Data.List

infixl 8 <++>, <?>

public export
data Doc
  = Nil
  | LineBreak
  | SoftSpace -- this will be ignored in compact printing
  | Text String
  | Nest Nat Doc
  | Seq Doc Doc

export
Semigroup Doc where
  Nil <+> y = y
  x <+> Nil = x
  x <+> y = Seq x y

export
Monoid Doc where
  neutral = Nil

public export %inline
shown : Show a => a -> Doc
shown a = Text (show a)

export
FromString Doc where
  fromString = Text

export
isMultiline : Doc -> Bool
isMultiline []         = False
isMultiline LineBreak  = True
isMultiline SoftSpace  = False
isMultiline (Text x)   = False
isMultiline (Nest k x) = isMultiline x
isMultiline (Seq x y)  = isMultiline x || isMultiline y

export
(<++>) : Doc -> Doc -> Doc
a <++> b = a <+> " " <+> b

export
vcat : List Doc -> Doc
vcat = concat . intersperse LineBreak

export
hcat : List Doc -> Doc
hcat = concat

export
hsep : List Doc -> Doc
hsep = concat . intersperse " "

export
block : Doc -> Doc
block b = concat ["{", Nest 1 (LineBreak <+> b), LineBreak, "}"]

export
paren : Doc -> Doc
paren d = "(" <+> d <+> ")"

export
lambdaArrow : Doc
lambdaArrow = SoftSpace <+> "=>" <+> SoftSpace

export
softComma : Doc
softComma = "," <+> SoftSpace

export
softColon : Doc
softColon = ":" <+> SoftSpace

export
softEq : Doc
softEq = SoftSpace <+> "=" <+> SoftSpace

export
compact : Doc -> String
compact = fastConcat . go
  where go : Doc -> List String
        go Nil        = []
        go LineBreak  = []
        go SoftSpace  = []
        go (Text x)   = [x]
        go (Nest _ y) = go y
        go (Seq x y)  = go x ++ go y

export
pretty : Doc -> String
pretty = fastConcat . go ""
  where nSpaces : Nat -> String
        nSpaces n = fastPack $ replicate n ' '

        go : (spaces : String) -> Doc -> List String
        go _ Nil        = []
        go s LineBreak  = ["\n",s]
        go _ SoftSpace  = [" "]
        go _ (Text x)   = [x]
        go s (Nest x y) = go (s ++ nSpaces x) y
        go s (Seq x y)  = go s x ++ go s y


text:
module Rhone.Canvas.Scene

import Control.MonadRec
import Data.Iterable
import JS
import Rhone.Canvas.Style
import Rhone.Canvas.Shape
import Rhone.Canvas.Transformation
import Web.Html

%default total

public export
data Scene : Type where
  S1 : (fs : List Style) -> (tr : Transformation) -> (shape : Shape) -> Scene
  SM : (fs : List Style) -> (tr : Transformation) -> List Scene -> Scene

--------------------------------------------------------------------------------
--          IO
--------------------------------------------------------------------------------

mutual
  export
  applyAll : CanvasRenderingContext2D -> List Scene -> JSIO ()
  applyAll ctxt = assert_total $ forM_ (apply ctxt)

  export
  apply : CanvasRenderingContext2D -> Scene -> JSIO ()
  apply ctxt (S1 fs tr shape) = do
    save    ctxt
    traverse_ (apply ctxt) fs
    apply   ctxt tr
    apply   ctxt shape
    restore ctxt

  apply ctxt (SM fs tr xs) = do
    save     ctxt
    traverse_ (apply ctxt) fs
    apply    ctxt tr
    applyAll ctxt xs
    restore  ctxt


text:
module Minecraft.Base.PreClassic.GrassBlock.Export

import public Minecraft.Base.PreClassic.GrassBlock.Block.Export
import public Minecraft.Base.PreClassic.GrassBlock.Item.Export
import public Minecraft.Base.PreClassic.GrassBlock.ItemEntity.Export

%default total

max_stars_repo_name: po-stulate/postulate

max_issues_repo_name: po-stulate/postulate

max_forks_repo_name: po-stulate/postulate


text:
import Data.Binary
import Data.Binary.Digit
import Data.Fin
import Data.List
import Data.List1
import Data.Nat
import Data.Vect
import Data.String
import Data.String.Parser

import System.File

Show Digit where
  show I = "1"
  show O = "0"

Algorithm : Type
Algorithm = Vect 512 Bool

Image : Nat -> Type
Image n = Vect n (Vect n Bool)

showImg : Image n -> String
showImg n = fastAppend $ intersperse "\n" $ toList $ (\r => pack $ toList $ (\b => if b then '#' else '.') <$> r) <$> n

Input : Nat -> Type
Input n = (Algorithm, Image n)

pixelParser : Parser Bool
pixelParser = char '.' $> False <|> char '#' $> True

parser : Parser (n ** Input n)
parser = do alg <- ntimes 512 pixelParser
            spaces
            row <- some pixelParser <* char '\n'
            let n = length row
            Just v <- pure $ toVect n row
              | Nothing => fail "not length"
            Yes ItIsSucc <- pure $ isItSucc n
              | No _ => fail "Row is zero"
            vs <- ntimes (pred n) ((ntimes n pixelParser) <* char '\n')
            pure $ MkDPair n (alg, v :: vs)

grow : Bool -> (n : Nat) -> Image n -> Image (4 + n)
grow d n img = let gr = (flip snoc) d . (flip snoc) d . (::) d . (::) d <$> img
                   emptyrow = replicate (4 + n) d in
                   (flip snoc) emptyrow $ (flip snoc) emptyrow $ (::) emptyrow $ (::) emptyrow $ gr

shrink : {n : Nat} -> Image (4 + n) -> Image (2 + n)
shrink = map (init . tail) . init . tail

decFin : Fin n -> Fin (S n)
decFin FZ = FZ
decFin (FS x) = weaken $ weaken x

neighbours : Fin n -> Fin n -> List (Fin (S n), Fin (S n))
neighbours x y = let xs = [ decFin x, weaken x, shift 1 x ]
                     ys = [ decFin y, weaken y, shift 1 y ] in
                     join $ (\y => (,y) <$> xs) <$> ys

getNumber : Image n -> List (Fin n, Fin n) -> Nat
getNumber img l = toNat $ reverse $ (\b => if b then I else O) <$> (\(x, y) => index x $ index y img) <$> l

lookupAlg : Algorithm -> Nat -> Bool
lookupAlg alg n = case natToFin n 512 of
                       Nothing => False
                       (Just i) => index i alg

enhance : {n : Nat} -> Algorithm -> ((k : Nat) -> Image k -> Image (4 + k)) -> Image n -> Image (2 + n)
enhance alg g img = let img' = g n img
                        indices = map (shift 1) $ forget $ allFins (S n)
                        positions = join $ (\x => (x,) <$> indices) <$> indices
                        enhanced = foldl (\i => \(x, y) => let k = getNumber img' $ neighbours x y
                                                               b = lookupAlg alg k in
                                                               updateAt (weaken y) (replaceAt (weaken x) b) i) img' positions in
                        shrink enhanced

enhanceN : {n : Nat} -> Nat -> Algorithm -> (Bool -> (k : Nat) -> Image k -> Image (4 + k)) -> Image n -> (m ** Image m)
enhanceN 0 alg g img = MkDPair n img
enhanceN (S s) alg g img = let en = enhance alg (g ((modNatNZ (S s) 2 SIsNonZero) == 1)) img in enhanceN {n = (S (S n))} s alg g en

countLit : Image n -> Nat
countLit = sum . map (count id)

part1 : {n : Nat} -> Input n -> IO String
part1 (alg, img) = pure $ show $ countLit $ enhance alg (grow True) $ enhance alg (grow False) img

part2 : {n : Nat} -> Input n -> IO String
part2 (alg, img) = let MkDPair _ enn = enhanceN 50 alg grow img in
                       pure $ show $ countLit $ enn

main : IO ()
main = do Right input <- readFile "input.txt"
            | Left err => printLn err
          Right (MkDPair n a, _) <- pure $ parse parser input
            | Left err => printLn err
          part1 a >>= putStrLn
          part2 a >>= putStrLn


text:
module Main

import Language.Reflection

%language ElabReflection

-- A performance test - previously this was slowing down hugely due to
-- quoting back HNFs on >>=, and as the environment gets bigger, the
-- environment of holes gets bigger and bigger, so quoting can start to take
-- far too long
perftest : Elab ()
perftest = do
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 1 . show)) [[the Int 1..10]] -- minor difference
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 2 . show)) [[the Int 1..10]] -- minor difference
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 3 . show)) [[the Int 1..10]] -- minor difference
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 4 . show)) [[the Int 1..10]] -- minor difference
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 5 . show)) [[the Int 1..10]] -- minor difference
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 6 . show)) [[the Int 1..10]] -- minor difference
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 7 . show)) [[the Int 1..10]] -- 0.3s
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 8 . show)) [[the Int 1..10]] -- 0.4s
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 9 . show)) [[the Int 1..10]] -- 0.5s
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 10 . show)) [[the Int 1..10]] -- 1.5s
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 11 . show)) [[the Int 1..10]] -- 4s
  logMsg "" 0 "Progress"
  traverse (traverse (logMsg "" 12 . show)) [[the Int 1..10]] -- 13s
  pure ()

%runElab perftest


text:
import Js.ASync

p : Int -> JS_IO Int
p x = do
  putStrLn' "ola"
  pure $ x + 1

call_fn : (Int -> JS_IO Int) -> Int -> JS_IO Int
call_fn f x =
  jscall
    "%0(%1)"
    ((JsFn (Int -> JS_IO Int)) -> Int -> JS_IO Int)
    (MkJsFn f)
    x

main : JS_IO ()
main = do
  v <- call_fn p 73
  putStrLn' $ show v

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
-- TypeFuns.idr

-- Demonstrates type functions to calculate stuff for either an int or string

StringOrInt : Bool -> Type
StringOrInt False = String
StringOrInt True = Int

||| Returns a String or Int literal, depending on the input
||| parameter.
getStringOrInt : (isInt : Bool) -> StringOrInt isInt
getStringOrInt False = "Ninety four"
getStringOrInt True = 94

||| Converts the given StringOrInt to a (trimmed) String
valToString : (isInt : Bool) -> StringOrInt isInt -> String
valToString False y = trim y
valToString True y = cast y

||| Converts the given StringOrInt to a (trimmed) String
||| Alternative implementation using a case construct
||| in the type signature
valToString2 : (isInt : Bool) -> (case isInt of
                                       False => String
                                       True => Int) -> String
valToString2 False y = trim y
valToString2 True y = cast y

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
> module Sigma.Operations

> import Data.Fin
> import Data.Vect

> import Sigma.Sigma
> import Finite.Predicates
> import Decidable.Predicates
> import Finite.Operations
> import Vect.Operations

> %default total

> %access public export

> |||
> outl : {A : Type} -> {P : A -> Type} -> Sigma A P -> A
> outl (MkSigma a _) = a

> |||
> outr : {A : Type} -> {P : A -> Type} -> (s : Sigma A P) -> P (outl s)
> outr (MkSigma _ p) = p

> ||| Maps a finite type |A| and a decidable predicate |P| to a vector |Sigma A P| values
> toVectSigma : {A : Type} ->
>               {P : A -> Type} ->
>               Finite A ->
>               Dec1 P ->
>               Sigma Nat (\ n => Vect n (Sigma A P))
> toVectSigma fA d1P = filterTagSigma d1P (toVect fA)

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Toolkit.Data.Pair

import Decidable.Equality

%default total

public export
data IsFirst : (this : a) -> (that : Pair a b) -> Type where
  IF : (prf : x = y)
    -> IsFirst x (y,b)

export
isFirst : DecEq type
       => (this : type)
       -> (that : Pair type b)
               -> Dec (IsFirst this that)
isFirst this (x, y) with (decEq this x)
  isFirst this (this, y) | (Yes Refl)
    = Yes (IF Refl)
  isFirst this (x, y) | (No contra)
    = No (\(IF Refl) => contra Refl)

public export
data IsSecond : (this : b) -> (that : Pair a b) -> Type where
  IS : (prf : x = y)
    -> IsSecond x (a,y)

export
isSecond : DecEq type
        => (this : type)
        -> (that : Pair a type)
                -> Dec (IsSecond this that)
isSecond this (x, y) with (decEq this y)
  isSecond this (x, this) | (Yes Refl)
    = Yes (IS Refl)
  isSecond this (x, y) | (No contra)
    = No (\(IS Refl) => contra Refl)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
-- --------------------------------------------------------- [ Interactive.idr ]
-- Module      : Exercises.Test.Interactive
-- Description : Test covering the Chapter 3 exercises in Edwin Brady's
--               book, "Type-Driven Development with Idris."
-- --------------------------------------------------------------------- [ EOH ]
module Exercises.Test.Interactive

import Exercises.Interactive

import Test.Helpers

import Data.Vect
%hide Data.Vect.overLength

%access export

testLength : IO Bool
testLength = "my_length" `assertEqual'` 10 $ my_length [1..10]

testReverse : IO Bool
testReverse = "my_reverse" `assertEqual'` [10,9..1] $ my_reverse [1..10]

testMap : IO Bool
testMap = "my_map" `assertEqual'` [2,4..20] $ my_map (*2) [1..10]

testVectMap : IO Bool
testVectMap =
  "my_vect_map" `assertEqual'` the (Vect _ Nat) [3, 3, 7, 4] $
  my_vect_map length ["Hot", "Dog", "Jumping", "Frog"]

testAddMatrix : (Eq elem, Num elem, Show elem) =>
                (a, b, expected : Vect n (Vect m elem)) ->
                IO Bool
testAddMatrix {n} {m} a b expected =
  unwords ["addMatrix", show n, "x", show m] `assertEqual'` expected $
  addMatrix a b

testMultMatrix : (Eq elem, Num elem, Show elem) =>
                 Vect n (Vect m elem) -> Vect m (Vect p elem) ->
                 Vect n (Vect p elem) ->
                 IO Bool
testMultMatrix {n} {m} {p} a b expected =
  unwords ["multMatrix (", show n, "x", show m, ") (", show m, "x", show p, ")"]
  `assertEqual'` expected $ multMatrix a b

testTransposeMat : (Eq elem, Show elem) =>
                   Vect n (Vect m elem) -> Vect m (Vect n elem) ->
                   IO Bool
testTransposeMat {n} {m} toTranspose expected =
  unwords ["transpose_mat", show n, "x", show m] `assertEqual'` expected $
  transpose_mat toTranspose

allTests : List (IO Bool)
allTests = [ testLength
           , testReverse
           , testMap
           , testVectMap
           , testTransposeMat [ [1, 2,   3,  4],
                                [5, 6,   7,  8],
                                [9, 10, 11, 12] ]
                              [ [1, 5,  9],
                                [2, 6, 10],
                                [3, 7, 11],
                                [4, 8, 12] ]
           , testTransposeMat [ [1, 2],
                                [3, 4],
                                [5, 6] ]
                              [ [1, 3, 5],
                                [2, 4, 6] ]
           , testAddMatrix [ [1, 2],
                             [3, 4] ]
                           [ [5, 6],
                             [7, 8] ]
                           [ [ 6,  8],
                             [10, 12] ]
           , testMultMatrix [ [  1,   2],
                              [  3,   4],
                              [  5,   6] ]
                            [ [  7,   8,   9,  10],
                              [ 11,  12,  13,  14] ]
                            [ [ 29,  32,  35,  38],
                              [ 65,  72,  79,  86],
                              [101, 112, 123, 134] ]
           ]

runTests : IO (Vect (length Interactive.allTests) Bool)
runTests = testChapter "3: Interactive development with types" allTests

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

max_stars_repo_name: yurrriq/tdd-with-idris

max_issues_repo_name: yurrriq/tdd-with-idris

max_forks_repo_name: yurrriq/tdd-with-idris


text:
-- examples in "Type-Driven Development with Idris"
-- chapter 11, section 1

import Data.Primitives.Views

-- check that all functions are total
%default total

data InfList : Type -> Type where
  (::) : (value : elem) -> Inf (InfList elem) -> InfList elem

%name InfList xs, ys, zs

countFrom : Integer -> InfList Integer
countFrom x = x :: Delay (countFrom (x + 1))

getPrefix : (count : Nat) -> InfList ty -> List ty
getPrefix Z xs = []
getPrefix (S k) (value :: xs) = value :: getPrefix k xs

labelWith : Stream labelType -> List a -> List (labelType, a)
labelWith lbs [] = []
labelWith (lbl :: lbls) (val :: vals) = (lbl, val) :: labelWith lbls vals

label : List a -> List (Integer, a)
label = labelWith (iterate (+1) 0)

randoms : Int -> Stream Int
randoms seed = let seed' = 1664525 * seed + 1013904223 in
                (seed' `shiftR` 2) :: randoms seed'

arithInputs : Int -> Stream Int
arithInputs seed = map bound (randoms seed)
  where
    bound : Int -> Int
    bound num with (divides num 12)
      bound ((12 * div) + rem) | (DivBy prf) = rem + 1

partial
quiz : Stream Int -> (score : Nat) -> IO ()
quiz  (num1 :: num2 :: nums) score
  = do putStrLn ("Score so far:" ++ show score)
       putStr (show num1 ++ " * " ++ show num2 ++ "? ")
       answer <- getLine
       if cast answer == num1 * num2
         then do putStrLn "Correct!"
                 quiz nums (score + 1)
         else do putStrLn ("Wrong, the answer is " ++ show (num1 * num2))
                 quiz nums score

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Web.Raw.Permissions

import JS
import Web.Internal.PermissionsPrim
import Web.Internal.Types

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

namespace PermissionStatus

  export
  onchange : PermissionStatus -> Attribute False Maybe EventHandlerNonNull
  onchange v = fromNullablePrim "PermissionStatus.getonchange"
                                prim__onchange
                                prim__setOnchange
                                v

  export
  state : (obj : PermissionStatus) -> JSIO PermissionState
  state a = tryJS "PermissionStatus.state" $ PermissionStatus.prim__state a

namespace Permissions

  export
  query :  (0 _ : JSType t1)
        => {auto 0 _ : Elem Object (Types t1)}
        -> (obj : Permissions)
        -> (permissionDesc : t1)
        -> JSIO (Promise PermissionStatus)
  query a b = primJS $ Permissions.prim__query a (up b)

--------------------------------------------------------------------------------
--          Dictionaries
--------------------------------------------------------------------------------

namespace CameraDevicePermissionDescriptor

  export
  new : (panTiltZoom : Optional Bool) -> JSIO CameraDevicePermissionDescriptor
  new a = primJS $ CameraDevicePermissionDescriptor.prim__new (toFFI a)

  export
  new' : JSIO CameraDevicePermissionDescriptor
  new' = primJS $ CameraDevicePermissionDescriptor.prim__new undef

  export
  panTiltZoom :  (0 _ : JSType t)
              => {auto 0 _ : Elem CameraDevicePermissionDescriptor (Types t)}
              -> t
              -> Attribute True Optional Bool
  panTiltZoom v = fromUndefOrPrim "CameraDevicePermissionDescriptor.getpanTiltZoom"
                                  prim__panTiltZoom
                                  prim__setPanTiltZoom
                                  False
                                  (v :> CameraDevicePermissionDescriptor)

namespace DevicePermissionDescriptor

  export
  new : (deviceId : Optional String) -> JSIO DevicePermissionDescriptor
  new a = primJS $ DevicePermissionDescriptor.prim__new (toFFI a)

  export
  new' : JSIO DevicePermissionDescriptor
  new' = primJS $ DevicePermissionDescriptor.prim__new undef

  export
  deviceId :  (0 _ : JSType t)
           => {auto 0 _ : Elem DevicePermissionDescriptor (Types t)}
           -> t
           -> Attribute False Optional String
  deviceId v = fromUndefOrPrimNoDefault "DevicePermissionDescriptor.getdeviceId"
                                        prim__deviceId
                                        prim__setDeviceId
                                        (v :> DevicePermissionDescriptor)

namespace MidiPermissionDescriptor

  export
  new : (sysex : Optional Bool) -> JSIO MidiPermissionDescriptor
  new a = primJS $ MidiPermissionDescriptor.prim__new (toFFI a)

  export
  new' : JSIO MidiPermissionDescriptor
  new' = primJS $ MidiPermissionDescriptor.prim__new undef

  export
  sysex :  (0 _ : JSType t)
        => {auto 0 _ : Elem MidiPermissionDescriptor (Types t)}
        -> t
        -> Attribute True Optional Bool
  sysex v = fromUndefOrPrim "MidiPermissionDescriptor.getsysex"
                            prim__sysex
                            prim__setSysex
                            False
                            (v :> MidiPermissionDescriptor)

namespace PermissionDescriptor

  export
  new : (name : PermissionName) -> JSIO PermissionDescriptor
  new a = primJS $ PermissionDescriptor.prim__new (toFFI a)

  export
  name :  (0 _ : JSType t)
       => {auto 0 _ : Elem PermissionDescriptor (Types t)}
       -> t
       -> Attribute True I PermissionName
  name v = fromPrim "PermissionDescriptor.getname"
                    prim__name
                    prim__setName
                    (v :> PermissionDescriptor)

namespace PermissionSetParameters

  export
  new :  (0 _ : JSType t1)
      => {auto 0 _ : Elem PermissionDescriptor (Types t1)}
      -> (descriptor : t1)
      -> (state : PermissionState)
      -> (oneRealm : Optional Bool)
      -> JSIO PermissionSetParameters
  new a b c = primJS
            $ PermissionSetParameters.prim__new (up a) (toFFI b) (toFFI c)

  export
  new' :  (0 _ : JSType t1)
       => {auto 0 _ : Elem PermissionDescriptor (Types t1)}
       -> (descriptor : t1)
       -> (state : PermissionState)
       -> JSIO PermissionSetParameters
  new' a b = primJS $ PermissionSetParameters.prim__new (up a) (toFFI b) undef

  export
  descriptor :  (0 _ : JSType t)
             => {auto 0 _ : Elem PermissionSetParameters (Types t)}
             -> t
             -> Attribute True I PermissionDescriptor
  descriptor v = fromPrim "PermissionSetParameters.getdescriptor"
                          prim__descriptor
                          prim__setDescriptor
                          (v :> PermissionSetParameters)

  export
  oneRealm :  (0 _ : JSType t)
           => {auto 0 _ : Elem PermissionSetParameters (Types t)}
           -> t
           -> Attribute True Optional Bool
  oneRealm v = fromUndefOrPrim "PermissionSetParameters.getoneRealm"
                               prim__oneRealm
                               prim__setOneRealm
                               False
                               (v :> PermissionSetParameters)

  export
  state :  (0 _ : JSType t)
        => {auto 0 _ : Elem PermissionSetParameters (Types t)}
        -> t
        -> Attribute True I PermissionState
  state v = fromPrim "PermissionSetParameters.getstate"
                     prim__state
                     prim__setState
                     (v :> PermissionSetParameters)

namespace PushPermissionDescriptor

  export
  new : (userVisibleOnly : Optional Bool) -> JSIO PushPermissionDescriptor
  new a = primJS $ PushPermissionDescriptor.prim__new (toFFI a)

  export
  new' : JSIO PushPermissionDescriptor
  new' = primJS $ PushPermissionDescriptor.prim__new undef

  export
  userVisibleOnly :  (0 _ : JSType t)
                  => {auto 0 _ : Elem PushPermissionDescriptor (Types t)}
                  -> t
                  -> Attribute True Optional Bool
  userVisibleOnly v = fromUndefOrPrim "PushPermissionDescriptor.getuserVisibleOnly"
                                      prim__userVisibleOnly
                                      prim__setUserVisibleOnly
                                      False
                                      (v :> PushPermissionDescriptor)


text:
module Main

import Data.Vect

Relation : (tys : Vect arity Type) -> Type
Relation [] = Type
Relation (ty :: tys) = ty -> Relation tys

RelationOn : (ty : Type) -> (arity : Nat) -> Type
RelationOn ty arity = Relation $ replicate arity ty

data Chan : (a : Type) -> Type where
     MkChan : (ty0 : Type) -> (ty1 : Type) -> Chan (Relation [ty0, ty1])

data Cat : Type where
     MkCat : {o : Type} ->
             {a : Type} ->
             ((Relation [a, o]), (Relation [a, o]), (Relation [o, a]), (Relation [(a,a), o])) -> Cat

     MkCat2 : {o : Type} ->
              {a : Type} ->
              (a -> o, a -> o, a -> a, (a, a) -> o) -> Cat

add : Int -> Int
add x = x + 1


text:
module Door

public export
data Usage = Once | Many

public export
data Lin : (Type -> Type) -> Usage -> Type -> Type where
     Pure : (1 x :   a) -> Lin m u a
     Lift : (1 x : m a) -> Lin m Many a
     BindOnce : (1 act : Lin m Once a) ->
                (1 k : (1 x : a) -> Lin m t b) -> Lin m t b
     BindMany : (1 act : Lin m Many a) ->
                (1 k : (x : a) -> Lin m t b) -> Lin m t b

public export
data Unrestricted : Type -> Type where
     MkUn : (x : a) -> Unrestricted a

export
pure : (1 x : a) -> Lin m u a
pure = Pure

export
lift : (1 x : m a) -> Lin m Many a
lift = Lift

public export
contType : (Type -> Type) -> Usage -> Usage -> Type -> Type -> Type
contType m Once q a b = (1 x : a) -> Lin m q b
contType m Many q a b = (x : a) -> Lin m q b

public export
(>>=) : {p : _}
     -> (1 f : Lin m p a)
     -> (1 k : contType m p q a b)
     -> Lin m q b
(>>=) {p=Once} = BindOnce
(>>=) {p=Many} = BindMany

export
run : Monad m => Lin m u t -> m t
run (Pure x) = pure x
run (Lift p) = p
run (BindOnce act k)
    = do act' <- run act
         run (k act')
run (BindMany act k)
    = do act' <- run act
         run (k act')

public export
One : (Type -> Type) -> Type -> Type
One m = Lin m Once

public export
Any : (Type -> Type) -> Type -> Type
Any m = Lin m Many

data DoorState = Closed | Open

-- changes start here

openWhen : Bool -> DoorState
openWhen ok = if ok then Open else Closed

data Door : DoorState -> Type where
  MkDoor : (isOpen : Bool) -> Door (if isOpen then Open else Closed)

-- Testing that 'if' works okay in an interface
interface Doored (m : Type -> Type) where
    newDoor    : One m (Door Closed)
    knock      : (1 d : Door t)      -> One m (Door t)
    openDoor   : (1 d : Door Closed)
             ->  One m (Res Bool (\ok => Door (if ok then Open else Closed)))
    closeDoor  : (1 d : Door Open)   -> One m (Door Closed)
    deleteDoor : (1 d : Door Closed) -> Any m ()


text:
module Unlambda

import Control.Monad.Trans
import src.ContT

-- Based on http://www.madore.org/~david/programs/unlambda/

data Rec : (r : Type) -> (m : Type -> Type) -> Type where
  RecK : (Rec r m -> ContT r m (Rec r m)) -> Rec r m

data Expr : Type where
  S : Expr
  K : Expr
  I : Expr
  R : Expr
  C : Expr
  Dot : Char -> Expr
  Backtick : Expr -> Expr -> Expr

apply : ContT r m (Rec r m) -> ContT r m (Rec r m) -> ContT r m (Rec r m)
apply first second = do (RecK k) <- first
                        b <- second
                        k b

eval : Monad m => Expr -> (Char -> m ()) -> ContT r m (Rec r m)
eval S put = pure $ RecK (\rec =>
             pure $ RecK (\rec' =>
             pure $ RecK (\rec'' => apply (apply (pure rec) (pure rec'')) (apply (pure rec') (pure rec'')))))
eval K put = pure $ RecK (\rec => pure $ RecK (\_ => pure rec))
eval I put = pure $ RecK (\rec => pure rec)
eval R put = pure $ RecK (\rec => do lift $ put '\n'; pure rec)
eval C put = pure $ RecK (\(RecK k) => callCC (\k' => k $ RecK k'))
eval (Dot char) put = pure $ RecK (\rec => do lift $ put char; pure rec)
eval (Backtick expr expr') put = apply (eval expr put) (eval expr' put)

parse :  List Char -> Maybe (Expr, List Char)
parse ('s' :: xs) = Just (S, xs)
parse ('k' :: xs) = Just (K, xs)
parse ('i' :: xs) = Just (I, xs)
parse ('r' :: xs) = Just (R, xs)
parse ('c' :: xs) = Just (C, xs)
parse ('.' :: c :: xs) = Just (Dot c, xs)
parse ('`' :: xs) = do (expr, xs') <- parse xs
                       (expr', xs'') <- parse xs'
                       Just (Backtick expr expr', xs'')
parse (x :: xs) = Nothing
parse [] = Nothing

callCCTest : String
callCCTest = "``cir"

helloWorldTest : String
helloWorldTest = "```si`k``s.H``s.e``s.l``s.l``s.o``s. ``s.w``s.o``s.r``s.l``s.d``s.!``sri``si``si``si``si``si``si``si``si`ki"

example : IO ()
example = case parse (unpack helloWorldTest) of
            Just (expr, _) => run (\_ => pure ()) $ eval expr putChar
            Nothing => putStrLn "Parse error"

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
> module Double.Properties

> import Data.So

> import Double.Predicates
> import Double.Postulates
> import Double.Operations
> import So.Properties
> import Ordering.Properties
> import Rel.TotalPreorder
> import So.Properties
> import Interfaces.Math

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

* Implementations

> implementation Math Double where
>   exp = Prelude.Doubles.exp
>   sin = Prelude.Doubles.sin
>   cos = Prelude.Doubles.cos

* Decidability of EQ

> |||
> decEQ : (x : Double) -> (y : Double) -> Dec (x `EQ` y)
> decEQ x y with (decSo (x == y))
>   | Yes p = Yes (MkEQ p)
>   | No contra = No (\ (MkEQ p) => contra p)

* Properties of Ord methods

> |||
> LTinLTE : {x, y : Double} -> So (x < y) -> So (x <= y)
> LTinLTE {x} {y} prf = soOrIntro1 (x < y) (x == y) prf
> -- LTinLTE : {x, y : Double} -> x `LT` y -> x `LTE` y
> -- LTinLTE {x} {y} (MkLT prf) = MkLTE (soOrIntro1 (x < y) (x == y) prf)

> |||
> EQinLTE : {x, y : Double} -> So (x == y) -> So (x <= y)
> EQinLTE {x} {y} prf = soOrIntro2 (x < y) (x == y) prf

> |||
> compareLT : {x, y : Double} -> LT = compare x y -> So (x < y)
> compareLT {x} {y} p with (compare x y)
>   compareLT {x} {y} _ | LT = Oh
>   compareLT {x} {y} p | EQ = absurd p
>   compareLT {x} {y} p | GT = absurd p

> compareEQ : {x, y : Double} -> EQ = compare x y -> So (x == y)
> compareEQ {x} {y} p with (compare x y) proof prf
>   | LT = absurd p
>   | EQ with (decSo (x == y))
>     | (Yes q) = q
>     | (No  c) = void (notCompareEQ c prf)
>   | GT = absurd p

> compareEQ' : {x, y : Double} -> So (x == y) -> compare x y = EQ
> compareEQ' {x} {y} p with (x == y) proof q
>   | True  = Refl
>   | False = absurd p

> |||
> compareGT : {x, y : Double} -> GT = compare x y -> So (x > y)
> compareGT {x} {y} p with (compare x y)
>   compareGT {x} {y} p | LT = absurd p
>   compareGT {x} {y} p | EQ = absurd p
>   compareGT {x} {y} _ | GT = Oh

* LT, LTE:

> ||| LTE is total
> totalLTE : (x, y : Double) -> Either (x `LTE` y) (y `LTE` x)
> totalLTE x y with (compare x y) proof prf
>   | LT = Left  (MkLTE (LTinLTE (compareLT prf)))
>   | EQ = Left  (MkLTE (EQinLTE (compareEQ prf)))
>   | GT = Right (MkLTE (LTinLTE (gtLT (compareGT prf))))

> ||| LTE is a total preorder
> totalPreorderLTE : TotalPreorder Double.Predicates.LTE
> totalPreorderLTE = MkTotalPreorder LTE reflexiveLTE transitiveLTE totalLTE

> ||| LT is decidable
> decLT : (x : Double) -> (y : Double) -> Dec (x `LT` y)
> decLT x y with (decSo (x < y))
>   | Yes prf    = Yes (MkLT prf)
>   |  No contra =  No (\ (MkLT prf) => void (contra prf))

> ||| LTE is decidable
> decLTE : (x : Double) -> (y : Double) -> Dec (x `LTE` y)
> decLTE x y with (decSo (x <= y))
>   | Yes prf    = Yes (MkLTE prf)
>   |  No contra =  No (\ (MkLTE prf) => void (contra prf))

> |||
> minusLTELemma : (x : Double) -> (y : Double) ->
>                 x `LTE` y -> 0.0 `LTE` y - x
> minusLTELemma x y xLTEy = s2 where
>   s1 : x - x `LTE` y - x
>   s1 = monotoneMinusConstLTE xLTEy
>   s2 : 0.0 `LTE` y - x
>   s2 = replace {P = \ X => X `LTE` y - x} (minusSelfZero) s1

> |||
> divLTELemma : (x : Double) -> (y : Double) -> x `LTE` y ->
>               Positive y -> x / y `LTE` 1.0
> divLTELemma x y xLTEy py = s2 where
>   s1 : x / y `LTE` y / y
>   s1 = monotoneDivConstLTE xLTEy py
>   s2 : x / y `LTE` 1.0
>   s2 = replace {P = \ X => x / y `LTE` X} (divPositiveSelfOne py) s1

> |||
> divNonNegativePositiveNonNegative : (x : Double) -> (y : Double) ->
>                                     0.0 `LTE` x -> Positive y ->
>                                     0.0 `LTE` x / y
> divNonNegativePositiveNonNegative x y zLTEx py = s2 where
>   s1 : 0.0 / y `LTE` x / y
>   s1 = monotoneDivConstLTE zLTEx py
>   s2 : 0.0 `LTE` x / y
>   s2 = replace {P = \ X => X `LTE` x / y} (divZeroPositiveZero py) s1

> ||| |sum| is monotone
> monotoneSum : {A : Type} ->
>               (f : A -> Double) -> (g : A -> Double) ->
>               (p : (a : A) -> f a `LTE` g a) ->
>               (as : List A) ->
>               sum (map f as) `LTE` sum (map g as)
> monotoneSum f g p Nil = reflexiveLTE 0.0
> monotoneSum f g p (a :: as) =
>   monotonePlusLTE {a = f a} {b = g a} {c = sum (map f as)} {d = sum (map g as)} (p a) (monotoneSum f g p as)

* Non-negative double precision floating point numbers:

> ||| Non-negative |Double|s are closed w.r.t. sum
> plusPreservesNonNegativity : {x, y : Double} ->
>                              NonNegative x -> NonNegative y -> NonNegative (x + y)
> plusPreservesNonNegativity {x} {y} zeroLTEx zeroLTEy = s2 where
>   s1 : 0.0 + 0.0 `LTE` x + y
>   s1 = monotonePlusLTE {a = 0.0} {b = x} {c = 0.0} {d = y} zeroLTEx zeroLTEy
>   s2 : 0.0 `LTE` x + y
>   s2 = replace {P = \ X => X `LTE` x + y} plusZeroLeftNeutral s1

> ||| Non-negative |Double|s are closed w.r.t. multiplication
> multPreservesNonNegativity : {x, y : Double} ->
>                              NonNegative x -> NonNegative y -> NonNegative (x * y)
> multPreservesNonNegativity {x} {y} zeroLTEx zeroLTEy = s2 where
>   s1 : 0.0 * 0.0 `LTE` x * y
>   s1 = monotoneMultLTE {a = 0.0} {b = x} {c = 0.0} {d = y} zeroLTEx zeroLTEy
>   s2 : 0.0 `LTE` x * y
>   s2 = replace {P = \ X => X `LTE` x * y} (multZeroLeftZero {x = 0.0}) s1

* Positive double precision floating point numbers:

> |||
> positiveImpliesNonNegative : {x : Double} -> Positive x -> NonNegative x
> positiveImpliesNonNegative (MkLT prf) = MkLTE (LTinLTE prf)

* Properties of constants:

> ||| one is not zero
> notOneEqZero : Not (1.0 = 0.0)
> notOneEqZero Refl impossible

> ||| zero is not positive
> notPositiveZero : Not (Positive 0.0)
> notPositiveZero (MkLT prf) = contra Refl prf

* Properties of |fromNat|

> |||
> fromNatNonNegative : {n : Nat} -> NonNegative (fromNat n)
> fromNatNonNegative {n = Z}   = MkLTE Oh
> fromNatNonNegative {n = S m} = plusPreservesNonNegativity (MkLTE Oh) fromNatNonNegative

> |||
> fromSuccPositive : {n : Nat} -> Positive (fromNat (S n))
> fromSuccPositive {n} = positivePlusAnyPositive (MkLT Oh) fromNatNonNegative

* Convexity

> |||
> convexLemma1 : (x1 : Double) -> (x2 : Double) -> Positive (x2 - x1) ->
>                (x : Double) -> (q : x1 `LTE` x) ->
>                0.0 `LTE` (x - x1) / (x2 - x1)
> convexLemma1 x1 x2 px2mx1 x x1LTEx =
>   divNonNegativePositiveNonNegative (x - x1) (x2 - x1) s1 px2mx1 where
>     s1 : 0.0 `LTE` (x - x1)
>     s1 = minusLTELemma x1 x x1LTEx

> |||
> convexLemma2 : (x1 : Double) -> (x2 : Double) -> Positive (x2 - x1) ->
>                (x : Double) -> (q : x `LTE` x2) ->
>                (x - x1) / (x2 - x1) `LTE` 1.0
> convexLemma2 x1 x2 px2mx1 x q = divLTELemma (x - x1) (x2 - x1) s1 px2mx1 where
>   s1 : (x - x1) `LTE` (x2 - x1)
>   s1 = monotoneMinusConstLTE q

> |||
> convexLemma : (x1 : Double) -> (x2 : Double) -> (alpha : Double) ->
>               NonNegative x1 -> NonNegative x2 ->
>               0.0 `LTE` alpha -> alpha `LTE` 1.0 ->
>               NonNegative (x1 * (1.0 - alpha) + x2 * alpha)
> convexLemma x1 x2 alpha nnx1 nnx2 (MkLTE p1) (MkLTE p2) = s4 where
>   s1 : NonNegative alpha
>   s1 = MkLTE p1
>   s2 : alpha - alpha `LTE` 1.0 - alpha
>   s2 = monotoneMinusConstLTE (MkLTE p2)
>   s3 : NonNegative (1.0 - alpha)
>   s3 = replace {P = \ X => X `LTE` 1.0 - alpha} minusSelfZero s2
>   s4 : NonNegative (x1 * (1.0 - alpha) + x2 * alpha)
>   s4 = plusPreservesNonNegativity {x = x1 * (1.0 - alpha)} {y = x2 * alpha}
>                                   (multPreservesNonNegativity nnx1 s3)
>                                   (multPreservesNonNegativity nnx2 s1)

* Properties of |mkLinearStepLemma|:

> |||
> mkLinearStepLemma : (x1 : Double) -> (x2 : Double) -> Positive (x2 - x1) ->
>                     (y1 : Double) -> (y2 : Double) ->
>                     NonNegative y1 -> NonNegative y2 ->
>                     (x : Double) -> NonNegative (mkLinearStep x1 x2 prf y1 y2 x)
> mkLinearStepLemma x1 x2 px2mx1 y1 y2 nny1 nny2 x with (decSo (x < x1))
>   | Yes _ = nny1
>   | No  _ with (decSo (x1 <= x && x <= x2))
>     | Yes prf = s3 where
>         alpha : Double
>         alpha = (x - x1) / (x2 - x1)
>         s1 : 0.0 `LTE` alpha
>         s1 = convexLemma1 x1 x2 px2mx1 x (MkLTE (soAndElim1 (x1 <= x) (x <= x2) prf))
>         s2 : alpha `LTE` 1.0
>         s2 = convexLemma2 x1 x2 px2mx1 x (MkLTE (soAndElim2 (x1 <= x) (x <= x2) prf))
>         s3 : NonNegative (y1 * (1.0 - alpha) + y2 * alpha)
>         s3 = convexLemma y1 y2 alpha nny1 nny2 s1 s2
>     | No _ = nny2

> {-

> ---}


text:
module Specifications.Semigroup

import public Common.Abbrev

%default total
%access public export

infixl 8 #

||| specification
isAssociative : Binop s -> Type
isAssociative (#) = (x,y,z : _) -> x # (y # z) = (x # y) # z

||| specification
isAbelian : Binop s -> Type
isAbelian (#) = (x,y : _) -> x # y = y # x

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Main

main : IO ()
main = putStrLn "Hello, Idris World!"

max_stars_repo_name: jeremy-miller/type-driven-development

max_issues_repo_name: jeremy-miller/type-driven-development

max_forks_repo_name: jeremy-miller/type-driven-development


text:
module Main

import Data.Primitives.Views
import System

%default total

data InfIO : Type where
  Do : IO a -> (a -> Inf InfIO) -> InfIO

(>>=) : IO a -> (a -> Inf InfIO) -> InfIO
(>>=) = Do

data Fuel = Dry | More (Lazy Fuel)

tank : Nat -> Fuel
tank Z = Dry
tank (S n) = More (tank n)

run : Fuel -> InfIO -> IO ()
run Dry _ = putStrLn "Out of fuel."
run (More fuel) (Do action cont) = do
  res <- action
  run fuel (cont res)

totalREPL : (prompt : String) -> (action : String -> String) -> InfIO
totalREPL prompt action = do
  putStr prompt
  line <- getLine
  putStrLn (action line)
  totalREPL prompt action

partial
forever : Fuel
forever = More forever

partial
main : IO ()
main = run forever (totalREPL "\n: " toUpper)

max_stars_repo_name: luc-tielen/idris-grin

max_issues_repo_name: luc-tielen/idris-grin

max_forks_repo_name: luc-tielen/idris-grin


text:
module Basic.Types.Qubit

import Data.Complex
import Data.Vect
import Effects
import Effect.Random
import Utils.Accomodation
import Utils.ComplexAddon

%default total
%access public export

record QuantumState a where
  constructor QS
  amplitude : Complex a
  label : String

%name QuantumState qs, qs1, qs2, qs3
implementation (Num a, Neg a, Show a, Eq a, Ord a)
                  => Show (QuantumState a) where
  show (QS amplitude label) = complexShow amplitude ++ "|" ++ label ++ ">" where
    complexShow : Complex a -> String
    complexShow (x :+ y) =
      if x == x + x
         then imShow y
         else if y <= y + y
                 then show x ++ "+" ++ imShow y
                 else show x ++ imShow y where
                      imShow : a -> String
                      imShow y =
                        if y > y + y
                           then "-" ++ imPosShow (negate y)
                           else imPosShow y where
                                imPosShow : (y : a) ->  String
                                imPosShow y = if y /= y + y
                                                 then if y * y == y
                                                         then "i"
                                                         else show y ++ "i"
                                                 else "0"

qMap : (f : Complex a -> Complex b) -> QuantumState a -> QuantumState b
qMap f (QS amplitude label) = QS (f amplitude) label

implementation Eq a => Eq (QuantumState a) where
  (QS amplitude1 label1) == (QS amplitude2 label2) =
    (amplitude1 == amplitude2) && (label1 == label2)
implementation [vectorization] Eq a => Ord (QuantumState a) where
  compare (QS amplitude1 label1) (QS amplitude2 label2) = compare label1 label2

qPredicate : (p : Complex a -> Bool) -> QuantumState a -> Bool
qPredicate p (QS amplitude label) = p amplitude

conjugateQS : Neg a => QuantumState a -> QuantumState a
conjugateQS = qMap conjugate

record Qubit a where
  constructor QB
  states : List (QuantumState a)
%name Qubit qb, qb1, qb2, qb3
partial
implementation (Num a, Neg a, Show a, Eq a, Ord a)
                => Show (Qubit a) where
  show (QB [])                  = ""
  show (QB (x :: []))           = show x
  show (QB (x :: qb@(y :: xs))) = show x ++ " + "
    ++ show (QB qb)

toAmplList : Qubit a -> List (Complex a)
toAmplList (QB states) = map amplitude states

toLabelList : Qubit a -> List String
toLabelList (QB states) = map label states

fromList : List (Complex a) -> List String -> Qubit a
fromList xs ys = QB (zipWith QS xs ys)

refine : Ord a => Qubit a -> List (QuantumState a)
refine (QB states) = sort @{vectorization} states

toFineList : Eq a => Qubit a -> List (Complex a)
toFineList (QB states) = map amplitude (sort @{vectorization} states)

fromFineList : List (Complex a) -> Qubit a
fromFineList xs = QB (zipWith QS xs (accomod "01" (degree (length xs) 2)))

liftQubit : (f : List (QuantumState a) -> List (QuantumState b))
              -> Qubit a -> Qubit b
liftQubit f (QB states) = QB (f states)

infix 2 <~>
(<~>) : Neg a => QuantumState a -> QuantumState a -> QuantumState a
(QS amplitude1 label1) <~> (QS amplitude2 label2) =
  QS (amplitude1 * amplitude2) (label1 ++ label2)

entangle : Neg a => Qubit a -> Qubit a -> Qubit a
entangle (QB states1) (QB states2) = QB [|states1 <~> states2|]

conjugateQubit : Neg a => Qubit a -> Qubit a
conjugateQubit = liftQubit (map conjugateQS)

scalarProduct : (Neg a, Eq a) => Qubit a -> Qubit a -> a
scalarProduct qb1 qb2 = realPart
                        (sum
                          (Prelude.List.zipWith (*)
                                                (toFineList qb1)
                                                (toFineList qb2)))

norm : (Cast a Double, Cast Double a, Neg a, Eq a) => Qubit a -> a
norm qb = (cast . sqrt . cast) (scalarProduct qb (conjugateQubit qb))

normalize : (Cast a Double, Cast Double a, Neg a, Eq a, Fractional a) =>
            Qubit a -> Qubit a
normalize qb = liftQubit ((map . qMap)
             (cast .
             (\x => x / (((sqrt . cast)
                          (scalarProduct qb (conjugateQubit qb))):+0)) .
             cast)) qb

extract : (Cast a Double, Cast Double a, Neg a, Eq a) =>
          Qubit a -> Eff String [RND]
extract qb = helper (map cast (toAmplList qb)) (toLabelList qb) where
  helper : List (Complex Double) -> List String-> Eff String [RND]
  helper ampl labels = help (part 0 ampl) labels where
    part : Double -> List (Complex Double) -> List Double
    part prev [] = []
    part prev ((x :+ y) :: xs) = curr :: part curr xs where
      curr : Double
      curr = prev + x * x + y * y
    help : List Double -> List String -> Eff String [RND]
    help [] _            = pure "Nothing"
    help ds@(x :: xs) ys =
      do rand <- assert_total (rndInt 0 (transmute (last ds)))
         findAns (zip (map transmute ds) ys) rand
      where
        transmute : Double -> Integer
        transmute x = cast (1000000000 * x)
        findAns : List (Integer, String) -> Integer -> Eff String [RND]
        findAns [] _                 = pure "Nothing"
        findAns ((p, label) :: xs) r = case p < r of
                                            False => findAns xs r
                                            True  => pure label

qubitZero : Qubit Double
qubitZero = QB ([(QS (1 :+ 0) "0"),
                (QS (0 :+ 0) "1")])

qubitOne : Qubit Double
qubitOne = QB ([(QS (0 :+ 0) "0"),
                (QS (1 :+ 0) "1")])

qubitPlus : Qubit Double
qubitPlus = QB ([(QS ((1 / sqrt 2) :+ 0) "0"),
                 (QS ((1 / sqrt 2) :+ 0) "1")])

qubitMinus : Qubit Double
qubitMinus = QB ([(QS ((1    / sqrt 2) :+ 0) "0"),
                  (QS (((-1) / sqrt 2) :+ 0) "1")])

qubitPhiPlus : Qubit Double
qubitPhiPlus = QB ([(QS ((1 / sqrt 2) :+ 0) "00"),
                    (QS ((1 / sqrt 2) :+ 0) "11")])

qubitPhiMinus : Qubit Double
qubitPhiMinus = QB ([(QS ((1    / sqrt 2) :+ 0) "00"),
                     (QS (((-1) / sqrt 2) :+ 0) "11")])

qubitPsiPlus : Qubit Double
qubitPsiPlus = QB ([(QS ((1 / sqrt 2) :+ 0) "01"),
                    (QS ((1 / sqrt 2) :+ 0) "10")])

qubitPsiMinus : Qubit Double
qubitPsiMinus = QB ([(QS ((1    / sqrt 2) :+ 0) "01"),
                     (QS (((-1) / sqrt 2) :+ 0) "10")])

max_stars_repo_name: GrandArchTemplar/QuantumProgramming

max_issues_repo_name: GrandArchTemplar/QuantumProgramming

max_forks_repo_name: GrandArchTemplar/QuantumProgramming


text:
module Order

data InclusiveEither : (typeLeft : Type) -> (typRight : Type) -> Type where
	OnlyLeft : typLeft -> Not typRight -> InclusiveEither typLeft typRight
	OnlyRight : Not typLeft -> typRight -> InclusiveEither typLeft typRight
	Both : typLeft -> typRight -> InclusiveEither typLeft typRight

|||Type of proof that a relation is reflexive
isReflexive : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isReflexive {typ} r = (a : typ) -> (r a a)

|||Type of proof that a relation is symmetric
isSymmetric : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isSymmetric {typ} r = (a : typ) -> (b : typ) -> (r a b) -> (r b a)

|||Type of proof that a relation is anti-symmetric
isAntiSymmetric : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isAntiSymmetric {typ} r = (a : typ) -> (b : typ) -> (r a b) -> (r b a) -> (a = b)

|||Type of proof that a relation is transitive
isTransitive : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isTransitive {typ} r = (a : typ) -> (b : typ) -> (c : typ) -> (r a b) -> (r b c) -> (r a c)

|||Type of proof that a relation is an equivalence
isEquivalence : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isEquivalence {typ} r = (isReflexive r, isSymmetric r, isTransitive r)

|||Type of proof that a relation is a partial order
isPartialOrder : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isPartialOrder {typ} r = (isReflexive r, isAntiSymmetric r, isTransitive r)

|||Type of proof that a relation is a total order
isTotalOrder : {typ : Type} -> (r : (typ -> typ -> Type)) -> Type
isTotalOrder {typ} r = (isPartialOrder r, (a : typ) -> (b : typ) -> (InclusiveEither (r a b) (r b a)))


text:
import Common

-- the `many` isomorphism: roughly List a <-> List b, constructed with
-- a retraction Maybe a < List b which satisfies a couple of simple
-- and necessary additional restrictions:
-- 1. (x:a) -> (all (isNothing . r) $ prefixes $ f (Just x) = True)
-- 2. (l:List b) -> isJust (r l) = True -> (f (r l)) = l

snoc : (x : a) -> List a -> List a
snoc x [] = [x]
snoc x (y :: xs) = (y :: snoc x xs)

reverse' : List a -> List a
reverse' [] = []
reverse' (x :: xs) = (snoc x (reverse' xs))

suffixes : List a -> List (List a)
suffixes [] = []
suffixes (x::xs) = xs :: suffixes xs

prefixes : List a -> List (List a)
prefixes = (map reverse') . suffixes . reverse'

all' : (a -> Bool) -> List a -> Bool
all' p [] = True
all' p (x::xs) = p x && all' p xs

data MRetraction : (a : Type) -> (b : Type) -> (f : Maybe a -> List b) -> (r : List b -> Maybe a) -> Type where
  MkMRetraction : (f : Maybe a -> List b) ->
                (r : List b -> Maybe a) ->
                (v : (x : Maybe a) -> r (f x) = x) ->
                (np: (x:a) -> (all' (isNothing . r) $ prefixes $ f (Just x) = True)) ->
                (ji: (l:List b) -> isJust (r l) = True -> (f (r l)) = l) ->
                (en: isNothing . r $ [] = True) ->
                MRetraction a b f r

data Many : Type -> Type -> Type where
  Nil : MRetraction a b f r ->
      (l: List b) ->
      (all' (isNothing . r) $ l :: prefixes l = True) ->
      Many a b
  Cons : MRetraction a b f r ->
       a ->
       Many a b ->
       Many a b

-- ^ this should be isomorphic to regular lists. informal proof:

-- Firstly, there is a retraction (Maybe a) < (List b), such that for
-- any l:List b = f x:a, there's no prefixes (counting Nil) of l that
-- could be read as other `a` values, and hence no ambiguity after
-- concatenation.

-- Secondly, input that can't be parsed goes into Many's Nil, and any
-- data that goes into Cons could be restored (another requirement on
-- the retraction), hence no data from List gets lost.

-- Obviously, no ambiguity in Maybe a -> List a translation, and no
-- data gets lost on translation into the list. Except for retraction
-- and proofs, maybe, so not that obviously, but they are kinda fixed.

manyExtractFirst' : (r : b -> Maybe a) -> (l: List b) -> all' (isNothing . r) l = False -> a
manyExtractFirst' r [] prf = void $ trueNotFalse prf
manyExtractFirst' r (x :: xs) prf with (r x)
  | Nothing = manyExtractFirst' r xs prf
  | Just x = x

manyExtractFirst : (r : List b -> Maybe a) ->
                 (l: List b) ->
                 (all' (isNothing . r) $ l :: prefixes l = False) ->
                 (isNothing . r $ [] = True) ->
                 a
manyExtractFirst r l p n = manyExtractFirst' r (l :: prefixes l) p

many : MRetraction a b f r ->
     Iso (Many a b) (List b)
many {a=a} {b=b} (MkMRetraction f r v np ji en) = MkIso to from tf ft
  where
  to : Many a b -> List b
  to (Nil r l s) = l
  to (Cons (MkMRetraction f _ _ _ _ _) x s) = f (Just x) ++ to s
  from : List b -> Many a b
  from l = case (inspect $ all' (isNothing . r) $ l :: prefixes l) of
    (match True {eq=eq}) => Nil (MkMRetraction f r v np ji en) l eq
    (match False {eq=eq}) =>
           Cons (MkMRetraction f r v np ji en)
                (manyExtractFirst r l eq en)
                (from (assert_smaller l (drop (length (f (Just (manyExtractFirst r l eq en)))) l)))
  tf x = ?manytf
  ft x = ?manyft

-- `Many` without a tail

data Many' : Type -> Type -> Type where
  Nil' : MRetraction a b f r ->
       Many' a b
  Cons' : MRetraction a b f r ->
        a ->
        Many' a b ->
        Many' a b

isNil : Many a b -> Bool
isNil (Nil _ _ _) = True
isNil (Cons _ _ _) = False

mto' : Many a b -> Many' a b
mto' (Nil r l s) = Nil' r
mto' (Cons r x m) = Cons' r x (mto' m)

mfrom' : Many' a b -> Many a b
mfrom' (Nil' (MkMRetraction f r v np ji en)) = Nil (MkMRetraction f r v np ji en) [] (rewrite en in Refl)
mfrom' (Cons' r x m) = Cons r x (mfrom' m)

mtail : Many a b -> List b
mtail (Cons _ _ m) = mtail m
mtail (Nil _ l _) = l

manyAnd : (mi: Iso (Many a b) (List b)) ->
        (cr: Retraction c (List b) cto cfrom) ->
        ((x:c) -> (isNil (unappIso mi (cto x)) = True)) ->
        ((l:List b) -> (isNil (unappIso mi l) = True) -> (cto (cfrom l) = l)) ->
        Iso (Many' a b, c) (List b)
manyAnd {a=a} {b=b} (MkIso mto mfrom mtf mft) (MkRetraction cto cfrom cft) p p2 = MkIso to from tf ft
  where
  to : (Many' a b, c) -> List b
  to (x, y) = mto (mfrom' x) ++ cto y
  from : List b -> (Many' a b, c)
  from l = case (mfrom l) of
    m => (mto' m, cfrom (mtail m))
  tf x = ?mvtf -- rewrite (ctf (mtail (mfrom x))) in ?mvtf
  ft x = ?mvft

-- examples

data Foo = Zero | One | End

bcto' : List Bool -> List Foo
bcto' [] = [End]
bcto' (False::xs) = Zero :: bcto' xs
bcto' (True::xs) = One :: bcto' xs

bcto : Maybe (List Bool) -> List Foo
bcto Nothing = []
bcto (Just l) = bcto' l

bcfrom : List Foo -> Maybe (List Bool)
bcfrom (Zero::xs) = do
  rest <- bcfrom xs
  Just (False :: rest)
bcfrom (One::xs) = do
  rest <- bcfrom xs
  Just (True :: rest)
bcfrom [End] = Just []
bcfrom _ = Nothing

boolFoo : MRetraction (List Bool) Foo bcto bcfrom
boolFoo = MkMRetraction bcto bcfrom v np ji en
  where
    v' : (l: List Bool) -> bcfrom (bcto' l) = Just l
    v' [] = Refl
    v' (False :: xs) = rewrite (v' xs) in Refl
    v' (True :: xs) = rewrite (v' xs) in Refl
    v : (l: Maybe (List Bool)) -> bcfrom (bcto l) = l
    v Nothing = Refl
    v (Just l) = v' l
    np x = believe_me ()
    ji l p = believe_me ()
    en = Refl

bsto : Bool -> Foo
bsto True = One
bsto False = Zero

bsfrom : Foo -> Bool
bsfrom End = False
bsfrom Zero = False
bsfrom One = True

boolFooS : Retraction (List Bool) (List Foo) (map bsto) (map bsfrom)
boolFooS = MkRetraction (map bsto) (map bsfrom) v
  where
  v [] = Refl
  v (False :: xs) = cong (v xs)
  v (True :: xs) = cong (v xs)

bfnbf : Iso (Many' (List Bool) Foo, List Bool) (List Foo)
bfnbf = manyAnd (many boolFoo) boolFooS p1 p2
  where
  -- ((x:List Bool) -> (isNil (unappIso (many boolFoo) (bsto x)) = True))
  -- there's never `End` in `bsto`, so it's `Nil`
  p1 = believe_me ()
  -- ((l:List b) -> (isNil (unappIso (many boolFoo) l) = True) -> (bsto (bsfrom l) = l))
  -- `Nil` happens only if there's no `End`, and in that case `bsto (bsfrom l) = l`
  p2 = believe_me ()

lfNil : Many (List Bool) Foo
lfNil = Nil boolFoo [] Refl

lfCons : List Bool -> Many (List Bool) Foo -> Many (List Bool) Foo
lfCons l m = Cons boolFoo l m

lfTest : Many (List Bool) Foo
lfTest =
       lfCons [True, False, True, True] $
              lfCons [True, True] $
                     lfCons [False, False] $
                            lfNil

-- λΠ> appIso (many boolFoo) lfTest
-- [One, Zero, One, One, End, One, One, End, Zero, Zero, End] : List Foo
-- λΠ> appIso (many boolFoo) $ unappIso (many boolFoo) [One, Zero, One, One, End, One, One, End, Zero, Zero]
-- [One, Zero, One, One, End, One, One, End, Zero, Zero] : List Foo
-- λΠ> appIso bfnbf ((mto' lfTest), [True, False])
-- [One, Zero, One, One, End, One, One, End, Zero, Zero, End, One, Zero] : List Foo

max_stars_repo_name: defanor/morphisms

max_issues_repo_name: defanor/morphisms

max_forks_repo_name: defanor/morphisms


text:
module Data.Scientific.Parser.Simple

import Data.Fin
import Data.List1

import Text.Lexer
import Text.Lexer.Core
import Text.Parser
import Text.Parser.Core

import Data.Scientific

||| Kinds of tokens that can occur in a textual representation of a Scientific 10.
public export
data ScientificTokenKind = TDigit
                         | TSeparator
                         | TExponator
                         | TSign

public export
Show ScientificTokenKind where
  show TDigit = "TDigit"
  show TSeparator = "TSeparator"
  show TExponator = "TExponator"
  show TSign = "TSign"

public export
TokenKind ScientificTokenKind where
  TokType TDigit = Fin 10
  TokType TSeparator = ()
  TokType TExponator = ()
  TokType TSign = Sign
  tokValue TDigit "0" = 0
  tokValue TDigit "1" = 1
  tokValue TDigit "2" = 2
  tokValue TDigit "3" = 3
  tokValue TDigit "4" = 4
  tokValue TDigit "5" = 5
  tokValue TDigit "6" = 6
  tokValue TDigit "7" = 7
  tokValue TDigit "8" = 8
  tokValue TDigit "9" = 9
  tokValue TDigit _ = ?exhaustiveBecauseOfTokenMap1 -- TODO
  tokValue TSeparator _ = ()
  tokValue TExponator _ = ()
  tokValue TSign "+" = Positive
  tokValue TSign "-" = Negative
  tokValue TSign _ = ?exhaustiveBecauseOfTokenMap2 -- TODO

public export
Eq ScientificTokenKind where
  TDigit == TDigit = True
  TSeparator == TSeparator = True
  TExponator == TExponator = True
  TSign == TSign = True
  _ == _ = False

export
tokenMap : TokenMap (Token ScientificTokenKind)
tokenMap = toTokenMap
  [ (digit, TDigit)
  , (is '.', TSeparator)
  , (oneOf "eE", TExponator)
  , (oneOf "+-", TSign)
  ]

private
grammarSign : Grammar (Token ScientificTokenKind) False Sign
grammarSign = fromMaybe Positive <$> optional (match TSign)

private
grammarBeforeSeparator : Grammar (Token ScientificTokenKind) True (Fin 9)
grammarBeforeSeparator = match TDigit >>= catchZero
  where catchZero : Fin 10 -> Grammar (Token ScientificTokenKind) False (Fin 9)
        catchZero FZ = fail "expected digit between 1 and 9"
        catchZero (FS x) = pure x

private
grammarZero : Grammar (Token ScientificTokenKind) True (Scientific 10)
grammarZero = match TDigit >>= f
  where f : Fin 10 -> Grammar _ False (Scientific 10)
        f 0 = pure SciZ
        f _ = fail "expected digit 0"

private
grammarSeparator : Grammar (Token ScientificTokenKind) True (List1 (Fin 10))
grammarSeparator = match TSeparator *> some (match TDigit)

private
fixCoeff : Fin 9 -> Maybe (List1 (Fin 10)) -> Maybe (Coefficient 10)
fixCoeff x Nothing = Just $ CoeffInt x
fixCoeff x (Just y) with (unsnoc y)
  fixCoeff x (Just y) | (zs, FZ) = Nothing
  fixCoeff x (Just y) | (zs, FS z) = Just $ CoeffFloat x zs z

private
grammarCoeff : Grammar (Token ScientificTokenKind) True (Coefficient 10)
grammarCoeff = fixCoeff <$> grammarBeforeSeparator <*> optional grammarSeparator >>= maybe (fail "expected ending on digit between 1 and 9") pure

private
fixExp : List1 (Fin 10) -> Integer
fixExp = foldr1 f . map finToInteger . reverse
  where f : Integer -> Integer -> Integer
        f x i = x + 10 * i

private
grammarExponent : Grammar (Token ScientificTokenKind) True Integer
grammarExponent = match TExponator *> applySign <$> grammarSign <*> fixExp <$> some (match TDigit)
  where applySign : Sign -> Integer -> Integer
        applySign Positive = id
        applySign Negative = negate

-- TODO: Fix exponent.
-- TODO: Expect eof after zero.
||| Grammar of a Scientific 10.
export
scientificGrammar : Grammar (Token ScientificTokenKind) True (Scientific 10)
scientificGrammar = grammarZero <|> (Sci <$> grammarSign <*> grammarCoeff <*> grammarExponent)