Commit fcee5a38 authored by bguillaum's avatar bguillaum

strategies for modules applications:

- ast
- parser

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/semagramme/libcaml-grew/trunk@8712 7838e531-6607-4d57-9587-6c381814729c
parent 8a2080cd
all:
pdflatex strat
arch:
dot -Tpdf arch.dot -o arch.pdf
clean:
......
\documentclass[a4paper]{article}
\usepackage{fullpage}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{amsmath}
\usepackage{url}
\usepackage{graphicx}
\usepackage{bussproofs}
\newtheorem{definition}{Definition}
\title{Strategies for Grew}
\author{Bruno Guillaume}
\begin{document}
\maketitle
\section{Notations} % (fold)
\label{sec:not}
When the graph $G$ rewrite 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} % (fold)
\label{sec:strat}
Given a set $\cal{M}$ of modules and a set $\cal{F}$ of filters, strategies are defined by the following grammar:
\[
S = M \mid S;S \mid S+S \mid \diamond S \mid S^* \mid F[S]
\]
Applying a strategy $S$ on the graph $G$ is an non-determintic process.
Hence, we define a relation $G \longrightarrow_S G'$ with the following rules:
\begin{prooftree}
\AxiomC{}
\LeftLabel{(Module)}
\UnaryInfC{$G \longrightarrow_M M(G)$}
\end{prooftree}
%
\begin{prooftree}
\AxiomC{$G \longrightarrow_{S_1} \{G_1, \ldots, G_k\}$}
\AxiomC{$\forall i \in[1,k], G_i \longrightarrow_{S_2} E_i$}
\LeftLabel{(Sequence)}
\BinaryInfC{$G \longrightarrow_{S_1;S_2} \bigcup_{1\leq i \leq k}{E_i}$}
\end{prooftree}
%
\begin{prooftree}
\AxiomC{$G \longrightarrow_{S_1} E_1$}
\AxiomC{$G \longrightarrow_{S_2} E_2$}
\LeftLabel{(Union)}
\BinaryInfC{$G \longrightarrow_{S_1 + S_2} E_1 \cup E_2 $}
\end{prooftree}
%
\begin{prooftree}
\AxiomC{$G \longrightarrow_S \emptyset $}
\LeftLabel{(Iter$_\emptyset$)}
\UnaryInfC{$G \longrightarrow_{S^*} \{G\}$}
\end{prooftree}
%
\begin{prooftree}
\AxiomC{$G \longrightarrow_{S} \{G_1, \ldots, G_k\}$}
\AxiomC{$\forall i \in[1,k], G_i \longrightarrow_{S^*} E_i$}
\LeftLabel{(Iter)}
\BinaryInfC{$G \longrightarrow_{S^*} \bigcup_{1\leq i \leq k}{E_i}$}
\end{prooftree}
%
\begin{prooftree}
\AxiomC{$G \longrightarrow_S \emptyset $}
\LeftLabel{(Diamond$_\emptyset$)}
\UnaryInfC{$G \longrightarrow_{\diamond S} \emptyset$}
\end{prooftree}
%
\begin{prooftree}
\AxiomC{$G \longrightarrow_{S} \{G_1, \ldots, G_k\}$}
\LeftLabel{(Diamond)}
\UnaryInfC{$G \longrightarrow_{\diamond S} \{G_i\}$}
\end{prooftree}
%
\begin{prooftree}
\AxiomC{$G \longrightarrow_{S} E$}
\LeftLabel{(Filter)}
\UnaryInfC{$G \longrightarrow_{F[S]} F(E)$}
\end{prooftree}
% section strat (end)
\end{document}
......@@ -215,13 +215,50 @@ module Ast = struct
mod_dir: string; (* the directory where the module is defined (for lp file localisation) *)
}
type sequence = {
type old_sequence = {
seq_name:string;
seq_mod:string list;
seq_doc:string list;
seq_loc:Loc.t;
}
type new_sequence =
| Ref of string
| List of new_sequence list
| Plus of new_sequence list
| Star of new_sequence
| Diamond of new_sequence
let rec new_sequence_to_string = function
| Ref m -> m
| List l -> "[" ^ (String.concat "; " (List.map new_sequence_to_string l)) ^ "]"
| Plus l -> "[" ^ (String.concat "+" (List.map new_sequence_to_string l)) ^ "]"
| Star s -> "[" ^ (new_sequence_to_string s) ^"]" ^ "*"
| Diamond s -> "◇" ^ "[" ^(new_sequence_to_string s)^"]"
let rec flatten = function
| Ref m -> Ref m
| Star s -> Star (flatten s)
| Diamond s -> Diamond (flatten s)
| List l ->
let fl = List.map flatten l in
let rec loop = function
| [] -> []
| (List l) :: tail -> l @ (loop tail)
| x :: tail -> x :: (loop tail)
in List (loop fl)
| Plus l ->
let fl = List.map flatten l in
let rec loop = function
| [] -> []
| (Plus l) :: tail -> l @ (loop tail)
| x :: tail -> x :: (loop tail)
in Plus (loop fl)
type sequence =
| Old of old_sequence
| New of ((string * Loc.t) * new_sequence)
(** a GRS: graph rewriting system *)
type module_or_include =
| Modul of modul
......
......@@ -155,12 +155,26 @@ module Ast : sig
mod_dir: string; (* the directory where the module is defined (for lp file localisation) *)
}
type sequence = {
seq_name:string;
seq_mod:string list;
seq_doc:string list;
seq_loc:Loc.t;
}
type old_sequence = {
seq_name:string;
seq_mod:string list;
seq_doc:string list;
seq_loc:Loc.t;
}
type new_sequence =
| Ref of string
| List of new_sequence list
| Plus of new_sequence list
| Star of new_sequence
| Diamond of new_sequence
val new_sequence_to_string : new_sequence -> string
val flatten : new_sequence -> new_sequence
type sequence =
| Old of old_sequence
| New of ((string * Loc.t) * new_sequence)
type module_or_include =
| Modul of modul
......
......@@ -199,11 +199,17 @@ module Sequence = struct
) t.def
let build module_list ast_sequence =
match ast_sequence with
| Ast.New ((n,_),s) ->
printf "----%s----> %s\n%!" n (Ast.new_sequence_to_string s);
printf "====%s====> %s\n%!" n (Ast.new_sequence_to_string (Ast.flatten s));
{name=n; def=[]; loc=Loc.file "No_file_given"; }
| Ast.Old old_seq ->
let sequence =
{
name = ast_sequence.Ast.seq_name;
def = ast_sequence.Ast.seq_mod;
loc = ast_sequence.Ast.seq_loc;
name = old_seq.Ast.seq_name;
def = old_seq.Ast.seq_mod;
loc = old_seq.Ast.seq_loc;
} in
check module_list sequence; sequence
end (* module Sequence *)
......
......@@ -335,7 +335,9 @@ module Html_doc = struct
wnl " <div class=\"navbar\">&nbsp;<a href=\"index.html\">Up</a></div>";
wnl " <center><h1>List of sequences</h1></center>";
List.iter
(fun seq ->
(function
| Ast.New _ -> failwith "Wait..."
| Ast.Old seq ->
wnl "<h6>%s</h6>" seq.Ast.seq_name;
List.iter (fun l -> wnl "<p>%s</p>" (doc_to_html l)) seq.Ast.seq_doc;
......
......@@ -110,6 +110,11 @@ let localize t = (t,get_loc ())
%start <Grew_ast.Ast.gr> gr
%start <Grew_ast.Ast.module_or_include list> included
%start <Grew_ast.Ast.pattern> pattern
%left SEMIC
%left PLUS
%nonassoc STAR
%nonassoc DISEQUAL
%%
......@@ -581,14 +586,29 @@ sequences:
sequence:
(* sequence { ant; p7_to_p7p-mc} *)
| doc=option(COMMENT) id_loc=simple_id_with_loc mod_names=delimited(LACC,separated_list_final_opt(SEMIC,simple_id),RACC)
/* | doc=option(COMMENT) id_loc=simple_id_with_loc mod_names=delimited(LACC,separated_list_final_opt(SEMIC,simple_id),RACC)
{
{ Ast.seq_name = fst id_loc;
seq_mod = mod_names;
seq_mod = mod_names;*/
| doc = option(COMMENT) id_loc=simple_id_with_loc mod_names=delimited(LACC,separated_list_final_opt(SEMIC,COMPLEX_ID),RACC)
{
Ast.Old { Ast.seq_name = fst id_loc;
seq_mod = List.map (fun x -> Ast.simple_id_of_ci x) mod_names ;
seq_doc = begin match doc with Some d -> d | None -> [] end;
seq_loc = snd id_loc;
}
}
| doc = option(COMMENT) id_loc=simple_id_with_loc EQUAL s=op_seq { Ast.New (id_loc, s) }
op_seq:
| m=COMPLEX_ID { Ast.Ref (Ast.simple_id_of_ci m) }
| LPAREN s=op_seq RPAREN { s }
| s=op_seq STAR { Ast.Star (s) }
| s1=op_seq PLUS s2=op_seq { Ast.Plus [s1; s2] }
| s1=op_seq SEMIC s2=op_seq { Ast.List [s1; s2] }
| DISEQUAL s=op_seq { Ast.Diamond s }
/*=============================================================================================*/
/* ISOLATED PATTERN (grep mode) */
......
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