Release coccinelle-0.1.8
[bpt/coccinelle.git] / parsing_cocci / parser_cocci_menhir.mly
index 1e71638..23c1c1e 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.
 * 
@@ -38,16 +38,16 @@ module P = Parse_aux
 %token EOF
 
 %token TIdentifier TExpression TStatement TFunction TLocal TType TParameter
-%token TIdExpression
+%token TIdExpression TInitialiser
 %token Tlist TFresh TConstant TError TWords TWhy0 TPlus0 TBang0
-%token TPure TContext
+%token TPure TContext TGenerated
 %token TTypedef TDeclarer TIterator TName TPosition TPosAny
-%token TUsing TDisable TExtends TDepends TOn TEver TNever TExists TForall TScript
-%token TReverse TNothing
+%token TUsing TDisable TExtends TDepends TOn TEver TNever TExists TForall
+%token TScript TInitialize TFinalize TReverse TNothing
 %token<string> TRuleName
 
 %token<Data.clt> Tchar Tshort Tint Tdouble Tfloat Tlong
-%token<Data.clt> Tvoid Tstruct Tunion
+%token<Data.clt> Tvoid Tstruct Tunion Tenum
 %token<Data.clt> Tunsigned Tsigned
 
 %token<Data.clt> Tstatic Tauto Tregister Textern Tinline Ttypedef
@@ -56,12 +56,13 @@ module P = Parse_aux
 
 %token <Data.clt> TIf TElse TWhile TFor TDo TSwitch TCase TDefault TReturn
 %token <Data.clt> TBreak TContinue TGoto TSizeof TFunDecl
-%token <string * Data.clt> TIdent TTypeId TDeclarerId TIteratorId
+%token <string * Data.clt> TIdent TTypeId TDeclarerId TIteratorId TPragma
 
 %token <Parse_aux.idinfo>     TMetaId TMetaFunc TMetaLocalFunc
 %token <Parse_aux.idinfo>     TMetaIterator TMetaDeclarer
-%token <Parse_aux.expinfo>    TMetaErr 
+%token <Parse_aux.expinfo>    TMetaErr
 %token <Parse_aux.info>       TMetaParam TMetaStm TMetaStmList TMetaType
+%token <Parse_aux.info>       TMetaInit
 %token <Parse_aux.list_info>  TMetaParamList TMetaExpList
 %token <Parse_aux.typed_info> TMetaExp TMetaIdExp TMetaLocalIdExp TMetaConst
 %token <Parse_aux.pos_info>   TMetaPos
@@ -75,10 +76,10 @@ module P = Parse_aux
 %token <Data.clt> TWhy TDotDot TBang TOPar TOPar0
 %token <Data.clt> TMid0 TCPar TCPar0
 
-%token <string>  TPragma TPathIsoFile
+%token <string>  TPathIsoFile
 %token <string * Data.clt> TIncludeL TIncludeNL
 %token <Data.clt * token> TDefine
-%token <Data.clt * token * int> TDefineParam
+%token <Data.clt * token * int * int> TDefineParam
 %token <string * Data.clt> TMinusFile TPlusFile
 
 %token <Data.clt> TInc TDec
@@ -89,7 +90,7 @@ module P = Parse_aux
 %token <Data.clt> TAndLog
 %token <Data.clt> TOr
 %token <Data.clt> TXor
-%token <Data.clt> TAnd 
+%token <Data.clt> TAnd
 %token <Data.clt> TEqEq TNotEq
 %token <Ast_cocci.logicalOp * Data.clt> TLogOp /* TInf TSup TInfEq TSupEq */
 %token <Ast_cocci.arithOp * Data.clt>   TShOp  /* TShl TShr */
@@ -119,7 +120,7 @@ module P = Parse_aux
 %left TAndLog
 %left TOr
 %left TXor
-%left TAnd 
+%left TAnd
 %left TEqEq TNotEq
 %left TLogOp /* TInf TSup TInfEq TSupEq */
 %left TShOp /* TShl TShr */
@@ -199,8 +200,17 @@ rule_name:
   nm=ioption(pure_ident) extends d=depends i=loption(choose_iso)
     a=loption(disable) e=exists ee=is_expression TArob
       { P.make_cocci_rule_name_result nm d i a e ee }
+  | TGenerated extends d=depends i=loption(choose_iso)
+    a=loption(disable) e=exists ee=is_expression TArob
+      /* these rules have no name as a cheap way to ensure that no normal
+      rule inherits their metavariables or depends on them */
+      { P.make_generated_rule_name_result None d i a e ee }
   | TScript TDotDot lang=pure_ident d=depends TArob
       { P.make_script_rule_name_result lang d }
+  | TInitialize TDotDot lang=pure_ident TArob
+      { P.make_initial_script_rule_name_result lang }
+  | TFinalize TDotDot lang=pure_ident TArob
+      { P.make_final_script_rule_name_result lang }
 
 extends:
   /* empty */                                     { () }
@@ -251,6 +261,9 @@ metadec:
   ar=arity ispure=pure
   kindfn=metakind ids=comma_list(pure_ident_or_meta_ident) TMPtVirg
     { P.create_metadec ar ispure kindfn ids }
+| kindfn=metakind_fresh ids=comma_list(pure_ident_or_meta_ident_with_seed)
+    TMPtVirg
+    { P.create_fresh_metadec kindfn ids }
 | ar=arity ispure=pure
   kindfn=metakind_atomic
   ids=comma_list(pure_ident_or_meta_ident_with_not_eq(not_eq)) TMPtVirg
@@ -265,7 +278,12 @@ metadec:
     { P.create_metadec_ne ar ispure kindfn ids }
 | ar=arity TPosition a=option(TPosAny)
     ids=comma_list(pure_ident_or_meta_ident_with_not_eq(not_pos)) TMPtVirg
-    { let kindfn arity name pure check_meta constraints =
+    (* pb: position variables can't be inherited from normal rules, and then
+       there is no way to inherit from a generated rule, so there is no point
+       to have a position variable *)
+    { (if !Data.in_generating
+      then failwith "position variables not allowed in a generated rule file");
+      let kindfn arity name pure check_meta constraints =
       let tok = check_meta(Ast.MetaPosDecl(arity,name)) in
       let any = match a with None -> Ast.PER | Some _ -> Ast.ALL in
       !Data.add_pos_meta name constraints any; tok in
@@ -289,12 +307,14 @@ metadec:
          !Data.add_explist_meta name (Some lenname) pure; tok)
        id ids }
 
-%inline metakind:
+%inline metakind_fresh:
   TFresh TIdentifier
-    { (fun arity name pure check_meta ->
-      let tok = check_meta(Ast.MetaFreshIdDecl(arity,name)) in
-      !Data.add_id_meta name [] pure; tok) }
-| TParameter
+    { (fun name check_meta seed ->
+      let tok = check_meta(Ast.MetaFreshIdDecl(name,seed)) in
+      !Data.add_fresh_id_meta name; tok) }
+
+%inline metakind:
+  TParameter
     { (fun arity name pure check_meta ->
       let tok = check_meta(Ast.MetaParamDecl(arity,name)) in
       !Data.add_param_meta name pure; tok) }
@@ -309,7 +329,11 @@ metadec:
 | TType
     { (fun arity name pure check_meta ->
       let tok = check_meta(Ast.MetaTypeDecl(arity,name)) in
-      !Data.add_type_meta name pure; tok) } 
+      !Data.add_type_meta name pure; tok) }
+| TInitialiser
+    { (fun arity name pure check_meta ->
+      let tok = check_meta(Ast.MetaInitDecl(arity,name)) in
+      !Data.add_init_meta name pure; tok) }
 | TStatement
     { (fun arity name pure check_meta ->
       let tok = check_meta(Ast.MetaStmDecl(arity,name)) in
@@ -412,9 +436,9 @@ metadec:
              if not
                  (List.exists
                     (function
-                        Type_cocci.BaseType(Type_cocci.IntType,_) -> true
-                      | Type_cocci.BaseType(Type_cocci.ShortType,_) -> true
-                      | Type_cocci.BaseType(Type_cocci.LongType,_) -> true
+                        Type_cocci.BaseType(Type_cocci.IntType) -> true
+                      | Type_cocci.BaseType(Type_cocci.ShortType) -> true
+                      | Type_cocci.BaseType(Type_cocci.LongType) -> true
                       | _ -> false)
                     vl)
              then failwith "metavariable with int constraint must be an int"
@@ -437,21 +461,26 @@ arity: TBang0 { Ast.UNIQUE }
      | TPlus0 { Ast.MULTI }
      | /* empty */ { Ast.NONE }
 
-generic_ctype:
-       q=ctype_qualif
-         { Ast0.wrap(Ast0.ImplicitInt(q)) }
-     | q=ioption(ctype_qualif) ty=Tchar
-         { Ast0.wrap(Ast0.BaseType(P.clt2mcode Ast.CharType ty, q)) }
-     | q=ioption(ctype_qualif) ty=Tshort
-         { Ast0.wrap(Ast0.BaseType(P.clt2mcode Ast.ShortType ty, q)) }
-     | q=ioption(ctype_qualif) ty=Tint
-         { Ast0.wrap(Ast0.BaseType(P.clt2mcode Ast.IntType ty, q)) }
+generic_ctype_full:
+       q=ctype_qualif_opt ty=Tchar
+        { q (Ast0.wrap(Ast0.BaseType(Ast.CharType,[P.clt2mcode "char" ty]))) }
+     | q=ctype_qualif_opt ty=Tshort
+        { q (Ast0.wrap(Ast0.BaseType(Ast.ShortType,[P.clt2mcode "short" ty])))}
+     | q=ctype_qualif_opt ty=Tint
+         { q (Ast0.wrap(Ast0.BaseType(Ast.IntType,[P.clt2mcode "int" ty]))) }
      | t=Tdouble
-         { Ast0.wrap(Ast0.BaseType(P.clt2mcode Ast.DoubleType t, None)) }
+         { Ast0.wrap(Ast0.BaseType(Ast.DoubleType,[P.clt2mcode "double" t])) }
      | t=Tfloat
-         { Ast0.wrap(Ast0.BaseType(P.clt2mcode Ast.FloatType t, None)) }
-     | q=ioption(ctype_qualif) ty=Tlong
-         { Ast0.wrap(Ast0.BaseType(P.clt2mcode Ast.LongType ty, q)) }
+         { Ast0.wrap(Ast0.BaseType(Ast.FloatType,[P.clt2mcode "float" t])) }
+     | q=ctype_qualif_opt ty=Tlong
+         { q (Ast0.wrap(Ast0.BaseType(Ast.LongType,[P.clt2mcode "long" ty]))) }
+     | q=ctype_qualif_opt ty=Tlong ty1=Tlong
+         { q (Ast0.wrap
+               (Ast0.BaseType
+                  (Ast.LongLongType,
+                     [P.clt2mcode "long" ty;P.clt2mcode "long" ty1]))) }
+     | s=Tenum i=ident
+        { Ast0.wrap(Ast0.EnumName(P.clt2mcode "enum" s, i)) }
      | s=struct_or_union i=ident
         { Ast0.wrap(Ast0.StructUnionName(s, Some i)) }
      | s=struct_or_union i=ioption(ident)
@@ -476,9 +505,13 @@ generic_ctype:
                                 Ast0.Impure (*will be ignored*))) }
      | p=TTypeId
         { Ast0.wrap(Ast0.TypeName(P.id2mcode p)) }
-     | p=TMetaType
+     | q=ctype_qualif_opt p=TMetaType
         { let (nm,pure,clt) = p in
-        Ast0.wrap(Ast0.MetaType(P.clt2mcode nm clt,pure)) }
+        q (Ast0.wrap(Ast0.MetaType(P.clt2mcode nm clt,pure))) }
+
+generic_ctype:
+       q=ctype_qualif     { q None }
+     | generic_ctype_full { $1 }
 
 struct_or_union:
        s=Tstruct { P.clt2mcode Ast.Struct s }
@@ -522,7 +555,20 @@ ctype:
         { P.pointerify (P.make_cv cv ty) m }
      | cv=ioption(const_vol) t=Tvoid m=nonempty_list(TMul)
          { let ty =
-            Ast0.wrap(Ast0.BaseType(P.clt2mcode Ast.VoidType t, None)) in
+            Ast0.wrap(Ast0.BaseType(Ast.VoidType,[P.clt2mcode "void" t])) in
+          P.pointerify (P.make_cv cv ty) m }
+   | lp=TOPar0 t=midzero_list(ctype,ctype) rp=TCPar0
+      /* more hacks */
+    { let (mids,code) = t in
+      Ast0.wrap
+       (Ast0.DisjType(P.clt2mcode "(" lp,code,mids, P.clt2mcode ")" rp)) }
+
+ctype_full:
+       cv=ioption(const_vol) ty=generic_ctype_full m=list(TMul)
+        { P.pointerify (P.make_cv cv ty) m }
+     | cv=ioption(const_vol) t=Tvoid m=nonempty_list(TMul)
+         { let ty =
+            Ast0.wrap(Ast0.BaseType(Ast.VoidType,[P.clt2mcode "void" t])) in
           P.pointerify (P.make_cv cv ty) m }
    | lp=TOPar0 t=midzero_list(ctype,ctype) rp=TCPar0
       /* more hacks */
@@ -535,19 +581,25 @@ fn_ctype: // allows metavariables
        ty=generic_ctype m=list(TMul) { P.pointerify ty m }
      | t=Tvoid m=list(TMul)
          { P.pointerify
-            (Ast0.wrap(Ast0.BaseType(P.clt2mcode Ast.VoidType t, None)))
+            (Ast0.wrap(Ast0.BaseType(Ast.VoidType,[P.clt2mcode "void" t])))
             m }
 
-ctype_qualif:
-       Tunsigned   { P.clt2mcode Ast.Unsigned $1 }
-     | Tsigned     { P.clt2mcode Ast.Signed $1 }
+%inline ctype_qualif:
+  r=Tunsigned
+   { function x -> Ast0.wrap(Ast0.Signed(P.clt2mcode Ast.Unsigned r,x)) }
+| r=Tsigned
+   { function x -> Ast0.wrap(Ast0.Signed(P.clt2mcode Ast.Signed r,x)) }
+
+%inline ctype_qualif_opt:
+  s=ctype_qualif  { function x -> s (Some x) }
+| /* empty */   { function x -> x }
 
 /*****************************************************************************/
 
 /* have to inline everything to avoid conflicts? switch to proper
 declarations, statements, and expressions for the subterms */
 
-minus_body: 
+minus_body:
     f=loption(filespec)
     b=loption(minus_start)
     ew=loption(error_words)
@@ -555,7 +607,7 @@ minus_body:
       [] -> raise (Semantic_cocci.Semantic "minus slice can't be empty")
     | code -> Top_level.top_level code }
 
-plus_body: 
+plus_body:
     f=loption(filespec)
     b=loption(plus_start)
     ew=loption(error_words)
@@ -635,10 +687,12 @@ defineop:
              Ast0.wrap Ast0.NoParams,
              body)) }
 | TDefineParam define_param_list_option TCPar
-    { let (clt,ident,parenoff) = $1 in
+    { let (clt,ident,parenoff,parencol) = $1 in
+      (* clt is the start of the #define itself *)
       let (arity,line,lline,offset,col,strbef,straft,pos) = clt in
       let lp =
-       P.clt2mcode "(" (arity,line,lline,parenoff,0,[],[],Ast0.NoMetaPos) in
+       P.clt2mcode "("
+         (arity,line,lline,parenoff,parencol,[],[],Ast0.NoMetaPos) in
       function body ->
        Ast0.wrap
          (Ast0.Define
@@ -698,7 +752,7 @@ funproto:
              id, P.clt2mcode ";" pt)) }
 | s=ioption(storage) t=Tvoid
   id=func_ident lp=TOPar d=decl_list(name_opt_decl) rp=TCPar pt=TPtVirg
-    { let t = Ast0.wrap(Ast0.BaseType(P.clt2mcode Ast.VoidType t, None)) in
+    { let t = Ast0.wrap(Ast0.BaseType(Ast.VoidType,[P.clt2mcode "void" t])) in
       Ast0.wrap
         (Ast0.UnInit
           (s,
@@ -775,7 +829,8 @@ decl: t=ctype i=ident
                P.clt2mcode "(" lp1,d,P.clt2mcode ")" rp1)) in
        Ast0.wrap(Ast0.Param(fnptr, Some i)) }
     | t=Tvoid
-       { let ty = Ast0.wrap(Ast0.BaseType(P.clt2mcode Ast.VoidType t, None)) in
+       { let ty =
+         Ast0.wrap(Ast0.BaseType(Ast.VoidType,[P.clt2mcode "void" t])) in
           Ast0.wrap(Ast0.VoidParam(ty)) }
     | TMetaParam
        { let (nm,pure,clt) = $1 in
@@ -839,7 +894,19 @@ stm_dots:
     { Ast0.wrap(Ast0.Nest(P.clt2mcode "<+..." $1, b,
                          P.clt2mcode "...+>" c, List.concat w, true)) }
 
-whenppdecs: w=whens(when_start,rule_elem_statement)
+%inline stm_dots_ell:
+  a=TEllipsis w=list(whenppdecs)
+    { Ast0.wrap(Ast0.Dots(P.clt2mcode "..." a, List.concat w)) }
+
+%inline stm_dots_nest:
+  a=TOEllipsis w=list(whenppdecs) b=nest_start c=TCEllipsis
+    { Ast0.wrap(Ast0.Nest(P.clt2mcode "<..." a, b,
+                         P.clt2mcode "...>" c, List.concat w, false)) }
+| a=TPOEllipsis w=list(whenppdecs) b=nest_start c=TPCEllipsis
+    { Ast0.wrap(Ast0.Nest(P.clt2mcode "<+..." a, b,
+                         P.clt2mcode "...+>" c, List.concat w, true)) }
+
+whenppdecs: w=whens(when_start,rule_elem_statement,any_strict)
     { w }
 
 /* a statement that fits into a single rule_elem.  should nests be included?
@@ -923,7 +990,7 @@ decl_var:
         [Ast0.wrap(Ast0.UnInit(s,fn t,id,P.clt2mcode ";" pv))] }
   | decl_ident TOPar eexpr_list_option TCPar TPtVirg
       { [Ast0.wrap(Ast0.MacroDecl($1,P.clt2mcode "(" $2,$3,
-                                 P.clt2mcode ")" $4,P.clt2mcode ";" $5))] } 
+                                 P.clt2mcode ")" $4,P.clt2mcode ";" $5))] }
   | s=ioption(storage)
     t=fn_ctype lp1=TOPar st=TMul d=d_ident rp1=TCPar
     lp2=TOPar p=decl_list(name_opt_decl) rp2=TCPar
@@ -935,7 +1002,7 @@ decl_var:
               (t,P.clt2mcode "(" lp1,P.clt2mcode "*" st,P.clt2mcode ")" rp1,
                P.clt2mcode "(" lp2,p,P.clt2mcode ")" rp2)) in
       [Ast0.wrap(Ast0.Init(s,fn t,id,P.clt2mcode "=" q,e,P.clt2mcode ";" pv))]}
-  | s=Ttypedef t=ctype id=typedef_ident pv=TPtVirg
+  | s=Ttypedef t=ctype_full id=typedef_ident pv=TPtVirg
       { let s = P.clt2mcode "typedef" s in
         [Ast0.wrap(Ast0.Typedef(s,t,id,P.clt2mcode ";" pv))] }
 
@@ -976,7 +1043,7 @@ one_decl_var:
         Ast0.wrap(Ast0.UnInit(s,fn t,id,P.clt2mcode ";" pv)) }
   | decl_ident TOPar eexpr_list_option TCPar TPtVirg
       { Ast0.wrap(Ast0.MacroDecl($1,P.clt2mcode "(" $2,$3,
-                                 P.clt2mcode ")" $4,P.clt2mcode ";" $5)) } 
+                                 P.clt2mcode ")" $4,P.clt2mcode ";" $5)) }
   | s=ioption(storage)
     t=fn_ctype lp1=TOPar st=TMul d=d_ident rp1=TCPar
     lp2=TOPar p=decl_list(name_opt_decl) rp2=TCPar
@@ -1012,6 +1079,9 @@ initialize:
       { Ast0.wrap
          (Ast0.InitList(P.clt2mcode "{" $1,Ast0.wrap(Ast0.DOTS []),
                         P.clt2mcode "}" $2)) }
+  | TMetaInit
+      {let (nm,pure,clt) = $1 in
+      Ast0.wrap(Ast0.MetaInit(P.clt2mcode nm clt,pure)) }
 
 initialize2:
   /*arithexpr and not eexpr because can have ambiguity with comma*/
@@ -1024,16 +1094,19 @@ initialize2:
        (Ast0.InitList(P.clt2mcode "{" $1,Ast0.wrap(Ast0.DOTS []),
                       P.clt2mcode "}" $2)) }
            /* gccext:, labeled elements */
-| TDot ident TEq initialize2
-    { Ast0.wrap(Ast0.InitGccDotName(P.clt2mcode "." $1,$2,P.clt2mcode "=" $3,$4)) }
+| list(designator) TEq initialize2
+    { Ast0.wrap(Ast0.InitGccExt($1,P.clt2mcode "=" $2,$3)) }
 | ident TDotDot initialize2
     { Ast0.wrap(Ast0.InitGccName($1,P.clt2mcode ":" $2,$3)) } /* in old kernel */
-| TOCro eexpr TCCro TEq initialize2
-    { Ast0.wrap(Ast0.InitGccIndex(P.clt2mcode "[" $1,$2,P.clt2mcode "]" $3,
-                                 P.clt2mcode "=" $4,$5)) }
-| TOCro eexpr TEllipsis eexpr TCCro TEq initialize2
-    { Ast0.wrap(Ast0.InitGccRange(P.clt2mcode "[" $1,$2,P.clt2mcode "..." $3,
-                                 $4,P.clt2mcode "]" $5,P.clt2mcode "=" $6,$7)) }
+
+designator: 
+ | TDot ident 
+     { Ast0.DesignatorField (P.clt2mcode "." $1,$2) } 
+ | TOCro eexpr TCCro 
+     { Ast0.DesignatorIndex (P.clt2mcode "[" $1,$2,P.clt2mcode "]" $3) }
+ | TOCro eexpr TEllipsis eexpr TCCro 
+     { Ast0.DesignatorRange (P.clt2mcode "[" $1,$2,P.clt2mcode "..." $3,
+                            $4,P.clt2mcode "]" $5) }
 
 initialize_list:
    initialize_list_start { Ast0.wrap(Ast0.DOTS($1)) }
@@ -1143,17 +1216,18 @@ dot_expressions:
   TEllipsis { Ast0.wrap(Ast0.Edots(P.clt2mcode "..." $1,None)) }
 | nest_expressions { $1 }
 
+/* not clear what whencode would mean, so just drop it */
 nest_expressions:
-  TOEllipsis w=option(whenexp) e=expr_dots(TEllipsis) c=TCEllipsis
+  TOEllipsis e=expr_dots(TEllipsis) c=TCEllipsis
     { Ast0.wrap(Ast0.NestExpr(P.clt2mcode "<..." $1,
                              Ast0.wrap(Ast0.DOTS(e (P.mkedots "..."))),
-                             P.clt2mcode "...>" c, w, false)) }
-| TPOEllipsis w=option(whenexp) e=expr_dots(TEllipsis) c=TPCEllipsis
+                             P.clt2mcode "...>" c, None, false)) }
+| TPOEllipsis e=expr_dots(TEllipsis) c=TPCEllipsis
     { Ast0.wrap(Ast0.NestExpr(P.clt2mcode "<+..." $1,
                              Ast0.wrap(Ast0.DOTS(e (P.mkedots "..."))),
-                             P.clt2mcode "...+>" c, w, true)) }
+                             P.clt2mcode "...+>" c, None, true)) }
 
-whenexp: TWhen TNotEq w=eexpr TLineEnd { w }
+//whenexp: TWhen TNotEq w=eexpr TLineEnd { w }
 
 basic_expr(recurser,primary_extra):
   assign_expr(recurser,primary_extra)                        { $1 }
@@ -1227,7 +1301,7 @@ unary_expr(r,pe):
       { Ast0.wrap(Ast0.Infix ($2, P.clt2mcode Ast.Inc $1)) }
   | TDec unary_expr(r,pe)
       { Ast0.wrap(Ast0.Infix ($2, P.clt2mcode Ast.Dec $1)) }
-  | unary_op unary_expr(r,pe)
+  | unary_op cast_expr(r,pe)
       { let mcode = $1 in Ast0.wrap(Ast0.Unary($2, mcode)) }
   | TBang unary_expr(r,pe)
       { let mcode = P.clt2mcode Ast.Not $1 in
@@ -1330,6 +1404,11 @@ pure_ident_or_meta_ident:
      | Tlist                     { (None,"list") }
      | TError                    { (None,"error") }
      | TType                     { (None,"type") }
+     | TName                     { (None,"name") }
+
+pure_ident_or_meta_ident_with_seed:
+       pure_ident_or_meta_ident { ($1,None) }
+     | pure_ident_or_meta_ident TEq s=TString { ($1,Some (P.id2name s)) }
 
 pure_ident_or_meta_ident_with_not_eq(not_eq):
        i=pure_ident_or_meta_ident l=loption(not_eq) { (i,l) }
@@ -1338,20 +1417,30 @@ not_eq:
        TNotEq i=pure_ident
          { (if !Data.in_iso
           then failwith "constraints not allowed in iso file");
+          (if !Data.in_generating
+           (* pb: constraints not stored with metavars; too lazy to search for
+             them in the pattern *)
+          then failwith "constraints not allowed in a generated rule file");
           [Ast0.wrap(Ast0.Id(P.id2mcode i))] }
      | TNotEq TOBrace l=comma_list(pure_ident) TCBrace
         { (if !Data.in_iso
           then failwith "constraints not allowed in iso file");
+          (if !Data.in_generating
+          then failwith "constraints not allowed in a generated rule file");
           List.map (function i -> Ast0.wrap(Ast0.Id(P.id2mcode i))) l }
 
 not_eqe:
        TNotEq i=pure_ident
          { (if !Data.in_iso
           then failwith "constraints not allowed in iso file");
+          (if !Data.in_generating
+          then failwith "constraints not allowed in a generated rule file");
           [Ast0.wrap(Ast0.Ident(Ast0.wrap(Ast0.Id(P.id2mcode i))))] }
      | TNotEq TOBrace l=comma_list(pure_ident) TCBrace
         { (if !Data.in_iso
           then failwith "constraints not allowed in iso file");
+          (if !Data.in_generating
+          then failwith "constraints not allowed in a generated rule file");
           List.map
             (function i ->
               Ast0.wrap(Ast0.Ident(Ast0.wrap(Ast0.Id(P.id2mcode i)))))
@@ -1361,10 +1450,14 @@ not_ceq:
        TNotEq i=ident_or_const
          { (if !Data.in_iso
           then failwith "constraints not allowed in iso file");
+          (if !Data.in_generating
+          then failwith "constraints not allowed in a generated rule file");
           [i] }
      | TNotEq TOBrace l=comma_list(ident_or_const) TCBrace
         { (if !Data.in_iso
           then failwith "constraints not allowed in iso file");
+          (if !Data.in_generating
+          then failwith "constraints not allowed in a generated rule file");
           l }
 
 ident_or_const:
@@ -1377,6 +1470,8 @@ not_pos:
        TNotEq i=meta_ident
          { (if !Data.in_iso
           then failwith "constraints not allowed in iso file");
+          (if !Data.in_generating
+          then failwith "constraints not allowed in a generated rule file");
           match i with
             (None,_) -> failwith "constraint must be an inherited variable"
           | (Some rule,name) ->
@@ -1386,6 +1481,8 @@ not_pos:
      | TNotEq TOBrace l=comma_list(meta_ident) TCBrace
         { (if !Data.in_iso
           then failwith "constraints not allowed in iso file");
+          (if !Data.in_generating
+          then failwith "constraints not allowed in a generated rule file");
           List.map
             (function
                 (None,_) ->
@@ -1439,7 +1536,8 @@ typedef_ident:
 /*****************************************************************************/
 
 decl_list(decl):
-   decl_list_start(decl)
+  /* empty */ { Ast0.wrap(Ast0.DOTS([])) }
+| decl_list_start(decl)
      {let circle x =
        match Ast0.unwrap x with Ast0.Pcircles(_) -> true | _ -> false in
      if List.exists circle $1
@@ -1464,7 +1562,7 @@ one_dec(decl):
        Some nm -> Some(P.clt2mcode nm clt)
       | None -> None in
     Ast0.wrap(Ast0.MetaParamList(nm,lenname,pure)) }
+
 comma_decls(dotter,decl):
   TComma dotter
     { function dot_builder ->
@@ -1514,9 +1612,16 @@ minus_start:
   fundecl                { [Ast0.wrap(Ast0.DECL($1))] }
 | ctype                  { [Ast0.wrap(Ast0.OTHER(Ast0.wrap(Ast0.Ty($1))))] }
 | top_init          { [Ast0.wrap(Ast0.OTHER(Ast0.wrap(Ast0.TopInit($1))))] }
-| toplevel_seq_start(toplevel_after_dots_init)
+| toplevel_seq_startne(toplevel_after_dots_init)
     { List.map (function x -> Ast0.wrap(Ast0.OTHER(x))) $1 }
 
+toplevel_seq_startne(after_dots_init):
+  a=stm_dots_ell b=after_dots_init           { a::b }
+| a=stm_dots_nest b=after_dots_init           { a::b }
+| a=stm_dots_nest                      { [a] }
+| expr toplevel_after_exp            { (Ast0.wrap(Ast0.Exp($1)))::$2 }
+| decl_statement_expr toplevel_after_stm  { $1@$2 }
+
 toplevel_seq_start(after_dots_init):
   stm_dots after_dots_init           { $1::$2 }
 | expr toplevel_after_exp            { (Ast0.wrap(Ast0.Exp($1)))::$2 }
@@ -1704,7 +1809,7 @@ edots_when(dotter,when_grammar):
     d=dotter                                      { (d,None) }
   | d=dotter TWhen TNotEq w=when_grammar TLineEnd { (d,Some w) }
 
-whens(when_grammar,simple_when_grammar):
+whens(when_grammar,simple_when_grammar,any_strict):
     TWhen TNotEq w=when_grammar TLineEnd { [Ast0.WhenNot w] }
   | TWhen TEq w=simple_when_grammar TLineEnd { [Ast0.WhenAlways w] }
   | TWhen comma_list(any_strict) TLineEnd
@@ -1718,6 +1823,11 @@ any_strict:
   | TForall { Ast.WhenForall }
   | TExists { Ast.WhenExists }
 
+any_only:
+    TAny    { Ast.WhenAny }
+  | TForall { Ast.WhenForall }
+  | TExists { Ast.WhenExists }
+
 /*****************************************************************************
 *
 *