Commit 89d5e7cc authored by Frontull Samuel's avatar Frontull Samuel
Browse files

fixed bug, consider nested lambdas such that variables are not named afresh

parent 105bc80b
......@@ -12,8 +12,8 @@ let () =
try str_to_term (Sys.argv.(1) ^ "\n") with _ -> failwith "Syntax error"
in
let lterm = Core.term_to_l_term term in
(* let tterm = Core.l_term_to_trsterm lterm in
(* let tterm = Core.l_term_to_trsterm lterm in *)
(* Printf.printf "%s\n" (Core.l_term_to_string (Core.components_lterm "y" lterm));
let trs = Core.l_term_to_trs lterm in
let trs' = Core.rstep trs in
Printf.printf "%s\n" (Core._term_to_string term);
......
......@@ -244,20 +244,20 @@ let rec l_term_to_trsterm lterm =
let fvs_t = _components_trsterm x "1" e_t in
TCon (l, fvs_t)
let rec _components_lterm x pos lterm =
let rec _components_lterm xs pos lterm =
if free_variables lterm = [] then LVar ("v_" ^ pos)
else
match lterm with
| LVar y -> if y = x then lterm else LVar ("v_" ^ pos)
| LVar y -> if L.mem y xs then lterm else LVar ("v_" ^ pos)
| LApp (e1, e2) ->
let e1' = _components_lterm x (pos ^ "1") e1 in
let e2' = _components_lterm x (pos ^ "2") e2 in
let e1' = _components_lterm xs (pos ^ "1") e1 in
let e2' = _components_lterm xs (pos ^ "2") e2 in
LApp (e1', e2')
| LLam (l, fvs, y, e) ->
let e' = _components_lterm x (pos ^ "1") e in
let e' = _components_lterm (y :: xs) (pos ^ "1") e in
LLam (l, fvs, y, e')
let components_lterm x lterm = _components_lterm x "e" lterm
let components_lterm x lterm = _components_lterm [x] "e" lterm
type trs_rule = RR of trs_term * trs_term
......@@ -465,24 +465,26 @@ lterm ...... -> ...... lterm'
*)
let rec _simulate_lterm_in_trs lterm trs =
let pos = weak_redexpos 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
let alpha_eq = default_names trs'_lterm = default_names lterm' in
( "lterm: "
^ _term_to_string (l_term_to_term lterm)
^ "\nredex@" ^ pos ^ "\n" ^ trs_to_string trs ^ "\n->" ^ pos ^ "\n"
^ trs_term_to_string (trs_term trs')
^ "\n\ntrs'_lterm: "
^ _term_to_string (l_term_to_term 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' trs')
if pos <> "" then
let lterm' = weak_step_pos lterm pos 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
( "+++++ REDUCTION STEP @" ^ pos ^ " +++++\n\n"
^ _term_to_string (l_term_to_term lterm)
^ "\n->" ^ pos ^ "\n"
^ _term_to_string (l_term_to_term lterm')
^ "\n\n" ^ trs_term_to_string_nopos (trs_term trs) ^ "\n->" ^ pos ^ "\n"
^ trs_term_to_string_nopos (trs_term trs')
^ "\n\nprojection to lambda term:\n"
^ _term_to_string (l_term_to_term trs'_lterm)
^ "\n\nalpha_eq: " ^ Bool.to_string alpha_eq )
:: (if lterm = lterm' then [] else _simulate_lterm_in_trs lterm' trs')
else []
let simulate_lterm_in_trs lterm =
let trs = l_term_to_trs lterm in
_simulate_lterm_in_trs lterm trs
(trs_to_string trs) ^ "\n\n" ^ (String.concat "\n\n" (_simulate_lterm_in_trs lterm trs))
let print_simulation lterm =
let sim = simulate_lterm_in_trs lterm in
......@@ -490,6 +492,5 @@ let print_simulation lterm =
(* Printf.printf
"\n%s\n\n++++++++++++++++\n++++++++++++++++\n++++++++++++++++\n\n%s\n" *)
Printf.printf
"\n%s\n"
(String.concat "\n\n========================\n\n" sim)
"\n%s\n" sim
(* (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