Commit 2be21bef authored by Frontull Samuel's avatar Frontull Samuel
Browse files

fixed name clashes in for lambda terms in list of free variables

parent 781293a9
......@@ -76,7 +76,8 @@ let rec rename_fv term x y =
match term with
| LVar s -> if s = x then LVar y else term
| LLam (l, fvs, s, t) ->
if s = x then term else LLam (l, fvs, s, rename_fv t x y)
let fvs' = L.map (fun t -> rename_fv t x y) fvs in
if s = x then term else LLam (l, fvs', s, rename_fv t x y)
| LApp (e1, e2) -> LApp (rename_fv e1 x y, rename_fv e2 x y)
let rec default_names_r term pos =
......@@ -156,22 +157,28 @@ let rec subst m x y =
| LVar z -> if z = x then LVar y else m
| LLam (l, fvs, z, e) ->
let z' = if z = x then y else z in
LLam (l, fvs, z', subst e x y)
let fvs' = L.map (fun t -> subst t x y) fvs in
LLam (l, fvs', z', subst e x y)
| LApp (e1, e2) -> LApp (subst e1 x y, subst e2 x y)
(** capture-avoiding substitution *)
let rec _casubst m x n fvn =
match m with
| LVar y -> if x = y then n else m
| LLam (l, fvs, y, e) ->
| LLam (l, fvs, y, e) -> (
if y = x then m
else if L.mem y fvn && L.mem x (L.map lvname (free_variables e)) then
(* rename x to fresh *)
let f = next_fresh () in
let m' = subst m y f in
_casubst m' x n fvn
else
LLam (l, L.map (fun z -> _casubst z x n fvn) fvs, y, _casubst e x n fvn)
(* get intersection of fvn and fvs variable names *)
let fvs_vars = L.map lvname (L.flatten (L.map free_variables fvs)) in
let inters = List.filter (fun x -> List.mem x (y :: fvs_vars)) fvn in
match inters with
| [] ->
LLam
(l, L.map (fun z -> _casubst z x n fvn) fvs, y, _casubst e x n fvn)
| hd :: _ ->
let f = next_fresh () in
let m' = subst m hd f in
_casubst m' x n fvn )
| LApp (e1, e2) -> LApp (_casubst e1 x n fvn, _casubst e2 x n fvn)
let casubst m x n = _casubst m x n (L.map lvname (free_variables n))
......@@ -193,13 +200,6 @@ let rec _weak_redexpos term pos =
let weak_redexpos term = _weak_redexpos term ""
(* let rec recompute_fvs lterm =
match lterm with
| LVar _ -> lterm
| LLam (l, _, y, e) ->
LLam (l, free_variables lterm, y, recompute_fvs e)
| LApp (e1, e2) -> LApp (recompute_fvs e1, recompute_fvs e2) *)
let rec _weak_step term pos p =
match term with
| LApp (LLam (_, _, _, _), _) -> if p = pos then beta term else term
......@@ -209,7 +209,7 @@ let rec _weak_step term pos p =
let weak_step term = _weak_step term (weak_redexpos term) ""
(* recompute_fvs (_weak_step term (weak_redexpos term) "") *)
let weak_step_pos term pos = _weak_step term pos ""
type trs_term =
| TVar of string
......@@ -299,6 +299,9 @@ let rec _rstep trsterm trsrules pos p =
let rstep trs =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs (redexpos t) "")
let rstep_pos trs pos =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs pos "")
let rec all_vars vs =
match vs with TVar _ :: xs -> all_vars xs | _ :: _ -> false | [] -> true
......@@ -374,7 +377,6 @@ let reduction_print term =
let l_term = term_to_l_term term in
let trs = l_term_to_trs l_term in
let weak_reductions = weak_reduction l_term in
(* let weak_reductions = L.map default_names2 weak_reductions in *)
let trs_reductions = trs_reduction trs in
let trs_reductions_t = L.map trs_term trs_reductions in
let bisim = L.combine weak_reductions trs_reductions in
......@@ -398,7 +400,8 @@ let reduction_print term =
(l_term_to_string (trs_to_term trs))
trs_str
(String.concat " ->\n "
(prepend_index (L.map l_term_to_string weak_reductions)))
(prepend_index
(L.map _term_to_string (L.map l_term_to_term weak_reductions))))
(String.concat " ->\n "
(prepend_index (L.map trs_term_to_string trs_reductions_t)))
(String.concat "\n"
......@@ -424,13 +427,12 @@ let reduction_print term =
in
s
^ l_term_to_string a_term_default
^ "\n\n" ^ trs_to_string a_term_trs ^ "\n\n" ^ "Maps to: \n"
^ l_term_to_string (trs_to_term a_term_trs)
^ "\n\n" ^ trs_to_string a_term_trs
^ "\n\n++++++++++++++++++++++\n\n" ^ trs_to_string b_trs ^ "\n\n"
^ l_term_to_string b_trs_term
^ "\n\n"
(* ^ trs_to_string b_term_trs ^ "\n\n" *)
^ "\n=====================\n")
^ "=====================\n")
(* "LC_" ^ string_of_int i ^ " ~ " ^ "TRS_" ^ string_of_int i *)
bisim))
......
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