amosr

(*
Simple, faster parser for value/const subset of Isabelle terms.

The Isabelle parser does some fancy mixfix stuff, but as a result it's quite complicated.
For some tasks, such as parsing a deep embedding of a moderate-sized program, using the full
parser can be overkill. Then, after we've parsed the term, we need to do full type inference.
These two together can be incredibly slow – a list with a thousand elements can take 7 seconds to
parse and type check.

In cases where we know ahead of time that our definition will only contain a subset of syntactic

amosr

theory AssocTree
imports Main
begin

(* Binary lookup in a sorted list *)
(* this seems silly because the list operations are linear, but if we can specialise this definition
  for a particular statically-known list then we'd end up with an efficient implementation *)
fun lookup_tree :: "(('a :: linorder) × 'b) list ⇒ 'b ⇒ 'a ⇒ 'b" where
    "lookup_tree [] def _ = def"
  | "lookup_tree [(k',v)] def k = (if k = k' then v else def)"

amosr

(* A very simple Coq encoding of the "Towers of Hanoi" puzzle game. *)

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Arith.Compare_dec.


(* Proof of a sorted list *)
Inductive Sorted : list nat -> Prop :=
 | sorted'nil : Sorted []

amosr

# random drum machine

# an array of times for when samples should play
# we'll have a corresponding array for which
# sample to sound at a particular time
def times_beat(i)
  # beats, quarter beats, and triplets
  times_one = [0, 1.0/4, 1.0/3, 1.0/2.0, 2.0/3, 3.0/4]
  times_one.map {|j| j + i}
end

amosr

Set Implicit Arguments.


Inductive Place
 := Kitchen | Bedroom | Hallway | Outside.

Inductive Card := NORTH | EAST | SOUTH | WEST.

Definition moveTo (p : Place) (c : Card) : option Place :=
 match p, c with

amosr

-- Which is faster?
-- Only difference is order of branches in 'if'.

sourceOfVector :: (Monad m, Generic.Vector v a) => v a -> Source m a
sourceOfVector !as0
 = Source 
 { init = return 0
 , pull = \ix -> if ix >= Generic.length as0
                 then return (Nothing, ix)
                 else return (Just $ Generic.unsafeIndex as0 ix, ix + 1)

amosr

(*
This one has no staging.
The idea is a simple schema and values, but it's (probably) terribly slow.
*)

(* Schema and value definitions *)
type schema
  = SInt
  | SArray of schema

amosr

(* Schema and value definitions *)
type schema
  = SInt
  | SBool
  | SArray of schema

type value
  = VInt of int
  | VBool of bool
  | VArray of value list

amosr

#!/usr/bin/perl

my $last_file, $last_file_used = 1;

while (<>) {
  my $current = $_;
  my $cat = $current;
  while (length $current == 80 &&
        !($current =~ m/\.\.\.$/)) {
    $current = <>;

amosr

! Undefined control sequence.
<recently read> \wedg
figures/FusionDef:60
   \> \> $\wedg
                  $ \> $b~\in~\ti{tryStepPair}~\ti{cs}~ @blocks@~p~l_p ~l_p~...
!  ==> Fatal error occurred, no output PDF file produced!