ghulette

-- Product category instance

import Prelude hiding ((.),id)
import Control.Category

data Product c d x y = Product (c x y) (d x y)
  deriving (Eq,Show)

instance (Category c,Category d) => Category (Product c d) where
  id = Product id id

ghulette

mapAll :: (a -> Maybe a) -> [a] -> Maybe [a]
mapAll _ [] = Just []
mapAll f (x:xs) = case f x of
  Just x' -> case mapAll f xs of
    Just xs' -> Just (x':xs')
    Nothing -> Nothing
  Nothing -> Nothing

mapOne :: (a -> Maybe a) -> [a] -> Maybe [a]
mapOne _ [] = Nothing

ghulette

escapes1 :: RealFloat a => Int -> Complex a -> Bool
escapes1 i c = any ((>) 2 . magnitude) (take i ps)
   where ps = iterate p (0 :+ 0)
         p = \z -> c + z^(2 :: Int)

escapes2 :: RealFloat a => Int -> Complex a -> Bool
escapes2 i c = escapes2' i c (0 :+ 0)

escapes2' :: RealFloat a => Int -> Complex a -> Complex a -> Bool
escapes2' 0 _ _ = False

ghulette

module Strategy where

type Strategy m a = a -> m (Maybe a)

success :: Monad m => Strategy m a
success = return . Just

failure :: Monad m => Strategy m a
failure _ = return Nothing

ghulette

Require Import Le.

(* We shouldn't really need the return clause here, but Coq 8.4pl2
will crash without it... *)

Definition test (i : nat) (x : {n : nat | n <= i}) : nat :=
  match x with
  | exist O _ => 0
  | exist (S x') p => 
    match i (* return (S x' <= i) -> nat *) with

ghulette

type value = int
type ptr = value ref
type st = unit

type 'a imp =
  | New of value * (ptr -> 'a imp)
  | Read of ptr * (value -> 'a imp)
  | Write of ptr * value * 'a imp
  | While of (st -> bool) * unit imp * 'a imp
  | Return of 'a

ghulette

(*******************************************************************************

   Getting a backtrace out of ocaml is not completely obvious. You
   have to compile the code with -g and then run with OCAMLRUNPARAM=b,
   like this:

   $ ocamlc -g -o test test.ml
   $ OCAMLRUNPARAM=b ./test
   backtrace_status: true
   Failure("nth")

ghulette

open Printf
(* Labeled arguments, the easy way *)

let _ =
  (* Declare a function with labeled arguments like this: *)
  let f ~x ~y = x + y in
  (* Type: f : x:int -> y:int -> int *)
  (* Call it like this: *)
  printf "%d\n" (f ~x:5 ~y:6);

ghulette

Require Import Coq.Logic.Classical.

Theorem conj_iff :
  forall P Q, P /\ Q <-> ~(P -> ~Q).
Proof.
  split.
  unfold not.
  intros (HP,HQ) H.
  apply H.
  apply HP.

ghulette

type formula =
  | False
  | True
  | Atom of string
  | Not of formula
  | And of formula * formula
  | Or of formula * formula

let is_lit = function
  | Atom _ | Not (Atom _) -> true