Commit 62e9e52b authored by Frontull Samuel's avatar Frontull Samuel
Browse files

new file for io functions

parent a13877f8
......@@ -12,4 +12,4 @@ let () =
try str_to_term (Sys.argv.(1) ^ "\n") with _ -> failwith "Syntax error"
in
let lterm = Core.term_to_l_term term in
Core.print_simulation lterm
Io.print_simulation lterm
......@@ -32,37 +32,6 @@ type l_term =
| LLam of string * string * l_term
| LApp of l_term * l_term
let rec _l_term_to_string term c label =
match term with
| LVar v -> v
| LLam (l, v, t) ->
if label then "λ" ^ v ^ "_" ^ l ^ "." ^ _l_term_to_string t (c + 1) label
else "λ" ^ v ^ "." ^ _l_term_to_string t (c + 1) label
| LApp (e1, e2) -> (
match (e1, e2) with
| LVar _, LVar _ ->
_l_term_to_string e1 c label ^ " " ^ _l_term_to_string e2 c label
| LVar _, _ ->
_l_term_to_string e1 c label
^ " ("
^ _l_term_to_string e2 c label
^ ")"
| _, LVar _ ->
"("
^ _l_term_to_string e1 c label
^ ") "
^ _l_term_to_string e2 c label
| _, _ ->
"("
^ _l_term_to_string e1 c label
^ ") ("
^ _l_term_to_string e2 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 uniq_cons x xs = if L.mem x xs then xs else x :: xs
let linear_list xs = L.fold_right uniq_cons xs []
......@@ -200,32 +169,6 @@ let vtname = function TVar n -> n | _ -> ""
let isvar = function TVar _ -> true | _ -> false
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 )
| 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
if fvs = [] then l
else if pp then l ^ "[" ^ String.concat "," (L.map fun_lp fvs) ^ "]"
else l ^ "[" ^ String.concat "," (L.map fun_l fvs) ^ "]"
let trs_term_to_string term = _trs_term_to_string term true
let trs_term_to_string_nopos term = _trs_term_to_string term false
let term_print term = Printf.printf "%s" (trs_term_to_string term)
let rec fvar_trsterm t =
match t with
| TVar _ -> [ t ]
......@@ -294,20 +237,8 @@ let rec rules lterm =
let trsterm_t = l_term_to_trsterm (LLam (l, x, e')) in
RR (TDes (trsterm_t, TVar x), e_t) :: rules e
let trs_rule_to_string term =
match term with
| RR (l, r) ->
trs_term_to_string_nopos l ^ " -> " ^ trs_term_to_string_nopos r
let rules_to_string xs = String.concat ".\n" (L.map trs_rule_to_string xs)
type trs = TRS of trs_rule list * trs_term
let trs_to_string trs =
match trs with
| TRS (xs, t) ->
"TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string_nopos t
let trs_rules = function TRS (xs, _) -> xs
let trs_term = function TRS (_, t) -> t
......@@ -443,44 +374,3 @@ let rec trs_to_term trs =
subst r (combine_fvs (L.map fst fvs_r) (L.map fst fvs))
)) )
| _ -> failwith "Not a RR found." ) )
(*
trs ....... -> ...... trs'
^ |
| v
lterm ...... -> ...... lterm'
*)
let rec _simulate_lterm_in_trs lterm trs 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 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)
^ "\n->" ^ pos ^ "\n"
^ trs_term_to_string_nopos (trs_term trs')
^ "\n\nprojection to lambda term:\n"
^ l_term_to_string trs'_lterm
^ "\n\nalpha_eq: " ^ Bool.to_string alpha_eq ^ " ("
^ Bool.to_string alltrue ^ ")"
in
str
::
(if lterm = lterm' then [] else _simulate_lterm_in_trs lterm' trs' 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)
^ "\n"
^ String.concat "\n\n" (_simulate_lterm_in_trs lterm trs true)
let print_simulation lterm =
let sim = simulate_lterm_in_trs lterm in
Printf.printf "\n%s\n" sim
open Core
let rec _l_term_to_string term c label =
match term with
| LVar v -> v
| LLam (l, v, t) ->
if label then "λ" ^ v ^ "_" ^ l ^ "." ^ _l_term_to_string t (c + 1) label
else "λ" ^ v ^ "." ^ _l_term_to_string t (c + 1) label
| LApp (e1, e2) -> (
match (e1, e2) with
| LVar _, LVar _ ->
_l_term_to_string e1 c label ^ " " ^ _l_term_to_string e2 c label
| LVar _, _ ->
_l_term_to_string e1 c label
^ " ("
^ _l_term_to_string e2 c label
^ ")"
| _, LVar _ ->
"("
^ _l_term_to_string e1 c label
^ ") "
^ _l_term_to_string e2 c label
| _, _ ->
"("
^ _l_term_to_string e1 c label
^ ") ("
^ _l_term_to_string e2 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 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 )
| 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
if fvs = [] then l
else if pp then l ^ "[" ^ String.concat "," (L.map fun_lp fvs) ^ "]"
else l ^ "[" ^ String.concat "," (L.map fun_l fvs) ^ "]"
let trs_term_to_string term = _trs_term_to_string term true
let trs_term_to_string_nopos term = _trs_term_to_string term false
let trs_rule_to_string term =
match term with
| RR (l, r) ->
trs_term_to_string_nopos l ^ " -> " ^ trs_term_to_string_nopos r
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) ->
"TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string_nopos t
let rec _simulate_lterm_in_trs lterm trs 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 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)
^ "\n->" ^ pos ^ "\n"
^ trs_term_to_string_nopos (trs_term trs')
^ "\n\nprojection to lambda term:\n"
^ l_term_to_string trs'_lterm
^ "\n\nalpha_eq: " ^ Bool.to_string alpha_eq ^ " ("
^ Bool.to_string alltrue ^ ")"
in
str
::
(if lterm = lterm' then [] else _simulate_lterm_in_trs lterm' trs' 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)
^ "\n"
^ String.concat "\n\n" (_simulate_lterm_in_trs lterm trs true)
let print_simulation lterm =
let sim = simulate_lterm_in_trs lterm in
Printf.printf "\n%s\n" sim
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