Commit 3878d8e5 authored by Samuel Frontull's avatar Samuel Frontull
Browse files

Merge branch 'master' into 'main'

Master

See merge request !4
parents 130e9597 b2a1b8ad
......@@ -11,4 +11,5 @@ let () =
let term =
try str_to_term (Sys.argv.(1) ^ "\n") with _ -> failwith "Syntax error"
in
Core.reduction_print term
let lterm = Core.term_to_l_term term in
Core.print_simulation lterm
......@@ -24,11 +24,6 @@ type l_term =
| LLam of string * l_term list * string * l_term
| LApp of l_term * l_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 _l_term_to_string term c =
match term with
| LVar v -> v
......@@ -47,8 +42,6 @@ let rec _l_term_to_string term c =
| _, _ ->
"(" ^ _l_term_to_string e1 c ^ ") (" ^ _l_term_to_string e2 c ^ ")" )
(* _term_to_string (l_term_to_term term) *)
let l_term_to_string term = _l_term_to_string term 0
(** Extract the name of a variable from a {e a_term} *)
......@@ -72,6 +65,11 @@ let rec term_to_l_term term =
LLam (l, fvs, x, term_to_l_term e)
| App (e1, e2) -> LApp (term_to_l_term e1, term_to_l_term e2)
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 =
match term with
| LVar s -> if s = x then LVar y else term
......@@ -266,9 +264,6 @@ let rec all_vars vs =
(* project : TRS -> term *)
let rec trs_rule trsrules label =
(* Printf.printf "---\ntrs_rule %s\n" label;
Printf.printf "trs_rules:\n %s\n---\n"
(String.concat "\n" (L.map trs_rule_to_string trsrules)); *)
match trsrules with
| RR (TDes (TCon (l, fvs), _), _) :: xs ->
if l = label && all_vars fvs then L.hd trsrules else trs_rule xs label
......@@ -282,7 +277,6 @@ let next_fresh_2 () =
"v" ^ string_of_int !counter_projection
let rec trs_to_term trs =
(* Printf.printf "trs_to_term\n"; *)
match trs with
| TRS (xs, t) -> (
match t with
......@@ -291,8 +285,6 @@ let rec trs_to_term trs =
LApp (trs_to_term (TRS (xs, e1)), trs_to_term (TRS (xs, e2)))
| TCon (label, fvs) -> (
let rr = trs_rule xs label in
(* Printf.printf "trs_rule rr:%s\n" (trs_rule_to_string rr);
Printf.printf "mapping term:%s\n" (trs_term_to_string t); *)
match rr with
| RR (TDes (TCon (_, fvs_r), var), r) ->
if L.mem var fvs then
......@@ -313,10 +305,9 @@ let rec trs_to_term trs =
| _ -> failwith "Not a RR found." ) )
let trs_to_string trs =
(* Printf.printf "%s\n" (trs_term_to_string (trs_term trs)); *)
match trs with
| TRS (xs, t) ->
"Rules:\n" ^ rules_to_string xs ^ ".\n\nTerm:\n" ^ trs_term_to_string t
"TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string t
let rec _weak_reduction term =
let wt = weak_step term in
......@@ -330,66 +321,49 @@ let rec _trs_reduction trs =
let trs_reduction trs = trs :: _trs_reduction trs
let prepend_index xs = L.mapi (fun i x -> "[" ^ string_of_int i ^ "] " ^ x) xs
let reduction_print term =
let l_term = term_to_l_term term in
let trs = l_term_to_trs l_term in
let weak_reductions = weak_reduction l_term in
let trs_reductions = trs_reduction trs in
let trs_reductions_t = L.map trs_term trs_reductions in
let bisim = L.combine weak_reductions trs_reductions in
let trs_str =
match trs with
| TRS (xs, t) ->
"Rules:\n" ^ rules_to_string xs ^ ".\n\nTerm:\n" ^ trs_term_to_string t
in
let rec simulate_trs_in_lterm trs =
match trs with
| TRS (_, t) ->
let pos = redexpos t in
let trs' = rstep_pos trs pos in
if t = trs_term trs' then []
else
let lterm = trs_to_term trs in
let lterm' = weak_step_pos lterm pos in
let lterm'_trs = l_term_to_trs lterm' in
( trs_to_string trs ^ "\n\n" ^ l_term_to_string lterm ^ "\n->" ^ pos
^ "\n" ^ l_term_to_string lterm' ^ "\n\n" ^ trs_to_string trs' ^ "\n\n"
^ trs_to_string lterm'_trs )
:: simulate_trs_in_lterm trs'
(*
trs ....... -> ...... trs'
^ |
| v
lterm ...... -> ...... lterm'
*)
let rec simulate_lterm_in_trs lterm =
let pos = weak_redexpos lterm in
let lterm' = weak_step_pos lterm pos in
if lterm = lterm' then []
else
let trs = l_term_to_trs lterm 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
( "lterm: " ^ l_term_to_string lterm ^ "\n\n" ^ trs_to_string trs ^ "\n->"
^ pos ^ "\n"
^ trs_term_to_string (trs_term trs')
^ "\n\ntrs'_lterm: "
^ l_term_to_string trs'_lterm
^ "\nlterm' : " ^ l_term_to_string lterm' ^ "\n\nalpha_eq: "
^ Bool.to_string alpha_eq )
:: simulate_lterm_in_trs lterm'
let print_simulation lterm =
let sim = simulate_lterm_in_trs lterm in
let sim2 = simulate_trs_in_lterm (l_term_to_trs lterm) in
Printf.printf
"\n\
%s\n\n\
-------[TRS]----------------\n\n\
%s\n\n\
-------[Reductions]---------\n\n\
LC:\n\
\ %s\n\n\
TRS:\n\
\ %s\n\n\
-------[Bisimulation]-------\n\n\
%s\n"
(l_term_to_string (trs_to_term trs))
trs_str
(String.concat " ->\n "
(prepend_index
(L.map _term_to_string (L.map l_term_to_term weak_reductions))))
(String.concat " ->\n "
(prepend_index (L.map trs_term_to_string trs_reductions_t)))
(String.concat "\n"
(L.mapi
(fun i (a_term, b_trs) ->
let a_term_default = a_term in
let a_term_trs = l_term_to_trs a_term_default in
let b_trs_term = trs_to_term b_trs in
(* let b_term_trs = l_term_to_trs b_trs_term in *)
let s =
if
l_term_to_string (default_names a_term)
= l_term_to_string (default_names b_trs_term)
&& trs_term a_term_trs = trs_term b_trs
then
"\n---------------------\n" ^ "TRS_" ^ string_of_int i ^ " ~ "
^ "LC_" ^ string_of_int i ^ "\n---------------------\n"
else
"\n---------------------\n" ^ "! TRS_" ^ string_of_int i
^ " ≁ " ^ "LC_" ^ string_of_int i
^ "\n---------------------\n"
in
s
^ l_term_to_string a_term_default
^ "\n\n" ^ trs_to_string a_term_trs
^ "\n\n++++++++++++++++++++++\n\n" ^ trs_to_string b_trs ^ "\n\n"
^ l_term_to_string b_trs_term
^ "\n\n"
(* ^ trs_to_string b_term_trs ^ "\n\n" *)
^ "=====================\n")
(* "LC_" ^ string_of_int i ^ " ~ " ^ "TRS_" ^ string_of_int i *)
bisim))
"%s\n\n++++++++++++++++\n++++++++++++++++\n++++++++++++++++\n\n%s\n"
(String.concat "\n\n========================\n\n" sim)
(String.concat "\n\n========================\n\n" sim2)
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