1(*****************************************************************************)
2(* Varmap.sml                                                                *)
3(* ---------------------                                                     *)
4(*                                                                           *)
5(* Definition of type varmap and various operations on it                    *)
6(*                                                                           *)
7(*****************************************************************************)
8(*                                                                           *)
9(* Revision history:                                                         *)
10(*                                                                           *)
11(*   Thu Oct  4 15:45:52 BST 2001 -- created file                            *)
12(*   Thu Nov 15 17:07:37 GMT 2001 -- added unify                             *)
13(*   Thu Mar 28 09:40:05 GMT 2002 -- added signature file                    *)
14(*                                                                           *)
15(*****************************************************************************)
16
17structure Varmap :> Varmap = struct
18
19(*
20load "Binarymap";
21*)
22
23local
24
25open Binarymap;
26
27open HolKernel Parse boolLib BasicProvers
28
29infixr 3 -->;
30infix ## |-> THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL;
31
32in
33
34(*****************************************************************************)
35(* A value of ML type term_bdd represents a judgement                        *)
36(*                                                                           *)
37(*    vm tm |--> bdd                                                         *)
38(*                                                                           *)
39(* where vm is a variable map, tm a term and bdd a BDD                       *)
40(*                                                                           *)
41(* A variable map associates BuDDy BDD variables (which are represented      *)
42(* as numbers) to HOL variables. Variable maps are represented as            *)
43(* dictionaries from the Moscow ML Library structure Binarymap.              *)
44(*****************************************************************************)
45
46
47(*****************************************************************************)
48(*                  START OF DEFINITION OF varmap                            *)
49(*****************************************************************************)
50
51type varmap = (string, int) Binarymap.dict;
52
53(*****************************************************************************)
54(* Create an empty var_map                                                   *)
55(*****************************************************************************)
56
57val empty = Binarymap.mkDict String.compare : (string, int) Binarymap.dict;
58
59(*****************************************************************************)
60(* Compute number of entries in a varmap                                     *)
61(*****************************************************************************)
62
63fun size (vm:varmap) = Binarymap.numItems vm;
64
65(*****************************************************************************)
66(* See if name is mapped to anything in a varmap.                           *)
67(* Return SOME n if name mapped to n, or NONE if not in the table            *)
68(*****************************************************************************)
69
70fun peek (vm:varmap) name = Binarymap.peek(vm,name);
71
72(*****************************************************************************)
73(* Explode a varmap into a list of string/int pairs                          *)
74(*****************************************************************************)
75
76fun dest (vm:varmap) = Binarymap.listItems vm;
77
78(*****************************************************************************)
79(* Insert a new entry in a varmap                                            *)
80(*****************************************************************************)
81
82fun insert (s,n) (vm:varmap) = Binarymap.insert(vm, s, n);
83
84(*****************************************************************************)
85(* Test pointer equality of varmaps                                          *)
86(*****************************************************************************)
87
88val eq = Portable.pointer_eq : varmap*varmap->bool;
89
90(*****************************************************************************)
91(* Test whether vm2 extends vm1                                              *)
92(* (i.e. every entry in vm1 is also in vm2)                                  *)
93(*****************************************************************************)
94
95fun extends (vm1:varmap) (vm2:varmap) =
96 eq(vm1,vm2)
97  orelse Binarymap.foldl
98          (fn (s,n,bv) => bv andalso (case Binarymap.peek(vm2,s) of
99                                         SOME m => (m=n)
100                                       | NONE   => false))
101          true
102          vm1;
103
104
105(*****************************************************************************)
106(* Compute smallest varmap vm such that extends vm1 vm and extends vm2 vm.   *)
107(* Raises unifyVarmapError if vm1 and vm2 are incompatible.                  *)
108(*****************************************************************************)
109
110exception unifyVarmapError;
111
112val unify =
113 Binarymap.foldl
114  (fn (v,n,vm) => case Binarymap.peek(vm:varmap, v) of
115                     SOME n' => if n=n' then vm else raise unifyVarmapError
116                   | NONE    => Binarymap.insert(vm,v,n));
117
118(*****************************************************************************)
119(* remove s vm removes entry for string s from vm                            *)
120(* (identity if no entry for s in vm)                                        *)
121(*****************************************************************************)
122
123fun remove s (vm:varmap) =
124 fst(Binarymap.remove(vm,s)) handle NotFound => vm;
125
126(*****************************************************************************)
127(*                    END OF DEFINITION OF varmap                            *)
128(*****************************************************************************)
129
130end;
131
132end
133