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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
|
(****************** Equation manipulations *************)
open Prelude;;
open Terms;;
type rule = int * (int * (term * term));;
(* standardizes an equation so its variables are 1,2,... *)
let mk_rule m n =
let all_vars = union (vars m) (vars n) in
let (k,subst) =
List.fold_left
(fun (i, sigma) v -> (i + 1,(v, Var(i)) :: sigma)) (1, []) all_vars in
(k - 1, (substitute subst m, substitute subst n))
;;
(* checks that rules are numbered in sequence and returns their number *)
let (check_rules: rule list -> int) =
List.fold_left
(fun n (k, _) ->
if k = n + 1 then k else failwith "Rule numbers not in sequence") 0
;;
let pretty_rule (k,(_,(m,n)): rule) =
print_int k; print_string " : ";
pretty_term m; print_string " = "; pretty_term n;
print_newline()
;;
let pretty_rules = List.iter pretty_rule
;;
(****************** Rewriting **************************)
(* Top-level rewriting. Let eq:l=r be an equation, m be a term such that l<=m.
With sigma = matching l m, we define the image of m by eq as sigma(r) *)
let reduce l m =
substitute (matching l m)
;;
(* A more efficient version of can (rewrite1 (l, r)) for r arbitrary *)
let reducible l =
let rec redrec m =
try
let _ = matching l m in true
with Failure _ ->
match m with
| Term(_, sons) -> List.exists redrec sons
| _ -> false in
redrec
;;
(* mreduce : rules -> term -> term *)
let mreduce rules m =
let redex (_, (_, (l, r))) = reduce l m r in try_find redex rules
;;
(* One step of rewriting in leftmost-outermost strategy, with multiple rules *)
(* fails if no redex is found *)
(* mrewrite1 : rules -> term -> term *)
let mrewrite1 rules =
let rec rewrec m =
try
mreduce rules m
with Failure _ ->
let rec tryrec = function
| [] -> failwith "mrewrite1"
| son :: rest ->
try
rewrec son :: rest
with Failure _ ->
son :: tryrec rest in
match m with
| Term (f, sons) -> Term (f, tryrec sons)
| _ -> failwith "mrewrite1" in
rewrec
;;
(* Iterating rewrite1. Returns a normal form. May loop forever *)
(* mrewrite_all : rules -> term -> term *)
let mrewrite_all rules m =
let rec rew_loop m =
try
rew_loop(mrewrite1 rules m)
with Failure _ -> m in
rew_loop m
;;
(*
pretty_term (mrewrite_all Group_rules m where m,_=<<A*(I(B)*B)>>);;
==> A*U
*)
|
