packages feed

gulcii 0.2.0.3 → 0.3

raw patch · 29 files changed

+1514/−423 lines, 29 filesdep ~filepathdep ~gtkbinary-added

Dependency ranges changed: filepath, gtk

Files

+ README.md view
@@ -0,0 +1,104 @@+GULCII+======++GULCII is an untyped lambda calculus interpreter supporting interactive+modification of a running program with graphical display of graph reduction.+++Syntax+------++Lambda calculus terms with some sugar coating:+  +    term ::= variable                    -- free or bound+         | '\' var+ strategy term        -- lambda abstraction+         | term+                         -- application+         | '(' term ')'+         | integer+         | list+    variable ::= [a-z][A-Za-z0-9]*+    strategy = '.' | '!' | '?'           -- lazy | strict | copy+    integer ::= [0-9]+                   -- uses Scott-encoding+    list ::= '[' (term (, T)*)? ']'      -- uses Scott-encoding++There are three variants of lambda abstraction: lazy, strict, and copy:++    \x . f x x    -- x is evaluated lazily with sharing+    \x ! f x x    -- x is evaluated strictly and shared+    \x ? f x x    -- x is copied before any evaluation++There is additional syntax sugar for natural numbers and lists, using+<http://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding#Scott_encoding>:++    [0,1,2,3]++There is a small standard library based loosely around the Haskell Prelude:++    :load prelude+    :browse++If you define a term using free variables, they can be modified while+the program is running, but sharing is lost.  If you define a term as+a fixed point (perhaps with Y-combinator) then sharing works (to some+extent), but you can't modify the code while it is running any more.+++Meta Commands+-------------++To exit type:++    :quit++Entering a term evaluates it.++Terms can be bound to names, stored in a global dictionary:++    foo = bar++The global dictionary can be listed or wiped clean:++    :browse+    :clear++Installed files can be loaded:++    :load church++Machine-readable node statistics are output to stdout, as well as when+free variables are instantiated by looking up their definitions.  These+are intended to be used for sonification, for example with Pure-data:++    pd extra/gulcii.pd &+    sleep 5+    gulcii | pdsend 8765++The sonification is controlled by two commands:++    :start+    :stop+++Settings+--------++There are some runtime adjustable settings:++    :get NewsOnTop+    :set NewsOnTop+    :unset NewsOnTop+    :toggle NewsOnTop++Where NewsOnTop is a setting.  Settings include:++    TraceEvaluation+    CollectGarbage+    RealTimeDelay+    RealTimeAcceleration+    RetryIrreducible+    EmitStatistics+    EmitRebindings+    EchoToStdOut+    EchoToGUI+    SaveImages+    NewsOnTop
+ doc/Makefile view
@@ -0,0 +1,12 @@+all: encoding.pdf++clean:+	-rm -f encoding.aux encoding.log encoding.md.tex encoding.nav encoding.out encoding.pdf encoding.snm encoding.toc encoding.vrb++encoding.pdf: encoding.tex encoding.md.tex+	pdflatex encoding.tex+	pdflatex encoding.tex+	pdflatex encoding.tex++encoding.md.tex: encoding.md+	pandoc -t beamer --slide-level 2 encoding.md -o encoding.md.tex
+ doc/encoding.md view
@@ -0,0 +1,518 @@+# Lambda calculus encodings++## Notation++Backslash is used for lambda:++* easier to type+* familiar from Haskell++Neighbouring lambdas can be combined with one backslash:++    \a b s z . a s (b s z)++Corresponds to:++    λa. λb. λs. λz. a s (b s z)+++## Church and Scott encodings++* encode data as lambda terms+* continuation passing style+* Church folds vs Scott case analysis+++## Continuation passing style++* the datum is a black box that knows itself+* the datum is passed functions that it calls with its deconstruction+* the datum has one argument per constructor+* each continuation has one argument per constructor argument+++## Simple types++Church and Scott encoding coincide for simple types.+++## Bool++Haskell:++    data Bool+      = False+      | True++Church, Scott:++    true  = \t f . t+    false = \t f . f++    and = \a b . a b a+    or  = \a b . a a b+    not = \a . a false true++The datum "true" takes two arguments, and returns the first, which (by+convention) denotes the value True.+++## Pair++Haskell:++    data Pair a b+      = Pair a b++Church, Scott:++    pair = \a b p . p a b++    fst  = \p . p (\a b . a)+    snd  = \p . p (\a b . b)++The datum "pair x y" takes one argument, which is a function of two arguments,+and passes it the stored values of "x" and "y".+++## Maybe++Haskell:++    data Maybe a+      = Nothing+      | Just a++Church, Scott:++    nothing = \n j . n+    just    = \a n j . j a++    maybe   = \n j m . m n j+++## Either++Haskell:++    data Either a b+      = Left a+      | Right b++Church, Scott:++    left   = \a l r . l a+    right  = \b l r . r b++    either = \l r e . e l r+++## Recursive types++* Church and Scott encoding differ for recursive types.++* Church encoding uses folds.++    The deconstruction continuation threads throughout+    the structure.++* Scott encoding is similar to case analysis.++    The deconstruction continuation+    unwraps one layer of constructors only.+++## Natural numbers++Haskell:++    data Nat+      = Zero+      | Succ Nat+  +Church:++    zero = \s z . z+    succ = \n s z . s (n s z)+  +Scott:++    zero = \s z . z+    succ = \n s z . s n+++## Nat examples++Haskell:++    Zero, Succ Zero, Succ(Succ Zero), Succ(Succ(Succ Zero))++Church, applying the same "s" "n" times at once:++    \s z . z+    \s z . s z+    \s z . s (s z)+    \s z . s (s (s z))++Scott, applying different "s" "n" times separately:++    \s z . z+    \s z . s (\s z . z)+    \s z . s (\s z . s (\s z . z))+    \s z . s (\s z . s (\s z . s (\s z . z)))+++## Church Nat succ++    zero = \s z . z+    succ = \n s z . s (n s z)++      succ zero+    = {- definition of succ -}+      (\n s z . s (n s z)) zero+    = {- beta -}+      \s z . s (zero s z)+    = {- definition of zero -}+      \s z . s ((\s z . z) s z)+    = {- beta -}+      \s z . s ((\z . z) z)+    = {- beta -}+      \s z . s z+    = {- definition of one -}+      one+++## Scott Nat succ++    zero = \s z . z+    succ = \n s z . s n++      succ zero+    = {- definition of succ -}+      (\n s z . s n) zero+    = {- beta -}+      \s z . s zero+    = {- definition of zero -}+      \s z . s (\s z . z)+    = {- definition of one -}+      one+++## Nat arithmetic++Church:++    add = \m n . m succ n+    mul = \m n . m (add n) zero+    exp = \m n . n m++Scott, open terms with `letrec`:++    add = \m n . m (\p . succ  (add p n)) n+    mul = \m n . m (\p . add n (mul p n)) zero+    exp = \m n . n (\p . mul m (exp m p)) one++Scott, closed terms with `fix`:++    add = fix (\add . \m n . m (\p . succ  (add p n)) n)+    mul = fix (\mul . \m n . m (\p . add n (mul p n)) zero)+    exp = fix (\exp . \m n . n (\p . mul m (exp m p)) one)+++## Fixed point combinator++Semantics:++    fix f = f (fix f)++Implementation:++    \f . (\x . f (x x)) (\x . f (x x))++What it computes:++* The unique least fixed point under the definedness order.++* Allows recursive functions to be defined as closed terms.+++## Nat predecessor++Church (courtesy Wikipedia):++    pred = \n f x . n (\g h . h (g f)) (\u . x) (\v . v)++Scott:++    pred = \n . n (\p . p) zero+++## Nat conversion++Church arithmetic is more concise (and doesn't need `fix`).++Scott predecessor is comprehensible.++Mix and match?++    churchToScott = \n . n scottSucc scottZero++    scottToChurch = \n . n+        (\p . churchSucc (scottToChurch p))+        churchZero++    scottToChurch = fix (\scottToChurch . \n . n+        (\p . churchSucc (scottToChurch p))+        churchZero)+++## Nat subtract and equality++Church:++    sub = \m n . n pred m++Scott:++    sub = \m n . m+      (\p . n (\q . sub p q) m)+      zero+    equal = \m n . m+      (\p . n (\q . equal p q) false)+      (n (\q . false) true)++Unwrap a layer of constructor from each number and recurse.++There is a different `equal` for booleans:++    equalBool = \a b . a b (not b)+++## List++Haskell:++    data List a+      = Nil+      | Cons a (List a)++Church:++    nil  = \c n . n+    cons = \x xs c n . c x (xs c n)++Scott:++    nil  = \c n . n+    cons = \x xs c n . c x xs+++## List operations++Church, Scott:++    isnil  = \l . l (\x xs . false) true+    head   = \l . l (\x xs . x) error++Church (`tail` courtesy Wikipedia):++    length = \l . l (\x xs . succ xs) zero+    tail   = \l c n . l+        (\x xs g . g x (xs c)) (\xs . n) (\x xs . xs)++Scott:++    length = \l . l (\x xs . succ (length xs)) zero+    tail   = \l . l (\x xs . xs) nil+++## More Scott functions++    compose = \f g x . f (g x)++    fold = \f e l . l (\x xs . f x (fold f e xs)) e++    sum  = fold add zero+    ands = fold and true+    ors  = fold or false++    map = \f . fold (compose cons f) nil+    all = \f . compose ands (map f)+    any = \f . compose ors (map f)++    take = \n l. n(\p. l (\x xs. cons x (take p xs))nil)nil+    drop = \n l. n(\p. l (\x xs. drop p xs) nil) l++    iterate = \f x . cons x (iterate f (f x))+++# How to perform lambda calculus+++## How to perform lambda calculus++* single step graph reduction++* visualisation of current state++* sonification of changes in state++* open terms vs closed terms+++## Graph reduction++    data Term+      = Free String+      | Reference Integer+      | Bound          -- de Bruijn index 0+      | Scope Term     -- see Lambdascope paper+      | Lambda Strategy Term+      | Apply Term Term++    reduce+      :: Definitions   -- Map String  Term+      -> References    -- Map Integer Term+      -> Term+      -> Maybe (References, Term)+++## Three kinds of Lambda++* strict (syntax inspired by Haskell's -XBangPatterns):++        (\v ! s) t++    t is fully reduced before substitution into s.++* copy:++        (\v ? s) t++    t is substituted for each occurrence of v in s.++* lazy:++        (\v . s) t++    a new `Reference` is created for t, and substituted into s.++    `reduce` reduces *inside* the `References` until it is irreducible, at which+    point the `Reference` is replaced with the `Term` it refers to.+++## Visualisation++![](visualisation.png){width=100%}\ ++## Sonification++* count number of nodes of each type++* statistics are forwarded to a Pure-data patch++* changes in each count control a harmonic (one for each type of node) in a+  simple phase modulation synth+++## Open terms++* free variables looked up on demand from environment++* allows definitions to be changed at runtime++* easier to write+++## Drawbacks of open terms++* no sharing++    subterms can be evaluated many times due to duplication++* exponential work (worst case)++* exponential space (worst case)+++## Fixed points++* closed terms with fixed point combinators++* allows evaluation to be shared++* sharing can be vital for efficiency+++# Future work+++## Better Evaluator++* current evaluator is still somewhat ad-hoc and doesn't preserve sharing++* previous evaluator even had correctness bugs++* switch to using Lambdascope (or similar) as a library?+++## Auto Fix++Automatically translating open terms to use fixed point combinators:++* recursive functions can use `fix`+* mutually recursive functions can use `fix` combined with tuples++        many = some `orElse` none+        some = one `andThen` many++    becomes:++        manysome = fix (\p -> pair+            (snd p `orElse` none)+            (one `andThen` fst p) )+        many = fst manysome+        some = snd manysome+++## Magic It++* refer to previously evaluated terms+* including the currently evaluating term+* without restarting evaluation++Haskell example (`ghci-8.0.1`):++    > 3+    3+    > it + 5+    8+    > it * 2+    16+++## Further Performances / Project Ideas++* "An infinite deal of nothing", a variety of non-terminating loops each with+  their own intrinsic computational rhythm.++* Implement in untyped lambda calculus an interpreter for a known+  Turing-complete tape mutation based language and run some simple programs+  in it.++    Illustrates Turing-completeness of untyped lambda calculus, albeit slowly.+++# EOF++## EOF++Thanks!++Questions?++    https://mathr.co.uk+    mailto:claude@mathr.co.uk++    https://hackage.haskell.org/package/gulcii+    https://code.mathr.co.uk/gulcii
+ doc/encoding.tex view
@@ -0,0 +1,31 @@+\documentclass[aspectratio=43]{beamer}+\usepackage{lmodern}+\usepackage[utf8]{inputenc}+\usepackage[T1]{fontenc}+\DeclareUnicodeCharacter{03BB}{\(\lambda\)}+\AtBeginSection[]{\begin{frame}\frametitle{Outline}\tableofcontents[currentsection]\end{frame}}+\def\tightlist{}++\definecolor{mathr}{RGB}{128,64,64}+\setbeamercolor{structure}{fg=mathr}+\setbeamercolor{title}{fg=mathr}+\setbeamercolor{titlelike}{fg=mathr}+\beamertemplatenavigationsymbolsempty++\renewcommand{\familydefault}{\sfdefault}++\title[GULCII]{Graphical\\ Untyped Lambda Calculus\\ Interactive Interpreter}+\subtitle{(GULCII)}+\author{Claude Heiland-Allen}+\institute{\url{https://mathr.co.uk} \\ \url{mailto:claude@mathr.co.uk}}+\date[Ed 2017]{Edinburgh, 2017}+\subject{Computer Science}++\begin{document}++\begin{frame} \titlepage \end{frame}+\begin{frame} \frametitle{Outline} \tableofcontents \end{frame}++\input{encoding.md.tex}++\end{document}
+ doc/visualisation.png view

binary file changed (absent → 127718 bytes)

− extra/fudi2midi.pd 
@@ -1,59 +0,0 @@-#N canvas 0 0 547 342 10;-#X obj 28 2 netreceive 8765;-#X obj 29 172 noteout;-#X msg 29 127 \$2 \$3 \$1;-#X msg 35 148 \$2 0 \$1;-#X obj 109 173 pgmout;-#X msg 109 150 \$2 \$1;-#X obj 176 173 ctlout;-#X msg 177 150 \$3 \$2 \$1;-#X msg 242 150 \$2 \$1;-#X obj 242 171 touchout;-#X msg 315 148 \$3 \$2 \$1;-#X obj 315 169 polytouchout;-#X msg 398 148 \$2 \$1;-#X obj 398 169 bendout;-#X obj 371 84 spigot;-#X obj 404 18 tgl 15 0 empty empty empty 17 7 0 10 -262144 -1 -1 1-1;-#X obj 158 1 print connection;-#X obj 371 105 print unhandled;-#X obj 416 44 spigot;-#X obj 447 16 tgl 15 0 empty empty empty 17 7 0 10 -262144 -1 -1 0-1;-#X obj 418 65 print debug;-#X obj 29 48 route noteon noteoff program control pressure touch bend-rebound;-#X floatatom 116 29 5 0 0 0 - - -;-#X obj 300 12 route rebound;-#X obj 296 36 print midi;-#X obj 297 -7 spigot;-#X obj 342 -5 tgl 15 0 empty empty empty 17 7 0 10 -262144 -1 -1 1-1;-#X connect 0 0 18 0;-#X connect 0 0 21 0;-#X connect 0 0 25 0;-#X connect 0 1 16 0;-#X connect 0 1 22 0;-#X connect 2 0 1 0;-#X connect 3 0 1 0;-#X connect 5 0 4 0;-#X connect 7 0 6 0;-#X connect 8 0 9 0;-#X connect 10 0 11 0;-#X connect 12 0 13 0;-#X connect 14 0 17 0;-#X connect 15 0 14 1;-#X connect 18 0 20 0;-#X connect 19 0 18 1;-#X connect 21 0 2 0;-#X connect 21 1 3 0;-#X connect 21 2 5 0;-#X connect 21 3 7 0;-#X connect 21 4 8 0;-#X connect 21 5 10 0;-#X connect 21 6 12 0;-#X connect 21 8 14 0;-#X connect 23 1 24 0;-#X connect 25 0 23 0;-#X connect 26 0 25 1;
+ extra/gulcii.pd view
@@ -0,0 +1,29 @@+#N canvas 3 58 335 369 10;+#X obj 18 10 netreceive 8765;+#X obj 21 101 loadbang;+#X obj 21 122 delay 1000;+#X msg 22 148 \; pd dsp 1;+#X obj 121 40 print;+#X obj 141 252 catch~ \$0-r;+#X obj 70 209 gulcii_v \$0 0;+#X obj 27 251 catch~ \$0-l;+#X obj 19 40 s \$0-control;+#X obj 168 126 list prepend set;+#X obj 168 148 list trim;+#X msg 168 170 rebound succ;+#X obj 59 65 route statistics;+#X obj 90 310 dac~;+#X obj 27 273 expr~ tanh($v1);+#X obj 142 275 expr~ tanh($v1);+#X connect 0 0 8 0;+#X connect 0 0 12 0;+#X connect 0 1 4 0;+#X connect 1 0 2 0;+#X connect 2 0 3 0;+#X connect 5 0 15 0;+#X connect 7 0 14 0;+#X connect 9 0 10 0;+#X connect 10 0 11 0;+#X connect 12 1 9 0;+#X connect 14 0 13 0;+#X connect 15 0 13 1;
+ extra/gulcii_m.pd view
@@ -0,0 +1,29 @@+#N canvas 3 58 450 300 10;+#X obj 21 22 receive~ \$1-p;+#X obj 20 218 throw~ \$1-l;+#X obj 97 218 throw~ \$1-r;+#X obj 21 134 expr~ sin($v1*6.283185307179586);+#X obj 97 157 expr~ sin($v1*6.283185307179586);+#X obj 147 19 inlet;+#X obj 147 40 float;+#X obj 147 61 vline~;+#X obj 21 43 *~ \$2;+#X obj 97 189 *~;+#X obj 20 192 *~;+#X obj 96 106 +~ 0.25;+#X obj 147 82 hip~ 1;+#X obj 147 103 lop~ 15;+#X connect 0 0 8 0;+#X connect 3 0 10 0;+#X connect 4 0 9 0;+#X connect 5 0 6 0;+#X connect 6 0 7 0;+#X connect 7 0 12 0;+#X connect 8 0 3 0;+#X connect 8 0 11 0;+#X connect 9 0 2 0;+#X connect 10 0 1 0;+#X connect 11 0 4 0;+#X connect 12 0 13 0;+#X connect 13 0 9 1;+#X connect 13 0 10 1;
+ extra/gulcii_v.pd view
@@ -0,0 +1,78 @@+#N canvas 3 63 472 453 10;+#X obj 46 214 vline~;+#X obj 37 392 *~;+#X obj 125 392 *~;+#X obj 182 246 send~ \$0-p;+#X obj 127 312 +~;+#X obj 143 267 catch~ \$0-l;+#X obj 223 267 catch~ \$0-r;+#X obj 209 312 +~;+#X obj 127 345 expr~ sin($v1*6.283185307179586);+#X obj 207 365 expr~ sin($v1*6.283185307179586);+#X obj 18 43 route start stop statistics;+#X obj 37 413 throw~ \$1-l;+#X obj 125 413 throw~ \$1-r;+#X obj 18 18 r \$1-control;+#X obj 358 107 gulcii_m \$0 6;+#X obj 358 128 gulcii_m \$0 5;+#X obj 358 149 gulcii_m \$0 4;+#X obj 358 170 gulcii_m \$0 3;+#X obj 358 191 gulcii_m \$0 2;+#X obj 358 212 gulcii_m \$0 1;+#X obj 143 288 *~ 0.125;+#X obj 224 288 *~ 0.125;+#X obj 133 109 +;+#X obj 163 109 +;+#X obj 193 109 +;+#X obj 223 109 +;+#X obj 253 109 +;+#X obj 132 136 vline~;+#X obj 132 179 lop~ 15;+#X obj 130 228 phasor~;+#X obj 132 158 hip~ 1;+#X obj 131 203 +~ 50;+#X msg 18 166 1 1000;+#X msg 80 168 0 1000;+#X obj 143 68 unpack f f f f f f;+#X connect 0 0 1 0;+#X connect 0 0 2 0;+#X connect 1 0 11 0;+#X connect 2 0 12 0;+#X connect 4 0 8 0;+#X connect 5 0 20 0;+#X connect 6 0 21 0;+#X connect 7 0 9 0;+#X connect 8 0 1 1;+#X connect 9 0 2 1;+#X connect 10 0 32 0;+#X connect 10 1 33 0;+#X connect 10 2 34 0;+#X connect 13 0 10 0;+#X connect 20 0 4 1;+#X connect 21 0 7 1;+#X connect 22 0 27 0;+#X connect 23 0 22 1;+#X connect 24 0 23 1;+#X connect 25 0 24 1;+#X connect 26 0 25 1;+#X connect 27 0 30 0;+#X connect 28 0 31 0;+#X connect 29 0 3 0;+#X connect 29 0 4 0;+#X connect 29 0 7 0;+#X connect 30 0 28 0;+#X connect 31 0 29 0;+#X connect 32 0 0 0;+#X connect 33 0 0 0;+#X connect 34 0 19 0;+#X connect 34 0 22 0;+#X connect 34 1 18 0;+#X connect 34 1 23 0;+#X connect 34 2 17 0;+#X connect 34 2 24 0;+#X connect 34 3 16 0;+#X connect 34 3 25 0;+#X connect 34 4 15 0;+#X connect 34 4 26 0;+#X connect 34 5 14 0;+#X connect 34 5 26 1;
gulcii.cabal view
@@ -1,84 +1,73 @@ Name:               gulcii-Version:            0.2.0.3+Version:            0.3 Synopsis:           graphical untyped lambda calculus interactive interpreter Description:   GULCII is an untyped lambda calculus interpreter supporting interactive   modification of a running program with graphical display of graph reduction.   .-  There are three variants of lambda abstraction: lazy, strict, and copy:-  .-  @> \x . f x x    -- x is evaluated lazily with sharing@-  @> \x ! f x x    -- x is evaluated strictly and shared@-  @> \x ? f x x    -- x is copied before any evaluation@-  .-  There is additional syntax sugar for natural numbers and lists, using-  <http://en.wikipedia.org/wiki/Mogensen%E2%80%93Scott_encoding#Scott_encoding>:-  .-  @> [0,1,2,3]@-  .-  There is a small standard library based loosely around the Haskell Prelude,-  with additions geared towards MIDI generation for live-coding music, implemented-  using a mechanism similar to 'Debug.Trace.trace':-  .-  @> \x y . &#123; print : x &#125; y@-  .-  Quick start:-  .-  > gulcii-  > :load mars-  > main-  > :quit-  .-  If you have Pure-data and Timidity, try:-  .-  > timidity -iA -Oj &-  > pd -alsamidi ~/.cabal/share/gulcii-0.2.0.3/extra/fudi2midi.pd &-  > gulcii | pdsend 8765-  .-  See also: live-sequencer which has many more features (but no sharing during-  evaluation).+  See README.md for the user manual. -Homepage:           http://code.mathr.co.uk/gulcii+Homepage:           https://code.mathr.co.uk/gulcii License:            GPL-2 License-file:       LICENSE Author:             Claude Heiland-Allen Maintainer:         claude@mathr.co.uk-Category:           Sound, Music, GUI+Category:           Compilers/Interpreters Build-type:         Simple Cabal-version:      >=1.6-Tested-With:        GHC==7.6.3, GHC==7.8.2+Tested-With:        GHC==8.2.1 -Data-files:         extra/fudi2midi.pd,-                    lib/bits.gu,+extra-source-files: doc/Makefile+                    doc/encoding.md+                    doc/encoding.tex+                    doc/visualisation.png+                    README.md++Data-files:         lib/bits.gu,                     lib/bool.gu,+                    lib/church.gu,                     lib/either.gu,-                    lib/event.gu,                     lib/function.gu,                     lib/list.gu,                     lib/maybe.gu,-                    lib/midi.gu,                     lib/natural.gu,                     lib/pair.gu,                     lib/prelude.gu,-                    lib/mars.gu+                    lib/edinburgh.gu,+                    extra/gulcii.pd,+                    extra/gulcii_m.pd,+                    extra/gulcii_v.pd  Executable gulcii   HS-source-dirs:   src   Main-is:          Main.hs   Build-depends:    base >= 3 && < 6,                     containers >= 0.3 && < 0.6,-                    filepath >= 1.1 && < 1.4,-                    gtk >= 0.11 && < 0.14,+                    filepath >= 1.1 && < 1.5,+                    gtk >= 0.11 && < 0.15,                     cairo >= 0.11 && < 0.14-  Other-modules:    Bruijn Command Draw Evaluation Graph Lambda Layout Meta Parse Sugar+  Other-modules:    Bruijn+                    Command+                    Draw+                    Evaluation+                    GC+                    Graph+                    Lambda+                    Layout+                    Meta+                    Parse+                    Paths_gulcii+                    Reduce+                    Setting+                    Sugar   ghc-options:      -Wall -threaded -rtsopts --  ghc-prof-options: -prof -auto-all -caf-all  Source-Repository head   Type: git-  Location: http://code.mathr.co.uk/gulcii.git+  Location: https://code.mathr.co.uk/gulcii.git  Source-Repository this   Type: git-  Tag: v0.2.0.3-  Location: http://code.mathr.co.uk/gulcii.git+  Tag: v0.3+  Location: https://code.mathr.co.uk/gulcii.git
+ lib/church.gu view
@@ -0,0 +1,33 @@+id = \x . x+const = \x y . x+true = \t f . t+false = \t f . f+and = \a b . a b a+or = \a b . a a b+not = \a . a false true+zero = \s z . z+succ = \n s z . s (n s z)+iszero = \n . n (const false) true+add = \m n . m succ n+mul = \m n . m (add n) zero+exp = \m n . n m+pred = \n s z . n (\g h . h (g s)) (\u . z) (\u . u)+sub = \m n . n pred m+equal = \m n . and (iszero (sub m n)) (iszero (sub n m))+nil = \c n . n+cons = \x xs c n . c x (xs c n)+isnil = \l . l (\x xs . false) true+head = \l . l (\x xs . x) id+tail = \l c n . l (\x xs g . g x (xs c)) (\xs . n) (\x xs . xs)+map = \f l . l (\x xs . cons (f x) xs) nil+sum = \l . l (\x xs . add x xs) zero+length = \l . l (\x xs . succ xs) zero+pair = \a b p . p a b+fst = \p . p (\a b . a)+snd = \p . p (\a b . b)+nothing = \n j . n+just = \a n j . j a+maybe = \n j m . m n j+left = \a l r . l a+right = \b l r . r b+either = \l r e . e l r
+ lib/edinburgh.gu view
@@ -0,0 +1,55 @@+# boolean+false = \ t f . f+true = \ t f . t+and = \ a b . a b a+or = \ a b . a a b+not = \ a . a false true+# function+id = \ a . a+const = \ a b . a+compose = \ bc ab a . bc (ab a)+flip = \ abc b a . abc a b+fix = \ f . (\x . f (x x)) (\x . f (x x))+error = \e . error e+seq = \ a ! \b . b+# list+nil = \ c n . n+cons = \ x xs c n . c x xs+null = \ l . l (\x xs . false) true+head = \ l . l (\x xs . x) (error head)+tail = \ l . l (\x xs . xs) (error tail)+map = \ f l . l (\x xs . cons (f x) (map f xs)) nil+append = \ us vs . us (\x xs . cons x (append xs vs)) vs+filter = \ p l . l (\x xs . p x (cons x) id (filter p xs)) nil+index = \ l n . n (\p . l (\x xs . index xs p) (error index)) (l (\x xs . x) (error index))+reverse = \ l . l (\x xs . append (reverse xs) (cons x nil)) nil+foldr = \ f e l . l (\x xs . f x (foldr f e xs)) e+length = foldr (const succ) zero+ands = foldr and true+ors = foldr or false+concat = foldr append nil+all = \f . compose ands (map f)+any = \f . compose ors (map f)+concatMap = \f . compose concat (map f)+composes = foldr compose id+sum = foldr add zero+product = foldr mul (succ zero)+repeat = \x . cons x (repeat x)+cycle = compose concat repeat+take = \n l . n (\p . l (\x xs . cons x (take p xs)) nil) nil+drop = \n l . n (\p . l (\x xs . drop p xs) nil) l+transpose = \l . l (\xs xss . xs (\y ys . cons (cons y (concatMap (take 1) xss)) (transpose (cons ys (map (drop 1) xss)))) (transpose xss)) nil+iterate = \f x . cons x (iterate f (f x))+last = \l . l (\x xs . xs (\y ys . last xs) x) (error last)+replicate = \n x . take n (repeat x)+# natural+zero = \ s z . z+succ = \ n s z . s n+infinity = succ infinity+even = \n . n odd true+odd = \n . n even false+add = \ m n . m (\p . succ (add n p)) n+mul = \ m n . m (\p . add n (mul n p)) zero+exp = \ m n . n (\p . mul m (exp m p)) one+sub = \ m n . m (\p . n (sub p) m) zero+equal = \ m n . m (\mm . n (\nn . equal mm nn) false) (n (\nn . false) true)
− lib/event.gu 
@@ -1,6 +0,0 @@-# event-wait = \n w e . w n-event = \x w e . e x-merge = \al bl . al (\a as . bl (\b bs . a (\aw . b (\bw . lessthan aw bw (cons a (merge as (cons (wait (sub bw aw)) bs))) (cons b (merge (cons (wait (sub aw bw)) as) bs))) (\e . cons b (merge al bs))) (\e . cons a (merge as bl))) al) bl-merges = foldr merge nil-play = \l . l (\x xs . x (\w . { wait : w } (play xs)) (\e . e (play xs))) (error play)
− lib/mars.gu 
@@ -1,5 +0,0 @@-:load prelude-main = play (cons (event (program 0 48)) timpanis)-timpanis = append timpani timpanis-timpani = concatMap makeNote [20,20,20,60,60,30,30,60]-makeNote = \d ! note d 0 43 96
− lib/midi.gu 
@@ -1,7 +0,0 @@-# midi-noteOn = \c n v ! \x . { noteon : [c, n, v] } x-noteOff = \c n v ! \x . { noteoff : [c, n, v] } x-program = \c p ! \x . { program : [c, p] } x-control = \c p v ! \x . { control : [c, p, v] } x-note = \d ! \c n v . [ event (noteOn c n v), wait d, event (noteOff c n v) ]-rest = \d ! [ wait d ]
lib/prelude.gu view
@@ -1,10 +1,8 @@ :load bits :load bool :load either-:load event :load function :load list :load maybe-:load midi :load natural :load pair
src/Bruijn.hs view
@@ -1,6 +1,6 @@ {-     gulcii -- graphical untyped lambda calculus interpreter-    Copyright (C) 2011, 2013  Claude Heiland-Allen+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen      This program is free software; you can redistribute it and/or modify     it under the terms of the GNU General Public License as published by@@ -17,7 +17,7 @@     51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. -} -module Bruijn (Term(..), bruijn, freeVariablesIn, bind) where+module Bruijn (Term(..), bruijn, freeVariablesIn) where  import Data.Maybe (listToMaybe) import Data.Set (Set, empty, singleton, union)@@ -27,10 +27,10 @@  data Term   = Free String-  | Bound Integer+  | Bound0+  | Scope Term   | Lambda Strategy Term   | Apply Term Term-  | Trace String Term Term   deriving (Read, Show, Eq, Ord)  bruijn :: U.Term -> Term@@ -42,25 +42,19 @@ bruijn' m (U.Variable v) =   case genericElemIndex v m of     Nothing -> Free v-    Just i -> Bound i-bruijn' m (U.Trace k s t) = Trace k (bruijn' m s) (bruijn' m t)--bind :: Strategy -> String -> Term -> Term-bind k v t = Lambda k (bind' 0 v t)+    Just i -> applyN i Scope Bound0 -bind' :: Integer -> String -> Term -> Term-bind' i v f@(Free u) = if u == v then Bound i else f-bind' _ _ b@(Bound _) = b-bind' i v (Apply s t) = Apply (bind' i v s) (bind' i v t)-bind' i v (Lambda _ t) = bind' (i + 1) v t-bind' i v (Trace k s t) = Trace k (bind' i v s) (bind' i v t)+applyN :: Integer -> (a -> a) -> a -> a+applyN n f+  | n == 0 = id+  | otherwise = f . applyN (n - 1) f  freeVariablesIn :: Term -> Set String freeVariablesIn (Free v) = singleton v-freeVariablesIn (Bound _) = empty+freeVariablesIn Bound0 = empty+freeVariablesIn (Scope t) = freeVariablesIn t freeVariablesIn (Lambda _ t) = freeVariablesIn t freeVariablesIn (Apply s t) = freeVariablesIn s `union` freeVariablesIn t-freeVariablesIn (Trace _ s t) = freeVariablesIn s `union` freeVariablesIn t  {- Generic list functions.
src/Command.hs view
@@ -1,6 +1,6 @@ {-     gulcii -- graphical untyped lambda calculus interpreter-    Copyright (C) 2011, 2013  Claude Heiland-Allen+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen      This program is free software; you can redistribute it and/or modify     it under the terms of the GNU General Public License as published by@@ -25,11 +25,10 @@ import qualified Meta as M import Parse -data Command = Define String S.Term | Evaluate S.Term | Execute S.Term | Meta M.Meta+data Command = Define String S.Term | Evaluate S.Term | Meta M.Meta   deriving (Read, Show, Eq, Ord)  parse :: Parser String Command parse =  (Define   <$> name <* sym "=" <*> S.parse)      <|> (Evaluate <$> S.parse)-     <|> (Execute  <$  sym "~" <*> S.parse)      <|> (Meta     <$  sym ":" <*> M.parse)
src/Draw.hs view
@@ -1,6 +1,6 @@ {-     gulcii -- graphical untyped lambda calculus interpreter-    Copyright (C) 2011, 2013  Claude Heiland-Allen+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen      This program is free software; you can redistribute it and/or modify     it under the terms of the GNU General Public License as published by@@ -19,11 +19,10 @@  module Draw (draw) where -import Data.List (genericDrop) import qualified Data.Map.Strict as M import Data.Map.Strict (Map) -import Graphics.Rendering.Cairo+import Graphics.Rendering.Cairo hiding (x, y)  import qualified Layout as L import Evaluation (Strategy(..))@@ -32,14 +31,14 @@  colour :: L.Term -> RGB colour (L.Free      _ _) = (0, 0.5, 1)-colour (L.Bound     _ _) = (0.5, 0, 1)+colour (L.Bound0      _) = (0.5, 0, 1)+colour (L.Scope     _ _) = (1, 1, 0) colour (L.Lambda Strict _ _) = (1, 0, 0) colour (L.Lambda Lazy   _ _) = (1, 0, 0.5) colour (L.Lambda Copy   _ _) = (1, 0, 1) colour (L.Apply   _ _ _) = (1, 0.5, 0) colour (L.RefInst _ _ _) = (0.5, 1, 0) colour (L.Reference _ _) = (0, 1, 0.5)-colour (L.Trace _ _ _ _) = (1, 1, 0)  circle :: L.Coords -> RGB -> Render () circle (x, y) (r, g, b) = do@@ -94,54 +93,53 @@   e <- textExtents s   moveTo (fromIntegral x - textExtentsWidth e / 2) (fromIntegral y)   textPath s-drawNames (L.Bound _ _) = return ()+drawNames (L.Bound0 _) = return ()+drawNames (L.Scope t _) = drawNames t drawNames (L.Lambda _ t _) = drawNames t drawNames (L.Apply a b _) = drawNames a >> drawNames b drawNames (L.RefInst _ t _) = drawNames t drawNames (L.Reference _ _) = return ()-drawNames (L.Trace s a b (x,y)) = do-  e <- textExtents s-  moveTo (fromIntegral x - textExtentsWidth e / 2) (fromIntegral y)-  textPath s-  drawNames a-  drawNames b  drawLinks :: Map Integer L.Coords -> L.Term -> Render ()-drawLinks _  (L.Free _ _) = return ()-drawLinks _  (L.Bound _ _) = return ()-drawLinks ps (L.Lambda _ t xy) = let x'y' = L.coordinates t-                                 in line xy x'y' >> drawLinks ps t-drawLinks ps (L.Apply a b xy) = let axay = L.coordinates a-                                    bxby = L.coordinates b-                                in line xy axay >> line xy bxby >> drawLinks ps a >> drawLinks ps b-drawLinks ps (L.RefInst _ t xy) = let x'y' = L.coordinates t-                                  in line xy x'y' >> drawLinks ps t-drawLinks ps (L.Reference p xy) = let Just x'y' = M.lookup p ps-                                  in line xy x'y'-drawLinks ps (L.Trace _ a b xy) =+drawLinks _  (L.Free _ _) =+  return ()+drawLinks _  (L.Bound0 _) =+  return ()+drawLinks ps (L.Scope t xy) =+  let x'y' = L.coordinates t+  in  line xy x'y' >> drawLinks ps t+drawLinks ps (L.Lambda _ t xy) =+  let x'y' = L.coordinates t+  in  line xy x'y' >> drawLinks ps t+drawLinks ps (L.Apply a b xy) =   let axay = L.coordinates a       bxby = L.coordinates b   in  line xy axay >> line xy bxby >> drawLinks ps a >> drawLinks ps b+drawLinks ps (L.RefInst _ t xy) =+  let x'y' = L.coordinates t+  in  line xy x'y' >> drawLinks ps t+drawLinks ps (L.Reference p xy) =+  let Just x'y' = M.lookup p ps+  in  line xy x'y'  drawVLinks :: [L.Coords] -> L.Term -> Render ()-drawVLinks ls (L.Bound n xy) =-  case genericDrop n ls of-    [] -> return ()-    x'y':_ -> line xy x'y'+drawVLinks ls (L.Bound0 xy) = case ls of+  [] -> return () -- should be error?+  x'y':_ -> line xy x'y'+drawVLinks ls (L.Scope t _) = drawVLinks (drop 1 ls) t drawVLinks ls (L.Lambda _ t xy) = drawVLinks (xy : ls) t drawVLinks ls (L.Apply  s t _) = drawVLinks ls s >> drawVLinks ls t drawVLinks ls (L.RefInst _ t _) = drawVLinks ls t-drawVLinks ls (L.Trace _ s t _) = drawVLinks ls s >> drawVLinks ls t drawVLinks _ _ = return ()  drawNodes :: L.Term -> Render () drawNodes n@(L.Free      _ _) = drawNode n-drawNodes n@(L.Bound     _ _) = drawNode n+drawNodes n@(L.Bound0      _) = drawNode n+drawNodes n@(L.Scope     t _) = drawNode n >> drawNodes t drawNodes n@(L.Lambda  _ t _) = drawNode n >> drawNodes t drawNodes n@(L.Apply   a b _) = drawNode n >> drawNodes a >> drawNodes b drawNodes n@(L.RefInst _ t _) = drawNode n >> drawNodes t drawNodes n@(L.Reference _ _) = drawNode n-drawNodes n@(L.Trace _ a b _) = drawNode n >> drawNodes a >> drawNodes b  drawNode :: L.Term -> Render () drawNode n = circle (L.coordinates n) (colour n)
+ src/GC.hs view
@@ -0,0 +1,85 @@+{-+    gulcii -- graphical untyped lambda calculus interpreter+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen++    This program is free software; you can redistribute it and/or modify+    it under the terms of the GNU General Public License as published by+    the Free Software Foundation; either version 2 of the License, or+    (at your option) any later version.++    This program is distributed in the hope that it will be useful,+    but WITHOUT ANY WARRANTY; without even the implied warranty of+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the+    GNU General Public License for more details.++    You should have received a copy of the GNU General Public License along+    with this program; if not, write to the Free Software Foundation, Inc.,+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.+-}++module GC (gc) where++import Graph++import Data.Map as Map++gc+  :: References -> Term+  -> (References, Term)++gc refs term+  = let counts = refCount refs term Map.empty+    in ( Map.fromList+           [ (r, compact counts refs (refs Map.! r))+           | (r, n) <- Map.toList counts+           , n > 1 ]+        , compact counts refs term )+++type Count = Integer++refCount+  :: References -> Term+  -> Map Integer Count -> Map Integer Count++compact+  :: Map Integer Count -> References+  -> Term -> Term+++refCount refs (Scope a) counts+  = refCount refs a counts++refCount refs (Lambda _ a) counts+  = refCount refs a counts++refCount refs (Apply a b) counts+  = refCount refs a (refCount refs b counts)++refCount refs (Reference r) counts+  = case r `Map.lookup` counts of+      Just n ->+        Map.insert r (n + 1) counts+      Nothing ->+        refCount refs (refs Map.! r)+               (Map.insert r 1 counts)++refCount _ _ counts = counts+++compact counts refs (Scope term)+  = Scope (compact counts refs term)++compact counts refs (Lambda strat term)+  = Lambda strat (compact counts refs term)++compact counts refs (Apply a b)+  = Apply (compact counts refs a)+          (compact counts refs b)++compact counts refs term@(Reference r)+  = case r `Map.lookup` counts of+      Just 1 -> compact counts refs (refs Map.! r)+      _ -> term++compact _ _ term = term
src/Graph.hs view
@@ -1,6 +1,6 @@ {-     gulcii -- graphical untyped lambda calculus interpreter-    Copyright (C) 2011, 2013  Claude Heiland-Allen+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen      This program is free software; you can redistribute it and/or modify     it under the terms of the GNU General Public License as published by@@ -17,9 +17,8 @@     51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. -} -module Graph (Term(..), Definitions, References, Reduction(..), graph, reduce, pretty) where+module Graph (Term(..), Definitions, References, graph, pretty) where -import qualified Data.Map.Strict as M import Data.Map.Strict (Map)  import qualified Bruijn as B@@ -27,23 +26,23 @@  data Term   = Free !String-  | Bound !Integer+  | Bound0+  | Scope !Term   | Lambda !Strategy !Term   | Apply !Term !Term   | Reference !Integer-  | Trace !String !Term !Term   deriving (Read, Show, Eq, Ord)  pretty :: Term -> String-pretty = unwords . pretty'+pretty = concat . pretty'  pretty' :: Term -> [String] pretty' (Free s) = [s]-pretty' (Bound i) = [show i]+pretty' (Bound0) = ["0"]+pretty' (Scope t) = ["S"] ++ pretty' t pretty' (Reference i) = ['#':show i] pretty' (Lambda k t) = ["(", "\\", pretty'' k] ++ pretty' t ++ [")"]-pretty' (Apply s t) = ["("] ++ pretty' s ++ pretty' t ++ [")"]-pretty' (Trace k s t) = ["(", "{", k, ":"] ++ pretty' s ++ ["}"] ++ pretty' t ++ [")"]+pretty' (Apply s t) = ["("] ++ pretty' s ++ [" "] ++ pretty' t ++ [")"]  pretty'' :: Strategy -> String pretty'' Strict = "!"@@ -53,96 +52,9 @@ type Definitions = Map String Term type References = Map Integer Term -next :: Map Integer a -> Integer-next refs = case M.maxViewWithKey refs of-  Nothing        -> 0-  Just ((k,_),_) -> k + 1- graph :: B.Term -> Term graph (B.Free v) = Free v-graph (B.Bound i) = Bound i+graph (B.Bound0) = Bound0+graph (B.Scope t) = Scope (graph t) graph (B.Lambda k t) = Lambda k (graph t) graph (B.Apply s t) = Apply (graph s) (graph t)-graph (B.Trace k s t) = Trace k (graph s) (graph t)--{--bind :: String -> Term -> Term -> Term-bind v s t@(Free u) = if u == v then s else t-bind _ _ t@(Bound _) = t-bind v s (Lambda k t) = Lambda k (bind v s t)-bind v s (Apply a b) = Apply (bind v s a) (bind v s b)-bind _ _ t@(Reference _) = t--}--{--Reduce a graph one step, returning Nothing if it is irreducible.--}--data Reduction = Reduced Term References | Rebound String Term References | Traced String Term Term References-  deriving (Read, Show, Eq, Ord)--mapR :: (Term -> Term) -> Reduction -> Reduction-mapR f (Reduced t refs) = Reduced (f t) refs-mapR f (Rebound s t refs) = Rebound s (f t) refs-mapR f (Traced k s t refs) = Traced k s (f t) refs--reduce, reduce' :: Definitions -> References -> Term -> Maybe Reduction-reduce _ refs (Trace k s t) = Just (Traced k s t refs)-reduce defs refs term = reduce' defs refs term---- free variables are replaced with their definition-reduce' defs refs (Free v) = case M.lookup v defs of-  Nothing -> Nothing-  Just t -> let r = next refs in Just (Rebound v (Reference r) (M.insert r t refs))---- bound variables are irreducible-reduce' _ _ (Bound _) = Nothing---- non top-level traces are irreducible?---reduce' _ _ (Trace _ _ _) = Nothing-reduce' _ refs (Trace k s t) = Just (Traced k s t refs)---- maybe reduce inside lambda-reduce' defs refs (Lambda k t) = mapR (Lambda k) `fmap` reduce' defs refs t--reduce' defs refs (Apply a b) = case a of-  -- beta reduction-  Lambda Strict a' -> case reduce defs refs b of-    Just r -> Just (mapR (a `Apply`) r)-    Nothing -> Just (uncurry Reduced (beta refs a' b))-  Lambda Copy a' -> Just (Reduced (beta' 0 a' b) refs)-  Lambda Lazy a' -> Just (uncurry Reduced (beta refs a' b))-  Reference r -> case M.lookup r refs of-    Just a' -> Just (Reduced (Apply a' b) refs)-    _ -> Nothing-  Free s -> case M.lookup s defs of-    Just a' -> Just (Rebound s (Apply a' b) refs)-    _ -> Nothing-  t@(Apply _ _) -> case reduce defs refs t of-    Just r -> Just (mapR (`Apply` b) r)-    _ -> Nothing-  _ -> Nothing -- Bound, Trace---- reduce references-reduce' defs refs s@(Reference r) = case M.lookup r refs of-  Nothing -> Nothing-  Just t -> case reduce' defs refs t of-    Just (Reduced t' refs') -> Just (Reduced s (M.insert r t' refs'))-    Just (Rebound v t' refs') -> Just (Rebound v s (M.insert r t' refs'))-    _ -> Just (Reduced t refs)---- beta reduction-beta :: References -> Term -> Term -> (Term, References)-beta refs a b = (beta' 0 a t, refs')-  where-    r = next refs-    refs' = M.insert r b refs-    t = Reference r--beta' :: Integer -> Term -> Term -> Term-beta' i s@(Bound j) t = if i == j then t else s-beta' i (Lambda k s) t = Lambda k (beta' (i + 1) s t)-beta' i (Apply a b) t = Apply (beta' i a t) (beta' i b t)-beta' _ s@(Free _) _ = s-beta' _ s@(Reference _) _ = s-beta' i (Trace k a b) t = Trace k (beta' i a t) (beta' i b t)
src/Lambda.hs view
@@ -1,6 +1,6 @@ {-     gulcii -- graphical untyped lambda calculus interpreter-    Copyright (C) 2011, 2013  Claude Heiland-Allen+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen      This program is free software; you can redistribute it and/or modify     it under the terms of the GNU General Public License as published by@@ -31,7 +31,6 @@   = Variable String   | Lambda Strategy String Term   | Apply Term Term-  | Trace String Term Term   deriving (Read, Show, Eq, Ord)  {-@@ -45,7 +44,6 @@ pretty' (Variable v) = [v] pretty' (Lambda k v t) = ["(", "\\", v, pretty'' k] ++ pretty' t ++ [")"] pretty' (Apply  s t) = ["("] ++ pretty' s ++ pretty' t ++ [")"]-pretty' (Trace k s t) = ["(", "{", k, ":"] ++ pretty' s ++ ["}"] ++ pretty' t ++ [")"]  pretty'' :: Strategy -> String pretty'' Strict = "!"@@ -60,7 +58,6 @@ isFreeIn n (Variable v)  = n == v isFreeIn n (Lambda _ v t)  = if n == v then False else n `isFreeIn` t isFreeIn n (Apply t t')  = n `isFreeIn` t || n `isFreeIn` t'-isFreeIn n (Trace _ t t')  = n `isFreeIn` t || n `isFreeIn` t'  {- Get all variable names defined or referenced by a term.@@ -70,7 +67,6 @@ variablesIn (Variable v)  = [v] variablesIn (Lambda _ v t)  = nub $ v : variablesIn t variablesIn (Apply t t')  = nub $ variablesIn t ++ variablesIn t'-variablesIn (Trace _ t t')  = nub $ variablesIn t ++ variablesIn t'  {- Get all free variables referenced by a term.
src/Layout.hs view
@@ -1,6 +1,6 @@ {-     gulcii -- graphical untyped lambda calculus interpreter-    Copyright (C) 2011, 2013  Claude Heiland-Allen+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen      This program is free software; you can redistribute it and/or modify     it under the terms of the GNU General Public License as published by@@ -17,7 +17,7 @@     51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA. -} -module Layout (Term(..), Coords, Layout(..), layout, coordinates) where+module Layout (Term(..), Coords, Layout(..), layout, coordinates, Counts(..), counts) where  import qualified Data.Map.Strict as M import Data.Map.Strict (Map)@@ -29,12 +29,12 @@  data Term   = Free String Coords-  | Bound Integer Coords+  | Bound0 Coords+  | Scope Term Coords   | Lambda Strategy Term Coords   | Apply Term Term Coords   | RefInst Integer Term Coords   | Reference Integer Coords-  | Trace String Term Term Coords   deriving (Read, Show, Eq, Ord)  data Layout = Layout Term Integer Integer (Map Integer Coords)@@ -42,33 +42,63 @@  coordinates :: Term -> Coords coordinates (Free      _ xy) = xy-coordinates (Bound     _ xy) = xy+coordinates (Bound0      xy) = xy+coordinates (Scope     _ xy) = xy coordinates (Lambda  _ _ xy) = xy coordinates (Apply   _ _ xy) = xy coordinates (RefInst _ _ xy) = xy coordinates (Reference _ xy) = xy-coordinates (Trace _ _ _ xy) = xy  layout :: G.Term -> G.References -> Layout layout = layout' (0, 0) M.empty  layout' :: Coords -> Map Integer Coords -> G.Term -> G.References -> Layout-layout' xy ps (G.Free v) _ = Layout (Free v xy) 1 1 ps-layout' xy ps (G.Bound v) _ = Layout (Bound v xy) 1 1 ps-layout' (x,y) ps (G.Lambda k t) g = let Layout lt w h ps' = layout' (x, y + 1) ps t g-                                        (px, _) = coordinates lt-                                    in  Layout (Lambda k lt (px, y)) w (h + 1) ps'-layout' (x,y) ps (G.Apply a b) g = let Layout la aw ah psa = layout' (x, y + 1) ps a g-                                       Layout lb bw bh psb = layout' (x + aw + 1, y + 1) psa b g-                                   in  Layout (Apply la lb (x + aw, y)) (1 + aw + bw) (1 + (ah `max` bh)) psb-layout' xy@(x,y) ps (G.Reference p) g = if p `M.member` ps-                                 then Layout (Reference p xy) 1 1 ps-                                 else case M.lookup p g of-                                        Nothing -> error $ "layout': bad pointer: " ++ show p-                                        Just t  -> let Layout lt w h pst = layout' (x, y + 1) ps t g-                                                       (px, py) = coordinates lt-                                                   in Layout (RefInst p lt (px, y)) w (1 + h) (M.insert p (px, py) pst)-layout' (x,y) ps (G.Trace s a b) g =+layout' xy ps (G.Free v) _ =+  Layout (Free v xy) 1 1 ps+layout' xy ps (G.Bound0) _ =+  Layout (Bound0 xy) 1 1 ps+layout' (x, y) ps (G.Scope t) g =+  let Layout lt w h ps' = layout' (x, y + 1) ps t g+      (px, _) = coordinates lt+  in  Layout (Scope lt (px, y)) w (h + 1) ps'+layout' (x,y) ps (G.Lambda k t) g =+  let Layout lt w h ps' = layout' (x, y + 1) ps t g+      (px, _) = coordinates lt+  in  Layout (Lambda k lt (px, y)) w (h + 1) ps'+layout' (x,y) ps (G.Apply a b) g =   let Layout la aw ah psa = layout' (x, y + 1) ps a g       Layout lb bw bh psb = layout' (x + aw + 1, y + 1) psa b g-  in  Layout (Trace s la lb (x + aw, y)) (1 + aw + bw) (1 + (ah `max` bh)) psb+  in  Layout (Apply la lb (x + aw, y)) (1 + aw + bw) (1 + (ah `max` bh)) psb+layout' xy@(x,y) ps (G.Reference p) g =+  if p `M.member` ps+    then Layout (Reference p xy) 1 1 ps+    else case M.lookup p g of+      Nothing -> error $ "layout': bad pointer: " ++ show p+      Just t  ->+        let Layout lt w h pst = layout' (x, y + 1) ps t g+            (px, py) = coordinates lt+        in  Layout (RefInst p lt (px, y)) w (1 + h) (M.insert p (px, py) pst)++data Counts = Counts+  { nFree, nBound0, nScope, nLambda, nApply, nRefInst, nReference :: !Int }++instance Monoid Counts where+  mempty = Counts 0 0 0 0 0 0 0+  mappend c d = Counts+                  { nFree = nFree c + nFree d+                  , nBound0 = nBound0 c + nBound0 d+                  , nScope = nScope c + nScope d+                  , nLambda = nLambda c + nLambda d+                  , nApply = nApply c + nApply d+                  , nRefInst = nRefInst c + nRefInst d+                  , nReference = nReference c + nReference d+                  }++counts :: Term -> Counts+counts (Free _ _) = mempty{ nFree = 1 }+counts (Bound0 _) = mempty{ nBound0 = 1 }+counts (Scope t _) =  let c = counts t in c{ nScope = nScope c + 1 }+counts (Lambda _ t _) = let c = counts t in c{ nLambda = nLambda c + 1 }+counts (Apply a b _) = let c = counts a ; d = counts b in mappend c d+counts (RefInst _ t _) = let c = counts t in c{ nRefInst = nRefInst c + 1 }+counts (Reference _ _) = mempty{ nReference = 1 }
src/Main.hs view
@@ -1,6 +1,6 @@ {-     gulcii -- graphical untyped lambda calculus interpreter-    Copyright (C) 2011, 2013  Claude Heiland-Allen+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen      This program is free software; you can redistribute it and/or modify     it under the terms of the GNU General Public License as published by@@ -19,30 +19,34 @@  module Main (main) where -import Control.Applicative ((<$>), (<*>))-import Control.Concurrent (forkIO, killThread, threadDelay, Chan, newChan, readChan, writeChan)-import Control.Monad (forever, when)+import Control.Applicative ((<$>))+import Control.Concurrent (forkIO, killThread, threadDelay, newChan, readChan, writeChan)+import Control.Monad (forever, when, unless, forM_) import qualified Data.Map.Strict as M-import Data.Map.Strict (Map)+import Data.Maybe (isJust) import Data.IORef (IORef, newIORef, readIORef, writeIORef, atomicModifyIORef) import System.IO (hSetBuffering, BufferMode(LineBuffering), stdout) import System.IO.Error (catchIOError) import System.FilePath ((</>), (<.>))-import Graphics.UI.Gtk hiding (Meta)-import Graphics.Rendering.Cairo+import Graphics.UI.Gtk hiding (Meta, Settings)+import Graphics.Rendering.Cairo hiding (width, height)  import Paths_gulcii (getDataFileName)  import qualified Command as C import qualified Meta as M+import Setting (Settings)+import qualified Setting import qualified Sugar as S import qualified Bruijn as B import qualified Graph as G+import qualified GC as GC+import qualified Reduce as R import qualified Layout as L import qualified Draw as D import qualified Parse as P -data Interpret = Fail | Skip | Define String G.Term | Pure G.Term | Run G.Term | Meta M.Meta+data Interpret = Fail | Skip | Define String G.Term | Pure G.Term | Meta M.Meta   deriving (Read, Show, Eq, Ord)  interpret :: String -> Interpret@@ -56,26 +60,32 @@       case S.desugar sterm of         Just term -> Pure . G.graph . B.bruijn $ term         _ -> Fail-    Just ((C.Execute sterm, []):_) ->-      case S.desugar sterm of-        Just term -> Run . G.graph . B.bruijn $ term-        _ -> Fail     Just ((C.Meta m, []):_) -> Meta m     Just [] -> Skip     _ -> Fail  main :: IO () main = do-  _args <- initGUI+  args <- initGUI+  let (width, height, fullscreen) = case args of+        [w,h,"fullscreen"] -> (read w, read h, True)+        [w,h] -> (read w, read h, False)+        _ -> (1280, 720, False)   envR <- newIORef M.empty   lRef <- newIORef Nothing   evalR <- newIORef Nothing+  settingsR <- newIORef Setting.defaults   outC <- newChan-  _ <- forkIO $ outputter outC   let out = writeChan outC   win <- windowNew   _ <- onDestroy win mainQuit-  windowSetDefaultSize win 1024 720+  windowSetDefaultSize win width height+  when fullscreen $ do+    windowSetGeometryHints win (Nothing `asTypeOf` Just win)+      (Just (width, height)) (Just (width, height)) Nothing Nothing Nothing+    set win [ windowDecorated := False ]+    windowSetKeepAbove win True+    windowMove win 0 0   vb <- vBoxNew False 0   hb <- hPanedNew   tt <- textTagTableNew@@ -115,7 +125,7 @@   _ <- da `on` exposeEvent $ do     dw <- eventWindow     liftIO $ do-      ml <- atomicModifyIORef lRef (\m -> (m, m))+      ml <- atomicModifyIORef lRef (\m -> (Nothing, m))       case ml of         Nothing -> return ()         Just l -> do@@ -124,7 +134,7 @@             D.draw (fromIntegral ww) (fromIntegral hh) l     return True   en <- entryNew-  entrySetWidthChars en 24+  entrySetWidthChars en 25   font <- fontDescriptionFromString "Monospaced 18"   widgetModifyFont tv (Just font)   widgetModifyFont en (Just font)@@ -133,8 +143,13 @@   containerAdd sw tv   al <- alignmentNew 1 0 1 1   set al [ containerChild := da ]-  boxPackStart vb en PackNatural 0-  boxPackStart vb sw PackGrow 0+  if Setting.newsOnTop Setting.defaults+    then do+      boxPackStart vb en PackNatural 0+      boxPackStart vb sw PackGrow 0+    else do+      boxPackStart vb sw PackGrow 0+      boxPackStart vb en PackNatural 0   panedPack1 hb vb False True   panedPack2 hb al True True   set win [ containerChild := hb ]@@ -142,6 +157,7 @@   let scrollDown = do         textViewScrollToMark tv mk 0 Nothing       addText tag txt = do+        newsOnTop <- Setting.newsOnTop <$> readIORef settingsR         start' <- textBufferGetIterAtOffset tb 0         end' <- textBufferGetIterAtOffset tb (-1)         textBufferDelete tb start' end'@@ -149,9 +165,10 @@         start <- textBufferGetIterAtOffset tb 0         end <- textBufferGetIterAtOffset tb (-1)         textBufferApplyTag tb tag start end-        pos <- textBufferGetIterAtOffset tf (-1)+        pos <- textBufferGetIterAtOffset tf (if newsOnTop then 0 else -1)         textBufferInsertRange tf pos start end-        textBufferMoveMark tf mk pos+        pos' <- textBufferGetIterAtOffset tf (if newsOnTop then 0 else -1)+        textBufferMoveMark tf mk pos'   _ <- en `onEntryActivate` do     let exec echo txt =           case interpret txt of@@ -172,21 +189,25 @@               case mtid of                 Nothing -> return ()                 Just tid -> killThread tid-              tid <- forkIO $ evaluator 10000 lRef out envR M.empty term goPure+              tid <- forkIO $ evaluator "gulcii-" 0 settingsR 500000 lRef out envR M.empty term goPure               writeIORef evalR (Just tid)-            Run term -> do+            Meta M.Start -> do               when echo $ do-                addText tagInputRun txt+                addText tagInputMeta txt                 entrySetText en ""-              mtid <- readIORef evalR-              case mtid of-                Nothing -> return ()-                Just tid -> killThread tid-              tid <- forkIO $ evaluator 10000 lRef out envR M.empty term (goRun (postGUIAsync . addText tagOutput))-              writeIORef evalR (Just tid)+              _ <- forkIO $ do+                out "start;"+              return ()+            Meta M.Stop -> do+              when echo $ do+                addText tagInputMeta txt+                entrySetText en ""+              _ <- forkIO $ do+                out "stop;"+              return ()             Meta M.Quit -> do               _ <- forkIO $ do-                out "quit ;"+                out "quit;"                 postGUISync mainQuit               return ()             Meta M.Clear -> do@@ -212,10 +233,45 @@                   mapM_ (exec False) (lines t)                 Left e ->                   addText tagError e+            Meta (M.Get s) -> do+              when echo $ do+                addText tagInputMeta txt+                entrySetText en ""+              addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR+            Meta (M.Set s) -> do+              when echo $ do+                addText tagInputMeta txt+                entrySetText en ""+              atomicModifyIORef settingsR $ (\ss -> (Setting.set s True ss, ()))+              addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR+            Meta (M.UnSet s) -> do+              when echo $ do+                addText tagInputMeta txt+                entrySetText en ""+              atomicModifyIORef settingsR $ (\ss -> (Setting.set s False ss, ()))+              addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR+            Meta (M.Toggle s) -> do+              when echo $ do+                addText tagInputMeta txt+                entrySetText en ""+              atomicModifyIORef settingsR $ (\ss -> (Setting.set s (not (Setting.get s ss)) ss, ()))+              addText tagOutputMeta . ((show s ++ " = ") ++) . show . Setting.get s =<< readIORef settingsR     txt <- entryGetText en     exec True txt     scrollDown-  _ <- flip timeoutAdd 100 $ widgetQueueDraw da >> return True++  _ <- forkIO $ do+        hSetBuffering stdout LineBuffering+        forever $ do+          settings <- readIORef settingsR+          s <- readChan outC+          when (Setting.echoToStdOut settings) $ putStrLn s+          when (Setting.echoToGUI    settings) $ postGUIAsync (addText tagOutput s >> scrollDown)++  _ <- flip timeoutAdd 10 $ do+    ml <- atomicModifyIORef lRef (\m -> (m, m))+    when (isJust ml) $ widgetQueueDraw da+    return True   widgetShowAll win   mainGUI @@ -224,82 +280,59 @@ goPure :: Go goPure refs term = return (term, refs) -goRun :: (String -> IO ()) -> Go-goRun out refs term = do-  out (G.pretty term)-  return (term, refs)--gc :: G.References -> G.Term -> (G.Term, G.References)-gc refs term =-  let keep = reachable refs term M.empty-      (collapse, later) = M.partition (1 ==) keep-  in  (compact refs term, M.fromList [ (k, compact refs (refs M.! k)) | k <- M.keys collapse ] `M.union` M.fromList [ (k, refs M.! k) | k <- M.keys later ])--reachable :: G.References -> G.Term -> Map Integer Integer -> Map Integer Integer-reachable r (G.Lambda _ t) m = reachable r t m-reachable r (G.Apply s t) m = reachable r s (reachable r t m)-reachable r (G.Reference p) m = (if p `M.member` m then id else reachable r (r M.! p)) (M.insertWith (+) p 1 m)-reachable r (G.Trace _ s t) m = reachable r s (reachable r t m)-reachable _ _ m = m--compact :: G.References -> G.Term -> G.Term-compact r (G.Reference p) = r M.! p-compact _ t = t--evaluator :: Int -> IORef (Maybe L.Layout) -> (String -> IO ()) -> IORef G.Definitions -> G.References -> G.Term -> Go -> IO ()-evaluator tick layout out defsR refs term go = do+evaluator :: String -> Int -> IORef Settings -> Int -> IORef (Maybe L.Layout) -> (String -> IO ()) -> IORef G.Definitions -> G.References -> G.Term -> Go -> IO ()+evaluator pngPrefix frame settingsR tick layout out defsR refs term go = do   defs <- readIORef defsR-  let (term1, refs1) = gc refs term+  settings <- readIORef settingsR+  when (Setting.traceEvaluation settings) $ do+    out $ "  " ++ G.pretty term+    unless (M.null refs) $ do+      out "   where"+      forM_ (M.toList refs) $ \(r, t) -> do+        out $ "    #" ++ show r ++ " = " ++ G.pretty t+  let (refs1, term1)+        | Setting.collectGarbage settings = GC.gc refs term+        | otherwise = (refs, term)+      collectedGarbage = term1 /= term || refs1 /= refs+  when (Setting.traceEvaluation settings && collectedGarbage) $ do+    out "$\\to$      {- collect garbage -}"+    out $ "  " ++ G.pretty term1+    unless (M.null refs1) $ do+      out "   where"+      forM_ (M.toList refs1) $ \(r, t) -> do+        out $ "    #" ++ show r ++ " = " ++ G.pretty t   (term0, refs0) <- go refs1 term1-  case G.reduce defs refs0 term0 of-    Nothing -> threadDelay tick >>        evaluator tick layout out defsR refs0 term0 go-    Just (G.Reduced term' refs') ->       evaluator tick layout out defsR refs' term' go-    Just (G.Rebound _var' term' refs') -> evaluator tick layout out defsR refs' term' go-    Just (G.Traced k s term' refs') -> do-      atomicModifyIORef layout $ \_ -> (Just $ L.layout term0 refs0, ())-      case k of-        "wait" -> case evalNatural (dereference refs0 s) of-          Just n -> threadDelay (tick * fromInteger n)-          _ -> return ()-        "noteon" -> case evalList evalNatural (dereference refs0 s) of-          Just msg@[_channel, _note, _velocity] ->-            out $ "noteon " ++ unwords (map show msg) ++ " ;"-          _ -> return ()-        "noteoff" -> case evalList evalNatural (dereference refs0 s) of-          Just msg@[_channel, _note, _velocity] ->-            out $ "noteoff " ++ unwords (map show msg) ++ " ;"-          _ -> return ()-        "program" -> case evalList evalNatural (dereference refs0 s) of-          Just msg@[_channel, _program] ->-            out $ "program " ++ unwords (map show msg) ++ " ;"-          _ -> return ()-        "control" -> case evalList evalNatural (dereference refs0 s) of-          Just msg@[_channel, _control, _value] ->-            out $ "control " ++ unwords (map show msg) ++ " ;"-          _ -> return ()-        _ -> print (k, G.pretty (dereference refs0 s))-      evaluator tick layout out defsR refs' term' go--dereference :: G.References -> G.Term -> G.Term-dereference r (G.Reference p) = dereference r (r M.! p)-dereference r (G.Lambda k t) = G.Lambda k (dereference r t)-dereference r (G.Apply a b) = G.Apply (dereference r a) (dereference r b)-dereference r (G.Trace k a b) = G.Trace k (dereference r a) (dereference r b)-dereference _ t = t--evalNatural :: G.Term -> Maybe Integer-evalNatural (G.Lambda _ (G.Lambda _ (G.Bound 0))) = Just 0-evalNatural (G.Lambda _ (G.Lambda _ (G.Apply (G.Bound 1) t))) = (1 +) `fmap` evalNatural t-evalNatural _ = Nothing--evalList :: (G.Term -> Maybe a) -> G.Term -> Maybe [a]-evalList _ (G.Lambda _ (G.Lambda _ (G.Bound 0))) = Just []-evalList f (G.Lambda _ (G.Lambda _ (G.Apply (G.Apply (G.Bound 1) s) t))) = (:) <$> f s <*> evalList f t-evalList _ _ = Nothing--outputter :: Chan String -> IO ()-outputter out = do-  hSetBuffering stdout LineBuffering-  forever $ do-    s <- readChan out-    putStrLn s+  (l, L.Counts c1 c2 c3 c4 c5 c6 c7) <- atomicModifyIORef layout $ \_ ->+    let l@(L.Layout lt _ _ _) = L.layout term0 refs0+    in  (Just l, (l, L.counts lt))+  when (Setting.saveImages settings) $ do+    withImageSurface FormatRGB24 1920 1080 $ \surface -> do+      renderWith surface $ do+        let g = 23 / 255+        setSourceRGB g g g+        paint+        D.draw 1920 1080 l+      surfaceWriteToPNG surface (pngPrefix ++ show frame ++ ".png")+  when (Setting.emitStatistics settings) $ do+    out $ "statistics " ++ unwords (map show [c1,c2,c3,c4,c5,c6,c7]) ++ ";"+  when (Setting.realTimeDelay settings) $ do+    threadDelay tick+  let tick'+        | Setting.realTimeAcceleration settings = ceiling (fromIntegral tick * 0.97 + 0.03 * 42000 :: Double)+        | otherwise = tick+  case R.reduce defs refs0 term0 of+    Nothing -> do+      when (Setting.traceEvaluation settings) $ do+        out "$\\to$      {- in normal form -}"+        out "  $\\qedsymbol$"+      when (Setting.retryIrreducible settings) $ do+        evaluator pngPrefix (frame + 1) settingsR tick layout out defsR refs0 term0 go+    Just (reason, (refs', term')) -> do+      when (Setting.traceEvaluation settings) $ do+        out $ "$\\to$      {- " ++ (case reason of+            R.Beta -> "beta reduce"+            R.RefInst -> "instantiate reference"+            R.Rebound var -> "definition of \"" ++ var ++ "\""+            R.Extrude -> "scope extrude"+          ) ++ " -}"+      evaluator pngPrefix (frame + 1) settingsR tick' layout out defsR refs' term' go
src/Meta.hs view
@@ -1,6 +1,6 @@ {-     gulcii -- graphical untyped lambda calculus interpreter-    Copyright (C) 2011, 2013  Claude Heiland-Allen+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen      This program is free software; you can redistribute it and/or modify     it under the terms of the GNU General Public License as published by@@ -21,13 +21,21 @@  import Control.Applicative((<|>), (<$), (<*>)) +import Setting (Setting)+import qualified Setting import Parse -data Meta = Quit | Clear | Browse | Load String+data Meta = Start | Stop | Quit | Clear | Browse | Load String | Get Setting | Set Setting | UnSet Setting | Toggle Setting   deriving (Read, Show, Eq, Ord)  parse :: Parser String Meta-parse =  (Quit   <$ sym "quit")+parse =  (Start  <$ sym "start")+     <|> (Stop   <$ sym "stop")+     <|> (Quit   <$ sym "quit")      <|> (Clear  <$ sym "clear")      <|> (Browse <$ sym "browse")      <|> (Load   <$ sym "load" <*> name)+     <|> (Get    <$ sym "get" <*> Setting.parse)+     <|> (Set    <$ sym "set" <*> Setting.parse)+     <|> (UnSet  <$ sym "unset" <*> Setting.parse)+     <|> (Toggle <$ sym "toggle" <*> Setting.parse)
src/Parse.hs view
@@ -1,6 +1,6 @@ {-     gulcii -- graphical untyped lambda calculus interpreter-    Copyright (C) 2011, 2013  Claude Heiland-Allen+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen      This program is free software; you can redistribute it and/or modify     it under the terms of the GNU General Public License as published by@@ -52,7 +52,7 @@ alphanum = alpha ++ digits  symbols :: String-symbols = "\\.!?()[],=~:{}"+symbols = "\\.!?()[],=:"  spaces :: String spaces = " "@@ -68,7 +68,8 @@ tokenize (c:cs)   | c `elem` digits  = let (t,ts) = span (`elem` digits) cs                        in ((c:t):) <$> tokenize ts-  | c `elem` lowers  = let (t,ts) = span (`elem` alphanum) cs+  | c `elem` uppers+  ||c `elem` lowers  = let (t,ts) = span (`elem` alphanum) cs                        in ((c:t):) <$> tokenize ts   | c `elem` symbols = ([c]:) <$> tokenize cs   | c `elem` spaces  = tokenize cs
+ src/Reduce.hs view
@@ -0,0 +1,142 @@+{-+    gulcii -- graphical untyped lambda calculus interpreter+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen++    This program is free software; you can redistribute it and/or modify+    it under the terms of the GNU General Public License as published by+    the Free Software Foundation; either version 2 of the License, or+    (at your option) any later version.++    This program is distributed in the hope that it will be useful,+    but WITHOUT ANY WARRANTY; without even the implied warranty of+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the+    GNU General Public License for more details.++    You should have received a copy of the GNU General Public License along+    with this program; if not, write to the Free Software Foundation, Inc.,+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.+-}++module Reduce (Reduce(..), Reduction, reduce) where++import Prelude hiding (replicate)++import qualified Data.Map.Strict as Map++import Evaluation (Strategy(..))+import Graph++{-+Reduce a graph one step, returning Nothing if it is irreducible.+-}++data Reduce = Beta | RefInst | Rebound String | Extrude+  deriving (Read, Show, Eq, Ord)++type Reduction = (Reduce, (References, Term))++mapTerm :: (Term -> Term) -> Reduction -> Reduction+mapTerm f = fmap (fmap f)+++reduce :: Definitions -> References -> Term -> Maybe Reduction+reduce defs refs term =+  case reduce' False defs refs term of+    Nothing -> reduce' True defs refs term+    r -> r+++reduce' :: Bool -> Definitions -> References -> Term -> Maybe Reduction++reduce' _ defs refs (Free var)+  = (,) (Rebound var) `fmap` (,) refs `fmap` Map.lookup var defs++reduce' _ _    _    (Bound0)+  = Nothing++reduce' _ _    refs (Scope (Lambda strat term))+  = Just (Extrude, (refs, Lambda strat (lifting refs 1 term)))++reduce' f defs refs (Scope t@(Reference _))+  = case dereference refs t of+      l@(Lambda _ _) ->+        Just (RefInst, (refs, Scope l))+      _ -> mapTerm Scope `fmap` reduce' f defs refs t++reduce' _ _    refs (Scope (Apply a b))+  = Just (Extrude, (refs, Apply (Scope a) (Scope b)))++reduce' f defs refs (Scope term)+  = mapTerm Scope `fmap` reduce' f defs refs term++reduce' f defs refs (Lambda strat term)+  = mapTerm (Lambda strat) `fmap` reduce' f defs refs term++reduce' f defs refs term@(Reference ref)+  = case Map.lookup ref refs of+      Just refTerm ->+        case reduce' f defs refs refTerm of+          Just (reason, (refs', term')) ->+            Just (reason, (Map.insert ref term' refs', term))+          Nothing ->+            Just (RefInst, (refs, refTerm))+      Nothing -> Nothing -- error "reference not found"++reduce' _ _    refs (Apply (Lambda Copy a) b)+  = Just (Beta, (refs, beta refs a b))++reduce' f defs refs (Apply l@(Lambda Strict a) b)+  = case reduce' f defs refs b of+      Just (reason, (refs', b')) -> Just (reason, (refs', Apply l b'))+      Nothing -> Just (Beta, (refs, beta refs a b))++reduce' _ _    refs (Apply (Lambda Lazy a) b)+  = let r = next refs+        refs' = Map.insert r b refs+    in  Just (Beta, ( refs'+                    , beta refs' a (Reference r) ))++reduce' f defs refs (Apply a b)+  = case (a, dereference refs a) of+      (Reference _, l@(Lambda _ _)) -> Just (RefInst, (refs, Apply l b))+      _ ->+       case reduce' f defs refs a of+          Just (reason, (refs', a')) ->+            Just (reason, (refs', Apply a' b))+          Nothing+            | f -> mapTerm (Apply a) `fmap` reduce' f defs refs b+            | otherwise -> Nothing+++beta :: References -> Term -> Term -> Term+beta refs l v = substitute refs l v 0++substitute :: References -> Term -> Term -> Integer -> Term+substitute _    Bound0 s 0 = s+substitute _    Bound0 _ _ = Bound0+substitute _    (Scope t) _ 0 = t+substitute refs (Scope t) s i = Scope (substitute refs t s (i - 1))+substitute refs (Lambda k t) s i = Lambda k (substitute refs t s (i + 1))+substitute refs (Apply a b) s i = Apply (substitute refs a s i) (substitute refs b s i)+substitute _    t@(Free _) _ _ = t+substitute refs (Reference r) s i = substitute refs (refs Map.! r) s i++lifting :: References -> Integer -> Term -> Term+lifting _    0 t = Scope t+lifting _    _ s@(Free _) = s+lifting _    _ Bound0 = Bound0+lifting refs i (Scope t) = Scope (lifting refs (i - 1) t)+lifting refs i (Lambda k t) = Lambda k (lifting refs (i + 1) t)+lifting refs i (Apply a b) = Apply (lifting refs i a) (lifting refs i b)+lifting refs i (Reference r) = lifting refs i (refs Map.! r)+++dereference :: References -> Term -> Term+dereference refs (Reference r) = dereference refs (refs Map.! r)+dereference _ t = t+++next :: References -> Integer+next refs = case Map.maxViewWithKey refs of+  Nothing        -> 0+  Just ((k,_),_) -> k + 1
+ src/Setting.hs view
@@ -0,0 +1,97 @@+{-+    gulcii -- graphical untyped lambda calculus interpreter+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen++    This program is free software; you can redistribute it and/or modify+    it under the terms of the GNU General Public License as published by+    the Free Software Foundation; either version 2 of the License, or+    (at your option) any later version.++    This program is distributed in the hope that it will be useful,+    but WITHOUT ANY WARRANTY; without even the implied warranty of+    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the+    GNU General Public License for more details.++    You should have received a copy of the GNU General Public License along+    with this program; if not, write to the Free Software Foundation, Inc.,+    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.+-}++module Setting (Setting(..), parse, Settings(..), get, set, defaults) where++import Control.Applicative ((<$))+import Data.Foldable (asum)++import Parse++data Setting+  = TraceEvaluation+  | CollectGarbage+  | RealTimeDelay+  | RealTimeAcceleration+  | RetryIrreducible+  | EmitStatistics+  | EmitRebindings+  | EchoToStdOut+  | EchoToGUI+  | SaveImages+  | NewsOnTop+  deriving (Eq, Ord, Enum, Bounded, Read, Show)++parse :: Parser String Setting+parse = asum [ s <$ sym (show s) | s <- [minBound .. maxBound :: Setting] ]++data Settings = Settings+  { traceEvaluation :: Bool+  , collectGarbage :: Bool+  , realTimeDelay :: Bool+  , realTimeAcceleration :: Bool+  , retryIrreducible :: Bool+  , emitStatistics :: Bool+  , emitRebindings :: Bool+  , echoToStdOut :: Bool+  , echoToGUI :: Bool+  , saveImages :: Bool+  , newsOnTop :: Bool+  }++get :: Setting -> Settings -> Bool+get TraceEvaluation = traceEvaluation+get CollectGarbage = collectGarbage+get RealTimeDelay = realTimeDelay+get RealTimeAcceleration = realTimeAcceleration+get RetryIrreducible = retryIrreducible+get EmitStatistics = emitStatistics+get EmitRebindings = emitRebindings+get EchoToStdOut = echoToStdOut+get EchoToGUI = echoToGUI+get SaveImages = saveImages+get NewsOnTop = newsOnTop++set :: Setting -> Bool -> Settings -> Settings+set TraceEvaluation b s = s{ traceEvaluation = b }+set CollectGarbage b s = s{ collectGarbage = b }+set RealTimeDelay b s = s{ realTimeDelay = b }+set RealTimeAcceleration b s = s{ realTimeAcceleration = b }+set RetryIrreducible b s = s{ retryIrreducible = b }+set EmitStatistics b s = s{ emitStatistics = b }+set EmitRebindings b s = s{ emitRebindings = b }+set EchoToStdOut b s = s{ echoToStdOut = b }+set EchoToGUI b s = s{ echoToGUI = b }+set SaveImages b s = s{ saveImages = b }+set NewsOnTop b s = s{ newsOnTop = b }++defaults :: Settings+defaults = Settings+  { traceEvaluation = False+  , collectGarbage = True+  , realTimeDelay = True+  , realTimeAcceleration = True+  , retryIrreducible = True+  , emitStatistics = True+  , emitRebindings = True+  , echoToStdOut = True+  , echoToGUI = False+  , saveImages = False+  , newsOnTop = True+  }
src/Sugar.hs view
@@ -1,6 +1,6 @@ {-     gulcii -- graphical untyped lambda calculus interpreter-    Copyright (C) 2011, 2013  Claude Heiland-Allen+    Copyright (C) 2011, 2013, 2017  Claude Heiland-Allen      This program is free software; you can redistribute it and/or modify     it under the terms of the GNU General Public License as published by@@ -31,7 +31,7 @@  module Sugar(Term(..), parse, desugar) where -import Control.Applicative(Applicative, Alternative, (<|>), (<$>), (<$), (<*>), (<*), some, liftA2)+import Control.Applicative((<|>), (<$>), (<$), (<*>), (<*), some, liftA2) import Data.List ((\\))  import Parse@@ -45,7 +45,6 @@   | Group Term   | Natural Integer   | List [Term]-  | Trace String Term Term   deriving (Read, Show, Eq, Ord)  parse :: Parser String Term@@ -57,7 +56,6 @@       <|> (Variable <$> name)       <|> (Natural <$> integer)       <|> (List <$ sym "[" <*> manySep (sym ",") parse <* sym "]")-      <|> (Trace <$ sym "{" <*> name <* sym ":" <*> parse <* sym "}" <*> parse)  strategy :: Parser String Strategy strategy =  (Strict <$ sym "!") <|> (Lazy <$ sym ".") <|> (Copy <$ sym "?")@@ -118,7 +116,6 @@       let (c:n:_) = (variables \\ U.freeVariablesIn t') \\ U.freeVariablesIn ts'       in Just $ lam c (lam n (U.Apply (U.Apply (U.Variable c) t') ts'))     _ -> Nothing-desugar (Trace k s t) = U.Trace k <$> desugar s <*> desugar t  lam :: String -> U.Term -> U.Term lam = U.Lambda Lazy