src/Pure/symtab.ML
author lcp
Tue, 18 Jan 1994 15:57:40 +0100
changeset 230 ec8a2b6aa8a7
parent 0 a5a9c433f639
child 234 1b3bee8d5d7e
permissions -rw-r--r--
Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title: 	symtab
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1989  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
(*Unbalanced binary trees indexed by strings
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
  No way to delete an entry
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
  could generalize alist_of to a traversal functional
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
signature SYMTAB = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
sig
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
   type 'a table
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
   val alist_of : 'a table -> (string*'a) list
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
   val balance : 'a table -> 'a table
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
   val lookup : 'a table * string -> 'a option
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
   val null : 'a table
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
   val is_null : 'a table -> bool
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
   val st_of_alist : (string*'a)list * 'a table -> 'a table
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
   val st_of_declist : (string list * 'a)list * 'a table -> 'a table
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
   val update : (string*'a) * 'a table -> 'a table
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
   val update_new : (string*'a) * 'a table -> 'a table
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
   exception DUPLICATE of string
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
functor SymtabFun () : SYMTAB = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
struct
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
(*symbol table errors, such as from update_new*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
exception DUPLICATE of string;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
datatype 'a table = Tip  |  Branch of (string * 'a * 'a table * 'a table);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    35
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    36
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
val null = Tip;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    39
fun is_null Tip = true
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
  | is_null _ = false;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    41
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    42
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    43
fun lookup (symtab: 'a table, key: string) : 'a option = 
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    44
  let fun look  Tip  = None
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    45
	| look (Branch (key',entry,left,right)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    46
	    if      key < key' then look left
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    47
	    else if key' < key then look right
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    48
	    else  Some entry
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    49
  in look symtab end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    50
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    51
(*update, allows overwriting of an entry*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    52
fun update ((key: string, entry: 'a), symtab : 'a table)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    53
  : 'a table =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    54
  let fun upd  Tip  = Branch (key,entry,Tip,Tip)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    55
	| upd (Branch(key',entry',left,right)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    56
	    if      key < key' then Branch (key',entry', upd left, right)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    57
	    else if key' < key then Branch (key',entry',left, upd right)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    58
	    else                    Branch (key,entry,left,right)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    59
  in  upd symtab  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    60
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    61
(*Like update but fails if key is already defined in table.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
  Allows st_of_alist, etc. to detect multiple definitions*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
fun update_new ((key: string, entry: 'a), symtab : 'a table)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    64
  : 'a table =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    65
  let fun upd Tip = Branch (key,entry,Tip,Tip)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    66
	| upd (Branch(key',entry',left,right)) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    67
	    if      key < key' then Branch (key',entry', upd left, right)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    68
	    else if key' < key then Branch (key',entry',left, upd right)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    69
	    else  raise DUPLICATE(key)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    70
  in  upd symtab  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    71
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    72
(*conversion of symbol table to sorted association list*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    73
fun alist_of (symtab : 'a table) : (string * 'a) list =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    74
  let fun ali (symtab,cont) = case symtab of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    75
		Tip => cont
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    76
	| Branch (key,entry,left,right) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    77
	    ali(left, (key,entry) :: ali(right,cont))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    78
  in  ali (symtab,[])  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    79
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    80
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    81
(*Make a balanced tree of the first n members of the sorted alist (sal).
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    82
  Utility for the function balance.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    83
fun bal_of (sal, 0) = Tip
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    84
  | bal_of (sal, n) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    85
      let val mid = n div 2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    86
      in  case  drop (mid,sal) of
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    87
	    [] => bal_of (sal, mid)   (*should not occur*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    88
	  | ((key,entry):: pairs) =>
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    89
		Branch(key,entry, bal_of(sal,mid), bal_of(pairs, n-mid-1))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    90
      end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    91
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    92
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    93
fun balance symtab =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    94
  let val sal = alist_of symtab
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    95
  in  bal_of (sal, length sal)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    96
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    97
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    98
(*Addition of association list to a symbol table*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    99
fun st_of_alist (al, symtab) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   100
    foldr update_new (al, symtab);
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   101
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   102
(*A "declaration" associates the same entry with a list of keys;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   103
  does not allow overwriting of an entry*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   104
fun decl_update_new ((keys : string list, entry: 'a), symtab)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   105
  : 'a table =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   106
  let fun decl (key,symtab) = update_new((key,entry), symtab)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   107
  in  foldr decl (keys, symtab)  end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   108
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   109
(*Addition of a list of declarations to a symbol table*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   110
fun st_of_declist (dl, symtab) =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   111
    balance (foldr decl_update_new (dl, symtab))
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   112
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   113
end;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
   114