gabriel-fallen

{-@ LIQUID "--exact-data-cons" @-}
{-@ LIQUID "--higherorder" @-}

module TreeSort where

import Prelude hiding ((.), concat, filter, foldr, map)
import Language.Haskell.Liquid.ProofCombinators


data List a = Nil | Cons a (List a)

gabriel-fallen

theory Compiler_Demo
  imports Main
begin

type_synonym 'a binop = "'a ⇒ 'a ⇒ 'a"

datatype ('a, 'v) expr
  = Const 'v
  | Var 'a
  | BinOp "'v binop" "('a, 'v) expr" "('a, 'v) expr"

gabriel-fallen

theory Demo
imports Predicate_Compile Extraction
begin

datatype 'a list = Nil
  | Cons (head: 'a) (tail: "'a list")
  for map: lmap

primrec append :: "'a list ⇒ 'a list ⇒ 'a list" where
  "append Nil ys = ys"

gabriel-fallen

gabriel-fallen

#lang racket/gui

;;; Files part

(define (image-files-list dir)
  (filter (lambda (p) (let ([ext (bytes->string/utf-8 (path-get-extension p))])
                        (or (string-ci=? ext ".jpg") (string-ci=? ext ".jpeg") (string-ci=? ext ".png"))))
          (directory-list dir #:build? #t)))

(define images-top    (map read-bitmap (image-files-list "top")))

gabriel-fallen

module SampleTheorems

%default total

reverse' : List a -> List a
reverse' [] = []
reverse' (x :: xs) = reverse' xs ++ [x]

append_nil : xs ++ [] = xs
append_nil {xs = []} = Refl

gabriel-fallen

theory GCD
imports Main
begin

fun gcd :: "nat ⇒ nat ⇒ nat" where
"gcd m 0 = m" |
"gcd m n = gcd n (m mod n)"


theorem gcd_dvd_both: "(gcd m n dvd m) ∧ (gcd m n dvd n)"

gabriel-fallen

(declare-sort Type)
(declare-sort Term)
(declare-fun HasType (Term Type) Bool)

(declare-fun string () Type) ; type of strings of a programming language
(declare-fun nat () Type)    ; type of natural numbers of a programming language
(declare-fun list () Type)   ; type of lists should be parametrized by type of elements but we ignore it for simplicity

(declare-fun BoxString (String) Term)

gabriel-fallen

Статьи против Программ

На днях заметил, что читать статьи (по computer science) гораздо сложнее, чем читать/писать программы. Кажется парадоксальным, но вполне объяснимо — всё дело в пресловутом управлении сложностью.

Как известно, объём "кэша" у человека сильно ограничен — одновременно можно думать всего о 5-9 вещах. Может быть, некоторые могут думать об 11 вещах одновременно, но едва ли больше. Если учесть, что как правило нужно помнить не только отдельные объекты, но и связи между ними, то получится удержать в сознании всего 3 (+ 3 связи = 6) или 4 (+ 6 связей = 10) сущности.

gabriel-fallen

# in ~/.fluxbox/keys
# change KB layout
# Mod4 k e # English
Mod4 45 26 :Exec setxkbmap us
# Mod4 k r # Russian
Mod4 45 27 :Exec setxkbmap ru