text:
module Utils

import Data.Vect

import RFC.Utils

%access public

-- ----------------------------------------------------------------- [ DayTime ]

||| Embarrassingly bad function to do conversion between unix time and
||| date time
private
convert : Int -> DayTime
convert i = MkDaytime
              (getYears + 1970)
              getMonths
              getDays
              getHours
              getMins
              getSecs
  where
    getYears : Int
    getYears = div i 31556926

    epoM : Int
    epoM = mod i 31556926

    getMonths : Int
    getMonths = div epoM 2629743

    epoD : Int
    epoD = mod epoM 2629743

    getDays : Int
    getDays = div epoD 86400

    epoH : Int
    epoH = mod epoD 86400

    getHours : Int
    getHours = div epoH 3600

    epoMin : Int
    epoMin = mod epoH 3600

    getMins : Int
    getMins = div epoMin 60

    epoSec : Int
    epoSec = mod epoMin 60

    getSecs : Int
    getSecs = epoSec

||| Return the daytime if possible.
%assert_total
getDayTime : Either String DayTime
getDayTime = let t = systime in
    if (t /= 0)
      then Right (convert t)
      else Left "No time"

  where
    systime : Int
    systime = unsafePerformIO time

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

max_stars_repo_name: jfdm/idris-protocol-examples

max_issues_repo_name: jfdm/idris-protocol-examples

max_forks_repo_name: jfdm/idris-protocol-examples


text:
module Replica.App.New

import Control.App
import Control.App.Console

import Data.String

import Language.JSON

import Replica.App.FileSystem
import Replica.App.Format
import Replica.App.Log
import Replica.App.Replica
import Replica.Command.New
import Replica.Other.Decorated
import Replica.Other.String

data NewContext : Type where

replicaURL : String
replicaURL = "https://raw.githubusercontent.com/ReplicaTest/replica-dhall/main/package.dhall"

jsonTestSample : JSON
jsonTestSample = JObject
 [ ("command", JString "echo \"Hello, World!\"")
 , ("description", JString "This test is a placeholder, you can edit it.")
 , ("spaceSensitive", JBoolean False)
 , ("status", JBoolean True)
 , ("stdOut", JObject
     [ ("generated", JBoolean False)
     , ("consecutive", JArray $ JString <$> ["Hello", "World"])
     , ("end", JString "!")
     ])
  ]

dhallTestSample : String
dhallTestSample =
  #"""
   let hello = Test.Success ::
      { command = "echo \"Hello, World!\""
      , description = Some "This test is a placeholder, you can edit it."
      , spaceSensitive = False
      , stdOut = Expectation ::
          {consecutive = ["Hello", "World"], end = Some "!"}
      }
   """#

jsonContent : (withSample : Bool) -> JSON
jsonContent withSample =
  JObject $ if withSample then [("hello", jsonTestSample)] else []

dhallContent : (withSample : Bool) -> String
dhallContent withSample = removeTrailingNL $ unlines
  [ "let Replica = \{replicaURL}"
  , "let Prelude = Replica.Prelude"
  , "let Test = Replica.Test"
  , "let Status = Replica.Status"
  , "let Expectation = Replica.Expectation"
  , ""
  , if withSample
       then dhallTestSample
       else ""
  , ""
  , "let tests : Replica.Type = \{sample}"
  , ""
  , "in tests"
  ]
  where
    sample : String
    sample = if withSample then "toMap { hello }" else "[] : Replica.Type"

export
newReplica : FileSystem (FSError :: e) =>
  Has
    [ State NewContext NewCommand
    , Exception ReplicaError
    , Console
    ] e =>
  App e ()
newReplica = do
  ctx <- get NewContext
  let content = case ctx.format of
        JSON => format 2 $ jsonContent ctx.includeSample
        Dhall => dhallContent ctx.includeSample
  catchNew (writeFile ctx.file content)
    (\err : FSError => throw (CantAccessTestFile ctx.file))
  putStrLn "Test file created (\{show ctx.format}): \{ctx.file}"

ext: idr

max_stars_repo_name: claymager/REPLica

max_issues_repo_name: claymager/REPLica

max_forks_repo_name: claymager/REPLica


text:
longer : String -> String -> Nat
longer word1 word2
    = let len1 = length word1
          len2 = length word2 in
          if len1 > len2 then len1 else len2

longerWord : String -> String -> String
longerWord word1 word2
    = case (length word1 == length word2) of
           True  => word1
           False => word2

pythagoras : Double -> Double -> Double
pythagoras x y = sqrt (square x + square y)
    where
      square : Double -> Double
      square x = x * x

max_stars_repo_name: wdomitrz/Coq-Exercises

max_issues_repo_name: wdomitrz/Coq-Exercises

max_forks_repo_name: wdomitrz/Coq-Exercises


text:
module Sub14Apply108x72

import ProofColDivSeqBase
import ProofColDivSeqPostulate

%default total
-- %language ElabReflection

-- 3(36x+24) --F[5,-2]->E[2,-4]--> 3(8x+5)
fe108x72To24x15 :
  (o:Nat) ->  P (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                              (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                  (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))) 2
    -> P (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))) 2
fe108x72To24x15 o prf =
  let prf2 = lvDown (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                              (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                  (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))) 2
                    prf in
    let prf3 = fe108x72To24x15' o prf2 in lvDown (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))) 3 prf3

export
apply108x72 : P (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                              (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                  (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))) 2
  -> (m : Nat **
        (LTE (S m)
             (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                 (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                           (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                     (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))),
         P m 2))
apply108x72 {o} col = let col2 = fe108x72To24x15 o col in ((S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))
                                                           ** (lte108x72 o, col2)) where
  lte108x72 : (o:Nat) -> LTE (S (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))
          (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                              (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                        (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                  (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o))) (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))))))))
  lte108x72 Z = (lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . lteSuccRight . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc . LTESucc) LTEZero
  lte108x72 (S o) = let lemma = lte108x72 o in

    rewrite (sym (plusSuccRightSucc o o)) in

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

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

    rewrite (sym (plusSuccRightSucc (plus o o)  o)) in

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

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

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

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

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


text:
module BigStep

-- Relation 'BigStep' for fully reducing terms
-- in the simply-typed lambda calculus to values.

import Term
import Subst

%default total
%access public export

-----------------------------------------------------------------------
-- Begin: BIG-STEP EVALUATION RELATION FOR TERMS IN THE LAMBDA CALCULUS

-- The relation 'BigStep' defines evaluation of terms in the lambda
-- calculus following big-step semantics.
--
-- Big-step semantics fully evaluates terms to values.
-- (A proof of this statement appears below.)
data BigStep : Term [] t -> (y: Term [] t) -> Type where
  BStValue    : (v : Value e) -> BigStep e e
  --
  BStApp      : BigStep e1 (TAbs e1') ->
                BigStep e2 e2' ->
                BigStep (subst e2' First e1') e ->
                BigStep (TApp e1 e2) e
  --
  BStFix      : BigStep e (TAbs e') ->
                BigStep (subst (TFix (TAbs e')) First e') e'' ->
                BigStep (TFix e) e''
  --
  BStSucc     : BigStep e e' ->
                BigStep (TSucc e) (TSucc e')
  --
  BStPredZero : BigStep e TZero ->
                BigStep (TPred e) TZero
  --
  BStPredSucc : BigStep e (TSucc e') ->
                BigStep (TPred e) e'
  --
  BStIfzZero  : BigStep e1 TZero ->
                BigStep e2 e ->
                BigStep (TIfz e1 e2 _) e
  --
  BStIfzSucc  : BigStep e1 (TSucc _) ->
                BigStep e3 e ->
                BigStep (TIfz e1 _ e3) e

bigStepFst : {e : Term [] t} -> BigStep e _ -> Term [] t
bigStepFst {e = e} _ = e

bigStepSnd : {e : Term [] t} -> BigStep _ e -> Term [] t
bigStepSnd {e = e} _ = e

bigStepValue : BigStep _ e -> Value e
bigStepValue (BStValue v)     = v
bigStepValue (BStApp _ _ z)   = bigStepValue z
bigStepValue (BStFix _ z)     = bigStepValue z
bigStepValue (BStSucc z)      = VSucc (bigStepValue z)
bigStepValue (BStPredZero _)  = VZero
bigStepValue (BStPredSucc z)  = case bigStepValue z of
                                    VZero impossible
                                    VSucc v => v
bigStepValue (BStIfzZero _ z) = bigStepValue z
bigStepValue (BStIfzSucc _ z) = bigStepValue z

bigStepValueIrreducible : BigStep e1 e2 -> Value e1 -> e1 = e2
bigStepValueIrreducible (BStValue VZero) VZero   = Refl
bigStepValueIrreducible (BStValue v1) (VSucc v2) = Refl
bigStepValueIrreducible (BStSucc bst) (VSucc v)  =
  cong $ bigStepValueIrreducible bst v
bigStepValueIrreducible (BStValue v)  VAbs       = Refl

bigStepTransitive : BigStep e1 e2 -> BigStep e2 e3 -> BigStep e1 e3
bigStepTransitive (BStValue v) bst = bst
bigStepTransitive (BStApp x w t) y = BStApp x w $ bigStepTransitive t y
bigStepTransitive (BStFix x w) y = BStFix x $ bigStepTransitive w y
bigStepTransitive (BStSucc x) (BStValue v) = BStSucc x
bigStepTransitive (BStSucc x) (BStSucc y)  = BStSucc $ bigStepTransitive x y
bigStepTransitive (BStPredZero x) (BStValue v) = BStPredZero x
bigStepTransitive (BStPredSucc x) y = let bst1 = BStSucc y
                                          bst2 = bigStepTransitive x bst1
                                      in BStPredSucc bst2
bigStepTransitive (BStIfzZero w s) y = BStIfzZero w (bigStepTransitive s y)
bigStepTransitive (BStIfzSucc w s) y = BStIfzSucc w (bigStepTransitive s y)

-- End: BIG-STEP EVALUATION RELATION FOR TERMS IN THE LAMBDA CALCULUS
---------------------------------------------------------------------

-------------------------------------------------------
-- Begin: CO-INDUCTIVE RELATION FOR BIG-STEP EVALUATION

codata CoBigStep : Term [] t -> (y: Term [] t) -> Type where
  CoBStValue    : (v : Value e) -> CoBigStep e e
  --
  CoBStApp      : CoBigStep e1 (TAbs e1') ->
                  CoBigStep e2 e2' ->
                  CoBigStep (subst e2' First e1') e ->
                  CoBigStep (TApp e1 e2) e
  --
  CoBStFix      : CoBigStep e (TAbs e') ->
                  CoBigStep (subst (TFix (TAbs e')) First e') e'' ->
                  CoBigStep (TFix e) e''
  --
  CoBStSucc     : CoBigStep e e' ->
                  CoBigStep (TSucc e) (TSucc e')
  --
  CoBStPredZero : CoBigStep e TZero ->
                  CoBigStep (TPred e) TZero
  --
  CoBStPredSucc : CoBigStep e (TSucc e') ->
                  CoBigStep (TPred e) e'
  --
  CoBStIfzZero  : CoBigStep e1 TZero ->
                  CoBigStep e2 e ->
                  CoBigStep (TIfz e1 e2 _) e
  --
  CoBStIfzSucc  : CoBigStep e1 (TSucc _) ->
                  CoBigStep e3 e ->
                  CoBigStep (TIfz e1 _ e3) e

coBigStepValueIrreducible : CoBigStep e1 e2 -> Value e1 -> e1 = e2
coBigStepValueIrreducible (CoBStValue VZero) VZero      = Refl
coBigStepValueIrreducible (CoBStValue v1)    (VSucc v2) = Refl
coBigStepValueIrreducible (CoBStSucc cbst)   (VSucc v)  =
  cong $ coBigStepValueIrreducible cbst v
coBigStepValueIrreducible (CoBStValue v)     VAbs       = Refl

coBigStepTransitive : CoBigStep e1 e2 -> CoBigStep e2 e3 -> CoBigStep e1 e3
coBigStepTransitive (CoBStValue v) y = y
coBigStepTransitive (CoBStApp x z w) y = CoBStApp x z $ coBigStepTransitive w y
coBigStepTransitive (CoBStFix x z) y = CoBStFix x $ coBigStepTransitive z y
coBigStepTransitive (CoBStSucc x) (CoBStValue v) = CoBStSucc x
coBigStepTransitive (CoBStSucc x) (CoBStSucc y) = CoBStSucc $ coBigStepTransitive x y
coBigStepTransitive (CoBStPredZero x) (CoBStValue v) = CoBStPredZero x
coBigStepTransitive (CoBStPredSucc x) y = let cbst1 = CoBStSucc y
                                          in CoBStPredSucc $ coBigStepTransitive x cbst1
coBigStepTransitive (CoBStIfzZero z w) y = CoBStIfzZero z $ coBigStepTransitive w y
coBigStepTransitive (CoBStIfzSucc w s) y = CoBStIfzSucc w $ coBigStepTransitive s y

bigStepToCoBigStep : BigStep e1 e2 -> CoBigStep e1 e2
bigStepToCoBigStep (BStValue v) = CoBStValue v
bigStepToCoBigStep (BStApp bst1 bst2 bst3) = CoBStApp (bigStepToCoBigStep bst1)
                                                      (bigStepToCoBigStep bst2)
                                                      (bigStepToCoBigStep bst3)
bigStepToCoBigStep (BStFix bst1 bst2) = CoBStFix (bigStepToCoBigStep bst1)
                                                 (bigStepToCoBigStep bst2)
bigStepToCoBigStep (BStSucc bst) = CoBStSucc $ bigStepToCoBigStep bst
bigStepToCoBigStep (BStPredZero bst) = CoBStPredZero $ bigStepToCoBigStep bst
bigStepToCoBigStep (BStPredSucc bst) = CoBStPredSucc $ bigStepToCoBigStep bst
bigStepToCoBigStep (BStIfzZero bst1 bst2) = CoBStIfzZero (bigStepToCoBigStep bst1)
                                                         (bigStepToCoBigStep bst2)
bigStepToCoBigStep (BStIfzSucc bst1 bst2) = CoBStIfzSucc (bigStepToCoBigStep bst1)
                                                         (bigStepToCoBigStep bst2)

-- End: CO-INDUCTIVE RELATION FOR BIG-STEP EVALUATION
-----------------------------------------------------

max_stars_repo_name: normanrink/PCF

max_issues_repo_name: normanrink/PCF

max_forks_repo_name: normanrink/PCF


text:
-- Idea taken from http://liamoc.net/posts/2015-09-10-girards-paradox.html

%default total

data Set : Type where
  MkSet : (x : Type) -> (x -> Set) -> Set

In : Set -> Set -> Type
In a (MkSet _ f) = (x ** a = f x)

D : Set
D = MkSet (s ** Not $ s `In` s) fst

xind : x `In` D -> Not $ x `In` x
xind ((_ ** f) ** Refl) = f

xinx : {x : _} -> Not (x `In` x) -> x `In` D
xinx f = ((_ ** f) ** Refl)

dnotind : Not $ D `In` D
dnotind dind = xind dind dind

falso : Void
falso = dnotind $ xinx dnotind

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
plus_commutes_Z : (m : Nat) -> m = plus m Z
plus_commutes_Z Z = Refl
plus_commutes_Z (S k)
   = let rec = plus_commutes_Z k in
         rewrite sym rec in Refl

plus_commutes_S : (k : Nat) -> (m : Nat) -> S (plus m k) = plus m (S k)
plus_commutes_S k Z = Refl
plus_commutes_S k (S j)
   = rewrite plus_commutes_S k j in Refl

total
plus_commutes : (n : Nat) -> (m : Nat) -> n + m = m + n
plus_commutes Z m = plus_commutes_Z m
plus_commutes (S k) m
    = rewrite plus_commutes k m in
              plus_commutes_S k m


text:
-- ------------------------------------------------------------ [ DeBruijn.idr ]
-- Module    : DeBruijn.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Data structure to compute de Bruijn indices.
|||
||| Thanks to christiansen's Galois tutorials for the accessor and
||| mutator functions for environments/object store.
module Data.DeBruijn

import Data.DList

%default total
%access public export

||| A de Bruijn Index.
|||
||| @T    The type of type's collected.
||| @ctxt The collection of types.
||| @t    The element collected at the current position.
public export
data Index : (T : Type)
          -> (ctxt : List T)
          -> (t : T)
          -> Type where
  ||| The first element in the index.
  First : Index ty (t::ts) t

  ||| The next element in the index.
  Next  : Index ty ts t -> Index ty (t'::ts) t

indexEmpty : DecEq type => Index type [] t -> Void
indexEmpty First impossible
indexEmpty (Next _) impossible

notInIndex : DecEq type
          => (contra : (t = x) -> Void)
          -> (f : Index type xs t -> Void)
          -> Index type (x :: xs) t
          -> Void
notInIndex contra f First = contra Refl
notInIndex contra f (Next x) = f x

isIndex : DecEq type
       => (t : type)
       -> (ctxt : List type)
       -> Dec (Index type ctxt t)
isIndex t [] = No indexEmpty
isIndex t (x :: xs) with (decEq t x)
  isIndex x (x :: xs) | (Yes Refl) = Yes First
  isIndex t (x :: xs) | (No contra) with (isIndex t xs)
    isIndex t (x :: xs) | (No contra) | (Yes prf) = Yes (Next prf)
    isIndex t (x :: xs) | (No contra) | (No f) = No (notInIndex contra f)

||| Sometimes it is bettern to think that we have this thing called an
||| environment and not a `DList`.
|||
||| @t    The Type for Types in our environment.
||| @obj  How we interpret the types in our DSL. Either this is a
|||       dependent type or a function that computes a type.
||| @ctxt The typing context.
public export
Env : (t : Type) -> (obj : t -> Type) -> (ctxt : List t) -> Type
Env ty obj ctxt = DList ty (\x => obj x) ctxt

||| Add an object from our typing environment.
||| @env The typing environment.
export
extend : {t : ty}
      -> (env : Env ty e ctxt)
      -> (obj : e t)
      -> Env ty e (t::ctxt)
extend env obj = obj :: env

||| Read an object from our typing environment.
|||
||| @idx The typing context.
||| @env The typing environment.
export
read : (idx : Index ty ctxt t)
    -> (env : Env ty e ctxt)
    -> e t
read First    (obj::store) = obj
read (Next x) (obj::store) = read x store

||| Add an object to our typnig environment.
|||
||| @idx The typing context.
||| @obj The object to add.
||| @env The environment to which the object is added.
export
update : (idx : Index ty ctxt t )
      -> (obj : e t)
      -> (env : Env ty e ctxt)
      -> Env ty e ctxt
update First    obj (_    :: store) = obj  :: store
update (Next x) obj (obj' :: store) = obj' :: update x obj store

namespace KV

  indexEmpty : DecEq type => (t ** Index (String, type) [] (k, t)) -> Void
  indexEmpty (x ** pf) with (pf)
    indexEmpty (_ ** _) | First impossible
    indexEmpty (_ ** _) | (Next _) impossible

  notInIndex : DecEq type
           => (contra : (k = a) -> Void)
           -> (xs : List (String, type))
           -> (f : (t : type ** Index (String, type) xs (k, t)) -> Void)
           -> (t : type ** Index (String, type) ((a, b) :: xs) (k, t))
           -> Void
  notInIndex contra xs f (x ** pf) with (pf)
    notInIndex contra xs f (b ** pf) | First = contra Refl
    notInIndex contra xs f (x ** pf) | (Next y) = f (_ ** y)

  isIndex : DecEq type
         => (k : String)
         -> (ctxt : List (String, type))
         -> Dec (t ** Index (String, type) ctxt (k,t))
  isIndex k [] = No KV.indexEmpty
  isIndex k ((a, b) :: xs) with (decEq k a)
    isIndex a ((a, b) :: xs) | (Yes Refl) = Yes (b ** First)
    isIndex k ((a, b) :: xs) | (No contra) with (isIndex k xs)
      isIndex k ((a, b) :: xs) | (No contra) | (Yes prf) = Yes (_ ** Next (snd prf))
      isIndex k ((a, b) :: xs) | (No contra) | (No f) = No (KV.notInIndex contra xs f)

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


text:
-- ------------------------------------------------------------ [ DeBruijn.idr ]
-- Module    : DeBruijn.idr
-- Copyright : (c) 2015,2016 See CONTRIBUTORS.md
-- License   : see LICENSE
-- --------------------------------------------------------------------- [ EOH ]
||| Data structure to compute de Bruijn indices.
|||
||| Thanks to christiansen's Galois tutorials for the accessor and
||| mutator functions for environments/object store.
module Toolkit.Data.List.DeBruijn

import public Decidable.Equality

import public Data.List.Elem

import public Toolkit.Data.DList

%default total

-- A reverse cons operator.
infixr 6 +=

namespace List

  ||| Proof that the given list (`xs`) contains the given element
  ||| (`x`).
  |||
  |||
  public export
  Contains : List a -> a -> Type
  Contains xs x = Elem x xs

  ||| Append `x` to the head of `xs`.
  public export
  (+=) : List a -> a -> List a
  (+=) xs x = x :: xs

||| A De Bruijn Index.
|||
||| @T    The type of type's collected.
||| @ctxt The collection of types.
||| @t    The element collected at the current position.
public export
Index : (type : Type)
     -> (ctxt : List type)
     -> (t    : type)
             -> Type
Index _ ctxt t = Elem t ctxt

||| Sometimes it is bettern to think that we have this thing called an
||| environment and not a `DList`.
|||
||| @t    The Type for Types in our environment.
||| @obj  How we interpret the types in our DSL. Either this is a
|||       dependent type or a function that computes a type.
||| @ctxt The typing context.
public export
Env : (t : Type) -> (obj : t -> Type) -> (ctxt : List t) -> Type
Env ty obj ctxt = DList ty obj ctxt

||| Add an object from our typing environment.
||| @env The typing environment.
export
extend : {t : ty}
      -> (env : Env ty e ctxt)
      -> (obj : e t)
      -> Env ty e (t::ctxt)
extend env obj = obj :: env

||| Read an object from our typing environment.
|||
||| @idx The typing context.
||| @env The typing environment.
export
read : (idx : Index ty ctxt t)
    -> (env : Env ty e ctxt)
    -> e t
read Here      (obj::store) = obj
read (There x) (obj::store) = read x store

||| Add an object to our typnig environment.
|||
||| @idx The typing context.
||| @obj The object to add.
||| @env The environment to which the object is added.
export
update : (idx : Index ty ctxt t )
      -> (obj : e t)
      -> (env : Env ty e ctxt)
      -> Env ty e ctxt
update Here      obj (_    :: store) = obj  :: store
update (There x) obj (obj' :: store) = obj' :: update x obj store

namespace KV

  public export
  indexEmpty : {k : String}
            -> (t ** Index (String, type) [] (k, t))
            -> Void
  indexEmpty (MkDPair fst snd) impossible

  public export
  notInIndex : (keyContra : (k = a) -> Void)
           -> (index     : List (String, type))
           -> (kvContra  : (t : type ** Index (String, type)            xs  (k, t)) -> Void)
           -> (prf       : (t : type ** Index (String, type) ((a, b) :: xs) (k, t)))
                        -> Void
  notInIndex keyContra index kvContra (MkDPair b Here) = keyContra Refl
  notInIndex keyContra index kvContra (MkDPair fst (There x)) = kvContra (_ ** x)

  public export
  isIndex : DecEq type
         => (k : String)
         -> (ctxt : List (String, type))
         -> Dec (t : type ** Index (String, type) ctxt (k,t))
  isIndex k [] = No indexEmpty
  isIndex k ((a,b) :: xs) with (decEq k a)
    isIndex a ((a,b) :: xs) | (Yes Refl) = Yes (b ** Here)
    isIndex k ((a,b) :: xs) | (No contra) with (isIndex k xs)
      isIndex k ((a,b) :: xs) | (No contra) | (Yes (MkDPair fst snd))
        = Yes (_ ** There snd)
      isIndex k ((a,b) :: xs) | (No contra) | (No f) = No (notInIndex contra xs f)

namespace Renaming

  public export
  weaken : (func : Contains old type
                -> Contains new type)
        -> (Contains (old += type') type
         -> Contains (new += type') type)

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

  public export
  interface Rename (type : Type) (term : List type -> type -> Type) | term where
    rename : {old, new : List type}
          -> (f : {ty : type} -> Contains old ty
                              -> Contains new ty)
          -> ({ty : type} -> term old ty
                          -> term new ty)

    var : {ty   : type}
       -> {ctxt : List type}
               -> Elem ty ctxt
               -> term ctxt ty

    weakens : {old, new : List type}
           -> (f : {ty  : type}
                       -> Contains old ty
                       -> term     new ty)
           -> ({ty,type' : type}
                  -> Contains (old += type') ty
                  -> term     (new += type') ty)
    weakens f Here = var Here
    weakens f (There rest) = rename There (f rest)

namespace Substitution

  namespace General
    public export
    interface Rename type term
           => Substitute (type : Type) (term : List type -> type -> Type) | term where

      subst : {old, new : List type}
           -> (f : {ty  : type}
                       -> Contains old ty
                       -> term     new ty)
           -> ({ty : type}
                  -> term old ty
                  -> term new ty)

  namespace Single

    apply : {type : Type}
         -> {term : List type -> type -> Type}
         -> Rename type term
         => {ctxt   : List type}
         -> {typeA  : type}
         -> {typeB  : type}
         -> (this   : term      ctxt    typeB)
         -> (idx    : Contains (ctxt += typeB) typeA)
                   -> term      ctxt           typeA
    apply this Here = this
    apply this (There rest) = var rest

    export
    subst : {type : Type}
         -> {term : List type -> type -> Type}
         -> Rename type term
         => Substitute type term
         => {ctxt          : List type}
         -> {typeA         : type}
         -> {typeB         : type}
         -> (this          : term  ctxt           typeB)
         -> (inThis        : term (ctxt += typeB) typeA)
                          -> term  ctxt           typeA
    subst {ctxt} {typeA} {typeB} this inThis
      = subst (apply this) inThis

  namespace Double

    public export
    apply : {type : Type}
         -> {term : List type -> type -> Type}
         -> Rename type term
         => {ctxt          : List type}
         -> {typeA, typeB, typeC : type}
         -> (this    : term       ctxt                     typeA)
         -> (andThis : term       ctxt                     typeB)
         -> (idx     : Contains ((ctxt += typeA) += typeB) typeC)
                    -> term       ctxt                     typeC
    apply this andThis Here              = andThis
    apply this andThis (There Here)      = this
    apply this andThis (There (There x)) = var x

    public export
    subst : {type : Type}
         -> {term : List type -> type -> Type}
         -> Rename type term
         => Substitute type term
         => {ctxt          : List type}
         -> {typeA, typeB, typeC : type}
         -> (this    : term  ctxt                     typeA)
         -> (andThis : term  ctxt                     typeB)
         -> (inThis  : term ((ctxt += typeA) += typeB) typeC)
                    -> term   ctxt                     typeC
    subst {ctxt} {typeA} {typeB} {typeC} this andThis inThis
      = General.subst (apply this andThis) inThis

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

max_stars_repo_name: gallais/linear-circuits

max_issues_repo_name: gallais/linear-circuits

max_forks_repo_name: gallais/linear-circuits


text:
module Language.LSP.Message.Diagnostics

import Language.JSON
import Language.LSP.Message.Derive
import Language.LSP.Message.Location
import Language.LSP.Message.URI
import Language.LSP.Message.Utils
import Language.Reflection

%language ElabReflection
%default total

namespace DiagnosticTag
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic
  public export
  data DiagnosticTag = Unnecessary | Deprecated

export
ToJSON DiagnosticTag where
  toJSON Unnecessary = JNumber 1
  toJSON Deprecated  = JNumber 2

export
FromJSON DiagnosticTag where
  fromJSON (JNumber 1) = pure Unnecessary
  fromJSON (JNumber 2) = pure Deprecated
  fromJSON _ = neutral

namespace DiagnosticSeverity
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic
  public export
  data DiagnosticSeverity = Error | Warning | Information | Hint

export
ToJSON DiagnosticSeverity where
  toJSON Error       = JNumber 1
  toJSON Warning     = JNumber 2
  toJSON Information = JNumber 3
  toJSON Hint        = JNumber 4

export
FromJSON DiagnosticSeverity where
  fromJSON (JNumber 1) = pure Error
  fromJSON (JNumber 2) = pure Warning
  fromJSON (JNumber 3) = pure Information
  fromJSON (JNumber 4) = pure Hint
  fromJSON _ = neutral

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic
public export
record DiagnosticRelatedInformation where
  constructor MkDiagnosticRelatedInformation
  location : Location
  message  : String
%runElab deriveJSON defaultOpts `{{DiagnosticRelatedInformation}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic
public export
record CodeDescription where
  constructor MkCodeDescription
  href : URI
%runElab deriveJSON defaultOpts `{{CodeDescription}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#diagnostic
public export
record Diagnostic where
  constructor MkDiagnostic
  range              : Range
  severity           : Maybe DiagnosticSeverity
  code               : Maybe (OneOf [Int, String])
  codeDescription    : Maybe CodeDescription
  source             : Maybe String
  message            : String
  tags               : Maybe (List DiagnosticTag)
  relatedInformation : Maybe (List DiagnosticRelatedInformation)
  data_              : Maybe JSON
%runElab deriveJSON (record {renames = [("data_", "data")]} defaultOpts) `{{Diagnostic}}

namespace PublishDiagnosticsClientCapabilities
  ||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics
  public export
  record TagSupport where
    constructor MkTagSupport
    valueSet : List DiagnosticTag
  %runElab deriveJSON defaultOpts `{{TagSupport}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics
public export
record PublishDiagnosticsClientCapabilities where
  constructor MkPublishDiagnosticsClientCapabilities
  relatedInformation     : Maybe Bool
  tagSupport             : Maybe TagSupport
  versionSupport         : Maybe Bool
  codeDescriptionSupport : Maybe Bool
  dataSupport            : Maybe Bool
%runElab deriveJSON defaultOpts `{{PublishDiagnosticsClientCapabilities}}

||| Refer to https://microsoft.github.io/language-server-protocol/specification.html#textDocument_publishDiagnostics
public export
record PublishDiagnosticsParams where
  constructor MkPublishDiagnosticsParams
  uri         : DocumentURI
  version     : Maybe Int
  diagnostics : List Diagnostic
%runElab deriveJSON defaultOpts `{{PublishDiagnosticsParams}}


text:
import Data.List

-- %default total

total
foo : Maybe a -> a
foo (Just x) = x

total
bar : %World -> ()
bar %MkWorld = ()

total
qsortBad : Ord a => List a -> List a
qsortBad [] = []
qsortBad (x :: xs)
   = qsortBad (filter (< x) xs) ++ x :: qsortBad (filter (> x) xs)

total
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
   = qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
         x :: qsort (assert_smaller (x :: xs) (filter (> x) xs))

partial
main : IO ()
main = do let x = foo Nothing
          printLn (the Int x)


text:
module Crop

public export
record Crop where
  constructor CreateCrop
  x : Double
  y : Double
  x2 : Double
  y2 : Double

max_stars_repo_name: GrandArchTemplar/IdrisVKAPI

max_issues_repo_name: GrandArchTemplar/IdrisVKAPI

max_forks_repo_name: GrandArchTemplar/IdrisVKAPI


text:
invReshape :
    Vector ((x1 * m)::x2::xs) t ->
    Vector (x1::(m * x2)::xs) t

invReshape v {x1 = Z} = []
invReshape v {x1 =S r} =
    map redDim $ incDim v

max_stars_repo_name: RossMeikleham/MSci-Project

max_issues_repo_name: RossMeikleham/MSci-Project

max_forks_repo_name: RossMeikleham/MSci-Project


text:
module Verified.Functor

%default total

class Functor f => VerifiedFunctor (f : Type -> Type) where
  functorIdentity : {a : Type} -> (x : f a) -> map id x = id x
  functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
                   (g1 : a -> b) -> (g2 : b -> c) ->
                   map (g2 . g1) x = (map g2 . map g1) x

max_stars_repo_name: yurrriq/idris-verified

max_issues_repo_name: yurrriq/idris-verified

max_forks_repo_name: yurrriq/idris-verified


text:
module Language.LSP.CodeAction.GenerateDef

import Core.Context
import Core.Core
import Core.Env
import Core.Metadata
import Core.UnifyState
import Data.List
import Data.List1
import Data.String
import Idris.IDEMode.CaseSplit
import Idris.Pretty
import Idris.REPL
import Idris.REPL.Opts
import Idris.Syntax
import Idris.Syntax
import Language.JSON
import Language.LSP.CodeAction
import Language.LSP.Message
import Libraries.Data.List.Extra
import Libraries.Data.PosMap
import Libraries.Text.PrettyPrint.Prettyprinter
import Server.Configuration
import Server.Response
import Server.Utils
import System.File
import Server.Log
import System.Clock
import TTImp.Interactive.GenerateDef
import TTImp.TTImp
import TTImp.Interactive.ExprSearch
import Parser.Unlit

-- forked from Language.LSP.CodeAction.ExprSearch
fueledTimedRepeat : Ref LSPConf LSPConfiguration
                 => Nat -> Clock Monotonic -> Clock Duration -> List a -> (Nat -> Core (Maybe a)) -> Core (List a)
fueledTimedRepeat Z _ _ acc _ = pure (reverse acc)
fueledTimedRepeat (S k) start timeout acc f = do
  Just res <- f k
    | Nothing => pure (reverse acc)
  time <- coreLift $ clockTime Monotonic
  let diff = timeDifference time start
  if diff < timeout
     then fueledTimedRepeat k start timeout (res :: acc) f
     else do logString Info "GeneratedDef timed out"
             pure (reverse acc)

number : Nat -> List a -> List (Nat, a)
number n [] = []
number n (x :: xs) = (n,x) :: number (S n) xs

pred : Nat -> Nat
pred Z     = Z
pred (S k) = k

-- This is needed as PosMap is not smart enough yet to track down
-- the non applied functions in the PosMap. This requires a change
-- in the compiler, for that reason the generateDef functionality
-- needs to have a backup strategy for names. If the PosMap
-- creation of the compiler changes probably this functions
-- will be rendered as reduntant one.
guessName : Ref MD Metadata
         => (Int, Int) -> Core (Maybe Name)
guessName (line, col) = do
  meta <- get MD
  let Nothing = findPointInTree (line, col) (nameLocMap meta)
      | Just name => pure (Just name)
  Nothing <- findTypeAt $ anyAt $ within (line, col)
      | Just (name, _, _) => pure (Just name)
  pure Nothing

export
generateDef : Ref LSPConf LSPConfiguration
            => Ref MD Metadata
            => Ref Ctxt Defs
            => Ref UST UState
            => Ref Syn SyntaxInfo
            => Ref ROpts REPLOpts
            => OneOf [Int, String, Null] -> CodeActionParams -> Core (List CodeAction)
generateDef msgId params = do
  defs <- branch
  let True = params.range.start.line == params.range.end.line
      | _ => do
        logString Debug "generateDef: start and end lines were different."
        pure []

  [] <- searchCache params.range GenerateDef
    | actions => do logString Debug "generateDef: found cached action"
                    pure actions

  let line = params.range.start.line
  let col = params.range.start.character
  Just name <- guessName (line, col)
    | Nothing => do
        logString Debug "generateDef: couldn't find name at: \{show (line, col)}"
        pure []

  timeout <- gets LSPConf longActionTimeout
  start <- coreLift $ clockTime Monotonic

  Edited (DisplayEdit block)
    <- Idris.REPL.process
        (Editing (GenerateDef False (fromInteger (cast (line + 1))) name 0)) -- off-by-one
    | Edited (EditError err) => do
        logString Debug "generateDef: had an EditError \{show err}"
        pure []
    | other => do
        logString Debug "generateDef: return unexpected REPL result."
        pure []

  time <- coreLift $ clockTime Monotonic
  let diff = timeDifference time start
  blocks <- case diff < timeout of
    False => do logString Info "GeneratedDef timed out"
                pure []
    True => do
      fuel <- gets LSPConf searchLimit
      fueledTimedRepeat (pred fuel) start timeout [] $ \k => do
        Edited (DisplayEdit block) <- Idris.REPL.process (Editing GenerateDefNext)
          | Edited (EditError err) => do
              logString Debug "generateDef next: had an EditError in \{show k}: \{show err}"
              pure Nothing
          | other => do
              logString Debug "generateDef next: returned unexpected REPL result in \{show k}"
              pure Nothing
        pure (Just block)

  put Ctxt defs

  let docURI = params.textDocument.uri
  let rng = MkRange (MkPosition (line + 1) 0) (MkPosition (line + 1) 0) -- insert

  actions <- for (number 1 (block :: blocks)) $ \(i,b) => do
    let funcDef = show b
    let lastLine = last (String.lines funcDef)
    let edit = MkTextEdit rng (funcDef ++ "\n") -- extra newline
    let workspaceEdit = MkWorkspaceEdit
          { changes           = Just (singleton docURI [edit])
          , documentChanges   = Nothing
          , changeAnnotations = Nothing
          }
    pure $ MkCodeAction
      { title = "Generate definition #\{show i} as ~ \{strSubstr 0 50 lastLine} ..."
      , kind        = Just $ Other "generate-def"
      , diagnostics = Just []
      , isPreferred = Just False
      , disabled    = Nothing
      , edit        = Just workspaceEdit
      , command     = Nothing
      , data_       = Nothing
      }
  -- TODO: retrieve the line length efficiently
  modify LSPConf (record { cachedActions $= insert (MkRange (MkPosition line 0) (MkPosition line 1000), GenerateDef, actions) })
  pure actions


text:
||| Position and geometry of Hexagonal grid system
||| https://www.redblobgames.com/grids/hexagons/
module Bautzen.Pos

import Data.Fin
import Data.Nat
import Data.Nat.DivMod
import Data.Nat.Parity
import Decidable.Equality
import Data.List

import public Data.ZZ
import public Data.ZZ.Extra

%default total

-- Positions & Map

||| A position/hex of the game board encoded as a pair of `Fin`s.
||| The type is indexed by the bounds on the number of rows and cols
||| which are basically dependent on the size of the terrain.
public export
data Loc : (c : Nat) -> (r : Nat) -> Type where
  Hex : (col : Fin c) -> (row : Fin r) -> Loc c r

colInjective : Hex c r = Hex col r' -> c = col
colInjective Refl = Refl

rowInjective : Hex c r = Hex c' row -> r = row
rowInjective Refl = Refl

public export
Eq (Loc c r) where
  (==) (Hex col row) (Hex col' row') = col == col' && row == row'

public export
DecEq (Loc c r) where
  decEq (Hex col row) (Hex k j ) with (decEq col k)
    decEq (Hex col row) (Hex k j ) | No contra = No $ \ h => contra (colInjective h)
    decEq (Hex col row) (Hex k j ) | Yes p with (decEq row j)
      decEq (Hex col row) (Hex k j ) | Yes p | No contra = No $ \ h => contra (rowInjective h)
      decEq (Hex col row) (Hex col row) | Yes Refl | Yes Refl = Yes Refl

public export
Show (Loc c r) where
  show (Hex c r) = "Hex " ++ show2Digits (finToNat c) ++ " " ++ show2Digits (finToNat r)
    where
      show2Digits : Nat -> String
      show2Digits n =
        if n <= 9
        then "0" ++ show n
        else show n

public export
Ord (Loc c r) where
  compare (Hex col row) (Hex col' row') =
    case compare col col' of
      LT => LT
      EQ => compare row row'
      GT => GT

||| Cube coordinates.
||| Cube coordinates stem from the observation a 2-D hexagonal grid is equivalent
||| to a diagonal "slice" of a 3-D cubic grid. Using cubic coordinates makes it
||| much easier to compute geometric values.
||| We only store the `x` (column) and `z` (depth) coordinates instead
||| of a triple as the `y` dimension can be simply recovered as `-x -z`.
public export
data Cube : Type where
  MkCube : (x : ZZ) -> (z : ZZ) -> Cube

||| Compute the L1 distance between 2 `Cube`s
||| see [Red Blob Games](https://www.redblobgames.com/grids/hexagons/#distances-cube) page
||| for details on the (pretty cool) algorithm.
public export
cubeDistance : Cube -> Cube -> Nat
cubeDistance (MkCube x z) (MkCube x' z') =
  let y  = negate x - z
      y' = negate x' - z'
  in max (max (absZ (x - x')) (absZ (y - y'))) (absZ (z - z'))

public export
posToCube : Loc c r -> Cube
posToCube (Hex col row) =
  let x = Pos (finToNat col)
      sign : ZZ
      sign = if odd (finToNat col) then 1 else 0
      z : ZZ
      z = Pos (finToNat row) - divZZNZ (x - sign) 2 {z = PosSIsNotZ }
  in MkCube x z

mutual
  public export
  data Distance : Type where
    IsDistance : (d : Nat) -> Distance

  export
  Num Distance where
    fromInteger = IsDistance . fromInteger
    IsDistance d1 * IsDistance d2 = IsDistance $ d1 * d2 -- meaningless
    IsDistance d1 + IsDistance d2 = IsDistance $ d1 + d2

  public export
  distance : {c : Nat} -> {r : Nat} -> Loc c r -> Loc c r -> Distance
  distance x y = IsDistance (cubeDistance (posToCube x) (posToCube y))

public export
data Mvmt : Type where
  Dec : Mvmt
  Neut : Mvmt
  Inc : Mvmt

public export
succNotLTEZ : Not (LTE (S m) Z)
succNotLTEZ LTEZero impossible

public export
fromLTESucc : LTE (S m) (S n) -> LTE m n
fromLTESucc (LTESucc x) = x

public export
lteSuccR : LTE n m -> LTE n (S m)
lteSuccR LTEZero     = LTEZero
lteSuccR (LTESucc x) = LTESucc (lteSuccR x)

public export
lteSuccL : LTE (S n) m -> LTE n m
lteSuccL (LTESucc x) = lteSuccR x

public export
isLte : (m, n : Nat) -> Dec (LTE m n)
isLte Z n = Yes LTEZero
isLte (S k) Z = No succNotLTEZ
isLte (S k) (S j)
    = case isLte k j of
           No contra => No (contra . fromLTESucc)
           Yes prf => Yes (LTESucc prf)

public export
shiftLoc : {bound : Nat} -> (x : Nat) -> Mvmt -> Maybe (Fin bound)
shiftLoc Z Dec = Nothing
shiftLoc (S k) Dec = natToFin k bound
shiftLoc x Neut = natToFin x bound
shiftLoc x Inc {bound} = natToFin (S x) bound

public export
makeLoc : {c : Nat} -> {r : Nat} -> (x : Nat) -> (y : Nat) -> (Mvmt, Mvmt) -> Maybe (Loc c r)
makeLoc col row (a, b) = do
  c' <- shiftLoc col a
  r' <- shiftLoc row b
  pure $ Hex c' r'

public export
oddShifts : List (Mvmt, Mvmt)
oddShifts = [ (Dec, Neut)
            , (Neut, Dec)
            , (Inc, Neut)
            , (Inc, Inc)
            , (Neut, Inc)
            , (Dec, Inc)
            ]

public export
evenShifts : List (Mvmt, Mvmt)
evenShifts = [ (Dec, Dec)
            , (Neut, Dec)
            , (Inc, Dec)
            , (Inc, Neut)
            , (Neut, Inc)
            , (Dec, Neut)
            ]

neighbours' : {col : Nat} -> {row : Nat} -> (x : Nat) -> (y : Nat) -> List (Loc col row)
neighbours' x y with (x `divMod` (S Z))
  neighbours' x@(Z + (q * 2)) y     | (MkDivMod q Z _) = catMaybes $ map (makeLoc x y) evenShifts
  neighbours' x@((S r) + (q * 2)) y | (MkDivMod q (S r) _) = catMaybes $ map (makeLoc x y) oddShifts
  neighbours' (S (S r) + (q * 2)) _ | (MkDivMod q (S (S r)) LTEZero) impossible

||| Compute the neighbours of a given position
||| There are at most 6 neighbours, with side and corner hexes having of
||| course less.
public export
neighbours : {c : Nat} -> {r : Nat} -> (pos : Loc c r) -> List (Loc c r)
neighbours (Hex col row) = neighbours' (finToNat col) (finToNat row)

namespace LocTest

  neighbours1_test : (neighbours {c=22} {r=12} (Hex 3 3) = [ Hex 2 3, Hex 3 2, Hex 4 3, Hex 4 4, Hex 3 4, Hex 2 4] )
  neighbours1_test = Refl

  neighbours_test : (neighbours {c=22} {r=12} (Hex 2 2) = [ Hex 1 1, Hex 2 1, Hex 3 1, Hex 3 2, Hex 2 3, Hex 1 2] )
  neighbours_test = Refl

  distance_to_odd_neighbours_is_1 : map (distance (Hex 3 2)) (neighbours {c=22} {r=12} (Hex 3 2)) = [ 1, 1, 1, 1, 1, 1 ]
  distance_to_odd_neighbours_is_1 = Refl

  distance_to_even_neighbours_is_1 : map (distance (Hex 2 2)) (neighbours {c=22} {r=12} (Hex 2 2)) = [ 1, 1, 1, 1, 1, 1 ]
  distance_to_even_neighbours_is_1 = Refl

  distance_test : distance {c=22} {r=12} (Hex 3 2) (Hex 4 4) = 2
  distance_test = Refl

max_stars_repo_name: abailly/hsgames

max_issues_repo_name: abailly/acquire

max_forks_repo_name: abailly/acquire


text:
module Main
import Data.Bits

boolToInt : Bool -> Int
boolToInt True = 1
boolToInt False = 0

main : IO ()
main = do
  putStrLn . show $ (the Bits8 200) + (the Bits8 100)
  putStrLn . show $ (the Bits8 200) - (the Bits8 100)
  putStrLn . show $ (the Bits8 200) * (the Bits8 100)
  putStrLn . show $ (the Bits8 200) `div` (the Bits8 7)
  putStrLn . show $ (the Bits8 200) `mod` (the Bits8 7)
  putStrLn . show $ -(the Bits8 100)
  putStrLn . show $ the Bits8 200 .&. the Bits8 100
  putStrLn . show $ the Bits8 200 .|. the Bits8 100
  putStrLn . show $ the Bits8 200 `xor` the Bits8 100
  putStrLn . show . boolToInt $ the Bits8 200 < the Bits8 100
  putStrLn . show . boolToInt $ the Bits8 200 <= the Bits8 100
  putStrLn . show . boolToInt $ the Bits8 200 == the Bits8 100
  putStrLn . show . boolToInt $ the Bits8 200 >= the Bits8 100
  putStrLn . show . boolToInt $ the Bits8 200 > the Bits8 100
  -- putStrLn . show  $ the Bits8 100 `shiftL` 1
  -- putStrLn . show  $ the Bits8 100 `shiftR` 1

max_stars_repo_name: skyro-compiler/skyro

max_issues_repo_name: skyro-compiler/skyro

max_forks_repo_name: skyro-compiler/skyro