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

cleanup

parent 62e9e52b
......@@ -10,17 +10,9 @@ let _LAM = "1"
type term = Var of string | Lam of string * term | App of term * term
(** 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 () =
......@@ -36,8 +28,6 @@ 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 []
let fvars term = linear_list (_fvars term)
(* lift : term -> TRS *)
let rec term_to_l_term term =
match term with
......@@ -84,7 +74,7 @@ let next_fresh () =
counter := !counter + 1;
"p_" ^ string_of_int !counter
(** replace every var occurrence by fresh var *)
(** replace every var x occurrence by var y *)
let rec subst m x y =
match m with
| LVar z -> if z = x then LVar y else m
......@@ -113,9 +103,7 @@ 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) ->
let res = casubst m x n in
res
| LApp (LLam (_, x, m), n) -> casubst m x n
| _ -> failwith "beta: Not a redex."
let rec _weak_redexpos term pos bvs =
......@@ -175,8 +163,6 @@ let rec fvar_trsterm t =
| TDes (e1, e2) -> fvar_trsterm e1 @ fvar_trsterm e2
| TCon (_, fvs) -> L.flatten (L.map (fun x -> fvar_trsterm (fst x)) fvs)
let diff l1 l2 = List.filter (fun x -> not (List.mem x l2)) l1
let rec _components_lterm xs pos lterm =
if free_variables lterm = [] then [ (lterm, pos) ]
else
......@@ -243,10 +229,6 @@ let trs_rules = function TRS (xs, _) -> xs
let trs_term = function TRS (_, t) -> t
let term_to_trs x =
let lx = term_to_l_term x in
TRS (rules lx, l_term_to_trsterm lx)
let l_term_to_trs x = TRS (rules x, l_term_to_trsterm x)
let rec _redexpos trsterm pos =
......@@ -299,7 +281,6 @@ let rec rewrite trsrules trsterm =
match (trsrules, trsterm) with
| RR (TDes (TCon (l, fvs), TVar x), r) :: xs, TDes (TCon (l2, fvs2), arg) ->
if l = l2 then
(* subst r ((TVar x, arg) :: L.combine (L.map fst fvs) (L.map fst fvs2)) *)
subst r ((TVar x, arg) :: combine_fvs (L.map fst fvs) (L.map fst fvs2))
else rewrite xs trsterm
| [], _ -> trsterm
......@@ -352,25 +333,29 @@ let rec trs_to_term trs =
let rr = trs_rule xs l in
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))
)) )
if
L.mem var
(L.flatten (L.map (fun f -> fvar_trsterm (fst f)) 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
(combine_fvs (L.map fst fvs_r) (L.map fst fvs)) ))
)
else
LLam
( l,
vtname var,
trs_to_term
(TRS
( xs,
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