Commit d190881a authored by Frontull Samuel's avatar Frontull Samuel
Browse files

fixed big nested lambdas

parent 89d5e7cc
......@@ -13,14 +13,14 @@ let () =
in
let lterm = Core.term_to_l_term term 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
(* 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);
(* Printf.printf "redex @ %s\n" (Core.weak_redexpos lterm); *)
Printf.printf "===================\n\n";
Printf.printf "%s\n" (Core.trs_term_to_string tterm);
(* Printf.printf "redex @ %s\n" (Core.redexpos tterm); *)
Printf.printf "===================\n\n"; *)
(* Printf.printf "%s\n" (Core.trs_term_to_string tterm); *)
(* Printf.printf "redex @ %s\n" (Core.redexpos tterm);
Printf.printf "---------------------------------\n%s\n\n"
(Core.rules_to_string (Core.rules lterm));
Printf.printf "%s\n" (Core.trs_term_to_string (Core.trs_term trs'));
......
......@@ -8,8 +8,7 @@ let rec _term_to_string term =
| Lam (v, t) -> (
match t with
| Lam (v2, t2) -> _term_to_string (Lam (v ^ " " ^ v2, t2))
| _ -> "λ" ^ v ^ "." ^ _term_to_string t
)
| _ -> "λ" ^ v ^ "." ^ _term_to_string t )
| App (e1, e2) -> (
match (e1, e2) with
| Var _, Var _ -> _term_to_string e1 ^ " " ^ _term_to_string e2
......@@ -185,6 +184,8 @@ type trs_term =
(** Extract the name of a variable from a {e a_term} *)
let vtname = function TVar n -> n | _ -> ""
let isvar = function TVar _ -> true | _ -> false
let rec trs_term_to_string term =
match term with
| TVar v -> v
......@@ -228,10 +229,16 @@ let rec _components_trsterm x pos trsterm =
_components_trsterm x (pos ^ "1") e1
@ _components_trsterm x (pos ^ "2") e2
| TCon (_, fvs) ->
if fvs = [] then [ (trsterm, pos) ]
let fvs_f = L.filter (fun x -> (isvar (fst x))) fvs in
if fvs_f = [] then [ (trsterm, pos) ]
else
L.flatten
(L.map (fun y -> _components_trsterm x ("1" ^ snd y) (fst y)) fvs)
(* [ (TCon (l, L.flatten (L.map
(fun y -> _components_trsterm x (snd y) (fst y))
fvs)), pos) ] *)
L.flatten
(L.map
(fun y -> _components_trsterm x ("1" ^ snd y) (fst y))
fvs)
let components_trsterm x trsterm = _components_trsterm x "e" trsterm
......@@ -257,7 +264,7 @@ let rec _components_lterm xs pos lterm =
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
......@@ -267,7 +274,11 @@ let rec trs_term_to_string_nopos term =
| TDes (e1, e2) -> (
match (e1, e2) with
| TDes _, TDes _ ->
"(" ^ trs_term_to_string_nopos e1 ^ ") (" ^ trs_term_to_string_nopos e2 ^ ")"
"("
^ trs_term_to_string_nopos e1
^ ") ("
^ trs_term_to_string_nopos e2
^ ")"
| TDes _, _ ->
"(" ^ trs_term_to_string_nopos e1 ^ ") " ^ trs_term_to_string_nopos e2
| _, TDes _ ->
......@@ -343,9 +354,11 @@ let rec subst m pairs =
let rec rewrite trsrules trsterm =
(* Printf.printf "Rewrite: %s\n" (trs_term_to_string trsterm); *)
match (trsrules, trsterm) with
| RR (TDes (TCon (l, fvs), TVar x), r) :: xs, TDes (TCon (l2, fvs2), arg) ->
| RR (TDes (TCon (l, fvs), TVar x), r) :: xs,
TDes (TCon (l2, fvs2), arg) ->
if l = l2 then
subst r ((TVar x, arg) :: L.combine (L.map fst fvs) (L.map fst fvs2))
subst r ((TVar x, arg) ::
L.combine (L.map fst fvs) (L.map fst fvs2))
else rewrite xs trsterm
| [], _ -> trsterm
| _, _ -> failwith "Not a rule or not a trsterm."
......@@ -388,7 +401,13 @@ let next_fresh_2 () =
counter_projection := !counter_projection + 1;
"v" ^ string_of_int !counter_projection
let trs_to_string trs =
match trs with
| TRS (xs, t) ->
"TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string t
let rec trs_to_term trs =
(* Printf.printf "trstoterm: %s\n\n" (trs_to_string trs); *)
match trs with
| TRS (xs, t) -> (
match t with
......@@ -425,11 +444,6 @@ let rec trs_to_term trs =
)) )
| _ -> failwith "Not a RR found." ) )
let trs_to_string trs =
match trs with
| TRS (xs, 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
if wt = term then [] else wt :: _weak_reduction wt
......@@ -470,27 +484,32 @@ let rec _simulate_lterm_in_trs lterm trs =
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"
let str = ( "+++++ 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"
^ "\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')
^ "\n\nalpha_eq: " ^ Bool.to_string alpha_eq ) in
str :: (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
(trs_to_string trs) ^ "\n\n" ^ (String.concat "\n\n" (_simulate_lterm_in_trs lterm trs))
trs_to_string trs ^ "\n\n"
^ _term_to_string (l_term_to_term (trs_to_term trs))
^ "\n"
^ String.concat "\n\n" (_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 *)
(* Printf.printf
"\n%s\n\n++++++++++++++++\n++++++++++++++++\n++++++++++++++++\n\n%s\n" *)
Printf.printf
"\n%s\n" sim
(* (String.concat "\n\n========================\n\n" sim2) *)
"\n%s\n\n++++++++++++++++\n++++++++++++++++\n++++++++++++++++\n\n%s\n" *)
Printf.printf "\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