Commit b06c5792 authored by Bruno Guillaume's avatar Bruno Guillaume

rew_display and new history

parent 88095ac7
...@@ -973,6 +973,14 @@ module Grs = struct ...@@ -973,6 +973,14 @@ module Grs = struct
(* ============================================================================================= *) (* ============================================================================================= *)
(* ============================================================================================= *) (* ============================================================================================= *)
(* ============================================================================================= *)
(* Rewriting in the deterministic case with graph type *)
(* ============================================================================================= *)
(* apply a package to an instance = apply only top level rules in the package *)
let onf_pack_rewrite ?domain decl_list graph = let onf_pack_rewrite ?domain decl_list graph =
let rec loop = function let rec loop = function
| [] -> None | [] -> None
...@@ -1037,12 +1045,12 @@ module Grs = struct ...@@ -1037,12 +1045,12 @@ module Grs = struct
| Some _ -> onf_strat_simple_rewrite ?domain pointed s2 graph | Some _ -> onf_strat_simple_rewrite ?domain pointed s2 graph
end end
| New_ast.Onf (s) -> onf_strat_simple_rewrite ?domain pointed s graph | New_ast.Onf (s) -> onf_strat_simple_rewrite ?domain pointed s graph (* TODO check Onf (P) == 1 rule app ? *)
(* ============================================================================================= *)
(* Rewriting in the non-deterministic case with Graph_with_history.t type *)
(* ============================================================================================= *)
(* non deterministic case *)
(* apply a package to an instance = apply only top level rules in the package *) (* apply a package to an instance = apply only top level rules in the package *)
let gwh_pack_rewrite ?domain decl_list gwh = let gwh_pack_rewrite ?domain decl_list gwh =
List.fold_left List.fold_left
...@@ -1148,6 +1156,119 @@ module Grs = struct ...@@ -1148,6 +1156,119 @@ module Grs = struct
(Graph_with_history_set.elements set) (Graph_with_history_set.elements set)
(* ============================================================================================= *)
(* production of rew_display of linear rewriting history for GUI *)
(* ============================================================================================= *)
type linear_rd = {
graph: G_graph.t;
steps: (string * G_graph.t * Libgrew_types.big_step) list;
}
let wrd_pack_rewrite ?domain decl_list graph_with_big_step =
let rec loop = function
| [] -> None
| Rule r :: tail_decl ->
(match Rule.wrd_apply ?domain r graph_with_big_step with
| Some x -> Some x
| None -> loop tail_decl
)
| _ :: tail_decl -> loop tail_decl in
loop decl_list
let rec wrd_pack_iter_rewrite ?domain decl_list graph_with_big_step =
match (graph_with_big_step, wrd_pack_rewrite ?domain decl_list graph_with_big_step) with
| (_, Some (new_gr, new_bs)) -> wrd_pack_iter_rewrite ?domain decl_list (new_gr, Some new_bs)
| ((gr, Some bs), None) -> Some (gr, bs)
| ((gr, None), None) -> None
(* functions [wrd_intern_simple_rewrite] and [wrd_strat_simple_rewrite] computes
one normal form and output the data needed for rew_display production.
output = list of ... tranformed later into rew_display by [build_rew_display_from_linear_rd]
[iter_flag] is set to true when rules application should be put together (in the old modules style).
*)
let rec wrd_intern_simple_rewrite ?domain iter_flag pointed strat_name linear_rd =
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,_) ->
begin
match Rule.wrd_apply ?domain r (linear_rd.graph, None) with
| None -> None
| Some (new_graph, big_step) -> Some {steps = (Rule.get_name r, linear_rd.graph, big_step) :: linear_rd.steps; graph = new_graph}
end
| Some (Package (name, decl_list), _) when iter_flag ->
begin
match wrd_pack_iter_rewrite ?domain decl_list (linear_rd.graph, None) with
| None -> None
| Some (new_graph, big_step) -> Some {steps = (name, linear_rd.graph, big_step) :: linear_rd.steps; graph = new_graph}
end
| Some (Package (name, decl_list), _) ->
begin
match wrd_pack_rewrite ?domain decl_list (linear_rd.graph, None) with
| None -> None
| Some (new_graph, big_step) -> Some {steps = (name, linear_rd.graph, big_step) :: linear_rd.steps; graph = new_graph}
end
| Some (Strategy (_,ast_strat), new_pointed) ->
wrd_strat_simple_rewrite ?domain iter_flag new_pointed ast_strat linear_rd
and wrd_strat_simple_rewrite ?domain iter_flag pointed strat linear_rd =
match strat with
| New_ast.Ref subname -> wrd_intern_simple_rewrite iter_flag ?domain pointed subname linear_rd
| New_ast.Pick strat -> wrd_strat_simple_rewrite iter_flag ?domain pointed strat linear_rd
| New_ast.Alt [] -> None
| New_ast.Alt strat_list ->
let rec loop = function
| [] -> None
| head_strat :: tail_strat ->
match wrd_strat_simple_rewrite ?domain false pointed head_strat linear_rd with
| None -> loop tail_strat
| Some x -> Some x in
loop strat_list
| New_ast.Seq [] -> Some linear_rd
| New_ast.Seq (head_strat :: tail_strat) ->
begin
match wrd_strat_simple_rewrite ?domain false pointed head_strat linear_rd with
| None -> None
| Some gwrd -> wrd_strat_simple_rewrite iter_flag ?domain pointed (New_ast.Seq tail_strat) gwrd
end
| New_ast.Iter sub_strat
| New_ast.Onf sub_strat ->
begin
match wrd_strat_simple_rewrite ?domain true pointed sub_strat linear_rd with
| None -> Some linear_rd
| Some gwrd -> wrd_strat_simple_rewrite ?domain iter_flag pointed strat gwrd
end
| New_ast.Try sub_strat ->
begin
match wrd_strat_simple_rewrite ?domain false pointed sub_strat linear_rd with
| None -> Some linear_rd
| Some i -> Some i
end
| New_ast.If (s, s1, s2) ->
begin
match onf_strat_simple_rewrite ?domain pointed s linear_rd.graph with
| None -> wrd_strat_simple_rewrite iter_flag ?domain pointed s1 linear_rd
| Some _ -> wrd_strat_simple_rewrite iter_flag ?domain pointed s2 linear_rd
end
let build_rew_display_from_linear_rd linear_rd =
List.fold_left
(fun acc (n,g,bs) -> Libgrew_types.Node (g, n, [Libgrew_types.swap bs, acc])) (Libgrew_types.Leaf linear_rd.graph) linear_rd.steps
let wrd_rewrite grs strat graph =
let domain = domain grs in
let casted_graph = match domain with
| None -> graph
| Some dom -> G_graph.cast dom graph in
match wrd_strat_simple_rewrite ?domain false (top grs) (Parser.strategy strat) {graph=casted_graph; steps=[]} with
| None -> Libgrew_types.Leaf graph
| Some linear_rd -> build_rew_display_from_linear_rd linear_rd
end (* module Grs *) end (* module Grs *)
......
...@@ -116,5 +116,5 @@ module Grs : sig ...@@ -116,5 +116,5 @@ module Grs : sig
val at_most_one: t -> string -> bool val at_most_one: t -> string -> bool
val gwh_simple_rewrite: t -> string -> G_graph.t -> G_graph.t list val gwh_simple_rewrite: t -> string -> G_graph.t -> G_graph.t list
val wrd_rewrite: t -> string -> G_graph.t -> Libgrew_types.rew_display
end end
...@@ -1368,6 +1368,8 @@ module Rule = struct ...@@ -1368,6 +1368,8 @@ module Rule = struct
let onf_find cnode ?loc (matching, created_nodes) = let onf_find cnode ?loc (matching, created_nodes) =
match cnode with match cnode with
| Command.Pat pid -> | Command.Pat pid ->
...@@ -1537,6 +1539,48 @@ module Rule = struct ...@@ -1537,6 +1539,48 @@ module Rule = struct
let rec wrd_apply ?domain rule (graph, big_step_opt) =
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)
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) graph new_partial_matching
) negs
) matching_list in
let (new_graph, created_nodes, eff) =
List.fold_left
(fun (graph, created_nodes, eff) command ->
onf_apply_command eff ?domain command graph first_matching_where_all_witout_are_fulfilled created_nodes
)
(graph, [], false)
rule.commands in
let rule_app = {
Libgrew_types.rule_name = rule.name;
up = match_deco rule.pattern first_matching_where_all_witout_are_fulfilled;
down = down_deco (first_matching_where_all_witout_are_fulfilled,created_nodes) rule.commands
} in
let new_big_step = match big_step_opt with
| None -> {Libgrew_types.small_step = []; first=rule_app}
| Some {Libgrew_types.small_step; first} -> {Libgrew_types.small_step = (graph,rule_app) :: small_step; first} in
if eff
then Some (new_graph, new_big_step)
else None
with Not_found -> (* raised by List.find, no matching apply *) None
......
...@@ -122,6 +122,9 @@ module Rule : sig ...@@ -122,6 +122,9 @@ module Rule : sig
val det_apply: ?domain: Domain.t -> t -> Instance.t -> Instance.t option val det_apply: ?domain: Domain.t -> t -> Instance.t -> Instance.t option
val wrd_apply: ?domain: Domain.t -> t -> (G_graph.t * Libgrew_types.big_step option) -> (G_graph.t * Libgrew_types.big_step) option
val onf_apply: ?domain: Domain.t -> t -> G_graph.t -> G_graph.t option val onf_apply: ?domain: Domain.t -> t -> G_graph.t -> G_graph.t option
val gwh_apply: ?domain: Domain.t -> t -> Graph_with_history.t -> Graph_with_history_set.t val gwh_apply: ?domain: Domain.t -> t -> Graph_with_history.t -> Graph_with_history_set.t
......
...@@ -311,11 +311,14 @@ module Rewrite = struct ...@@ -311,11 +311,14 @@ module Rewrite = struct
let set_debug_loop () = Grew_rule.Rule.set_debug_loop () let set_debug_loop () = Grew_rule.Rule.set_debug_loop ()
let old_display ~gr ~grs ~seq = let old_old_display ~gr ~grs ~seq =
handle ~name:"Rewrite.old_display" (fun () -> Grew_grs.Old_grs.build_rew_display grs seq gr) () handle ~name:"Rewrite.old_old_display" (fun () -> Grew_grs.Old_grs.build_rew_display grs seq gr) ()
let old_display ~gr ~grs ~strat =
handle ~name:"Rewrite.old_display" (fun () -> Grew_grs.Grs.det_rew_display grs strat gr) ()
let display ~gr ~grs ~strat = let display ~gr ~grs ~strat =
handle ~name:"Rewrite.display" (fun () -> Grew_grs.Grs.det_rew_display grs strat gr) () handle ~name:"Rewrite.display" (fun () -> Grew_grs.Grs.wrd_rewrite grs strat gr) ()
let set_timeout t = Grew_base.Timeout.timeout := t let set_timeout t = Grew_base.Timeout.timeout := t
...@@ -326,7 +329,7 @@ module Rewrite = struct ...@@ -326,7 +329,7 @@ module Rewrite = struct
handle ~name:"Rewrite.old_simple_rewrite" (fun () -> Grew_grs.Old_grs.simple_rewrite grs strat gr) () handle ~name:"Rewrite.old_simple_rewrite" (fun () -> Grew_grs.Old_grs.simple_rewrite grs strat gr) ()
let simple_rewrite ~gr ~grs ~strat = let simple_rewrite ~gr ~grs ~strat =
handle ~name:"Rewrite.simple_rewrite" (fun () -> Grew_grs.Grs.simple_rewrite grs strat gr) () handle ~name:"Rewrite.simple_rewrite" (fun () -> Grew_grs.Grs.gwh_simple_rewrite grs strat gr) ()
let at_least_one ~grs ~strat = let at_least_one ~grs ~strat =
handle ~name:"Rewrite.at_least_one" (fun () -> Grew_grs.Grs.at_least_one grs strat) () handle ~name:"Rewrite.at_least_one" (fun () -> Grew_grs.Grs.at_least_one grs strat) ()
......
...@@ -166,6 +166,7 @@ module Rewrite: sig ...@@ -166,6 +166,7 @@ module Rewrite: sig
@param gr the grapth to rewrite @param gr the grapth to rewrite
@param grs the graph rewriting system @param grs the graph rewriting system
@param seq the name of the sequence to apply *) @param seq the name of the sequence to apply *)
val old_display: gr:Graph.t -> grs:Grs.t -> strat:string -> display
val display: gr:Graph.t -> grs:Grs.t -> strat:string -> display val display: gr:Graph.t -> grs:Grs.t -> strat:string -> display
val at_least_one: grs:Grs.t -> strat:string -> bool val at_least_one: grs:Grs.t -> strat:string -> 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