text:
--- Day 7: The Treachery of Whales ---

module TheTreacheryOfWhales
import System
import System.File
import Data.List
import Data.List1
import Data.Strings
import Data.Fin
import Util

{--
A giant whale has decided your submarine is its next meal, and it's much faster than you are. There's nowhere to run!

Suddenly, a swarm of crabs (each in its own tiny submarine - it's too deep for them otherwise) zooms in to rescue you! They seem to be preparing to blast a hole in the ocean floor; sensors indicate a massive underground cave system just beyond where they're aiming!

The crab submarines all need to be aligned before they'll have enough power to blast a large enough hole for your submarine to get through. However, it doesn't look like they'll be aligned before the whale catches you! Maybe you can help?

There's one major catch - crab submarines can only move horizontally.

You quickly make a list of the horizontal position of each crab (your puzzle input). Crab submarines have limited fuel, so you need to find a way to make all of their horizontal positions match while requiring them to spend as little fuel as possible.

For example, consider the following horizontal positions:

16,1,2,0,4,2,7,1,2,14
This means there's a crab with horizontal position 16, a crab with horizontal position 1, and so on.

Each change of 1 step in horizontal position of a single crab costs 1 fuel. You could choose any horizontal position to align them all on, but the one that costs the least fuel is horizontal position 2:

Move from 16 to 2: 14 fuel
Move from 1 to 2: 1 fuel +
Move from 2 to 2: 0 fuel +
Move from 0 to 2: 2 fuel
Move from 4 to 2: 2 fuel +
Move from 2 to 2: 0 fuel +
Move from 7 to 2: 5 fuel +
Move from 1 to 2: 1 fuel +
Move from 2 to 2: 0 fuel +
Move from 14 to 2: 12 fuel
This costs a total of 37 fuel. This is the cheapest possible outcome; more expensive outcomes include aligning at position 1 (41 fuel), position 3 (39 fuel), or position 10 (71 fuel).

Determine the horizontal position that the crabs can align to using the least fuel possible. How much fuel must they spend to align to that position?

--- Part Two ---
The crabs don't seem interested in your proposed solution. Perhaps you misunderstand crab engineering?

As it turns out, crab submarine engines don't burn fuel at a constant rate. Instead, each change of 1 step in horizontal position costs 1 more unit of fuel than the last: the first step costs 1, the second step costs 2, the third step costs 3, and so on.

As each crab moves, moving further becomes more expensive. This changes the best horizontal position to align them all on; in the example above, this becomes 5:

Move from 16 to 5: 66 fuel
Move from 1 to 5: 10 fuel
Move from 2 to 5: 6 fuel
Move from 0 to 5: 15 fuel
Move from 4 to 5: 1 fuel
Move from 2 to 5: 6 fuel
Move from 7 to 5: 3 fuel
Move from 1 to 5: 10 fuel
Move from 2 to 5: 6 fuel
Move from 14 to 5: 45 fuel
This costs a total of 168 fuel. This is the new cheapest possible outcome; the old alignment position (2) now costs 206 fuel instead.

Determine the horizontal position that the crabs can align to using the least fuel possible so they can make you an escape route! How much fuel must they spend to align to that position?
--}

abs': Nat -> Nat -> Nat
abs' k j = if k >= j then minus k j else minus j k

median : List Nat -> Maybe Nat
median xs = do
              let int = fromIntegerNat $ div (cast $ length xs) 2
              let (Just idx) = natToFin int $ length xs | Nothing => Nothing
              pure $ index' xs idx

mean: List Nat -> Nat
mean xs = fromIntegerNat $ div (cast $ sum xs) (cast $ length xs)

series: (n: Nat) -> Nat
series n = fromIntegerNat $ div ((cast n) * ((cast n) + 1)) 2

calcFuel: (pos: List Nat) -> Maybe Nat
calcFuel pos = do
                let (Just m) = (median . sort) pos | Nothing => Nothing
                pure $ foldr (plus . abs' m) Z pos

calcFuel2: (pos: List Nat) -> Nat
calcFuel2 pos = min (fuel $ mean pos) (fuel $ S $ mean pos)
                where
                  fuel: (m: Nat) -> Nat
                  fuel m = foldr (plus . series . abs' m) Z pos

main: IO ()
main = do
         args <- getArgs
         let (file :: _) = drop 1 args | [] => putStrLn "No file provided!"
         (Right symbols) <- readFile file | (Left error) => putStrLn $ show error
         let (Just pos) = consolidate $ map parsePositive $ forget $ split ( == ',') symbols | Nothing => putStrLn "Parsing error!"
         let (Just fuel) = calcFuel pos | Nothing => pure ()
         putStrLn . show $ fuel
         putStrLn . show $ calcFuel2 pos


text:
module Idris.Pretty

import Data.List
import Data.Strings
import Control.ANSI.SGR
import public Text.PrettyPrint.Prettyprinter
import public Text.PrettyPrint.Prettyprinter.Render.Terminal
import public Text.PrettyPrint.Prettyprinter.Util

import Algebra
import Idris.REPLOpts
import Idris.Syntax
import Utils.Term

%default covering

public export
data IdrisAnn
  = Warning
  | Error
  | ErrorDesc
  | FileCtxt
  | Code
  | Meta
  | Keyword
  | Pragma

export
colorAnn : IdrisAnn -> AnsiStyle
colorAnn Warning = color Yellow <+> bold
colorAnn Error = color BrightRed <+> bold
colorAnn ErrorDesc = bold
colorAnn FileCtxt = color BrightBlue
colorAnn Code = color Magenta
colorAnn Keyword = color Red
colorAnn Pragma = color BrightMagenta
colorAnn Meta = color Green

export
error : Doc IdrisAnn -> Doc IdrisAnn
error = annotate Error

export
errorDesc : Doc IdrisAnn -> Doc IdrisAnn
errorDesc = annotate ErrorDesc

export
fileCtxt : Doc IdrisAnn -> Doc IdrisAnn
fileCtxt = annotate FileCtxt

export
keyword : Doc IdrisAnn -> Doc IdrisAnn
keyword = annotate Keyword

export
meta : Doc IdrisAnn -> Doc IdrisAnn
meta = annotate Meta

export
code : Doc IdrisAnn -> Doc IdrisAnn
code = annotate Code

let_ : Doc IdrisAnn
let_ = keyword (pretty "let")

in_ : Doc IdrisAnn
in_ = keyword (pretty "in")

case_ : Doc IdrisAnn
case_ = keyword (pretty "case")

of_ : Doc IdrisAnn
of_ = keyword (pretty "of")

do_ : Doc IdrisAnn
do_ = keyword (pretty "do")

with_ : Doc IdrisAnn
with_ = keyword (pretty "with")

record_ : Doc IdrisAnn
record_ = keyword (pretty "record")

impossible_ : Doc IdrisAnn
impossible_ = keyword (pretty "impossible")

auto_ : Doc IdrisAnn
auto_ = keyword (pretty "auto")

default_ : Doc IdrisAnn
default_ = keyword (pretty "default")

rewrite_ : Doc IdrisAnn
rewrite_ = keyword (pretty "rewrite")

export
pragma : Doc IdrisAnn -> Doc IdrisAnn
pragma = annotate Pragma

export
prettyRig : RigCount -> Doc ann
prettyRig = elimSemi (pretty '0' <+> space)
                     (pretty '1' <+> space)
                     (const emptyDoc)

mutual
  prettyAlt : PClause -> Doc IdrisAnn
  prettyAlt (MkPatClause _ lhs rhs _) =
    space <+> pipe <++> prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs <+> semi
  prettyAlt (MkWithClause _ lhs wval flags cs) =
    space <+> pipe <++> angles (angles (reflow "with alts not possible")) <+> semi
  prettyAlt (MkImpossible _ lhs) =
    space <+> pipe <++> prettyTerm lhs <++> impossible_ <+> semi

  prettyCase : PClause -> Doc IdrisAnn
  prettyCase (MkPatClause _ lhs rhs _) =
    prettyTerm lhs <++> pretty "=>" <++> prettyTerm rhs
  prettyCase (MkWithClause _ lhs rhs flags _) =
    space <+> pipe <++> angles (angles (reflow "with alts not possible"))
  prettyCase (MkImpossible _ lhs) =
    prettyTerm lhs <++> impossible_

  prettyDo : PDo -> Doc IdrisAnn
  prettyDo (DoExp _ tm) = prettyTerm tm
  prettyDo (DoBind _ n tm) = pretty n <++> pretty "<-" <++> prettyTerm tm
  prettyDo (DoBindPat _ l tm alts) =
    prettyTerm l <++> pretty "<-" <++> prettyTerm tm <+> hang 4 (fillSep $ prettyAlt <$> alts)
  prettyDo (DoLet _ l rig _ tm) =
    let_ <++> prettyRig rig <+> pretty l <++> equals <++> prettyTerm tm
  prettyDo (DoLetPat _ l _ tm alts) =
    let_ <++> prettyTerm l <++> equals <++> prettyTerm tm <+> hang 4 (fillSep $ prettyAlt <$> alts)
  prettyDo (DoLetLocal _ ds) =
    let_ <++> braces (angles (angles (pretty "definitions")))
  prettyDo (DoRewrite _ rule) = rewrite_ <+> prettyTerm rule

  prettyUpdate : PFieldUpdate -> Doc IdrisAnn
  prettyUpdate (PSetField path v) =
    concatWith (surround dot) (pretty <$> path) <++> equals <++> prettyTerm v
  prettyUpdate (PSetFieldApp path v) =
    concatWith (surround dot) (pretty <$> path) <++> pretty '$' <+> equals <++> prettyTerm v

  export
  prettyTerm : PTerm -> Doc IdrisAnn
  prettyTerm = go Open
    where
      startPrec : Prec
      startPrec = User 0
      appPrec : Prec
      appPrec = User 10
      leftAppPrec : Prec
      leftAppPrec = User 9
      parenthesise : Bool -> Doc IdrisAnn -> Doc IdrisAnn
      parenthesise b = if b then parens else id

      go : Prec -> PTerm -> Doc IdrisAnn
      go d (PRef _ n) = pretty n
      go d (PPi _ rig Explicit Nothing arg ret) =
        parenthesise (d > startPrec) $ group $
          branchVal
            (go startPrec arg <++> "->" <++> go startPrec ret)
            (parens (prettyRig rig <+> "_" <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret)
            rig
      go d (PPi _ rig Explicit (Just n) arg ret) =
        parenthesise (d > startPrec) $ group $
          parens (prettyRig rig <+> pretty n <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret
      go d (PPi _ rig Implicit Nothing arg ret) =
        parenthesise (d > startPrec) $ group $
          braces (prettyRig rig <+> pretty '_' <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret
      go d (PPi _ rig Implicit (Just n) arg ret) =
        parenthesise (d > startPrec) $ group $
          braces (prettyRig rig <+> pretty n <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret
      go d (PPi _ rig AutoImplicit Nothing arg ret) =
        parenthesise (d > startPrec) $ group $
          branchVal
            (go startPrec arg <++> "=>" <+> line <+> go startPrec ret)
            (braces (auto_ <++> prettyRig rig <+> "_" <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret)
            rig
      go d (PPi _ rig AutoImplicit (Just n) arg ret) =
        parenthesise (d > startPrec) $ group $
          braces (auto_ <++> prettyRig rig <+> pretty n <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret
      go d (PPi _ rig (DefImplicit t) Nothing arg ret) =
        parenthesise (d > startPrec) $ group $
          braces (default_ <++> go appPrec t <++> prettyRig rig <+> "_" <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret
      go d (PPi _ rig (DefImplicit t) (Just n) arg ret) =
        parenthesise (d > startPrec) $ group $
          braces (default_ <++> go appPrec t <++> prettyRig rig <+> pretty n <++> colon <++> go startPrec arg) <++> "->" <+> line <+> go startPrec ret
      go d (PLam _ rig _ n ty sc) =
          let (ns, sc) = getLamNames [(rig, n, ty)] sc in
              parenthesise (d > startPrec) $ group $ align $ hang 2 $
                backslash <+> prettyBindings ns <++> "=>" <+> line <+> go startPrec sc
        where
          getLamNames : List (RigCount, PTerm, PTerm) -> PTerm -> (List (RigCount, PTerm, PTerm), PTerm)
          getLamNames acc (PLam _ rig _ n ty sc) = getLamNames ((rig, n, ty) :: acc) sc
          getLamNames acc sc = (reverse acc, sc)
          prettyBindings : List (RigCount, PTerm, PTerm) -> Doc IdrisAnn
          prettyBindings [] = neutral
          prettyBindings [(rig, n, (PImplicit _))] = prettyRig rig <+> go startPrec n
          prettyBindings [(rig, n, ty)] = prettyRig rig <+> go startPrec n <++> colon <++> go startPrec ty
          prettyBindings ((rig, n, (PImplicit _)) :: ns) = prettyRig rig <+> go startPrec n <+> comma <+> line <+> prettyBindings ns
          prettyBindings ((rig, n, ty) :: ns) = prettyRig rig <+> go startPrec n <++> colon <++> go startPrec ty <+> comma <+> line <+> prettyBindings ns
      go d (PLet _ rig n (PImplicit _) val sc alts) =
        parenthesise (d > startPrec) $ group $ align $
          let_ <++> (group $ align $ hang 2 $ prettyRig rig <+> go startPrec n <++> equals <+> line <+> go startPrec val) <+> line
            <+> in_ <++> (group $ align $ hang 2 $ go startPrec sc)
      go d (PLet _ rig n ty val sc alts) =
        parenthesise (d > startPrec) $ group $ align $
          let_ <++> (group $ align $ hang 2 $ prettyRig rig <+> go startPrec n <++> colon <++> go startPrec ty <++> equals <+> line <+> go startPrec val) <+> hardline
            <+> hang 4 (fillSep (prettyAlt <$> alts)) <+> line <+> in_ <++> (group $ align $ hang 2 $ go startPrec sc)
      go d (PCase _ tm cs) =
        parenthesise (d > appPrec) $ align $ case_ <++> go startPrec tm <++> of_ <+> line <+>
          braces (vsep $ punctuate semi (prettyCase <$> cs))
      go d (PLocal _ ds sc) =
        parenthesise (d > startPrec) $ group $ align $
          let_ <++> braces (angles (angles "definitions")) <+> line <+> in_ <++> go startPrec sc
      go d (PUpdate _ fs) =
        parenthesise (d > appPrec) $ group $ record_ <++> braces (vsep $ punctuate comma (prettyUpdate <$> fs))
      go d (PApp _ f a) = parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> go appPrec a
      go d (PWithApp _ f a) = go d f <++> pipe <++> go d a
      go d (PDelayed _ LInf ty) = parenthesise (d > appPrec) $ "Inf" <++> go appPrec ty
      go d (PDelayed _ _ ty) = parenthesise (d > appPrec) $ "Lazy" <++> go appPrec ty
      go d (PDelay _ tm) = parenthesise (d > appPrec) $ "Delay" <++> go appPrec tm
      go d (PForce _ tm) = parenthesise (d > appPrec) $ "Force" <++> go appPrec tm
      go d (PImplicitApp _ f Nothing a) =
        parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> "@" <+> braces (go startPrec a)
      go d (PImplicitApp _ f (Just n) (PRef _ a)) =
        parenthesise (d > appPrec) $ group $
          if n == a
             then go leftAppPrec f <++> braces (pretty n)
             else go leftAppPrec f <++> braces (pretty n <++> equals <++> pretty a)
      go d (PImplicitApp _ f (Just n) a) =
        parenthesise (d > appPrec) $ group $ go leftAppPrec f <++> braces (pretty n <++> equals <++> go d a)
      go d (PSearch _ _) = pragma "%search"
      go d (PQuote _ tm) = parenthesise (d > appPrec) $ "`" <+> parens (go startPrec tm)
      go d (PQuoteName _ n) = parenthesise (d > appPrec) $ "`" <+> braces (braces (pretty n))
      go d (PQuoteDecl _ tm) = parenthesise (d > appPrec) $ "`" <+> brackets (angles (angles (pretty "declaration")))
      go d (PUnquote _ tm) = parenthesise (d > appPrec) $ "~" <+> parens (go startPrec tm)
      go d (PRunElab _ tm) = parenthesise (d > appPrec) $ pragma "%runElab" <++> go startPrec tm
      go d (PPrimVal _ c) = pretty c
      go d (PHole _ _ n) = meta (pretty (strCons '?' n))
      go d (PType _) = pretty "Type"
      go d (PAs _ n p) = pretty n <+> "@" <+> go d p
      go d (PDotted _ p) = dot <+> go d p
      go d (PImplicit _) = "_"
      go d (PInfer _) = "?"
      go d (POp _ op x y) = parenthesise (d > appPrec) $ group $ go startPrec x <++> pretty op <++> go startPrec y
      go d (PPrefixOp _ op x) = parenthesise (d > appPrec) $ pretty op <+> go startPrec x
      go d (PSectionL _ op x) = parens (pretty op <++> go startPrec x)
      go d (PSectionR _ x op) = parens (go startPrec x <++> pretty op)
      go d (PEq fc l r) = parenthesise (d > appPrec) $ go startPrec l <++> equals <++> go startPrec r
      go d (PBracketed _ tm) = parens (go startPrec tm)
      go d (PDoBlock _ ns ds) = parenthesise (d > appPrec) $ group $ align $ hang 2 $ do_ <++> (vsep $ punctuate semi (prettyDo <$> ds))
      go d (PBang _ tm) = "!" <+> go d tm
      go d (PIdiom _ tm) = enclose (pretty "[|") (pretty "|]") (go startPrec tm)
      go d (PList _ xs) = brackets (group $ align $ vsep $ punctuate comma (go startPrec <$> xs))
      go d (PPair _ l r) = group $ parens (go startPrec l <+> comma <+> line <+> go startPrec r)
      go d (PDPair _ l (PImplicit _) r) = group $ parens (go startPrec l <++> pretty "**" <+> line <+> go startPrec r)
      go d (PDPair _ l ty r) = group $ parens (go startPrec l <++> colon <++> go startPrec ty <++> pretty "**" <+> line <+> go startPrec r)
      go d (PUnit _) = "()"
      go d (PIfThenElse _ x t e) =
        parenthesise (d > appPrec) $ group $ align $ hang 2 $ vsep
          [keyword "if" <++> go startPrec x, keyword "then" <++> go startPrec t, keyword "else" <++> go startPrec e]
      go d (PComprehension _ ret es) =
          group $ brackets (go startPrec (dePure ret) <++> pipe <++> vsep (punctuate comma (prettyDo . deGuard <$> es)))
        where
          dePure : PTerm -> PTerm
          dePure tm@(PApp _ (PRef _ n) arg) = if dropNS n == UN "pure" then arg else tm
          dePure tm = tm

          deGuard : PDo -> PDo
          deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg)) = if dropNS n == UN "guard" then DoExp fc arg else tm
          deGuard tm = tm
      go d (PRewrite _ rule tm) =
        parenthesise (d > appPrec) $ group $ rewrite_ <++> go startPrec rule <+> line <+> in_ <++> go startPrec tm
      go d (PRange _ start Nothing end) =
        brackets (go startPrec start <++> pretty ".." <++> go startPrec end)
      go d (PRange _ start (Just next) end) =
        brackets (go startPrec start <+> comma <++> go startPrec next <++> pretty ".." <++> go startPrec end)
      go d (PRangeStream _ start Nothing) = brackets (go startPrec start <++> pretty "..")
      go d (PRangeStream _ start (Just next)) =
        brackets (go startPrec start <+> comma <++> go startPrec next <++> pretty "..")
      go d (PUnifyLog _ lvl tm) = go d tm
      go d (PPostfixProjs fc rec fields) =
        parenthesise (d > appPrec) $ go startPrec rec <++> dot <+> concatWith (surround dot) (go startPrec <$> fields)
      go d (PPostfixProjsSection fc fields args) =
        parens (dot <+> concatWith (surround dot) (go startPrec <$> fields) <+> fillSep (go appPrec <$> args))
      go d (PWithUnambigNames fc ns rhs) = parenthesise (d > appPrec) $ group $ with_ <++> pretty ns <+> line <+> go startPrec rhs

export
render : {auto o : Ref ROpts REPLOpts} -> Doc IdrisAnn -> Core String
render doc = do
  consoleWidth <- getConsoleWidth
  color <- getColor
  opts <- case consoleWidth of
               Nothing => do cols <- coreLift getTermCols
                             pure $ MkLayoutOptions (AvailablePerLine cols 1)
               Just 0 => pure $ MkLayoutOptions Unbounded
               Just cw => pure $ MkLayoutOptions (AvailablePerLine (cast cw) 1)
  let layout = layoutPretty opts doc
  pure $ renderString $ if color then reAnnotateS colorAnn layout else unAnnotateS layout

export
renderWithoutColor : {auto o : Ref ROpts REPLOpts} -> Doc IdrisAnn -> Core String
renderWithoutColor doc = do
  consoleWidth <- getConsoleWidth
  opts <- case consoleWidth of
               Nothing => do cols <- coreLift getTermCols
                             pure $ MkLayoutOptions (AvailablePerLine cols 1)
               Just 0 => pure $ MkLayoutOptions Unbounded
               Just cw => pure $ MkLayoutOptions (AvailablePerLine (cast cw) 1)
  let layout = layoutPretty opts doc
  pure $ renderString $ unAnnotateS layout

ext: idr


text:
import Data.Vect
double : Num ty => ty -> ty
double x = x * x

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

twice : (a -> a) -> a -> a
twice f x = f (f x)

quadruple : Num a => a -> a
quadruple = twice double

fourInts : Vect 4 Int
fourInts = [0, 1, 2, 3]
sixInts : Vect 6 Int
sixInts = [4, 5, 6, 7, 8, 9]

let tenInts  = fourInts ++ sixInts

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module IR.Lens

import Control.Category

data Store s a = MkStore (s -> a) s

class Functor w => Comonad (w : Type -> Type) where
  extract : w a -> a
  extend : (w a -> b) -> w a -> w b

class Comonad w => VerifiedComonad (w : Type -> Type) where
  comonadLaw1 : (wa : w a) ->
                extend extract wa = wa
  comonadLaw2 : (f : w a -> b) ->
                (wa : w a) ->
                extract (extend f wa) = f wa
  comonadLaw3 : (f : w b -> c) ->
                (g : w a -> b) ->
                (wa : w a) ->
                extend f (extend g wa) = extend (\d => f (extend g d)) wa

instance Functor (Store s) where
  map f (MkStore g a) = MkStore (f . g) a

instance Comonad (Store s) where
  extract (MkStore f a) = f a
  extend f (MkStore g a) = MkStore (\b => f (MkStore g b)) a

instance VerifiedComonad (Store s) where
  comonadLaw1 (MkStore f a) = ?storeIdentityProof
  comonadLaw2 f (MkStore g a) = refl
  comonadLaw3 f g (MkStore h a) = refl

-- TODO: This is evil.
-- Supposedly (jonsterling) this definition used to work without the believe_me.
eta : (f : a -> b) -> f = (\c => f c)
eta g = believe_me refl {g}

storeIdentityProof = proof
  intros
  rewrite eta f
  trivial

pos : Store s a -> s
pos (MkStore _ s) = s

peek : s -> Store s a -> a
peek s (MkStore f _) = f s

peeks : (s -> s) -> Store s a -> a
peeks f (MkStore g s) = g (f s)

data Lens a b = MkLens (a -> Store b a)

instance Category Lens where
  id = MkLens (MkStore id)
  (.) (MkLens f) (MkLens g) = MkLens (\a => case g a of
    MkStore ba b => case f b of
      MkStore cb c => MkStore (Prelude.Basics.(.) ba cb) c)

lens : (a -> b) -> (b -> a -> a) -> Lens a b
lens f g = MkLens (\a => MkStore (\b => g b a) (f a))

iso : (a -> b) -> (b -> a) -> Lens a b
iso f g = MkLens (\a => MkStore g (f a))

getL : Lens a b -> a -> b
getL (MkLens f) a = pos (f a)

setL : Lens a b -> b -> a -> a
setL (MkLens f) b = peek b . f

modL : Lens a b -> (b -> b) -> a -> a
modL (MkLens f) g = peeks g . f

infixr 0 ^$
(^$) : Lens a b -> a -> b
(^$) = getL

infixr 4 ^=
(^=) : Lens a b -> b -> a -> a
(^=) = setL

infixr 4 ^%=
(^%=) : Lens a b -> (b -> b) -> a -> a
(^%=) = modL

max_stars_repo_name: puffnfresh/iridium

max_issues_repo_name: victoredwardocallaghan/iridium

max_forks_repo_name: victoredwardocallaghan/iridium


text:
module Data.Fufunctor

import Data.Morphisms

%default total
%access public export
%language LinearTypes

-- FuFunctor is dual to Zifunctor
-- More precisely dual would be t c b a, but in current form
-- it is already used in ZIO library and (Schedule)
-- also it match the Function2 shape a -> b -> c

-- Since it is not exact dual the name is not CoZifunctor but Function2 Functor
-- or FuFunctor in short
interface Fufunctor (t : Type -> Type -> Type -> Type) where
  fumap : (rr -> r) -> (ee -> e) -> (a -> aa) -> t r e a -> t rr ee aa

  dimap : (rr -> r) -> (a -> aa) -> t r e a -> t rr e aa
  dimap r = fumap r id

  dimapRight : (ee -> e) -> (a -> aa) -> t r e a -> t r ee aa
  dimapRight e a = fumap id e a

  map : (a -> aa) -> t r e a -> t r e aa
  map = fumap id id

  contramap : (rr -> r) -> t r e a -> t rr e a
  contramap r = fumap r id id

-- Fufunctor Trimorphism where
--   fumap f g h (Trimo fa) = Trimo ( \ee -> \aa -> h (fa (f ee) (g aa)) )

max_stars_repo_name: lemastero/Idris-Trifunctors

max_issues_repo_name: lemastero/Idris-Trifunctors

max_forks_repo_name: lemastero/Idris-Trifunctors


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
||| This is the root module for the Idris API to XLA.
module XLA

max_stars_repo_name: joelberkeley/spidr

max_issues_repo_name: joelberkeley/spidr

max_forks_repo_name: joelberkeley/spidr


text:
-- WordLength.idr
--

allLengths : List String -> List Nat
allLengths [] = []
allLengths (word :: words) = length word :: allLengths words

-- demonstrate pattern matching
invert : Bool -> Bool
invert False = True
invert True = False

describeList : List Int -> String
describeList [] = "Empty"
describeList (x :: xs) = "Non-empty, tail = " ++ show xs

xor : Bool -> Bool -> Bool
xor False y = y
xor True y = not y

isEven : Nat -> Bool
isEven Z = True
isEven (S k) = not (isEven k)

-- mutally definde functions
mutual
  isEven2 : Nat -> Bool
  isEven2 Z = True
  isEven2 (S k) = isOdd2 k

  isOdd2 : Nat -> Bool
  isOdd2 Z = False
  isOdd2 (S k) = isEven2 k

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
-- Example stolen from https://github.com/edwinb/idris-php,
-- with the numbers changed to make it run for longer

module Main

-- this speeds up the Idris native version a bit.
%flag C "-O3"

pythag : Int -> List (Int, Int, Int)
pythag max = [(x, y, z) | z <- [1..max], y <- [1..z], x <- [1..y],
                              x * x + y *y == z * z]

main : IO ()
main = putStrLn (show (pythag 500))

max_stars_repo_name: ioanluca/real-world-idris

max_issues_repo_name: ioanluca/real-world-idris

max_forks_repo_name: ioanluca/real-world-idris


text:
module Main

-- LFExp
-- LFLog
-- LFSin
-- LFCos
-- LFTan
-- LFASin
-- LFACos
-- LFATan
-- LFATan2

input : List (String, String)
input = [
  ("exp", "1"),
  ("log", "1"),
  ("sin", "1"),
  ("cos", "1"),
  ("tan", "1")
]

main : IO ()
main = traverse_ (printLn . evalInput) input
where
  evalInput : (String, String) -> Double
  evalInput ("exp", x) = exp (cast x)
  evalInput ("log", x) = log (cast x)
  evalInput ("sin", x) = sin (cast x)
  evalInput ("cos", x) = cos (cast x)
  evalInput ("tan", x) = tan (cast x)

max_stars_repo_name: asandroq/idris-gambit

max_issues_repo_name: asandroq/idris-gambit

max_forks_repo_name: asandroq/idris-gambit


text:
module Control.Monad.Reader.Interface

import Control.Monad.Maybe
import Control.Monad.Error.Either
import Control.Monad.Reader.Reader
import Control.Monad.State.State
import Control.Monad.RWS.CPS
import Control.Monad.Trans
import Control.Monad.Writer.CPS

%default total

||| A computation which runs in a static context and produces an output
public export
interface Monad m => MonadReader stateType m | m where
  ||| Get the context
  ask : m stateType

  ||| `local f c` runs the computation `c` in an environment modified by `f`.
  local : (stateType -> stateType) -> m a -> m a

||| Evaluate a function in the context held by this computation
public export
asks : MonadReader stateType m => (stateType -> a) -> m a
asks f = map f ask

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

public export %inline
Monad m => MonadReader stateType (ReaderT stateType m) where
  ask = MkReaderT (\st => pure st)

  local f (MkReaderT action) = MkReaderT (action . f)

public export %inline
Monad m => MonadReader r (RWST r w s m) where
  ask       = MkRWST $ \r,s,w => pure (r,s,w)
  local f m = MkRWST $ \r,s,w => unRWST m (f r) s w

public export %inline
MonadReader r m => MonadReader r (EitherT e m) where
  ask = lift ask
  local = mapEitherT . local

public export %inline
MonadReader r m => MonadReader r (MaybeT m) where
  ask = lift ask
  local = mapMaybeT . local

public export %inline
MonadReader r m => MonadReader r (StateT s m) where
  ask = lift ask
  local = mapStateT . local

public export %inline
MonadReader r m => MonadReader r (WriterT w m) where
  ask   = lift ask

  -- this differs from the implementation in the mtl package
  -- which uses mapWriterT. However, it seems strange that
  -- this should require a Monoid instance to further
  -- accumulate values, while the implementation of
  -- MonadReader for RWST does no such thing.
  local f (MkWriterT m) = MkWriterT $ \w => local f (m w)


text:
module Examples.CSS.Fractals

import Data.Vect
import Examples.CSS.Colors
import public Examples.CSS.Core
import Rhone.JS
import Text.CSS

--------------------------------------------------------------------------------
--          IDs
--------------------------------------------------------------------------------

public export
out : ElemRef HTMLDivElement
out = Id Div "fractals_out"

public export
btnRun : ElemRef HTMLButtonElement
btnRun = Id Button "fractals_run"

public export
txtIter : ElemRef HTMLInputElement
txtIter = Id Input "fractals_iterations"

public export
txtRedraw : ElemRef HTMLInputElement
txtRedraw = Id Input "fractals_redrawdelay"

--------------------------------------------------------------------------------
--          Classes
--------------------------------------------------------------------------------

export
fractalContent : String
fractalContent = "fractals_content"

export
lblIter : String
lblIter = "fractals_lbliter"

export
lblDelay : String
lblDelay = "fractals_lbldelay"

--------------------------------------------------------------------------------
--          Rules
--------------------------------------------------------------------------------

data Tag = LIter | IIter | LDel | IDel | BRun | Fract | Dot

AreaTag Tag where
  showTag LIter = "LIter"
  showTag IIter = "IIter"
  showTag LDel  = "LDel"
  showTag IDel  = "IDel"
  showTag BRun  = "BRun"
  showTag Fract = "Fract"
  showTag Dot   = "."

export
css : List (Rule 1)
css =
  [ Media "min-width: 300px"
      [ class fractalContent !!
          [ Display             .= Area
              (replicate 4 MinContent)
              [MaxContent, MaxContent]
              [ [LIter, IIter]
              , [LDel,  IDel ]
              , [Dot,   BRun ]
              , [Fract, Fract]
              ]

          , ColumnGap           .= px 10
          , RowGap              .= px 10
          , Padding             .= VH (px 20) (px 10)
          ]
      ]

  , Media "min-width: 800px"
      [ class fractalContent !!
          [ Display             .= Area
              (replicate 4 MinContent)
              [MaxContent, MaxContent, fr 1]
              [ [LIter, IIter, Fract]
              , [LDel,  IDel,  Fract]
              , [Dot,   BRun,  Fract]
              , [Dot,   Dot,   Fract]
              ]

          , ColumnGap           .= px 10
          , RowGap              .= px 10
          , Padding             .= VH (px 20) (px 10)
          ]
      ]
  , class lblIter !! [ GridArea .= LIter ]

  , idRef txtIter !!
      [ GridArea        .= IIter
      , TextAlign       .= End
      ]

  , class lblDelay !! [ GridArea .= LDel ]

  , idRef txtRedraw !!
      [ GridArea        .= IDel
      , TextAlign       .= End
      ]

  , idRef btnRun !! [ GridArea .= BRun ]

  , idRef out !!
      [ JustifySelf     .= Center
      , GridArea        .= Fract
      , BorderStyle     .= Left Solid
      , BorderWidth     .= Left (px 2)
      , BorderColor     .= Left base80
      , MaxWidth        .= px 500
      , Width           .= px 500
      ]
  ]


text:
||| Evaluation strategies for GRL instances.
|||
||| A evaluation strategies consists of the following three steps.
|||
||| 1. Initialize the evaluation values for the preselected strategy.
||| 2. Perform forward propagation of the evaluation values to other elements.
||| 3. Calculate the satisfaction of the actors.
|||
||| Once completed this module will provide the strategies described
||| in Amyot2010egm: Qualitative, Quantitative, and Hybrid. Currently
||| only the qualitative evaluation is provided.
|||
module GRL.Eval

import GRL.Common
import GRL.Model

import public GRL.Eval.Qualitative
import public GRL.Eval.Forward
import public GRL.Eval.Strategy
import public GRL.Eval.Common

public export
data EvalAlgo = FORWARD | HYBRID | BACKWARDS

export
evalModel : GModel -> Maybe Strategy -> EvalResult
evalModel g s = forwardEval s g

export
evaluate : EvalAlgo -> Maybe Strategy -> GModel -> EvalResult
evaluate FORWARD   s g = forwardEval s g
evaluate BACKWARDS s g = forwardEval s g
evaluate HYBRID    s g = forwardEval s g

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

max_stars_repo_name: jfdm/idris-grl

max_issues_repo_name: jfdm/idris-grl

max_forks_repo_name: jfdm/idris-grl


text:
module Program

import CommonTestingStuff

export
beforeString : String
beforeString = "before coop"

export
program : PrintString m => CanSleep m => Zippable m => m ()
program = do
  offset <- currentTime
  printTime offset "start"
  res <- zipWith (++)
    (for [1, 2, 3, 4, 5] $ \i => do
      printTime offset "proc 1, before 1000, \{show i}"
      sleepFor 1.seconds
      printTime offset "proc 1, before 2000, \{show i}"
      sleepFor 2.seconds
      pure $ the Int $ i * 10)
    (for [10, 20, 30, 40, 50, 60, 70, 80, 90, 95] $ \i => do
      printTime offset "                                proc 2, before 350, \{show i}"
      sleepFor 350.millis
      printTime offset "                                proc 2, before 750, \{show i}"
      sleepFor 750.millis
      pure $ the Int $ i * 10)
  printTime offset $ "res: " ++ show res
  sleepFor 1.seconds
  printTime offset "end"


text:
module Main
import CFFI

%lib C "tensorflow"
%include C "tensorflow/c/c_api.h"
-- %include C "/usr/include/tensorflow/c/c_api.h"
-- %link C "testlib.o"

-- data TF_Tensor
-- IO (Raw TF_Tensor) works,but c warns assignment from incompatible pointer type
-- data TF_Status2:(a:Type)->Type where --safer way
--  TF_Status22:TF_Status2 Ptr

TF_Status : Type
TF_Status = Ptr -- attention!

-- Tfs : Raw TF_Status
-- Tfs = MkRaw TF_Status
{-
typedef enum TF_Code {
  TF_OK = 0,
  TF_CANCELLED = 1,
  TF_UNKNOWN = 2,
  TF_INVALID_ARGUMENT = 3,
  TF_DEADLINE_EXCEEDED = 4,
  TF_NOT_FOUND = 5,
  TF_ALREADY_EXISTS = 6,
  TF_PERMISSION_DENIED = 7,
  TF_UNAUTHENTICATED = 16,
  TF_RESOURCE_EXHAUSTED = 8,
  TF_FAILED_PRECONDITION = 9,
  TF_ABORTED = 10,
  TF_OUT_OF_RANGE = 11,
  TF_UNIMPLEMENTED = 12,
  TF_INTERNAL = 13,
  TF_UNAVAILABLE = 14,
  TF_DATA_LOSS = 15,
} TF_Code;

17 fields !
-}
TF_Code_struct : Composite
TF_Code_struct = STRUCT $ replicate 17 I32

tfNewStatus : IO TF_Status
tfNewStatus = foreign FFI_C "TF_NewStatus" (IO TF_Status)

tfGetCode : TF_Status ->IO Int
tfGetCode = foreign FFI_C "TF_Code" (TF_Status ->IO Int)

tfVersion : IO String
tfVersion = foreign FFI_C "TF_Version" (IO String)

|||Always returns an empty string if TF_GetCode(s) is  TF_OK.
tfMessage : TF_Status -> IO String
tfMessage = foreign FFI_C "TF_Message" (TF_Status -> IO String)

TF_Buffer : Type
TF_Buffer = Ptr

TF_Library : Type
TF_Library = Ptr

||| Get the OpList of OpDefs defined in the library pointed by lib_handle,like matmul,placeholder,etc
tfGetOpList : TF_Library->IO TF_Buffer
tfGetOpList = foreign FFI_C "TF_GetOpList" (TF_Library->IO TF_Buffer )

main : IO ()
main = do
     ver<-tfVersion
     s<-tfNewStatus
     msg<-tfMessage s
     putStrLn $ "tfMessage is : " ++ msg
     putStrLn $ "tfVersion is : " ++ ver

max_stars_repo_name: doofin/differentiable-idris

max_issues_repo_name: doofin/differentiable-idris

max_forks_repo_name: doofin/differentiable-idris


text:
module Solutions.Eq

import Data.HList
import Data.Vect
import Decidable.Equality

%default total

data ColType = I64 | Str | Boolean | Float

Schema : Type
Schema = List ColType

IdrisType : ColType -> Type
IdrisType I64     = Int64
IdrisType Str     = String
IdrisType Boolean = Bool
IdrisType Float   = Double

Row : Schema -> Type
Row = HList . map IdrisType

record Table where
  constructor MkTable
  schema : Schema
  size   : Nat
  rows   : Vect size (Row schema)

data SameColType : (c1, c2 : ColType) -> Type where
  SameCT : SameColType c1 c1

--------------------------------------------------------------------------------
--          Equality as a Type
--------------------------------------------------------------------------------

-- 1

sctReflexive : SameColType c1 c1
sctReflexive = SameCT

-- 2

sctSymmetric : SameColType c1 c2 -> SameColType c2 c1
sctSymmetric SameCT = SameCT

-- 3

sctTransitive : SameColType c1 c2 -> SameColType c2 c3 -> SameColType c1 c3
sctTransitive SameCT SameCT = SameCT

-- 4

sctCong : (f : ColType -> a) -> SameColType c1 c2 -> f c1 = f c2
sctCong f SameCT = Refl

-- 5

natEq : (n1,n2 : Nat) -> Maybe (n1 = n2)
natEq 0     0     = Just Refl
natEq (S k) (S j) = cong S <$> natEq k j
natEq (S k) 0     = Nothing
natEq 0     (S _) = Nothing

-- 6

appRows : {ts1 : _} -> Row ts1 -> Row ts2 -> Row (ts1 ++ ts2)
appRows {ts1 = []}     Nil      y = y
appRows {ts1 = _ :: _} (h :: t) y = h :: appRows t y

zip : Table -> Table -> Maybe Table
zip (MkTable s1 m rs1) (MkTable s2 n rs2) = case natEq m n of
  Just Refl => Just $ MkTable _ _ (zipWith appRows rs1 rs2)
  Nothing   => Nothing

--------------------------------------------------------------------------------
--          Programs as Proofs
--------------------------------------------------------------------------------

-- 1

mapIdEither : (ea : Either e a) -> map Prelude.id ea = ea
mapIdEither (Left ve)  = Refl
mapIdEither (Right va) = Refl

-- 2

mapIdList : (as : List a) -> map Prelude.id as = as
mapIdList []        = Refl
mapIdList (x :: xs) = cong (x ::) $ mapIdList xs

-- 3

data BaseType = DNABase | RNABase

data Nucleobase : BaseType -> Type where
  Adenine  : Nucleobase b
  Cytosine : Nucleobase b
  Guanine  : Nucleobase b
  Thymine  : Nucleobase DNABase
  Uracile  : Nucleobase RNABase

NucleicAcid : BaseType -> Type
NucleicAcid = List . Nucleobase

complementBase : (b : BaseType) -> Nucleobase b -> Nucleobase b
complementBase DNABase Adenine  = Thymine
complementBase RNABase Adenine  = Uracile
complementBase _       Cytosine = Guanine
complementBase _       Guanine  = Cytosine
complementBase _       Thymine  = Adenine
complementBase _       Uracile  = Adenine

complement : (b : BaseType) -> NucleicAcid b -> NucleicAcid b
complement b = map (complementBase b)

complementBaseId :  (b  : BaseType)
                 -> (nb : Nucleobase b)
                 -> complementBase b (complementBase b nb) = nb
complementBaseId DNABase Adenine  = Refl
complementBaseId RNABase Adenine  = Refl
complementBaseId DNABase Cytosine = Refl
complementBaseId RNABase Cytosine = Refl
complementBaseId DNABase Guanine  = Refl
complementBaseId RNABase Guanine  = Refl
complementBaseId DNABase Thymine  = Refl
complementBaseId RNABase Uracile  = Refl

complementId :  (b  : BaseType)
             -> (na : NucleicAcid b)
             -> complement b (complement b na) = na
complementId b []        = Refl
complementId b (x :: xs) =
  cong2 (::) (complementBaseId b x) (complementId b xs)

-- 4

replaceVect : Fin n -> a -> Vect n a -> Vect n a
replaceVect FZ     v (x :: xs) = v :: xs
replaceVect (FS k) v (x :: xs) = x :: replaceVect k v xs

indexReplace :  (ix : Fin n)
             -> (v : a)
             -> (as : Vect n a)
             -> index ix (replaceVect ix v as) = v
indexReplace FZ     v (x :: xs) = Refl
indexReplace (FS k) v (x :: xs) = indexReplace k v xs

-- 5

insertVect : (ix : Fin (S n)) -> a -> Vect n a -> Vect (S n) a
insertVect FZ     v xs        = v :: xs
insertVect (FS k) v (x :: xs) = x :: insertVect k v xs

indexInsert :  (ix : Fin (S n))
             -> (v : a)
             -> (as : Vect n a)
             -> index ix (insertVect ix v as) = v
indexInsert FZ     v xs        = Refl
indexInsert (FS k) v (x :: xs) = indexInsert k v xs

--------------------------------------------------------------------------------
--          Into the Void
--------------------------------------------------------------------------------

-- 1

Uninhabited (Vect (S n) Void) where
  uninhabited (_ :: _) impossible

-- 2

Uninhabited a => Uninhabited (Vect (S n) a) where
  uninhabited = uninhabited . head

-- 3

notSym : Not (a = b) -> Not (b = a)
notSym f prf = f $ sym prf

-- 4

notTrans : a = b -> Not (b = c) -> Not (a = c)
notTrans ab f ac = f $ trans (sym ab) ac

-- 5

data Crud : (i : Type) -> (a : Type) -> Type where
  Create : (value : a) -> Crud i a
  Update : (id : i) -> (value : a) -> Crud i a
  Read   : (id : i) -> Crud i a
  Delete : (id : i) -> Crud i a

Uninhabited a => Uninhabited i => Uninhabited (Crud i a) where
  uninhabited (Create value)    = uninhabited value
  uninhabited (Update id value) = uninhabited value
  uninhabited (Read id)         = uninhabited id
  uninhabited (Delete id)       = uninhabited id

-- 6

namespace DecEq
  DecEq ColType where
    decEq I64 I64         = Yes Refl
    decEq I64 Str         = No $ \case Refl impossible
    decEq I64 Boolean     = No $ \case Refl impossible
    decEq I64 Float       = No $ \case Refl impossible

    decEq Str I64         = No $ \case Refl impossible
    decEq Str Str         = Yes Refl
    decEq Str Boolean     = No $ \case Refl impossible
    decEq Str Float       = No $ \case Refl impossible

    decEq Boolean I64     = No $ \case Refl impossible
    decEq Boolean Str     = No $ \case Refl impossible
    decEq Boolean Boolean = Yes Refl
    decEq Boolean Float   = No $ \case Refl impossible

    decEq Float I64       = No $ \case Refl impossible
    decEq Float Str       = No $ \case Refl impossible
    decEq Float Boolean   = No $ \case Refl impossible
    decEq Float Float     = Yes Refl

-- 7

ctNat : ColType -> Nat
ctNat I64     = 0
ctNat Str     = 1
ctNat Boolean = 2
ctNat Float   = 3

ctNatInjective : (c1,c2 : ColType) -> ctNat c1 = ctNat c2 -> c1 = c2
ctNatInjective I64     I64     Refl = Refl
ctNatInjective Str     Str     Refl = Refl
ctNatInjective Boolean Boolean Refl = Refl
ctNatInjective Float   Float   Refl = Refl

DecEq ColType where
  decEq c1 c2 = case decEq (ctNat c1) (ctNat c2) of
    Yes prf    => Yes $ ctNatInjective c1 c2 prf
    No  contra => No $ contra . cong ctNat

--------------------------------------------------------------------------------
--          Rewrite Rules
--------------------------------------------------------------------------------

-- 1

psuccRightSucc : (m,n : Nat) -> S (m + n) = m + S n
psuccRightSucc 0     n = Refl
psuccRightSucc (S k) n = cong S $ psuccRightSucc k n

-- 2

minusSelfZero : (n : Nat) -> minus n n = 0
minusSelfZero 0     = Refl
minusSelfZero (S k) = minusSelfZero k

-- 3

minusZero : (n : Nat) -> minus n 0 = n
minusZero 0     = Refl
minusZero (S k) = Refl

-- 4

timesOneLeft : (n : Nat) -> 1 * n = n
timesOneLeft 0     = Refl
timesOneLeft (S k) = cong S $ timesOneLeft k

timesOneRight : (n : Nat) -> n * 1 = n
timesOneRight 0     = Refl
timesOneRight (S k) = cong S $ timesOneRight k

-- 5

plusCommutes : (m,n : Nat) -> m + n = n + m
plusCommutes 0     n = rewrite plusZeroRightNeutral n in Refl
plusCommutes (S k) n =
  rewrite sym (psuccRightSucc n k)
  in cong S (plusCommutes k n)

-- 6

mapOnto : (a -> b) -> Vect k b -> Vect m a -> Vect (k + m) b
mapOnto            _ xs []        =
  rewrite plusZeroRightNeutral k in reverse xs
mapOnto {m = S m'} f xs (y :: ys) =
  rewrite sym (plusSuccRightSucc k m') in mapOnto f (f y :: xs) ys

mapTR : (a -> b) -> Vect n a -> Vect n b
mapTR f = mapOnto f Nil

-- 7

mapAppend :  (f : a -> b)
          -> (xs : List a)
          -> (ys : List a)
          -> map f (xs ++ ys) = map f xs ++ map f ys
mapAppend f []        ys = Refl
mapAppend f (x :: xs) ys = cong (f x ::) $ mapAppend f xs ys

-- 8

zip2 : Table -> Table -> Maybe Table
zip2 (MkTable s1 m rs1) (MkTable s2 n rs2) = case decEq m n of
  Yes Refl =>
    let rs2 = zipWith (++) rs1 rs2
     in Just $ MkTable (s1 ++ s2) _ (rewrite mapAppend IdrisType s1 s2 in rs2)
  No  _    => Nothing


text:
> module SequentialDecisionProblems.applications.Main

> import Data.Vect
> -- import Data.Fin
> -- import Data.List
> -- import Data.List.Quantifiers
> import Data.So
> import Effects
> import Effect.Exception
> import Effect.StdIO

> import SequentialDecisionProblems.CoreTheory
> import SequentialDecisionProblems.FullTheory
> import SequentialDecisionProblems.TabBackwardsInduction
> import SequentialDecisionProblems.Utils
> import SequentialDecisionProblems.NonDeterministicDefaults
> import SequentialDecisionProblems.CoreTheoryOptDefaults
> import SequentialDecisionProblems.FullTheoryOptDefaults
> import SequentialDecisionProblems.TabBackwardsInductionOptDefaults

> import BoundedNat.BoundedNat
> -- import FastSimpleProb.SimpleProb
> -- import FastSimpleProb.BasicOperations
> -- import FastSimpleProb.BasicProperties
> -- import FastSimpleProb.MonadicOperations
> -- import FastSimpleProb.MonadicProperties
> -- import FastSimpleProb.Measures
> -- import FastSimpleProb.MeasuresProperties
> -- import FastSimpleProb.Operations
> -- import Sigma.Sigma
> import Double.Predicates
> -- import Double.Postulates
> -- import Double.Operations
> -- import Double.Properties
> import NonNegDouble.NonNegDouble
> -- import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Properties
> import NonNegDouble.Predicates
> import NonNegDouble.LTEProperties
> -- import Finite.Predicates
> -- import Finite.Operations
> -- import Finite.Properties
> -- import Decidable.Predicates
> -- import Decidable.Properties
> -- import LocalEffect.Exception
> -- import LocalEffect.StdIO
> -- import Fin.Operations
> -- import List.Operations
> -- import Unit.Properties

> -- %default total
> %auto_implicits off

> -- %logging 5

* States

> data Tag = V | X | O

> Board : Type
> Board = Vect 9 Tag

> validBoard : Nat -> Board -> Bool

> data ValidBoard : Nat -> Type where
>   MkValidBoard : (t : Nat) -> (b : Board) -> validBoard t b = True -> ValidBoard t

> SequentialDecisionProblems.CoreTheory.State = ValidBoard

* Controls

> Move : Type
> Move = Maybe (LTB 9) -- Nothing is for the case the game is over before 5 rounds

> validMove : (t : Nat) -> ValidBoard t -> Move -> Bool

> data ValidMove : (t : Nat) -> ValidBoard t -> Type where
>   MkValidMove : (t : Nat) -> (b : ValidBoard t) -> (m : Move) -> validMove t b m = True -> ValidMove t b

> SequentialDecisionProblems.CoreTheory.Ctrl = ValidMove

* Transition function

> possible : (t : Nat) -> (b : ValidBoard t) -> (m : ValidMove t b) -> List (ValidBoard (S t))

> SequentialDecisionProblems.CoreTheory.nexts t x y = possible t x y

* |Val| and |LTE|:

> SequentialDecisionProblems.CoreTheory.Val =
>   NonNegDouble.NonNegDouble

> SequentialDecisionProblems.CoreTheory.plus =
>   NonNegDouble.Operations.plus

> SequentialDecisionProblems.CoreTheory.zero =
>   fromInteger 0

> SequentialDecisionProblems.CoreTheory.LTE =
>   NonNegDouble.Predicates.LTE

> SequentialDecisionProblems.FullTheory.reflexiveLTE =
>   NonNegDouble.LTEProperties.reflexiveLTE

> SequentialDecisionProblems.FullTheory.transitiveLTE =
>   NonNegDouble.LTEProperties.transitiveLTE

> SequentialDecisionProblems.FullTheory.monotonePlusLTE =
>   NonNegDouble.LTEProperties.monotonePlusLTE

> SequentialDecisionProblems.CoreTheoryOptDefaults.totalPreorderLTE =
>   NonNegDouble.LTEProperties.totalPreorderLTE

* Reward function

> won  : (t : Nat) -> (b : ValidBoard t) -> Bool
> lost : (t : Nat) -> (b : ValidBoard t) -> Bool

> SequentialDecisionProblems.CoreTheory.reward t x y x' =
>   if won (S t) x'
>   then cast 2.0
>   else if lost (S t) x'
>        then cast 0.0
>        else cast 1.0

> {-

* Completing the problem specification

To be able to apply the verified, generic backwards induction algorithm
of |CoreTheory| to compute optimal policies for our problem, we have to
explain how the decision maker accounts for uncertainties on rewards
induced by uncertainties in the transition function. We first assume
that the decision maker measures uncertain rewards by their expected
value:

> SequentialDecisionProblems.CoreTheory.meas = expectedValue -- worst -- expectedValue
> SequentialDecisionProblems.FullTheory.measMon = monotoneExpectedValue -- monotoneWorst -- monotoneExpectedValue

Further on, we have to implement the notions of viability and
reachability. We start by positing that all states are viable for any
number of steps:

> -- Viable : (n : Nat) -> State t -> Type
> SequentialDecisionProblems.CoreTheory.Viable n x = Unit

From this definition, it trivially follows that all elements of an
arbitrary list of states are viable for an arbitrary number of steps:

> viableLemma : {t, n : Nat} -> (xs : List (State t)) -> All (Viable n) xs
> viableLemma  Nil      = Nil
> viableLemma {t} {n} (x :: xs) = () :: (viableLemma {t} {n} xs)

This fact and the (less trivial) result that simple probability
distributions are never empty, see |nonEmptyLemma| in
|MonadicProperties| in |SimpleProb|, allows us to show that the above
definition of |Viable| fulfills |viableSpec1|:

> -- viableSpec1 : (x : State t) -> Viable (S n) x -> GoodCtrl t x
> SequentialDecisionProblems.CoreTheory.viableSpec1 {t} {n} s v =
>   MkSigma High (ne, av) where
>     ne : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts t s High)
>     ne = nonEmptyLemma (nexts t s High)
>     av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} n) (nexts t s High)
>     av = viableLemma {t = S t} (support (nexts t s High))

> SequentialDecisionProblems.Utils.finiteViable n x = finiteUnit

> SequentialDecisionProblems.Utils.decidableViable n x = decidableUnit

For reachability, we proceed in a similar way. We say that all states
are reachable

> -- Reachable : State t' -> Type
> SequentialDecisionProblems.CoreTheory.Reachable x' = Unit

which immediately implies |reachableSpec1|:

> -- reachableSpec1 : (x : State t) -> Reachable {t' = t} x -> (y : Ctrl t x) -> All (Reachable {t' = S t}) (nexts t x y)
> SequentialDecisionProblems.CoreTheory.reachableSpec1 {t} x r y = all (nexts t x y) where
>   all : (sp : SimpleProb  (State (S t))) -> SequentialDecisionProblems.CoreTheory.All (Reachable {t' = S t}) sp
>   all sp = all' (support sp) where
>     all' : (xs : List (State (S t))) -> Data.List.Quantifiers.All (Reachable {t' = S t}) xs
>     all' Nil = Nil
>     all' (x :: xs) = () :: (all' xs)

and decidability of |Reachable|:

> SequentialDecisionProblems.TabBackwardsInduction.decidableReachable x = decidableUnit

Finally, we have to show that controls are finite

> -- finiteCtrl : {t : Nat} -> (x : State t) -> Finite (Ctrl t x)
> SequentialDecisionProblems.Utils.finiteCtrl _ = finiteLowHigh

and, in order to use the fast, tail-recursive tabulated version of
backwards induction, that states are finite:

> SequentialDecisionProblems.TabBackwardsInduction.finiteState t =
>   finiteTuple4 finiteFin finiteLowHigh finiteAvailableUnavailable finiteGoodBad

* Optimal policies, optimal decisions, ...

We can now apply the results of our |CoreTheory| and of the |FullTheory|
to compute verified optimal policies, possible state-control sequences,
etc. To this end, we need to be able to show the outcome of the decision
process. This means implemeting functions to print states and controls:

> -- showState : {t : Nat} -> State t -> String
> SequentialDecisionProblems.Utils.showState {t} (e, High, Unavailable, Good) =
>   "(" ++ show (finToNat e) ++ ",H,U,G)"
> SequentialDecisionProblems.Utils.showState {t} (e, High, Unavailable,  Bad) =
>   "(" ++ show (finToNat e) ++ ",H,U,B)"
> SequentialDecisionProblems.Utils.showState {t} (e, High,   Available, Good) =
>   "(" ++ show (finToNat e) ++ ",H,A,G)"
> SequentialDecisionProblems.Utils.showState {t} (e, High,   Available,  Bad) =
>   "(" ++ show (finToNat e) ++ ",H,A,B)"
> SequentialDecisionProblems.Utils.showState {t} (e,  Low, Unavailable, Good) =
>   "(" ++ show (finToNat e) ++ ",L,U,G)"
> SequentialDecisionProblems.Utils.showState {t} (e,  Low, Unavailable,  Bad) =
>   "(" ++ show (finToNat e) ++ ",L,U,B)"
> SequentialDecisionProblems.Utils.showState {t} (e,  Low,   Available, Good) =
>   "(" ++ show (finToNat e) ++ ",L,A,G)"
> SequentialDecisionProblems.Utils.showState {t} (e,  Low,   Available,  Bad) =
>   "(" ++ show (finToNat e) ++ ",L,A,B)"

> -- showControl : {t : Nat} -> {x : State t} -> Ctrl t x -> String
> SequentialDecisionProblems.Utils.showCtrl {t} {x}  Low = "L"
> SequentialDecisionProblems.Utils.showCtrl {t} {x} High = "H"

> -- ad-hoc trajectories computation
> adHocPossibleStateCtrlSeqs : {t, n : Nat} ->
>                              (ps : PolicySeq t n) ->
>                              (x : State t) ->
>                              SimpleProb (StateCtrlSeq t n)
> adHocPossibleStateCtrlSeqs {t} {n = Z}         Nil  x =
>   FastSimpleProb.MonadicOperations.ret (Nil x)
> adHocPossibleStateCtrlSeqs {t} {n = S m} (p :: ps') x =
> {-
>   FastSimpleProb.MonadicOperations.fmap ((MkSigma x y) ::) (FastSimpleProb.MonadicOperations.naivebind mx' f) where
>     y   :  Ctrl t x
>     y   =  ctrl (p x () ())
>     mx' :  SimpleProb (State (S t))
>     mx' =  nexts t x y
>     f   :  State (S t) -> M (StateCtrlSeq (S t) m)
>     f   =  adHocPossibleStateCtrlSeqs {n = m} ps'
> ---}
> --{-
>   let y   = ctrl (p x () ()) in
>   let mx' =  nexts t x y in
>   let f   =  adHocPossibleStateCtrlSeqs {n = m} ps' in
>   FastSimpleProb.MonadicOperations.fmap ((MkSigma x y) ::) (FastSimpleProb.MonadicOperations.naivebind mx' f)
> ---}

> constHigh : (t : Nat) -> (n : Nat) -> PolicySeq t n
> constHigh t  Z    = Nil
> constHigh t (S n) = p :: (constHigh (S t) n) where
>   p : Policy t (S n)
>   p x r v = MkSigma High (ne, av) where
>     ne : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts t x High)
>     ne = nonEmptyLemma (nexts t x High)
>     av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} n) (nexts t x High)
>     av = viableLemma {t = S t} (support (nexts t x High))

> ||| Constant low policy sequences
> constLow : (t : Nat) -> (n : Nat) -> PolicySeq t n
> constLow t  Z    = Nil
> constLow t (S n) = p :: (constLow (S t) n) where
>   p : Policy t (S n)
>   p x r v = MkSigma Low (ne, av) where
>     ne : SequentialDecisionProblems.CoreTheory.NotEmpty (nexts t x Low)
>     ne = nonEmptyLemma (nexts t x Low)
>     av : SequentialDecisionProblems.CoreTheory.All (Viable {t = S t} n) (nexts t x Low)
>     av = viableLemma {t = S t} (support (nexts t x Low))

> computation : { [STDIO] } Eff ()
> computation =
>   do putStr ("enter number of steps:\n")
>      nSteps <- getNat
>      putStrLn "nSteps (number of decision steps):"
>      putStrLn ("  " ++ show nSteps)
>
>      putStrLn "crE (crit. cumulated emissions threshold):"
>      putStrLn ("  " ++ show crE)
>      putStrLn "crN (crit. number of decision steps):"
>      putStrLn ("  " ++ show crN)
>
>      putStrLn "pS1 (prob. of staying in a good world, cumulated emissions below crE):"
>      putStrLn ("  " ++ show pS1)
>      putStrLn "pS2 (prob. of staying in a good world, cumulated emissions above crE):"
>      putStrLn ("  " ++ show pS2)
>
>      putStrLn "pA1 (prob. of eff. tech. becoming available, number of steps below crN):"
>      putStrLn ("  " ++ show pA1)
>      putStrLn "pA2 (prob. of eff. tech. becoming available, number of steps above crN):"
>      putStrLn ("  " ++ show pA2)
>
>      putStrLn "pLL (prob. of low emission policies, emissions low, low selected):"
>      putStrLn ("  " ++ show pLL)
>      putStrLn "pLH (prob. of low emission policies, emissions high, low selected):"
>      putStrLn ("  " ++ show pLH)
>      putStrLn "pHL (prob. of high emission policies, emissions low, high selected):"
>      putStrLn ("  " ++ show pHL)
>      putStrLn "pHH (prob. of high emission policies, emissions high, high selected):"
>      putStrLn ("  " ++ show pHH)
>
>      putStrLn "badOverGood (step benefits ratio: bad over good world):"
>      putStrLn ("  " ++ show badOverGood)
>      putStrLn "lowOverGoodUnavailable (benefits ratio: low emissions over step, good world, eff. tech. unavailable):"
>      putStrLn ("  " ++ show lowOverGoodUnavailable)
>      putStrLn "lowOverGoodAvailable (benefits ratio: low emissions over step, good world, eff. tech. available):"
>      putStrLn ("  " ++ show lowOverGoodAvailable)
>      putStrLn "highOverGood (benefits ratio: High emissions over step, good world):"
>      putStrLn ("  " ++ show highOverGood)
>
>      putStrLn "computing constHigh policies ..."
>      constHigh_ps <- pure (constHigh Z nSteps)
>
>      putStrLn "computing constHigh state-control sequences ..."
>      constHigh_mxys <- pure (adHocPossibleStateCtrlSeqs constHigh_ps (FZ, High, Unavailable, Good))
>      putStrLn "pairing constHigh state-control sequences with their values ..."
>      constHigh_mxysv <- pure (possibleStateCtrlSeqsRewards' constHigh_mxys)
>      -- putStrLn "constHigh state-control sequences and their values:"
>      -- putStrLn (showlong constHigh_mxysv)
>
>      putStrLn "computing (naively) the number of constHigh state-control sequences ..."
>      constHigh_n <- pure (length (toList constHigh_mxysv))
>      putStrLn "number of constHigh state-control sequences:"
>      putStrLn ("  " ++ show constHigh_n)
>
>      putStrLn "computing (naively) the most probable constHigh state-control sequence ..."
>      constHigh_xysv <- pure (naiveMostProbableProb constHigh_mxysv)
>      putStrLn "most probable constHigh state-control sequence and its probability:"
>      putStrLn ("  " ++ show constHigh_xysv)
>
>      putStrLn "sorting (naively) the constHigh state-control sequence ..."
>      constHigh_xysvs <- pure (naiveSortToList constHigh_mxysv)
>      putStrLn "most probable constHigh state-control sequences (first 3) and their probabilities:"
>      putStrLn (showlong (take 3 constHigh_xysvs))
>
>      putStrLn "measure of constHigh rewards:"
>      putStrLn ("  " ++ show (meas (SequentialDecisionProblems.CoreTheory.fmap snd constHigh_mxysv)))
>
>      putStrLn "computing constLow policies ..."
>      constLow_ps <- pure (constLow Z nSteps)
>
>      putStrLn "computing constLow state-control sequences ..."
>      constLow_mxys <- pure (adHocPossibleStateCtrlSeqs constLow_ps (FZ, High, Unavailable, Good))
>      putStrLn "pairing constLow state-control sequences with their values ..."
>      constLow_mxysv <- pure (possibleStateCtrlSeqsRewards' constLow_mxys)
>
>      putStrLn "computing (naively) the number of constLow state-control sequences ..."
>      constLow_n <- pure (length (toList constLow_mxysv))
>      putStrLn "number of constLow state-control sequences:"
>      putStrLn ("  " ++ show constLow_n)
>
>      putStrLn "computing (naively) the most probable constLow state-control sequence ..."
>      constLow_xysv <- pure (naiveMostProbableProb constLow_mxysv)
>      putStrLn "most probable constLow state-control sequence and its probability:"
>      putStrLn ("  " ++ show constLow_xysv)
>
>      putStrLn "sorting (naively) the constLow state-control sequence ..."
>      constLow_xysvs <- pure (naiveSortToList constLow_mxysv)
>      putStrLn "most probable constLow state-control sequences (first 3) and their probabilities:"
>      putStrLn (showlong (take 3 constLow_xysvs))
>
>      putStrLn "measure of constLow rewards:"
>      putStrLn ("  " ++ show (meas (SequentialDecisionProblems.CoreTheory.fmap snd constLow_mxysv)))
>
>      putStrLn "computing optimal policies ..."
>      ps <- pure (tabTailRecursiveBackwardsInduction Z nSteps)
>
>      putStrLn "computing possible state-control sequences ..."
>      mxys <- pure (adHocPossibleStateCtrlSeqs ps (FZ, High, Unavailable, Good))
>      putStrLn "pairing possible state-control sequences with their values ..."
>      mxysv <- pure (possibleStateCtrlSeqsRewards' mxys)
>      -- putStrLn "possible state-control sequences and their values:"
>      -- putStrLn (showlong mxysv)
>
>      putStrLn "computing (naively) the number of possible state-control sequences ..."
>      n <- pure (length (toList mxysv))
>      putStrLn "number of possible state-control sequences:"
>      putStrLn ("  " ++ show n)
>
>      putStrLn "computing (naively) the most probable state-control sequence ..."
>      xysv <- pure (naiveMostProbableProb mxysv)
>      putStrLn "most probable state-control sequence and its probability:"
>      putStrLn ("  " ++ show xysv)
>
>      putStrLn "sorting (naively) the possible state-control sequence ..."
>      xysvs <- pure (naiveSortToList mxysv)
>      putStrLn "most probable state-control sequences (first 3) and their probabilities:"
>      putStrLn (showlong (take 3 xysvs))
>
>      putStrLn "measure of possible rewards:"
>      putStrLn ("  " ++ show (meas (SequentialDecisionProblems.CoreTheory.fmap snd mxysv)))

>      putStrLn "done!"

> main : IO ()
> main = run computation

> ---}

-- Local Variables:
-- idris-packages: ("effects")
-- End:

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Web.Raw.Event

import JS
import Web.Internal.EventPrim
import Web.Internal.Types

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

namespace CompositionEvent

  public export
  JSType CompositionEvent where
    parents =  [ UIEvent , Event , Object ]

    mixins =  []

namespace FocusEvent

  public export
  JSType FocusEvent where
    parents =  [ UIEvent , Event , Object ]

    mixins =  []

namespace InputEvent

  public export
  JSType InputEvent where
    parents =  [ UIEvent , Event , Object ]

    mixins =  []

namespace KeyboardEvent

  public export
  JSType KeyboardEvent where
    parents =  [ UIEvent , Event , Object ]

    mixins =  []

  public export
  DOM_KEY_LOCATION_LEFT : UInt32
  DOM_KEY_LOCATION_LEFT = 0x1

  public export
  DOM_KEY_LOCATION_NUMPAD : UInt32
  DOM_KEY_LOCATION_NUMPAD = 0x3

  public export
  DOM_KEY_LOCATION_RIGHT : UInt32
  DOM_KEY_LOCATION_RIGHT = 0x2

  public export
  DOM_KEY_LOCATION_STANDARD : UInt32
  DOM_KEY_LOCATION_STANDARD = 0x0

namespace MouseEvent

  public export
  JSType MouseEvent where
    parents =  [ UIEvent , Event , Object ]

    mixins =  []

namespace UIEvent

  public export
  JSType UIEvent where
    parents =  [ Event , Object ]

    mixins =  []

namespace WheelEvent

  public export
  JSType WheelEvent where
    parents =  [ MouseEvent , UIEvent , Event , Object ]

    mixins =  []

  public export
  DOM_DELTA_LINE : UInt32
  DOM_DELTA_LINE = 0x1

  public export
  DOM_DELTA_PAGE : UInt32
  DOM_DELTA_PAGE = 0x2

  public export
  DOM_DELTA_PIXEL : UInt32
  DOM_DELTA_PIXEL = 0x0

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

namespace CompositionEventInit

  public export
  JSType CompositionEventInit where
    parents =  [ UIEventInit , EventInit , Object ]

    mixins =  []

namespace EventModifierInit

  public export
  JSType EventModifierInit where
    parents =  [ UIEventInit , EventInit , Object ]

    mixins =  []

namespace FocusEventInit

  public export
  JSType FocusEventInit where
    parents =  [ UIEventInit , EventInit , Object ]

    mixins =  []

namespace InputEventInit

  public export
  JSType InputEventInit where
    parents =  [ UIEventInit , EventInit , Object ]

    mixins =  []

namespace KeyboardEventInit

  public export
  JSType KeyboardEventInit where
    parents =  [ EventModifierInit , UIEventInit , EventInit , Object ]

    mixins =  []

namespace MouseEventInit

  public export
  JSType MouseEventInit where
    parents =  [ EventModifierInit , UIEventInit , EventInit , Object ]

    mixins =  []

namespace UIEventInit

  public export
  JSType UIEventInit where
    parents =  [ EventInit , Object ]

    mixins =  []

namespace WheelEventInit

  public export
  JSType WheelEventInit where
    parents =  [ MouseEventInit
               , EventModifierInit
               , UIEventInit
               , EventInit
               , Object
               ]

    mixins =  []


text:
module Main

-- First iteration, complected number generation with labeling

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

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

-- Second iteration, split number generation from labeling

countFrom : Integer -> List Integer
countFrom n = n :: countFrom (n+1)

labelWith : List Integer -> List a -> List (Integer, a)
labelWith _ []  = []
labelWith (x :: xs) (y :: ys) = (x, y) :: labelWith xs ys

-- this works on the REPL because it's lazy
label' : List a -> List (Integer, a)
label' = labelWith (countFrom 0)

-- Third iteration, Infinite Lists!

data InfList : Type -> Type where
  (::) : (value : elem) -> Inf (InfList elem) -> InfList elem
-- there's no [] constructor because infinite lists just don't end

-- countFrom' is a corecursive function that returns codata
total countFrom' : Integer -> InfList Integer
countFrom' x = x :: countFrom' (x + 1)

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

main : IO ()
main = print $ getPrefix 10 (countFrom' 0)

-- the following line doesn't work:
-- main = print $ label' [1,2,3]

max_stars_repo_name: ostera/asdf

max_issues_repo_name: ostera/asdf

max_forks_repo_name: ostera/asdf


text:
import Data.List.Lazy

f : Nat -> (Nat, Nat)
f n = unsafePerformIO $ do
  putStrLn "with \{show n}"
  pure (n+1, n+2)

x : Nat -> (Lazy Nat, Nat)
x n = let (a, b) = f n in
      (delay $ a + b, 1)

y : Nat -> (Lazy Nat, Nat)
y n = let u = f n in
      (delay $ fst u + snd u, 1)

y' : Nat -> (Lazy Nat, Nat)
y' n = let u : (Nat, Nat)
           u = f n in
       (delay $ fst u + snd u, 1)

z : Nat -> (Lazy Nat, Nat)
z n = (delay $ fst (f n) + snd (f n), 1)

-- :exec putStrLn $ show $ snd $ y 4
-- :exec putStrLn $ show $ snd $ y' 4

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
import Data.Buffer

export
data ForeignPtr : Type -> Type where
  MkFP : Buffer -> ForeignPtr a

public export
interface Storable a where

  size : ForeignPtr a -> Int

  peekByteOff : HasIO io => ForeignPtr a -> Int -> io a

  peekElemOff : HasIO io => ForeignPtr a -> Int -> io a
  peekElemOff fp off = peekByteOff fp (off * size fp)

Storable Bits8 where

  size _ = 8
  peekByteOff (MkFP b) off = getBits8 b off


text:
||| Additional FFI help for more interesting C types
module System.FFI
-- Some assumptions are made about the existence of this module in
-- Compiler.CompileExpr

%default total

||| A struct with a name and a list of key-value pairs of field names and their
||| types.
export
data Struct : String -> -- C struct name
              List (String, Type) -> -- field names and types
              Type where

||| A proof that the field exists as an entry in the list of field names and
||| their types.
public export
data FieldType : String -> Type -> List (String, Type) -> Type where
     First : FieldType n t ((n, t) :: ts)
     Later : FieldType n t ts -> FieldType n t (f :: ts)

%extern
prim__getField : {s : _} -> forall fs, ty .
                         Struct s fs -> (n : String) ->
                         FieldType n ty fs -> ty
%extern
prim__setField : {s : _} -> forall fs, ty .
                         Struct s fs -> (n : String) ->
                         FieldType n ty fs -> ty -> PrimIO ()

||| Retrieve the value of the specified field in the given `Struct`.
|||
||| @ s the `Struct` to retrieve the value from
||| @ n the name of the field in the `Struct`.
public export %inline
getField : {sn : _} -> (s : Struct sn fs) -> (n : String) ->
           {auto fieldok : FieldType n ty fs} -> ty
getField s n = prim__getField s n fieldok

||| Set the value of the specified field in the given `Struct`.
|||
||| @ s   the `Struct` in which the field exists
||| @ n   the name of the field to set
||| @ val the value to set the field to
public export %inline
setField : {sn : _} -> (s : Struct sn fs) -> (n : String) ->
           {auto fieldok : FieldType n ty fs} -> (val : ty) -> IO ()
setField s n val = primIO (prim__setField s n fieldok val)

%foreign "C:idris2_malloc, libidris2_support, idris_memory.h"
prim__malloc : (size : Int) -> PrimIO AnyPtr

%foreign "C:idris2_free, libidris2_support, idris_memory.h"
prim__free : AnyPtr -> PrimIO ()

||| Allocate memory with libc `malloc`.
|||
||| @ size the number of bytes to allocate
export
malloc : HasIO io => (size : Int) -> io AnyPtr
malloc size = primIO $ prim__malloc size

||| Release memory with libc `free`.
export
free : HasIO io => AnyPtr -> io ()
free ptr = primIO $ prim__free ptr


text:
module Data.Time.Clock.DiffTime

import Data.So
import Data.Fixed

import Generics.Derive

%default total
%language ElabReflection

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

public export
record DiffTime' (nominal:Bool) where
  constructor SecondsToDiffTime
  seconds : Fixed 12
%runElab derive "DiffTime'" [Generic, Eq, Ord, DecEq]

public export DiffTime : Type
DiffTime = DiffTime' False

public export NominalDiffTime : Type
NominalDiffTime = DiffTime' True

--public export Eq (DiffTime' b) where x == y = x.seconds == y.seconds
--public export Ord (DiffTime' b) where compare x y = compare x.seconds y.seconds
public export
Num (DiffTime' b) where
  x + y = SecondsToDiffTime $ x.seconds + y.seconds
  x * y = SecondsToDiffTime $ x.seconds * y.seconds
  fromInteger x = SecondsToDiffTime $ fromInteger x
public export
Neg (DiffTime' b) where
  negate x = { seconds $= negate } x
  x - y = SecondsToDiffTime $ x.seconds - y.seconds

public export Show (DiffTime' b) where show x = show x.seconds ++ "s"

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

export %inline picosecondsToDiffTime : {nominal:Bool} -> Integer -> DiffTime' nominal
picosecondsToDiffTime x = SecondsToDiffTime $ MkFixed x

export %inline secondsToDiffTime : {nominal:Bool} -> Fixed 12 -> DiffTime' nominal
secondsToDiffTime x = SecondsToDiffTime x

export %inline diffTimeToPicoseconds : {nominal:Bool} -> DiffTime' nominal -> Integer
diffTimeToPicoseconds x = let MkFixed x' = x.seconds in x'

export %inline nominalDay : NominalDiffTime
nominalDay = 86400

export %inline scale : Integer -> DiffTime' b -> DiffTime' b
scale n dt = SecondsToDiffTime $ scale n dt.seconds

export %inline daysToDiffTime : Integer -> NominalDiffTime
daysToDiffTime n = scale n nominalDay

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


text:
module chap07

-- 7.1.6 Exercises
data Shape = Triangle Double Double
           | Rectangle Double Double
           | Circle Double

Eq Shape where
  (==) (Triangle x y) (Triangle x' y') = x == x' && y == y'
  (==) (Rectangle x y) (Rectangle x' y') = x == x' && y == y'
  (==) (Circle d) (Circle d') = d == d'
  (==) _ _ = False

area : Shape -> Double
area (Triangle x y) = x * y / 2
area (Rectangle x y) = x * y
area (Circle x) = pi * x * x

Ord Shape where
    compare x y = compare (area x) (area y)

data Expr num = Val num
              | Add (Expr num) (Expr num)
              | Sub (Expr num) (Expr num)
              | Mul (Expr num) (Expr num)
              | Div (Expr num) (Expr num)
              | Abs (Expr num)

eval : (Neg num, Integral num) => Expr num -> num
eval (Val x) = x
eval (Add x y) = eval x + eval y
eval (Sub x y) = eval x - eval y
eval (Mul x y) = eval x * eval y
eval (Div x y) = eval x `div` eval y
eval (Abs x) = abs (eval x)

-- interface Show a where
--  show : a -> String

-- 7.3.4 Exercises 1
Functor Expr where
    map func (Val x) = Val (func x)
    map func (Add x y) = Add (map func x) (map func y)
    map func (Sub x y) = Sub (map func x) (map func y)
    map func (Mul x y) = Mul (map func x) (map func y)
    map func (Div x y) = Div (map func x) (map func y)
    map func (Abs x) = Abs (map func x)

-- *chap07> map (*2) (the (Expr _) (1 + 2 * 3))
-- Add (Val 2) (Mul (Val 4) (Val 6)) : Expr Integer
-- *chap07> map show (the (Expr _) (1 + 2 * 3))
-- Add (Val "1") (Mul (Val "2") (Val "3")) : Expr String

-- 7.3.4 Exercises 2
data Vect : Nat -> Type -> Type where
     Nil : Vect Z a
     (::) : a -> Vect k a -> Vect (S k) a

-- Eq and Foldable
Eq ty => Eq (Vect n ty) where
    (==) [] [] = True
    (==) (x :: xs) (x' :: xs') = (x == x') && (xs == xs')

-- foldr : Foldable t => (elem -> acc -> acc) -> acc -> t elem -> acc
-- foldl : Foldable t => (acc -> elem -> acc) -> acc -> t elem -> acc

Foldable (Vect n) where
    foldr func acc [] = acc
    foldr func acc (x :: y) = func x (foldr func acc y)
    foldl func acc [] = ?Foldable_rhs_1
    foldl func acc (x :: y) = func (foldl func acc y) x

-- 7.2.4 Exercises

Show ty => Show (Expr ty) where
    show (Val x) = " " ++ show x ++ " "
    show (Add x y) = "(Add " ++ show x ++ show y ++ ")"
    show (Sub x y) = "(Sub " ++ show x ++ show y ++ ")"
    show (Mul x y) = "(Mul " ++ show x ++ show y ++ ")"
    show (Div x y) = "(Div " ++ show x ++ show y ++ ")"
    show (Abs x) = "(Abs " ++ show x ++ ")"

(Neg ty, Integral ty, Eq ty) => Eq (Expr ty) where
    (==) x y = (==) (eval x) (eval y)

Num ty => Num (Expr ty) where
  (+) = Add
  (*) = Mul
  fromInteger = Val . fromInteger

Neg ty => Neg (Expr ty) where
  negate x = 0 - x
  (-) = Sub
  abs = Abs

  -- *chap07> Circle 2 == Circle 2
  -- True : Bool
  -- *chap07> Circle 2 == Circle 3
  -- False : Bool
  -- *chap07> Circle 2 == Rectangle 1 3
  -- False : Bool

-- counts the number of occurrences of a specific value, of some generic type ty, in a list
occurrences : Eq ty => (item : ty) -> (values : List ty) -> Nat
occurrences item [] = 0
occurrences item (x :: xs) = if item == x
                             then 1 + occurrences item xs
                             else occurrences item xs

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

Functor Tree where
  map f Empty = Empty
  map f (Node l e r) = Node (map f l) (f e) (map f r)

-- *chap07> map (*2) (Node (Node Empty 1 Empty) 5 (Node Empty 7 Empty))
-- Node (Node Empty 2 Empty) 10 (Node Empty 14 Empty) : Tree Integer

Foldable Tree where
    foldr func acc Empty = acc
    foldr func acc (Node l e r) = func e (foldr func (foldr func acc l) r)
    foldl func acc Empty = acc
    foldl func acc (Node l e r) = func (foldl func (foldl func acc r) l) e

-- *chap07> foldl (+) 0 (Node (Node Empty 1 Empty) 5 (Node Empty 7 (Node Empty 2 (Node Empty 1 Empty))))
-- 16 : Integer
-- *chap07> foldr (+) 0 (Node (Node Empty 1 Empty) 5 (Node Empty 7 (Node Empty 2 (Node Empty 1 Empty))))
-- 16 : Integer


text:
module InvParComb2

%default total
%hide Prelude.Algebra.(<*>)
%hide Prelude.Applicative.(<|>)

-- http://www.informatik.uni-marburg.de/~rendel/unparse/

-- core definitions

data PartIso a b = MkPartIso (a -> Maybe b) (b -> Maybe a)

class PartIsoFunctor (f : Type -> Type -> Type) where
  (<$>) : PartIso a b -> (f a c -> f b c)

class PFunctor (f : Type -> Type -> Type) where
  (<*>) : f a c -> Lazy (f b c) -> f (a, b) c

class PAlternative (f : Type -> Type -> Type) where
  (<|>) : f a c -> Lazy (f a c) -> f a c
  empty : f a c

class (PartIsoFunctor d, PFunctor d, PAlternative d) => Syntax (d : Type -> Type -> Type) c where
  pure : Eq a => a -> d a c
  item : d c c

-- helper functions

ipc_inverse : PartIso a b -> PartIso b a
ipc_inverse (MkPartIso f g) = MkPartIso g f

ipc_apply : PartIso a b -> a -> Maybe b
ipc_apply (MkPartIso f g) = f

ipc_unapply : PartIso a b -> b -> Maybe a
ipc_unapply = ipc_apply . ipc_inverse

-- Algebra

infixr 1 >=>
(>=>) : Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
f >=> g = \x => f x >>= g

pId : PartIso a a
pId = MkPartIso (\x => Just x) (\x => Just x)

(.) : PartIso b c -> PartIso a b -> PartIso a c
g . f = MkPartIso (ipc_apply f >=> ipc_apply g) (ipc_unapply g >=> ipc_unapply f)

pTup : PartIso a b -> PartIso c d -> PartIso (a, c) (b, d)
pTup i j = MkPartIso f g where
  f (a, b) = case (ipc_apply i a) of
    Nothing => Nothing
    Just x => case (ipc_apply j b) of
      Nothing => Nothing
      Just y => Just (x, y)
  g (c, d) = case (ipc_unapply i c) of
    Nothing => Nothing
    Just x => case (ipc_unapply j d) of
      Nothing => Nothing
      Just y => Just (x, y)

associate : PartIso (a, (b, c)) ((a, b), c)
associate = MkPartIso f g where
  f (a, (b, c)) = Just ((a, b), c)
  g ((a, b), c) = Just (a, (b, c))

commute : PartIso (a, b) (b, a)
commute = MkPartIso f f where
  f : (c, d) -> Maybe (d, c)
  f (a, b) = Just (b, a)

unit : PartIso a (a, ())
unit = MkPartIso f g where
  f a = Just (a, ())
  g (a, ()) = Just a

-- *>, <*

infixl 3 *>
(*>) : Syntax d c => d () c -> d a c -> d a c
p *> q = ipc_inverse unit . commute <$> p <*> q

infixl 3 <*
(<*) : Syntax d c => d a c -> d () c -> d a c
p <* q = ipc_inverse unit <$> p <*> q

ignore : a -> PartIso a ()
ignore x = MkPartIso f g where
  f y = Just ()
  g () = Just x

-- Parser

data Parser a c = MkParser (List c -> Maybe (a, List c))

parse : Parser a c -> List c -> Maybe a
parse (MkParser p) s = p s >>= pure . fst

instance PartIsoFunctor Parser where
  iso <$> (MkParser p) = MkParser pf
  where
    pf l = do
      (x, rest) <- p l
      y <- ipc_apply iso x
      return (y, rest)

instance PFunctor Parser where
  (MkParser p) <*> mkpq = MkParser pf
  where
    pf l = do
      (x, rest) <- p l
      case mkpq of
        (MkParser q) => do
          (y, ret) <- q rest
          return ((x, y), ret)

instance PAlternative Parser where
  (MkParser p) <|> mkpq = MkParser pf
  where
    pf l = case p l of
      Just x => Just x
      Nothing => case mkpq of
        (MkParser q) => q l
  empty = MkParser (\s => Nothing)

instance Syntax Parser c where
  pure x = MkParser (\s => Just (x, s))
  item = MkParser f
  where
    f [] = Nothing
    f (x :: xs) = Just (x, xs)

-- Printer

data Printer a c = MkPrinter (a -> Maybe (List c))

compose : Printer a c -> a -> Maybe (List c)
compose (MkPrinter p) x = p x

instance PartIsoFunctor Printer where
  iso <$> (MkPrinter p) = MkPrinter (\b => ipc_unapply iso b >>= p)

instance PFunctor Printer where
  (MkPrinter p) <*> mkpq = MkPrinter pf
  where
    pf (x, y) = do
      x' <- p x
      case mkpq of
        (MkPrinter q) => do
          y' <- q y
          return (x' ++ y')

instance PAlternative Printer where
  (MkPrinter p) <|> mkpq = MkPrinter $ \s =>
    case (p s) of
      Nothing => case mkpq of
        (MkPrinter q) => q s
      x => x
  empty = MkPrinter (\s => Nothing)

instance Syntax Printer γ where
  pure x = MkPrinter (\y =>
    if x == y
    then Just []
    else Nothing)
  item = MkPrinter (\t => Just [t])

-- Basic parsers/composers

sat : Syntax d a => (a -> Bool) -> d a a
sat p = (MkPartIso check check) <$> item
  where check x = if p x then Just x else Nothing

val : (Syntax d a, Eq a) => a -> d a a
val x = sat (== x)

-- rep

nilv : PartIso () (Vect 0 a)
nilv = MkPartIso (const . Just $ Vect.Nil {a=a})
                 (\xs => case xs of
                   [] => Just ()
                   _ => Nothing)

consv : PartIso (a, Vect n a) (Vect (S n) a)
consv = MkPartIso c1 c2
  where c1 (x, xs) = Just (x :: xs)
        c2 (x :: xs) = Just (x, xs)

rep : Syntax d c => (n : Nat) -> d a c -> d (Vect n a) c
rep Z p = nilv <$> pure ()
rep (S k) p = consv <$> p <*> rep k p

-- many

nil : PartIso () (List a)
nil = MkPartIso c1 c2
  where
    c1 () = Just []
    c2 [] = Just ()
    c2 (x :: xs) = Nothing

cons : PartIso (a, List a) (List a)
cons = MkPartIso c1 c2
  where
    c1 (x, l) = Just $ x :: l
    c2 [] = Nothing
    c2 (x :: xs) = Just (x, xs)

partial many : Syntax d c => d a c -> d (List a) c
many p = (cons <$> (p <*> (many p)))
     <|> (nil <$> pure ())

-- Various types

-- List Bool <-> Nat, with size and endianness

data Endianness = BE | LE

order : Endianness -> Vect n Bool -> Vect n Bool
order BE = reverse
order LE = id

natToBits : Nat -> Endianness -> (k : Nat) -> Vect k Bool
natToBits n e v = order e $ natToBits' n v
  where natToBits' : Nat -> (k : Nat) -> Vect k Bool
        natToBits' n Z = []
        natToBits' Z bits = replicate bits False
        natToBits' n (S bits) = (mod n 2 /= Z) :: natToBits' (div n 2) bits

bitsToNat : Vect n Bool -> Endianness -> Nat
bitsToNat v e = bitsToNat' (order e v)
  where bitsToNat' : Vect k Bool -> Nat
        bitsToNat' [] = Z
        bitsToNat' (v :: l) = (if v then 1 else 0) + 2 * bitsToNat' l

nat : Syntax d Bool => Endianness -> Nat -> d Nat Bool
nat endianness size = MkPartIso pf cf <$> rep size item
  where
    pf l = Just $ bitsToNat l endianness
    cf x = Just $ natToBits x endianness size

-- testing

test : Syntax d Nat => d (Nat, Nat) Nat
test = (val 1) <*> item
   <|> (val 2) <*> (val 3)

test2 : Syntax d Bool => d (Nat, Bool) Bool
test2 = (nat BE 4) <*> (val True)
    <|> (nat BE 2) <*> (val False)

partial test3 : Syntax d Bool => d (Bool, List Nat) Bool
test3 = (val True) <*> ((ignore False <$> item) *> (many $ nat BE 4))
    <|> (val False) <*> ((ignore True <$> item) *> (many $ nat LE 3))

-- compose test3 (False, [1,2,3])
-- parse test3 [False, True, False, False, False, True, False, True, True, False]

-- foldl

partial driver : (a -> Maybe a) -> (a -> a)
driver step state = case step state of
  Just state' => driver step state'
  Nothing => state

partial iterate : PartIso a a -> PartIso a a
iterate step = MkPartIso f g where
  f = Just . driver (ipc_apply step)
  g = Just . driver (ipc_unapply step)

step : PartIso (a, b) a -> PartIso (a, List b) (a, List b)
step i = (pTup i pId) . associate . (pTup pId (ipc_inverse cons))

partial foldl : PartIso (a, b) a -> PartIso (a, List b) a
foldl i = ipc_inverse unit . (pTup pId (ipc_inverse nil)) . iterate (step i)

max_stars_repo_name: defanor/parcomb

max_issues_repo_name: defanor/parcomb

max_forks_repo_name: defanor/parcomb


text:
{--
Copyright 2021 Joel Berkeley

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
--}
module BayesianOptimization.Morphisms

import public Data.Morphisms
import Distribution
import Tensor
import Model

infix 9 >>>

||| Compose two functions that each use two values and wrap them in a morphism. This is a
||| convenience function for contructing unary wrappers with `Empiric`s and the corresponding
||| handler functions for data and models.
export
(>>>) : (i -> (a, b)) -> (a -> b -> o) -> i ~> o
f >>> g = Mor (uncurry g . f)

||| Extract the underlying function from a `Morphism`.
export
run : (i ~> o) -> i -> o
run = applyMor


text:
record Foo where
  constructor MkFoo
  {Gnu : Char}

AFoo : Foo
AFoo = MkFoo {Gnu = 'c'}

Bar : Foo
Bar = { Gnu := '?' } AFoo


text:
module Main

import Data.SortedMap
import FLK_sos
import FLK_ast
import Effects
import Effect.StdIO

done : (s ** CF s) -> { [STDIO] } Eff (s ** CF s)
done (Done ** config) = do
  putStrLn $ "Finished with "++(show config)++" which is a value!"
  pure (Done ** config)
done (a ** config) = do
  putStrLn $ "Finished with "++(show config)++" which is stuck!"
  pure (a ** config)

transStr : (CF a) -> (CF b) -> (Step c d) -> String
transStr x x1 x2 =
  "Transitioning from:\n\t"++(show x)++"\n to \n\t"++(show x1)++"\n by rule ["++(show x2)++"]"

evalPrint : (s ** CF s) -> { [STDIO] } Eff (s' ** CF s')
evalPrint (MkSigma Inter pf) with (search pf)
  evalPrint (MkSigma Inter pf) | Nothing = done $ MkSigma Inter pf
  evalPrint (MkSigma Inter pf) | (Just (MkSigma x (MkSigma y z))) = do
    putStrLn $ transStr pf y z
    evalPrint $ MkSigma x y
evalPrint p@(MkSigma Done pf) = done p
evalPrint (MkSigma Lam pf) with (searchLam pf)
  evalPrint (MkSigma Lam pf) | Nothing = do done $ MkSigma Lam pf
  evalPrint (MkSigma Lam pf) | (Just (x ** (y ** z))) = do
    putStrLn $ transStr pf y z
    evalPrint $ MkSigma x y
evalPrint (MkSigma RecLam pf) = let (x ** (y ** z)) = recTrans pf in do
                                      putStrLn $ transStr pf y z
                                      evalPrint (x ** y)

runEval : Sigma Status (\s => (CF s)) -> IO (Sigma Status (\s' => CF s'))
runEval s = run $ evalPrint s

main : IO ()
main = do { runEval ycomb; pure ()}
  where example : (s ** CF s)
        example = (Inter ** (Prim2 Plus (Prim2 Plus (N 3) (N 4)) (B False)) >- emptyEnv)
        exp2 : Exp Inter
        exp2 = (App (Abs "x" (Prim2 Plus (N 4) (Id "x"))) (N 4))
        example2 : (s ** CF s)
        example2 = (Inter ** (exp2 >- emptyEnv))

max_stars_repo_name: ezrosent/FLK-Semantics

max_issues_repo_name: ezrosent/FLK-Semantics

max_forks_repo_name: ezrosent/FLK-Semantics


text:
module Circuits.NetList.Parser

import Data.Nat
import Data.List1

import Text.Lexer
import Text.Parser

import Toolkit.Data.Location
import Toolkit.Text.Lexer.Run
import Toolkit.Text.Parser.Support
import Toolkit.Text.Parser.Location
import Toolkit.Text.Parser.Run
import Toolkit.Data.Whole

import Ref

import Circuits.NetList.Types
import Circuits.NetList.AST
import Circuits.NetList.Lexer

%default total

namespace NetList
  public export
  Rule : Type -> Type
  Rule = Rule Unit Token

  public export
  RuleEmpty : Type -> Type
  RuleEmpty = RuleEmpty Unit Token

  export
  eoi : RuleEmpty Unit
  eoi = eoi isEOI
    where
      isEOI : Token -> Bool
      isEOI EndInput = True
      isEOI _ = False

namespace API
  export
  symbol : String -> Rule Unit
  symbol str
    = terminal ("Expected Symbol '" ++ str ++ "'")
               (\x => case x of
                             Symbol s => if s == str then Just MkUnit
                                                     else Nothing
                             _ => Nothing)

  export
  nat : Rule Nat
  nat = terminal "Expected nat literal"
               (\x => case x of
                           LitNat i => Just i
                           _ => Nothing)

  export
  keyword : String -> Rule Builtin.Unit
  keyword str
    = terminal ("Expected Keyword '" ++ str ++ "'")
                 (\x => case x of
                             Keyword s => if s == str then Just Builtin.MkUnit
                                                      else Nothing
                             _ => Nothing)

  export
  identifier : Rule String
  identifier
    = terminal "Expected Identifier"
               (\x => case x of
                                  ID str => Just str
                                  _ => Nothing)

  export
  name : Rule String
  name = identifier

  export
  ref : Rule Ref
  ref =
    do s <- Toolkit.location
       n <- name
       e <- Toolkit.location
       pure (MkRef (newFC s e) n)

  export
  gives : String -> a -> Rule a
  gives s ctor
    = do keyword s
         pure ctor

  export
  inserts : Rule a -> (a -> b) -> Rule b
  inserts value ctor
    = do v <- value
         pure (ctor v)

  export
  whole : Rule Whole
  whole =
      do n <- nat
         isWhole n
    where
      isWhole : Nat -> RuleEmpty Whole
      isWhole Z = fail "expected whole"
      isWhole (S n) = pure (W (S n) ItIsSucc)

namespace Direction
  export
  direction : Rule Direction
  direction = gives "inout"  INOUT
          <|> gives "input"  INPUT
          <|> gives "output" OUTPUT

namespace Types

  mutual
    logic : Rule DType
    logic = gives "logic" LOGIC

    array : Rule DType
    array
        = do ty <- logic
             ns <- indices
             pure (arraytype ty ns)
      where
        mustBeZero : Nat -> Whole -> RuleEmpty Whole
        mustBeZero    Z  (W w prf) = pure (W (S w) ItIsSucc)
        mustBeZero (S n)    w      = fail "No ranges or big endian supported"

        index : Rule Whole
        index
          = do symbol "["
               n <- whole
               symbol ":"
               a <- nat
               symbol "]"
               mustBeZero a n

        indices : Rule (List1 Whole)
        indices = some index

        arraytype : DType -> List1 Whole -> DType
        arraytype ty (x:::xs) = foldl (\ty, n => BVECT n ty) ty (x::xs)

    export
    type : Rule DType
    type = array <|> logic

namespace Kinds

  export
  gateUnaryKind : Rule Unary.Kind
  gateUnaryKind
           =  gives "not" NOT

  export
  gateBinaryKind : Rule Binary.Kind
  gateBinaryKind
           =  gives "nand" ANDN
          <|> gives "and"  AND
          <|> gives "xor"  XOR
          <|> gives "xnor" XORN
          <|> gives "or"  IOR
          <|> gives "nor" IORN

namespace Terms

  portDecl : Rule (Location, Ref, Direction, DType)
  portDecl
    = do s <- Toolkit.location
         d <- direction
         t <- type
         r <- ref
         pure (s,r,d,t)

  portList : Rule (List1 (Location,Ref, Direction, DType))
  portList
    = do symbol "("
         ps <- sepBy1 (symbol ",") portDecl
         symbol ")"
         symbol ";"
         pure ps

  shim : Direction -> Rule AST -> Rule AST
  shim d port
    = do s <- Toolkit.location
         p <- port
         e <- Toolkit.location
         pure (Shim (newFC s e) d p)

  port : Direction -> Rule AST
  port d
      = (shim d idx) <|> (shim d ref')
    where

      ref' : Rule AST
      ref' = pure (Var !ref)

      value : Rule (Pair Nat Location)
      value
        = do symbol "["
             n <- nat
             symbol "]"
             e <- Toolkit.location
             pure (n,e)

      indices : Rule (List1 (Nat, Location))
      indices
        = some value

      build : Location
            -> AST
            -> List1 (Nat,Location)
            -> AST
      build s first (x:::xs)
        = foldl (\i, (n,e) => Index (newFC s e) n i) first (x::xs)

      idx : Rule AST
      idx
        = do s <- Toolkit.location
             r <- ref'
             is <- indices
             pure (build s r is)

  data Body = WDecl  FileContext DType Ref
            | GInst  FileContext Binary.Kind Ref AST AST AST
            | NInst  FileContext Unary.Kind Ref AST AST
            | MInst  FileContext Ref AST AST AST AST
            | AInst  FileContext AST AST
            | CInst  FileContext Ref AST AST AST
            | SInst  FileContext Ref AST AST AST

  assign : Rule Body
  assign
    = do s <- Toolkit.location
         keyword "assign"
         o <- port OUTPUT
         symbol "="
         i <- port INPUT
         symbol ";"
         e <- Toolkit.location
         pure (AInst (newFC s e) i o)

  gateNot : Rule Body
  gateNot
    = do s <- Toolkit.location
         k <- gateUnaryKind
         n <- ref
         symbol "("
         o <- port OUTPUT
         symbol ","
         i <- port INPUT
         symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (NInst (newFC s e) k n o i)

  gateBin : Rule Body
  gateBin
    = do s <- Toolkit.location
         k <- gateBinaryKind
         n <- ref
         symbol "("
         o <- port OUTPUT
         symbol ","
         a <- port INPUT
         symbol ","
         b <- port INPUT
         symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (GInst (newFC s e) k n o a b)

  gateMux : Rule Body
  gateMux
    = do s <- Toolkit.location
         keyword "mux"
         n <- ref
         symbol "("
         o <- port OUTPUT
         symbol ","
         c <- port INPUT
         symbol ","
         a <- port INPUT
         symbol ","
         b <- port INPUT
         symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (MInst (newFC s e) n o c a b)

  collect : Rule Body
  collect
    = do s <- Toolkit.location
         keyword "collect"
         n <- ref
         symbol "("
         o <- port OUTPUT
         symbol ","
         a <- port INPUT
         symbol ","
         b <- port INPUT
         symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (CInst (newFC s e) n o a b)

  split : Rule Body
  split
    = do s <- Toolkit.location
         keyword "split"
         n <- ref
         symbol "("
         o <- port OUTPUT
         symbol ","
         a <- port OUTPUT
         symbol ","
         b <- port INPUT
         symbol ")"
         symbol ";"
         e <- Toolkit.location
         pure (SInst (newFC s e) n o a b)

  wireDecl : Rule Body
  wireDecl
      = do s <- Toolkit.location
           keyword "wire"
           t <- type
           a <- ref
           symbol ";"
           e <- Toolkit.location
           pure (WDecl (newFC s e) t a)

  expr : Rule Body
  expr = assign <|> wireDecl <|> gateNot <|> gateBin <|> gateMux

  foldBody : Location
          -> List Body
          -> AST
  foldBody l bs
        = foldr doFold (Stop (newFC l l)) bs
    where
      doFold : Body -> AST -> AST

      doFold (WDecl x y z)
        = Wire x y z

      doFold (MInst v n w x y z)
        = GateDecl v n (Mux v w x y z)

      doFold (GInst x k n y z w)
        = GateDecl x n (GateB x k y z w)

      doFold (NInst x k n y z)
        = GateDecl x n (GateU x k y z)

      doFold (AInst fc i o)
        = Assign fc i o

      doFold (CInst fc n o a b)
        = GateDecl fc n (Collect fc o a b)

      doFold (SInst fc n o a b)
        = GateDecl fc n (Split fc o a b)

  foldPorts : Location
           -> List1 (Location,Ref, Direction, DType)
           -> AST
           -> AST
  foldPorts e (x:::xs) y
    = foldr (\(s,r,d,t), body => Port (newFC s e) d t r body) y (x::xs)

  export
  design : Rule AST
  design
    = do keyword "module"
         n <- ref
         ps <- portList
         b <- many expr
         e <- Toolkit.location
         keyword "endmodule"
         symbol ";"
         pure (foldPorts e ps (foldBody e b))

namespace Idealised

  export
  fromFile : (fname : String)
                   -> IO (Either (ParseError Token) AST)
  fromFile fname
    = case !(parseFile Idealised.Lexer design fname) of
        Left err  => pure (Left err)
        Right ast => pure (Right (setSource fname ast)) -- @TODO add name
-- [ EOF ]

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Libgit.Oid

import Control.Monad.Managed

import Libgit.FFI
import Libgit.Types

withOidFromString : String -> (GitResult GitOid -> IO a) -> IO a
withOidFromString str act = do
  let cresult = git_oid_from_string str
  (err, ptr) <- getGitResultPair cresult
  res <- act (MkGitOid <$> toGitResult err ptr)
  primIO (prim_free ptr)
  pure res

||| Attempt to parse a Git Object ID from a string
|||
||| Returns on success a managed reference to an object ID
||| Returns on failure a Git error code
|||
||| @str a string representation of an object ID
export
oidFromString : (str : String) -> Managed (GitResult GitOid)
oidFromString str = managed (withOidFromString str)

||| Generate a hex-string representation of an object id
export
gitOidToString : GitOid -> String
gitOidToString (MkGitOid oid) = git_oid_to_string oid

max_forks_repo_name: bigs/libgit-idris