diff --git a/Jenkinsfile b/Jenkinsfile
index c4c337697..3a50777ec 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -94,7 +94,8 @@ melt.trynode('silver') {
 
   stage("Integration") {
     // Projects with 'develop' as main branch, we'll try to build specific branch names if they exist
-    def github_projects = ["/melt-umn/ableC", "/melt-umn/Oberon0", "/melt-umn/ableJ14", "/melt-umn/meta-ocaml-lite", "/melt-umn/rewriting-lambda-calculus",
+    def github_projects = ["/melt-umn/ableC", "/melt-umn/Oberon0", "/melt-umn/ableJ14", "/melt-umn/meta-ocaml-lite",
+                           "/melt-umn/rewriting-lambda-calculus", "/melt-umn/rewriting-regex-matching", "/melt-umn/rewriting-optimization-demo",
                            "/internal/ring"]
     // Specific other jobs to build
     def specific_jobs = ["/internal/matlab/master", "/internal/metaII/master", "/internal/simple/master"]
diff --git a/grammars/core/List.sv b/grammars/core/List.sv
index 6fd95ccc4..327d028fc 100644
--- a/grammars/core/List.sv
+++ b/grammars/core/List.sv
@@ -277,6 +277,12 @@ function repeat
          else v :: repeat(v, times-1);
 }
 
+function range
+[Integer] ::= lower::Integer upper::Integer
+{
+  return if lower >= upper then [] else lower :: range(lower + 1, upper);
+}
+
 function zipWith
 [c] ::= f::(c ::= a b)  l1::[a]  l2::[b]
 {
diff --git a/grammars/silver/composed/idetest/Analyze.sv b/grammars/silver/composed/idetest/Analyze.sv
index a3912c85d..0292addc4 100644
--- a/grammars/silver/composed/idetest/Analyze.sv
+++ b/grammars/silver/composed/idetest/Analyze.sv
@@ -9,6 +9,8 @@ import silver:util:cmdargs;
 import silver:definition:core;
 import silver:definition:env;
 
+import silver:rewrite;
+
 -- This function is mostly copied from function cmdLineRun in driver/BuildProcess.sv
 function ideAnalyze
 IOVal<[Message]> ::= args::[String]  svParser::SVParser ioin::IO
@@ -102,12 +104,12 @@ function rewriteMessages
 function rewriteMessage
 Message ::= path::String m::Message
 {
-  return case m of
-  | err(loc(file, a, b, c, d, e, f), g) -> err(loc(path ++ "/" ++ file, a, b, c, d, e, f), g)
-  | wrn(loc(file, a, b, c, d, e, f), g) -> wrn(loc(path ++ "/" ++ file, a, b, c, d, e, f), g)
-  | info(loc(file, a, b, c, d, e, f), g) -> info(loc(path ++ "/" ++ file, a, b, c, d, e, f), g)
-  | nested(loc(file, a, b, c, d, e, f), g, others) ->
-    nested(loc(path ++ "/" ++ file, a, b, c, d, e, f), g, map(rewriteMessage(path, _), others))
-  end;
+  return
+    rewriteWith(
+      allTopDown(
+        rule on Location of
+        | loc(file, a, b, c, d, e, f) -> loc(path ++ "/" ++ file, a, b, c, d, e, f)
+        end),
+      m).fromJust;
 }
 
diff --git a/grammars/silver/definition/core/QName.sv b/grammars/silver/definition/core/QName.sv
index b97321526..f5a7252bf 100644
--- a/grammars/silver/definition/core/QName.sv
+++ b/grammars/silver/definition/core/QName.sv
@@ -216,6 +216,8 @@ top::QNameAttrOccur ::= at::QName
   top.dcl = if top.found then head(dclsNarrowed) else
     error("INTERNAL ERROR: Accessing dcl of occurrence " ++ at.name ++ " at " ++ top.grammarName ++ " " ++ top.location.unparse);
   top.attrDcl = if top.found then head(attrsNarrowed) else
+    -- Workaround fix for proper error reporting - appairently there are some places where this is still demanded.
+    if !null(at.lookupAttribute.dcls) then head(at.lookupAttribute.dcls) else
     error("INTERNAL ERROR: Accessing dcl of attribute " ++ at.name ++ " at " ++ top.grammarName ++ " " ++ top.location.unparse);
 }
 
diff --git a/grammars/silver/extension/autoattr/Functor.sv b/grammars/silver/extension/autoattr/Functor.sv
index adba5da28..2b0a9a02c 100644
--- a/grammars/silver/extension/autoattr/Functor.sv
+++ b/grammars/silver/extension/autoattr/Functor.sv
@@ -22,6 +22,7 @@ top::AGDcl ::= 'functor' 'attribute' a::Name ';'
 abstract production functorAttributionDcl
 top::AGDcl ::= at::Decorated QName attl::BracketedOptTypeExprs nt::QName nttl::BracketedOptTypeExprs
 {
+  top.unparse = "attribute " ++ at.unparse ++ attl.unparse ++ " occurs on " ++ nt.unparse ++ nttl.unparse ++ ";";
   forwards to
     defaultAttributionDcl(
       at,
@@ -45,31 +46,29 @@ top::AGDcl ::= at::Decorated QName attl::BracketedOptTypeExprs nt::QName nttl::B
 abstract production propagateFunctor
 top::ProductionStmt ::= attr::Decorated QName
 {
+  top.unparse = s"propagate ${attr.unparse};";
+  
   -- No explicit errors, for now.  The only conceivable issue is the attribute not
   -- occuring on the LHS but this should be caught by the forward errors.  
   
   -- Generate the arguments for the constructor
-  local topName::QName = qName(top.location, top.frame.signature.outputElement.elementName);
-  local prodName::QName = qName(top.location, top.frame.fullName);
-  prodName.grammarName = top.grammarName;
-  prodName.config = top.config;
-  prodName.env = top.env;
-
   local inputs :: [Expr] = 
     map(makeArg(top.location, top.env, attr, _), top.frame.signature.inputElements);
   local annotations :: [Pair<String Expr>] = 
-    map(makeAnnoArg(top.location, topName, _), top.frame.signature.namedInputElements);
+    map(
+      makeAnnoArg(top.location, top.frame.signature.outputElement.elementName, _),
+      top.frame.signature.namedInputElements);
 
   -- Construct an attribute def and call with the generated arguments
-  forwards to 
+  forwards to
     attributeDef(
-      concreteDefLHS(topName, location=top.location),
+      concreteDefLHS(qName(top.location, top.frame.signature.outputElement.elementName), location=top.location),
       '.',
       qNameAttrOccur(new(attr), location=top.location),
       '=',
       mkFullFunctionInvocation(
         top.location,
-        baseExpr(prodName, location=top.location),
+        baseExpr(qName(top.location, top.frame.fullName), location=top.location),
         inputs,
         annotations),
       ';',
@@ -112,7 +111,7 @@ Expr ::= loc::Location env::Decorated Env attrName::Decorated QName input::Named
  - @return A list of AnnoExprs to be used to build the named arguments
  -}
 function makeAnnoArg
-Pair<String Expr> ::= loc::Location baseName::QName input::NamedSignatureElement
+Pair<String Expr> ::= loc::Location baseName::String input::NamedSignatureElement
 {
   -- TODO: This is a hacky way of getting the base name, not sure if correct
   -- trouble is the annotations are listed as fullnames, but have to be supplied as shortnames. weird.
@@ -121,7 +120,7 @@ Pair<String Expr> ::= loc::Location baseName::QName input::NamedSignatureElement
   return
     pair(annoName,
       access(
-        baseExpr(baseName, location=loc), '.',
+        baseExpr(qName(loc, baseName), location=loc), '.',
         qNameAttrOccur(qName(loc, annoName), location=loc),
         location=loc));
 }
diff --git a/grammars/silver/extension/autoattr/Monoid.sv b/grammars/silver/extension/autoattr/Monoid.sv
index 0d5a8a559..3ca28d880 100644
--- a/grammars/silver/extension/autoattr/Monoid.sv
+++ b/grammars/silver/extension/autoattr/Monoid.sv
@@ -84,6 +84,8 @@ top::Operation ::=
 abstract production propagateMonoid
 top::ProductionStmt ::= attr::Decorated QName
 {
+  top.unparse = s"propagate ${attr.unparse};";
+  
   -- No explicit errors, for now.  The only conceivable issue is the attribute not
   -- occuring on the LHS but this should be caught by the forward errors.  
   
@@ -94,13 +96,6 @@ top::ProductionStmt ::= attr::Decorated QName
         input.typerep.isDecorable &&
         !null(getOccursDcl(attrFullName, input.typerep.typeName, top.env)),
       top.frame.signature.inputElements);
-  
-  local topName::QName = qName(top.location, top.frame.signature.outputElement.elementName);
-  local prodName::QName = qName(top.location, top.frame.fullName);
-  prodName.grammarName = top.grammarName;
-  prodName.config = top.config;
-  prodName.env = top.env;
-
   local res :: Expr = 
     if null(inputsWithAttr)
     then attr.lookupAttribute.dcl.emptyVal
@@ -119,7 +114,7 @@ top::ProductionStmt ::= attr::Decorated QName
   -- Construct an attribute def and call with the generated arguments
   forwards to
     attrContainsBase(
-      concreteDefLHS(topName, location=top.location),
+      concreteDefLHS(qName(top.location, top.frame.signature.outputElement.elementName), location=top.location),
       '.',
       qNameAttrOccur(new(attr), location=top.location),
       ':=', res, ';', location=top.location);
diff --git a/grammars/silver/extension/autoattr/Propagate.sv b/grammars/silver/extension/autoattr/Propagate.sv
index 2e8a463b9..df8962182 100644
--- a/grammars/silver/extension/autoattr/Propagate.sv
+++ b/grammars/silver/extension/autoattr/Propagate.sv
@@ -69,7 +69,7 @@ top::AGDcl ::= d::DclInfo attrs::NameList
   top.errors :=
     if null(forward.errors)
     then []
-    else [nested(top.location, s"In propagate for production ${d.fullName}:", forward.errors)];
+    else [nested(top.location, s"In propagate of ${attrs.unparse} for production ${d.fullName}:", forward.errors)];
   
   forwards to
     aspectProductionDcl(
diff --git a/grammars/silver/extension/convenience/Productions.sv b/grammars/silver/extension/convenience/Productions.sv
index ff52288ef..a8e677067 100644
--- a/grammars/silver/extension/convenience/Productions.sv
+++ b/grammars/silver/extension/convenience/Productions.sv
@@ -2,6 +2,14 @@ grammar silver:extension:convenience;
 
 import silver:modification:copper;
 
+-- "production" short for "abstract production"
+concrete production productionDclImplicitAbs
+top::AGDcl ::= 'production' id::Name ns::ProductionSignature body::ProductionBody
+{
+  forwards to productionDcl('abstract', $1, id, ns, body, location=top.location);
+}
+
+-- "concrete productions" syntax
 nonterminal ProductionDclStmts with unparse, location, proddcls, lhsdcl, grammarName;
 nonterminal ProductionDclStmt with unparse, location, proddcls, lhsdcl, grammarName;
 
diff --git a/grammars/silver/extension/patternmatching/Case.sv b/grammars/silver/extension/patternmatching/Case.sv
index 9e55a3f15..69401e8c6 100644
--- a/grammars/silver/extension/patternmatching/Case.sv
+++ b/grammars/silver/extension/patternmatching/Case.sv
@@ -14,9 +14,10 @@ terminal Arrow_kwd '->' lexer classes {SPECOP};
 terminal Vbar_kwd '|' lexer classes {SPECOP};
 terminal Opt_Vbar_t /\|?/ lexer classes {SPECOP}; -- optional Coq-style vbar.
 terminal When_kwd 'when' lexer classes {KEYWORD,RESERVED};
+terminal Matches_kwd 'matches' lexer classes {KEYWORD};
 
 -- MR | ...
-nonterminal MRuleList with location, config, unparse, env, errors, matchRuleList, matchRulePatternSize;
+nonterminal MRuleList with location, config, unparse, env, frame, errors, matchRuleList, matchRulePatternSize;
 
 -- Turns MRuleList (of MatchRules) into [AbstractMatchRule]
 synthesized attribute matchRuleList :: [AbstractMatchRule];
@@ -24,8 +25,8 @@ synthesized attribute matchRuleList :: [AbstractMatchRule];
 autocopy attribute matchRulePatternSize :: Integer;
 
 -- P -> E
-nonterminal MatchRule with location, config, unparse, env, errors, matchRuleList, matchRulePatternSize;
-nonterminal AbstractMatchRule with location, headPattern, isVarMatchRule, expandHeadPattern;
+nonterminal MatchRule with location, config, unparse, env, frame, errors, matchRuleList, matchRulePatternSize;
+nonterminal AbstractMatchRule with location, unparse, headPattern, isVarMatchRule, expandHeadPattern;
 
 -- The head pattern of a match rule
 synthesized attribute headPattern :: Decorated Pattern;
@@ -35,7 +36,7 @@ synthesized attribute isVarMatchRule :: Boolean;
 synthesized attribute expandHeadPattern :: (AbstractMatchRule ::= [String]);
 
 -- P , ...
-nonterminal PatternList with location, config, unparse, patternList, env, errors, patternVars, patternVarEnv;
+nonterminal PatternList with location, config, unparse, patternList, env, frame, errors, patternVars, patternVarEnv;
 
 -- Turns PatternList into [Pattern]
 synthesized attribute patternList :: [Decorated Pattern];
@@ -75,13 +76,18 @@ top::Expr ::= 'case' es::Exprs 'of' Opt_Vbar_t ml::MRuleList 'end'
 abstract production caseExpr
 top::Expr ::= es::[Expr] ml::[AbstractMatchRule] failExpr::Expr retType::Type
 {
-  top.unparse = error("Internal error: pretty of intermediate data structure");
+  top.unparse =
+    "(case " ++ implode(", ", map((.unparse), es)) ++ " of " ++ 
+    implode(" | ", map((.unparse), ml)) ++ " | _ -> " ++ failExpr.unparse ++
+    " end :: " ++ prettyType(retType) ++ ")";
 
   -- 4 cases: no patterns left, all constructors, all variables, or mixed con/var.
   -- errors cases: more patterns no scrutinees, more scrutinees no patterns, no scrutinees multiple rules
   forwards to
     case ml of
     | matchRule([], c, e) :: _ -> buildMatchWhenConditionals(ml, failExpr) -- valid or error case
+    -- No match rules, only possible through abstract syntax
+    | [] -> Silver_Expr { let res :: $TypeExpr{typerepTypeExpr(retType, location=top.location)} = $Expr{failExpr} in res end }
     | _ -> if null(es) then failExpr -- error case
            else if null(varRules) then allConCase
            else if null(prodRules) then allVarCase
@@ -141,17 +147,59 @@ top::Expr ::= es::[Expr] ml::[AbstractMatchRule] failExpr::Expr retType::Type
       -- So don't try that!
   
   {--
-   - Mixed con/var? Partition, and push the vars into the "fail" branch.
-   - Use a let for it, to avoid code duplication!
+    - Mixed con/var? Partition into segments and build nested case expressions
+    - The whole segment partitioning is done in a function rather than grabbing the initial segment
+      and forwarding to do the rest of the segments (another workable option) for efficiency
    -}
+  local mixedCase :: Expr = buildMixedCaseMatches(es, ml, failExpr, retType, top.location);
+}
+
+
+--Get the initial segment of the match rules which all have the same
+--pattern type (constructor or var) and the rest of the rules
+function initialSegmentPatternType
+Pair<[AbstractMatchRule] [AbstractMatchRule]> ::= lst::[AbstractMatchRule]
+{
+  return case lst of
+           --this probably shouldn't be called with an empty list, but catch it anyway
+         | [] -> pair([], [])
+         | [mr] -> pair([mr], [])
+         | mr1::mr2::rest ->
+           if mr1.isVarMatchRule == mr2.isVarMatchRule
+           then --both have the same type of pattern
+              let sub::Pair<[AbstractMatchRule] [AbstractMatchRule]> = initialSegmentPatternType(mr2::rest)
+              in pair(mr1::sub.fst, sub.snd) end
+           else --the first has a different type of pattern than the second
+              pair([mr1], mr2::rest)
+         end;
+}
+
+{-
+  Build the correct match expression when we are mixing constructor
+  and variable patterns for the first match.  We do this by
+  partitioning the list into segments of only constructor or variable
+  patterns in order, then putting each segment into its own match.
+-}
+function buildMixedCaseMatches
+Expr ::= es::[Expr] ml::[AbstractMatchRule] failExpr::Expr retType::Type loc::Location
+{
   local freshFailName :: String = "__fail_" ++ toString(genInt());
-  local mixedCase :: Expr =
-    makeLet(top.location,
-      freshFailName, retType, caseExpr(es, varRules, failExpr, retType, location=top.location),
-      caseExpr(es, prodRules, baseExpr(qName(top.location, freshFailName), location=top.location),
-        retType, location=top.location));
+  return if null(ml)
+         then failExpr
+         else let segments::Pair<[AbstractMatchRule] [AbstractMatchRule]> =
+                            initialSegmentPatternType(ml)
+              in
+                makeLet(loc, freshFailName, retType,
+                        buildMixedCaseMatches(es, segments.snd, failExpr, retType, loc),
+                        caseExpr(es, segments.fst, baseExpr(qName(loc, freshFailName), location=loc),
+                                 retType, location=loc))
+              end;
 }
 
+
+
+
+--Match Rules
 concrete production mRuleList_one
 top::MRuleList ::= m::MatchRule
 {
@@ -197,12 +245,36 @@ top::MatchRule ::= pt::PatternList 'when' cond::Expr '->' e::Expr
 
   pt.patternVarEnv = [];
 
-  top.matchRuleList = [matchRule(pt.patternList, just(cond), e, location=top.location)];
+  top.matchRuleList = [matchRule(pt.patternList, just(pair(cond, nothing())), e, location=top.location)];
+}
+
+concrete production matchRuleWhenMatches_c
+top::MatchRule ::= pt::PatternList 'when' cond::Expr 'matches' p::Pattern '->' e::Expr
+{
+  top.unparse = pt.unparse ++ " when " ++ cond.unparse ++ " matches " ++ p.unparse ++ " -> " ++ e.unparse;
+  top.errors := pt.errors; -- e.errors is examined later, after transformation, as is cond.errors
+  
+  top.errors <-
+    if length(pt.patternList) == top.matchRulePatternSize then []
+    else [err(pt.location, "case expression matching against " ++ toString(top.matchRulePatternSize) ++ " values, but this rule has " ++ toString(length(pt.patternList)) ++ " patterns")];
+
+  pt.patternVarEnv = [];
+  p.patternVarEnv = pt.patternVars;
+
+  top.matchRuleList = [matchRule(pt.patternList, just(pair(cond, just(p))), e, location=top.location)];
 }
 
 abstract production matchRule
-top::AbstractMatchRule ::= pl::[Decorated Pattern] cond::Maybe<Expr> e::Expr
+top::AbstractMatchRule ::= pl::[Decorated Pattern] cond::Maybe<Pair<Expr Maybe<Pattern>>> e::Expr
 {
+  top.unparse =
+    implode(", ", map((.unparse), pl)) ++
+    case cond of
+    | just(pair(c, just(p))) -> " when " ++ c.unparse ++ " matches " ++ p.unparse
+    | just(pair(c, nothing())) -> " when " ++ c.unparse
+    | nothing() -> ""
+    end ++
+    " -> " ++ e.unparse;
   top.headPattern = head(pl);
   -- If pl is null, and we're consulted, then we're missing patterns, pretend they're _
   top.isVarMatchRule = null(pl) || head(pl).patternIsVariable;
@@ -374,15 +446,18 @@ AbstractMatchRule ::= headExpr::Expr  headType::Type  absRule::AbstractMatchRule
   -- If it's '_' we do nothing, otherwise, bind away!
   return case absRule of
   | matchRule(headPat :: restPat, cond, e) ->
-      matchRule(restPat,
-        case headPat.patternVariableName, cond of
-        | just(pvn), just(c) -> just(makeLet(absRule.location, pvn, headType, headExpr, c))
-        | _, _ -> cond
+    case headPat.patternVariableName of
+    | just(pvn) ->
+      matchRule(
+        restPat,
+        case cond of
+        | just(pair(c, p)) -> just(pair(makeLet(absRule.location, pvn, headType, headExpr, c), p))
+        | nothing() -> nothing()
         end,
-        case headPat.patternVariableName of
-        | just(pvn) -> makeLet(absRule.location, pvn, headType, headExpr, e)
-        | nothing() -> e
-        end, location=absRule.location)
+        makeLet(absRule.location, pvn, headType, headExpr, e),
+        location=absRule.location)
+    | nothing() -> matchRule(restPat, cond, e, location=absRule.location)
+    end
   end;
 }
 
@@ -437,11 +512,18 @@ Expr ::= ml::[AbstractMatchRule] failExpr::Expr
 {
   return
     case ml of
-    | matchRule(_, just(c), e) :: tl ->
+    | matchRule(_, just(pair(c, nothing())), e) :: tl ->
+      Silver_Expr {
+        if $Expr{c}
+        then $Expr{e}
+        else $Expr{buildMatchWhenConditionals(tl, failExpr)}
+      }
+    | matchRule(_, just(pair(c, just(p))), e) :: tl ->
       Silver_Expr {
-        if $Expr {c}
-        then $Expr {e}
-        else $Expr {buildMatchWhenConditionals(tl, failExpr)}
+        case $Expr{c} of
+        | $Pattern{p} -> $Expr{e}
+        | _ -> $Expr{buildMatchWhenConditionals(tl, failExpr)}
+        end
       }
     | matchRule(_, nothing(), e) :: tl -> e
     | [] -> failExpr
diff --git a/grammars/silver/extension/patternmatching/PatternTypes.sv b/grammars/silver/extension/patternmatching/PatternTypes.sv
index a6f663e2b..6bb0fe288 100644
--- a/grammars/silver/extension/patternmatching/PatternTypes.sv
+++ b/grammars/silver/extension/patternmatching/PatternTypes.sv
@@ -5,7 +5,7 @@ import silver:extension:list only LSqr_t, RSqr_t;
 {--
  - The forms of syntactic patterns that are permissible in (nested) case expresssions.
  -}
-nonterminal Pattern with location, config, unparse, env, errors, patternVars, patternVarEnv, patternIsVariable, patternVariableName, patternSubPatternList, patternNamedSubPatternList, patternSortKey;
+nonterminal Pattern with location, config, unparse, env, frame, errors, patternVars, patternVarEnv, patternIsVariable, patternVariableName, patternSubPatternList, patternNamedSubPatternList, patternSortKey;
 
 {--
  - The names of all var patterns in the pattern.
diff --git a/grammars/silver/extension/rewriting/Expr.sv b/grammars/silver/extension/rewriting/Expr.sv
index a119d6998..b916855fe 100644
--- a/grammars/silver/extension/rewriting/Expr.sv
+++ b/grammars/silver/extension/rewriting/Expr.sv
@@ -2,6 +2,7 @@ grammar silver:extension:rewriting;
 
 -- Environment mapping variables that were defined on the rule RHS to Booleans indicating whether
 -- the variable was explicitly (i.e. not implicitly) decorated in the pattern.
+-- TODO: Lots of flow errors in this grammar because we are pretending this attribute is in the reference set 
 autocopy attribute boundVars::[Pair<String Boolean>] occurs on Expr, Exprs, ExprInhs, ExprInh, AppExprs, AppExpr, AnnoAppExprs, AnnoExpr, AssignExpr, PrimPatterns, PrimPattern;
 
 attribute transform<ASTExpr> occurs on Expr;
@@ -36,7 +37,10 @@ top::Expr ::= q::Decorated QName _ _
             Silver_Expr {
               silver:rewrite:anyASTExpr(
                 \ e::$TypeExpr{typerepTypeExpr(finalType(top).decoratedType, location=builtin)} ->
-                  decorate e with {})
+                  $Expr{
+                    decorateExprWithEmpty(
+                      'decorate', Silver_Expr { e }, 'with', '{', '}',
+                      location=top.location)})
             }),
           consASTExpr(varASTExpr(q.name), nilASTExpr()),
           nilNamedASTExpr())
@@ -51,7 +55,7 @@ top::Expr ::= q::Decorated QName _ _
             }),
           consASTExpr(varASTExpr(q.name), nilASTExpr()),
           nilNamedASTExpr())
-      -- Neither the bound value nor desired type is a decorated nonterminal - just return the value
+      -- Both (or neither) the bound value/desired type is a decorated nonterminal - just return the value
       else varASTExpr(q.name)
     | nothing() ->
       -- The variable is bound in an enclosing let/match
@@ -185,14 +189,56 @@ aspect production synDecoratedAccessHandler
 top::Expr ::= e::Decorated Expr  q::Decorated QNameAttrOccur
 {
   top.transform =
-    applyASTExpr(
-      antiquoteASTExpr(
-        Silver_Expr {
-          silver:rewrite:anyASTExpr(
-            \ e::$TypeExpr{typerepTypeExpr(finalType(e), location=builtin)} -> e.$qName{q.name})
-        }),
-      consASTExpr(e.transform, nilASTExpr()),
-      nilNamedASTExpr());
+    case e of
+    -- Special cases to avoid introducing a reference and causing flow errors.
+    | decorateExprWith(_, eUndec, _, _, inh, _) ->
+      applyASTExpr(
+        antiquoteASTExpr(
+          Silver_Expr {
+            silver:rewrite:anyASTExpr(
+              $Expr{
+                lambdap(
+                  productionRHSCons(
+                    productionRHSElem(
+                      name("_e", builtin), '::',
+                      typerepTypeExpr(finalType(eUndec), location=builtin),
+                      location=builtin),
+                    inh.lambdaParams,
+                    location=builtin),
+                  Silver_Expr {
+                    $Expr{
+                      decorateExprWith(
+                        'decorate', baseExpr(qName(builtin, "_e"), location=builtin),
+                        'with', '{', inh.bodyExprInhTransform, '}',
+                        location=builtin)}.$qName{q.name}
+                  },
+                  location=builtin)})
+          }),
+        consASTExpr(eUndec.transform, inh.transform),
+        nilNamedASTExpr())
+    | lexicalLocalReference(qn, _, _) when
+        case lookupBy(stringEq, qn.name, top.boundVars) of
+        | just(bindingIsDecorated) -> !bindingIsDecorated
+        | nothing() -> false
+        end -> 
+      applyASTExpr(
+        antiquoteASTExpr(
+          Silver_Expr {
+            silver:rewrite:anyASTExpr(
+              \ e::$TypeExpr{typerepTypeExpr(finalType(e).decoratedType, location=builtin)} -> e.$qName{q.name})
+          }),
+        consASTExpr(varASTExpr(qn.name), nilASTExpr()),
+        nilNamedASTExpr())
+    | _ ->
+      applyASTExpr(
+        antiquoteASTExpr(
+          Silver_Expr {
+            silver:rewrite:anyASTExpr(
+              \ e::$TypeExpr{typerepTypeExpr(finalType(e), location=builtin)} -> e.$qName{q.name})
+          }),
+        consASTExpr(e.transform, nilASTExpr()),
+        nilNamedASTExpr())
+    end;
 }
 
 aspect production inhDecoratedAccessHandler
diff --git a/grammars/silver/extension/rewriting/Pattern.sv b/grammars/silver/extension/rewriting/Pattern.sv
index 81d63fb7c..cd8274dfb 100644
--- a/grammars/silver/extension/rewriting/Pattern.sv
+++ b/grammars/silver/extension/rewriting/Pattern.sv
@@ -105,7 +105,37 @@ top::MatchRule ::= pt::PatternList 'when' cond::Expr _ e::Expr
   top.wrappedMatchRuleList =
     [matchRule(
       pt.patternList,
-      just(hackWrapKey(toString(top.ruleIndex) ++ "_cond", cond, location=e.location)),
+      just(pair(hackWrapKey(toString(top.ruleIndex) ++ "_cond", cond, location=e.location), nothing())),
+      hackWrapKey(toString(top.ruleIndex), e, location=e.location),
+      location=top.location)];
+}
+
+aspect production matchRuleWhenMatches_c
+top::MatchRule ::= pt::PatternList 'when' cond::Expr 'matches' p::Pattern _ e::Expr
+{
+  top.transform =
+    require(
+      pt.firstTransform,
+      matchASTExpr(
+        case lookupBy(stringEq, toString(top.ruleIndex) ++ "_cond", top.decRuleExprsIn) of
+        | just(e) -> e.transform
+        | nothing() -> error("Failed to find decorated RHS " ++ toString(top.ruleIndex) ++ "_cond")
+        end,
+        p.transform, booleanASTExpr(true), booleanASTExpr(false))) <*
+    rewriteRule(
+      pt.firstTransform,
+      case lookupBy(stringEq, toString(top.ruleIndex), top.decRuleExprsIn) of
+      | just(e) -> e.transform
+      | nothing() -> error("Failed to find decorated RHS " ++ toString(top.ruleIndex))
+      end);
+  
+  top.isPolymorphic = head(pt.patternList).patternIsVariable || pt.isPolymorphic;
+  pt.typesHaveUniversalVars = [true];
+  
+  top.wrappedMatchRuleList =
+    [matchRule(
+      pt.patternList,
+      just(pair(hackWrapKey(toString(top.ruleIndex) ++ "_cond", cond, location=e.location), just(p))),
       hackWrapKey(toString(top.ruleIndex), e, location=e.location),
       location=top.location)];
 }
@@ -133,7 +163,11 @@ top::PatternList ::= p::Pattern
   top.transform = consASTPattern(p.transform, nilASTPattern());
   top.firstTransform = p.transform;
   top.isPolymorphic = p.isPolymorphic;
-  p.typeHasUniversalVars = head(top.typesHaveUniversalVars);
+  p.typeHasUniversalVars =
+    case top.typesHaveUniversalVars of
+    | h :: _ -> h
+    | _ -> false
+    end;
 }
 aspect production patternList_more
 top::PatternList ::= p::Pattern ',' ps::PatternList
@@ -141,8 +175,16 @@ top::PatternList ::= p::Pattern ',' ps::PatternList
   top.transform = consASTPattern(p.transform, ps.transform);
   top.firstTransform = p.transform;
   top.isPolymorphic = p.isPolymorphic || ps.isPolymorphic;
-  p.typeHasUniversalVars = head(top.typesHaveUniversalVars);
-  ps.typesHaveUniversalVars = tail(top.typesHaveUniversalVars);
+  p.typeHasUniversalVars =
+    case top.typesHaveUniversalVars of
+    | h :: _ -> h
+    | _ -> false
+    end;
+  ps.typesHaveUniversalVars =
+    case top.typesHaveUniversalVars of
+    | _ :: t -> t
+    | _ -> []
+    end;
 }
 
 aspect production patternList_nil
diff --git a/grammars/silver/extension/rewriting/Rewriting.sv b/grammars/silver/extension/rewriting/Rewriting.sv
index 6baf16822..6a95f5e25 100644
--- a/grammars/silver/extension/rewriting/Rewriting.sv
+++ b/grammars/silver/extension/rewriting/Rewriting.sv
@@ -28,15 +28,16 @@ top::Expr ::= 'rewriteWith' '(' s::Expr ',' e::Expr ')'
   errCheckS.finalSubst = top.finalSubst;
   
   local localErrors::[Message] =
-    if errCheckS.typeerror
-    then [err(top.location, "First argument to rewriteWith must be Strategy. Instead got " ++ errCheckS.leftpp)]
-    else [];
+    s.errors ++ e.errors ++ 
+    (if errCheckS.typeerror
+     then [err(top.location, "First argument to rewriteWith must be Strategy. Instead got " ++ errCheckS.leftpp)]
+     else []) ++
+    (if null(getTypeDcl("silver:rewrite:Strategy", top.env))
+     then [err(top.location, "Term rewriting requires import of silver:rewrite")]
+     else []);
   
   -- Can't use an error production here, unfourtunately, due to circular dependency issues.
-  top.errors :=
-    if !null(s.errors ++ e.errors ++ localErrors)
-    then s.errors ++ e.errors ++ localErrors
-    else forward.errors;
+  top.errors := if !null(localErrors) then localErrors else forward.errors;
   
   -- TODO: Equation needed due to weirdness with lets auto-undecorating bindings.
   -- See comments in definition of lexicalLocalReference (grammars/silver/modification/let_fix/Let.sv)
@@ -101,7 +102,11 @@ top::Expr ::= 'traverse' n::QName '(' es::AppExprs ',' anns::AnnoAppExprs ')'
     map(namedArgType(_, nonterminalType("silver:rewrite:Strategy", [])), annotations);
   anns.remainingFuncAnnotations = anns.funcAnnotations;
  
-  local localErrors::[Message] = es.errors ++ anns.traverseErrors;
+  local localErrors::[Message] =
+    es.errors ++ anns.traverseErrors ++
+    if null(getTypeDcl("silver:rewrite:Strategy", top.env))
+    then [err(top.location, "Term rewriting requires import of silver:rewrite")]
+    else [];
 
   es.downSubst = top.downSubst;
   anns.downSubst = es.upSubst;
@@ -265,11 +270,14 @@ top::Expr ::= 'rule' 'on' ty::TypeExpr 'of' Opt_Vbar_t ml::MRuleList 'end'
   ml.ruleIndex = 0;
   ml.decRuleExprsIn = checkExpr.decRuleExprs;
   
+  local localErrors::[Message] =
+    ty.errors ++ ml.errors ++ checkExpr.errors ++
+    if null(getTypeDcl("silver:rewrite:Strategy", top.env))
+    then [err(top.location, "Term rewriting requires import of silver:rewrite")]
+    else [];
+  
   -- Can't use an error production here, unfourtunately, due to circular dependency issues.
-  top.errors :=
-    if !null(ty.errors ++ ml.errors ++ checkExpr.errors)
-    then ty.errors ++ ml.errors ++ checkExpr.errors
-    else forward.errors;
+  top.errors := if !null(localErrors) then localErrors else forward.errors;
   
   checkExpr.downSubst = top.downSubst;
   forward.downSubst = checkExpr.upSubst;
diff --git a/grammars/silver/extension/silverconstruction/Syntax.sv b/grammars/silver/extension/silverconstruction/Syntax.sv
index 0af251a3a..e7021dc71 100644
--- a/grammars/silver/extension/silverconstruction/Syntax.sv
+++ b/grammars/silver/extension/silverconstruction/Syntax.sv
@@ -6,6 +6,7 @@ imports silver:definition:core;
 imports silver:definition:env;
 imports silver:definition:type:syntax;
 imports silver:extension:list;
+imports silver:extension:patternmatching;
 
 concrete production quoteAGDcl
 top::Expr ::= 'Silver_AGDcl' '{' ast::AGDcl '}'
@@ -28,23 +29,55 @@ top::Expr ::= 'Silver_Expr' '{' ast::Expr '}'
   forwards to translate(top.location, reflect(new(ast)));
 }
 
+concrete production quoteExprInh
+top::Expr ::= 'Silver_ExprInh' '{' ast::ExprInh '}'
+{
+  top.unparse = s"Silver_ExprInh {${ast.unparse}}";
+  forwards to translate(top.location, reflect(new(ast)));
+}
+
+concrete production quotePattern
+top::Expr ::= 'Silver_Pattern' '{' ast::Pattern '}'
+{
+  top.unparse = s"Silver_Pattern {${ast.unparse}}";
+  forwards to translate(top.location, reflect(new(ast)));
+}
+
 concrete production antiquoteExpr
 top::Expr ::= '$Expr' '{' e::Expr '}'
 {
   top.unparse = s"$$Expr{${e.unparse}}";
   forwards to
     errorExpr(
-      [err(top.location, "$Expr should not occur outside of Silver_Expr")],
+      [err(top.location, "$Expr should not occur outside of quoted Silver literal")],
       location=top.location);
 }
 
+concrete production antiquoteExprInhs
+top::ExprInhs ::= '$ExprInhs' '{' e::Expr '}'
+{
+  top.unparse = s"$$ExprInhs{${e.unparse}}";
+  -- TODO: [err(top.location, "$ExprInhs should not occur outside of quoted Silver literal")]
+  forwards to exprInhsEmpty(location=top.location);
+}
+
 concrete production antiquoteTypeExpr
 top::TypeExpr ::= '$TypeExpr' '{' e::Expr '}'
 {
   top.unparse = s"$$TypeExpr{${e.unparse}}";
   forwards to
     errorTypeExpr(
-      [err(top.location, "$TypeExpr should not occur outside of Silver_Expr")],
+      [err(top.location, "$TypeExpr should not occur outside of quoted Silver literal")],
+      location=top.location);
+}
+
+concrete production antiquotePattern
+top::Pattern ::= '$Pattern' '{' e::Expr '}'
+{
+  top.unparse = s"$$Pattern{${e.unparse}}";
+  forwards to
+    errorPattern(
+      [err(top.location, "$Pattern should not occur outside of quoted Silver literal")],
       location=top.location);
 }
 
@@ -54,7 +87,19 @@ top::QName ::= '$QName' '{' e::Expr '}'
   top.unparse = s"$$QName{${e.unparse}}";
   forwards to
     qNameError(
-      [err(top.location, "$QName should not occur outside of Silver_Expr")],
+      [err(top.location, "$QName should not occur outside of quoted Silver literal")],
+      location=top.location);
+}
+
+concrete production antiquoteQNameAttrOccur
+top::QNameAttrOccur ::= '$QNameAttrOccur' '{' e::Expr '}'
+{
+  top.unparse = s"$$QNameAttrOccur{${e.unparse}}";
+  forwards to
+    qNameAttrOccur(
+      qNameError(
+        [err(top.location, "$QNameAttrOccur should not occur outside of quoted Silver literal")],
+        location=top.location),
       location=top.location);
 }
 
@@ -62,7 +107,7 @@ concrete production antiquoteName
 top::Name ::= '$Name' '{' e::Expr '}'
 {
   top.unparse = s"$$Name{${e.unparse}}";
-  -- TODO: [err(top.location, "$Name should not occur outside of Silver_Expr")]
+  -- TODO: [err(top.location, "$Name should not occur outside of quoted Silver literal")]
   forwards to name("err", top.location);
 }
 
@@ -80,6 +125,6 @@ concrete production antiquote_name
 top::Name ::= '$name' '{' e::Expr '}'
 {
   top.unparse = s"$$name{${e.unparse}}";
-  -- TODO: [err(top.location, "$Name should not occur outside of Silver_Expr")]
+  -- TODO: [err(top.location, "$Name should not occur outside of quoted Silver literal")]
   forwards to name("err", top.location);
 }
diff --git a/grammars/silver/extension/silverconstruction/Terminals.sv b/grammars/silver/extension/silverconstruction/Terminals.sv
index f43aaa15a..2d8214b8c 100644
--- a/grammars/silver/extension/silverconstruction/Terminals.sv
+++ b/grammars/silver/extension/silverconstruction/Terminals.sv
@@ -1,15 +1,20 @@
 grammar silver:extension:silverconstruction;
 
 marking terminal SilverExpr_t           'Silver_Expr'           lexer classes {KEYWORD, RESERVED};
+marking terminal SilverExprInh_t        'Silver_ExprInh'        lexer classes {KEYWORD, RESERVED};
+marking terminal SilverPattern_t        'Silver_Pattern'        lexer classes {KEYWORD, RESERVED};
 marking terminal SilverAGDcl_t          'Silver_AGDcl'          lexer classes {KEYWORD, RESERVED};
 marking terminal SilverProductionStmt_t 'Silver_ProductionStmt' lexer classes {KEYWORD, RESERVED};
 
 temp_imp_ide_font font_escape color(160, 32, 240) bold italic;
-lexer class Escape font=font_escape;
+lexer class Antiquote font=font_escape;
 
-terminal EscapeExpr_t              '$Expr'              lexer classes {Escape};
-terminal EscapeTypeExpr_t          '$TypeExpr'          lexer classes {Escape};
-terminal EscapeQName_t             '$QName'             lexer classes {Escape};
-terminal EscapeName_t              '$Name'              lexer classes {Escape};
-terminal Escape_qName_t            '$qName'             lexer classes {Escape};
-terminal Escape_name_t             '$name'              lexer classes {Escape};
+terminal AntiquoteExpr_t              '$Expr'              lexer classes {Antiquote};
+terminal AntiquoteExprInhs_t          '$ExprInhs'          lexer classes {Antiquote};
+terminal AntiquoteTypeExpr_t          '$TypeExpr'          lexer classes {Antiquote};
+terminal AntiquotePattern_t           '$Pattern'           lexer classes {Antiquote};
+terminal AntiquoteQName_t             '$QName'             lexer classes {Antiquote};
+terminal AntiquoteQNameAttrOccur_t    '$QNameAttrOccur'    lexer classes {Antiquote};
+terminal AntiquoteName_t              '$Name'              lexer classes {Antiquote};
+terminal Antiquote_qName_t            '$qName'             lexer classes {Antiquote};
+terminal Antiquote_name_t             '$name'              lexer classes {Antiquote};
diff --git a/grammars/silver/extension/silverconstruction/Translation.sv b/grammars/silver/extension/silverconstruction/Translation.sv
index 8a16aac42..a82b53598 100644
--- a/grammars/silver/extension/silverconstruction/Translation.sv
+++ b/grammars/silver/extension/silverconstruction/Translation.sv
@@ -8,8 +8,11 @@ top::AST ::= prodName::String children::ASTs annotations::NamedASTs
 {
   directAntiquoteProductions <-
     ["silver:extension:silverconstruction:antiquoteExpr",
+     "silver:extension:silverconstruction:antiquoteExprInhs",
      "silver:extension:silverconstruction:antiquoteTypeExpr",
+     "silver:extension:silverconstruction:antiquotePattern",
      "silver:extension:silverconstruction:antiquoteQName",
+     "silver:extension:silverconstruction:antiquoteQNameAttrOccur",
      "silver:extension:silverconstruction:antiquoteName"];
   
   -- "Indirect" antiquote productions
diff --git a/grammars/silver/extension/strategyattr/ConcreteSyntax.sv b/grammars/silver/extension/strategyattr/ConcreteSyntax.sv
new file mode 100644
index 000000000..eae5b0ab4
--- /dev/null
+++ b/grammars/silver/extension/strategyattr/ConcreteSyntax.sv
@@ -0,0 +1,241 @@
+grammar silver:extension:strategyattr;
+
+inherited attribute givenGenName::String;
+
+concrete production partialStrategyAttributeDcl
+top::AGDcl ::= 'partial' 'strategy' 'attribute' a::Name '=' e::StrategyExpr_c ';'
+{
+  top.unparse = "strategy attribute " ++ a.unparse ++ "=" ++ e.unparse ++ ";";
+  e.givenGenName = a.name;
+  forwards to strategyAttributeDcl(false, a, [], [], e.ast, location=top.location);
+}
+
+concrete production totalStrategyAttributeDcl
+top::AGDcl ::= 'strategy' 'attribute' a::Name '=' e::StrategyExpr_c ';'
+{
+  top.unparse = "strategy attribute " ++ a.unparse ++ "=" ++ e.unparse ++ ";";
+  e.givenGenName = a.name;
+  forwards to strategyAttributeDcl(true, a, [], [], e.ast, location=top.location);
+}
+
+closed nonterminal StrategyExpr_c with location, givenGenName, unparse, ast<StrategyExpr>;
+
+concrete productions top::StrategyExpr_c
+| 'id'
+{
+  top.unparse = "id";
+  top.ast = id(genName=top.givenGenName, location=top.location);
+}
+| 'fail'
+{
+  top.unparse = "fail";
+  top.ast = fail(genName=top.givenGenName, location=top.location);
+}
+| s1::StrategyExpr_c '<*' s2::StrategyExpr_c
+{
+  top.unparse = s"(${s1.unparse} <* ${s2.unparse})";
+  top.ast = sequence(s1.ast, s2.ast, genName=top.givenGenName, location=top.location);
+  s1.givenGenName = top.givenGenName ++ "_fst";
+  s2.givenGenName = top.givenGenName ++ "_snd";
+}
+| s1::StrategyExpr_c '<+' s2::StrategyExpr_c
+{
+  top.unparse = s"(${s1.unparse} <+ ${s2.unparse})";
+  top.ast = choice(s1.ast, s2.ast, genName=top.givenGenName, location=top.location);
+  s1.givenGenName = top.givenGenName ++ "_left";
+  s2.givenGenName = top.givenGenName ++ "_right";
+}
+| 'all' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"all(${s.unparse})";
+  top.ast = allTraversal(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_all_arg";
+}
+| 'some' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"some(${s.unparse})";
+  top.ast = someTraversal(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_some_arg";
+}
+| 'one' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"one(${s.unparse})";
+  top.ast = oneTraversal(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_one_arg";
+}
+| id::StrategyQName '(' s::StrategyExprs_c ')'
+{
+  top.unparse = s"${id.ast.unparse}(${s.unparse})";
+  top.ast = prodTraversal(id.ast, s.ast, genName=top.givenGenName, location=top.location);
+  s.index = 1;
+  s.givenGenName = top.givenGenName ++ "_" ++ id.ast.name;
+}
+| 'rec' n::Name Arrow_t s::StrategyExpr_c
+{
+  top.unparse = s"rec ${n.name} -> (${s.unparse})";
+  top.ast = recComb(n, s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName;
+}
+| 'rule' 'on' id::Name '::' ty::TypeExpr 'of' Opt_Vbar_t ml::MRuleList 'end'
+{
+  top.unparse = "rule on " ++ id.unparse ++ "::" ++ ty.unparse ++ " of " ++ ml.unparse ++ " end";
+  top.ast = rewriteRule(id, ty, ml, genName=top.givenGenName, location=top.location);
+}
+| 'rule' 'on' ty::TypeExpr 'of' Opt_Vbar_t ml::MRuleList 'end'
+{
+  top.unparse = "rule on " ++ ty.unparse ++ " of " ++ ml.unparse ++ " end";
+  top.ast = rewriteRule(name("top", top.location), ty, ml, genName=top.givenGenName, location=top.location);
+}
+| id::StrategyQName
+{
+  top.unparse = id.ast.unparse;
+  top.ast = nameRef(id.ast, genName=top.givenGenName, location=top.location);
+}
+| '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"(${s.unparse})";
+  top.ast = s.ast;
+  s.givenGenName = top.givenGenName;
+}
+| 'printTerm'
+{
+  top.unparse = s"printTerm";
+  top.ast = printTerm(genName=top.givenGenName, location=top.location);
+}
+| 'try' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"try(${s.unparse})";
+  top.ast = try(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_try_arg";
+}
+| 'repeat' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"repeat(${s.unparse})";
+  top.ast = repeatS(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_repeat_arg";
+}
+| 'reduce' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"reduce(${s.unparse})";
+  top.ast = reduce(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_reduce_arg";
+}
+| 'bottomUp' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"bottomUp(${s.unparse})";
+  top.ast = bottomUp(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_bottomUp_arg";
+}
+| 'topDown' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"topDown(${s.unparse})";
+  top.ast = topDown(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_topDown_arg";
+}
+| 'downUp' '(' s1::StrategyExpr_c ',' s2::StrategyExpr_c ')'
+{
+  top.unparse = s"downUp(${s1.unparse}, ${s2.unparse})";
+  top.ast = downUp(s1.ast, s2.ast, genName=top.givenGenName, location=top.location);
+  s1.givenGenName = top.givenGenName ++ "_downUp_arg1";
+  s2.givenGenName = top.givenGenName ++ "_downUp_arg2";
+}
+| 'allBottomUp' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"allBottomUp(${s.unparse})";
+  top.ast = allBottomUp(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_allBottomUp_arg";
+}
+| 'allTopDown' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"allTopDown(${s.unparse})";
+  top.ast = allTopDown(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_allTopDown_arg";
+}
+| 'allDownUp' '(' s1::StrategyExpr_c ',' s2::StrategyExpr_c ')'
+{
+  top.unparse = s"allDownUp(${s1.unparse}, ${s2.unparse})";
+  top.ast = allDownUp(s1.ast, s2.ast, genName=top.givenGenName, location=top.location);
+  s1.givenGenName = top.givenGenName ++ "_allDownUp_arg1";
+  s2.givenGenName = top.givenGenName ++ "_allDownUp_arg2";
+}
+| 'someBottomUp' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"someBottomUp(${s.unparse})";
+  top.ast = someBottomUp(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_someBottomUp_arg";
+}
+| 'someTopDown' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"someTopDown(${s.unparse})";
+  top.ast = someTopDown(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_someTopDown_arg";
+}
+| 'someDownUp' '(' s1::StrategyExpr_c ',' s2::StrategyExpr_c ')'
+{
+  top.unparse = s"someDownUp(${s1.unparse}, ${s2.unparse})";
+  top.ast = someDownUp(s1.ast, s2.ast, genName=top.givenGenName, location=top.location);
+  s1.givenGenName = top.givenGenName ++ "_someDownUp_arg1";
+  s2.givenGenName = top.givenGenName ++ "_someDownUp_arg2";
+}
+| 'onceBottomUp' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"onceBottomUp(${s.unparse})";
+  top.ast = onceBottomUp(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_onceBottomUp_arg";
+}
+| 'onceTopDown' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"onceTopDown(${s.unparse})";
+  top.ast = onceTopDown(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_onceTopDown_arg";
+}
+| 'onceDownUp' '(' s1::StrategyExpr_c ',' s2::StrategyExpr_c ')'
+{
+  top.unparse = s"onceDownUp(${s1.unparse}, ${s2.unparse})";
+  top.ast = onceDownUp(s1.ast, s2.ast, genName=top.givenGenName, location=top.location);
+  s1.givenGenName = top.givenGenName ++ "_onceDownUp_arg1";
+  s2.givenGenName = top.givenGenName ++ "_onceDownUp_arg2";
+}
+| 'innermost' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"innermost(${s.unparse})";
+  top.ast = innermost(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_innermost_arg";
+}
+| 'outermost' '(' s::StrategyExpr_c ')'
+{
+  top.unparse = s"outermost(${s.unparse})";
+  top.ast = outermost(s.ast, genName=top.givenGenName, location=top.location);
+  s.givenGenName = top.givenGenName ++ "_outermost_arg";
+}
+
+autocopy attribute index::Integer;
+
+nonterminal StrategyExprs_c with location, index, givenGenName, unparse, ast<StrategyExprs>;
+concrete productions top::StrategyExprs_c
+| h::StrategyExpr_c ',' t::StrategyExprs_c
+{
+  top.unparse = h.unparse ++ ", " ++ t.unparse;
+  top.ast = consStrategyExpr(h.ast, t.ast);
+  h.givenGenName = top.givenGenName ++ "_arg" ++ toString(top.index);
+  t.givenGenName = top.givenGenName;
+  t.index = top.index + 1;
+}
+| h::StrategyExpr_c
+{
+  top.unparse = h.unparse;
+  top.ast = consStrategyExpr(h.ast, nilStrategyExpr());
+  h.givenGenName = top.givenGenName ++ "_arg" ++ toString(top.index);
+}
+|
+{
+  top.unparse = "";
+  top.ast = nilStrategyExpr();
+}
+
+nonterminal StrategyQName with location, ast<QName>;
+concrete productions top::StrategyQName
+(strategyQNameOne) | id::StrategyName_t
+{ top.ast = qNameId(name(id.lexeme, id.location), location=top.location); }
+(strategyQNameCons) | id::StrategyName_t ':' qn::StrategyQName
+{ top.ast = qNameCons(name(id.lexeme, id.location), $2, qn.ast, location=top.location); }
diff --git a/grammars/silver/extension/strategyattr/DclInfo.sv b/grammars/silver/extension/strategyattr/DclInfo.sv
new file mode 100644
index 000000000..5113958e7
--- /dev/null
+++ b/grammars/silver/extension/strategyattr/DclInfo.sv
@@ -0,0 +1,58 @@
+grammar silver:extension:strategyattr;
+
+synthesized attribute isStrategy::Boolean occurs on DclInfo;
+attribute isTotal occurs on DclInfo;
+synthesized attribute containsErrors::Boolean occurs on DclInfo;
+synthesized attribute liftedStrategyNames::[String] occurs on DclInfo;
+synthesized attribute givenRecVarNameEnv::[Pair<String String>] occurs on DclInfo;
+synthesized attribute givenRecVarTotalEnv::[Pair<String Boolean>] occurs on DclInfo;
+attribute partialRefs, totalRefs occurs on DclInfo;
+synthesized attribute strategyExpr :: StrategyExpr occurs on DclInfo;
+
+aspect default production
+top::DclInfo ::=
+{
+  top.isStrategy = false;
+  top.isTotal = true;
+  top.containsErrors = false;
+  top.liftedStrategyNames = [];
+  top.givenRecVarNameEnv = [];
+  top.givenRecVarTotalEnv = [];
+  top.partialRefs := [];
+  top.totalRefs := [];
+  top.strategyExpr = error("Internal compiler error: must be defined for all strategy attribute declarations");
+}
+
+abstract production strategyDcl
+top::DclInfo ::=
+  sg::String sl::Location fn::String isTotal::Boolean tyVar::TyVar
+  containsErrors::Boolean liftedStrategyNames::[String] givenRecVarNameEnv::[Pair<String String>] givenRecVarTotalEnv::[Pair<String Boolean>] partialRefs::[String] totalRefs::[String]
+  e::StrategyExpr
+{
+  top.sourceGrammar = sg;
+  top.sourceLocation = sl;
+  top.fullName = fn;
+
+  top.typerep =
+    if isTotal
+    then varType(tyVar)
+    else nonterminalType("core:Maybe", [varType(tyVar)]);
+  top.dclBoundVars = [tyVar];
+  top.isSynthesized = true;
+  top.isStrategy = true;
+  
+  top.decoratedAccessHandler = synDecoratedAccessHandler(_, _, location=_);
+  top.undecoratedAccessHandler = accessBounceDecorate(synDecoratedAccessHandler(_, _, location=_), _, _, _);
+  top.attrDefDispatcher = synthesizedAttributeDef(_, _, _, location=_); -- Allow normal syn equations
+  top.attributionDispatcher = strategyAttributionDcl(_, _, _, _, location=_);
+  top.propagateDispatcher = propagateStrategy(_, location=_);
+  
+  top.isTotal = isTotal;
+  top.containsErrors = containsErrors;
+  top.liftedStrategyNames = liftedStrategyNames;
+  top.givenRecVarNameEnv = givenRecVarNameEnv;
+  top.givenRecVarTotalEnv = givenRecVarTotalEnv;
+  top.partialRefs := partialRefs;
+  top.totalRefs := totalRefs;
+  top.strategyExpr = e;
+}
diff --git a/grammars/silver/extension/strategyattr/Project.sv b/grammars/silver/extension/strategyattr/Project.sv
new file mode 100644
index 000000000..49a1ffc1a
--- /dev/null
+++ b/grammars/silver/extension/strategyattr/Project.sv
@@ -0,0 +1,16 @@
+grammar silver:extension:strategyattr;
+
+imports silver:definition:core;
+imports silver:definition:env;
+imports silver:definition:type;
+imports silver:definition:type:syntax;
+imports silver:extension:autoattr;
+imports silver:extension:patternmatching;
+imports silver:extension:list;
+--imports silver:extension:rewriting;
+imports silver:extension:silverconstruction;
+imports silver:modification:let_fix;
+imports silver:modification:lambda_fn;
+
+exports silver:extension:strategyattr:convenience;
+exports silver:extension:strategyattr:construction;
diff --git a/grammars/silver/extension/strategyattr/Strategy.sv b/grammars/silver/extension/strategyattr/Strategy.sv
new file mode 100644
index 000000000..495953e8b
--- /dev/null
+++ b/grammars/silver/extension/strategyattr/Strategy.sv
@@ -0,0 +1,179 @@
+grammar silver:extension:strategyattr;
+
+import silver:definition:flow:driver only ProductionGraph, FlowType, constructAnonymousGraph;
+import silver:driver:util;
+
+abstract production strategyAttributeDcl
+top::AGDcl ::= isTotal::Boolean a::Name recVarNameEnv::[Pair<String String>] recVarTotalEnv::[Pair<String Boolean>] e::StrategyExpr
+{
+  top.unparse = (if isTotal then "" else "partial ") ++ "strategy attribute " ++ a.unparse ++ "=" ++ e.unparse ++ ";";
+
+  production attribute fName :: String;
+  fName = top.grammarName ++ ":" ++ a.name;
+  
+  -- Define these directly to avoid circular dependencies,
+  -- since the forward contributes to the env.
+  propagate errors, moduleNames;
+  
+  top.errors <-
+    if length(getAttrDclAll(fName, top.env)) > 1
+    then [err(a.location, "Attribute '" ++ fName ++ "' is already bound.")]
+    else [];
+  top.errors <-
+    if null(getValueDcl("core:monad:bindMaybe", top.env))
+    then [err(top.location, "Strategy attributes require import of core:monad")]
+    else [];
+  top.errors <-
+    if isTotal && !e.isTotal
+    -- Not an error since we can still translate this, but the translation may raise run-time errors in case of failure
+    then [wrn(e.location, s"Implementation of total strategy ${a.name} is not total")]
+    else []; 
+  
+  -- Frame doesn't really matter, since we will re-check any expressions occuring in e when propagated.
+  -- Need all this to construct a bogus frame...
+  local myFlow :: EnvTree<FlowType> = head(searchEnvTree(top.grammarName, top.compiledGrammars)).grammarFlowTypes;
+  local myProds :: EnvTree<ProductionGraph> = head(searchEnvTree(top.grammarName, top.compiledGrammars)).productionFlowGraphs;
+  local myFlowGraph :: ProductionGraph = 
+    constructAnonymousGraph(e.flowDefs, top.env, myProds, myFlow);
+  e.frame = globalExprContext(myFlowGraph);
+  
+  e.recVarNameEnv = recVarNameEnv;
+  e.recVarTotalEnv = recVarTotalEnv;
+  e.outerAttr = just(a.name);
+  
+  local fwrd::AGDcl =
+    foldr(
+      appendAGDcl(_, _, location=top.location),
+      defsAGDcl(
+        [attrDef(
+           defaultEnvItem(
+             strategyDcl(
+               top.grammarName, a.location, fName, isTotal, freshTyVar(),
+               !null(top.errors), map(fst, e.liftedStrategies), recVarNameEnv, recVarTotalEnv, e.partialRefs, e.totalRefs, e)))],
+        location=top.location),
+      map(
+        \ d::Pair<String Decorated StrategyExpr> ->
+          strategyAttributeDcl(
+            d.snd.isTotal, name(d.fst, top.location), d.snd.recVarNameEnv, d.snd.recVarTotalEnv, new(d.snd),
+            location=top.location),
+        decorate e with {
+          env = emptyEnv(); -- Forward (and thus lifting) cannot depend on top.env to avoid circular dependency
+          config = e.config; grammarName = e.grammarName; recVarNameEnv = recVarNameEnv; recVarTotalEnv = recVarTotalEnv; outerAttr = e.outerAttr;
+        }.liftedStrategies));
+  
+  -- Uncomment for debugging
+  --forwards to unsafeTrace(fwrd, print(a.name ++ " = " ++ e.unparse ++ "; lifted  " ++ implode(",  ", map(fst, e.liftedStrategies)) ++ "\n\n", unsafeIO()));
+  
+  -- Flow errors here due to exceeding the allowable host forward flow type.
+  -- I'm not actually sure where we depend on flowEnv, config or compiledGrammars.
+  -- This could be fixed by seeding the host flow type or tracking down those dependencies and substituting dummy values.
+  forwards to fwrd;
+}
+
+abstract production strategyAttributionDcl
+top::AGDcl ::= at::Decorated QName attl::BracketedOptTypeExprs nt::QName nttl::BracketedOptTypeExprs
+{
+  production attribute localErrors::[Message] with ++;
+  localErrors :=
+    attl.errors ++ attl.errorsTyVars ++ nt.lookupType.errors ++ nttl.errors ++ nttl.errorsTyVars;
+  localErrors <-
+    if length(attl.types) > 0
+    then [err(attl.location, "Explicit type arguments are not allowed for strategy attributes")]
+    else [];
+  
+  -- Technically we could do this check on the propagate, but it seems clearer to raise it here
+  localErrors <-
+    flatMap(
+      \ totalAttr::String ->
+        if null(getOccursDcl(totalAttr, nt.lookupType.fullName, top.env))
+        then [err(top.location, s"Total strategy attribute ${totalAttr} referenced by ${at.name} does not occur on ${nt.name}")]
+        else [],
+      nubBy(stringEq, at.lookupAttribute.dcl.totalRefs));
+  
+  -- TODO: Check that the type parameters of any rules of type nt match nttl
+  
+  top.errors := if !null(localErrors) then localErrors else forward.errors;
+
+  forwards to
+    foldr(
+      appendAGDcl(_, _, location=top.location),
+      defaultAttributionDcl(
+        at,
+        botlSome(
+          '<',
+          typeListSingle(
+            nominalTypeExpr(nt.qNameType, nttl, location=top.location),
+            location=top.location),
+          '>', location=top.location),
+        nt, nttl,
+        location=top.location),
+      map(
+        \ n::String ->
+          attributionDcl(
+            'attribute', qName(top.location, n), attl, 'occurs', 'on', nt, nttl, ';',
+            location=top.location),
+        at.lookupAttribute.dcl.liftedStrategyNames));
+}
+
+{--
+ - Propagate a strategy attribute on the enclosing production
+ - @param attr  The name of the attribute to propagate
+ -}
+abstract production propagateStrategy
+top::ProductionStmt ::= attr::Decorated QName
+{
+  top.unparse = s"propagate ${attr.unparse}";
+  
+  production isTotal::Boolean = attr.lookupAttribute.dcl.isTotal;
+  production e::StrategyExpr = attr.lookupAttribute.dcl.strategyExpr;
+  e.grammarName = top.grammarName;
+  e.config = top.config;
+  e.frame = top.frame;
+  e.env = top.env;
+  e.recVarNameEnv = attr.lookupAttribute.dcl.givenRecVarNameEnv;
+  e.recVarTotalEnv = attr.lookupAttribute.dcl.givenRecVarTotalEnv;
+  e.outerAttr = just(attr.lookupAttribute.fullName);
+  e.inlinedStrategies = [attr.lookupAttribute.fullName]; -- Don't unfold the top-level strategy within itself
+  
+  production e2::StrategyExpr = e.optimize;
+  e2.grammarName = e.grammarName;
+  e2.config = e.config;
+  e2.frame = e.frame;
+  e2.env = e.env;
+  e2.recVarNameEnv = e.recVarNameEnv;
+  e2.recVarTotalEnv = e.recVarTotalEnv;
+  e2.outerAttr = e.outerAttr;
+  e2.inlinedStrategies = e.inlinedStrategies;
+  
+  -- Can't do this with forwarding to avoid circular dependency of
+  -- forward -> dcl.containsErrors -> dcl.flowEnv -> forward.flowDefs
+  top.errors :=
+    if
+      -- Check for errors in this or inlined strategy expressions that would be reported on the attribute definition
+      attr.lookupAttribute.dcl.containsErrors ||
+      any(map((.containsErrors), flatMap(getAttrDcl(_, top.env), attr.lookupAttribute.dcl.partialRefs))) ||
+      -- Check for total strategy ref occurs errors that would already be reported on the occurence
+      (!null(getOccursDcl(attr.lookupAttribute.fullName, top.frame.signature.outputElement.typerep.typeName, top.env)) &&
+       any(map(null, map(getOccursDcl(_, top.frame.signature.outputElement.typerep.typeName, top.env), attr.lookupAttribute.dcl.totalRefs))))
+    then []
+    else forward.errors;
+  
+  local fwrd::ProductionStmt =
+    foldr(
+      productionStmtAppend(_, _, location=top.location),
+      attributeDef(
+        concreteDefLHS(qName(top.location, top.frame.signature.outputElement.elementName), location=top.location),
+        '.',
+        qNameAttrOccur(new(attr), location=top.location),
+        '=',
+        if isTotal then e2.totalTranslation else e2.partialTranslation,
+        ';',
+        location=top.location),
+      map(
+        \ n::String -> propagateOneAttr(qName(top.location, n), location=top.location),
+        attr.lookupAttribute.dcl.liftedStrategyNames));
+  
+  -- Uncomment for debugging
+  --forwards to unsafeTrace(fwrd, print(attr.name ++ " on " ++ top.frame.fullName ++ " = " ++ (if isTotal then e2.totalTranslation else e2.partialTranslation).unparse ++ ";\n\n", unsafeIO()));
+  forwards to fwrd;
+}
diff --git a/grammars/silver/extension/strategyattr/StrategyExpr.sv b/grammars/silver/extension/strategyattr/StrategyExpr.sv
new file mode 100644
index 000000000..bba3109c7
--- /dev/null
+++ b/grammars/silver/extension/strategyattr/StrategyExpr.sv
@@ -0,0 +1,994 @@
+grammar silver:extension:strategyattr;
+
+import silver:metatranslation;
+import core:monad;
+
+annotation genName::String; -- Used to generate the names of lifted strategy attributes
+
+autocopy attribute recVarNameEnv::[Pair<String String>]; -- name, (isTotal, genName)
+autocopy attribute recVarTotalEnv::[Pair<String Boolean>]; -- name, (isTotal, genName)
+inherited attribute outerAttr::Maybe<String>;
+autocopy attribute inlinedStrategies::[String];
+monoid attribute liftedStrategies::[Pair<String Decorated StrategyExpr>] with [], ++;
+synthesized attribute attrRefName::Maybe<String>;
+synthesized attribute isId::Boolean;
+synthesized attribute isTotal::Boolean;
+inherited attribute givenInputElements::[NamedSignatureElement];
+synthesized attribute attrRefNames::[Maybe<String>];
+monoid attribute containsFail::Boolean with false, ||;
+monoid attribute allId::Boolean with true, &&;
+monoid attribute freeRecVars::[String] with [], ++;
+monoid attribute partialRefs::[String] with [], ++;
+monoid attribute totalRefs::[String] with [], ++;
+monoid attribute matchesFrame::Boolean with false, ||;
+
+synthesized attribute partialTranslation::Expr; -- Maybe<a> on a
+synthesized attribute totalTranslation::Expr; -- a on a, can raise a runtime error if demanded on partial strategy expression
+
+-- Nonterminal-independent algebraic simplifications
+-- Theoretically these could be applied to the strategy before lifting/propagation,
+-- but probably not much of an improvement.
+partial strategy attribute genericStep =
+  rule on top::StrategyExpr of
+  | sequence(fail(), _) -> fail(location=top.location, genName=top.genName)
+  | sequence(_, fail()) -> fail(location=top.location, genName=top.genName)
+  | sequence(id(), s) -> s
+  | sequence(s, id()) -> s
+  | choice(fail(), s) -> s
+  | choice(s, fail()) -> s
+  | choice(s, _) when s.isTotal -> s
+  | allTraversal(id()) -> id(location=top.location, genName=top.genName)
+  | someTraversal(fail()) -> fail(location=top.location, genName=top.genName)
+  | oneTraversal(fail()) -> fail(location=top.location, genName=top.genName)
+  | prodTraversal(_, ss) when ss.containsFail -> fail(location=top.location, genName=top.genName)
+  | prodTraversal(_, ss) when ss.allId -> id(location=top.location, genName=top.genName)
+  | recComb(n, s) when !containsBy(stringEq, n.name, s.freeRecVars) -> s
+  | inlined(_, fail()) -> fail(location=top.location, genName=top.genName)
+  end;
+-- Nonterminal-dependent, production-independent optimizations
+partial strategy attribute ntStep =
+  rule on top::StrategyExpr of
+  -- Only inline references to partial strategies, as inlining total
+  -- strategies would not permit any additional simplification.
+  | partialRef(n) when
+      n.matchesFrame && n.attrDcl.isStrategy &&
+      !containsBy(stringEq, n.attrDcl.fullName, top.inlinedStrategies) &&
+      null(n.attrDcl.givenRecVarNameEnv) ->
+    inlined(n, n.attrDcl.strategyExpr, location=top.location, genName=top.genName)
+  | partialRef(n) when !n.matchesFrame -> fail(location=top.location, genName=top.genName)
+  | inlined(n, _) when !n.matchesFrame -> fail(location=top.location, genName=top.genName)
+  | inlined(n, id()) when n.matchesFrame -> id(location=top.location, genName=top.genName)
+  | inlined(n1, totalRef(n2)) when n1.matchesFrame -> totalRef(n2, location=top.location, genName=top.genName)
+  end;
+-- Production-dependent optimizations
+partial strategy attribute prodStep =
+  rule on top::StrategyExpr of
+  | allTraversal(s) when !attrMatchesChild(top.env, fromMaybe(s.genName, s.attrRefName), top.frame) -> id(location=top.location, genName=top.genName)
+  | someTraversal(s) when !attrMatchesChild(top.env, fromMaybe(s.genName, s.attrRefName), top.frame) -> fail(location=top.location, genName=top.genName)
+  | oneTraversal(s) when !attrMatchesChild(top.env, fromMaybe(s.genName, s.attrRefName), top.frame) -> fail(location=top.location, genName=top.genName)
+  | prodTraversal(p, s) when p.lookupValue.fullName != top.frame.fullName -> fail(location=top.location, genName=top.genName)
+  | rewriteRule(_, _, ml) when !ml.matchesFrame -> fail(location=top.location, genName=top.genName)
+  end <+
+  rewriteRule(
+    id, id,
+    onceBottomUp(
+      rule on top::MRuleList of
+      | mRuleList_cons(h, _, t) when !h.matchesFrame -> t
+      | mRuleList_cons(h, _, mRuleList_one(t)) when !t.matchesFrame -> mRuleList_one(h, location=top.location)
+      end));
+attribute prodStep occurs on MRuleList;
+
+strategy attribute simplify = innermost(genericStep <+ ntStep);
+strategy attribute optimize =
+  (sequence(optimize, simplify) <+
+   choice(optimize, optimize) <+
+   allTraversal(simplify) <+
+   someTraversal(simplify) <+
+   oneTraversal(simplify) <+
+   prodTraversal(id, simplify) <+
+   recComb(id, optimize) <+
+   inlined(id, optimize) <+
+   id) <*
+  try((genericStep <+ ntStep <+ prodStep) <* optimize);
+
+nonterminal StrategyExpr with
+  config, grammarName, env, location, unparse, errors, frame, compiledGrammars, flowEnv, flowDefs, -- Normal expression stuff
+  genName, outerAttr, recVarNameEnv, recVarTotalEnv, liftedStrategies, attrRefName, isId, isTotal, freeRecVars, partialRefs, totalRefs, -- Frame-independent attrs
+  partialTranslation, totalTranslation, matchesFrame, -- Frame-dependent attrs
+  inlinedStrategies, genericStep, ntStep, prodStep, simplify, optimize; -- Optimization stuff
+
+nonterminal StrategyExprs with
+  config, grammarName, env, unparse, errors, frame, compiledGrammars, flowEnv, flowDefs, -- Normal expression stuff
+  recVarNameEnv, recVarTotalEnv, givenInputElements, liftedStrategies, attrRefNames, containsFail, allId, freeRecVars, partialRefs, totalRefs, -- Frame-independent attrs
+  inlinedStrategies, simplify; -- Optimization stuff
+
+flowtype StrategyExpr =
+  decorate {env, grammarName, config, recVarNameEnv, recVarTotalEnv, outerAttr}, -- NOT frame
+  -- Normal expression stuff
+  unparse {}, errors {decorate, frame, compiledGrammars, flowEnv}, flowDefs {decorate, frame, compiledGrammars, flowEnv},
+  -- Frame-independent attrs
+  liftedStrategies {decorate}, attrRefName {decorate}, isId {decorate}, isTotal {decorate}, freeRecVars {decorate}, partialRefs {decorate}, totalRefs {decorate},
+  -- Frame-dependent attrs
+  partialTranslation {decorate, frame}, totalTranslation {decorate, frame}, matchesFrame {decorate, frame};
+
+flowtype StrategyExprs =
+  decorate {env, grammarName, config, recVarNameEnv, recVarTotalEnv}, -- NOT frame
+  -- Normal expression stuff
+  unparse {}, errors {decorate, frame, givenInputElements, compiledGrammars, flowEnv}, flowDefs {decorate, frame, compiledGrammars, flowEnv},
+  -- Frame-independent attrs
+  liftedStrategies {decorate}, attrRefNames {decorate, givenInputElements},
+  containsFail {decorate}, allId {decorate}, freeRecVars {decorate}, partialRefs {decorate}, totalRefs {decorate};
+
+propagate errors on StrategyExpr, StrategyExprs excluding partialRef, totalRef;
+propagate flowDefs on StrategyExpr, StrategyExprs;
+propagate containsFail, allId on StrategyExprs;
+propagate freeRecVars on StrategyExpr, StrategyExprs excluding recComb;
+propagate partialRefs, totalRefs on StrategyExpr, StrategyExprs;
+propagate simplify on StrategyExprs;
+propagate prodStep on MRuleList;
+propagate genericStep, ntStep, prodStep, simplify, optimize on StrategyExpr;
+
+-- Convert an expression of type a to Maybe<a>
+function asPartial
+Expr ::= e::Expr
+{ return Silver_Expr { core:just($Expr{e}) }; }
+
+-- Convert an expression of type Maybe<a> to a
+function asTotal
+Expr ::= t::Type e::Expr
+{
+  return
+    Silver_Expr {
+      let res::$TypeExpr{typerepTypeExpr(t, location=e.location)} =
+          core:error("Total result demanded when partial strategy failed")
+      in core:fromMaybe(res, $Expr{e})
+      end
+    };
+}
+
+aspect default production
+top::StrategyExpr ::=
+{
+  -- At least 1 of these should be defined for every production:
+  top.partialTranslation = asPartial(top.totalTranslation);
+  top.totalTranslation = asTotal(top.frame.signature.outputElement.typerep, top.partialTranslation);
+  
+  top.attrRefName = nothing();
+  top.matchesFrame := true; -- Consulted only when attrRefName is just(...)
+  top.isId = false;
+  top.isTotal = false;
+}
+
+-- Basic combinators
+abstract production id
+top::StrategyExpr ::=
+{
+  top.unparse = "id";
+  propagate liftedStrategies;
+  top.isId = true;
+  top.isTotal = true;
+  top.totalTranslation = Silver_Expr { $name{top.frame.signature.outputElement.elementName} };
+}
+
+abstract production fail
+top::StrategyExpr ::=
+{
+  top.unparse = "fail";
+  propagate liftedStrategies;
+  top.partialTranslation = Silver_Expr { core:nothing() };
+}
+
+abstract production sequence
+top::StrategyExpr ::= s1::StrategyExpr s2::StrategyExpr
+{
+  top.unparse = s"(${s1.unparse} <* ${s2.unparse})";
+  
+  local s2Name::String = fromMaybe(top.genName ++ "_snd", s2.attrRefName);
+  local s2Total::Boolean = attrIsTotal(top.env, s2Name); -- Can differ from s2.isTotal because we lift without env
+  top.liftedStrategies :=
+    s1.liftedStrategies ++
+    if s2.attrRefName.isJust
+    then []
+    else [pair(s2Name, s2)];
+  top.isTotal = s1.isTotal && s2.isTotal;
+  
+  s1.outerAttr = nothing();
+  s2.outerAttr = nothing();
+  
+  -- Equations for all inh attributes on the nt that we know about.
+  -- This is safe because the MWDA requires that all inh dependencies of a syn attribute
+  -- be exported by the syn occurence anyway.
+  -- TODO - future optimization potential: this is where common sub-trees shared between
+  -- the incoming tree and the result of s1 get re-decorated.
+  local allInhs::ExprInhs =
+    foldr(
+      exprInhsCons(_, _, location=top.location),
+      exprInhsEmpty(location=top.location),
+      map(
+        \ a::DclInfo ->
+          Silver_ExprInh {
+            $name{a.fullName} = $name{top.frame.signature.outputElement.elementName}.$name{a.fullName};
+          },
+        filter(
+          (.isInherited),
+          flatMap(
+            getAttrDcl(_, top.env),
+            map((.attrOccurring), getAttrsOn(top.frame.lhsNtName, top.env))))));
+  top.partialTranslation =
+    -- Optimizations when one or both of these is total, in this case a
+    -- monadic bind may not be required.
+    case s1.isTotal, s2Total of
+    | true, true ->
+      Silver_Expr {
+        core:just(decorate $Expr{s1.totalTranslation} with { $ExprInhs{allInhs} }.$name{s2Name})
+      }
+    | true, false ->
+      Silver_Expr {
+        decorate $Expr{s1.totalTranslation} with { $ExprInhs{allInhs} }.$name{s2Name}
+      }
+    | false, true ->
+      Silver_Expr {
+        core:mapMaybe(
+          \ res::$TypeExpr{typerepTypeExpr(top.frame.signature.outputElement.typerep, location=top.location)} ->
+            decorate res with { $ExprInhs{allInhs} }.$name{s2Name},
+          $Expr{s1.partialTranslation})
+      }
+    | false, false ->
+      Silver_Expr {
+        core:monad:bindMaybe(
+          $Expr{s1.partialTranslation},
+          \ res::$TypeExpr{typerepTypeExpr(top.frame.signature.outputElement.typerep, location=top.location)} ->
+            decorate res with { $ExprInhs{allInhs} }.$name{s2Name})
+      }
+    end;
+  local totalTrans::Expr =
+    Silver_Expr {
+      decorate $Expr{s1.totalTranslation} with { $ExprInhs{allInhs} }.$name{s2Name}
+    };
+  top.totalTranslation = if s2Total then totalTrans else asTotal(top.frame.signature.outputElement.typerep, totalTrans);
+}
+
+abstract production choice
+top::StrategyExpr ::= s1::StrategyExpr s2::StrategyExpr
+{
+  top.unparse = s"(${s1.unparse} <+ ${s2.unparse})";
+  propagate liftedStrategies;
+  top.isTotal = s1.isTotal || s2.isTotal;
+  
+  s1.outerAttr = nothing();
+  s2.outerAttr = nothing();
+  
+  top.partialTranslation =
+    Silver_Expr {
+      core:orElse($Expr{s1.partialTranslation}, $Expr{s2.partialTranslation})
+    };
+  top.totalTranslation =
+    if s1.isTotal
+    then s1.totalTranslation
+    else 
+      Silver_Expr {
+        core:fromMaybe($Expr{s2.totalTranslation}, $Expr{s1.partialTranslation})
+      };
+}
+
+-- Traversals
+abstract production allTraversal
+top::StrategyExpr ::= s::StrategyExpr
+{
+  top.unparse = s"all(${s.unparse})";
+  
+  local sName::String = fromMaybe(top.genName ++ "_all_arg", s.attrRefName);
+  local sTotal::Boolean = attrIsTotal(top.env, sName); -- Can differ from s.isTotal because we lift without env
+  top.liftedStrategies :=
+    if s.attrRefName.isJust
+    then []
+    else [pair(sName, s)];
+  top.isTotal = s.isTotal;
+  
+  s.outerAttr = nothing();
+  
+  local sBaseName::String = last(explode(":", sName));
+  -- pair(child name, attr occurs on child)
+  local childAccesses::[Pair<String Boolean>] =
+    map(
+      \ e::NamedSignatureElement ->
+        pair(e.elementName, attrMatchesFrame(top.env, sName, e.typerep)),
+      top.frame.signature.inputElements);
+  top.partialTranslation =
+    if sTotal
+    then asPartial(top.totalTranslation)
+    else
+      {- Translation of all(s) for prod::(Foo ::= a::Foo b::Integer c::Bar):
+           case a.s, c.s of
+           | just(a_s), just(c_s) -> just(prod(a_s, b, c_s))
+           | _, _ -> nothing()
+           end
+         Could also be implemented as chained monadic binds.  Maybe more efficient this way? -}
+      caseExpr(
+        flatMap(
+          \ a::Pair<String Boolean> ->
+            if a.snd then [Silver_Expr { $name{a.fst}.$name{sName} }] else [],
+          childAccesses),
+        [matchRule(
+           flatMap(
+             \ a::Pair<String Boolean> ->
+               if a.snd
+               then
+                 [decorate Silver_Pattern { core:just($name{a.fst ++ "_" ++ sBaseName}) }
+                  with { config = top.config; env = top.env; frame = top.frame; patternVarEnv = []; }]
+               else [],
+             childAccesses),
+           nothing(),
+           Silver_Expr {
+             core:just(
+               $Expr{
+                 mkFullFunctionInvocation(
+                   top.location,
+                   baseExpr(qName(top.location, top.frame.fullName), location=top.location),
+                   map(
+                     \ a::Pair<String Boolean> ->
+                       if a.snd
+                       then Silver_Expr { $name{a.fst ++ "_" ++ sBaseName} }
+                       else Silver_Expr { $name{a.fst} },
+                     childAccesses),
+                   map(
+                     makeAnnoArg(top.location, top.frame.signature.outputElement.elementName, _),
+                     top.frame.signature.namedInputElements))})
+           },
+           location=top.location)],
+        Silver_Expr { core:nothing() },
+        nonterminalType("core:Maybe", [top.frame.signature.outputElement.typerep]),
+        location=top.location);
+  top.totalTranslation =
+    if sTotal
+    then
+      {- When s is total, optimized translation of all(s) for prod::(Foo ::= a::Foo b::Integer c::Bar):
+           prod(a.s, b, c.s) -}
+       mkFullFunctionInvocation(
+         top.location,
+         baseExpr(qName(top.location, top.frame.fullName), location=top.location),
+         map(
+           \ a::Pair<String Boolean> ->
+             if a.snd
+             then Silver_Expr { $name{a.fst}.$name{sName} }
+             else Silver_Expr { $name{a.fst} },
+           childAccesses),
+         map(
+           makeAnnoArg(top.location, top.frame.signature.outputElement.elementName, _),
+           top.frame.signature.namedInputElements))
+    else asTotal(top.frame.signature.outputElement.typerep, top.partialTranslation);
+}
+
+abstract production someTraversal
+top::StrategyExpr ::= s::StrategyExpr
+{
+  top.unparse = s"some(${s.unparse})";
+  
+  local sName::String = fromMaybe(top.genName ++ "_some_arg", s.attrRefName);
+  local sTotal::Boolean = attrIsTotal(top.env, sName); -- Can differ from s.isTotal because we lift without env
+  top.liftedStrategies :=
+    if s.attrRefName.isJust
+    then []
+    else [pair(sName, s)];
+  
+  s.outerAttr = nothing();
+  
+  -- pair(child name, attr occurs on child)
+  local childAccesses::[Pair<String Boolean>] =
+    map(
+      \ e::NamedSignatureElement ->
+        pair(e.elementName, attrMatchesFrame(top.env, sName, e.typerep)),
+      top.frame.signature.inputElements);
+  local matchingChildren::[String] = map(fst, filter(snd, childAccesses));
+  top.partialTranslation =
+    if sTotal
+    then
+      if !null(matchingChildren)
+      then asPartial(top.totalTranslation)
+      else Silver_Expr { core:nothing() }
+    else
+      {- Translation of some(s) for prod::(Foo ::= a::Foo b::Integer c::Bar):
+           if a.s.isJust || c.s.isJust
+           then just(prod(fromMaybe(a, a.s), b, fromMaybe(c, c.s)))
+           else nothing()
+         Not sure of a clean way to do this with monads -}
+      Silver_Expr {
+        if $Expr{
+          foldr(
+            or(_, '||', _, location=top.location),
+            falseConst('false', location=top.location),
+            map(
+              \ a::String -> Silver_Expr { $name{a}.$name{sName}.isJust },
+              matchingChildren))}
+        then
+          core:just(
+            $Expr{
+              mkFullFunctionInvocation(
+                top.location,
+                baseExpr(qName(top.location, top.frame.fullName), location=top.location),
+                map(
+                  \ a::Pair<String Boolean> ->
+                    if a.snd
+                    then Silver_Expr { core:fromMaybe($name{a.fst}, $name{a.fst}.$name{sName}) }
+                    else Silver_Expr { $name{a.fst} },
+                  childAccesses),
+                map(
+                  makeAnnoArg(top.location, top.frame.signature.outputElement.elementName, _),
+                  top.frame.signature.namedInputElements))})
+        else core:nothing()
+      };
+  top.totalTranslation =
+    if sTotal && !null(matchingChildren)
+    then
+      {- When s is total, optimized translation of all(s) for prod::(Foo ::= a::Foo b::Integer c::Bar):
+           prod(a.s, b, c.s) -}
+       mkFullFunctionInvocation(
+         top.location,
+         baseExpr(qName(top.location, top.frame.fullName), location=top.location),
+         map(
+           \ a::Pair<String Boolean> ->
+             if a.snd
+             then Silver_Expr { $name{a.fst}.$name{sName} }
+             else Silver_Expr { $name{a.fst} },
+           childAccesses),
+         map(
+           makeAnnoArg(top.location, top.frame.signature.outputElement.elementName, _),
+           top.frame.signature.namedInputElements))
+    else asTotal(top.frame.signature.outputElement.typerep, top.partialTranslation);
+}
+abstract production oneTraversal
+top::StrategyExpr ::= s::StrategyExpr
+{
+  top.unparse = s"one(${s.unparse})";
+  
+  local sName::String = fromMaybe(top.genName ++ "_one_arg", s.attrRefName);
+  local sTotal::Boolean = attrIsTotal(top.env, sName); -- Can differ from s.isTotal because we lift without env
+  top.liftedStrategies :=
+    if s.attrRefName.isJust
+    then []
+    else [pair(sName, s)];
+  
+  s.outerAttr = nothing();
+  
+  local sBaseName::String = last(explode(":", sName));
+  -- pair(child name, attr occurs on child)
+  local childAccesses::[Pair<String Boolean>] =
+    map(
+      \ e::NamedSignatureElement ->
+        pair(e.elementName, attrMatchesFrame(top.env, sName, e.typerep)),
+      top.frame.signature.inputElements);
+  local matchingChildren::[String] = map(fst, filter(snd, childAccesses));
+  top.partialTranslation =
+    if sTotal
+    then
+      if !null(matchingChildren)
+      then asPartial(top.totalTranslation)
+      else Silver_Expr { core:nothing() }
+    else
+      {- Translation of one(s) for prod::(Foo ::= a::Foo b::Integer c::Bar):
+           case a.s, c.s of
+           | just(a_s), _ -> just(prod(a_s, b, c))
+           | _, just(c_s) -> just(prod(a, b, c_s))
+           | _, _ -> nothing()
+           end
+         Could also be implemented as
+           orElse(
+             bindMaybe(a.s, \ a_s::Foo -> returnMaybe(prod(a_s, b, c))),
+             bindMaybe(c.s, \ c_s::Bar -> returnMaybe(prod(a, b, c_s)))  -}
+      caseExpr(
+        map(
+          \ a::String -> Silver_Expr { $name{a}.$name{sName} },
+          matchingChildren),
+        map(
+          \ i::Integer ->
+            let childI::String = head(drop(i, matchingChildren))
+            in let childIndex::Integer = positionOf(stringEq, childI, map(fst, childAccesses))
+            in 
+              matchRule(
+                map(
+                  \ p::Pattern -> decorate p with { config = top.config; env = top.env; frame = top.frame; patternVarEnv = []; },
+                  repeat(wildcPattern('_', location=top.location), i) ++
+                  Silver_Pattern { core:just($name{childI ++ "_" ++ sBaseName}) } ::
+                  repeat(wildcPattern('_', location=top.location), length(matchingChildren) - (i + 1))),
+                nothing(),
+                Silver_Expr {
+                  core:just(
+                    $Expr{
+                      mkFullFunctionInvocation(
+                        top.location,
+                        baseExpr(qName(top.location, top.frame.fullName), location=top.location),
+                        map(
+                          \ a::Pair<String Boolean> -> Silver_Expr { $name{a.fst} },
+                          take(childIndex, childAccesses)) ++
+                        Silver_Expr { $name{childI ++ "_" ++ sBaseName} } ::
+                        map(
+                          \ a::Pair<String Boolean> -> Silver_Expr { $name{a.fst} },
+                          drop(childIndex + 1, childAccesses)),
+                        map(
+                          makeAnnoArg(top.location, top.frame.signature.outputElement.elementName, _),
+                          top.frame.signature.namedInputElements))})
+                },
+                location=top.location)
+            end end,
+            range(0, length(matchingChildren))),
+        Silver_Expr { core:nothing() },
+        nonterminalType("core:Maybe", [top.frame.signature.outputElement.typerep]),
+        location=top.location);
+  top.totalTranslation =
+    if sTotal && !null(matchingChildren)
+    then
+      {- When s is total, optimized translation of one(s) for prod::(Foo ::= a::Foo b::Integer c::Bar):
+           prod(a.s, b, c) -}
+      mkFullFunctionInvocation(
+        top.location,
+        baseExpr(qName(top.location, top.frame.fullName), location=top.location),
+        map(
+          \ a::Pair<String Boolean> ->
+            if a.fst == head(matchingChildren)
+            then Silver_Expr { $name{a.fst}.$name{sName} }
+            else Silver_Expr { $name{a.fst} },
+          childAccesses),
+        map(
+          makeAnnoArg(top.location, top.frame.signature.outputElement.elementName, _),
+          top.frame.signature.namedInputElements))
+    else asTotal(top.frame.signature.outputElement.typerep, top.partialTranslation);
+}
+
+abstract production prodTraversal
+top::StrategyExpr ::= prod::QName s::StrategyExprs
+{
+  top.unparse = s"${prod.unparse}(${s.unparse})";
+  
+  top.errors <- prod.lookupValue.errors;
+  
+  local numParams::Integer = length(s.givenInputElements);
+  local numArgs::Integer = length(s.attrRefNames);
+  top.errors <-
+    if prod.lookupValue.found && numArgs != numParams
+    then [err(top.location, s"Wrong number of arguments to ${prod.name}: expected ${toString(numParams)}, got ${toString(numArgs)}")]
+    else [];
+  
+  propagate liftedStrategies;
+  
+  s.givenInputElements =
+    if prod.lookupValue.found
+    then prod.lookupValue.dcl.namedSignature.inputElements
+    else [];
+  
+  -- pair(child name, if attr occurs on child then just(attr name) else nothing())
+  local childAccesses::[Pair<String Maybe<String>>] =
+    zipWith(pair, top.frame.signature.inputNames, s.attrRefNames);
+  top.partialTranslation = -- This is never total
+    if prod.lookupValue.fullName == top.frame.fullName
+    then
+      {- Translation of prod(s1, s2, s3, s4) for prod::(Foo ::= a::Foo b::Integer c::Bar d::Baz)
+         where s4 is total:
+           case a.s1, c.s3 of
+           | just(a_s1), just(c_s3) -> just(prod(a_s1, b, c_s3, d.s4))
+           | _, _ -> nothing()
+           end
+         Could also be implemented as chained monadic binds.  Maybe more efficient this way? -}
+      caseExpr(
+        flatMap(
+          \ a::Pair<String Maybe<String>> ->
+            case a.snd of
+            | just(attr) when !attrIsTotal(top.env, attr) -> [Silver_Expr { $name{a.fst}.$name{attr} }]
+            | _ -> []
+            end,
+          childAccesses),
+        [matchRule(
+           flatMap(
+             \ a::Pair<String Maybe<String>> ->
+               case a.snd of
+               | just(attr) when !attrIsTotal(top.env, attr)  ->
+                 [decorate Silver_Pattern { core:just($name{a.fst ++ "_" ++ last(explode(":", attr))}) }
+                  with { config = top.config; env = top.env; frame = top.frame; patternVarEnv = []; }]
+               | _ -> []
+               end,
+             childAccesses),
+           nothing(),
+           Silver_Expr {
+             core:just(
+               $Expr{
+                 mkFullFunctionInvocation(
+                   top.location,
+                   baseExpr(qName(top.location, top.frame.fullName), location=top.location),
+                   map(
+                     \ a::Pair<String Maybe<String>> ->
+                       case a.snd of
+                       | just(attr) when attrIsTotal(top.env, attr) -> Silver_Expr { $name{a.fst}.$name{attr} }
+                       | just(attr) -> Silver_Expr { $name{a.fst ++ "_" ++ last(explode(":", attr))} }
+                       | nothing() -> Silver_Expr { $name{a.fst} }
+                       end,
+                     childAccesses),
+                   map(
+                     makeAnnoArg(top.location, top.frame.signature.outputElement.elementName, _),
+                     top.frame.signature.namedInputElements))})
+           },
+           location=top.location)],
+        Silver_Expr { core:nothing() },
+        nonterminalType("core:Maybe", [top.frame.signature.outputElement.typerep]),
+        location=top.location)
+    else Silver_Expr { core:nothing() };
+}
+
+abstract production consStrategyExpr
+top::StrategyExprs ::= h::StrategyExpr t::StrategyExprs
+{
+  top.unparse = s"${h.unparse}, ${t.unparse}";
+   
+  top.liftedStrategies :=
+    -- Slight hack: when h is id (common case for prod traversals), there is no need for a new attribute.
+    -- However this can't be avoided during the optimization phase, which happens after lifting.
+    -- So, just don't lift the strategy, and we won't find the occurence of the non-existant attribute
+    -- during translation - which means we will treat it as id anyway!
+    (if h.attrRefName.isJust || h.isId
+     then []
+     else [pair(h.genName, h)]) ++
+    t.liftedStrategies;
+  
+  local hType::Type = head(top.givenInputElements).typerep;
+  local attr::String = fromMaybe(h.genName, h.attrRefName);
+  local attrMatch::Boolean = attrMatchesFrame(top.env, attr, hType);
+  top.attrRefNames =
+   (if !null(top.givenInputElements) && attrMatch && !h.isId
+    then just(attr)
+    else nothing()) :: t.attrRefNames;
+  top.errors <-
+    if !null(top.givenInputElements) && !attrMatch && !h.isId
+    then [wrn(h.location, s"This (non-identity) strategy attribute does not occur on ${prettyType(hType)} and will be treated as identity")]
+    else [];
+  
+  top.containsFail <- case h of fail() -> true | _ -> false end;
+  top.allId <- case h of id() -> true | _ -> false end;
+  
+  h.outerAttr = nothing();
+  t.givenInputElements =
+    if !null(top.givenInputElements) then tail(top.givenInputElements) else [];
+}
+
+abstract production nilStrategyExpr
+top::StrategyExprs ::=
+{
+  top.unparse = "";
+  top.liftedStrategies := [];
+  top.attrRefNames = [];
+}
+
+-- Recursive strategies
+abstract production recComb
+top::StrategyExpr ::= n::Name s::StrategyExpr
+{
+  top.unparse = s"rec ${n.name} -> (${s.unparse})";
+  
+  local sName::String = fromMaybe(top.genName ++ "_rec_body", top.outerAttr);
+  top.liftedStrategies :=
+    if top.outerAttr.isJust
+    then s.liftedStrategies
+    else [pair(sName, s)];
+  top.freeRecVars := removeBy(stringEq, n.name, s.freeRecVars);
+  top.isTotal =
+    decorate s with {
+      recVarTotalEnv = pair(n.name, true) :: s.recVarTotalEnv;
+      env = s.env; config = s.config; grammarName = s.grammarName; recVarNameEnv = s.recVarNameEnv; outerAttr = s.outerAttr;
+    }.isTotal;
+  
+  s.recVarNameEnv = pair(n.name, sName) :: top.recVarNameEnv;
+  s.recVarTotalEnv = pair(n.name, top.isTotal) :: top.recVarTotalEnv;
+  s.outerAttr = top.outerAttr;
+  
+  local sTotal::Boolean = attrIsTotal(top.env, sName);
+  top.partialTranslation =
+    if top.outerAttr.isJust
+    then s.partialTranslation
+    else if sTotal
+    then asPartial(top.totalTranslation)
+    else Silver_Expr { $name{top.frame.signature.outputElement.elementName}.$name{sName} };
+  top.totalTranslation =
+    if top.outerAttr.isJust
+    then s.totalTranslation
+    else if sTotal
+    then Silver_Expr { $name{top.frame.signature.outputElement.elementName}.$name{sName} }
+    else asTotal(top.frame.signature.outputElement.typerep, top.partialTranslation);
+}
+
+-- Rules
+abstract production rewriteRule
+top::StrategyExpr ::= id::Name ty::TypeExpr ml::MRuleList
+{
+  top.unparse = "rule on " ++ id.name ++ "::" ++ ty.unparse ++ " of " ++ ml.unparse ++ " end";
+  propagate liftedStrategies;
+  
+  -- Pattern matching error checking (mostly) happens on what caseExpr forwards to,
+  -- so we need to decorate one of those here.
+  local checkExpr::Expr =
+    letp(
+      assignExpr(id, '::', ty, '=', errorExpr([], location=top.location), location=top.location),
+      caseExpr(
+        [hackExprType(ty.typerep, location=top.location)],
+        ml.matchRuleList,
+        errorExpr([], location=top.location),
+        ty.typerep,
+        location=top.location),
+      location=top.location);
+  checkExpr.env = top.env;
+  checkExpr.flowEnv = top.flowEnv;
+  checkExpr.downSubst = emptySubst();
+  checkExpr.finalSubst = checkExpr.upSubst;
+  checkExpr.grammarName = top.grammarName;
+  checkExpr.frame = top.frame;
+  checkExpr.config = top.config;
+  checkExpr.compiledGrammars = top.compiledGrammars;
+  
+  top.errors <- checkExpr.errors;
+  top.errors <-
+    if !ty.typerep.isDecorable
+    then [wrn(ty.location, "Only rules on nonterminals can have an effect")]
+    else []; 
+  
+  top.flowDefs <- checkExpr.flowDefs;
+  
+  ml.matchRulePatternSize = 1;
+  
+  local res::Expr =
+    caseExpr(
+      [Silver_Expr { $name{top.frame.signature.outputElement.elementName} }],
+      ml.translation,
+      Silver_Expr { core:nothing() },
+      nonterminalType("core:Maybe", [ty.typerep]),
+      location=top.location);
+  top.partialTranslation =
+    if unify(ty.typerep, top.frame.signature.outputElement.typerep).failure
+    then Silver_Expr { core:nothing() }
+    else if top.frame.signature.outputElement.elementName == id.name
+    then res
+    else Silver_Expr {
+      let $Name{id}::$TypeExpr{ty} = $name{top.frame.signature.outputElement.elementName}
+      in $Expr{res}
+      end
+    };
+}
+
+-- Hack dummy expr with a given type
+abstract production hackExprType
+top::Expr ::= t::Type
+{
+  top.typerep = t;
+  forwards to errorExpr([], location=top.location);
+}
+
+attribute matchesFrame occurs on MRuleList, MatchRule, PatternList, Pattern;
+propagate matchesFrame on MRuleList, MatchRule, PatternList;
+
+synthesized attribute translation<a>::a;
+attribute translation<[AbstractMatchRule]> occurs on MRuleList;
+
+aspect production mRuleList_one
+top::MRuleList ::= m::MatchRule
+{
+  top.translation = [m.translation];
+}
+
+aspect production mRuleList_cons
+top::MRuleList ::= h::MatchRule '|' t::MRuleList
+{
+  top.translation = h.translation :: t.translation;
+}
+
+attribute translation<AbstractMatchRule> occurs on MatchRule;
+
+aspect production matchRule_c
+top::MatchRule ::= pt::PatternList _ e::Expr
+{
+  top.translation =
+    matchRule(
+      pt.patternList, nothing(), Silver_Expr { core:just($Expr{e}) },
+      location=top.location);
+}
+
+aspect production matchRuleWhen_c
+top::MatchRule ::= pt::PatternList 'when' cond::Expr _ e::Expr
+{
+  top.translation =
+    matchRule(
+      pt.patternList, just(pair(cond, nothing())), Silver_Expr { core:just($Expr{e}) },
+      location=top.location);
+}
+
+aspect production matchRuleWhenMatches_c
+top::MatchRule ::= pt::PatternList 'when' cond::Expr 'matches' p::Pattern _ e::Expr
+{
+  top.translation =
+    matchRule(
+      pt.patternList, just(pair(cond, just(p))), Silver_Expr { core:just($Expr{e}) },
+      location=top.location);
+}
+
+aspect default production
+top::Pattern ::=
+{
+  top.matchesFrame := true;
+}
+
+aspect production prodAppPattern_named
+top::Pattern ::= prod::QName '(' ps::PatternList ',' nps::NamedPatternList ')'
+{
+  top.matchesFrame := prod.lookupValue.fullName == top.frame.fullName;
+}
+
+-- References to other attributes or rec variables
+abstract production nameRef
+top::StrategyExpr ::= id::QName
+{
+  top.unparse = id.unparse;
+  
+  -- Forwarding depends on env here, these must be computed without env
+  propagate liftedStrategies;
+  top.attrRefName = just(fromMaybe(id.name, lookupBy(stringEq, id.name, top.recVarNameEnv)));
+  top.isId = false;
+  
+  local attrDcl::DclInfo = id.lookupAttribute.dcl;
+  attrDcl.givenNonterminalType = error("Not actually needed"); -- Ugh environment needs refactoring
+  forwards to
+    if lookupBy(stringEq, id.name, top.recVarNameEnv).isJust
+    then recVarRef(id, genName=top.genName, location=top.location)
+    else if !null(id.lookupAttribute.errors)
+    then errorRef(id.lookupAttribute.errors, id, genName=top.genName, location=top.location)
+    else if attrIsTotal(top.env, id.name)
+    then totalRef(qNameAttrOccur(id, location=top.location), genName=top.genName, location=top.location)
+    else partialRef(qNameAttrOccur(id, location=top.location), genName=top.genName, location=top.location);
+}
+abstract production errorRef
+top::StrategyExpr ::= msg::[Message] id::Decorated QName
+{
+  top.unparse = id.unparse;
+  
+  propagate liftedStrategies;
+  top.attrRefName = just(id.name);
+  
+  top.errors <- msg;
+  top.partialTranslation = Silver_Expr { core:nothing() };
+}
+abstract production recVarRef
+top::StrategyExpr ::= id::Decorated QName
+{
+  top.unparse = id.unparse;
+  
+  propagate liftedStrategies;
+  top.attrRefName = lookupBy(stringEq, id.name, top.recVarNameEnv);
+  top.isTotal = lookupBy(stringEq, id.name, top.recVarTotalEnv).fromJust;
+  top.freeRecVars <- [id.name];
+  
+  top.partialTranslation =
+    if attrIsTotal(top.env, top.attrRefName.fromJust)
+    then asPartial(top.totalTranslation)
+    else Silver_Expr { $name{top.frame.signature.outputElement.elementName}.$qName{top.attrRefName.fromJust} };
+  top.totalTranslation =
+    if attrIsTotal(top.env, top.attrRefName.fromJust)
+    then Silver_Expr { $name{top.frame.signature.outputElement.elementName}.$qName{top.attrRefName.fromJust} }
+    else asTotal(top.frame.signature.outputElement.typerep, top.partialTranslation);
+}
+abstract production partialRef
+top::StrategyExpr ::= attr::QNameAttrOccur
+{
+  top.unparse = attr.unparse;
+  
+  -- Lookup for error checking is *not* contextual, since we don't know the frame here
+  local attrDcl::DclInfo = case attr of qNameAttrOccur(a) -> a.lookupAttribute.dcl end;
+  attrDcl.givenNonterminalType = error("Not actually needed"); -- Ugh environment needs refactoring
+  top.errors :=
+    case attrDcl.typerep, attrDcl.dclBoundVars of
+    | nonterminalType("core:Maybe", [varType(a1)]), [a2] when tyVarEqual(a1, a2) -> []
+    | nonterminalType("core:Maybe", [nonterminalType(nt, _)]), _ ->
+      if null(getOccursDcl(attrDcl.fullName, nt, top.env))
+      then [wrn(attr.location, s"Attribute ${attr.name} cannot be used as a partial strategy, because it doesn't occur on its own nonterminal type ${nt}")]
+      else []
+    | errorType(), _ -> []
+    | _, _ -> [err(attr.location, s"Attribute ${attr.name} cannot be used as a partial strategy")]
+    end;
+  
+  propagate liftedStrategies;
+  top.attrRefName = just(attr.name);
+  top.matchesFrame := attr.matchesFrame;
+  top.isTotal = false;
+  top.partialRefs <- [attrDcl.fullName];
+  
+  attr.attrFor = top.frame.signature.outputElement.typerep;
+  
+  top.partialTranslation =
+    if attr.matchesFrame
+    then Silver_Expr { $name{top.frame.signature.outputElement.elementName}.$QNameAttrOccur{attr} }
+    else Silver_Expr { core:nothing() };
+}
+abstract production totalRef
+top::StrategyExpr ::= attr::QNameAttrOccur
+{
+  top.unparse = attr.unparse;
+  
+  -- Lookup for error checking is *not* contextual, since we don't know the frame here
+  local attrDcl::DclInfo = case attr of qNameAttrOccur(a) -> a.lookupAttribute.dcl end;
+  attrDcl.givenNonterminalType = error("Not actually needed"); -- Ugh environment needs refactoring
+  top.errors :=
+    case attrDcl.typerep, attrDcl.dclBoundVars of
+    | varType(a1), [a2] when tyVarEqual(a1, a2) -> []
+    | nonterminalType(nt, _), _ ->
+      if null(getOccursDcl(attrDcl.fullName, nt, top.env))
+      then [wrn(attr.location, s"Attribute ${attr.name} cannot be used as total strategy, because it doesn't occur on its own nonterminal type ${nt}")]
+      else []
+    | errorType(), _ -> []
+    | _, _ -> [err(attr.location, s"Attribute ${attr.name} cannot be used as total strategy")]
+    end;
+  
+  propagate liftedStrategies;
+  top.attrRefName = just(attr.name);
+  top.matchesFrame := attr.matchesFrame;
+  top.isTotal = true;
+  top.totalRefs <- [attrDcl.fullName];
+  
+  attr.attrFor = top.frame.signature.outputElement.typerep;
+  
+  top.totalTranslation = Silver_Expr { $name{top.frame.signature.outputElement.elementName}.$QNameAttrOccur{attr} };
+}
+
+-- The result of performing an inlining optimization
+abstract production inlined
+top::StrategyExpr ::= attr::Decorated QNameAttrOccur s::StrategyExpr
+{
+  top.unparse = s"(${s.unparse} aka ${attr.unparse})";
+  propagate liftedStrategies;
+  top.attrRefName = just(attr.attrDcl.fullName);
+  top.isTotal = s.isTotal;
+  top.partialTranslation =
+    if attr.matchesFrame
+    then s.partialTranslation
+    else Silver_Expr { core:nothing() };
+  top.totalTranslation = s.totalTranslation;
+  
+  s.outerAttr = top.outerAttr;
+  s.inlinedStrategies = attr.attrDcl.fullName :: top.inlinedStrategies;
+}
+
+attribute matchesFrame occurs on QNameAttrOccur;
+
+aspect production qNameAttrOccur
+top::QNameAttrOccur ::= at::QName
+{
+  top.matchesFrame := top.found &&
+    case top.typerep of
+    | nonterminalType("core:Maybe", [t]) -> !unify(top.attrFor, t).failure
+    | t -> !unify(top.attrFor, t).failure
+    end;
+}
+
+function attrIsTotal
+Boolean ::= env::Decorated Env attrName::String
+{
+  local dcls::[DclInfo] = getAttrDcl(attrName, env);
+  return
+    case dcls of
+    | [] -> false
+    | d :: _ ->
+      case decorate d with { givenNonterminalType = error("Not actually needed"); }.typerep of -- Ugh environment needs refactoring
+      | nonterminalType("core:Maybe", _) -> false
+      | _ -> true
+      end
+    end;
+}
+
+function attrMatchesFrame
+Boolean ::= env::Decorated Env attrName::String attrFor::Type
+{
+  return
+    decorate qNameAttrOccur(qName(loc("", -1, -1, -1, -1, -1, -1), attrName), location=loc("", -1, -1, -1, -1, -1, -1))
+    with { env = env; attrFor = attrFor; }.matchesFrame;
+}
+
+function attrMatchesChild
+Boolean ::= env::Decorated Env attrName::String frame::BlockContext
+{
+  return
+    any(
+      map(
+        \ e::NamedSignatureElement -> attrMatchesFrame(env, attrName, e.typerep),
+        frame.signature.inputElements));
+}
diff --git a/grammars/silver/extension/strategyattr/StrategyUtils.sv b/grammars/silver/extension/strategyattr/StrategyUtils.sv
new file mode 100644
index 000000000..9a0648965
--- /dev/null
+++ b/grammars/silver/extension/strategyattr/StrategyUtils.sv
@@ -0,0 +1,191 @@
+grammar silver:extension:strategyattr;
+
+import silver:metatranslation;
+import silver:modification:copper; -- print keyword
+
+-- Debugging
+abstract production printTerm
+top::StrategyExpr ::=
+{
+  top.unparse = s"printTerm";
+  
+  propagate liftedStrategies;
+  top.isTotal = true;
+  top.totalTranslation =
+    Silver_Expr {
+      core:unsafeTrace(
+        $name{top.frame.signature.outputElement.elementName},
+        core:print(
+          hackUnparse($name{top.frame.signature.outputElement.elementName}) ++ "\n\n",
+          core:unsafeIO()))
+    };
+}
+
+-- Utilities
+abstract production try
+top::StrategyExpr ::= s::StrategyExpr
+{
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      $StrategyExpr{s} <+ id
+    };
+}
+
+abstract production repeatS -- name clash with repeat from core
+top::StrategyExpr ::= s::StrategyExpr
+{
+  local recVarName::String = "repeat_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> try($StrategyExpr{s} <* $strategyQName{recVarName})
+    };
+}
+
+abstract production reduce
+top::StrategyExpr ::= s::StrategyExpr
+{
+  local recVarName::String = "reduce_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      repeat(rec $name{recVarName} -> some($strategyQName{recVarName}) <+ $StrategyExpr{s})
+    };
+}
+
+abstract production bottomUp
+top::StrategyExpr ::= s::StrategyExpr
+{
+  local recVarName::String = "bottomUp_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> all($strategyQName{recVarName}) <* $StrategyExpr{s}
+    };
+}
+
+abstract production topDown
+top::StrategyExpr ::= s::StrategyExpr
+{
+  local recVarName::String = "topDown_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> $StrategyExpr{s} <* all($strategyQName{recVarName})
+    };
+}
+
+abstract production downUp
+top::StrategyExpr ::= s1::StrategyExpr s2::StrategyExpr
+{
+  local recVarName::String = "downUp_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> $StrategyExpr{s1} <* all($strategyQName{recVarName}) <* $StrategyExpr{s2}
+    };
+}
+
+abstract production allBottomUp
+top::StrategyExpr ::= s::StrategyExpr
+{
+  local recVarName::String = "allBottomUp_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> all($strategyQName{recVarName}) <+ $StrategyExpr{s}
+    };
+}
+
+abstract production allTopDown
+top::StrategyExpr ::= s::StrategyExpr
+{
+  local recVarName::String = "allTopDown_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> $StrategyExpr{s} <+ all($strategyQName{recVarName})
+    };
+}
+
+abstract production allDownUp
+top::StrategyExpr ::= s1::StrategyExpr s2::StrategyExpr
+{
+  local recVarName::String = "allDownUp_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> $StrategyExpr{s1} <+ all($strategyQName{recVarName}) <+ $StrategyExpr{s2}
+    };
+}
+
+abstract production someBottomUp
+top::StrategyExpr ::= s::StrategyExpr
+{
+  local recVarName::String = "someBottomUp_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> some($strategyQName{recVarName}) <+ $StrategyExpr{s}
+    };
+}
+
+abstract production someTopDown
+top::StrategyExpr ::= s::StrategyExpr
+{
+  local recVarName::String = "someTopDown_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> $StrategyExpr{s} <+ some($strategyQName{recVarName})
+    };
+}
+
+abstract production someDownUp
+top::StrategyExpr ::= s1::StrategyExpr s2::StrategyExpr
+{
+  local recVarName::String = "someDownUp_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> $StrategyExpr{s1} <+ some($strategyQName{recVarName}) <+ $StrategyExpr{s2}
+    };
+}
+
+abstract production onceBottomUp
+top::StrategyExpr ::= s::StrategyExpr
+{
+  local recVarName::String = "onceBottomUp_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> one($strategyQName{recVarName}) <+ $StrategyExpr{s}
+    };
+}
+
+abstract production onceTopDown
+top::StrategyExpr ::= s::StrategyExpr
+{
+  local recVarName::String = "onceTopDown_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> $StrategyExpr{s} <+ one($strategyQName{recVarName})
+    };
+}
+
+abstract production onceDownUp
+top::StrategyExpr ::= s1::StrategyExpr s2::StrategyExpr
+{
+  local recVarName::String = "onceDownUp_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> $StrategyExpr{s1} <+ one($strategyQName{recVarName}) <+ $StrategyExpr{s2}
+    };
+}
+
+abstract production innermost
+top::StrategyExpr ::= s::StrategyExpr
+{
+  local recVarName::String = "innermost_" ++ toString(genInt());
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      rec $name{recVarName} -> bottomUp(try($StrategyExpr{s} <* $strategyQName{recVarName}))
+    };
+}
+
+abstract production outermost
+top::StrategyExpr ::= s::StrategyExpr
+{
+  forwards to
+    Silver_StrategyExpr (top.genName) {
+      repeat(onceTopDown($StrategyExpr{s}))
+    };
+}
diff --git a/grammars/silver/extension/strategyattr/Terminals.sv b/grammars/silver/extension/strategyattr/Terminals.sv
new file mode 100644
index 000000000..86ebabb37
--- /dev/null
+++ b/grammars/silver/extension/strategyattr/Terminals.sv
@@ -0,0 +1,38 @@
+grammar silver:extension:strategyattr;
+
+terminal Strategy_kwd 'strategy' lexer classes {KEYWORD, RESERVED};
+terminal Partial_kwd  'partial'  lexer classes {KEYWORD, RESERVED};
+
+terminal Sequence_t '<*'  precedence = 12, association = left; -- Same as *
+terminal Choice_t   '<+'  precedence = 11, association = left; -- Same as +
+
+lexer class Strategy dominates StrategyName_t;
+
+terminal Id_t    'id'   lexer classes {KEYWORD, Strategy};
+terminal Fail_t  'fail' lexer classes {KEYWORD, Strategy};
+terminal All_t   'all'  lexer classes {KEYWORD, Strategy};
+terminal Some_t  'some' lexer classes {KEYWORD, Strategy};
+terminal One_t   'one'  lexer classes {KEYWORD, Strategy};
+terminal Rule_t  'rule' lexer classes {KEYWORD, Strategy};
+terminal Rec_t   'rec'  lexer classes {KEYWORD, Strategy};
+
+terminal PrintTerm_t    'printTerm'    lexer classes {KEYWORD, Strategy};
+terminal Try_t          'try'          lexer classes {KEYWORD, Strategy};
+terminal Repeat_t       'repeat'       lexer classes {KEYWORD, Strategy};
+terminal Reduce_t       'reduce'       lexer classes {KEYWORD, Strategy};
+terminal BottomUp_t     'bottomUp'     lexer classes {KEYWORD, Strategy};
+terminal TopDown_t      'topDown'      lexer classes {KEYWORD, Strategy};
+terminal DownUp_t       'downUp'       lexer classes {KEYWORD, Strategy};
+terminal AllBottomUp_t  'allBottomUp'  lexer classes {KEYWORD, Strategy};
+terminal AllTopDown_t   'allTopDown'   lexer classes {KEYWORD, Strategy};
+terminal AllDownUp_t    'allDownUp'    lexer classes {KEYWORD, Strategy};
+terminal SomeBottomUp_t 'someBottomUp' lexer classes {KEYWORD, Strategy};
+terminal SomeTopDown_t  'someTopDown'  lexer classes {KEYWORD, Strategy};
+terminal SomeDownUp_t   'someDownUp'   lexer classes {KEYWORD, Strategy};
+terminal OnceBottomUp_t 'onceBottomUp' lexer classes {KEYWORD, Strategy};
+terminal OnceTopDown_t  'onceTopDown'  lexer classes {KEYWORD, Strategy};
+terminal OnceDownUp_t   'onceDownUp'   lexer classes {KEYWORD, Strategy};
+terminal Innermost_t    'innermost'    lexer classes {KEYWORD, Strategy};
+terminal Outermost_t    'outermost'    lexer classes {KEYWORD, Strategy};
+
+terminal StrategyName_t /[a-z][A-Za-z0-9\_]*/ lexer classes {IDENTIFIER};
diff --git a/grammars/silver/extension/strategyattr/construction/Construction.sv b/grammars/silver/extension/strategyattr/construction/Construction.sv
new file mode 100644
index 000000000..5300ec7cc
--- /dev/null
+++ b/grammars/silver/extension/strategyattr/construction/Construction.sv
@@ -0,0 +1,64 @@
+grammar silver:extension:strategyattr:construction;
+
+imports silver:definition:core;
+imports silver:extension:strategyattr;
+imports silver:extension:silverconstruction;
+
+imports silver:reflect;
+imports silver:metatranslation;
+imports silver:rewrite as s;
+imports silver:langutil:pp;
+
+terminal SilverStrategyExpr_t 'Silver_StrategyExpr' lexer classes {KEYWORD, RESERVED};
+terminal AntiquoteStrategyExpr_t '$StrategyExpr' lexer classes {Antiquote, Strategy};
+terminal AntiquoteStrategyQName_t '$strategyQName' lexer classes {Antiquote, Strategy};
+
+concrete production quoteStrategyExpr
+top::Expr ::= 'Silver_StrategyExpr' '(' genName::Expr ')' '{' cst::StrategyExpr_c '}'
+{
+  top.unparse = s"Silver_StrategyExpr (${genName.unparse}) {${cst.unparse}}";
+  -- The meta-translation library directly translates all annotation values into
+  -- static initialization code, however we want to specify genName at runtime.
+  -- Solution: construct the term with "" as the base genName and translate it
+  -- into an expression like normal, then use term rewriting to replace all all
+  -- occurences of `genName=$e` with `genName=$genName ++ $e`.
+  -- Confused yet?
+  -- A "simpler" approach would be to handle this in the meta-translation library
+  -- in one pass, but we want to keep that code as a generic library as much as possible.
+  cst.givenGenName = "";
+  forwards to
+    rewriteWith(
+      s:allTopDown(
+        rule on AnnoExpr of
+        | annoExpr(n, _, presentAppExpr(e), location=l) when n.name == "genName" ->
+          annoExpr(n, '=', presentAppExpr(plusPlus(genName, '++', e, location=l), location=l), location=l)
+        end),
+        translate(top.location, reflect(cst.ast))).fromJust;
+}
+
+concrete production antiquoteStrategyExpr_c
+top::StrategyExpr_c ::= '$StrategyExpr' '{' e::Expr '}'
+{
+  top.unparse = s"$$StrategyExpr{${e.unparse}}";
+  top.ast = antiquoteStrategyExpr(e, genName=top.givenGenName, location=top.location);
+}
+
+concrete production antiquote_strategyQName
+top::StrategyQName ::= '$strategyQName' '{' e::Expr '}'
+{
+  top.ast = antiquote_qName('$qName', $2, e, $4, location=top.location);
+}
+
+abstract production antiquoteStrategyExpr
+top::StrategyExpr ::= e::Expr
+{
+  top.unparse = s"$$StrategyExpr{${e.unparse}}";
+  forwards to error("no forward");
+}
+
+aspect production nonterminalAST
+top::AST ::= prodName::String children::ASTs annotations::NamedASTs
+{
+  directAntiquoteProductions <-
+    ["silver:extension:strategyattr:construction:antiquoteStrategyExpr"];
+}
diff --git a/grammars/silver/extension/strategyattr/convenience/Convenience.sv b/grammars/silver/extension/strategyattr/convenience/Convenience.sv
new file mode 100644
index 000000000..a31847dad
--- /dev/null
+++ b/grammars/silver/extension/strategyattr/convenience/Convenience.sv
@@ -0,0 +1,31 @@
+grammar silver:extension:strategyattr:convenience;
+
+import silver:extension:strategyattr;
+import silver:extension:convenience;
+import silver:definition:core;
+import silver:definition:concrete_syntax;
+import silver:definition:type:syntax;
+import silver:definition:type;
+import silver:definition:env;
+
+concrete production partialStrategyAttributeDclMultiple
+top::AGDcl ::= 'partial' 'strategy' 'attribute' a::Name '=' e::StrategyExpr_c 'occurs' 'on' qs::QNames ';'
+{
+  top.unparse = "partial strategy attribute " ++ a.name ++ " occurs on " ++ qs.unparse ++ ";";
+  forwards to
+    appendAGDcl(
+      partialStrategyAttributeDcl($1, $2, $3, a, $5, e, $10, location=a.location),
+      makeOccursDclsHelp($1.location, qNameWithTL(qNameId(a, location=a.location), botlNone(location=top.location)), qs.qnames),
+      location=top.location);
+}
+
+concrete production totalStrategyAttributeDclMultiple
+top::AGDcl ::= 'strategy' 'attribute' a::Name '=' e::StrategyExpr_c 'occurs' 'on' qs::QNames ';'
+{
+  top.unparse = "strategy attribute " ++ a.name ++ " occurs on " ++ qs.unparse ++ ";";
+  forwards to
+    appendAGDcl(
+      totalStrategyAttributeDcl($1, $2, a, $4, e, $9, location=a.location),
+      makeOccursDclsHelp($1.location, qNameWithTL(qNameId(a, location=a.location), botlNone(location=top.location)), qs.qnames),
+      location=top.location);
+}
diff --git a/grammars/silver/host/Project.sv b/grammars/silver/host/Project.sv
index 2656bb17a..2cc9ad779 100644
--- a/grammars/silver/host/Project.sv
+++ b/grammars/silver/host/Project.sv
@@ -41,6 +41,7 @@ exports silver:extension:patternmatching;
 exports silver:extension:treegen;
 exports silver:extension:doc;
 exports silver:extension:autoattr;
+exports silver:extension:strategyattr;
 exports silver:extension:monad;
 exports silver:extension:reflection;
 exports silver:extension:rewriting;
diff --git a/grammars/silver/rewrite/Strategy.sv b/grammars/silver/rewrite/Strategy.sv
index 3514ddd27..7f1d4bade 100644
--- a/grammars/silver/rewrite/Strategy.sv
+++ b/grammars/silver/rewrite/Strategy.sv
@@ -265,5 +265,5 @@ top::Strategy ::= s::Strategy
 abstract production outermost
 top::Strategy ::= s::Strategy
 {
-  forwards to topDown(try(s <* outermost(s)));
+  forwards to repeat(onceTopDown(s));
 }
diff --git a/test/patt/Basics.sv b/test/patt/Basics.sv
index 7d88ea2ba..deac25c3a 100644
--- a/test/patt/Basics.sv
+++ b/test/patt/Basics.sv
@@ -48,8 +48,8 @@ equalityTest ( basic3(nothing(), just("w"), nothing()), "w", String, pat_tests )
 equalityTest ( basic3(just("w"), nothing(), nothing()), "w", String, pat_tests ) ;
 equalityTest ( basic3(nothing(), nothing(), just("w")), "w", String, pat_tests ) ;
 
--- TODO: Well, we do left-to-right preferred above all. Haskell preferrs top-to-bottom above all....
-equalityTest ( basic3(just("g"), just("w"), just("h")), "g", String, pat_tests ) ;
+-- test top-to-bottom matching
+equalityTest ( basic3(just("g"), just("w"), just("h")), "w", String, pat_tests ) ;
 
 function basic4 -- using integers
 Integer ::= p::Pair<Integer Maybe<Integer>>
@@ -117,7 +117,7 @@ end;
 }
 
 -- once, this test returned 40, just to clarify what we're testing here.
-equalityTest ( basic7(mytriple(1,just(20),just(300))), 21, Integer, pat_tests ) ;
+equalityTest ( basic7(mytriple(1,just(20),just(300))), 301, Integer, pat_tests ) ;
 equalityTest ( basic7(mytriple(1,nothing(),just(300))), 301, Integer, pat_tests ) ;
 
 function basic8 -- using mixed name/fullnames
@@ -136,3 +136,25 @@ equalityTest ( basic8(pair(1,3)), 2, Integer, pat_tests );
 equalityTest ( basic8(pair(2,1)), 3, Integer, pat_tests );
 equalityTest ( basic8(pair(3,1)), 4, Integer, pat_tests );
 
+
+-- more testing mixing variable and constructor patterns
+function basic9
+Integer ::= a::Maybe<Integer> b::Maybe<Integer> c::Maybe<Integer>
+{
+return case a, b, c of
+| aa, just(bb), nothing() -> bb
+| just(aa), bb, cc -> aa
+| aa, just(bb), just(cc) -> bb + cc
+| nothing(), bb, cc -> 0
+end;
+}
+
+equalityTest ( basic9(just(1), just(2), just(5)), 1, Integer, pat_tests ) ;
+equalityTest ( basic9(just(1), just(2), nothing()), 2, Integer, pat_tests ) ;
+equalityTest ( basic9(just(1), nothing(), just(5)), 1, Integer, pat_tests ) ;
+equalityTest ( basic9(just(1), nothing(), nothing()), 1, Integer, pat_tests ) ;
+equalityTest ( basic9(nothing(), just(2), just(5)), 7, Integer, pat_tests ) ;
+equalityTest ( basic9(nothing(), just(2), nothing()), 2, Integer, pat_tests ) ;
+equalityTest ( basic9(nothing(), nothing(), just(5)), 0, Integer, pat_tests ) ;
+equalityTest ( basic9(nothing(), nothing(), nothing()), 0, Integer, pat_tests ) ;
+
diff --git a/test/silver_features/Monoid.sv b/test/silver_features/Monoid.sv
index 390fac9ab..62b37a64b 100644
--- a/test/silver_features/Monoid.sv
+++ b/test/silver_features/Monoid.sv
@@ -50,7 +50,7 @@ top::Thing1 ::= Thing2
 {}
 
 -- Test for both parts of 2-part error message
-wrongCode "In propagate for production silver_features:thing2Thing1" {
+wrongCode "In propagate of things for production silver_features:thing2Thing1" {
   propagate things on Thing1;
 }
 wrongCode "things has type [Integer] but the expression being assigned to it has type [Float]" {
diff --git a/test/silver_features/Strategy.sv b/test/silver_features/Strategy.sv
new file mode 100644
index 000000000..8d41ea92b
--- /dev/null
+++ b/test/silver_features/Strategy.sv
@@ -0,0 +1,183 @@
+grammar silver_features;
+
+import core:monad;
+
+strategy attribute elimPlusZero =
+  bottomUp(try(rule on SExpr of addSExpr(e, constSExpr(0)) -> e end));
+
+nonterminal SExpr with elimPlusZero;
+
+abstract production addSExpr
+top::SExpr ::= e1::SExpr e2::SExpr
+{
+  propagate elimPlusZero;
+}
+abstract production constSExpr
+top::SExpr ::= i::Integer
+{
+  propagate elimPlusZero;
+}
+abstract production idSExpr
+top::SExpr ::= id::String
+{
+  propagate elimPlusZero;
+}
+
+nonterminal SStmt with elimPlusZero;
+abstract production seqSStmt
+top::SStmt ::= s1::SStmt s2::SStmt
+{
+  propagate elimPlusZero;
+}
+abstract production assignSStmt
+top::SStmt ::= n::String e::SExpr
+{
+  propagate elimPlusZero;
+}
+
+equalityTest(
+  hackUnparse(addSExpr(constSExpr(42), constSExpr(0)).elimPlusZero),
+  "silver_features:constSExpr(42)",
+  String, silver_tests);
+
+equalityTest(
+  hackUnparse(addSExpr(addSExpr(constSExpr(42), constSExpr(0)), constSExpr(0)).elimPlusZero),
+  "silver_features:constSExpr(42)",
+  String, silver_tests);
+
+equalityTest(
+  hackUnparse(
+    seqSStmt(
+      assignSStmt("a", addSExpr(constSExpr(42), constSExpr(0))),
+      assignSStmt("b", addSExpr(addSExpr(idSExpr("a"), constSExpr(0)), constSExpr(0)))).elimPlusZero),
+  "silver_features:seqSStmt(silver_features:assignSStmt(\"a\", silver_features:constSExpr(42)), silver_features:assignSStmt(\"b\", silver_features:idSExpr(\"a\")))",
+  String, silver_tests);
+
+partial strategy attribute removeLastStmt =
+    rule on SStmt of
+    | seqSStmt(s, assignSStmt(_, _)) -> s
+    end <+
+    seqSStmt(id, removeLastStmt)
+  occurs on SStmt, SExpr;
+propagate removeLastStmt on SStmt, SExpr;
+
+equalityTest(
+  hackUnparse(
+    seqSStmt(
+      assignSStmt("a", addSExpr(constSExpr(42), constSExpr(0))),
+      assignSStmt("b", addSExpr(addSExpr(idSExpr("a"), constSExpr(0)), constSExpr(0)))).removeLastStmt),
+  "core:just(silver_features:assignSStmt(\"a\", silver_features:addSExpr(silver_features:constSExpr(42), silver_features:constSExpr(0))))",
+  String, silver_tests);
+
+equalityTest(
+  hackUnparse(
+    assignSStmt("a", addSExpr(constSExpr(42), constSExpr(0))).removeLastStmt),
+  "core:nothing()",
+  String, silver_tests);
+
+equalityTest(
+  hackUnparse(
+    addSExpr(constSExpr(42), constSExpr(0)).removeLastStmt),
+  "core:nothing()",
+  String, silver_tests);
+
+
+functor attribute incConstsF occurs on SStmt, SExpr;
+propagate incConstsF on SStmt, SExpr excluding constSExpr;
+aspect production constSExpr
+top::SExpr ::= i::Integer
+{ top.incConstsF = constSExpr(i + 1); }
+
+strategy attribute incConsts =
+  (fail <+ id <+ fail) <*
+  allTopDown(
+    rule on SExpr of
+    | constSExpr(i) -> constSExpr(i + 1)
+    end) occurs on SStmt, SExpr;
+propagate incConsts on SStmt, SExpr;
+
+strategy attribute incTwice = incConstsF <* incConsts
+  occurs on SStmt, SExpr;
+propagate incTwice on SStmt, SExpr;
+
+equalityTest(
+  hackUnparse(
+    assignSStmt("a", addSExpr(constSExpr(42), constSExpr(0))).incTwice),
+  "silver_features:assignSStmt(\"a\", silver_features:addSExpr(silver_features:constSExpr(44), silver_features:constSExpr(2)))",
+  String, silver_tests);
+
+
+autocopy attribute target::String occurs on SStmt, SExpr;
+strategy attribute incTargetConsts =
+  allTopDown(
+    rule on top::SStmt of
+    | assignSStmt(n, _) when n == top.target -> top
+    end <* incConsts)
+  occurs on SStmt, SExpr;
+propagate incTargetConsts on SStmt, SExpr;
+
+equalityTest(
+  hackUnparse(
+    decorate
+      seqSStmt(
+        assignSStmt("a", addSExpr(constSExpr(42), constSExpr(0))),
+        assignSStmt("b", addSExpr(addSExpr(idSExpr("a"), constSExpr(2)), constSExpr(17))))
+    with {target = "b";}.incTargetConsts),
+  "silver_features:seqSStmt(silver_features:assignSStmt(\"a\", silver_features:addSExpr(silver_features:constSExpr(42), silver_features:constSExpr(0))), silver_features:assignSStmt(\"b\", silver_features:addSExpr(silver_features:addSExpr(silver_features:idSExpr(\"a\"), silver_features:constSExpr(3)), silver_features:constSExpr(18))))",
+  String, silver_tests);
+
+strategy attribute incThenElim = incConsts <* elimPlusZero
+  occurs on SStmt, SExpr;
+propagate incThenElim on SStmt, SExpr;
+
+equalityTest(
+  hackUnparse(
+    assignSStmt("a", addSExpr(constSExpr(42), constSExpr(-1))).incThenElim),
+  "silver_features:assignSStmt(\"a\", silver_features:constSExpr(43))",
+  String, silver_tests);
+
+
+strategy attribute incAll = all(incConsts) occurs on SStmt, SExpr;
+partial strategy attribute incSome = some(incConsts) occurs on SStmt, SExpr;
+partial strategy attribute incOne = one(incConsts) occurs on SStmt, SExpr;
+partial strategy attribute incFstElimSnd = seqSStmt(incConsts, elimPlusZero) occurs on SStmt, SExpr;
+propagate incAll, incSome, incOne, incFstElimSnd on SStmt, SExpr;
+
+equalityTest(
+  hackUnparse(
+    seqSStmt(
+      assignSStmt("a", constSExpr(1)),
+      assignSStmt("b", constSExpr(2))).incAll),
+  "silver_features:seqSStmt(silver_features:assignSStmt(\"a\", silver_features:constSExpr(2)), silver_features:assignSStmt(\"b\", silver_features:constSExpr(3)))",
+  String, silver_tests);
+equalityTest(
+  hackUnparse(
+    seqSStmt(
+      assignSStmt("a", constSExpr(1)),
+      assignSStmt("b", constSExpr(2))).incSome),
+  "core:just(silver_features:seqSStmt(silver_features:assignSStmt(\"a\", silver_features:constSExpr(2)), silver_features:assignSStmt(\"b\", silver_features:constSExpr(3))))",
+  String, silver_tests);
+equalityTest(
+  hackUnparse(
+    seqSStmt(
+      assignSStmt("a", constSExpr(1)),
+      assignSStmt("b", constSExpr(2))).incOne),
+  "core:just(silver_features:seqSStmt(silver_features:assignSStmt(\"a\", silver_features:constSExpr(2)), silver_features:assignSStmt(\"b\", silver_features:constSExpr(2))))",
+  String, silver_tests);
+equalityTest(
+  hackUnparse(
+    seqSStmt(
+      assignSStmt("a", addSExpr(constSExpr(1), constSExpr(0))),
+      assignSStmt("b", addSExpr(constSExpr(2), constSExpr(0)))).incFstElimSnd),
+  "core:just(silver_features:seqSStmt(silver_features:assignSStmt(\"a\", silver_features:addSExpr(silver_features:constSExpr(2), silver_features:constSExpr(1))), silver_features:assignSStmt(\"b\", silver_features:constSExpr(2))))",
+  String, silver_tests);
+
+-- Negative tests
+inherited attribute badInh<a>::a;
+wrongCode "cannot be used as total strategy" {
+  strategy attribute badInhS = badInh;
+}
+
+warnCode "is not total" {
+  strategy attribute notTotal = rule on SExpr of constSExpr(i) -> constSExpr(i + 1) end;
+}
diff --git a/test/silver_features/rewrite/expreval/AbstractSyntax.sv b/test/silver_features/rewrite/expreval/AbstractSyntax.sv
index 8d84c2d3d..65445df60 100644
--- a/test/silver_features/rewrite/expreval/AbstractSyntax.sv
+++ b/test/silver_features/rewrite/expreval/AbstractSyntax.sv
@@ -3,6 +3,7 @@ grammar silver_features:rewrite:expreval;
 imports silver:langutil;
 imports silver:langutil:pp;
 imports silver:rewrite;
+imports core:monad;
 
 synthesized attribute needsParens::Boolean;
 
@@ -63,6 +64,7 @@ String ::= e::Expr
   return show(80, e.pp);
 }
 
+-- Term rewriting library/extension
 function subst
 Strategy ::= n::String e::Expr
 {
@@ -120,3 +122,67 @@ global simplifyFrac::Strategy =
   end;
 
 global eval::Strategy = innermost(evalStep <+ simplifyConstIdent <+ simplifyFrac);
+
+-- Strategy attributes
+autocopy attribute substName::String;
+autocopy attribute substExpr::Expr;
+strategy attribute substRes =
+  allTopDown(
+    rule on top::Expr of
+    | var(n1) when top.substName == n1 -> top.substExpr
+    end);
+attribute substName, substExpr, substRes occurs on Expr;
+propagate substRes on Expr;
+
+partial strategy attribute evalStep =
+  rule on Expr of
+  | add(const(a), const(b)) -> const(a + b)
+  | sub(const(a), const(b)) -> const(a - b)
+  | mul(const(a), const(b)) -> const(a * b)
+  | div(const(a), const(b)) when b != 0 && a % b == 0 -> const(a / b)
+  | div(const(a), const(b)) when b != 0 && gcd(a, b) > 1 ->
+     let g::Integer = gcd(a, b) in div(const(a / g), const(b / g)) end
+  -- This rule does not respect lexical shadowing;
+  -- it is assumed that the overall rewrite will be done in an innermost order.
+  | letE(n, e1, e2) -> decorate e2 with {substName = n; substExpr = e1;}.substRes
+  end;
+
+partial strategy attribute simplifyConstIdent =
+  rule on Expr of
+  | add(a, const(0)) -> a
+  | add(const(0), a) -> a
+  
+  | sub(a, const(0)) -> a
+  
+  | mul(_, const(0)) -> const(0)
+  | mul(const(0), _) -> const(0)
+  | mul(a, const(1)) -> a
+  | mul(const(1), a) -> a
+  
+  | div(const(0), _) -> const(0)
+  | div(a, const(1)) -> a
+  end;
+
+partial strategy attribute simplifyFrac =
+  rule on Expr of
+  | add(div(a, b), c) -> div(add(a, mul(b, c)), b)
+  | sub(div(a, b), c) -> div(sub(a, mul(b, c)), b)
+  | mul(div(a, b), c) -> div(mul(a, c), b)
+  | div(div(a, b), c) -> div(a, mul(b, c))
+  
+  | add(a, div(b, c)) -> div(add(mul(a, c), b), c)
+  | sub(a, div(b, c)) -> div(sub(mul(a, c), b), c)
+  | mul(a, div(b, c)) -> div(mul(a, b), c)
+  | div(a, div(b, c)) -> div(mul(a, c), b)
+  
+  | add(div(a, b), div(c, d)) -> div(add(mul(a, d), mul(c, b)), mul(b, d))
+  | sub(div(a, b), div(c, d)) -> div(sub(mul(a, d), mul(c, b)), mul(b, d))
+  | mul(div(a, b), div(c, d)) -> div(mul(a, c), mul(c, d))
+  | div(div(a, b), div(c, d)) -> div(mul(a, d), mul(b, c))
+  end;
+
+strategy attribute eval = innermost(evalStep <+ simplifyConstIdent <+ simplifyFrac);
+
+attribute evalStep, simplifyConstIdent, simplifyFrac, eval occurs on Expr;
+propagate evalStep, simplifyConstIdent, simplifyFrac, eval on Expr;
+
diff --git a/test/silver_features/rewrite/expreval/Tests.sv b/test/silver_features/rewrite/expreval/Tests.sv
index 3efc9e0d0..214867832 100644
--- a/test/silver_features/rewrite/expreval/Tests.sv
+++ b/test/silver_features/rewrite/expreval/Tests.sv
@@ -4,26 +4,44 @@ import silver:testing;
 import lib:extcore;
 import silver_features;
 
-global result1::Maybe<Expr> = rewriteWith(eval, parseExpr("1 + (2 * 3)"));
-equalityTest(result1.isJust, true, Boolean, silver_tests);
-equalityTest(showExpr(fromMaybe(const(12345), result1)), "7", String, silver_tests);
+global test1::Expr = parseExpr("1 + (2 * 3)");
+global result1a::Maybe<Expr> = rewriteWith(eval, test1);
+equalityTest(result1a.isJust, true, Boolean, silver_tests);
+equalityTest(showExpr(fromMaybe(const(12345), result1a)), "7", String, silver_tests);
+global result1b::Expr = test1.eval;
+equalityTest(showExpr(result1b), "7", String, silver_tests);
 
-global result2::Maybe<Expr> = rewriteWith(eval, parseExpr("7 + 4 - ((1 + 1) / 0)"));
-equalityTest(result2.isJust, true, Boolean, silver_tests);
-equalityTest(showExpr(fromMaybe(const(12345), result2)), "-2 / 0", String, silver_tests);
+global test2::Expr = parseExpr("7 + 4 - ((1 + 1) / 0)");
+global result2a::Maybe<Expr> = rewriteWith(eval, test2);
+equalityTest(result2a.isJust, true, Boolean, silver_tests);
+equalityTest(showExpr(fromMaybe(const(12345), result2a)), "-2 / 0", String, silver_tests);
+global result2b::Expr = test2.eval;
+equalityTest(showExpr(result2b), "-2 / 0", String, silver_tests);
 
-global result3::Maybe<Expr> = rewriteWith(eval, parseExpr("(2 + 2) / 6"));
-equalityTest(result3.isJust, true, Boolean, silver_tests);
-equalityTest(showExpr(fromMaybe(const(12345), result3)), "2 / 3", String, silver_tests);
+global test3::Expr = parseExpr("(2 + 2) / 6");
+global result3a::Maybe<Expr> = rewriteWith(eval, test3);
+equalityTest(result3a.isJust, true, Boolean, silver_tests);
+equalityTest(showExpr(fromMaybe(const(12345), result3a)), "2 / 3", String, silver_tests);
+global result3b::Expr = test3.eval;
+equalityTest(showExpr(result3b), "2 / 3", String, silver_tests);
 
-global result4::Maybe<Expr> = rewriteWith(eval, parseExpr("1 + 1 / (1 + 1 / (1 + 1 / (1 + 1 / (1 + 1 / (1 + 1 / (1 + 1))))))"));
-equalityTest(result4.isJust, true, Boolean, silver_tests);
-equalityTest(showExpr(fromMaybe(const(12345), result4)), "34 / 21", String, silver_tests);
+global test4::Expr = parseExpr("1 + 1 / (1 + 1 / (1 + 1 / (1 + 1 / (1 + 1 / (1 + 1 / (1 + 1))))))");
+global result4a::Maybe<Expr> = rewriteWith(eval, test4);
+equalityTest(result4a.isJust, true, Boolean, silver_tests);
+equalityTest(showExpr(fromMaybe(const(12345), result4a)), "34 / 21", String, silver_tests);
+global result4b::Expr = test4.eval;
+equalityTest(showExpr(result4b), "34 / 21", String, silver_tests);
 
-global result5::Maybe<Expr> = rewriteWith(eval, parseExpr("let a = 1 / 2 in let b = a * 2 in a + b"));
-equalityTest(result5.isJust, true, Boolean, silver_tests);
-equalityTest(showExpr(fromMaybe(const(12345), result5)), "3 / 2", String, silver_tests);
+global test5::Expr = parseExpr("let a = 1 / 2 in let b = a * 2 in a + b");
+global result5a::Maybe<Expr> = rewriteWith(eval, test5);
+equalityTest(result5a.isJust, true, Boolean, silver_tests);
+equalityTest(showExpr(fromMaybe(const(12345), result5a)), "3 / 2", String, silver_tests);
+global result5b::Expr = test5.eval;
+equalityTest(showExpr(result5b), "3 / 2", String, silver_tests);
 
-global result6::Maybe<Expr> = rewriteWith(eval, parseExpr("0 + 1 * a - 2 / b"));
-equalityTest(result6.isJust, true, Boolean, silver_tests);
-equalityTest(showExpr(fromMaybe(const(12345), result6)), "((a * b) - 2) / b", String, silver_tests);
+global test6::Expr = parseExpr("0 + 1 * a - 2 / b");
+global result6a::Maybe<Expr> = rewriteWith(eval, test6);
+equalityTest(result6a.isJust, true, Boolean, silver_tests);
+equalityTest(showExpr(fromMaybe(const(12345), result6a)), "((a * b) - 2) / b", String, silver_tests);
+global result6b::Expr = test6.eval;
+equalityTest(showExpr(result6b), "((a * b) - 2) / b", String, silver_tests);