text:
||| Types and utilities for laying out components in a grid.
module Text.CSS.Grid

import Data.List
import Text.CSS.Length
import Text.CSS.Percentage
import Text.CSS.Render

--------------------------------------------------------------------------------
--          Flex Values
--------------------------------------------------------------------------------

public export
record Flex where
  constructor MkFlex
  value : Bits16

export %inline
fr : Cast Flex a => Bits16 -> a
fr = cast . MkFlex

export
Render Flex where
  render f = "\{show f.value}fr"

--------------------------------------------------------------------------------
--          MinMax Values
--------------------------------------------------------------------------------

public export
data MinMaxValue : Type where
  Auto       : MinMaxValue
  MML        : Length     -> MinMaxValue
  MMP        : Percentage -> MinMaxValue
  MMF        : Flex       -> MinMaxValue
  MinContent : MinMaxValue
  MaxContent : MinMaxValue

export %inline
Cast Length MinMaxValue where
  cast = MML

export %inline
Cast Percentage MinMaxValue where
  cast = MMP

export %inline
Cast Flex MinMaxValue where
  cast = MMF

export
Render MinMaxValue where
  render Auto       = "auto"
  render MinContent = "min-content"
  render MaxContent = "max-content"
  render (MML x)    = render x
  render (MMP x)    = render x
  render (MMF x)    = render x

--------------------------------------------------------------------------------
--          GridValue
--------------------------------------------------------------------------------

namespace GridValue
  public export
  data GridValue : Type where
    GL         : Length -> GridValue
    GP         : Percentage -> GridValue
    GF         : Flex -> GridValue
    MinMax     : (min,max : MinMaxValue) -> GridValue
    MaxContent : GridValue
    MinContent : GridValue

export
Render GridValue where
  render (GL x)           = render x
  render (GP x)           = render x
  render (GF x)           = render x
  render (MinMax min max) = "minmax(\{render min}, \{render max})"
  render MaxContent       = "max-content"
  render MinContent       = "min-content"

export
Render (List GridValue) where
  render = fastConcat . intersperse " " . map render

export %inline
Cast Length GridValue where
  cast = GL

export %inline
Cast Percentage GridValue where
  cast = GP

export %inline
Cast Flex GridValue where
  cast = GF

--------------------------------------------------------------------------------
--          GridPosition
--------------------------------------------------------------------------------

public export
data GridPosition : Type where
  At     : Bits32 -> GridPosition
  FromTo : Bits32 -> Bits32 -> GridPosition

export
Render GridPosition where
  render (At x)       = show x
  render (FromTo x y) = "\{show x} / \{show y}"


text:
module Language.LSP.CodeAction.AddClause

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Idris.IDEMode.CaseSplit
import Idris.REPL.Opts
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction.Utils
import Language.LSP.Message
import Server.Configuration
import Server.Log
import Server.Utils

buildCodeAction : URI -> TextEdit -> CodeAction
buildCodeAction uri edit =
  MkCodeAction
    { title       = "Add clause"
    , kind        = Just RefactorRewrite
    , diagnostics = Nothing
    , isPreferred = Nothing
    , disabled    = Nothing
    , edit        = Just $ MkWorkspaceEdit
        { changes           = Just (singleton uri [edit])
        , documentChanges   = Nothing
        , changeAnnotations = Nothing
        }
    , command     = Nothing
    , data_       = Nothing
    }

export
addClause : Ref LSPConf LSPConfiguration
         => Ref Ctxt Defs
         => Ref MD Metadata
         => Ref ROpts REPLOpts
         => Ref Syn SyntaxInfo
         => Ref UST UState
         => CodeActionParams -> Core (Maybe CodeAction)
addClause params = do
  logI AddClause "Checking for \{show params.textDocument.uri} at \{show params.range}"
  withSingleLine AddClause params (pure Nothing) $ \line => do

    Just clause <- getClause (line + 1) (UN "")
      | Nothing => do logD AddClause "No clause defined at line \{show line}"
                      pure Nothing

    -- FIXME: check where the declaration ends instead of putting it one line under the cursor
    let range = MkRange (MkPosition (line + 1) 0) (MkPosition (line + 1) 0)
    let edit = MkTextEdit range (clause ++ "\n")

    pure $ Just $ buildCodeAction params.textDocument.uri edit

ext: idr


text:
module Main

main : IO ()
main = do
  printLn $ lines "" == []
  printLn $ lines "\n" == [""]
  printLn $ lines "\n\n" == ["", ""]
  printLn $ lines "\n\n\n" == ["", "", ""]
  printLn $ lines "1\n2\n3" == ["1", "2", "3"]
  printLn $ lines "1\n2\n3\n" == ["1", "2", "3"]
  printLn $ unlines [] == ""
  printLn $ unlines ["1"] == "1\n"
  printLn $ unlines ["1", "2"] == "1\n2\n"
  printLn $ unlines ["1", "2", "3"] == "1\n2\n3\n"

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:
> module Fraction.NormalizeProperties

> import Syntax.PreorderReasoning

> import Fraction.Fraction
> import Fraction.BasicOperations
> import Fraction.Normalize
> import Fraction.Predicates
> import Fraction.Normal
> import Fraction.BasicProperties
> import Fraction.EqProperties
> import Fraction.LTEProperties
> import PNat.PNat
> import PNat.Operations
> import PNat.Properties
> import Nat.Positive
> import Basic.Operations
> import Nat.LTEProperties
> import Nat.LTProperties
> import Nat.OperationsProperties
> import Nat.GCD
> import Nat.GCDOperations
> import Nat.GCDProperties
> import Nat.Divisor
> import Nat.DivisorOperations
> import Nat.DivisorProperties
> import Nat.Coprime
> import Nat.CoprimeProperties
> import Nat.GCDAlgorithm
> import Nat.GCDEuclid
> import Pairs.Operations
> import Sigma.Sigma

> %default total
> %access public export
> -- %access export

Basic properties of |normalize|:

> |||
> normalNormalize : (x : Fraction) -> Normal (normalize x)
> normalNormalize (m, n') =
>   let n       :  Nat
>               =  toNat n' in
>   let zLTn    :  (Z `LT` n)
>               =  toNatLTLemma n' in
>   let d       :  Nat
>               =  gcdAlg m n in
>   let dGCDmn  :  (GCD d m n)
>               =  gcdAlgLemma m n in
>   let dDm     :  (d `Divisor` m)
>               =  gcdDivisorFst dGCDmn in
>   let dDn     :  (d `Divisor` n)
>               =  gcdDivisorSnd dGCDmn in
>   let zLTd    :  (Z `LT` d)
>               =  gcdPreservesPositivity2 zLTn (MkSigma d dGCDmn) in
>   MkNormal (gcdCoprimeLemma d m n dDm dDn zLTd dGCDmn)
> %freeze normalNormalize

> ||| Normalization of normal fraction is identity
> normalizePreservesNormal : (x : Fraction) -> Normal x -> normalize x = x
> normalizePreservesNormal (m, n') (MkNormal (MkCoprime prf)) =
>   let n       :  Nat
>               =  toNat n' in
>   let d       :  Nat
>               =  gcdAlg m n in
>   let dGCDmn  :  (GCD d m n)
>               =  gcdAlgLemma m n in
>   let dDm     :  (d `Divisor` m)
>               =  gcdDivisorFst dGCDmn in
>   let dDn     :  (d `Divisor` n)
>               =  gcdDivisorSnd dGCDmn in
>   let o       :  Nat
>               =  quotient m d dDm in
>   let p       :  Nat
>               =  quotient n d dDn in
>   let zLTn    :  (Z `LT` n)
>               =  toNatLTLemma n' in
>   let zLTp    :  (Z `LT` p)
>               =  quotientPreservesPositivity n d dDn zLTn in
>   let dEQ1    :  (d = S Z)
>               =  prf in
>
>     ( normalize (m, n') )
>   ={ Refl }=
>     ( (o, fromNat p zLTp) )
>   ={ cong2 (quotientAnyOneAny m d dDm dEQ1) (toNatEqLemma (quotientAnyOneAny n d dDn dEQ1)) }=
>     ( (m, n') )
>   QED
> %freeze normalizePreservesNormal

> ||| normalize is idempotent
> normalizeIdempotent : (x : Fraction) -> normalize (normalize x) = normalize x
> normalizeIdempotent x =
>     ( normalize (normalize x) )
>   ={ normalizePreservesNormal (normalize x) (normalNormalize x) }=
>     ( normalize x )
>   QED
> %freeze normalizeIdempotent

> |||
> normalizeUpscaleLemma : (x : Fraction) -> (e : PNat) -> normalize (upscale x e) = normalize x
> normalizeUpscaleLemma (m, d') e' =
>   let d              :  Nat
>                      =  toNat d' in
>   let g              :  Nat
>                      =  gcdAlg m d in
>   let gmd            :  (GCD g m d)
>                      =  gcdAlgLemma m d in
>   let gDm            :  (g `Divisor` m)
>                      =  gcdDivisorFst gmd in
>   let gDd            :  (g `Divisor` d)
>                      =  gcdDivisorSnd gmd in
>   let qmg            :  Nat
>                      =  quotient m g gDm in
>   let qdg            :  Nat
>                      =  quotient d g gDd in
>   let zLTd           :  (Z `LT` d)
>                      =  toNatLTLemma d' in
>   let zLTg           :  (Z `LT` g)
>                      =  gcdPreservesPositivity2 zLTd (MkSigma g gmd) in
>   let zLTqdg         :  (Z `LT` qdg)
>                      =  quotientPreservesPositivity d g gDd zLTd in
>   let e              :  Nat
>                      =  toNat e' in
>   let zLTe           :  (Z `LT` e)
>                      =  toNatLTLemma e' in
>   let ed             :  Nat
>                      =  toNat (e' * d') in
>   let h              :  Nat
>                      =  gcdAlg (e * m) ed in
>   let hemed          :  (GCD h (e * m) ed)
>                      =  gcdAlgLemma (e * m) ed in
>   let hDem           :  (h `Divisor` (e * m))
>                      =  gcdDivisorFst hemed in
>   let hDed           :  (h `Divisor` ed)
>                      =  gcdDivisorSnd hemed in
>   let qemh           :  Nat
>                      =  quotient (e * m) h hDem in
>   let qedh           :  Nat
>                      =  quotient ed h hDed in
>   let zLTed          :  (Z `LT` ed)
>                      =  toNatLTLemma (e' * d') in
>   let zLTqedh        :  (Z `LT` qedh)
>                      =  quotientPreservesPositivity ed h hDed zLTed in

>   let edEQed         :  (toNat (e' * d') = e * d)
>                      =  toNatMultLemma in
>   let hemed'         :  (GCD h (e * m) (e * d))
>                      =  replace {P = \ ZUZU => GCD h (e * m) ZUZU} edEQed hemed in
>   let hEQeg          :  (h = e * g)
>                      =  gcdScaleInvariant g m d h e gmd hemed' in
>   let egemed         :  (GCD (e * g) (e * m) (e * d))
>                      =  replace {P = \ ZUZU => GCD ZUZU (e * m) (e * d)} hEQeg hemed' in
>   let egDem          :  ((e * g) `Divisor` (e * m))
>                      =  gcdDivisorFst egemed in
>   let egDed          :  ((e * g) `Divisor` (e * d))
>                      =  gcdDivisorSnd egemed in
>   let qemeg          :  Nat
>                      =  quotient (e * m) (e * g) egDem in
>   let qedeg          :  Nat
>                      =  quotient (e * d) (e * g) egDed in
>   let zLTed'         :  (Z `LT` (e * d))
>                      =  multZeroLTZeroLT e d zLTe zLTd in
>   let zLTqedeg       :  (Z `LT` qedeg)
>                      =  quotientPreservesPositivity (e * d) (e * g) egDed zLTed' in
>   let nhEQZ          :  (Not (h = Z))
>                      =  gtZisnotZ (gcdPreservesPositivity2 zLTed (MkSigma h hemed)) in
>   let negEQZ         :  (Not (e * g = Z))
>                      =  gtZisnotZ (multZeroLTZeroLT e g zLTe zLTg) in
>   let qemhEQqemeg    :  (qemh = qemeg)
>                      =  quotientEqLemma (e * m) h hDem (e * m) (e * g) egDem Refl hEQeg nhEQZ in
>   let qedhEQqedeg    :  (qedh = qedeg)
>                      =  quotientEqLemma ed h hDed (e * d) (e * g) egDed edEQed hEQeg nhEQZ in
>   let qemegEQqmg     :  (qemeg = qmg)
>                      =  sym (quotientScaleInvariant m g e negEQZ gDm egDem) in
>   let qedegEQqdg     :  (qedeg = qdg)
>                      =  sym (quotientScaleInvariant d g e negEQZ gDd egDed) in
>   let qedh'          :  PNat
>                      =  fromNat qedh zLTqedh in
>   let qedeg'         :  PNat
>                      =  fromNat qedeg zLTqedeg in
>   let qedh'EQqedeg'  :  (qedh' = qedeg')
>                      =  toNatEqLemma {x = fromNat qedh zLTqedh} {y = fromNat qedeg zLTqedeg} qedhEQqedeg in
>   let qdg'           :  PNat
>                      =  fromNat qdg zLTqdg in
>   let qedeg'EQqdg'   :  (qedeg' = qdg')
>                      =  toNatEqLemma {x = fromNat qedeg zLTqedeg} {y = fromNat qdg zLTqdg} qedegEQqdg in
>
>     ( normalize (upscale (m, d') e') )
>   ={ Refl }=
>     ( normalize (m * e, d' * e') )
>   ={ cong {f = \ ZUZU => normalize (ZUZU, d' * e')} (multCommutative m e) }=
>     ( normalize (e * m, d' * e') )
>   ={ cong {f = \ ZUZU => normalize (e * m, ZUZU)} (multCommutative d' e') }=
>     ( normalize (e * m, e' * d') )
>   ={ Refl }=
>     ( (qemh, qedh') )
>   ={ cong {f = \ ZUZU => (ZUZU, qedh')} qemhEQqemeg }=
>     ( (qemeg, qedh') )
>   ={ cong {f = \ ZUZU => (qemeg, ZUZU)} qedh'EQqedeg' }=
>     ( (qemeg, qedeg') )
>   ={ cong {f = \ ZUZU => (ZUZU, qedeg')} qemegEQqmg }=
>     ( (qmg, qedeg') )
>   ={ cong {f = \ ZUZU => (qmg, ZUZU)} qedeg'EQqdg' }=
>     ( (qmg, qdg') )
>   ={ Refl }=
>     ( normalize (m, d') )
>   QED
> %freeze normalizeUpscaleLemma

Properties of |normalize|, |Eq|:

> |||
> normalizeEqLemma1 : (x : Fraction) -> (normalize x) `Eq` x
> normalizeEqLemma1 (m, n') =
>   let n     :  Nat
>             =  toNat n' in
>   let d     :  Nat
>             =  gcdAlg m n in
>   let v     :  (GCD d m n)
>             =  gcdAlgLemma m n in
>   let dDm   :  (d `Divisor` m)
>             =  gcdDivisorFst v in
>   let dDn   :  (d `Divisor` n)
>             =  gcdDivisorSnd v in
>
>  flipQuotientLemma m n d dDm dDn
> %freeze normalizeEqLemma1

> |||
> normalizeEqLemma2 : (x : Fraction) -> (y : Fraction) ->
>                     x `Eq` y -> normalize x = normalize y
> normalizeEqLemma2 (m1, n1') (m2, n2') m1n2EQm2n1 =
>   let n1  =  toNat n1' in
>   let n2  =  toNat n2' in
>
>     ( normalize (m1, n1') )
>   ={ sym (normalizeUpscaleLemma (m1, n1') n2') }=
>     ( normalize (m1 * n2, n1' * n2') )
>   ={ cong {f = \ ZUZU => normalize (ZUZU, n1' * n2')} m1n2EQm2n1 }=
>     ( normalize (m2 * n1, n1' * n2') )
>   ={ cong {f = \ ZUZU => normalize (m2 * n1, ZUZU)} (multCommutative n1' n2') }=
>     ( normalize (m2 * n1, n2' * n1') )
>   ={ normalizeUpscaleLemma (m2, n2') n1' }=
>     ( normalize (m2, n2') )
>   QED
> %freeze normalizeEqLemma2

Further properties of |normalize|:

> |||
> normalizePlusElimLeft : (x : Fraction) -> (y : Fraction) ->
>                         normalize (normalize x + y) = normalize (x + y)
> normalizePlusElimLeft x y =
>   let nxEqx   = normalizeEqLemma1 x in
>   let nxyEqxy = plusPreservesEq (normalize x) x y y nxEqx EqReflexive in
>   normalizeEqLemma2 (normalize x + y) (x + y) nxyEqxy
> %freeze normalizePlusElimLeft

> |||
> normalizePlusElimRight : (x : Fraction) -> (y : Fraction) ->
>                          normalize (x + normalize y) = normalize (x + y)
> normalizePlusElimRight x y =
>   let nyEqy   = normalizeEqLemma1 y in
>   let xnyEqxy = plusPreservesEq x x (normalize y) y EqReflexive nyEqy in
>   normalizeEqLemma2 (x + normalize y) (x + y) xnyEqxy
> %freeze normalizePlusElimRight

> |||
> normalizePlusElim : (x : Fraction) -> (y : Fraction) ->
>                     normalize (normalize x + normalize y) = normalize (x + y)
> normalizePlusElim x y =
>   let nxEqx   = normalizeEqLemma1 x in
>   let nyEqy   = normalizeEqLemma1 y in
>   let nxnyEqxy = plusPreservesEq (normalize x) x (normalize y) y nxEqx nyEqy in
>   normalizeEqLemma2 (normalize x + normalize y) (x + y) nxnyEqxy
> %freeze normalizePlusElim

> |||
> normalizeMultElimLeft : (x : Fraction) -> (y : Fraction) ->
>                         normalize ((normalize x) * y) = normalize (x * y)
> normalizeMultElimLeft x y =
>   let nxEqx   = normalizeEqLemma1 x in
>   let nxyEqxy = multPreservesEq (normalize x) x y y nxEqx EqReflexive in
>   normalizeEqLemma2 ((normalize x) * y) (x * y) nxyEqxy
> %freeze normalizeMultElimLeft

> |||
> normalizeMultElimRight : (x : Fraction) -> (y : Fraction) ->
>                          normalize (x * (normalize y)) = normalize (x * y)
> normalizeMultElimRight x y =
>   let nyEqy   = normalizeEqLemma1 y in
>   let xnyEqxy = multPreservesEq x x (normalize y) y EqReflexive nyEqy in
>   normalizeEqLemma2 (x * (normalize y)) (x * y) xnyEqxy
> %freeze normalizeMultElimRight

> |||
> normalizeMultElim : (x : Fraction) -> (y : Fraction) ->
>                     normalize ((normalize x) * (normalize y)) = normalize (x * y)
> normalizeMultElim x y =
>   let nxEqx   = normalizeEqLemma1 x in
>   let nyEqy   = normalizeEqLemma1 y in
>   let nxnyEqxy = multPreservesEq (normalize x) x (normalize y) y nxEqx nyEqy in
>   normalizeEqLemma2 ((normalize x) * (normalize y)) (x * y) nxnyEqxy
> %freeze normalizeMultElim

> |||
> normalizeLTELemma : (x : Fraction) -> (y : Fraction) ->
>                     x `LTE` y -> normalize x `LTE` normalize y
> normalizeLTELemma (nx, dx') (ny, dy') xLTEy = s11 where
>
>   dx  : Nat
>   dx  = toNat dx'
>   zLTdx : Z `LT` dx
>   zLTdx = toNatLTLemma dx'
>
>   dy  : Nat
>   dy  = toNat dy'
>   zLTdy : Z `LT` dy
>   zLTdy = toNatLTLemma dy'
>
>   gx  : Nat
>   gx  = gcdAlg nx dx
>   pgx : GCD gx nx dx
>   pgx = gcdAlgLemma nx dx
>   gxDnx : gx `Divisor` nx
>   gxDnx = gcdDivisorFst pgx
>   gxDdx : gx `Divisor` dx
>   gxDdx = gcdDivisorSnd pgx
>   zLTgx : Z `LT` gx
>   zLTgx = gcdPreservesPositivity2 zLTdx (MkSigma gx pgx)
>
>   gy  : Nat
>   gy  = gcdAlg ny dy
>   pgy : GCD gy ny dy
>   pgy = gcdAlgLemma ny dy
>   gyDny : gy `Divisor` ny
>   gyDny = gcdDivisorFst pgy
>   gyDdy : gy `Divisor` dy
>   gyDdy = gcdDivisorSnd pgy
>   zLTgy : Z `LT` gy
>   zLTgy = gcdPreservesPositivity2 zLTdy (MkSigma gy pgy)
>
>   nnx : Nat
>   nnx = quotient nx gx gxDnx
>   dnx : Nat
>   dnx = quotient dx gx gxDdx
>   zLTdnx : Z `LT` dnx
>   zLTdnx = quotientPreservesPositivity dx gx gxDdx zLTdx
>   dnx' : PNat
>   dnx' = fromNat dnx zLTdnx
>
>   nny : Nat
>   nny = quotient ny gy gyDny
>   dny : Nat
>   dny = quotient dy gy gyDdy
>   zLTdny : Z `LT` dny
>   zLTdny = quotientPreservesPositivity dy gy gyDdy zLTdy
>   dny' : PNat
>   dny' = fromNat dny zLTdny
>
>   nxdy : Nat
>   nxdy = nx * dy
>   nydx : Nat
>   nydx = ny * dx
>   gxgy : Nat
>   gxgy = gx * gy
>   gygx : Nat
>   gygx = gy * gx
>   gxgyDnxdy : gxgy `Divisor` nxdy
>   gxgyDnxdy = divisorMultLemma1 nx gx gxDnx dy gy gyDdy
>   gygxDnydx : gygx `Divisor` nydx
>   gygxDnydx = divisorMultLemma1 ny gy gyDny dx gx gxDdx
>   ngxgyZ : Not (gxgy = Z)
>   ngxgyZ = multNotZeroNotZero gx gy (gtZisnotZ zLTgx) (gtZisnotZ zLTgy)

>   s01 : LTE nxdy nydx
>   s01 = xLTEy
>   s02 : LTE ((quotient nxdy gxgy gxgyDnxdy) * gxgy) nydx
>   s02 = replace {P = \ ZUZ => LTE ZUZ nydx}
>                 (sym (quotientLemma' nxdy gxgy gxgyDnxdy)) s01
>   s03 : LTE ((quotient nxdy gxgy gxgyDnxdy) * gxgy) ((quotient nydx gygx gygxDnydx) * gygx)
>   s03 = replace {P = \ ZUZ => LTE ((quotient nxdy gxgy gxgyDnxdy) * gxgy) ZUZ}
>                 (sym (quotientLemma' nydx gygx gygxDnydx)) s02
>   s04 : LTE (quotient nxdy gxgy gxgyDnxdy) (quotient nydx gygx gygxDnydx)
>   s04 = elimRightMultLTE s03 (multCommutative gx gy) ngxgyZ
>   s05 : LTE ((quotient nx gx gxDnx) * (quotient dy gy gyDdy)) (quotient nydx gygx gygxDnydx)
>   s05 = replace {P = \ ZUZ => LTE ZUZ (quotient nydx gygx gygxDnydx)}
>                 (sym (quotientMultLemma nx gx gxDnx dy gy gyDdy)) s04
>   s06 : LTE ((quotient nx gx gxDnx) * (quotient dy gy gyDdy)) ((quotient ny gy gyDny) * (quotient dx gx gxDdx))
>   s06 = replace {P = \ ZUZ => LTE ((quotient nx gx gxDnx) * (quotient dy gy gyDdy)) ZUZ}
>                 (sym (quotientMultLemma ny gy gyDny dx gx gxDdx)) s05
>   s07 : LTE (nnx * dny) (nny * dnx)
>   s07 = s06
>   s08 : LTE (nnx * (toNat dny')) (nny * dnx)
>   s08 = replace {P = \ ZUZ => LTE (nnx * ZUZ) (nny * dnx)} (sym (toNatfromNatLemma dny zLTdny)) s07
>   s09 : LTE (nnx * (toNat dny')) (nny * (toNat dnx'))
>   s09 = replace {P = \ ZUZ => LTE (nnx * (toNat dny')) (nny * ZUZ)} (sym (toNatfromNatLemma dnx zLTdnx)) s08
>   s10 : (nnx, dnx') `LTE` (nny, dny')
>   s10 = s09
>   s11 : normalize (nx, dx') `LTE` normalize (ny, dy')
>   s11 = s10
> %freeze normalizeLTELemma

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Machine

import Syntax as S
import Effects
import Effect.Exception
import Data.List

public export
MName : Type
MName = S.Name

mutual
  export
  data MValue
    = MInt Integer
    | MBool Bool
    | MClosure MName Frame Env

  export
  implementation Show MValue where
    show (MInt n)         = show n
    show (MBool b)        = show b
    show (MClosure _ _ _) = "<fun>"

  public export
  data Instr
    = IMult
    | IAdd
    | ISub
    | IEqual
    | ILess
    | IVar MName
    | IInt Integer
    | IBool Bool
    | IClosure MName MName Frame
    | IBranch Frame Frame
    | ICall
    | IPopEnv

  ||| A stack of instructions.
  public export
  Frame : Type
  Frame = List Instr

  public export
  Env : Type
  Env = List (MName, Lazy MValue)

  Stack : Type
  Stack = List MValue

public export
MachineError : Type
MachineError = String

public export
MEff : Type -> Type
--MEff a = Eff a [EXCEPTION MachineError]
MEff a = Either MachineError a

error : String -> MEff b
--error msg = raise (MkMachineError msg)
error msg = Left msg

Environs : Type
Environs = List Env

lookup : MName -> Environs -> MEff MValue
lookup x envs = case head' envs of
  Just env => case lookup x env of
                Just v  => pure v
                Nothing => error $ "Unknown " ++ x
  Nothing  => error $ "No environment in which to lookup " ++ x

pop : Stack -> MEff (MValue, Stack)
pop [] = error "Empty stack"
pop (v :: vs) = pure $ (v, vs)

popBool : Stack -> MEff (Bool, Stack)
popBool (MBool b :: vs) = pure (b, vs)
popBool _               = error "Bool expected"

||| Pop a value and a closure from a stack
popApp : Stack -> MEff (MName, Frame, Env, MValue, Stack)
popApp (v :: MClosure n fr env :: vs) = pure (n, fr, env, v, vs)
popApp _                           = error "Value and closure expected"

mult : Stack -> MEff Stack
mult (MInt i2 :: MInt i1 :: vs) = pure $ MInt (i1 * i2) :: vs
mult _                          = error "int and int expected in mult"

add : Stack -> MEff Stack
add (MInt i2 :: MInt i1 :: vs) = pure $ MInt (i1 + i2) :: vs
add _                          = error "int and int expected in add"

sub : Stack -> MEff Stack
sub (MInt i2 :: MInt i1 :: vs) = pure $ MInt (i1 - i2) :: vs
sub _                          = error "int and int expected in sub"

equal : Stack -> MEff Stack
equal (MInt i2 :: MInt i1 :: vs) = pure $ MBool (i1 == i2) :: vs
equal _                          = error "int and int expected in equal"

less : Stack -> MEff Stack
less (MInt i2 :: MInt i1 :: vs) = pure $ MBool (i1 < i2) :: vs
less _                          = error "int and int expected in less"

Frames : Type
Frames = List Frame

buildClosure : Frames -> Stack -> Environs -> Env -> MName -> MName -> Frame -> (Frames, Stack, Environs)
buildClosure frames stack envs env fnm nm frame =
  (frames, c :: stack, envs)
    where c = MClosure nm frame ((fnm, c) :: env)

exec : Instr -> Frames -> Stack -> Environs -> MEff (Frames, Stack, Environs)
exec instr frames stack envs = case instr of
  -- Arithmetic operations.
  IMult => do stack' <- mult stack
              pure (frames, stack', envs)
  IAdd  => do stack' <- add stack
              pure (frames, stack', envs)
  ISub  => do stack' <- sub stack
              pure (frames, stack', envs)
  IEqual=> do stack' <- equal stack
              pure (frames, stack', envs)
  ILess => do stack' <- less stack
              pure (frames, stack', envs)
  -- Pushing values onto the stack.
  IVar nm  => do v <- lookup nm envs
                 pure $ (frames, v :: stack, envs)
  IInt n   => pure $ (frames, MInt n :: stack, envs)
  IBool b  => pure $ (frames, MBool b :: stack, envs)

  IClosure f nm frame =>
    case head' envs of
      Just env => pure $ buildClosure frames stack envs env f nm frame
      Nothing  => error "No environment for a closure"

  -- Control instructions.
  IBranch f1 f2 => do (b, stack') <- popBool stack
                      pure $ ((if b then f1 else f2) :: frames, stack', envs)

  ICall => do (nm, frame, env, v, stack') <- popApp stack
              pure $ (frame :: frames, stack', ((nm, v) :: env) :: envs)

  IPopEnv => case envs of
    _ :: envs' => pure (frames, stack, envs')
    _          => error "No environment to pop"

export
mrun : Frame -> Env -> MEff (MValue, Env)
mrun frame env = loop ([frame], [], [env])
  where
    loop : (Frames, Stack, Environs) -> MEff (MValue, Env)
    loop ([], [v], [env]) = pure (v, env)
    loop ((i::is) :: frames, stack, envs) = do r <- exec i (is::frames) stack envs
                                               loop r
    loop ([] :: frames, stack, envs) = loop (frames, stack, envs)

max_stars_repo_name: steshaw/idris-miniml

max_issues_repo_name: steshaw/idris-miniml

max_forks_repo_name: steshaw/idris-miniml


text:
module Postgres.Data.ConnectionStatus

public export
data ConnectionStatus = OK
                      | BAD
                      | STARTED
                      | MADE
                      | AWAITING_RESPONSE
                      | AUTH_OK
                      | SETENV
                      | SSL_STARTUP
                      | NEEDED
                      | OTHER Int

export
Show ConnectionStatus where
    show OK                = "OK"
    show BAD               = "BAD"
    show STARTED           = "STARTED"
    show MADE              = "MADE"
    show AWAITING_RESPONSE = "AWAITING_RESPONSE"
    show AUTH_OK           = "AUTH_OK"
    show SETENV            = "SETENV"
    show SSL_STARTUP       = "SSL_STARTUP"
    show NEEDED            = "NEEDED"
    show (OTHER x)         = "OTHER " ++ (show x)

max_stars_repo_name: mattpolzin/pg-idris

max_issues_repo_name: mattpolzin/pg-idris

max_forks_repo_name: mattpolzin/pg-idris


text:
--- Day 2: Dive! ---

module Dive
import System
import System.File
import Data.List
import Data.String
import Data.Either
import Data.String.Parser

Point : Type
Point = (Integer, Integer)

Point2 : Type
Point2 = (Integer, Point)

data Command = Forward Integer | Down Integer | Up Integer

implementation Show Command where
        show (Forward dx) = "Forward " ++ show dx
        show (Down dy) = "Down " ++ show dy
        show (Up dy) = "Up " ++ show dy

parseCommand : Parser Command
parseCommand = string "forward" *> space $> Forward <*> integer
           <|> string "down" *> space $> Down <*> integer
           <|> string "up" *> space $> Up <*> integer

parseCommands : Parser (List Command)
parseCommands = sepBy parseCommand $ char '\n'

move : (pos : Point) -> Command -> Point
move (x, y) cmd = case cmd of
                  (Forward dx) => (x + dx, y)
                  (Down dy) => (x, y + dy)
                  (Up dy) => (x, y - dy)

move2 : (pos : Point2) -> Command -> Point2
move2 (x, y, aim) cmd = case cmd of
                     (Forward dx) => (x + dx, y + aim * dx, aim)
                     (Down dy) => (x, y, aim + dy)
                     (Up dy) => (x, y, aim - dy)

eval : (cmds : List Command) -> Integer
eval = uncurry (*) . foldl move (0, 0)

eval2 : (cmds : List Command) -> Integer
eval2 cmds = let (x, y, _) = foldl move2 (0, 0, 0) cmds in x * y

main : IO ()
main = do
        args <- getArgs
        let (file :: _) = drop 1 args | [] => printLn "No file provided!"
        (Right symbols) <- readFile file | (Left error) => printLn error
        let (Right cmds) = parse parseCommands symbols | (Left error) => printLn error
        (printLn . eval . fst) cmds
        (printLn . eval2 . fst) cmds


text:
module Data.Word.Word8

-- We'll remove this module once Bits8 has more casts. Casting an Int to Integer
-- to cast to Bits8 isn't ideal.

-- TODO: Add modulo to base to incentivise backend support.
-- In Idris2 currently mod is really rem!
private
%foreign "scheme:modulo"
mod' : Int -> Int -> Int

private
mod256 : Int -> Int
mod256 x = mod' x 256

export
data Word8 : Type where
  W8 : Int -> Word8

private
fromInt : Int -> Word8
fromInt = W8 . mod256

%tcinline
private
fromInteger' : Integer -> Word8
fromInteger' = W8 . mod256 . cast

 -- might need to %tcinline this, depends how private affects things
private
%inline -- %spec or %inline? TODO: test each
word8Over : (f : Int -> Int -> Int) -> Word8 -> Word8 -> Word8
word8Over f (W8 x) (W8 y) = W8 $ mod256 (x `f` y)

export
implementation
Num Word8 where
  (+) = word8Over (+)
  (*) = word8Over (*)
  -- Careful, silently overflows as a literal.
  fromInteger x = if x >= 0 && x < 256
                    then W8 $ cast x
                    else fromInteger' x

export
implementation
Integral Word8 where
  mod = word8Over mod
  div = word8Over div

export
implementation
Neg Word8 where
  negate = word8Over (-) 0
  (-)    = word8Over (-)

export
implementation
Eq Word8 where
  W8 x == W8 y = x == y

export
implementation
Ord Word8 where
    W8 x `compare` W8 y = x `compare` y

export
implementation
Cast Int Word8 where
  cast = fromInt

export
implementation
Cast Word8 Int where
  cast (W8 i) = i

export
implementation
Cast Word8 Bits8 where
  cast = believe_me

export
implementation
Cast Bits8 Word8 where
  cast = W8 . believe_me

export
Show Word8 where
  show (W8 i) = show i


text:
import Data.Vect

append_nil : Vect m elem -> Vect (plus m 0) elem
append_nil {m} xs = rewrite plusZeroRightNeutral m in xs

append_xs : Vect (S (m + k)) elem -> Vect (plus m (S k)) elem
append_xs {m} {k} xs = rewrite sym
                       (plusSuccRightSucc m k) in xs

append : Vect n elem -> Vect m elem -> Vect (m + n) elem
append [] ys = append_nil ys
append (x :: xs) ys = append_xs (x :: append xs ys)


text:
||| Projection based on Plain Merge.
|||
||| The POPL '08 Paper /Multi-Party Asynchronous Session Types/.
||| When projecting a =Choice= in which the projected role is not involved,
||| projection occurs when all choices are equal.
module Sessions.Projection.Plain

import Decidable.Equality
import Data.List
import Data.List.Elem

import Data.List1

import Sessions.Meta

import Sessions.Global
import Sessions.Global.Involved

import Sessions.Local
import Sessions.Local.Same
import Sessions.Local.Same.All

import public Sessions.Projection.Error
import public Sessions.Projection

%default total

public export
data Merge : (this  : List1 (typeL, typeM, Local typeR typeL typeM rs g))
          -> (that  :                      Local typeR typeL typeM rs g)
                   -> Type
  where
    PMerge : (same : All ((cl,cm,c):::cs))
                  -> Merge ((cl,cm,c):::cs) c

public export
merge : DecEq typeR typeL typeM
     => (this : List1 (typeL, typeM, Local typeR typeL typeM rs g))
             -> Maybe (that ** Merge this that)
merge ((l,(m,c)) ::: tail) with (allSame ((l,(m,c)) ::: tail))
  merge ((l,(m,c)) ::: tail) | (Yes prf)
    = Just (c ** PMerge prf)
  merge ((l,(m,c)) ::: tail) | (No contra)
    = Nothing

public export
project : DecEq typeR typeL typeM
       => {rs    : List Ty}
       -> {g     :      Ty}
       -> (role  : typeR)
       -> (termG : Global typeR typeL typeM rs g)
                -> Maybe (termL ** Project Merge role termG termL)
project = Projection.Term.project merge

-- [ EOF ]

max_stars_repo_name: DSbD-AppControl/sessions-playground

max_issues_repo_name: DSbD-AppControl/sessions-playground

max_forks_repo_name: DSbD-AppControl/sessions-playground


text:
module Circuits.NetList.Linear.Usage.DataType.Use.Partial

import Decidable.Equality

import Data.Nat
import Data.List.Elem
import Data.List.Quantifiers

import Data.Vect
import Data.Vect.AtIndex
import Data.Vect.Quantifiers

import Data.String

import Toolkit.Data.Whole
import Toolkit.Data.DList
import Toolkit.Data.DList.Elem

import Toolkit.Data.Vect.Extra

import Circuits.Common
import Circuits.NetList.Types
import Circuits.NetList.Linear.Usage.DataType

import Circuits.NetList.Linear.Usage.DataType.Use.Full

%default total

mutual
  public export
  data Use : (idx  : Fin m)

          -> (type : DType)
          -> (old  : Usage        (BVECT (W (S n) ItIsSucc) type))
          -> (prfF : IsFreeAt idx (BVECT (W (S n) ItIsSucc) type)  old)

          -> (new  : Usage        (BVECT (W (S n) ItIsSucc) type))
          -> (prfU : IsUsedAt idx (BVECT (W (S n) ItIsSucc) type)  new)
                  -> Type
    where
      UA : Use idx type        fs          prfFS         us          prfUS
        -> Use idx type (Array fs) (FreeAt prfFS) (Array us) (UsedAt prfUS)

  public export
  data Result : (idx  : Fin m)
             -> (type : DType)
             -> (old  : Usage        (BVECT (W (S n) ItIsSucc) type))
             -> (free : IsFreeAt idx (BVECT (W (S n) ItIsSucc) type)  old)
                     -> Type
    where
      R : (new   : Usage        (BVECT (W (S n) ItIsSucc) type))
       -> (prfU  : IsUsedAt idx (BVECT (W (S n) ItIsSucc) type)         new)
       -> (holds : Use      idx                           type old prfF new prfU)
                -> Result   idx                           type old prfF

  namespace Vect
    public export
    data Use : (idx  : Fin  m)
            -> (type : DType)
            -> (old  : Vect n   (Usage type))
            -> (this : AtIndexI (Usage type) (IsFree type) m n idx old)
            -> (new  : Vect n   (Usage type))
            -> (that : AtIndexI (Usage type) (IsUsed type) m n idx new)
                    -> Type
      where
        Here : (use : Use    type  f                prfF    u                prfU)
                   -> Use FZ type (f::fs) (At (Here prfF)) (u::fs) (At (Here prfU))

        Next : Use     next  type         fs  (At        next_f)          us  (At        next_u)
            -> Use (FS next) type (not_f::fs) (At (There next_f)) (not_u::us) (At (There next_u))

    public export
    data Result : (idx  : Fin m)
               -> (type : DType)
               -> (old  : Vect n (Usage type))
               -> (this : AtIndexI (Usage type) (IsFree type) m n idx old)
                       -> Type
      where
        R : (new   : Vect n   (Usage type))
         -> (prfU  : AtIndexI (Usage type) (IsUsed type) m n idx new)
         -> (holds : Use    idx type old this new prfU)
                  -> Result idx type old this

mutual

  use : {type : DType}
     -> (idx  : Fin m)
     -> {old  : Usage        (BVECT (W (S n) ItIsSucc) type)}
     -> (free : IsFreeAt idx (BVECT (W (S n) ItIsSucc) type) old)
             -> Result   idx                           type old free
  use idx (FreeAt prf) with (use idx prf)
    use idx (FreeAt prf) | (R new prfU holds)
      = R (Array new) (UsedAt prfU) (UA holds)

  namespace Vect

    export
    use : {type : DType}
       -> (idx  : Fin m)
       -> {old  : Vect n (Usage type)}
       -> (this : AtIndexI (Usage type) (IsFree type) m n idx old)
               -> Result idx type old this
    use FZ {old=(x :: xs)} (At (Here prf)) with (use prf)
      use FZ {old=(x :: xs)} (At (Here prf)) | (R u used result)
        = R (u :: xs) (At (Here used)) (Here result)

    use (FS next) {old=(not_x :: xs)} (At (There later)) with (use next (At later))
      use (FS next) {old=(not_x :: xs)} (At (There later)) | (R new (At x) holds)
        = R (not_x :: new) (At (There x)) (Next holds)

-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Main

printLength : IO ()
printLength = do putStr "Input string: "
                 input <- getLine
                 let len = length input
                 putStrLn (show len)

main : IO ()
main = do
  putStr "Enter your name: "
  x <- getLine
  putStrLn ("Hello " ++ x ++ "!")

max_stars_repo_name: brunoflores/type-driven-with-idris

max_issues_repo_name: brunoflores/type-driven-with-idris

max_forks_repo_name: brunoflores/type-driven-with-idris


text:
module Determinism

import BigStep
import Progress
import Step
import Subst
import Term
import Equivalence

%default total
%access export

stepDeterministic : (Step e1 e2) -> (Step e1 e3) ->
                    e2 = e3
-- case split in the following order: (Step e1 e2), (Step e1 e3)
stepDeterministic {e1 = TRec _ e10 e11} (StRec x) (StRec y) =
  cong {f = \e => TRec e e10 e11} $ stepDeterministic x y
--
stepDeterministic (StRec x) (StRecSucc y) = absurd $ valueIrreducible _ y x
--
stepDeterministic StRecZero StRecZero = Refl
--
stepDeterministic (StRecSucc x) (StRec y) = absurd $ valueIrreducible _ x y
--
stepDeterministic (StRecSucc x) (StRecSucc y) = Refl
--
stepDeterministic {e1 = TApp _ e11} (StApp1 x) (StApp1 y) =
  cong {f = \e => TApp e e11} $ stepDeterministic x y
--
stepDeterministic (StApp1 x) (StApp2 y z) = absurd $ valueIrreducible _ y x
--
stepDeterministic (StApp1 x) (StBeta y) = absurd $ valueIrreducible _ VAbs x
--
stepDeterministic (StApp2 x z) (StApp1 y) = absurd $ valueIrreducible _ x y
--
stepDeterministic {e1 = TApp e11 _} (StApp2 x z) (StApp2 y w) =
  cong {f = \e => TApp e11 e} $ stepDeterministic z w
--
stepDeterministic (StApp2 x z) (StBeta y) = absurd $ valueIrreducible _ y z
--
stepDeterministic (StBeta x) (StApp2 y z) = absurd $ valueIrreducible _ x z
--
stepDeterministic (StBeta x) (StBeta y) = Refl
--
stepDeterministic (StSucc x) (StSucc y) = cong $ stepDeterministic x y
--
stepDeterministic (StPred x) (StPred y) = cong $ stepDeterministic x y
--
stepDeterministic (StPred x) StPredZero = absurd $ valueIrreducible _ VZero x
--
stepDeterministic (StPred x) (StPredSucc y) = absurd $ valueIrreducible _ (VSucc y) x
--
stepDeterministic StPredZero (StPred x) = absurd $ valueIrreducible _ VZero x
--
stepDeterministic StPredZero StPredZero = Refl
--
stepDeterministic (StPredSucc x) (StPred y) = absurd $ valueIrreducible _ (VSucc x) y
--
stepDeterministic (StPredSucc x) (StPredSucc y) = Refl
--
stepDeterministic {e1 = TIfz _ e12 e13} (StIfz x) (StIfz y) =
  cong {f = \e => TIfz e e12 e13} $ stepDeterministic x y
--
stepDeterministic (StIfz x) StIfzZero = absurd $ valueIrreducible _ VZero x
--
stepDeterministic (StIfz x) (StIfzSucc y) = absurd $ valueIrreducible _ (VSucc y) x
--
stepDeterministic StIfzZero (StIfz x) = absurd $ valueIrreducible _ VZero x
--
stepDeterministic StIfzZero StIfzZero = Refl
--
stepDeterministic (StIfzSucc x) (StIfz y) = absurd $ valueIrreducible _ (VSucc x) y
--
stepDeterministic (StIfzSucc x) (StIfzSucc y) = Refl

transStepDeterministic : (v2 : Value e2) -> (TransStep e1 e2) ->
                         (v3 : Value e3) -> (TransStep e1 e3) ->
                         e2 = e3
transStepDeterministic v2 (TStRefl e3) v3 (TStRefl e3) = Refl
--
transStepDeterministic v2 (TStRefl e2) v3 (TStTrans x y) =
  absurd $ valueIrreducible e2 v2 x
--
transStepDeterministic v2 (TStTrans x z) v3 (TStRefl e3) =
  absurd $ valueIrreducible e3 v3 x
--
transStepDeterministic {e2 = e2} v2 (TStTrans x z) v3 (TStTrans y w) =
  let eq = stepDeterministic x y
      z' = replace {P = \x => x} (cong {f = \e => TransStep e e2} eq) z
  in transStepDeterministic v2 z' v3 w

-- The following proof of the determinism of 'BigStep'
-- relies on the equivalence of 'Step' and 'BigStep'.
bigStepDeterministic' : (BigStep e1 e2) ->
                        (BigStep e1 e3) ->
                        e2 = e3
bigStepDeterministic' x y =
  let (tst2, v2) = bigStepToTransStep x
      (tst3, v3) = bigStepToTransStep y
  in transStepDeterministic v2 tst2 v3 tst3

injectiveAbs : (TAbs e1 = TAbs e2) -> e1 = e2
injectiveAbs Refl = Refl

injectiveSucc : (TSucc e1 = TSucc e2) -> e1 = e2
injectiveSucc Refl = Refl

zeroNotSucc : (TZero = TSucc _) -> Void
zeroNotSucc Refl impossible

pairEq : a = b -> c = d -> (a, c) = (b, d)
pairEq Refl Refl = Refl

valueBigStepEq : Value e1 -> BigStep e1 e2 -> e1 = e2
valueBigStepEq VZero (BStValue _)     = Refl
valueBigStepEq (VSucc x) (BStValue _) = Refl
valueBigStepEq (VSucc x) (BStSucc y)  = cong $ valueBigStepEq x y
valueBigStepEq VAbs (BStValue _)      = Refl

bigStepDeterministic : (BigStep e1 e2) -> (BigStep e1 e3) ->
                       e2 = e3
-- case split in the following order: (BigStep e1 e2), (BigStep e1 e3)
bigStepDeterministic (BStRecZero y z) (BStValue _) impossible
--
bigStepDeterministic (BStRecZero y z) (BStRecZero w s) = bigStepDeterministic z s
--
bigStepDeterministic (BStRecZero y z) (BStRecSucc x w) =
  let ih = bigStepDeterministic y x
  in absurd $ zeroNotSucc ih
--
bigStepDeterministic (BStRecSucc x y) (BStValue _) impossible
--
bigStepDeterministic (BStRecSucc x y) (BStRecZero w s) =
  let ih = bigStepDeterministic x w
  in absurd $ zeroNotSucc $ sym ih
--
bigStepDeterministic {e1 = TRec e e10 e11} {e2 = e2} (BStRecSucc x y) (BStRecSucc z w) =
  let ih = injectiveSucc $ bigStepDeterministic x z
      y' = replace {P = \x => BigStep (subst x FZ (subst (TRec x e10 e11) FZ e11)) e2} ih y
  in bigStepDeterministic y' w
--
bigStepDeterministic (BStValue _) (BStValue _) = Refl
--
bigStepDeterministic (BStValue _) (BStApp z w t) impossible
--
bigStepDeterministic (BStValue v2) (BStSucc x) = case v2 of
  VAbs      impossible
  VZero     impossible
  VSucc v2' => cong $ valueBigStepEq v2' x
--
bigStepDeterministic (BStValue _) (BStPredZero y) impossible
--
bigStepDeterministic (BStValue _) (BStPredSucc x) impossible
--
bigStepDeterministic (BStValue _) (BStIfzZero z w) impossible
--
bigStepDeterministic (BStValue _) (BStIfzSucc w s) impossible
--
bigStepDeterministic (BStApp w t u) (BStValue _) impossible
--
bigStepDeterministic {e2 = e2} (BStApp w t u) (BStApp z s v) =
  let ih1 = injectiveAbs $ bigStepDeterministic w z
      ih2 = bigStepDeterministic t s
      peq = pairEq ih1 ih2
      u'  = replace {P = \x => BigStep (subst (snd x) FZ (fst x)) e2} peq u
  in bigStepDeterministic u' v
--
bigStepDeterministic (BStSucc x) (BStValue v3) = case v3 of
  VAbs      impossible
  VZero     impossible
  VSucc v3' => cong . sym $ valueBigStepEq v3' x
--
bigStepDeterministic (BStSucc x) (BStSucc y) = cong $ bigStepDeterministic x y
--
bigStepDeterministic (BStPredZero z) (BStValue _) impossible
--
bigStepDeterministic (BStPredZero z) (BStPredZero y) = Refl
--
bigStepDeterministic (BStPredZero z) (BStPredSucc x) =
  let ih = bigStepDeterministic z x
  in absurd $ zeroNotSucc ih
--
bigStepDeterministic (BStPredSucc x) (BStValue _) impossible
--
bigStepDeterministic (BStPredSucc x) (BStPredZero z) =
  let ih = bigStepDeterministic x z
  in absurd $ zeroNotSucc (sym ih)
--
bigStepDeterministic (BStPredSucc x) (BStPredSucc y) = injectiveSucc $ bigStepDeterministic x y
--
bigStepDeterministic (BStIfzZero w s) (BStValue _) impossible
--
bigStepDeterministic (BStIfzZero w s) (BStIfzZero y z) = bigStepDeterministic s z
--
bigStepDeterministic (BStIfzZero w s) (BStIfzSucc z t) =
  let ih = bigStepDeterministic w z
  in absurd $ zeroNotSucc ih
--
bigStepDeterministic (BStIfzSucc s t) (BStValue _) impossible
--
bigStepDeterministic (BStIfzSucc s t) (BStIfzZero y z) =
  let ih = bigStepDeterministic s y
  in absurd $ zeroNotSucc (sym ih)
--
bigStepDeterministic (BStIfzSucc s t) (BStIfzSucc z w) = bigStepDeterministic t w

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module Matrixes

import Data.Vect

sum : Num numType => Vect rows (Vect cols numType) ->
                     Vect rows (Vect cols numType) ->
                     Vect rows (Vect cols numType)


text:
module Optimisation.Untupling

import Data.SortedSet
import Data.SortedMap
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import Core.Context
import Data.List
import CommonDef
import Primitives.Externals
import CairoCode.Traversal.Base
import CairoCode.Traversal.Composition
import Utils.Lens
import CairoCode.Traversal.ValueTracker
import Debug.Trace

%hide Prelude.toList

-- Todo: Rename to ReturnUntupler
-- Todo: Make ParamUntupler : Only if tupled then called then untupled (& tupled is not needed except by projets)
--       We need ensure that we not untuple over more than one call border (otherwise it gets more expensive)

-- Collects all functions that are underApplied
underAppliedFunctionsDefs : List (Name, CairoDef) -> SortedSet Name
underAppliedFunctionsDefs defs = snd $ runVisitConcatCairoDefs (pureTraversal underApplyCollectorTraversal) defs
    where underApplyCollectorTraversal : InstVisit CairoReg -> SortedSet Name
          underApplyCollectorTraversal (VisitMkClosure _ name _ _) = singleton name
          underApplyCollectorTraversal _ = empty

-- Collects all functions that are fullyApplied
fullyAppliedFunctionsDefs : List (Name, CairoDef) -> SortedSet Name
fullyAppliedFunctionsDefs defs = snd $ runVisitConcatCairoDefs (pureTraversal fullApplyCollectorTraversal) defs
    where fullApplyCollectorTraversal : InstVisit CairoReg -> SortedSet Name
          fullApplyCollectorTraversal (VisitCall _ _ name _) = singleton name
          fullApplyCollectorTraversal _ = empty

-- Data to represent Tupling Information internally
data UntupleInfo : Type where
 Undecided : UntupleInfo                                -- It is not known yet if this can be untupled or not
 Candidate : Int -> List UntupleInfo -> UntupleInfo     -- It is a Candidate for being untupled nothing speaks against it for now
 Untouched : UntupleInfo                                -- This can or should not be Untupled, either something prevents or we are not sure (recursion)

toUntupleInfo : TupleStructure -> UntupleInfo
toUntupleInfo (Tupled t fields) = Candidate t (map toUntupleInfo fields)
toUntupleInfo ReturnValue = Untouched

untupledExtPrimDefs : List (Name, CairoDef) -> SortedMap Name UntupleInfo
untupledExtPrimDefs defs = fromList ((toList $ snd $ runVisitConcatCairoDefs (pureTraversal allExistingExtPrims) defs) >>= resolveUtInfo)
    where allExistingExtPrims : InstVisit CairoReg -> SortedSet Name
          allExistingExtPrims (VisitExtprim _ _ name _) = singleton name
          allExistingExtPrims _ = empty
          resolveUtInfo : Name -> List (Name, UntupleInfo)
          resolveUtInfo name = case (externalTupleSig name) of
            Nothing => Nil
            (Just ts) => [(name, toUntupleInfo ts)]

-- Collects tail Constructs and tail Calls (including EXTPRIM)

mergeUntupleInfo : UntupleInfo -> UntupleInfo -> UntupleInfo
mergeUntupleInfo Untouched _ = Untouched
mergeUntupleInfo _ Untouched = Untouched
mergeUntupleInfo Undecided b = b
mergeUntupleInfo a Undecided = a
mergeUntupleInfo (Candidate t1 fs1) (Candidate t2 fs2) = if t1 /= t2 || (length fs1) /= (length fs2)
    then Untouched
    else Candidate t1 (zipWith mergeUntupleInfo fs1 fs2)

Semigroup UntupleInfo where (<+>) = mergeUntupleInfo
Monoid UntupleInfo where neutral = Undecided

-- Assign is deliberately not tracked as then all untupled args need to be assigned (making matter worse than better)
extractUntupleInfoDef : SortedMap Name UntupleInfo -> (Name, CairoDef) -> Maybe UntupleInfo
-- Ignore already untupled
extractUntupleInfoDef resolved def@(_, FunDef _ _ [_] _) = snd (runVisitConcatCairoDef (traversal $ valueCollector idLens (dbgDef def) (passThroughImpls $ defaultNoImplValBind (\_ => Untouched) tupledReturnTracker) returnCollector) def)
    where dbgDef : (Name, CairoDef) -> CairoReg -> UntupleInfo
          dbgDef (name, def) reg = trace "Register not bound in \{show name}: \{show reg}" Undecided
          tupledReturnTracker : (v:InstVisit UntupleInfo) -> Traversal (ScopedBindings UntupleInfo) (Maybe (NoImplValBindType v UntupleInfo))
          tupledReturnTracker (VisitMkCon _ tag args) = pure $ Just $ Candidate (fromMaybe 0 tag) args
          tupledReturnTracker (VisitCall [r] _ name _ ) = pure $ Just [fromMaybe Undecided (lookup name resolved)]
          tupledReturnTracker (VisitExtprim [r] _ name _ ) = pure $ Just [fromMaybe Undecided (lookup name resolved)]
          tupledReturnTracker _ = pure $ Nothing
          returnCollector : InstVisit UntupleInfo -> Traversal (ScopedBindings UntupleInfo) (Maybe UntupleInfo)
          returnCollector (VisitReturn [singleRes] _) = pure $ Just singleRes
          returnCollector (VisitReturn _ _) = pure $ Just Untouched -- already untupled
          returnCollector _ = pure Nothing
          Semigroup (Maybe UntupleInfo) where
            (<+>) Nothing res = res
            (<+>) res Nothing = res
            (<+>) (Just res1) (Just res2)  = Just (res1 <+> res2)
          Monoid (Maybe UntupleInfo) where neutral = Nothing
extractUntupleInfoDef _ (_, ForeignDef (MkForeignInfo _ ut _ _ _) _ 1) = map toUntupleInfo ut
extractUntupleInfoDef _ _  = Nothing

-- Here is the iterative tupler analysis

-- Like merge Info but changes are only allowed from: Undecided -> Candidate -> Untouched
--  Ensures that the iterative algorithm terminates
--  The Bool is false if (snd (mergeInfoUp old new)) == old and true otherwise
mergeInfoUp : (old:UntupleInfo) -> (new:UntupleInfo) -> (Bool, UntupleInfo)
mergeInfoUp a Undecided = (False, a)
mergeInfoUp Undecided b = (True, b)
mergeInfoUp Untouched _ = (False, Untouched)
mergeInfoUp _ Untouched = (True, Untouched)
mergeInfoUp (Candidate t1 fs1) (Candidate t2 fs2) = if t1 /= t2 || (length fs1) /= (length fs2)
    then (True, Untouched)
    else (any fst zipped, Candidate t1 (map snd zipped))
  where zipped : List (Bool, UntupleInfo)
        zipped = zipWith mergeInfoUp fs1 fs2

runFindTuplingTargetDef : SortedMap Name UntupleInfo -> (Name, CairoDef) -> (Bool, SortedMap Name UntupleInfo)
runFindTuplingTargetDef info d@(name,def) = (reinsertInfo (mergeInfo (extractUntupleInfoDef info d)))
    where mergeInfo : Maybe UntupleInfo -> Maybe (Bool, UntupleInfo)
          mergeInfo Nothing = Nothing
          mergeInfo (Just inf) = Just (mergeInfoUp (fromMaybe Undecided (lookup name info)) inf)
          reinsertInfo : Maybe (Bool, UntupleInfo) -> (Bool, SortedMap Name UntupleInfo)
          reinsertInfo (Just (mod, inf)) = (mod, insert name inf info)
          reinsertInfo Nothing = (False, info)

runFindTuplingTargetDefs : SortedMap Name UntupleInfo -> List (Name, CairoDef) -> (Bool, SortedMap Name UntupleInfo)
runFindTuplingTargetDefs info defs = foldl processDef (False,info) defs
    where processDef : (Bool, SortedMap Name UntupleInfo) -> (Name, CairoDef) -> (Bool, SortedMap Name UntupleInfo)
          processDef (mod, inf) def = let (lmod, ninf) = runFindTuplingTargetDef inf def in (mod || lmod, ninf)

-- runs runFindTuplingTargetDefs until nothing changed
iterFindTuplingTargetDefs : SortedMap Name UntupleInfo -> List (Name, CairoDef) -> SortedMap Name UntupleInfo
iterFindTuplingTargetDefs info defs = if fst singleRun
    then iterFindTuplingTargetDefs (snd singleRun) defs
    else snd singleRun
    where singleRun : (Bool, SortedMap Name UntupleInfo)
          singleRun = runFindTuplingTargetDefs info defs

-- Here is the Closure rewiring

record TupGenRes where
  constructor MkTupGenRes
  regGen: RegisterGen
  regs: List CairoReg
  code: List CairoInst

-- Generates code to build the tuple described by UntupleInfo and assign it to trg.
--  src contains the fields, however it may contain more the rest is returned

generateRetupling : RegisterGen -> (depth:Int) -> UntupleInfo -> (resReg: CairoReg) -> TupGenRes
generateRetupling regGen depth (Candidate tag fields) resReg = produceRes (foldl processField ([], MkTupGenRes regGen [] []) fields)
    where processField : (List CairoReg, TupGenRes) -> UntupleInfo -> (List CairoReg, TupGenRes)
          processField (acc, MkTupGenRes regGen sources code) info = let (MkTupGenRes newRegGen newSources newCode) = generateRetupling (snd fieldReg) depth info (fst fieldReg)
            in (acc ++ [fst fieldReg], MkTupGenRes newRegGen (sources ++ newSources) (code ++ newCode))
            where fieldReg : (CairoReg, RegisterGen)
                  fieldReg = nextRegister regGen depth
          produceRes : (List CairoReg, TupGenRes) -> TupGenRes
          produceRes (fieldRegs, MkTupGenRes regGen sources code) = MkTupGenRes regGen sources (code ++ [MKCON resReg (Just tag) fieldRegs])

generateRetupling regGen _ _ resReg = MkTupGenRes regGen [resReg] []

deriveUntupledName : Name -> Name
deriveUntupledName name = MN ("tupled_"++(cairoName name)) 0 --Todo: A nice prefix function in common def

generateReTupledClosure : Name -> List LinearImplicit -> List CairoReg -> UntupleInfo -> (Name, CairoDef)
generateReTupledClosure name linImpls args info = let (MkTupGenRes newNextReg sources code) = generateRetupling (snd retReg) 0 info (fst retReg)
        in (deriveUntupledName name, FunDef args implicitParams ["tupledRet"] (((CALL sources callLinearImplicits name args)::code) ++ [RETURN [(fst retReg)] returnLinearImplicits]))
    where retReg : (CairoReg, RegisterGen)
          retReg = nextRegister (mkRegisterGen "retupling") 0
          implicitRegs : List CairoReg
          implicitRegs = snd $ foldl (\(n,acc), _ => (n+1, (Unassigned (Just "implicit") n 0)::acc)) (1, []) linImpls
          implicitParams : SortedMap LinearImplicit CairoReg
          implicitParams = fromList $ map (\i => (i, NamedParam (implicitName i))) linImpls
          callLinearImplicits : SortedMap LinearImplicit (CairoReg, CairoReg)
          callLinearImplicits = fromList $ map (\(i,r) => (i, (fromMaybe Eliminated (lookup i implicitParams), r))) (zip linImpls implicitRegs)
          returnLinearImplicits : SortedMap LinearImplicit CairoReg
          returnLinearImplicits = fromList $ zip linImpls implicitRegs

generateReTupledClosureDef : Name -> CairoDef -> UntupleInfo -> (Name, CairoDef)
generateReTupledClosureDef name (FunDef args linImpls _ _) info = generateReTupledClosure name (keys linImpls) args info
generateReTupledClosureDef name (ForeignDef i Z _) info = generateReTupledClosure name (implicits i) [] info
generateReTupledClosureDef name (ForeignDef i (S remArgs) _) info = generateReTupledClosure name (implicits i) (map Param (fromZeroTo (cast remArgs))) info

rewireUntupledClosures : SortedMap Name UntupleInfo -> List (Name, CairoDef) -> List (Name, CairoDef)
rewireUntupledClosures inf defs = (mapMaybe genRetuplingFun (toList allUntupledClosures)) ++ (snd $ runVisitTransformCairoDefs (pureTraversal rewireTransform) defs)
    where allUntupledClosures : SortedSet Name
          allUntupledClosures = intersection (keySet inf) (underAppliedFunctionsDefs defs)
          defLookup : SortedMap Name CairoDef
          defLookup = fromList defs
          genRetuplingFun : Name -> Maybe (Name, CairoDef)
          genRetuplingFun name = pure (generateReTupledClosureDef name !(lookup name defLookup) !(lookup name inf))
          rewireTransform : InstVisit CairoReg -> List (InstVisit CairoReg)
          rewireTransform inst@(VisitMkClosure res name miss args) = if contains name allUntupledClosures
                then [VisitMkClosure res (deriveUntupledName name) miss args]
                else [inst]
          rewireTransform inst = [inst]

-- Here is the code transformer based on the analysis
generateUntupling : RegisterGen -> (depth:Int) -> UntupleInfo -> (src: CairoReg) -> TupGenRes
generateUntupling regGen depth (Candidate _ fields) src = processFields regGen 0 fields
    where processFields : RegisterGen -> Nat -> List UntupleInfo -> TupGenRes
          processFields regGen _ Nil = MkTupGenRes regGen [] []
          processFields regGen pos (f::fs) = MkTupGenRes rem.regGen (unpacked.regs++rem.regs) ((PROJECT (fst nReg) src pos)::(unpacked.code++rem.code))
             where nReg : (CairoReg, RegisterGen)
                   nReg = nextRegister regGen depth
                   unpacked : TupGenRes
                   unpacked = generateUntupling (snd nReg) depth f (fst nReg)
                   rem : TupGenRes
                   rem = processFields (unpacked.regGen) (pos+1) fs

generateUntupling nextReg _ _ src = MkTupGenRes nextReg [src] []

untupledRets : UntupleInfo -> Int
untupledRets (Candidate tag fields) = foldl (\acc,sub => acc + untupledRets sub) 0 fields
untupledRets _ = 1

adaptReturn : Maybe UntupleInfo -> (Name, CairoDef) -> (Name, CairoDef)
adaptReturn (Just uinf) (name, ForeignDef linImpls argsN 1) = (name, ForeignDef linImpls argsN (cast (untupledRets uinf)))
adaptReturn (Just uinf) (name, FunDef params implicits [_] body) = (name, FunDef params implicits retNames body)
    where retNames : List String
          retNames = map (\i => "r_"++(show i)) (fromZeroTo ((untupledRets uinf)-1))
adaptReturn _ def = def

untupleDef : SortedMap Name UntupleInfo -> (Name, CairoDef) -> (Name, CairoDef)
untupleDef info def@(name,_) = adaptReturn (lookup name info) (orderUnassignedRegIndexes (snd $ runVisitTransformCairoDef (rawTraversal untuplerTransform (mkRegisterGen "untupling", 0)) def))
    where untuplerTransform : InstVisit CairoReg -> Traversal (RegisterGen,Int) (List (InstVisit CairoReg))
          untuplerTransform inst@(VisitCall (oldRet::Nil) linImpls target args) = case (lookup target info) of
            Nothing => pure [inst]
            (Just Untouched) => pure [inst]
            (Just utinfo) => do
                (regGen, depth) <- readState
                let (MkTupGenRes newRegGen sources code) = generateRetupling regGen depth utinfo oldRet
                _ <- writeState (newRegGen, depth)
                pure ((VisitCall sources linImpls target args)::(fromCairoInsts code))
          untuplerTransform inst@(VisitExtprim (oldRet::Nil) linImpls target args) = case (lookup target info) of
            Nothing => pure [inst]
            (Just Untouched) => pure [inst]
            (Just utinfo) => do
                (regGen, depth) <- readState
                let (MkTupGenRes newRegGen sources code) = generateRetupling regGen depth utinfo oldRet
                _ <- writeState (newRegGen, depth)
                pure ((VisitExtprim sources linImpls target args)::(fromCairoInsts code))
          untuplerTransform inst@(VisitReturn (oldRet::Nil) linImpls) = case (lookup name info) of
            Nothing => pure [inst]
            (Just Untouched) => pure [inst]
            (Just utinfo) => do
                (regGen, depth) <- readState
                let (MkTupGenRes newRegGen targets code) = generateUntupling regGen depth utinfo oldRet
                _ <- writeState (newRegGen, depth)
                pure ((fromCairoInsts code) ++ [VisitReturn targets linImpls])
          untuplerTransform inst@(VisitCase reg) = map (\_ => [inst]) (updateStateL rightLens (+1))
          untuplerTransform VisitCaseEnd = map (\_ => [VisitCaseEnd]) (updateStateL rightLens (\x => x-1))
          untuplerTransform inst = pure [inst]

export
untupling : List (Name, CairoDef) -> List (Name, CairoDef)
untupling defs = rewireUntupledClosures untuplingTargets (map (untupleDef untuplingTargets) defs)
    where directlyCalledTargets : SortedSet Name
          directlyCalledTargets = fullyAppliedFunctionsDefs defs
          untupledCallInfo :  SortedMap Name UntupleInfo
          untupledCallInfo = iterFindTuplingTargetDefs empty (filter (\(n,_) => contains n directlyCalledTargets) defs)
          untuplingTargets : SortedMap Name UntupleInfo
          untuplingTargets = mergeLeft (untupledExtPrimDefs defs) untupledCallInfo

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
module Main

import Data.Primitives.Views
import System

%default total

data Command : Type -> Type where
  PutStr : String -> Command ()
  GetLine : Command String
  ReadFile : String -> Command (Either FileError String)
  WriteFile : String -> String -> Command (Either FileError ())

  Pure : ty -> Command ty
  Bind : Command a -> (a -> Command b) -> Command b

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

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

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

runCommand : Command a -> IO a
runCommand (PutStr x)       = putStr x
runCommand GetLine          = getLine
runCommand (ReadFile f)     = readFile f
runCommand (WriteFile f c)  = writeFile f c
runCommand (Pure x)         = pure x
runCommand (Bind m k)       = do
  res <- runCommand m
  runCommand (k res)

data Input = Answer Int
           | QuitCmd

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

data State = Answers Nat Nat

correctAnswer : State -> State
correctAnswer (Answers s t) = Answers (s + 1) (t + 1)

incorrectAnswer : State -> State
incorrectAnswer (Answers s t) = Answers s (t + 1)

mutual
  correct : Stream Int -> State -> ConsoleIO Nat
  correct nums answers = do
    PutStr "Correct!\n"
    quiz nums (correctAnswer answers)

  wrong : Stream Int -> Int -> State -> ConsoleIO Nat
  wrong nums ans answers = do
    PutStr ("Wrong, the answer is " ++ show ans ++ "\n")
    quiz nums (incorrectAnswer answers)

  quiz : Stream Int -> State -> ConsoleIO Nat
  quiz (num1 :: num2 :: nums) answers@(Answers score ttl) = do
    PutStr ("Score so far: " ++ show score ++ " / " ++ show ttl ++ "\n")
    input <- readInput (show num1 ++ " * " ++ show num2 ++ "? ")
    case input of
        Answer answer => if answer == num1 * num2
                            then correct nums answers
                            else wrong nums (num1 * num2) answers
        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 x with (divides x 12)
      bound ((12 * div) + rem) | (DivBy prf) = abs rem + 1

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

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

run : Fuel -> ConsoleIO a -> IO (Maybe a)
run Dry _ = pure Nothing
run _ (Quit a) = pure $ Just a
run (More fuel) (Do c f) = do
  res <- runCommand c
  run fuel (f res)

partial
main : IO ()
main = do
  let seed = 0
  Just score <- run (tank 20) (quiz (arithInputs (fromInteger seed)) (Answers 0 0))
    | Nothing => putStrLn "Ran out of fuel"
  putStrLn ("Final score: " ++ show score)

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 Language.SystemVerilog.Micro.Pretty

import Data.Vect

import public Text.PrettyPrint.Prettyprinter

import Toolkit.Data.DList
import Toolkit.Data.DVect

import Toolkit.Data.Vect.Extra

import Language.SystemVerilog.Gates

import Language.SystemVerilog.Micro

%default total

krStyle : (l,r  : Doc ())
       -> (body : List (Doc ()))
               -> Doc ()
krStyle l r body = vsep [l, indent 2 (align $ vcat body), r]

krStyleParams : (l,r  : Doc ())
             -> (sep  : Doc ())
             -> (body : List (Doc ()))
                     -> Doc ()
krStyleParams l r sep body = vsep [l, indent 2 (align $ vcat (punctuate sep body)), r]

prettyGate : TyGateComb -> Doc ()
prettyGate AND = pretty "and"
prettyGate IOR = pretty "or"
prettyGate XOR = pretty "xor"

mutual

  covering
  prettyDecls' : (decls : Decls gtypes) -> List (Doc ())
  prettyDecls' Empty = Nil
  prettyDecls' (DeclAdd this beThis IsDeclM rest )
    = prettyDecls' rest ++ [pretty "module" <++> pretty this <++> prettyExpr beThis <++> line]
  prettyDecls' (DeclAdd this beThis IsDeclD rest )
    = prettyDecls' rest ++ [pretty "typedef" <++> prettyExpr beThis <++> (pretty this <+> semi) <++> line]

  covering
  prettyDecls : (decls : Decls gtypes) -> Doc ()
  prettyDecls = (vsep . prettyDecls')

  covering
  prettyExpr : Expr lctxt gctxt type -> Doc ()

  prettyExpr End  = emptyDoc
  prettyExpr TYPE = emptyDoc
  prettyExpr GATE = emptyDoc

  prettyExpr (Local label x) = pretty label
  prettyExpr (Global label x)   = pretty label

  prettyExpr (Let this beThis withType IsLetCD inThis) =
    vsep [ hsep [ pretty "wire"
                , prettyExpr withType
                , hcat [pretty this, prettyExpr beThis, semi]
                ]
         , prettyExpr inThis
         ]

  prettyExpr (Let this (Not o i) withType IsLetGG inThis) =
    vsep [ hsep [ pretty "not"
                , hcat [pretty this, prettyExpr (Not o i), semi]
                ]
         , prettyExpr inThis
         ]

  prettyExpr (Let this (Gate ty o ins) withType IsLetGG inThis) =
    vsep [ hsep [ prettyGate ty
                , hcat [pretty this, prettyExpr (Gate ty o ins), semi]
                ]
         , prettyExpr inThis
         ]

  prettyExpr (Let this beThis withType prf inThis) =
    vsep [ hsep [ prettyExpr withType
                , hcat [pretty this, prettyExpr beThis, semi]
                ]
         , prettyExpr inThis
         ]

  prettyExpr (Seq x y) =
    vcat [ prettyExpr x
         , prettyExpr y]

  prettyExpr DataLogic = pretty "logic"

  prettyExpr (DataArray type Z) = prettyExpr type
  prettyExpr (DataArray type (S size)) =
          prettyExpr type
      <+> brackets (pretty size <+> colon <+> pretty "0")

  prettyExpr (DataStruct xs) =
    let xs' = map (\(l,d) => hsep [prettyExpr d, pretty l <+> semi]) xs
     in pretty "struct packed" <+> hardline <+> krStyle lbrace rbrace (toList xs')

  prettyExpr (DataUnion xs) =
    let xs' = map (\(l,d) => hsep [prettyExpr d, pretty l <+> semi]) xs in
      pretty "union packed" <+> hardline <+> krStyle lbrace rbrace (toList xs')

  prettyExpr (Port label dir type) =
    hsep [ prettyDir dir
         , prettyExpr type
         , pretty label
         ]
  prettyExpr (MDecl x) =
    vcat [ softline
         , krStyleParams lparen rparen comma (mapToList prettyExpr x) <+> semi
         , pretty "// TO ADD"
         , pretty "endmodule;"
         ]

  prettyExpr NewChan = emptyDoc
  prettyExpr (NewModule xs) =
    let params = map (\(l,c) => dot <+> pretty l <+> parens (prettyExpr c)) xs
    in let ps' = indent 2 (krStyleParams lparen rparen comma params)
    in hardline <++> ps'

  prettyExpr (Not o i)
    = krStyle lparen rparen (punctuate comma $ [prettyExpr o, prettyExpr i])
  prettyExpr (Gate ty o ins)
    = let ins' = map prettyExpr ins
      in krStyle lparen rparen (punctuate comma $ prettyExpr o :: (toList ins'))

export
covering
prettySpec : Spec -> Doc ()
prettySpec (MkSpec rest x) =
  vcat [ prettyDecls rest
       , pretty "module Top ();"
       , indent 2 (prettyExpr x)
       , pretty "endmodule;"]

-- [ EOF ]

max_stars_repo_name: border-patrol/lightclick

max_issues_repo_name: border-patrol/lightclick

max_forks_repo_name: border-patrol/lightclick


text:
module Main

import IdrisJvm.IO
import Java.Lang

mutual
  evenT : Nat -> JVM_IO ()
  evenT Z = printLn True
  evenT (S k) = do
    setProperty "bar" (show k)
    oddT k

  oddT : Nat -> JVM_IO ()
  oddT Z = printLn False
  oddT (S k) = do
    setProperty "foo" (show k)
    evenT k

main : JVM_IO ()
main = evenT 99999


text:
f : (a : Int) => Int
f @{x} = x

g : Int
g = f {a=4}

h : Int
h = f @{5}

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Test.Utils

import Test.Unit
import Demo.Utils

%access export

partial
testDemoSquareInt : IO Bool
testDemoSquareInt = genericTest
  (Just "testDemoSquareInt")
  [demoSquare 5, demoSquare 12, demoSquare (-1)]
  [25, 144, 1]
  (==)

partial
testDemoSquareDouble : IO Bool
testDemoSquareDouble = genericTest
  (Just "testDemoSquareDouble")
  [demoSquare 5.0, demoSquare 12.0, demoSquare (-1.0)]
  [25.0, 144.0, 1.0]
  (==)

partial
testDemoQuad : IO Bool
testDemoQuad = genericTest
  (Just "testDemoQuad")
  (demoQuad 5)
  625
  (==)

partial
runTest : IO ()
runTest = do
  putStrLn "Testing Utils"
  putStrLn infoLine
  NonReporting.runTests
    [ testDemoSquareInt
    , testDemoSquareDouble
    , testDemoQuad
    ]

max_stars_repo_name: roycrippen/scratch

max_issues_repo_name: roycrippen/scratch

max_forks_repo_name: roycrippen/scratch


text:
> module FastSimpleProb.MonadicOperations

> import Data.List
> import Data.List.Quantifiers
> import Data.So

> import FastSimpleProb.SimpleProb
> import FastSimpleProb.BasicOperations
> import FastSimpleProb.BasicProperties
> import Double.Predicates
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Postulates
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import List.Operations
> import List.Properties
> import Fun.Operations
> import Sigma.Sigma

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

* |SimpleProb| is a functor:

> using implementation NumNonNegDouble
>   |||
>   fmap : {A, B : Type} -> (A -> B) -> SimpleProb A -> SimpleProb B
>   fmap f (MkSimpleProb aps psum) = MkSimpleProb aps' psum' where
>     aps'  : List (B, NonNegDouble)
>     aps'  = map (cross f id) aps
>     psum' : Positive (toDouble (sumMapSnd aps'))
>     psum' = replace {P = \ X => Positive (toDouble X)} s2 psum where
>       s1 : map snd (map (cross f id) aps) = map snd aps
>       s1 = mapSndMapCrossAnyIdLemma f aps
>       s2 : sumMapSnd aps = sumMapSnd aps'
>       s2 = cong {f = sum} (sym s1)

* |SimpleProb| is a monad:

> |||
> ret : {A : Type} -> A -> SimpleProb A
> ret a = MkSimpleProb [(a, one)] positiveOne

> using implementation NumNonNegDouble
>   |||
>   bind : {A, B : Type} -> SimpleProb A -> (A -> SimpleProb B) -> SimpleProb B
>   bind {A} {B} (MkSimpleProb aps psum) f = normalize (MkSimpleProb bps' psum') where
>     f' : A -> List (B, NonNegDouble)
>     f' a = toList (normalize (f a))
>     psums' : (a : A) -> Positive (toDouble (sumMapSnd (f' a)))
>     psums' a = toListLemma (normalize (f a))
>     bps' : List (B, NonNegDouble)
>     bps' = mvMult aps f'
>     psum' : Positive (toDouble (sumMapSnd bps'))
>     psum' = mvMultLemma aps psum f' psums'

> using implementation NumNonNegDouble
>   |||
>   naivebind : {A, B : Type} -> SimpleProb A -> (A -> SimpleProb B) -> SimpleProb B
>   {-
>   naivebind {A} {B} (MkSimpleProb aps psum) f = MkSimpleProb bps' psum' where
>     f' : A -> List (B, NonNegDouble)
>     f' a = toList (f a)
>     psums' : (a : A) -> Positive (toDouble (sumMapSnd (f' a)))
>     psums' a = toListLemma (f a)
>     bps' : List (B, NonNegDouble)
>     bps' = mvMult aps f'
>     psum' : Positive (toDouble (sumMapSnd bps'))
>     psum' = mvMultLemma aps psum f' psums'
>   -}
>   naivebind {A} {B} (MkSimpleProb aps psum) f =
>     let f'     : (A -> List (B, NonNegDouble))
>                = toList . f in
>     let psums' : ((a : A) -> Positive (toDouble (sumMapSnd (f' a))))
>                = (\ a => toListLemma (f a)) in
>     let bps'   : List (B, NonNegDouble)
>                = mvMult aps f' in
>     let psum'  : Positive (toDouble (sumMapSnd bps'))
>                = mvMultLemma aps psum f' psums' in
>     MkSimpleProb bps' psum'

* |SimpleProb| is a container monad:

> |||
> Elem : {A : Type} -> A -> SimpleProb A -> Type
> Elem a sp = Elem a (support sp)

> |||
> NonEmpty : {A : Type} -> SimpleProb A -> Type
> NonEmpty sp = List.Operations.NonEmpty (support sp)

> |||
> All : {A : Type} -> (P : A -> Type) -> SimpleProb A -> Type
> All P sp = All P (support sp)

> using implementation NumNonNegDouble
>   ||| Tagging
>   tagElem  :  {A : Type} -> (sp : SimpleProb A) -> SimpleProb (Sigma A (\ a => a `Elem` sp))
>   tagElem sp = MkSimpleProb aps' psum' where
>     ssp  : List A
>     ssp  = support sp
>     wsp  : List NonNegDouble
>     wsp  = weights sp
>     as'  : List (Sigma A (\ a => a `Elem` sp))
>     as'  = List.Operations.tagElem ssp
>     aps' : List (Sigma A (\ a => a `Elem` sp), NonNegDouble)
>     aps' = zip as' wsp
>     psum' : Positive (toDouble (sumMapSnd aps'))
>     psum' = s9 where
>       s1 : sumMapSnd aps' = sum (snd (unzip aps'))
>       s1 = sumMapSndUnzipLemma aps'
>       s2 : length as' = length ssp
>       s2 = tagElemPreservesLength ssp
>       s3 : length ssp = length wsp
>       s3 = lengthSupportWeightsLemma sp
>       s4 : length as' = length wsp
>       s4 = trans s2 s3
>       s5 : unzip (zip as' wsp) = (as', wsp)
>       s5 = unzipZipLemma as' wsp s4
>       s6 : snd (unzip aps') = wsp
>       s6 = cong {f = snd} s5
>       s7 : Positive (toDouble (sum wsp))
>       s7 = positiveWeights sp
>       s8 : Positive (toDouble (sum (snd (unzip aps'))))
>       s8 = replace {P = \ X => Positive (toDouble (sum X))} (sym s6) s7
>       s9 : Positive (toDouble (sumMapSnd aps'))
>       s9 = replace {P = \ X => Positive (toDouble X)} (sym s1) s8

> {-

> ---}


text:
module Contract Types

--------------------------------------------------
--               contract structs
BlockNum : Type
Address : Type
UTCTime : Type
Balance : Type

BlockNum = Int
Address = Int
UTCTime = Int
Balance = Int

data ImmutBCData = MkImmutBCData BlockNum UTCTime
data ImmutContractData = MkImmutContractData Address
data MutContractData a = MkMutContractData Balance a

max_stars_repo_name: nickgeoca/QVM

max_issues_repo_name: nickgeoca/QVM

max_forks_repo_name: nickgeoca/QVM


text:
module Libraries.Data.List1

import Data.List1

%default total

-- TODO: Remove this, once Data.List1.unsnoc from base is available
--       to the compiler
export
unsnoc : (xs : List1 a) -> (List a, a)
unsnoc (h ::: Nil)       = (Nil, h)
unsnoc (h ::: (x :: xs)) =
  let (ini,lst) = Libraries.Data.List1.unsnoc (x ::: xs)
   in (h :: ini, lst)

max_stars_repo_name: mmhelloworld/idris-jvm

max_issues_repo_name: mmhelloworld/idris-jvm

max_forks_repo_name: mmhelloworld/idris-jvm


text:
module Control.App.FileIO

import Control.App

import Data.List
import Data.String
import System.File

%default covering

toFileEx : FileError -> FileEx
toFileEx (GenericFileError i) = GenericFileEx i
toFileEx FileReadError = FileReadError
toFileEx FileWriteError = FileWriteError
toFileEx FileNotFound = FileNotFound
toFileEx PermissionDenied = PermissionDenied
toFileEx FileExists = FileExists

public export
interface Has [Exception IOError] e => FileIO e where
  withFile : String -> Mode ->
             (onError : IOError -> App e a) ->
             (onOpen : File -> App e a) ->
             App e a
  fGetStr : File -> App e String
  fGetChars : File -> Int -> App e String
  fGetChar : File -> App e Char
  fPutStr : File -> String -> App e ()
  fPutStrLn : File -> String -> App e ()
  fflush : File -> App e ()
  fEOF : File -> App e Bool

-- TODO : Add Binary File IO with buffers

export
readFile : FileIO e => String -> App e String
readFile f
    = withFile f Read throw $ \h =>
        do content <- read [] h
           pure (fastAppend content)
  where
    read : List String -> File -> App e (List String)
    read acc h
        = do eof <- FileIO.fEOF h
             if eof
                then pure (reverse acc)
                else do str <- fGetStr h
                        read (str :: acc) h

fileOp : IO (Either FileError a) -> Has [PrimIO, Exception IOError] e => App e a
fileOp fileRes
      = do Right res <- primIO $ fileRes
             | Left err => throw (FileErr (toFileEx err))
           pure res

export
Has [PrimIO, Exception IOError] e => FileIO e where
  withFile fname m onError proc
      = do Right h <- primIO $ openFile fname m
              | Left err => onError (FileErr (toFileEx err))
           res <- catch (proc h) onError
           primIO $ closeFile h
           pure res

  fGetStr f = fileOp (fGetLine f)

  fGetChars f n = fileOp (fGetChars f n)

  fGetChar f = fileOp (fGetChar f)

  fPutStr f str = fileOp (fPutStr f str)

  fPutStrLn f str = fileOp (File.ReadWrite.fPutStrLn f str)

  fflush f = primIO $ fflush f

  fEOF f = primIO $ fEOF f

export
withFileIO : Has [PrimIO] e =>
             App (IOError :: e) a ->
             (ok : a -> App e b) ->
             (err : IOError -> App e b) -> App e b
withFileIO prog ok err = handle prog ok err


text:
module Doc

||| World!
export
world : Nat -> Nat
world x = x*2

nope : Nat
nope = 0

export
||| Hello!
hello : Int -> Int
hello x = x*2

public export
data WrappedInt : Type where
  MkWrappedInt : Int -> WrappedInt

public export
record SimpleRec where
  constructor MkSimpleRec
  a : Int
  b : String

namespace NS

  namespace NestedNS

    ||| A type of Foo
    Foo : Type
    Foo = ()


text:
maybeAdd : Maybe Int -> Maybe Int -> Maybe Int
maybeAdd x y = case x of
                    Nothing => Nothing
                    Just x_val => case y of
                                       Nothing => Nothing
                                       Just y_val => Just (x_val + y_val)

maybeAdd' : Maybe Int -> Maybe Int -> Maybe Int
maybeAdd' x y = x >>= \x_val =>
                y >>= \y_val =>
                Just (x_val + y_val)

maybeAdd'' : Maybe Int -> Maybe Int -> Maybe Int
maybeAdd'' x y = do x_val <- x
                    y_val <- y
                    Just (x_val + y_val)

max_issues_repo_name: gdevanla/TypeDD-Samples

max_forks_repo_name: gdevanla/TypeDD-Samples


text:
module Utilities

import Data.Bits
import Data.Fin

%default total

-- not sure why these casts are not included already. goes without
-- saying that some conversions are potentially lossy.

export
Cast Int Bits16 where
  cast = prim__zextInt_B16

export
Cast Int Bits8 where
  cast = prim__truncInt_B8

export
Cast Integer Bits8 where
  cast = fromInteger

export
Cast Bits16 Int where
  cast = prim__zextB16_Int

export
Cast Bits8 Int where
  cast = prim__zextB8_Int

export
Cast Bits8 Bits16 where
  cast = prim__zextB8_B16

export
Cast Bits8 (Bits 8) where
  cast x =
    let asInt: Int = cast x in
    intToBits $ the Integer $ cast asInt

export
Cast (Bits 8) Bits8 where
  cast x =
    let asInteger: Integer = bitsToInt x in
    cast $ the Int $ fromInteger asInteger

export
Cast Bits8 (Fin 16) where
  cast x =
    let reg: Int = cast x in
    let fin = fromIntegerNat $ cast reg in
    case natToFin fin 16 of
      Just f => f
      Nothing => idris_crash "value exceeded bounds" -- sad face

export
Cast (Fin 16) Bits8 where
  cast x =
    let value: Int = cast $ finToNat x in
    cast value

Cast Bits16 (Bits 16) where
  cast x =
    let asInt: Int = cast x in
    intToBits $ the Integer $ cast asInt

Cast (Bits 16) Bits16 where
  cast x =
    let asInteger: Integer = bitsToInt x in
    cast $ the Int $ fromInteger asInteger

extractNibble : (value : Bits16) -> (n : Integer) -> Bits8
extractNibble value n =
  let v: Bits 16 = cast value in
  let shift = intToBits $ 4 * n in
  let mask = intToBits 0xf `shiftLeft` shift in
  let result = (and v mask) `shiftRightLogical` shift in
  cast $ the Int $ fromInteger $ bitsToInt result

export
extractFirstNibble : (value : Bits16) -> Bits8
extractFirstNibble value = extractNibble value 3

export
extractSecondNibble : (value : Bits16) -> Bits8
extractSecondNibble value = extractNibble value 2

export
extractThirdNibble : (value : Bits16) -> Bits8
extractThirdNibble value = extractNibble value 1

export
extractFourthNibble : (value : Bits16) -> Bits8
extractFourthNibble value = extractNibble value 0

export
extractFirstByte : (value : Bits16) -> Bits8
extractFirstByte value =
  let v: Bits 16 = cast value in
  let mask = intToBits 0xff00 in
  let shift = intToBits 8 in
  let result = (and v mask) `shiftRightLogical` shift in
  cast $ the Int $ fromInteger $ bitsToInt result

export
extractSecondByte : (value : Bits16) -> Bits8
extractSecondByte value =
  let v: Bits 16 = cast value in
  let mask = intToBits 0x00ff in
  let result = and v mask in
  cast $ the Int $ fromInteger $ bitsToInt result

export
extractMask0xfff : (value : Bits16) -> Bits16
extractMask0xfff value =
  let v: Bits 16 = cast value in
  let mask = intToBits 0x0fff in
  let result = and v mask in
  cast result


text:
module TTImp.Elab.Rewrite

import Core.Context
import Core.Context.Log
import Core.Core
import Core.Env
import Core.GetType
import Core.Metadata
import Core.Normalise
import Core.Unify
import Core.TT
import Core.Value

import TTImp.Elab.Check
import TTImp.Elab.Delayed
import TTImp.TTImp

import Data.List

%default covering

-- TODO: Later, we'll get the name of the lemma from the type, if it's one
-- that's generated for a dependent type. For now, always return the default
findRewriteLemma : {auto c : Ref Ctxt Defs} ->
                   FC -> (rulety : Term vars) ->
                   Core Name
findRewriteLemma loc rulety
   = case !getRewrite of
          Nothing => throw (GenericMsg loc "No rewrite lemma defined")
          Just n => pure n

getRewriteTerms : {vars : _} ->
                  {auto c : Ref Ctxt Defs} ->
                  FC -> Defs -> NF vars -> Error ->
                  Core (NF vars, NF vars, NF vars)
getRewriteTerms loc defs (NTCon nfc eq t a args) err
    = if !(isEqualTy eq)
         then case reverse $ map snd args of
                   (rhs :: lhs :: rhsty :: lhsty :: _) =>
                        pure (!(evalClosure defs lhs),
                              !(evalClosure defs rhs),
                              !(evalClosure defs lhsty))
                   _ => throw err
         else throw err
getRewriteTerms loc defs ty err
    = throw err

rewriteErr : Error -> Bool
rewriteErr (NotRewriteRule _ _ _) = True
rewriteErr (RewriteNoChange _ _ _ _) = True
rewriteErr (InType _ _ err) = rewriteErr err
rewriteErr (InCon _ _ err) = rewriteErr err
rewriteErr (InLHS _ _ err) = rewriteErr err
rewriteErr (InRHS _ _ err) = rewriteErr err
rewriteErr (WhenUnifying _ _ _ _ _ err) = rewriteErr err
rewriteErr _ = False

-- Returns the rewriting lemma to use, and the predicate for passing to the
-- rewriting lemma
export
elabRewrite : {vars : _} ->
              {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              FC -> Env Term vars ->
              (expected : Term vars) ->
              (rulety : Term vars) ->
              Core (Name, Term vars, Term vars)
elabRewrite loc env expected rulety
    = do defs <- get Ctxt
         parg <- genVarName "rwarg"
         tynf <- nf defs env rulety
         (lt, rt, lty) <- getRewriteTerms loc defs tynf (NotRewriteRule loc env rulety)
         lemn <- findRewriteLemma loc rulety

         -- Need to normalise again, since we might have been delayed and
         -- the metavariables might have been updated
         expnf <- nf defs env expected

         logNF "elab.rewrite" 5 "Rewriting" env lt
         logNF "elab.rewrite" 5 "Rewriting in" env expnf
         rwexp_sc <- replace defs env lt (Ref loc Bound parg) expnf
         logTerm "elab.rewrite" 5 "Rewritten to" rwexp_sc

         empty <- clearDefs defs
         let pred = Bind loc parg (Lam loc top Explicit
                          !(quote empty env lty))
                          (refsToLocals (Add parg parg None) rwexp_sc)
         gpredty <- getType env pred
         predty <- getTerm gpredty
         exptm <- quote defs env expected

         -- if the rewritten expected type converts with the original,
         -- then the rewrite did nothing, which is an error
         when !(convert defs env rwexp_sc exptm) $
             throw (RewriteNoChange loc env rulety exptm)
         pure (lemn, pred, predty)

export
checkRewrite : {vars : _} ->
               {auto c : Ref Ctxt Defs} ->
               {auto m : Ref MD Metadata} ->
               {auto u : Ref UST UState} ->
               {auto e : Ref EST (EState vars)} ->
               RigCount -> ElabInfo ->
               NestedNames vars -> Env Term vars ->
               FC -> RawImp -> RawImp -> Maybe (Glued vars) ->
               Core (Term vars, Glued vars)
checkRewrite rigc elabinfo nest env fc rule tm Nothing
    = throw (GenericMsg fc "Can't infer a type for rewrite")
checkRewrite {vars} rigc elabinfo nest env ifc rule tm (Just expected)
    = delayOnFailure ifc rigc env (Just expected) rewriteErr Rewrite $ \delayed =>
        do let vfc = virtualiseFC ifc
           (rulev, grulet) <- check erased elabinfo nest env rule Nothing
           rulet <- getTerm grulet
           expTy <- getTerm expected
           when delayed $ log "elab.rewrite" 5 "Retrying rewrite"
           (lemma, pred, predty) <- elabRewrite vfc env expTy rulet

           rname <- genVarName "_"
           pname <- genVarName "_"

           let pbind = Let vfc erased pred predty
           let rbind = Let vfc erased (weaken rulev) (weaken rulet)

           let env' = rbind :: pbind :: env

           -- Nothing we do in this last part will affect the EState,
           -- we're only doing the application this way to make sure the
           -- implicits for the rewriting lemma are in the right place. But,
           -- we still need the right type for the EState, so weaken it once
           -- for each of the let bindings above.
           (rwtm, grwty) <-
              inScope vfc (pbind :: env) $ \e' =>
                inScope {e=e'} vfc env' $ \e'' =>
                  let offset = mkSizeOf [rname, pname] in
                  check {e = e''} rigc elabinfo (weakenNs offset nest) env'
                                (apply (IVar vfc lemma) [IVar vfc pname,
                                                         IVar vfc rname,
                                                         tm])
                                (Just (gnf env' (weakenNs offset expTy)))
           rwty <- getTerm grwty
           let binding = Bind vfc pname pbind . Bind vfc rname rbind
           pure (binding rwtm, gnf env (binding rwty))


text:
module Issue833

import Data.Fin

%default total

data Singleton : Nat -> Type where
  Sing : {n : Nat} -> Singleton n

f : (n : Singleton Z) -> n === Sing
f = \ Sing => Refl

g : (k : Fin 1) -> k === FZ
g = \ FZ => Refl

sym : {t, u : a} -> t === u -> u === t
sym = \Refl => Refl


text:
module Extra.File

import System.File

||| `fputc` in C
%foreign "C:fputc,libc"
export
prim__fputc : Int -> FilePtr -> PrimIO Int

||| `fputc` with higher level primitives in idris2
export
fputc : HasIO io => Bits8 -> File -> io (Either FileError ())
fputc b (FHandle ptr) = do
  let c = cast b
  c' <- primIO $ prim__fputc c ptr
  pure $ if c' == c then Right () else Left FileWriteError


text:
module Data.JSError

%access public export

data JSError = MkJSError Ptr

--------------------------------------------------------------------------------
-- Functions
--------------------------------------------------------------------------------

mkError : String -> JSError
mkError s = MkJSError $ unsafePerformIO $
  foreign FFI_JS "new Error(%0)" (String -> JS_IO Ptr) s

message : JSError -> String
message (MkJSError err) = unsafePerformIO $
  foreign FFI_JS "%0.message" (Ptr -> JS_IO String) err

showError : JSError -> String
showError (MkJSError err) = unsafePerformIO $
  foreign FFI_JS "%0.stack || %0.toString()" (Ptr -> JS_IO String) err

stack : JSError -> Maybe String
stack (MkJSError err) = unsafePerformIO $ do
  -- There is currently no boolean type for the JS FFI, so use an empty string
  errStack <- foreign FFI_JS "%0.stack || ''" (Ptr -> JS_IO String) err
  pure $ if (errStack == "")
    then Nothing
    else Just errStack

-- Current FFI does variable assignment on ffi calls, so run statement in closure
throw : JSError -> JS_IO ()
throw (MkJSError err) = foreign FFI_JS "(function() { throw %0 })()" (Ptr -> JS_IO ()) err

catch : (JSError -> JS_IO ()) -> JS_IO a -> JS_IO ()
catch cb m = foreign FFI_JS
  """(function() {
    try { %0() }
    catch (e) { %1(e) }
  })()""" (JsFn (() -> JS_IO ()) -> JsFn (Ptr -> JS_IO ()) -> JS_IO ())
  (MkJsFn $ \_ => believe_me m) (MkJsFn (\e => cb (MkJSError e)))

--------------------------------------------------------------------------------
-- Implementations
--------------------------------------------------------------------------------

Show JSError where
  show = showError

max_stars_repo_name: Risto-Stevcev/idris-jserror

max_issues_repo_name: Risto-Stevcev/idris-jserror

max_forks_repo_name: Risto-Stevcev/idris-jserror


text:
module Language.JSON.Data

import Data.Bits
import Data.List
import Data.Nat
import Data.String.Extra
import Data.String

%default total

public export
data JSON
   = JNull
   | JBoolean Bool
   | JNumber Double
   | JString String
   | JArray (List JSON)
   | JObject (List (String, JSON))

%name JSON json

private
b16ToHexString : Bits16 -> String
b16ToHexString n =
  case n of
    0 => "0"
    1 => "1"
    2 => "2"
    3 => "3"
    4 => "4"
    5 => "5"
    6 => "6"
    7 => "7"
    8 => "8"
    9 => "9"
    10 => "A"
    11 => "B"
    12 => "C"
    13 => "D"
    14 => "E"
    15 => "F"
    other => assert_total $
               b16ToHexString (n `shiftR` fromNat 4) ++
               b16ToHexString (n .&. 15)

private
showChar : Char -> String
showChar c
  = case c of
         '\b' => "\\b"
         '\f' => "\\f"
         '\n' => "\\n"
         '\r' => "\\r"
         '\t' => "\\t"
         '\\' => "\\\\"
         '"'  => "\\\""
         c => if isControl c || c >= '\127'
                 then let hex = b16ToHexString (cast $ ord c)
                       in "\\u" ++ justifyRight 4 '0' hex
                 else singleton c

private
showString : String -> String
showString x = "\"" ++ concatMap showChar (unpack x) ++ "\""

||| Convert a JSON value into its string representation.
||| No whitespace is added.
private
stringify : JSON -> String
stringify JNull = "null"
stringify (JBoolean x) = if x then "true" else "false"
stringify (JNumber x) = show x
stringify (JString x) = showString x
stringify (JArray xs) = "[" ++ stringifyValues xs ++ "]"
  where
    stringifyValues : List JSON -> String
    stringifyValues [] = ""
    stringifyValues (x :: xs) = stringify x
                             ++ if isNil xs
                                   then ""
                                   else "," ++ stringifyValues xs
stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}"
  where
    stringifyProp : (String, JSON) -> String
    stringifyProp (key, value) = showString key ++ ":" ++ stringify value

    stringifyProps : List (String, JSON) -> String
    stringifyProps [] = ""
    stringifyProps (x :: xs) = stringifyProp x
                            ++ if isNil xs
                                  then ""
                                  else "," ++ stringifyProps xs

export
Show JSON where
  show = stringify

||| Format a JSON value, indenting by `n` spaces per nesting level.
|||
||| @curr The current indentation amount, measured in spaces.
||| @n The amount of spaces to indent per nesting level.
export
format : {default 0 curr : Nat} -> (n : Nat) -> JSON -> String
format {curr} n json = indent curr $ formatValue curr n json
  where
    formatValue : (curr, n : Nat) -> JSON -> String
    formatValue _ _ (JArray []) = "[]"
    formatValue curr n (JArray xs@(_ :: _)) = "[\n" ++ formatValues xs
                                           ++ indent curr "]"
      where
        formatValues : (xs : List JSON) -> {auto ok : NonEmpty xs} -> String
        formatValues (x :: xs) = format {curr=(curr + n)} n x
                              ++ case xs of
                                      _ :: _ => ",\n" ++ formatValues xs
                                      [] => "\n"
    formatValue _ _ (JObject []) = "{}"
    formatValue curr n (JObject xs@(_ :: _)) = "{\n" ++ formatProps xs
                                            ++ indent curr "}"
      where
        formatProp : (String, JSON) -> String
        formatProp (key, value) = indent (curr + n) (showString key ++ ": ")
                               ++ formatValue (curr + n) n value

        formatProps : (xs : List (String, JSON)) -> {auto ok : NonEmpty xs} -> String
        formatProps (x :: xs) = formatProp x
                             ++ case xs of
                                     _ :: _ => ",\n" ++ formatProps xs
                                     [] => "\n"
    formatValue _ _ x = stringify x


text:
module AutoDiff

record Diff a where
    constructor MkDiff
    getGradient : a
    getValue : a

-- dC/dx = 0
export
constant : Num a => a -> Diff a
constant = MkDiff 0

-- dx/dx = 1
export
independent : Num a => a -> Diff a
independent = MkDiff 1

-- du/dx = du/dv * dv/dx
export
elementary : Num a => (a -> a) -> (a -> a) -> Diff a -> Diff a
elementary f f' (MkDiff dy y) = MkDiff (f' y * dy) (f y)

arithmetic : Num a => (a -> a -> a) -> (a -> a -> (a, a)) -> Diff a -> Diff a -> Diff a
arithmetic f f' (MkDiff du u) (MkDiff dv v) =
  let (dx, dy) = f' u v in MkDiff (dx * du + dy * dv) (f u v)

squared : Num a => a -> a
squared x = x * x

diff' : Num a => (Diff a -> Diff a) -> a -> Diff a
diff' f = f . independent
export
diff : Num a => (Diff a -> Diff a) -> a -> a
diff f = getGradient . diff' f

export
sin' : Diff Double -> Diff Double
sin' = elementary sin cos
export
cos' : Diff Double -> Diff Double
cos' = elementary cos (negate . sin)

Eq a => Eq (Diff a) where
  u == v = getValue u == getValue v

Ord a => Ord (Diff a) where
  compare u v = compare (getValue u) (getValue v)

Num a => Num (Diff a) where
  -- d(u+v) = du + dv
  (+) = arithmetic (+) (\_, _ => (1, 1))
  -- d(uv) = v(du) + u(dv)
  (*) = arithmetic (*) (\u, v => (v, u))
  fromInteger = constant . fromInteger

Neg a => Neg (Diff a) where
  -- d(u-v) = du - dv
  (-) = arithmetic (-) (\_, _ => (1, -1))
  -- d(-x) = -1
  negate = elementary negate (const (-1))

max_stars_repo_name: dannypsnl/auto-diff

max_issues_repo_name: dannypsnl/auto-diff

max_forks_repo_name: dannypsnl/auto-diff


text:
module Fibonacci

fibpair: Nat -> (Nat, Nat)
fibpair Z = (1, 1)
fibpair (S k) = case (fibpair k) of
                     (a, b) => (b, a + b)

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

fiblist: Nat -> List (Nat)
fiblist Z = []
fiblist (S k) = case (fibpair k) of
                     (a, b) => append (fiblist k) a

tuple: Nat -> Type
tuple Z = Unit
tuple (S k) = (Nat, tuple k)

fibtup: (n: Nat) -> tuple n
fibtup Z = ()
fibtup (S k) = case (fibpair k) of
                    (a, b) => (a, fibtup k)

apptup: (n: Nat) -> tuple n -> Nat -> tuple (succ n)
apptup Z () k = (k, ())
apptup (S j) (a, b) k = (a, tail) where
  tail = apptup j b k

rev: (n: Nat) -> tuple n -> tuple n
rev Z () = ()
rev (S k) (a, b) = apptup k (rev k b) a

revv: {n: Nat} -> tuple n -> tuple n
revv {n = Z} () = ()
revv {n = (S k)} (a, b) = apptup k (revv b) a

total ack : Nat -> Nat -> Nat
ack Z n = n + 1
ack (S k) Z = ack k 1
ack (S k) (S j) = ack k (ack (S k) j)

rec : (a : Type) -> a -> (Nat -> a -> a) -> (Nat -> a)
rec a x f Z = x
rec a x f (S k) = f k (rec a x f k)

base : Nat -> Nat
base k = k + 1

s : (m : Nat) -> (ackm : Nat -> Nat) -> Nat -> Nat -> Nat
s m ackm k j = ackm j

step : Nat -> (Nat -> Nat) -> Nat -> Nat
step m ackm = rec Nat (ackm 1)(s m ackm)

ackrec : Nat -> Nat -> Nat
ackrec = rec (Nat -> Nat) base step