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

Merge branch 'master' into 'main'

maximal free subterms only one function

See merge request !7
parents 861d340c 117665ac
......@@ -10,9 +10,6 @@ let _LAM = "1"
type term = Var of string | Lam of string * term | App of term * term
let remove l1 f x =
L.fold_left (fun acc hd -> if f hd = x then acc else hd :: acc) [] l1
let label = ref 0
let next_label () =
......@@ -32,9 +29,7 @@ type l_term =
(** lambda term to labeled lambda term *)
let rec term_to_l_term = function
| Var x -> LVar x
| Lam (x, e) ->
let l = next_label () in
LLam (l, x, term_to_l_term e)
| Lam (x, e) -> LLam (next_label (), x, term_to_l_term e)
| App (e1, e2) -> LApp (term_to_l_term e1, term_to_l_term e2)
(** labeled lambda term to lambda term *)
......@@ -43,7 +38,7 @@ let rec l_term_to_term = function
| LLam (_, v, t) -> Lam (v, l_term_to_term t)
| LApp (e1, e2) -> App (l_term_to_term e1, l_term_to_term e2)
(** rename every occurrence of variable {e x} in {e term} to {e y} *)
(** rename the free occurrences of variable {e x} in {e term} to {e y} *)
let rec rename term x y =
match term with
| LVar s -> if s = x then LVar y else term
......@@ -61,13 +56,14 @@ let rec default_names_r pos = function
let default_names term = default_names_r _ROOT term
(** Extract the name of a variable from a {e a_term} *)
let lvname = function LVar n -> n | _ -> ""
(** remove element {e x} from list {e l1} *)
let remove l1 x =
L.fold_left (fun acc hd -> if hd = x then acc else hd :: acc) [] l1
(** Extract the free variables in a {e a_term} *)
let rec free_variables = function
| LVar x -> [ LVar x ]
| LLam (_, x, e) -> remove (free_variables e) lvname x
| LLam (_, x, e) -> remove (free_variables e) (LVar x)
| LApp (e1, e2) -> free_variables e1 @ free_variables e2
let counter = ref 0
......@@ -86,22 +82,17 @@ let rec subst m x y =
| LApp (e1, e2) -> LApp (subst e1 x y, subst e2 x y)
(** capture-avoiding substitution *)
let rec _casubst m x n fvn =
let rec casubst m x n =
match m with
| LVar y -> if x = y then n else m
| LApp (e1, e2) -> LApp (_casubst e1 x n fvn, _casubst e2 x n fvn)
| LLam (l, y, e) -> (
| LApp (e1, e2) -> LApp (casubst e1 x n, casubst e2 x n)
| LLam (l, y, e) ->
if y = x then m
else
let inters = List.filter (fun x -> x = y) fvn in
match inters with
| [] -> LLam (l, y, _casubst e x n fvn)
| hd :: _ ->
let f = next_fresh () in
let m' = subst m hd f in
_casubst m' x n fvn )
let casubst m x n = _casubst m x n (L.map lvname (free_variables n))
else if L.mem (LVar y) (free_variables n) then
let f = next_fresh () in
let m' = subst m y f in
casubst m' x n
else LLam (l, y, casubst e x n)
(** apply a beta step *)
let beta = function
......@@ -149,9 +140,7 @@ let rec _weak_step term pos p =
| LLam (l, x, e) -> LLam (l, x, _weak_step e pos (p ^ _LAM))
| _ -> term
let weak_step term = _weak_step term (weak_redexpos term) _ROOT
let weak_step_pos term pos = _weak_step term pos _ROOT
let weak_step term pos = _weak_step term pos _ROOT
(** TRS term *)
type trs_term =
......@@ -168,7 +157,7 @@ let rec fvar_trsterm = function
| TDes (e1, e2) -> fvar_trsterm e1 @ fvar_trsterm e2
| TCon (_, fvs) -> L.flatten (L.map (fun x -> fvar_trsterm (fst x)) fvs)
let rec _components_lterm xs pos lterm =
let rec maximal_free_subterms xs pos lterm =
if free_variables lterm = [] then [ (lterm, pos) ]
else
match lterm with
......@@ -180,40 +169,35 @@ let rec _components_lterm xs pos lterm =
match (e1_fvs, e2_fvs) with
| [], [] -> [ (lterm, pos) ]
| [], _ ->
[ (e1, pos ^ _APP_L) ] @ _components_lterm xs (pos ^ _APP_R) e2
[ (e1, pos ^ _APP_L) ] @ maximal_free_subterms xs (pos ^ _APP_R) e2
| _, [] ->
_components_lterm xs (pos ^ _APP_L) e1 @ [ (e2, pos ^ _APP_R) ]
maximal_free_subterms xs (pos ^ _APP_L) e1 @ [ (e2, pos ^ _APP_R) ]
| _, _ ->
_components_lterm xs (pos ^ _APP_L) e1
@ _components_lterm xs (pos ^ _APP_R) e2 )
| LLam (_, y, e) -> _components_lterm (LVar y :: xs) (pos ^ _LAM) e
maximal_free_subterms xs (pos ^ _APP_L) e1
@ maximal_free_subterms xs (pos ^ _APP_R) e2 )
| LLam (_, y, e) -> maximal_free_subterms (LVar y :: xs) (pos ^ _LAM) e
let rec l_term_to_trsterm = function
| LVar x -> TVar x
| LApp (e1, e2) -> TDes (l_term_to_trsterm e1, l_term_to_trsterm e2)
| LLam (l, x, e) ->
let cmps = _components_lterm [ LVar x ] _LAM e in
let cmps = maximal_free_subterms [ LVar x ] _LAM e in
TCon (l, L.map (fun (t, p) -> (l_term_to_trsterm t, p)) cmps)
let rec _cs_to_var xs pos lterm =
if free_variables lterm = [] then LVar ("v_" ^ pos)
else
match lterm with
| LVar _ -> if L.mem lterm xs then lterm else LVar ("v_" ^ pos)
| LApp (e1, e2) -> (
let e1_fvs = intersect xs (free_variables e1) in
let e2_fvs = intersect xs (free_variables e2) in
match (e1_fvs, e2_fvs) with
| [], [] -> LVar ("v_" ^ pos)
| _, _ ->
let e1' = _cs_to_var xs (pos ^ _APP_L) e1 in
let e2' = _cs_to_var xs (pos ^ _APP_R) e2 in
LApp (e1', e2') )
| LLam (l, y, e) ->
let e' = _cs_to_var (LVar y :: xs) (pos ^ _LAM) e in
LLam (l, y, e')
let rec _term_to_pattern lterm ps p =
if L.mem p ps then LVar ("v_" ^ p) else
match lterm with
| LVar _ -> lterm
| LApp (e1, e2) ->
LApp (_term_to_pattern e1 ps (p ^ _APP_L),
_term_to_pattern e2 ps (p ^ _APP_R))
| LLam (l, x, e) ->
LLam (l, x, _term_to_pattern e ps (p ^ _LAM))
let cs_to_var lterm xs = _cs_to_var xs _ROOT lterm
let term_to_pattern lterm xs =
let fs = maximal_free_subterms xs _ROOT lterm in
let ps = L.map snd fs in
_term_to_pattern lterm ps _ROOT
type trs_rule = RR of trs_term * trs_term
......@@ -221,10 +205,10 @@ let rec rules = function
| LVar _ -> []
| LApp (e1, e2) -> rules e1 @ rules e2
| LLam (l, x, e) ->
let e' = cs_to_var e [ LVar x ] 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 p = term_to_pattern e [ LVar x ] in
let rhs = l_term_to_trsterm p in
let lhs = l_term_to_trsterm (LLam (l, x, p)) in
RR (TDes (lhs, TVar x), rhs) :: rules e
let rec _redexpos pos = function
| TDes (TCon (_, _), _) -> pos
......@@ -294,11 +278,7 @@ let rec _rewrite_step tterm rules pos p =
fvs )
| _ -> tterm
let rewrite_step xs t =
_rewrite_step t xs (redexpos t) _ROOT
let rewrite_step_at_pos xs t pos =
_rewrite_step t xs pos _ROOT
let rewrite_step xs t pos = _rewrite_step t xs pos _ROOT
let rec find_rule rules label =
match rules with
......@@ -314,23 +294,18 @@ let next_fresh_2 () =
"v" ^ string_of_int !counter_projection
let rec trsterm_to_lterm xs = function
| TVar x -> LVar x
| TDes (e1, e2) ->
LApp (trsterm_to_lterm xs e1, trsterm_to_lterm xs e2)
| TCon (l, tcs) -> (
let rule = find_rule xs l in
match rule with
| RR (TDes (TCon (_, rcs), var), r) ->
if
L.mem var
(L.flatten (L.map (fun f -> fvar_trsterm (fst f)) tcs))
then
let f = next_fresh_2 () in
let r' = subst r [ (var, TVar f) ] in
LLam (l, f, trsterm_to_lterm xs (subst r' (zip_cs rcs tcs)))
else
LLam
( l,
vtname var,
trsterm_to_lterm xs (subst r (zip_cs rcs tcs)))
| _ -> failwith "Not a RR found." )
| TVar x -> LVar x
| TDes (e1, e2) -> LApp (trsterm_to_lterm xs e1, trsterm_to_lterm xs e2)
| TCon (l, tcs) -> (
let rule = find_rule xs l in
match rule with
| RR (TDes (TCon (_, rcs), var), rhs) ->
if L.mem var (L.flatten (L.map (fun f -> fvar_trsterm (fst f)) tcs))
then
let f = next_fresh_2 () in
let r' = subst rhs [ (var, TVar f) ] in
LLam (l, f, trsterm_to_lterm xs (subst r' (zip_cs rcs tcs)))
else
LLam
(l, vtname var, trsterm_to_lterm xs (subst rhs (zip_cs rcs tcs)))
| _ -> failwith "No rule with such label." )
......@@ -55,14 +55,14 @@ let trs_rule_to_string term =
let rules_to_string xs = String.concat ".\n" (L.map trs_rule_to_string xs)
let trs_to_string xs t =
"TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string_nopos t
"TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string_nopos t
let rec _simulate_lterm_in_trs lterm rules tterm alltrue =
let pos = weak_redexpos lterm in
if pos <> "" then
let lterm' = weak_step_pos lterm pos in
let trsterm' = rewrite_step_at_pos rules tterm pos in
let trsterm'_lterm = trsterm_to_lterm rules trsterm' in
let lterm' = weak_step lterm pos in
let trsterm' = rewrite_step rules tterm pos in
let trsterm'_lterm = trsterm_to_lterm rules trsterm' in
let alpha_eq = default_names trsterm'_lterm = default_names lterm' in
let alltrue = alltrue && alpha_eq in
let str =
......@@ -78,7 +78,8 @@ let rec _simulate_lterm_in_trs lterm rules tterm alltrue =
in
str
::
(if lterm = lterm' then [] else _simulate_lterm_in_trs lterm' rules trsterm' alltrue)
( if lterm = lterm' then []
else _simulate_lterm_in_trs lterm' rules trsterm' alltrue )
else []
let simulate_lterm_in_trs lterm =
......@@ -91,4 +92,4 @@ let simulate_lterm_in_trs lterm =
let print_simulation lterm =
let sim = simulate_lterm_in_trs lterm in
Printf.printf "\n%s\n" sim
Printf.printf "%s" sim
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