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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
(***********************************************************************)
(* *)
(* Objective Caml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. All rights reserved. This file is distributed *)
(* under the terms of the Q Public License version 1.0. *)
(* *)
(***********************************************************************)
(* $Id$ *)
(****************** Term manipulations *****************)
type term =
Var of int
| Term of string * term list
let rec union l1 l2 =
match l1 with
[] -> l2
| a::r -> if List.mem a l2 then union r l2 else a :: union r l2
let rec vars = function
Var n -> [n]
| Term(_,l) -> vars_of_list l
and vars_of_list = function
[] -> []
| t::r -> union (vars t) (vars_of_list r)
let rec substitute subst = function
Term(oper,sons) -> Term(oper, List.map (substitute subst) sons)
| Var(n) as t -> try List.assoc n subst with Not_found -> t
(* Term replacement: replace M u N is M[u<-N]. *)
let rec replace m u n =
match (u, m) with
[], _ -> n
| i::u, Term(oper, sons) -> Term(oper, replace_nth i sons u n)
| _ -> failwith "replace"
and replace_nth i sons u n =
match sons with
s::r -> if i = 1
then replace s u n :: r
else s :: replace_nth (i-1) r u n
| [] -> failwith "replace_nth"
(* Term matching. *)
let matching term1 term2 =
let rec match_rec subst t1 t2 =
match (t1, t2) with
Var v, _ ->
if List.mem_assoc v subst then
if t2 = List.assoc v subst then subst else failwith "matching"
else
(v, t2) :: subst
| Term(op1,sons1), Term(op2,sons2) ->
if op1 = op2
then List.fold_left2 match_rec subst sons1 sons2
else failwith "matching"
| _ -> failwith "matching" in
match_rec [] term1 term2
(* A naive unification algorithm. *)
let compsubst subst1 subst2 =
(List.map (fun (v,t) -> (v, substitute subst1 t)) subst2) @ subst1
let rec occurs n = function
Var m -> m = n
| Term(_,sons) -> List.exists (occurs n) sons
let rec unify term1 term2 =
match (term1, term2) with
Var n1, _ ->
if term1 = term2 then []
else if occurs n1 term2 then failwith "unify"
else [n1, term2]
| term1, Var n2 ->
if occurs n2 term1 then failwith "unify"
else [n2, term1]
| Term(op1,sons1), Term(op2,sons2) ->
if op1 = op2 then
List.fold_left2 (fun s t1 t2 -> compsubst (unify (substitute s t1)
(substitute s t2)) s)
[] sons1 sons2
else failwith "unify"
(* We need to print terms with variables independently from input terms
obtained by parsing. We give arbitrary names v1,v2,... to their variables.
*)
let infixes = ["+";"*"]
let rec pretty_term = function
Var n ->
print_string "v"; print_int n
| Term (oper,sons) ->
if List.mem oper infixes then begin
match sons with
[s1;s2] ->
pretty_close s1; print_string oper; pretty_close s2
| _ ->
failwith "pretty_term : infix arity <> 2"
end else begin
print_string oper;
match sons with
[] -> ()
| t::lt -> print_string "(";
pretty_term t;
List.iter (fun t -> print_string ","; pretty_term t) lt;
print_string ")"
end
and pretty_close = function
Term(oper, _) as m ->
if List.mem oper infixes then begin
print_string "("; pretty_term m; print_string ")"
end else
pretty_term m
| m ->
pretty_term m
|
