text:
module Main

using (Ord a, Num n)

  isort : List a -> List a
  isort [] = []
  isort (x :: xs) = insert x (isort xs)
    where -- insert : a -> List a -> List a
          insert x [] = [x]
          insert x (y :: ys) = if x < y then x :: y :: ys
                                         else y :: insert x ys

  msum : Num n => List n -> n
  msum [] = 0
  msum (x :: xs) = x + msum xs

  mprod : List n -> n
  mprod [] = 1
  mprod (x :: xs) = x * mprod xs

main : IO ()
main = do printLn $ isort [1,5,3,5,1,9,8]
          printLn $ msum [1..10]
          printLn $ mprod [1..10]


text:
module Main

range : Integer -> Integer -> List Integer
range bottom top
    = if bottom > top then []
         else bottom :: range (bottom + 1) top

pythag : Integer -> List (Integer, Integer, Integer)
pythag top
   = [(x, y, z) | z <- range 1 top, y <- range 1 z, x <- range 1 y,
                  x * x + y * y == z * z]

main : IO ()
main = printLn (pythag 200)

ext: idr

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
-- Copyright (c) 2013 Radek Micek

module Main

import Common
import D3

main : IO ()
main = do
  xs <- mkArray ["cat", "dog"]
  ys <- mkArray ["oak", "birch", "maple"]
  arr <- mkArray [xs, ys]

  items <- d3 ?? selectAll "body > ul" >=>
             bind arr  >=>
             selectAll "body > ul > li" >=>
             bind' (\a, i => return a)

  items ?? style "background-color" "orange"
  items ?? enter >=>
    append "li" >=>
    text "New item:" >=>
    style "background-color" "green" >=>
    append "ul" >=>
    append "li"
  items ?? exit >=>
    style "background-color" "red"

  items ?? select "ul" >=>
    select "li" >=>
    text' (\str, i => return $ str ++ "/" ++ show i)

  return ()

max_stars_repo_name: radekm/satviz

max_issues_repo_name: radekm/satviz

max_forks_repo_name: radekm/satviz


text:
module ZZsubs

import congruence
import Quotient_Type
import ZZ_alt
import Product_Type_Eq
import ZZplus

%access public export
%default total

negate : ZZ1 -> ZZ1
negate (a, b) = (b, a)

negatePassesThrough : (a, b : ZZ1) -> (ZZ_Rel a b) -> (ZZ_Rel (negate a) (negate b))
negatePassesThrough (a1, a2) (b1, b2) pfRel = sym pfRel

subs : ZZ1 -> ZZ1 -> ZZ1
subs a b = plus a (negate b)

subsPassesThrough : (a, b, c, d : ZZ1) -> (ZZ_Rel a c) -> (ZZ_Rel b d) ->
                    (ZZ_Rel (subs a b) (subs c d))

subsPassesThrough a b c d pfac pfbd = let

    pf1 : (ZZ_Rel (negate b) (negate d))
        = negatePassesThrough b d pfbd

    pf2 : (ZZ_Rel (plus a (negate b)) (plus c (negate d)))
        = plusPassesThrough a (negate b) c (negate d) pfac pf1

    in
    pf2


text:
module CodeGen.CodeGen

import Core.Name.Namespace
import Core.Context
import Compiler.Common
import Core.CompileExpr
import Compiler.ANF
import Data.List
import Data.String
import Data.Vect
import Data.Either
import Data.SortedSet
import Data.SortedMap
import CairoCode.CairoCode
import CairoCode.CairoCodeUtils
import CairoCode.Traversal.Base
import CommonDef
import CodeGen.CodeGenHelper
import CodeGen.CurryingBasedClosures

import Primitives.Externals
import Primitives.Primitives
import Primitives.Common

%hide Prelude.toList

-- This is all for now maybe we need morw later
record CodeGenInfo where
    constructor MkCodeGenInfo
    -- to get the order right for foreign calls
    implicits: List LinearImplicit

extractCodeGenInfoFromDef : CairoDef ->  CodeGenInfo
extractCodeGenInfoFromDef (FunDef _ impls _ _) = MkCodeGenInfo $ keys impls
extractCodeGenInfoFromDef (ForeignDef (MkForeignInfo _ _ impls _ _) _ _) = MkCodeGenInfo impls

collectCodeGenInfo : List (Name, CairoDef) -> SortedMap Name CodeGenInfo
collectCodeGenInfo defs = fromList $ map (\(n,def) => (n, extractCodeGenInfoFromDef def)) defs

-- Helper for compiling calls
compileCall : Name -> CodeGenInfo -> List CairoReg -> LinearImplicitArgs -> List CairoReg -> String
compileCall n info rs linImpls args = """
     let (\{ regList }) = \{ cairoName n } (\{ paramList })
     \{ assigList }
     """
     where join : List String -> String
           join Nil = ""
           join (x::xs) = foldl1 (\s1,s2 => s1 ++ ", "++s2 ) (x::xs)
           manifestReg : CairoReg -> String
           manifestReg r = if isLocal r then (regName r) ++ "_tmp" else regName r
           implList : List (CairoReg, CairoReg)
           implList = map (\i => fromMaybe (assert_total $ idris_crash "missing implicit") (lookup i linImpls)) (implicits info)
           joinedRs : List CairoReg
           joinedRs = rs ++ (map snd implList)
           regList : String
           regList = join (map manifestReg joinedRs)
           paramList : String
           paramList = showSep ", " (map compileReg ((map fst implList) ++ args))
           implRes : List CairoReg
           implRes = map fst implList
           assigList : String
           assigList = concatMap (\r => (compileRegDecl r) ++ " = " ++ (compileReg r) ++"_tmp\n") (filter isLocal joinedRs)

compileConstructor : List String -> Int -> CairoReg -> String
compileConstructor values start reg = """
 #MKCON
 let (\{ compileReg reg }_ptr) = alloc()
 \{ compileRegDecl reg } = cast(\{ compileReg reg }_ptr,felt)
 \{ fst res }
 """
  where
    res : (String, Int)
    res = foldl (\(acc, cnt), comp => (acc ++ "assert [" ++ (compileReg reg) ++ " + " ++ show cnt ++ "] = " ++ comp ++ "\n", cnt+1)) ("", start) values

{-
-- More efficient but not starknet compatible (because it uses hints)
compileConstructor : List String -> Int -> String -> String -> String -> String
compileConstructor values start defineReg regName postfix = """
 #MKCON
 \{ defineReg }
 %{ ids.\{regName} = segments.add() %}
 \{ fst res }
 \{ postfix }

 """
 where res : (String, Int)
       res = foldl (\(acc, cnt), comp => (acc ++ "assert [" ++ regName ++ " + " ++ show cnt ++ "] = " ++ comp ++ "\n", cnt+1)) ("", start) values
-}

mutual
     compileGeneralCase: SortedMap Name CodeGenInfo -> String -> String -> List CairoInst -> String -> String
     compileGeneralCase cInf value tagOrConst vminsts elseCase = """
        if \{ value } == \{ tagOrConst }:
            \{ concatMap (compileCairoInst cInf) vminsts }
        else:
            \{ elseCase }
        end

        """

     compileCase : SortedMap Name CodeGenInfo -> CairoReg -> (Int, List CairoInst) -> String -> String
     compileCase cInf reg (tag, vminsts) elseCase = compileGeneralCase cInf ("[" ++ compileReg reg ++ "]") (show tag) vminsts elseCase
     compileCases : SortedMap Name CodeGenInfo -> CairoReg -> List (Int, List CairoInst) -> Maybe (List CairoInst) -> String
     compileCases _ scr Nil Nothing = ""
     compileCases cInf scr Nil (Just def) = concatMap (compileCairoInst cInf) def
     compileCases cInf scr ((_,cs)::Nil) Nothing = concatMap (compileCairoInst cInf) cs
     compileCases cInf scr alts (Just def) = foldr (\c, acc => compileCase cInf scr c acc) (concatMap (compileCairoInst cInf) def) alts
     compileCases cInf scr ((_,cs)::alts) Nothing = foldr (\c, acc => compileCase cInf scr c acc) (concatMap (compileCairoInst cInf) cs) alts

     compileConstCase : SortedMap Name CodeGenInfo ->  CairoReg -> (CairoConst, List CairoInst) -> String -> String
     compileConstCase  cInf reg (constant, vminsts) elseCase = compileGeneralCase cInf (compileReg reg) (compileConst constant) vminsts elseCase
     compileConstCases : SortedMap Name CodeGenInfo ->  CairoReg -> List (CairoConst, List CairoInst) -> Maybe (List CairoInst) -> String
     compileConstCases _ reg Nil Nothing = ""
     compileConstCases cInf reg Nil (Just def) = concatMap (compileCairoInst cInf) def
     compileConstCases cInf reg ((_,cs)::Nil) Nothing = concatMap (compileCairoInst cInf) cs
     compileConstCases cInf reg alts (Just def) = foldr (\c, acc => compileConstCase cInf reg c acc) (concatMap (compileCairoInst cInf) def) alts
     compileConstCases cInf reg ((_,cs)::alts) Nothing = foldr (\c, acc => compileConstCase cInf reg c acc) (concatMap (compileCairoInst cInf) cs) alts

     compileCairoInst : SortedMap Name CodeGenInfo -> CairoInst -> String
     compileCairoInst _ (ASSIGN r v) = "\{ compileRegDecl r } = \{ compileReg v }\n"
     -- Todo: Add Unpacked Versions (They are basically just multi assignes)
     compileCairoInst _ (MKCON r (Just t) args) = compileConstructor (show t :: map compileReg args) 0 r
     compileCairoInst _ (MKCON r Nothing args) = compileConstructor (map compileReg args) 1 r
     compileCairoInst _ (MKCLOSURE r n m args) = genMkClosure r n m args

     -- Todo: This does not work with closures pointing to %foreign as the impl param order may be wrong
     --       However, Closure system needs overhaul or defunct anyway
     --       If we leave as is, we need to make wrappers for foreign closures that reorder implicit args if necessary
     compileCairoInst _ (APPLY r linImpls f a) = genMkApply r linImpls f a
     compileCairoInst _ (MKCONSTANT r c) =
        if (isLocal r) then "\{ compileRegDecl r } = \{ compileConst c }\n"
        else if (isConst r) then  ""
        else compileConstRegDecl r ++ " = \{ compileConst c }\n"

     compileCairoInst cInf (CALL rs linImpls n args) = compileCall n (fromMaybe (assert_total $ idris_crash "missing function") (lookup n cInf) ) rs linImpls args
     -- compile primFns
     compileCairoInst cinf (OP r linImpls op args) =
       case generatePrimFnCode op r args linImpls of
         Instructions insts =>  concatMap (compileCairoInst cinf) insts
         Raw code => code
     compileCairoInst _ (EXTPRIM rs linImpls n args) = externalCodeGen n rs linImpls args
     compileCairoInst cInf (CASE scr alts def) = compileCases cInf scr alts def
     compileCairoInst cInf (CONSTCASE scr alts def) = compileConstCases cInf scr alts def
     compileCairoInst _ (RETURN rs linImpls) = "return (" ++ join (map compileReg (rs ++ (values linImpls))) ++ ")\n"
        where join : List String -> String
              join Nil = ""
              join (x::xs) = foldl1 (\s1,s2 => s1 ++ ", "++s2 ) (x::xs)

     -- Project pos + 1 since pos + 0 is the tag
     compileCairoInst _ (PROJECT r val pos) = "\{ compileRegDecl r } = [\{ compileReg val } + \{ show (pos + 1) }]\n"
     compileCairoInst _ (NULL r ) = compileRegDecl r ++ " = 0\n"
     compileCairoInst _ (ERROR r str) = impossibleCase r (show str)

compileCairoDef : SortedMap Name CodeGenInfo -> Name -> CairoDef -> String
compileCairoDef cInf name def@(FunDef args linImplicits rets body) = """
     func \{ cairoName name }(\{ showSep ", " (map regName ((values linImplicits) ++ args)) }) -> (\{ showSep ", " (rets ++ (map implicitName (keys linImplicits))) }):
       \{if isNil collectedLocals then "" else ("alloc_locals\n" ++ compiledLocals)}
       \{concatMap (compileCairoInst cInf) body}
     end

     """
     where collectedLocals : List CairoReg
           collectedLocals = toList $ collectLocals (name, def)
           compiledLocals : String
           compiledLocals = concatMap (\reg => "local " ++ (compileReg reg) ++ "\n") collectedLocals

compileCairoDef _ name (ForeignDef info _ _) = code info

extractKnownBuiltin : LinearImplicit -> List String
extractKnownBuiltin (MKLinearImplicit "bitwise_ptr") = ["bitwise"]
extractKnownBuiltin (MKLinearImplicit "pedersen_ptr") = ["pedersen"]
extractKnownBuiltin (MKLinearImplicit "output_ptr") = ["output"]
extractKnownBuiltin (MKLinearImplicit "range_check_ptr") = ["range_check"]
extractKnownBuiltin (MKLinearImplicit "ecdsa_ptr") = ["ecdsa"]
extractKnownBuiltin _ = []

-- TODO Group by namespace, deduplicate functions names and generate mutli-imports
compileImports : SortedSet Import -> String
compileImports imports =
  showSep "\n" (map (\(MkImport ns f) => "from " ++ ns ++ " import " ++ f ) (toList imports))

builtinsPragma : List LinearImplicit -> String
builtinsPragma builtins = "%builtins " ++ showSep " " (builtins >>= extractKnownBuiltin)

addHeader : Bool -> List LinearImplicit -> SortedSet Import -> String -> String
addHeader isLib builtins imports defs =
"""
\{ if not isLib then builtinsPragma builtins else "" }
\{ compileImports imports }
# HACK: The dw 0 is here because the programStart: label used in the closure generators would not work if there are no imports
dw 0
programStart:
\{ defs }

"""

extractMainImplicits : Name -> List (Name, CairoDef) -> List LinearImplicit
extractMainImplicits _ Nil = assert_total $ idris_crash "no cairo_main found"
extractMainImplicits mainName ((name, (FunDef _ impls _ _))::xs) =
    if mainName == name
        then keys impls
        else extractMainImplicits mainName xs
extractMainImplicits mainName (def::xs) = extractMainImplicits mainName xs

collectImports : List (Name, CairoDef) -> SortedSet Import
collectImports cairocode = snd $ runVisitConcatCairoDefs (pureTraversal importTraversal) cairocode
    where importTraversal : InstVisit CairoReg -> SortedSet Import
          importTraversal (VisitMkCon _ _ _) = singleton (MkImport "starkware.cairo.common.alloc" "alloc")
          importTraversal (VisitMkClosure _ _ _ _) = singleton (MkImport "starkware.cairo.common.alloc" "alloc")
          importTraversal (VisitForeignFunction _ fi _ _) = fi.imports
          importTraversal (VisitExtprim _ _ name _) = externalImports name
          importTraversal (VisitOp _ _ fn _) = primFnImports fn
          importTraversal _ = empty

export
generateCairoCode : Bool -> Name -> List (Name, CairoDef) -> String
generateCairoCode isLib mainName cairocode = addHeader isLib mainImplicits imports compiledDefs
    where mainImplicits : List LinearImplicit
          mainImplicits = extractMainImplicits mainName cairocode
          cInf : SortedMap Name CodeGenInfo
          cInf = collectCodeGenInfo cairocode
          imports : SortedSet Import
          imports = collectImports cairocode
          compiledDefs : String
          compiledDefs = concatMap (\(name, cairodef) => compileCairoDef cInf name cairodef ++ "\n\n") cairocode

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro


text:
import Data.Primitives.Views
import Data.Bits
import Data.String
import System

%default total

record Score where
       constructor MkScore
       correct : Nat
       attempted : Nat

record GameState where
       constructor MkGameState
       score : Score
       difficulty : Int

Show GameState where
    show st = show (correct (score st)) ++ "/" ++
              show (attempted (score st)) ++ "\n" ++
              "Difficulty: " ++ show (difficulty st)

initState : GameState
initState = MkGameState (MkScore 0 0) 12

addWrong : GameState -> GameState
addWrong = record { score.attempted $= (+1) }

addCorrect : GameState -> GameState
addCorrect = record { score.correct $= (+1),
                      score.attempted $= (+1) }

setDifficulty : Int -> GameState -> GameState
setDifficulty newDiff state = record { difficulty = newDiff } state

export
data Command : Type -> Type where
     PutStr : String -> Command ()
     GetLine : Command String

     GetRandom : Command Int
     GetGameState : Command GameState
     PutGameState : GameState -> Command ()

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

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

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

  export
  (>>) : Command () -> Inf (ConsoleIO a) -> ConsoleIO a
  (>>) = Seq

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

  export
  (>>) : Command () -> Command b -> Command b
  ma >> mb  = ma >>= \ () => mb

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

runCommand : Stream Int -> GameState -> Command a ->
             IO (a, Stream Int, GameState)
runCommand rnds state (PutStr x) = do putStr x
                                      pure ((), rnds, state)
runCommand rnds state GetLine = do str <- getLine
                                   pure (str, rnds, state)
runCommand (val :: rnds) state GetRandom
      = pure (getRandom val (difficulty state), rnds, state)
  where
    getRandom : Int -> Int -> Int
    getRandom val max with (divides val max)
      getRandom val 0 | DivByZero = 1
      getRandom ((max * div) + rem) max | (DivBy div rem prf) = abs rem + 1
runCommand rnds state GetGameState
      = pure (state, rnds, state)
runCommand rnds state (PutGameState newState)
      = pure ((), rnds, newState)

runCommand rnds state (Pure val)
      = pure (val, rnds, state)
runCommand rnds state (Bind c f)
      = do (res, newRnds, newState) <- runCommand rnds state c
           runCommand newRnds newState (f res)

data Fuel = Dry | More (Lazy Fuel)

partial
forever : Fuel
forever = More forever

run : Fuel -> Stream Int -> GameState -> ConsoleIO a ->
      IO (Maybe a, Stream Int, GameState)
run fuel rnds state (Quit val) = do pure (Just val, rnds, state)
run (More fuel) rnds state (Do c f)
     = do (res, newRnds, newState) <- runCommand rnds state c
          run fuel newRnds newState (f res)
run (More fuel) rnds state (Seq c f)
     = do ((), newRnds, newState) <- runCommand rnds state c
          run fuel newRnds newState f
run Dry rnds state p = pure (Nothing, rnds, state)

mutual
  correct : ConsoleIO GameState
  correct = do PutStr "Correct!\n"
               st <- GetGameState
               PutGameState (addCorrect st)
               quiz

  wrong : Int -> ConsoleIO GameState
  wrong ans
        = do PutStr ("Wrong, the answer is " ++ show ans ++ "\n")
             st <- GetGameState
             PutGameState (addWrong st)
             quiz

  data Input = Answer Int
             | QuitCmd

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

  quiz : ConsoleIO GameState
  quiz = do num1 <- GetRandom
            num2 <- GetRandom
            st <- GetGameState
            PutStr (show st ++ "\n")

            input <- readInput (show num1 ++ " * " ++ show num2 ++ "? ")
            case input of
               Answer answer => if answer == num1 * num2
                                   then correct
                                   else wrong (num1 * num2)
               QuitCmd => Quit st

partial
main : IO ()
main = do seed <- time
          (Just score, _, state) <-
              run forever (randoms (fromInteger seed)) initState quiz
                  | _ => putStrLn "Ran out of fuel"
          putStrLn ("Final score: " ++ show state)


text:
module Tasks

-- Based on https://www.microsoft.com/en-us/research/uploads/prod/2018/03/build-systems-final.pdf

data Task : (c : (Type -> Type) -> Type) -> Type -> Type -> Type where
  MkTask : ({f : Type -> Type} -> c f -> (k -> f v) -> f v) -> Task c k v

Tasks : ((Type -> Type) -> Type) -> Type -> Type -> Type
Tasks c k v = k -> Maybe (Task c k v)

data Const m a = MkConst m

Functor (Const m) where
  map _ (MkConst m) = MkConst m

[const] Monoid m => Applicative (Const m) where
  pure _ = MkConst neutral
  (MkConst x) <*> (MkConst y) = MkConst (x <+> y)

sprsh1 : Tasks Applicative String Integer
sprsh1 "B1" = Just $ MkTask $ \constr, fetch => B1 @{constr} fetch
  where
    B1 : Applicative f => (String -> f Integer) -> f Integer
    B1 fetch = (+) <$> fetch "A1" <*> fetch "A2"
sprsh1 "B2" = Just $ MkTask $ \constr, fetch => B2 @{constr} fetch
  where
    B2 : Applicative f => (String -> f Integer) -> f Integer
    B2 fetch = (* 2) <$> fetch "B1"
sprsh1 _ = Nothing

dependencies : Task Applicative k v -> List k
dependencies (MkTask task) = let (MkConst xs) = task const (\k => MkConst [k]) in xs

test1 : Maybe (List String)
test1 = sprsh1 "B1" >>= \task => Just $ dependencies task

test2 : Maybe (List String)
test2 = sprsh1 "B2" >>= \task => Just $ dependencies task

max_stars_repo_name: STELIORD/idris-snippets

max_issues_repo_name: stjordanis/idris-snippets

max_forks_repo_name: stjordanis/idris-snippets


text:
||| Algebra.Semigroup: A representation of semigroups.
|||
||| A semigroup is an associative magma. In other words, it is a pair
||| \\(\mathscr{S}=(S:\mathscr{V},\*:S^2\to S)\\) satisfying the following
||| (rather short!) list of axioms:
|||
||| * \\((x\*y)\*z = x\*(y\*z)\\)
|||
||| In addition to interesting combinatorial questions (like those exhibited by
||| magmas; see `Algebra.Magma`), semigroups, with their richer structure, yield
||| more interesting behavior.
|||
||| TODO: expand
module Algebra.Semigroup

import Data.ZZ
import Algebra.Magma

%default total
%hide Semigroup

-- infixr 7 |*|

||| Semigroup: The record representing semigroups.
|||
||| The requirement that a semigroup be a magma is just a declaration of the
||| signature of semigroups; namely, one set and one binary operation over it.
||| There is one law that must be obeyed: associativity. Note that you cannot
||| even construct a semigroup until you have proven that the magma is indeed
||| associative. Thus, the associativity is guaranteed by the typechecker; if a
||| function utilizing a type that claims to be a semigroup, you know that it
||| indeed must be one. mathematically speaking, iff it typechecks. (Of course,
||| as usual, this only holds when all of one's proofs are total.)
export
record Semigroup where
  constructor MkSemigroup'
  magma : Magma
  { assoc : {s,t,u : Set {magma}} -> s |*| (t |*| u) = (s |*| t) |*| u }

export
MkSemigroup : (T : Type) -> (op : T -> T -> T) -> {auto assoc : {s,t,u : T} -> s `op` (t `op` u) = (s `op` t) `op` u} -> Semigroup
MkSemigroup t op {assoc} = MkSemigroup' (MkMagma t op) {assoc=assoc}
{-
public export
MkSemigroup : (T : Type) -> (op : T -> T -> T) -> {auto asc : {s,t,u : T} -> op s (op t u) = op (op s t) u} -> Semigroup
MkSemigroup set op {asc} = MkSemigroup' (MkMagma set op) asc
-}

-- toInteger : ZZ -> Integer
-- toInteger (Pos  n) = toIntegerNat n
-- toInteger (NegS n) = -(toIntegerNat (S n))

%hint
plusAssociative' : {a,b,c : Nat} -> a + (b + c) = (a + b) + c
plusAssociative' {a} {b} {c} = plusAssociative a b c

%hint
multAssociative' : {a,b,c : Nat} -> a * (b * c) = (a * b) * c
multAssociative' {a} {b} {c} = multAssociative a b c

%hint
plusAssociativeZ' : {a,b,c : ZZ} -> a + (b + c) = (a + b) + c
plusAssociativeZ' {a} {b} {c} = plusAssociativeZ a b c

%hint
multAssociativeZ' : {a,b,c : ZZ} -> a * (b * c) = (a * b) * c
multAssociativeZ' {a} {b} {c} = multAssociativeZ a b c

NatAddSemi : Semigroup
NatAddSemi = MkSemigroup Nat (+)
{-
export
NatAddMagma : Magma
NatAddMagma = MkMagma Nat (+)

-- export
-- NatAddSemi : Semigroup
-- NatAddSemi = MkSemigroup NatAddMagma

export NatMultSemi : Semigroup
NatMultSemi = MkSemigroup Nat (*)     -- what the hell

-- SemigroupToMagma : Semigroup -> Magma
-- SemigroupToMagma (

-- export IntAddSemi : Semigroup
-- IntAddSemi = MkSemigroup ZZ (+)

-- export IntMultSemi : Semigroup
-- IntMultSemi = MkSemigroup ZZ (*)
-- -}

max_stars_repo_name: greatBigDot/algebra

max_issues_repo_name: greatBigDot/algebra

max_forks_repo_name: greatBigDot/algebra


text:
||| An approach to intrinsically-typed STLC with Type Synonyms and New types.
|||
||| We treat type 'aliases' and 'newtypes' as term level constructs,
||| which ensures named types can be differentiated by name i.e. De
||| Bruijn indices.  Type universes are used to separate descriptions
||| of how types are formed and their use to type values.
|||
||| Standard constructions are used to represent the language as an
||| EDSL, together with proof of progress taken from PLFA Part 2.
|||
||| This module compliments Section 5 of the Functional Pearl.
|||
||| Although the code appears to be total, there is a known issues
||| with Idris2 totality checker that causes it to slow down when
||| dealing with mutually defined terms.
|||
module Razor.LetFoo

import Razor.Common

%default covering

namespace Types

  ||| Levels at which types and their types are defined in our type
  ||| universes.
  public export
  data Level = TYPE -- Build types here
             | VALUE -- Use types here.

  ||| Our types are meta types...
  public export
  data MTy : Level -> Type where

    -- Explicit Type formers
    IntTyDesc : MTy TYPE
    IntTy : MTy VALUE

    CharTyDesc : MTy TYPE
    CharTy : MTy VALUE

    -- Implicit constructions.
    NewtypeTy : MTy level -> MTy level

  ||| A predicate to type check types against type formers.
  public export
  data TyCheck : (type : MTy TYPE)
              -> (value : MTy VALUE)
              -> Type
    where
      ChkInt  : TyCheck IntTyDesc IntTy
      ChkChar : TyCheck CharTyDesc CharTy

      ChkNewtype : TyCheck innerType innerValue
                -> TyCheck (NewtypeTy innerType)
                           (NewtypeTy innerValue)

  ||| A context is a list of types in different universes.
  public export
  Context : List Level -> Type
  Context = DList Level MTy

  public export
  Elem : Context lvls -> MTy level -> Type
  Elem g ty = Elem Level MTy ty g

namespace Terms

    public export
    data SystemFoo : Context lvls -> MTy level -> Type where
      -- STLC

      Var : Elem Level MTy type ctxt -> SystemFoo ctxt type

      -- Type Constructors
      TyInt  : SystemFoo ctxt IntTyDesc
      TyChar : SystemFoo ctxt CharTyDesc

      -- Type Ascriptions
      The : {  mtypeType  : MTy TYPE}
         -> {  mtypeValue : MTy VALUE}
         -> (  type  : SystemFoo ctxt mtypeType)
         -> (  value : SystemFoo ctxt mtypeValue)
         -> (0 prf   : TyCheck mtypeType mtypeValue)
                    -> SystemFoo ctxt mtypeValue

      -- Base Values

      I : Int -> SystemFoo ctxt IntTy
      C : Char -> SystemFoo ctxt CharTy

      -- NewType Type & Value Constructors, and Matching.
      TyCTor : {type : MTy TYPE}
            -> (desc : SystemFoo ctxt type)
                    -> SystemFoo ctxt (NewtypeTy type)

      CTor : {typeM : MTy TYPE}
          -> {typeV : MTy VALUE}
          -> (  type  : SystemFoo ctxt (NewtypeTy typeM))
          -> (  value : SystemFoo ctxt typeV)
          -> (0 prf   : TyCheck typeM typeV)
          -> SystemFoo ctxt (NewtypeTy typeV)

      Match : {type  : MTy VALUE}
           -> {bodyTy : MTy VALUE}
           -> (value : SystemFoo ctxt           (NewtypeTy type))
           -> (body  : SystemFoo (ctxt += type) bodyTy)
                    -> SystemFoo ctxt           bodyTy

      -- Binders
      Let : {  exprTy, bodyType : MTy VALUE}
         -> (  value : SystemFoo ctxt exprTy)
         -> (  body  : SystemFoo (ctxt += exprTy) bodyType)
                    -> SystemFoo  ctxt            bodyType

      NewType : {lvl : Level}
             -> {type : MTy TYPE}
             -> {bodyType : MTy lvl}
             -> (desc : SystemFoo ctxt     (NewtypeTy type))
             -> (body : SystemFoo (ctxt += (NewtypeTy type)) bodyType)
                     -> SystemFoo ctxt                       bodyType

      TypeAlias : {lvl : Level}
               -> {type : MTy TYPE}
               -> {bodyTy : MTy lvl}
               -> (desc : SystemFoo  ctxt    type)
               -> (body : SystemFoo (ctxt += type) bodyTy)
                       -> SystemFoo  ctxt          bodyTy

namespace Renaming

  public export
  weaken : (func : Types.Elem old type
                -> Types.Elem new type)
        -> (Elem (old += type') type
         -> Types.Elem (new += type') type)

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

  public export
  rename : (f : {level : Level}
             -> {type  : MTy level}
                      -> Types.Elem old type
                      -> Types.Elem new type)
        -> ({level : Level}
         -> {type : MTy level}
         -> SystemFoo old type
         -> SystemFoo new type)

  -- STLC
  rename f (Var idx) = Var (f idx)

  -- Type Constructors
  rename f TyInt               = TyInt
  rename f TyChar              = TyChar

  -- Type Ascriptions
  rename f (The type value prf) = The (rename f type)
                                      (rename f value)
                                      prf
  -- Base Values
  rename f (I i) = (I i)
  rename f (C c)  = (C c)

  -- NewType Type & Value Constructors, and Matching.
  rename f (TyCTor desc) = TyCTor (rename f desc)

  rename f (CTor type value prf)
      = CTor (rename f type)
             (rename f value)
             prf

  rename f (Match scrutinee body)
      = Match (rename f scrutinee)
              (rename (weaken f) body)

  -- Binders
  rename f (Let expr body)
      = Let (rename f expr)
            (rename (weaken f) body)

  rename f (NewType type body)
      = NewType (rename f type)
                (rename (weaken f) body)

  rename f (TypeAlias type body)
      = TypeAlias (rename f type)
                  (rename (weaken f) body)

namespace Substitution
  public export
  weakens : (f : {level : Level}
              -> {type  : MTy level}
                       -> Types.Elem old type
                       -> SystemFoo new type)
         -> ({level : Level}
          -> {type  : MTy level}
                   -> Types.Elem (old += type') type
                   -> SystemFoo (new += type') type)
  weakens f Here = Var Here
  weakens f (There rest) = rename There (f rest)

  -- general substitute
  namespace General
    public export
    subst : (f : {level : Level}
              -> {type  : MTy level}
                       -> Types.Elem old type
                       -> SystemFoo new type)
         -> ({level : Level}
          -> {type  : MTy level}
                   -> SystemFoo old type
                   -> SystemFoo new type)

    -- STLC
    subst f (Var idx) = f idx

    -- Types
    subst f TyInt  = TyInt
    subst f TyChar = TyChar

    -- Type Ascriptions
    subst f (The type value prf)
        = The (subst f type)
              (subst f value)
              prf

    -- Base Values
    subst f (I i) = (I i)
    subst f (C c) = (C c)

    -- NewType Type & Value Constructors, and Matching.
    subst f (Match scrutinee body)
        = Match (subst f scrutinee) (subst (weakens f) body)

    subst f (CTor type value prf)
        = CTor (subst f type) (subst f value) prf

    subst f (TyCTor desc) = TyCTor (subst f desc)

    -- Bindings
    subst f (Let expr body)
        = Let (subst f expr)
              (subst (weakens f) body)

    subst f (NewType desc body)
        = NewType (subst f desc) (subst (weakens f) body)

    subst f (TypeAlias type body)
        = TypeAlias (subst f type) (subst (weakens f) body)

  namespace Single
    public export
    apply : {levelA : Level}
         -> {typeA  : MTy levelA}
         -> (this   : SystemFoo ctxt typeB)
         -> (idx    : Elem (ctxt += typeB) typeA)
                   -> SystemFoo ctxt typeA
    apply this Here = this
    apply this (There rest) = Var rest

    public export
    subst : {levelA,levelB : Level}
         -> {typeA         : MTy levelA}
         -> {typeB         : MTy levelB}
         -> (this          : SystemFoo  ctxt           typeB)
         -> (inThis        : SystemFoo (ctxt += typeB) typeA)
                          -> SystemFoo  ctxt           typeA
    subst {ctxt} {typeA} {typeB} {levelA} {levelB} this inThis
      = General.subst (apply this) inThis

namespace Values

  public export
  data Value : SystemFoo ctxt type -> Type where
    TyCharV : Value TyChar
    TyIntV : Value TyInt

    TyCTorV : Value desc -> Value (TyCTor desc)
    CTorV   : Value value -> Value (CTor type value prf)

    IntV  : Value (I i)
    CharV : Value (C c)

namespace Reduction

  public export
  data Redux : (this : SystemFoo ctxt type)
            -> (that : SystemFoo ctxt type)
            -> Type
    where

      -- Ascriptions
      SimplifyTheType : (type : Redux this that)
                             -> Redux (The this value prf)
                                      (The that value prf)

      SimplifyTheValue : {this, that : SystemFoo ctxt vtype}
                      -> {type       : SystemFoo ctxt ttype}
                      -> (prf : Value type)
                      -> (value : Redux this that)
                      -> Redux (The type this prf')
                               (The type that prf')

      ReduceThe : {type  : SystemFoo ctxt ttype}
               -> {value : SystemFoo ctxt vtype}
               -> (typeVal  : Value type)
               -> (valueVal : Value value)
                           -> Redux (The type value prf)
                                    value

      -- Matching newtypes
      SimplifyTyCTor : (desc : Redux this that)
                            -> Redux (TyCTor this) (TyCTor that)

      SimplifyCTorType : {this, that : SystemFoo ctxt (NewtypeTy typeM)}
                      -> {value      : SystemFoo ctxt type}
                      -> (theType    : Redux this that)
                                    -> Redux (CTor this value prf)
                                             (CTor that value prf)

      SimplifyCTorValue : {this, that : SystemFoo ctxt typeV}
                       -> {theType : SystemFoo ctxt (NewtypeTy typeD)}
                       -> (typeV   : Value theType)
                       -> (value   : Redux this that)
                                  -> Redux (CTor theType this prf)
                                           (CTor theType that prf)

      SimplifyMatchScrut : {this, that : SystemFoo ctxt (NewtypeTy stype)}
                        -> {body : SystemFoo (ctxt += stype) btype}
                        -> (scutinee : Redux this that)
                                    -> Redux (Match this body)
                                             (Match that body)

      ReduceMatchBody : {type : SystemFoo ctxt (NewtypeTy ttype)}
                     -> {value : SystemFoo ctxt vtype}
                     -> {body : SystemFoo (ctxt += vtype) btype}
                     -> (valueVal : Value value)
                                 -> Redux (Match (CTor type value prf) body)
                                          (subst value body)

      -- Let binding
      SimplifyLetValue : {this, that : SystemFoo ctxt typeV}
                      -> {body : SystemFoo (ctxt += typeV) typeB}
                      -> (value   : Redux this that)
                                 -> Redux (Let this body)
                                          (Let that body)

      ReduceLetBody : {value : SystemFoo ctxt typeV}
                   -> {body  : SystemFoo (ctxt += typeV) typeB}
                   -> (valueVal : Value value)
                               -> Redux (Let value body)
                                        (subst value body)

      -- Newtypes

      SimplifyNewType : {this, that : SystemFoo ctxt (NewtypeTy typeV)}
                     -> {body : SystemFoo (ctxt += (NewtypeTy typeV)) typeB}
                     -> (desc : Redux this that)
                             -> Redux (NewType this body)
                                      (NewType that body)

      ReduceNewType : {typeD : MTy TYPE}
                   -> {desc : SystemFoo ctxt (NewtypeTy typeD)}
                   -> {body : SystemFoo (ctxt += (NewtypeTy typeD))    typeB}
                   -> (value : Value desc)
                            -> Redux (NewType desc body)
                                     (subst   desc body)

      SimplifyTypeAlias : {this, that : SystemFoo ctxt typeV}
                       -> {body       : SystemFoo (ctxt += typeV)    typeB}
                       -> (desc : Redux this that)
                               -> Redux (TypeAlias this body) (TypeAlias that body)

      ReduceTypeAlias : {desc : SystemFoo ctxt typeD}
                     -> {body : SystemFoo (ctxt += typeD)    typeB}
                     -> (descVal : Value desc)
                              -> Redux (TypeAlias desc body)
                                       (subst desc body)

namespace Progress
  public export
  data Progress : (term : SystemFoo Nil type)
                       -> Type
    where
      Done : forall mty . {term : SystemFoo Nil mty}
                        -> Value term
                        -> Progress term
      Step : {this, that : SystemFoo Nil type}
          -> (prf        : Redux this that)
                        -> Progress this

  public export
  progress : (term : SystemFoo Nil type)
          -> Progress term
  progress {type} (Var _) impossible

  -- Type Constructors
  progress TyInt  = Done TyIntV
  progress TyChar = Done TyCharV

  progress (The type value prf) with (progress type)
    progress (The type value prf) | (Done valueT) with (progress value)
      progress (The type value prf) | (Done valueT) | (Done valueV)
        = Step (ReduceThe valueT valueV)
      progress (The type value prf) | (Done valueT) | (Step prfV)
        = Step (SimplifyTheValue valueT prfV)
    progress (The type value prf) | (Step prfT)
        = Step (SimplifyTheType prfT)

  -- Base Values
  progress (I i) = Done IntV
  progress (C c) = Done CharV

  -- NewType Type & Value Constructors, and Matching.
  progress (TyCTor type) with (progress type)
    progress (TyCTor type) | (Done valueT) = Done (TyCTorV valueT)
    progress (TyCTor type) | (Step prfT) = Step (SimplifyTyCTor prfT)

  progress (CTor type value prf) with (progress type)
    progress (CTor type value prf) | (Done valueT) with (progress value)
      progress (CTor type value prf) | (Done valueT) | (Done valueV)
        = Done (CTorV valueV)
      progress (CTor type value prf) | (Done valueT) | (Step prfV)
        = Step (SimplifyCTorValue valueT prfV)
    progress (CTor type value prf) | (Step prfT)
        = Step (SimplifyCTorType prfT)

  progress (Match scrutinee body) with (progress scrutinee)
    progress (Match (CTor type' value prf) body) | (Done (CTorV valueV))
      = Step (ReduceMatchBody valueV)
    progress (Match scrutinee body) | (Step prfS)
      = Step (SimplifyMatchScrut prfS)

  -- Binders
  progress (Let value body) with (progress value)
      progress (Let value body) | (Done valueV)
        = Step (ReduceLetBody valueV)
      progress (Let value body) | (Step prfV)
        = Step (SimplifyLetValue prfV)

  progress (NewType desc body) with (progress desc)
    progress (NewType desc body) | (Done valueD)
      = Step (ReduceNewType valueD)
    progress (NewType desc body) | (Step prfD)
     = Step (SimplifyNewType prfD)

  progress (TypeAlias desc body) with (progress desc)
    progress (TypeAlias desc body) | (Done valueD)
      = Step (ReduceTypeAlias valueD)
    progress (TypeAlias desc body) | (Step prfD)
      = Step (SimplifyTypeAlias prfD)

namespace Evaluation

  public export
  data Reduces : (this : SystemFoo ctxt type)
              -> (that : SystemFoo ctxt type)
              -> Type
    where
      Refl  : {this : SystemFoo ctxt type}
                   -> Reduces this this

      Trans : {this, that, end : SystemFoo ctxt type}
           -> Redux this that
           -> Reduces that end
           -> Reduces this end

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

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

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

  public export
  covering
  forever : Fuel
  forever = More forever

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

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

-- namespace Example

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

max_stars_repo_name: border-patrol/pearly-razors

max_issues_repo_name: border-patrol/pearly-razors

max_forks_repo_name: border-patrol/pearly-razors


text:
module Main

import Specdris.SpecIO

%default total

querySelector : (selector : String) -> JS_IO Ptr
querySelector = foreign FFI_JS "document.querySelector(%0)" _

isNull : Ptr -> JS_IO Bool
isNull ptr = do
  "true" <- foreign FFI_JS "(%0 === null).toString()" (Ptr -> JS_IO String) ptr
    | _ => pure False
  pure True

getInnerText : Ptr -> JS_IO String
getInnerText = foreign FFI_JS "%0.innerText" _

removeTestElements : JS_IO SpecResult -> JS_IO SpecResult
removeTestElements resultIO = do
  result <- resultIO
  foreign FFI_JS
    """
      document.body.querySelectorAll(':not(script)').forEach(function(child) {
        document.body.removeChild(child);
      })
    """ (JS_IO ())
  pure result

addParagraph : String -> JS_IO ()
addParagraph = foreign FFI_JS
  "document.body.appendChild(document.createElement('p')).innerText = %0" _

addParagraphSpec : SpecTree' FFI_JS
addParagraphSpec =
  describe "addParagraph" $ do
    it "appends a <p> element" $ do
      addParagraph ""

      null <- querySelector "p" >>= isNull
      pure $ shouldBeFalse null
    it "creates the correct text" $ do
      let expected = "hello specdris"
      addParagraph expected

      actual <- querySelector "p" >>= getInnerText
      pure $ actual === expected

main : JS_IO ()
main = specIO' {around = removeTestElements} $ do
  addParagraphSpec

max_stars_repo_name: pheymann/specdris

max_issues_repo_name: pheymann/specdris

max_forks_repo_name: pheymann/specdris


text:
||| `Header` is a wrapper for `OrdList` that hides the order relationship
||| and allows order independent list syntax for headers fields declaration.
|||
||| For example
||| `the (Header Char) ['a' ::: String, 'b' ::: Bool] = the (Header Char) ['b' ::: Bool, 'a' ::: String]`
||| holds.
|||
||| While `Header` doesn't define the usual `List` constructors,
||| the `List` syntax is available (and should be use)
||| as both `Nil` and `::` are defined for `Header`
module Flexidisc.Header.Type

import Flexidisc.OrdList

%default total
%access public export

||| Wrapper for `OrdList` that hide the order relationship
data Header' : (k, t : Type) -> Type where
  H : (o : Ord k) => OrdList k o t -> Header' k t

implementation Functor (Header' k) where

  map f (H xs) = H (map f xs)

||| Wrapper for `OrdList` that hide the order relationship
Header : (k : Type) -> Type
Header k = Header' k Type

||| Extract the wrapped `OrdList` along with it's order relation
unwrap : Header' k a -> (o ** OrdList k o a)
unwrap (H hs) = (_ ** hs)

||| A helper for the empty header creation
Nil : Ord k => Header' k a
Nil = H []

||| Append actually called insert on the underlying `OrdList`, to ensure that
||| the header labels are sorted
(::) : (k, a) -> Header' k a -> Header' k a
(::) x (H h) = H (insert x h)

merge : (xs, ys : Header' k a) -> Header' k a
merge (H xs) (H ys) = H (merge xs ys)

toList : Header' k a -> List (k, a)
toList (H xs) = toList xs

optional : Header k -> Header k
optional (H xs) = H (map Maybe xs)

max_stars_repo_name: berewt/flexidisc

max_issues_repo_name: LIST-LUXEMBOURG/flexidisc

max_forks_repo_name: LIST-LUXEMBOURG/flexidisc


text:
module Test

export
aString : String
aString = "Hello, World!"

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
module StringLiteral

rawStr : String
rawStr = #""""""#

interp1 : String
interp1 = "Just 1 + Just 2 = \{
  show $ do a <- Just 1
            b <- Just 2
            Just (a + b)
}"

interp2 : String
interp2 = "hello\{ " " ++ ##"world\##{#"."#}"## }"

multi1 : String
multi1 = """
  [project]
  name: "project"
  version: "0.1.0"
  [deps]
  "semver" = 0.2
  """

multi2 : String
multi2 = #"""
            a\#
             b\n
              \#{"c"}
            """#

multi3 : String
multi3 = """
  \{"sticking"} \{"together"}\{
 ""}\{#"""
!

"""#}
  """

multi4 : String
multi4 = """
  A very very \n\nvery very very \n
  very long string. \
  """

test : IO ()
test = do
    putStrLn rawStr
    putStrLn interp1
    putStrLn interp2
    let idris = "Idris"
    putStrLn "Hello \{idris ++ show 2}!"
    putStrLn multi1
    putStrLn multi2
    putStrLn multi3
    putStrLn multi4
    putStrLn """
    """
    putStrLn ##"""
a
"""##
    putStrLn ##"""
name: #"foo"
version: "bar"
bzs: \#\'a\n\t\\'
"""
"""##
    printLn "contains\NULcharacter"


text:
module Http.Uri

import public Data.Vect

%access public export

record URIAuth where
  constructor MkURIAuth
  uriUsername : Maybe String
  uriPassword : Maybe String
  uriHost : String
  uriPort : Int

record URI where
  constructor MkURI
  uriScheme : String
  uriAuth : URIAuth
  uriPath : String
  uriQuery : Vect q (String, String)
  uriFragment : String

urlEncode : String -> String
urlEncode = id -- TODO: Implement

||| This functions folds a list of query parameters
||| into a query string without prepending '?'.
||| It will also url encode all strings.
|||
||| For example `encodeQuery [("hello", "world"), ("foo", "bar")]`
||| encodes to "hello=world&foo=bar".
|||
||| @ n The length of the vector => the number of query parameters
||| @ q The vector of query param tuples
encodeQuery : (q : Vect n (String, String)) -> String
encodeQuery [] = ""
encodeQuery ((k,v) :: []) = urlEncode k ++ "=" ++ urlEncode v
encodeQuery ((k,v) :: xs) =
  urlEncode k ++ "=" ++ urlEncode v ++ "&" ++ encodeQuery xs

uriToString : URI -> String
uriToString u = let query = encodeQuery (uriQuery u) in
  uriScheme u ++ "://" ++ authStr (uriAuth u) ++
  (uriHost . uriAuth $ u) ++ ":" ++ show (uriPort . uriAuth $ u) ++
  uriPath u ++ querySeperator query ++ query ++ uriFragment u
  where
    authPassword : URIAuth -> String
    authPassword u' = fromMaybe "" (uriPassword u' >>= pure . (":" ++))

    authStrMaybe : URIAuth -> Maybe String
    authStrMaybe u' = pure $
      !(uriUsername u') ++ authPassword u' ++ "@"

    authStr : URIAuth -> String
    authStr u' = fromMaybe "" (authStrMaybe u')

    querySeperator : String -> String
    querySeperator "" = ""
    querySeperator _ = "?"

max_stars_repo_name: unthingable/idris-https

max_issues_repo_name: unthingable/idris-https

max_forks_repo_name: unthingable/idris-https


text:
module Idris2Rust.Main

import Core.Context
import Compiler.Common
import Idris.Driver

import System
import System.Directory
import System.File
import System.Info

import Libraries.Data.NameMap
import Libraries.Data.Version

import Idris2Rust.CompileCfg

-- %default covering

compile : Profile
       -> Ref Ctxt Defs
       -> (tmpDir : String)
       -> (outputDir : String)
       -> ClosedTerm
       -> (outfile : String)
       -> Core (Maybe String)
compile profile defs tmpDir outputDir term file
  = do coreLift $ putStrLn "I'd rather not."
       pure $ Nothing

execute : Profile -> Ref Ctxt Defs -> (tmpDir : String) -> ClosedTerm -> Core ()
execute profile defs tmpDir term = do coreLift $ putStrLn "Maybe in an hour."

export
rustCodegen : Profile -> Codegen
rustCodegen profile = MkCG (compile profile) (execute profile) Nothing Nothing

main : IO ()
main = mainWithCodegens [
  ("rust-debug", rustCodegen Debug),
  ("rust-release", rustCodegen Release)
]


text:
module Matrix

import Data.Vect
import Data.Nat
import Complex
import Lemmas

%default total

public export
Matrix : Nat -> Nat ->  Type
Matrix n m = Vect n (Vect m (Complex Double))

public export
Vector : Nat -> Type
Vector n = Vect n (Complex Double)

private
idRow : (n : Nat) -> Nat -> Vector n
idRow 0 _ = []
idRow (S k) 0 = 1 :: idRow k (S k)
idRow (S k) (S p) = 0 :: idRow k p

export
matrixId : (n : Nat) -> Matrix n n
matrixId n = matrixId' n 0 n where
  matrixId' : (k : Nat) -> (p : Nat) -> (n : Nat) -> Matrix k n
  matrixId' 0 p n = []
  matrixId' (S k) p n = (idRow n p) :: matrixId' k (S p) n

export
addVector : Vector n -> Vector n -> Vector n
addVector [] [] = []
addVector (x::xs) (y::ys) = (x+y) :: (addVector xs ys)

export
addMatrix : Matrix n m -> Matrix n m -> Matrix n m
addMatrix [] [] = []
addMatrix (x :: xs) (y :: ys) = (addVector x y) :: (addMatrix xs ys)

private
vectProduct : Vector n -> Vector n -> Complex Double
vectProduct [] [] = 0
vectProduct (x :: xs) (y :: ys) = x * y + vectProduct xs ys

private
makeCol : Vector n -> Matrix n 1
makeCol [] = []
makeCol (x :: xs) = [x] :: makeCol xs

private
addCol : Vector n -> Matrix n p -> Matrix n (S p)
addCol [] [] = []
addCol (x :: xs) (v :: vs) = (x :: v) :: addCol xs vs

export
transposeMatrix : {n : Nat} -> {p : Nat} ->  Matrix n p -> Matrix p n
transposeMatrix [] = replicate _ []
transposeMatrix (x :: xs) = addCol x (transposeMatrix xs)

export
multVectMatrix : {n : Nat} -> {p : Nat} ->  Vector n -> Matrix n p -> Vector p
multVectMatrix v m =
  let mt = transposeMatrix m in multVectMatrix' v mt where
    multVectMatrix' : Vector l -> Matrix k l -> Vector k
    multVectMatrix' v [] = []
    multVectMatrix' v (x :: xs) = (vectProduct v x) :: multVectMatrix' v xs

export
matrixMult : {n : Nat} -> {m : Nat} -> {p : Nat} -> Matrix n m -> Matrix m p -> Matrix n p
matrixMult [] ys = []
matrixMult (x :: xs) ys = (multVectMatrix x ys) :: matrixMult xs ys

export
multScalarVect : Complex Double -> Vector n -> Vector n
multScalarVect _ [] = []
multScalarVect x (y :: ys) = (x * y) :: multScalarVect x ys

export
multScalarMatrix : Complex Double -> Matrix n m -> Matrix n m
multScalarMatrix _ [] = []
multScalarMatrix x (y :: ys) = multScalarVect x y :: multScalarMatrix x ys

private
concatRows : Matrix n p -> Matrix n q -> Matrix n (p + q)
concatRows [] [] = []
concatRows (x :: xs) (y :: ys) = (x ++ y) :: (concatRows xs ys)

private
concatCols : Matrix n p -> Matrix m p -> Matrix (n + m) p
concatCols v w = v ++ w

private
tensorProduct' : Vector (S n) -> Matrix p r -> Matrix p ((S n) * r)
tensorProduct' [x] m = rewrite multZeroLeftZero r in rewrite plusZeroRightNeutral r in multScalarMatrix x m
tensorProduct' (x :: y :: ys) m = (multScalarMatrix x m) `concatRows` (tensorProduct' (y :: ys) m)

export
tensorProduct : Matrix n (S m) -> Matrix p r -> Matrix (n * p) ((S m) * r)
tensorProduct [] _ = []
tensorProduct [v] xs = rewrite multZeroLeftZero p in rewrite plusZeroRightNeutral p in tensorProduct' v xs
tensorProduct (v :: w :: vs) xs = (tensorProduct' v xs) `concatCols` (tensorProduct (assert_smaller (v::w::vs) (w :: vs)) xs)

export
printComplex : Complex Double -> String
printComplex (x :+ y) =
  if y == 0 then show x
            else if x == 0 then show y ++ "i"
                 else show x ++ " + " ++ show y ++ "i"

export
printVector : Vector n -> String
printVector v = "[" ++ printVector' v ++ "]" where
  printVector' : Vector m -> String
  printVector' [] = ""
  printVector' [x] = printComplex x
  printVector' (x :: xs) = printComplex x ++ " , " ++  printVector' xs

export
printMatrix : Matrix n m -> String
printMatrix v = "[ " ++ printMat' v where
  printMat' : Matrix p q -> String
  printMat' [] = ""
  printMat' [x] = printVector x ++ " ]"
  printMat' (x :: xs) = printVector x ++ "\n  " ++ printMat' xs

------------ Lemmas about matrices ---------------------------------------

export
powPlusMultZeroRightNeutral : (n : Nat) -> plus (power 2 n) (mult 0 (power 2 n)) = power 2 n
powPlusMultZeroRightNeutral n = rewrite plusZeroRightNeutral (power 2 n) in Refl

export
multPowerPowerPlus : (base, exp, exp' : Nat) ->
                     power base (exp + exp') = (power base exp) * (power base exp')
multPowerPowerPlus base Z       exp' =
    rewrite plusZeroRightNeutral (power base exp') in Refl
multPowerPowerPlus base (S exp) exp' =
  rewrite multPowerPowerPlus base exp exp' in
    rewrite sym $ multAssociative base (power base exp) (power base exp') in
       Refl

export
powPlusZeroRightNeutral : {m : Nat} -> Matrix (plus (plus (power 2 m) (plus (power 2 m) 0)) 0) 1 -> Matrix (plus (power 2 m) (plus (power 2 m) 0)) 1
powPlusZeroRightNeutral mat = rewrite sym $ plusZeroRightNeutral (plus (power 2 m) (plus (power 2 m) 0)) in mat

------------ LINEAR-ALGEBRAIC SIMULATION: MATRIX OPERATIONS ---------------

export
matrixH : Matrix 2 2
matrixH = [[(1/(sqrt 2)) :+ 0, (1/(sqrt 2)) :+ 0], [(1/(sqrt 2)) :+ 0 , (-1/(sqrt 2)) :+ 0]]

export
matrixP : Double -> Matrix 2 2
matrixP p = [[1 , 0] , [0, cis p]]

export
matrixCNOT : Matrix 4 4
matrixCNOT = [[1,0,0,0] , [0,1,0,0] , [0,0,0,1] , [0,0,1,0]]

export
matrixX : Matrix 2 2
matrixX = [[0,1] , [1,0]]

export
matrixKet0Bra0 : Matrix 2 2
matrixKet0Bra0 = [[1,0] , [0,0]]

export
matrixKet1Bra1 : Matrix 2 2
matrixKet1Bra1 = [[0,0] , [0,1]]

export
simpleTensor : Matrix 2 2 -> (n : Nat) -> Nat -> Matrix (power 2 n) (power 2 n)
simpleTensor _ 0 _ = [[1]]
simpleTensor m (S n) 0 = m `tensorProduct` (simpleTensor m n (S n))
simpleTensor m (S n) (S k) = (matrixId 2) `tensorProduct` (simpleTensor m n k)

export
tensorCnotAux : (n : Nat) -> (control : Nat) -> (target : Nat) -> Matrix (power 2 n) (power 2 n)
tensorCnotAux 0 _ _ = [[1]]
tensorCnotAux (S n) 0 0 = (matrixId 2) `tensorProduct` (tensorCnotAux n (S n) (S n)) --should not be happening
tensorCnotAux (S n) 0 (S m) = matrixKet1Bra1 `tensorProduct` (tensorCnotAux n (S n) m)
tensorCnotAux (S n) (S k) 0 = matrixX `tensorProduct` (tensorCnotAux n k (S n))
tensorCnotAux (S n) (S k) (S m) = (matrixId 2) `tensorProduct` (tensorCnotAux n k m)

export
tensorCNOT : (n : Nat) -> (control : Nat) -> (target : Nat) -> Matrix (power 2 n) (power 2 n)
tensorCNOT nbQbits control target = (simpleTensor matrixKet0Bra0 nbQbits control) `addMatrix` (tensorCnotAux nbQbits control target)

export
tensorProductVect : Matrix (power 2 n) 1 -> Matrix (power 2 p) 1 -> Matrix (power 2 (n + p)) 1
tensorProductVect xs ys =
  rewrite multPowerPowerPlus 2 n p
  in tensorProduct xs ys

export
normState2 : Matrix n 1 -> Double
normState2 [] = 0
normState2 ([x] :: xs) = let m = magnitude x in m * m + normState2 xs

export
toTensorBasis : Matrix n 2 -> Matrix (power 2 n) 1
toTensorBasis [] = [[1]]
toTensorBasis ([x,y] :: xs) = tensorProduct [[x] , [y]] (toTensorBasis xs)

export
ket0 : (n : Nat) -> Matrix n 2
ket0 0 = []
ket0 (S k) = [1 , 0] :: ket0 k

export
inv : Double -> Double
inv x = if x == 0 then 0 else 1/x

export
projectState : {n : Nat} -> Matrix (power 2 (S n)) 1 -> (i : Nat) ->
               Bool -> Matrix (power 2 n) 1
projectState v 0 b =
  let (v1, v2) = splitAt (power 2 n) v in
      case b of
           True => rewrite sym $ powPlusMultZeroRightNeutral n in v2
           False => v1
projectState {n = 0} _ (S k) _ = [[1]]
projectState {n = S m} v (S k) b =
  let (v1, v2) = splitAt (power 2 (S m)) v
      v1' = projectState {n = m} v1 k b
      v2' = projectState {n = m} (powPlusZeroRightNeutral v2) k b
  in rewrite plusZeroRightNeutral (power 2 m) in v1' ++ v2'

max_stars_repo_name: zamdzhiev/Qimaera

max_issues_repo_name: zamdzhiev/Qimaera

max_forks_repo_name: zamdzhiev/Qimaera


text:
-- ------------------------------------------------------ [ Tree.idr<RedBlack> ]
-- Module    : Tree.idr
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
-- http://www.cs.kent.ac.uk/people/staff/smk/redblack/Untyped.hs
module Data.RedBlack.Tree

import Debug.Error
%language ElabReflection

%default total
%access export

-- ------------------------------------------------------------- [ Definitions ]
public export
data Colour = R | B

||| The core tree key-value data structure used to represent an
||| Red-Black Tree.
|||
||| This structure doesn't encode the invariants of the tree and is
||| *simply* a container. This structure ideally shouldn't be exposed
||| to the user at all. This structure should be used to build other
||| data structures.  See the modules alongside this for appropriate
||| interfaces for using the tree.
|||
||| @keyTy The type associated with the key.
||| @valTy The type associated with the value.
public export
data Tree : (colour : Colour)
         -> (keyTy : Type)
         -> (valTy : Type)
         -> Type
  where
    ||| An empty Tree node.
    Empty : Tree B k v

    ||| A Key Value node in the Tree.
    |||
    ||| @key   The key.
    ||| @val   The value associated with the key.
    ||| @left  The left child of the Node
    ||| @right THe right child of the Node.
    Node : (c3 : Colour)
        -> (key   : k)
        -> (val   : v)
        -> (left  : Tree c1 k v)
        -> (right : Tree c2 k v)
        -> Tree c3 k v

%name Tree t, tree

public export
data RBInvariant : (blackHeight : Nat)
                -> (colour : Colour)
                -> (valid : Bool)
                -> (tree : Tree colour k v)
                -> Type
  where
    ||| A tree of height zero.
    RBEmpty : RBInvariant 0 B True Empty
    ||| A balanced black tree.
    |||
    ||| @left  The invariant of the left child.
    ||| @right The invariant of the right child.
    BNode : (left  : RBInvariant n _ True l)
         -> (right : RBInvariant n _ True r)
         -> RBInvariant (S n) B True (Node B k v l r)
    ||| A balanced red tree.
    |||
    ||| @left  The invariant of the left child.
    ||| @right The invariant of the right child.
    RNode : (left  : RBInvariant n B True l)
         -> (right : RBInvariant n B True r)
         -> RBInvariant n R True (Node R k v l r)

    ||| A red tree with a red left child.
    |||
    ||| @left  The invariant of the left child.
    ||| @right The invariant of the right child.
    LBad : (left  : RBInvariant n R True l)
        -> (right : RBInvariant n B True r)
        -> RBInvariant n R False (Node R k v l r)

    ||| A red tree with a red right child.
    |||
    ||| @left  The invariant of the left child.
    ||| @right The invariant of the right child.
    RBad : (left  : RBInvariant n B True l)
        -> (right : RBInvariant n R True r)
        -> RBInvariant n R False (Node R k v l r)

%name RBInvariant inv

||| An Red-Black Tree.
|||
||| Modelled using subset to separate the invariants from the tree
||| implementation itself.
|||
||| @blackHeight  The height of the Tree.
||| @keyTy        The type associated with the keys.
||| @valueTy      The type associated with the values.
public export
RBTree : (blackHeight  : Nat)
      -> (colour : Colour)
      -> (keyTy   : Type)
      -> (valueTy : Type)
      -> Type
RBTree n c k v = Subset (Tree c k v) (RBInvariant n c True)

private
InsTree : (blackHeight  : Nat)
       -> (colour : Colour)
       -> (keyTy   : Type)
       -> (valueTy : Type)
       -> (valid : Bool)
       -> Type
InsTree n c k v valid = Subset (Tree c k v) (RBInvariant n c valid)

-- --------------------------------------------------------------- [ Insertion ]

private
balance : k -> v -> RBTree n c1 k v -> RBTree n c2 k v -> (c3 ** RBTree (S n) c3 k v)
balance {n} y vy (Element (Node _ x vx a b) (RNode pf_l_l pf_l_r))
                 (Element (Node _ z vz c d) (RNode pf_r_l pf_r_r)) =
  let t = (Node R y vy (Node B x vx a b) (Node B z vz c d))
      pf = RNode (BNode pf_l_l pf_l_r) (BNode pf_r_l pf_r_r)
  in (R ** Element t pf)
balance {n} x vx (Element a pf_a) (Element b pf_b) =
  let t = (Node B x vx a b)
      pf = BNode pf_a pf_b
  in (B ** Element t pf)

private
recolorRight : (Ord k) => k -> v -> RBTree n c k v -> InsTree n R k v False -> (c' ** valid ** InsTree (S n) c' k v valid)

recolorRight g vg (Element (Node R u vu t5 t4) (RNode pf_5 pf_4))
                  (Element (Node R p vp t3 tn) (RBad pf_3 pf_n)) =
  (R ** True ** Element (Node R g vg (Node B u vu t5 t4) (Node B p vp t3 tn))
                        (RNode (BNode pf_5 pf_4) (BNode pf_3 pf_n)))

recolorRight g vg (Element (Node R u vu t5 t4) (RNode pf_5 pf_4))
                  (Element (Node R p vp tn t3) (LBad pf_n pf_3)) =
  (R ** True ** Element (Node R g vg (Node B u vu t4 t5) (Node B p vp tn t3))
                        (RNode (BNode pf_4 pf_5) (BNode pf_n pf_3)))

recolorRight g vg (Element (Node B u vu t5 t4) (BNode pf_5 pf_4))
                  (Element (Node R p vp t3 (Node R n vn t2 t1)) (RBad pf_3 (RNode pf_2 pf_1))) =
  (B ** True ** Element (Node B p vp (Node R g vg (Node B u vu t5 t4) t3)
                                     (Node R n vn t2 t1))
                        (BNode (RNode (BNode pf_5 pf_4) pf_3) (RNode pf_2 pf_1)))

recolorRight g vg (Element Empty RBEmpty)
                  (Element (Node R p vp t3 (Node R n vn t2 t1)) (RBad pf_3 (RNode pf_2 pf_1))) =
  (B ** True ** Element (Node B p vp (Node R g vg Empty t3)
                                     (Node R n vn t2 t1))
                        (BNode (RNode RBEmpty pf_3) (RNode pf_2 pf_1)))

recolorRight g vg (Element (Node B u vu t5 t4) (BNode pf_5 pf_4))
                  (Element (Node R p vp (Node R n vn t3 t2) t1) (LBad (RNode pf_3 pf_2) pf_1)) =
  (B ** True ** Element (Node B n vn (Node R g vg (Node B u vu t5 t4) t3)
                                     (Node R p vp t2 t1))
                        (BNode (RNode (BNode pf_5 pf_4) pf_3) (RNode pf_2 pf_1)))

recolorRight g vg (Element Empty RBEmpty)
                  (Element (Node R p vp (Node R n vn t3 t2) t1) (LBad (RNode pf_3 pf_2) pf_1)) =
  (B ** True ** Element (Node B n vn (Node R g vg Empty t3)
                                     (Node R p vp t2 t1))
                        (BNode (RNode RBEmpty pf_3) (RNode pf_2 pf_1)))

private
recolorLeft : (Ord k) => k -> v -> InsTree n R k v False -> RBTree n c k v -> (c' ** valid ** InsTree (S n) c' k v valid)

recolorLeft g vg (Element (Node R p vp tn t3) (LBad pf_n pf_3))
                 (Element (Node R u vu t4 t5) (RNode pf_4 pf_5)) =
  (R ** True ** Element (Node R g vg (Node B p vp tn t3)
                                     (Node B u vu t4 t5))
                        (RNode (BNode pf_n pf_3) (BNode pf_4 pf_5)))

recolorLeft g vg (Element (Node R p vp t1 tn) (RBad pf_1 pf_n))
                 (Element (Node R u vu t4 t5) (RNode pf_4 pf_5)) =
  (R ** True ** Element (Node R g vg (Node B p vp t1 tn)
                                     (Node B u vu t4 t5))
                        (RNode (BNode pf_1 pf_n) (BNode pf_4 pf_5)))

recolorLeft g vg (Element (Node R p vp (Node R n vn t1 t2) t3) (LBad (RNode pf_1 pf_2) pf_3))
                 (Element (Node B u vu t4 t5) (BNode pf_4 pf_5)) =
  (B ** True ** Element (Node B p vp (Node R n vn t1 t2)
                                     (Node R g vg t3 (Node B u vu t4 t5)))
                        (BNode (RNode pf_1 pf_2) (RNode pf_3 (BNode pf_4 pf_5))))

recolorLeft g vg (Element (Node R p vp (Node R n vn t1 t2) t3) (LBad (RNode pf_1 pf_2) pf_3))
                 (Element Empty RBEmpty) =
  (B ** True ** Element (Node B p vp (Node R n vn t1 t2)
                                     (Node R g vg t3 Empty))
                        (BNode (RNode pf_1 pf_2) (RNode pf_3 RBEmpty)))

recolorLeft g vg (Element (Node R p vp t1 (Node R n vn t2 t3)) (RBad pf_1 (RNode pf_2 pf_3)))
                 (Element (Node B u vu t4 t5) (BNode pf_4 pf_5)) =
  (B ** True ** Element (Node B n vn (Node R p vp t1 t2)
                                     (Node R g vg t3 (Node B u vu t4 t5)))
                        (BNode (RNode pf_1 pf_2) (RNode pf_3 (BNode pf_4 pf_5))))

recolorLeft g vg (Element (Node R p vp t1 (Node R n vn t2 t3)) (RBad pf_1 (RNode pf_2 pf_3)))
                 (Element Empty RBEmpty) =
  (B ** True ** Element (Node B n vn (Node R p vp t1 t2)
                                     (Node R g vg t3 Empty))
                        (BNode (RNode pf_1 pf_2) (RNode pf_3 RBEmpty)))

private
ins : Ord k => k -> v -> RBTree n c k v -> (c' ** valid ** InsTree n c' k v valid)
ins x vx (Element Empty RBEmpty) = (R ** True ** Element (Node R x vx Empty Empty) (RNode RBEmpty RBEmpty))
ins x vx t@(Element (Node _ y _ _ _) _) = insWith x vx t (compare x y)
  where
    addValid : (c ** InsTree n c k v True) -> (c ** valid ** InsTree n c k v valid)
    addValid (c ** t) = (c ** True ** t)

    insWith : Ord k => k -> v -> RBTree n c k v -> Ordering -> (c' ** valid ** InsTree n c' k v valid)

    insWith x vx (Element Empty RBEmpty) _ =  -- unreachable, but make totality checker happy
      (R ** True ** Element (Node R x vx Empty Empty) (RNode RBEmpty RBEmpty))

    insWith x vx (Element n@(Node B y vy a b) pf) EQ =
      (B ** True ** Element n pf)
    insWith x vx t@(Element (Node B y vy a b) (BNode pf_a pf_b)) LT =
      let t_a = assert_smaller t (Element a pf_a)
      in case ins x vx t_a of
        (_ ** True ** t_a') => addValid (balance y vy t_a' (Element b pf_b))
        (R ** False ** t_a') => recolorLeft y vy t_a' (Element b pf_b)
        (B ** False ** (Element _ _)) impossible
    insWith x vx t@(Element (Node B y vy a b) (BNode pf_a pf_b)) GT =
      let t_b = assert_smaller t (Element b pf_b)
      in case ins x vx t_b of
        (_ ** True ** t_b') => addValid (balance y vy (Element a pf_a) t_b')
        (R ** False ** t_b') => recolorRight y vy (Element a pf_a) t_b'
        (B ** False ** (Element _ _)) impossible

    insWith x vx (Element n@(Node R y vy a b) pf) EQ =
      (R ** True ** Element n pf)
    insWith x vx t@(Element (Node R y vy a b) (RNode pf_a pf_b)) LT =
      let t_a = assert_smaller t (Element a pf_a)
      in case ins x vx t_a of
        (B ** True ** Element a' pf_a') => (R ** True ** Element (Node R y vy a' b) (RNode pf_a' pf_b))
        (R ** True ** Element a' pf_a') => (R ** False ** Element (Node R y vy a' b) (LBad pf_a' pf_b))
        (R ** False ** t_a') => error "impossible"
        (B ** False ** Element _ _) impossible
    insWith x vx t@(Element (Node R y vy a b) (RNode pf_a pf_b)) GT =
      let t_b = assert_smaller t (Element b pf_b)
      in case ins x vx t_b of
        (B ** True ** Element b' pf_b') => (R ** True ** Element (Node R y vy a b') (RNode pf_a pf_b'))
        (R ** True ** Element b' pf_b') => (R ** False ** Element (Node R y vy a b') (RBad pf_a pf_b'))
        (R ** False ** t_b') => error "impossible"
        (B ** False ** Element _ _) impossible

-- --------------------------------------- [ Public API for working with Trees ]

||| An empty tree
empty : RBTree 0 B k v
empty = Element Empty RBEmpty

||| Insert a key value pair into the tree, returning a the new tree
||| and possibly its new height.
insert : Ord k => k -> v -> RBTree n B k v -> (n' : Nat ** RBTree n' B k v)
insert x vx s =
  case ins x vx s of
    (B ** True ** t) => (_ ** t)
    (R ** True ** Element (Node R k v l r) (RNode pf_l pf_r)) =>
      (_ ** Element (Node B k v l r) (BNode pf_l pf_r))
    (B ** False ** Element _ _) impossible
    (R ** False ** Element (Node R k v l r) (RBad pf_l pf_r)) =>
      (_ ** Element (Node B k v l r) (BNode pf_l pf_r))
    (R ** False ** Element (Node R k v l r) (LBad pf_l pf_r)) =>
      (_ ** Element (Node B k v l r) (BNode pf_l pf_r))

||| Find a value in the tree.
lookup : (Ord k) => k -> RBTree n B k v -> Maybe v
lookup key (Element t _) = lookup' key t
  where
    lookup' : (Ord k) => k -> Tree c k v -> Maybe v
    lookup' key Empty = Nothing
    lookup' key (Node _ key' value' l r) with (compare key key')
      lookup' key (Node _ key' value' l r) | LT = lookup' key l
      lookup' key (Node _ key' value' l r) | EQ = Just value'
      lookup' key (Node _ key' value' l r) | GT = lookup' key r

||| Perform a right fold over the tree.
foldr : (step : k -> v -> p -> p)
     -> (init : p)
     -> RBTree n B k v
     -> p
foldr step init (Element t _) = foldr' step init t
  where
    foldr' : (k -> v -> p -> p) -> p -> Tree c k v -> p
    foldr' step' init' Empty = init'
    foldr' step' init' (Node _ key val l r) = foldr' step' (step' key val (foldr' step' init' r)) l

||| Construct a AVL Tree from an association list.
fromList : (Ord k) => List (k, v) -> (n : Nat ** RBTree n B k v)
fromList xs = go xs empty
  where go : (Ord k) => List (k, v) -> RBTree n B k v -> (n' : Nat ** RBTree n' B k v)
        go [] t = (0 ** Element Empty RBEmpty)
        go ((k, v) :: xs) t = case insert k v t of
          (_ ** t') => go xs t'

||| Flatten the tree to an association list.
toList : RBTree n B k v -> List (k, v)
toList = foldr (\k,v,xs => (k, v) :: xs) []

||| Size of the tree.
size : RBTree n B k v -> Nat
size t = Tree.foldr (\_,_,res => S res) Z t

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


text:
module GCDZZ
import Divisors
import ZZ
import NatUtils
import gcd
import ZZUtils
%access public export

|||Converts the expression (a=r+(q*b)) to its integer equivalent
total
ExpNatToZZ:{a:Nat}->{b:Nat}->(a=r+(q*b))->((Pos a)=Pos(r)+((Pos q)*(Pos b)))
ExpNatToZZ Refl = Refl

|||Given a nonnegative integer a and positive integer b, it returns quotient and remainder
|||with proof of (a = rem + (quot * b) and that 0<=rem<b
total
QuotRemZ:(a:ZZ)->(b:ZZ)->IsNonNegative a -> IsPositive b ->
(quot : ZZ ** (rem : ZZ ** ((a = rem + (quot * b)), LTZ rem b,(IsNonNegative rem))))
QuotRemZ (Pos j) (Pos (S k)) NonNegative Positive =
  case (euclidDivide j (S k) (SIsNotZ {x=(k)})) of
    (q ** (r ** (equality, rlessb))) =>
         ((Pos q)**((Pos r)**((ExpNatToZZ equality),(ltNatToZZ rlessb),NonNegative)))

|||Returns gcd of a and b with proof when a is positive and b is nonnegative
GCDCalc :(a:ZZ)->(b:ZZ)->(IsPositive a)->(IsNonNegative b)->(d**(GCDZ a b d))
GCDCalc a (Pos Z) x NonNegative = (a**(gcdOfZeroAndInteger a x))
GCDCalc (Pos (S j)) (Pos  (S k)) Positive NonNegative =
  case QuotRemZ (Pos (S j)) (Pos  (S k)) NonNegative Positive of
    (quot ** (rem  ** (equality, remLessb,remNonNeg))) =>
       (case GCDCalc (Pos (S k)) rem Positive remNonNeg of
             (x ** pf) => (x**(euclidConservesGcdWithProof equality pf)))

|||Returns gcd of two integers with proof given that not both of them are zero
gcdZZ:(a:ZZ)->(b:ZZ)->(NotBothZeroZ a b)->(d**(GCDZ a b d))
gcdZZ (Pos (S k)) (Pos j) LeftPositive =
  GCDCalc (Pos (S k)) (Pos j) Positive NonNegative
gcdZZ (Pos (S k)) (NegS j) LeftPositive =
  case GCDCalc (Pos (S k)) (-(NegS j)) Positive NonNegative of
                (x ** pf) => (x**(negatingPreservesGcdRight pf))
gcdZZ (NegS k) (Pos j) LeftNegative =
  case GCDCalc (-(NegS k)) (Pos j) Positive NonNegative of
    (x**pf) =>(x**(negatingPreservesGcdLeft pf))
gcdZZ (NegS k) (NegS j) LeftNegative =
  case GCDCalc (-(NegS k)) (-(NegS j)) Positive NonNegative of
        (x ** pf) => (x**((negatingPreservesGcdLeft (negatingPreservesGcdRight pf))))
gcdZZ a (Pos (S k)) RightPositive =
  case gcdZZ (Pos (S k)) a LeftPositive of
    (x ** pf) => (x** (gcdSymZ pf))
gcdZZ a (NegS k) RightNegative =
  case gcdZZ (NegS k) a LeftNegative of
      (x ** pf) => (x** (gcdSymZ pf))


text:
{-
  An embeded DSL for prolog-style logic programming, based on the
  pure-prolog parser and interpreter originally written in Haskell

  Original author: Ken Friis Larsen      <kflarsen@diku.dk>
  Translated into Idris by Nathan Bedell <nbedell@tulane.edu>
-}

module Ast

%access public export

----------------------------------------------------------------------
-- Abstract Syntax Tree
----------------------------------------------------------------------

Atom : Type
Atom = String

Variable : Type
Variable = String

data Term : Type where
 Var : Variable -> Term
 Comp : Atom -> List Term -> Term

and' : List Bool -> Bool
and' [] = True
and' xs = foldr1 p xs
  where p True True = True
        p x y = False

implementation Eq Term where
  (Var x) == (Var y) = assert_total $ x == y
  (Comp x y) == (Comp x' y') = assert_total $ (x == x') && (and' $ Prelude.List.zipWith (==) y y')
  x == y = assert_total $ False

implementation Show Term where
  show (Var s) = s
  show (Comp s []) = s
  show (Comp s xs) = s ++ "(" ++ (concat $ intersperse "," (map show xs)) ++ ")"

Terms : Type
Terms = List Term

Clause : Type
Clause = (Term, Terms) -- head and body

Clauses : Type
Clauses = List Clause

Goal : Type
Goal = List Term

Program : Type
Program = Clauses

max_stars_repo_name: Sintrastes/idr-pure-prolog

max_issues_repo_name: Sintrastes/idr-pure-prolog

max_forks_repo_name: Sintrastes/idr-pure-prolog


text:
module Flexidisc.Transformation.TransHeader

import Flexidisc.Dec.IsYes
import Flexidisc.Header.Type
import Flexidisc.OrdList
import Flexidisc.Transformation.Type

%default total
%access public export

data TransHeader : (k : Type) -> Type where
  T : (o : Ord k) => OrdList k o MapValue -> TransHeader k

Nil : Ord k => TransHeader k
Nil = T []

(::) : (k, MapValue) -> TransHeader k -> TransHeader k
(::) x (T h) = T (insert x h)

IsFresh : (DecEq label) => (l : label) -> (xs : TransHeader label) -> Type
IsFresh l (T xs) = IsYes (decFresh l xs)

toLabels : TransHeader k -> List k
toLabels (T xs) = toLabels xs

toSource : TransHeader k -> Header k
toSource (T xs) = H (toSource xs)

toTarget : TransHeader k -> Header k
toTarget (T xs) = H (toTarget xs)


text:
module Main

import Effects
import Effect.StdIO
import Effect.Random
import Data.So
import Data.Fin
import Data.Vect
import VectMissing

-----------------------------------------------------------------------
-- GAME STATE
-----------------------------------------------------------------------

{- First, the game state, HState, where the type specifies how many guesses
are left and how many missing letters there are still to get. -}

data HState = Running Nat Nat | NotRunning

data Hangman : HState -> Type where
     Init     : Hangman NotRunning -- initialising, but not ready
     GameWon  : String -> Hangman NotRunning
     GameLost : String -> Hangman NotRunning
     MkH      : (word : String) ->
                (guesses : Nat) ->
                (got : List Char) ->
                (missing : Vect m Char) ->
                Hangman (Running guesses m)

implementation Default (Hangman NotRunning) where
    default = Init

implementation Show (Hangman s) where
    show Init = "Not ready yet"
    show (GameWon w) = "You won! Successfully guessed " ++ w
    show (GameLost w) = "You lost! The word was " ++ w
    show (MkH w guesses got missing)
         = let w' = pack (map showGot (unpack w)) in
               w' ++ "\n\n" ++ show guesses ++ " guesses left"
      where showGot : Char -> Char
            showGot ' ' = '/'
            showGot c = if ((not (isAlpha c)) || (c `elem` got)) then c else '-'

{- Initialise the state with the missing letters in a word -}

total
letters : String -> List Char
letters x with (strM x)
  letters "" | StrNil = []
  letters (strCons y xs) | (StrCons y xs)
          = let xs' = assert_total (letters xs) in
                if ((not (isAlpha y)) || (y `elem` xs')) then xs' else y :: xs'

initState : (x : String) -> Hangman (Running 6 (length (letters x)))
initState w = let xs = letters w in
                  MkH w _ [] (fromList (letters w))

-----------------------------------------------------------------------
-- RULES
-----------------------------------------------------------------------

{- Now, the rules of the game, written as an Effect.
We can think of the rules as giving a protocol that the game player and
the machine must follow for an implementation of the game to make sense.
-}

data HangmanRules : Effect where

-- Rule:
-- Precondition: we can make a guess if we have one or more guess available
-- (S g) and one or more letters are still missing (S w)

-- Postcondition: return whether the character was in the word. If so, reduce
-- the number of missing letters, if not, reduce the number of guesses left

     Guess : (x : Char) ->
             sig HangmanRules Bool
                 (Hangman (Running (S g) (S w)))
                 (\inword =>
                        Hangman (case inword of
                             True => (Running (S g) w)
                             False => (Running g (S w))))

-- The 'Won' operation requires that there are no missing letters

     Won  : sig HangmanRules ()
                (Hangman (Running g 0))
                (Hangman NotRunning)

-- The 'Lost' operation requires that there are no guesses left

     Lost : sig HangmanRules ()
                (Hangman (Running 0 g))
                (Hangman NotRunning)

-- Set up a new game, initialised with 6 guesses and the missing letters in
-- the given word. Note that if there are no letters in the word, we won't
-- be able to run 'Guess'!

     NewWord : (w : String) ->
               sig HangmanRules () h (Hangman (Running 6 (length (letters w))))

-- Finally, allow us to get the current game state

     Get  : sig HangmanRules h h

HANGMAN : HState -> EFFECT
HANGMAN h = MkEff (Hangman h) HangmanRules

-- Promote explicit effects to Eff programs

guess : Char -> Eff Bool
                [HANGMAN (Running (S g) (S w))]
                (\inword => [HANGMAN (case inword of
                                        True => Running (S g) w
                                        False => Running g (S w))])
guess c = call (Main.Guess c)

won :  Eff () [HANGMAN (Running g 0)] [HANGMAN NotRunning]
won = call Won

lost : Eff () [HANGMAN (Running 0 g)] [HANGMAN NotRunning]
lost = call Lost

new_word : (w : String) -> Eff () [HANGMAN h]
                                  [HANGMAN (Running 6 (length (letters w)))]
new_word w = call (NewWord w)

get : Eff (Hangman h) [HANGMAN h]
get = call Get

-----------------------------------------------------------------------
-- IMPLEMENTATION OF THE RULES
-----------------------------------------------------------------------

{- This effect handler simply updates the game state as necessary for
each operation. 'Guess' is slightly tricky, in that it needs to check
whether the letter is in the word, and branch accordingly (and if it
is in the word, update the vector of missing letters to be the right
length). -}

implementation Handler HangmanRules m where
    handle (MkH w g got []) Won k = k () (GameWon w)
    handle (MkH w Z got m) Lost k = k () (GameLost w)

    handle st Get k = k st st
    handle st (NewWord w) k = k () (initState w)

    handle (MkH w (S g) got m) (Guess x) k =
      case isElem x m of
           No _ => k False (MkH w _ got m)
           Yes p => k True (MkH w _ (x :: got) (shrink m p))

-----------------------------------------------------------------------
-- USER INTERFACE
-----------------------------------------------------------------------

{- Finally, an implementation of the game which reads user input and calls
the operations we defined above when appropriate.

The type indicates that the game must start in a running state, with some
guesses available, and get to a not running state (i.e. won or lost).
Since we picked a word at random, we can't actually make the assumption there
were valid letters in it!
-}

soRefl : So x -> (x = True)
soRefl Oh = Refl

game : Eff () [HANGMAN (Running (S g) w), STDIO]
              [HANGMAN NotRunning, STDIO]
game {w=Z} = won
game {w=S _}
     = do putStrLn (show !get)
          putStr "Enter guess: "
          let guess = trim !getStr
          case choose (not (guess == "")) of
               (Left p) => processGuess (strHead' guess (soRefl p))
               (Right p) => do putStrLn "Invalid input!"
                               game
  where
    processGuess : Char -> Eff () [HANGMAN (Running (S g) (S w)), STDIO]
                                  [HANGMAN NotRunning, STDIO]
    processGuess {g} c {w}
      = case !(guess c) of
             True => do putStrLn "Good guess!"
                        case w of
                             Z => won
                             (S k) => game
             False => do putStrLn "No, sorry"
                         case g of
                              Z => lost
                              (S k) => game

{- Some candidate words. We'll use programming languages. We don't want to
write the length explicitly, so infer it with a proof search. -}

words : ?wlen
words = with Vect ["idris","agda","haskell","miranda",
         "java","javascript","fortran","basic","racket",
         "coffeescript","rust","purescript","clean","links",
         "koka","cobol"]

wlen = proof search

{- It typechecks! Ship it! -}

runGame : Eff () [HANGMAN NotRunning, RND, STDIO]
runGame = do srand 1234567890
             let w = index !(rndFin _) words
             new_word w
             game
             putStrLn (show !get)

{- I made a couple of mistakes while writing this. For example, the following
were caught by the type checker:

* Forgetting to check the 'Won' state before continuing with 'game'
* Accidentally checking the number of missing letters rather than the number
  of guesses when checking if 'Lost' was callable

-}

main : IO ()
main = run runGame

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

max_stars_repo_name: grin-compiler/idris-grin

max_issues_repo_name: grin-compiler/idris-grin

max_forks_repo_name: grin-compiler/idris-grin


text:
X : Nat
X = let a : Nat
        a = 0
        in a

Y : Nat
Y = let a : Nat
        a = 0
    in a

Z : Nat
Z = let a : Nat
        a = 0
 in a

A : Nat
A = let a : Nat
        a = 0
          in a


text:
module Control.Monad.Trace

%default total
%access public export

-- Interface -------------------------------------------------------------------

interface ( Show l, Monad m ) => MonadTrace l (m : Type -> Type) | m where
  trace : l -> a -> m a

-- Instances -------------------------------------------------------------------

Show l => MonadTrace l IO where
  trace l x = do
    putStrLn $ "** " ++ show l
    pure x

max_stars_repo_name: mklinik/task-semantics

max_issues_repo_name: mklinik/task-semantics

max_forks_repo_name: mklinik/task-semantics


text:
module CIO

import public Control.Catchable

%default total

||| Catchable IO.
public export
record CIO e a where
  constructor MkCIO
  runCIO : IO (Either e a)

export
Functor (CIO e) where
  map f (MkCIO a) = MkCIO $ map (map f) a

export
Applicative (CIO e) where
  pure = MkCIO . pure . Right
  (MkCIO f) <*> a = MkCIO $ do
    f <- f
    case f of
      Left err => pure $ Left err
      Right f => runCIO $ map f a

export
Monad (CIO e) where
  (MkCIO a) >>= f = MkCIO $ do
    a <- a
    case a of
      Left err => pure $ Left err
      Right a => runCIO $ f a

export
Catchable (CIO e) e where
  throw = MkCIO . pure . Left
  catch (MkCIO a) f = MkCIO $ do
    a <- a
    case a of
      Left err => runCIO $ f err
      Right a => pure $ Right a

export
lift : IO a -> CIO e a
lift x = MkCIO $ do
  x <- x
  pure $ Right x

max_stars_repo_name: yubrot/idrlisp

max_issues_repo_name: yubrot/idrlisp

max_forks_repo_name: yubrot/idrlisp


text:
= Rel : Properties of Relations

> module Rel
>

\todo[inline]{Add hyperlinks}

This short (and optional) chapter develops some basic definitions and a few
theorems about binary relations in Idris. The key definitions are repeated where
they are actually used (in the `Smallstep` chapter), so readers who are already
comfortable with these ideas can safely skim or skip this chapter. However,
relations are also a good source of exercises for developing facility with
Idris's basic reasoning facilities, so it may be useful to look at this material
just after the `IndProp` chapter.

> import Logic
> import IndProp
>

A binary _relation_ on a set \idr{t} is a family of propositions parameterized
by two elements of \idr{t} — i.e., a proposition about pairs of elements of
\idr{t}.

> Relation : Type -> Type
> Relation t = t -> t -> Type

\todo[inline]{Edit, there's n-relation \idr{Data.Rel} in \idr{contrib}, but no
\idr{Relation}}

Confusingly, the Idris standard library hijacks the generic term "relation" for
this specific instance of the idea. To maintain consistency with the library, we
will do the same. So, henceforth the Idris identifier `relation` will always
refer to a binary relation between some set and itself, whereas the English word
"relation" can refer either to the specific Idris concept or the more general
concept of a relation between any number of possibly different sets. The context
of the discussion should always make clear which is meant.

\todo[inline]{There's a similar concept called \idr{LTE} in \idr{Prelude.Nat},
but it's defined by induction from zero}

An example relation on \idr{Nat} is \idr{Le}, the less-than-or-equal-to
relation, which we usually write \idr{n1 <= n2}.

```idris
λΠ> the (Relation Nat) Le
Le : Nat -> Nat -> Type
```

\todo[inline]{Edit to show it (probably) doesn't matter in Idris}

(Why did we write it this way instead of starting with \idr{data Le : Relation
Nat ...}? Because we wanted to put the first \idr{Nat} to the left of the
\idr{:}, which makes Idris generate a somewhat nicer induction principle for
reasoning about \idr{<='}.)

== Basic Properties

As anyone knows who has taken an undergraduate discrete math course, there is a
lot to be said about relations in general, including ways of classifying
relations (as reflexive, transitive, etc.), theorems that can be proved
generically about certain sorts of relations, constructions that build one
relation from another, etc. For example...

=== Partial Functions

A relation \idr{r} on a set \idr{t} is a _partial function_ if, for every
\idr{x}, there is at most one \idr{y} such that \idr{r x y} — i.e., \idr{r x y1}
and \idr{r x y2} together imply \idr{y1 = y2}.

> Partial_function : (r : Relation t) -> Type
> Partial_function {t} r = (x, y1, y2 : t) -> r x y1 -> r x y2 -> y1 = y2

\todo[inline]{"Earlier" = in \idr{IndProp}, add hyperlink?}

For example, the \idr{Next_nat} relation defined earlier is a partial function.

```idris
λΠ> the (Relation Nat) Next_nat
Next_nat : Nat -> Nat -> Type
```

> next_nat_partial_function : Partial_function Next_nat
> next_nat_partial_function x (S x) (S x) Nn Nn = Refl

However, the \idr{<='} relation on numbers is not a partial function. (Assume,
for a contradiction, that \idr{<='} is a partial function. But then, since
\idr{0 <=' 0} and \idr{0 <=' 1}, it follows that \idr{0 = 1}. This is nonsense,
so our assumption was contradictory.)

> le_not_a_partial_function : Not (Partial_function Le)
> le_not_a_partial_function f = absurd $ f 0 0 1 Le_n (Le_S Le_n)

==== Exercise: 2 stars, optional

\ \todo[inline]{Again, "earlier" = \idr{IndProp}}

Show that the \idr{Total_relation} defined in earlier is not a partial function.

> -- FILL IN HERE

$\square$

==== Exercise: 2 stars, optional

Show that the \idr{Empty_relation} that we defined earlier is a partial
function.

> --FILL IN HERE

$\square$

=== Reflexive Relations

A _reflexive_ relation on a set \idr{t} is one for which every element of
\idr{t} is related to itself.

> Reflexive : (r : Relation t) -> Type
> Reflexive {t} r = (a : t) -> r a a

> le_reflexive : Reflexive Le
> le_reflexive n = Le_n {n}

=== Transitive Relations

A relation \idr{r} is _transitive_ if \idr{r a c} holds whenever \idr{r a b} and
\idr{r b c} do.

> Transitive : (r : Relation t) -> Type
> Transitive {t} r = (a, b, c : t) -> r a b -> r b c -> r a c

> le_trans : Transitive Le
> le_trans _ _ _ lab Le_n = lab
> le_trans a b (S c) lab (Le_S lbc) = Le_S $ le_trans a b c lab lbc

> lt_trans : Transitive Lt
> lt_trans a b c lab lbc = le_trans (S a) (S b) c (Le_S lab) lbc

==== Exercise: 2 stars, optional

We can also prove \idr{lt_trans} more laboriously by induction, without using
\idr{le_trans}. Do this.

> lt_trans' : Transitive Lt
> -- Prove this by induction on evidence that a is less than c.
> lt_trans' a b c lab lbc = ?lt_trans__rhs

$\square$

==== Exercise: 2 stars, optional

\ \todo[inline]{Not sure how is this different from \idr{lt_trans'}?}

Prove the same thing again by induction on \idr{c}.

> lt_trans'' : Transitive Lt
> lt_trans'' a b c lab lbc = ?lt_trans___rhs

$\square$

The transitivity of \idr{Le}, in turn, can be used to prove some facts that will
be useful later (e.g., for the proof of antisymmetry below)...

> le_Sn_le : ((S n) <=' m) -> (n <=' m)
> le_Sn_le {n} {m} = le_trans n (S n) m (Le_S Le_n)

==== Exercise: 1 star, optional

> le_S_n : ((S n) <=' (S m)) -> (n <=' m)
> le_S_n less = ?le_S_n_rhs

$\square$

==== Exercise: 2 stars, optional (le_Sn_n_inf)

Provide an informal proof of the following theorem:

Theorem: For every \idr{n}, \idr{Not ((S n) <=' n)}

A formal proof of this is an optional exercise below, but try writing an
informal proof without doing the formal proof first.

Proof:

> -- FILL IN HERE

$\square$

==== Exercise: 1 star, optional

> le_Sn_n : Not ((S n) <=' n)
> le_Sn_n = ?le_Sn_n_rhs

$\square$

Reflexivity and transitivity are the main concepts we'll need for later
chapters, but, for a bit of additional practice working with relations in Idris,
let's look at a few other common ones...

=== Symmetric and Antisymmetric Relations

A relation \idr{r} is _symmetric_ if \idr{r a b} implies \idr{r b a}.

> Symmetric : (r : Relation t) -> Type
> Symmetric {t} r = (a, b : t) -> r a b -> r b a

==== Exercise: 2 stars, optional

> le_not_symmetric : Not (Symmetric Le)
> le_not_symmetric = ?le_not_symmetric_rhs

$\square$

A relation \idr{r} is _antisymmetric_ if \idr{r a b} and \idr{r b a} together
imply \idr{a = b} — that is, if the only "cycles" in \idr{r} are trivial ones.

> Antisymmetric : (r : Relation t) -> Type
> Antisymmetric {t} r = (a, b : t) -> r a b -> r b a -> a = b

==== Exercise: 2 stars, optional

> le_antisymmetric : Antisymmetric Le
> le_antisymmetric = ?le_antisymmetric_rhs

$\square$

==== Exercise: 2 stars, optional

> le_step : (n <' m) -> (m <=' (S p)) -> (n <=' p)
> le_step ltnm lemsp = ?le_step_rhs

$\square$

=== Equivalence Relations

A relation is an _equivalence_ if it's reflexive, symmetric, and transitive.

> Equivalence : (r : Relation t) -> Type
> Equivalence r = (Reflexive r, Symmetric r, Transitive r)

=== Partial Orders and Preorders

\ \todo[inline]{Edit}

A relation is a _partial order_ when it's reflexive, _anti_-symmetric, and
transitive. In the Idris standard library it's called just "order" for short.

> Order : (r : Relation t) -> Type
> Order r = (Reflexive r, Antisymmetric r, Transitive r)

A preorder is almost like a partial order, but doesn't have to be antisymmetric.

> Preorder : (r : Relation t) -> Type
> Preorder r = (Reflexive r, Transitive r)

> le_order : Order Le
> le_order = (le_reflexive, le_antisymmetric, le_trans)

== Reflexive, Transitive Closure

\ \todo[inline]{Edit}

The _reflexive, transitive closure_ of a relation \idr{r} is the smallest
relation that contains \idr{r} and that is both reflexive and transitive.
Formally, it is defined like this in the Relations module of the Idris standard
library:

> data Clos_refl_trans : (r : Relation t) -> Relation t where
>   Rt_step : r x y -> Clos_refl_trans r x y
>   Rt_refl : Clos_refl_trans r x x
>   Rt_trans : Clos_refl_trans r x y -> Clos_refl_trans r y z ->
>              Clos_refl_trans r x z

For example, the reflexive and transitive closure of the \idr{Next_nat} relation
coincides with the \idr{Le} relation.

> next_nat_closure_is_le : (n <=' m) <-> (Clos_refl_trans Next_nat n m)
> next_nat_closure_is_le = (to, fro)
>   where
>     to : Le n m -> Clos_refl_trans Next_nat n m
>     to Le_n = Rt_refl
>     to (Le_S {m} le) = Rt_trans {y=m} (to le) (Rt_step Nn)
>     fro : Clos_refl_trans Next_nat n m -> Le n m
>     fro (Rt_step Nn) = Le_S Le_n
>     fro Rt_refl = Le_n
>     fro (Rt_trans {x=n} {y} {z=m} ny ym) =
>       le_trans n y m (fro ny) (fro ym)

The above definition of reflexive, transitive closure is natural: it says,
explicitly, that the reflexive and transitive closure of \idr{r} is the least
relation that includes \idr{r} and that is closed under rules of reflexivity and
transitivity. But it turns out that this definition is not very convenient for
doing proofs, since the "nondeterminism" of the \idr{Rt_trans} rule can
sometimes lead to tricky inductions. Here is a more useful definition:

> data Clos_refl_trans_1n : (r : Relation t) -> (x : t) -> t -> Type where
>   Rt1n_refl : Clos_refl_trans_1n r x x
>   Rt1n_trans : r x y -> Clos_refl_trans_1n r y z -> Clos_refl_trans_1n r x z

\todo[inline]{Edit}

Our new definition of reflexive, transitive closure "bundles" the \idr{Rt_step}
and \idr{Rt_trans} rules into the single rule step. The left-hand premise of
this step is a single use of \idr{r}, leading to a much simpler induction
principle.

Before we go on, we should check that the two definitions do indeed define the
same relation...

First, we prove two lemmas showing that \idr{Clos_refl_trans_1n} mimics the
behavior of the two "missing" \idr{Clos_refl_trans} constructors.

> rsc_R : r x y -> Clos_refl_trans_1n r x y
> rsc_R rxy = Rt1n_trans rxy Rt1n_refl

==== Exercise: 2 stars, optional (rsc_trans)

> rsc_trans : Clos_refl_trans_1n r x y -> Clos_refl_trans_1n r y z ->
>             Clos_refl_trans_1n r x z
> rsc_trans crxy cryz = ?rsc_trans_rhs

$\square$

Then we use these facts to prove that the two definitions of reflexive,
transitive closure do indeed define the same relation.

==== Exercise: 3 stars, optional (rtc_rsc_coincide)

> rtc_rsc_coincide : (Clos_refl_trans r x y) <-> (Clos_refl_trans_1n r x y)
> rtc_rsc_coincide = ?rtc_rsc_coincide_rhs

$\square$

ext: lidr

max_stars_repo_name: diseraluca/software-foundations

max_issues_repo_name: diseraluca/software-foundations

max_forks_repo_name: diseraluca/software-foundations