Commit 069fd75d authored by Frontull Samuel's avatar Frontull Samuel
Browse files

print simulation

parent d352cbd8
......@@ -11,4 +11,6 @@ let () =
let term =
try str_to_term (Sys.argv.(1) ^ "\n") with _ -> failwith "Syntax error"
in
Core.reduction_print term
(* Core.reduction_print term *)
let lterm = Core.term_to_l_term term in
Core.print_simulation lterm
......@@ -313,10 +313,9 @@ let rec trs_to_term trs =
| _ -> failwith "Not a RR found." ) )
let trs_to_string trs =
(* Printf.printf "%s\n" (trs_term_to_string (trs_term trs)); *)
match trs with
| TRS (xs, t) ->
"Rules:\n" ^ rules_to_string xs ^ ".\n\nTerm:\n" ^ trs_term_to_string t
"TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string t
let rec _weak_reduction term =
let wt = weak_step term in
......@@ -330,6 +329,52 @@ let rec _trs_reduction trs =
let trs_reduction trs = trs :: _trs_reduction trs
let rec simulate_trs_in_lterm trs =
match trs with
| TRS (_, t) ->
let pos = redexpos t in
let trs' = rstep_pos trs pos in
if t = trs_term trs' then []
else
let lterm = trs_to_term trs in
let lterm' = weak_step_pos lterm pos in
let lterm'_trs = l_term_to_trs lterm' in
( trs_to_string trs ^ "\n\n"
^ l_term_to_string lterm ^ "\n-> " ^ l_term_to_string lterm' ^ "\n\n"
^ trs_to_string trs' ^ "\n\n" ^ trs_to_string lterm'_trs )
:: simulate_trs_in_lterm trs'
(*
trs ....... -> ...... trs'
^ |
| v
lterm ...... -> ...... lterm'
*)
let rec simulate_lterm_in_trs lterm =
let pos = weak_redexpos lterm in
let lterm' = weak_step_pos lterm pos in
if lterm = lterm' then []
else
let trs = l_term_to_trs lterm in
let trs' = rstep_pos trs pos in
let trs'_lterm = trs_to_term trs' in
let alpha_eq = default_names trs'_lterm = default_names lterm' in
( "lterm: " ^ l_term_to_string lterm ^ "\n\n"
^ trs_to_string trs ^ "\n-> "
^ trs_term_to_string (trs_term trs')
^ "\n\ntrs'_lterm: "
^ l_term_to_string trs'_lterm
^ "\nlterm' : " ^ l_term_to_string lterm' ^ "\n\nalpha_eq: "
^ Bool.to_string alpha_eq )
:: simulate_lterm_in_trs lterm'
let print_simulation lterm =
let sim = simulate_lterm_in_trs lterm in
let sim2 = simulate_trs_in_lterm (l_term_to_trs lterm) in
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 =
......
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