-- | Translation of bang patterns, which introduce implicit threading. module Syntax.ImplicitThreading ( threadDecls, threadDecl, threadProg, ) where import Util import AST import Data.Loc import Error import Meta.Quasi import Syntax.Construction import qualified Syntax.Ppr as Ppr import Prelude () import Data.Generics (Data, everywhere, mkT, extT) import qualified Data.Map as M import qualified Data.Set as S type R = Raw type ThreadTrans a = MonadAlmsError m ⇒ a → m a threadProg ∷ ThreadTrans (Prog R) threadDecls ∷ ThreadTrans [Decl R] threadDecl ∷ ThreadTrans (Decl R) threadProg [prQ| $list:ds in $opt:me |] = do ds' ← mapM threadDecl ds me' ← mapM threadExpr me return [prQ| $list:ds' in $opt:me' |] threadDecls = mapM threadDecl threadDecl d0 = withLocation d0 $ case d0 of [dc| let $π = $e |] → do withLocation π $ bassert (not (patternHasBang π)) [msg| Implicit threading translation does not allow ! patterns to appear declaration let bindings. |] e' ← threadExpr e return [dc| let $π = $e' |] [dc| let rec $list:bns |] → do bns' ← mapM threadBinding bns return [dc| let rec $list:bns' |] [dc| type $list:_ |] → return d0 [dc| type $tid:_ = type $qtid:_ |] → return d0 [dc| abstype $list:abstys with $list:ds end |] → do ds' ← mapM threadDecl ds return [dc| abstype $list:abstys with $list:ds' end |] [dc| module $mid:mid = $modexp |] → do modexp' ← threadModExp modexp return [dc| module $mid:mid = $modexp' |] [dc| module type $sid:_ = $_ |] → return d0 [dc| open $modexp |] → do modexp' ← threadModExp modexp return [dc| open $modexp' |] [dc| local $list:ds1 with $list:ds2 end |] → do ds1' ← mapM threadDecl ds1 ds2' ← mapM threadDecl ds2 return [dc| local $list:ds1' with $list:ds2' end |] [dc| exception $uid:_ of $opt:_ |] → return d0 [dc| $anti:a |] → $antifail threadModExp ∷ ThreadTrans (ModExp R) threadModExp modexp0 = withLocation modexp0 $ case modexp0 of [meQ| struct $list:ds end |] → do ds' ← mapM threadDecl ds return [meQ| struct $list:ds' end |] [meQ| $qmid:_ $list:_ |] → return modexp0 [meQ| $modexp : $sigexp |] → do modexp' ← threadModExp modexp return [meQ| $modexp' : $sigexp |] [meQ| $anti:a |] → $antifail threadBinding ∷ ThreadTrans (Binding R) threadBinding bn0 = withLocation bn0 $ case bn0 of [bnQ| $vid:x = $e |] → do e' ← threadExpr e return [bnQ| $vid:x = $e' |] [bnQ| $antiB:a |] → $antifail threadCaseAlt ∷ ThreadTrans (CaseAlt R) threadCaseAlt ca0 = case ca0 of [caQ| $π → $e |] | (π', xs@(_:_)) ← patternBangRename π → do e' ← beginTranslate xs e return [caQ| $π' → $e' |] | otherwise → do e' ← threadExpr e return [caQ| $π → $e' |] [caQ| #$uid:c $opt:mπ → $e |] | Just (π', xs@(_:_)) ← patternBangRename <$> mπ → do e' ← beginTranslate xs e return [caQ| #$uid:c $π' → $e' |] | otherwise → do e' ← threadExpr e return [caQ| #$uid:c $opt:mπ → $e' |] [caQ| $antiC:a |] → $antifail threadField ∷ ThreadTrans (Field R) threadField fd0 = case fd0 of [fdQ| $uid:u = $e |] → do e' ← threadExpr e return [fdQ| $uid:u = $e' |] [fdQ| $antiF:a |] → $antifail threadExpr ∷ ThreadTrans (Expr R) threadExpr e = case e of [ex| $qvid:_ |] → return e [ex| $lit:_ |] → return e [ex| $qcid:c $opt:me |] → do me' ← mapM threadExpr me return [ex| $qcid:c $opt:me' |] [ex| let $π = $e1 in $e2 |] | (π', xs@(_:_)) ← patternBangRename π → do e1' ← threadExpr e1 e2' ← beginTranslate xs e2 return [ex| let $π' = $e1' in $e2' |] | otherwise → do e1' ← threadExpr e1 e2' ← threadExpr e2 return [ex| let $π = $e1' in $e2' |] [ex| match $e0 with $list:cas |] → do e0' ← threadExpr e0 cas' ← mapM threadCaseAlt cas return [ex| match $e0' with $list:cas' |] [ex| let rec $list:bns in $e1 |] → do bns' ← mapM threadBinding bns e1' ← threadExpr e1 return [ex| let rec $list:bns' in $e1' |] [ex| let $decl:d in $e1 |] → do d' ← threadDecl d e1' ← threadExpr e1 return [ex| let $decl:d' in $e1' |] [ex| ($e1, $e2) |] → do e1' ← threadExpr e1 e2' ← threadExpr e2 return [ex| ($e1', $e2') |] [ex| λ $π → $e2 |] | (π', xs@(_:_)) ← patternBangRename π → do e2' ← beginTranslate xs e2 return [ex| λ $π' → $e2' |] | otherwise → do e2' ← threadExpr e2 return [ex| λ $π → $e2' |] [ex| $e1 $e2 |] → do e1' ← threadExpr e1 e2' ← threadExpr e2 return [ex| $e1' $e2' |] [ex| `$uid:c $opt:me |] → do me' ← mapM threadExpr me return [ex| `$uid:c $opt:me' |] [ex| #$uid:c $e2 |] → do e2' ← threadExpr e2 return [ex| #$uid:c $e2' |] [ex| { $list:flds | $e2 } |] → do flds' ← mapM threadField flds e2' ← threadExpr e2 return [ex| { $list:flds' | $e2' } |] [ex| {+ $list:flds | $e2 +} |] → do flds' ← mapM threadField flds e2' ← threadExpr e2 return [ex| {+ $list:flds' | $e2' +} |] [ex| $e1.$uid:u |] → do e1' ← threadExpr e1 return [ex| $e1'.$uid:u |] [ex| $e1 : $annot |] → do e1' ← threadExpr e1 return [ex| $e1' : $annot |] [ex| $e1 :> $annot |] → do e1' ← threadExpr e1 return [ex| $e1' :> $annot |] [ex| $anti:_ |] → return e -- Synthesized attributes data Synth = S { code ∷ !(Expr R), typ ∷ ![[VarId R]], vars ∷ ![VarId R] } deriving Show beginTranslate ∷ MonadAlmsError m ⇒ [VarId R] → Expr R → m (Expr R) beginTranslate env0 e00 = do let e00_env = S.fromList env0 e00' ← loop e00_env M.empty e00 return $ exLet' (r1 -*- vars e00') (code e00') $ r1 -*- ren env0 where loop env funs e = withLocation e $ case e of [ex| λ $π → $e1 |] → do let (π', new) = patternBangRename π e1_env = (env ∖ dv π) ∪ new e1' ← loop e1_env funs e1 let latent = vars e1' ∖ ren new body = optExAbs latent $ exLet' (r1 -*- vars e1') (code e1') $ r1 -*- ren new ++ latent return S { vars = emptySet, typ = latent : typ e1', code = [ex| λ $π' → $body |] } -- [ex| $e1 $e2 |] | Just dv_π2@(_:_) ← expr2pattVars env e2 → do e1' ← loop env funs e1 let (latent, cod_e1_typ) = splitType (typ e1') e_vars = toList (vars e1' ∪ ren dv_π2 ∪ latent) interference = ren dv_π2 ∩ latent e2' = ren e2 bassert (null interference) $ [msg| In implicit threading syntax expansion, the the operand of an application expression uses the some imperative variables that were also captured by the definition of the operator:
operator:
$5:e1
operand:
$5:e2
variables:
$interference
|] return S { vars = e_vars, typ = cod_e1_typ, code = exLet' (r1 -*- vars e1') (code e1') $ exLet' (r2 -*- ren dv_π2 ++ latent) (optExApp [ex| $vid:r1 $e2' |] latent) $ r2 -*- e_vars } | otherwise → do e1' ← loop env funs e1 e2' ← loop env funs e2 assertNotFun e2' "operand of an application expression" e2 let (latent, cod_e1_typ) = splitType (typ e1') e_vars = toList (vars e1' ∪ vars e2' ∪ latent) return S { vars = e_vars, typ = cod_e1_typ, code = exLet' (r1 -*- vars e1') (code e1') $ exLet' (r2 -*- vars e2') (code e2') $ exLet' (r -*- latent) (optExApp [ex| $vid:r1 $vid:r2 |] latent) $ r -*- e_vars } -- [ex| $vid:x |] | x ∈ env → return S { vars = [ren x], typ = [], code = exPair (ren e) exUnit } | otherwise → return S { vars = [], typ = M.findWithDefault [] x funs, code = e } [ex| $qvid:_ |] → return S { vars = [], typ = [], code = e } [ex| $qcid:_ |] → return S { vars = [], typ = [], code = e } [ex| $qcid:c1 $e2 |] → do e2' ← loop env funs e2 assertNotFun e2' "argument of a data constructor" e2 return S { vars = vars e2', typ = [], code = exLet' (r -*- vars e2') (code e2') $ [ex| $qcid:c1 $vid:r |] -*- vars e2' } [ex| let $π = $e1 in $e2 |] | Just dv_π1@(_:_) ← expr2pattVars env e1 → do let (π', new) = patternBangRename π hidden = dv_π1 ∖ (dv π ∖ new) e2_env = (env ∖ hidden ∖ dv π) ∪ new e1' = ren e1 e2' ← loop e2_env funs e2 let e_vars = ren dv_π1 ∪ (vars e2' ∖ ren new) e_vars' = [ if v ∈ ren new then exUnit else toExpr v | v ← e_vars ] body = censorVars (ren (dv_π1 ∖ dv π)) $ exLet (r2 -*- vars e2') (code e2') $ r2 -*- (toExpr <$> ren new) ++ e_vars' π'' = renOnly (env ∖ new) π' return S { vars = e_vars, typ = typ e2', code = [ex| let $π'' = $e1' in $body |] } | otherwise → do e1' ← loop env funs e1 case typ e1' of _:_ | [pa| $vid:x |] ← π → do let e2_env = env ∖ [x] e2_funs = M.insert x (typ e1') funs e2' ← loop e2_env e2_funs e2 let e_vars = vars e1' ∪ vars e2' return S { vars = e_vars, typ = typ e2', code = (exLet (x -*- vars e1') (code e1') $ exLet' (r2 -*- vars e2') (code e2') $ r2 -*- e_vars) <<@ _loc } _ → do assertNotFun e1' "right-hand side of a let expression" e1 let (π', new) = patternBangRename π e2_env = env ∪ new e2' ← loop e2_env funs e2 let e_vars = vars e1' ∪ (vars e2' ∖ ren new) return S { vars = e_vars, typ = typ e2', code = (exLet' (r1 -*- vars e1') (code e1') $ exLet' (r -*- (vars e2' ∖ ren new)) (exLet π' (toExpr r1) $ exLet' (r2 -*- vars e2') (code e2') $ ((r2 -*- ren new ∷ Expr Raw) -*- (vars e2' ∖ ren new))) $ (r -*- e_vars)) <<@ _loc } [ex| $lit:_ |] → return S { vars = [], typ = [], code = e } -- [ex| match $e0 with $list:cas |] → do (used, changed, rhs) ← case expr2pattVars env e0 of Just dv_π0@(_:_) → return (S.fromList dv_π0, [], ren e0) _ → do e0' ← loop env funs e0 assertNotFun e0' "expression in match" e0 return (emptySet, vars e0', code e0') let decompose [caQ|@=loc $πi → $ei |] = let (πi', newi) = patternBangRename πi in (dv πi, newi ∖ used, Left πi', ei, loc) decompose [caQ|@=loc #$uid:c → $ei |] = ([], [], Right (c, Nothing), ei, loc) decompose [caQ|@=loc #$uid:c $πi → $ei |] = let (πi', newi) = patternBangRename πi in (dv πi, newi ∖ used, Right (c, Just πi'), ei, loc) decompose [caQ|@=loc $antiC:a |] = $antierror let (dv_πs, news, eπs', es, locs) = unzip5 (decompose <$> cas) hides = ren ((used ∖) <$> dv_πs) ei_envs = zipWith (\dv_πi newi → (env ∖ dv_πi) ∪ used ∪ newi) dv_πs news synths ← zipWithM (loop <-> funs) ei_envs es let e_vars = foldl' (∪) (changed ∪ ren used) (zipWith (∖) (vars <$> synths) (ren news)) e_typ = foldl' joinType [] (typ <$> synths) coerces = (`coerceType` e_typ) <$> typ <$> synths cas' = [ let body = censorVars (toList hidei) $ exLet' (r -*- vars ei') (code ei') $ coercei -*- e_vars in case renOnly used eπi' of Left πi' → [caQ|@=loc $πi' → $body |] Right (c, mπi') → [caQ|@=loc #$uid:c $opt:mπi' → $body |] | eπi' ← eπs' | hidei ← hides | ei' ← synths | coercei ← coerces | loc ← locs] return S { vars = e_vars, typ = e_typ, code = exLet' (r -*- changed) rhs $ [ex| match $vid:r with $list:cas' |] } -- [ex| let rec $list:bns in $e2 |] → do -- We infer the types of recursive functions by iterating to -- a fixpoint. Does this terminate? I believe it's monotone -- and in a finite domain, so it should. let bloop previous = do let env' = env ∖ (fst <$> previous) funs' = foldr (uncurry M.insert) funs previous (fτs, bns') ← unzip `liftM` mapM (binding env' funs') bns if (previous == fτs) then return (env', funs', bns') else bloop fτs (e2_env, e2_funs, bns') ← bloop [] e2' ← loop e2_env e2_funs e2 let e2_code = code e2' return S { vars = vars e2', typ = typ e2', code = [ex| let rec $list:bns' in $e2_code |] } [ex| let $decl:d in $e2 |] → do d' ← threadDecl d -- Note: decl bindings do not shadow bang variables e2' ← loop env funs e2 let e2_code = code e2' return S { vars = vars e2', typ = typ e2', code = [ex| let $decl:d' in $e2_code |] } [ex| ($e1, $e2) |] → do e1' ← loop env funs e1 e2' ← loop env funs e2 assertNotFun e1' "tuple component" e1 assertNotFun e2' "tuple component" e2 let e_vars = vars e1' ∪ vars e2' return S { vars = e_vars, typ = [], code = exLet' (r1 -*- vars e1') (code e1') $ exLet' (r2 -*- vars e2') (code e2') $ [ex| ($vid:r1, $vid:r2) |] -*- e_vars } [ex| `$uid:_ |] → return S { vars = [], typ = [], code = e } [ex| `$uid:c1 $e2 |] → do e2' ← loop env funs e2 assertNotFun e2' "argument of a variant constructor" e2 return S { vars = vars e2', typ = [], code = exLet' (r -*- vars e2') (code e2') $ [ex| `$uid:c1 $vid:r |] -*- vars e2' } [ex| #$uid:c1 $e2 |] → do e2' ← loop env funs e2 assertNotFun e2' "argument of a variant embedding" e2 return S { vars = vars e2', typ = [], code = exLet' (r -*- vars e2') (code e2') $ [ex| #$uid:c1 $vid:r |] -*- vars e2' } [ex| { $list:flds1 | $e2 } |] → let eachField [] = withLocation e2 $ do e2' ← loop env funs e2 assertNotFun e2' "record in extension expression" e2 return e2' eachField ([fdQ|@=loci $uid:ui = $ei |]:flds) = withLocation loci $ do ei' ← loop env funs ei flds' ← eachField flds assertNotFun ei' "field of record" ei let each_vars = vars ei' ∪ vars flds' return S { vars = each_vars, typ = [], code = exLet' (r1 -*- vars ei') (code ei') $ exLet' (r2 -*- vars flds') (code flds') $ [ex| { $uid:ui = $vid:r1 | $vid:r2 } |] -*- each_vars } eachField ([fdQ|! $antiF:a |]:_) = $antifail in eachField flds1 [ex| {+ $list:flds1 | $e2 +} |] → do sequence_ [ withLocation loci $ do ei' ← loop env funs ei assertNotFun ei' "field of record" ei assertNoCapture ei' "Additive-record field" | [fdQ|@=loci $uid:_ = $ei |] ← flds1 ] e2' ← loop env funs e2 assertNotFun e2' "record in extension expression" e2 assertNoCapture e2' "Additive-record in extension expression" return S { vars = [], typ = [], code = e } [ex| $e1.$uid:u |] → do e1' ← loop env funs e1 assertNotFun e1' "record in selector expression" e1 return S { vars = vars e1', typ = [], code = exLet' (r1 -*- vars e1') (code e1') $ [ex| $vid:r1.$uid:u |] -*- vars e1' } [ex| $e1 : $annot |] → do e1' ← loop env funs e1 return S { vars = vars e1', typ = typ e1', code = exLet' (r -*- vars e1') (code e1') $ [ex| $vid:r : $annot |] -*- vars e1' } [ex| $e1 :> $annot |] → do e1' ← loop env funs e1 return S { vars = vars e1', typ = typ e1', code = exLet' (r -*- vars e1') (code e1') $ [ex| $vid:r :> $annot |] -*- vars e1' } [ex| $anti:a |] → $antifail -- binding env funs bn = withLocation bn $ case bn of [bnQ| $vid:f = $e |] → do let env_e = env ∖ [f] e' ← loop env_e funs e bassert (null (vars e')) $ [msg| In implicit threading syntax expansion, imperative variables may not be used on the right-hand side of a let rec binding unless they occur in the body of a function.
In binding:
$f
Used variables:
$1
|] (vars e') let e_code = code e' return ((f, typ e'), [bnQ| $vid:f = $e_code |]) [bnQ| $antiB:a |] → $antifail -- Find the least-upper bound of two variable/effect types. joinType ∷ [[VarId R]] → [[VarId R]] → [[VarId R]] joinType (vs1:rest1) (vs2:rest2) = (vs1 ∪ vs2) : joinType rest1 rest2 joinType [] τ2 = τ2 joinType τ1 [] = τ1 -- | Coerce a value whose variable/effect type is the first argument -- to have the effect of the second. Assumes that the second subsumes -- the first. Assumes that the value is named @r@. coerceType ∷ [[VarId R]] → [[VarId R]] → Expr R coerceType _ [] = toExpr r coerceType reste restg | reste == restg = toExpr r coerceType [] (gots:restg) = exAbsVar' r1 $ optExAbs gots $ exLetVar' r (exApp (toExpr r) (toExpr r1)) $ coerceType [] restg -*- gots coerceType (exps:reste) (gots:restg) = exAbsVar' r1 $ optExAbs gots $ exLet' (r -*- exps) (optExApp (exApp (toExpr r) (toExpr r1)) exps) $ coerceType reste restg -*- gots -- | Shadow some variables with @()@. censorVars ∷ [VarId R] → Expr R → Expr R censorVars [] = id censorVars (v:vs) = exLet' (v -*- vs) (exUnit -*- exUnit <$ vs) -- Given an expression and a list, apply the expression to the -- tuple of the list only if the list is non-empty. optExApp ∷ (Tag i, ToExpr a i) ⇒ Expr i → [a] → Expr i optExApp e0 [] = e0 optExApp e0 (e1:es) = exApp e0 (e1 -*- es) -- Given an expression and a list, abstract to a tuple pattern -- of the list only if the list is non-empty. optExAbs ∷ (Tag i, ToPatt a i) ⇒ [a] → Expr i → Expr i optExAbs [] e0 = e0 optExAbs (π1:πs) e0 = exAbs' (π1 -*- πs) e0 -- Split a type into the latent effect and the codomain splitType ∷ [[a]] → ([a], [[a]]) splitType [] = ([], []) splitType (v:vs) = (v, vs) -- | Given a pattern, rename any !-ed variables, remove the ! itself, -- and return the list of renamed variables. patternBangRename ∷ Patt R → (Patt R, [VarId R]) patternBangRename = runWriter . loop False where loop doIt π0 = case π0 of [pa| $vid:x |] | doIt → do tell [x] let x' = ren x return [pa| $vid:x' |] | otherwise → return π0 [pa| _ |] → return π0 [pa| $qcid:c $opt:mπ |] → do mπ' ← mapM (loop doIt) mπ return [pa| $qcid:c $opt:mπ' |] [pa| ($π1, $π2) |] → do π1' ← loop doIt π1 π2' ← loop doIt π2 return [pa| ($π1', $π2') |] [pa| $lit:_ |] → return π0 [pa| $π as $vid:x |] → do π' ← loop doIt π return [pa| $π' as $vid:x |] [pa| `$uid:c $opt:mπ |] → do mπ' ← mapM (loop doIt) mπ return [pa| `$uid:c $opt:mπ' |] [pa| $π : $annot |] → do π' ← loop doIt π return [pa| $π' : $annot |] [pa| {$uid:u = $π1 | $π2} |] → do π1' ← loop doIt π1 π2' ← loop doIt π2 return [pa| { $uid:u = $π1' | $π2' } |] [pa| ! $π |] → loop True π [pa| $anti:a |] → $antifail patternHasBang ∷ Patt i → Bool patternHasBang π0 = case π0 of [pa| $vid:_ |] → False [pa| _ |] → False [pa| $qcid:_ $opt:mπ |] → maybe False patternHasBang mπ [pa| ($π1, $π2) |] → patternHasBang π1 || patternHasBang π2 [pa| $lit:_ |] → False [pa| $π as $vid:_ |] → patternHasBang π [pa| `$uid:_ $opt:mπ |] → maybe False patternHasBang mπ [pa| $π : $_ |] → patternHasBang π [pa| {$uid:_ = $π1 | $π2} |] → patternHasBang π1 || patternHasBang π2 [pa| ! $_ |] → True [pa| $anti:a |] → $antierror ren :: Data a => a → a ren = everywhere (mkT eachRaw `extT` eachRen) where eachRaw ∷ VarId Raw → VarId Raw eachRen ∷ VarId Renamed → VarId Renamed eachRaw = each; eachRen = each each ∷ Tag i ⇒ VarId i → VarId i each (VarId (LidAnti a)) = VarId (LidAnti a) each (VarId (Lid i s)) = VarId (Lid i (s ++ "!")) renOnly :: ∀ a i. (Data a, Tag i) ⇒ S.Set (VarId i) → a → a renOnly set = everywhere (mkT each) where each ∷ VarId i → VarId i each vid | vid `S.member` set = ren vid | otherwise = vid {- ---- The first order, one variable case: (x is the variable name, y is the fresh state name) fun !(x:t) -> e === fun y:t -> [[ e ]] let !x = e1 in e2 === let y = e1 in [[ e ]] [[ e1 x ]] = let (r, y) = [[ e1 ]] in r y [[ e1 e2 ]] = let (r1, y) = [[ e1 ]] in let (r2, y) = [[ e2 ]] in (r1 r2, y) [[ x ]] = (y, ()) [[ v ]] = (v, y) [[ match e with | p1 -> e1 | ... | pk -> ek ]] = let (r, y) = [[ e ]] in match r with | p1 -> [[ e1 ]] | ... | pk -> [[ ek ]] [[ c e ]] = let (r, y) = [[ e ]] in (c r, y) -- The first order pattern case (2): (p! is a renaming of p) fun !(p:t) -> e === fun p!:t -> let (r1, e.vars) = e.code in (r1, p!) where e.env = dv p in let !p = e1 in e2 === let p! = e1 in let (r1, e.vars) = e.code in (r1, p!) where e.env = dv p in e ::= e1 p2 | dv p2 `subseteq` dv e.env && dv p2 != empty e1.env = e.env e.vars = e1.vars `union` dv p2! e.code = let (r1, e1.vars) = e1.code in let (r2, p2!) = r1 p2! in (r2, e.vars) e ::= e1 e2 e1.env = e2.env = e.env e.vars = e1.vars `union` e2.vars e.code = let (r1, e1.vars) = e1.code in let (r2, e2.vars) = e2.code in (r1 r2, e.vars) e ::= x | x `member` dv p e.vars = x! e.code = (x!, ()) e ::= v e.vars = fv v `intersect` env e.code = let e.vars = e.vars! in (v, [ () | _ <- e.vars ]) e ::= match p0 with | p1 -> e1 | ... | pk -> ek | dv p0 `subseteq` dv e.env && dv p0 != empty if p1 is a bang pattern then e1.env = e.env `union` dv p1 else e1.env = e.env - (dv p1 - dv p0) ... if pk is a bang pattern then ek.env = e.env `union` dv pk else ek.env = e.env - (dv pk - dv p0) e.vars = e.env `intersection` (e1.vars `union` ... `union` ek.vars) e.code = match p0! with | p1[p0!/p0] -> let (p0 - p1)! = ((), ..., ()) in let (r2, e1.vars) = e1.code in (r2, e.vars) | ... (if pk is not a bang pattern then) | pk[p0!/p0] -> let (p0 - pk)! = ((), ..., ()) in let (r2, e1.vars) = e1.code in (r2, e.vars) (else) | pk! -> let (p0 - pk)! = ((), ..., ()) in let (r2, e1.vars) = e1.code in (r2, e.vars) e ::= match e0 with | p1 -> e1 | ... | pk -> ek e0.env = e.env e1.env = e.env - dv p1 ... ek.env = e.env - dv pk e.vars = e.env `intersection` (e0.vars `union` e1.vars `union` ... `union` ek.vars) e.code = let (r1, e0.vars) = e0.code in match r1 with | p1 -> let (r2, e1.vars) = e1.code in (r2, e.vars) | ... | pk -> let (r2, ek.vars) = ek.code in (r2, e.vars) e ::= let rec f1 = v1 and ... and fk = vk in e1 captured = { x `in` (fv v1 `union` ... `union` fv vk) | x! `in` e.env } e1.env = e.env - { f1, ..., fk } e.vars = e1.vars `union` captured! e.code = let captured = captured! in let captured! = ((), ..., ()) in let rec f1 = v1 and ... and fk = vk in let (r1, e1.vars) = e1.code in (r1, e.vars) e ::= let !p1 = e1 in e2 e1.env = e.env e2.env = e.env `union` dv p1 e.vars = e1.vars `union` (e2.vars `intersection` e.env) e.code = let (p1!, e1.vars) = e1.code in let (r2, e2.vars) = e2.code in ((r2, p1!), e.vars) [assuming no shadowing] -- The pattern and function case (3): Types: τ ∷= 1 → τ / [VarId] | 1 Inherited attributes: - env ∷ S.Set VarId - funs ∷ S.Map VarId τ -- τ is renamed Synthesized attributes: - vars ∷ [VarId] -- renamed - type ∷ τ -- renamed - code ∷ Expr Notation • e! is e renamed • [xs/ys]e is the substitution of xs for ys in e • [!xs]e = [!xs/xs]e • {vs} means include this only if vs is non-empty π → e1 ==> [!e1.env]π → let (r1, e1.vars) = e1.code in (r1, !e1.env) where e1.env = bangvars(π) e1.funs = ∅ let π = e1 in e2 ==> let [!e.env]π = e1 in let (r1, e2.vars) = e2.code in (r1, !e2.env) where e2.env = bangvars π e2.funs = ∅ e ::= λ π → e1 new = bangvars(π) latent = e1.vars \ !new e1.env = (e.env \ dv π) ∪ new e.vars = ∅ e.type = 1 → e1.type / latent e.code = λ [!new]π {latent} → let (r, e1.vars) = e1.code in (r, {!new}, {latent}) e ::= e1 π2 [ dv π2 nonempty ⊆ e.env ] latent = latent(e1.type) [ !(dv π2) ∩ latent ≠ ∅ ] ERROR! e.vars = e1.vars ∪ !(dv π2) ∪ latent e.type = cod(e1.type) e.code = let (r1, e1.vars) = e1.code in let (r, !(dv π2), {latent}) = r1 !π2 {latent} in (r, e.vars) e ::= e1 e2 [ e2.type ≠ 1 ] ERROR! latent = latent(e1.type) e.vars = e1.vars ∪ e2.vars ∪ latent e.type = cod(e1.type) e.code = let (r1, e1.vars) = e1.code in let (r2, e2.vars) = e2.code in let (r, {latent}) = r1 r2 {latent} in (r, e.vars) e ::= x [ x ∈ e.env ] e.vars = !x e.type = 1 e.code = (!x, ()) [ otherwise ] e.vars = ∅ e.type = e.funs(x) || 1 e.code = x e ::= c1 e2 [ e2.type ≠ 1 ] ERROR! [ otherwise ] e.vars = e2.vars e.type = 1 e.code = let (r, e2.vars) = e2 in (c1 r, e.vars) e ::= let π = π1 in e2 [ dv π1 nonempty ⊆ e.env ] new = bangvars(π) hidden = dv π1 \ (dv π \ new) e2.env = (e.env \ hidden \ dv π) ∪ new e.vars = !(dv π1) ∪ (e2.vars \ !new) e.type = e2.type e.code = let [!new][!π1]π = !π1 in let !(dv π1 \ dv π) = () ... () in let (r2, e2.vars) = e2.code in ((r2, !new), [()/!new]e.vars) e ::= let x = e1 in e2 [ e1.type ≠ 1 ] e2.env = e.env \ x e2.funs = e.funs[x ↦ e1.type] e.vars = e1.vars ∪ e2.vars e.type = e2.type e.code = let (x, e1.vars) = e1 in let (r2, e2.vars) = e2 in (r2, e.vars) e ::= let π = e1 in e2 [ e1.type ≠ 1 ] ERROR! [ otherwise ] new = bangvars(π) e2.env = e.env ∪ new e.vars = e1.vars ∪ (e2.vars \ !new) e.type = e2.type e.code = let (r1, e1.vars) = e1.code in let (r, e2.vars \ !new) = let [!new]π = r1 in let (r2, e2.vars) = e2.code in ((r2, !new), e2.vars \ !new) in (r, e.vars) e ::= match e0 with | π1 → e1 ⋮ | πk → ek { [ e0 = π0 ⋀ dv π0 nonempty ⊆ e.env ] used = dv π0 changed = ∅ rhs = !π0 [ e0.type ≠ 1 ] ERROR [ otherwise ] used = ∅ changed = e0.vars rhs = e0.code } newᵢ = bangvars(πᵢ) \ used hideᵢ = !(used \ dv πᵢ) eᵢ.env = (e.env \ dv πᵢ) ∪ used ∪ newᵢ e.vars = !used ∪ changed ∪ (e1.vars \ !new1) ∪ ... ∪ (ek.vars \ !newk) e.type = e1.type ⊔ ... ⊔ ek.type coerceᵢ= eᵢ.type ⇝ e.type e.code = let (r, changed) = rhs in match r with | [!used][!new]π1 → let hide1 = () ... () in let (r, e1.vars) = e1.code in (coerce1 r, e.vars) ⋮ | [!used][!new]πk → let hidek = () ... () in let (r, ek.vars) = ek.code in (coercek r, e.vars) -} r, r1, r2 :: VarId R r = ident "r.!" r1 = ident "r1.!" r2 = ident "r2.!" -- | Transform an expression into a pattern, if possible, using only -- the specified variables, and return the set of variables used. expr2pattVars ∷ S.Set (VarId R) → Expr R → Maybe [VarId R] expr2pattVars vs0 e0 = evalStateT (loop e0) vs0 where loop e = case e of [ex| $vid:x |] → do possible ← get if x `S.member` possible then do put (S.delete x possible) return [x] else mzero [ex| $lit:_ |] → return [] [ex| $qcid:_ $opt:me |] → concatMapM loop me [ex| ($e1, $e2) |] → mappend <$> loop e1 <*> loop e2 [ex| `$uid:_ $opt:me |] → concatMapM loop me [ex| $e1 : $_ |] → loop e1 [ex| $qvid:_ |] → mzero [ex| let $_ = $_ in $_ |] → mzero [ex| match $_ with $list:_ |] → mzero [ex| let rec $list:_ in $_ |] → mzero [ex| let $decl:_ in $_ |] → mzero [ex| λ $_ → $_ |] → mzero [ex| $_ $_ |] → mzero [ex| #$uid:_ $_ |] → mzero [ex| { $list:flds | $e2 } |] → mappend <$> concatMapM loopField flds <*> loop e2 [ex| {+ $list:_ | $_ +} |] → mzero [ex| $_.$uid:_ |] → mzero [ex| $anti:_ |] → mzero [ex| $_ :> $_ |] → mzero -- loopField [fdQ| $uid:_ = $ei |] = loop ei loopField [fdQ| $antiF:_ |] = mzero --- --- Producing errors --- -- | Indicate a bug in the bang translator. bangBug ∷ MonadAlmsError m ⇒ String → String → m a bangBug = throwAlms <$$> almsBug ParserPhase -- | Indicate a bug in the bang translator, with no Alms error monad. bangBugError ∷ String → String → a bangBugError = throw <$$> almsBug ParserPhase -- | Indicate a bang translation error. bangError ∷ (MonadAlmsError m, Bogus a) ⇒ Message V → m a bangError msg0 = do reportAlms (AlmsError ParserPhase bogus msg0) return bogus -- | Indicate a bang error. bangError_ ∷ MonadAlmsError m ⇒ Message V → m () bangError_ = bangError -- | Indicate a bang error from which we cannot recover. bangError' ∷ MonadAlmsError m ⇒ Message V → m a bangError' = throwAlms <$> AlmsError ParserPhase bogus -- | Assert some condition, indicating a bang translation error if -- it doesn't hold. bassert ∷ MonadAlmsError m ⇒ Bool → Message V → m () bassert True _ = return () bassert False m = bangError m -- | Assert that the type of the given synthesized attribute is trivial, -- indicating that the term it belongs to hasn't captured any bang -- vars. Also takes a description of the role of the term and the -- term itself. assertNotFun ∷ (MonadAlmsError m, Ppr.Ppr a, Ppr.Ppr b) ⇒ Synth → a → b → m () assertNotFun e' = bassert (all null (typ e')) <$$> [msg| In implicit threading syntax expansion, the $2 cannot be a function that captures some imperative variables.
culprit:
$5:3
captured:
$1
|] (fromOpt [] (typ e')) assertNoCapture ∷ (MonadAlmsError m, Ppr.Ppr a) ⇒ Synth → a → m () assertNoCapture e' = bassert (null (vars e')) <$> [msg| $2 may not capture implicitly threaded variables:
captures:
$1
|] (vars e')