-- 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.Maybe (mapMaybe) 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 | L binds ∷ Binds body ∷ Λ -- let binding | S var ∷ V body ∷ Λ -- adbmal / scope delimiter | I var ∷ V body ∷ Λ -- indirection node 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 but eager scope" } -- {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 (mapMaybe showVar $ reverse prefix) ⧺ ")" where showVar (v,fs) = if v == "*" ∧ Set.null fs then Nothing else Just $ 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