Commit 105bc80b authored by Frontull Samuel's avatar Frontull Samuel
Browse files

only create rules once

parent 913918a6
......@@ -463,9 +463,8 @@ let rec simulate_trs_in_lterm trs =
| v
lterm ...... -> ...... lterm'
*)
let rec simulate_lterm_in_trs lterm =
let rec _simulate_lterm_in_trs lterm trs =
let pos = weak_redexpos lterm in
let trs = l_term_to_trs lterm in
let lterm' = weak_step_pos lterm pos in
let trs' = rstep_pos trs pos in
let trs'_lterm = trs_to_term trs' in
......@@ -479,12 +478,18 @@ let rec simulate_lterm_in_trs lterm =
^ "\nlterm' : "
^ _term_to_string (l_term_to_term lterm')
^ "\n\nalpha_eq: " ^ Bool.to_string alpha_eq )
:: (if lterm = lterm' then [] else simulate_lterm_in_trs lterm')
:: (if lterm = lterm' then [] else _simulate_lterm_in_trs lterm' trs')
let simulate_lterm_in_trs lterm =
let trs = l_term_to_trs lterm in
_simulate_lterm_in_trs lterm trs
let print_simulation lterm =
let sim = simulate_lterm_in_trs lterm in
let sim2 = simulate_trs_in_lterm (l_term_to_trs lterm) in
(* let sim2 = simulate_trs_in_lterm (l_term_to_trs lterm) in *)
(* Printf.printf
"\n%s\n\n++++++++++++++++\n++++++++++++++++\n++++++++++++++++\n\n%s\n" *)
Printf.printf
"\n%s\n\n++++++++++++++++\n++++++++++++++++\n++++++++++++++++\n\n%s\n"
"\n%s\n"
(String.concat "\n\n========================\n\n" sim)
(String.concat "\n\n========================\n\n" sim2)
(* (String.concat "\n\n========================\n\n" sim2) *)
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