io.ml 3.14 KB
Newer Older
Frontull Samuel's avatar
Frontull Samuel committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
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

Frontull Samuel's avatar
Frontull Samuel committed
32
let l_term_to_string_with_label term = _l_term_to_string term 0 true
Frontull Samuel's avatar
Frontull Samuel committed
33
34
35
36

let rec _trs_term_to_string term pp =
  match term with
  | TVar v -> v
Frontull Samuel's avatar
Frontull Samuel committed
37
38
  | TDes (e1, e2) ->
      "D(" ^ _trs_term_to_string e1 pp ^ ", " ^ _trs_term_to_string e2 pp ^ ")"
Frontull Samuel's avatar
Frontull Samuel committed
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
  | 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)

Frontull Samuel's avatar
Frontull Samuel committed
57
let trs_to_string xs t =
58
  "TRS:\n" ^ rules_to_string xs ^ ".\n----\n" ^ trs_term_to_string_nopos t
Frontull Samuel's avatar
Frontull Samuel committed
59

Frontull Samuel's avatar
Frontull Samuel committed
60
let rec _simulate_lterm_in_trs lterm rules tterm alltrue =
Frontull Samuel's avatar
Frontull Samuel committed
61
62
  let pos = weak_redexpos lterm in
  if pos <> "" then
63
64
65
    let lterm' = weak_step lterm pos in
    let trsterm' = rewrite_step rules tterm pos in
    let trsterm'_lterm = trsterm_to_lterm rules trsterm' in
Frontull Samuel's avatar
Frontull Samuel committed
66
    let alpha_eq = default_names trsterm'_lterm = default_names lterm' in
Frontull Samuel's avatar
Frontull Samuel committed
67
68
69
70
    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"
Frontull Samuel's avatar
Frontull Samuel committed
71
      ^ trs_term_to_string_nopos tterm
Frontull Samuel's avatar
Frontull Samuel committed
72
      ^ "\n->" ^ pos ^ "\n"
Frontull Samuel's avatar
Frontull Samuel committed
73
      ^ trs_term_to_string_nopos trsterm'
Frontull Samuel's avatar
Frontull Samuel committed
74
      ^ "\n\nprojection to lambda term:\n"
Frontull Samuel's avatar
Frontull Samuel committed
75
76
77
      ^ l_term_to_string trsterm'_lterm
      ^ "\n\nalpha_eq: " ^ Bool.to_string alpha_eq ^ "\nall steps alpha_eq: "
      ^ Bool.to_string alltrue
Frontull Samuel's avatar
Frontull Samuel committed
78
79
80
    in
    str
    ::
81
82
    ( if lterm = lterm' then []
    else _simulate_lterm_in_trs lterm' rules trsterm' alltrue )
Frontull Samuel's avatar
Frontull Samuel committed
83
84
85
  else []

let simulate_lterm_in_trs lterm =
Frontull Samuel's avatar
Frontull Samuel committed
86
87
88
89
  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)
Frontull Samuel's avatar
Frontull Samuel committed
90
  ^ "\n"
Frontull Samuel's avatar
Frontull Samuel committed
91
  ^ String.concat "\n\n" (_simulate_lterm_in_trs lterm rules tterm true)
Frontull Samuel's avatar
Frontull Samuel committed
92
93
94

let print_simulation lterm =
  let sim = simulate_lterm_in_trs lterm in
95
  Printf.printf "%s" sim