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

fixed l_term_to_trsterm but relative positions to fix

parent a20c0d0c
......@@ -12,14 +12,19 @@ let () =
try str_to_term (Sys.argv.(1) ^ "\n") with _ -> failwith "Syntax error"
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 "%s\n" (Core.l_term_to_string (Core.components_lterm "y" lterm)); *)
(* Printf.printf "%s\n"
(Core.l_term_to_string (Core.components_lterm "_" lterm)); *)
(* let trs = Core.l_term_to_trs lterm in
let trs' = Core.rstep trs in
Printf.printf "%s\n" (Core.trs_to_string trs);
let trsterm = Core.l_term_to_trsterm lterm in
Printf.printf "\n----------------------\n%s\n" (Core.trs_term_to_string_nopos trsterm); *)
(* 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 "A: %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));
......
......@@ -145,27 +145,36 @@ let beta term =
let rec _weak_redexpos term pos bvs =
match term with
| LApp (LLam (_, _, _), _) -> (
| LApp (LLam (l, v, b), arg) -> (
(* Printf.printf "%s\n" (l_term_to_string term); *)
let fvs = free_variables term in
let f_bvs = L.filter (fun x -> L.mem x bvs) fvs in
match f_bvs with
| [] -> pos
| _ -> ""
)
(* if free_variables term = [] then pos else "" *)
| _ ->
let posl = _weak_redexpos (LLam (l, v, b)) (pos ^ "1") bvs in
if posl <> "" then posl else _weak_redexpos arg (pos ^ "2") bvs
(* if free_variables term = [] then pos else "" *) )
| 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)
if posl <> "" then posl else _weak_redexpos e2 (pos ^ "2") bvs
| LLam (_, x, e) -> _weak_redexpos e (pos ^ "1") (LVar x :: bvs)
| _ -> ""
let weak_redexpos term = _weak_redexpos term "e" []
let starts_with p s =
if String.length p <= String.length s then
String.sub s 0 (String.length p) = p
else false
let rec _weak_step term pos p =
match term with
| LApp (LLam (_, _, _), _) -> if p = pos then beta term else term
| LApp (LLam (l, v, b), arg) ->
if p = pos then beta term
else if starts_with (p ^ "1") pos then
_weak_step (LLam (l, v, b)) pos (p ^ "1")
else _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"))
......@@ -219,44 +228,66 @@ let next_fresh_component () =
components_counter := !components_counter + 1;
"v_" ^ string_of_int !components_counter
let rec _components_trsterm x pos trsterm =
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 =
(* Printf.printf "_components_trsterm: %s\n" (trs_term_to_string trsterm); *)
match trsterm with
| TVar _ -> if trsterm = TVar x then [] else [ (trsterm, pos) ]
| TVar v -> if v = z then [] else [ (trsterm, pos) ]
| TDes (e1, e2) ->
if fvar_trsterm trsterm = [] then [ (trsterm, pos) ]
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 x (pos ^ "1") e1
@ _components_trsterm x (pos ^ "2") e2
_components_trsterm z (pos ^ "1") e1
@ _components_trsterm z (pos ^ "2") e2
| TCon (_, fvs) ->
let fvs_f = L.filter (fun x -> isvar (fst x)) fvs in
if fvs_f = [] then [ (trsterm, pos) ]
else
(* [ (TCon (l, L.flatten (L.map
(fun y -> _components_trsterm x (snd y) (fst y))
fvs)), pos) ] *)
let fvs_c =
L.flatten
(L.map (fun y -> _components_trsterm x ("1" ^ snd y) (fst y)) fvs)
(L.map (fun y -> _components_trsterm z ("1" ^ snd y) (fst y)) fvs)
in
let fvs_f = L.filter (fun x -> isvar (fst x)) fvs_c in
if fvs_f = [] then [ (trsterm, pos) ] else fvs_c
let components_trsterm x trsterm = _components_trsterm x "e" trsterm
let rec l_term_to_trsterm lterm =
let rec _l_term_to_trsterm lterm xs =
match lterm with
| LVar x -> TVar x
| LApp (e1, e2) -> TDes (l_term_to_trsterm e1, l_term_to_trsterm e2)
| 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 *)
| LLam (l, x, e) ->
let e_t = l_term_to_trsterm e in
let fvs_t = _components_trsterm x "1" e_t in
TCon (l, fvs_t)
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
let l_term_to_trsterm lterm = _l_term_to_trsterm lterm []
let rec _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) ->
| LApp (e1, e2) -> (
let e1' = _components_lterm xs (pos ^ "1") e1 in
let e2' = _components_lterm xs (pos ^ "2") e2 in
LApp (e1', e2')
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
LLam (l, y, e')
......@@ -265,6 +296,16 @@ let components_lterm x lterm = _components_lterm [ x ] "e" lterm
type trs_rule = RR of trs_term * trs_term
let rec rules lterm =
match lterm with
| LVar _ -> []
| LApp (e1, e2) -> rules e1 @ rules e2
| LLam (l, x, e) ->
let e' = 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
let rec trs_term_to_string_nopos term =
match term with
| TVar v -> v
......@@ -286,7 +327,8 @@ let rec trs_term_to_string_nopos term =
if fvs = [] then l
else
l ^ "["
^ String.concat "," (L.map (fun x -> trs_term_to_string (fst x)) fvs)
^ String.concat ","
(L.map (fun x -> trs_term_to_string_nopos (fst x)) fvs)
^ "]"
let trs_rule_to_string term =
......@@ -294,16 +336,6 @@ let trs_rule_to_string term =
| RR (l, r) ->
trs_term_to_string_nopos l ^ " -> " ^ trs_term_to_string_nopos r
let rec rules lterm =
match lterm with
| LVar _ -> []
| LApp (e1, e2) -> rules e1 @ rules e2
| LLam (l, x, e) ->
let e' = 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
let rules_to_string xs = String.concat ".\n" (L.map trs_rule_to_string xs)
type trs = TRS of trs_rule list * trs_term
......@@ -359,7 +391,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