Commit 1b24bfb1 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

removed reduction print

parent 069fd75d
......@@ -11,6 +11,5 @@ let () =
let term =
try str_to_term (Sys.argv.(1) ^ "\n") with _ -> failwith "Syntax error"
in
(* Core.reduction_print term *)
let lterm = Core.term_to_l_term term in
Core.print_simulation lterm
......@@ -374,67 +374,3 @@ let print_simulation lterm =
Printf.printf "%s\n\n++++++++++++++++\n++++++++++++++++\n++++++++++++++++\n\n%s\n"
(String.concat "\n\n========================\n\n" sim)
(String.concat "\n\n========================\n\n" sim2)
let prepend_index xs = L.mapi (fun i x -> "[" ^ string_of_int i ^ "] " ^ x) xs
let reduction_print term =
let l_term = term_to_l_term term in
let trs = l_term_to_trs l_term in
let weak_reductions = weak_reduction l_term in
let trs_reductions = trs_reduction trs in
let trs_reductions_t = L.map trs_term trs_reductions in
let bisim = L.combine weak_reductions trs_reductions in
let trs_str =
match trs with
| TRS (xs, t) ->
"Rules:\n" ^ rules_to_string xs ^ ".\n\nTerm:\n" ^ trs_term_to_string t
in
Printf.printf
"\n\
%s\n\n\
-------[TRS]----------------\n\n\
%s\n\n\
-------[Reductions]---------\n\n\
LC:\n\
\ %s\n\n\
TRS:\n\
\ %s\n\n\
-------[Bisimulation]-------\n\n\
%s\n"
(l_term_to_string (trs_to_term trs))
trs_str
(String.concat " ->\n "
(prepend_index
(L.map _term_to_string (L.map l_term_to_term weak_reductions))))
(String.concat " ->\n "
(prepend_index (L.map trs_term_to_string trs_reductions_t)))
(String.concat "\n"
(L.mapi
(fun i (a_term, b_trs) ->
let a_term_default = a_term in
let a_term_trs = l_term_to_trs a_term_default in
let b_trs_term = trs_to_term b_trs in
(* let b_term_trs = l_term_to_trs b_trs_term in *)
let s =
if
l_term_to_string (default_names a_term)
= l_term_to_string (default_names b_trs_term)
&& trs_term a_term_trs = trs_term b_trs
then
"\n---------------------\n" ^ "TRS_" ^ string_of_int i ^ " ~ "
^ "LC_" ^ string_of_int i ^ "\n---------------------\n"
else
"\n---------------------\n" ^ "! TRS_" ^ string_of_int i
^ " ≁ " ^ "LC_" ^ string_of_int i
^ "\n---------------------\n"
in
s
^ l_term_to_string a_term_default
^ "\n\n" ^ trs_to_string a_term_trs
^ "\n\n++++++++++++++++++++++\n\n" ^ trs_to_string b_trs ^ "\n\n"
^ l_term_to_string b_trs_term
^ "\n\n"
(* ^ trs_to_string b_term_trs ^ "\n\n" *)
^ "=====================\n")
(* "LC_" ^ string_of_int i ^ " ~ " ^ "TRS_" ^ string_of_int i *)
bisim))
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