Commit 0ede555c authored by Frontull Samuel's avatar Frontull Samuel
Browse files

removed list of fvs in lterm

parent d190881a
......@@ -16,6 +16,17 @@ let rec _term_to_string term =
| _, Var _ -> "(" ^ _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 | _ -> ""
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
let label = ref 0
let next_label () =
......@@ -24,16 +35,14 @@ let next_label () =
type l_term =
| LVar of string
| LLam of string * l_term list * string * l_term
| LLam of string * string * l_term
| LApp of l_term * l_term
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)
^ "]."
| LLam (l, v, t) ->
"λ" ^ v ^ "_" ^ l
^ _l_term_to_string t (c + 1)
| LApp (e1, e2) -> (
match (e1, e2) with
......@@ -47,17 +56,6 @@ let rec _l_term_to_string term c =
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
let uniq_cons x xs = if L.mem x xs then xs else x :: xs
let linear_list xs = L.fold_right uniq_cons xs []
......@@ -70,29 +68,27 @@ let rec term_to_l_term term =
| 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)
LLam (l, x, term_to_l_term e)
| App (e1, e2) -> LApp (term_to_l_term e1, term_to_l_term e2)
let rec l_term_to_term = function
| LVar v -> Var v
| LLam (_, _, v, t) -> Lam (v, l_term_to_term t)
| 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 rename_fv term x y =
match term with
| LVar s -> if s = x then LVar y else term
| LLam (l, fvs, s, t) ->
let fvs' = L.map (fun t -> rename_fv t x y) fvs in
if s = x then term else LLam (l, fvs', 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 =
match term with
| LVar v -> LVar v
| LLam (l, _, v, t) ->
| LLam (l, v, t) ->
let vf = "x_" ^ pos in
LLam (l, [], vf, default_names_r (rename_fv t v vf) (pos ^ "0"))
LLam (l, 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"))
......@@ -104,7 +100,7 @@ let lvname = function LVar n -> n | _ -> ""
(** 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) lvname x
| LApp (e1, e2) -> free_variables e1 @ free_variables e2
let counter = ref 0
......@@ -117,27 +113,23 @@ let next_fresh () =
let rec subst m x y =
match m with
| LVar z -> if z = x then LVar y else m
| LLam (l, fvs, z, e) ->
| LLam (l, z, e) ->
let z' = if z = x then y else z in
let fvs' = L.map (fun t -> subst t x y) fvs in
LLam (l, fvs', z', subst e x y)
LLam (l, 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
| LVar y -> if x = y then n else m
| LLam (l, fvs, y, e) -> (
| LLam (l, y, e) -> (
if y = x then m
else
(* get intersection of fvn and fvs variable names *)
(* let fvs_vars = L.map lvname (L.flatten (L.map free_variables fvs)) in
let inters = List.filter (fun x -> List.mem x (y :: fvs_vars)) fvn in *)
let inters = List.filter (fun x -> x = y) fvn in
match inters with
| [] ->
LLam
(l, L.map (fun z -> _casubst z x n fvn) fvs, y, _casubst e x n fvn)
(l, y, _casubst e x n fvn)
| hd :: _ ->
let f = next_fresh () in
let m' = subst m hd f in
......@@ -148,28 +140,28 @@ let casubst m x n = _casubst m x n (L.map lvname (free_variables n))
let beta term =
match term with
| LApp (LLam (_, _, 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
| LApp (LLam (_, _, _, _), _) -> if free_variables term = [] then pos else ""
| LApp (LLam (_, _, _), _) -> 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")
| LLam (_, _, e) -> _weak_redexpos e (pos ^ "1")
| _ -> ""
let weak_redexpos term = _weak_redexpos term "e"
let rec _weak_step term pos p =
match term with
| LApp (LLam (_, _, _, _), _) -> if p = pos then beta term else term
| 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"))
| LLam (l, f, x, e) -> LLam (l, f, x, _weak_step e pos (p ^ "1"))
| LLam (l, x, e) -> LLam (l, x, _weak_step e pos (p ^ "1"))
| _ -> term
let weak_step term = _weak_step term (weak_redexpos term) "e"
......@@ -246,7 +238,7 @@ let rec l_term_to_trsterm lterm =
match lterm with
| LVar x -> TVar x
| LApp (e1, e2) -> TDes (l_term_to_trsterm e1, l_term_to_trsterm e2)
| LLam (l, _, x, e) ->
| 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)
......@@ -260,9 +252,9 @@ let rec _components_lterm xs pos lterm =
let e1' = _components_lterm xs (pos ^ "1") e1 in
let e2' = _components_lterm xs (pos ^ "2") e2 in
LApp (e1', e2')
| LLam (l, fvs, y, e) ->
| LLam (l, y, e) ->
let e' = _components_lterm (y :: xs) (pos ^ "1") e in
LLam (l, fvs, y, e')
LLam (l, y, e')
let components_lterm x lterm = _components_lterm [ x ] "e" lterm
......@@ -301,10 +293,10 @@ let rec rules lterm =
match lterm with
| LVar _ -> []
| LApp (e1, e2) -> rules e1 @ rules e2
| LLam (l, f, x, e) ->
| 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, f, x, 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)
......@@ -423,8 +415,6 @@ let rec trs_to_term trs =
let rfresh = subst r [ (var, TVar fresh) ] in
LLam
( label,
L.map trs_to_term
(L.map (fun st -> TRS (xs, st)) (L.map fst fvs)),
fresh,
trs_to_term
(TRS
......@@ -434,8 +424,6 @@ let rec trs_to_term trs =
else
LLam
( label,
L.map trs_to_term
(L.map (fun st -> TRS (xs, st)) (L.map fst fvs)),
vtname var,
trs_to_term
(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