Skip to content

GitLab

Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit ae5d1358 authored by bguillaum's avatar bguillaum
Browse files

Change strategies syntax: “pick(S)”, “try(S)” and “S!” 

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/semagramme/libcaml-grew/trunk@9149 7838e531-6607-4d57-9587-6c381814729c
parent 51bcc0ee
Hide whitespace changes
Inline Side-by-side
Showing with 82 additions and 71 deletions
dev/strat.tex
View file @ ae5d1358
......@@ -12,10 +12,11 @@
\newtheorem{lemma}{Lemma}
\newcommand{\ie}{{\it i.e.\ }}
\newcommand{\pick}{\mathrm{pick}}
\newcommand{\try}{\mathrm{try}}
\title{Strategies for Grew}
%\author{Bruno Guillaume}
\date{}
\begin{document}
......@@ -24,34 +25,24 @@
\section{Notations}
\label{sec:not}
Let $\cal{G}$ be the set of graphs.
When the graph $G$ rewrites to $G'$ with some rule $R$, we write $G \Longrightarrow_R G'$.
When a matching exists for pattern $P$ in the graph $G$, we write $P \hookrightarrow G$; if it is not the case, we write $P \not\hookrightarrow G$
\begin{definition}
A {\em module} is a set of rewriting rules.
A {\em filter} is a set of patterns.
\end{definition}
Given a module $M$ and a graph $G$, we define the set of graphs $M(G) = \{ G' \mid G \Longrightarrow_R G', R \in M\}$.
Given a filter $F$ and a set $E$ of graphs, we define $F(E) = \{ G \in E \mid \forall P \in F, P \not\hookrightarrow G \}$.
% section not (end)
\section{Strategies}
\label{sec:strat}
Given a set $\cal{M}$ of modules and a set $\cal{F}$ of filters, strategies are defined by the following grammar:
Given a set $\cal{R}$ of rules, strategies are defined by the following grammar:
\[
S = M \mid S;S \mid S+S \mid S^\diamond \mid S^? \mid S^* \mid F[S]
S = R \mid (S) \mid S;S \mid S+S \mid S^* \mid \pick(S) \mid \try(S)
\]
Applying a strategy $S$ on the graph $G$ is a non-deterministic process.
Hence, we define a relation $G \longrightarrow_S G'$ with the following rules:
Applying a strategy $S$ on the graph $G$ is a non-deterministic and non confluent process.
Hence, we define a relation between a graph $G \in \cal{G}$ and a set of graphs $\cal{S} \subset \cal{G}$ written $G \longrightarrow_S \cal{S}$ with the following rules:
\begin{prooftree}
\AxiomC{}
\LeftLabel{(Module)}
\UnaryInfC{$G \longrightarrow_M M(G)$}
\LeftLabel{(Rule)}
\UnaryInfC{$G \longrightarrow_R \{ G' \mid G \Longrightarrow_R G'\}$}
\end{prooftree}
......@@ -86,61 +77,43 @@ Hence, we define a relation $G \longrightarrow_S G'$ with the following rules:
\DisplayProof
\end{center}
\begin{center}
\AxiomC{$G \longrightarrow_S \emptyset $}
\LeftLabel{(One$_\emptyset$)}
\UnaryInfC{$G \longrightarrow_{S^?} \{G\}$}
\LeftLabel{(Pick$_\emptyset$)}
\UnaryInfC{$G \longrightarrow_{\pick(S)} \emptyset$}
\DisplayProof
%
\qquad
%
\AxiomC{$G \longrightarrow_{S} \{G_1, \ldots, G_k\}$}
\LeftLabel{(One)}
\UnaryInfC{$G \longrightarrow_{S^?} \{G_i\}$}
\LeftLabel{(Pick)}
\UnaryInfC{$G \longrightarrow_{\pick(S)} \{G_i\}$}
\DisplayProof
\end{center}
\begin{center}
\AxiomC{$G \longrightarrow_S \emptyset $}
\LeftLabel{(Diamond$_\emptyset$)}
\UnaryInfC{$G \longrightarrow_{S^\diamond} \emptyset$}
\LeftLabel{(One$_\emptyset$)}
\UnaryInfC{$G \longrightarrow_{\try(S)} \{G\}$}
\DisplayProof
%
\qquad
%
\AxiomC{$G \longrightarrow_{S} \{G_1, \ldots, G_k\}$}
\LeftLabel{(Diamond)}
\UnaryInfC{$G \longrightarrow_{S^\diamond} \{G_i\}$}
\DisplayProof
\end{center}
\begin{center}
\AxiomC{$G \longrightarrow_{S} E$}
\LeftLabel{(Filter)}
\UnaryInfC{$G \longrightarrow_{F[S]} F(E)$}
\LeftLabel{(One)}
\UnaryInfC{$G \longrightarrow_{\try(S)} \{G_i\}$}
\DisplayProof
\end{center}
A strategy is called \emph{filter-free} if it contains no filter, \ie if it is defined by the following grammar:
\[
S = M \mid S;S \mid S+S \mid S^\diamond \mid S^? \mid S^*
\]
\begin{lemma}
If $S$ is a filter-free strategy, then $(S^\diamond)^* \equiv (S^*)^\diamond$.
In particular, for any module $M$, $(M^\diamond)^* \equiv (M^*)^\diamond$.
If $S$ is a strategy, then $(\pick(S))^* \equiv \pick(S^*)$.
\end{lemma}
\begin{proof}
TODO
\end{proof}
We use the notation $S^! = (S^*)^\diamond$ as a shortcut.
We use the notation $S^! = \pick(S^*)$ as a shortcut.
\end{document}
src/grew_ast.ml
View file @ ae5d1358
......@@ -319,15 +319,19 @@ module Ast = struct
| Seq of strat_def list (* a sequence of strategies to apply one after the other *)
| Plus of strat_def list (* a set of strategies to apply in parallel *)
| Star of strat_def (* a strategy to apply iteratively *)
| Diamond of strat_def (* pick one normal form a the given strategy *)
| Bang of strat_def (* a strategy to apply iteratively and deterministically *)
| Pick of strat_def (* pick one normal form a the given strategy; return 0 if nf *)
| Try of strat_def (* pick one normal form a the given strategy; return input if nf *)
| Sequence of string list (* compatibility mode with old code *)
let rec strat_def_to_string = function
| Ref m -> m
| Seq l -> "[" ^ (String.concat "; " (List.map strat_def_to_string l)) ^ "]"
| Plus l -> "[" ^ (String.concat "+" (List.map strat_def_to_string l)) ^ "]"
| Star s -> "[" ^ (strat_def_to_string s) ^"]" ^ "*"
| Diamond s -> "◇" ^ "[" ^(strat_def_to_string s)^"]"
| Seq l -> "(" ^ (String.concat "; " (List.map strat_def_to_string l)) ^ ")"
| Plus l -> "(" ^ (String.concat "+" (List.map strat_def_to_string l)) ^ ")"
| Star s -> "(" ^ (strat_def_to_string s) ^")" ^ "*"
| Bang s -> "(" ^ (strat_def_to_string s) ^")" ^ "!"
| Pick s -> "pick" ^ "(" ^(strat_def_to_string s)^")"
| Try s -> "try" ^ "(" ^(strat_def_to_string s)^")"
| Sequence names -> "{" ^ (String.concat ";" names) ^ "}"
(* invariant: Seq list and Plus list are not empty in the input and so not empty in the output *)
......@@ -335,7 +339,9 @@ module Ast = struct
| Sequence l -> Sequence l
| Ref m -> Ref m
| Star s -> Star (strat_def_flatten s)
| Diamond s -> Diamond (strat_def_flatten s)
| Bang s -> Bang (strat_def_flatten s)
| Pick s -> Pick (strat_def_flatten s)
| Try s -> Try (strat_def_flatten s)
| Seq l ->
let fl = List.map strat_def_flatten l in
let rec loop = function
......
src/grew_ast.mli
View file @ ae5d1358
......@@ -199,7 +199,9 @@ module Ast : sig
| Seq of strat_def list (* a sequence of strategies to apply one after the other *)
| Plus of strat_def list (* a set of strategies to apply in parallel *)
| Star of strat_def (* a strategy to apply iteratively *)
| Diamond of strat_def (* pick one normal form a the given strategy *)
| Bang of strat_def (* a strategy to apply iteratively and deterministically *)
| Pick of strat_def (* pick one normal form a the given strategy; return 0 if nf *)
| Try of strat_def (* pick one normal form a the given strategy; return input if nf *)
| Sequence of string list (* compatibility mode with old code *)
val strat_def_to_string: strat_def -> string
......
src/grew_grs.ml
View file @ ae5d1358
......@@ -272,7 +272,7 @@ module Grs = struct
loop (Instance.from_graph graph) (strategy.Ast.strat_def)
(* [new_style grs module_list] return an equivalent strategy expressed with Seq, Diamond and Star *)
(* [new_style grs module_list] return an equivalent strategy expressed with Seq, Pick and Star *)
let new_style grs module_list =
Ast.Seq
(List.map
......@@ -281,7 +281,7 @@ module Grs = struct
try List.find (fun m -> m.Modul.name=module_name) grs.modules
with Not_found -> Log.fcritical "No module named '%s'" module_name in
if modul.Modul.confluent
then Ast.Diamond (Ast.Star (Ast.Ref module_name))
then Ast.Pick (Ast.Star (Ast.Ref module_name))
else Ast.Star (Ast.Ref module_name)
) module_list
)
......@@ -325,8 +325,17 @@ module Grs = struct
| None -> Some inst
| Some new_inst -> loop new_inst (Ast.Star sub_strat)
end
(* Diamond *)
| Ast.Diamond sub_strat -> loop inst sub_strat
(* Pick *)
| Ast.Pick sub_strat -> loop inst sub_strat
(* Bang *)
| Ast.Bang sub_strat -> loop inst (Ast.Star sub_strat)
(* Try *)
| Ast.Try sub_strat ->
begin
match loop inst sub_strat with
| None -> Some inst
| Some new_inst -> Some new_inst
end
(* Old style seq definition *)
| Ast.Sequence module_list -> loop inst (new_style grs module_list) in
loop inst strat
......@@ -361,28 +370,38 @@ module Grs = struct
if Instance_set.is_empty one_iter
then Instance_set.singleton inst
else Instance_set.fold (fun new_inst acc -> Instance_set.union acc (loop new_inst (Ast.Star sub_strat))) one_iter Instance_set.empty
(* Diamond *)
| Ast.Diamond sub_strat ->
(* Pick *)
| Ast.Pick sub_strat ->
begin
match one_rewrite grs sub_strat inst with
| Some new_inst -> Instance_set.singleton new_inst
| None -> Instance_set.empty
end
(* Try *)
| Ast.Try sub_strat ->
begin
match one_rewrite grs sub_strat inst with
| Some new_inst -> Instance_set.singleton new_inst
| None -> Instance_set.singleton inst
end
(* Bang *)
| Ast.Bang sub_strat -> loop inst (Ast.Pick (Ast.Star sub_strat))
(* Old style seq definition *)
| Ast.Sequence module_list -> loop inst (new_style grs module_list) in
List.map
(fun inst -> inst.Instance.graph)
(Instance_set.elements (loop (Instance.from_graph graph) (Parser.strat_def strat_desc)))
(* ---------------------------------------------------------------------------------------------------- *)
(* construction of the rew_display *)
let rec diamond = function
let rec pick = function
| Libgrew_types.Node (_, _, []) -> Log.bug "Empty node"; exit 12
| Libgrew_types.Node (graph, name, (bs,rd)::_) -> Libgrew_types.Node (graph, "pick(" ^ name^")", [(bs, pick rd)])
| x -> x
let rec try_ = function
| Libgrew_types.Node (_, _, []) -> Log.bug "Empty node"; exit 12
| Libgrew_types.Node (graph, name, (bs,rd)::_) -> Libgrew_types.Node (graph, "◇" ^ name, [(bs, diamond rd)])
| Libgrew_types.Node (graph, name, (bs,rd)::_) -> Libgrew_types.Node (graph, "try(" ^ name^")", [(bs, pick rd)])
| x -> x
(* ---------------------------------------------------------------------------------------------------- *)
......@@ -494,7 +513,9 @@ module Grs = struct
let one_step = loop instance head_strat in decr indent;
apply_leaf (Ast.Seq tail_strat) one_step
| Ast.Diamond strat -> diamond (loop instance strat)
| Ast.Pick strat -> pick (loop instance strat)
| Ast.Try strat -> try_ (loop instance strat)
| Ast.Bang strat -> loop instance (Ast.Pick (Ast.Star strat))
(* ========> Strat defined as a sequence of sub-strategies <========= *)
| Ast.Plus [] -> Log.bug "[Grs.build_rew_display] Empty union!"; exit 2
......
src/grew_lexer.mll
View file @ ae5d1358
......@@ -178,6 +178,9 @@ and standard target = parse
| "filter" { FILTER }
| "sequences" { SEQUENCES }
| "pick" { PICK }
| "try" { TRY }
| "graph" { GRAPH }
| digit+ ('.' digit*)? as number { FLOAT (float_of_string number) }
......
src/grew_parser.mly
View file @ ae5d1358
......@@ -97,6 +97,9 @@ let localize t = (t,get_loc ())
%token ADD_NODE /* add_node */
%token DEL_FEAT /* del_feat */
%token PICK /* pick */
%token TRY /* try */
%token <string> DOLLAR_ID /* $id */
%token <string> AROBAS_ID /* @id */
%token <string> COLOR /* @#89abCD */
......@@ -127,7 +130,7 @@ let localize t = (t,get_loc ())
%left SEMIC
%left PLUS
%nonassoc STAR
%nonassoc DISEQUAL
%nonassoc BANG
%%
......@@ -712,12 +715,15 @@ sequence:
}
strat_def_rec:
| m=simple_id { Ast.Ref m }
| LPAREN s=strat_def_rec RPAREN { s }
| s=strat_def_rec STAR { Ast.Star (s) }
| m=simple_id { Ast.Ref m }
| LPAREN s=strat_def_rec RPAREN { s }
| s=strat_def_rec STAR { Ast.Star (s) }
| s=strat_def_rec BANG { Ast.Star (s) }
| s1=strat_def_rec PLUS s2=strat_def_rec { Ast.Plus [s1; s2] }
| s1=strat_def_rec SEMIC s2=strat_def_rec { Ast.Seq [s1; s2] }
| DISEQUAL s=strat_def_rec { Ast.Diamond s }
| PICK LPAREN s=strat_def_rec RPAREN { Ast.Pick s }
| TRY LPAREN s=strat_def_rec RPAREN { Ast.Try s }
strat_def: s = strat_def_rec EOF { s }
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment