text:
module Sub06LTE108t27

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total

-- 6(18t+4)+3 --CF[4,1,-2]--> 6(16t+3)+3
export
lte108t27 : (l : Nat) -> LTE (S (S (S (S (l+l+l+l)+(l+l+l+l)+(l+l+l+l)+(l+l+l+l)))))
  (S ((S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l))) + (S ((l+l+l)+(l+l+l)))))
lte108t27 Z     = (LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
lte108t27 (S l) =
  let lemma = lte108t27 l in

  rewrite (sym (plusSuccRightSucc l l)) in

  rewrite (sym (plusSuccRightSucc (plus l l) l)) in

  rewrite (sym (plusSuccRightSucc (plus (plus l l) l) l)) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) l)
                                  (S (S (S (plus (plus (plus l l) l) l)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) l)
                                     (S (S (plus (plus (plus l l) l) l))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) l)
                                        (S (plus (plus (plus l l) l) l)))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) l)
                                           (plus (plus (plus l l) l) l))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) l) (plus (plus (plus l l) l) l))
                                  (S (S (S (plus (plus (plus l l) l) l)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) l) (plus (plus (plus l l) l) l))
                                     (S (S (plus (plus (plus l l) l) l))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) l) (plus (plus (plus l l) l) l))
                                        (S (plus (plus (plus l l) l) l)))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) l) (plus (plus (plus l l) l) l))
                                           (plus (plus (plus l l) l) l))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus l l) l) l) (plus (plus (plus l l) l) l))
                                                                       (plus (plus (plus l l) l) l))
                                  (S (S (S (plus (plus (plus l l) l) l)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus l l) l) l) (plus (plus (plus l l) l) l))
                                                                       (plus (plus (plus l l) l) l))
                                     (S (S (plus (plus (plus l l) l) l))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus l l) l) l) (plus (plus (plus l l) l) l))
                                                                       (plus (plus (plus l l) l) l))
                                        (S (plus (plus (plus l l) l) l)))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus (plus l l) l) l) (plus (plus (plus l l) l) l))
                                                                       (plus (plus (plus l l) l) l))
                                           (plus (plus (plus l l) l) l))) in

  rewrite (sym (plusSuccRightSucc (plus (plus l l) l)
                                  (S (S (plus (plus l l) l))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus l l) l)
                                     (S (plus (plus l l) l)))) in
  rewrite (sym (plusSuccRightSucc (plus (plus l l) l)
                                        (plus (plus l l) l))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l))
                                  (S (S (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l)))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l))
                                     (S (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l))
                                        (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l)))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l))
                                           (S (S (S (plus (plus (plus l l) l) (plus (plus l l) l))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l))
                                              (S (S (plus (plus (plus l l) l) (plus (plus l l) l)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus l l) l) (plus (plus l l) l))
                                                 (S (plus (plus (plus l l) l) (plus (plus l l) l))))) in

  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                      (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                  (S (S (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l)
                                             l)))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                      (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                     (S (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l)
                                             l))))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                      (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                        (S (S (S (S (plus (plus (plus l l) l) (plus (plus l l)
                                             l)))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                      (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                           (S (S (S (plus (plus (plus l l) l) (plus (plus l l)
                                             l))))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                      (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                              (S (S (plus (plus (plus l l) l) (plus (plus l l)
                                             l)))))) in
  rewrite (sym (plusSuccRightSucc (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                      (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                                 (S (plus (plus (plus l l) l) (plus (plus l l)
                                             l))))) in

    (lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) lemma


text:
module Arduino.Util

import Data.Vect
import Data.Vect.Quantifiers

%default total

--------------------------------------------------------
--- Type-level massive disjunctions and conjunctions ---
--------------------------------------------------------

namespace Logic

  public export
  data OneOf : Vect n Type -> Type where
    MkOneOf : (idx : Fin n) -> index idx types -> OneOf types

  public export
  data AllOf : Vect n Type -> Type where
    Nil  :                               AllOf []
    (::) : {x : Type} -> x -> AllOf v -> AllOf (x::v)

  -- Curry-Howard coding of a short-circuiting conjunction
  public export
  data AndThen : (l : Type) -> (r : l -> Type) -> Type where
    ShortConj : (v : l) -> (w : r v) -> l `AndThen` r

  -- Short-circuting disjunction
  public export
  data OrElse : (l : Type) -> (r : (l -> Void) -> Type) -> Type where
    MkLeft  :                      (v : l)     -> l `OrElse` r
    MkRight : (noL : l -> Void) -> (w : r noL) -> l `OrElse` r

----------------------------------------------
--- Additional quantifiers for collections ---
----------------------------------------------

namespace Quantif

  public export
  data AllDiffer : Vect n a -> Type where
    Nil  : AllDiffer []
    (::) : {xs : Vect n a} -> (x : a) -> {auto ev : All (Not . \u => u = x) xs} -> AllDiffer xs -> AllDiffer (x::xs)

----------------------------------
--- "Easier constructor" stuff ---
----------------------------------

-- Dependent pair `(x : a ** guarantee x)` with `auto` `guarantee` parameter in constructor.
public export
data That : (a : Type) -> (a -> Type) -> Type where
  Bounded : (x : a) -> {auto ev : prop x} -> a `That` prop

public export
Debounded : a `That` prop -> a
Debounded (Bounded x) = x

public export
SummonAuto : {auto a : t} -> t
SummonAuto {a} = a

-------------------
--- Combinators ---
-------------------

infixr 9 ..., ....

-- Beloved "blackbird" combinator
public export
%inline
(...) : (c -> d) -> (a -> b -> c) -> a -> b -> d
(...) = (.) . (.)

public export
%inline
(....) : (d -> e) -> (a -> b -> c -> d) -> a -> b -> c -> e
(....) = (.) . (...)

--- Functor stuff ---

public export
unit : Functor f => f a -> f ()
unit = map $ const ()

ext: idr

max_stars_repo_name: buzden/idris-arduino-lib

max_issues_repo_name: buzden/idris-arduino-lib

max_forks_repo_name: buzden/idris-arduino-lib


text:
import Data.Vect

append : (elem : Type) -> (n : Nat) -> (m : Nat) ->
         Vect n elem -> Vect m elem -> Vect (n + m) elem
append elem Z m [] ys = ys
append elem (S k) m (x :: xs) ys = x :: append elem k m xs ys

createEmpties : Vect n (Vect 0 a)
createEmpties {n = Z} = []
createEmpties {n = (S k)} = [] :: createEmpties


text:
module Processor

import Hardware

incPC : Memory -> Memory
incPC m = updtRD PC (1 + toRD PC m) m

getInstruction : Int -> Memory -> Instruction
getInstruction 0 (MkMemory regs' (instr :: asm')) = instr
getInstruction i (MkMemory regs' (instr :: asm'))
  = getInstruction (i - 1) (MkMemory regs' asm')

outOfBounds : Int -> Memory -> Bool
outOfBounds i (MkMemory regs' instrs) = cast i >= length instrs

export
evaluator : Memory -> Memory
evaluator mem = if outOfBounds (pc $ regs mem) mem then mem else
                  case getInstruction (pc $ regs mem) mem of
  ADD r r' r'' => evaluator $ incPC $ (updtRD r ((toRD r' mem) + (toRD r'' mem)) mem)
  -- SHA3    : Register -> Register -> ISA
  ADDRESS r => evaluator $ incPC mem -- todo
  LOAD r r' => evaluator $ incPC mem -- todo
  JUMPI r i => evaluator $ updtRD PC ((if (toRD r mem) == 0 then 1 else i) + toRD PC mem) mem
  EQUAL r r' r'' => evaluator $ incPC $ updtRD r (if (toRD r' mem) == (toRD r'' mem) then 1 else 0) mem
  NOT r r' => evaluator $ incPC $ updtRD r (if (toRD r' mem) == 0 then 1 else 0) mem
  STOP => mem -- todo
  DATA i => mem -- todo

max_stars_repo_name: nickgeoca/QVM

max_issues_repo_name: nickgeoca/QVM

max_forks_repo_name: nickgeoca/QVM


text:
import Aoc
import Data.List
import Data.List1
import Data.Stream
import Data.Strings
%default total

||| Give integers a short name.
Z : Type
Z = Integer

||| A residue class: (k, m) represents all integers ≡ k mod m.
RC : Type
RC = (Z, Z)

||| "Actual" modulo, with (-1) %% 5 == 4
(%%) : Z -> Z -> Z
(%%) a b = ((a `mod` b) + b) `mod` b
infixl 15 %%

||| What's the smallest integer ≥n that's ≡k (mod m)?
nextInRC : RC -> Z -> Z
nextInRC (k, m) n = n + ((k-n) %% m)

||| Given (a,b), compute (g,s,t) so that a*s + b*t = g = gcd(a,b).
partial
egcd : Z -> Z -> (Z, Z, Z)
egcd 0 b = (b, 0, 1)
egcd a b = let (g, s, t) = egcd (b %% a) a in (g, t - s * div b a, s)

||| Try to compute the modular inverse of a (mod m).
inv : Z -> Z -> Maybe Z
inv a m =
  case egcd a m of
    (1, s, _) => Just (s %% m)
    _ => Nothing

||| Try to intersect two RCs into a new RC, with the Chinese remainder theorem.
||| This will only work if m1 and m2 are coprime. But it's ok, because the input is all coprime numbers! Even though this is nowhere specified. So, did I really "solve the puzzle" or overfit and cheat?? merry christmas
crt : RC -> RC -> Maybe RC
crt (k1, m1) (k2, m2) = do
  i <- inv m2 m1
  let k = k2 + m2 * (k1 - k2) * i
  let m = m1 * m2
  pure (k %% m, m)

||| A wait time and bus number for a bus-taking decision.
record TakeBus where
  constructor mkTakeBus
  waitTime : Integer
  bus : Integer

||| Take the first available bus from a list starting at `time`.
partial
takeBusFrom : (buses : List1 Integer) -> (time : Integer) -> TakeBus
takeBusFrom buses time =
  let options = map (\b => mkTakeBus (nextInRC (0, b) time - time) b) buses
  in minimumBy (.waitTime) options

main : IO ()
main = do
  Just time <- parseInteger <$> getLine
    | Nothing => putStrLn "couldn't parse timestamp"
  buses <- map parseInteger . toList . split (==',') <$> getLine
  Just available <- pure $ Data.List1.fromList (catMaybes buses)
    | Nothing => putStrLn "no available buses"

  putStr "*   "
  let result = takeBusFrom available time
  printLn $ result.bus * result.waitTime

  putStr "**  "
  let buses' = mapMaybe (\(i,b) => map (-i,) b) $ enumerate buses
  Just (k, m) <- pure (foldlM crt (0,1) buses')
    | Nothing => putStrLn "bus numbers not coprime"
  printLn k


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

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

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

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

-- Exercise 1

showOp : Show a => String -> a -> a -> String
showOp op x y = "(" ++ show x ++ op ++ show y ++ ")"

Show ty => Show (Expr ty) where
    show (Val x) = show x
    show (Add x y) = showOp " + " x y
    show (Sub x y) = showOp " - " x y
    show (Mul x y) = showOp " * " x y
    show (Div x y) = showOp " / " x y
    show (Abs x) = "abs " ++ show x

-- Exercise 2

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

-- Exercise 3

(Neg num, Integral num) => Cast (Expr num) num where
    cast orig = eval orig


text:
||| For Plain Merge we need to assert that all branches in a choice are the same.
module Sessions.Local.Same.All

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

import Data.List1

import Sessions.Meta
import Sessions.Local
import Sessions.Local.Same

%default total

namespace List
  public export
  data All : (c  : Branch    role local msg rs g)
          -> (cs : Branches' role local msg rs g)
          -> (ne : NonEmpty cs)
                -> Type
    where
      Base : (prf : Equal c d)
                 -> All c (d :: Nil) IsNonEmpty

      Extend : (prf   : Equal c d)
            -> (prfNE : NonEmpty rest)
            -> (later : All c     rest  prfNE)
                     -> All c (d::rest) IsNonEmpty

  notEmpty : NonEmpty [] -> Void
  notEmpty IsNonEmpty impossible

  nonEmpty : (xs : List a) -> Dec (NonEmpty xs)
  nonEmpty [] = No notEmpty
  nonEmpty (x :: xs) = Yes IsNonEmpty

  data Shape : (xs : List a) -> Type where
    IsCons : Shape (x::xs)
    IsNil  : Shape Nil

  shape : (xs : List a) -> Shape xs
  shape [] = IsNil
  shape (x :: xs) = IsCons

  notSameHead : (c = x -> Void)
             -> All c (x :: xs) IsNonEmpty -> Void
  notSameHead f (Base prf) = f prf
  notSameHead f (Extend prf prfNE later) = f prf

  notSameRest : (All x (y :: xs) IsNonEmpty -> Void)
              -> All x (x :: (y :: xs)) IsNonEmpty
              -> Void
  notSameRest f (Extend Refl IsNonEmpty later) = f later

  export
  allSame : DecEq role label msg
         => (c     : Branch    role label msg rs g)
         -> (cs    : Branches' role label msg rs g)
         -> (prfNE : NonEmpty cs)
                  -> Dec (All c cs prfNE)
  allSame c (x :: xs) IsNonEmpty with (same c x)
    allSame x (x :: xs) IsNonEmpty | (Yes Refl) with (shape xs)
      allSame x (x :: (y :: xs)) IsNonEmpty | (Yes Refl) | IsCons with (allSame x (y::xs) IsNonEmpty)
        allSame x (x :: (y :: xs)) IsNonEmpty | (Yes Refl) | IsCons | (Yes prf) = Yes (Extend Refl IsNonEmpty prf)
        allSame x (x :: (y :: xs)) IsNonEmpty | (Yes Refl) | IsCons | (No contra)
          = No (notSameRest contra)
      allSame x (x :: []) IsNonEmpty | (Yes Refl) | IsNil
        = Yes (Base Refl)

    allSame c (x :: xs) IsNonEmpty | (No contra)
      = No (notSameHead contra)

namespace List1
  public export
  data All : (cs : Branches role label msg rs g)
              -> Type
    where
      Yes : All c (c::cs) IsNonEmpty -> All (c ::: cs)

  notAllSame : (All h (h :: t) IsNonEmpty -> Void) -> All (h ::: t) -> Void
  notAllSame f (Yes x) = f x

  export
  allSame : DecEq role label msg
         => (cs : Branches role label msg rs g)
               -> Dec (All cs)
  allSame (head ::: tail) with (allSame head (head :: tail) IsNonEmpty)
    allSame (head ::: tail) | (Yes prf) = Yes (Yes prf)
    allSame (head ::: tail) | (No contra)
      = No (notAllSame contra)

-- [ EOF ]

max_stars_repo_name: DSbD-AppControl/sessions-playground

max_issues_repo_name: DSbD-AppControl/sessions-playground

max_forks_repo_name: DSbD-AppControl/sessions-playground


text:
module Utils

import LispVal
import Data.Vect

%access public export

mapLeft : (a -> c) -> Either a b -> Either c b
mapLeft f = mirror . (map f) . mirror

toVect2Maybe : List LispVal -> Maybe (Vect 2 LispVal)
toVect2Maybe [x, y] = Just (fromList [x, y])
toVect2Maybe _      = Nothing

toVect2 : List LispVal -> Either LispError (Vect 2 LispVal)
toVect2 ls = maybeToEither (NumArgs 2 ls) (toVect2Maybe ls)


text:
||| Specialized implementation of an interval map with finger trees [1].
||| This data structure is meant to get efficiently data with a correlated NonEmptyFC.
||| The element data type must implement the `Measure` interface. An implementation
||| is provided already for NonEmptyFC and tuples with NonEmptyFC as first element.
|||
||| [1] https://www.staff.city.ac.uk/~ross/papers/FingerTree.pdf
module Libraries.Data.PosMap

import Core.FC

import Data.List

%default total

infixr 5 <|, <:
infixl 5 |>, :>

public export
FileRange : Type
FileRange = (FilePos, FilePos)

||| Type for rightmost intervals, ordered by their low endpoints and annotated
||| with the maximum of the high endpoints.
data RMFileRange = MkRange FileRange FilePos

Eq RMFileRange where
  (MkRange low high) == (MkRange low' high') = low == low' && high == high'

Show RMFileRange where
  showPrec p (MkRange low high) = showCon p "MkRange" $ showArg low ++ showArg high

Semigroup RMFileRange where
  -- The semigroup operation on righmost intervals is the composition of two
  -- monoids applied to each component:
  -- 1) the operation on low endpoints always returns the last key it contains,
  --    assuming the keys are ordered (enforced by the insertion function), the
  --    FingerTree behaves as a store of ordered sequences, with measures
  --    serving as signpost keys.
  -- 2) the operation on high endpoints returns the maximum of the endpoints,
  --    thus the FingerTree behaves as a max-priority queue.
  (MkRange low high) <+> (MkRange low' high') = MkRange low' (max high high')

data Interval = MkInterval RMFileRange | NoInterval

Eq Interval where
  (MkInterval range) == (MkInterval range') = range == range'
  NoInterval == NoInterval = True
  _ == _ = False

Show Interval where
  showPrec p (MkInterval range) = showCon p "MkInterval" $ showArg range
  showPrec p NoInterval = "NoInterval"

Semigroup Interval where
  NoInterval <+> i = i
  i <+> NoInterval = i
  (MkInterval range) <+> (MkInterval range') = MkInterval (range <+> range')

Monoid Interval where
  neutral = NoInterval

Cast FileRange RMFileRange where
  cast (l, h) = MkRange (l, h) h

Cast FileRange Interval where
  cast (l, h) = MkInterval (MkRange (l, h) h)

Cast RMFileRange Interval where
  cast = MkInterval

||| Things that have an associated interval in the source files.
public export
interface Measure a where
  measure : a -> FileRange

interface MeasureRM a where
  measureRM : a -> RMFileRange

public export
Measure a => MeasureRM a where
  measureRM = cast . measure

measureInterval : Measure a => a -> Interval
measureInterval = cast . measure

data Digit : Type -> Type where
  One : a -> Digit a
  Two : a -> a -> Digit a
  Three : a -> a -> a -> Digit a
  Four : a -> a -> a -> a -> Digit a

Eq a => Eq (Digit a) where
  (One x) == (One x') = x == x'
  (Two x y) == (Two x' y') = x == x' && y == y'
  (Three x y z) == (Three x' y' z') = x == x' && y == y' && z == z'
  (Four x y z w) == (Four x' y' z' w') = x == x' && y == y' && z == z' && w == w'
  _ == _ = False

Show a => Show (Digit a) where
  showPrec p (One x) = showCon p "One" $ showArg x
  showPrec p (Two x y) = showCon p "Two" $ showArg x ++ showArg y
  showPrec p (Three x y z) = showCon p "Three" $ showArg x ++ showArg y ++ showArg z
  showPrec p (Four x y z w) = showCon p "Four" $ showArg x ++ showArg y ++ showArg z ++ showArg w

Functor Digit where
  map f (One x) = One (f x)
  map f (Two x y) = Two (f x) (f y)
  map f (Three x y z) = Three (f x) (f y) (f z)
  map f (Four x y z w) = Four (f x) (f y) (f z) (f w)

Foldable Digit where
  foldr f init (One a) = f a init
  foldr f init (Two a b) = f a (f b init)
  foldr f init (Three a b c) = f a (f b (f c init))
  foldr f init (Four a b c d) = f a (f b (f c (f d init)))

  foldl f init (One a) = f init a
  foldl f init (Two a b) = f (f init a) b
  foldl f init (Three a b c) = f (f (f init a) b) c
  foldl f init (Four a b c d) = f (f (f (f init a) b) c) d

  null _ = False

Traversable Digit where
  traverse f (One x) = [| One (f x) |]
  traverse f (Two x y) = [| Two (f x) (f y) |]
  traverse f (Three x y z) = [| Three (f x) (f y) (f z) |]
  traverse f (Four x y z w) = [| Four (f x) (f y) (f z) (f w) |]

MeasureRM a => MeasureRM (Digit a) where
  measureRM (One x) = measureRM x
  measureRM (Two x y) = measureRM x <+> measureRM y
  measureRM (Three x y z) = measureRM x <+> measureRM y <+> measureRM z
  measureRM (Four x y z w) = measureRM x <+> measureRM y <+> measureRM z <+> measureRM w

data Node : Type -> Type where
  Node2 : RMFileRange -> a -> a -> Node a
  Node3 : RMFileRange -> a -> a -> a -> Node a

node2 : MeasureRM a => a -> a -> Node a
node2 x y = Node2 (measureRM x <+> measureRM y) x y

node3 : MeasureRM a => a -> a -> a -> Node a
node3 x y z = Node3 (measureRM x <+> measureRM y <+> measureRM z) x y z

Foldable Node where
  foldr f init (Node2 _ x y) = f x (f y init)
  foldr f init (Node3 _ x y z) = f x (f y (f z init))

  foldl f init (Node2 v a b) = f (f init a) b
  foldl f init (Node3 v a b c) = f (f (f init a) b) c

MeasureRM (Node a) where
  measureRM (Node2 v {}) = v
  measureRM (Node3 v {}) = v

namespace Node
  export
  map : MeasureRM b => (a -> b) -> Node a -> Node b
  map f (Node2 _ x y) = node2 (f x) (f y)
  map f (Node3 _ x y z) = node3 (f x) (f y) (f z)

  export
  traverse : (Applicative f, MeasureRM b) => (a -> f b) -> Node a -> f (Node b)
  traverse f (Node2 _ x y) = [| node2 (f x) (f y) |]
  traverse f (Node3 _ x y z) = [| node3 (f x) (f y) (f z) |]

nodeToDigit : MeasureRM a => Node a -> Digit a
nodeToDigit (Node2 _ x y) = Two x y
nodeToDigit (Node3 _ x y z) = Three x y z

export
data PosMap : Type -> Type where
  Empty : PosMap a
  Single : a -> PosMap a
  Deep : RMFileRange -> Digit a -> PosMap (Node a) -> Digit a -> PosMap a

measureTree : MeasureRM a => PosMap a -> Interval
measureTree Empty = neutral
measureTree (Single x) = cast (measureRM x)
measureTree (Deep v {}) = cast v

addIntervalRight : RMFileRange -> Interval -> RMFileRange
addIntervalRight range (MkInterval range') = range <+> range'
addIntervalRight range NoInterval = range

addIntervalLeft : Interval -> RMFileRange -> RMFileRange
addIntervalLeft (MkInterval range) range' = range <+> range'
addIntervalLeft NoInterval range' = range'

deep : MeasureRM a => Digit a -> PosMap (Node a) -> Digit a -> PosMap a
deep pr t sf = Deep value pr t sf
  where value : RMFileRange
        value = case measureTree t of
                     MkInterval range => measureRM pr <+> range <+> measureRM sf
                     NoInterval => measureRM pr <+> measureRM sf

digitToTree : MeasureRM a => Digit a -> PosMap a
digitToTree (One a) = Single a
digitToTree (Two a b) = deep (One a) Empty (One b)
digitToTree (Three a b c) = deep (Two a b) Empty (One c)
digitToTree (Four a b c d) = deep (Two a b) Empty (Two c d)

(<|) : MeasureRM a => a -> PosMap a -> PosMap a
a <| Empty                        = Single a
a <| (Single b)                   = deep (One a) Empty (One b)
a <| (Deep _ (One b) m sf)        = deep (Two a b) m sf
a <| (Deep _ (Two b c) m sf)      = deep (Three a b c) m sf
a <| (Deep _ (Three b c d) m sf)  = deep (Four a b c d) m sf
a <| (Deep _ (Four b c d e) m sf) = deep (Two a b) (node3 c d e <| m) sf

(|>) : MeasureRM a => PosMap a -> a -> PosMap a
Empty                        |> a = Single a
(Single b)                   |> a = deep (One b) Empty (One a)
(Deep _ pr m (One b))        |> a = deep pr m (Two b a)
(Deep _ pr m (Two c b))      |> a = deep pr m (Three c b a)
(Deep _ pr m (Three d c b))  |> a = deep pr m (Four d c b a)
(Deep _ pr m (Four e d c b)) |> a = deep pr (m |> node3 e d c) (Two b a)

export
Foldable PosMap where
  foldr f init Empty = init
  foldr f init (Single x) = f x init
  foldr f init (Deep _ pr m sf) = foldr f (foldr (flip (foldr f)) (foldr f init sf) m) pr

  foldl f init Empty = init
  foldl f init (Single x) = f init x
  foldl f init (Deep _ pr m sf) = foldl f (foldl (foldl f) (foldl f init pr) m) sf

  null Empty = True
  null (Single {}) = False
  null (Deep {}) = False

export
empty : PosMap a
empty = Empty

export
singleton : a -> PosMap a
singleton x = Single x

toTree : (Foldable f, MeasureRM a) => f a -> PosMap a
toTree xs = foldr (<|) empty xs

data ViewL : Type -> Type where
  EmptyL : ViewL a
  (<:) : a -> PosMap a -> ViewL a

rotl : MeasureRM a => PosMap (Node a) -> Digit a -> PosMap a
viewl : MeasureRM a => PosMap a -> ViewL a

rotl t sf =
  case viewl t of
       EmptyL => digitToTree sf
       a <: t' => case measureTree t of
                       MkInterval range => Deep (range <+> measureRM sf) (nodeToDigit a) t' sf
                       NoInterval => Deep (measureRM sf) (nodeToDigit a) t' sf

viewl Empty = EmptyL
viewl (Single x) = x <: Empty
viewl (Deep _ (One x) t sf) = x <: rotl t sf
viewl (Deep _ (Two x y) t sf) = x <: deep (One y) t sf
viewl (Deep _ (Three x y z) t sf) = x <: deep (Two y z) t sf
viewl (Deep _ (Four x y z w) t sf) = x <: deep (Three y z w) t sf

data ViewR : Type -> Type where
  EmptyR : ViewR a
  (:>) : PosMap a -> a -> ViewR a

rotr : MeasureRM a => Digit a -> PosMap (Node a) -> PosMap a
viewr : MeasureRM a => PosMap a -> ViewR a

rotr pr t =
  case viewr t of
       EmptyR => digitToTree pr
       t' :> a => case measureTree t of
                       MkInterval range => Deep (measureRM pr <+> range) pr t' (nodeToDigit a)
                       NoInterval => Deep (measureRM pr) pr t' (nodeToDigit a)

viewr Empty = EmptyR
viewr (Single x) = Empty :> x
viewr (Deep _ pr t (One x)) = rotr pr t :> x
viewr (Deep _ pr t (Two x y)) = deep pr t (One x) :> y
viewr (Deep _ pr t (Three x y z)) = deep pr t (Two x y) :> z
viewr (Deep _ pr t (Four x y z w)) = deep pr t (Three x y z) :> w

appendTree0 : MeasureRM a => PosMap a -> PosMap a -> PosMap a
appendTree1 : MeasureRM a => PosMap a -> a -> PosMap a -> PosMap a
appendTree2 : MeasureRM a => PosMap a -> a -> a -> PosMap a -> PosMap a
appendTree3 : MeasureRM a => PosMap a -> a -> a -> a -> PosMap a -> PosMap a
appendTree4 : MeasureRM a => PosMap a -> a -> a -> a -> a -> PosMap a -> PosMap a
addDigits0  : MeasureRM a => PosMap (Node a) -> Digit a -> Digit a -> PosMap (Node a) -> PosMap (Node a)
addDigits1  : MeasureRM a => PosMap (Node a) -> Digit a -> a -> Digit a -> PosMap (Node a) -> PosMap (Node a)
addDigits2  : MeasureRM a => PosMap (Node a) -> Digit a -> a -> a -> Digit a -> PosMap (Node a) -> PosMap (Node a)
addDigits3  : MeasureRM a => PosMap (Node a) -> Digit a -> a -> a -> a -> Digit a -> PosMap (Node a) -> PosMap (Node a)
addDigits4  : MeasureRM a => PosMap (Node a) -> Digit a -> a -> a -> a -> a -> Digit a -> PosMap (Node a) -> PosMap (Node a)

appendTree0 Empty xs = xs
appendTree0 xs Empty = xs
appendTree0 (Single x) xs = x <| xs
appendTree0 xs (Single x) = xs |> x
appendTree0 (Deep _ pr1 t1 sf1) (Deep _ pr2 t2 sf2) = deep pr1 (addDigits0 t1 sf1 pr2 t2) sf2

appendTree1 Empty a xs = a <| xs
appendTree1 xs a Empty = xs |> a
appendTree1 (Single x) a xs = x <| a <| xs
appendTree1 xs a (Single x) = xs |> a |> x
appendTree1 (Deep _ pr1 t1 sf1) a (Deep _ pr2 t2 sf2) = deep pr1 (addDigits1 t1 sf1 a pr2 t2) sf2

appendTree2 Empty a b xs = a <| b <| xs
appendTree2 xs a b Empty = xs |> a |> b
appendTree2 (Single x) a b xs = x <| a <| b <| xs
appendTree2 xs a b (Single x) = xs |> a |> b |> x
appendTree2 (Deep _ pr1 t1 sf1) a b (Deep _ pr2 t2 sf2) = deep pr1 (addDigits2 t1 sf1 a b pr2 t2) sf2

appendTree3 Empty a b c xs = a <| b <| c <| xs
appendTree3 xs a b c Empty = xs |> a |> b |> c
appendTree3 (Single x) a b c xs = x <| a <| b <| c <| xs
appendTree3 xs a b c (Single x) = xs |> a |> b |> c |> x
appendTree3 (Deep _ pr1 t1 sf1) a b c (Deep _ pr2 t2 sf2) = deep pr1 (addDigits3 t1 sf1 a b c pr2 t2) sf2

appendTree4 Empty a b c d xs = a <| b <| c <| d <| xs
appendTree4 xs a b c d Empty = xs |> a |> b |> c |> d
appendTree4 (Single x) a b c d xs = a <| b <| c <| d <| x <| xs
appendTree4 xs a b c d (Single x) = xs |> a |> b |> c |> d |> x
appendTree4 (Deep _ pr1 m1 sf1) a b c d (Deep _ pr2 m2 sf2) = deep pr1 (addDigits4 m1 sf1 a b c d pr2 m2) sf2

addDigits0 t1 (One a)        (One b)        t2 = appendTree1 t1 (node2 a b) t2
addDigits0 t1 (One a)        (Two b c)      t2 = appendTree1 t1 (node3 a b c) t2
addDigits0 t1 (One a)        (Three b c d)  t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
addDigits0 t1 (One a)        (Four b c d e) t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
addDigits0 t1 (Two a b)      (One c)        t2 = appendTree1 t1 (node3 a b c) t2
addDigits0 t1 (Two a b)      (Two c d)      t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
addDigits0 t1 (Two a b)      (Three c d e)  t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
addDigits0 t1 (Two a b)      (Four c d e f) t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits0 t1 (Three a b c)  (One d)        t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
addDigits0 t1 (Three a b c)  (Two d e)      t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
addDigits0 t1 (Three a b c)  (Three d e f)  t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits0 t1 (Three a b c)  (Four d e f g) t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits0 t1 (Four a b c d) (One e)        t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
addDigits0 t1 (Four a b c d) (Two e f)      t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits0 t1 (Four a b c d) (Three e f g)  t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits0 t1 (Four a b c d) (Four e f g h) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2

addDigits1 t1 (One a)        b (One c)        t2 = appendTree1 t1 (node3 a b c) t2
addDigits1 t1 (One a)        b (Two c d)      t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
addDigits1 t1 (One a)        b (Three c d e)  t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
addDigits1 t1 (One a)        b (Four c d e f) t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits1 t1 (Two a b)      c (One d)        t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
addDigits1 t1 (Two a b)      c (Two d e)      t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
addDigits1 t1 (Two a b)      c (Three d e f)  t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits1 t1 (Two a b)      c (Four d e f g) t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits1 t1 (Three a b c)  d (One e)        t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
addDigits1 t1 (Three a b c)  d (Two e f)      t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits1 t1 (Three a b c)  d (Three e f g)  t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits1 t1 (Three a b c)  d (Four e f g h) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits1 t1 (Four a b c d) e (One f)        t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits1 t1 (Four a b c d) e (Two f g)      t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits1 t1 (Four a b c d) e (Three f g h)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits1 t1 (Four a b c d) e (Four f g h i) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2

addDigits2 t1 (One a)        b c (One d)        t2 = appendTree2 t1 (node2 a b) (node2 c d) t2
addDigits2 t1 (One a)        b c (Two d e)      t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
addDigits2 t1 (One a)        b c (Three d e f)  t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits2 t1 (One a)        b c (Four d e f g) t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits2 t1 (Two a b)      c d (One e)        t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
addDigits2 t1 (Two a b)      c d (Two e f)      t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits2 t1 (Two a b)      c d (Three e f g)  t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits2 t1 (Two a b)      c d (Four e f g h) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits2 t1 (Three a b c)  d e (One f)        t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits2 t1 (Three a b c)  d e (Two f g)      t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits2 t1 (Three a b c)  d e (Three f g h)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits2 t1 (Three a b c)  d e (Four f g h i) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
addDigits2 t1 (Four a b c d) e f (One g)        t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits2 t1 (Four a b c d) e f (Two g h)      t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits2 t1 (Four a b c d) e f (Three g h i)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
addDigits2 t1 (Four a b c d) e f (Four g h i j) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2

addDigits3 t1 (One a)        b c d (One e)        t2 = appendTree2 t1 (node3 a b c) (node2 d e) t2
addDigits3 t1 (One a)        b c d (Two e f)      t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits3 t1 (One a)        b c d (Three e f g)  t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits3 t1 (One a)        b c d (Four e f g h) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits3 t1 (Two a b)      c d e (One f)        t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits3 t1 (Two a b)      c d e (Two f g)      t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits3 t1 (Two a b)      c d e (Three f g h)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits3 t1 (Two a b)      c d e (Four f g h i) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
addDigits3 t1 (Three a b c)  d e f (One g)        t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits3 t1 (Three a b c)  d e f (Two g h)      t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits3 t1 (Three a b c)  d e f (Three g h i)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
addDigits3 t1 (Three a b c)  d e f (Four g h i j) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2
addDigits3 t1 (Four a b c d) e f g (One h)        t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits3 t1 (Four a b c d) e f g (Two h i)      t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
addDigits3 t1 (Four a b c d) e f g (Three h i j)  t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2
addDigits3 t1 (Four a b c d) e f g (Four h i j k) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) t2

addDigits4 t1 (One a)        b c d e (One f)        t2 = appendTree2 t1 (node3 a b c) (node3 d e f) t2
addDigits4 t1 (One a)        b c d e (Two f g)      t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits4 t1 (One a)        b c d e (Three f g h)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits4 t1 (One a)        b c d e (Four f g h i) t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
addDigits4 t1 (Two a b)      c d e f (One g)        t2 = appendTree3 t1 (node3 a b c) (node2 d e) (node2 f g) t2
addDigits4 t1 (Two a b)      c d e f (Two g h)      t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits4 t1 (Two a b)      c d e f (Three g h i)  t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
addDigits4 t1 (Two a b)      c d e f (Four g h i j) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2
addDigits4 t1 (Three a b c)  d e f g (One h)        t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node2 g h) t2
addDigits4 t1 (Three a b c)  d e f g (Two h i)      t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
addDigits4 t1 (Three a b c)  d e f g (Three h i j)  t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2
addDigits4 t1 (Three a b c)  d e f g (Four h i j k) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) t2
addDigits4 t1 (Four a b c d) e f g h (One i)        t2 = appendTree3 t1 (node3 a b c) (node3 d e f) (node3 g h i) t2
addDigits4 t1 (Four a b c d) e f g h (Two i j)      t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node2 g h) (node2 i j) t2
addDigits4 t1 (Four a b c d) e f g h (Three i j k)  t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node3 g h i) (node2 j k) t2
addDigits4 t1 (Four a b c d) e f g h (Four i j k l) t2 = appendTree4 t1 (node3 a b c) (node3 d e f) (node3 g h i) (node3 j k l) t2

Split : Type -> Type -> Type
Split t a = (t, a, t)

data SearchResult : Type -> Type where
  Position : PosMap a -> a -> PosMap a -> SearchResult a
  OnLeft : SearchResult a
  OnRight : SearchResult a
  Nowhere : SearchResult a

searchDigit : MeasureRM a => (Interval -> Interval -> Bool) -> Interval -> Digit a -> Interval -> Split (Maybe (Digit a)) a
searchDigit p vl (One a) vr = (Nothing, a, Nothing)
searchDigit p vl (Two a b) vr =
  let va = vl <+> cast (measureRM a)
      vb = cast (measureRM b) <+> vr in
      if p va vb
         then (Nothing, a, Just (One b))
         else (Just (One a), b, Nothing)
searchDigit p vl (Three a b c) vr =
  let va  = vl <+> cast (measureRM a)
      vab = va <+> cast (measureRM b)
      vc  = cast (measureRM c) <+> vr
      vbc = cast (measureRM b) <+> vc in
      if p va vbc
         then (Nothing, a, Just (Two b c))
         else if p vab vc
                 then (Just (One a), b, Just (One c))
                 else (Just (Two a b), c, Nothing)
searchDigit p vl (Four a b c d) vr =
  let va   = vl <+> cast (measureRM a)
      vab  = va <+> cast (measureRM b)
      vabc = vab <+> cast (measureRM c)
      vd   = cast (measureRM d) <+> vr
      vcd  = cast (measureRM c) <+> vd
      vbcd = cast (measureRM b) <+> vcd in
      if p va vbcd
         then (Nothing, a, Just (Three b c d))
         else if p vab vcd
                 then (Just (One a), b, Just (Two c d))
                 else if p vabc vd
                         then (Just (Two a b), c, Just (One d))
                         else (Just (Three a b c), d, Nothing)

deepl : MeasureRM a => Maybe (Digit a) -> PosMap (Node a) -> Digit a -> PosMap a
deepl Nothing m sf = rotl m sf
deepl (Just pr) m sf = deep pr m sf

deepr : MeasureRM a => Digit a -> PosMap (Node a) -> Maybe (Digit a) -> PosMap a
deepr pr m Nothing = rotr pr m
deepr pr m (Just sf) = deep pr m sf

searchNode : MeasureRM a => (Interval -> Interval -> Bool) -> Interval -> Node a -> Interval -> Split (Maybe (Digit a)) a
searchNode p vl x vr = searchDigit p vl (nodeToDigit x) vr

searchTree : MeasureRM a => (Interval -> Interval -> Bool) -> Interval -> PosMap a -> Interval -> Maybe (Split (PosMap a) a)
searchTree p vl Empty vr = Nothing
searchTree p vl (Single x) vr = Just (Empty, x, Empty)
searchTree p vl (Deep _ pr m sf) vr =
  let vm   = measureTree m
      vsr  = cast (measureRM sf) <+> vr
      vmsr = vm <+> vsr
      vlp  = vl <+> cast (measureRM pr)
      vlpm = vlp <+> vm in
      if p vlp vmsr
         then let (l, x, r) = searchDigit p vl pr vmsr in
                  Just (maybe Empty digitToTree l, x, deepl r m sf)
         else if p vlpm vsr
                 then do (ml, xs, mr) <- searchTree p vlp m vsr
                         let (l, x, r) = searchNode p (vlp <+> measureTree ml) xs (measureTree mr <+> vsr)
                         Just (deepr pr ml l, x, deepl r mr sf)
                 else let (l, x, r) = searchDigit p vlpm sf vr in
                          Just (deepr pr m l, x, maybe Empty digitToTree r)

search' : MeasureRM a => (Interval -> Interval -> Bool) -> PosMap a -> SearchResult a
search' p t =
  let vt     = measureTree t
      pLeft  = p neutral vt
      pRight = p vt neutral in
      case (pLeft, pRight) of
           (True,  True)  => OnLeft
           (False, True)  => case searchTree p neutral t neutral of
                                  Just (l, x, r) => Position l x r
                                  Nothing => Nowhere
           (False, False) => OnRight
           (True,  False) => Nowhere

split : MeasureRM a => (Interval -> Bool) -> PosMap a -> (PosMap a, PosMap a)
split p Empty = (Empty, Empty)
split p xs =
  case searchTree (\a, _ => p a) neutral xs neutral of
       Just (l, x, r) => if p (measureTree xs)
                            then (l, x <| r)
                            else (xs, Empty)
       Nothing => (xs, Empty)

(++) : MeasureRM a => PosMap a -> PosMap a -> PosMap a
xs ++ ys = appendTree0 xs ys

export
map : MeasureRM b => (a -> b) -> PosMap a -> PosMap b
map f Empty = Empty
map f (Single x) = Single (f x)
map f (Deep _ pr t sf) = deep (map f pr) (map (map f) t) (map f sf)

export
traverse : (Applicative f, MeasureRM b) => (a -> f b) -> PosMap a -> f (PosMap b)
traverse f Empty = [| Empty |]
traverse f (Single x) = [| Single (f x) |]
traverse f (Deep _ pr t sf) = [| deep (traverse f pr) (traverse (traverse f) t) (traverse f sf) |]

export
takeUntil : MeasureRM a => (Interval -> Bool) -> PosMap a -> PosMap a
takeUntil p = fst . split p

export
dropUntil : MeasureRM a => (Interval -> Bool) -> PosMap a -> PosMap a
dropUntil p = snd . split p

export
Show a => Show (PosMap a) where
  showPrec p xs = showCon p "fromList" $ showArg (foldr (::) [] xs)

larger : FileRange -> Interval -> Bool
larger i (MkInterval (MkRange k _)) = k >= i
larger i NoInterval = False

larger' : FileRange -> Interval -> Bool
larger' i (MkInterval (MkRange k _)) = k > i
larger' i NoInterval = False

||| Inserts a new element in the map, in lexicographical order.
export
insert : Measure a => a -> PosMap a -> PosMap a
insert v m = let (l, r) = split (larger (measure v)) m in l ++ (v <| r)

||| Builds a new map from a list of measurable elements, inserting in
||| lexicographical order.
export
fromList : Measure a => List a -> PosMap a
fromList = foldr insert empty

merge1 : Measure a => PosMap a -> PosMap a -> PosMap a
merge2 : Measure a => PosMap a -> PosMap a -> PosMap a

merge1 xs ys =
  case viewl xs of
       EmptyL => ys
       a <: as' => let (l, r) = split (larger (measure a)) ys in
                       l ++ (a <| assert_total (merge2 as' r))

merge2 xs ys =
  case viewl ys of
       EmptyL => xs
       b <: bs' => let (l, r) = split (larger' (measure b)) xs in
                       l ++ (b <| assert_total (merge1 r bs'))

||| Merges two interval maps.
export
union : Measure a => PosMap a -> PosMap a -> PosMap a
union xs ys = merge1 xs ys

atleast : FilePos -> Interval -> Bool
atleast k (MkInterval (MkRange _ high)) = k <= high
atleast k NoInterval = False

greater : FilePos -> Interval -> Bool
greater k (MkInterval (MkRange low _)) = fst low > k
greater k NoInterval = False

||| Finds all the intervals that overlap with the given interval.
export
inRange : MeasureRM a => FilePos -> FilePos -> PosMap a -> List a
inRange low high t = matches (takeUntil (greater high) t)
  -- takeUntil selects all the intervals within the given upper bound,
  -- however the remaining interval are not necessarily adjacent in
  -- the sequence, thus it drops elements until the next intersecting
  -- interval with dropUntil.
  where matches : PosMap a -> List a
        matches xs = case viewl (dropUntil (atleast low) xs) of
                          EmptyL => []
                          x <: xs' => x :: assert_total (matches xs')

||| Finds the values matching the exact interval input
export
exactRange : MeasureRM a => FilePos -> FilePos -> PosMap a -> List a
exactRange low high t = flip mapMaybe (inRange low high t) $ \ a =>
  do let (MkRange rng _) = measureRM a
     guard (rng == (low, high))
     pure a

||| Returns all the interval that contains the given point.
export
searchPos : MeasureRM a => FilePos -> PosMap a -> List a
searchPos p = inRange p p

||| Returns all the intervals that intersect the given interval.
export
intersections : MeasureRM a => FileRange -> PosMap a -> List a
intersections i = inRange (fst i) (snd i)

||| Returns all the intervals that contain the given interval.
export
dominators : MeasureRM a => FileRange -> PosMap a -> List a
dominators i = inRange (snd i) (fst i)

||| Returns the extreme boundaries of the map, if non empty.
export
bounds : Measure a => PosMap a -> Maybe FileRange
bounds t =
  case measureTree t of
       NoInterval => Nothing
       MkInterval (MkRange _ high) =>
         case viewl t of
              EmptyL => Nothing
              x <: _ => Just (fst (measure x), high)

public export
Measure NonEmptyFC where
  measure = snd

public export
Measure (NonEmptyFC, a) where
  measure = measure . fst


text:
module Main

import Sixel

partial
main : IO ()
main = do
  Right decoder <- MkDecoder
    | Left error => putStrLn getAdditionalMessage
  Right _ <- setOpt decoder OptFlagInput "lena512.sixel"
    | Left error => putStrLn getAdditionalMessage
  Right _ <- setOpt decoder OptFlagOutput "lena512.bmp"
    | Left error => putStrLn getAdditionalMessage
  Right _ <- decode decoder
    | Left error => putStrLn getAdditionalMessage
  pure ()

max_stars_repo_name: Kaiepi/id-sixel

max_issues_repo_name: Kaiepi/id-sixel

max_forks_repo_name: Kaiepi/id-sixel


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

import Data.Vect

-- check that all functions are total
%default total

infixr 5 .+.

data Schema = SString
            | SInt
            | SChar
            | (.+.) Schema Schema

SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType SChar = Char
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

record DataStore where
  constructor MkData
  schema : Schema
  size : Nat
  items : Vect size (SchemaType schema)

addToStore : (store : DataStore) -> SchemaType (schema store) -> DataStore
addToStore (MkData schema size store) newItem
  = MkData schema _ (addToData store)
  where
    addToData : Vect oldsize (SchemaType schema) ->
                Vect (S oldsize) (SchemaType schema)
    addToData [] = [newItem]
    addToData (x :: xs) = x :: addToData xs

||| Supported commands
data Command : Schema -> Type where
               ||| Set schema
               SetSchema : (newSchema : Schema) -> Command schema
               ||| Add an item
               Add : SchemaType schema -> Command schema
               ||| Get an item by its id
               Get : Integer -> Command schema
               ||| List the contents of the store
               List : Command schema
               ||| Get the number of items
               Size : Command schema
               |||| Quit
               Quit : Command schema

parseSchema : List String -> Maybe Schema
parseSchema ("String" :: xs) =
  case xs of
    [] => Just SString
    _ => parseSchema xs >>= Just . (SString .+.)
parseSchema ("Int" :: xs) =
  case xs of
    [] => Just SInt
    _ => parseSchema xs >>= Just . (SInt .+.)
parseSchema ("Char" :: xs) =
  case xs of
    [] => Just SChar
    _ => parseSchema xs >>= Just . (SChar .+.)
parseSchema _ = Nothing

parsePrefix : (schema : Schema) -> String -> Maybe (SchemaType schema, String)
parsePrefix SString input = getQuoted (unpack input)
  where
    getQuoted : List Char -> Maybe (String, String)
    getQuoted ('"' :: xs)
      = case span (/= '"') xs of
          (quoted, '"' :: rest) => Just (pack quoted, ltrim (pack rest))
          _ => Nothing
    getQuoted _ = Nothing
parsePrefix SInt input = case span isDigit input of
                      ("", rest) => Nothing
                      (num, rest) => Just (cast num, ltrim rest)
parsePrefix SChar input = case unpack input of
                      [] => Nothing
                      (x :: rest) => Just (x, ltrim (pack rest))
parsePrefix (schema1 .+. schema2) input =
  do (val1, rest1) <- parsePrefix schema1 input
     (val2, rest2) <- parsePrefix schema2 rest1
     Just ((val1, val2), rest2)

parseBySchema : (schema : Schema) -> String -> Maybe (SchemaType schema)
parseBySchema schema input =
  do (res, rest) <- parsePrefix schema input
     if rest == "" then Just res else Nothing

parseCommand : (schema : Schema) -> String -> String -> Maybe (Command schema)
parseCommand schema "schema" rest
  = parseSchema (words rest) >>= Just . SetSchema
parseCommand schema "add" rest
  = parseBySchema schema rest >>= Just . Add
parseCommand schema "get" "" = Just List
parseCommand schema "get" val = case all isDigit (unpack val) of
                                  False => Nothing
                                  True => Just (Get (cast val))
parseCommand schema "size" "" = Just Size
parseCommand schema "quit" "" = Just Quit
parseCommand _ _ _ = Nothing

parse : (schema : Schema) -> (input : String) -> Maybe (Command schema)
parse schema input = case span (/= ' ') input of
                      (cmd, args) => parseCommand schema cmd (ltrim args)

display : SchemaType schema -> String
display {schema = SString} item = item
display {schema = SInt} item = show item
display {schema = SChar} item = show item
display {schema = (x .+. y)} (item1, item2)
  = display item1 ++ ", " ++ display item2

getEntry : (pos : Integer) -> (store : DataStore) -> Maybe (String, DataStore)
getEntry pos store
  = let store_items = items store in
      case integerToFin pos (size store) of
        Nothing => Just ("Out of range \n", store)
        Just id => Just (display (index id store_items) ++ "\n", store)

setSchema : (store : DataStore) -> Schema -> Maybe DataStore
setSchema store schema = case size store of
                          Z => Just (MkData schema _ [])
                          S k => Nothing

presentResults : Vect _ (Nat, SchemaType schema) -> String
presentResults results = foldl (++) "" $ map helper results
  where
    helper : (Nat, SchemaType schema) -> String
    helper (x, res) = show x ++ ": " ++ (display res) ++ "\n"

listStore : (store : DataStore) -> String
listStore store = presentResults $ helper (items store) 0
  where
    helper : Vect size' (SchemaType (schema store)) ->
             Nat ->
             Vect size' (Nat, SchemaType (schema store))
    helper [] _ = []
    helper (x :: xs) k = (k, x) :: helper xs (S k)

processInput : DataStore -> String -> Maybe (String, DataStore)
processInput store input
  = case parse (schema store) input of
        Nothing => Just ("Invalid command\n", store)
        Just (SetSchema schema') =>
          case setSchema store schema' of
            Nothing => Just ("Can't update schema\n", store)
            Just store' => Just ("OK\n", store')
        Just (Add item) =>
          Just ("ID " ++ show (size store) ++ "\n", addToStore store item)
        Just (Get pos) => getEntry pos store
        Just List => Just (listStore store, store)
        Just Size => Just (show (size store) ++ "\n", store)
        Just Quit => Nothing

partial
main : IO ()
main = replWith (MkData SString _ []) "Command: " processInput

max_stars_repo_name: pascalpoizat/idris-book

max_issues_repo_name: pascalpoizat/idris-book

max_forks_repo_name: pascalpoizat/idris-book


text:
import Data.Vect

containsWord : {- LogMessage -} String -> Bool
containsWord = const True

stringToList : String -> List Char
stringToList "" = []
stringToList s = strHead s :: stringToList (strTail s)

listToVector : (s : List a) -> Vect (length s) a
listToVector [] = Nil
listToVector (l::ls) = l :: listToVector (ls)

stringToVector : (s : String) -> Vect (length (stringToList s)) Char
stringToVector s = listToVector $ stringToList s

breakOffWord : Vect (S (a + b)) Char -> (Vect a Char, Vect b Char)
breakOffWord (s :: st) = if s == ' '
    then (Nil, st)
    else let (a, b) = breakOffWord st in (s :: a, b)


text:
module Toolkit.Data.List.Interleaving

%default total

infixr 6 <::
infixr 6 ::>

public export
data Interleaving : (xs, ys, zs : List type) -> Type where
  Empty   : Interleaving Nil Nil Nil

  Left : {xs,ys,zs : List type}
      -> (x : type)
      -> (rest : Interleaving xs ys zs)
              -> Interleaving (x::xs) ys (x::zs)
  Right : {xs,ys,zs : List type}
       -> (y : type)
       -> (rest : Interleaving xs ys zs)
               -> Interleaving xs (y::ys) (y::zs)

public export
(<::) : {xs,ys,zs : List type}
     -> (x : type)
     -> (rest : Interleaving xs ys zs)
             -> Interleaving (x::xs) ys (x::zs)
(<::) = Left

public export
(::>) : {xs,ys,zs : List type}
     -> (y : type)
     -> (rest : Interleaving xs ys zs)
             -> Interleaving xs (y::ys) (y::zs)
(::>) = Right

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
-- Vehicle.idr
--
-- Demonstrates type families
-- includes first part of exercise 4.2

||| Power source for Vehicle type
data PowerSource = Petrol | Pedal | Electric

||| Vehicle data type parametrized by power source
data Vehicle : PowerSource -> Type where
  ||| Unicycle, powered by pedal
  Unicycle : Vehicle Pedal
  ||| Bicycle, powered by pedal
  Bicycle : Vehicle Pedal
  ||| Motorcycle, powered by petrol
  Motorcycle : (fuel : Nat) -> Vehicle Petrol
  ||| Car, powered by petrol
  Car : (fuel : Nat) -> Vehicle Petrol
  ||| Bus, powered by petrol
  Bus : (fuel : Nat) -> Vehicle Petrol
  ||| Tram, electical powered
  Tram : Vehicle Electric
  ||| ECar, electrical powered by battery
  ECar : (bat : Nat) -> Vehicle Electric

||| gives number of wheels
wheels : Vehicle power -> Nat
wheels Bicycle = 2
wheels (Car fuel) = 4
wheels (Bus fuel) = 4
wheels Unicycle = 1
wheels (Motorcycle fuel) = 2
wheels Tram = 16
wheels ECar = 4

||| refuels petrol powered vehicles
refuel : Vehicle Petrol -> Vehicle Petrol
refuel (Car fuel) = Car 100
refuel (Bus fuel) = Bus 200
refuel (Motorcycle fuel) = Motorcycle 50
refuel Bicycle impossible
refuel Unicycle impossible

||| charges electrical powered vehicles with battery
charge : Vehicle Electric -> Vehicle Electric
charge Tram = Tram   -- nothing changed, not fully reflected by type
charge (ECar bat) = ECar 70

max_stars_repo_name: kkirstein/proglang-playground

max_issues_repo_name: kkirstein/proglang-playground

max_forks_repo_name: kkirstein/proglang-playground


text:
-- -------------------------------------------------------------- [ Parser.idr ]
-- Description : A command line argument parser
-- Copyright   : (c) Huw Campbell
-- --------------------------------------------------------------------- [ EOH ]
module Options.Applicative.Types
import public Text.PrettyPrint.WL

import        Control.Monad.Trans
import        Control.Lens

%default total
%access public export

data ParamType = OptionParams
               | FlagParams
               | ArgParams
               | CmdParams

data Visibility = Visible
                | Hidden
                | Internal

Eq Visibility where
  (==) Visible Visible   = True
  (==) Hidden Hidden     = True
  (==) Internal Internal = True
  (==) _ _               = False

data OptProperties = MkOptProperties Visibility Doc

data OptName : Type where
  ShortName : Char   -> OptName
  LongName  : String -> OptName

Eq OptName where
  (ShortName a) == (ShortName b) = a == b
  (LongName  a) == (LongName  b) = a == b
  _             == _             = False

data ParseError : Type where
  ErrorMsg : String -> ParseError

mutual
  data OptReader : ParamType -> a -> Type where
    OptionReader : List OptName -> (String -> Either ParseError a) -> String -> OptReader OptionParams a
    FlagReader   : List OptName -> a                                         -> OptReader FlagParams a
    ArgReader    :                 (String -> Either ParseError a) -> String -> OptReader ArgParams a
    CmdReader    : List (String, Parser a)                         -> String -> OptReader CmdParams a

  Functor (OptReader ps) where
    map f (OptionReader n p m) = OptionReader n (map f . p) m
    map f (FlagReader n d)     = FlagReader n (f d)
    map f (ArgReader p m)      = ArgReader (map f . p) m
    map f (CmdReader ps m)     = assert_total $ CmdReader ((\(n,p) => (n, map f p)) <$> ps) m

  data Option : ParamType -> a -> Type where
    Opt : OptProperties -> OptReader ps a -> Option ps a

  Functor (Option ps) where
    map f (Opt props rdr) = Opt props (map f rdr)

  data Parser : (a : Type) -> Type where
    NilP : Maybe a -> Parser a
    OptP : Option ps a -> Parser a
    AppP : Parser (x -> a) -> Parser x -> Parser a
    AltP : Parser a -> Parser a -> Parser a

  Functor Parser where
    map f (NilP x) = NilP (map f x)
    map f (OptP x) = OptP (map f x)
    map f (AppP ff a) = AppP (map (f .) ff) a
    map f (AltP a b) = AltP (map f a) (map f b)

Applicative Parser where
  pure  = NilP . Just
  (<*>) = AppP

Alternative Parser where
  empty = NilP Nothing
  (<|>) = AltP

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

max_stars_repo_name: statebox/optparse-idris

max_issues_repo_name: statebox/optparse-idris

max_forks_repo_name: statebox/optparse-idris


text:
> module NonNegRational.MeasureProperties

> import Syntax.PreorderReasoning

> import NonNegRational.NonNegRational
> import NonNegRational.Measures
> import NonNegRational.BasicOperations
> import NonNegRational.BasicProperties
> import NonNegRational.Predicates
> import NonNegRational.LTEProperties
> import Fraction.Fraction
> import Fraction.Normal
> import Fraction.Predicates
> import Fraction.BasicProperties
> import List.Properties
> import Nat.Positive
> import PNat.PNat
> import PNat.Operations
> import PNat.Properties

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

* Properties of |factor|:

> %freeze fromFraction

> |||
> factorLemma : {A, B, C : Type} ->
>               (as : List A) -> (f : A -> B) -> (g : A -> C) ->
>               factor (map f as) = factor (map g as)
> factorLemma  Nil f g = Refl
> factorLemma (a :: as) f g =
>     ( factor (map f (a :: as)) )
>   ={ Refl }=
>     ( factor (f a :: map f as) )
>   ={ Refl }=
>     ( fromFraction (1, Element (S (length (map f as))) MkPositive) )
>   ={ cong {f = \ ZUZU => fromFraction (1, Element (S ZUZU) MkPositive)} (lengthLemma as f g) }=
>     ( fromFraction (1, Element (S (length (map g as))) MkPositive) )
>   ={ Refl }=
>     ( factor (g a :: map g as) )
>   ={ Refl }=
>     ( factor (map g (a :: as)) )
>   QED
> %freeze factorLemma

* Properties of |sum|:

> %thaw fromFraction

> ||| |sum| is monotone
> monotoneSum : {A : Type} ->
>               (f : A -> NonNegRational) -> (g : A -> NonNegRational) ->
>               (p : (a : A) -> f a `LTE` g a) ->
>               (as : List A) ->
>               sum (map f as) `LTE` sum (map g as)
> monotoneSum f g p Nil = LTEZero
> monotoneSum f g p (a :: as) = s5 where
>   s1 : sum (map f (a :: as)) = f a + sum (map f as)
>   s1 = Refl
>   s2 : sum (map g (a :: as)) = g a + sum (map g as)
>   s2 = Refl
>   s3 : f a `LTE` g a
>   s3 = p a
>   s4 : sum (map f as) `LTE` sum (map g as)
>   s4 = monotoneSum f g p as
>   s5 : sum (map f (a :: as)) `LTE` sum (map g (a :: as))
>   s5 = NonNegRational.LTEProperties.monotonePlusLTE s3 s4

> %freeze fromFractionLinear
> %freeze fromFraction

> ||| The sum of n terms of the form 1/(S m) is n/(S m)
> sumLemma0 : (n : Nat) -> (m : Nat ) ->
>             sum (replicate n (fromFraction (1, Element (S m) MkPositive)))
>             =
>             fromFraction (n, Element (S m) MkPositive)

> sumLemma0 Z m =
>   let Sm' = Element (S m) MkPositive in
>   let SZ' = Element 1 MkPositive in
>     ( sum (replicate Z (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( sum Nil )
>   ={ Refl }=
>     ( fromFraction (0, SZ') )
>   ={ fromFractionEqLemma (0, SZ') (0, Sm') Refl }=
>     ( fromFraction (0, Sm') )
>   QED

> sumLemma0 (S n) m =
>   let Sm' : PNat = Element (S m) MkPositive in
>   let Sm  : Nat  = toNat Sm' in
>   let Sn  : Nat  = S n in
>     ( sum (replicate (S n) (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( sum (fromFraction (1, Sm') :: replicate n (fromFraction (1, Sm'))) )
>   ={ Refl }=
>     ( fromFraction (1, Sm') + sum (replicate n (fromFraction (1, Sm'))) )
>   ={ cong {f = \ X => fromFraction (1, Sm') + X} (sumLemma0 n m) }=
>     ( fromFraction (1, Sm') + fromFraction (n, Sm') )
>   ={ sym (fromFractionLinear (1, Sm') (n, Sm')) }=
>     ( fromFraction ((1, Sm') + (n, Sm')) )
>   ={ cong {f = fromFraction} Refl }=
>     ( fromFraction (1 * Sm + n * Sm, Sm' * Sm') )
>   ={ cong {f = \ X => fromFraction (X, Sm' * Sm')} (sym (multDistributesOverPlusLeft 1 n Sm)) }=
>     ( fromFraction ((1 + n) * Sm, Sm' * Sm') )
>   ={ multElimRight (1 + n) Sm' Sm' }=
>     ( fromFraction (1 + n, Sm') )
>   ={ cong {f = \ X => fromFraction (X, Sm')} (plusOneSucc n) }=
>     ( fromFraction (Sn, Sm') )
>   QED

* Properties of |average|:

> %freeze monotoneSum

> ||| |average| is monotone
> monotoneAverage : {A : Type} ->
>                   (f : A -> NonNegRational) -> (g : A -> NonNegRational) ->
>                   (p : (a : A) -> f a `LTE` g a) ->
>                   (as : List A) ->
>                   average (map f as) `LTE` average (map g as)
> monotoneAverage f g p as = monotoneMultLTE {a = sum (map f as)}
>                                            {b = sum (map g as)}
>                                            {c = factor (map f as)}
>                                            {d = factor (map g as)}
>                                            s1 s3 where
>   s1 : sum (map f as) `LTE` sum (map g as)
>   s1 = monotoneSum f g p as
>   s2 : factor (map f as) `LTE` factor (map f as)
>   s2 = reflexiveLTE (factor (map f as))
>   s3 : factor (map f as) `LTE` factor (map g as)
>   s3 = replace {P = \ ZUZU => factor (map f as) `LTE` ZUZU} (factorLemma as f g) s2
> %freeze monotoneAverage

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Interpreter

import Data.Fin
import Data.Vect

data Ty = TyInt | TyBool | TyFun Ty Ty

interpTy : Ty -> Type
interpTy TyInt = Integer
interpTy TyBool = Bool
interpTy (TyFun x y) = interpTy x -> interpTy y

using (G : Vect n Ty)
  -- See 'De Bruijn index'

  -- HasType i G t means variable i in context G has type t
  -- This type acts like a Nat, like an index to variables
  data HasType : (i : Fin n) -> Vect n Ty -> Ty -> Type where
    Stop : HasType FZ (t :: G) t
    Pop  : HasType k G t -> HasType (FS k) (u :: G) t

  data Expr : Vect n Ty -> Ty -> Type where
    Var : HasType i G t -> Expr G t
    Val : (x : Integer) -> Expr G TyInt
    Lam : Expr (a :: G) t -> Expr G (TyFun a t)
    App : Expr G (TyFun a t) -> Expr G a -> Expr G t
    Op  : (interpTy a -> interpTy b -> interpTy c) ->
          Expr G a -> Expr G b -> Expr G c
    If  : Expr G TyBool -> Lazy (Expr G a) -> Lazy (Expr G a) -> Expr G a

  data Env : Vect n Ty -> Type where
    Nil  : Env Nil
    (::) : interpTy a -> Env G -> Env (a :: G)

  lookup : HasType i G t -> Env G -> interpTy t
  lookup Stop    (x :: xs) = x
  lookup (Pop k) (x :: xs) = lookup k xs

  interp : Env G -> Expr G t -> interpTy t
  interp env (Var i) = lookup i env
  interp env (Val x) = x
  interp env (Lam f) = \x => interp (x :: env) f
  interp env (App f x) = (interp env f) (interp env x)
  interp env (Op f x y) = f (interp env x) (interp env y)
  interp env (If b x y) = if interp env b
                          then interp env x
                          else interp env y

max_stars_repo_name: shouya/thinking-dumps

max_issues_repo_name: shouya/thinking-dumps

max_forks_repo_name: shouya/thinking-dumps