Commit 645e0bae authored by Bruno Guillaume's avatar Bruno Guillaume

New strategies

parent 0d7a7dcb
......@@ -483,9 +483,7 @@ module New_ast = struct
| Iter of strat (* a strategy to apply iteratively *)
| If of strat * strat * strat (* choose a stragegy with a test *)
(* syntactic sugar *)
| Empty (* ≜ Seq [] *)
| Try of strat (* ≜ If (S, S, Empty): pick one normal form a the given strategy; return input if nf *)
| Rules of Ast.node_ident (* ≜ Alt (rules defined in the top level of the package with the given name *)
type decl =
| Features of Ast.feature_spec list
......
......@@ -254,9 +254,7 @@ module New_ast : sig
| Iter of strat (* a strategy to apply iteratively *)
| If of strat * strat * strat (* choose a stragegy with a test *)
(* syntactic sugar *)
| Empty (* ≜ Seq [] *)
| Try of strat (* ≜ If (S, S, Empty): pick one normal form a the given strategy; return input if nf *)
| Rules of Ast.node_ident (* ≜ Alt (rules defined in the top level of the package with the given name *)
type decl =
| Features of Ast.feature_spec list
......
......@@ -324,7 +324,7 @@ module Grs = struct
let modul =
try List.find (fun m -> m.Modul.name=name) grs.modules
with Not_found -> Error.build "No module or strategy named '%s'" name in
Rule.conf_one_step ?domain: grs.domain name inst modul.Modul.rules
Rule.conf_one_step ?domain: grs.domain inst modul.Modul.rules
end
(* Union of strategies *)
| Ast.Plus [] -> None (* the list can be empty in a recursive call! *)
......@@ -378,7 +378,7 @@ module Grs = struct
let modul =
try List.find (fun m -> m.Modul.name=name) grs.modules
with Not_found -> Error.build "No module or strategy named '%s'" name in
Rule.one_step ?domain: grs.domain name inst modul.Modul.rules
Rule.one_step ?domain: grs.domain inst modul.Modul.rules
end
(* Union of strategies *)
| Ast.Plus strat_list ->
......@@ -514,7 +514,7 @@ module Grs = struct
begin
printf "%s one_step (module=%s)...%!" (String.make (2 * (max 0 !indent)) ' ') modul.Modul.name;
let domain = get_domain grs in
match Instance_set.elements (Rule.one_step ?domain modul.Modul.name instance modul.Modul.rules) with
match Instance_set.elements (Rule.one_step ?domain instance modul.Modul.rules) with
| [] -> printf "0\n%!"; let res = Libgrew_types.Empty in decr indent; res
| instance_list -> printf "%d\n%!" (List.length instance_list);
Libgrew_types.Node
......@@ -589,6 +589,28 @@ module Grs = struct
end (* module Grs *)
module New_grs = struct
type decl =
......@@ -596,6 +618,7 @@ module New_grs = struct
| Strategy of string * New_ast.strat
| Package of string * decl list
type t = {
filename: string;
domain: Domain.t option;
......@@ -668,4 +691,191 @@ module New_grs = struct
domain;
decls;
}
(* The type [pointed] is a zipper style data structure for resolving names x.y.z *)
type pointed =
| Top of decl list
| Pack of (decl list * pointed) (* (content, mother package) *)
let top grs = Top grs.decls
let decl_list = function
| Top dl -> dl
| Pack (dl, _) -> dl
let down pointed name =
let rec loop = function
| [] -> None
| Package (n,dl) :: _ when n=name -> Some (Pack (dl, pointed))
| _::t -> loop t in
loop (decl_list pointed)
(* search for a decl named [name] defined in the working directory [wd] in [grs] *)
let rec search_at pointed path = match path with
| [] -> None
| [one] ->
(
try
let item = List.find (* ?? rule and strategy with the same name ?? *)
(function
| Strategy (s,_) when s=one -> true
| Rule r when Rule.get_name r = one -> true
| Package (p,_) when p=one -> true
| _ -> false
) (decl_list pointed) in
Some (item, pointed)
with Not_found -> None
)
| head::tail ->
match down pointed head with
| None -> None
| Some new_p -> search_at new_p tail
(* search for the path in current location and recursively on mother structure *)
let rec search_from pointed path =
match search_at pointed path with
| Some r_or_s -> Some r_or_s
| None ->
(match pointed with
| Top _ -> None
| Pack (_,mother) -> search_from mother path
)
let rec intern_simple_rewrite pointed strat_name instance =
let path = Str.split (Str.regexp "\\.") strat_name in
match search_from pointed path with
| None -> Error.build "Simple rewrite, cannot find strat %s" strat_name
| Some (Rule r,_) -> Rule.apply r instance
| Some (Package (_, decl_list), _) -> pack_rewrite decl_list instance
| Some (Strategy (_,ast_strat), new_pointed) ->
strat_simple_rewrite new_pointed ast_strat instance
and det_intern_simple_rewrite pointed strat_name instance =
let path = Str.split (Str.regexp "\\.") strat_name in
match search_from pointed path with
| None -> Error.build "Simple rewrite, cannot find strat %s" strat_name
| Some (Rule r,_) -> Rule.det_apply r instance
| Some (Package (_, decl_list), _) -> det_pack_rewrite decl_list instance
| Some (Strategy (_,ast_strat), new_pointed) ->
det_strat_simple_rewrite new_pointed ast_strat instance
and pack_rewrite decl_list instance =
List.fold_left
(fun acc decl ->
match decl with
| Rule r -> Instance_set.union acc (Rule.apply r instance)
| _ -> acc
) Instance_set.empty decl_list
and det_pack_rewrite decl_list instance =
let rec loop = function
| [] -> None
| Rule r :: tail_decl ->
(match Rule.det_apply r instance with
| None -> loop tail_decl
| Some x -> Some x
)
| _ :: tail_decl -> loop tail_decl in
loop decl_list
and strat_simple_rewrite pointed strat instance =
match strat with
| New_ast.Ref subname -> intern_simple_rewrite pointed subname instance
| New_ast.Pick strat ->
begin
match det_strat_simple_rewrite pointed strat instance with
| None -> Grew_rule.Instance_set.empty
| Some x -> Instance_set.singleton x
end
| New_ast.Alt [] -> Grew_rule.Instance_set.empty
| New_ast.Alt strat_list -> List.fold_left
(fun acc strat -> Instance_set.union acc (strat_simple_rewrite pointed strat instance)
) Instance_set.empty strat_list
| New_ast.Seq [] -> Instance_set.singleton instance
| New_ast.Seq (head_strat :: tail_strat) ->
let first_strat = strat_simple_rewrite pointed head_strat instance in
Instance_set.fold
(fun instance acc -> Instance_set.union acc (strat_simple_rewrite pointed (New_ast.Seq tail_strat) instance)
) first_strat Instance_set.empty
| New_ast.Iter strat ->
let one_step = strat_simple_rewrite pointed strat instance in
if Instance_set.is_empty one_step
then Instance_set.singleton instance
else Instance_set.fold
(fun instance acc -> Instance_set.union acc (strat_simple_rewrite pointed (New_ast.Iter strat) instance)
) one_step Instance_set.empty
| New_ast.Try strat ->
begin
let one_step = strat_simple_rewrite pointed strat instance in
if Instance_set.is_empty one_step
then Instance_set.singleton instance
else one_step
end
| New_ast.If (s, s1, s2) ->
begin
match det_strat_simple_rewrite pointed s instance with
| None -> strat_simple_rewrite pointed s1 instance
| Some _ -> strat_simple_rewrite pointed s2 instance
end
and det_strat_simple_rewrite pointed strat instance =
match strat with
| New_ast.Ref subname -> det_intern_simple_rewrite pointed subname instance
| New_ast.Pick strat -> det_strat_simple_rewrite pointed strat instance
| New_ast.Alt [] -> None
| New_ast.Alt strat_list ->
let rec loop = function
| [] -> None
| head_strat :: tail_strat ->
match det_strat_simple_rewrite pointed head_strat instance with
| None -> loop tail_strat
| Some x -> Some x in
loop strat_list
| New_ast.Seq [] -> Some instance
| New_ast.Seq (head_strat :: tail_strat) ->
begin
match det_strat_simple_rewrite pointed head_strat instance with
| None -> None
| Some inst -> det_strat_simple_rewrite pointed (New_ast.Seq tail_strat) inst
end
| New_ast.Iter strat ->
begin
match det_strat_simple_rewrite pointed strat instance with
| None -> Some instance
| Some inst -> det_strat_simple_rewrite pointed (New_ast.Iter strat) inst
end
| New_ast.Try strat ->
begin
match det_strat_simple_rewrite pointed strat instance with
| None -> Some instance
| Some i -> Some i
end
| New_ast.If (s, s1, s2) ->
begin
match det_strat_simple_rewrite pointed s instance with
| None -> det_strat_simple_rewrite pointed s1 instance
| Some _ -> det_strat_simple_rewrite pointed s2 instance
end
let simple_rewrite grs name graph =
let instance = Instance.from_graph graph in
let set = intern_simple_rewrite (top grs) name instance in
List.map
(fun inst -> inst.Instance.graph)
(Instance_set.elements set)
end
......@@ -121,4 +121,6 @@ module New_grs : sig
val dump: t -> unit
val domain: t -> Domain.t option
val simple_rewrite: t -> string -> G_graph.t -> G_graph.t list
end
\ No newline at end of file
......@@ -188,9 +188,9 @@ and standard target = parse
| "Seq" { SEQ }
| "Iter" { ITER }
| "If" { IF }
| "Empty" { EMPTY }
| "Try" { TRY }
| "Rules" { RULES }
| "Emty" { EMPTY }
| "Onf" { ONF }
| "graph" { GRAPH }
......
......@@ -101,9 +101,9 @@ let localize t = (t,get_loc ())
%token SEQ /* Seq */
%token ITER /* Iter */
%token IF /* If */
%token ONF /* Onf */
%token EMPTY /* Empty */
%token TRY /* Try */
%token RULES /* Rules */
%token <string> DOLLAR_ID /* $id */
%token <string> AROBAS_ID /* @id */
......@@ -769,7 +769,7 @@ strat_desc:
| SEQ LPAREN sl=separated_list_final_opt(COMA,strat_desc) RPAREN { New_ast.Seq sl }
| ITER LPAREN s=strat_desc RPAREN { New_ast.Iter s }
| IF LPAREN s1=strat_desc COMA s2=strat_desc COMA s3=strat_desc RPAREN { New_ast.If (s1,s2,s3) }
| EMPTY { New_ast.Empty }
| TRY LPAREN s=strat_desc RPAREN { New_ast.Try s }
| RULES LPAREN id=node_id RPAREN { New_ast.Rules id }
| ONF LPAREN s=strat_desc RPAREN { New_ast.Pick (New_ast.Iter s) }
| EMPTY { New_ast.Seq [] }
%%
......@@ -1064,7 +1064,7 @@ module Rule = struct
(* ---------------------------------------------------------------------- *)
(** [apply_rule instance matching rule] returns a new instance after the application of the rule *)
let apply_rule ?domain modul_name instance matching rule =
let apply_rule ?domain instance matching rule =
(* Timeout check *)
(try Timeout.check () with Timeout.Stop -> Error.run "Time out");
......@@ -1155,37 +1155,41 @@ module Rule = struct
List.map fst filtered_matching_list
(* ---------------------------------------------------------------------- *)
(** [one_step ?domain modul_name instance rules] computes the list of one-step reduct with rules *)
let one_step ?domain modul_name instance rules =
(** [one_step ?domain instance rules] computes the list of one-step reduct with rules *)
let one_step ?domain instance rules =
(* limit the rewriting depth to avoid looping rewriting *)
if List.length instance.Instance.rules >= !max_depth_non_det
then
if !debug_loop
then Instance_set.empty
else Error.run "[Module %s] max depth %d reached, last rules applied: …, %s"
modul_name !max_depth_non_det (List_.rev_to_string (fun x->x) ", " (List_.cut 5 instance.Instance.rules))
else Error.run "max depth %d reached, last rules applied: …, %s"
!max_depth_non_det (List_.rev_to_string (fun x->x) ", " (List_.cut 5 instance.Instance.rules))
else
List.fold_left
(fun acc rule ->
let matching_list = match_in_graph ?domain ?param:rule.param rule.pattern instance.Instance.graph in
List.fold_left
(fun acc1 matching ->
Instance_set.add (apply_rule ?domain modul_name instance matching rule) acc1
Instance_set.add (apply_rule ?domain instance matching rule) acc1
) acc matching_list
) Instance_set.empty rules
(* ---------------------------------------------------------------------- *)
(** [conf_one_step ?domain modul_name instance rules] computes one Some (one-step reduct) with rules, None if no rule apply *)
let rec conf_one_step ?domain modul_name (instance : Instance.t) rules =
let rec conf_one_step ?domain (instance : Instance.t) rules =
(* limit the rewriting depth to avoid looping rewriting *)
if List.length instance.Instance.rules >= !max_depth_det
then
if !debug_loop
then None
else Error.run "[Module %s] max depth %d reached, last rules applied: …, %s"
modul_name !max_depth_det (List_.rev_to_string (fun x->x) ", " (List_.cut 5 instance.Instance.rules))
else Error.run "max depth %d reached, last rules applied: …, %s"
!max_depth_det (List_.rev_to_string (fun x->x) ", " (List_.cut 5 instance.Instance.rules))
else
match rules with
| [] -> None
......@@ -1208,8 +1212,8 @@ module Rule = struct
fulfill ?domain (pos.graph,neg.graph) instance.Instance.graph new_partial_matching
) negs
) matching_list in
Some (apply_rule ?domain modul_name instance first_matching_where_all_witout_are_fulfilled rule)
with Not_found -> (* try another rule *) conf_one_step ?domain modul_name instance rule_tail
Some (apply_rule ?domain instance first_matching_where_all_witout_are_fulfilled rule)
with Not_found -> (* try another rule *) conf_one_step ?domain instance rule_tail
(* ---------------------------------------------------------------------- *)
(** filter nfs being equal *)
......@@ -1233,7 +1237,7 @@ module Rule = struct
let (new_to_do_set,new_nf_set) =
Instance_set.fold
(fun v (to_do_set_acc,nf_set_acc) ->
match Instance_set.elements (one_step ?domain modul_name v rules) with
match Instance_set.elements (one_step ?domain v rules) with
| [] -> (to_do_set_acc,Instance_set.add (Instance.rev_steps v) nf_set_acc)
| step_of_v -> (List.fold_left (fun acc v1 -> Instance_set.add v1 acc) to_do_set_acc step_of_v, nf_set_acc)
)
......@@ -1250,14 +1254,67 @@ module Rule = struct
reduced_nfs
(* ---------------------------------------------------------------------- *)
let rec conf_normalize ?domain modul_name instance rules =
match conf_one_step ?domain modul_name instance rules with
| Some new_instance -> conf_normalize ?domain modul_name new_instance rules
let rec conf_normalize ?domain instance rules =
match conf_one_step ?domain instance rules with
| Some new_instance -> conf_normalize ?domain new_instance rules
| None -> Instance.rev_steps instance
(* ---------------------------------------------------------------------- *)
let normalize ?domain modul_name ?(deterministic=false) rules instance =
if deterministic
then Instance_set.singleton (conf_normalize ?domain modul_name instance rules)
then Instance_set.singleton (conf_normalize ?domain instance rules)
else normalize_instance ?domain modul_name instance rules
let apply ?domain rule instance =
(* limit the rewriting depth to avoid looping rewriting *)
if List.length instance.Instance.rules >= !max_depth_non_det
then
if !debug_loop
then Instance_set.empty
else Error.run "max depth %d reached, last rules applied: …, %s"
!max_depth_non_det (List_.rev_to_string (fun x->x) ", " (List_.cut 5 instance.Instance.rules))
else
let matching_list = match_in_graph ?domain ?param:rule.param rule.pattern instance.Instance.graph in
List.fold_left
(fun acc matching ->
Instance_set.add (apply_rule ?domain instance matching rule) acc
) Instance_set.empty matching_list
let rec det_apply ?domain rule instance =
(* limit the rewriting depth to avoid looping rewriting *)
if List.length instance.Instance.rules >= !max_depth_det
then
if !debug_loop
then None
else Error.run "max depth %d reached, last rules applied: …, %s"
!max_depth_det (List_.rev_to_string (fun x->x) ", " (List_.cut 5 instance.Instance.rules))
else
let (pos,negs) = rule.pattern in
(* get the list of partial matching for positive part of the pattern *)
let matching_list =
extend_matching
?domain
(pos.graph,P_graph.empty)
instance.Instance.graph
(init rule.param pos) in
try
let (first_matching_where_all_witout_are_fulfilled,_) =
List.find
(fun (sub, already_matched_gids) ->
List.for_all
(fun neg ->
let new_partial_matching = update_partial pos.graph neg (sub, already_matched_gids) in
fulfill ?domain (pos.graph,neg.graph) instance.Instance.graph new_partial_matching
) negs
) matching_list in
Some (apply_rule ?domain instance first_matching_where_all_witout_are_fulfilled rule)
with Not_found -> None
end (* module Rule *)
......@@ -94,8 +94,8 @@ module Rule : sig
Instance.t ->
Instance_set.t
val one_step: ?domain: Domain.t -> string -> Instance.t -> t list -> Instance_set.t
val conf_one_step: ?domain: Domain.t -> string -> Instance.t -> t list -> Instance.t option
val one_step: ?domain: Domain.t -> Instance.t -> t list -> Instance_set.t
val conf_one_step: ?domain: Domain.t -> Instance.t -> t list -> Instance.t option
(** the type matching encodes the graph morphism from a pattern to a graph *)
(* NB: it was made public for the grep mode *)
......@@ -117,4 +117,14 @@ module Rule : sig
(** [match_deco rule matching] builds the decoration of the [graph] illustrating the given [matching] of the [rule] *)
(* NB: it can be computed independly from the graph itself! *)
val match_deco: pattern -> matching -> G_deco.t
val apply: ?domain: Domain.t -> t -> Instance.t -> Instance_set.t
val det_apply: ?domain: Domain.t -> t -> Instance.t -> Instance.t option
end (* module Rule *)
......@@ -321,6 +321,10 @@ module Rewrite = struct
let simple_rewrite ~gr ~grs ~strat =
handle ~name:"Rewrite.simple_rewrite" (fun () -> Grew_grs.Grs.simple_rewrite grs strat gr) ()
let new_simple_rewrite ~gr ~grs ~strat =
handle ~name:"Rewrite.new_simple_rewrite" (fun () -> Grew_grs.New_grs.simple_rewrite grs strat gr) ()
let is_empty rh =
handle ~name:"Rewrite.is_empty" (fun () -> Grew_grs.Rewrite_history.is_empty rh) ()
......
......@@ -165,6 +165,7 @@ module Rewrite: sig
val rewrite: gr:Graph.t -> grs:Grs.t -> seq:string -> history
val simple_rewrite: gr:Graph.t -> grs:Grs.t -> strat:string -> Graph.t list
val new_simple_rewrite: gr:Graph.t -> grs:New_grs.t -> strat:string -> Graph.t list
val is_empty: history -> bool
......
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