X-Git-Url: http://git.hcoop.net/bpt/coccinelle.git/blobdiff_plain/708f4980a90e2a254d7863f875888e9f5c6db0b3..65038c617fe3e5d7a284059fbfa78dddfbb9b9c4:/parsing_cocci/iso_pattern.ml
diff --git a/parsing_cocci/iso_pattern.ml b/parsing_cocci/iso_pattern.ml
index 16d484b..bdbb350 100644
--- a/parsing_cocci/iso_pattern.ml
+++ b/parsing_cocci/iso_pattern.ml
@@ -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 .
-*
-* 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 .
+ *
+ * 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