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

refactoring

parent a3724954
......@@ -255,15 +255,13 @@ let rec _components_lterm xs pos lterm =
@ _components_lterm xs (pos ^ _APP_R) e2 )
| LLam (_, y, e) -> _components_lterm (LVar y :: xs) (pos ^ _LAM) e
let rec _l_term_to_trsterm lterm xs =
let rec l_term_to_trsterm lterm =
match lterm with
| LVar x -> TVar x
| LApp (e1, e2) -> TDes (_l_term_to_trsterm e1 xs, _l_term_to_trsterm e2 xs)
| 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) xs, snd c)) cmps)
let l_term_to_trsterm lterm = _l_term_to_trsterm lterm []
TCon (l, L.map (fun c -> (l_term_to_trsterm (fst c), snd c)) cmps)
let rec _fvar_components_lterm xs pos lterm =
if free_variables lterm = [] then LVar ("v_" ^ pos)
......@@ -340,19 +338,21 @@ let rec _redexpos trsterm pos =
let redexpos trsterm = _redexpos trsterm _ROOT
let rec combine a b =
match a,b with
| TVar _, _ -> [(a,b)]
| TDes (a1, a2), TDes (b1, b2) ->
combine a1 b1 @ combine a2 b2
match (a, b) with
| TVar _, _ -> [ (a, b) ]
| TDes (a1, a2), TDes (b1, b2) -> combine a1 b1 @ combine a2 b2
| TCon (_, a1), TCon (_, b1) ->
L.flatten (L.map (fun x -> combine (fst x) (snd x)) (L.combine (L.map fst a1) (L.map fst b1)))
| _, _ -> failwith("combine not same structure.")
L.flatten
(L.map
(fun x -> combine (fst x) (snd x))
(L.combine (L.map fst a1) (L.map fst b1)))
| _, _ -> failwith "combine not same structure."
let rec combine_fvs fvs_r fvs =
match fvs_r, fvs with
match (fvs_r, fvs) with
| t :: ts, f :: fs -> combine t f @ combine_fvs ts fs
| [], [] -> []
| _, _ -> failwith("combine_fvs not same length.")
| _, _ -> failwith "combine_fvs not same length."
let rec search_pairs v f = function
| (x, n) :: xs -> if f v = f x then n else search_pairs v f xs
......@@ -422,26 +422,26 @@ let rec trs_to_term trs =
match rr with
| RR (TDes (TCon (_, fvs_r), var), r) ->
(* if L.mem var (L.map fst fvs) then
let f = next_fresh_2 () in
let rfresh = subst r [ (var, TVar f) ] in
LLam
( l,
f,
trs_to_term
(TRS
( xs,
subst rfresh
(L.combine (L.map fst fvs_r) (L.map fst fvs)) )) )
else *)
LLam
( l,
vtname var,
trs_to_term
(TRS
( xs,
(* subst r (L.combine (L.map fst fvs_r) (L.map fst fvs)) *)
subst r (combine_fvs (L.map fst fvs_r) (L.map fst fvs))
)) )
let f = next_fresh_2 () in
let rfresh = subst r [ (var, TVar f) ] in
LLam
( l,
f,
trs_to_term
(TRS
( xs,
subst rfresh
(L.combine (L.map fst fvs_r) (L.map fst fvs)) )) )
else *)
LLam
( l,
vtname var,
trs_to_term
(TRS
( xs,
(* subst r (L.combine (L.map fst fvs_r) (L.map fst fvs)) *)
subst r (combine_fvs (L.map fst fvs_r) (L.map fst fvs))
)) )
| _ -> failwith "Not a RR found." ) )
(*
......
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