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

no need for fresh labels

parent 2be21bef
......@@ -106,51 +106,6 @@ let next_fresh () =
counter := !counter + 1;
"p_" ^ string_of_int !counter
let rec replace_label lterm l n =
match lterm with
| LVar _ -> lterm
| LLam (lo, fvs, v, t) ->
let rt = replace_label t l n in
let fvst = L.map (fun fvt -> replace_label fvt l n) fvs in
if lo = l then LLam (n, fvst, v, replace_label rt l n)
else LLam (lo, fvst, v, replace_label rt l n)
| LApp (e1, e2) -> LApp (replace_label e1 l n, replace_label e2 l n)
let uniq_cons x xs = if List.mem x xs then xs else x :: xs
let remove_from_right xs = List.fold_right uniq_cons xs []
let rec _l_term_labels lterm =
match lterm with
| LVar _ -> []
| LLam (l, fvs, _, t) ->
(l :: L.flatten (L.map _l_term_labels fvs)) @ _l_term_labels t
| LApp (e1, e2) -> _l_term_labels e1 @ _l_term_labels e2
let l_term_labels term = remove_from_right (_l_term_labels term)
let new_label_pairs labels = L.map (fun x -> (x, next_label ())) labels
let id x = x
let rec search_pairs v f = function
| (x, n) :: xs -> if f v = f x then n else search_pairs v f xs
| [] -> v
let rec _assign_labels term pairs =
match term with
| LVar v -> LVar v
| LLam (l, fvs, v, t) ->
(* let lf = search_pairs l id pairs in *)
let lf = next_label () in
let rt = replace_label t l lf in
let fvst = L.map (fun x -> _assign_labels x pairs) fvs in
LLam (lf, fvst, v, _assign_labels rt pairs)
| LApp (e1, e2) -> LApp (_assign_labels e1 pairs, _assign_labels e2 pairs)
let fresh_labels term =
_assign_labels term (new_label_pairs (l_term_labels term))
(** replace every var occurrence by fresh var *)
let rec subst m x y =
match m with
......@@ -407,7 +362,6 @@ let reduction_print term =
(String.concat "\n"
(L.mapi
(fun i (a_term, b_trs) ->
(* let a_term_default = fresh_labels a_term in *)
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
......@@ -435,28 +389,3 @@ let reduction_print term =
^ "=====================\n")
(* "LC_" ^ string_of_int i ^ " ~ " ^ "TRS_" ^ string_of_int i *)
bisim))
let example = App (Lam ("x", Var "y"), Var "z")
let example2 =
App
( Lam ("x", App (Var "x", Var "x")),
Lam ("y", Lam ("z", App (Var "y", Var "z"))) )
let example3 =
App
( Lam ("x", App (App (Var "x", Var "x"), Var "x")),
Lam ("y", Lam ("z", App (Var "y", Var "z"))) )
let example4 =
App
( Lam ("x", App (App (Var "x", Var "x"), Var "x")),
Lam ("y", Lam ("z", App (Var "y", Var "z"))) )
let trs = term_to_trs example
let trs2 = term_to_trs example2
let trs3 = term_to_trs example3
(* let () = reduction_print example3 *)
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