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