1 module Lookup where 2 3 import Vtslib 4 5 import Core_datatype 6 7 {- 8 (******************************************************************************) 9 (* memoised lookup table of signatures. *) 10 (******************************************************************************) 11 -} 12 13 {- 14 (******************************************************************************) 15 (* A lookup table is an list of association lists. *) 16 (* Each element of an association list consists of *) 17 (* string - The name of a symbol (or constructor) *) 18 (* int * bool - The j index of a symbol, or *) 19 (* int * int * int list - The j,k indexes for of a constructor *) 20 (* (int * opr) option - The precedence and type of operator *) 21 (* The boolean in the symbol part indicates wheather the symbol is *) 22 (* accessabe by a rec expression. *) 23 (* in *) 24 (******************************************************************************) 25 -} 26 27 type Index = Sum (Int , Bool) ( Int , Int , [(Int , Int)] ) 28 29 type Entry = [(String , Option (Index , (Int , String) ))] 30 31 type Lookup_table = [Entry] 32 33 {- 34 35 local 36 37 (******************************************************************************) 38 (* Turn a name into a lookup table *) 39 (******************************************************************************) 40 41 fun get_nms jf (Name s) = 42 [(s, (jf, NONE))] 43 | get_nms jf (Operator (s,p,opr)) = 44 [(s,(jf,SOME (p,opr)))] 45 46 (******************************************************************************) 47 (* Turn a list of names and a list of list of terms (taken from a *) 48 (* datatype declaration) and turn them into a lookup table *) 49 (******************************************************************************) 50 51 and get_nmsL jf k [] [] = 52 [] 53 | get_nmsL jf k (nm :: nmL) (tmL :: tmLL) = 54 get_nms (inr (jf,k,(length tmL, rec_pars 0 tmL))) nm @ 55 get_nmsL jf (k+1) nmL tmLL 56 | get_nmsL jf k _ _ = 57 [] 58 59 and rec_pars _ [] = [] 60 | rec_pars i (tm :: tmL) = 61 (if is_00_sm tm then [i] else []) @ rec_pars (i+1) tmL 62 63 and is_00_sm (Sym (0,0,_,_)) = true 64 | is_00_sm _ = false 65 66 67 (******************************************************************************) 68 (* Return the lookup table for a declaration *) 69 (******************************************************************************) 70 71 fun get_dec_nms rec_flag j (Symbol_dec (_,attL)) = 72 (case get_att Name_Style attL 73 of SOME (Symbol_Name nm) => (get_nms (inl (j,rec_flag)) nm, j) 74 | _ => ([], j)) 75 | get_dec_nms rec_flag j (Axiom_dec (_,attL)) = 76 (case get_att Name_Style attL 77 of SOME (Symbol_Name nm) => (get_nms (inl (j,rec_flag)) nm, j) 78 | _ => ([], j)) 79 | get_dec_nms rec_flag j (Def (_,_,attL)) = 80 (case get_att Name_Style attL 81 of SOME (Symbol_Name nm) => (get_nms (inl (j,rec_flag)) nm, j) 82 | _ => ([], j)) 83 | get_dec_nms rec_flag j (Data (_,tmLL,attL)) = 84 (case get_att Name_Style attL 85 of SOME (Datatype_Name (nm::nmL)) => 86 (get_nms (inr (j,0,(0,[]))) nm @ 87 get_nmsL j 1 nmL tmLL, j) 88 | _ => ([], j)) 89 | get_dec_nms rec_flag j (Decpair (dc1,dc2,_)) = 90 let val (nms1,j1) = get_dec_nms rec_flag (j+1) dc1 91 val (nms2,j2) = get_dec_nms rec_flag (j1+1) dc2 92 in (nms1@nms2, j2) end 93 94 (******************************************************************************) 95 (* Return the lookup table for a pass1 decaration *) 96 (******************************************************************************) 97 98 fun get_pdec_nms rec_flag j (P1_Dec (nmL, _)) = get_p1_nmsL rec_flag j nmL 99 | get_pdec_nms rec_flag j (P1_Def (P1_Lhs (_,nm,_),_)) = 100 get_p1_nmsL rec_flag j [nm] 101 | get_pdec_nms rec_flag j (P1_Define (nm,_,_)) = 102 get_p1_nmsL rec_flag j [nm] 103 | get_pdec_nms rec_flag j (P1_Data (P1_Lhs (_,nm,_), conL,_)) = 104 (get_nms (inr (j,0,(0,[]))) nm @ get_con_nms j 1 conL, j) 105 | get_pdec_nms rec_flag j (P1_Decp (dc1,dc2)) = 106 let val (nms1,j1) = get_pdec_nms rec_flag (j+1) dc1 107 val (nms2,j2) = get_pdec_nms rec_flag (j1+1) dc2 108 in (nms1@nms2, j2) end 109 | get_pdec_nms rec_flag j (P1_BDec dc) = 110 get_p1bdc rec_flag j dc 111 | get_pdec_nms rec_flag j (P1_Database_dec dc) = 112 let val (dc1, _) = internal_Dec dc 113 in get_dec_nms rec_flag j dc1 end 114 115 (******************************************************************************) 116 (* Return the lookup table for a pass1 binding declaration *) 117 (******************************************************************************) 118 119 and get_p1bdc rec_flag j (P1_Bdec (nmL, _)) = 120 get_p1_nmsL rec_flag j nmL 121 | get_p1bdc rec_flag j (P1_Bdecp (dc1,dc2)) = 122 let val (nms1, j1) = get_p1bdc rec_flag (j+1) dc1 123 val (nms2, j2) = get_p1bdc rec_flag (j1+1) dc2 124 in (nms1@nms2, j2) end 125 126 (******************************************************************************) 127 (* Return the llokup table for a list of names, that representing *) 128 (* sequence of paired declarations *) 129 (******************************************************************************) 130 131 and get_p1_nmsL rec_flag j [nm] = (get_nms (inl (j,rec_flag)) nm, j) 132 | get_p1_nmsL rec_flag j (nm :: nmL) = 133 let val nms1 = get_nms (inl (j+1,rec_flag)) nm 134 val (nms2,j1) = get_p1_nmsL rec_flag (j+2) nmL 135 in (nms1@nms2, j1) end 136 | get_p1_nmsL rec_flag j [] = ([], j) 137 138 (******************************************************************************) 139 (* Return the lookup table for the constuctors of a pass1 datatype *) 140 (* declaration *) 141 (******************************************************************************) 142 143 and get_con_nms j k [] = [] 144 | get_con_nms j k (P1_Rhs (nm,tmL) :: nmL) = 145 get_nms (inr (j,k,(length tmL,get_pvars 0 tmL))) nm @ 146 get_con_nms j (k+1) nmL 147 148 and get_pvars _ [] = [] 149 | get_pvars i (tm :: tmL) = 150 (if is_00_psm tm then [i] else []) @ get_pvars (i+1) tmL 151 152 and is_00_psm (P1_Sym (0,0,_)) = true 153 | is_00_psm _ = false 154 155 in (* local *) 156 157 (******************************************************************************) 158 (* Take a signature and return its lookup table *) 159 (******************************************************************************) 160 161 fun create_lookup_table (sg : sgn) : lookup_table = 162 case sg 163 of Empty _ => 164 [] 165 | Extend (dc,sg,_) => 166 extend_lookup_table true dc (create_lookup_table sg) 167 | Combine (sg1,sg2,_,_,_) => 168 let val tbl1 = create_lookup_table sg2 169 and tbl2 = create_lookup_table sg1 170 in [] :: tbl1 @ tbl2 end 171 | Share (sg,_,_,_,_,_) => 172 [] :: create_lookup_table sg 173 174 (******************************************************************************) 175 (* Extend a lookup table with a new declaration *) 176 (******************************************************************************) 177 178 and extend_lookup_table rec_flag dc tbl : lookup_table = 179 let val (nms, _) = get_dec_nms rec_flag 0 dc 180 in nms :: tbl end 181 182 fun combine_lookup_table tbl1 tbl2 : lookup_table = 183 tbl2 @ [[]] @ tbl1 184 185 fun share_lookup_table tbl (i : int) (j : int) : lookup_table = 186 [] :: tbl 187 188 fun create_tbl (sg : pass1_sgn) : lookup_table = 189 case sg 190 of P1_Empty => 191 [] 192 | P1_Signature (dc) => 193 extend_tbl true dc [] 194 | P1_Extend (dc,sg) => 195 extend_tbl true dc (create_tbl sg) 196 | P1_Combine (sg1,sg2) => 197 let val tbl1 = create_tbl sg2 198 and tbl2 = create_tbl sg1 199 in [] :: tbl1 @ tbl2 end 200 | P1_Sharing (sg,_) => 201 [] :: create_tbl sg 202 | P1_Database_sgn sg => 203 create_lookup_table (internal_Sgn sg) 204 | P1_Named_sgn (_,sg) => 205 create_tbl sg 206 | P1_plus_plus (sg1,sg2) => 207 let val tbl1 = create_tbl sg2 208 and tbl2 = create_tbl sg1 209 in [] :: tbl1 @ tbl2 end 210 211 and extend_tbl rec_flag pdc tbl : lookup_table = 212 let val (nms,_) = get_pdec_nms rec_flag 0 pdc 213 in nms :: tbl end 214 215 (******************************************************************************) 216 (* Lookup a string in the lookup table and return the pass1 symbol (or *) 217 (* constructor) and its optional operator status *) 218 (******************************************************************************) 219 220 fun lookup_name (tbl : lookup_table) (str : string) = 221 let fun lookup i [] = 222 NONE 223 | lookup i (entry :: tbl) = 224 case assoc str entry 225 of SOME (inl (j,true),opr_op) => 226 SOME (P1_Sym (i,j,true), opr_op) 227 | SOME (inr (j,k,_),opr_op) => 228 SOME (P1_Const (i,j,k,true), opr_op) 229 | _ => lookup (i+1) tbl 230 in lookup 0 tbl end 231 232 fun lookup_rec_name (tbl : lookup_table) (str : string) = 233 let fun lookup i [] = 234 NONE 235 | lookup i (entry :: tbl) = 236 case assoc str entry 237 of SOME (inl (j, false),opr_op) => 238 SOME (P1_Sym (i,j,true), opr_op) 239 | _ => lookup (i+1) tbl 240 in lookup 0 tbl end 241 242 exception BadIndex 243 244 fun lookup_sm_index (tbl : lookup_table) (i,j) = 245 let val entry = tbl !! i 246 fun is_sm (_,(inl (j',_),_)) = j = j' 247 | is_sm _ = false 248 in case filter is_sm entry 249 of ((s,(inl (_,f),NONE)) :: _) => SOME (s, f, NONE) 250 | ( (s,(inl (_,f),SOME (i, opr))) :: _) => 251 SOME (s, f, SOME (i,opr)) 252 | _ => NONE 253 end 254 255 fun lookup_cn_index (tbl : lookup_table) (i,j,k) = 256 let val entry = tbl !! i 257 fun is_sm (_,(inr (j',k',_),_)) = (j',k') = (j,k) 258 | is_sm _ = false 259 in case filter is_sm entry 260 of ( (s,(inr (_,_,_),SOME (i, opr))) :: _) => 261 SOME (s, SOME (i,opr)) 262 | ((s,(inr (_,_,_),_)) :: _) => SOME (s, NONE) 263 | _ => NONE 264 end 265 end (* of local *) 266 267 fun rec_parameters (tbl : lookup_table) (i,j,k) = 268 let val entry = tbl !! i 269 fun is_sm (_,(inr (j',k',_),_)) = (j',k') = (j,k) 270 | is_sm _ = false 271 in case filter is_sm entry 272 of ((_,(inr (_,_,iL),_)) :: _) => iL 273 | _ => raise BadIndex 274 end 275 276 fun operators ([] : lookup_table) = [] 277 | operators (ent :: tbl) = 278 foldr (curry op@) (operators tbl) (map get_ops ent) 279 280 and get_ops (id, (inr _, SOME (i, opr))) = 281 [(id, Operator (id,i,opr))] 282 | get_ops (id, (inr _, NONE)) = 283 [(id, Name id)] 284 | get_ops _ = 285 [] 286 end 287 -}