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

refactoring

parent e450b42b
......@@ -19,9 +19,11 @@ let next_label () =
label := !label + 1;
"C" ^ string_of_int !label
type var = string
type l_term =
| LVar of string
| LLam of string * string * l_term
| LVar of var
| LLam of string * var * l_term
| LApp of l_term * l_term
let uniq_cons x xs = if L.mem x xs then xs else x :: xs
......@@ -42,18 +44,18 @@ 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)
let rec rename_fv term x y =
let rec rename 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)
| LApp (e1, e2) -> LApp (rename_fv e1 x y, rename_fv e2 x y)
| LLam (l, s, t) -> if s = x then term else LLam (l, s, rename t x y)
| LApp (e1, e2) -> LApp (rename e1 x y, rename e2 x y)
let rec default_names_r term pos =
match term with
| LVar v -> LVar v
| LLam (l, v, t) ->
let vf = "x_" ^ pos in
LLam (l, vf, default_names_r (rename_fv t v vf) (pos ^ _LAM))
LLam (l, vf, default_names_r (rename t v vf) (pos ^ _LAM))
| LApp (e1, e2) ->
LApp (default_names_r e1 (pos ^ _APP_L), default_names_r e2 (pos ^ _APP_R))
......@@ -106,18 +108,19 @@ let beta term =
| LApp (LLam (_, x, m), n) -> casubst m x n
| _ -> failwith "beta: Not a redex."
let intersect l1 l2 = L.filter (fun z -> L.mem z l2) l1
let rec _weak_redexpos term pos bvs =
match term with
| 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
let f_bvs = intersect fvs bvs in
match f_bvs with
| [] -> pos
| _ ->
let posl = _weak_redexpos (LLam (l, v, b)) (pos ^ _APP_L) bvs in
if posl <> "" then posl else _weak_redexpos arg (pos ^ _APP_R) bvs
(* if free_variables term = [] then pos else "" *) )
)
| LApp (e1, e2) ->
let posl = _weak_redexpos e1 (pos ^ _APP_L) bvs in
if posl <> "" then posl else _weak_redexpos e2 (pos ^ _APP_R) bvs
......@@ -155,8 +158,6 @@ type trs_term =
(** Extract the name of a variable from a {e a_term} *)
let vtname = function TVar n -> n | _ -> ""
let isvar = function TVar _ -> true | _ -> false
let rec fvar_trsterm t =
match t with
| TVar _ -> [ t ]
......@@ -169,10 +170,9 @@ let rec _components_lterm xs pos lterm =
match lterm with
| LVar _ -> if L.mem lterm xs then [] else [ (lterm, pos) ]
| LApp (e1, e2) -> (
(* check if abstracted variables occur in left argument *)
let e1_fvs = L.filter (fun z -> L.mem z (free_variables e1)) xs in
(* check if abstracted variables occur in right argument *)
let e2_fvs = L.filter (fun z -> L.mem z (free_variables e2)) xs in
(* check if abstracted variables occur in left/right argument *)
let e1_fvs = intersect xs (free_variables e1) in
let e2_fvs = intersect xs (free_variables e2) in
match (e1_fvs, e2_fvs) with
| [], [] -> [ (lterm, pos) ]
| [], _ ->
......@@ -190,7 +190,7 @@ let rec l_term_to_trsterm lterm =
| 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
TCon (l, L.map (fun c -> (l_term_to_trsterm (fst c), snd c)) cmps)
TCon (l, L.map (fun (t,p) -> (l_term_to_trsterm t, p)) cmps)
let rec _fvar_components_lterm xs pos lterm =
if free_variables lterm = [] then LVar ("v_" ^ pos)
......@@ -198,18 +198,21 @@ let rec _fvar_components_lterm xs pos lterm =
match lterm with
| LVar y -> if L.mem y xs then lterm else LVar ("v_" ^ pos)
| LApp (e1, e2) -> (
let e1' = _fvar_components_lterm xs (pos ^ _APP_L) e1 in
let e2' = _fvar_components_lterm xs (pos ^ _APP_R) e2 in
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') )
let e1_fvs = intersect xs (L.map lvname (free_variables e1)) in
let e2_fvs = intersect xs (L.map lvname (free_variables e2)) in
match (e1_fvs, e2_fvs) with
| [], [] -> LVar ("v_" ^ pos)
| _, _ ->
let e1' = _fvar_components_lterm xs (pos ^ _APP_L) e1 in
let e2' = _fvar_components_lterm xs (pos ^ _APP_R) e2 in
LApp (e1', e2')
)
| LLam (l, y, e) ->
let e' = _fvar_components_lterm (y :: xs) (pos ^ _LAM) e in
LLam (l, y, e')
let fvar_components_lterm x lterm = _fvar_components_lterm [ x ] _ROOT lterm
let fvar_components_lterm x lterm =
_fvar_components_lterm [ x ] _ROOT lterm
type trs_rule = RR of trs_term * trs_term
......
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