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

removed trs type

parent ba07c015
......@@ -226,14 +226,6 @@ let rec rules = function
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 pos = function
| TDes (TCon (_, _), _) -> pos
| TDes (e1, e2) ->
......@@ -282,31 +274,37 @@ let rec subst tterm s_pairs =
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
| 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."
| _, _ -> failwith "Not a rule or not a trsterm redex."
let rec _rstep tterm rules pos p =
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 rules pos (p ^ _APP_L), _rstep e2 rules pos (p ^ _APP_R))
TDes
( _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) rules pos (p ^ snd z), snd z)) fvs)
( l,
L.map
(fun z -> (_rewrite_step (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 rewrite_step xs t =
_rewrite_step t xs (redexpos t) _ROOT
let rstep_pos pos = function TRS (xs, t) -> TRS (xs, _rstep t xs pos _ROOT)
let rewrite_step_at_pos xs t pos =
_rewrite_step t xs pos _ROOT
let rec trs_rule rules label =
let rec find_rule rules label =
match rules with
| RR (TDes (TCon (l, _), _), _) :: xs ->
if l = label then L.hd rules 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
......@@ -315,27 +313,24 @@ let next_fresh_2 () =
counter_projection := !counter_projection + 1;
"v" ^ string_of_int !counter_projection
let rec trs_to_term = function
(* Printf.printf "trstoterm: %s\n\n" (trs_to_string trs); *)
| 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, 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)) tcs))
then
let f = next_fresh_2 () in
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 (zip_cs rcs tcs))) )
| _ -> 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 pos trs 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