Commit 38c528fa authored by Frontull Samuel's avatar Frontull Samuel
Browse files

replace also free variables in abstraction list

parent 13379937
open Wltrs
(* ((/x.x x) (/y z.y z)) ((/x.x x) (/y z.y z)) *)
let str_to_term s = Grammar.input Lexer.token (Lexing.from_string s)
let () =
......
......@@ -13,34 +13,97 @@ let rec _term_to_string term =
| _, Var _ -> "(" ^ _term_to_string e1 ^ ") " ^ _term_to_string e2
| _, _ -> "(" ^ _term_to_string e1 ^ ") (" ^ _term_to_string e2 ^ ")" )
let label = ref 0
let next_label () =
label := !label + 1;
"C" ^ string_of_int !label
type l_term =
| LVar of string
| LLam of string * l_term list * string * l_term
| LApp of l_term * l_term
let rec l_term_to_term = function
| LVar v -> Var v
| LLam (_, _, v, t) -> Lam (v, l_term_to_term t)
| LApp (e1, e2) -> App (l_term_to_term e1, l_term_to_term e2)
let rec _l_term_to_string term c =
match term with
| LVar v -> v
| LLam (l, fvs, v, t) ->
"λ" ^ v ^ "_" ^ l ^ "["
^ String.concat " " (L.map (fun k -> _l_term_to_string k 0) fvs)
^ "]."
^ _l_term_to_string t (c + 1)
| LApp (e1, e2) -> (
match (e1, e2) with
| LVar _, LVar _ -> _l_term_to_string e1 c ^ " " ^ _l_term_to_string e2 c
| LVar _, _ ->
_l_term_to_string e1 c ^ " (" ^ _l_term_to_string e2 c ^ ")"
| _, LVar _ ->
"(" ^ _l_term_to_string e1 c ^ ") " ^ _l_term_to_string e2 c
| _, _ ->
"(" ^ _l_term_to_string e1 c ^ ") (" ^ _l_term_to_string e2 c ^ ")" )
(* _term_to_string (l_term_to_term term) *)
let l_term_to_string term = _l_term_to_string term 0
(** Extract the name of a variable from a {e a_term} *)
let vname = function Var n -> n | _ -> ""
let remove l1 f x =
L.fold_left (fun acc hd -> if f hd = x then acc else hd :: acc) [] l1
let rec fvars = function
| Var x -> [ Var x ]
| Lam (x, e) -> remove (fvars e) vname x
| App (e1, e2) -> fvars e1 @ fvars e2
(* lift : term -> TRS *)
let rec term_to_l_term term =
match term with
| Var x -> LVar x
| Lam (x, e) ->
let l = next_label () in
let fvs = L.map term_to_l_term (fvars term) in
LLam (l, fvs, x, term_to_l_term e)
| App (e1, e2) -> LApp (term_to_l_term e1, term_to_l_term e2)
let rec rename_fv term x y =
match term with
| Var s -> if s = x then Var y else term
| Lam (s, t) -> if s = x then term else Lam (s, rename_fv t x y)
| App (e1, e2) -> App (rename_fv e1 x y, rename_fv e2 x y)
| 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)
| LApp (e1, e2) -> LApp (rename_fv e1 x y, rename_fv e2 x y)
let rec default_names_r term pos =
match term with
| Var v -> Var v
| Lam (v, t) ->
| LVar v -> LVar v
| LLam (l, fvs, v, t) ->
let vf = "x_" ^ pos in
Lam (vf, default_names_r (rename_fv t v vf) (pos ^ "0"))
| App (e1, e2) ->
App (default_names_r e1 (pos ^ "0"), default_names_r e2 (pos ^ "1"))
LLam (l, fvs, vf, default_names_r (rename_fv t v vf) (pos ^ "0"))
| LApp (e1, e2) ->
LApp (default_names_r e1 (pos ^ "0"), default_names_r e2 (pos ^ "1"))
let default_names term = default_names_r term "e"
let remove l1 f x =
L.fold_left (fun acc hd -> if f hd = x then acc else hd :: acc) [] l1
let rec default_labels term =
match term with
| LVar v -> LVar v
| LLam (_, fvs, v, t) -> LLam (next_label (), fvs, v, default_labels t)
| LApp (e1, e2) -> LApp (default_labels e1, default_labels e2)
(** Extract the name of a variable from a {e a_term} *)
let vname = function Var n -> n | _ -> ""
let lvname = function LVar n -> n | _ -> ""
(** Extract the free variables in a {e a_term} *)
let rec free_variables = function
| Var x -> [ Var x ]
| Lam (x, e) -> remove (free_variables e) vname x
| App (e1, e2) -> free_variables e1 @ free_variables e2
| LVar x -> [ LVar x ]
| LLam (_, _, x, e) -> remove (free_variables e) lvname x
| LApp (e1, e2) -> free_variables e1 @ free_variables e2
let counter = ref 0
......@@ -51,97 +114,63 @@ let next_fresh () =
(** replace every var occurrence by fresh var *)
let rec subst m x y =
match m with
| Var z -> if z = x then Var y else m
| Lam (z, e) ->
| 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
Lam (z', subst e x y)
| App (e1, e2) -> App (subst e1 x y, subst e2 x y)
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
| Var y -> if x = y then n else m
| Lam (y, e) ->
| LVar y -> if x = y then n else m
| LLam (l, fvs, y, e) ->
if y = x then m
else if L.mem y fvn && L.mem x (L.map vname (free_variables e)) then
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 Lam (y, _casubst e x n fvn)
| App (e1, e2) -> App (_casubst e1 x n fvn, _casubst e2 x n fvn)
else
LLam (l, L.map (fun z -> _casubst z x n fvn) fvs, y, _casubst e 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 vname (free_variables n))
let casubst m x n = _casubst m x n (L.map lvname (free_variables n))
let beta term =
match term with
| App (Lam (x, m), n) ->
| LApp (LLam (_, _, x, m), n) ->
let res = casubst m x n in
res
| _ -> failwith "beta: Not a redex."
let rec _weak_redexpos term pos =
match term with
| App (Lam (_, _), _) -> pos
| App (e1, e2) ->
| LApp (LLam (_, _, _, _), _) -> pos
| LApp (e1, e2) ->
let posl = _weak_redexpos e1 (pos ^ "1") in
if posl != "" then posl else _weak_redexpos e2 (pos ^ "2")
| _ -> ""
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
| App (Lam (_, _), _) -> if p = pos then beta term else term
| App (e1, e2) ->
App (_weak_step e1 pos (p ^ "1"), _weak_step e2 pos (p ^ "2"))
| LApp (LLam (_, _, _, _), _) -> if p = pos then beta term else term
| LApp (e1, e2) ->
LApp (_weak_step e1 pos (p ^ "1"), _weak_step e2 pos (p ^ "2"))
| _ -> term
let weak_step term = _weak_step term (weak_redexpos term) ""
let label = ref 0
let next_label () =
label := !label + 1;
"C" ^ string_of_int !label
type l_term =
| LVar of string
| LLam of string * l_term list * string * l_term
| LApp of l_term * l_term
let rec l_term_to_term = function
| LVar v -> Var v
| LLam (_, _, v, t) -> Lam (v, l_term_to_term t)
| LApp (e1, e2) -> App (l_term_to_term e1, l_term_to_term e2)
let rec _l_term_to_string term c =
match term with
| LVar v -> v
| LLam (l, _, v, t) -> "λ" ^ v ^ "_" ^ l ^ "." ^ _l_term_to_string t (c + 1)
| LApp (e1, e2) -> (
match (e1, e2) with
| LVar _, LVar _ -> _l_term_to_string e1 c ^ " " ^ _l_term_to_string e2 c
| LVar _, _ ->
_l_term_to_string e1 c ^ " (" ^ _l_term_to_string e2 c ^ ")"
| _, LVar _ ->
"(" ^ _l_term_to_string e1 c ^ ") " ^ _l_term_to_string e2 c
| _, _ ->
"(" ^ _l_term_to_string e1 c ^ ") (" ^ _l_term_to_string e2 c ^ ")" )
(* _term_to_string (l_term_to_term term) *)
let l_term_to_string term = _l_term_to_string term 0
(* lift : term -> TRS *)
let rec label term =
match term with
| Var x -> LVar x
| Lam (x, e) ->
let l = next_label () in
let fvs = L.map label (free_variables term) in
LLam (l, fvs, x, label e)
| App (e1, e2) -> LApp (label e1, label e2)
(* recompute_fvs (_weak_step term (weak_redexpos term) "") *)
type trs_term =
| TVar of string
......@@ -161,17 +190,11 @@ let rec trs_term_to_string term =
let term_print term = Printf.printf "%s" (trs_term_to_string term)
let rec lterm_to_trsterm lterm =
let rec l_term_to_trsterm lterm =
match lterm with
| LVar x -> TVar x
| LLam (l, fvs, _, _) -> TCon (l, L.map lterm_to_trsterm fvs)
| LApp (e1, e2) -> TDes (lterm_to_trsterm e1, lterm_to_trsterm e2)
let rec lterm_to_term lterm =
match lterm with
| LVar x -> Var x
| LLam (_, _, x, t) -> Lam (x, lterm_to_term t)
| LApp (e1, e2) -> App (lterm_to_term e1, lterm_to_term e2)
| LLam (l, fvs, _, _) -> TCon (l, L.map l_term_to_trsterm fvs)
| LApp (e1, e2) -> TDes (l_term_to_trsterm e1, l_term_to_trsterm e2)
type trs_rule = RR of trs_term * trs_term
......@@ -183,26 +206,23 @@ let rec rules lterm =
match lterm with
| LVar _ -> []
| LLam (_, _, x, e) ->
RR (TDes (lterm_to_trsterm lterm, TVar x), lterm_to_trsterm e) :: rules e
RR (TDes (l_term_to_trsterm lterm, TVar x), l_term_to_trsterm e)
:: rules e
| LApp (e1, e2) -> rules e1 @ rules e2
let rules_to_string xs = String.concat ".\n" (L.map trs_rule_to_string xs)
type trs = TRS of trs_rule list * trs_term
let trs_to_string = function
| TRS (xs, t) ->
"Rules:\n" ^ rules_to_string xs ^ ".\n\nTerm:\n" ^ trs_term_to_string t
let trs_rules = function TRS (xs, _) -> xs
let trs_term = function TRS (_, t) -> t
let term_to_trs x =
let lx = label x in
TRS (rules lx, lterm_to_trsterm lx)
let lx = term_to_l_term x in
TRS (rules lx, l_term_to_trsterm lx)
let term_trs_print term = Printf.printf "%s" (trs_to_string (term_to_trs term))
let l_term_to_trs x = TRS (rules x, l_term_to_trsterm x)
let rec _redexpos trsterm pos =
match trsterm with
......@@ -219,6 +239,7 @@ let rec search_pairs v = function
| [] -> v
let rec subst m pairs =
(* Printf.printf "subst\n"; *)
match m with
| TVar _ -> search_pairs m pairs
| TCon (l, fvs) -> TCon (l, L.map (fun z -> subst z pairs) fvs)
......@@ -243,11 +264,17 @@ let rec _rstep trsterm trsrules pos p =
let rstep trs =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs (redexpos t) "")
let rec all_vars vs =
match vs with TVar _ :: xs -> all_vars xs | _ :: _ -> false | [] -> true
(* project : TRS -> term *)
let rec trs_rule trsrules label =
(* Printf.printf "trs_rule %s\n" label;
Printf.printf "trs_rules %s\n"
(String.concat "\n" (L.map trs_rule_to_string trsrules)); *)
match trsrules with
| RR (TDes (TCon (l, _), _), _) :: xs ->
if l = label then L.hd trsrules else trs_rule xs label
| RR (TDes (TCon (l, fvs), _), _) :: xs ->
if l = label && all_vars fvs then L.hd trsrules else trs_rule xs label
| _ :: xs -> trs_rule xs label
| [] -> failwith "No rule with such label."
......@@ -255,9 +282,10 @@ let counter_projection = ref 0
let next_fresh_2 () =
counter_projection := !counter_projection + 1;
"v_" ^ string_of_int !counter_projection
"v" ^ string_of_int !counter_projection
let rec trs_to_term trs =
(* Printf.printf "trs_to_term\n"; *)
match trs with
| TRS (xs, t) -> (
match t with
......@@ -266,6 +294,8 @@ let rec trs_to_term trs =
LApp (trs_to_term (TRS (xs, e1)), trs_to_term (TRS (xs, e2)))
| TCon (label, fvs) -> (
let rr = trs_rule xs label in
(* Printf.printf "trs_rule rr:%s\n" (trs_rule_to_string rr);
Printf.printf "mapping term:%s\n" (trs_term_to_string t); *)
match rr with
| RR (TDes (TCon (_, fvs_r), var), r) ->
if L.mem var fvs then
......@@ -285,6 +315,12 @@ let rec trs_to_term trs =
trs_to_term (TRS (xs, subst r (L.combine fvs_r fvs))) )
| _ -> failwith "Not a RR found." ) )
let trs_to_string trs =
(* Printf.printf "%s\n" (trs_term_to_string (trs_term trs)); *)
match trs with
| TRS (xs, t) ->
"Rules:\n" ^ rules_to_string xs ^ ".\n\nTerm:\n" ^ trs_term_to_string t
let rec _weak_reduction term =
let wt = weak_step term in
if wt = term then [] else wt :: _weak_reduction wt
......@@ -297,12 +333,13 @@ let rec _trs_reduction trs =
let trs_reduction trs = trs :: _trs_reduction trs
let prepend_index xs =
L.mapi (fun i -> fun x -> "[" ^ (string_of_int i) ^ "] " ^ x) xs
let prepend_index xs = L.mapi (fun i x -> "[" ^ string_of_int i ^ "] " ^ x) xs
let reduction_print term =
let trs = term_to_trs term in
let weak_reductions = weak_reduction term in
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
......@@ -325,16 +362,40 @@ let reduction_print term =
%s\n"
(l_term_to_string (trs_to_term trs))
trs_str
(String.concat " ->\n " (prepend_index (L.map _term_to_string weak_reductions)))
(String.concat " ->\n " (prepend_index (L.map trs_term_to_string trs_reductions_t)))
(String.concat " ->\n "
(prepend_index (L.map l_term_to_string weak_reductions)))
(String.concat " ->\n "
(prepend_index (L.map trs_term_to_string trs_reductions_t)))
(String.concat "\n"
(L.mapi
(fun i -> fun (a, b) ->
let b_t = l_term_to_term (trs_to_term b) in
if default_names a = default_names b_t then
"LC_" ^ string_of_int i ^ " ~ " ^ "TRS_" ^ string_of_int i
else
"\t! LC_" ^ string_of_int i ^ " ≁ " ^ "TRS_" ^ string_of_int i)
(fun i (a_term, b_trs) ->
let a_term_default = default_labels a_term in
let a_term_trs = l_term_to_trs a_term_default in
let b_trs_term = trs_to_term b_trs in
(* let b_term_trs = l_term_to_trs b_trs_term in *)
let s =
if
l_term_to_string (default_names a_term)
= l_term_to_string (default_names b_trs_term)
&& trs_term a_term_trs = trs_term b_trs
then
"\n---------------------\n" ^ "TRS_" ^ string_of_int i ^ " ~ "
^ "LC_" ^ string_of_int i ^ "\n---------------------\n"
else
"\n---------------------\n" ^ "! TRS_" ^ string_of_int i
^ " ≁ " ^ "LC_" ^ string_of_int i
^ "\n---------------------\n"
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++++++++++++++++++++++\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")
(* "LC_" ^ string_of_int i ^ " ~ " ^ "TRS_" ^ string_of_int i *)
bisim))
let example = App (Lam ("x", Var "y"), Var "z")
......
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