text:
module Idris.Doc.Keywords

import Decidable.Equality
import Parser.Lexer.Source
import Data.List.Quantifiers
import Data.String

import Idris.Doc.Annotations
import Idris.Pretty

import Libraries.Data.List.Quantifiers.Extra

infix 10 ::=
data DocFor : String -> Type where
  (::=) : (0 str : String) -> (doc : Doc IdrisDocAnn) -> DocFor str

doc : DocFor _ -> Doc IdrisDocAnn
doc (_ ::= d) = d

fixity : Doc IdrisDocAnn
fixity = vcat $
    header "Fixity declarations" :: ""
    :: map (indent 2) [
    """
    Operators can be assigned a priority level and associativity. During parsing
    operators with a higher priority will collect their arguments first and the
    declared associativity will inform how subterms are grouped.

    For instance the expression `a + b * c * d + e` is parsed as
    `(a + ((b * c) * d)) + e` because:
      `(+)` is at level 8 and associates to the left
      `(*)` is at level 9 and associates to the left
    """]

recordtypes : Doc IdrisDocAnn
recordtypes = vcat $
    header "Record types" :: ""
    :: map (indent 2) [
    """
    Records are data types with a single constructor. Each of the constructor's
    argument is given a name and the corresponding projections and record update
    functions are automatically generated.
    For instance, we can define a type of pairs of natural numbers
    """, "",
    """
    ```idris
    record Nat2 where
      constructor MkNat2
      fst : Nat
      snd : Nat
    ```
    """, "",
    """
    and we can then immediately use all of `fst`, `snd`, `{ fst := ?h1 }`,
    or `{ snd $= ?h2 }` to respectively project values out of a record,
    replace values, or update them.
    """
    ]

datatypes : Doc IdrisDocAnn
datatypes = vcat $
    header "(Co)Data types" :: ""
    :: map (indent 2) [
    """
    Keyword to introduce a (co)inductive type definition.
    You can either use a BNF-style definition for simple types
    """, "",
    """
    ```idris
    data List a = Nil | (::) a (List a)
    ```
    """, "",
    """
    or a GADT-style definition for indexed types
    """, "",
    """
    ```idris
    data Vect : Nat -> Type -> Type where
      Nil  : Vect 0 a
      (::) : a -> Vect n a -> Vect (S n) a
    ```
    """, "",
    """
    Coinductive data is introduced using the same syntax except
    that the type of potentially infinite subterms is wrapped in
    an `Inf` type constructor.
    """]

totality : Doc IdrisDocAnn
totality = vcat $
    header "Totality" :: ""
    :: map (indent 2) [
    """
    Definitions can be individually declared `total`, `covering`, or partial`.
    It is also possible to set the default totality flag for definitions in a
    module by using the `%default` pragma.
    """, "",
    """
    * `total` offers the highest guarantees. Definitions using this flag are
      only accepted if:
        1. their patterns are covering all possible cases;
        2. they are either obviously terminating (for recursive functions)
           or productive (for corecursive functions);
        3. all the auxiliary functions used are total themselves.
    """, "",
    """
    * `covering` is the default level of guarantees. It only enforces that
      pattern matchings are exhaustive.
    """, "",
    """
    * `partial` is the absence of any totality requirement: as long as the
      definition typechecks, it is accepted. It is possible to call a partial
      function from a total one by using the `assert_total` escape hatch.
    """]

visibility : Doc IdrisDocAnn
visibility = vcat $
    header "Visibility" :: ""
    :: map (indent 2) [
    """
    Programmers can decide which parts of a module they expose to the outside
    world.
    """, "",
    """
    * `public export` ensures that both the declaration and the definition
       are accessible from the outside of the module. This means the function
       will be able to reduce in types.
    """, "",
    """
    * `export` means that only the declaration will be made available to the
      outside world. Users will be able to call the function but its internals
      will not be exposed because it will not reduce in types.
    """, "",
    """
    * `private` means that neither the declaration nor the definition will be
      exported. This is the default and is the ideal setting for auxiliary
      definitions.
    """]

ifthenelse : Doc IdrisDocAnn
ifthenelse = vcat $
    header "Boolean conditional" :: ""
    :: map (indent 2) [
    """
    The `if ... then ... else ...` construct is dependently typed. This means
    that if you are branching over a variable, the branches will have refined
    types where that variable has been replaced by either `True` or `False`.
    For instance, in the following incomplete program
    """, "",
    """
    ```idris
    notInvolutive : (b : Bool) -> not (not b) === b
    notInvolutive b = if b then ?holeTrue else ?holeFalse
    ```
    """, "",
    """
    the two holes have respective types `True === True` and `False === False`.
    """, "", "",
    """
    If you do not need the added power granted by dependently typed branches,
    consider using the simpler `ifThenElse` function defined in `Prelude`.
    """]

impossibility : Doc IdrisDocAnn
impossibility = vcat $
    header  "Impossible branches" :: ""
    :: map (indent 2) [
    """
    The `impossible` keyword can be used to dismiss a clause involving an
    argument with an uninhabited type. For instance an assumption stating
    that 0 is equal to 1:
    """, "",
    """
    ```idris
    zeroIsNotOne : 0 === 1 -> Void
    zeroIsNotOne eq impossible
    ```
    """]

caseof : Doc IdrisDocAnn
caseof = vcat $
    header "Case block" :: ""
    :: map (indent 2) [
    """
    The `case ... of ...` construct is dependently typed. This means that if you
    are branching over a variable, the branches will have refined types where
    that variable has been replaced by the appropriate pattern.
    For instance, in the following program
    """, "",
    """
    ```idris
    assoc : (ma, mb, mc : Maybe a) ->
            ((ma <|> mb) <|> mc) === (ma <|> (mb <|> mc))
    assoc ma mb mc = case ma of
      Nothing => Refl
      Just a  => Refl
    ```
    """, "",
    """
    the branches typecheck because in their respective types `ma` has been replaced
    either by `Nothing` or `Just a` and that was enough for them to compute to
    `(mb <|> mc) === (mb <|> mc)` and `Just a === Just a` respectively. Both of
    which can be discharged using `Refl`.
    """]

importing : Doc IdrisDocAnn
importing = vcat $
    header "Importing" :: ""
    :: map (indent 2) [
    """
    Importing a module brings the definition it exports into scope.
    Combined with `public` it also re-exports these definitions.
    """]

forallquantifier : Doc IdrisDocAnn
forallquantifier = vcat $
    header "Forall quantifier" :: ""
    :: map (indent 2) [
    """
    `forall` quantification is syntactic sugar for implicit runtime-irrelevant
    universal quantification. That is to say that `forall x, y, z. ...`
    desugars to `{0 x, y, z : _} -> ...`.
    """]

implicitarg : Doc IdrisDocAnn
implicitarg = vcat $
    header  "Implicit arguments" :: ""
    :: map (indent 2) [
    """
    Implicit arguments can be solved using various strategies. By default
    they will be filled in using unification but programmers can use various
    keywords to change that.
    """, "",
    """
    * `auto` will use the same mechanism as interface resolution to build the
      argument. Users can add new hints to the database by adding a `%hint`
      pragma to their declarations. By default all data constructors are hints.
      For instance, the following function
      ```idris
      f : (n : Nat) -> {auto _ : n === Z} -> Nat
      f n = n
      ```
      will only accept arguments that can be automatically proven to be equal
      to zero.
    """, "",
    """
    * `default` takes a value of the appropriate type and if no argument is
      explicitly passed at a call site, will use that default value.
      For instance, the following function
      ```idris
      f : {default 0 n : Nat} -> Nat
      f = n
      ```
      will return `0` if no argument is passed and its argument otherwise.
    """]

unusedKeyword : Doc IdrisDocAnn
unusedKeyword = "Currently unused keyword"

interfacemechanism : Doc IdrisDocAnn
interfacemechanism = vcat $
    header "Interfaces" :: ""
    :: map (indent 2) [
    """
    Interfaces offer ad-hoc polymorphism. Programmers can declare new
    interfaces offering a set of methods (some of which may have default
    implementations in terms of the interface's other methods) and write
    programs generic over all types implementing the interface.
    """, "",
    """
    In the following example we define a `Failing` interface that allows
    users to abort in case a computation is doomed to fail. We implement
    the `whenJust` construct using this interface and show a couple of
    implementations:
    """, "",
    """
    ```idris
    interface Failing (0 a : Type) where
      fail : a

    whenJust : Failing ret => Maybe a -> (a -> ret) -> ret
    whenJust (Just v) k = k v
    whenJust Nothing  _ = fail

    implementation Failing Bool where
      fail = False

    Failing (Maybe a) where
      fail = Nothing
    ```
    """, "",
    """
    As you can see the `implementation` keyword is optional. Note that the
    proof search machinery powering interface resolution works best if your
    implementations are for specific type constructors (here `Bool` and `Maybe`).
    """]

doblock : Doc IdrisDocAnn
doblock = vcat $
    header "Do block" :: ""
    :: map (indent 2) [
    #"""
    Do blocks are a popular way to structure (among other things) effectful code.
    They are desugared using `(>>=)` and `(>>)` respectively depending on whether
    the result of a subcomputation is bound. Let bindings and local definitions
    can be used (omitting `in` because the layout is already controlled by the
    `do`-based indentation) and desugared to the corresponding `let` constructs.

    For instance the following block
    ```idris
      do x <- e1
         e2
         let y = e3
         e4
    ```
    is equivalent to the expression `e1 >>= \ x => e2 >> let y = e3 in e4`.
    """#, "",
    """
    By default `(>>=)` and `(>>)` are then selected using the usual type
    directed disambiguation mechanisms. Users who want to bypass this implicit
    disambiguation step can use a qualified `do`: by writing `M.do` they ensure
    Idris will explicitly use `M.(>>=)` and `M.(>>)` during elaboration.
    """ ]

whereblock : Doc IdrisDocAnn
whereblock = vcat $
    header "Where block" :: ""
    :: map (indent 2) [
    header "NB:" <++> """
    `where` is used as a layout keyword in `data`, `record`, `interface`,
    and `implementation` blocks. This documentation snippet focuses instead
    on the `where` blocks introducing local definitions.
    """, "",
    """
    A `where` block allows the introduction of local auxiliary definitions
    that are parametrised over the variables bound on the left hand side of
    the parent clause (cf. the doc for `parameters`).
    """
    ]

parametersblock : Doc IdrisDocAnn
parametersblock = vcat $
    header "Parameters block" :: ""
    :: map (indent 2) [
    """
    Definitions that share a common parameter can be grouped in a parameters
    block to avoid having to explicitly pass it around. Outside of the block
    all the definitions will take additional arguments corresponding to the
    parameters. For instance the functions in the following block all use a
    default value `dflt`
    """, "",
    """
    ```idris
    parameters (dflt : a)

      head : List a -> a
      head (x :: xs) = x
      head _ = dflt

      last : List a -> a
      last [x] = x
      last (_ :: xs) = last xs
      last _ = dflt
    ```
    """, "",
    """
    and their respective types outside of the parameters block are
    `head : a -> List a -> a` and `last : a -> List a -> a`.
    """]

mutualblock : Doc IdrisDocAnn
mutualblock = vcat $
    header "Mutual block" :: ""
    :: map (indent 2) [
    """
    Mutual blocks allow users to have inter-dependent declarations. For instance
    we can define the `odd` and `even` checks in terms of each other like so:
    ```idris
    mutual

      odd : Nat -> Bool
      odd Z = False
      odd (S n) = even n

      even : Nat -> Bool
      even Z = True
      even (S n) = odd n
    ```
    """, "",
    """
    Internally this is implemented in terms of the more fundamental
    forward-declaration feature: all the mutual declarations come first and then
    their definitions. In other words, the earlier example using a `mutual` block
    is equivalent to the following
    ```idris
    odd : Nat -> Bool
    even : Nat -> Bool

    odd Z = False
    odd (S n) = even n

    even Z = True
    even (S n) = odd n
    ```
    """]

namespaceblock : Doc IdrisDocAnn
namespaceblock = vcat $
    header "Namespace block" :: ""
    :: map (indent 2) [
    """
    Attempting to declare two functions with the same name in a given module
    will lead to a scope error. Putting each one in a different `namespace`
    block can help bypass this issue by ensuring that they are assigned distinct
    fully qualified names. For instance
    ```idris
    module M

    namespace Zero
      val : Nat
      val = 0

    namespace One
      val : Nat
      val = 1
    ```
    declares a module `M` containing two values `M.Zero.val` and `M.One.val`.
    You can use `export` or `public export` to control whether a function
    declared in a namespace is available outside of it.
    """]

rewriteeq : Doc IdrisDocAnn
rewriteeq = vcat $
    header "Rewrite" :: ""
    :: map (indent 2) [
    """
    Users can deploy an equality proof to adjust a type by replacing the value
    on the left hand side of the equality by that on the right hand side.
    For instance, if we know that the types `a` and `b` are propositionally
    equal, we can return a value of type `a` as if it had type `b`:
    ```idris
    transport : a === b -> a -> b
    transport eq x = rewrite sym eq in x
    ```
    """]

withabstraction : Doc IdrisDocAnn
withabstraction = vcat $
    header "With abstraction" :: ""
    :: map (indent 2) [
    """
    We often need to match on the result of an intermediate computation.
    When this intermediate computation additionally appears in the type of the
    function being defined, the `with` construct allows us to capture these
    occurences so that the observations made in the patterns will be reflected
    in the type.
    If we additionally need to remember that the link between the patterns and
    the intermediate computation we can use the `proof` keyword to retain an
    equality proof.
    """, "",
    """
    In the following example we want to implement a `filter` function that not
    only returns values that satisfy the input predicate but also proofs that
    they do. The `with (p x)` construct introduces a value of type `Bool`
    obtained by testing `x` with `p`. The additional `proof eq` part records in
    `eq` an equality proof stating that the `True`/`False` patterns in the further
    clauses are equal to the result of evaluating `p x`. This is the reason why
    we can successfully form `(x ** eq)` in the `True` branch.
    ```idris
    filter : (p : a -> Bool) -> List a -> List (x : a ** p x === True)
    filter p [] = []
    filter p (x :: xs) with (p x) proof eq
      _ | True = (x ** eq) :: filter p xs
      _ | False = filter p xs
    ```
    """]

letbinding : Doc IdrisDocAnn
letbinding = vcat $
    header "Let binding" :: ""
    :: map (indent 2) [
    """
    The `let` keyword is used for both local definitions and let bindings.
    Local definitions are just like top-level definitions except that they are
    defined in whatever extended context is available at the definition site.

    Let bindings can be used to bind the result of intermediate computations.
    They do not necessitate but can have a type annotation. They will not unfold
    in the type of subsequent terms so may not be appropriate in all cases.

    For instance, in the following definition the let-bound value `square`
    ensures that `n * n` is only computed once:
    ```idris
    power4 : Nat -> Nat
    power4 n = let square := n * n in square * square
    ```

    It is also possible to pattern-match on the result of the intermediate
    computation. The main pattern is written in place of the variable and
    an alternative list of clauses can be given using the `|` separator.
    For instance, we can shortcut the `square * square` computation in case
    the returned value is 0 like so:
    ```idris
    power4 : Nat -> Nat
    power4 n = let square@(S _) := n * n
                     | Z => Z
               in square * square
    ```
    """]

keywordsDoc : All DocFor Source.keywords
keywordsDoc =
     "data" ::= datatypes
  :: "module" ::= "Keyword to start a module definition"
  :: "where" ::= whereblock
  :: "let" ::= letbinding
  :: "in" ::= "Used by `let` and `rewrite`. See either of them for more details."
  :: "do" ::= doblock
  :: "record" ::= recordtypes
  :: "auto" ::= implicitarg
  :: "default" ::= implicitarg
  :: "implicit" ::= unusedKeyword
  :: "mutual" ::= mutualblock
  :: "namespace" ::= namespaceblock
  :: "parameters" ::= parametersblock
  :: "with" ::= withabstraction
  :: "proof" ::= withabstraction
  :: "impossible" ::= impossibility
  :: "case" ::= caseof
  :: "of" ::= caseof
  :: "if" ::= ifthenelse
  :: "then" ::= ifthenelse
  :: "else" ::= ifthenelse
  :: "forall" ::= forallquantifier
  :: "rewrite" ::= rewriteeq
  :: "using" ::= ""
  :: "interface" ::= interfacemechanism
  :: "implementation" ::= interfacemechanism
  :: "open" ::= unusedKeyword
  :: "import" ::= importing
  :: "public" ::= visibility
  :: "export" ::= visibility
  :: "private" ::= visibility
  :: "infixl" ::= fixity
  :: "infixr" ::= fixity
  :: "infix" ::= fixity
  :: "prefix" ::= fixity
  :: "total" ::= totality
  :: "partial" ::= totality
  :: "covering" ::= totality
  :: []

export
getDocsForKeyword : String -> Doc IdrisDocAnn
getDocsForKeyword k
  = maybe (annotate (Syntax Keyword) $ pretty k) doc
  $ lookup k keywordsDoc

unusedSymbol : Doc IdrisDocAnn
unusedSymbol = "Currently unused symbol"

lambdaAbstraction : Doc IdrisDocAnn
lambdaAbstraction = """
  An anonymous function is introduced using a lambda `\\` and binds a
  comma-separated list of either variable names or irrefutable patterns
  before returning a right hand side using `=>`.

  For instance we can implement `transport` like so:
  ```
  transport : a === b -> a -> b
  transport = \ Refl, v => v
  ```
  """

fatArrow : Doc IdrisDocAnn
fatArrow = vcat
  [ """
    Used for an interface constraint in a type signature or as part of a
    lambda abstraction or case block.

    1. Interface constraint
    """
  , indent 2 """
    `a => b` corresponds to `{auto _ : a} -> b`
    """, ""
  , """
    2. Lambda abstraction
    """
  , indent 2 lambdaAbstraction
  , "", """
    3. Case block
    """
  ]

bang : Doc IdrisDocAnn
bang = """
  Directive to lift the following effectful expression to the nearest enclosing
  (potentially implicit) `do` block. In the following definition for instance

  ```
  anyM : Monad m => (a -> m Bool) -> List a -> m (Maybe a)
  anyM p [] = pure Nothing
  anyM p (x :: xs) = if !(p x) then pure (Just x) else anyM p xs
  ```

  the expression `if !(p x) then pure (Just x) else anyM p xs` is equivalent to
  the following `do` block:

  ```
  do b <- p x
     if b then pure (Just x) else anyM p xs
  ```
  """

asPattern : Doc IdrisDocAnn
asPattern = """
  An as pattern `@` can be used to both pattern match on a variable
  and retain a name for the compound expression. E.g. instead of writing
  ```
  last : List a -> Maybe a
  last [] = Nothing
  last [x] = Just x
  last (x :: y :: ys) = last (y :: ys)
  ```

  where, in the last clasue, we take `y :: ys` apart on the left hand side
  before reconstructing it on the right hand side, we can write:

  ```
  last (x :: xs@(_ :: _)) = last xs
  ```
  """

tupleSyntax : Doc IdrisDocAnn
tupleSyntax = "Used to build dependent pairs together with parentheses"

rangeSyntax : Doc IdrisDocAnn
rangeSyntax = """
  The ellipsis `..` can be used to generate lists or streams of values for
  types that implement the `Range` interface.

  Lists can be generated using an initial value, an (optional) second value
  and a final one. For instance, we can generate lists of integers like so:
    1. `[1..5]`   evaluates to `[1,2,3,4,5]`
    2. `[1,3..5]` evaluates to `[1, 3, 5]`

  Streams can be generated using an initial value and an optional second value.
  For instance the following streams of integers:
    1. `[1..]`   for all positive integers
    2. `[1,3..]` for all positive odds
  """

recordUpdate : Doc IdrisDocAnn
recordUpdate = vcat $ header "Record updates" :: ""
  :: map (indent 2) [
  """
  If a record `r` has a field `n` of type `Nat`, it is possible to either

  1. overwrite the current value with `0` by using the assignment symbol `:=`
     like so: `{ n := 0 } r`

  2. modify the current value by adding `2` by using the modification symbol `$=`
     like so: `{ n $= (2 +) } r`.

  Multiple updates can be combined in a single update by grouping a comma-separated
  list of assignments and/or modifications like so: `{ a := Z, b $= S } r`.
  """
  ]

symbolsDoc : All DocFor (Source.symbols ++ Source.reservedInfixSymbols)
symbolsDoc
  = "," ::= ""
  :: ";" ::= ""
  :: "_" ::= """
             An implicit value either solved by unification or bound
             as a pattern or type variable.
             """
  :: "`" ::= ""
  :: "%" ::= "Start of a pragma"
  :: "\\" ::= lambdaAbstraction
  :: ":" ::= """
             Type declaration, for instance `id : a -> a`
             declares a new toplevel definition `id` of type `a -> a`.
             """
  :: "=" ::= "Definition or equality type"
  :: ":=" ::= "Let binding or record assignment"
  :: "$=" ::= recordUpdate
  :: "|" ::= "Additional patterns showing up in a `with` clause"
  :: "|||" ::= "Document string attached to the following definition"
  :: "<-" ::= "Bind in a do block"
  :: "->" ::= "Function type"
  :: "=>" ::= fatArrow
  :: "?" ::= "An implicit value solved by unification."
  :: "!" ::= bang
  :: "&" ::= unusedSymbol
  :: "**" ::= tupleSyntax
  :: ".." ::= rangeSyntax
  :: "~" ::= ""
  :: "@" ::= asPattern
  :: []

export
getDocsForSymbol : String -> Doc IdrisDocAnn
getDocsForSymbol k
  = maybe (annotate (Syntax Keyword) $ pretty k) doc
  $ lookup k symbolsDoc


text:
module PLFI.Part1.Relations

import PLFI.Part1.Induction
import PLFI.Part1.Naturals
import Syntax.PreorderReasoning

%default total

%hide Prelude.(+)
%hide Prelude.(*)

-- z≤n --------
--     zero ≤ n

--     m ≤ n
-- s≤s -------------
--     suc m ≤ suc n

-- z≤n -----
--     0 ≤ 2
-- s≤s -------
--     1 ≤ 3
-- s≤s ---------
--     2 ≤ 4

infix 4 <=

data (<=) : N -> N -> Type where

  Zero
    : {n : N} ->
    -------------
     Zero <= n

  Suc
     : {m, n : N} ->
        (m <= n) ->
    -------------------
    (Suc m) <= (Suc n)

invSucLTE : {m,n : N} -> (Suc m) <= (Suc n) -> m <= n
invSucLTE (Suc lte) = lte

invZeroLTE : {m : N} -> m <= Zero -> m = Zero
invZeroLTE Zero = Refl

-- Exercise orderings (practice)
-- Give an example of a preorder that is not a partial order
-- Give an example of a partial order that is not a total order

-- Reflexivity

-- lteRefl0 : n <= n
-- lteRefl0 {n} = ?h1

lteRefl
  : {n : N} ->
  ------------
    n <= n
lteRefl {n = Zero}    = Zero
lteRefl {n = (Suc m)} = Suc lteRefl

-- Transitivity

lteTrans
  : {m,n,p : N} ->
    m <= n ->
    n <= p ->
  ----------------
    m <= p
lteTrans Zero    y       = Zero
lteTrans (Suc x) (Suc y) = Suc (lteTrans x y)

-- lteTrans {n = n}       {m = Zero}    {p = p}       Zero    np        = Zero
-- lteTrans {n = (Suc n)} {m = (Suc m)} {p = (Suc p)} (Suc mn) (Suc np) = Suc (lteTrans mn np)

lteAntisym
  : {m,n : N} ->
    m <= n ->
    n <= m ->
  --------------
     n = m
lteAntisym Zero Zero = Refl
-- lteAntisym (Suc x) (Suc y) = rewrite (lteAntisym x y) in Refl
lteAntisym (Suc x) (Suc y) = cong Suc (lteAntisym x y)
-- lteAntisym (Suc x) (Suc y) = let Refl = lteAntisym x y in Refl

-- Total

-- data Total0 : N -> N -> Type where

--   Forward0
--     : m <= n ->
--     -----------
--       Total0 m n

--   Flipped0
--     : n <= m ->
--     -----------
--       Total0 m n

data Total : (m, n : N) -> Type where

  Forward
    : m <= n ->
    -----------
      Total m n

  Flipped
    : n <= m ->
    -----------
      Total m n

-- lteTotal : (m, n : N) -> Total m n
-- lteTotal Zero    n       = Forward Zero
-- lteTotal (Suc m) Zero    = Flipped Zero
-- lteTotal (Suc m) (Suc n) with (lteTotal m n)
--   _ | Forward mn = Forward (Suc mn)
--   _ | Flipped nm = Flipped (Suc nm)

lteTotal : (m, n : N) -> Total m n
lteTotal Zero    n       = Forward Zero
lteTotal (Suc m) Zero    = Flipped Zero
lteTotal (Suc m) (Suc n) = case lteTotal m n of
  Forward mn => Forward (Suc mn)
  Flipped nm => Flipped (Suc nm)

%hint
addMonoR_LTE
  : (n,p,q : N)    ->
       p <= q      ->
  -------------------
   (n + p) <= (n + q)
addMonoR_LTE Zero    p q pq = pq
addMonoR_LTE (Suc m) p q pq = Suc (addMonoR_LTE m p q pq)

%hint
addMonoL_LTE
  :   (m,n,p : N)  ->
        m <= n     ->
  -------------------
  (m + p) <= (n + p)
addMonoL_LTE m n p mn =
  rewrite (addComm m p) in
  rewrite (addComm n p) in
  addMonoR_LTE p m n mn

addMono_LTE
  : (m,n,p,q : N)  ->
       m <= n      ->
       p <= q      ->
  -------------------
  (m + p) <= (n + q)
addMono_LTE m n p q mn pq
  = lteTrans
      {n=(n + p)}
      (addMonoL_LTE m n p mn)
      (addMonoR_LTE n p q pq)

-- Exercise (strech) *-mono-≤

multMonoLTE
  : (m,n,p,q : N)  ->
        m <= n     ->
        p <= q     ->
  -------------------
   (m * p) <= (n * q)

-- Strict inequality

infix 4 <

public export
data (<) : N -> N -> Type where

  ZeroLT
    :   {n : N}  ->
    ---------------
    Zero < (Suc n)

  SucLT
    :  {m, n : N}   ->
         m < n      ->
    ------------------
     (Suc m) < (Suc n)

-- Exercise lteTrans (recommended)

ltTrans
  : {m,n,p : N} ->
       m < n    ->
       n < p    ->
  ----------------
       m < p
ltTrans ZeroLT    (SucLT x) = ZeroLT
ltTrans (SucLT x) (SucLT y) = SucLT (ltTrans x y)

namespace LTTrans

  ltTrans1
    : (m,n,p : N) ->
        m < n    ->
        n < p    ->
    ----------------
        m < p
  ltTrans1 Zero    (Suc n) (Suc p) ZeroLT    (SucLT x) = ZeroLT
  ltTrans1 (Suc m) (Suc n) (Suc p) (SucLT x) (SucLT y) = SucLT (ltTrans1 m n p x y)

  public export
  ltTrans2
    : {m,n,p : N} ->
        m < n    ->
        n < p    ->
    ----------------
        m < p
  ltTrans2 {m,n,p} mn np = ltTrans1 m n p mn np

-- Exercise trichotomy (practice)

data Trichotomy : N -> N -> Type where
  LT : m < n -> Trichotomy m n
  EQ : m = n -> Trichotomy m n
  GT : n < m -> Trichotomy m n

--  0 m : N
--  0 n : N
-- ------------------------------
-- trichotomy_rhs : Trichotomy m n
0
trich : forall m , n . Trichotomy m n
trich {m = Zero} {n = Zero} = EQ Refl
trich {m = Zero} {n = (Suc m)} = LT ZeroLT
trich {m = (Suc m)} {n = n} = ?trichotomy_rhs0_2

trichotomy : (m, n : N) -> Trichotomy m n
trichotomy Zero    Zero     = EQ Refl
trichotomy Zero    (Suc _)  = LT ZeroLT
trichotomy (Suc _) Zero     = GT ZeroLT
trichotomy (Suc m) (Suc n)  = case (trichotomy m n) of
  (LT mn) => LT (SucLT mn)
  (EQ mm) => EQ (cong Suc mm)
  (GT nm) => GT (SucLT nm)

-- trichotomy (Suc m) (Suc n) with (trichotomy m n)
--   _ | (LT x)   = ?trichotomy_rhs_4_rhs4_1
--   _ | (EQ prf) = ?trichotomy_rhs_4_rhs4_2
--   _ | (GT x)   = ?trichotomy_rhs_4_rhs4_3

-- Exercise addMonoLT (practice)

addMonoR_LT
  : (n,p,q : N)    ->
       p < q       ->
  -------------------
   (n + p) < (n + q)
addMonoR_LT Zero    p q pq = pq
addMonoR_LT (Suc m) p q pq = SucLT (addMonoR_LT m p q pq)

addMonoL_LT
  :   (m,n,p : N)  ->
         m < n     ->
  -------------------
   (m + p) < (n + p)
addMonoL_LT m n p mn =
  rewrite (addComm m p) in
  rewrite (addComm n p) in
  addMonoR_LT p m n mn

addMonoLT
  : (m,n,p,q : N) ->
        m < n     ->
        p < q     ->
  ------------------
   (m + p) < (n + q)
addMonoLT m n p q mn pq
  = ltTrans
      {n=(n + p)}
      (addMonoL_LT m n p mn)
      (addMonoR_LT n p q pq)

{-
Memo:
interface Transitive rel => Proof (rel : N -> N -> Type) where
  {-# MINIMAL (monoL | monoR) #-}
  monoL : ({n,m,p: _} -> rel n m -> rel (n + p) (m + p))
  monoL = monoLFromMonoRAndPlusComm
  monoR : ({n,m,p: _} -> rel n m -> rel (n + p) (m + p))
  monoR = monoRFromMonoLAndPlusComm

proofIsMonoProof : Proof rel => rel n m -> rel p q -> rel (n + p) (m + p)
proofIsMonoProof
  = trans
      {n=(n + p)}
      (monoL m n p mn)
      (monoR n p q pq)

Transitive : (rel : N -> N -> Type) -> Type
Transitive rel = forall n,m,p : rel n m -> rel m p -> rel n p
-- Transitive rel = {n,m,p : N} -> rel n m -> rel m p -> rel n p
-}

-- Exercise lte iff lt (recommended)

lteIffLtL
  :   (m,n : N)   ->
    (Suc m) <= n  ->
  ------------------
       m < n
lteIffLtL Zero    (Suc _) (Suc x) = ZeroLT
lteIffLtL (Suc m) (Suc _) (Suc x) = SucLT (lteIffLtL m _ x)

lteIffLtR
  : (m,n : N)  ->
      m < n    ->
  ---------------
    (Suc m) <= n
lteIffLtR Zero    (Suc _) ZeroLT    = Suc Zero
lteIffLtR (Suc m) (Suc _) (SucLT x) = Suc (lteIffLtR m _ x)

-- Exercise ltTransRevisited (practice)

-- Give an alternative proof that strict inequality is transitive,
-- using the relation between strict inequality and inequality
-- and the fact that inequality is transitive.

{-
lteIffLtR
  : (m,n : N)  ->
      m < n    ->
  ---------------
    (Suc m) <= n
lteIffLtL
  :   (m,n : N)   ->
    (Suc m) <= n  ->
  ------------------
       m < n
lteTrans
  : {m,n,p : N} ->
    m <= n ->
    n <= p ->
  ----------------
    m <= p
-}

lteSucc : (n : N) -> n <= Suc n
lteSucc Zero    = Zero
lteSucc (Suc m) = Suc (lteSucc m)

infixr 4 `lteTrans`

ltTransRevisited
  : (m,n,p : N) ->
       m < n   ->
       n < p   ->
  ----------------
       m < p
ltTransRevisited m n p mn np with (lteIffLtR m n mn, lteIffLtR n p np)
  _ | (lr1, lr2) = lteIffLtL m p $ lr1 `lteTrans` lteSucc n `lteTrans` lr2

ltTransRevisited2
  : (m,n,p : N) ->
       m < n   ->
       n < p   ->
  ----------------
       m < p
ltTransRevisited2 m n p mn np
  = lteIffLtL m p
  $ lteIffLtR m n mn `lteTrans` lteSucc n `lteTrans` lteIffLtR n p np

{-
   lr1 : Suc m <= n
   lr4 : n <= Suc n
   lr2 : Suc n <= p
------------------------------
   h1 : Suc m <= p
-}

namespace Even0

  public export
  data Prop = Even | Odd

  public export
  flip : Prop -> Prop
  flip Even = Odd
  flip Odd = Even

  public export
  data EvenOrOdd : Prop -> N -> Type where
    Zero : EvenOrOdd Even Zero
    Suc  : EvenOrOdd p    n -> EvenOrOdd (flip p) (Suc n)

  public export
  isEven : N -> Type
  isEven n = EvenOrOdd Even n

mutual

  namespace Even

    public export
    data Even : N -> Type where

      Zero :
        ---------
        Even Zero

      Suc
        : {n : N} ->
          Odd n   ->
        ------------
        Even (Suc n)

  namespace Odd

    public export
    data Odd : N -> Type where

      Suc
        : {n : N} ->
          Even n  ->
        -------------
        Odd (Suc n)

total
evenAddEven
  : {m, n : N} ->
      Even m   ->
      Even n   ->
  ---------------
    Even (m + n)

total
oddAddEven
  : {m, n : N} ->
      Odd m    ->
      Even n   ->
  ---------------
    Odd (m + n)

evenAddEven Zero     en = en
evenAddEven (Suc om) en = Suc (oddAddEven om en)

oddAddEven (Suc em) on = Suc (evenAddEven em on)

-- Exercise - Bin-predicates

-- Can : Bin -> Type

-- Can b
-- -----------
-- Can (inc b)

-- ----------
-- Can (to n)

--      Can b
-- ---------------
-- to (from b) = b

ext: idr

max_stars_repo_name: andorp/PLFI

max_issues_repo_name: andorp/PLFI

max_forks_repo_name: andorp/PLFI


text:
module Erlang.Data.MutableStorageBuffer

import Erlang
import public Erlang.System.File

%default total

export
data Buffer : Type where [external]

export
newBuffer : HasIO io => Int -> io (Maybe Buffer)
newBuffer size = do
  MkRaw buf <- pure $ erlUnsafeCall (Raw Buffer) "mutable_storage" "buffer_new" [size]
  pure (Just buf)

-- might be needed if we do this in C...
export
freeBuffer : HasIO io => Buffer -> io ()
freeBuffer buf = pure ()

export
rawSize : HasIO io => Buffer -> io Int
rawSize buf = do
  pure $ erlUnsafeCall Int "mutable_storage" "buffer_raw_size" [MkRaw buf]

-- Assumes val is in the range 0-255
export
setByte : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setByte buf loc val = do
  ignore $ pure $ erlUnsafeCall ErlTerm "mutable_storage" "buffer_set_bits8" [MkRaw buf, loc, val]

export
getByte : HasIO io => Buffer -> (loc : Int) -> io Int
getByte buf loc = do
  pure $ erlUnsafeCall Int "mutable_storage" "buffer_get_bits8" [MkRaw buf, loc]

export
setBits8 : HasIO io => Buffer -> (loc : Int) -> (val : Bits8) -> io ()
setBits8 buf loc val = do
  ignore $ pure $ erlUnsafeCall ErlTerm "mutable_storage" "buffer_set_bits8" [MkRaw buf, loc, MkRaw val]

export
getBits8 : HasIO io => Buffer -> (loc : Int) -> io Bits8
getBits8 buf loc = do
  MkRaw val <- pure $ erlUnsafeCall (Raw Bits8) "mutable_storage" "buffer_get_bits8" [MkRaw buf, loc]
  pure val

export
setBits16 : HasIO io => Buffer -> (loc : Int) -> (val : Bits16) -> io ()
setBits16 buf loc val = do
  ignore $ pure $ erlUnsafeCall ErlTerm "mutable_storage" "buffer_set_bits16" [MkRaw buf, loc, MkRaw val]

export
getBits16 : HasIO io => Buffer -> (loc : Int) -> io Bits16
getBits16 buf loc = do
  MkRaw val <- pure $ erlUnsafeCall (Raw Bits16) "mutable_storage" "buffer_get_bits16" [MkRaw buf, loc]
  pure val

export
setBits32 : HasIO io => Buffer -> (loc : Int) -> (val : Bits32) -> io ()
setBits32 buf loc val = do
  ignore $ pure $ erlUnsafeCall ErlTerm "mutable_storage" "buffer_set_bits32" [MkRaw buf, loc, MkRaw val]

export
getBits32 : HasIO io => Buffer -> (loc : Int) -> io Bits32
getBits32 buf loc = do
  MkRaw val <- pure $ erlUnsafeCall (Raw Bits32) "mutable_storage" "buffer_get_bits32" [MkRaw buf, loc]
  pure val

export
setBits64 : HasIO io => Buffer -> (loc : Int) -> (val : Bits64) -> io ()
setBits64 buf loc val = do
  ignore $ pure $ erlUnsafeCall ErlTerm "mutable_storage" "buffer_set_bits64" [MkRaw buf, loc, MkRaw val]

export
getBits64 : HasIO io => Buffer -> (loc : Int) -> io Bits64
getBits64 buf loc = do
  MkRaw val <- pure $ erlUnsafeCall (Raw Bits64) "mutable_storage" "buffer_get_bits64" [MkRaw buf, loc]
  pure val

export
setInt32 : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setInt32 buf loc val = do
  ignore $ pure $ erlUnsafeCall ErlTerm "mutable_storage" "buffer_set_int32" [MkRaw buf, loc, val]

export
getInt32 : HasIO io => Buffer -> (loc : Int) -> io Int
getInt32 buf loc = do
  pure $ erlUnsafeCall Int "mutable_storage" "buffer_get_int32" [MkRaw buf, loc]

export
setInt : HasIO io => Buffer -> (loc : Int) -> (val : Int) -> io ()
setInt buf loc val = do
  ignore $ pure $ erlUnsafeCall ErlTerm "mutable_storage" "buffer_set_int64" [MkRaw buf, loc, val]

export
getInt : HasIO io => Buffer -> (loc : Int) -> io Int
getInt buf loc = do
  pure $ erlUnsafeCall Int "mutable_storage" "buffer_get_int64" [MkRaw buf, loc]

export
setDouble : HasIO io => Buffer -> (loc : Int) -> (val : Double) -> io ()
setDouble buf loc val = do
  ignore $ pure $ erlUnsafeCall ErlTerm "mutable_storage" "buffer_set_double" [MkRaw buf, loc, val]

export
getDouble : HasIO io => Buffer -> (loc : Int) -> io Double
getDouble buf loc = do
  pure $ erlUnsafeCall Double "mutable_storage" "buffer_get_double" [MkRaw buf, loc]

export
stringByteLength : String -> Int
stringByteLength str =
  erlUnsafeCall Int "erlang" "byte_size" [str]

export
setString : HasIO io => Buffer -> (loc : Int) -> (val : String) -> io ()
setString buf loc val = do
  binary <- pure $ erlUnsafeCall String "erlang" "iolist_to_binary" [val]
  ignore $ pure $ erlUnsafeCall ErlTerm "mutable_storage" "buffer_set_binary" [MkRaw buf, loc, binary]

export
getString : HasIO io => Buffer -> (loc : Int) -> (len : Int) -> io String
getString buf loc len = do
  pure $ erlUnsafeCall String "mutable_storage" "buffer_get_binary" [MkRaw buf, loc, len]

export covering
bufferData : HasIO io => Buffer -> io (List Int)
bufferData buf = do
  len <- rawSize buf
  unpackTo [] len
  where
    covering
    unpackTo : List Int -> Int -> io (List Int)
    unpackTo acc 0 = pure acc
    unpackTo acc loc = do
      val <- getByte buf (loc - 1)
      unpackTo (val :: acc) (loc - 1)

export
copyData : HasIO io => (src : Buffer) -> (start, len : Int) -> (dest : Buffer) -> (loc : Int) -> io ()
copyData src start len dest loc = do
  ignore $ pure $ erlUnsafeCall ErlTerm "mutable_storage" "buffer_copy" [MkRaw src, start, len, MkRaw dest, loc]

-- Create a new buffer by reading all the contents from the given file
-- Fails if no bytes can be read or buffer can't be created
export
createBufferFromFile : HasIO io => (filePath : String) -> io (Either FileError Buffer)
createBufferFromFile filePath = do
  result <- pure $ erlUnsafeCall ErlTerm "file" "read_file" [filePath]
  let Right str = erlDecode (okTuple string) result
    | _ => pure (Left FileReadError)
  let strSize = erlUnsafeCall Int "erlang" "byte_size" [str]
  Just buf <- newBuffer strSize
    | Nothing => pure (Left FileReadError)
  setString buf 0 str
  pure (Right buf)

-- TODO: `maxbytes` is unused
export
writeBufferToFile : HasIO io => (filePath : String) -> Buffer -> (maxbytes : Int) -> io (Either FileError ())
writeBufferToFile filePath buf maxBytes = do
  size <- rawSize buf
  bin <- getString buf 0 (min size maxBytes)
  result <- pure $ erlUnsafeCall ErlTerm "file" "write_file" [filePath, bin]
  pure $ erlDecodeDef (Left FileWriteError) (exact (MkAtom "ok") *> pure (Right ())) result

export
resizeBuffer : HasIO io => Buffer -> Int -> io (Maybe Buffer)
resizeBuffer buf newSize = do
  ignore $ pure $ erlUnsafeCall ErlTerm "mutable_storage" "buffer_resize" [MkRaw buf, newSize]
  pure (Just buf)


text:
> module Double.Operations

> import Data.So
> import Data.Fin

> import Double.Predicates
> import So.Properties

> %default total
> %access public export

> |||
> fromNat : (n : Nat) -> Double
> fromNat  Z    = 0.0
> fromNat (S m) = 1.0 + (fromNat m)

> |||
> fromFin : {n : Nat} -> Fin n -> Double
> fromFin = fromNat . finToNat

> |||
> mkLinear : Double -> Double -> Double -> Double
> mkLinear a b x = a + b * x

> mkLinearStep : (x1 : Double) -> (x2 : Double) -> Positive (x2 - x1) ->
>                (y1 : Double) -> (y2 : Double) ->
>                Double -> Double
> mkLinearStep x1 x2 px2mx1 y1 y2 x with (decSo (x < x1))
>   | Yes _ = y1
>   | No  _ with (decSo (x1 <= x && x <= x2))
>     | Yes _ = y1 * (1.0 - alpha) + y2 * alpha where
>         alpha : Double
>         alpha = (x - x1) / (x2 - x1)
>     | No  _ = y2

ext: lidr

max_stars_repo_name: zenntenn/IdrisLibs

max_issues_repo_name: zenntenn/IdrisLibs

max_forks_repo_name: zenntenn/IdrisLibs


text:
module Data.Morphisms

public export
record Morphism a b where
  constructor Mor
  applyMor : a -> b

infixr 1 ~>

public export
(~>) : Type -> Type -> Type
(~>) = Morphism

public export
record Endomorphism a where
  constructor Endo
  applyEndo : a -> a

public export
record Kleislimorphism (f : Type -> Type) a b where
  constructor Kleisli
  applyKleisli : a -> f b

export
Functor (Morphism r) where
  map f (Mor a) = Mor $ f . a

export
Applicative (Morphism r) where
  pure a = Mor $ const a
  (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r

export
Monad (Morphism r) where
  (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r

export
Semigroup a => Semigroup (Morphism r a) where
  f <+> g = Mor $ \r => (applyMor f) r <+> (applyMor g) r

export
Monoid a => Monoid (Morphism r a) where
  neutral = Mor \r => neutral

export
Semigroup (Endomorphism a) where
  (Endo f) <+> (Endo g) = Endo $ g . f

export
Monoid (Endomorphism a) where
  neutral = Endo id

export
Functor f => Functor (Kleislimorphism f a) where
  map f (Kleisli g) = Kleisli (map f . g)

export
Applicative f => Applicative (Kleislimorphism f a) where
  pure a = Kleisli $ const $ pure a
  (Kleisli f) <*> (Kleisli a) = Kleisli $ \r => f r <*> a r

export
Monad f => Monad (Kleislimorphism f a) where
  (Kleisli f) >>= g = Kleisli $ \r => do
    k1 <- f r
    applyKleisli (g k1) r

-- Applicative is a bit too strong, but there is no suitable superclass
export
(Semigroup a, Applicative f) => Semigroup (Kleislimorphism f r a) where
  f <+> g = Kleisli \r => (<+>) <$> (applyKleisli f) r <*> (applyKleisli g) r

export
(Monoid a, Applicative f) => Monoid (Kleislimorphism f r a) where
  neutral = Kleisli \r => pure neutral

export
Cast (Endomorphism a) (Morphism a a) where
  cast (Endo f) = Mor f

export
Cast (Morphism a a) (Endomorphism a) where
  cast (Mor f) = Endo f

export
Cast (Morphism a (f b)) (Kleislimorphism f a b) where
  cast (Mor f) = Kleisli f

export
Cast (Kleislimorphism f a b) (Morphism a (f b)) where
  cast (Kleisli f) = Mor f


text:
-- 参考Belleve@zhihu

data Tree:Type -> Type where
    Leaf: a-> Tree a
    Branch : a->Tree a->Tree a->Tree a

flipTree : Tree a-> Tree a
flipTree (Leaf x)= Leaf x
flipTree (Branch x l r) = Branch x (flipTree r) (flipTree l)

flipTreeSym :  (t:Tree a) -> t = flipTree (flipTree t)
flipTreeSym (Leaf x) = Refl
flipTreeSym (Branch x l r) = do
    let recL = flipTreeSym l
    let recR = flipTreeSym r
    rewrite recL in
        rewrite recR in Refl

{-
map_id : Functor f => f a -> f a
map_id : map id

interface Functor f => VerifiedFunctor (f:Type->Type) where
    identity: (fa:fa) -> map_id fa = fa
    dist : (fa:fa) -> (g:b->c)->(h:a->b)->map (g.h) fa = (map g).(map h) $ fa

VerifiedFunctor List where
    identity [] = Refl
    identity (x:xs) = let ih = (identity xs) in rewrite ih in Refl

dist [] _ _ = Refl
dist (x:xs) g h = let ih = (dist xs g h) in rewrite ih in Refl
-}

max_stars_repo_name: shij-hsu/idr

max_issues_repo_name: shij-hsu/idr

max_forks_repo_name: shij-hsu/idr


text:
module Language.LSP.Message.SelectionRange

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.Progress
import Language.LSP.Message.TextDocument
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange
public export
record SelectionRangeClientCapabilities where
  constructor MkSelectionRangeClientCapabilities
  dynamicRegistration : Maybe Bool
%runElab deriveJSON defaultOpts `{{SelectionRangeClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange
public export
record SelectionRangeOptions where
  constructor MkSelectionRangeOptions
  workDoneProgress : Maybe Bool
%runElab deriveJSON defaultOpts `{{SelectionRangeOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange
public export
record SelectionRangeRegistrationOptions where
  constructor MkSelectionRangeRegistrationOptions
  workDoneProgress : Maybe Bool
  documentSelector : OneOf [DocumentSelector, Null]
  id               : Maybe String
%runElab deriveJSON defaultOpts `{{SelectionRangeRegistrationOptions}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange
public export
record SelectionRangeParams where
  constructor MkSelectionRangeParams
  workDoneToken      : Maybe ProgressToken
  partialResultToken : Maybe ProgressToken
  textDocument       : TextDocumentIdentifier
  positions          : List Position
%runElab deriveJSON defaultOpts `{{SelectionRangeParams}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_selectionRange
public export
record SelectionRange where
  constructor MkSelectionRange
  range  : Range
  parent : Maybe (Inf SelectionRange)

export -- FIXME: Can I avoid asser_total? Maybe indexing by the depth of the structure?
ToJSON SelectionRange where
  toJSON (MkSelectionRange range parent) = assert_total $
    JObject (catMaybes [ Just ("range", toJSON range)
                       , (MkPair "parent" . toJSON) <$> parent
                       ])

export covering
FromJSON SelectionRange where
  fromJSON (JObject arg) =
    pure MkSelectionRange <*> (lookup "range" arg >>= fromJSON)
                          <*> (pure $ lookup "parent" arg >>= fromJSON)
  fromJSON _ = neutral


text:
||| Common types and utility funtions for the LSP server implementation.
|||
||| (C) The Idris Community, 2021
module Server.Utils

import Core.Core
import Core.FC
import Core.Name
import Data.Bits
import Data.List
import Data.Strings
import Language.JSON
import Libraries.Data.PosMap
import System.File

||| Gets a specific component of a reference, using the supplied projection.
export
gets : (l : label) -> Ref l a => (a -> b) -> Core b
gets l f = f <$> get l

||| Reads a single header from an LSP message on the supplied file handle.
||| Headers end with the string "\r\n".
export
fGetHeader : (h : File) -> Core (Either FileError String)
fGetHeader handle = do
  Right l <- coreLift $ fGetLine handle
    | Left err => pure $ Left err
  -- TODO: reading up to a string should probably be handled directly by the FFI primitive
  --       or at least in a more efficient way in Idris2
  if isSuffixOf "\r\n" l
     then pure $ Right l
     else (map (l ++)) <$> fGetHeader handle

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

private
showChar : Char -> String
showChar c
  = case c of
         '\b' => "\\b"
         '\f' => "\\f"
         '\n' => "\\n"
         '\r' => "\\r"
         '\t' => "\\t"
         '\\' => "\\\\"
         '"'  => "\\\""
         c => if isControl c || c >= '\127'
                 then "\\u" ++ b16ToHexString (cast (ord c)) -- quick hack until b16ToHexString is available in Idris2
                 else singleton c

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

export
stringify : JSON -> String
stringify JNull = "null"
stringify (JBoolean x) = if x then "true" else "false"
stringify (JNumber x) = let s = show x in
                            if isSuffixOf ".0" s
                               then substr 0 (length s `minus` 2) s
                               else s
stringify (JString x) = showString x
stringify (JArray xs) = "[" ++ stringifyValues xs ++ "]"
  where
    stringifyValues : List JSON -> String
    stringifyValues [] = ""
    stringifyValues (x :: xs) = stringify x
                             ++ if isNil xs
                                   then ""
                                   else "," ++ stringifyValues xs
stringify (JObject xs) = "{" ++ stringifyProps xs ++ "}"
  where
    stringifyProp : (String, JSON) -> String
    stringifyProp (key, value) = showString key ++ ":" ++ stringify value

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

export
findInTreeLoc : FilePos -> PosMap (NonEmptyFC, Name) -> Maybe (NonEmptyFC, Name)
findInTreeLoc p m = head' $ 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 - sr2)

export
findInTree : FilePos -> PosMap (NonEmptyFC, Name) -> Maybe Name
findInTree p m = snd <$> findInTreeLoc p m

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


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

checkEqNat : (num1 : Nat) -> (num2 : Nat) -> Maybe (num1 = num2)
checkEqNat Z Z = Just Refl
checkEqNat Z (S k) = Nothing
checkEqNat (S k) Z = Nothing
checkEqNat (S k) (S j) = case checkEqNat k j of
                            Nothing => Nothing
                            Just eq => Just (cong eq)

exactLength : (len : Nat) -> (input : Vect m a) -> Maybe (Vect len a)
exactLength {m} len input = case decEq m len of
                                Yes Refl => Just input
                                No contra => Nothing

sameCons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys
sameCons Refl = Refl

sameLists : {xs : List a} -> {ys : List a} -> x = y -> xs = ys -> x :: xs = y :: ys
sameLists Refl Refl = Refl

data ThreeEq : (x1 : a) -> (x2 : a) -> (x3 : a) -> Type where
    Same : (x : a) -> ThreeEq x x x

allSameS : (x, y, z : Nat) -> ThreeEq x y z -> ThreeEq (S x) (S y) (S z)
allSameS z z z (Same z) = Same (S z)


text:
ts1 : Applicative m => m a -> m b -> m (a, a, b)
ts1 as bs = [| (,,) as as bs |]

ts2 : Applicative m => m a -> m b -> m (a, a, b)
ts2 as bs = [| (as, as, bs) |]

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module Compiler.Separate

import public Core.FC
import public Core.Name
import public Core.Name.Namespace
import public Core.CompileExpr
import public Compiler.VMCode
import public Libraries.Data.Graph
import public Libraries.Data.SortedMap
import public Libraries.Data.SortedSet
import public Libraries.Data.StringMap

import Core.Hash
import Core.TT
import Data.List
import Data.List1
import Data.Vect
import Data.Maybe

%default covering

-- Compilation unit IDs are intended to be opaque,
-- just to be able to express dependencies via keys in a map and such.
export
record CompilationUnitId where
  constructor CUID
  int : Int

export
Eq CompilationUnitId where
  CUID x == CUID y = x == y

export
Ord CompilationUnitId where
  compare (CUID x) (CUID y) = compare x y

export
Hashable CompilationUnitId where
  hashWithSalt h (CUID int) = hashWithSalt h int

||| A compilation unit is a set of namespaces.
|||
||| The record is parameterised by the type of the definition,
||| which makes it reusable for various IRs provided by getCompileData.
public export
record CompilationUnit def where
  constructor MkCompilationUnit

  ||| Unique identifier of a compilation unit within a CompilationUnitInfo record.
  id : CompilationUnitId

  ||| Namespaces contained within the compilation unit.
  namespaces : List1 Namespace

  ||| Other units that this unit depends on.
  dependencies : SortedSet CompilationUnitId

  ||| The definitions belonging into this compilation unit.
  definitions : List (Name, def)

export
Hashable def => Hashable (CompilationUnit def) where
  hashWithSalt h cu =
    h `hashWithSalt` SortedSet.toList cu.dependencies
      `hashWithSalt` cu.definitions

private
getNS : Name -> Namespace
getNS (NS ns _) = ns
getNS _ = emptyNS

||| Group definitions by namespace.
private
splitByNS : List (Name, def) -> List (Namespace, List (Name, def))
splitByNS = SortedMap.toList . foldl addOne SortedMap.empty
  where
    addOne
      : SortedMap Namespace (List (Name, def))
      -> (Name, def)
      -> SortedMap Namespace (List (Name, def))
    addOne nss ndef@(n, _) =
      SortedMap.mergeWith
        (++)
        (SortedMap.singleton (getNS n) [ndef])
        nss

public export
interface HasNamespaces a where
  ||| Return the set of namespaces mentioned within
  nsRefs : a -> SortedSet Namespace

-- For now, we have instances only for NamedDef and VMDef.
-- For other IR representations, we'll have to add more instances.
-- This is not hard, just a bit of tedious mechanical work.
mutual
  export
  HasNamespaces NamedCExp where
    nsRefs (NmLocal fc n) = SortedSet.empty
    nsRefs (NmRef fc n) = SortedSet.singleton $ getNS n
    nsRefs (NmLam fc n rhs) = nsRefs rhs
    nsRefs (NmLet fc n val rhs) = nsRefs val <+> nsRefs rhs
    nsRefs (NmApp fc f args) = nsRefs f <+> concatMap nsRefs args
    nsRefs (NmCon fc cn ci tag args) = concatMap nsRefs args
    nsRefs (NmForce fc reason rhs) = nsRefs rhs
    nsRefs (NmDelay fc reason rhs) = nsRefs rhs
    nsRefs (NmErased fc) = SortedSet.empty
    nsRefs (NmPrimVal ft x) = SortedSet.empty
    nsRefs (NmOp fc op args) = concatMap nsRefs args
    nsRefs (NmExtPrim fc n args) = concatMap nsRefs args
    nsRefs (NmConCase fc scrut alts mbDflt) =
      nsRefs scrut <+> concatMap nsRefs alts <+> concatMap nsRefs mbDflt
    nsRefs (NmConstCase fc scrut alts mbDflt) =
      nsRefs scrut <+> concatMap nsRefs alts <+> concatMap nsRefs mbDflt
    nsRefs (NmCrash fc msg) = SortedSet.empty

  export
  HasNamespaces NamedConAlt where
    nsRefs (MkNConAlt n ci tag args rhs) = nsRefs rhs

  export
  HasNamespaces NamedConstAlt where
    nsRefs (MkNConstAlt c rhs) = nsRefs rhs

  export
  HasNamespaces NamedDef where
    nsRefs (MkNmFun argNs rhs) = nsRefs rhs
    nsRefs (MkNmCon tag arity nt) = SortedSet.empty
    nsRefs (MkNmForeign ccs fargs rty) = SortedSet.empty
    nsRefs (MkNmError rhs) = nsRefs rhs

export
HasNamespaces VMInst where
  nsRefs (DECLARE x) = empty
  nsRefs START = empty
  nsRefs (ASSIGN x y) = empty
  nsRefs (MKCON x tag args) = either (const empty) (singleton . getNS) tag
  nsRefs (MKCLOSURE x n missing args) = singleton $ getNS n
  nsRefs (MKCONSTANT x y) = empty
  nsRefs (APPLY x f a) = empty
  nsRefs (CALL x tailpos n args) = singleton $ getNS n
  nsRefs (OP x y xs) = empty
  nsRefs (EXTPRIM x n xs) = singleton $ getNS n
  nsRefs (CASE x alts def) =
    maybe empty (concatMap nsRefs) def <+>
    concatMap ((concatMap nsRefs) . snd) alts <+>
    concatMap ((either (const empty) (singleton . getNS)) . fst) alts
  nsRefs (CONSTCASE x alts def) =
    maybe empty (concatMap nsRefs) def <+>
    concatMap ((concatMap nsRefs) . snd) alts
  nsRefs (PROJECT x value pos) = empty
  nsRefs (NULL x) = empty
  nsRefs (ERROR x) = empty

export
HasNamespaces VMDef where
  nsRefs (MkVMFun args is) = concatMap nsRefs is
  nsRefs (MkVMForeign _ _ _) = empty
  nsRefs (MkVMError is) = concatMap nsRefs is

-- a slight hack for convenient use with CompileData.namedDefs
export
HasNamespaces a => HasNamespaces (FC, a) where
  nsRefs (_, x) = nsRefs x

-- another slight hack for convenient use with CompileData.namedDefs
export
Hashable def => Hashable (FC, def) where
  -- ignore FC in hash, like everywhere else
  hashWithSalt h (fc, x) = hashWithSalt h x

||| Output of the codegen separation algorithm.
||| Should contain everything you need in a separately compiling codegen.
public export
record CompilationUnitInfo def where
  constructor MkCompilationUnitInfo

  ||| Compilation units computed from the given definitions,
  ||| ordered topologically, starting from units depending on no other unit.
  compilationUnits : List (CompilationUnit def)

  ||| Mapping from ID to CompilationUnit.
  byId : SortedMap CompilationUnitId (CompilationUnit def)

  ||| Maps each namespace to the compilation unit that contains it.
  namespaceMap : SortedMap Namespace CompilationUnitId

||| Group the given definitions into compilation units for separate code generation.
export
getCompilationUnits : HasNamespaces def => List (Name, def) -> CompilationUnitInfo def
getCompilationUnits {def} defs =
  let
    -- Definitions grouped by namespace.
    defsByNS : SortedMap Namespace (List (Name, def))
      = SortedMap.fromList $ splitByNS defs

    -- Mapping from a namespace to all namespaces mentioned within.
    -- Represents graph edges pointing in that direction.
    nsDeps : SortedMap Namespace (SortedSet Namespace)
      = foldl (SortedMap.mergeWith SortedSet.union) SortedMap.empty
          [ SortedMap.singleton (getNS n) (SortedSet.delete (getNS n) (nsRefs d))
          | (n, d) <- defs
          ]

    -- Strongly connected components of the NS dep graph,
    -- ordered by output degree ascending.
    --
    -- Each SCC will become a compilation unit.
    components : List (List1 Namespace)
      = List.reverse $ tarjan nsDeps  -- tarjan generates reverse toposort

    -- Maps a namespace to the compilation unit that contains it.
    nsMap : SortedMap Namespace CompilationUnitId
      = SortedMap.fromList [(ns, cuid) | (cuid, nss) <- withCUID components, ns <- List1.forget nss]

    -- List of all compilation units, ordered by number of dependencies, ascending.
    units : List (CompilationUnit def)
      = [mkUnit nsDeps nsMap defsByNS cuid nss | (cuid, nss) <- withCUID components]

  in MkCompilationUnitInfo
      { compilationUnits = units
      , byId = SortedMap.fromList [(unit.id, unit) | unit <- units]
      , namespaceMap = nsMap
      }

  where
    withCUID : List a -> List (CompilationUnitId, a)
    withCUID xs = [(CUID $ cast i, x) | (i, x) <- zip [0..length xs] xs]

    ||| Wrap all information in a compilation unit record.
    mkUnit :
      SortedMap Namespace (SortedSet Namespace)
      -> SortedMap Namespace CompilationUnitId
      -> SortedMap Namespace (List (Name, def))
      -> CompilationUnitId -> List1 Namespace -> CompilationUnit def
    mkUnit nsDeps nsMap defsByNS cuid nss =
      MkCompilationUnit
      { id = cuid
      , namespaces = nss
      , dependencies = SortedSet.delete cuid dependencies
      , definitions = definitions
      }
     where
      dependencies : SortedSet CompilationUnitId
      dependencies = SortedSet.fromList $ do
        ns <- List1.forget nss  -- NS contained within
        depsNS <- SortedSet.toList $  -- NS we depend on
          fromMaybe SortedSet.empty $
            SortedMap.lookup ns nsDeps

        case SortedMap.lookup depsNS nsMap of
          Nothing => []
          Just depCUID => [depCUID]

      definitions : List (Name, def)
      definitions = concat [fromMaybe [] $ SortedMap.lookup ns defsByNS | ns <- nss]


text:
module Chapter6

import Data.Vect

Position : Type
Position = (Double, Double)

-- this showcases that a type signature is really an expression.
valToString : (isInt : Bool) -> (case isInt of
                                      False => String
                                      True => Int) -> String
valToString False x = trim x
valToString True x = cast x

AdderType : (num_args : Nat) -> Type
AdderType Z = Int
AdderType (S k) = Int -> AdderType k   -- Mind Blown!
                                       -- what exactly is -> ?
                                       -- I can't do :t (->) on it..
                                       -- I can do :t Int -> Nat

-- Seems like we require an accumulator...
--adder : (num_args : Nat) -> AdderType num_args
--adder Z = 0
--adder (S k) = \x => ?h

adder : (num_args : Nat) -> (acc : Int) -> AdderType num_args
adder Z acc = acc
adder (S k) acc = \x => adder k (acc + x)

AdderType2 : (num_args : Nat) -> Type -> Type
AdderType2 Z x = x
AdderType2 (S k) x = x -> AdderType2 k x

adder2 : Num t => (num_args : Nat) -> t -> AdderType2 num_args t
adder2 Z acc = acc
adder2 (S k) acc = \x => adder2 k (x + acc)

-- Let's go to type-checked Printf.idr!

--exercises
--ex1

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

testMatrix : Matrix 2 3
testMatrix = [[0,0,0], [0,0,0]]

--ex2 (see Printf.idr)

--ex3
TupleVect : Nat -> Type -> Type
TupleVect Z x = ()
TupleVect (S k) x = (x, TupleVect k x)

test : TupleVect 4 Nat
test = (1,2,3,4,())

-- Go to DataStore.idr

max_stars_repo_name: neduard/type-driven-development

max_issues_repo_name: neduard/type-driven-development

max_forks_repo_name: neduard/type-driven-development


text:
module Bezout

import Data.Vect
import Data.Fin

{-Copied from Chinmay's code. Gives quotient and remainder on divison-}
Eucl: (a: Nat) -> (b: Nat) -> (Nat, Nat)
Eucl Z b = (0,0)
Eucl (S k) b = case (lte (S (S k)) b) of
                    False => (S(fst(Eucl (minus (S k) b) b)), snd(Eucl (minus (S k) b) b))
                    True => (0, S k)

{-Let rk be the remainder in the Euclidean algorithm at the k-2th step.
Let rk = ak*r0 + bk*r1 where r0 and r1 are the original inputs.Correspondingly  rsk = ask*r0 + bsk*r1 where sk = k+1
Then the I am going to the next step in the Euclid algorithm and changing the coefficients.
These formulas can be easily derived.-}
Euclnos: (Int,Int,Int,Int,Int,Int)->(Int,Int,Int,Int,Int,Int)
Euclnos (rk, rsk ,ak ,ask, bk ,bsk) = (rsk,rssk,ask,assk,bsk,bssk) where
  rssk = cast(snd (Eucl (cast rk) (cast rsk)))
  bssk =bk-bsk* (cast(fst (Eucl (cast rk) (cast rsk))))
  assk =ak-ask* (cast(fst (Eucl (cast rk) (cast rsk))))
{-Does the Euclnos repeatedy until the remainder is zero. Then the previous remainder is the GCD.-}
Bezouttuple: (Int,Int,Int,Int,Int,Int)->(Int,Int,Int,Int,Int,Int)
Bezouttuple (rk, rsk ,ak ,ask, bk, bsk) = case rsk of
                                        0 => (rk, rsk, ak, ask, bk, bsk)
                                        _ => (Bezouttuple (Euclnos (rk ,rsk, ak ,ask ,bk ,bsk)))
{-Returns 2 particular integers out of a 6 tuple-}
returnab: (Int,Int,Int,Int,Int,Int)->(Int,Int)
returnab (a ,b ,c ,d, e ,f)  = (c,e)
{-Returns the Bezout coefficients-}
Bezout : Nat ->Nat ->(Int, Int)
Bezout k j =  (returnab(Bezouttuple((cast k) , (cast j),1, 0 ,0 ,1)))


text:
import Data.List

data SnocList : List a -> Type where
     Empty : SnocList []
     Snoc : (x, xs : _) -> (rec : SnocList xs) -> SnocList (xs ++ [x])

snocListHelp : {input : _} ->
               (snoc : SnocList input) -> (rest : List a) -> SnocList (input ++ rest)
snocListHelp snoc [] = rewrite appendNilRightNeutral input in snoc
snocListHelp snoc (x :: xs)
    = rewrite appendAssociative input [x] xs in
              snocListHelp (Snoc x input snoc) xs

snocList : (xs : List a) -> SnocList xs
snocList xs = snocListHelp Empty xs

my_reverse_help : (input : List a) -> SnocList input -> List a
my_reverse_help [] Empty = []
my_reverse_help (xs ++ [x]) (Snoc x xs rec) = x :: my_reverse_help xs rec

my_reverse1 : List a -> List a
my_reverse1 input = my_reverse_help input (snocList input)

my_reverse : List a -> List a
my_reverse input with (snocList input)
  my_reverse [] | Empty = []
  my_reverse (xs ++ [x]) | (Snoc x xs rec) = x :: my_reverse xs | rec