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

refactoring and some documentation

parent 3968cb1b
......@@ -21,16 +21,15 @@ let next_label () =
type var = string
type label = string
(** labeled lambda term *)
type l_term =
| LVar of var
| LLam of string * var * l_term
| LLam of label * var * l_term
| LApp of l_term * l_term
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 []
(* lift : term -> TRS *)
(** lambda term to labeled lambda term *)
let rec term_to_l_term = function
| Var x -> LVar x
| Lam (x, e) ->
......@@ -38,17 +37,20 @@ let rec term_to_l_term = function
LLam (l, 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 *)
let rec l_term_to_term = function
| LVar v -> Var v
| 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} *)
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 t x y)
| LApp (e1, e2) -> LApp (rename e1 x y, rename e2 x y)
(** assign default names (depending on the position of their binder) to each variable *)
let rec default_names_r pos = function
| LVar v -> LVar v
| LLam (l, v, t) ->
......@@ -101,12 +103,15 @@ let rec _casubst m x n fvn =
let casubst m x n = _casubst m x n (L.map lvname (free_variables n))
(** apply a beta step *)
let beta = function
| LApp (LLam (_, x, m), n) -> casubst m x n
| _ -> failwith "beta: Not a redex."
(** compute the intersection of the lists {e l1} and {e l2} *)
let intersect l1 l2 = L.filter (fun z -> L.mem z l2) l1
(** determine a position of a weak redex in {e term} *)
let rec _weak_redexpos term pos bvs =
match term with
| LApp (LLam (l, v, b), arg) -> (
......@@ -125,11 +130,13 @@ let rec _weak_redexpos term pos bvs =
let weak_redexpos term = _weak_redexpos term _ROOT []
(** check whether {e p} is a prefix of the string {e s} *)
let starts_with p s =
if String.length p <= String.length s then
String.sub s 0 (String.length p) = p
else false
(** compute a weak reduction step at position {e pos} *)
let rec _weak_step term pos p =
match term with
| LApp (LLam (l, v, b), arg) ->
......@@ -146,6 +153,7 @@ let weak_step term = _weak_step term (weak_redexpos term) _ROOT
let weak_step_pos term pos = _weak_step term pos _ROOT
(** TRS term *)
type trs_term =
| TVar of string
| TCon of string * (trs_term * string) list
......@@ -154,6 +162,7 @@ type trs_term =
(** Extract the name of a variable from a {e a_term} *)
let vtname = function TVar n -> n | _ -> ""
(** compute free variables in a {e trs_term} *)
let rec fvar_trsterm = function
| TVar v -> [ TVar v ]
| TDes (e1, e2) -> fvar_trsterm e1 @ fvar_trsterm e2
......@@ -186,7 +195,7 @@ let rec l_term_to_trsterm = function
let cmps = _components_lterm [ LVar x ] _LAM e in
TCon (l, L.map (fun (t, p) -> (l_term_to_trsterm t, p)) cmps)
let rec _fvar_components_lterm xs pos lterm =
let rec _cs_to_var xs pos lterm =
if free_variables lterm = [] then LVar ("v_" ^ pos)
else
match lterm with
......@@ -197,14 +206,14 @@ let rec _fvar_components_lterm xs pos lterm =
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
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' = _fvar_components_lterm (LVar y :: xs) (pos ^ _LAM) e in
let e' = _cs_to_var (LVar y :: xs) (pos ^ _LAM) e in
LLam (l, y, e')
let fvar_components_lterm xs lterm = _fvar_components_lterm xs _ROOT lterm
let cs_to_var lterm xs = _cs_to_var xs _ROOT lterm
type trs_rule = RR of trs_term * trs_term
......@@ -212,7 +221,7 @@ let rec rules = function
| LVar _ -> []
| LApp (e1, e2) -> rules e1 @ rules e2
| LLam (l, x, e) ->
let e' = fvar_components_lterm [ LVar x ] e in
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
......@@ -230,79 +239,73 @@ let rec _redexpos pos = function
| TDes (e1, e2) ->
let posl = _redexpos (pos ^ _APP_L) e1 in
if posl != "" then posl else _redexpos (pos ^ _APP_R) e2
| TCon (_, fvs) ->
if fvs = [] then ""
| TCon (_, tcs) ->
if tcs = [] then ""
else
let xs =
L.filter
(fun y -> y != "")
(L.map (fun x -> _redexpos (pos ^ snd x) (fst x)) fvs)
(L.map (fun x -> _redexpos (pos ^ snd x) (fst x)) tcs)
in
if L.length xs > 0 then L.hd xs else ""
| _ -> ""
let redexpos trsterm = _redexpos _ROOT trsterm
let rec combine a b =
let rec zip_c a b =
match (a, b) with
| TVar _, _ -> [ (a, b) ]
| TDes (a1, a2), TDes (b1, b2) -> combine a1 b1 @ combine a2 b2
| TDes (a1, a2), TDes (b1, b2) -> zip_c a1 b1 @ zip_c a2 b2
| TCon (_, a1), TCon (_, b1) ->
L.flatten
(L.map
(fun x -> combine (fst x) (snd x))
(fun x -> zip_c (fst x) (snd x))
(L.combine (L.map fst a1) (L.map fst b1)))
| _, _ -> failwith "combine not same structure."
| _, _ -> failwith "zip_c not same structure."
let rec combine_fvs fvs_r fvs =
match (fvs_r, fvs) with
| t :: ts, f :: fs -> combine t f @ combine_fvs ts fs
let rec zip_cs rcs tcs =
match (rcs, tcs) with
| r :: rs, t :: ts -> zip_c (fst r) (fst t) @ zip_cs rs ts
| [], [] -> []
| _, _ -> failwith "combine_fvs not same length."
| _, _ -> failwith "zip_cs 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
let rec subst_var v = function
| (x, n) :: xs -> if v = x then n else subst_var v xs
| [] -> v
let rec subst m pairs =
match m with
| TVar _ -> search_pairs m vtname pairs
| TDes (e1, e2) -> TDes (subst e1 pairs, subst e2 pairs)
| TCon (l, fvs) -> TCon (l, L.map (fun z -> (subst (fst z) pairs, snd z)) fvs)
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) :: combine_fvs (L.map fst fvs) (L.map fst fvs2))
else rewrite xs trsterm
| [], _ -> trsterm
let rec subst tterm s_pairs =
match tterm with
| TVar _ -> subst_var tterm s_pairs
| TDes (e1, e2) -> TDes (subst e1 s_pairs, subst e2 s_pairs)
| TCon (l, tcs) ->
TCon (l, L.map (fun z -> (subst (fst z) s_pairs, snd z)) tcs)
let rec rewrite rules term =
match (rules, term) with
| RR (TDes (TCon (l1, rcs), TVar x), r) :: xs, TDes (TCon (l2, tcs), arg) ->
if l1 = l2 then subst r ((TVar x, arg) :: zip_cs rcs tcs)
else rewrite xs term
| [], _ -> term
| _, _ -> failwith "Not a rule or not a trsterm."
let rec _rstep trsterm trsrules pos p =
match trsterm with
| TDes (TCon (_, _), _) ->
if p = pos then rewrite trsrules trsterm else trsterm
let rec _rstep tterm rules pos p =
match tterm with
| TDes (TCon (_, _), _) -> if p = pos then rewrite rules tterm else tterm
| TDes (e1, e2) ->
TDes
( _rstep e1 trsrules pos (p ^ _APP_L),
_rstep e2 trsrules pos (p ^ _APP_R) )
TDes (_rstep e1 rules pos (p ^ _APP_L), _rstep e2 rules pos (p ^ _APP_R))
| TCon (l, fvs) ->
TCon
( l,
L.map (fun z -> (_rstep (fst z) trsrules pos (p ^ snd z), snd z)) fvs
)
| _ -> trsterm
(l, L.map (fun z -> (_rstep (fst z) rules pos (p ^ snd z), snd z)) fvs)
| _ -> tterm
let rstep = function TRS (xs, t) -> TRS (xs, _rstep t xs (redexpos t) _ROOT)
let rstep_pos pos = function TRS (xs, t) -> TRS (xs, _rstep t xs pos _ROOT)
(* project : TRS -> term *)
let rec trs_rule trsrules label =
match trsrules with
let rec trs_rule rules label =
match rules with
| RR (TDes (TCon (l, _), _), _) :: xs ->
if l = label then L.hd trsrules else trs_rule xs label
if l = label then L.hd rules else trs_rule xs label
| _ :: xs -> trs_rule xs label
| [] -> failwith "No rule with such label."
......@@ -319,33 +322,20 @@ let rec trs_to_term = function
| TVar x -> LVar x
| TDes (e1, e2) ->
LApp (trs_to_term (TRS (xs, e1)), trs_to_term (TRS (xs, e2)))
| TCon (l, fvs) -> (
let rr = trs_rule xs l in
match rr with
| RR (TDes (TCon (_, fvs_r), var), r) ->
| TCon (l, tcs) -> (
let rule = trs_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)) fvs))
(L.flatten (L.map (fun f -> fvar_trsterm (fst f)) tcs))
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)) ))
)
let r' = subst r [ (var, TVar f) ] in
LLam (l, f, trs_to_term (TRS (xs, subst r' (zip_cs rcs tcs))))
else
LLam
( l,
vtname var,
trs_to_term
(TRS
( xs,
subst r
(combine_fvs (L.map fst fvs_r) (L.map fst fvs)) ))
)
trs_to_term (TRS (xs, subst r (zip_cs rcs tcs))) )
| _ -> 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