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

solution to position mismatch problem

parent a0c12333
......@@ -13,7 +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 *)
(* 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
......
......@@ -228,31 +228,29 @@ let next_fresh_component () =
components_counter := !components_counter + 1;
"v_" ^ string_of_int !components_counter
let rec prepend_pos p t =
match t with
| TCon (l, fvs) ->
TCon (l, L.map (fun (x,y) -> (x, p ^ y)) fvs)
| TDes (e1, e2) ->TDes (prepend_pos p e1, prepend_pos p e2)
| _ -> t
let rec _components_trsterm z pos trsterm =
let rec _components_trsterm z pos trsterm lterm =
(* Printf.printf "_components_trsterm: %s\n" (trs_term_to_string trsterm); *)
match trsterm with
| TVar v -> if v = z then [] else [ (trsterm, pos) ]
| TDes (e1, e2) ->
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
@ _components_trsterm z (pos ^ "2") e2
| TCon (_, fvs) ->
_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)) fvs)
(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
......@@ -268,31 +266,35 @@ let rec _l_term_to_trsterm lterm xs =
else _l_term_to_trsterm e2 xs *)
| LLam (l, x, e) ->
let e_t = _l_term_to_trsterm e (x :: xs) in
let cmps = _components_trsterm x "1" e_t in
(* TCon (l, cmps) *)
let xs' = L.filter (fun z -> L.mem (LVar z) (free_variables lterm)) xs in
if xs' = [] then TCon (l, cmps) else e_t
(* 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 l_term_to_trsterm lterm = _l_term_to_trsterm lterm []
let l_term_to_trsterm lterm =
_l_term_to_trsterm lterm []
let rec _components_lterm xs pos lterm =
let rec _fvar_components_lterm xs pos lterm =
if free_variables lterm = [] then LVar ("v_" ^ pos)
else
match lterm with
| LVar y -> if L.mem y xs then lterm else LVar ("v_" ^ pos)
| LApp (e1, e2) -> (
let e1' = _components_lterm xs (pos ^ "1") e1 in
let e2' = _components_lterm xs (pos ^ "2") e2 in
let e1' = _fvar_components_lterm xs (pos ^ "1") e1 in
let e2' = _fvar_components_lterm xs (pos ^ "2") e2 in
match (e1', e2') with
| LVar x, LVar y ->
if L.mem x xs || L.mem y xs then LApp (e1', e2')
else LVar ("v_" ^ pos)
| _ -> LApp (e1', e2') )
| LLam (l, y, e) ->
let e' = _components_lterm (y :: xs) (pos ^ "1") e in
let e' = _fvar_components_lterm (y :: xs) (pos ^ "1") e in
LLam (l, y, e')
let components_lterm x lterm = _components_lterm [ x ] "e" lterm
let fvar_components_lterm x lterm = _fvar_components_lterm [ x ] "e" lterm
type trs_rule = RR of trs_term * trs_term
......@@ -301,7 +303,7 @@ let rec rules lterm =
| LVar _ -> []
| LApp (e1, e2) -> rules e1 @ rules e2
| LLam (l, x, e) ->
let e' = components_lterm x e in
let e' = fvar_components_lterm x e in
let e_t = l_term_to_trsterm e' in
let trsterm_t = l_term_to_trsterm (LLam (l, x, e')) in
RR (TDes (trsterm_t, TVar x), e_t) :: rules e
......@@ -391,7 +393,7 @@ let rec rewrite trsrules trsterm =
| _, _ -> failwith "Not a rule or not a trsterm."
let rec _rstep trsterm trsrules pos p =
Printf.printf "%s # %s # %s\n" (trs_term_to_string trsterm) pos p;
(* Printf.printf "%s # %s # %s\n" (trs_term_to_string trsterm) pos p; *)
match trsterm with
| TDes (TCon (_, _), _) ->
if p = pos then rewrite trsrules trsterm else trsterm
......
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