author | wenzelm |
Wed, 20 Jun 2007 22:07:52 +0200 | |
changeset 23442 | 028e39e5e8f3 |
child 23510 | 4521fead5609 |
permissions | -rw-r--r-- |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
1 |
(* ========================================================================= *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
2 |
(* MATCHING AND UNIFICATION FOR SETS OF FIRST ORDER LOGIC TERMS *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
3 |
(* Copyright (c) 2001-2006 Joe Hurd, distributed under the GNU GPL version 2 *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
4 |
(* ========================================================================= *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
5 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
6 |
structure TermNet :> TermNet = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
7 |
struct |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
8 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
9 |
open Useful; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
10 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
11 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
12 |
(* Quotient terms *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
13 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
14 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
15 |
datatype qterm = VAR | FN of NameArity.nameArity * qterm list; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
16 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
17 |
fun termToQterm (Term.Var _) = VAR |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
18 |
| termToQterm (Term.Fn (f,l)) = FN ((f, length l), map termToQterm l); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
19 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
20 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
21 |
fun qm [] = true |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
22 |
| qm ((VAR,_) :: rest) = qm rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
23 |
| qm ((FN _, VAR) :: _) = false |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
24 |
| qm ((FN (f,a), FN (g,b)) :: rest) = f = g andalso qm (zip a b @ rest); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
25 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
26 |
fun matchQtermQterm qtm qtm' = qm [(qtm,qtm')]; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
27 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
28 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
29 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
30 |
fun qm [] = true |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
31 |
| qm ((VAR,_) :: rest) = qm rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
32 |
| qm ((FN _, Term.Var _) :: _) = false |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
33 |
| qm ((FN ((f,n),a), Term.Fn (g,b)) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
34 |
f = g andalso n = length b andalso qm (zip a b @ rest); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
35 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
36 |
fun matchQtermTerm qtm tm = qm [(qtm,tm)]; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
37 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
38 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
39 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
40 |
fun qn qsub [] = SOME qsub |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
41 |
| qn qsub ((Term.Var v, qtm) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
42 |
(case NameMap.peek qsub v of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
43 |
NONE => qn (NameMap.insert qsub (v,qtm)) rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
44 |
| SOME qtm' => if qtm = qtm' then qn qsub rest else NONE) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
45 |
| qn _ ((Term.Fn _, VAR) :: _) = NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
46 |
| qn qsub ((Term.Fn (f,a), FN ((g,n),b)) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
47 |
if f = g andalso length a = n then qn qsub (zip a b @ rest) else NONE; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
48 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
49 |
fun matchTermQterm qsub tm qtm = qn qsub [(tm,qtm)]; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
50 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
51 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
52 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
53 |
fun qv VAR x = x |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
54 |
| qv x VAR = x |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
55 |
| qv (FN (f,a)) (FN (g,b)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
56 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
57 |
val _ = f = g orelse raise Error "TermNet.qv" |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
58 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
59 |
FN (f, zipwith qv a b) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
60 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
61 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
62 |
fun qu qsub [] = qsub |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
63 |
| qu qsub ((VAR, _) :: rest) = qu qsub rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
64 |
| qu qsub ((qtm, Term.Var v) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
65 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
66 |
val qtm = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
67 |
case NameMap.peek qsub v of NONE => qtm | SOME qtm' => qv qtm qtm' |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
68 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
69 |
qu (NameMap.insert qsub (v,qtm)) rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
70 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
71 |
| qu qsub ((FN ((f,n),a), Term.Fn (g,b)) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
72 |
if f = g andalso n = length b then qu qsub (zip a b @ rest) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
73 |
else raise Error "TermNet.qu"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
74 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
75 |
fun unifyQtermQterm qtm qtm' = total (qv qtm) qtm'; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
76 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
77 |
fun unifyQtermTerm qsub qtm tm = total (qu qsub) [(qtm,tm)]; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
78 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
79 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
80 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
81 |
fun qtermToTerm VAR = Term.Var "" |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
82 |
| qtermToTerm (FN ((f,_),l)) = Term.Fn (f, map qtermToTerm l); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
83 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
84 |
val ppQterm = Parser.ppMap qtermToTerm Term.pp; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
85 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
86 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
87 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
88 |
(* A type of term sets that can be efficiently matched and unified. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
89 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
90 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
91 |
type parameters = {fifo : bool}; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
92 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
93 |
datatype 'a net = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
94 |
RESULT of 'a list |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
95 |
| SINGLE of qterm * 'a net |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
96 |
| MULTIPLE of 'a net option * 'a net NameArityMap.map; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
97 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
98 |
datatype 'a termNet = NET of parameters * int * (int * (int * 'a) net) option; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
99 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
100 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
101 |
(* Basic operations. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
102 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
103 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
104 |
fun new parm = NET (parm,0,NONE); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
105 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
106 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
107 |
fun computeSize (RESULT l) = length l |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
108 |
| computeSize (SINGLE (_,n)) = computeSize n |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
109 |
| computeSize (MULTIPLE (vs,fs)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
110 |
NameArityMap.foldl |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
111 |
(fn (_,n,acc) => acc + computeSize n) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
112 |
(case vs of SOME n => computeSize n | NONE => 0) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
113 |
fs; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
114 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
115 |
fun netSize NONE = NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
116 |
| netSize (SOME n) = SOME (computeSize n, n); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
117 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
118 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
119 |
fun size (NET (_,_,NONE)) = 0 |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
120 |
| size (NET (_, _, SOME (i,_))) = i; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
121 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
122 |
fun null net = size net = 0; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
123 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
124 |
fun singles qtms a = foldr SINGLE a qtms; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
125 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
126 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
127 |
fun pre NONE = (0,NONE) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
128 |
| pre (SOME (i,n)) = (i, SOME n); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
129 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
130 |
fun add (RESULT l) [] (RESULT l') = RESULT (l @ l') |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
131 |
| add a (input1 as qtm :: qtms) (SINGLE (qtm',n)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
132 |
if qtm = qtm' then SINGLE (qtm, add a qtms n) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
133 |
else add a input1 (add n [qtm'] (MULTIPLE (NONE, NameArityMap.new ()))) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
134 |
| add a (VAR :: qtms) (MULTIPLE (vs,fs)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
135 |
MULTIPLE (SOME (oadd a qtms vs), fs) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
136 |
| add a (FN (f,l) :: qtms) (MULTIPLE (vs,fs)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
137 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
138 |
val n = NameArityMap.peek fs f |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
139 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
140 |
MULTIPLE (vs, NameArityMap.insert fs (f, oadd a (l @ qtms) n)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
141 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
142 |
| add _ _ _ = raise Bug "TermNet.insert: Match" |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
143 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
144 |
and oadd a qtms NONE = singles qtms a |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
145 |
| oadd a qtms (SOME n) = add a qtms n; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
146 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
147 |
fun ins a qtm (i,n) = SOME (i + 1, oadd (RESULT [a]) [qtm] n); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
148 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
149 |
fun insert (NET (p,k,n)) (tm,a) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
150 |
NET (p, k + 1, ins (k,a) (termToQterm tm) (pre n)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
151 |
handle Error _ => raise Bug "TermNet.insert: should never fail"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
152 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
153 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
154 |
fun fromList parm l = foldl (fn (tm_a,n) => insert n tm_a) (new parm) l; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
155 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
156 |
fun filter pred = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
157 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
158 |
fun filt (RESULT l) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
159 |
(case List.filter (fn (_,a) => pred a) l of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
160 |
[] => NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
161 |
| l => SOME (RESULT l)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
162 |
| filt (SINGLE (qtm,n)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
163 |
(case filt n of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
164 |
NONE => NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
165 |
| SOME n => SOME (SINGLE (qtm,n))) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
166 |
| filt (MULTIPLE (vs,fs)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
167 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
168 |
val vs = Option.mapPartial filt vs |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
169 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
170 |
val fs = NameArityMap.mapPartial (fn (_,n) => filt n) fs |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
171 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
172 |
if not (Option.isSome vs) andalso NameArityMap.null fs then NONE |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
173 |
else SOME (MULTIPLE (vs,fs)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
174 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
175 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
176 |
fn net as NET (_,_,NONE) => net |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
177 |
| NET (p, k, SOME (_,n)) => NET (p, k, netSize (filt n)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
178 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
179 |
handle Error _ => raise Bug "TermNet.filter: should never fail"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
180 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
181 |
fun toString net = "TermNet[" ^ Int.toString (size net) ^ "]"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
182 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
183 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
184 |
(* Specialized fold operations to support matching and unification. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
185 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
186 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
187 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
188 |
fun norm (0 :: ks, (f as (_,n)) :: fs, qtms) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
189 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
190 |
val (a,qtms) = revDivide qtms n |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
191 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
192 |
addQterm (FN (f,a)) (ks,fs,qtms) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
193 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
194 |
| norm stack = stack |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
195 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
196 |
and addQterm qtm (ks,fs,qtms) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
197 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
198 |
val ks = case ks of [] => [] | k :: ks => (k - 1) :: ks |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
199 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
200 |
norm (ks, fs, qtm :: qtms) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
201 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
202 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
203 |
and addFn (f as (_,n)) (ks,fs,qtms) = norm (n :: ks, f :: fs, qtms); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
204 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
205 |
val stackEmpty = ([],[],[]); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
206 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
207 |
val stackAddQterm = addQterm; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
208 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
209 |
val stackAddFn = addFn; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
210 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
211 |
fun stackValue ([],[],[qtm]) = qtm |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
212 |
| stackValue _ = raise Bug "TermNet.stackValue"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
213 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
214 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
215 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
216 |
fun fold _ acc [] = acc |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
217 |
| fold inc acc ((0,stack,net) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
218 |
fold inc (inc (stackValue stack, net, acc)) rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
219 |
| fold inc acc ((n, stack, SINGLE (qtm,net)) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
220 |
fold inc acc ((n - 1, stackAddQterm qtm stack, net) :: rest) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
221 |
| fold inc acc ((n, stack, MULTIPLE (v,fns)) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
222 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
223 |
val n = n - 1 |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
224 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
225 |
val rest = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
226 |
case v of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
227 |
NONE => rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
228 |
| SOME net => (n, stackAddQterm VAR stack, net) :: rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
229 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
230 |
fun getFns (f as (_,k), net, x) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
231 |
(k + n, stackAddFn f stack, net) :: x |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
232 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
233 |
fold inc acc (NameArityMap.foldr getFns rest fns) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
234 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
235 |
| fold _ _ _ = raise Bug "TermNet.foldTerms.fold"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
236 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
237 |
fun foldTerms inc acc net = fold inc acc [(1,stackEmpty,net)]; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
238 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
239 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
240 |
fun foldEqualTerms pat inc acc = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
241 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
242 |
fun fold ([],net) = inc (pat,net,acc) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
243 |
| fold (pat :: pats, SINGLE (qtm,net)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
244 |
if pat = qtm then fold (pats,net) else acc |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
245 |
| fold (VAR :: pats, MULTIPLE (v,_)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
246 |
(case v of NONE => acc | SOME net => fold (pats,net)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
247 |
| fold (FN (f,a) :: pats, MULTIPLE (_,fns)) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
248 |
(case NameArityMap.peek fns f of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
249 |
NONE => acc |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
250 |
| SOME net => fold (a @ pats, net)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
251 |
| fold _ = raise Bug "TermNet.foldEqualTerms.fold"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
252 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
253 |
fn net => fold ([pat],net) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
254 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
255 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
256 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
257 |
fun fold _ acc [] = acc |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
258 |
| fold inc acc (([],stack,net) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
259 |
fold inc (inc (stackValue stack, net, acc)) rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
260 |
| fold inc acc ((VAR :: pats, stack, net) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
261 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
262 |
fun harvest (qtm,n,l) = (pats, stackAddQterm qtm stack, n) :: l |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
263 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
264 |
fold inc acc (foldTerms harvest rest net) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
265 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
266 |
| fold inc acc ((pat :: pats, stack, SINGLE (qtm,net)) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
267 |
(case unifyQtermQterm pat qtm of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
268 |
NONE => fold inc acc rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
269 |
| SOME qtm => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
270 |
fold inc acc ((pats, stackAddQterm qtm stack, net) :: rest)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
271 |
| fold |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
272 |
inc acc |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
273 |
(((pat as FN (f,a)) :: pats, stack, MULTIPLE (v,fns)) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
274 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
275 |
val rest = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
276 |
case v of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
277 |
NONE => rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
278 |
| SOME net => (pats, stackAddQterm pat stack, net) :: rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
279 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
280 |
val rest = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
281 |
case NameArityMap.peek fns f of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
282 |
NONE => rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
283 |
| SOME net => (a @ pats, stackAddFn f stack, net) :: rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
284 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
285 |
fold inc acc rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
286 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
287 |
| fold _ _ _ = raise Bug "TermNet.foldUnifiableTerms.fold"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
288 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
289 |
fun foldUnifiableTerms pat inc acc net = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
290 |
fold inc acc [([pat],stackEmpty,net)]; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
291 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
292 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
293 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
294 |
(* Matching and unification queries. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
295 |
(* *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
296 |
(* These function return OVER-APPROXIMATIONS! *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
297 |
(* Filter afterwards to get the precise set of satisfying values. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
298 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
299 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
300 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
301 |
fun idwise ((m,_),(n,_)) = Int.compare (m,n); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
302 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
303 |
fun fifoize ({fifo, ...} : parameters) l = if fifo then sort idwise l else l; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
304 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
305 |
fun finally parm l = map snd (fifoize parm l); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
306 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
307 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
308 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
309 |
fun mat acc [] = acc |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
310 |
| mat acc ((RESULT l, []) :: rest) = mat (l @ acc) rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
311 |
| mat acc ((SINGLE (qtm,n), tm :: tms) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
312 |
mat acc (if matchQtermTerm qtm tm then (n,tms) :: rest else rest) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
313 |
| mat acc ((MULTIPLE (vs,fs), tm :: tms) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
314 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
315 |
val rest = case vs of NONE => rest | SOME n => (n,tms) :: rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
316 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
317 |
val rest = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
318 |
case tm of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
319 |
Term.Var _ => rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
320 |
| Term.Fn (f,l) => |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
321 |
case NameArityMap.peek fs (f, length l) of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
322 |
NONE => rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
323 |
| SOME n => (n, l @ tms) :: rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
324 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
325 |
mat acc rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
326 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
327 |
| mat _ _ = raise Bug "TermNet.match: Match"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
328 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
329 |
fun match (NET (_,_,NONE)) _ = [] |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
330 |
| match (NET (p, _, SOME (_,n))) tm = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
331 |
finally p (mat [] [(n,[tm])]) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
332 |
handle Error _ => raise Bug "TermNet.match: should never fail"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
333 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
334 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
335 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
336 |
fun unseenInc qsub v tms (qtm,net,rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
337 |
(NameMap.insert qsub (v,qtm), net, tms) :: rest; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
338 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
339 |
fun seenInc qsub tms (_,net,rest) = (qsub,net,tms) :: rest; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
340 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
341 |
fun mat acc [] = acc |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
342 |
| mat acc ((_, RESULT l, []) :: rest) = mat (l @ acc) rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
343 |
| mat acc ((qsub, SINGLE (qtm,net), tm :: tms) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
344 |
(case matchTermQterm qsub tm qtm of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
345 |
NONE => mat acc rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
346 |
| SOME qsub => mat acc ((qsub,net,tms) :: rest)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
347 |
| mat acc ((qsub, net as MULTIPLE _, Term.Var v :: tms) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
348 |
(case NameMap.peek qsub v of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
349 |
NONE => mat acc (foldTerms (unseenInc qsub v tms) rest net) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
350 |
| SOME qtm => mat acc (foldEqualTerms qtm (seenInc qsub tms) rest net)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
351 |
| mat acc ((qsub, MULTIPLE (_,fns), Term.Fn (f,a) :: tms) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
352 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
353 |
val rest = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
354 |
case NameArityMap.peek fns (f, length a) of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
355 |
NONE => rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
356 |
| SOME net => (qsub, net, a @ tms) :: rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
357 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
358 |
mat acc rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
359 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
360 |
| mat _ _ = raise Bug "TermNet.matched.mat"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
361 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
362 |
fun matched (NET (_,_,NONE)) _ = [] |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
363 |
| matched (NET (parm, _, SOME (_,net))) tm = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
364 |
finally parm (mat [] [(NameMap.new (), net, [tm])]) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
365 |
handle Error _ => raise Bug "TermNet.matched: should never fail"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
366 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
367 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
368 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
369 |
fun inc qsub v tms (qtm,net,rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
370 |
(NameMap.insert qsub (v,qtm), net, tms) :: rest; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
371 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
372 |
fun mat acc [] = acc |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
373 |
| mat acc ((_, RESULT l, []) :: rest) = mat (l @ acc) rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
374 |
| mat acc ((qsub, SINGLE (qtm,net), tm :: tms) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
375 |
(case unifyQtermTerm qsub qtm tm of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
376 |
NONE => mat acc rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
377 |
| SOME qsub => mat acc ((qsub,net,tms) :: rest)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
378 |
| mat acc ((qsub, net as MULTIPLE _, Term.Var v :: tms) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
379 |
(case NameMap.peek qsub v of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
380 |
NONE => mat acc (foldTerms (inc qsub v tms) rest net) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
381 |
| SOME qtm => mat acc (foldUnifiableTerms qtm (inc qsub v tms) rest net)) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
382 |
| mat acc ((qsub, MULTIPLE (v,fns), Term.Fn (f,a) :: tms) :: rest) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
383 |
let |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
384 |
val rest = case v of NONE => rest | SOME net => (qsub,net,tms) :: rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
385 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
386 |
val rest = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
387 |
case NameArityMap.peek fns (f, length a) of |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
388 |
NONE => rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
389 |
| SOME net => (qsub, net, a @ tms) :: rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
390 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
391 |
mat acc rest |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
392 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
393 |
| mat _ _ = raise Bug "TermNet.unify.mat"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
394 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
395 |
fun unify (NET (_,_,NONE)) _ = [] |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
396 |
| unify (NET (parm, _, SOME (_,net))) tm = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
397 |
finally parm (mat [] [(NameMap.new (), net, [tm])]) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
398 |
handle Error _ => raise Bug "TermNet.unify: should never fail"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
399 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
400 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
401 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
402 |
(* Pretty printing. *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
403 |
(* ------------------------------------------------------------------------- *) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
404 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
405 |
local |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
406 |
fun inc (qtm, RESULT l, acc) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
407 |
foldl (fn ((n,a),acc) => (n,(qtm,a)) :: acc) acc l |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
408 |
| inc _ = raise Bug "TermNet.pp.inc"; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
409 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
410 |
fun toList (NET (_,_,NONE)) = [] |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
411 |
| toList (NET (parm, _, SOME (_,net))) = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
412 |
finally parm (foldTerms inc [] net); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
413 |
in |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
414 |
fun pp ppA = |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
415 |
Parser.ppMap toList (Parser.ppList (Parser.ppBinop " |->" ppQterm ppA)); |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
416 |
end; |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
417 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
418 |
end |