Commit 28be4c67 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

l_term_to_trsterm refactoring - now works for pcp

parent 8e0506bc
......@@ -13,8 +13,8 @@ let () =
in
let lterm = Core.term_to_l_term term in
(* Printf.printf "redex @ %s\n" (Core.weak_redexpos lterm); *)
(* let tterm = Core.l_term_to_trsterm lterm in
Printf.printf "\n----------------------\n%s\n" (Core.trs_term_to_string tterm); *)
let tterm = Core.l_term_to_trsterm lterm in
Printf.printf "\n----------------------\n%s\n" (Core.trs_term_to_string tterm);
(* Printf.printf "%s\n"
(Core.l_term_to_string (Core.components_lterm "_" lterm)); *)
(* let trs = Core.l_term_to_trs lterm in
......
......@@ -158,7 +158,7 @@ let rec _weak_redexpos term pos bvs =
| LApp (e1, e2) ->
let posl = _weak_redexpos e1 (pos ^ "1") bvs in
if posl <> "" then posl else _weak_redexpos e2 (pos ^ "2") bvs
| LLam (_, x, e) -> _weak_redexpos e (pos ^ "1") (LVar x :: bvs)
| LLam (_, x, e) -> _weak_redexpos e (pos ^ "3") (LVar x :: bvs)
| _ -> ""
let weak_redexpos term = _weak_redexpos term "e" []
......@@ -177,13 +177,35 @@ let rec _weak_step term pos p =
else LApp (LLam (l, v, b), _weak_step arg pos (p ^ "2"))
| LApp (e1, e2) ->
LApp (_weak_step e1 pos (p ^ "1"), _weak_step e2 pos (p ^ "2"))
| LLam (l, x, e) -> LLam (l, x, _weak_step e pos (p ^ "1"))
| LLam (l, x, e) -> LLam (l, x, _weak_step e pos (p ^ "3"))
| _ -> term
let weak_step term = _weak_step term (weak_redexpos term) "e"
let weak_step_pos term pos = _weak_step term pos "e"
let rec _subterm term pos p =
if p = pos then term else (
match term with
| LVar _ ->
Printf.printf "pos: %s\n" pos;
failwith("_subterm: subterm at specified position does not exist.")
| LApp (a1, a2) ->
if starts_with (p ^ "1") pos then
_subterm a1 pos (p ^ "1")
else _subterm a2 pos (p ^ "2")
| LLam (_, _, b) ->
if starts_with (p ^ "3") pos then
_subterm b pos (p ^ "3")
else _subterm b pos p
)
let subterm_skip term pos =
Printf.printf "subterm_skip: %s _ %s\n" (l_term_to_string term) pos;
let res = _subterm term pos "" in
Printf.printf "subterm_skip: %s\n" (l_term_to_string res);
res
type trs_term =
| TVar of string
| TCon of string * (trs_term * string) list
......@@ -228,51 +250,43 @@ let next_fresh_component () =
components_counter := !components_counter + 1;
"v_" ^ string_of_int !components_counter
let rec _components_trsterm z pos trsterm lterm =
(* Printf.printf "_components_trsterm: %s\n" (trs_term_to_string trsterm); *)
match trsterm, lterm with
| TVar v, LVar _ -> if v = z then [] else [ (trsterm, pos) ]
| _, LVar _ ->
failwith("_components_trsterm: _, LVar _ Cannot be the case.")
| TDes (e1, e2), LApp (a1, a2) ->
let fvs = fvar_trsterm trsterm in
let f_fvs = L.filter (fun x -> x = TVar z) fvs in
if fvs = [] || f_fvs = [] then [ (trsterm, pos) ]
else
_components_trsterm z (pos ^ "1") e1 a1
@ _components_trsterm z (pos ^ "2") e2 a2
| _, LApp _ ->
failwith("_components_trsterm: _, LApp _ Cannot be the case.")
| TCon (_, fvs), LLam (_, _, b) ->
let fvs_c =
L.flatten
(L.map (fun y -> _components_trsterm z ("1" ^ snd y) (fst y) b) fvs)
in
let fvs_f = L.filter (fun x -> isvar (fst x)) fvs_c in
if fvs_f = [] then [ (trsterm, pos) ] else fvs_c
| _, LLam (_, _, b) -> _components_trsterm z (pos ^ "1") trsterm b
let components_trsterm x trsterm = _components_trsterm x "e" trsterm
let diff l1 l2 = List.filter (fun x -> not (List.mem x l2)) l1
let rec _components_lterm xs pos lterm =
if free_variables lterm = [] then [(lterm, pos)]
else
match lterm with
| LVar _ -> if L.mem lterm xs then [] else [(lterm, pos)]
| LApp (e1, e2) -> (
(* check if abstracted variables occur in left argument *)
let e1_fvs = L.filter (fun z -> L.mem z (free_variables e1)) xs in
(* check if abstracted variables occur in right argument *)
let e2_fvs = L.filter (fun z -> L.mem z (free_variables e2)) xs in
match e1_fvs, e2_fvs with
| [], [] -> [(lterm, pos)]
| [], _ -> [(e1, pos ^ "1")] @ _components_lterm xs (pos ^ "2") e2
| _, [] -> _components_lterm xs (pos ^ "1") e1 @ [(e2, pos ^ "2")]
| _, _ ->
_components_lterm xs (pos ^ "1") e1 @
_components_lterm xs (pos ^ "2") e2
)
| LLam (_, y, e) -> (
(* let e_fvs = diff (free_variables lterm) xs in *)
let e_fvs = free_variables lterm in
match e_fvs with
| [] -> [(lterm, pos)]
| _ -> _components_lterm (LVar y :: xs) (pos ^ "3") e
)
let rec _l_term_to_trsterm lterm xs =
match lterm with
| LVar x -> TVar x
| LApp (e1, e2) ->
(* let fv_e1 = L.filter (fun z -> L.mem (LVar z) (free_variables e1)) xs in
let fv_e2 = L.filter (fun z -> L.mem (LVar z) (free_variables e2)) xs in
if fv_e1 = [] && fv_e2 = [] then *)
TDes (_l_term_to_trsterm e1 xs, _l_term_to_trsterm e2 xs)
(* else if fv_e1 = [] then _l_term_to_trsterm e1 xs
else _l_term_to_trsterm e2 xs *)
| LApp (e1, e2) -> (
TDes (_l_term_to_trsterm e1 xs, _l_term_to_trsterm e2 xs)
)
| LLam (l, x, e) ->
let e_t = _l_term_to_trsterm e (x :: xs) in
(* TCon (l, cmps) *)
let xs' = L.filter (fun z -> L.mem (LVar z) (free_variables lterm)) xs in
(* check if vars of previous lambdas occur or not *)
if xs' = [] then
let cmps = _components_trsterm x "1" e_t e in
TCon (l, cmps)
else e_t
let cmps = _components_lterm [ LVar x ] "3" e in
TCon (l, L.map (fun c -> (_l_term_to_trsterm (fst c) xs, snd c)) cmps)
let l_term_to_trsterm lterm =
_l_term_to_trsterm lterm []
......@@ -291,7 +305,7 @@ let rec _fvar_components_lterm xs pos lterm =
else LVar ("v_" ^ pos)
| _ -> LApp (e1', e2') )
| LLam (l, y, e) ->
let e' = _fvar_components_lterm (y :: xs) (pos ^ "1") e in
let e' = _fvar_components_lterm (y :: xs) (pos ^ "3") e in
LLam (l, y, e')
let fvar_components_lterm x lterm = _fvar_components_lterm [ x ] "e" lterm
......
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