Coccinelle release 1.0.0-rc3
[bpt/coccinelle.git] / parsing_cocci / iso_pattern.ml
index 16d484b..bdbb350 100644 (file)
@@ -1,23 +1,25 @@
 (*
-* Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
-* Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller
-* This file is part of Coccinelle.
-* 
-* Coccinelle is free software: you can redistribute it and/or modify
-* it under the terms of the GNU General Public License as published by
-* the Free Software Foundation, according to version 2 of the License.
-* 
-* Coccinelle is distributed in the hope that it will be useful,
-* but WITHOUT ANY WARRANTY; without even the implied warranty of
-* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-* GNU General Public License for more details.
-* 
-* You should have received a copy of the GNU General Public License
-* along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
-* 
-* The authors reserve the right to distribute this or future versions of
-* Coccinelle under other licenses.
-*)
+ * Copyright 2010, INRIA, University of Copenhagen
+ * Julia Lawall, Rene Rydhof Hansen, Gilles Muller, Nicolas Palix
+ * Copyright 2005-2009, Ecole des Mines de Nantes, University of Copenhagen
+ * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
+ * This file is part of Coccinelle.
+ *
+ * Coccinelle is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, according to version 2 of the License.
+ *
+ * Coccinelle is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Coccinelle.  If not, see <http://www.gnu.org/licenses/>.
+ *
+ * The authors reserve the right to distribute this or future versions of
+ * Coccinelle under other licenses.
+ *)
 
 
 (* Potential problem: offset of mcode is not updated when an iso is
@@ -26,6 +28,8 @@ same offset.  On the other hand, at the moment offset only seems to be used
 before this phase.  Furthermore add_dot_binding relies on the offset to
 remain the same between matching an iso and instantiating it with bindings. *)
 
+(* Consider whether ... in iso should match <... ...> in smpl? *)
+
 (* --------------------------------------------------------------------- *)
 (* match a SmPL expression against a SmPL abstract syntax tree,
 either - or + *)
@@ -44,11 +48,12 @@ type isomorphism =
 
 let strip_info =
   let mcode (term,_,_,_,_,_) =
-    (term,Ast0.NONE,Ast0.default_info(),Ast0.PLUS,ref Ast0.NoMetaPos,-1) in
+    (term,Ast0.NONE,Ast0.default_info(),Ast0.PLUS Ast.ONE,
+     ref [],-1) in
   let donothing r k e =
     let x = k e in
     {(Ast0.wrap (Ast0.unwrap x)) with
-      Ast0.mcodekind = ref Ast0.PLUS;
+      Ast0.mcodekind = ref (Ast0.PLUS Ast.ONE);
       Ast0.true_if_test = x.Ast0.true_if_test} in
   V0.flat_rebuilder
     mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
@@ -71,7 +76,8 @@ let anything_equal = function
   | (Ast0.DotsCaseTag(d1),Ast0.DotsCaseTag(d2)) ->
       failwith "not a possible variable binding"
   | (Ast0.IdentTag(d1),Ast0.IdentTag(d2)) ->
-      (strip_info.VT0.rebuilder_rec_ident d1) = (strip_info.VT0.rebuilder_rec_ident d2)
+      (strip_info.VT0.rebuilder_rec_ident d1) =
+      (strip_info.VT0.rebuilder_rec_ident d2)
   | (Ast0.ExprTag(d1),Ast0.ExprTag(d2)) ->
       (strip_info.VT0.rebuilder_rec_expression d1) =
       (strip_info.VT0.rebuilder_rec_expression d2)
@@ -114,12 +120,14 @@ let dot_term (var1,_,info,_,_,_) =
 
 
 type reason =
-    NotPure of Ast0.pure * (string * string) * Ast0.anything
-  | NotPureLength of (string * string)
+    NotPure of Ast0.pure * Ast.meta_name * Ast0.anything
+  | NotPureLength of Ast.meta_name
   | ContextRequired of Ast0.anything
   | NonMatch
   | Braces of Ast0.statement
-  | Position of string * string
+  | Nest of Ast0.statement
+  | Position of Ast.meta_name
+  | Multiposition
   | TypeMatch of reason list
 
 let rec interpret_reason name line reason printer =
@@ -154,9 +162,15 @@ let rec interpret_reason name line reason printer =
       Printf.printf "braces must be all minus (plus code allowed) or all\ncontext (plus code not allowed in the body) to match:\n";
       Unparse_ast0.statement "" s;
       Format.print_newline()
+  | Nest(s) ->
+      Printf.printf "iso with nest doesn't match whencode (TODO):\n";
+      Unparse_ast0.statement "" s;
+      Format.print_newline()
   | Position(rule,name) ->
       Printf.printf "position variable %s.%s conflicts with an isomorphism\n"
-       rule name;
+       rule name
+  | Multiposition _ ->
+      Printf.printf "multiple position variables conflict with an isomorphism\n"
   | TypeMatch reason_list ->
       List.iter (function r -> interpret_reason name line r printer)
        reason_list
@@ -285,11 +299,11 @@ let rec is_pure_context s =
       | Ast0.MINUS(mc) ->
          (match !mc with
        (* do better for the common case of replacing a stmt by another one *)
-           ([[Ast.StatementTag(s)]],_) ->
+           (Ast.REPLACEMENT([[Ast.StatementTag(s)]],_),_) ->
              (match Ast.unwrap s with
                Ast.IfThen(_,_,_) -> false (* potentially dangerous *)
              | _ -> true)
-         |     (_,_) -> false)
+         | (_,_) -> false)
       | _ -> false))
 
 let is_minus e =
@@ -303,20 +317,24 @@ let match_list matcher is_list_matcher do_list_match la lb =
     | _ -> return false in
   loop (la,lb)
 
+let all_caps = Str.regexp "^[A-Z_][A-Z_0-9]*$"
+
 let match_maker checks_needed context_required whencode_allowed =
 
-  let check_mcode pmc cmc binding =
+  let check_mcode pmc (*pattern*) cmc (*code*) binding =
     if checks_needed
     then
       match Ast0.get_pos cmc with
-       (Ast0.MetaPos (name,_,_)) as x ->
+        [(Ast0.MetaPos (name,_,_)) as x] ->
          (match Ast0.get_pos pmc with
-           Ast0.MetaPos (name1,_,_) ->
+           [Ast0.MetaPos (name1,_,_)] ->
              add_binding name1 (Ast0.MetaPosTag x) binding
-         | Ast0.NoMetaPos ->
+         | [] ->
              let (rule,name) = Ast0.unwrap_mcode name in
-             Fail (Position(rule,name)))
-      | Ast0.NoMetaPos -> OK binding
+             Fail (Position(rule,name))
+         | _ -> Fail Multiposition)
+      | [] -> OK binding
+      | _ -> Fail Multiposition
     else OK binding in
 
   let match_dots matcher is_list_matcher do_list_match d1 d2 =
@@ -357,7 +375,9 @@ let match_maker checks_needed context_required whencode_allowed =
              (Ast.NOTHING,_,_) -> Ast0.PureContext
            | _ -> Ast0.Context)
        | Ast0.MINUS(mc) ->
-           (match !mc with ([],_) -> Ast0.Pure | _ ->  Ast0.Impure)
+           (match !mc with
+             (Ast.NOREPLACEMENT,_) -> Ast0.Pure
+           | _ ->  Ast0.Impure)
        | _ -> Ast0.Impure in
     let donothing r k e =
       bind (pure_mcodekind (Ast0.get_mcodekind e)) (k e) in
@@ -370,7 +390,7 @@ let match_maker checks_needed context_required whencode_allowed =
     let ident r k i =
       bind (bind (pure_mcodekind (Ast0.get_mcodekind i)) (k i))
        (match Ast0.unwrap i with
-         Ast0.MetaId(name,_,pure) | Ast0.MetaFunc(name,_,pure)
+         Ast0.MetaId(name,_,_,pure) | Ast0.MetaFunc(name,_,pure)
        | Ast0.MetaLocalFunc(name,_,pure) -> pure
        | _ -> Ast0.Impure) in
 
@@ -391,7 +411,7 @@ let match_maker checks_needed context_required whencode_allowed =
     let init r k t =
       bind (bind (pure_mcodekind (Ast0.get_mcodekind t)) (k t))
        (match Ast0.unwrap t with
-         Ast0.MetaInit(name,pure) -> pure
+         Ast0.MetaInit(name,pure) | Ast0.MetaInitList(name,_,pure) -> pure
        | _ -> Ast0.Impure) in
 
     let param r k p =
@@ -400,6 +420,14 @@ let match_maker checks_needed context_required whencode_allowed =
          Ast0.MetaParam(name,pure) | Ast0.MetaParamList(name,_,pure) -> pure
        | _ -> Ast0.Impure) in
 
+    let decl r k d =
+      bind (bind (pure_mcodekind (Ast0.get_mcodekind d)) (k d))
+       (match Ast0.unwrap d with
+         Ast0.MetaDecl(name,pure) | Ast0.MetaField(name,pure)
+       | Ast0.MetaFieldList(name,_,pure) ->
+           pure
+       | _ -> Ast0.Impure) in
+
     let stmt r k s =
       bind (bind (pure_mcodekind (Ast0.get_mcodekind s)) (k s))
        (match Ast0.unwrap s with
@@ -409,7 +437,7 @@ let match_maker checks_needed context_required whencode_allowed =
     V0.flat_combiner bind option_default
       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
       donothing donothing donothing donothing donothing donothing
-      ident expression typeC init param donothing stmt donothing
+      ident expression typeC init param decl stmt donothing
       donothing in
 
   let add_pure_list_binding name pure is_pure builder1 builder2 lst =
@@ -468,7 +496,7 @@ let match_maker checks_needed context_required whencode_allowed =
 
   let rec match_ident pattern id =
     match Ast0.unwrap pattern with
-      Ast0.MetaId(name,_,pure) ->
+      Ast0.MetaId(name,_,_,pure) ->
        (add_pure_binding name pure pure_sp_code.VT0.combiner_rec_ident
          (function id -> Ast0.IdentTag id) id)
     | Ast0.MetaFunc(name,_,pure) -> failwith "metafunc not supported"
@@ -481,6 +509,8 @@ let match_maker checks_needed context_required whencode_allowed =
              if mcode_equal namea nameb
              then check_mcode namea nameb
              else return false
+         | (Ast0.DisjId(_,ids,_,_),_) ->
+             failwith "not allowed in the pattern of an isomorphism"
          | (Ast0.OptIdent(ida),Ast0.OptIdent(idb))
          | (Ast0.UniqueIdent(ida),Ast0.UniqueIdent(idb)) ->
              match_ident ida idb
@@ -500,6 +530,13 @@ let match_maker checks_needed context_required whencode_allowed =
              let rec matches e =
                match Ast0.unwrap e with
                  Ast0.Constant(c) -> true
+               | Ast0.Ident(c) ->
+                   (match Ast0.unwrap c with
+                     Ast0.Id(nm) ->
+                       let nm = Ast0.unwrap_mcode nm in
+                       (* all caps is a const *)
+                       Str.string_match all_caps nm 0
+                   | _ -> false)
                | Ast0.Cast(lp,ty,rp,e) -> matches e
                | Ast0.SizeOfExpr(se,exp) -> true
                | Ast0.SizeOfType(se,lp,ty,rp) -> true
@@ -592,7 +629,8 @@ let match_maker checks_needed context_required whencode_allowed =
                    expr
                else return false
          | None ->
-             add_pure_binding name pure pure_sp_code.VT0.combiner_rec_expression
+             add_pure_binding name pure
+               pure_sp_code.VT0.combiner_rec_expression
                (function expr -> Ast0.ExprTag expr)
                expr
        else return false
@@ -762,9 +800,16 @@ let match_maker checks_needed context_required whencode_allowed =
              conjunct_many_bindings
                [check_mcode lb1 lb; check_mcode rb1 rb;
                  match_typeC tya tyb; match_option match_expr sizea sizeb]
-         | (Ast0.EnumName(kinda,namea),Ast0.EnumName(kindb,nameb)) ->
+         | (Ast0.EnumName(kinda,Some namea),
+            Ast0.EnumName(kindb,Some nameb)) ->
              conjunct_bindings (check_mcode kinda kindb)
                (match_ident namea nameb)
+         | (Ast0.EnumDef(tya,lb1,idsa,rb1),
+            Ast0.EnumDef(tyb,lb,idsb,rb)) ->
+              conjunct_many_bindings
+                [check_mcode lb1 lb; check_mcode rb1 rb;
+                  match_typeC tya tyb;
+                  match_dots match_expr no_list do_nolist_match idsa idsb]
          | (Ast0.StructUnionName(kinda,Some namea),
             Ast0.StructUnionName(kindb,Some nameb)) ->
               if mcode_equal kinda kindb
@@ -782,7 +827,7 @@ let match_maker checks_needed context_required whencode_allowed =
              if mcode_equal namea nameb
              then check_mcode namea nameb
              else return false
-         | (Ast0.DisjType(_,typesa,_,_),Ast0.DisjType(_,typesb,_,_)) ->
+         | (Ast0.DisjType(_,typesa,_,_),_) ->
              failwith "not allowed in the pattern of an isomorphism"
          | (Ast0.OptType(tya),Ast0.OptType(tyb))
          | (Ast0.UniqueType(tya),Ast0.UniqueType(tyb)) -> match_typeC tya tyb
@@ -792,63 +837,74 @@ let match_maker checks_needed context_required whencode_allowed =
        else return_false (ContextRequired (Ast0.TypeCTag t))
 
   and match_decl pattern d =
-    if not(checks_needed) or not(context_required) or is_context d
-    then
-      match (Ast0.unwrap pattern,Ast0.unwrap d) with
-       (Ast0.Init(stga,tya,ida,eq1,inia,sc1),
-        Ast0.Init(stgb,tyb,idb,eq,inib,sc)) ->
-         if bool_match_option mcode_equal stga stgb
-         then
-           conjunct_many_bindings
-             [check_mcode eq1 eq; check_mcode sc1 sc;
-               match_option check_mcode stga stgb;
-               match_typeC tya tyb; match_ident ida idb;
-               match_init inia inib]
-         else return false
-      | (Ast0.UnInit(stga,tya,ida,sc1),Ast0.UnInit(stgb,tyb,idb,sc)) ->
-         if bool_match_option mcode_equal stga stgb
-         then
-           conjunct_many_bindings
-             [check_mcode sc1 sc; match_option check_mcode stga stgb;
-               match_typeC tya tyb; match_ident ida idb]
-         else return false
-      | (Ast0.MacroDecl(namea,lp1,argsa,rp1,sc1),
-        Ast0.MacroDecl(nameb,lp,argsb,rp,sc)) ->
-          conjunct_many_bindings
-            [match_ident namea nameb;
-              check_mcode lp1 lp; check_mcode rp1 rp;
-              check_mcode sc1 sc;
-              match_dots match_expr is_elist_matcher do_elist_match
-                argsa argsb]
-      | (Ast0.TyDecl(tya,sc1),Ast0.TyDecl(tyb,sc)) ->
-         conjunct_bindings (check_mcode sc1 sc) (match_typeC tya tyb)
-      | (Ast0.Typedef(stga,tya,ida,sc1),Ast0.Typedef(stgb,tyb,idb,sc)) ->
-         conjunct_bindings (check_mcode sc1 sc)
-           (conjunct_bindings (match_typeC tya tyb) (match_typeC ida idb))
-      | (Ast0.DisjDecl(_,declsa,_,_),Ast0.DisjDecl(_,declsb,_,_)) ->
-         failwith "not allowed in the pattern of an isomorphism"
-      | (Ast0.Ddots(d1,None),Ast0.Ddots(d,None)) -> check_mcode d1 d
-      |        (Ast0.Ddots(dd,None),Ast0.Ddots(d,Some wc)) ->
-         conjunct_bindings (check_mcode dd d)
+    match Ast0.unwrap pattern with
+      Ast0.MetaDecl(name,pure) ->
+       add_pure_binding name pure pure_sp_code.VT0.combiner_rec_declaration
+         (function d -> Ast0.DeclTag d)
+         d
+    | Ast0.MetaField(name,pure) ->
+       add_pure_binding name pure pure_sp_code.VT0.combiner_rec_declaration
+         (function d -> Ast0.DeclTag d)
+         d
+    | Ast0.MetaFieldList(name,_,pure) -> failwith "metafieldlist not supporte"
+    | up ->
+       if not(checks_needed) or not(context_required) or is_context d
+       then
+         match (up,Ast0.unwrap d) with
+           (Ast0.Init(stga,tya,ida,eq1,inia,sc1),
+            Ast0.Init(stgb,tyb,idb,eq,inib,sc)) ->
+              if bool_match_option mcode_equal stga stgb
+              then
+                conjunct_many_bindings
+                  [check_mcode eq1 eq; check_mcode sc1 sc;
+                    match_option check_mcode stga stgb;
+                    match_typeC tya tyb; match_ident ida idb;
+                    match_init inia inib]
+              else return false
+         | (Ast0.UnInit(stga,tya,ida,sc1),Ast0.UnInit(stgb,tyb,idb,sc)) ->
+             if bool_match_option mcode_equal stga stgb
+             then
+               conjunct_many_bindings
+                 [check_mcode sc1 sc; match_option check_mcode stga stgb;
+                   match_typeC tya tyb; match_ident ida idb]
+             else return false
+         | (Ast0.MacroDecl(namea,lp1,argsa,rp1,sc1),
+            Ast0.MacroDecl(nameb,lp,argsb,rp,sc)) ->
+              conjunct_many_bindings
+                [match_ident namea nameb;
+                  check_mcode lp1 lp; check_mcode rp1 rp;
+                  check_mcode sc1 sc;
+                  match_dots match_expr is_elist_matcher do_elist_match
+                    argsa argsb]
+         | (Ast0.TyDecl(tya,sc1),Ast0.TyDecl(tyb,sc)) ->
+             conjunct_bindings (check_mcode sc1 sc) (match_typeC tya tyb)
+         | (Ast0.Typedef(stga,tya,ida,sc1),Ast0.Typedef(stgb,tyb,idb,sc)) ->
+             conjunct_bindings (check_mcode sc1 sc)
+               (conjunct_bindings (match_typeC tya tyb) (match_typeC ida idb))
+         | (Ast0.DisjDecl(_,declsa,_,_),_) ->
+             failwith "not allowed in the pattern of an isomorphism"
+         | (Ast0.Ddots(d1,None),Ast0.Ddots(d,None)) -> check_mcode d1 d
+         |     (Ast0.Ddots(dd,None),Ast0.Ddots(d,Some wc)) ->
+             conjunct_bindings (check_mcode dd d)
            (* hope that mcode of ddots is unique somehow *)
-           (let (ddots_whencode_allowed,_,_) = whencode_allowed in
-           if ddots_whencode_allowed
-           then add_dot_binding dd (Ast0.DeclTag wc)
-           else
-             (Printf.printf "warning: not applying iso because of whencode";
-              return false))
-      | (Ast0.Ddots(_,Some _),_) ->
-         failwith "whencode not allowed in a pattern1"
-
-      | (Ast0.OptDecl(decla),Ast0.OptDecl(declb))
-      | (Ast0.UniqueDecl(decla),Ast0.UniqueDecl(declb)) ->
-         match_decl decla declb
-      | (_,Ast0.OptDecl(declb))
-      | (_,Ast0.UniqueDecl(declb)) ->
-         match_decl pattern declb
-      | _ -> return false
-    else return_false (ContextRequired (Ast0.DeclTag d))
-
+               (let (ddots_whencode_allowed,_,_) = whencode_allowed in
+               if ddots_whencode_allowed
+               then add_dot_binding dd (Ast0.DeclTag wc)
+               else
+                 (Printf.printf "warning: not applying iso because of whencode";
+                  return false))
+         | (Ast0.Ddots(_,Some _),_) ->
+             failwith "whencode not allowed in a pattern1"
+               
+         | (Ast0.OptDecl(decla),Ast0.OptDecl(declb))
+         | (Ast0.UniqueDecl(decla),Ast0.UniqueDecl(declb)) ->
+             match_decl decla declb
+         | (_,Ast0.OptDecl(declb))
+         | (_,Ast0.UniqueDecl(declb)) ->
+             match_decl pattern declb
+         | _ -> return false
+       else return_false (ContextRequired (Ast0.DeclTag d))
+           
   and match_init pattern i =
     match Ast0.unwrap pattern with
       Ast0.MetaInit(name,pure) ->
@@ -861,8 +917,9 @@ let match_maker checks_needed context_required whencode_allowed =
          match (up,Ast0.unwrap i) with
            (Ast0.InitExpr(expa),Ast0.InitExpr(expb)) ->
              match_expr expa expb
-         | (Ast0.InitList(lb1,initlista,rb1),Ast0.InitList(lb,initlistb,rb))
-           ->
+         | (Ast0.InitList(lb1,initlista,rb1,oa),
+            Ast0.InitList(lb,initlistb,rb,ob))
+           when oa = ob ->
              conjunct_many_bindings
                [check_mcode lb1 lb; check_mcode rb1 rb;
                  match_dots match_init no_list do_nolist_match
@@ -998,7 +1055,8 @@ let match_maker checks_needed context_required whencode_allowed =
                       bodya bodyb
                   else return_false (Braces(s))))
          | (Ast0.ExprStatement(expa,sc1),Ast0.ExprStatement(expb,sc)) ->
-             conjunct_bindings (check_mcode sc1 sc) (match_expr expa expb)
+             conjunct_bindings (check_mcode sc1 sc)
+               (match_option match_expr expa expb)
          | (Ast0.IfThen(if1,lp1,expa,rp1,branch1a,_),
             Ast0.IfThen(if2,lp2,expb,rp2,branch1b,_)) ->
               conjunct_many_bindings
@@ -1043,12 +1101,14 @@ let match_maker checks_needed context_required whencode_allowed =
                   match_dots match_expr is_elist_matcher do_elist_match
                     argsa argsb;
                   match_statement bodya bodyb]
-         | (Ast0.Switch(s1,lp1,expa,rp1,lb1,casesa,rb1),
-            Ast0.Switch(s,lp,expb,rp,lb,casesb,rb)) ->
+         | (Ast0.Switch(s1,lp1,expa,rp1,lb1,declsa,casesa,rb1),
+            Ast0.Switch(s,lp,expb,rp,lb,declsb,casesb,rb)) ->
               conjunct_many_bindings
                 [check_mcode s1 s; check_mcode lp1 lp; check_mcode rp1 rp;
                   check_mcode lb1 lb; check_mcode rb1 rb;
                   match_expr expa expb;
+                  match_dots match_statement is_slist_matcher do_slist_match
+                    declsa declsb;
                   match_dots match_case_line no_list do_nolist_match
                     casesa casesb]
          | (Ast0.Break(b1,sc1),Ast0.Break(b,sc))
@@ -1066,8 +1126,25 @@ let match_maker checks_needed context_required whencode_allowed =
                [check_mcode r1 r; check_mcode sc1 sc; match_expr expa expb]
          | (Ast0.Disj(_,statement_dots_lista,_,_),_) ->
              failwith "disj not supported in patterns"
+         | (Ast0.Nest(_,stmt_dotsa,_,[],multia),
+            Ast0.Nest(_,stmt_dotsb,_,wc,multib)) ->
+              if multia = multib
+              then
+                (match wc with
+                  [] ->
+                 (* not sure this is correct, perhaps too restrictive *)
+                    if not(checks_needed) or is_minus s or
+                      (is_context s &&
+                       List.for_all is_pure_context (Ast0.undots stmt_dotsb))
+                    then
+                      match_dots match_statement
+                        is_slist_matcher do_slist_match
+                        stmt_dotsa stmt_dotsb
+                    else return_false (Braces(s))
+                | _ -> return_false (Nest(s)))
+              else return false (* diff kind of nest *)
          | (Ast0.Nest(_,stmt_dotsa,_,_,_),_) ->
-             failwith "nest not supported in patterns"
+             failwith "nest with whencode not supported in patterns"
          | (Ast0.Exp(expa),Ast0.Exp(expb)) -> match_expr expa expb
          | (Ast0.TopExp(expa),Ast0.TopExp(expb)) -> match_expr expa expb
          | (Ast0.Exp(expa),Ast0.TopExp(expb)) -> match_expr expa expb
@@ -1162,6 +1239,8 @@ let match_maker checks_needed context_required whencode_allowed =
            [check_mcode ca1 ca; check_mcode c1 c; match_expr expa expb;
              match_dots match_statement is_slist_matcher do_slist_match
                codea codeb]
+      | (Ast0.DisjCase(_,case_linesa,_,_),_) ->
+         failwith "not allowed in the pattern of an isomorphism"
       |        (Ast0.OptCase(ca),Ast0.OptCase(cb)) -> match_case_line ca cb
       |        (_,Ast0.OptCase(cb)) -> match_case_line pattern cb
       |        _ -> return false
@@ -1202,7 +1281,8 @@ let make_minus =
      match mcodekind with
        Ast0.CONTEXT(mc) ->
         (match !mc with
-          (Ast.NOTHING,_,_) -> Ast0.MINUS(ref([],Ast0.default_token_info))
+          (Ast.NOTHING,_,_) ->
+            Ast0.MINUS(ref(Ast.NOREPLACEMENT,Ast0.default_token_info))
         | _ -> failwith "make_minus: unexpected befaft")
      | Ast0.MINUS(mc) -> mcodekind (* in the part copied from the src term *)
      | _ -> failwith "make_minus mcode: unexpected mcodekind" in
@@ -1213,10 +1293,11 @@ let make_minus =
       Ast0.CONTEXT(mc) ->
        (match !mc with
          (Ast.NOTHING,_,_) ->
-           mcodekind := Ast0.MINUS(ref([],Ast0.default_token_info))
+           mcodekind :=
+             Ast0.MINUS(ref(Ast.NOREPLACEMENT,Ast0.default_token_info))
        | _ -> failwith "make_minus: unexpected befaft")
     | Ast0.MINUS(_mc) -> () (* in the part copied from the src term *)
-    | Ast0.PLUS -> failwith "make_minus donothing: unexpected plus mcodekind"
+    | Ast0.PLUS -> failwith "make_minus donothing: unexpected plus mcodekind"
     | _ -> failwith "make_minus donothing: unexpected mcodekind" in
 
   let donothing r k e =
@@ -1294,7 +1375,8 @@ let make_minus =
          Ast0.MIXED(mc) | Ast0.CONTEXT(mc) ->
            (match !mc with
              (Ast.NOTHING,_,_) ->
-               mcodekind := Ast0.MINUS(ref([],Ast0.default_token_info));
+               mcodekind :=
+                 Ast0.MINUS(ref(Ast.NOREPLACEMENT,Ast0.default_token_info));
                e
            | _ -> failwith "make_minus: unexpected befaft")
          (* code already processed by an enclosing iso *)
@@ -1324,12 +1406,12 @@ let make_minus =
 let rebuild_mcode start_line =
   let copy_mcodekind = function
       Ast0.CONTEXT(mc) -> Ast0.CONTEXT(ref (!mc))
-    | Ast0.MINUS(mc) -> Ast0.MINUS(ref (!mc))
-    | Ast0.MIXED(mc) -> Ast0.MIXED(ref (!mc))
-    | Ast0.PLUS ->
+    | Ast0.MINUS(mc) ->   Ast0.MINUS(ref (!mc))
+    | Ast0.MIXED(mc) ->   Ast0.MIXED(ref (!mc))
+    | Ast0.PLUS count ->
        (* this function is used elsewhere where we need to rebuild the
           indices, and so we allow PLUS code as well *)
-        Ast0.PLUS in
+        Ast0.PLUS count in
 
   let mcode (term,arity,info,mcodekind,pos,adj) =
     let info =
@@ -1450,21 +1532,26 @@ let lookup name bindings mv_bindings =
 isomorphism *)
 let instantiate bindings mv_bindings =
   let mcode x =
-    match Ast0.get_pos x with
-      Ast0.MetaPos(name,_,_) ->
-       (try
-         match lookup name bindings mv_bindings with
-           Common.Left(Ast0.MetaPosTag(id)) -> Ast0.set_pos id x
-         | _ -> failwith "not possible"
-       with Not_found -> Ast0.set_pos Ast0.NoMetaPos x)
-    | _ -> x in
+    let pos_names =
+      List.map (function Ast0.MetaPos(name,_,_) -> name) (Ast0.get_pos x) in
+    let new_names =
+      List.fold_left
+       (function prev ->
+         function name ->
+           try
+             match lookup name bindings mv_bindings with
+               Common.Left(Ast0.MetaPosTag(id)) -> id::prev
+             | _ -> failwith "not possible"
+           with Not_found -> prev)
+       [] pos_names in
+    Ast0.set_pos new_names x in
   let donothing r k e = k e in
 
   (* cases where metavariables can occur *)
   let identfn r k e =
     let e = k e in
     match Ast0.unwrap e with
-      Ast0.MetaId(name,constraints,pure) ->
+      Ast0.MetaId(name,constraints,seed,pure) ->
        (rebuild_mcode None).VT0.rebuilder_rec_ident
          (match lookup name bindings mv_bindings with
            Common.Left(Ast0.IdentTag(id)) -> id
@@ -1472,7 +1559,7 @@ let instantiate bindings mv_bindings =
          | Common.Right(new_mv) ->
              Ast0.rewrap e
                (Ast0.MetaId
-                  (Ast0.set_mcode_data new_mv name,constraints,pure)))
+                  (Ast0.set_mcode_data new_mv name,constraints,seed,pure)))
     | Ast0.MetaFunc(name,_,pure) -> failwith "metafunc not supported"
     | Ast0.MetaLocalFunc(name,_,pure) -> failwith "metalocalfunc not supported"
     | _ -> e in
@@ -1589,6 +1676,11 @@ let instantiate bindings mv_bindings =
        failwith "metaexprlist not supported"
     | Ast0.Unary(exp,unop) ->
        (match Ast0.unwrap_mcode unop with
+         (* propagate negation only when the propagated and the encountered
+            negation have the same transformation, when there is nothing
+            added to the original one, and when there is nothing added to
+            the expression into which we are doing the propagation.  This
+            may be too conservative. *)
          Ast.Not ->
            let was_meta =
              (* k e doesn't change the outer structure of the term,
@@ -1599,65 +1691,95 @@ let instantiate bindings mv_bindings =
                    Ast0.MetaExpr(name,constraints,x,form,pure) -> true
                  | _ -> false)
              | _ -> failwith "not possible" in
-           let nomodif e =
-             let mc = Ast0.get_mcodekind exp in
-             match mc with
+           let nomodif = function
                Ast0.MINUS(x) ->
                  (match !x with
-                   ([],_) -> true
+                   (Ast.NOREPLACEMENT,_) -> true
                  | _ -> false)
              | Ast0.CONTEXT(x) | Ast0.MIXED(x) ->
                  (match !x with
                    (Ast.NOTHING,_,_) -> true
                  | _ -> false)
              | _ -> failwith "plus not possible" in
-           if was_meta && nomodif exp && nomodif e
+           let same_modif newop oldop =
+             (* only propagate ! is they have the same modification
+                and no + code on the old one (the new one from the iso
+                surely has no + code) *)
+             match (newop,oldop) with
+               (Ast0.MINUS(x1),Ast0.MINUS(x2)) -> nomodif oldop
+             | (Ast0.CONTEXT(x1),Ast0.CONTEXT(x2)) -> nomodif oldop
+             | (Ast0.MIXED(x1),Ast0.MIXED(x2)) -> nomodif oldop
+             | _ -> false in
+           if was_meta
            then
              let idcont x = x in
              let rec negate e (*for rewrapping*) res (*code to process*) k =
                (* k accumulates parens, to keep negation outside if no
                   propagation is possible *)
-               match Ast0.unwrap res with
-                 Ast0.Unary(e1,op) when Ast0.unwrap_mcode op = Ast.Not ->
-                   k (Ast0.rewrap e (Ast0.unwrap e1))
-               | Ast0.Edots(_,_) -> k (Ast0.rewrap e (Ast0.unwrap res))
-               | Ast0.Paren(lp,e,rp) ->
-                   negate e e
-                     (function x ->
-                       k (Ast0.rewrap res (Ast0.Paren(lp,x,rp))))
-               | Ast0.Binary(e1,op,e2) ->
-                   let reb nop = Ast0.rewrap_mcode op (Ast.Logical(nop)) in
-                   let k1 x = k (Ast0.rewrap e x) in
-                   (match Ast0.unwrap_mcode op with
-                     Ast.Logical(Ast.Inf) ->
-                       k1 (Ast0.Binary(e1,reb Ast.SupEq,e2))
-                   | Ast.Logical(Ast.Sup) ->
-                       k1 (Ast0.Binary(e1,reb Ast.InfEq,e2))
-                   | Ast.Logical(Ast.InfEq) ->
-                       k1 (Ast0.Binary(e1,reb Ast.Sup,e2))
-                   | Ast.Logical(Ast.SupEq) ->
-                       k1 (Ast0.Binary(e1,reb Ast.Inf,e2))
-                   | Ast.Logical(Ast.Eq) ->
-                       k1 (Ast0.Binary(e1,reb Ast.NotEq,e2))
-                   | Ast.Logical(Ast.NotEq) ->
-                       k1 (Ast0.Binary(e1,reb Ast.Eq,e2))
-                   | Ast.Logical(Ast.AndLog) ->
-                       k1 (Ast0.Binary(negate e1 e1 idcont,reb Ast.OrLog,
-                                      negate e2 e2 idcont))
-                   | Ast.Logical(Ast.OrLog) ->
-                       k1 (Ast0.Binary(negate e1 e1 idcont,reb Ast.AndLog,
-                                      negate e2 e2 idcont))
-                   | _ ->
-                       Ast0.rewrap e
-                         (Ast0.Unary(k res,Ast0.rewrap_mcode op Ast.Not)))
-               | Ast0.DisjExpr(lp,exps,mids,rp) ->
+               if nomodif (Ast0.get_mcodekind e)
+               then
+                 match Ast0.unwrap res with
+                   Ast0.Unary(e1,op) when Ast0.unwrap_mcode op = Ast.Not &&
+                     same_modif
+                       (Ast0.get_mcode_mcodekind unop)
+                       (Ast0.get_mcode_mcodekind op) ->
+                         k e1
+                 | Ast0.Edots(_,_) -> k (Ast0.rewrap e (Ast0.unwrap res))
+                 | Ast0.Paren(lp,e1,rp) ->
+                     negate e e1
+                       (function x ->
+                         k (Ast0.rewrap res (Ast0.Paren(lp,x,rp))))
+                 | Ast0.Binary(e1,op,e2) when
+                     same_modif
+                       (Ast0.get_mcode_mcodekind unop)
+                       (Ast0.get_mcode_mcodekind op) ->
+                         let reb nop =
+                           Ast0.rewrap_mcode op (Ast.Logical(nop)) in
+                         let k1 x = k (Ast0.rewrap e x) in
+                         (match Ast0.unwrap_mcode op with
+                           Ast.Logical(Ast.Inf) ->
+                             k1 (Ast0.Binary(e1,reb Ast.SupEq,e2))
+                         | Ast.Logical(Ast.Sup) ->
+                             k1 (Ast0.Binary(e1,reb Ast.InfEq,e2))
+                         | Ast.Logical(Ast.InfEq) ->
+                             k1 (Ast0.Binary(e1,reb Ast.Sup,e2))
+                         | Ast.Logical(Ast.SupEq) ->
+                             k1 (Ast0.Binary(e1,reb Ast.Inf,e2))
+                         | Ast.Logical(Ast.Eq) ->
+                             k1 (Ast0.Binary(e1,reb Ast.NotEq,e2))
+                         | Ast.Logical(Ast.NotEq) ->
+                             k1 (Ast0.Binary(e1,reb Ast.Eq,e2))
+                         | Ast.Logical(Ast.AndLog) ->
+                             k1 (Ast0.Binary(negate_reb e e1 idcont,
+                                             reb Ast.OrLog,
+                                             negate_reb e e2 idcont))
+                         | Ast.Logical(Ast.OrLog) ->
+                             k1 (Ast0.Binary(negate_reb e e1 idcont,
+                                             reb Ast.AndLog,
+                                             negate_reb e e2 idcont))
+                         | _ ->
+                             Ast0.rewrap e
+                               (Ast0.Unary(k res,
+                                           Ast0.rewrap_mcode op Ast.Not)))
+                 | Ast0.DisjExpr(lp,exps,mids,rp) ->
                      (* use res because it is the transformed argument *)
-                   let exps = List.map (function e -> negate e e k) exps in
-                   Ast0.rewrap res (Ast0.DisjExpr(lp,exps,mids,rp))
-               | _ ->
+                     let exps =
+                       List.map (function e1 -> negate_reb e e1 k) exps in
+                     Ast0.rewrap res (Ast0.DisjExpr(lp,exps,mids,rp))
+                 | _ ->
                      (*use e, because this might be the toplevel expression*)
-                   Ast0.rewrap e
-                     (Ast0.Unary(k res,Ast0.rewrap_mcode unop Ast.Not)) in
+                     Ast0.rewrap e
+                       (Ast0.Unary(k res,Ast0.rewrap_mcode unop Ast.Not))
+               else
+                 Ast0.rewrap e
+                   (Ast0.Unary(k res,Ast0.rewrap_mcode unop Ast.Not))
+             and negate_reb e e1 k =
+               (* used when ! is propagated to multiple places, to avoid
+                  duplicating mcode cells *)
+               let start_line =
+                 Some ((Ast0.get_info e).Ast0.pos_info.Ast0.line_start) in
+               (rebuild_mcode start_line).VT0.rebuilder_rec_expression
+                 (negate e e1 k) in
              negate e exp idcont
            else e
        | _ -> e)
@@ -1711,7 +1833,25 @@ let instantiate bindings mv_bindings =
   let declfn r k e =
     let e = k e in
     match Ast0.unwrap e with
-      Ast0.Ddots(d,_) ->
+      Ast0.MetaDecl(name,pure) ->
+       (rebuild_mcode None).VT0.rebuilder_rec_declaration
+         (match lookup name bindings mv_bindings with
+           Common.Left(Ast0.DeclTag(d)) -> d
+         | Common.Left(_) -> failwith "not possible 1"
+         | Common.Right(new_mv) ->
+             Ast0.rewrap e
+               (Ast0.MetaDecl(Ast0.set_mcode_data new_mv name, pure)))
+    | Ast0.MetaField(name,pure) ->
+       (rebuild_mcode None).VT0.rebuilder_rec_declaration
+         (match lookup name bindings mv_bindings with
+           Common.Left(Ast0.DeclTag(d)) -> d
+         | Common.Left(_) -> failwith "not possible 1"
+         | Common.Right(new_mv) ->
+             Ast0.rewrap e
+               (Ast0.MetaField(Ast0.set_mcode_data new_mv name, pure)))
+    | Ast0.MetaFieldList(name,lenname,pure) ->
+       failwith "metafieldlist not supported"
+    | Ast0.Ddots(d,_) ->
        (try
          (match List.assoc (dot_term d) bindings with
            Ast0.DeclTag(exp) -> Ast0.rewrap e (Ast0.Ddots(d,Some exp))
@@ -1746,7 +1886,7 @@ let instantiate bindings mv_bindings =
   let stmtfn r k e =
     let e = k e in
     match Ast0.unwrap e with
-    Ast0.MetaStmt(name,pure) ->
+      Ast0.MetaStmt(name,pure) ->
        (rebuild_mcode None).VT0.rebuilder_rec_statement
          (match lookup name bindings mv_bindings with
            Common.Left(Ast0.StmtTag(stm)) -> stm
@@ -1801,7 +1941,8 @@ let merge_plus model_mcode e_mcode =
        Ast0.MINUS(emc) ->
          emc :=
            (match (!mc,!emc) with
-             (([],_),(x,t)) | ((x,_),([],t)) -> (x,t)
+             ((Ast.NOREPLACEMENT,_),(x,t))
+           | ((x,_),(Ast.NOREPLACEMENT,t)) -> (x,t)
            | _ -> failwith "how can we combine minuses?")
       |        _ -> failwith "not possible 6")
   | Ast0.CONTEXT(mc) ->
@@ -1814,44 +1955,62 @@ let merge_plus model_mcode e_mcode =
          let merged =
            match (mba,eba) with
              (x,Ast.NOTHING) | (Ast.NOTHING,x) -> x
-           | (Ast.BEFORE(b1),Ast.BEFORE(b2)) -> Ast.BEFORE(b1@b2)
-           | (Ast.BEFORE(b),Ast.AFTER(a)) -> Ast.BEFOREAFTER(b,a)
-           | (Ast.BEFORE(b1),Ast.BEFOREAFTER(b2,a)) ->
-               Ast.BEFOREAFTER(b1@b2,a)
-           | (Ast.AFTER(a),Ast.BEFORE(b)) -> Ast.BEFOREAFTER(b,a)
-           | (Ast.AFTER(a1),Ast.AFTER(a2)) ->Ast.AFTER(a2@a1)
-           | (Ast.AFTER(a1),Ast.BEFOREAFTER(b,a2)) -> Ast.BEFOREAFTER(b,a2@a1)
-           | (Ast.BEFOREAFTER(b1,a),Ast.BEFORE(b2)) ->
-               Ast.BEFOREAFTER(b1@b2,a)
-           | (Ast.BEFOREAFTER(b,a1),Ast.AFTER(a2)) ->
-               Ast.BEFOREAFTER(b,a2@a1)
-           | (Ast.BEFOREAFTER(b1,a1),Ast.BEFOREAFTER(b2,a2)) ->
-                Ast.BEFOREAFTER(b1@b2,a2@a1) in
+           | (Ast.BEFORE(b1,it1),Ast.BEFORE(b2,it2)) ->
+               Ast.BEFORE(b1@b2,Ast.lub_count it1 it2)
+           | (Ast.BEFORE(b,it1),Ast.AFTER(a,it2)) ->
+               Ast.BEFOREAFTER(b,a,Ast.lub_count it1 it2)
+           | (Ast.BEFORE(b1,it1),Ast.BEFOREAFTER(b2,a,it2)) ->
+               Ast.BEFOREAFTER(b1@b2,a,Ast.lub_count it1 it2)
+           | (Ast.AFTER(a,it1),Ast.BEFORE(b,it2)) ->
+               Ast.BEFOREAFTER(b,a,Ast.lub_count it1 it2)
+           | (Ast.AFTER(a1,it1),Ast.AFTER(a2,it2)) ->
+               Ast.AFTER(a2@a1,Ast.lub_count it1 it2)
+           | (Ast.AFTER(a1,it1),Ast.BEFOREAFTER(b,a2,it2)) ->
+               Ast.BEFOREAFTER(b,a2@a1,Ast.lub_count it1 it2)
+           | (Ast.BEFOREAFTER(b1,a,it1),Ast.BEFORE(b2,it2)) ->
+               Ast.BEFOREAFTER(b1@b2,a,Ast.lub_count it1 it2)
+           | (Ast.BEFOREAFTER(b,a1,it1),Ast.AFTER(a2,it2)) ->
+               Ast.BEFOREAFTER(b,a2@a1,Ast.lub_count it1 it2)
+           | (Ast.BEFOREAFTER(b1,a1,it1),Ast.BEFOREAFTER(b2,a2,it2)) ->
+                Ast.BEFOREAFTER(b1@b2,a2@a1,Ast.lub_count it1 it2) in
          emc := (merged,tb,ta)
       |        Ast0.MINUS(emc) ->
          let (anything_bef_aft,_,_) = !mc in
          let (anythings,t) = !emc in
-         emc :=
-           (match anything_bef_aft with
-             Ast.BEFORE(b) -> (b@anythings,t)
-           | Ast.AFTER(a) -> (anythings@a,t)
-           | Ast.BEFOREAFTER(b,a) -> (b@anythings@a,t)
-           | Ast.NOTHING -> (anythings,t))
+         (match (anything_bef_aft,anythings) with
+           (Ast.BEFORE(b1,it1),Ast.NOREPLACEMENT) ->
+             emc := (Ast.REPLACEMENT(b1,it1),t)
+         | (Ast.AFTER(a1,it1),Ast.NOREPLACEMENT) ->
+             emc := (Ast.REPLACEMENT(a1,it1),t)
+         | (Ast.BEFOREAFTER(b1,a1,it1),Ast.NOREPLACEMENT) ->
+             emc := (Ast.REPLACEMENT(b1@a1,it1),t)
+         | (Ast.NOTHING,Ast.NOREPLACEMENT) ->
+             emc := (Ast.NOREPLACEMENT,t)
+         | (Ast.BEFORE(b1,it1),Ast.REPLACEMENT(a2,it2)) ->
+             emc := (Ast.REPLACEMENT(b1@a2,Ast.lub_count it1 it2),t)
+         | (Ast.AFTER(a1,it1),Ast.REPLACEMENT(a2,it2)) ->
+             emc := (Ast.REPLACEMENT(a2@a1,Ast.lub_count it1 it2),t)
+         | (Ast.BEFOREAFTER(b1,a1,it1),Ast.REPLACEMENT(a2,it2)) ->
+             emc := (Ast.REPLACEMENT(b1@a2@a1,Ast.lub_count it1 it2),t)
+         | (Ast.NOTHING,Ast.REPLACEMENT(a2,it2)) -> ()) (* no change *)
+      | Ast0.MIXED(_) -> failwith "how did this become mixed?"
       |        _ -> failwith "not possible 7")
   | Ast0.MIXED(_) -> failwith "not possible 8"
-  | Ast0.PLUS -> failwith "not possible 9"
+  | Ast0.PLUS -> failwith "not possible 9"
 
 let copy_plus printer minusify model e =
   if !Flag.sgrep_mode2
   then e (* no plus code, can cause a "not possible" error, so just avoid it *)
   else
-    let e =
-      match Ast0.get_mcodekind model with
-       Ast0.MINUS(mc) -> minusify e
-      | Ast0.CONTEXT(mc) -> e
-      | _ -> failwith "not possible: copy_plus\n" in
-    merge_plus (Ast0.get_mcodekind model) (Ast0.get_mcodekind e);
-    e
+    begin
+      let e =
+       match Ast0.get_mcodekind model with
+          Ast0.MINUS(mc) -> minusify e
+       | Ast0.CONTEXT(mc) -> e
+       | _ -> failwith "not possible: copy_plus\n" in
+      merge_plus (Ast0.get_mcodekind model) (Ast0.get_mcodekind e);
+      e
+    end
 
 let copy_minus printer minusify model e =
   match Ast0.get_mcodekind model with
@@ -1861,7 +2020,7 @@ let copy_minus printer minusify model e =
       if !Flag.sgrep_mode2
       then e
       else failwith "not possible 8"
-  | Ast0.PLUS -> failwith "not possible 9"
+  | Ast0.PLUS -> failwith "not possible 9"
 
 let whencode_allowed prev_ecount prev_icount prev_dcount
     ecount icount dcount rest =
@@ -1918,7 +2077,9 @@ let new_mv (_,s) =
   "_"^s^"_"^(string_of_int ct)
 
 let get_name = function
-    Ast.MetaIdDecl(ar,nm) ->
+    Ast.MetaMetaDecl(ar,nm) ->
+      (nm,function nm -> Ast.MetaMetaDecl(ar,nm))
+  | Ast.MetaIdDecl(ar,nm) ->
       (nm,function nm -> Ast.MetaIdDecl(ar,nm))
   | Ast.MetaFreshIdDecl(nm,seed) ->
       (nm,function nm -> Ast.MetaFreshIdDecl(nm,seed))
@@ -1926,6 +2087,8 @@ let get_name = function
       (nm,function nm -> Ast.MetaTypeDecl(ar,nm))
   | Ast.MetaInitDecl(ar,nm) ->
       (nm,function nm -> Ast.MetaInitDecl(ar,nm))
+  | Ast.MetaInitListDecl(ar,nm,nm1) ->
+      (nm,function nm -> Ast.MetaInitListDecl(ar,nm,nm1))
   | Ast.MetaListlenDecl(nm) ->
       failwith "should not be rebuilt"
   | Ast.MetaParamDecl(ar,nm) ->
@@ -1944,6 +2107,12 @@ let get_name = function
       (nm,function nm -> Ast.MetaLocalIdExpDecl(ar,nm,ty))
   | Ast.MetaExpListDecl(ar,nm,nm1) ->
       (nm,function nm -> Ast.MetaExpListDecl(ar,nm,nm1))
+  | Ast.MetaDeclDecl(ar,nm) ->
+      (nm,function nm -> Ast.MetaDeclDecl(ar,nm))
+  | Ast.MetaFieldListDecl(ar,nm,nm1) ->
+      (nm,function nm -> Ast.MetaFieldListDecl(ar,nm,nm1))
+  | Ast.MetaFieldDecl(ar,nm) ->
+      (nm,function nm -> Ast.MetaFieldDecl(ar,nm))
   | Ast.MetaStmDecl(ar,nm) ->
       (nm,function nm -> Ast.MetaStmDecl(ar,nm))
   | Ast.MetaStmListDecl(ar,nm) ->
@@ -1979,8 +2148,8 @@ let make_new_metavars metavars bindings =
 let do_nothing x = x
 
 let mkdisj matcher metavars alts e instantiater mkiso disj_maker minusify
-    rebuild_mcodes name printer extra_plus update_others =
-  let call_instantiate bindings mv_bindings alts =
+    rebuild_mcodes name printer extra_plus update_others has_context =
+  let call_instantiate bindings mv_bindings alts pattern has_context =
     List.concat
       (List.map
         (function (a,_,_,_) ->
@@ -1988,11 +2157,17 @@ let mkdisj matcher metavars alts e instantiater mkiso disj_maker minusify
           (* no need to create duplicates when the bindings have no effect *)
             (List.map
                (function bindings ->
-                 Ast0.set_iso
-                   (copy_plus printer minusify e
-                      (extra_plus e
-                         (instantiater bindings mv_bindings
-                            (rebuild_mcodes a))))
+                 let instantiated =
+                   instantiater bindings mv_bindings (rebuild_mcodes a) in
+                 let plus_added =
+                   if has_context (* ie if pat is not just a metavara *)
+                   then
+                     copy_plus printer minusify e (extra_plus e instantiated)
+                   else instantiated in
+                 if pattern = a
+                 then plus_added
+                 else (* iso tracking *)
+                 Ast0.set_iso plus_added
                    ((name,mkiso a)::(Ast0.get_iso e))) (* keep count, not U *)
                bindings))
         alts) in
@@ -2014,7 +2189,7 @@ let mkdisj matcher metavars alts e instantiater mkiso disj_maker minusify
              | _ -> ());
            inner_loop all_alts (prev_ecount + ecount) (prev_icount + icount)
              (prev_dcount + dcount) rest
-       | OK (bindings : (((string * string) * 'a) list list)) ->
+       | OK (bindings : ((Ast.meta_name * 'a) list list)) ->
            let all_alts =
              (* apply update_others to all patterns other than the matched
                 one.  This is used to desigate the others as test
@@ -2035,7 +2210,8 @@ let mkdisj matcher metavars alts e instantiater mkiso disj_maker minusify
                  make_new_metavars metavars (nub(List.concat bindings)) in
                Common.Right
                  (new_metavars,
-                  call_instantiate bindings mv_bindings all_alts))) in
+                  call_instantiate bindings mv_bindings all_alts pattern
+                    (has_context pattern)))) in
   let rec outer_loop prev_ecount prev_icount prev_dcount = function
       [] | [[_]] (*only one alternative*)  -> (0,[],e) (* nothing matched *)
     | (alts::rest) as all_alts ->
@@ -2139,6 +2315,8 @@ let transform_type (metavars,alts,name) e =
        make_disj_type make_minus.VT0.rebuilder_rec_typeC
        (rebuild_mcode start_line).VT0.rebuilder_rec_typeC
        name Unparse_ast0.typeC extra_copy_other_plus do_nothing
+       (function x ->
+         match Ast0.unwrap x with Ast0.MetaType _ -> false | _ -> true)
   | _ -> (0,[],e)
 
 
@@ -2164,9 +2342,21 @@ let transform_expr (metavars,alts,name) e =
       (make_disj_expr e)
       make_minus.VT0.rebuilder_rec_expression
       (rebuild_mcode start_line).VT0.rebuilder_rec_expression
-      name Unparse_ast0.expression extra_copy_other_plus update_others in
+      name Unparse_ast0.expression extra_copy_other_plus update_others
+      (function x ->
+         match Ast0.unwrap x with
+           Ast0.MetaExpr _ | Ast0.MetaExprList _ | Ast0.MetaErr _ -> false
+         | _ -> true)
+  in
   match alts with
-    (Ast0.ExprTag(_)::_)::_ -> process do_nothing
+    (Ast0.ExprTag(_)::r)::rs ->
+      (* hack to accomodate ToTestExpression case, where the first pattern is
+        a normal expression, but the others are test expressions *)
+      let others = r @ (List.concat rs) in
+      let is_test = function Ast0.TestExprTag(_) -> true | _ -> false in
+      if List.for_all is_test others then process Ast0.set_test_exp
+      else if List.exists is_test others then failwith "inconsistent iso"
+      else process do_nothing
   | (Ast0.ArgExprTag(_)::_)::_ when Ast0.get_arg_exp e -> process do_nothing
   | (Ast0.TestExprTag(_)::_)::_ when Ast0.get_test_pos e ->
       process Ast0.set_test_exp
@@ -2196,6 +2386,7 @@ let transform_decl (metavars,alts,name) e =
        make_minus.VT0.rebuilder_rec_declaration
        (rebuild_mcode start_line).VT0.rebuilder_rec_declaration
        name Unparse_ast0.declaration extra_copy_other_plus do_nothing
+       (function _ -> true (* no metavars *))
   | _ -> (0,[],e)
 
 let transform_stmt (metavars,alts,name) e =
@@ -2221,12 +2412,16 @@ let transform_stmt (metavars,alts,name) e =
        make_disj_stmt make_minus.VT0.rebuilder_rec_statement
        (rebuild_mcode start_line).VT0.rebuilder_rec_statement
        name (Unparse_ast0.statement "") extra_copy_stmt_plus do_nothing
+       (function x ->
+         match Ast0.unwrap x with
+           Ast0.MetaStmt _ | Ast0.MetaStmtList _ -> false
+         | _ -> true)
   | _ -> (0,[],e)
 
 (* sort of a hack, because there is no disj at top level *)
 let transform_top (metavars,alts,name) e =
   match Ast0.unwrap e with
-    Ast0.DECL(declstm) ->
+    Ast0.NONDECL(declstm) ->
       (try
        let strip alts =
          List.map
@@ -2239,7 +2434,7 @@ let transform_top (metavars,alts,name) e =
                 | _ -> raise (Failure "")))
            alts in
        let (count,mv,s) = transform_stmt (metavars,strip alts,name) declstm in
-       (count,mv,Ast0.rewrap e (Ast0.DECL(s)))
+       (count,mv,Ast0.rewrap e (Ast0.NONDECL(s)))
       with Failure _ -> (0,[],e))
   | Ast0.CODE(stmts) ->
       let (count,mv,res) =
@@ -2268,6 +2463,7 @@ let transform_top (metavars,alts,name) e =
                make_minus.VT0.rebuilder_rec_statement_dots x)
              (rebuild_mcode start_line).VT0.rebuilder_rec_statement_dots
              name Unparse_ast0.statement_dots extra_copy_other_plus do_nothing
+             (function _ -> true)
        | _ -> (0,[],stmts) in
       (count,mv,Ast0.rewrap e (Ast0.CODE res))
   | _ -> (0,[],e)
@@ -2418,5 +2614,5 @@ let apply_isos isos rule rule_name =
                   (new_extra_meta@extra_meta,t))
                 ([],t) isos)
             rule) in
-      (List.concat extra_meta, Compute_lines.compute_lines rule)
+      (List.concat extra_meta, (Compute_lines.compute_lines true) rule)
     end