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

changed definition of weak redex

parent 0ede555c
......@@ -14,13 +14,13 @@ let () =
let lterm = Core.term_to_l_term term in
(* let tterm = Core.l_term_to_trsterm lterm in *)
(* Printf.printf "%s\n" (Core.l_term_to_string (Core.components_lterm "y" lterm)); *)
(* let trs = Core.l_term_to_trs lterm in
(* let trs = Core.l_term_to_trs lterm in
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 "redex @ %s\n" (Core.redexpos tterm);
(* Printf.printf "%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));
Printf.printf "%s\n" (Core.trs_term_to_string (Core.trs_term trs'));
......
......@@ -2,7 +2,7 @@ module L = List
type term = Var of string | Lam of string * term | App of term * term
let rec _term_to_string term =
(* let rec _term_to_string term =
match term with
| Var v -> v
| Lam (v, t) -> (
......@@ -14,7 +14,7 @@ let rec _term_to_string term =
| Var _, Var _ -> _term_to_string e1 ^ " " ^ _term_to_string e2
| Var _, _ -> _term_to_string e1 ^ " (" ^ _term_to_string e2 ^ ")"
| _, Var _ -> "(" ^ _term_to_string e1 ^ ") " ^ _term_to_string e2
| _, _ -> "(" ^ _term_to_string e1 ^ ") (" ^ _term_to_string e2 ^ ")" )
| _, _ -> "(" ^ _term_to_string e1 ^ ") (" ^ _term_to_string e2 ^ ")" ) *)
(** Extract the name of a variable from a {e a_term} *)
let vname = function Var n -> n | _ -> ""
......@@ -41,8 +41,9 @@ type l_term =
let rec _l_term_to_string term c =
match term with
| LVar v -> v
| LLam (l, v, t) ->
"λ" ^ v ^ "_" ^ l
| LLam (_, v, t) ->
"λ" ^ v ^ "."
(* "λ" ^ v ^ "_" ^ l ^ "." *)
^ _l_term_to_string t (c + 1)
| LApp (e1, e2) -> (
match (e1, e2) with
......@@ -79,8 +80,7 @@ let rec l_term_to_term = function
let rec rename_fv term x y =
match term with
| LVar s -> if s = x then LVar y else term
| LLam (l, s, t) ->
if s = x then term else LLam (l, s, rename_fv t x y)
| LLam (l, s, t) -> if s = x then term else LLam (l, 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 =
......@@ -127,9 +127,7 @@ let rec _casubst m x n fvn =
else
let inters = List.filter (fun x -> x = y) fvn in
match inters with
| [] ->
LLam
(l, y, _casubst e x n fvn)
| [] -> LLam (l, y, _casubst e x n fvn)
| hd :: _ ->
let f = next_fresh () in
let m' = subst m hd f in
......@@ -145,16 +143,25 @@ let beta term =
res
| _ -> failwith "beta: Not a redex."
let rec _weak_redexpos term pos =
let rec _weak_redexpos term pos bvs =
match term with
| LApp (LLam (_, _, _), _) -> if free_variables term = [] then pos else ""
| LApp (LLam (_, _, _), _) -> (
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 "" *)
| LApp (e1, e2) ->
let posl = _weak_redexpos e1 (pos ^ "1") in
if posl <> "" then posl else _weak_redexpos e2 (pos ^ "2")
| LLam (_, _, e) -> _weak_redexpos e (pos ^ "1")
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)
| _ -> ""
let weak_redexpos term = _weak_redexpos term "e"
let weak_redexpos term = _weak_redexpos term "e" []
let rec _weak_step term pos p =
match term with
......@@ -221,16 +228,14 @@ let rec _components_trsterm x pos trsterm =
_components_trsterm x (pos ^ "1") e1
@ _components_trsterm x (pos ^ "2") e2
| TCon (_, fvs) ->
let fvs_f = L.filter (fun x -> (isvar (fst x))) fvs in
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) ] *)
L.flatten
(L.map
(fun y -> _components_trsterm x ("1" ^ snd y) (fst y))
fvs)
(* [ (TCon (l, L.flatten (L.map
(fun y -> _components_trsterm x (snd y) (fst y))
fvs)), pos) ] *)
L.flatten
(L.map (fun y -> _components_trsterm x ("1" ^ snd y) (fst y)) fvs)
let components_trsterm x trsterm = _components_trsterm x "e" trsterm
......@@ -346,11 +351,9 @@ let rec subst m pairs =
let rec rewrite trsrules trsterm =
(* Printf.printf "Rewrite: %s\n" (trs_term_to_string trsterm); *)
match (trsrules, trsterm) with
| RR (TDes (TCon (l, fvs), TVar x), r) :: xs,
TDes (TCon (l2, fvs2), arg) ->
| RR (TDes (TCon (l, fvs), TVar x), r) :: xs, TDes (TCon (l2, fvs2), arg) ->
if l = l2 then
subst r ((TVar x, arg) ::
L.combine (L.map fst fvs) (L.map fst fvs2))
subst r ((TVar x, arg) :: L.combine (L.map fst fvs) (L.map fst fvs2))
else rewrite xs trsterm
| [], _ -> trsterm
| _, _ -> failwith "Not a rule or not a trsterm."
......@@ -452,11 +455,9 @@ let rec simulate_trs_in_lterm trs =
let lterm = trs_to_term trs in
let lterm' = weak_step_pos lterm pos in
let lterm'_trs = l_term_to_trs lterm' in
( trs_to_string trs ^ "\n\n"
^ _term_to_string (l_term_to_term lterm)
^ "\n->" ^ pos ^ "\n"
^ _term_to_string (l_term_to_term lterm')
^ "\n\n" ^ trs_to_string trs' ^ "\n\n" ^ trs_to_string lterm'_trs )
( trs_to_string trs ^ "\n\n" ^ l_term_to_string lterm ^ "\n->" ^ pos
^ "\n" ^ l_term_to_string lterm' ^ "\n\n" ^ trs_to_string trs' ^ "\n\n"
^ trs_to_string lterm'_trs )
:: (if t = trs_term trs' then [] else simulate_trs_in_lterm trs')
(*
......@@ -472,24 +473,23 @@ let rec _simulate_lterm_in_trs lterm trs =
let trs' = rstep_pos trs pos in
let trs'_lterm = trs_to_term trs' in
let alpha_eq = default_names trs'_lterm = default_names lterm' in
let str = ( "+++++ REDUCTION STEP @" ^ pos ^ " +++++\n\n"
^ _term_to_string (l_term_to_term lterm)
^ "\n->" ^ pos ^ "\n"
^ _term_to_string (l_term_to_term lterm')
^ "\n\n"
^ trs_term_to_string_nopos (trs_term trs)
^ "\n->" ^ pos ^ "\n"
^ trs_term_to_string_nopos (trs_term trs')
^ "\n\nprojection to lambda term:\n"
^ _term_to_string (l_term_to_term trs'_lterm)
^ "\n\nalpha_eq: " ^ Bool.to_string alpha_eq ) in
let str =
"+++++ REDUCTION STEP @" ^ pos ^ " +++++\n\n" ^ l_term_to_string lterm
^ "\n->" ^ pos ^ "\n" ^ l_term_to_string lterm' ^ "\n\n"
^ trs_term_to_string_nopos (trs_term trs)
^ "\n->" ^ pos ^ "\n"
^ trs_term_to_string_nopos (trs_term trs')
^ "\n\nprojection to lambda term:\n"
^ l_term_to_string trs'_lterm
^ "\n\nalpha_eq: " ^ Bool.to_string alpha_eq
in
str :: (if lterm = lterm' then [] else _simulate_lterm_in_trs lterm' trs')
else []
let simulate_lterm_in_trs lterm =
let trs = l_term_to_trs lterm in
trs_to_string trs ^ "\n\n"
^ _term_to_string (l_term_to_term (trs_to_term trs))
^ l_term_to_string (trs_to_term trs)
^ "\n"
^ String.concat "\n\n" (_simulate_lterm_in_trs lterm trs)
......
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