maxsharing (empty) → 1.0

raw patch · 8 files changed

+917/−0 lines, 8 filesdep +HaLeXdep +IndentParserdep +basebuild-type:Customsetup-changed

Dependencies added: HaLeX, IndentParser, base, base-unicode-symbols, boxes, containers, containers-unicode-symbols, mtl, parsec, process, uuagc, uuagc-cabal

Files

• LICENSE +10/−0
• Lambda.ag +616/−0
• MaxSharing.hs +91/−0
• Parser.hs +72/−0
• Setup.hs +5/−0
• Spanning.hs +81/−0
• maxsharing.cabal +40/−0
• uuagc_options +2/−0

@@ -0,0 +1,10 @@+Copyright (c) 2010, Jan Rochel+All rights reserved.++Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:++* Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.+* Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.+* Neither the name of the University of Utrecht nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,616 @@+-- Here: λ-term = λ-letrec-term+-- The relevant attributes: scoped and dfa+module {Lambda} {Λ (..), V, Params (..), LetPrefixLengths (..), LambdaDfa, State, Symbol (..),+                 showNameless, showTR, showTRNameless, combinations, synthesise,+                 scoped_Syn_R, deBruijn_Syn_R, dfa_Syn_R, readback_Syn_R, proof_Syn_R, unscoped_Syn_R}+{+import Data.Set (Set)+import qualified Data.Set as Set+import Data.Map (Map)+import qualified Data.Map as Map+import Data.Monoid.Unicode+import Prelude.Unicode+import Data.Char (toLower)+import Language.HaLex.Dfa (Dfa (..))+import Text.PrettyPrint.Boxes+import Data.Functor+import Data.Graph+import Data.Tree (flatten)+import Data.List ((\\), delete, partition)+import Data.Either (partitionEithers)+}++{type V = String} -- variables++data Λ -- multi-purpose type for λ-terms+	| V  var ∷ V                  -- variable+	| A  fun ∷ Λ  arg ∷ Λ        -- application+	| Λ  var ∷ V  body ∷ Λ       -- lambda+	| S  var ∷ V  body ∷ Λ       -- abdmal / scope delimiter+	| I  var ∷ V  body ∷ Λ       -- indirection node+	| L  binds ∷ Binds  body ∷ Λ -- let binding++type Binds = [Bind]+type Bind  = (V,Λ)++data R | R  body ∷ Λ -- a root for λ-terms; for supplying initial values of inherited attributes++{ -- `execution' of the attribute grammar+synthesise params t = wrap_R (sem_R $ R t) (Inh_R params False)+}++-- pretty printing++attr R Λ Bind Binds+	inh ppNameless ∷ Bool++attr R Λ Bind+	syn pp ∷ Box++attr R Λ+	syn ppTR ∷ Box -- pretty printing using term rewriting syntax++attr Binds+	syn pps ∷ {[Box]}++attr Λ+	syn isComposed ∷ Bool+	syn isApp ∷ Bool++sem Λ+	| A Λ I L lhs.isComposed = True+	| V S lhs.isComposed = False+	| A lhs.isApp = True+	| V Λ S I L lhs.isApp = False++{+maybeWrap ∷ Bool → Box → Box+maybeWrap isComposed box = if isComposed then char '(' <> box <#> char ')' else box+}++sem Λ+	| A loc.pp = @loc.funPP <#> nullBox <+> @loc.argPP+	    loc.funPP = if @fun.isApp then @fun.pp else maybeWrap @fun.isComposed @fun.pp+	    loc.argPP = maybeWrap @arg.isComposed @arg.pp+	| Λ loc.pp = text ("λ" ⧺ (if @lhs.ppNameless then "" else @var) ⧺ ".") <+> @body.pp+	| S loc.pp = if @lhs.ppNameless+	    		then text "S(" <> maybeWrap @body.isComposed @body.pp <> char ')'+	    		else text ("/" ⧺ @var ⧺ ".") <+> @body.pp+	| I loc.pp = text ("|" ⧺ @var ⧺ ".") <+> @body.pp+	| V loc.pp = if @lhs.ppNameless ∧ @loc.varType == Λ_Bound then char '0' else text @var+	| L loc.pp = let+				binds = vcat left [f <+> char '=' <+> e | (f,e) <- zip fs' @binds.pps]+				width = maximum $ map cols fs+				fs  = map text @binds.binders+				fs' = map (alignHoriz left width) fs+			in text "let" <+> binds // (text "in" <+> @body.pp)++sem Binds+	| Nil  loc.pps = []+	| Cons loc.pps = @hd.pp : @tl.pps++{+app ∷ String → [Box] → Box+app f xs = text f <> char '(' <> punctuateH bottom (text ", ") xs <> char ')'+}++sem Λ+	| A loc.ppTR = app "@" [@fun.ppTR, @arg.ppTR]+	| Λ loc.ppTR = app (if @lhs.ppNameless then "L" else "L" ⧺ @var) [@body.ppTR]+	| S loc.ppTR = app (if @lhs.ppNameless then "S" else "/" ⧺ @var ⧺ ".") [@body.ppTR]+	| I loc.ppTR = app ("|" ⧺ @var) [@body.ppTR]+	| V loc.ppTR = if @lhs.ppNameless ∧ @loc.varType == Λ_Bound then char '0' else text @var+	| L loc.ppTR = error "term rewriting syntax currently only supported for let-bindings"++{+(<#>) ∷ Box → Box → Box+(<#>) l r = hcat bottom [l,r]++instance Show Λ where+	show = render ∘ pp False++showNameless ∷ Λ → String+showNameless = render ∘ pp True++showTRNameless ∷ Λ → String+showTRNameless = render ∘ ppTR True++showTR ∷ Λ → String+showTR = render ∘ ppTR False++pp ∷ Bool → Λ → Box+pp nameless t = pp_Syn_R $ wrap_R (sem_R $ R t) (Inh_R undefined nameless)++ppTR ∷ Bool → Λ → Box+ppTR nameless t = ppTR_Syn_R $ wrap_R (sem_R $ R t) (Inh_R undefined nameless)++combinations ∷ [a] → [[a]]+combinations xs = [[x] | x ← xs] ⧺ [x : c | c ← combinations xs, x ← xs]+}++-- Generic attributes ---------------------------------------------------------++{+data Params = Params -- various parameters to customise the attribute grammar by+	{letPrefixLengths ∷ LetPrefixLengths, -- which abstraction prefixes to use in the let-rule+	 withVarBacklinks,      -- whether to use backlinks for variable vertices+	 withSBacklinks,        -- whether to use backlinks for scope delimiters+	 withSharedVars ∷ Bool} -- whether variables are shared implicitely+	-- TODO: del-rule+}++attr R Λ Bind Binds+	inh params ∷ Params++-- binders++attr Bind+	syn binder ∷ V++attr Binds+	syn binders ∷ {[V]}++sem Bind | Tuple loc.binder = @x1++sem Binds+	| Nil lhs.binders = []+	| Cons lhs.binders = @hd.binder : @tl.binders+++{data VarType = Free | LetBound | Λ_Bound deriving (Eq, Show)}++attr Λ Bind Binds+	inh varTypeEnv ∷ {Map V VarType}++sem R | R body.varTypeEnv = ∅++sem Λ+	| Λ body.varTypeEnv  = Map.insert @var Λ_Bound @lhs.varTypeEnv+	| L loc.varTypeEnv   = @lhs.varTypeEnv ⊕ Map.fromList [(b, LetBound) | b <- @binds.binders]+	    binds.varTypeEnv = @loc.varTypeEnv+	    body.varTypeEnv  = @loc.varTypeEnv+	| V loc.varType = Map.findWithDefault Free @var @lhs.varTypeEnv++-- 'unscoped' synthesises an S-less version of the term++attr R+	syn unscoped ∷ Λ+attr Λ Bind Binds+	syn unscoped ∷ self++sem Λ | S lhs.unscoped = @body.unscoped++-- The set of free/used variables ---------------------------------------------++attr Λ Bind -- the sets contain both recursion and abstraction variables+	syn fv ∷ {Set V} -- the set of free variables+	syn uv ∷ {Set V} -- the set of used variables is very similar to the set of free variables+	                  -- but it only takes into account function bindings that are actually used++sem Λ+	| V loc.fv = Set.singleton @var -- O(1)+	    loc.uv = Set.singleton @var -- O(1)+	| Λ loc.fv = Set.delete @var @body.fv -- O(log(n))+	    loc.uv = Set.delete @var @body.uv -- O(log(n))+	| A loc.fv = @fun.fv ⊕ @arg.fv -- O(n)+	    loc.uv = @fun.uv ⊕ @arg.uv -- O(n)+	| L loc.deleteBinders = flip (foldr Set.delete) @binds.binders -- O(n)+	    loc.fv = @loc.deleteBinders $ Set.unions $ @body.fv : @binds.fvs -- O(n)+	    loc.uv = @loc.deleteBinders $ Set.unions $ @body.uv : -- O(n)+	    		[Map.findWithDefault (∅) v @loc.uvsTC | v <- Set.elems @body.uv] -- O(n) (if intersection is used)+	    -- transitive closure of the local call graph; O(n^2) but O(n) possible if SCCs are used instead+	    loc.uvsTC = transClos $ Map.fromList $ zip @binds.binders @binds.uvs+	| S I loc.fv = undefined+	      loc.uv = undefined++{+-- TODO: Use Tarjan's algorithm instead (http://hackage.haskell.org/package/GraphSCC)+-- since SCCs is sufficient for our purposes.+transClos ∷ Ord a ⇒ Map a (Set a) → Map a (Set a)+transClos = converge $ \m → fmap (\ys → Set.unions $ ys : [Map.findWithDefault (∅) y m | y ← Set.elems ys]) m++-- compute fixpoint of a function by iterating it until it becomes monotonous+converge ∷ Eq a ⇒ (a → a) → a → a+converge step = fixPoint ∘ iterate step where+	fixPoint (x:y:zs) = if x == y then x else fixPoint (y:zs)+}++attr Binds+	syn fvs ∷ {[Set V]}+	syn uvs ∷ {[Set V]}++sem Binds+	| Nil loc.fvs = []+	      loc.uvs = []+	| Cons loc.fvs = @hd.fv : @tl.fvs+	       loc.uvs = @hd.uv : @tl.uvs++-- used functions / garbage collection++attr Λ Binds Bind+	inh usedBinds ∷ {Set V}++sem R | R body.usedBinds = ∅++sem Λ | L loc.usedBinds = @loc.uv `Set.intersection` Set.fromList @binds.binders++attr Bind+	syn alive ∷ Bool++sem Bind | Tuple loc.alive = @loc.binder `Set.member` @lhs.usedBinds++attr R+	syn garbageFree ∷ Λ+	syn hasGarbage ∷ Bool++attr Λ Binds Bind+	syn garbageFree ∷ self+	syn hasGarbage use {∨} {False} ∷ Bool++sem Binds | Cons+	lhs.garbageFree = if @hd.alive then @hd.garbageFree : @tl.garbageFree else @tl.garbageFree+	lhs.hasGarbage = not @hd.alive ∨ @tl.hasGarbage++-- The set of required variables (TODO: currently requires unique naming) ----++attr Λ Bind Binds+	inh rvEnv ∷ {Map V (Set V)} -- rv-sets of functions defined further above+	syn rv use {⊕} {∅} ∷ {Set V} -- O(n)++attr Binds+	syn rvs ∷ {[Set V]}++sem Binds+	| Nil lhs.rvs = []+	| Cons lhs.rvs = @hd.rv : @tl.rvs++sem R | R body.rvEnv = ∅++sem Λ+	| Λ body.rvEnv = Map.delete @var @lhs.rvEnv -- O(log(n))+	    loc.rv = Set.delete @var @body.rv -- O(log(n))+	| S loc.rv = @body.rv+	| V loc.rv = Map.findWithDefault (Set.singleton @var) @var @lhs.rvEnv -- O(log(n))+	| A loc.rv = @fun.rv ⊕ @arg.rv -- O(n)+	| L loc.rvEnv = @lhs.rvEnv ⊕ fmap (substVars @lhs.rvEnv) @loc.uvsTC -- TODO: O(n) when using SCCs?+	    loc.rv = @loc.deleteBinders @body.rv -- O(n)+	| I loc.rv = undefined++{+substVars ∷ Map V (Set V) → Set V → Set V+substVars rvEnv vs = Set.unions [Map.findWithDefault (Set.singleton v) v rvEnv | v ← Set.elems vs]+}++-- Scoped representation of a λ-term with de Bruijn indexes ------------------+-- TODO: currently only works (properly) for non-letrec λ-terms++attr R+	syn deBruijn ∷ Λ++attr Λ Bind Binds+	inh scope ∷ {[V]} -- all bound variables (extended scope / prefix with lazy scope-closure)+	syn deBruijn ∷ self++sem R | R body.scope = []++sem Λ+	| V lhs.deBruijn = if @loc.varType == LetBound+	                     then V @var+	                     else churnr (S <$> takeWhile (/= @var) @lhs.scope) (V @var)+	| Λ body.scope = @var : @lhs.scope++-- Scoped representation of λ-terms ------------------------------------------++attr R+	syn scoped ∷ Λ++data LetPrefixLengths -- abstraction prefixes chosen for the bindings of a binding group+	| MaxPrefix -- maximal lengths, i.e. the inherited prefix is used for all bindings+	| MinPrefix -- minimal lengths, resulting in unshared scope delimiters+	| MaxEagPre -- maximal lengths that still guarantee eager scope-closure+	| MaxEagTmp -- internal policy used my MaxEagPre that determines the prefixes of functions at all use sites++{+instance Show LetPrefixLengths where+	show lpl = case lpl of+		MaxPrefix → "maximal prefix lengths"+		MinPrefix → "minimal prefix lengths"+		MaxEagPre → "maximal prefix lengths while maintaining eager scope-closure"+}++-- {type Prefix = [V]}+{type Prefix = [(V, Set V)]}++attr Λ Bind Binds+	inh mkPrefix ∷ {LetPrefixLengths -> Prefix}+	syn maxEagTmp use {unionMaxPrefixes} {∅} ∷ {Map V Int} -- O(n)+	syn scoped ∷ self++sem R | R body.mkPrefix = const [("*", (∅))]++{+-- Apply a list of functions to a value+churnr ∷ [a → a] → a → a+churnr = foldr (.) id++shortenPrefix ∷ Prefix → Set V → Prefix+shortenPrefix ps fv = dropWhile noFv ps where+	noFv ("*",fs) = False+	noFv (v,fs) = Set.null $ fv `Set.intersection` Set.insert v fs++-- Add a function symbol to a prefix at the given position+enrichPrefix ∷ (V, Int) → Prefix → Prefix+enrichPrefix (f,l) ps = updateAt (length ps - l) (\(x,fs) → (x, Set.insert f fs)) ps++updateAt ∷ Int → (a → a) → [a] → [a]+updateAt i f xs = let (ls,r:rs) = splitAt i xs in ls ⧺ f r : rs++unionMaxPrefixes ∷ Map V Int → Map V Int → Map V Int+unionMaxPrefixes = Map.unionWith min+}++sem Λ Bind+	| * loc.prefix       = @loc.mkPrefix $ letPrefixLengths @lhs.params+	    loc.parentPrefix = @lhs.mkPrefix $ letPrefixLengths @lhs.params++sem Λ+	| * loc.mkPrefix = \strat -> case strat of+							MaxEagTmp -> shortenPrefix (@lhs.mkPrefix MaxEagTmp) @loc.rv+							strat -> shortenPrefix (@lhs.mkPrefix strat) @loc.fv+	| Λ body.mkPrefix = ((@var, (∅)) :) ∘ @loc.mkPrefix+	| L loc.mkPrefixLengths = \strat -> case strat of+	    				MinPrefix -> map (length ∘ shortenPrefix @loc.prefix) @binds.rvs+	    				MaxPrefix -> replicate (length @binds.binders) (length $ @loc.mkPrefix MaxPrefix)+	    				MaxEagPre -> [Map.findWithDefault 0 f @loc.maxEagTmp | f <- @binds.binders]+	    				MaxEagTmp -> replicate (length @binds.binders) (length $ @loc.mkPrefix MaxPrefix)+	    loc.newPrefix = \strat -> case strat of+	    				MaxEagTmp -> @loc.mkPrefix MaxPrefix+	    				strat -> foldr enrichPrefix @loc.prefix $ zip @binds.binders (@loc.mkPrefixLengths strat)+	    binds.mkPrefix = @loc.newPrefix+	    body.mkPrefix = @loc.newPrefix++attr Binds+	inh mkPrefixLengths ∷ {LetPrefixLengths → [Int]}++sem Binds | Cons+	hd.mkPrefix = \strat -> drop (length (@lhs.mkPrefix strat) - head (@lhs.mkPrefixLengths strat)) (@lhs.mkPrefix strat)+	tl.mkPrefixLengths = tail ∘ @lhs.mkPrefixLengths++sem Bind | Tuple+	loc.mkPrefix = @lhs.mkPrefix++sem Λ+	| V lhs.maxEagTmp = if @loc.varType == LetBound then Map.singleton @var (length $ @lhs.mkPrefix MaxEagTmp) else (∅)+	| Λ lhs.maxEagTmp = Map.delete @var @body.maxEagTmp+	| L lhs.maxEagTmp = foldr Map.delete @loc.maxEagTmp @binds.binders -- O(n)+	    loc.maxEagTmp = @body.maxEagTmp `unionMaxPrefixes` @binds.maxEagTmp++sem Λ+	| Λ A V L loc.scoped = churnr [S x | x <- @loc.killVars] @loc.scoped'+	| * loc.killVars = take (length @loc.parentPrefix - length @loc.prefix) (map fst @loc.parentPrefix)+  | Λ loc.scoped' = Λ @var @body.scoped+  | A loc.scoped' = A @fun.scoped @arg.scoped+	| V loc.scoped' = V @var+  | L loc.scoped' = L @binds.scoped @body.scoped+	| S I loc.scoped' = undefined++sem Bind | Tuple lhs.scoped = (@loc.binder, @x2.scoped)++sem Binds+	| Nil lhs.scoped = []+	| Cons lhs.scoped = @hd.scoped : @tl.scoped++-- DFA generation ------------------------------------------------------------++{+type LambdaDfa = Dfa State Symbol++type State = Int+dummyState, freevarState ∷ State+freevarState = 0+dummyState   = -1 -- this is where `non-existing' transitions point+nextState    = succ+firstState   = 1++data Symbol = S_Λ | S_A0 | S_A1 | S_V | S_S0 | S_S1 | S_F V | S_I deriving (Eq, Ord)++instance Show Symbol where+	show l = case l of+		S_Λ   → "L"+		S_A0  → "A0"+		S_A1  → "A1"+		S_V   → "0"+		S_S0  → "S0"+		S_S1  → "S1"+		S_F v → v+		S_I   → "I"++type Transition = (State,Symbol,State)++data VarOcc = LamOcc State State | LetOcc State++-- | Transforms a λ-DFA by contracting all I-connected components (ICCs).+-- If an ICC is cyclic it becomes a blackhole (no outgoing edges), otherwise it vanishes.+contractI ∷ LambdaDfa → LambdaDfa+contractI (Dfa symbols states start accept trans) =+	Dfa symbols states' start' (delete dummyState states') trans' where++		states' = (states \\ concatMap fst iTrees) \\ concatMap tail blackholes+		start' = Map.findWithDefault start start combinedMap+		trans' state symbol = if state `Map.member` blackholeMap+			then dummyState+			else let target = trans state symbol in Map.findWithDefault target target combinedMap++		combinedMap = blackholeMap ⊕ indirectionMap++		blackholeMap ∷ Map State State+		blackholeMap = Map.fromList [(s, head ss) | ss ← blackholes, s ← ss]++		indirectionMap ∷ Map State State+		indirectionMap = Map.fromList [(s, exit) | (ss, exit) ← iTrees, s ← ss]++		blackholes ∷ [[State]] -- ^ I-cycles+		iTrees ∷ [([State], State)] -- ^ non-cyclic I-connected components together with the non-I successor+		(blackholes, iTrees) = partitionEithers $ map (blackholeOrNot ∘ flatten) (components iGraph) where++			-- graph containing only the I-vertices of the DFA+			iGraph = buildG (0, maximum states) iEdges where+				iEdges = [(source,target) | source ← states, let target = trans source S_I, target ≢ dummyState]++			blackholeOrNot states = case partition isI states of+				(ss, [exit]) → Right (ss, exit)+				(ss, [    ]) → Left ss -- blackhole+				anythingElse → error "Infringement!1" -- cannot occur since I-vertices have only one exit+				where isI s = trans s S_I ≢ dummyState+++mkDfa ∷ State → [Transition] → LambdaDfa+mkDfa start transitions = contractI $ Dfa symbols (dummyState : states) start states trans where+	states = nub $ concat [[source,target] | (source,label,target) ← transitions]+	symbols = S_Λ : S_A0 : S_A1 : S_V : S_S0 : S_S1 : S_I : nub [S_F v | (from, S_F v, to) ← transitions]+	trans state symbol = Map.findWithDefault dummyState (state,symbol) mapping where+		mapping = Map.fromList $ map mkTrans transitions+		mkTrans (source, label, target) = ((source, label), target)++	nub ∷ Ord a ⇒ [a] → [a]+	nub = Set.elems ∘ Set.fromList+}++attr R+	syn dfa ∷ {LambdaDfa}++sem R | R lhs.dfa = mkDfa @body.node @body.transitions+          body.freshState = firstState+          body.dfaEnv = ∅+++{nextUnique n = (nextState n, n)}++attr Λ Bind Binds+	inh dfaEnv ∷ {Map V VarOcc} -- environment for the backlinks+	chn freshState ∷ State+	syn transitions ∷ {[Transition]}++attr Λ Bind+	syn node ∷ State++attr Binds+	syn nodes ∷ {[State]}++sem Binds+	| Nil  lhs.transitions = []+	       lhs.nodes = []+	| Cons lhs.transitions = @hd.transitions ⧺ @tl.transitions+	       lhs.nodes = @hd.node : @tl.nodes++sem Bind | Tuple+	lhs.transitions = (@loc.node, S_I, @x2.node) : @x2.transitions+	loc.node ∷ uniqueref freshState++sem Λ+	| Λ loc.node ∷ uniqueref freshState+	    loc.occ  ∷ uniqueref freshState+	    body.dfaEnv = Map.insert @var (LamOcc @loc.occ @loc.node) @lhs.dfaEnv+	    lhs.transitions = (@loc.node, S_Λ, @body.node) : @body.transitions+	| A loc.node ∷ uniqueref freshState+	    lhs.transitions = (@loc.node, S_A0, @fun.node) : (@loc.node, S_A1, @arg.node) : @fun.transitions ⧺ @arg.transitions+	| L lhs.node = @body.node+	    loc.newDfaEnv = @lhs.dfaEnv ⊕ Map.fromList [(v, LetOcc i) | (v,i) <- zip @binds.binders @binds.nodes]+	    binds.dfaEnv = @loc.newDfaEnv+	    body.dfaEnv = @loc.newDfaEnv+	    lhs.transitions = @body.transitions ⧺ @binds.transitions+	| V loc.dfaLookup = Map.lookup @var @lhs.dfaEnv+	    lhs.transitions = case @loc.dfaLookup of+	    			Nothing -> [(@loc.node, S_F @var, freevarState)] -- free variable+	    			Just (LamOcc occ abs) -> [(@loc.node, S_V, if withVarBacklinks @lhs.params then abs else freevarState)]+	    			Just (LetOcc i) -> []+		  loc.node = case @loc.dfaLookup of+		  			Nothing -> @loc.maybeNode -- free variable. TODO: take into account withSharedVars+		  			Just (LamOcc occ abs) -> if withSharedVars @lhs.params then occ else @loc.maybeNode+		  			Just (LetOcc i) -> i+		  loc.maybeNode ∷ uniqueref freshState+	| S loc.abs = case Map.lookup @var @lhs.dfaEnv of+						Just (LamOcc occ abs) -> abs+						_ -> error $ "delimiter couldn't find his abstraction: " ⧺ @var+	    lhs.transitions = (@loc.node, S_S0, @body.node) : (@loc.node, S_S1, @loc.abs) : @body.transitions+	    loc.node ∷ uniqueref freshState++-- readback ------------------------------------------------------------++attr R+	syn readback ∷ Λ++sem R+	| R lhs.readback = case head @body.bindings of+					[] -> @body.readback+					bs -> L bs @body.readback++attr Λ+	syn readback ∷ Λ+	syn bindings ∷ {[Binds]}++sem Λ+	| Λ lhs.bindings = tail @body.bindings+      lhs.readback = Λ @var $ @loc.addL @body.readback+      loc.addL = case head @body.bindings of+      				[] -> id+      				bs -> L bs+  | S lhs.bindings = [] : @body.bindings+      lhs.readback = S @var @body.readback+  | A lhs.bindings = zipWith (⧺) @fun.bindings @arg.bindings+      lhs.readback = A @fun.readback @arg.readback+  | I lhs.bindings = let (bs:bss) = @body.bindings in ((@var,@body.readback) : bs) : bss+      lhs.readback = V @var+  | V lhs.bindings = repeat []+      lhs.readback = V @var+  | L lhs.bindings = @loc.readbackError+      lhs.readback = @loc.readbackError+      loc.readbackError = error "readback is only defined for λ-spanning-trees"++-- proof generation ----------------------------------------------------++{+infer ∷ String → [Box] → Box → Box+infer step assumptions conclusion = vcat left [asBox, line, conclusion] where+	line = text (replicate (max (cols asBox) (cols conclusion)) '-') <+> text step+	asBox = hsep 2 bottom assumptions++mkProof ∷ Bool → String → [Box] → Prefix → Box → Int → Box+mkProof isLetVar name assumptions prefix term numS = let conclusion = mkPrefix prefix <+> term in+	if numS ≡ 0+		then if isLetVar then conclusion else infer name assumptions conclusion+		else infer "S" [mkProof isLetVar name assumptions (tail prefix) term (numS - 1)] conclusion++mkPrefix ∷ Prefix → Box+mkPrefix prefix = text $ "(" ⧺ unwords (map showVar $ reverse prefix) ⧺ ")"+	where showVar (v,fs) = v ⧺ if Set.null fs then "" else "[" ⧺ unwords (Set.toList fs) ⧺ "]"+}++attr R Λ Bind+	syn proof ∷ Box++sem Λ+	| * loc.proof = mkProof @loc.isLvar @loc.proofstep @loc.assumptions @loc.parentPrefix @loc.pp (length @loc.killVars)+	| V loc.proofstep = "0"+	    loc.assumptions = []+	| A loc.proofstep = "@"+	    loc.assumptions = [@fun.proof, @arg.proof]+	| Λ loc.proofstep = "λ"+	    loc.assumptions = [@body.proof]+	| S loc.proofstep = "S"+	    loc.assumptions = [@body.proof]+	| L loc.proofstep = "let"+	    loc.assumptions = @binds.proofs ⧺ [@body.proof]+	| I loc.proofstep   = undefined+	    loc.assumptions = undefined+	| V loc.isLvar = @loc.varType == LetBound+	| A S Λ L I loc.isLvar = False++sem Bind | Tuple lhs.proof = @x2.proof++attr Binds+	syn proofs ∷ {[Box]}++sem Binds+	| Nil lhs.proofs = []+	| Cons lhs.proofs = @hd.proof : @tl.proofs

@@ -0,0 +1,91 @@+{-# LANGUAGE UnicodeSyntax #-}+module Main where++import Prelude.Unicode+import Parser+import Lambda (Params (..), LetPrefixLengths (..), showNameless, showTRNameless,+	synthesise, scoped_Syn_R, dfa_Syn_R, readback_Syn_R, proof_Syn_R, unscoped_Syn_R)+import System.Environment+import Language.HaLex.Minimize+import System.Cmd+import Language.HaLex.FaAsDiGraph (tographviz)+import Language.HaLex.Dfa (Dfa, beautifyDfa)+import Language.HaLex.FaOperations (dfa2ndfa)+import Language.HaLex.Equivalence (equivDfa)+import Spanning+import Text.PrettyPrint.Boxes (render)+import System.Console.GetOpt+import Control.Monad (when)+++data Opt+	= OptNoVarBacklinks+	| OptNoSBacklinks+	| OptSharedVars+	| OptMaxPrefix+	| OptMinPrefix+	deriving Eq++options = let option s o d = Option [] [s] (NoArg o) d in+	[option "no-var-backlinks" OptNoVarBacklinks "no backlinks for variable occurrences",+	 option "no-s-backlinks"   OptNoSBacklinks   "no backlinks for delimiter vertices",+	 option "shared-variables" OptSharedVars     "implicit sharing of variable occurrences",+	 option "max-prefix"       OptMaxPrefix      "maximal (same) prefix lengths for let-bindings",+	 option "min-prefix"       OptMinPrefix      "minimal prefix lengths for let-bindings"]++usage = "maxsharing [options] file1 ..." ++main ∷ IO ()+main = do+	args ← getArgs++	let (params, files) = case getOpt Permute options args of+		(options, files, []) → (processOptions options, files)+		(_,_,errs) → error (concat errs ++ usageInfo usage options)++	mapM_ (processFile params) files++processOptions options = let has opt = opt ∈ options in Params+	{letPrefixLengths   = if has OptMaxPrefix then MaxPrefix else if has OptMinPrefix then MinPrefix else MaxEagPre,+ 	 withVarBacklinks   = not $ has OptNoVarBacklinks,+ 	 withSBacklinks     = not $ has OptNoSBacklinks,+ 	 withSharedVars     = has OptSharedVars}++processFile ∷ Params → FilePath → IO ()+processFile params f = let syn = synthesise params in do+	λTerm ← parseFile f+	putStrLn "λ-letrec-term:" >> print λTerm+	let λTermSyn = syn λTerm+	putStrLn $ "translation used: " ⧺ show (letPrefixLengths params) ⧺ "\n"+	let scoped = scoped_Syn_R λTermSyn+	putStrLn ("scoped (with adbmals):") >> print scoped+	putStrLn ("scoped (with scope delimiters and nameless abstractions):") >> putStrLn (showNameless scoped)+	putStrLn "derivation:" >> putStrLn (render $ proof_Syn_R λTermSyn)+	let dfa = dfa_Syn_R $ syn scoped+	putStr "DFA: " >> dot (f ⧺ ".dfa") dfa >> putStrLn ""+	let tree = spanning params dfa+	putStrLn "spanning tree:" >> putStrLn (showTRNameless tree)+	putStrLn "readback:" >> print (readback_Syn_R $ syn tree)++	let minDfa = stdMinimizeDfa dfa+	putStr "minimised DFA: " >> dot (f ⧺ ".dfa.min") minDfa >> putStrLn ""+	let minTree = spanning params minDfa+	putStrLn "spanning tree:" >> putStrLn (showTRNameless minTree)+	let minλTerm = readback_Syn_R $ syn minTree+	putStrLn "readback:" >> putStr (show $ unscoped_Syn_R $ syn minλTerm)++	let readbackDfa = dfa_Syn_R $ syn minλTerm+	let (beautifulMinDfa, beautifulReadbackDfa) = (beautifyDfa minDfa, beautifyDfa readbackDfa)+	when (not $ beautifulMinDfa `equivDfa` beautifulReadbackDfa) $ do+		putStrLn "Sanity check failed! Minimised DFA and readback DFA are not equivalent."+		putStrLn $ "(see files with .dfa.min.bf. and .dfa.rb. in their names)" +		dot (f ⧺ "dfa.min.bf") beautifulMinDfa >> dot (f ⧺ ".dfa.rb") beautifulReadbackDfa++dot ∷ (Show st, Show sy, Ord st, Ord sy) ⇒ String → Dfa st sy → IO ()+dot name dfa = do+	let dotfile = name ⧺ ".dot"+	let pdffile = name ⧺ ".pdf"+	putStrLn $ "writing to files " ⧺ dotfile ⧺ " and " ⧺ pdffile+	writeFile dotfile (tographviz (dfa2ndfa dfa) "g" "circle" "TB" (show . show))+	_ ← system $ "dot -Tpdf -o" ⧺ pdffile ⧺ " " ⧺ dotfile+	return ()

@@ -0,0 +1,72 @@+{-# LANGUAGE UnicodeSyntax #-}+module Parser where++import Lambda+import Prelude.Unicode+import Text.ParserCombinators.Parsec as Parsec+import Text.ParserCombinators.Parsec.IndentParser as Indent+import Text.ParserCombinators.Parsec.Language+import Text.ParserCombinators.Parsec.IndentParser.Token+import Control.Monad (liftM)+++parse ∷ String → Λ+parse str = either (error ∘ show) id (Indent.parse parser "(null)" str)++parseFile ∷ FilePath → IO Λ+parseFile = liftM (either (error ∘ show) id) ∘ Indent.parseFromFile parser++parser ∷ IndentCharParser st Λ+parser = expression where++	expression = flip label "expression" $ application <|> letBinding++	application = liftM (foldl1 A) $ many1 $ choice [parenthetic, abstraction, variable]++	parenthetic = parens haskell expression++	abstraction = flip label "abstraction" $ do+		_ ← sym "λ" <|> sym "\\"+		vars ← many1 ident+		_ ← sym "." <|> sym "→" <|> sym "->"+		body ← expression+		return $ foldr Λ body vars++	variable = liftM V $ ident <|> liftM (either show show) (naturalOrFloat haskell)++	-- Ugly, but works. Keyword "in" terminates binding blocks and bindings. Allows empty lets+	letBinding = flip label "let binding" $ do+		keyword "let"+		let parseBindings = do+			e ← optionMaybe $ keyword "in" >> expression+			case e of+				Just je → return ([], Just je)+				Nothing → do+					(b,e) ← lineFold $ do+						b ← binding+						e ← optionMaybe $ keyword "in" >> expression+						return (b,e)+					case e of+						Nothing → do+							rec ← optionMaybe parseBindings+							case rec of+								Nothing → return ([b], Nothing)+								Just (bs, me) → return (b:bs, me)+						Just je → return ([b], Just je)+		(binds, e) ← block parseBindings+		case e of+			Nothing → liftM (L binds) (keyword "in" >> expression)+			Just je → return $ L binds je++	binding ∷ IndentCharParser st (String,Λ)+	binding = flip label "binding" $ do+		funct  ← ident+		params ← many ident+		body   ← sym "=" >> expression+		return (funct, foldr Λ body params)++	keyword = reserved haskell+	ident = do+		i ← identifier haskell+		if head i ≡ 'λ' then fail "'λ' is reserved for abstractions" else return i+	sym = symbol haskell

@@ -0,0 +1,5 @@+import Distribution.Simple (defaultMainWithHooks)+import Distribution.Simple.UUAGC (uuagcLibUserHook)+import UU.UUAGC (uuagc)++main = defaultMainWithHooks $ uuagcLibUserHook uuagc

@@ -0,0 +1,81 @@+{-# LANGUAGE UnicodeSyntax, ScopedTypeVariables, TypeFamilies #-}+module Spanning where++import Prelude.Unicode+import Lambda (Λ (..), Symbol (..), Params (..), V, combinations)+import Language.HaLex.Dfa (Dfa (..))+import Data.Map (Map)+import qualified Data.Map as Map+import Data.List ((\\),sort)+import Control.Monad.State+import Control.Applicative+++-- | Turns a λ-DFA into a λ-spanning-tree. The I-symbol is used for indirection nodes+spanning ∷ ∀ state. Ord state => Params → Dfa state Symbol -> Λ+spanning params (Dfa symbols states start _ trans) = evalState (spanningΛ start) funcVarsVisited where++	-- Stateful computation that remembers which shared states have already been dispatched+	spanningΛ ∷ state → State (Map state (V,Bool)) Λ+	spanningΛ s = let descend = spanningLoc in do+		sharedStates ← get+		case Map.lookup s sharedStates of -- we check the status of s+			Nothing → descend s           -- s is not a shared state+			Just (f,True) → pure $ V f        -- s is a shared state that has already been dispatched+			Just (f,False) → do               -- s is a shared state that we will dispatch right now+				modify $ Map.insert s (f,True) -- we mark s as dispatched+				I f <$> descend s          -- we create an indirection node and descend below s++	spanningLoc ∷ state → State (Map state (V,Bool)) Λ+	spanningLoc s = let descend = spanningΛ in case outEdges s of+	   [(S_Λ,e)] → Λ (lookupMap s varMap) <$> descend e+	   [(S_A0,f), (S_A1,x)] → A <$> descend f <*> descend x+	   [(S_V,x)] → pure $ V (lookupMap x varMap)+	   [(S_S0,e),(S_S1,abs)] → S (lookupMap abs varMap) <$> descend e+	   [(S_F v, _)] → pure $ V v+	   [] → pure $ I "bh" (V "bh") -- blackhole+	   _ → error "This seems not to be a λ-DFA"++	varMap ∷ Map state V+	varMap = Map.fromList $ filter isAbstraction states `zip` vs where+		vs ∷ [V]+		vs = combinations "xyzabcderstuvw" \\ freeVariables+		isAbstraction ∷ state → Bool+		isAbstraction node = trans node S_Λ ≢ dummy++	dummy ∷ state -- the state whose outgoing edges all point to itself+	dummy = case [s | s ← states, all (\sym → trans s sym ≡ s) symbols] of+		[x] → x+		___ → error $ "couldn't identify dummy state"++	freeVariables ∷ [V]+	freeVariables = [v | S_F v ← symbols]++	fs ∷ [V]+	fs = combinations ['F'..'U'] \\ freeVariables++	-- same as funcVars only with the additional information wether we have already visited a node+	funcVarsVisited ∷ Map state (V,Bool)+	funcVarsVisited = fmap (\v → (v,False)) funcVars++	funcVars ∷ Map state V -- maps shared states to a unique function variable+	funcVars = Map.fromList $ {-filter (not . isVarOcc)-} sharedStates `zip` fs where+		isVarOcc s = any (\l → trans s l ≢ dummy) (filter isVarSymbol symbols) where+			isVarSymbol (S_V) = True+			isVarSymbol (S_F _) = True+			isVarSymbol _ = False++	-- states with multiple incoming (non-backlink) edges (shared subgraphs)+	sharedStates ∷ [state]+	sharedStates = Map.keys $ Map.filter (≥2) $ Map.fromListWith (+) (succList `zip` repeat 1) where+		succList = start : [target | (sym,target) ← concatMap outEdges states, not $ isBacklink sym]+		isBacklink (S_V)   = True+		isBacklink (S_F _) = True+		isBacklink (S_S1)  = True+		isBacklink _______ = False++	outEdges ∷ state → [(Symbol, state)]+	outEdges source = sort [(sym, target) | sym ← symbols, let target = trans source sym, target ≢ dummy]++lookupMap ∷ Ord k ⇒ k → Map k a → a+lookupMap = Map.findWithDefault (error "lookupMap: key not found")

@@ -0,0 +1,40 @@+Name:           maxsharing+Version:        1.0+Copyright:      (c) 2013, Jan Rochel+Author:         Jan Rochel+Maintainer:     jan@rochel.info+Homepage:       http://rochel.info/maxsharing/+License:        BSD3+License-file:   LICENSE+Stability:      beta+Build-type:     Custom+Synopsis:       Maximal sharing of terms in the lambda calculus with letrec+Description:    Parses a lambda-letrec term; transforms it into a first-order+                term graph representation; minimises the graph; reads back a+                lambda-letrec term which has the same unfolding as the original+                term, but exhibits maximal sharing.+                If executable "dot" from graphviz is available, the graphs are+                displayed (tested for Linux).+                The approach is described in a technical report:+                http://arxiv.org/abs/1401.1460+Category:       Graphs, Compiler+Cabal-Version:  >= 1.6+Extra-Source-Files: uuagc_options++Executable maxsharing+  Build-Depends:+    base < 4.7,+    base-unicode-symbols < 0.3,+    parsec < 3.2,+    IndentParser < 0.3,+    containers < 0.6,+    containers-unicode-symbols < 0.4,+    mtl < 2.2,+    uuagc-cabal < 1.1,+    uuagc >= 0.9.50.2,+    HaLeX >= 1.2.1,+    boxes < 0.2,+    process < 1.2+  Extensions: UnicodeSyntax+  Other-Modules:  Lambda Parser Spanning+  Main-Is: MaxSharing.hs

@@ -0,0 +1,2 @@+file : "Lambda.ag"+options : catas, wrappers, semfuns, data, signatures, self, haskellsyntax