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

formatting

parent 1b24bfb1
......@@ -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
......@@ -339,9 +331,9 @@ let rec simulate_trs_in_lterm trs =
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-> " ^ l_term_to_string lterm' ^ "\n\n"
^ trs_to_string trs' ^ "\n\n" ^ trs_to_string lterm'_trs )
( 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'
(*
......@@ -359,8 +351,8 @@ let rec simulate_lterm_in_trs lterm =
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-> "
( "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
......@@ -371,6 +363,7 @@ let rec 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 "%s\n\n++++++++++++++++\n++++++++++++++++\n++++++++++++++++\n\n%s\n"
Printf.printf
"%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