Release coccinelle-0.1.6
[bpt/coccinelle.git] / parsing_cocci / iso_pattern.ml
index 6bbf1a7..f4036ee 100644 (file)
@@ -1,5 +1,5 @@
 (*
-* Copyright 2005-2008, Ecole des Mines de Nantes, University of Copenhagen
+* 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.
 * 
@@ -51,7 +51,6 @@ let strip_info =
       Ast0.true_if_test = x.Ast0.true_if_test} in
   V0.rebuilder
     mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
-    mcode
     donothing donothing donothing donothing donothing donothing
     donothing donothing donothing donothing donothing donothing donothing
     donothing donothing
@@ -100,12 +99,17 @@ let anything_equal = function
   | (Ast0.TopTag(d1),Ast0.TopTag(d2)) ->
       (strip_info.V0.rebuilder_top_level d1) =
       (strip_info.V0.rebuilder_top_level d2)
+  | (Ast0.IsoWhenTTag(_),_) | (_,Ast0.IsoWhenTTag(_)) ->
+      failwith "only for isos within iso phase"
+  | (Ast0.IsoWhenFTag(_),_) | (_,Ast0.IsoWhenFTag(_)) ->
+      failwith "only for isos within iso phase"
   | (Ast0.IsoWhenTag(_),_) | (_,Ast0.IsoWhenTag(_)) ->
       failwith "only for isos within iso phase"
   | _ -> false
 
 let term (var1,_,_,_,_) = var1
-let dot_term (var1,_,info,_,_) = ("", var1 ^ (string_of_int info.Ast0.offset))
+let dot_term (var1,_,info,_,_) =
+  ("", var1 ^ (string_of_int info.Ast0.pos_info.Ast0.offset))
 
 
 type reason =
@@ -115,8 +119,9 @@ type reason =
   | NonMatch
   | Braces of Ast0.statement
   | Position of string * string
+  | TypeMatch of reason list
 
-let interpret_reason name line reason printer =
+let rec interpret_reason name line reason printer =
   Printf.printf
     "warning: iso %s does not match the code below on line %d\n" name line;
   printer(); Format.print_newline();
@@ -151,6 +156,9 @@ let interpret_reason name line reason printer =
   | Position(rule,name) ->
       Printf.printf "position variable %s.%s conflicts with an isomorphism\n"
        rule name;
+  | TypeMatch reason_list ->
+      List.iter (function r -> interpret_reason name line r printer)
+       reason_list
   | _ -> failwith "not possible"
 
 type 'a either = OK of 'a | Fail of reason
@@ -338,14 +346,18 @@ let match_maker checks_needed context_required whencode_allowed =
   let pure_sp_code =
     let bind = Ast0.lub_pure in
     let option_default = Ast0.Context in
-    let pure_mcodekind = function
-       Ast0.CONTEXT(mc) ->
-         (match !mc with
-           (Ast.NOTHING,_,_) -> Ast0.PureContext
-         | _ -> Ast0.Context)
-      | Ast0.MINUS(mc) ->
-         (match !mc with ([],_) -> Ast0.Pure | _ ->  Ast0.Impure)
-      | _ -> Ast0.Impure in
+    let pure_mcodekind mc =
+      if !Flag.sgrep_mode2
+      then Ast0.PureContext
+      else
+       match mc with
+         Ast0.CONTEXT(mc) ->
+           (match !mc with
+             (Ast.NOTHING,_,_) -> Ast0.PureContext
+           | _ -> Ast0.Context)
+       | Ast0.MINUS(mc) ->
+           (match !mc with ([],_) -> Ast0.Pure | _ ->  Ast0.Impure)
+       | _ -> Ast0.Impure in
     let donothing r k e =
       bind (pure_mcodekind (Ast0.get_mcodekind e)) (k e) in
 
@@ -375,6 +387,12 @@ let match_maker checks_needed context_required whencode_allowed =
          Ast0.MetaType(name,pure) -> pure
        | _ -> Ast0.Impure) in
 
+    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.Impure) in
+
     let param r k p =
       bind (bind (pure_mcodekind (Ast0.get_mcodekind p)) (k p))
        (match Ast0.unwrap p with
@@ -387,11 +405,10 @@ let match_maker checks_needed context_required whencode_allowed =
          Ast0.MetaStmt(name,pure) | Ast0.MetaStmtList(name,pure) -> pure
        | _ -> Ast0.Impure) in
 
-    V0.combiner bind option_default 
+    V0.combiner bind option_default
       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
-      mcode
       donothing donothing donothing donothing donothing donothing
-      ident expression typeC donothing param donothing stmt donothing
+      ident expression typeC init param donothing stmt donothing
       donothing in
 
   let add_pure_list_binding name pure is_pure builder1 builder2 lst =
@@ -518,34 +535,46 @@ let match_maker checks_needed context_required whencode_allowed =
                    (match expty with
                      Some expty ->
                        let tyname = Ast0.rewrap_mcode name tyname in
-                       (function bindings ->
-                         let attempts =
-                           List.map
-                             (function expty ->
-                               (try
-                                 conjunct_bindings
-                                   (add_pure_binding tyname Ast0.Impure
-                                      (function _ -> Ast0.Impure)
-                                      (function ty -> Ast0.TypeCTag ty)
-                                      (Ast0.rewrap expr
-                                         (Ast0.reverse_type expty)))
-                                   (add_pure_binding name pure
-                                      pure_sp_code.V0.combiner_expression
-                                      (function expr -> Ast0.ExprTag expr)
-                                      expr)
-                                   bindings
-                               with Ast0.TyConv ->
-                                 Printf.printf "warning: unconvertible type";
-                                 return false bindings))
-                             expty in
-                         match
-                           List.concat
-                             (List.map (function Fail _ -> [] | OK x -> x)
-                                attempts)
-                         with
-                           [] -> Fail NonMatch
-                         | x -> OK x)
-                   |   _ ->
+                       conjunct_bindings
+                         (add_pure_binding name pure
+                            pure_sp_code.V0.combiner_expression
+                            (function expr -> Ast0.ExprTag expr)
+                            expr)
+                         (function bindings ->
+                           let attempts =
+                             List.map
+                               (function expty ->
+                                 (try
+                                   add_pure_binding tyname Ast0.Impure
+                                     (function _ -> Ast0.Impure)
+                                     (function ty -> Ast0.TypeCTag ty)
+                                     (Ast0.rewrap expr
+                                        (Ast0.reverse_type expty))
+                                     bindings
+                                 with Ast0.TyConv ->
+                                   Printf.printf
+                                     "warning: unconvertible type";
+                                   return false bindings))
+                               expty in
+                           if List.exists
+                               (function Fail _ -> false | OK x -> true)
+                               attempts
+                           then
+                               (* not sure why this is ok. can there be more
+                                than one OK? *)
+                             OK (List.concat
+                                   (List.map
+                                      (function Fail _ -> [] | OK x -> x)
+                                      attempts))
+                           else
+                             Fail
+                               (TypeMatch
+                                  (List.map
+                                     (function
+                                         Fail r -> r
+                                       | OK x -> failwith "not possible")
+                                     attempts)))
+                   | _ ->
                  (*Printf.printf
                     "warning: type metavar can only match one type";*)
                        return false)
@@ -676,7 +705,7 @@ let match_maker checks_needed context_required whencode_allowed =
          | (_,Ast0.UniqueExp(expb)) -> match_expr pattern expb
          | _ -> return false
        else return_false (ContextRequired (Ast0.ExprTag expr))
-           
+
 (* the special case for function types prevents the eg T X; -> T X = E; iso
    from applying, which doesn't seem very relevant, but it also avoids a
    mysterious bug that is obtained with eg int attach(...); *)
@@ -698,16 +727,18 @@ let match_maker checks_needed context_required whencode_allowed =
              then
                conjunct_bindings (check_mcode cva cvb) (match_typeC tya tyb)
              else return false
-         | (Ast0.BaseType(tya,signa),Ast0.BaseType(tyb,signb)) ->
-             if (mcode_equal tya tyb &&
-                 bool_match_option mcode_equal signa signb)
+         | (Ast0.BaseType(tya,stringsa),Ast0.BaseType(tyb,stringsb)) ->
+             if tya = tyb
              then
-               conjunct_bindings (check_mcode tya tyb)
-                 (match_option check_mcode signa signb)
+               match_list check_mcode
+                 (function _ -> false) (function _ -> failwith "")
+                 stringsa stringsb
              else return false
-         | (Ast0.ImplicitInt(signa),Ast0.ImplicitInt(signb)) ->
+         | (Ast0.Signed(signa,tya),Ast0.Signed(signb,tyb)) ->
              if mcode_equal signa signb
-             then check_mcode signa signb
+             then
+               conjunct_bindings (check_mcode signa signb)
+                 (match_option match_typeC tya tyb)
              else return false
          | (Ast0.Pointer(tya,star1),Ast0.Pointer(tyb,star)) ->
              conjunct_bindings (check_mcode star1 star) (match_typeC tya tyb)
@@ -730,6 +761,9 @@ 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)) ->
+             conjunct_bindings (check_mcode kinda kindb)
+               (match_ident namea nameb)
          | (Ast0.StructUnionName(kinda,Some namea),
             Ast0.StructUnionName(kindb,Some nameb)) ->
               if mcode_equal kinda kindb
@@ -755,7 +789,7 @@ let match_maker checks_needed context_required whencode_allowed =
          | (_,Ast0.UniqueType(tyb)) -> match_typeC pattern tyb
          | _ -> return false
        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
@@ -804,7 +838,7 @@ let match_maker checks_needed context_required whencode_allowed =
               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
@@ -813,59 +847,75 @@ let match_maker checks_needed context_required whencode_allowed =
          match_decl pattern declb
       | _ -> return false
     else return_false (ContextRequired (Ast0.DeclTag d))
-       
+
   and match_init pattern i =
-    if not(checks_needed) or not(context_required) or is_context i
-    then
-      match (Ast0.unwrap pattern,Ast0.unwrap i) with
-       (Ast0.InitExpr(expa),Ast0.InitExpr(expb)) ->
-         match_expr expa expb
-      | (Ast0.InitList(lb1,initlista,rb1),Ast0.InitList(lb,initlistb,rb)) ->
-         conjunct_many_bindings
-           [check_mcode lb1 lb; check_mcode rb1 rb;
-             match_dots match_init no_list do_nolist_match
-               initlista initlistb]
-      | (Ast0.InitGccDotName(d1,namea,e1,inia),
-        Ast0.InitGccDotName(d,nameb,e,inib)) ->
-          conjunct_many_bindings
-            [check_mcode d1 d; check_mcode e1 e;
-              match_ident namea nameb; match_init inia inib]
-      | (Ast0.InitGccName(namea,c1,inia),Ast0.InitGccName(nameb,c,inib)) ->
-         conjunct_many_bindings
-           [check_mcode c1 c; match_ident namea nameb;
-             match_init inia inib]
-      | (Ast0.InitGccIndex(lb1,expa,rb1,e1,inia),
-        Ast0.InitGccIndex(lb2,expb,rb2,e2,inib)) ->
-         conjunct_many_bindings
-            [check_mcode lb1 lb2; check_mcode rb1 rb2; check_mcode e1 e2;
-              match_expr expa expb; match_init inia inib]
-      | (Ast0.InitGccRange(lb1,exp1a,d1,exp2a,rb1,e1,inia),
-        Ast0.InitGccRange(lb2,exp1b,d2,exp2b,rb2,e2,inib)) ->
-         conjunct_many_bindings
-            [check_mcode lb1 lb2; check_mcode d1 d2;
-              check_mcode rb1 rb2; check_mcode e1 e2;
-              match_expr exp1a exp1b; match_expr exp2a exp2b;
-              match_init inia inib]
-      | (Ast0.IComma(c1),Ast0.IComma(c)) -> check_mcode c1 c
-      | (Ast0.Idots(d1,None),Ast0.Idots(d,None)) -> check_mcode d1 d
-      | (Ast0.Idots(id,None),Ast0.Idots(d,Some wc)) ->
-         conjunct_bindings (check_mcode id d)
+    match Ast0.unwrap pattern with
+      Ast0.MetaInit(name,pure) ->
+       add_pure_binding name pure pure_sp_code.V0.combiner_initialiser
+         (function ini -> Ast0.InitTag ini)
+         i
+    | up ->
+       if not(checks_needed) or not(context_required) or is_context i
+       then
+         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))
+           ->
+             conjunct_many_bindings
+               [check_mcode lb1 lb; check_mcode rb1 rb;
+                 match_dots match_init no_list do_nolist_match
+                   initlista initlistb]
+         | (Ast0.InitGccExt(designators1,e1,inia),
+            Ast0.InitGccExt(designators2,e2,inib)) ->
+              conjunct_many_bindings
+                [match_list match_designator
+                    (function _ -> false) (function _ -> failwith "")
+                    designators1 designators2;
+                  check_mcode e1 e2;
+                  match_init inia inib]
+         | (Ast0.InitGccName(namea,c1,inia),Ast0.InitGccName(nameb,c,inib)) ->
+             conjunct_many_bindings
+               [check_mcode c1 c; match_ident namea nameb;
+                 match_init inia inib]
+         | (Ast0.IComma(c1),Ast0.IComma(c)) -> check_mcode c1 c
+         | (Ast0.Idots(d1,None),Ast0.Idots(d,None)) -> check_mcode d1 d
+         | (Ast0.Idots(id,None),Ast0.Idots(d,Some wc)) ->
+             conjunct_bindings (check_mcode id d)
          (* hope that mcode of edots is unique somehow *)
-           (let (_,idots_whencode_allowed,_) = whencode_allowed in
-           if idots_whencode_allowed
-           then add_dot_binding id (Ast0.InitTag wc)
-           else
-             (Printf.printf "warning: not applying iso because of whencode";
-              return false))
-      | (Ast0.Idots(_,Some _),_) ->
-         failwith "whencode not allowed in a pattern2"
-      | (Ast0.OptIni(ia),Ast0.OptIni(ib))
-      | (Ast0.UniqueIni(ia),Ast0.UniqueIni(ib)) -> match_init ia ib
-      | (_,Ast0.OptIni(ib))
-      | (_,Ast0.UniqueIni(ib)) -> match_init pattern ib
-      | _ -> return false
-    else return_false (ContextRequired (Ast0.InitTag i))
-       
+               (let (_,idots_whencode_allowed,_) = whencode_allowed in
+               if idots_whencode_allowed
+               then add_dot_binding id (Ast0.InitTag wc)
+               else
+                 (Printf.printf
+                    "warning: not applying iso because of whencode";
+                  return false))
+         | (Ast0.Idots(_,Some _),_) ->
+             failwith "whencode not allowed in a pattern2"
+         | (Ast0.OptIni(ia),Ast0.OptIni(ib))
+         | (Ast0.UniqueIni(ia),Ast0.UniqueIni(ib)) -> match_init ia ib
+         | (_,Ast0.OptIni(ib))
+         | (_,Ast0.UniqueIni(ib)) -> match_init pattern ib
+         | _ -> return false
+       else return_false (ContextRequired (Ast0.InitTag i))
+
+  and match_designator pattern d =
+    match (pattern,d) with
+      (Ast0.DesignatorField(dota,ida),Ast0.DesignatorField(dotb,idb)) ->
+       conjunct_bindings (check_mcode dota dotb) (match_ident ida idb)
+    | (Ast0.DesignatorIndex(lba,expa,rba),
+       Ast0.DesignatorIndex(lbb,expb,rbb)) ->
+        conjunct_many_bindings
+          [check_mcode lba lbb; match_expr expa expb;
+            check_mcode rba rbb]
+    | (Ast0.DesignatorRange(lba,mina,dotsa,maxa,rba),
+       Ast0.DesignatorRange(lbb,minb,dotsb,maxb,rbb)) ->
+        conjunct_many_bindings
+          [check_mcode lba lbb; match_expr mina minb;
+            check_mcode dotsa dotsb; match_expr maxa maxb;
+            check_mcode rba rbb]
+    | _ -> return false
+
   and match_param pattern p =
     match Ast0.unwrap pattern with
       Ast0.MetaParam(name,pure) ->
@@ -891,7 +941,7 @@ let match_maker checks_needed context_required whencode_allowed =
          | (_,Ast0.UniqueParam(paramb)) -> match_param pattern paramb
          | _ -> return false
        else return_false (ContextRequired (Ast0.ParamTag p))
-           
+
   and match_statement pattern s =
     match Ast0.unwrap pattern with
       Ast0.MetaStmt(name,pure) ->
@@ -1020,6 +1070,7 @@ let match_maker checks_needed context_required whencode_allowed =
          | (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
+         | (Ast0.TopInit(inita),Ast0.TopInit(initb)) -> match_init inita initb
          | (Ast0.Ty(tya),Ast0.Ty(tyb)) -> match_typeC tya tyb
          | (Ast0.Dots(d,[]),Ast0.Dots(d1,wc))
          | (Ast0.Circles(d,[]),Ast0.Circles(d1,wc))
@@ -1041,6 +1092,14 @@ let match_maker checks_needed context_required whencode_allowed =
                             | Ast0.WhenAlways wc ->
                                 conjunct_bindings prev
                                   (add_multi_dot_binding d (Ast0.StmtTag wc))
+                            | Ast0.WhenNotTrue wc ->
+                                conjunct_bindings prev
+                                  (add_multi_dot_binding d
+                                     (Ast0.IsoWhenTTag wc))
+                            | Ast0.WhenNotFalse wc ->
+                                conjunct_bindings prev
+                                  (add_multi_dot_binding d
+                                     (Ast0.IsoWhenFTag wc))
                             | Ast0.WhenModifier(x) ->
                                 conjunct_bindings prev
                                   (add_multi_dot_binding d
@@ -1060,7 +1119,7 @@ let match_maker checks_needed context_required whencode_allowed =
          | (_,Ast0.UniqueStm(reb)) -> match_statement pattern reb
          |     _ -> return false
        else return_false (ContextRequired (Ast0.StmtTag s))
-           
+
   (* first should provide a subset of the information in the second *)
   and match_fninfo patterninfo cinfo =
     let patterninfo = List.sort compare patterninfo in
@@ -1087,7 +1146,7 @@ let match_maker checks_needed context_required whencode_allowed =
          | _ -> failwith "not possible")
       |        _ -> return false in
     loop (patterninfo,cinfo)
-      
+
   and match_case_line pattern c =
     if not(checks_needed) or not(context_required) or is_context c
     then
@@ -1106,36 +1165,36 @@ let match_maker checks_needed context_required whencode_allowed =
       |        (_,Ast0.OptCase(cb)) -> match_case_line pattern cb
       |        _ -> return false
     else return_false (ContextRequired (Ast0.CaseLineTag c)) in
-  
+
   let match_statement_dots x y =
     match_dots match_statement is_slist_matcher do_slist_match x y in
-  
+
   (match_expr, match_decl, match_statement, match_typeC,
    match_statement_dots)
-    
+
 let match_expr dochecks context_required whencode_allowed =
   let (fn,_,_,_,_) = match_maker dochecks context_required whencode_allowed in
   fn
-    
+
 let match_decl dochecks context_required whencode_allowed =
   let (_,fn,_,_,_) = match_maker dochecks context_required whencode_allowed in
   fn
-    
+
 let match_statement dochecks context_required whencode_allowed =
   let (_,_,fn,_,_) = match_maker dochecks context_required whencode_allowed in
   fn
-    
+
 let match_typeC dochecks context_required whencode_allowed =
   let (_,_,_,fn,_) = match_maker dochecks context_required whencode_allowed in
   fn
-    
+
 let match_statement_dots dochecks context_required whencode_allowed =
   let (_,_,_,_,fn) = match_maker dochecks context_required whencode_allowed in
   fn
-    
+
 (* --------------------------------------------------------------------- *)
 (* make an entire tree MINUS *)
-    
+
 let make_minus =
   let mcode (term,arity,info,mcodekind,pos) =
     let new_mcodekind =
@@ -1147,7 +1206,7 @@ let make_minus =
      | Ast0.MINUS(mc) -> mcodekind (* in the part copied from the src term *)
      | _ -> failwith "make_minus mcode: unexpected mcodekind" in
     (term,arity,info,new_mcodekind,pos) in
-  
+
   let update_mc mcodekind e =
     match !mcodekind with
       Ast0.CONTEXT(mc) ->
@@ -1158,11 +1217,11 @@ let make_minus =
     | Ast0.MINUS(_mc) -> () (* in the part copied from the src term *)
     | Ast0.PLUS -> failwith "make_minus donothing: unexpected plus mcodekind"
     | _ -> failwith "make_minus donothing: unexpected mcodekind" in
-  
+
   let donothing r k e =
     let mcodekind = Ast0.get_mcodekind_ref e in
     let e = k e in update_mc mcodekind e; e in
-  
+
   (* special case for whencode, because it isn't processed by contextneg,
      since it doesn't appear in the + code *)
   (* cases for dots and nests *)
@@ -1185,7 +1244,7 @@ let make_minus =
                         r.V0.rebuilder_expression_dots expr_dots,
                         mcode ender,whencode,multi))
     | _ -> donothing r k e in
-  
+
   let declaration r k e =
     let mcodekind = Ast0.get_mcodekind_ref e in
     match Ast0.unwrap e with
@@ -1193,7 +1252,7 @@ let make_minus =
        (*don't recurse because whencode hasn't been processed by context_neg*)
        update_mc mcodekind e; Ast0.rewrap e (Ast0.Ddots(mcode d,whencode))
     | _ -> donothing r k e in
-  
+
   let statement r k e =
     let mcodekind = Ast0.get_mcodekind_ref e in
     match Ast0.unwrap e with
@@ -1210,7 +1269,7 @@ let make_minus =
          (Ast0.Nest(mcode starter,r.V0.rebuilder_statement_dots stmt_dots,
                     mcode ender,whencode,multi))
     | _ -> donothing r k e in
-  
+
   let initialiser r k e =
     let mcodekind = Ast0.get_mcodekind_ref e in
     match Ast0.unwrap e with
@@ -1218,7 +1277,7 @@ let make_minus =
        (*don't recurse because whencode hasn't been processed by context_neg*)
        update_mc mcodekind e; Ast0.rewrap e (Ast0.Idots(mcode d,whencode))
     | _ -> donothing r k e in
-  
+
   let dots r k e =
     let info = Ast0.get_info e in
     let mcodekind = Ast0.get_mcodekind_ref e in
@@ -1226,10 +1285,11 @@ let make_minus =
       Ast0.DOTS([]) ->
        (* if context is - this should be - as well.  There are no tokens
           here though, so the bottom-up minusifier in context_neg leaves it
-          as mixed.  It would be better to fix context_neg, but that would
+          as mixed (or context for sgrep2).  It would be better to fix
+          context_neg, but that would
           require a special case for each term with a dots subterm. *)
        (match !mcodekind with
-         Ast0.MIXED(mc) ->
+         Ast0.MIXED(mc) | Ast0.CONTEXT(mc) ->
            (match !mc with
              (Ast.NOTHING,_,_) ->
                mcodekind := Ast0.MINUS(ref([],Ast0.default_token_info));
@@ -1240,20 +1300,19 @@ let make_minus =
        | _ ->
            failwith
              (Printf.sprintf
-                "%d: make_minus donothingxxx: unexpected mcodekind"
-                info.Ast0.line_start))
+                "%d: make_minus donothingxxx: unexpected mcodekind: %s"
+                info.Ast0.pos_info.Ast0.line_start (Dumper.dump e)))
     | _ -> donothing r k e in
-  
+
   V0.rebuilder
     mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
-    mcode
     dots dots dots dots dots dots
     donothing expression donothing initialiser donothing declaration
     statement donothing donothing
-    
+
 (* --------------------------------------------------------------------- *)
 (* rebuild mcode cells in an instantiated alt *)
-    
+
 (* mcodes will be side effected later with plus code, so we have to copy
    them on instantiating an isomorphism.  One could wonder whether it would
    be better not to use side-effects, but they are convenient for insert_plus
@@ -1269,25 +1328,35 @@ let rebuild_mcode start_line =
        (* this function is used elsewhere where we need to rebuild the
           indices, and so we allow PLUS code as well *)
         Ast0.PLUS in
-  
+
   let mcode (term,arity,info,mcodekind,pos) =
     let info =
       match start_line with
-       Some x -> {info with Ast0.line_start = x; Ast0.line_end = x}
+       Some x ->
+         let new_pos_info =
+           {info.Ast0.pos_info with
+             Ast0.line_start = x;
+             Ast0.line_end = x; } in
+         {info with Ast0.pos_info = new_pos_info}
       |        None -> info in
     (term,arity,info,copy_mcodekind mcodekind,pos) in
-  
+
   let copy_one x =
     let old_info = Ast0.get_info x in
     let info =
       match start_line with
-       Some x -> {old_info with Ast0.line_start = x; Ast0.line_end = x}
+       Some x ->
+         let new_pos_info =
+           {old_info.Ast0.pos_info with
+             Ast0.line_start = x;
+             Ast0.line_end = x; } in
+         {old_info with Ast0.pos_info = new_pos_info}
       |        None -> old_info in
     {x with Ast0.info = info; Ast0.index = ref(Ast0.get_index x);
       Ast0.mcodekind = ref (copy_mcodekind (Ast0.get_mcodekind x))} in
-  
+
   let donothing r k e = copy_one (k e) in
-  
+
   (* case for control operators (if, etc) *)
   let statement r k e =
     let s = k e in
@@ -1322,20 +1391,19 @@ let rebuild_mcode start_line =
          Ast0.AddingBetweenDots(r.V0.rebuilder_statement s)
       | Ast0.DroppingBetweenDots s ->
          Ast0.DroppingBetweenDots(r.V0.rebuilder_statement s)) in
-  
+
   V0.rebuilder
     mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
-    mcode
     donothing donothing donothing donothing donothing donothing
     donothing donothing donothing donothing donothing
     donothing statement donothing donothing
-    
+
 (* --------------------------------------------------------------------- *)
 (* The problem of whencode.  If an isomorphism contains dots in multiple
    rules, then the code that is matched cannot contain whencode, because we
    won't know which dots it goes with. Should worry about nests, but they
    aren't allowed in isomorphisms for the moment. *)
-    
+
 let count_edots =
   let mcode x = 0 in
   let option_default = 0 in
@@ -1345,14 +1413,13 @@ let count_edots =
     match Ast0.unwrap e with
       Ast0.Edots(_,_) | Ast0.Ecircles(_,_) | Ast0.Estars(_,_) -> 1
     | _ -> 0 in
-  
+
   V0.combiner bind option_default
     mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
-    mcode
     donothing donothing donothing donothing donothing donothing
     donothing exprfn donothing donothing donothing donothing donothing
     donothing donothing
-    
+
 let count_idots =
   let mcode x = 0 in
   let option_default = 0 in
@@ -1360,14 +1427,13 @@ let count_idots =
   let donothing r k e = k e in
   let initfn r k e =
     match Ast0.unwrap e with Ast0.Idots(_,_) -> 1 | _ -> 0 in
-  
+
   V0.combiner bind option_default
     mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
-    mcode
     donothing donothing donothing donothing donothing donothing
     donothing donothing donothing initfn donothing donothing donothing
     donothing donothing
-    
+
 let count_dots =
   let mcode x = 0 in
   let option_default = 0 in
@@ -1377,16 +1443,15 @@ let count_dots =
     match Ast0.unwrap e with
       Ast0.Dots(_,_) | Ast0.Circles(_,_) | Ast0.Stars(_,_) -> 1
     | _ -> 0 in
-  
+
   V0.combiner bind option_default
     mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
-    mcode
     donothing donothing donothing donothing donothing donothing
     donothing donothing donothing donothing donothing donothing stmtfn
     donothing donothing
-    
+
 (* --------------------------------------------------------------------- *)
-    
+
 let lookup name bindings mv_bindings =
   try Common.Left (List.assoc (term name) bindings)
   with
@@ -1561,46 +1626,52 @@ let instantiate bindings mv_bindings =
              | _ -> failwith "plus not possible" in
            if was_meta && nomodif exp && nomodif e
            then
-             let rec negate e (*for rewrapping*) res (*code to process*) =
+             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 ->
-                   Ast0.rewrap e (Ast0.unwrap e1)
-               | Ast0.Edots(_,_) -> Ast0.rewrap e (Ast0.unwrap res)
+                   k (Ast0.rewrap e (Ast0.unwrap e1))
+               | Ast0.Edots(_,_) -> k (Ast0.rewrap e (Ast0.unwrap res))
                | Ast0.Paren(lp,e,rp) ->
-                   Ast0.rewrap res (Ast0.Paren(lp,negate e 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 invop =
-                     match Ast0.unwrap_mcode op with
-                       Ast.Logical(Ast.Inf) ->
-                         Ast0.Binary(e1,reb Ast.SupEq,e2)
-                     | Ast.Logical(Ast.Sup) ->
-                         Ast0.Binary(e1,reb Ast.InfEq,e2)
-                     | Ast.Logical(Ast.InfEq) ->
-                         Ast0.Binary(e1,reb Ast.Sup,e2)
-                     | Ast.Logical(Ast.SupEq) ->
-                         Ast0.Binary(e1,reb Ast.Inf,e2)
-                     | Ast.Logical(Ast.Eq) ->
-                         Ast0.Binary(e1,reb Ast.NotEq,e2)
-                     | Ast.Logical(Ast.NotEq) ->
-                         Ast0.Binary(e1,reb Ast.Eq,e2)
-                     | Ast.Logical(Ast.AndLog) ->
-                         Ast0.Binary(negate e1 e1,reb Ast.OrLog,
-                                     negate e2 e2)
-                     | Ast.Logical(Ast.OrLog) ->
-                         Ast0.Binary(negate e1 e1,reb Ast.AndLog,
-                                     negate e2 e2)
-                     | _ -> Ast0.Unary(res,Ast0.rewrap_mcode op Ast.Not) in
-                   Ast0.rewrap e invop
+                   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) ->
                      (* use res because it is the transformed argument *)
-                   let exps = List.map (function e -> negate e e) exps in
+                   let exps = List.map (function e -> negate e e 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(res,Ast0.rewrap_mcode unop Ast.Not)) in
-             negate e exp
+                     (Ast0.Unary(res,Ast0.rewrap_mcode unop Ast.Not)) in
+             negate e exp idcont
            else e
        | _ -> e)
     | Ast0.Edots(d,_) ->
@@ -1637,6 +1708,19 @@ let instantiate bindings mv_bindings =
                (Ast0.MetaType(Ast0.set_mcode_data new_mv name,pure)))
     | _ -> e in
 
+  let initfn r k e =
+    let e = k e in
+    match Ast0.unwrap e with
+      Ast0.MetaInit(name,pure) ->
+       (rebuild_mcode None).V0.rebuilder_initialiser
+         (match lookup name bindings mv_bindings with
+           Common.Left(Ast0.InitTag(ty)) -> ty
+         | Common.Left(_) -> failwith "not possible 1"
+         | Common.Right(new_mv) ->
+             Ast0.rewrap e
+               (Ast0.MetaInit(Ast0.set_mcode_data new_mv name,pure)))
+    | _ -> e in
+
   let declfn r k e =
     let e = k e in
     match Ast0.unwrap e with
@@ -1663,6 +1747,15 @@ let instantiate bindings mv_bindings =
        failwith "metaparamlist not supported"
     | _ -> e in
 
+  let whenfn (_,v) =
+    match v with
+      Ast0.DotsStmtTag(stms) -> Ast0.WhenNot stms
+    | Ast0.StmtTag(stm) -> Ast0.WhenAlways stm
+    | Ast0.IsoWhenTTag(stm) -> Ast0.WhenNotTrue stm
+    | Ast0.IsoWhenFTag(stm) -> Ast0.WhenNotFalse stm
+    | Ast0.IsoWhenTag(x) -> Ast0.WhenModifier(x)
+    | _ -> failwith "unexpected binding" in
+
   let stmtfn r k e =
     let e = k e in
     match Ast0.unwrap e with
@@ -1679,45 +1772,26 @@ let instantiate bindings mv_bindings =
        Ast0.rewrap e
          (Ast0.Dots
             (d,
-             List.map
-               (function (_,v) ->
-                 match v with
-                   Ast0.DotsStmtTag(stms) -> Ast0.WhenNot stms
-                 | Ast0.StmtTag(stm) -> Ast0.WhenAlways stm
-                 | Ast0.IsoWhenTag(x) -> Ast0.WhenModifier(x)
-                 | _ -> failwith "unexpected binding")
+             List.map whenfn
                (List.filter (function (x,v) -> x = (dot_term d)) bindings)))
     | Ast0.Circles(d,_) ->
        Ast0.rewrap e
          (Ast0.Circles
             (d,
-             List.map
-               (function (_,v) ->
-                 match v with
-                   Ast0.DotsStmtTag(stms) -> Ast0.WhenNot stms
-                 | Ast0.StmtTag(stm) -> Ast0.WhenAlways stm
-                 | Ast0.IsoWhenTag(x) -> Ast0.WhenModifier(x)
-                 | _ -> failwith "unexpected binding")
+             List.map whenfn
                (List.filter (function (x,v) -> x = (dot_term d)) bindings)))
     | Ast0.Stars(d,_) ->
        Ast0.rewrap e
          (Ast0.Stars
             (d,
-             List.map
-               (function (_,v) ->
-                 match v with
-                   Ast0.DotsStmtTag(stms) -> Ast0.WhenNot stms
-                 | Ast0.StmtTag(stm) -> Ast0.WhenAlways stm
-                 | Ast0.IsoWhenTag(x) -> Ast0.WhenModifier(x)
-                 | _ -> failwith "unexpected binding")
+             List.map whenfn
                (List.filter (function (x,v) -> x = (dot_term d)) bindings)))
     | _ -> e in
 
   V0.rebuilder
     mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
-    mcode
     (dots elist) donothing (dots plist) (dots slist) donothing donothing
-    identfn exprfn tyfn donothing paramfn declfn stmtfn donothing donothing
+    identfn exprfn tyfn initfn paramfn declfn stmtfn donothing donothing
 
 (* --------------------------------------------------------------------- *)
 
@@ -1863,6 +1937,8 @@ let get_name = function
       (nm,function nm -> Ast.MetaFreshIdDecl(ar,nm))
   | Ast.MetaTypeDecl(ar,nm) ->
       (nm,function nm -> Ast.MetaTypeDecl(ar,nm))
+  | Ast.MetaInitDecl(ar,nm) ->
+      (nm,function nm -> Ast.MetaInitDecl(ar,nm))
   | Ast.MetaListlenDecl(nm) ->
       failwith "should not be rebuilt"
   | Ast.MetaParamDecl(ar,nm) ->
@@ -1987,10 +2063,12 @@ let mkdisj matcher metavars alts e instantiater mkiso disj_maker minusify
 (* no one should ever look at the information stored in these mcodes *)
 let disj_starter lst =
   let old_info = Ast0.get_info(List.hd lst) in
+  let new_pos_info =
+    { old_info.Ast0.pos_info with
+      Ast0.line_end = old_info.Ast0.pos_info.Ast0.line_start;
+      Ast0.logical_end = old_info.Ast0.pos_info.Ast0.logical_start; } in
   let info =
-    { old_info with
-      Ast0.line_end = old_info.Ast0.line_start;
-      Ast0.logical_end = old_info.Ast0.logical_start;
+    { Ast0.pos_info = new_pos_info;
       Ast0.attachable_start = false; Ast0.attachable_end = false;
       Ast0.mcode_start = []; Ast0.mcode_end = [];
       Ast0.strings_before = []; Ast0.strings_after = [] } in
@@ -1998,10 +2076,12 @@ let disj_starter lst =
 
 let disj_ender lst =
   let old_info = Ast0.get_info(List.hd lst) in
+  let new_pos_info =
+    { old_info.Ast0.pos_info with
+      Ast0.line_start = old_info.Ast0.pos_info.Ast0.line_end;
+      Ast0.logical_start = old_info.Ast0.pos_info.Ast0.logical_end; } in
   let info =
-    { old_info with
-      Ast0.line_start = old_info.Ast0.line_end;
-      Ast0.logical_start = old_info.Ast0.logical_end;
+    { Ast0.pos_info = new_pos_info;
       Ast0.attachable_start = false; Ast0.attachable_end = false;
       Ast0.mcode_start = []; Ast0.mcode_end = [];
       Ast0.strings_before = []; Ast0.strings_after = [] } in
@@ -2052,7 +2132,8 @@ let transform_type (metavars,alts,name) e =
   match alts with
     (Ast0.TypeCTag(_)::_)::_ ->
       (* start line is given to any leaves in the iso code *)
-      let start_line = Some ((Ast0.get_info e).Ast0.line_start) in
+      let start_line =
+       Some ((Ast0.get_info e).Ast0.pos_info.Ast0.line_start) in
       let alts =
        List.map
          (List.map
@@ -2076,7 +2157,8 @@ let transform_type (metavars,alts,name) e =
 let transform_expr (metavars,alts,name) e =
   let process update_others =
       (* start line is given to any leaves in the iso code *)
-    let start_line = Some ((Ast0.get_info e).Ast0.line_start) in
+    let start_line =
+      Some ((Ast0.get_info e).Ast0.pos_info.Ast0.line_start) in
     let alts =
       List.map
        (List.map
@@ -2091,7 +2173,8 @@ let transform_expr (metavars,alts,name) e =
       (function b -> function mv_b ->
        (instantiate b mv_b).V0.rebuilder_expression)
       (function e -> Ast0.ExprTag e)
-      (make_disj_expr e) make_minus.V0.rebuilder_expression
+      (make_disj_expr e)
+      make_minus.V0.rebuilder_expression
       (rebuild_mcode start_line).V0.rebuilder_expression
       name Unparse_ast0.expression extra_copy_other_plus update_others in
   match alts with
@@ -2105,7 +2188,8 @@ let transform_decl (metavars,alts,name) e =
   match alts with
     (Ast0.DeclTag(_)::_)::_ ->
       (* start line is given to any leaves in the iso code *)
-      let start_line = Some (Ast0.get_info e).Ast0.line_start in
+      let start_line =
+       Some (Ast0.get_info e).Ast0.pos_info.Ast0.line_start in
       let alts =
        List.map
          (List.map
@@ -2130,7 +2214,8 @@ let transform_stmt (metavars,alts,name) e =
   match alts with
     (Ast0.StmtTag(_)::_)::_ ->
       (* start line is given to any leaves in the iso code *)
-      let start_line = Some (Ast0.get_info e).Ast0.line_start in
+      let start_line =
+       Some (Ast0.get_info e).Ast0.pos_info.Ast0.line_start in
       let alts =
        List.map
          (List.map
@@ -2173,7 +2258,8 @@ let transform_top (metavars,alts,name) e =
        match alts with
          (Ast0.DotsStmtTag(_)::_)::_ ->
               (* start line is given to any leaves in the iso code *)
-           let start_line = Some ((Ast0.get_info e).Ast0.line_start) in
+           let start_line =
+             Some ((Ast0.get_info e).Ast0.pos_info.Ast0.line_start) in
            let alts =
              List.map
                (List.map
@@ -2190,7 +2276,8 @@ let transform_top (metavars,alts,name) e =
              (function s -> Ast0.DotsStmtTag s)
              (function x ->
                Ast0.rewrap e (Ast0.DOTS([make_disj_stmt_list x])))
-             make_minus.V0.rebuilder_statement_dots
+             (function x ->
+               make_minus.V0.rebuilder_statement_dots x)
              (rebuild_mcode start_line).V0.rebuilder_statement_dots
              name Unparse_ast0.statement_dots extra_copy_other_plus do_nothing
        | _ -> ([],stmts) in
@@ -2218,21 +2305,27 @@ let transform (alts : isomorphism) t =
     let (extra_meta,stm) = transform_stmt alts (k e) in
     extra_meta_decls := extra_meta @ !extra_meta_decls;
     stm in
-  
+
   let typefn r k e =
-    let (extra_meta,ty) = transform_type alts (k e) in
-    extra_meta_decls := extra_meta @ !extra_meta_decls;
-    ty in
-  
+   let continue =
+     match Ast0.unwrap e with
+       Ast0.Signed(signb,tyb) ->
+       (* Hack!  How else to prevent iso from applying under an
+         unsigned??? *)
+        e
+     | _ -> k e in
+   let (extra_meta,ty) = transform_type alts continue in
+   extra_meta_decls := extra_meta @ !extra_meta_decls;
+   ty in
+
   let topfn r k e =
     let (extra_meta,ty) = transform_top alts (k e) in
     extra_meta_decls := extra_meta @ !extra_meta_decls;
     ty in
-  
+
   let res =
     V0.rebuilder
       mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
-      mcode
       donothing donothing donothing donothing donothing donothing
       donothing exprfn typefn donothing donothing declfn stmtfn
       donothing topfn in
@@ -2247,7 +2340,6 @@ let rewrap =
   let donothing r k e = Ast0.context_wrap(Ast0.unwrap(k e)) in
   V0.rebuilder
     mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode mcode
-    mcode
     donothing donothing donothing donothing donothing donothing
     donothing donothing donothing donothing donothing donothing donothing
     donothing donothing
@@ -2276,7 +2368,8 @@ let rewrap_anything = function
   | Ast0.StmtTag(d) -> Ast0.StmtTag(rewrap.V0.rebuilder_statement d)
   | Ast0.CaseLineTag(d) -> Ast0.CaseLineTag(rewrap.V0.rebuilder_case_line d)
   | Ast0.TopTag(d) -> Ast0.TopTag(rewrap.V0.rebuilder_top_level d)
-  | Ast0.IsoWhenTag(_) -> failwith "only for isos within iso phase"
+  | Ast0.IsoWhenTag(_) | Ast0.IsoWhenTTag(_) | Ast0.IsoWhenFTag(_) ->
+      failwith "only for isos within iso phase"
   | Ast0.MetaPosTag(p) -> Ast0.MetaPosTag(p)
 
 (* --------------------------------------------------------------------- *)