text:
||| An expression language with mechanical proof of type-safety.
|||
||| `Variant` is an expression language supporting Let-bindings, and
||| type unsafe variants.  Standard constructions are used to
||| represent the language as an EDSL, together with proof of progress
||| taken from PLFA Part 2.
|||
||| This module compliments Section 4.1 of the Functional Pearl.
|||
module Razor.Variant

import Razor.Common

%default total

namespace Types

  public export
  data Ty = TyInt
          | TyChar
          | TyVariant (Vect (S n) (Pair String Ty))

namespace Terms
  mutual
    public export
    data Case : (ctxt  : List Ty)
             -> (label : String)
             -> (type  : Ty)
             -> (body  : Ty)
             -> Type
      where
        MkCase : (label  : String)
              -> (branch : Variant (ctxt +=    type) body)
                        -> Case     ctxt label type body

    public export
    data Cases : (ctxt  : List Ty)
              -> (types : Vect (S n) (Pair String Ty))
              -> (body  : Ty)
              -> Type
      where
          Singleton : (branch : Case  g   label  ty   b)
                             -> Cases g [(label, ty)] b

          Extend : (branch : Case  g   label  ty          b)
                -> (rest   : Cases g                 kvs  b)
                          -> Cases g ((label, ty) :: kvs) b

    public export
    data Variant : List Ty -> Ty -> Type where
      -- Let-Binding & Variables
      Var : Elem ty g -> Variant g ty

      Let : {expr, body : Ty}
         -> (this     : Variant        g  expr)
         -> (beInThis : Variant (expr::g) body)
                     -> Variant        g  body

      -- Base Values
      I : Int  -> Variant g TyInt
      C : Char -> Variant g TyChar

      -- Variants & Accessors
      Tag : {kvs : Vect (S n) (Pair String Ty)}
         -> (label : String)
         -> (value : Variant g ty)
         -> (prf   : Elem (label, ty) kvs)
                  -> Variant g (TyVariant kvs)

      Match : {kvs : Vect (S n) (Pair String Ty)}
           -> {b : Ty}
           -> (value : Variant g (TyVariant kvs))
           -> (cases : Cases   g            kvs   b)
                    -> Variant g                  b

namespace Renaming
  public export
  weaken : forall type
         . (Contains  old           type -> Contains  new           type)
        -> (Contains (old += type') type -> Contains (new += type') type)

  weaken func Here         = Here
  weaken func (There rest) = There (func rest)

  mutual
    namespace Case

      public export
      rename : (forall type . Contains old type -> Contains new type)
            -> (forall type, body . Case old label type body
                                 -> Case new label type body)
      rename f (MkCase label branch)
        = MkCase label (rename (weaken f) branch)

    namespace Cases
      public export
      rename : (forall type . Contains (old) type -> Contains (new) type)
            -> (forall types, type . Cases old types type
                                  -> Cases new types type)
      rename f (Singleton branch)
        = Singleton (Case.rename f branch)
      rename f (Extend branch rest)
        = Extend (Case.rename f branch) (rename f rest)

    public export
    rename : (forall type . Contains old type -> Contains new type)
          -> (forall type . Variant  old type -> Variant  new type)
    -- Let-Bindings & Variables
    rename f (Var x) = Var (f x)
    rename f (Let this beInThis)
      = Let (rename f this)
            (rename (weaken f) beInThis)

    -- Base Variables
    rename f (I x) = I x
    rename f (C x) = C x

    -- Variants & Accesors
    rename f (Tag label value prf) = Tag label (rename f value) prf
    rename f (Match value cases) = Match (rename f value)
                                         (Cases.rename f cases)

namespace Substitution
  public export
  weakens : forall old, new
          . (f : forall type
               . Contains old type
              -> Variant  new type)
         -> (forall type . Contains (old += type') type
                        -> Variant  (new += type') type)
  weakens f Here         = Var Here
  weakens f (There rest) = rename There (f rest)

  namespace General
    mutual
      namespace Case
        public export
        subst : (f : forall type
                   . Contains old type
                  -> Variant  new type)
             -> (forall type, body . Case old label type body
                                  -> Case new label type body)
        subst f (MkCase label branch)
          = MkCase label (subst (weakens f) branch)

      namespace Cases
        public export
        subst : (f : forall type
                   . Contains old type
                  -> Variant new type)
             -> (forall types, type . Cases old types type
                                   -> Cases new types type)
        subst f (Singleton branch)
          = Singleton (Case.subst f branch)
        subst f (Extend branch rest)
          = Extend (Case.subst f branch) (subst f rest)

      public export
      subst : (forall type . Contains old type -> Variant new type)
           -> (forall type . Variant  old type -> Variant new type)
      -- Let-Bindings & Variables
      subst f (Var x) = f x
      subst f (Let this beInThis)
        = Let (subst f this) (subst (weakens f) beInThis)

      -- Base Values
      subst f (I x) = I x
      subst f (C x) = C x

      -- Variants & Accessors
      subst f (Tag label value prf)
        = Tag label (subst f value) prf
      subst f (Match value cases)
        = Match (subst f value) (subst f cases)

  namespace Single
    public export
    apply : (this : Variant ctxt typeB)
         -> (idx  : Contains (ctxt += typeB) typeA)
                 -> Variant ctxt typeA
    apply this Here         = this
    apply this (There rest) = Var rest

    public export
    subst : (this   : Variant  ctxt           typeB)
         -> (inThis : Variant (ctxt += typeB) typeA)
                   -> Variant  ctxt           typeA
    subst {ctxt} {typeA} {typeB} this inThis
       = General.subst (apply this) inThis

namespace Values

  public export
  data Value : Variant ctxt type -> Type where
    -- Base Values
    IV : Value (I i)
    CV : Value (C c)

    -- Variants
    MkTagV : {kvs    : Vect (S n) (Pair String Ty)}
          -> {value' : Variant Nil type}
          -> (value  : Value value')
          -> {prf    : Elem (label, type) kvs}
                    -> Value (Tag label value' prf)

namespace Reduction

  namespace Cases
    public export
    data Redux : (value  : Variant g type)
              -> (cases  : Cases g kvs body)
              -> (idx    : Elem (label, type) kvs)
              -> (result : Variant g body)
              -> Type
      where
        ReduceSingleton : {value : Variant g type}
                                -> Value value
                                -> Redux value
                                         (Singleton (MkCase label branch))
                                         Here
                                         (subst value branch)
        ReduceExtend : {value : Variant g type}
                    -> {rest  : Cases g kvs body}
                    -> Value value
                    -> Redux value
                             (Extend (MkCase label branch) rest)
                             Here
                             (Single.subst value branch)
        SkipThis : Redux value rest later result
                -> Redux value
                         (Extend branch rest)
                         (There later)
                         result

  public export
  data Redux : (this, that : Variant ctxt type) -> Type where
    -- Let Bindings
    SimplifyLetValue : Redux this that
                    -> Redux (Let this body)
                             (Let that body)
    ReduceLetBody : Value value
                 -> Redux (Let value body)
                          (subst value body)

    -- Variants & Accessors
    SimplifyTag : {kvs   : Vect (S n) (Pair String Ty)}
               -> {prf   : Elem (label, type) kvs}
               -> (redux : Redux this that)
                        -> Redux (Tag label this prf) (Tag label that prf)

    SimplifyMatchCase : {cases : Cases _ kvs type}
                     -> (redux : Redux this that)
                              -> Redux (Match this cases) (Match that cases)

    ReduceCases : {kvs   : Vect (S n) (Pair String Ty)}
               -> {idx   : Elem (label, type') kvs}
               -> {value : Variant g type'}
               -> {this  : Cases g kvs type}
               -> {that  : Variant g type}
               -> (prf   : Value value)
               -> (redux : Redux value this idx that)
                        -> Redux (Match (Tag label value idx) this)
                                 that

namespace Progress

  public export
  data Progress : (term : Variant Nil type)
                       -> Type
    where
      Done : {term  : Variant Nil type}
          -> (value : Value term)
                   -> Progress term

      Step : {type       : Ty}
          -> {this, that : Variant Nil type}
          -> (step       : Redux this that)
                        -> Progress this

  namespace Cases
    public export
    data Progress : (label : String)
                 -> (value : Variant Nil type)
                 -> (idx   : Elem (label, type) kvs)
                 -> (term  : Cases Nil kvs body)
                 -> Type
      where
        Step : {value : Variant Nil type'}
            -> {idx   : Elem (label, type') kvs}
            -> {cases : Cases Nil kvs type}
            -> {that  : Variant Nil type}
            -> (step  : Redux value cases idx that)
                    -> Progress label value idx cases
  mutual
    namespace Cases
      public export
      progress : {value' : Variant Nil type}
              -> (idx    : Elem (label, type) kvs)
              -> (value  : Value value')
              -> (term   : Cases Nil kvs body)
                        -> Progress label value' idx term
      progress Here value (Singleton (MkCase label branch))
        = Step (ReduceSingleton value)
      progress Here value (Extend (MkCase label branch) rest)
        = Step (ReduceExtend value)
      progress (There later) value (Extend branch rest) with (progress later value rest)
        progress (There later) value (Extend branch rest) | Step step
          = Step (SkipThis step)

    public export
    progress : forall type . (term : Variant Nil type) -> Progress term
    -- Let-Bindings & Variables
    progress (Var _) impossible

    progress (Let this beInThis) with (progress this)
      progress (Let this beInThis) | (Done value) = Step (ReduceLetBody value)
      progress (Let this beInThis) | (Step step) = Step (SimplifyLetValue step)

    -- Base Values
    progress (I x) = Done IV
    progress (C x) = Done CV

    -- Variants & Accessors
    progress (Tag label value prf) with (progress value)
      progress (Tag label value prf) | (Done value') = Done (MkTagV value')
      progress (Tag label value prf) | (Step step) = Step (SimplifyTag step)

    progress (Match value cases) with (progress value)
      progress (Match (Tag label value' prf) cases) | (Done (MkTagV x)) with (progress prf x cases)
        progress (Match (Tag label value' prf) cases) | (Done (MkTagV x)) | (Step step)
          = Step (ReduceCases x step)
      progress (Match value cases) | (Step step) = Step (SimplifyMatchCase step)

namespace Evaluation

  public export
  data Reduces : (this : Variant ctxt type)
              -> (that : Variant ctxt type)
              -> Type
    where
      Refl  : {this : Variant ctxt type}
                   -> Reduces this this
      Trans : {this, that, end : Variant ctxt type}
           -> Redux this that
           -> Reduces that end
           -> Reduces this end

  public export
  data Finished : (term : Variant ctxt type)
                       -> Type
    where
      Normalised : {term : Variant ctxt type}
                -> (this : Value term)
                        -> Finished term
      OOF : Finished term

  public export
  data Evaluate : (term : Variant Nil type) -> Type where
    RunEval : {this, that : Variant Nil type}
           -> (steps      : Inf (Reduces this that))
           -> (result     : Finished that)
                         -> Evaluate this

  public export
  data Fuel = Empty | More (Lazy Fuel)

  public export
  covering
  forever : Fuel
  forever = More forever

  public export
  compute : (fuel : Fuel)
         -> (term : Variant Nil type)
                 -> Evaluate term
  compute Empty term = RunEval Refl OOF
  compute (More fuel) term with (progress term)
    compute (More fuel) term | (Done value) = RunEval Refl (Normalised value)
    compute (More fuel) term | (Step step {that}) with (compute fuel that)
      compute (More fuel) term | (Step step {that = that}) | (RunEval steps result)
        = RunEval (Trans step steps) result

public export
covering
run : (this : Variant Nil type)
           -> Maybe (Subset (Variant Nil type) (Reduces this))
run this with (compute forever this)
  run this | (RunEval steps (Normalised {term} x)) = Just (Element term steps)
  run this | (RunEval steps OOF) = Nothing

namespace Examples

  public export
  ici : Variant Nil (TyVariant [("int", TyInt), ("char", TyChar)])
  ici = Tag "int" (I 1) Here

  public export
  icc : Variant Nil (TyVariant [("int", TyInt), ("char", TyChar)])
  icc = Tag "char" (C 'c') (There Here)

  public export
  iciM : Variant Nil TyInt
  iciM = Match ici (Extend (MkCase "int" (Var Here)) (Singleton (MkCase "char" $ I 2)))

  public export
  iccM : Variant Nil TyInt
  iccM = Match icc (Extend (MkCase "int" $ Var Here) (Singleton (MkCase "char" $ I 2)))

{-
  public export
  snip : Variant Nil TyInt
  snip = (Match (Tag "int" (I 1) Here) (Extend (MkCase "int" (Var Here))
                                       (Singleton (MkCase "char" (I 2)))))
-}


text:
module WebAssembly.Validation.Modules.Memories

import WebAssembly.Structure
import WebAssembly.Validation.Conventions
import WebAssembly.Validation.Types

||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/modules.html#memories)
|||
||| ```
||| ⊢ memtype ok
||| --------------------------------
||| C ⊢ {type memtype} : memtype
||| ```
public export
data ValidMem : Context -> Mem -> MemType -> Type where
  MkValidMem : (c : Context)
            -> (memtype : MemType)
            -> ValidMemoryType memtype
            -> ValidMem c (MkMem memtype) memtype

ext: idr

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
module Language.JSON.String

import Language.JSON.String.Lexer
import Language.JSON.String.Parser
import Language.JSON.String.Tokens
import Text.Lexer

%default total

export
permissiveStringLit : Lexer
permissiveStringLit
  = quo <+> manyUntil quo (esc any <|> any) <+> opt quo

export
stringValue : String -> Maybe String
stringValue x = parseString !(lexString x)


text:
total
countFrom : Integer -> Stream Integer
countFrom x = iterate (+1) x
-- countFrom x = x :: countFrom (x + 1)

total
labelFrom : Integer -> List a -> List (Integer, a)
labelFrom lbl [] = []
labelFrom lbl (x :: xs) = (lbl, x) :: labelFrom (lbl + 1) xs

label : List a -> List (Integer, a)
label = labelFrom 0

max_stars_repo_name: tekerson/type-driven-development

max_issues_repo_name: tekerson/type-driven-development

max_forks_repo_name: tekerson/type-driven-development


text:
module DepPairs

import Data.Vect

%default total

--data Vect : Nat -> Type -> Type where
--  Nil : Vect Z a
--  (::) : a -> Vect k a -> Vect (S k) a
--
data DepPair : (a : Type) -> (p : a -> Type) -> Type where
  MkDepPair : { p : a -> Type } -> (x : a) -> p x -> DepPair a p

vi : Vect 10 Nat
vi = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]

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

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

vFilter : (a -> Bool) -> Vect n a -> (p : Nat ** Vect p a)
vFilter _ [] = (0 ** [])
vFilter p (x :: xs) = case p x of
                           False => vFilter p xs
                           True => let (_ ** res) = vFilter p xs in
                                       (_ ** (x :: res))

vFilter' :  { a: _ } -> (a -> Bool) -> Vect n a -> DepPair Nat (\p => Vect p a)
vFilter' _ [] = MkDepPair 0 []
vFilter' p (x :: xs) = case p x of
                            False => vFilter' p xs
                            True => let (MkDepPair _ res) = vFilter' p xs in
                                        MkDepPair _ (x :: res)

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

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

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


text:
-- exercises in "Type-Driven Development with Idris"
-- chapter 4

-- check that all functions are total
%default total

||| Powersources for vehicles
data PowerSource = Petrol | Pedal | Electric

||| Vehicles
data Vehicle : PowerSource -> Type where
  Unicycle : Vehicle Pedal
  Bicycle : Vehicle Pedal
  Motorcycle : (fuel : Nat) -> Vehicle Petrol
  Car : (fuel : Nat) -> Vehicle Petrol
  Bus : (fuel : Nat) -> Vehicle Petrol
  Tram : Vehicle Electric
  ElectricCar : Vehicle Electric

wheels : Vehicle power -> Nat
wheels Unicycle = 1
wheels Bicycle = 2
wheels (Motorcycle fuel) = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4
wheels Tram = 10
wheels ElectricCar = 4

refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Motorcycle fuel) = Motorcycle 50
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200
refuel Unicycle impossible
refuel Bicycle impossible
refuel Tram impossible
refuel ElectricCar impossible

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
module Data.Optics

import public Data.Optics.Lens
import public Data.Optics.Iso
import public Data.Optics.Prism
import public Data.Optics.Optional

import Control.Category

--
-- Conversions
--

-- Iso

isoAsPrism: (Iso s a) -> (Prism s a)
isoAsPrism (MkIso to from) = MkPrism (\s => Just (to s)) (\a => from a)

isoAsLens: (Iso s a) -> (Lens s a)
isoAsLens (MkIso to from) = MkLens (to) (\s => from)

isoAsOptional: (Iso s a) -> (Optional s a)
isoAsOptional (MkIso to from) = MkOptional (\s =>  Just(to s)) (\s,a => from a)

-- Lens

lensAsOptional: (Lens s a ) -> (Optional s a)
lensAsOptional (MkLens get set) = MkOptional (\s => Just (get s)) (set)

-- Prism

prismAsOptional: Prism s a -> Optional s a
prismAsOptional (MkPrism to from) = MkOptional (to) (\s => from)

--
--  Compositions
--

infixr 9 <:+
||| the composition of a prism with a lens is an optional
(<:+) : Prism a b -> Lens s a -> Optional s b
(<:+) prism lens = let prismOptional = prismAsOptional prism
                       lensOptional = lensAsOptional lens
                       in prismOptional ?:+ lensOptional

infixr 9 +:>
(+:>) : Lens s a -> Prism a b -> Optional s b
(+:>) = flip (<:+)

--
-- instances
--

||| An Iso forms a Category
instance Category Iso where
 id = MkIso id id
 (.) = (-:+)

||| A Lens forms a Category
instance Category Lens where
 id = MkLens (id) (\a => id)
 (.) = (#:+)

||| An Optonal forms a Category
instance Category Optional where
 id = MkOptional Just (\a => id)
 (.) = (?:+)

||| A Prism forms a Category
instance Category Prism where
 id = MkPrism Just id
 (.) = (<:+)

max_stars_repo_name: justjoheinz/idris-optics

max_issues_repo_name: justjoheinz/idris-optics

max_forks_repo_name: justjoheinz/idris-optics


text:
module Main
main : IO()
main = putStrLn "Hello world"

max_stars_repo_name: lonelyhentai/workspace

max_issues_repo_name: lonelyhentai/workspace

max_forks_repo_name: lonelyhentai/workspace


text:
module Example

import Data.AVL.Dependent.Graph

towns : List String
towns = ["Munchen",
         "Augsburg",
         "Nurnburg",
         "Stuttgart",
         "Kassel",
         "Erfurt",
         "Wurzburg",
         "Karlsruhe",
         "Frankfurt",
         "Mannheim"]

links : List (String, String, Maybe Int)
links = [("Frankfurt"  ,"Mannheim" , Just 85),
         ("Frankfurt"  ,"Wurzburg"  , Just 217),
         ("Frankfurt"  ,"Kassel"    , Just 173),
         ("Mannheim"   ,"Karlsruhe" , Just 80),
         ("Karlsruhe"  ,"Augsburg"  , Just 250),
         ("Augsburg"   ,"Munchen"   , Just 84),
         ("Wurzburg"   ,"Erfurt"    , Just 186),
         ("Wurzburg"   ,"Nurnburg"  , Just 167),
         ("Nurnburg"   ,"Stuttgart" , Just 183),
         ("Nurnburg"   ,"Munchen"   , Just 167),
         ("Kassel"     ,"Munchen"   , Just 502)]

g : Graph String Int
g = with List buildG towns links

 -- g1 : Graph String String
 -- g1 = buildG (zip [1..4] ["a", "b", "c", "d"] Refl) [("Munchen","Ausburg","a"),("Nurnburg","Ausburg","b"),("Munchen","Stuttgart","a")]

data HasNode : String -> Graph String Int -> Type where
  Has : HasNode a g

hasNode : (a : String) -> (g : Graph String Int) -> Dec (HasNode a g)
hasNode val g = case hasValue val g of
  True  => Yes (Has)
  False => No (believe_me)

gs : List Bool
gs = map (\x => doCheck x g) towns
  where
    doCheck : String -> Graph String Int -> Bool
    doCheck x g with (hasNode x g)
      | Yes prf = True
      | No  con = False
-- --------------------------------------------------------------------- [ DFS ]

namespace Main
  main : IO ()
  main = do
    putStrLn "A Graph"
    putStrLn $ show g

    printLn gs

    printLn (updateNodeValueUsing "Mannheim" (\x => "as") g)

    -- putStrLn "Trace of a Depth First Traversal"
    -- traceDfsIO 9 g
    -- putStrLn "Trace of a Breadth First Traversal"
    -- traceBfsIO 9 g

{-
9
5
7
10
1
3
6
8
4
2
-}

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


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

import Data.Maybe

import Data.String
import Data.List

import Data.Fixed

%default total

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

public export
record DecimalFormat where
  constructor MkDecimalFormat
  width : Maybe Nat
  prec  : Maybe Nat
  pad   : Maybe Char
  spc   : Char
  point : Char
  minus : Maybe (Either String String)
  plus  : Maybe (Either String String)

export defaultDecimalFormat : DecimalFormat
defaultDecimalFormat =
  MkDecimalFormat Nothing Nothing Nothing ' ' '.' (Just $ Left "-") Nothing

export zeroPad : Nat -> DecimalFormat -> DecimalFormat
zeroPad w = record { width = Just w, pad = Just '0' }

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

lpad : Nat -> Char -> String -> String
lpad n c str = replicate (fromInteger $ cast $ cast n - strLength str) c ++ str

formatDecimal : DecimalFormat -> Maybe (Either String String) -> String -> String -> String
formatDecimal fmt sign dec frc = let
  dec' = case (fmt.width, fmt.pad) of
              (Just w, Just c) => lpad w c dec
              _ => dec
  frc' = case fmt.prec of
              Nothing => if frc == "" then "" else (singleton fmt.point ++ frc)
              Just 0  => ""
              Just n  => (singleton fmt.point) ++ frc ++ lpad n '0' frc
  str  = case sign of
              Nothing => lpad (fromMaybe 0 fmt.width) ' ' dec' ++ frc'
              Just (Left s) => lpad (fromMaybe 0 fmt.width) ' ' (s ++ dec') ++ frc'
              Just (Right s) => lpad (fromMaybe 0 fmt.width) ' ' dec' ++ frc' ++ s
  in case fmt.width of
          Nothing => str
          Just n  => replicate (fromInteger $ cast $ cast n - strLength str) fmt.spc
                     ++ str

public export formatIntegral : (Show ty, Neg ty, Num ty, Ord ty) => DecimalFormat -> ty -> String
formatIntegral fmt x =
  if x < 0
     then formatDecimal fmt fmt.minus (show $ negate x) ""
     else formatDecimal fmt fmt.plus (show x) ""

public export formatFixed : {n:Nat} -> DecimalFormat -> Fixed n -> String
formatFixed {n=n} fmt (MkFixed x') with (n)
  formatFixed {n=n} fmt (MkFixed x') | 0 = formatIntegral fmt x'
  formatFixed {n=n} fmt (MkFixed x') | _ = let
    (x, sign) = if x' < 0 then (negate x', fmt.minus) else (x', fmt.plus)
    MkResV _ r _ = expToResolution n
    dec = show $ x `div` r
    frc' = show $ x `mod` r
    frc = replicate (fromInteger $ cast $ cast n - strLength frc') '0' ++ frc'
    in formatDecimal fmt sign dec frc

public export interface FormatDecimal t where format : DecimalFormat -> t -> String
public export FormatDecimal Nat where format fmt = formatIntegral fmt .  natToInteger
public export FormatDecimal Int where format = formatIntegral
public export FormatDecimal Integer where format = formatIntegral
public export {n:Nat} -> FormatDecimal (Fixed n) where format = formatFixed {n=n}

public export format' : FormatDecimal ty => (DecimalFormat -> DecimalFormat) -> ty -> String
format' f x = format (f defaultDecimalFormat) x

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


text:
> module Matrix.Operations

> import Data.Fin
> import Data.Vect

> import Matrix.Matrix

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

> row : (Fin m) -> Matrix m n t -> Vect n t
> row k xss = index k xss

> toVect : Matrix m n t -> Vect (m * n) t
> toVect = concat

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Console

import Effects
import Effect.StdIO
import Effect.State

Names : Type
Names = List String

name : Eff () [STATE Names, STDIO]
name = do putStr "Name? "
          n <- getStr
          case n of
            ""        => name
            "bye!"    => putStrLn "bye"
            otherwise => do names <- get
                            put $ n :: names
                            putStrLn $ show !get
                            putStrLn $ "hi, " ++ n
                            name

main : IO ()
main = run name

-- *src/Console> :exec main
-- Name? John
-- ["John"]
-- hi, John
-- Name? Jim
-- ["Jim", "John"]
-- hi, Jim
-- Name? Jane
-- ["Jane", "Jim", "John"]
-- hi, Jane
-- Name? Jerry
-- ["Jerry", "Jane", "Jim", "John"]


text:
module Effect.Monad

import Effects

-- Eff is a monad too, so we can happily use it in a monad transformer.

using (xs : List EFFECT, m : Type -> Type)
  instance Functor (\a => EffM m a xs (\v => xs)) where
    map f prog = do t <- prog
                    value (f t)

  instance Applicative (\a => EffM m a xs (\v => xs)) where
    pure = value
    (<$>) f a = do f' <- f
                   a' <- a
                   value (f' a')

  instance Monad (\a => Eff m a xs (\v => xs)) where
    (>>=) = Effects.(>>=)

max_stars_repo_name: edwinb/Eff-new

max_issues_repo_name: edwinb/Eff-new

max_forks_repo_name: edwinb/Eff-new


text:
public export
record UInt where
    -- Then we should instance some type class for
    -- UInt or other custom primitive types.
    -- Note!!! The impl for those primitive types
    -- could use foreign functions, which makes it
    -- super fast!
    constructor MkUInt
    i : Int

public export
unsigned : Int -> UInt
unsigned = MkUInt

mutual
    public export
    data Com_Fn t = MkComFn t

    public export
    data Com_Raw t = MkComRaw t

    public export
    data Com_FunTypes : Type -> Type where
        Com_Fun       : Com s -> Com_FunTypes t -> Com_FunTypes (s -> t)
        Com_FnIO      : Com t -> Com_FunTypes (CamIO t)
        Com_FnBase    : Com t -> Com_FunTypes t

    public export
    data Com : Type -> Type where
        ComUnit   : Com ()
        ComStr    : Com String
        ComDouble : Com Double -- bit -> type
        ComInt    : Com Int    -- bit -> type
        ComUInt   : Com UInt   -- an example of extensive primitive type impl
        ComPtr    : Com Ptr
        ComFun    : Com_FunTypes a -> Com (Com_Fn a)
        ComChar   : Com Char
        ComRaw    : Com (Com_Raw a)

    public export
    data ForeignName
       = Builtin String
       | Library String String

    public export
    FFICam : FFI
    FFICam = MkFFI Com ForeignName String

    public export
    CamIO : Type -> Type
    CamIO = IO' FFICam

%inline
camCall: (ty : Type) -> (fname : ForeignName) -> {auto fty : FTy FFICam [] ty} -> ty
camCall ty fname = foreign FFICam fname ty

println : String -> CamIO ()
println s = camCall (String -> CamIO ()) (Builtin "println") s

data FileHandler;

openFile : String -> CamIO (Com_Raw FileHandler)
openFile filename = camCall (String -> CamIO (Com_Raw FileHandler)) (Builtin "simple_open") filename

readFile : Com_Raw FileHandler -> CamIO String
readFile handle = camCall (Com_Raw FileHandler -> CamIO String) (Builtin "simple_read") handle

main : CamIO ()
main = do
    fh <- openFile "./text.txt"
    s <- readFile fh
    println s

max_stars_repo_name: thautwarm/idris-cam

max_issues_repo_name: thautwarm/idris-cam

max_forks_repo_name: thautwarm/idris-cam


text:
module Parser.Source

import public Parser.Lexer.Source
import public Parser.Rule.Source
import public Parser.Unlit

import Core.Core
import Core.Name
import Core.Metadata
import Core.FC

import System.File

%default total

export
runParserTo : {e : _} ->
              (origin : OriginDesc) ->
              Maybe LiterateStyle -> Lexer ->
              String -> Grammar SemanticDecorations Token e ty ->
              Either Error (List Warning, SemanticDecorations, ty)
runParserTo origin lit reject str p
    = do str    <- mapFst (fromLitError origin) $ unlit lit str
         toks   <- mapFst (fromLexError origin) $ lexTo reject str
         (decs, ws, (parsed, _)) <- mapFst (fromParsingErrors origin) $ parseWith p toks
         let ws = ws <&> \ (mb, warn) =>
                    let mkFC = \ b => MkFC origin (startBounds b) (endBounds b)
                    in ParserWarning (maybe EmptyFC mkFC mb) warn
         Right (ws, decs, parsed)

export
runParser : {e : _} ->
            (origin : OriginDesc) -> Maybe LiterateStyle -> String ->
            Grammar SemanticDecorations Token e ty ->
            Either Error (List Warning, SemanticDecorations, ty)
runParser origin lit = runParserTo origin lit (pred $ const False)

export covering
parseFile : (fname : String)
         -> (origin : OriginDesc)
         -> Rule ty
         -> IO (Either Error (List Warning, SemanticDecorations, ty))
parseFile fname origin p
    = do Right str <- readFile fname
             | Left err => pure (Left (FileErr fname err))
         pure (runParser origin (isLitFile fname) str p)


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

module Toolkit.Options.ArgParse.Error

import Data.String

import System.File

import Toolkit.Data.Location

import Toolkit.Options.ArgParse.Model
import Toolkit.Options.ArgParse.Lexer
import Toolkit.Options.ArgParse.Parser

%default total

public export
data ArgParseError : Type where
  InvalidOption   : Arg -> ArgParseError
  MalformedOption : ParseError Token -> ArgParseError

export
(Show Arg) => Show ArgParseError where
  show (InvalidOption o)
    = "Invalid Option " ++ show o
  show (MalformedOption err)
    = "Malformed Option " ++ show err

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

max_stars_repo_name: border-patrol/linear-circuits

max_issues_repo_name: border-patrol/linear-circuits

max_forks_repo_name: border-patrol/linear-circuits


text:
-- Adder.idr

-- Demonstrate functions with variable number of arguments by an
-- adder function

AdderType : (numargs : Nat) -> Type -> Type
AdderType Z numType = numType
AdderType (S k) numType = (next : numType) -> AdderType k numType

||| An adder function for variable number of arguments
adder : Num numType => (numargs : Nat) -> (acc : numType) -> AdderType numargs numType
adder Z acc = acc
adder (S k) acc = \next => adder k (next + acc)

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
module Main

%include C "memory.h"

-- use calloc to ensure zeroed out memory
malloc : Int -> IO Ptr
malloc size = foreign FFI_C "calloc" (Int -> Int -> IO Ptr) size 1

free : Ptr -> IO ()
free ptr = foreign FFI_C "free" (Ptr -> IO ()) ptr

main : IO ()
main = do
    p <- malloc 1000
    prim_poke16 p 0 0xffff
    prim_poke8 p 8 1
    prim_poke8 p 9 2
    prim_poke8 p 10 3
    prim_poke8 p 11 4
    a <- prim_peek32 p 8
    b <- prim_peek64 p 0
    printLn a
    printLn b
    free p

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
||| Turns and segment logic
module Bautzen.Game.Turn

import Bautzen.Combats
import Bautzen.GameUnit
import Bautzen.Game.Core
import Bautzen.Pos
import Bautzen.Terrain

import Data.Fin

public export
newTurn : Game -> Either GameError Event
newTurn (MkGame _ (MkGameState FZ _ _ _) _) = Right GameEnded
newTurn (MkGame _ (MkGameState (FS x) _ _ _) _) = Right $ TurnEnded (weaken x)

public export
nextSegment : Game -> Either GameError Event
nextSegment (MkGame _ (MkGameState _ _ Supply _) _) = Right (SegmentChanged Supply Move)
nextSegment (MkGame _ (MkGameState _ _  Move _) _) = Right (SegmentChanged Move (Combat NoCombat))
nextSegment (MkGame _ (MkGameState _ Axis (Combat NoCombat) _) _) = Right AxisTurnDone
nextSegment game@(MkGame _ (MkGameState _ Allies (Combat NoCombat) _) _) = newTurn game
nextSegment game@(MkGame _ (MkGameState _ side seg@(Combat (AssignStrategicSupport supSide state)) _) _) =
  if side == supSide
  then Right (SegmentChanged seg (Combat (AssignStrategicSupport (flipSide supSide) state)))
  else Right (SegmentChanged seg (Combat (Resolve state)))
nextSegment (MkGame _ (MkGameState _ side (Combat _) _) _) = Left $ CombatInProgress side
nextSegment (MkGame _ (MkGameState _ _ GameEnd _) _) = Left GameHasEnded

max_stars_repo_name: steshaw/hsgames

max_issues_repo_name: steshaw/hsgames

max_forks_repo_name: steshaw/hsgames


text:
import System.Concurrency.Channels

data Message = Add Nat Nat

adder : IO ()
adder =
    do
        Just senderChan <- listen 1
            | Nothing => adder
        Just msg <- unsafeRecv Message senderChan
            | Nothing => adder
        case msg of
            Add x y =>
                do
                    ok <- unsafeSend senderChan (x + y)
                    adder

main : IO ()
main =
    do
        Just addedPID <- spawn adder
            | Nothing => putStrLn "Spawn failed"
        Just chan <- connect addedPID
            | Nothing => putStrLn "Connection failed"
        ok <- unsafeSend chan (Add 2 3)
        Just answer <- unsafeRecv String chan
            | Nothing => putStrLn "Send failed"
        printLn answer


text:
import Js.ASync

ffn : Int -> JS_IO Int
ffn x =
  jscall
    "(%0 + 1)"
    (Int -> JS_IO Int)
    x

main : JS_IO ()
main = do
  v <- ffn 1
  putStrLn' $ show v

max_stars_repo_name: rbarreiro/idrisjs

max_issues_repo_name: prozacchiwawa/idrisjs

max_forks_repo_name: prozacchiwawa/idrisjs


text:
module FLK_sos

import FLK_ast
import Data.SortedMap

-- operational semanitcs for FLK
-- TODO: Need way to have abstractions step
mutual
  infixr 5 >==> -- read like => in SOS-land
  (>==>) : (CF a) -> (CF b) -> Type
  l >==> r = Step l r

  syntax "[" [ex1] "=>" [ex2] "]"=
    ex1 >- _ `Step` ex2 >- _

  syntax "[" [ex1] "," [env1] "=>" [ex2] "," [env2] "]"=
    ex1 >- env1 `Step` ex2 >- env2

  data Step  : (CF a) -> (CF b) -> Type where
    PNot     :  [Prim1 Not (B b), e => B (not b),  e]

    PrimStep :  [b => b']
             -> [Prim1 o b, e => Prim1 o b', e]

    ArithOp  :  {o : Op2 Arith}
             -> [Prim2 o (N n1) (N n2), e => N (arithOp o n1 n2), e]

    RelOp    :  {o : Op2 Rel}
             -> [Prim2 o (N b1) (N b2), e => B (relop o b1 b2), e]

    GenOp    :  {o : Op2 Gen} -> {op1 : Exp Done} -> {op2 : Exp Done}
             -> [Prim2 o op1 op2, e => genOp o op1 op2, e]

    Prim2L   :  [b => b']
             -> [Prim2 o b re, e => Prim2 o b' re, e]

    Prim2R   :  {le : Exp Done}
             -> [b => b']
             -> [Prim2 o le b, e => Prim2 o le b', e]

    IfCase   :  [b => b']
             -> [If b t f, e' => If b' t f, e']

    IfT      :  [If (B True) t f, e => t, e]

    IfF      :  [If (B False) t f, e => f, e]

    ClosLam  :  [Abs ident exp, e => Clos e (Abs ident exp), e]

    AppFunT  :  [b => b']
             -> [App b exp, e => App b' exp, e]

    AppArgT  :  [arg => arg']
             -> [App (Clos env lam) arg, e => App (Clos env lam) arg', e]

    AppLam   :  {val : Exp Done}
             -> [App (Clos env (Abs ident body)) val, e => body, insert ident (Left val) env]

    IdTrans  :  {e : Env} -> {n : Ident}
             -> Sigma (Exp Done) (\v => lookup n e = (Just (Left v)))
             -> [(Id n), e => v, e]

    IdRecTrans :  {e : Env} -> {n : Ident}
              -> Sigma (Exp RecLam) (\v => lookup n e = (Just (Right v)))
              -> [(Id n), e => v, e]

    RecTrans :  [(Rec ident exp), e => exp, insert ident (Right $ Rec ident exp) e]

  syntax "[[" [str] "," [sub] "]]" = str++" ["++(show sub)++"]";

  instance Show (Step a b) where
    show PNot = "PNot"
    show (PrimStep w) = [["PrimStep", w]]
    show ArithOp = "ArithOp"
    show RelOp = "RelOp"
    show GenOp = "GenOp"
    show (Prim2L t) = [["Prim2L", t]]
    show (Prim2R s) = [["Prim2R", s]]
    show (IfCase s) = [["IfCase", s]]
    show IfT = "IfT"
    show IfF = "IfF"
    show ClosLam = "ClosLam"
    show (AppFunT s) = [["AppFunT", s]]
    show (AppArgT z) = [["AppArgT", z]]
    show AppLam = "AppLam"
    show (IdTrans x) = "IdTrans"
    show (IdRecTrans x) = "IdRecTrans"
    show RecTrans = "RecTrans"

-- Simple rule application
testStep1 : Prim1 Not (B True) >- e >==> (B False) >- e
testStep1 = PNot

-- Compose two rules
testStep : [(Prim1 Not (Prim1 Not (B False))), e => Prim1 Not (B True), e]
testStep {e=e} = PrimStep $ PNot {e=e}

takeStep : {state' : CF b} -> {rule : state >==> state'} -> (state : CF a) ->  CF b
takeStep {state' = s} _ = s

default : Exp a -> CF a
default x = x >- emptyEnv

opResolve : {e : Env}
         -> (op : Op2 a)
         -> (o1 : Exp Done)
         -> (o2 : Exp Done)
         -> Maybe (Sigma (Exp Done) (\state => Step ((Prim2 op o1 o2) >- e) (state >- e)))
opResolve EQ op1 op2 = Just ((genOp EQ op1 op2) ** GenOp)
opResolve NEQ op1 op2 = Just ((genOp NEQ op1 op2) ** GenOp)
opResolve Plus (N k) (N z) =  Just ((N $ arithOp Plus k z) ** ArithOp)
opResolve Minus (N k) (N z) = Just ((N $ arithOp Minus k z) ** ArithOp)
opResolve LThan (N k) (N z) =  Just ((B $ relop LThan k z) ** RelOp)
opResolve LEThan (N k) (N z) = Just ((B $ relop LEThan k z) ** RelOp)
opResolve GThan (N k) (N z) =  Just ((B $ relop GThan k z) ** RelOp)
opResolve GEThan (N k) (N z) =  Just ((B $ relop GEThan k z) ** RelOp)
opResolve x x1 x2 = Nothing

mutual
  -- Evaluator based on operational semantics
  -- TODO: add printing, with effects and such
  goTill : Sigma Status (\s => CF s) -> Sigma Status (\s' => CF s')
  goTill (MkSigma Inter pf) with (search pf)
    goTill (MkSigma Inter pf) | Nothing = MkSigma Inter pf
    goTill (MkSigma Inter pf) | (Just (MkSigma x (MkSigma y z))) = goTill $ MkSigma x y
  goTill p@(MkSigma Done pf) = p
  goTill (MkSigma Lam pf) with (searchLam pf)
    goTill (MkSigma Lam pf) | Nothing = (MkSigma Lam pf)
    goTill (MkSigma Lam pf) | (Just (MkSigma x (MkSigma y z))) = goTill $ MkSigma x y
  goTill (MkSigma RecLam pf) = let (x ** (y ** z)) = recTrans pf in goTill (x ** y)

  -- Search rules for the semantics
  -- Forall states, we get
  --      Maybe (exists a Status such that there exists a state with
  --            that status that is transitioned to by the state)
  search : (start : CF Inter) -> Maybe (Sigma Status (\s => (Sigma (CF s) (\o => Step start o))))
  search ((App z w) >- y)     = search_app y z w
  search ((If z w s) >- y)    = search_if z w s y
  search ((Prim1 z w) >- y)   = search_prim1 z w y
  search ((Prim2 z w s) >- y) = search_prim2 z w s y
  search ((Id x) >- y) with (idSteps x y)
    search ((Id x) >- y) | Nothing with (idRecSteps x y)
      search ((Id x) >- y) | Nothing | Nothing = Nothing
      search ((Id x) >- y) | Nothing | (Just (v ** pf)) =
        Just $ (RecLam ** (v >- y ** IdRecTrans (v ** pf)))
    search ((Id x) >- y) | Just (v ** pf) = Just $ (Done ** (v >- y ** IdTrans (v ** pf)))

  -- This is a macro that will do most of the intermediate computations needed for some common
  -- lemmas
  -- My understanding is that this sort of thing should be done with a high-level tactic
  -- involving reflection. I do not fully understand how to use this feature, so I am using the
  -- 'syntax' feature as a macro system of sorts
  syntax "[[" {state} "," {trans} "," [env] "," [ex] "," [newstate] "," [rule] "]]" =
               case (search $ ex >- env) of {
                 Nothing => Nothing ;
                 Just (status ** (state >- y' ** trans)) =>
                      Just (Inter ** (newstate >- env ** rule));
               }

  -- transition intermediate-result composite expressions. wrapper for above macro
  syntax "[[" [env] ";" [ex] ";" [newstate] ";" [rule] "]]" =
    [[ state, trans, env, ex, (newstate state), (rule trans)]]

  -- transition abstractions
  syntax "<[" [trans] "," [abs] "," [env] "," [state] "]>" =
    Just $ (_ ** (((state (Clos env abs)) >- env) ** trans ClosLam));
  -- transition rec expressions
  syntax "<[" [trans] ";" [rec] ";" [env] ";" [state] "]>" =
    let (tag ** (newstate >- env' ** newtrans)) = recTrans (rec >- env) in
        Just $ (_ ** ((state newstate) >- env ** trans newtrans));

  search_prim2_rhs_7 : (z : Op2 y)
                    -> (exp : Exp Done)
                    -> (s : Exp b)
                    -> (y : SortedMap String (Either (Exp Done) (Exp RecLam)))
                    -> Maybe (Sigma Status (\s2 => Sigma (CF s2)
                                   (\o => Step ((Prim2 z exp s) >- y) o)))
  search_prim2_rhs_7 z exp (App x w) y = [[y; (App x w); Prim2 z exp; Prim2R]]
  search_prim2_rhs_7 z exp (Abs x w) y = <[Prim2R, (Abs x w), y, Prim2 z exp]>
  search_prim2_rhs_7 z exp (Rec x w) y = <[Prim2R; (Rec x w); y; Prim2 z exp]>
  search_prim2_rhs_7 z exp (If x w s) y = [[y; If x w s; Prim2 z exp; Prim2R]]
  search_prim2_rhs_7 z exp (Prim1 x w) y = [[y; Prim1 x w; Prim2 z exp; Prim2R]]
  search_prim2_rhs_7 z exp (Prim2 w s t) y = [[y; Prim2 w s t; Prim2 z exp; Prim2R]]
  search_prim2_rhs_7 z exp (Id x) y = [[y; Id x; Prim2 z exp; Prim2R]]
  search_prim2_rhs_7 z exp (N k) y with (opResolve {e=y} z exp (N k))
    search_prim2_rhs_7 z exp (N k) y | Nothing = Nothing
    search_prim2_rhs_7 z exp (N k) y | (Just (exp ** step)) = Just (Done ** (exp >- y ** step))
  search_prim2_rhs_7 z exp (B x) y with (opResolve {e=y} z exp (B x))
    search_prim2_rhs_7 z exp (B x) y | Nothing = Nothing
    search_prim2_rhs_7 z exp (B x) y | (Just (exp ** step)) = Just (Done ** (exp >- y ** step))
  search_prim2_rhs_7 z exp (Clos x w) y with (opResolve {e=y} z exp (Clos x w))
    search_prim2_rhs_7 z exp (Clos x w) y | Nothing = Nothing
    search_prim2_rhs_7 z exp (Clos x w) y | (Just (exp ** step)) = Just (Done ** (exp >- y ** step))

  search_prim2 : (z : Op2 y)
              -> (w : Exp a)
              -> (s : Exp b)
              -> (y : SortedMap String (Either (Exp Done) (Exp RecLam)))
              -> Maybe (Sigma Status (\s1 => Sigma (CF s1)
                                             (\o => Step ((Prim2 z w s) >- y) o)))
  search_prim2 z (App x w) s y = [[y; (App x w); \st => Prim2 z st s; Prim2L]]
  search_prim2 z (Abs x w) s y = <[Prim2L, (Abs x w), y, \st => Prim2 z st s]>
  search_prim2 z (Rec x w) s y = <[Prim2L; (Rec x w); y; \st => Prim2 z st s]>
  search_prim2 z (If x w t) s y = [[y; If x w t; \st => Prim2 z st s; Prim2L]]
  search_prim2 z (Prim1 x w) s y = [[y; Prim1 x w; \st => Prim2 z st s; Prim2L]]
  search_prim2 z (Prim2 w t u) s y = [[y; Prim2 w t u; \st => Prim2 z st s; Prim2L]]
  search_prim2 z (Id x) s y = [[y; Id x; \st => Prim2 z st s; Prim2L]]
  search_prim2 z (N k) s y = search_prim2_rhs_7 z (N k) s y
  search_prim2 z (B x) s y = search_prim2_rhs_7 z (B x) s y
  search_prim2 z (Clos x w) s y = search_prim2_rhs_7 z (Clos x w) s y

  total
  searchLam : (start : CF Lam)
           -> Maybe (Sigma Status (\s => (Sigma (CF s) (\o => Step start o))))
  searchLam ((Abs x z) >- y) = <[ id , (Abs x z), y, id ]>

  total
  recTrans : (start : CF RecLam)
          -> (Sigma Status (\s => (Sigma (CF s) (\o => Step start o))))
  recTrans ((Rec x z) >- y) = (getTag z ** (z >- (insert x (Right $ Rec x z) y) ** RecTrans))

  total
  searchRec : (start : CF RecLam)
           -> Maybe (Sigma Status (\s => (Sigma (CF s) (\o => Step start o))))
  searchRec r = Just $ recTrans r

  search_if : (z : Exp a)
           -> (w : Exp b)
           -> (s : Exp c)
           -> (y : Env)
           -> Maybe (Sigma Status (\s1 => Sigma (CF s1) (\o => Step ((If z w s) >- y) o)))
  search_if (Abs x z) w s y  = <[IfCase, (Abs x z), y, \c => If c w s]> --Nothing
  search_if (Rec i b) w s y  = <[IfCase; (Rec i b); y; \c => If c w s]>
  search_if (N _) _ _ _      = Nothing
  search_if (Clos _ _) _ _ _ = Nothing
  search_if (B x) w s y = case x of
                               True  => let t = getTag w in
                                            Just (t ** (w >- y ** IfT))
                               False => let t = getTag s in
                                            Just (t ** (s >- y ** IfF))
  search_if (App lam st)  w s y = [[state, trans, y, App lam st, If state w s , IfCase trans]]
  search_if (If x z t)    w s y = [[y; (If x z t); \state => If state w s; IfCase]]
  search_if (Prim1 x z)   w s y = [[y; (Prim1 x z); \state => If state w s; IfCase]]
  search_if (Prim2 x z t) w s y = [[y; (Prim2 x z t); \state => If state w s; IfCase]]
  search_if (Id x)        w s y = [[y; (Id x); \state => If state w s; IfCase]]

  search_prim1 : (z : Op1)
              -> (w : Exp a)
              -> (y : Env)
              -> Maybe (Sigma Status (\s => Sigma (CF s) (\o => Step ((Prim1 z w) >- y) o)))
  search_prim1 Not (Abs x z)  y = <[PrimStep, (Abs x z), y, (Prim1 Not)]>
  search_prim1 Not (Rec x z)  y = <[PrimStep; (Rec x z); y; (Prim1 Not)]>
  search_prim1 Not (N k)      y = Nothing
  search_prim1 Not (Clos x z) y = Nothing
  search_prim1 Not (B x) y = Just $ (Done ** (B (not x) >- y ** PNot))
  search_prim1 Not (App x z)     y = [[y; (App x z); Prim1 Not; PrimStep]]
  search_prim1 Not (If x z w)    y = [[y; (If x z w); Prim1 Not; PrimStep]]
  search_prim1 Not (Prim1 x z)   y = [[y; (Prim1 x z); Prim1 Not; PrimStep]]
  search_prim1 Not (Prim2 z w s) y = [[y; (Prim2 z w s); Prim1 Not; PrimStep]]
  search_prim1 Not (Id x)        y = [[y; (Id x); Prim1 Not; PrimStep]]

  search_subst_env : (y : Env) -- Outer environment
                  -> (x : Env) -- Closure environment
                  -> (z : Exp Lam)
                  -> (k : Exp Done)
                  -> Maybe (Sigma Status
                                 (\s => Sigma (CF s)
                                              (\o => Step ((App (Clos x z) k) >- y) o)))
  search_subst_env y x (Abs iden w) k =
    Just $ (getTag w ** (w >- (insert iden (Left k) x) ** AppLam))

  search_app : (y : Env)
            -> (z : Exp a)
            -> (w : Exp b)
            -> Maybe (Sigma Status (\s => Sigma (CF s) (\o => Step ((App z w) >- y) o)))
  search_app y p@(Abs id body) w  = <[AppFunT, (Abs id body), y, (\clos => App clos w)]>
  search_app y (App e b)        w = [[y; (App e b); \s => App s w; AppFunT]]
  search_app y (If c t f)       w = [[y; (If c t f); \s => App s w; AppFunT]]
  search_app y (Prim1 op oa)    w = [[y; (Prim1 op oa); \s => App s w; AppFunT]]
  search_app y (Prim2 op o1 o2) w = [[y; (Prim2 op o1 o2); \s => App s w; AppFunT]]
  search_app y (Id x)           w = [[y; (Id x); \s => App s w; AppFunT]]
  search_app y (N k)            w = Nothing
  search_app y (B x)            w = Nothing
  search_app y (Rec x z)        w   = <[AppFunT; (Rec x z); y; (\clos => App clos w)]>
  search_app y (Clos x z) (Rec w s) = <[AppArgT; (Rec w s); y; (\arg => App (Clos x z) arg)]>
  search_app y (Clos x z) (App e b)        = [[y; App e b; App (Clos x z); AppArgT]]
  search_app y (Clos x z) (If c t f)       = [[y; If c t f; App (Clos x z); AppArgT]]
  search_app y (Clos x z) (Prim1 op oa)    = [[y; Prim1 op oa; App (Clos x z); AppArgT]]
  search_app y (Clos x z) (Prim2 op o1 o2) = [[y; Prim2 op o1 o2; App (Clos x z); AppArgT]]
  search_app y (Clos x z) (Id i)           = [[y; Id i; App (Clos x z); AppArgT]]
  search_app y (Clos x z) p@(Abs _ _)      = Just $ (Inter **
                                                     (App (Clos x z) (Clos y p) >- y **
                                                       AppArgT ClosLam))
  search_app y (Clos x z) p@(N k)          = search_subst_env y x z p
  search_app y (Clos x z) p@(B w)          = search_subst_env y x z p
  search_app y (Clos x z) p@(Clos w s)     = search_subst_env y x z p

max_stars_repo_name: ezrosent/FLK-Semantics

max_issues_repo_name: ezrosent/FLK-Semantics

max_forks_repo_name: ezrosent/FLK-Semantics


text:
import Language.Reflection

%language ElabReflection

solveReflected : TTImp -> Elab any
solveReflected `(Builtin.Equal {a=_} {b=_} ~(left) ~(right))
    = do logTerm "" 0 "Left" left
         logTerm "" 0 "Right" right
         fail "Not done"
solveReflected g
    = do logTerm "" 0 "Goal" g
         fail "I don't know how to prove this"

%macro
prove : Elab any
prove
    = do env <- localVars
         Just g <- goal
              | Nothing => fail "No goal to solve"
         logMsg "" 0 (show env)
         solveReflected g

commutes : (x, y : Nat) -> plus x y = plus y x
commutes x y = prove


text:
data Matter = Solid | Liquid | Gas

Eq Matter where
  (==) Solid Solid = True
  (==) Liquid Liquid = True
  (==) Gas Gas = True
  (==) _ _ = False

  (/=) x y = not (x == y)

occurences : Eq ty => (item : ty) -> (values : List ty) -> Nat
occurences item [] = 0
occurences item (value :: values) = case value == item of
                                         False => occurences item values
                                         True => 1 + occurences item values

data Tree elem = Empty
               | Node (Tree elem) elem (Tree elem)

Eq elem => Eq (Tree elem) where
  (==) Empty Empty = True
  (==) (Node left e right) (Node left' e' right')
      = left == left' && e == e' && right == right'
  (==) _ _ = False


text:
module System.Random

import Data.Fin
import Data.Vect
import Data.List

public export
interface Random a where
  randomIO : HasIO io => io a

  -- Takes a range (lo, hi), and returns a random value uniformly
  -- distributed in the closed interval [lo, hi]. It is unspecified what
  -- happens if lo > hi.
  randomRIO : HasIO io => (a, a) -> io a

%foreign "scheme:blodwen-random"
prim__randomInt : Int -> PrimIO Int

randomInt : Int -> IO Int
randomInt upperBound = fromPrim (prim__randomInt upperBound)

public export
Random Int where
  -- Generate a random value within [-2^31, 2^31-1].
  randomIO =
    let maxInt = shiftL 1 31 - 1
        minInt = negate $ shiftL 1 31
        range = maxInt - minInt
     in map (+ minInt) $ liftIO $ randomInt range

  -- Generate a random value within [lo, hi].
  randomRIO (lo, hi) =
    let range = hi - lo + 1
     in map (+ lo) $ liftIO $ randomInt range

%foreign "scheme:blodwen-random"
prim__randomDouble : PrimIO Double

randomDouble : IO Double
randomDouble = fromPrim prim__randomDouble

public export
Random Double where
  -- Generate a random value within [0, 1].
  randomIO = liftIO randomDouble

  -- Generate a random value within [lo, hi].
  randomRIO (lo, hi) = map ((+ lo) . (* (hi - lo))) (liftIO randomDouble)

%foreign "scheme:blodwen-random-seed"
prim__srand : Bits64 -> PrimIO ()

||| Sets the random seed
export
srand : Bits64 -> IO ()
srand n = fromPrim (prim__srand n)

||| Generate a random number in Fin (S `k`)
|||
||| Note that rndFin k takes values 0, 1, ..., k.
public export
rndFin : (n : Nat) -> IO (Fin (S n))
rndFin 0 = pure FZ
rndFin (S k) = do
  let intBound = the Int (cast (S k))
  randomInt <- randomRIO (0, intBound)
  pure $ restrict (S k) (cast randomInt)

||| Select a random element from a vector
public export
rndSelect' : {k : Nat} -> Vect (S k) a -> IO a
rndSelect' {k} xs = pure $ Vect.index !(rndFin k) xs

||| Select a random element from a non-empty list
public export
rndSelect : (elems : List a) -> {auto prf : NonEmpty elems} -> IO a
rndSelect (x :: xs) {prf = IsNonEmpty} = rndSelect' $ fromList (x :: xs)


text:
module Control.Monad.Indexed

import Control.Functor.Indexed
import Control.Applicative.Indexed

infixl 1 >>>=, =<<<, >>>, >>=>, <=<<

public export
interface IndexedApplicative z m => IndexedMonad z m | m where
  total
  bind : {0 i,j,k : z} -> m a i j -> (a -> m b j k) -> m b i k

  total
  join : {0 i,j,k : z} -> m (m a j k) i j -> m a i k

  -- default implementations
  bind x f = join (map f x)
  join x = bind x id

public export
(>>>=) : IndexedMonad z m => m a i j -> (a -> m b j k) -> m b i k
(>>>=) = bind

||| Flipped version of `>>>=`
public export
(=<<<) : IndexedMonad z m => (a -> m b j k) -> m a i j -> m b i k
(=<<<) = flip (>>>=)

||| Sequence effects taking the value of the second.
public export
(>>>) : IndexedMonad z m => m () i j -> Lazy (m b j k) -> m b i k
(>>>) x y = x >>>= \_ => y

||| Left-to-right Kleisli composition of indexed monads.
public export
(>>=>) : IndexedMonad z m => (a -> m b i j) -> (b -> m c j k) -> (a -> m c i k)
(>>=>) f g x = f x >>>= g

||| Right-to-left Kleisli composition of indexed monads, flipped version of `>=>`.
public export
(<=<<) : IndexedMonad z m => (b -> m c j k) -> (a -> m b i j) -> (a -> m c i k)
(<=<<) = flip (>>=>)

max_stars_repo_name: mattpolzin/idris-indexed

max_issues_repo_name: mattpolzin/idris-indexed

max_forks_repo_name: mattpolzin/idris-indexed


text:
module ArithCmd

import Data.Primitives.Views
import System

%default total

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

data Command : Type -> Type where
  PutStr  : String -> Command ()
  GetLine : Command String
  ReadFile: (filepath: String) -> Command (Either FileError String)
  WriteFile: (filepath: String) -> (content: String) -> Command (Either FileError ())
  Bind : Command a -> (a -> Command b) -> Command b
  Pure : a -> Command a

data ConsoleIO : Type -> Type where
  Quit : a -> ConsoleIO a
  Do   : Command a -> (a -> Inf(ConsoleIO b)) -> ConsoleIO b

data Input = Answer Int | QuitCmd
data ShellCmd = Cat String | Copy String String | ExitCmd

namespace CommandDo
  (>>=) : Command a -> (a -> Command b) -> Command b
  (>>=) = Bind

namespace ConsoleDo
  (>>=) : Command a -> (a -> Inf(ConsoleIO b)) -> ConsoleIO b
  (>>=) = Do

readInput: (prompt: String) -> Command Input
readInput prompt =
  do
    PutStr prompt
    answer <- GetLine
    if toLower answer == "quit"
      then Pure QuitCmd
      else Pure (Answer (cast answer))

splitBySpace : String -> List String
splitBySpace str = split (==' ') str

parseShellCmd : List String -> Either String ShellCmd
parseShellCmd []                 = Left "Pls input a command"
parseShellCmd ["exit"]           = Right ExitCmd
parseShellCmd ["cat",  filename] = Right (Cat filename)
parseShellCmd ["copy", src, dst] = Right (Copy src dst)
parseShellCmd (unsupported :: t) = Left ("Cmd [" ++ unsupported ++ "] is unsupported")

-- execShellCmd : ShellCmd -> ConsoleIO ()
-- execShellCmd (Cat file) =
  -- do
  --   result <- ReadFile file
  --   case result of
  --     (Left err)      => PutStr (show err)
  --     (Right content) => PutStr content
-- execShellCmd (Copy src dst) =
  -- do
  --   Right content <- ReadFile src          | Left err => PutStr (show err)
  --   Right _       <- WriteFile dst content | Left err => PutStr (show err)
  --   PutStr "file has been copied successfully"
-- execShellCmd ExitCmd = ?execShellCmd_rhs_3

readShellInput: (prompt: String) -> Command (Either String ShellCmd)
readShellInput prompt =
  do
    PutStr prompt
    cmdStr <- GetLine
    case parseShellCmd(splitBySpace(cmdStr)) of
      (Left err) => Pure (Left err)
      (Right cmd) => Pure (Right cmd)

runCommand : Command ty -> IO ty
runCommand (PutStr x)       = putStr x
runCommand GetLine          = getLine
runCommand (Bind cmdA func) =
  do
    res <- runCommand cmdA
    runCommand (func res)
runCommand (Pure x)         = pure x
runCommand (ReadFile path)  = readFile path
runCommand (WriteFile path cnt) = writeFile path cnt

run : Fuel -> ConsoleIO a -> IO (Maybe a)
run Dry      _                = pure Nothing
run (More fuel) (Quit res)    = pure (Just res)
run (More fuel) (Do cmd func) =
  do
    cmdRes <- runCommand cmd
    let res = func cmdRes
    run fuel res

scoreStr: (score: Nat) -> (attempts: Nat) -> String
scoreStr score attempts =
  "Score so far: " ++ show score ++ "/" ++ show attempts ++ "\n"

quiz : Stream Int -> (score: Nat) -> (attempts: Nat) -> ConsoleIO Nat
quiz (num1 :: num2 :: nums) score attempts =
  do
    PutStr (scoreStr score attempts)
    input <- readInput (show num1 ++ " * " ++ show num2 ++ " = ? ")
    case input of
      Answer answer =>
        if answer == num1 * num2
          then do PutStr ("Correct! ")
                  quiz nums (score + 1) (attempts + 1)
          else do PutStr ("Wrong! The answer is " ++ show (num1 * num2) ++ "\n")
                  quiz nums score (attempts + 1)
      QuitCmd  => Quit score

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
-- main: IO ()
-- main =
--   do
--     seed       <- time
--     Just score <- run forever (quiz (arithInputs(fromInteger seed)) 0 0)
--         | Nothing => putStrLn "Run out of fuel"
--     putStrLn ("Final score = " ++ show score)

shell : ConsoleIO ()
shell =
  do
    cmdOrErr <- readShellInput ":> "
    case cmdOrErr of
      (Left err)  => do PutStr err
                        shell
      (Right (Cat file)) => do result <- ReadFile file
                               case result of
                                  (Left err)      => PutStr (show err)
                                  (Right content) => PutStr content
                               shell
      (Right (Copy src dst)) => do readResult <- ReadFile src
                                   case readResult of
                                     (Left err) => PutStr (show err)
                                     (Right content) => do writeResult <- WriteFile dst content
                                                           case writeResult of
                                                            (Left err) => PutStr (show err)
                                                            (Right ()) => PutStr "file copied"
                                   shell
      (Right ExitCmd) => Quit ()

partial
main: IO ()
main =
  do
    Just val <- run forever shell
        | Nothing => putStrLn "Run out of fuel"
    putStrLn "Bye!"

max_stars_repo_name: coffius/idris-exercises

max_issues_repo_name: coffius/idris-exercises

max_forks_repo_name: coffius/idris-exercises


text:
module Types

-- WebGL Context
-- returned by canvasElement.getContext('webgl')
data GLCxt : Type where
  MkCxt : Ptr -> GLCxt

-- GL Buffer
-- returned by gl.createBuffer()
data GLBuffer : Type where
  MkBuf : Ptr -> GLBuffer

-- GL Program
-- For use with shaders etc
-- returned by gl.createProgram()
data GLProgram : Type where
  MkGLProg : Ptr -> GLProgram

-- JavaScript Float32Array()
-- returned by 'new Float32Array([0.3...])'
data F32Array : Type where
  MkF32Array : Ptr -> F32Array

-- Shader Types for keeping the type of shader
-- mixed with the actual shader code.
data Shader = Vertex String
            | Fragment String

-- Shader Program
-- returned by gl.createShader()
data ShaderProg : Type where
  MkShdrPrg : Ptr -> ShaderProg

-- Standard JavaScript Array
-- FFI Doesn't have full conversion for types and probably should stay that way imho.
-- returned by 'new Array()'
data JSArray : Type where
  MkJSArray : Ptr -> JSArray

-- HTML Element
-- Stolen from Idris/JavaScript
data Element : Type where
    MkElem : Ptr -> Element

max_stars_repo_name: mankyKitty/idris-webgl

max_issues_repo_name: mankyKitty/idris-webgl

max_forks_repo_name: mankyKitty/idris-webgl


text:
module Main

import Effects
import Effect.File

import Package
import PackageFormat

data InstallResult = Installed (List Pkg)
                   | NotReady
                   | Error String

installable : Pkg -> Bool
installable pkg = (length $ deps pkg) == 0 -- Make an implementation for Eq (List Dep) to speed this up!

--| TODO: Require that the Pkg be proven to be in the range of a PkgConstraint
install : (p : Pkg) -> Either String (IO ())
install pkg = Right $ do putStrLn $ "Cloning package " ++ pname pkg
                         putStrLn $ "Compiling package " ++ pname pkg
                         putStrLn $ "Installing package " ++ pname pkg

handle : Either String (IO ()) -> List Pkg -> IO InstallResult
handle (Left msg)  pkgs = return $ Error msg
handle (Right eff) pkgs = do eff
                             putStrLn "Done."
                             return $ Installed pkgs

prepare : Dep -> List Pkg -> List Pkg -> IO InstallResult
prepare (Dependency s c [])      pkgs srcs = case queryPkg s c srcs of
                                               Just pkg => handle (install $ record {deps = []} pkg) (record {deps = []} pkg :: pkgs)
                                               Nothing  => return $ Error $ "No package matching " ++ show (Dependency s c []) ++ " is available"
prepare (Dependency s c $ x::xs) pkgs srcs = case queryPkg' x srcs of
                                               Nothing  => return $ Error $ "No package matching " ++ show x ++ " is available"
                                               Just pkg => if pkg `elem` pkgs then prepare (Dependency s c xs) pkgs srcs
                                                           else do case !(prepare x pkgs srcs) of
                                                                     Installed pkgs' => prepare (Dependency s c xs) pkgs' srcs
                                                                     Error msg       => return $ Error msg
                                                                     NotReady        => prepare (Dependency s c $ xs ++ [x]) pkgs srcs
  where queryPkg' : Dep -> List Pkg -> Maybe Pkg
        queryPkg' (Dependency s v _) = queryPkg s v

main : IO ()
main = do let packages = [] -- Represents installed packages on system
          let H = Dependency "H" (Up $ V 3 5 0) []
          let D = Dependency "D" (Down $ V 1 7 0)
                    [ Dependency "F" (Exactly $ V 2 4 0) [H]
                    , Dependency "G" (Between (V 0 0 0)  (V 1 0 0)) [H]
                    ]
          let C = Dependency "C" Any [D]
          let B = Dependency "B" (Exactly $ V 1 4 1)
                    [ Dependency "E" (Exactly $ V 3 2 1) []
                    , C
                    ]
          let A = Dependency "A" (Exactly $ V 1 2 3) [B, C, D]
          let sources = [ Package "H" (V 3 5 1) "" "" "" "" None [] -- Represents database of available packages
                        , Package "H" (V 3 5 0) "" "" "" "" None []
                        , Package "D" (V 1 6 7) "" "" "" "" None []
                        , Package "F" (V 2 4 0) "" "" "" "" None []
                        , Package "G" (V 0 3 7) "" "" "" "" None []
                        , Package "C" (V 2 4 3) "" "" "" "" None []
                        , Package "B" (V 1 4 1) "" "" "" "" None []
                        , Package "E" (V 3 2 1) "" "" "" "" None []
                        , Package "A" (V 1 2 3) "" "" "" "" None []]
          case !(prepare A packages sources) of
            Installed pkgs => putStrLn $ "Successfully installed packages:" ++ show pkgs ++ "."
            Error msg      => putStrLn $ "Encountered error: '" ++ msg ++ "' while installing packages."
            NotReady       => putStrLn $ "Could not complete the request at this time. Packages may be broken."
          x <- run $ readPackage "pkg"
          putStrLn $ show x

max_stars_repo_name: nv-vn/Anvil

max_issues_repo_name: nv-vn/Anvil

max_forks_repo_name: nv-vn/Anvil


text:
module DataVect

import public Data.Fin
import Language.Reflection

%access public export
%default total

infixr 7 :>

data Vec : Nat -> Type -> Type where
  V0   :                 Vec  Z    a
  (:>) : a -> Vec n a -> Vec (S n) a

implementation Eq a => Eq (Vec n a) where
  (==)       V0        V0  = True
  (==) (l :> ls) (r :> rs) = l == r && ls == rs

implementation Show a => Show (Vec n a) where
  show       V0  = "V0"
  show (x :> xs) = show x ++ " :> " ++ show xs

vappend : Vec m a -> Vec n a -> Vec (m + n) a
vappend       V0  ys = ys
vappend (x :> xs) ys = x :> vappend xs ys

vtake : (m : Nat) -> Vec (m + n) a -> Vec m a
vtake  Z          xs  = V0
vtake (S k) (x :> xs) = x :> vtake k xs

vdrop : (n : Nat) -> Vec (n + m) a -> Vec m a
vdrop  Z          xs  =        xs
vdrop (S k) (x :> xs) = vdrop k xs

vlength : Vec n _ -> Nat
vlength {n} _ = n

vchop : (m : Nat) -> Vec (m + n) a -> (Vec m a, Vec n a)
vchop m xs = (vtake m xs, vdrop m xs)
{-
vchop' : (m : Nat) -> Vec (m + n) a -> (Vec m a, Vec n a)
vchop'  Z          xs  = (V0, xs)
vchop' (S k) (x :> xs) = (x :> Prelude.Basics.fst yszs, Prelude.Basics.snd yszs)
  where yszs = vchop' k xs
-}

-- TODO

arity : (n : Nat) -> (a : Type) -> Type
arity  Z    x = x
arity (S n) x = x -> arity n x

-- varity :: Arity n x -> Vec n x -> x
-- varity x       V0  =           x
-- varity f (x :> xs) = varity (f x) xs

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

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

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


text:
module Data.Optics.Iso

import Data.Optics.Prism

||| Isomorphism
data Iso s a =
  ||| create an isomorphism between s and a
  MkIso  (s -> a) (a -> s)

%name Iso iso, iso1, iso2

%default total

to: Iso s a -> s -> a
to (MkIso f g) s = f s

from: Iso s a -> a -> s
from (MkIso f g) a = g a

modify: (a -> a) -> (Iso s a) -> s -> s
modify f (MkIso to from) s = (from . f . to ) s

--
-- Compositions
--

infixr 9 -:+
||| compose two Isomorphisms
(-:+): Iso a b -> Iso s a -> Iso s b
x -:+ y = MkIso newTo newFrom
  where
    newTo: s -> b
    newTo  =  (to x . to y)
    newFrom: b -> s
    newFrom = (from y . from x)

infixr 9 +:-
(+:-) : (Iso s a) -> (Iso a b) -> (Iso s b)
(+:-) = flip (-:+)

max_stars_repo_name: justjoheinz/idris-optics

max_issues_repo_name: justjoheinz/idris-optics

max_forks_repo_name: justjoheinz/idris-optics


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

import Control.Monad.State
import Tree

-- check that all functions are total
%default total

testTree : Tree String
testTree = Node (Node (Node Empty "Jim" Empty) "Fred"
                      (Node Empty "Sheila" Empty)) "Alice"
                (Node Empty "Bob" (Node Empty "Eve" Empty))

namespace WithoutState

  treeLabelWith : Stream labelType -> Tree a ->
                  (Stream labelType, Tree (labelType, a))
  treeLabelWith lbs Empty = (lbs, Empty)
  treeLabelWith lbs (Node left val right)
    = let (lblthis :: lbsleft, lblleft) = treeLabelWith lbs left
          (lbsright, lblright) = treeLabelWith lbsleft right
          in
          (lbsright, Node lblleft (lblthis, val) lblright)

  treeLabel : Tree a -> Tree (Integer, a)
  treeLabel t = snd (treeLabelWith [1..] t)

namespace WithState

  treeLabelWith : Tree a -> State (Stream labelType) (Tree (labelType, a))
  treeLabelWith Empty = pure Empty
  treeLabelWith (Node left val right)
    = do lblleft <- treeLabelWith left
         (lblthis :: rest) <- get
         put rest
         lblright <- treeLabelWith right
         pure (Node lblleft (lblthis, val) lblright)

  treeLabel : Tree a -> Tree (Integer, a)
  treeLabel t = evalState (treeLabelWith t) [1..]

-- > :exec printLn $ WithoutState.treeLabel testTree
-- (4, "Alice")
-- |
-- +- (2, "Fred")
-- |  |
-- |  +- (1, "Jim")
-- |  |  |
-- |  |  +- *
-- |  |  |
-- |  |  `- *
-- |  |
-- |  `- (3, "Sheila")
-- |     |
-- |     +- *
-- |     |
-- |     `- *
-- |
-- `- (5, "Bob")
--    |
--    +- *
--    |
--    `- (6, "Eve")
--       |
--       +- *
--       |
--       `- *

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
foo : (pf : Nat -> Either (S Z = Z) (Z = S Z)) -> Z = S Z
foo  pf =
 let baz : Z = S Z
     baz  with (pf 0)
      baz | (Left Refl) impossible
      baz | (Right pf') = pf'
 in baz


text:
module LightClick.IR.Channel.Normalise.FreshBinders

import Data.List
import Data.Vect

import Toolkit.Data.Vect.Extra
import Toolkit.Data.DList
import Toolkit.Data.DVect

import LightClick.Types
import LightClick.Terms

import LightClick.IR.ModuleCentric
import LightClick.IR.ChannelCentric

import LightClick.IR.Channel.Normalise.Error
import LightClick.IR.Channel.Normalise.LetFloat

%default total

createModuleBinders : (state : List String)
                   -> (counter : Nat)
                   -> (expr  : ChannelIR type)
                            -> ChannelIR type
createModuleBinders state counter (CLet bind this inThis)
  = CLet bind this $ createModuleBinders (bind::state) counter inThis

createModuleBinders state counter (CSeq (CModuleInst mname xs) y)
  = CLet ("lightclick_module_" <+> show counter)
         (CModuleInst mname xs)
         (createModuleBinders state (S counter) y)

createModuleBinders state counter (CSeq (CNot o i) y)
  = CLet ("lightclick_module_" <+> show counter)
         (CNot o i)
         (createModuleBinders state (S counter) y)

createModuleBinders state counter (CSeq (CGate ty o ins) y)
  = CLet ("lightclick_module_" <+> show counter)
         (CGate ty o ins)
         (createModuleBinders state (S counter) y)

createModuleBinders state counter (CSeq x y)
  = CSeq (createModuleBinders state counter x) y

createModuleBinders state counter expr = expr

export
covering
freshBinders : (expr : ChannelIR type)
                    -> Normalise (ChannelIR type)
freshBinders expr
  = runLetFloat (createModuleBinders Nil Z expr)

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
||| Mathematicians often make an appeal to 'symmetry' to derive
||| variations on a lemma or theorem.
module Symmetry.Opposite

import Specifications.TranslationInvariance
import Specifications.Ring

%default total
%access export

private
oppAssoc : isAssociative op -> isAssociative (flip op)
oppAssoc spec x y z = sym (spec z y x)

namespace Monoid
  opposite : MonoidSpec op e -> MonoidSpec (flip op) e
  opposite (MkMonoid a l r) = MkMonoid (oppAssoc a) r l

namespace Group
  opposite : GroupSpec op e inv -> GroupSpec (flip op) e inv
  opposite (MkGroup m l r) = MkGroup (opposite m) r l

namespace PreRing
  multiplicativeOpposite : PreRingSpec add mul -> PreRingSpec add (flip mul)
  multiplicativeOpposite {add} {mul} (MkPreRing l r abel) =
    MkPreRing rop lop abel where
      rop : isDistributativeL add (flip mul)
      rop a x y = r x y a
      lop : isDistributativeR add (flip mul)
      lop x y a = l a x y

namespace Ring
  multiplicativeOpposite : RingSpec add zero neg mul ->
    RingSpec add zero neg (flip mul)
  multiplicativeOpposite (MkRing pre grp multassoc) =
    MkRing (multiplicativeOpposite pre) grp (oppAssoc multassoc)

namespace PartiallyOrderedMagma
  opposite : PartiallyOrderedMagmaSpec op leq ->
    PartiallyOrderedMagmaSpec (flip op) leq
  opposite (MkPartiallyOrderedMagma o l r) = MkPartiallyOrderedMagma o r l

namespace PartiallyOrderedGroup
  opposite : PartiallyOrderedGroupSpec op inv e leq ->
    PartiallyOrderedGroupSpec (flip op) inv e leq
  opposite (MkPartiallyOrderedGroup g m) =
    MkPartiallyOrderedGroup (opposite g) (opposite m)

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra