Commit 861d340c authored by Samuel Frontull's avatar Samuel Frontull
Browse files

Merge branch 'master' into 'main'

Master

See merge request !6
parents 461c6fdf d98c5076
......@@ -19,45 +19,47 @@ let next_label () =
label := !label + 1;
"C" ^ string_of_int !label
type l_term =
| LVar of string
| LLam of string * string * l_term
| LApp of l_term * l_term
type var = string
let uniq_cons x xs = if L.mem x xs then xs else x :: xs
type label = string
let linear_list xs = L.fold_right uniq_cons xs []
(** labeled lambda term *)
type l_term =
| LVar of var
| LLam of label * var * l_term
| LApp of l_term * l_term
(* lift : term -> TRS *)
let rec term_to_l_term term =
match term with
(** lambda term to labeled lambda term *)
let rec term_to_l_term = function
| Var x -> LVar x
| Lam (x, e) ->
let l = next_label () in
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)
let rec rename_fv term x y =
(** 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_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
(** 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) ->
let vf = "x_" ^ pos in
LLam (l, vf, default_names_r (rename_fv t v vf) (pos ^ _LAM))
LLam (l, vf, default_names_r (pos ^ _LAM) (rename t v vf))
| LApp (e1, e2) ->
LApp (default_names_r e1 (pos ^ _APP_L), default_names_r e2 (pos ^ _APP_R))
LApp (default_names_r (pos ^ _APP_L) e1, default_names_r (pos ^ _APP_R) e2)
let default_names term = default_names_r term _ROOT
let default_names term = default_names_r _ROOT term
(** Extract the name of a variable from a {e a_term} *)
let lvname = function LVar n -> n | _ -> ""
......@@ -101,23 +103,25 @@ let rec _casubst m x n fvn =
let casubst m x n = _casubst m x n (L.map lvname (free_variables n))
let beta term =
match term with
(** 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) -> (
(* 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 "" *) )
if posl <> "" then posl else _weak_redexpos arg (pos ^ _APP_R) bvs )
| 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
......@@ -126,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) ->
......@@ -147,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
......@@ -155,11 +162,9 @@ 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 ]
(** 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
| TCon (_, fvs) -> L.flatten (L.map (fun x -> fvar_trsterm (fst x)) fvs)
......@@ -169,10 +174,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) ]
| [], _ ->
......@@ -184,135 +188,123 @@ 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 =
match lterm with
let rec l_term_to_trsterm = function
| LVar x -> TVar x
| 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 =
let rec _cs_to_var xs pos lterm =
if free_variables lterm = [] then LVar ("v_" ^ pos)
else
match lterm with
| LVar y -> if L.mem y xs then lterm else LVar ("v_" ^ pos)
| LVar _ -> if L.mem lterm 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 (free_variables e1) in
let e2_fvs = intersect xs (free_variables e2) in
match (e1_fvs, e2_fvs) with
| [], [] -> LVar ("v_" ^ pos)
| _, _ ->
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 (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 x lterm = _fvar_components_lterm [ x ] _ROOT lterm
let cs_to_var lterm xs = _cs_to_var xs _ROOT lterm
type trs_rule = RR of trs_term * trs_term
let rec rules lterm =
match lterm with
let rec rules = function
| LVar _ -> []
| LApp (e1, e2) -> rules e1 @ rules e2
| LLam (l, x, e) ->
let e' = fvar_components_lterm 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
type trs = TRS of trs_rule list * trs_term
let trs_rules = function TRS (xs, _) -> xs
let trs_term = function TRS (_, t) -> t
let l_term_to_trs x = TRS (rules x, l_term_to_trsterm x)
let rec _redexpos trsterm pos =
match trsterm with
let rec _redexpos pos = function
| TDes (TCon (_, _), _) -> pos
| TDes (e1, e2) ->
let posl = _redexpos e1 (pos ^ _APP_L) in
if posl != "" then posl else _redexpos e2 (pos ^ _APP_R)
| TCon (_, fvs) ->
if fvs = [] then ""
let posl = _redexpos (pos ^ _APP_L) e1 in
if posl != "" then posl else _redexpos (pos ^ _APP_R) e2
| TCon (_, tcs) ->
if tcs = [] then ""
else
let xs =
L.filter
(fun y -> y != "")
(L.map (fun x -> _redexpos (fst x) (pos ^ snd 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 trsterm _ROOT
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
| _, _ -> 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 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), x), r) :: xs, TDes (TCon (l2, tcs), arg) ->
if l1 = l2 then subst r ((x, arg) :: zip_cs rcs tcs) else rewrite xs term
| [], _ -> term
| _, _ -> failwith "Not a rule or not a trsterm redex."
let rec _rewrite_step 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) )
( _rewrite_step e1 rules pos (p ^ _APP_L),
_rewrite_step 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.map
(fun z -> (_rewrite_step (fst z) rules pos (p ^ snd z), snd z))
fvs )
| _ -> tterm
let rstep trs =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs (redexpos t) _ROOT)
let rewrite_step xs t =
_rewrite_step t xs (redexpos t) _ROOT
let rstep_pos trs pos =
match trs with TRS (xs, t) -> TRS (xs, _rstep t xs pos _ROOT)
let rewrite_step_at_pos xs t pos =
_rewrite_step t xs pos _ROOT
(* project : TRS -> term *)
let rec trs_rule trsrules label =
match trsrules with
let rec find_rule rules label =
match rules with
| RR (TDes (TCon (l, _), _), _) :: xs ->
if l = label then L.hd trsrules else trs_rule xs label
| _ :: xs -> trs_rule xs label
if l = label then L.hd rules else find_rule xs label
| _ :: xs -> find_rule xs label
| [] -> failwith "No rule with such label."
let counter_projection = ref 0
......@@ -321,41 +313,24 @@ let next_fresh_2 () =
counter_projection := !counter_projection + 1;
"v" ^ string_of_int !counter_projection
let rec trs_to_term trs =
(* Printf.printf "trstoterm: %s\n\n" (trs_to_string trs); *)
match trs with
| TRS (xs, t) -> (
match t with
| 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) ->
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." ) )
let rec trsterm_to_lterm xs = function
| TVar x -> LVar x
| TDes (e1, e2) ->
LApp (trsterm_to_lterm xs e1, trsterm_to_lterm xs e2)
| TCon (l, tcs) -> (
let rule = find_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)) tcs))
then
let f = next_fresh_2 () in
let r' = subst r [ (var, TVar f) ] in
LLam (l, f, trsterm_to_lterm xs (subst r' (zip_cs rcs tcs)))
else
LLam
( l,
vtname var,
trsterm_to_lterm xs (subst r (zip_cs rcs tcs)))
| _ -> failwith "Not a RR found." )
......@@ -29,21 +29,13 @@ let rec _l_term_to_string term c label =
let l_term_to_string term = _l_term_to_string term 0 false
let l_term_with_label_to_string term = _l_term_to_string term 0 true
let l_term_to_string_with_label term = _l_term_to_string term 0 true
let rec _trs_term_to_string term pp =
match term with
| TVar v -> v
| TDes (e1, e2) -> (
match (e1, e2) with
| TDes _, TDes _ ->
"(" ^ _trs_term_to_string e1 pp ^ ") (" ^ _trs_term_to_string e2 pp
^ ")"
| TDes _, _ ->
"(" ^ _trs_term_to_string e1 pp ^ ") " ^ _trs_term_to_string e2 pp
| _, TDes _ ->
_trs_term_to_string e1 pp ^ " (" ^ _trs_term_to_string e2 pp ^ ")"
| _, _ -> _trs_term_to_string e1 pp ^ " " ^ _trs_term_to_string e2 pp )
| TDes (e1, e2) ->
"D(" ^ _trs_term_to_string e1 pp ^ ", " ^ _trs_term_to_string e2 pp ^ ")"
| TCon (l, fvs) ->
let fun_lp x = "(" ^ _trs_term_to_string (fst x) pp ^ ")@" ^ snd x in
let fun_l x = _trs_term_to_string (fst x) pp in
......@@ -62,41 +54,40 @@ let trs_rule_to_string term =
let rules_to_string xs = String.concat ".\n" (L.map trs_rule_to_string xs)
let trs_to_string trs =
match trs with
| TRS (xs, t) ->
let trs_to_string xs t =
"TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string_nopos t
let rec _simulate_lterm_in_trs lterm trs alltrue =
let rec _simulate_lterm_in_trs lterm rules tterm alltrue =
let pos = weak_redexpos lterm in
if pos <> "" then
let lterm' = weak_step_pos lterm pos in
let trs' = rstep_pos trs pos in
let trs'_lterm = trs_to_term trs' in
let alpha_eq = default_names trs'_lterm = default_names lterm' in
let trsterm' = rewrite_step_at_pos rules tterm pos in
let trsterm'_lterm = trsterm_to_lterm rules trsterm' in
let alpha_eq = default_names trsterm'_lterm = default_names lterm' in
let alltrue = alltrue && alpha_eq in
let str =
"\n+++++ REDUCTION STEP @" ^ pos ^ " +++++\n\n" ^ l_term_to_string lterm
^ "\n->" ^ pos ^ "\n" ^ l_term_to_string lterm' ^ "\n\n"
^ trs_term_to_string_nopos (trs_term trs)
^ trs_term_to_string_nopos tterm
^ "\n->" ^ pos ^ "\n"
^ trs_term_to_string_nopos (trs_term trs')
^ trs_term_to_string_nopos trsterm'
^ "\n\nprojection to lambda term:\n"
^ l_term_to_string trs'_lterm
^ "\n\nalpha_eq: " ^ Bool.to_string alpha_eq ^ " ("
^ Bool.to_string alltrue ^ ")"
^ l_term_to_string trsterm'_lterm
^ "\n\nalpha_eq: " ^ Bool.to_string alpha_eq ^ "\nall steps alpha_eq: "
^ Bool.to_string alltrue
in
str
::
(if lterm = lterm' then [] else _simulate_lterm_in_trs lterm' trs' alltrue)
(if lterm = lterm' then [] else _simulate_lterm_in_trs lterm' rules trsterm' alltrue)
else []
let simulate_lterm_in_trs lterm =
let trs = l_term_to_trs lterm in
trs_to_string trs ^ "\n\n"
^ l_term_to_string (trs_to_term trs)
let rules = rules lterm in
let tterm = l_term_to_trsterm lterm in
trs_to_string rules tterm ^ "\n\n"
^ l_term_to_string (trsterm_to_lterm rules tterm)
^ "\n"
^ String.concat "\n\n" (_simulate_lterm_in_trs lterm trs true)
^ String.concat "\n\n" (_simulate_lterm_in_trs lterm rules tterm true)
let print_simulation lterm =
let sim = simulate_lterm_in_trs lterm in
......
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