text:
module Universality

import public Category
import public Isomorphism

%default total

public export
IsUnique : {cat : Category} -> {a, b : Object cat} ->
  (property : Morphism cat a b -> Type) -> (f : Morphism cat a b) -> Type
IsUnique {cat} {a} {b} property f =
    (property f, (g : Morphism cat a b) -> property g -> g = f)

public export
IsOnlyMorphism : {cat : Category} -> {a, b : Object cat} ->
    Morphism cat a b -> Type
IsOnlyMorphism f = IsUnique (\_ => ()) f

public export
OnlyMorphismIsUnique : {cat : Category} -> {a, b : Object cat} ->
    {f : Morphism cat a b} -> IsOnlyMorphism {cat} {a} {b} f ->
    (g, h : Morphism cat a b) -> g = h
OnlyMorphismIsUnique (_, onlyAB) g h = rewrite (onlyAB h ()) in (onlyAB g ())

public export
IsTerminal : {cat : Category} -> (a : Object cat) -> Type
IsTerminal {cat} a = (b : Object cat) -> DPair (Morphism cat b a) IsOnlyMorphism

public export
IdOnlyTerminalEndomorphism : {cat : Category} -> {a : Object cat} ->
  (aIsTerminal : IsTerminal {cat} a) -> (f : Morphism cat a a) ->
  f = Identity cat a
IdOnlyTerminalEndomorphism {cat} {a} aIsTerminal f =
  OnlyMorphismIsUnique (snd (aIsTerminal a)) f (Identity cat a)

public export
IsInitial : {cat : Category} -> (a : Object cat) -> Type
IsInitial {cat} a = (b : Object cat) -> DPair (Morphism cat a b) IsOnlyMorphism

public export
IdOnlyInitialEndomorphism : {cat : Category} -> {a : Object cat} ->
  (aIsInitial : IsInitial {cat} a) -> (f : Morphism cat a a) ->
  f = Identity cat a
IdOnlyInitialEndomorphism {cat} {a} aIsInitial f =
  OnlyMorphismIsUnique (snd (aIsInitial a)) f (Identity cat a)

public export
IsUniqueMorphismWithProperty : {cat : Category} -> {a, b : Object cat} ->
  (property : Morphism cat a b -> Type) -> (m : Morphism cat a b) -> Type
IsUniqueMorphismWithProperty property m =
  (property m, (m' : Morphism cat a b) -> property m' -> m' = m)

public export
AreUniquelyIsomorphic : {cat : Category} -> (a, b : Object cat) -> Type
AreUniquelyIsomorphic {cat} a b =
  (iso : Isomorphic a b **
   IsUniqueMorphismWithProperty IsIsomorphism (fst iso))

public export
IsUniqueUpToUniqueIsomorphism : {cat : Category} ->
  (property : Object cat -> Type) -> Object cat -> Type
IsUniqueUpToUniqueIsomorphism {cat} property a =
  (property a,
   (b : Object cat) -> property b -> AreUniquelyIsomorphic a b)

max_stars_repo_name: rokopt/dao-fp-exercises

max_issues_repo_name: rokopt/dao-fp-exercises

max_forks_repo_name: rokopt/dao-fp-exercises


text:
module lib.sub.Sub

export
subslaute : String
subslaute = ", and Sub!!!"

ext: idr


text:
import Data.List

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

Show a => Show (Vect n a) where
  show [] = "END"
  show (x :: xs) = show x ++ ", " ++ show xs

Show (Vect n Integer) where
  show [] = "END"
  show (x :: xs) = show x ++ ", " ++ show xs

wrong : String
wrong = show (the (Vect _ _) [1])


text:
module Common.Abbrev

%default total
%access public export

Binop : Type -> Type
Binop s = s -> s -> s

Binrel : Type -> Type
Binrel s = s -> s -> Type

OuterBinop : {index : Type} -> (f : index -> Type) -> (a,b,c : index) -> Type
OuterBinop f a b c = f a -> f b -> f c

infixl 5 ===
infixl 5 @==

||| associative infix syntax for `trans`
(===) : a = b -> b = c -> a = c
(===) Refl Refl = Refl

(@==) : a = b -> a = c -> b = c
(@==) Refl Refl = Refl

max_stars_repo_name: jeroennoels/verified-algebra

max_issues_repo_name: jeroennoels/verified-algebra

max_forks_repo_name: jeroennoels/verified-algebra


text:
module Expr

data Expr : Type where
  Value : (a:Int) -> Expr
  Plus : Expr -> Expr -> Expr
  Minus : Expr -> Expr -> Expr
  Mult : Expr -> Expr -> Expr

evaluate : Expr -> Int
evaluate (Value x) = x
evaluate (Plus x y) = (evaluate x) + (evaluate y)
evaluate (Minus x y) = (evaluate x) - (evaluate y)
evaluate (Mult x y) = (evaluate x) * (evaluate y)

max_stars_repo_name: janschultecom/idris-examples

max_issues_repo_name: janschultecom/idris-examples

max_forks_repo_name: janschultecom/idris-examples


text:
module Occupation

public export
record Occupation where
  constructor CreateOccupation
  type : String
  id : String
  name : String

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
module Replica.Option.Types

import Data.List
import public Data.List1
import public Data.List.AtIndex
import Data.Maybe
import public Data.OpenUnion

import Replica.Help
import public Replica.Other.Free

%default total

export
prefixLongOption : String -> String
prefixLongOption = ("--" <+>)

export
prefixShortOption : Char -> String
prefixShortOption x = pack ['-',x]

public export
record Value a where
  constructor MkValue
  name : String
  parser : String -> Maybe a

export
Functor Value where
  map func x = MkValue x.name (map func . x.parser)

public export
record Mod a where
  constructor MkMod
  longNames : List1 String
  shortNames : List Char
  param : Either a (Value a)
  description : String

export
Functor Mod where
  map func x = MkMod x.longNames x.shortNames
    (bimap func (map func) x.param)
    x.description

public export
record Option b a where
  constructor MkOption
  mods : List1 (Mod a)
  defaultValue : a
  setter : a -> b -> Either String b

export
embedOption : (c -> b) -> (b -> c -> c) -> Option b a -> Option c a
embedOption f g x = MkOption x.mods x.defaultValue (embed f g x.setter)
  where
    embed : (c -> b) -> (b -> c -> c) -> (a -> b -> Either String b) -> a -> c -> Either String c
    embed unwrap wrap set p w = flip wrap w <$> set p (unwrap w)

namespace Param

  public export
  record Param b a where
    constructor MkParam
    name : String
    parser : String -> Maybe a
    setter : a -> b -> Either String b

  export
  embedParam : (c -> b) -> (b -> c -> c) -> Param b a -> Param c a
  embedParam f g x = MkParam x.name x.parser (embed f g x.setter)
    where
      embed : (c -> b) -> (b -> c -> c) -> (a -> b -> Either String b) -> a -> c -> Either String c
      embed unwrap wrap set p w = flip wrap w <$> set p (unwrap w)

namespace Parts

  public export
  Part : Type -> Type -> Type
  Part b a = Union (\p => p b a) [Param, Option]

  export
  embedPart : (c -> b) -> (b -> c -> c) -> Part b a -> Part c a
  embedPart get set x = let
    Left x1 = decomp x
      | Right v => inj $ embedParam get set v
    v = decomp0 x1
    in inj $ embedOption get set v

public export
OptParse : Type -> Type -> Type
OptParse = Ap . Part

export
embed : (c -> b) -> (b -> c -> c) -> OptParse b a -> OptParse c a
embed get set (Pure x) = Pure x
embed get set (MkAp x y) = MkAp (embedPart get set x) $ embed get set y

namespace Parser

  Parser : (a : Type) -> Type
  Parser a = List String -> Maybe (List String, a)

  modParser : Mod a -> Parser a
  modParser m [] = Nothing
  modParser m (x::xs) = let
    validOption = map prefixLongOption (forget m.longNames)
                  ++ map prefixShortOption m.shortNames
    in do
      guard $ x `elem` validOption
      let Right v = m.param
        | Left r => pure (xs, r)
      case xs of
           [] => Nothing
           (y::ys) => MkPair ys <$> v.parser y

  optionParser : Option b a -> Parser (b -> Either String b)
  optionParser x xs = map x.setter <$> choiceMap (flip modParser xs) x.mods

  partParser : Part b a -> Parser (b -> Either String b)
  partParser x xs = let
    Left x1 = decomp x
      | Right v => case xs of
                        [y] => MkPair [] . v.setter <$> v.parser y
                        _   => Nothing
    in optionParser (decomp0 x1) xs

  public export
  data ParseResult a
    = InvalidOption (List1 String)
    | InvalidMix String -- reason
    | Done a

  export
  Functor ParseResult where
    map func (InvalidOption xs) = InvalidOption xs
    map func (InvalidMix x) = InvalidMix x
    map func (Done x) = Done (func x)

  export
  parse : a ->
    OptParse a b ->
    List String ->
    ParseResult a
  parse acc o [] = Done acc
  parse acc o (x::xs) = let
    Just (xs', f) = runApM (\p => partParser p (x::xs)) o
      | Nothing => InvalidOption (x:::xs)
    in either
         InvalidMix
         (\y => parse y o $ assert_smaller (x::xs) xs')
         (f acc)

namespace Default

  defaultOption : Option b a -> Maybe a
  defaultOption = Just . defaultValue

  defaultParam : Param b a -> Maybe a
  defaultParam = const Nothing

  export
  defaultPart : Part b a -> Maybe a
  defaultPart x = let
   Left x1 = decomp x
     | Right v => defaultParam v
   v = decomp0 x1
   in defaultOption v

namespace Help

  optionName : (long : List String) -> (short : List Char) ->
               (param : Either a (Value b)) -> String
  optionName long short param =
    either (flip const) (\v => (++ " \{v.name}")) param $
    (concat $ intersperse ", " $
       map ("--" ++) long ++ map (\c => pack ['-',c]) short)

  modHelp : Mod a -> Help
  modHelp x = MkHelp (optionName (forget x.longNames) x.shortNames x.param)
                     Nothing x.description [] Nothing

  export
  partHelp : Part b a -> List Help
  partHelp x = let
    Left x1 = decomp x
      | Right v => []
    v = decomp0 x1
    in map modHelp $ forget v.mods

  export
  commandHelp :
    (name : String) -> (description : String) ->
    (options : OptParse b c) ->
    (param : Maybe String) -> Help
  commandHelp name description options param = MkHelp
    name
    (Just "replica \{name} [OPTIONS]\{paramExt param}")
    description
    ( catMaybes
       [ map (MkPair "Options") $
           toList1' $ reverse $ runApM (\p => partHelp p) options
       ])
    Nothing
    where
      paramExt : Maybe String -> String
      paramExt = maybe "" (" "<+>)

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica


text:
> module Main

> import Data.Fin
> import Data.Vect
> import Data.Matrix
> import Data.Matrix.Numeric

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

* Preliminaries

This is a re-implementation of

  https://gist.github.com/mrkgnao/a45059869590d59f05100f4120595623

which, in turn, is an Idris implementation of

  https://blog.jle.im/entry/practical-dependent-types-in-haskell-1.html

* Layers

A layer of type |A| with |n| inputs and |m| outputs is a vector of |m|
elements of type |A| (the biases) and a |m| x |n| matrix of elements of
type |A| (the weights):

> data Layer : Nat -> Nat -> Type -> Type where
>   MkLayer : {m, n : Nat} -> {A : Type} ->
>             (biases : Vect m A) -> (weights : Matrix m n A) -> Layer n m A

* Sequential neural networks

A sequential neural network of type |A| with |n| inputs, |m| outputs and
a sequence of intermediate layers is a sequence of layers of type
|A|. It can consist of either a single (Output) layer or of a layer with
|n| inputs and |k| outputs together with a network with |k| inputs and
|m| outputs:

> infixr 5 :>:

> data Network : Nat -> List Nat -> Nat -> Type -> Type where
>   Output : {n, m : Nat} -> {A : Type} ->
>            Layer n m A -> Network n [] m A
>   (:>:)  : {n, k, m : Nat} -> {ks : List Nat} -> {A : Type} ->
>            Layer n k A -> Network k ks m A -> Network n (k :: ks) m A

* Feed-forward

The idea is that, given a sequential neural network of type |A| with |n|
inputs and |m| outputs and a vector of |n| inputs of matching type, one
can compute a vector of |n| outputs.

The computation is called feed-forward. It requires |A| to implement
addition and multiplication and depends on an "activation" function |s :
A -> A|:

> feedForward : {n, m : Nat} -> {ks : List Nat} -> {A : Type} -> Num A =>
>               (A -> A) -> Vect n A -> Network n ks m A -> Vect m A

The idea is to feed the input into the first layer and pass its output
(activated through |s|) as input for the next layer. With

> evalLayer : {n, m : Nat} -> {t : Type} -> Num t =>
>             Vect n t -> Layer n m t -> Vect m t
> evalLayer {n} {m} {t} input (MkLayer biases weights) = output where
>   output : Vect m t
>   output = biases + (weights </> input)

the implementation of |feedForward| is trivial:

> feedForward s input (Output l) = map s (evalLayer input l)
> feedForward s input (l :>: ls) = feedForward s (map s (evalLayer input l)) ls

* Error

Given a training pair |(x, y)|, the error is simply the difference
between |y| and the output of the network when fed with the input |x|:

> error : {n, m : Nat} -> {ks : List Nat} -> {t : Type} -> Num t => Neg t =>
>         (t -> t) -> Vect n t -> Vect m t -> Network n ks m t -> Vect m t
> error {m} {t} s input target network = target - output where
>   output : Vect m t
>   output = (feedForward s input network)

* Back propagation

> backPropagation : {n, m : Nat} -> {ks : List Nat} -> {t : Type} ->
>                   Num t => Neg t =>
>                   (s      : t -> t) ->
>                   (s'     : t -> t) ->
>                   (eta    : t) ->
>                   (input  : Vect n t) ->
>                   (target : Vect m t) ->
>                   Network n ks m t -> Network n ks m t

> backPropagation {t} s s' eta input target net = fst (go input target net)
>
>   where go : {n, m : Nat} -> {ks : List Nat} ->
>              Vect n t -> Vect m t ->  Network n ks m t -> (Network n ks m t, Vect n t)
>
>         go input target ((MkLayer bias weights) :>: rest) =
>           let y             = evalLayer input (MkLayer bias weights)
>               output        = map s y
>               (rest', dWs') = go output target rest
>               dEdy          = (map s' y) * dWs'
>               bias'         = bias - (eta <# dEdy)
>               weights'      = weights - (eta <#> (dEdy >< input))
>               layer'        = (MkLayer bias' weights')
>               dWs           = (transpose weights) </> dEdy
>           in (layer' :>: rest', dWs)
>
>         go input target (Output (MkLayer bias weights)) =
>           let y        = evalLayer input (MkLayer bias weights)
>               output   = map s y
>               dEdy     = (map s' y) * (output - target)
>               bias'    = bias - (eta <# dEdy)
>               weights' = weights - (eta <#> (dEdy >< input))
>               layer'   = (MkLayer bias' weights')
>               dWs      = (transpose weights) </> dEdy
>           in (Output layer', dWs)

* Example

> initial : Network 2 [2] 2 Double
> initial = first :>: second
>   where first  = MkLayer [0.35, 0.35]
>                          [ [0.15, 0.20],
>                            [0.25, 0.30]
>                          ]
>         second = Output
>                $ MkLayer [0.60, 0.60]
>                          [ [0.40, 0.45],
>                            [0.50, 0.55]
>                          ]

> input : Vect 2 Double
> input = [0.05,0.10]

> target : Vect 2 Double
> target = [0.01,0.99]

> s : Double -> Double
> s x = 1 / (1 + exp (-x))

> s' : Double -> Double
> s' x = (s x) * (1 - s x)

> main : IO ()
> main = let step   = backPropagation s s' 0.5 input target
>            errorF = error s input target
>            states = iterate step initial
>        in putStrLn . unlines $ map (show . errorF) (take 100 states)

> {-

> ---}

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Control.Function

public export
interface Injective (f : a -> b) where
  constructor MkInjective
  injective : {x, y : a} -> f x = f y -> x = y

public export
inj : (0 f : a -> b) -> {auto 0 _ : Injective f} -> {0 x, y : a} -> (0 _ : f x = f y) -> x = y
inj _ eq = irrelevantEq (injective eq)


text:
module Determinism

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

%default total
%access export

------------------------------------------------------------------------------
-- Begin: DETERMINISM OF INDUCTIVELY DEFINED SMALL-STEP AND BIG-STEP SEMANTICS

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

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

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

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

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

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

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

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

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

-- End: DETERMINISM OF INDUCTIVELY DEFINED SMALL-STEP AND BIG-STEP SEMANTICS
----------------------------------------------------------------------------

----------------------------------------------------------------------------------
-- Begin: VERY RESTRICTED FROM OF DETERMINISM FOR CO-INDUCTIVELY DEFINED SEMANTICS

-- The coinductive relation 'CoBigStep' is not deterministic as, for example,
-- the term 'omega' can evaluate to anything. However, the following form of
-- determinism holds for terminating terms:
-- (cf. Lemma 35 in "Coinductive big-step operational semantics" by
-- X. Leroy and H. Grall)
coBigStepDeterministic' : BigStep e1 e2 -> CoBigStep e1 e3 -> e2 = e3
--
coBigStepDeterministic' (BStValue v) cbst = coBigStepValueIrreducible cbst v
--
coBigStepDeterministic' (BStApp bst1 bst2 bst3) cbst = case cbst of
  (CoBStValue v)               impossible
  (CoBStApp cbst1 cbst2 cbst3) =>
    case coBigStepDeterministic' bst1 cbst1 of
         Refl => case coBigStepDeterministic' bst2 cbst2 of
                      Refl => case coBigStepDeterministic' bst3 cbst3 of
                                   Refl => Refl
--
coBigStepDeterministic' (BStFix bst1 bst2) cbst = case cbst of
  (CoBStValue v)         impossible
  (CoBStFix cbst1 cbst2) =>
    case coBigStepDeterministic' bst1 cbst1 of
         Refl => case coBigStepDeterministic' bst2 cbst2 of
                      Refl => Refl
--
coBigStepDeterministic' (BStSucc bst) cbst = case cbst of
  (CoBStValue (VSucc v)) => cong . sym $ bigStepValueIrreducible bst v
  (CoBStSucc cbst)       => case coBigStepDeterministic' bst cbst of
                                 Refl => Refl
--
coBigStepDeterministic' (BStPredZero bst) cbst = case cbst of
  (CoBStValue v)       impossible
  (CoBStPredZero cbst) => case coBigStepDeterministic' bst cbst of
                               Refl => Refl
  (CoBStPredSucc cbst) => case coBigStepDeterministic' bst cbst of
                               Refl impossible
--
coBigStepDeterministic' (BStPredSucc bst) cbst = case cbst of
  (CoBStValue v)       impossible
  (CoBStPredZero cbst) => case coBigStepDeterministic' bst cbst of
                               Refl impossible
  (CoBStPredSucc cbst) => case coBigStepDeterministic' bst cbst of
                               Refl => Refl
--
coBigStepDeterministic' (BStIfzZero bst1 bst2) cbst = case cbst of
  (CoBStValue v)             impossible
  (CoBStIfzZero cbst1 cbst2) => coBigStepDeterministic' bst2 cbst2
  (CoBStIfzSucc cbst1 cbst2) => case coBigStepDeterministic' bst1 cbst1 of
                                     Refl impossible
--
coBigStepDeterministic' (BStIfzSucc bst1 bst2) cbst = case cbst of
  (CoBStValue v)             impossible
  (CoBStIfzZero cbst1 cbst2) => case coBigStepDeterministic' bst1 cbst1 of
                                     Refl impossible
  (CoBStIfzSucc cbst1 cbst2) => coBigStepDeterministic' bst2 cbst2

-- An analogous statement holds for terminating terms and the coinductive
-- relation 'CoTransStep', which is generally not deterministic either:
coTransStepDeterministic' : Value e2 -> TransStep e1 e2 ->
                            Value e3 -> CoTransStep e1 e3 ->
                            e2 = e3
coTransStepDeterministic' v2 (TStRefl e1)       v3 (CoTStRefl e1)    = Refl
coTransStepDeterministic' v2 (TStRefl e1)       v3 (CoTStTrans st _) =
  absurd $ valueIrreducible _ v2 st
coTransStepDeterministic' v2 (TStTrans st tst)  v3 (CoTStRefl e1)    =
  absurd $ valueIrreducible _ v3 st
coTransStepDeterministic' v2 (TStTrans st1 tst) v3 (CoTStTrans st2 ctst) =
  case stepDeterministic st1 st2 of
       Refl => coTransStepDeterministic' v2 tst v3 ctst

-- The following statement can also be seen as a restricted
-- from of determinism of the 'CoTransStep' relation given
-- that 'TransStep' terminates:
coTransStepExtends : TransStep e1 e2 -> Value e2 ->
                     CoTransStep e1 e3 -> CoTransStep e3 e2
coTransStepExtends (TStRefl e2)       v (CoTStRefl e2)       = CoTStRefl e2
coTransStepExtends (TStRefl e2)       v (CoTStTrans st ctst) =
  absurd $ valueIrreducible _ v st
coTransStepExtends (TStTrans st tst)  v (CoTStRefl e1)   =
  CoTStTrans st $ transToCoTrans tst
coTransStepExtends (TStTrans st1 tst) v (CoTStTrans st2 ctst) =
  case stepDeterministic st1 st2 of
       Refl => coTransStepExtends tst v ctst

coTransStepExtends' : TransStep e1 e2 -> Value e2 ->
                      CoTransStep e1 e3 -> CoTransStep e1 e2
coTransStepExtends' tst v ctst = coTransStepTransitive ctst $ coTransStepExtends tst v ctst

-- Another result that relies on
--   (a) irreducibility of values and
--   (b) determinism of the 'Step' relation:
coTransStepInterpolates : CoTransStep e1 e3 -> Value e3 -> Step e1 e2 -> CoTransStep e2 e3
coTransStepInterpolates (CoTStRefl e1)        v st = absurd $ valueIrreducible _ v st
coTransStepInterpolates (CoTStTrans st' ctst) v st =
  let eq = stepDeterministic st st'
  in rewrite eq in ctst

-- End: VERY RESTRICTED FROM OF DETERMINISM FOR CO-INDUCTIVELY DEFINED SEMANTICS
--------------------------------------------------------------------------------

-----------------------------------------------------------
-- Begin: DIVERGENCE OF TERM 'Subst.omega' UNDER SMALL-STEP

-- Term 'omega' steps to itself in one step:
stepOmega : Step Subst.omega Subst.omega
stepOmega = StFixBeta

-- That 'omega' steps to itself under the reflexive,
-- transitive closure of 'Step' is trivial:
transStepOmega : TransStep Subst.omega Subst.omega
transStepOmega = TStRefl _

-- By determinism of 'Step', the term 'omega' steps to nothing but itself:
stepOmegaOnly : Step Subst.omega e -> e = Subst.omega
stepOmegaOnly st = stepDeterministic st stepOmega

-- To extend the previous result 'stepOmegaOnly' to the transitive closure
-- of the 'Step' relation, an indexed version of 'TransStep' is needed:
data TransStepN : Nat -> Term [] t -> Term [] t -> Type where
   TStNRefl   : (e : Term [] t) -> TransStepN Z e e
   TStNTrans  : {e : Term [] t} -> {e' : Term [] t} -> {e'' : Term [] t} ->
                Step e e' -> TransStepN n e' e'' -> TransStepN (S n) e e''

transStepFromN : TransStepN n e1 e2 -> TransStep e1 e2
transStepFromN (TStNRefl e1)       = TStRefl e1
transStepFromN (TStNTrans st tstn) = TStTrans st (transStepFromN tstn)

transStepToN : TransStep e1 e2 -> (n : Nat ** TransStepN n e1 e2)
transStepToN (TStRefl e1)      = (Z ** TStNRefl e1)
transStepToN (TStTrans st tst) = let (m ** tstn) = transStepToN tst
                                 in ((S m) ** TStNTrans st tstn)

transStepNOmegaOnly : (n : Nat) -> TransStepN n Subst.omega e -> e = Subst.omega
transStepNOmegaOnly     Z     (TStNRefl _)        = Refl
transStepNOmegaOnly {e} (S k) (TStNTrans st tstk) =
  let eq    = stepOmegaOnly st
      tstk' = replace {P = \x => TransStepN k x e} eq tstk
  in transStepNOmegaOnly k tstk'

-- Finally, the fact that 'omega' only steps to itself is proven
-- by appealing to the indexed version of the transitive closure:
-- (An induction argument analogous to the one in 'transStepNOmegaOnly'
-- is not accepted by Idris' totality checker. Induction would proceed on
-- the structure of the 'TransStep omega e' argument, and the induction
-- hypothesis would be applied to the second argument of the 'TStTrans'
-- constructor, which would again have the type 'TransStep omega e' but
-- only after rewriting with the equation obtained from 'stepOmegaOnly'.)
transStepOmegaOnly : TransStep Subst.omega e -> e = Subst.omega
transStepOmegaOnly tst = let (n ** tstn) = transStepToN tst
                         in transStepNOmegaOnly n tstn

transStepDivergenceOmega : TransStep Subst.omega e -> (Value e -> Void)
transStepDivergenceOmega tst v = let eq = transStepOmegaOnly tst
                                 in case (replace {P = \x => Value x} eq v) of
                                          VZero     impossible
                                          (VSucc _) impossible
                                          VAbs      impossible

-- Instead of diverging, the term 'omega' can evaluate to anything
-- under the coinductive relation 'CoTransStep'. Hence evaluation
-- under 'CoTransStep' is not deterministic:
coTransStepOmegaAny : CoTransStep Subst.omega e
coTransStepOmegaAny = CoTStTrans StFixBeta (coTransStepOmegaAny)

-- End: DIVERGENCE OF TERM 'Subst.omega' UNDER SMALL-STEP
---------------------------------------------------------

---------------------------------------------------------
-- Begin: DIVERGENCE OF TERM 'Subst.omega' UNDER BIG-STEP

-- The following straightforward approach to proving
-- that 'omega' diverges does not pass Idris' totality
-- checker because of the rewriting of 'bst' in the
-- induction step:
--
-- divergenceOmega : BigStep Subst.omega e -> Void
-- divergenceOmega {e = _} (BStValue v) = case v of
--                                             VZero     impossible
--                                             (VSucc _) impossible
--                                             VAbs      impossible
-- divergenceOmega {e = e} (BStFix (BStValue v) bst) =
--   let bst' = replace {P = \x => BigStep x e} substOmega bst
--   in divergenceOmega bst'

-- To prove that 'omega' diverges under big-step semantics,
-- an indexed version of the 'BigStep' relation is introduced:
data BigStepN : Nat -> Term [] t -> (y: Term [] t) -> Type where
  BStValueN    : (v : Value e) -> BigStepN Z e e
  --
  BStAppN      : BigStepN k e1 (TAbs e1') ->
                 BigStepN m e2 e2' ->
                 BigStepN n (subst e2' First e1') e ->
                 BigStepN (S $ k+m+n) (TApp e1 e2) e
  --
  BStFixN      : BigStepN m e (TAbs e') ->
                 BigStepN n (subst (TFix (TAbs e')) First e') e'' ->
                 BigStepN (S $ m+n) (TFix e) e''
  --
  BStSuccN     : BigStepN n e e' ->
                 BigStepN (S n) (TSucc e) (TSucc e')
  --
  BStPredZeroN : BigStepN n e TZero ->
                 BigStepN (S n) (TPred e) TZero
  --
  BStPredSuccN : BigStepN n e (TSucc e') ->
                 BigStepN (S n) (TPred e) e'
  --
  BStIfzZeroN  : BigStepN m e1 TZero ->
                 BigStepN n e2 e ->
                 BigStepN (S $ m+n) (TIfz e1 e2 _) e
  --
  BStIfzSuccN  : BigStepN m e1 (TSucc _) ->
                 BigStepN n e3 e ->
                 BigStepN (S $ m+n) (TIfz e1 _ e3) e

bigStepToN : BigStep e1 e2 -> (n : Nat ** BigStepN n e1 e2)
bigStepToN (BStValue v) = (Z ** BStValueN v)
--
bigStepToN (BStApp bst1 bst2 bst3) = let (n1 ** bstn1) = bigStepToN bst1
                                         (n2 ** bstn2) = bigStepToN bst2
                                         (n3 ** bstn3) = bigStepToN bst3
                                     in ((S $ n1+n2+n3) ** BStAppN bstn1 bstn2 bstn3)
--
bigStepToN (BStFix bst1 bst2) = let (n1 ** bstn1) = bigStepToN bst1
                                    (n2 ** bstn2) = bigStepToN bst2
                                in ((S $ n1+n2) ** BStFixN bstn1 bstn2)
--
bigStepToN (BStSucc bst) = let (n ** bstn) = bigStepToN bst
                           in ((S n) ** BStSuccN bstn)
--
bigStepToN (BStPredZero bst) = let (n ** bstn) = bigStepToN bst
                               in ((S n) ** BStPredZeroN bstn)
--
bigStepToN (BStPredSucc bst) = let (n ** bstn) = bigStepToN bst
                               in ((S n) ** BStPredSuccN bstn)
--
bigStepToN (BStIfzZero bst1 bst2) = let (n1 ** bstn1) = bigStepToN bst1
                                        (n2 ** bstn2) = bigStepToN bst2
                                    in ((S $ n1+n2) ** BStIfzZeroN bstn1 bstn2)
--
bigStepToN (BStIfzSucc bst1 bst2) = let (n1 ** bstn1) = bigStepToN bst1
                                        (n2 ** bstn2) = bigStepToN bst2
                                    in ((S $ n1+n2) ** BStIfzSuccN bstn1 bstn2)

bigStepFromN : BigStepN n e1 e2 -> BigStep e1 e2
bigStepFromN (BStValueN v) = BStValue v
--
bigStepFromN (BStAppN bstn1 bstn2 bstn3) = let bst1 = bigStepFromN bstn1
                                               bst2 = bigStepFromN bstn2
                                               bst3 = bigStepFromN bstn3
                                           in BStApp bst1 bst2 bst3
--
bigStepFromN (BStFixN bstn1 bstn2) = let bst1 = bigStepFromN bstn1
                                         bst2 = bigStepFromN bstn2
                                     in BStFix bst1 bst2
--
bigStepFromN (BStSuccN bstn) = let bst = bigStepFromN bstn
                               in BStSucc bst
--
bigStepFromN (BStPredZeroN bstn) = let bst = bigStepFromN bstn
                                   in BStPredZero bst
--
bigStepFromN (BStPredSuccN bstn) = let bst = bigStepFromN bstn
                                   in BStPredSucc bst
--
bigStepFromN (BStIfzZeroN bstn1 bstn2) = let bst1 = bigStepFromN bstn1
                                             bst2 = bigStepFromN bstn2
                                         in BStIfzZero bst1 bst2
--
bigStepFromN (BStIfzSuccN bstn1 bstn2) = let bst1 = bigStepFromN bstn1
                                             bst2 = bigStepFromN bstn2
                                         in BStIfzSucc bst1 bst2

-- Divergence of 'omega' under the indexed version of big-step semantics:
bigStepDivergenceOmega' : (n : Nat) -> BigStepN n Subst.omega e -> Void
bigStepDivergenceOmega' Z (BStValueN v) = case v of
                                               VZero     impossible
                                               (VSucc _) impossible
                                               VAbs      impossible
bigStepDivergenceOmega' {e} (S n) bstn = case bstn of
  (BStFixN (BStValueN v) bstn2) => let bstn2' = replace {P = \x => BigStepN n x e}
                                                        substOmega bstn2
                                   in bigStepDivergenceOmega' n bstn2'

bigStepDivergenceOmega : BigStep Subst.omega e -> Void
bigStepDivergenceOmega bst = let (n ** bstn) = bigStepToN bst
                             in bigStepDivergenceOmega' n bstn

-- Instead of diverging, the term 'omega' can evaluate to anything
-- under the coinductive relation 'CoBigStep'. Hence, evaluation
-- under 'CoBigStep' is non-deterministic:
coBigStepOmegaAny : CoBigStep Subst.omega e
coBigStepOmegaAny = CoBStFix (CoBStValue VAbs) Determinism.coBigStepOmegaAny

-- End: DIVERGENCE OF TERM 'Subst.omega' UNDER BIG-STEP
-------------------------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
module TypeFuns

SorI : Bool -> Type
SorI False = String
SorI True = Int

getStringOrInt : (isInt : Bool) -> SorI isInt
getStringOrInt False = "Twenty four"
getStringOrInt True = 24

valToString : (isInt : Bool) -> SorI isInt -> String
valToString False x = trim x
valToString True x = cast x

vts : (isInt : Bool) -> (case isInt of
                              False => String
                              True => Int) -> String
vts False x = trim x
vts True x = cast x


text:
module Control.Arrow

import Control.Category
import Data.Either
import Data.Morphisms

infixr 5 <++>
infixr 3 ***
infixr 3 &&&
infixr 2 +++
infixr 2 \|/

public export
interface Category arr => Arrow (0 arr : Type -> Type -> Type) where
  ||| Converts a function from input to output into a arrow computation.
  arrow  : (a -> b) -> arr a b
  ||| Converts an arrow from `a` to `b` into an arrow on pairs, that applies
  ||| its argument to the first component and leaves the second component
  ||| untouched, thus saving its value across a computation.
  first  : arr a b -> arr (a, c) (b, c)
  ||| Converts an arrow from `a` to `b` into an arrow on pairs, that applies
  ||| its argument to the second component and leaves the first component
  ||| untouched, thus saving its value across a computation.
  second : arr a b -> arr (c, a) (c, b)
  second f = arrow {arr = arr} swap >>> first f >>> arrow {arr = arr} swap
    where
    swap : (x, y) -> (y, x)
    swap (a, b) = (b, a)
  ||| A combinator which processes both components of a pair.
  (***)  : arr a b -> arr a' b' -> arr (a, a') (b, b')
  f *** g = first f >>> second g
  ||| A combinator which builds a pair from the results of two arrows.
  (&&&)  : arr a b -> arr a b' -> arr a (b, b')
  f &&& g = arrow dup >>> f *** g

public export
implementation Arrow Morphism where
  arrow  f            = Mor f
  first  (Mor f)      = Mor $ \(a, b) => (f a, b)
  second (Mor f)      = Mor $ \(a, b) => (a, f b)
  (Mor f) *** (Mor g) = Mor $ \(a, b) => (f a, g b)
  (Mor f) &&& (Mor g) = Mor $ \a => (f a, g a)

public export
implementation Monad m => Arrow (Kleislimorphism m) where
  arrow f = Kleisli (pure . f)
  first (Kleisli f) =  Kleisli $ \(a, b) => do x <- f a
                                               pure (x, b)

  second (Kleisli f) = Kleisli $ \(a, b) => do x <- f b
                                               pure (a, x)

  (Kleisli f) *** (Kleisli g) = Kleisli $ \(a, b) => do x <- f a
                                                        y <- g b
                                                        pure (x, y)

  (Kleisli f) &&& (Kleisli g) = Kleisli $ \a => do x <- f a
                                                   y <- g a
                                                   pure (x, y)

public export
interface Arrow arr => ArrowZero (0 arr : Type -> Type -> Type) where
  zeroArrow : arr a b

public export
interface ArrowZero arr => ArrowPlus (0 arr : Type -> Type -> Type) where
  (<++>) : arr a b -> arr a b -> arr a b

public export
interface Arrow arr => ArrowChoice (0 arr : Type -> Type -> Type) where
  left  : arr a b -> arr (Either a c) (Either b c)

  right : arr a b -> arr (Either c a) (Either c b)
  right f = arrow mirror >>> left f >>> arrow mirror

  (+++) : arr a b -> arr c d -> arr (Either a c) (Either b d)
  f +++ g = left f >>> right g

  (\|/) : arr a b -> arr c b -> arr (Either a c) b
  f \|/ g = f +++ g >>> arrow fromEither
    where
    fromEither : Either b b -> b
    fromEither (Left b) = b
    fromEither (Right b) = b

public export
implementation Monad m => ArrowChoice (Kleislimorphism m) where
  left f                      = f          +++ (arrow id)
  right f                     = (arrow id) +++ f
  f           +++ g           = (f >>> (arrow Left)) \|/ (g >>> (arrow Right))
  (Kleisli f) \|/ (Kleisli g) = Kleisli (either f g)

public export
interface Arrow arr => ArrowApply (0 arr : Type -> Type -> Type) where
  app : arr (arr a b, a) b

public export
implementation Monad m => ArrowApply (Kleislimorphism m) where
  app = Kleisli $ \(Kleisli f, x) => f x

public export
data ArrowMonad : (Type -> Type -> Type) -> Type -> Type where
  MkArrowMonad : (runArrowMonad : arr (the Type ()) a) -> ArrowMonad arr a

public export
runArrowMonad : ArrowMonad arr a -> arr (the Type ()) a
runArrowMonad (MkArrowMonad a) = a

public export
implementation Arrow a => Functor (ArrowMonad a) where
  map f (MkArrowMonad m) = MkArrowMonad $ m >>> arrow f

public export
implementation Arrow a => Applicative (ArrowMonad a) where
  pure x = MkArrowMonad $ arrow $ \_ => x
  (MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)

public export
implementation ArrowApply a => Monad (ArrowMonad a) where
  (MkArrowMonad m) >>= f =
    MkArrowMonad $ m >>> (arrow $ \x => (runArrowMonad (f x), ())) >>> app

public export
interface Arrow arr => ArrowLoop (0 arr : Type -> Type -> Type) where
  loop : arr (Pair a c) (Pair b c) -> arr a b

||| Applying a binary operator to the results of two arrow computations.
public export
liftA2 : Arrow arr => (a -> b -> c) -> arr d a -> arr d b -> arr d c
liftA2 op f g = (f &&& g) >>> arrow (\(a, b) => a `op` b)


text:
module Idris.REPL

import Compiler.Scheme.Chez
import Compiler.Scheme.ChezSep
import Compiler.Scheme.Racket
import Compiler.Scheme.Gambit
import Compiler.ES.Node
import Compiler.ES.Javascript
import Compiler.Common
import Compiler.RefC.RefC
import Compiler.Jvm.Codegen
import Compiler.Inline

import Core.AutoSearch
import Core.CaseTree
import Core.CompileExpr
import Core.Context
import Core.Context.Log
import Core.Directory
import Core.Env
import Core.FC
import Core.InitPrimitives
import Core.LinearCheck
import Core.Metadata
import Core.Normalise
import Core.Options
import Core.TT
import Core.Termination
import Core.Unify
import Core.Value

import Parser.Unlit

import Idris.Desugar
import Idris.Doc.String
import Idris.Error
import Idris.IDEMode.CaseSplit
import Idris.IDEMode.Commands
import Idris.IDEMode.MakeClause
import Idris.IDEMode.Holes
import Idris.ModTree
import Idris.Parser
import Idris.Pretty
import Idris.ProcessIdr
import Idris.Resugar
import Idris.Syntax
import Idris.Version

import public Idris.REPL.Common
import Idris.REPL.FuzzySearch

import TTImp.TTImp.Functor
import TTImp.Elab
import TTImp.Elab.Check
import TTImp.Elab.Local
import TTImp.Interactive.CaseSplit
import TTImp.Interactive.ExprSearch
import TTImp.Interactive.GenerateDef
import TTImp.Interactive.MakeLemma
import TTImp.TTImp
import TTImp.BindImplicits
import TTImp.ProcessDecls

import Data.List
import Data.List1
import Data.Maybe
import Libraries.Data.ANameMap
import Libraries.Data.NameMap
import Libraries.Data.PosMap
import Data.Stream
import Data.String
import Data.DPair
import Libraries.Data.String.Extra
import Libraries.Data.List.Extra
import Libraries.Text.PrettyPrint.Prettyprinter
import Libraries.Text.PrettyPrint.Prettyprinter.Util
import Libraries.Text.PrettyPrint.Prettyprinter.Render.Terminal
import Libraries.Utils.Path
import Libraries.System.Directory.Tree

import System
import System.File
import System.Directory

%hide Data.String.lines
%hide Data.String.lines'
%hide Data.String.unlines
%hide Data.String.unlines'

%default covering

showInfo : {auto c : Ref Ctxt Defs} ->
           (Name, Int, GlobalDef) -> Core ()
showInfo (n, idx, d)
    = do coreLift_ $ putStrLn (show (fullname d) ++ " ==> " ++
                              show !(toFullNames (definition d)))
         coreLift_ $ putStrLn (show (multiplicity d))
         coreLift_ $ putStrLn ("Erasable args: " ++ show (eraseArgs d))
         coreLift_ $ putStrLn ("Detaggable arg types: " ++ show (safeErase d))
         coreLift_ $ putStrLn ("Specialise args: " ++ show (specArgs d))
         coreLift_ $ putStrLn ("Inferrable args: " ++ show (inferrable d))
         whenJust (compexpr d) $ \ expr =>
           coreLift_ $ putStrLn ("Compiled: " ++ show expr)
         coreLift_ $ putStrLn ("Refers to: " ++
                               show !(traverse getFullName (keys (refersTo d))))
         coreLift_ $ putStrLn ("Refers to (runtime): " ++
                               show !(traverse getFullName (keys (refersToRuntime d))))
         coreLift_ $ putStrLn ("Flags: " ++ show (flags d))
         when (not (isNil (sizeChange d))) $
            let scinfo = map (\s => show (fnCall s) ++ ": " ++
                                    show (fnArgs s)) !(traverse toFullNames (sizeChange d)) in
                coreLift_ $ putStrLn $
                        "Size change: " ++ showSep ", " scinfo

prettyTerm : IPTerm -> Doc IdrisAnn
prettyTerm = reAnnotate Syntax . Idris.Pretty.prettyTerm

displayType : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> (Name, Int, GlobalDef) ->
              Core (Doc IdrisAnn)
displayType defs (n, i, gdef)
    = maybe (do tm <- resugar [] !(normaliseHoles defs [] (type gdef))
                nm <- aliasName (fullname gdef)
                let ann = showCategory Syntax gdef
                pure (ann (pretty nm) <++> colon <++> prettyTerm tm))
            (\num => reAnnotate Syntax <$> prettyHole defs [] n num (type gdef))
            (isHole gdef)

getEnvTerm : {vars : _} ->
             List Name -> Env Term vars -> Term vars ->
             (vars' ** (Env Term vars', Term vars'))
getEnvTerm (n :: ns) env (Bind fc x b sc)
    = if n == x
         then getEnvTerm ns (b :: env) sc
         else (_ ** (env, Bind fc x b sc))
getEnvTerm _ env tm = (_ ** (env, tm))

displayTerm : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> ClosedTerm ->
              Core (Doc IdrisAnn)
displayTerm defs tm
    = do ptm <- resugar [] !(normaliseHoles defs [] tm)
         pure (prettyTerm ptm)

displayPatTerm : {auto c : Ref Ctxt Defs} ->
                 {auto s : Ref Syn SyntaxInfo} ->
                 Defs -> ClosedTerm ->
                 Core String
displayPatTerm defs tm
    = do ptm <- resugarNoPatvars [] !(normaliseHoles defs [] tm)
         pure (show ptm)

displayClause : {auto c : Ref Ctxt Defs} ->
                {auto s : Ref Syn SyntaxInfo} ->
                Defs -> (vs ** (Env Term vs, Term vs, Term vs)) ->
                Core (Doc IdrisAnn)
displayClause defs (vs ** (env, lhs, rhs))
    = do lhstm <- resugar env !(normaliseHoles defs env lhs)
         rhstm <- resugar env !(normaliseHoles defs env rhs)
         pure (prettyTerm lhstm <++> equals <++> prettyTerm rhstm)

displayPats : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Defs -> (Name, Int, GlobalDef) ->
              Core (Doc IdrisAnn)
displayPats defs (n, idx, gdef)
    = case definition gdef of
           PMDef _ _ _ _ pats
               => do ty <- displayType defs (n, idx, gdef)
                     ps <- traverse (displayClause defs) pats
                     pure (vsep (ty :: ps))
           _ => pure (pretty n <++> reflow "is not a pattern matching definition")

setOpt : {auto c : Ref Ctxt Defs} ->
         {auto o : Ref ROpts REPLOpts} ->
         REPLOpt -> Core ()
setOpt (ShowImplicits t)
    = do pp <- getPPrint
         setPPrint (record { showImplicits = t } pp)
setOpt (ShowNamespace t)
    = do pp <- getPPrint
         setPPrint (record { fullNamespace = t } pp)
setOpt (ShowTypes t)
    = do opts <- get ROpts
         put ROpts (record { showTypes = t } opts)
setOpt (EvalMode m)
    = do opts <- get ROpts
         put ROpts (record { evalMode = m } opts)
setOpt (Editor e)
    = do opts <- get ROpts
         put ROpts (record { editor = e } opts)
setOpt (CG e)
    = do defs <- get Ctxt
         case getCG (options defs) e of
            Just cg => setCG cg
            Nothing => iputStrLn (reflow "No such code generator available")
setOpt (Profile t)
    = do pp <- getSession
         setSession (record { profile = t } pp)

getOptions : {auto c : Ref Ctxt Defs} ->
         {auto o : Ref ROpts REPLOpts} ->
         Core (List REPLOpt)
getOptions = do
  pp <- getPPrint
  opts <- get ROpts
  pure $ [ ShowImplicits (showImplicits pp), ShowNamespace (fullNamespace pp)
         , ShowTypes (showTypes opts), EvalMode (evalMode opts)
         , Editor (editor opts)
         ]

anyAt : (a -> Bool) -> a -> b -> Bool
anyAt p loc _ = p loc

printClause : {auto c : Ref Ctxt Defs} ->
              {auto s : Ref Syn SyntaxInfo} ->
              Maybe String -> Nat -> ImpClause ->
              Core String
printClause l i (PatClause _ lhsraw rhsraw)
    = do lhs <- pterm $ map defaultKindedName lhsraw -- hack
         rhs <- pterm $ map defaultKindedName rhsraw -- hack
         pure (relit l (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs))
printClause l i (WithClause _ lhsraw wvraw prf flags csraw)
    = do lhs <- pterm $ map defaultKindedName lhsraw -- hack
         wval <- pterm $ map defaultKindedName wvraw -- hack
         cs <- traverse (printClause l (i + 2)) csraw
         pure (relit l ((pack (replicate i ' ')
                ++ show lhs
                ++ " with (" ++ show wval ++ ")"
                ++ maybe "" (\ nm => " proof " ++ show nm) prf
                ++ "\n"))
               ++ showSep "\n" cs)
printClause l i (ImpossibleClause _ lhsraw)
    = do lhs <- pterm $ map defaultKindedName lhsraw -- hack
         pure (relit l (pack (replicate i ' ') ++ show lhs ++ " impossible"))

lookupDefTyName : Name -> Context ->
                  Core (List (Name, Int, (Def, ClosedTerm)))
lookupDefTyName = lookupNameBy (\g => (definition g, type g))

updateFile : {auto r : Ref ROpts REPLOpts} ->
             (List String -> List String) -> Core EditResult
updateFile update
    = do opts <- get ROpts
         let Just f = mainfile opts
             | Nothing => pure (DisplayEdit emptyDoc) -- no file, nothing to do
         Right content <- coreLift $ readFile f
               | Left err => throw (FileErr f err)
         coreLift_ $ writeFile (f ++ "~") content
         coreLift_ $ writeFile f (unlines (update (forget $ lines content)))
         pure (DisplayEdit emptyDoc)

rtrim : String -> String
rtrim str = reverse (ltrim (reverse str))

addClause : String -> Nat -> List String -> List String
addClause c Z [] = rtrim c :: []
addClause c Z (x :: xs)
    = if all isSpace (unpack x)
         then rtrim c :: x :: xs
         else x :: addClause c Z xs
addClause c (S k) (x :: xs) = x :: addClause c k xs
addClause c (S k) [] = [c]

caseSplit : String -> Nat -> List String -> List String
caseSplit c Z (x :: xs) = rtrim c :: xs
caseSplit c (S k) (x :: xs) = x :: caseSplit c k xs
caseSplit c _ [] = [c]

proofSearch : Name -> String -> Nat -> List String -> List String
proofSearch n res Z (x :: xs) = replaceStr ("?" ++ show n) res x :: xs
  where
    replaceStr : String -> String -> String -> String
    replaceStr rep new "" = ""
    replaceStr rep new str
        = if isPrefixOf rep str
             then new ++ pack (drop (length rep) (unpack str))
             else assert_total $ strCons (prim__strHead str)
                          (replaceStr rep new (prim__strTail str))
proofSearch n res (S k) (x :: xs) = x :: proofSearch n res k xs
proofSearch n res _ [] = []

addMadeLemma : Maybe String -> Name -> String -> String -> Nat -> List String -> List String
addMadeLemma lit n ty app line content
    = addApp lit line [] (proofSearch n app line content)
  where
    -- Put n : ty in the first blank line
    insertInBlank : Maybe String -> List String -> List String
    insertInBlank lit [] = [relit lit $ show n ++ " : " ++ ty ++ "\n"]
    insertInBlank lit (x :: xs)
        = if trim x == ""
             then ("\n" ++ (relit lit $ show n ++ " : " ++ ty ++ "\n")) :: xs
             else x :: insertInBlank lit xs

    addApp : Maybe String -> Nat -> List String -> List String -> List String
    addApp lit Z acc rest = reverse (insertInBlank lit acc) ++ rest
    addApp lit (S k) acc (x :: xs) = addApp lit k (x :: acc) xs
    addApp _ (S k) acc [] = reverse acc

-- Replace a line; works for 'case' and 'with'
addMadeCase : Maybe String -> List String -> Nat -> List String -> List String
addMadeCase lit wapp line content
    = addW line [] content
  where
    addW : Nat -> List String -> List String -> List String
    addW Z acc (_ :: rest) = reverse acc ++ map (relit lit) wapp ++ rest
    addW Z acc [] = [] -- shouldn't happen!
    addW (S k) acc (x :: xs) = addW k (x :: acc) xs
    addW (S k) acc [] = reverse acc

nextProofSearch : {auto c : Ref Ctxt Defs} ->
                  {auto u : Ref UST UState} ->
                  {auto o : Ref ROpts REPLOpts} ->
                  Core (Maybe (Name, RawImp))
nextProofSearch
    = do opts <- get ROpts
         let Just (n, res) = psResult opts
              | Nothing => pure Nothing
         Just (res, next) <- nextResult res
              | Nothing =>
                    do put ROpts (record { psResult = Nothing } opts)
                       pure Nothing
         put ROpts (record { psResult = Just (n, next) } opts)
         pure (Just (n, res))

nextGenDef : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto o : Ref ROpts REPLOpts} ->
             (reject : Nat) ->
             Core (Maybe (Int, (FC, List ImpClause)))
nextGenDef reject
    = do opts <- get ROpts
         let Just (line, res) = gdResult opts
              | Nothing => pure Nothing
         Just (res, next) <- nextResult res
              | Nothing =>
                    do put ROpts (record { gdResult = Nothing } opts)
                       pure Nothing
         put ROpts (record { gdResult = Just (line, next) } opts)
         case reject of
              Z => pure (Just (line, res))
              S k => nextGenDef k

dropLams : Nat -> RawImp' nm -> RawImp' nm
dropLams Z tm = tm
dropLams (S k) (ILam _ _ _ _ _ sc) = dropLams k sc
dropLams _ tm = tm

dropLamsTm : {vars : _} ->
             Nat -> Env Term vars -> Term vars ->
             (vars' ** (Env Term vars', Term vars'))
dropLamsTm Z env tm = (_ ** (env, tm))
dropLamsTm (S k) env (Bind _ _ b sc) = dropLamsTm k (b :: env) sc
dropLamsTm _ env tm = (_ ** (env, tm))

findInTree : FilePos -> Name -> PosMap (NonEmptyFC, Name) -> Maybe Name
findInTree p hint m = map snd $ head' $ filter match $ sortBy (\x, y => cmp (measure x) (measure y)) $ searchPos p m
  where
    cmp : FileRange -> FileRange -> Ordering
    cmp ((sr1, sc1), (er1, ec1)) ((sr2, sc2), (er2, ec2)) =
      compare (er1 - sr1, ec1 - sc1) (er2 - sr2, ec2 - sc2)

    match : (NonEmptyFC, Name) -> Bool
    match (_, n) = matches hint n && userNameRoot n == userNameRoot hint

processEdit : {auto c : Ref Ctxt Defs} ->
              {auto u : Ref UST UState} ->
              {auto s : Ref Syn SyntaxInfo} ->
              {auto m : Ref MD Metadata} ->
              {auto o : Ref ROpts REPLOpts} ->
              EditCmd -> Core EditResult
processEdit (TypeAt line col name)
    = do defs <- get Ctxt
         meta <- get MD

         -- Search the correct name by location for more precise search
         -- and fallback to given name if nothing found
         let name = fromMaybe name $ findInTree (line - 1, col - 1) name (nameLocMap meta)

         -- Lookup the name globally
         globals <- lookupCtxtName name (gamma defs)

         -- Get the Doc for the result
         globalResult <- case globals of
           [] => pure Nothing
           ts => do tys <- traverse (displayType defs) ts
                    pure $ Just (vsep tys)

         -- Lookup the name locally (The name at the specified position)
         localResult <- findTypeAt $ anyAt $ within (line-1, col-1)

         case (globalResult, localResult) of
              -- Give precedence to the local name, as it shadows the others
              (_, Just (n, _, type)) => pure $ DisplayEdit $
                pretty (nameRoot n) <++> colon <++> !(displayTerm defs type)
              (Just globalDoc, Nothing) => pure $ DisplayEdit $ globalDoc
              (Nothing, Nothing) => undefinedName replFC name

processEdit (CaseSplit upd line col name)
    = do let find = if col > 0
                       then within (line-1, col-1)
                       else onLine (line-1)
         OK splits <- getSplits (anyAt find) name
             | SplitFail err => pure (EditError (pretty $ show err))
         lines <- updateCase splits (line-1) (col-1)
         if upd
            then updateFile (caseSplit (unlines lines) (integerToNat (cast (line - 1))))
            else pure $ DisplayEdit (vsep $ pretty <$> lines)
processEdit (AddClause upd line name)
    = do Just c <- getClause line name
             | Nothing => pure (EditError (pretty name <++> reflow "not defined here"))
         if upd
            then updateFile (addClause c (integerToNat (cast line)))
            else pure $ DisplayEdit (pretty c)
processEdit (ExprSearch upd line name hints)
    = do defs <- get Ctxt
         syn <- get Syn
         let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
         case !(lookupDefName name (gamma defs)) of
              [(n, nidx, Hole locs _)] =>
                  do let searchtm = exprSearch replFC name []
                     ropts <- get ROpts
                     put ROpts (record { psResult = Just (name, searchtm) } ropts)
                     defs <- get Ctxt
                     Just (_, restm) <- nextProofSearch
                          | Nothing => pure $ EditError "No search results"
                     let tm' = dropLams locs restm
                     itm <- pterm $ map defaultKindedName tm' -- hack
                     let itm'  = ifThenElse brack (addBracket replFC itm) itm
                     if upd
                        then updateFile (proofSearch name (show itm') (integerToNat (cast (line - 1))))
                        else pure $ DisplayEdit (prettyTerm itm')
              [(n, nidx, PMDef pi [] (STerm _ tm) _ _)] =>
                  case holeInfo pi of
                       NotHole => pure $ EditError "Not a searchable hole"
                       SolvedHole locs =>
                          do let (_ ** (env, tm')) = dropLamsTm locs [] !(normaliseHoles defs [] tm)
                             itm <- resugar env tm'
                             let itm'= ifThenElse brack (addBracket replFC itm) itm
                             if upd
                                then updateFile (proofSearch name (show itm') (integerToNat (cast (line - 1))))
                                else pure $ DisplayEdit (prettyTerm itm')
              [] => pure $ EditError $ "Unknown name" <++> pretty name
              _ => pure $ EditError "Not a searchable hole"
processEdit ExprSearchNext
    = do defs <- get Ctxt
         syn <- get Syn
         Just (name, restm) <- nextProofSearch
              | Nothing => pure $ EditError "No more results"
         [(n, nidx, Hole locs _)] <- lookupDefName name (gamma defs)
              | _ => pure $ EditError "Not a searchable hole"
         let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
         let tm' = dropLams locs restm
         itm <- pterm $ map defaultKindedName tm'
         let itm' = ifThenElse brack (addBracket replFC itm) itm
         pure $ DisplayEdit (prettyTerm itm')

processEdit (GenerateDef upd line name rej)
    = do defs <- get Ctxt
         Just (_, n', _, _) <- findTyDeclAt (\p, n => onLine (line - 1) p)
             | Nothing => pure (EditError ("Can't find declaration for" <++> pretty name <++> "on line" <++> pretty line))
         case !(lookupDefExact n' (gamma defs)) of
              Just None =>
                 do let searchdef = makeDefSort (\p, n => onLine (line - 1) p)
                                                16 mostUsed n'
                    ropts <- get ROpts
                    put ROpts (record { gdResult = Just (line, searchdef) } ropts)
                    Just (_, (fc, cs)) <- nextGenDef rej
                         | Nothing => pure (EditError "No search results")

                    let l : Nat = integerToNat $ cast $ startCol (toNonEmptyFC fc)

                    Just srcLine <- getSourceLine line
                       | Nothing => pure (EditError "Source line not found")
                    let (markM, srcLineUnlit) = isLitLine srcLine
                    ls <- traverse (printClause markM l) cs
                    if upd
                       then updateFile (addClause (unlines ls) (integerToNat (cast line)))
                       else pure $ DisplayEdit (vsep $ pretty <$> ls)
              Just _ => pure $ EditError "Already defined"
              Nothing => pure $ EditError $ "Can't find declaration for" <++> pretty name
processEdit GenerateDefNext
    = do Just (line, (fc, cs)) <- nextGenDef 0
              | Nothing => pure (EditError "No more results")
         let l : Nat = integerToNat $ cast $ startCol (toNonEmptyFC fc)
         Just srcLine <- getSourceLine line
            | Nothing => pure (EditError "Source line not found")
         let (markM, srcLineUnlit) = isLitLine srcLine
         ls <- traverse (printClause markM l) cs
         pure $ DisplayEdit (vsep $ pretty <$> ls)
processEdit (MakeLemma upd line name)
    = do defs <- get Ctxt
         syn <- get Syn
         let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
         case !(lookupDefTyName name (gamma defs)) of
              [(n, nidx, Hole locs _, ty)] =>
                  do (lty, lapp) <- makeLemma replFC name locs ty
                     pty <- pterm $ map defaultKindedName lty -- hack
                     papp <- pterm $ map defaultKindedName lapp -- hack
                     opts <- get ROpts
                     let pappstr = show (ifThenElse brack
                                            (addBracket replFC papp)
                                            papp)
                     Just srcLine <- getSourceLine line
                       | Nothing => pure (EditError "Source line not found")
                     let (markM,_) = isLitLine srcLine
                     if upd
                        then updateFile (addMadeLemma markM name (show pty) pappstr
                                                      (max 0 (integerToNat (cast (line - 1)))))
                        else pure $ MadeLemma markM name pty pappstr
              _ => pure $ EditError "Can't make lifted definition"
processEdit (MakeCase upd line name)
    = do litStyle <- getLitStyle
         syn <- get Syn
         let brack = elemBy (\x, y => dropNS x == dropNS y) name (bracketholes syn)
         Just src <- getSourceLine line
              | Nothing => pure (EditError "Source line not available")
         let Right l = unlit litStyle src
              | Left err => pure (EditError "Invalid literate Idris")
         let (markM, _) = isLitLine src
         let c = forget $ lines $ makeCase brack name l
         if upd
            then updateFile (addMadeCase markM c (max 0 (integerToNat (cast (line - 1)))))
            else pure $ MadeCase markM c
processEdit (MakeWith upd line name)
    = do litStyle <- getLitStyle
         Just src <- getSourceLine line
              | Nothing => pure (EditError "Source line not available")
         let Right l = unlit litStyle src
              | Left err => pure (EditError "Invalid literate Idris")
         let (markM, _) = isLitLine src
         let w = forget $ lines $ makeWith name l
         if upd
            then updateFile (addMadeCase markM w (max 0 (integerToNat (cast (line - 1)))))
            else pure $ MadeWith markM w

getItDecls :
    {auto o : Ref ROpts REPLOpts} ->
    Core (List ImpDecl)
getItDecls
    = do opts <- get ROpts
         case evalResultName opts of
            Nothing => pure []
            Just n =>
              let it = UN $ Basic "it" in
              pure [ IClaim replFC top Private [] (MkImpTy replFC EmptyFC it (Implicit replFC False))
                  , IDef replFC it [PatClause replFC (IVar replFC it) (IVar replFC n)]]

prepareExp :
    {auto c : Ref Ctxt Defs} ->
    {auto u : Ref UST UState} ->
    {auto s : Ref Syn SyntaxInfo} ->
    {auto m : Ref MD Metadata} ->
    {auto o : Ref ROpts REPLOpts} ->
    PTerm -> Core ClosedTerm
prepareExp ctm
    = do ttimp <- desugar AnyExpr [] (PApp replFC (PRef replFC (UN $ Basic "unsafePerformIO")) ctm)
         let ttimpWithIt = ILocal replFC !getItDecls ttimp
         inidx <- resolveName (UN $ Basic "[input]")
         (tm, ty) <- elabTerm inidx InExpr [] (MkNested [])
                                 [] ttimpWithIt Nothing
         tm_erased <- linearCheck replFC linear True [] tm
         compileAndInlineAll
         pure tm_erased

processLocal : {vars : _} ->
             {auto c : Ref Ctxt Defs} ->
             {auto m : Ref MD Metadata} ->
             {auto u : Ref UST UState} ->
             {auto e : Ref EST (EState vars)} ->
             List ElabOpt ->
             NestedNames vars -> Env Term vars ->
             List ImpDecl -> (scope : List ImpDecl) ->
             Core ()
processLocal {vars} eopts nest env nestdecls_in scope
    = localHelper nest env nestdecls_in $ \nest' => traverse_ (processDecl eopts nest' env) scope

export
execExp : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto m : Ref MD Metadata} ->
          {auto o : Ref ROpts REPLOpts} ->
          PTerm -> Core REPLResult
execExp ctm
    = do tm_erased <- prepareExp ctm
         Just cg <- findCG
              | Nothing =>
                   do iputStrLn (reflow "No such code generator available")
                      pure CompilationFailed
         execute cg tm_erased
         pure $ Executed ctm

execDecls : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto m : Ref MD Metadata} ->
            {auto o : Ref ROpts REPLOpts} ->
            List PDecl -> Core REPLResult
execDecls decls = do
  traverse_ execDecl decls
  pure DefDeclared
  where
    execDecl : PDecl -> Core ()
    execDecl decl = do
      i <- desugarDecl [] decl
      inidx <- resolveName (UN $ Basic "[defs]")
      _ <- newRef EST (initEStateSub inidx [] SubRefl)
      processLocal [] (MkNested []) [] !getItDecls i

export
compileExp : {auto c : Ref Ctxt Defs} ->
             {auto u : Ref UST UState} ->
             {auto s : Ref Syn SyntaxInfo} ->
             {auto m : Ref MD Metadata} ->
             {auto o : Ref ROpts REPLOpts} ->
             PTerm -> String -> Core REPLResult
compileExp ctm outfile
    = do tm_erased <- prepareExp ctm
         Just cg <- findCG
              | Nothing =>
                   do iputStrLn (reflow "No such code generator available")
                      pure CompilationFailed
         ok <- compile cg tm_erased outfile
         maybe (pure CompilationFailed)
               (pure . Compiled)
               ok

export
loadMainFile : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto m : Ref MD Metadata} ->
               {auto o : Ref ROpts REPLOpts} ->
               String -> Core REPLResult
loadMainFile f
    = do opts <- get ROpts
         put ROpts (record { evalResultName = Nothing } opts)
         modIdent <- ctxtPathToNS f
         resetContext (PhysicalIdrSrc modIdent)
         Right res <- coreLift (readFile f)
            | Left err => do setSource ""
                             pure (ErrorLoadingFile f err)
         errs <- logTime "+ Build deps" $ buildDeps f
         updateErrorLine errs
         setSource res
         resetProofState
         case errs of
           [] => pure (FileLoaded f)
           _ => pure (ErrorsBuildingFile f errs)

||| Given a REPLEval mode for evaluation,
||| produce the normalization function that normalizes terms
||| using that evaluation mode
replEval : {auto c : Ref Ctxt Defs} ->
  {vs : _} ->
  REPLEval -> Defs -> Env Term vs -> Term vs -> Core (Term vs)
replEval NormaliseAll = normaliseOpts (record { strategy = CBV } withAll)
replEval _ = normalise

record TermWithType where
  constructor WithType
  termOf : Term []
  typeOf : Term []

||| Produce the elaboration of a PTerm, along with its inferred type
inferAndElab : {auto c : Ref Ctxt Defs} ->
  {auto u : Ref UST UState} ->
  {auto s : Ref Syn SyntaxInfo} ->
  {auto m : Ref MD Metadata} ->
  {auto o : Ref ROpts REPLOpts} ->
  ElabMode ->
  PTerm ->
  Core TermWithType
inferAndElab emode itm
  = do ttimp <- desugar AnyExpr [] itm
       let ttimpWithIt = ILocal replFC !getItDecls ttimp
       inidx <- resolveName (UN $ Basic "[input]")
       -- a TMP HACK to prioritise list syntax for List: hide
       -- foreign argument lists. TODO: once the new FFI is fully
       -- up and running we won't need this. Also, if we add
       -- 'with' disambiguation we can use that instead.
       catch (do hide replFC (NS primIONS (UN $ Basic "::"))
                 hide replFC (NS primIONS (UN $ Basic "Nil")))
             (\err => pure ())
       (tm , gty) <- elabTerm inidx emode [] (MkNested [])
                   [] ttimpWithIt Nothing
       ty <- getTerm gty
       pure (tm `WithType` ty)

||| Produce the normal form of a PTerm, along with its inferred type
inferAndNormalize : {auto c : Ref Ctxt Defs} ->
  {auto u : Ref UST UState} ->
  {auto s : Ref Syn SyntaxInfo} ->
  {auto m : Ref MD Metadata} ->
  {auto o : Ref ROpts REPLOpts} ->
  REPLEval ->
  PTerm ->
  Core TermWithType
inferAndNormalize emode itm
  = do (tm `WithType` ty) <- inferAndElab (elabMode emode) itm
       logTerm "repl.eval" 10 "Elaborated input" tm
       defs <- get Ctxt
       let norm = replEval emode
       ntm <- norm defs [] tm
       logTermNF "repl.eval" 5 "Normalised" [] ntm
       pure $ ntm `WithType` ty
  where
    elabMode : REPLEval -> ElabMode
    elabMode EvalTC = InType
    elabMode _ = InExpr

||| Process a single `REPLCmd`
|||
||| Returns `REPLResult` for display by the higher level shell which
||| is invoking this interactive command processing.
export
process : {auto c : Ref Ctxt Defs} ->
          {auto u : Ref UST UState} ->
          {auto s : Ref Syn SyntaxInfo} ->
          {auto m : Ref MD Metadata} ->
          {auto o : Ref ROpts REPLOpts} ->
          REPLCmd -> Core REPLResult
process (NewDefn decls) = execDecls decls
process (Eval itm)
    = do opts <- get ROpts
         let emode = evalMode opts
         case emode of
            Execute => do ignore (execExp itm); pure (Executed itm)
            _ =>
              do
                 (ntm `WithType` ty) <- inferAndNormalize emode itm
                 itm <- resugar [] ntm
                 defs <- get Ctxt
                 opts <- get ROpts
                 let norm = replEval emode
                 evalResultName <- DN "it" <$> genName "evalResult"
                 ignore $ addDef evalResultName
                   $ newDef replFC evalResultName top [] ty Private
                   $ PMDef defaultPI [] (STerm 0 ntm) (STerm 0 ntm) []
                 addToSave evalResultName
                 put ROpts (record { evalResultName = Just evalResultName } opts)
                 if showTypes opts
                    then do ity <- resugar [] !(norm defs [] ty)
                            pure (Evaluated itm (Just ity))
                    else pure (Evaluated itm Nothing)
process (Check (PRef fc (UN (Basic "it"))))
    = do opts <- get ROpts
         case evalResultName opts of
              Nothing => throw (UndefinedName fc (UN $ Basic "it"))
              Just n => process (Check (PRef fc n))
process (Check (PRef fc fn))
    = do defs <- get Ctxt
         case !(lookupCtxtName fn (gamma defs)) of
              [] => undefinedName fc fn
              ts => do tys <- traverse (displayType defs) ts
                       pure (Printed $ vsep tys)
process (Check itm)
    = do (tm `WithType` ty) <- inferAndElab InExpr itm
         defs <- get Ctxt
         itm <- resugar [] !(normaliseHoles defs [] tm)
         -- ty <- getTerm gty
         ity <- resugar [] !(normaliseScope defs [] ty)
         pure (TermChecked itm ity)
process (CheckWithImplicits itm)
    = do showImplicits <- showImplicits <$> getPPrint
         setOpt (ShowImplicits True)
         result <- process (Check itm)
         setOpt (ShowImplicits showImplicits)
         pure result
process (PrintDef fn)
    = do defs <- get Ctxt
         case !(lookupCtxtName fn (gamma defs)) of
              [] => undefinedName replFC fn
              ts => do defs <- traverse (displayPats defs) ts
                       pure (Printed $ vsep defs)
process Reload
    = do opts <- get ROpts
         case mainfile opts of
              Nothing => pure NoFileLoaded
              Just f => loadMainFile f
process (Load f)
    = do opts <- get ROpts
         put ROpts (record { mainfile = Just f } opts)
         -- Clear the context and load again
         loadMainFile f
process (ImportMod m)
    = do catch (do addImport (MkImport emptyFC False m (miAsNamespace m))
                   pure $ ModuleLoaded (show m))
               (\err => pure $ ErrorLoadingModule (show m) err)
process (CD dir)
    = do setWorkingDir dir
         workDir <- getWorkingDir
         pure (CurrentDirectory workDir)
process CWD
    = do workDir <- getWorkingDir
         pure (CurrentDirectory workDir)
process Edit
    = do opts <- get ROpts
         case mainfile opts of
              Nothing => pure NoFileLoaded
              Just f =>
                do let line = maybe "" (\i => " +" ++ show (i + 1)) (errorLine opts)
                   coreLift_ $ system (editor opts ++ " \"" ++ f ++ "\"" ++ line)
                   loadMainFile f
process (Compile ctm outfile)
    = compileExp ctm outfile
process (Exec ctm)
    = execExp ctm
process Help
    = pure RequestedHelp
process (TypeSearch searchTerm)
    = do defs <- branch
         let curr = currentNS defs
         let ctxt = gamma defs
         rawTy <- desugar AnyExpr [] searchTerm
         bound <- piBindNames replFC [] rawTy
         (ty, _) <- elabTerm 0 InType [] (MkNested []) [] bound Nothing
         ty' <- toResolvedNames ty
         filteredDefs <-
           do names   <- allNames ctxt
              defs    <- traverse (flip lookupCtxtExact ctxt) names
              let defs = flip mapMaybe defs $ \ md =>
                             do d <- md
                                guard (visibleIn curr (fullname d) (visibility d))
                                guard (isJust $ userNameRoot (fullname d))
                                pure d
              allDefs <- traverse (resolved ctxt) defs
              filterM (\def => equivTypes def.type ty') allDefs
         put Ctxt defs
         doc <- traverse (docsOrSignature replFC) $ fullname <$> filteredDefs
         pure $ PrintedDoc $ vsep doc
process (Missing n)
    = do defs <- get Ctxt
         case !(lookupCtxtName n (gamma defs)) of
              [] => undefinedName replFC n
              ts => map Missed $ traverse (\fn =>
                                         do tot <- getTotality replFC fn
                                            case isCovering tot of
                                                 MissingCases cs =>
                                                    do tms <- traverse (displayPatTerm defs) cs
                                                       pure $ CasesMissing fn tms
                                                 NonCoveringCall ns_in =>
                                                   do ns <- traverse getFullName ns_in
                                                      pure $ CallsNonCovering fn ns
                                                 _ => pure $ AllCasesCovered fn)
                               (map fst ts)
process (Total n)
    = do defs <- get Ctxt
         case !(lookupCtxtName n (gamma defs)) of
              [] => undefinedName replFC n
              ts => map CheckedTotal $
                    traverse (\fn =>
                          do ignore $ checkTotal replFC fn
                             tot <- getTotality replFC fn >>= toFullNames
                             pure $ (fn, tot))
                               (map fst ts)
process (Doc itm)
    = do doc <- getDocsForPTerm itm
         pure $ PrintedDoc doc
process (Browse ns)
    = do doc <- getContents ns
         pure $ PrintedDoc doc
process (DebugInfo n)
    = do defs <- get Ctxt
         traverse_ showInfo !(lookupCtxtName n (gamma defs))
         pure Done
process (SetOpt opt)
    = do setOpt opt
         pure Done
process GetOpts
    = do opts <- getOptions
         pure $ OptionsSet opts
process (SetLog lvl)
    = do addLogLevel lvl
         pure $ LogLevelSet lvl
process (SetConsoleWidth n)
    = do setConsoleWidth n
         pure $ ConsoleWidthSet n
process (SetColor b)
    = do setColor b
         pure $ ColorSet b
process Metavars
    = do defs <- get Ctxt
         let ctxt = gamma defs
         ms  <- getUserHoles
         let globs = concat !(traverse (\n => lookupCtxtName n ctxt) ms)
         let holesWithArgs = mapMaybe (\(n, i, gdef) => do args <- isHole gdef
                                                           pure (n, gdef, args))
                                      globs
         hData <-
             traverse (\n_gdef_args =>
                        -- Inference can't deal with this for now :/
                        let (n, gdef, args) = the (Name, GlobalDef, Nat) n_gdef_args in
                        holeData defs [] n args (type gdef))
                      holesWithArgs
         pure $ FoundHoles hData

process (Editing cmd)
    = do ppopts <- getPPrint
         -- Since we're working in a local environment, don't do the usual
         -- thing of printing out the full environment for parameterised
         -- calls or calls in where blocks
         setPPrint (record { showFullEnv = False } ppopts)
         res <- processEdit cmd
         setPPrint ppopts
         pure $ Edited res
process (CGDirective str)
    = do setSession (record { directives $= (str::) } !getSession)
         pure Done
process (RunShellCommand cmd)
    = do coreLift_ (system cmd)
         pure Done
process Quit
    = pure Exited
process NOP
    = pure Done
process ShowVersion
    = pure $ VersionIs  version
process (ImportPackage package) = do
  defs <- get Ctxt
  let searchDirs = defs.options.dirs.extra_dirs
  let Just packageDir = find
        (\d => isInfixOf package (fromMaybe d (fileName d)))
        searchDirs
    | _ => pure (REPLError (pretty "Package not found in the known search directories"))
  let packageDirPath = parse packageDir
  tree <- coreLift $ explore packageDirPath
  fentries <- coreLift $ toPaths (toRelative tree)
  errs <- for fentries $ \entry => do
    let entry' = dropExtension entry
    let sp = forget $ split (== dirSeparator) entry'
    let ns = concat $ intersperse "." sp
    let ns' = mkNamespace ns
    catch (do addImport (MkImport emptyFC False (nsAsModuleIdent ns') ns'); pure Nothing)
          (\err => pure (Just err))
  let errs' = catMaybes errs
  res <- case errs' of
    [] => pure (pretty "Done")
    onePlus => pure $ vsep !(traverse display onePlus)
  pure (Printed res)
 where
  toPaths : {root : _} -> Tree root -> IO (List String)
  toPaths tree =
    depthFirst (\x => map (toFilePath x ::) . force) tree (pure [])

process (FuzzyTypeSearch expr) = fuzzySearch expr

processCatch : {auto c : Ref Ctxt Defs} ->
               {auto u : Ref UST UState} ->
               {auto s : Ref Syn SyntaxInfo} ->
               {auto m : Ref MD Metadata} ->
               {auto o : Ref ROpts REPLOpts} ->
               REPLCmd -> Core REPLResult
processCatch cmd
    = do c' <- branch
         u' <- get UST
         s' <- get Syn
         o' <- get ROpts
         catch (do r <- process cmd
                   commit
                   pure r)
               (\err => do put Ctxt c'
                           put UST u'
                           put Syn s'
                           put ROpts o'
                           msg <- display err
                           pure $ REPLError msg
                           )

parseEmptyCmd : EmptyRule (Maybe REPLCmd)
parseEmptyCmd = eoi *> (pure Nothing)

parseCmd : EmptyRule (Maybe REPLCmd)
parseCmd = do c <- command; eoi; pure $ Just c

export
parseRepl : String -> Either Error (Maybe REPLCmd)
parseRepl inp
    = case runParser (Virtual Interactive) Nothing inp (parseEmptyCmd <|> parseCmd) of
        Left err => Left err
        Right (_, _, result) => Right result

export
interpret : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto m : Ref MD Metadata} ->
            {auto o : Ref ROpts REPLOpts} ->
            String -> Core REPLResult
interpret inp
    = do setCurrentElabSource inp
         case parseRepl inp of
           Left err => pure $ REPLError !(perror err)
           Right Nothing => pure Done
           Right (Just cmd) => processCatch cmd

mutual
  export
  replCmd : {auto c : Ref Ctxt Defs} ->
            {auto u : Ref UST UState} ->
            {auto s : Ref Syn SyntaxInfo} ->
            {auto m : Ref MD Metadata} ->
            {auto o : Ref ROpts REPLOpts} ->
            String -> Core ()
  replCmd "" = pure ()
  replCmd cmd
      = do res <- interpret cmd
           displayResult res

  export
  repl : {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         {auto s : Ref Syn SyntaxInfo} ->
         {auto m : Ref MD Metadata} ->
         {auto o : Ref ROpts REPLOpts} ->
         Core ()
  repl
      = do ns <- getNS
           opts <- get ROpts
           coreLift_ (putStr (prompt (evalMode opts) ++ show ns ++ "> "))
           coreLift_ (fflush stdout)
           inp <- coreLift getLine
           end <- coreLift $ fEOF stdin
           if end
             then do
               -- start a new line in REPL mode (not relevant in IDE mode)
               coreLift_ $ putStrLn ""
               iputStrLn $ pretty "Bye for now!"
              else do res <- interpret inp
                      handleResult res

    where
      prompt : REPLEval -> String
      prompt EvalTC = "[tc] "
      prompt NormaliseAll = ""
      prompt Execute = "[exec] "

  export
  handleMissing' : MissedResult -> String
  handleMissing' (CasesMissing x xs) = show x ++ ":\n" ++ showSep "\n" xs
  handleMissing' (CallsNonCovering fn ns) = (show fn ++ ": Calls non covering function"
                                           ++ (case ns of
                                                 [f] => " " ++ show f
                                                 _ => "s: " ++ showSep ", " (map show ns)))
  handleMissing' (AllCasesCovered fn) = show fn ++ ": All cases covered"

  export
  handleMissing : MissedResult -> Doc IdrisAnn
  handleMissing (CasesMissing x xs) = pretty x <+> colon <++> vsep (code . pretty <$> xs)
  handleMissing (CallsNonCovering fn ns) =
    pretty fn <+> colon <++> reflow "Calls non covering"
      <++> (case ns of
                 [f] => "function" <++> code (pretty f)
                 _ => "functions:" <++> concatWith (surround (comma <+> space)) (code . pretty <$> ns))
  handleMissing (AllCasesCovered fn) = pretty fn <+> colon <++> reflow "All cases covered"

  export
  handleResult : {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         {auto s : Ref Syn SyntaxInfo} ->
         {auto m : Ref MD Metadata} ->
         {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core ()
  handleResult Exited = iputStrLn (reflow "Bye for now!")
  handleResult other = do { displayResult other ; repl }

  export
  displayResult : {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         {auto s : Ref Syn SyntaxInfo} ->
         {auto m : Ref MD Metadata} ->
         {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core ()
  displayResult (REPLError err) = printResult err
  displayResult (Evaluated x Nothing) = printResult $ prettyTerm x
  displayResult (Evaluated x (Just y)) = printResult (prettyTerm x <++> colon <++> prettyTerm y)
  displayResult (Printed xs) = printResult xs
  displayResult (PrintedDoc xs) = printDocResult xs
  displayResult (TermChecked x y) = printResult (prettyTerm x <++> colon <++> prettyTerm y)
  displayResult (FileLoaded x) = printResult (reflow "Loaded file" <++> pretty x)
  displayResult (ModuleLoaded x) = printResult (reflow "Imported module" <++> pretty x)
  displayResult (ErrorLoadingModule x err) = printResult (reflow "Error loading module" <++> pretty x <+> colon <++> !(perror err))
  displayResult (ErrorLoadingFile x err) = printResult (reflow "Error loading file" <++> pretty x <+> colon <++> pretty (show err))
  displayResult (ErrorsBuildingFile x errs) = printResult (reflow "Error(s) building file" <++> pretty x) -- messages already displayed while building
  displayResult NoFileLoaded = printResult (reflow "No file can be reloaded")
  displayResult (CurrentDirectory dir) = printResult (reflow "Current working directory is" <++> dquotes (pretty dir))
  displayResult CompilationFailed = printResult (reflow "Compilation failed")
  displayResult (Compiled f) = printResult (pretty "File" <++> pretty f <++> pretty "written")
  displayResult (ProofFound x) = printResult (prettyTerm x)
  displayResult (Missed cases) = printResult $ vsep (handleMissing <$> cases)
  displayResult (CheckedTotal xs) = printResult (vsep (map (\(fn, tot) => pretty fn <++> pretty "is" <++> pretty tot) xs))
  displayResult (FoundHoles []) = printResult (reflow "No holes")
  displayResult (FoundHoles [x]) = do
     let hole = pretty x.name <++> colon <++> prettyTerm x.type
     printResult (reflow "1 hole" <+> colon <++> hole)
  displayResult (FoundHoles xs) = do
    let header = pretty (length xs) <++> pretty "holes" <+> colon
    let holes  = xs <&> \ x => pretty x.name <++> colon <++> prettyTerm x.type
    printResult $ vcat (header :: map (indent 2) holes)
  displayResult (LogLevelSet Nothing) = printResult (reflow "Logging turned off")
  displayResult (LogLevelSet (Just k)) = printResult (reflow "Set log level to" <++> pretty k)
  displayResult (ConsoleWidthSet (Just k)) = printResult (reflow "Set consolewidth to" <++> pretty k)
  displayResult (ConsoleWidthSet Nothing) = printResult (reflow "Set consolewidth to auto")
  displayResult (ColorSet b) = printResult (reflow (if b then "Set color on" else "Set color off"))
  displayResult (VersionIs x) = printResult (pretty (showVersion True x))
  displayResult (RequestedHelp) = printResult (pretty displayHelp)
  displayResult (Edited (DisplayEdit Empty)) = pure ()
  displayResult (Edited (DisplayEdit xs)) = printResult xs
  displayResult (Edited (EditError x)) = printResult x
  displayResult (Edited (MadeLemma lit name pty pappstr))
    = printResult $ pretty (relit lit (show name ++ " : " ++ show pty ++ "\n") ++ pappstr)
  displayResult (Edited (MadeWith lit wapp)) = printResult $ pretty $ showSep "\n" (map (relit lit) wapp)
  displayResult (Edited (MadeCase lit cstr)) = printResult $ pretty $ showSep "\n" (map (relit lit) cstr)
  displayResult (OptionsSet opts) = printResult (vsep (pretty <$> opts))

  -- do not use a catchall so that we are warned when a new constructor is added
  displayResult Done = pure ()
  displayResult (Executed _) = pure ()
  displayResult DefDeclared = pure ()
  displayResult Exited = pure ()

  export
  displayHelp : String
  displayHelp =
    showSep "\n" $ map cmdInfo help
    where
      makeSpace : Nat -> String
      makeSpace n = pack $ take n (repeat ' ')

      col : Nat -> Nat -> String -> String -> String -> String
      col c1 c2 l m r =
        l ++ (makeSpace $ c1 `minus` length l) ++
        m ++ (makeSpace $ c2 `minus` length m) ++ r

      cmdInfo : (List String, CmdArg, String) -> String
      cmdInfo (cmds, args, text) = " " ++ col 18 20 (showSep " " cmds) (show args) text

  export
  displayErrors : {auto c : Ref Ctxt Defs} ->
         {auto u : Ref UST UState} ->
         {auto s : Ref Syn SyntaxInfo} ->
         {auto m : Ref MD Metadata} ->
         {auto o : Ref ROpts REPLOpts} -> REPLResult -> Core ()
  displayErrors (ErrorLoadingFile x err) = printError (reflow "File error in" <++> pretty x <+> colon <++> pretty (show err))
  displayErrors _ = pure ()


text:
module Bord

import System.Concurrency.Channels

import Data.Vect

%default total

infixl 9 -.-
infixl 3 ~>~

main: JS_IO ()
main = putStrLn' "hello"

namespace SigTy
  data SigTy: Type where
    Pos: Type -> SigTy
    Neg: Type -> SigTy
    (+): SigTy -> SigTy -> SigTy

  dual: SigTy -> SigTy
  dual (Pos x) = Neg x
  dual (Neg x) = Pos x
  dual (x + y) = dual x + dual y

data (~>~): SigTy -> SigTy -> Type where
  Pure:   (a -> b) -> Pos a ~>~ Pos b
  Io:     (a -> IO b) -> Pos a ~>~ Pos b
  (-.-):  (x ~>~ y) -> (y ~>~ z) -> (x ~>~ z)
  (+):    (w ~>~ x) -> (y ~>~ z) -> (w + y ~>~ x + z)
  Dual:   (x ~>~ y) -> (dual y ~>~ dual x)
  Unit:   (x: SigTy) -> (Pos Void ~>~ (dual x + x))
  CoUnit: (x: SigTy) -> (x + dual x ~>~ Pos Void)
  Join:   Pos a + Pos b    ~>~ Pos (Either a b)
  Split:  Pos (Either a b) ~>~ Pos a + Pos b
  Assoc:  (x,y,z: SigTy) -> x + (y + z) ~>~ (x + y) + z

plusEq: {x,x',y,y': SigTy} -> x = x' -> y = y' -> x + y = x' + y'
plusEq Refl Refl = Refl

dualIdem: (x: SigTy) -> dual (dual x) = x
dualIdem (Pos x) = Refl
dualIdem (Neg x) = Refl
dualIdem (x + y) = plusEq (dualIdem x) (dualIdem y)

lemma1: (x,y,z: SigTy) -> dual (dual x + dual y + dual z) = x + y + z
lemma1 x y z = plusEq (plusEq (dualIdem x) (dualIdem y)) (dualIdem z)

lemma2: (x,y,z: SigTy) -> dual (dual x + (dual y + dual z)) = x + (y + z)
lemma2 x y z = plusEq (dualIdem x) (plusEq (dualIdem y) (dualIdem z))

revAssoc: (x,y,z: SigTy) -> (x + y) + z ~>~ x + (y + z)
revAssoc x y z =    rewrite sym (lemma1 x y z)
                 in rewrite sym (lemma2 x y z)
                 in Dual (Assoc (dual x) (dual y) (dual z))

alpha: Pos Int ~>~ Pos Int
alpha = Pure id

beta: Pos String ~>~ Pos String
beta = Pure id

gamma: Neg String ~>~ Neg String
gamma = Dual (Pure id)

alphabeta: Pos Int + Pos String ~>~ Pos Int + Pos String
alphabeta = alpha + beta

middle: Pos Int + Pos String + Neg String ~>~ Pos Int + Pos String + Neg String
middle = alphabeta + gamma

right: Pos Int + Pos String + Neg String ~>~ Pos Int + Pos Void
right = revAssoc (Pos Int) (Pos String) (Neg String) -.- (Pure id + CoUnit (Pos String))

left: Pos Int + Pos Void ~>~ Pos Int + Pos String + Neg String
left = (Pure id + Unit (Neg String)) -.- Assoc (Pos Int) (Pos String) (Neg String)

big: Pos Int + Pos Void ~>~ Pos Int + Pos Void
big = left -.- middle -.- right

-- make processes

partial
inPortLoop: (a: Type) -> (f: a -> b) -> Channel -> Channel -> IO ()
inPortLoop a f sender_chan worker_chan = do
  Just i <- unsafeRecv a sender_chan
  ok <- unsafeSend worker_chan i
  inPortLoop a f sender_chan worker_chan

partial
inPort: (a: Type) -> (f: a -> b) -> IO ()
inPort a f = do
  Just sender_chan <- listen 1
  Just worker_chan <- listen 1
  inPortLoop a f sender_chan worker_chan

outPort: (b: Type) -> IO ()
outPort b = ?outPort_rhs

-- mkPure: (a -> b) -> IO (Maybe (Channel, Channel))
-- mkPure f = do
--   Just pure_id <- spawn pureProc
--     | Nothing => putStrLn "Error"

max_stars_repo_name: jameshaydon/smproc

max_issues_repo_name: jameshaydon/smproc

max_forks_repo_name: jameshaydon/smproc


text:
module Data.Ref

import Data.IORef

%default total

export
data Ref : (l : label) -> Type -> Type where
  [search l]
  MkRef : IORef a -> Ref l a

export
newRef : HasIO io => (l : label) -> t -> io (Ref l t)
newRef l val = do ref <- newIORef val
                  pure (MkRef ref)

export %inline
get : HasIO io => (l : label) -> Ref l t => io t
get @{_} l @{MkRef ref} = readIORef ref

export %inline
put : HasIO io => (l : label) -> Ref l t => t -> io ()
put @{_} l @{MkRef ref} val = writeIORef ref val

export %inline
modify : HasIO io => (l : label) -> Ref l t => (t -> t) -> io ()
modify @{_} l @{MkRef ref} f = readIORef ref >>= writeIORef ref . f


text:
module Web.Internal.FileTypes

import JS

--------------------------------------------------------------------------------
--          Enums
--------------------------------------------------------------------------------

namespace EndingType

  public export
  data EndingType = Transparent | Native

  public export
  Show EndingType where
    show Transparent = "transparent"
    show Native = "native"

  public export
  Eq EndingType where
    (==) = (==) `on` show

  public export
  Ord EndingType where
    compare = compare `on` show

  public export
  read : String -> Maybe EndingType
  read "transparent" = Just Transparent
  read "native" = Just Native
  read _ = Nothing

  public export
  fromString :  (s : String)
             -> {auto 0 _ : IsJust (EndingType.read s)}
             -> EndingType
  fromString s = fromJust $ read s

  export
  ToFFI EndingType String where
    toFFI = show

  export
  FromFFI EndingType String where
    fromFFI = read

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

export data Blob : Type where [external]

export
ToFFI Blob Blob where toFFI = id

export
FromFFI Blob Blob where fromFFI = Just

export
SafeCast Blob where
  safeCast = unsafeCastOnPrototypeName "Blob"

export data File : Type where [external]

export
ToFFI File File where toFFI = id

export
FromFFI File File where fromFFI = Just

export
SafeCast File where
  safeCast = unsafeCastOnPrototypeName "File"

export data FileList : Type where [external]

export
ToFFI FileList FileList where toFFI = id

export
FromFFI FileList FileList where fromFFI = Just

export
SafeCast FileList where
  safeCast = unsafeCastOnPrototypeName "FileList"

export data FileReader : Type where [external]

export
ToFFI FileReader FileReader where toFFI = id

export
FromFFI FileReader FileReader where fromFFI = Just

export
SafeCast FileReader where
  safeCast = unsafeCastOnPrototypeName "FileReader"

export data FileReaderSync : Type where [external]

export
ToFFI FileReaderSync FileReaderSync where toFFI = id

export
FromFFI FileReaderSync FileReaderSync where fromFFI = Just

export
SafeCast FileReaderSync where
  safeCast = unsafeCastOnPrototypeName "FileReaderSync"

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

export data BlobPropertyBag : Type where [external]

export
ToFFI BlobPropertyBag BlobPropertyBag where toFFI = id

export
FromFFI BlobPropertyBag BlobPropertyBag where fromFFI = Just

export data FilePropertyBag : Type where [external]

export
ToFFI FilePropertyBag FilePropertyBag where toFFI = id

export
FromFFI FilePropertyBag FilePropertyBag where fromFFI = Just