david-christiansen

module ClassNonsense

import Language.Reflection.Elab

class Foo a where
  foo : a -> () -> a

class Foo a => Bar a where
  constructor MkFoo
  bar : a -> Int

david-christiansen

module Main

import Data.So
import Debug.Trace

%include C "bytes.h"
%link C "bytes.o"

%access public

david-christiansen

mutual
  class Foo a where
    foo : a -> Type
    bar : (x : a) -> foo @{nonsense} x -> Int

  instance Foo a where
    foo x = Nat
    bar x n = 354

  instance [nonsense] Foo a where

david-christiansen

18:38:27 -> ((:docs-for "Nat")
 94)
18:38:27 <- (:return
 (:ok "Data type Nat : Type\n    Unary natural numbers\n    \nConstructors:\n    Z : Nat\n        Zero\n        \n    S : Nat -> Nat\n        Successor\n        "
      ((10 3
           ((:name "Prelude.Nat.Nat")
            (:implicit :False)
            (:decor :type)
            (:doc-overview "Unary natural numbers")
            (:type "Type")

david-christiansen

module Finite

import Data.Fin
import Language.Reflection.Elab
import Language.Reflection.Utils

%default total

||| A bijection between some type and bounded numbers
data Finite : Type -> Nat -> Type where

david-christiansen

module Snoc

data SnocList : List a -> Type where
  SnocNil : SnocList []
  Snoc : (xs : List a) -> (x : a) -> SnocList (xs ++ [x])

snocList : (xs : List a) -> SnocList xs
snocList [] = SnocNil
snocList (x :: xs) with (snocList xs)
  snocList (x :: []) | SnocNil = Snoc [] x

david-christiansen

;;; Helm support for finding my stuff
(defvar helm-david-christiansen-git-repo-list nil
  "The Git repos found for my Helm launcher.")
(defvar helm-david-christiansen-git-repo-finder-process nil
  "The process finding Git repos for my Helm launcher.")
(defun helm-david-christiansen-git-repo-finder-output-filter (proc string)
  (when (buffer-live-p (process-buffer proc))
    (with-current-buffer (process-buffer proc)
      (let ((moving (= (point) (process-mark proc))))
        (save-excursion

david-christiansen

(defun helm-ghc-errors-in-buffer ()
  (with-current-buffer helm-current-buffer
    (remove-if-not #'(lambda (o) (overlay-get o 'ghc-check))
                   (overlays-in (point-min) (point-max)))))

(defun helm-ghc-describe-overlay (o)
  (cl-flet ((abbreviate (str)
                        (if (> (length str) fill-column)
                            (concat (substring str 0 (- fill-column 3)) "...")

david-christiansen

module FizzBuzz

-- Dependently-typed FizzBuzz, about 5 years late to the party.

-- A specification of the problem.  Each constructor tells the conditions
-- under which it can be applied, and the "auto" keyword means that proof
-- search will be used in the context where they are applied to fill them
-- out. For instance, applying `N` to some Nat fails unless there's a proof in
-- scope that the argument meets the criteria.
data FB : Nat -> Type where

david-christiansen

drc@drc:~/tmp$ idris Quasiquote.idr
     ____    __     _                                          
    /  _/___/ /____(_)____                                     
    / // __  / ___/ / ___/     Version 0.9.13.1-git:f8ec244
  _/ // /_/ / /  / (__  )      http://www.idris-lang.org/      
 /___/\__,_/_/  /_/____/       Type :? for help               

Idris is free software with ABSOLUTELY NO WARRANTY.            
For details type :warranty.
Type checking ./Quasiquote.idr