Commit 0f922eb8 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

legal paths limited and only approximated for dot

parent 7ab65e0c
......@@ -25,7 +25,7 @@ let () =
let vc_terminated = fst (fst scc_analysis) in
let closed_term = Core.a_term_to_string (Core.make_closed term) in
let reduction =
if vc_terminated then Core.sn_reduce_to_nf Core.casubst term
if false then Core.sn_reduce_to_nf Core.casubst term
else Core.reduce_to_nf term max_depth
in
let reduction_str = List.map Core.a_term_to_string reduction in
......
......@@ -479,7 +479,6 @@ let rec app_composition nodes appapp applam_list =
| [] -> [ Empty ]
let rec app_composition_2 nodes appapp_list applam =
(* Printf.printf "\app_composition: (%s)\n\n" ((wbp_tostring) p1); *)
match appapp_list with
| y :: ys ->
let body =
......@@ -487,7 +486,6 @@ let rec app_composition_2 nodes appapp_list applam =
(L.hd (get_node (node_pos (last_wbp applam) ^ "0") nodes))
in
let newpath = append_wbp (append_wbp y (wbp_tail applam)) body in
(* Printf.printf "APP_COMPOSITION 2\nAA: %s\nAL: %s\nRS: %s\n\n" (wbp_tostring y) (wbp_tostring applam) (wbp_tostring newpath); *)
newpath :: app_composition_2 nodes ys applam
| [] -> [ Empty ]
......@@ -543,12 +541,7 @@ let rec similar_redex wbp = function
|| similar_redex wbp xs
| [] -> false
let rec _well_balanced_paths newpaths acc nodes bedges n =
(* Printf.printf "newpaths (%d)\n" (L.length newpaths);
L.map (fun x -> Printf.printf "newpaths: (%s)\n" x) (L.map (wbp_tostring) newpaths); *)
(* Printf.printf "newpaths (%d)\n" (L.length newpaths);
Printf.printf "accpaths (%d)\n" (L.length acc); *)
(* Printf.printf "---------------------------------------[%d]------------------------------------------\n\n" n; *)
let rec _well_balanced_paths newpaths acc nodes bedges n approx =
if n <= 0 then (false, acc)
else
let paths = composition newpaths acc nodes bedges in
......@@ -557,15 +550,15 @@ let rec _well_balanced_paths newpaths acc nodes bedges n =
(fun x ->
(not (L.mem x acc))
&& (not (first_wbp x = last_wbp x))
&& not (similar_redex x acc))
&& (approx && not (similar_redex x acc)))
paths
in
let newacc = acc @ newpaths in
match newpaths with
| [] -> (true, acc)
| _ -> _well_balanced_paths newpaths newacc nodes bedges (n - 1)
| _ -> _well_balanced_paths newpaths newacc nodes bedges (n - 1) approx
let well_balanced_paths term =
let well_balanced_paths term max_compositions approx =
let nodes = term_nodes term in
let bedges = b_edges term in
let apps =
......@@ -584,114 +577,22 @@ let well_balanced_paths term =
| _ -> Empty)
apps
in
let max_compositions = 12 in
let compose = _well_balanced_paths acc acc nodes bedges max_compositions in
let compose = _well_balanced_paths acc acc nodes bedges max_compositions approx in
(* let applam = L.filter (fun p -> islam_node (last_wbp p)) (snd compose) in *)
(fst compose, snd compose)
let well_balanced_paths_al term =
let wbp = well_balanced_paths term in
let well_balanced_paths_al term max_compositions approx =
let wbp = well_balanced_paths term max_compositions approx in
let applam = L.filter (fun p -> islam_node (last_wbp p)) (snd wbp) in
(fst wbp, applam)
let legal_paths term =
let wbp = well_balanced_paths_al term in
let legal_paths term max_compositions approx =
let wbp = well_balanced_paths_al term max_compositions approx in
(* let wbp = L.filter is_legal wbp in *)
(fst wbp, L.map wbp_tolist (snd wbp))
let prepos pos = String.sub pos 0 (String.length pos - 1)
let rec _lazy_well_balanced_paths newpaths acc nodes bedges n =
if n <= 0 then (false, acc)
else
let apps =
L.filter
(fun x -> match x with pa, AS _, _ -> pa != "e" | _ -> false)
nodes
in
let activatedapps =
L.filter
(fun x -> not (wbp_isempty x))
(L.map
(fun x ->
match x with
| pa, AS s, typ ->
let ppa = prepos pa in
let pexists =
List.exists
(fun x -> x = ppa)
(List.map node_pos (List.map last_wbp acc))
in
let acc_acl =
L.filter (fun p -> islam_node (last_wbp p)) acc
in
let pexists2 =
List.exists
(fun x -> x = ppa)
(List.map node_pos (List.map first_wbp acc_acl))
in
if pexists || pexists2 then
Comp
[
Node (pa, AS s, typ);
posymtyp_to_node (L.hd (get_node (pa ^ "0") nodes));
]
else Empty
| _ -> Empty)
apps)
in
let newpaths = newpaths @ activatedapps in
let paths = composition newpaths acc nodes bedges in
let newpaths =
L.filter
(fun x -> (not (L.mem x acc)) && not (first_wbp x = last_wbp x))
paths
in
let newacc = acc @ newpaths in
match newpaths with
| [] -> (true, acc)
| _ -> _lazy_well_balanced_paths newpaths newacc nodes bedges (n - 1)
let lazy_well_balanced_paths term =
let nodes = term_nodes term in
let bedges = b_edges term in
let apps =
L.filter
(fun x -> match x with pa, AS _, _ -> pa = "e" | _ -> false)
nodes
in
let acc =
L.filter
(fun x -> not (wbp_isempty x))
(L.map
(fun x ->
match x with
| pa, AS s, typ -> (
let fp = posymtyp_to_node (L.hd (get_node (pa ^ "0") nodes)) in
match fp with
| Node (_, LS _, _) -> Comp [ Node (pa, AS s, typ); fp ]
| _ -> Empty )
| _ -> Empty)
apps)
in
let max_compositions = 10 in
let compose =
_lazy_well_balanced_paths acc acc nodes bedges max_compositions
in
(fst compose, snd compose)
let lazy_well_balanced_paths_al term =
let lazy_wbp = lazy_well_balanced_paths term in
let applam = L.filter (fun p -> islam_node (last_wbp p)) (snd lazy_wbp) in
(fst lazy_wbp, applam)
let lazy_legal_paths term =
let lazy_wbp = lazy_well_balanced_paths_al term in
(* let wbp = L.filter is_legal wbp in *)
(fst lazy_wbp, L.map wbp_tolist (snd lazy_wbp))
let is_scc nodes path =
let f = get_node (L.hd path) nodes in
let l = get_node (L.hd (L.rev path)) nodes in
......@@ -738,7 +639,7 @@ let harmless_scc sccpath be =
let scc tterm max_depth sim =
let ae = a_edges tterm in
let lp = legal_paths tterm in
let lp = legal_paths tterm max_depth false in
let re = snd lp in
let normalizing = fst lp in
let be = b_edges tterm in
......
......@@ -223,7 +223,7 @@ let term_ctx_to_dot ctx tterm reduction scc_paths name =
^ b_edges_to_dot name (b_edges tterm)
^ c_edges_to_dot name (c_edges tterm)
^ a_edges_to_dot name (a_edges tterm)
^ r_paths_to_dot name (snd (legal_paths tterm))
^ r_paths_to_dot name (snd (legal_paths tterm 12 true))
^ nodes_order name nodes ^ ctx_str ^ "} " ^ reduction_dot
^ "subgraph cluster_paths { color=invis "
^ scc_paths_to_dot scc_paths tterm nodes
......
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