1 2 {- 3 * Mon Nov 5 09:54:24 GMT 1990 4 * 5 * Implementation of untyped terms, signatures and declarations 6 * 7 * Each constructors last argument (of the tuple) is a list of 8 * information attributes that the parser, unparsers, tactics etc use. 9 * 10 * Each terms' next to last argument is a list of alternative types the the 11 * term can have to its natutal type. 12 * 13 -} 14 15 module Sub_Core2 where 16 17 import Vtslib 18 19 import Core_datatype 20 21 import Sub_Core1 22 23 mk_smsl :: [IDec] -> Int -> [ITrm] -> [ITrm] 24 mk_sms :: IDec -> Int -> Int -> (ITrm, Int) 25 mk_fnspace :: ITrm -> ITrm -> ITrm 26 mk_pi :: IDec -> ITrm -> ITrm 27 typ_of_dec :: IDec -> ITrm 28 is_def_dec :: IDec -> Bool 29 is_axm_dec :: IDec -> Bool 30 is_sym_dec :: IDec -> Bool 31 remake_ty :: ITrm -> [a] -> ITrm -> ITrm 32 extract_dc :: Int -> IDec -> IDec 33 uncurry_trm :: IDec -> Int -> ITrm -> ITrm 34 uncurry_cn :: [Int] -> Int -> Int -> Int -> Int -> Int -> [ITrm] -> [Attribute] -> ITrm 35 uncurry_sm :: [Int] -> Int -> Int -> Int -> Int -> [ITrm] -> [Attribute] -> ITrm 36 subst_dec :: IDec -> IDec -> ITrm -> IDec 37 subst_trm :: IDec -> ITrm -> ITrm -> ITrm 38 subst_cn :: a -> Int -> Int -> Int -> [ITrm] -> [Attribute] -> ITrm 39 --subst_sm :: [(Int, ITrm)] -> Int -> Int -> Int -> [ITrm] -> [Attribute] -> ITrm 40 create_table :: Int -> IDec -> ITrm -> (Int, [(Int , ITrm)]) 41 shift_dec :: [Int] -> Int -> IDec -> IDec 42 shift_trm :: [Int] -> Int -> ITrm -> ITrm 43 share_trm :: [Int] -> ITrm -> ITrm 44 shift_cn :: [Int] -> Int -> Int -> Int -> Int -> Int -> [ITrm] -> [Attribute] -> ITrm 45 shift_sm :: [Int] -> Int -> Int -> Int -> Int -> [ITrm] -> [Attribute] -> ITrm 46 share_cn :: [Int] -> Int -> Int -> Int -> Int -> [ITrm] -> [Attribute] -> ITrm 47 share_sm :: [Int] -> Int -> Int -> Int -> [ITrm] -> [Attribute] -> ITrm 48 --canonical_i :: (Integral a) => [a] -> a -> a 49 get_share_map :: ISgn -> [Int] 50 51 52 53 {- 54 return the share_map of a signature 55 Note: share maps are memoised at every Share and Combine node 56 -} 57 58 -- get_share_map :: ISgn -> Share_map 59 60 get_share_map sg 61 = shared sg 0 62 where 63 shared :: ISgn -> Int -> Share_map 64 65 shared (Share _ _ _ _ sm _) j 66 = (list 0 j) ++ (map negate sm) -- ++ (map (\ i -> i + j) sm) 67 68 shared (Combine _ _ _ sm _) j 69 = (list 0 j) ++ (map negate sm) -- ++ (map (\ i -> i + j) sm) 70 71 shared (Empty _) j 72 = list 0 j 73 74 shared (Extend _ sg _) j 75 = shared sg (j+1) 76 77 78 {- return the list [i,i+1,...,j-1] -} 79 80 list :: Int -> Int -> [Int] 81 82 list i j = init [ i..j ] 83 84 {- 85 list i j = if i >= j then [] 86 else i : list (i+1) j 87 -} 88 89 90 91 92 93 {- take a share_map and and i-index and return the canonical i-index -} 94 95 canonical_i :: Share_map -> Int -> Int 96 97 canonical_i [] i = i 98 99 canonical_i shareL i = shareL !! i 100 101 102 103 104 105 share_sm shareL depth i j tyL att 106 = Sym (depth+canonical_i shareL (i-depth)) j tyL att 107 108 109 share_cn shareL depth i j k tyL att 110 = Const (depth+canonical_i shareL (i-depth)) j k tyL att 111 112 113 shift_sm shareL offset depth i j tmL att 114 = share_sm shareL depth (i+offset) j tmL att 115 116 117 shift_cn shareL offset depth i j k tyL att 118 = share_cn shareL depth (i+offset) j k tyL att 119 120 121 122 123 124 {- 125 apply sharing to a term. ie replace all global symbols 126 that may be shared with the root symbol 127 -} 128 129 -- share_trm :: Share_map -> ITrm -> ITrm 130 131 share_trm shareL tm 132 = f3 tm 133 where 134 f1 = share_sm shareL 135 f2 = share_cn shareL 136 (f3,_) = map_fn f1 f2 137 138 139 140 141 142 {- shift a term by an offset and then do any sharing that may be required -} 143 144 shift_trm shareL offset tm 145 = f3 tm 146 where 147 f1 = shift_sm shareL offset 148 f2 = shift_cn shareL offset 149 (f3,_) = map_fn f1 f2 150 151 152 153 154 155 {- shift a dec by an offset and then do any sharing that may be required -} 156 157 shift_dec shareL offset dc 158 = f3 dc 159 where 160 f1 = shift_sm shareL offset 161 f2 = shift_cn shareL offset 162 (_,f3) = map_fn f1 f2 163 164 165 166 167 {- 168 create a assoc list of j indexes and terms from a declatation 169 and a term. The term should match the declaration pair for 170 decpair. 171 -} 172 173 create_table j (Decpair dc1 dc2 _) (Pair tm1 tm2 _ _ _) 174 = (j2,al1 ++ al2) 175 where 176 (j1,al1) = create_table (j+1) dc1 tm1 177 (j2,al2) = create_table (j1+1) dc2 tm2 178 179 create_table j (Symbol_dec _ _) tm 180 = (j,[(j,tm)]) 181 182 --create_table _ _ _ 183 -- = error "SubstError" -- ** exn 184 185 186 187 188 189 190 subst_sm table n i j tyL att 191 | i==n = case assoc j table of 192 SOME tm -> shift_trm [] n tm 193 -- NONE -> error "System_Error" -- ** exn 194 | i/=n = Sym (i-1) j tyL att 195 196 197 198 199 subst_cn n i j k tyL att 200 = Const (i-1) j k tyL att 201 202 203 204 {- 205 * substitute a term for the symbols <0,j> in a term 206 * An empty share_map may given to the 207 * shift_trm function since the shift is 208 * upwards so no new sharing can be done 209 -} 210 211 subst_trm dc tm1 tm2 212 = f3 tm1 213 where 214 (_,table) = create_table 0 dc tm2 215 f1 = subst_sm table 216 f2 = subst_cn 217 (f3,_) = map_fn f1 f2 218 219 220 221 222 subst_dec dc1 dc2 tm 223 = f3 dc2 224 where 225 (_,table) = create_table 0 dc1 tm 226 f1 = subst_sm table 227 f2 = subst_cn 228 (_,f3) = map_fn f1 f2 229 230 231 232 233 {- 234 * build a list of all the indices down the spine of symbol dec 235 * with then in a declaration 236 -} 237 238 ext_indices :: IDec -> Int -> [Int] 239 240 ext_indices dc j 241 = ext j dc 0 [] [] 242 where 243 ext :: Int -> IDec -> Int -> [Int] -> [( IDec , [Int])] -> [Int] 244 245 ext 0 d j l _ = l 246 247 ext i (Decpair dc1 dc2 _) j l cl 248 = ext (i-1) dc1 (j+1) l ((dc2,j+1:l):cl) 249 250 ext i _ j _ ((dc,l):cl) = ext (i-1) dc (j+1) l cl 251 252 253 254 uncurry_sm iL dec_depth local_depth i j tmL attL 255 = if i - local_depth < dec_depth 256 then Sym local_depth (j + (iL !! i)) tmL attL 257 else Sym (i - dec_depth + 1) j tmL attL 258 259 260 261 262 263 uncurry_cn iL dec_depth local_depth i j k tmL attL 264 = if i - local_depth < dec_depth 265 then Const local_depth (j + (iL !! i)) k tmL attL 266 else Const (i - dec_depth + 1) j k tmL attL 267 268 269 270 {- 271 (* move a term defined within a declaration to a term defined *) 272 (* on a signature extended by that declaration *) 273 -} 274 275 uncurry_trm dc j tm 276 = f3 tm 277 where 278 iL = ext_indices dc j 279 f1 = uncurry_sm iL (length iL) 280 f2 = uncurry_cn iL (length iL) 281 (f3,_) = map_fn f1 f2 282 283 284 285 286 287 extract_dc i dc 288 = extract i dc [] 289 where 290 extract :: Int -> IDec -> [IDec] -> IDec 291 292 extract 0 (dc @ (Symbol_dec _ _)) _ = dc 293 294 extract 0 (dc @ (Axiom_dec _ _)) _ = dc 295 296 extract 0 (dc @ (Def _ _ _)) _ = dc 297 298 extract 0 (dc @ (Data _ _ _)) _ = dc 299 300 -- extract 0 _ _ = error "BadIndex" -- ** exn 301 302 extract i (Symbol_dec _ _) (dc:dcL) 303 = extract (i-1) dc dcL 304 305 extract i (Axiom_dec _ _) (dc:dcL) 306 = extract (i-1) dc dcL 307 308 extract i (Def _ _ _) (dc:dcL) 309 = extract (i-1) dc dcL 310 311 extract i (Data _ _ _) (dc:dcL) 312 = extract (i-1) dc dcL 313 314 extract i (Decpair dc1 dc2 _) dcL 315 = extract (i-1) dc1 (dc2:dcL) 316 317 -- extract _ _ _ = error "BadIndex" -- ** exn 318 319 320 321 322 323 remake_ty (Binder q dc tm _ _) [] tm1 324 = subst_trm dc tm tm1 325 326 remake_ty (Binder q dc tm tmL att) (_:l) tm1 327 = Binder q dc (remake_ty tm l tm1) tmL att 328 329 --remake_ty _ _ _ = 330 -- error "VTS_ERROR" -- ** exn 331 332 333 334 335 336 {- 337 (* return if a declaration defines just symbols *) 338 -} 339 340 is_sym_dec (Symbol_dec _ _) = True 341 342 is_sym_dec (Decpair dc1 dc2 _) 343 = is_sym_dec dc1 && is_sym_dec dc2 344 345 is_sym_dec _ = False 346 347 348 349 350 351 {- return if a declaration defines just axioms -} 352 353 is_axm_dec (Axiom_dec _ _) = True 354 355 is_axm_dec (Decpair dc1 dc2 _) 356 = is_axm_dec dc1 && is_axm_dec dc2 357 358 is_axm_dec _ = False 359 360 361 362 363 364 {- return if a declaration defines definitions -} 365 366 is_def_dec (Def _ _ _) = True 367 368 is_def_dec (Decpair dc1 dc2 _) 369 = is_def_dec dc1 && is_def_dec dc2 370 371 is_def_dec _ = False 372 373 374 375 376 {- return the type introduced by a declaration -} 377 378 typ_of_dec (Symbol_dec tm _) = tm 379 380 typ_of_dec (Axiom_dec tm _) = tm 381 382 typ_of_dec (dc @ (Decpair dc1 dc2 _)) 383 = if is_sym_dec dc 384 then Binder Sigma dc1 (typ_of_dec dc2) [] [] 385 else if is_axm_dec dc 386 then Binary' And (typ_of_dec dc1) 387 (shift_trm [] (-1) (typ_of_dec dc2)) [] [] 388 else Sym 0 0 [] []-- TEMPORARY DEBUG SYM 0 NOT CORRECTerror "System_Error" -- ** exn 389 390 --typ_of_dec _ = error "System_Error" -- ** exn 391 392 393 394 395 396 mk_pi dc tm 397 = Binder Pi dc tm [] [] 398 399 400 401 mk_fnspace tm1 tm2 402 = Binder Pi (Symbol_dec tm1 []) (shift_trm [] 1 tm2) [] [] 403 404 405 406 407 408 409 410 mk_sms (Symbol_dec _ _) i j 411 = (Sym i j [] [] , j+1) 412 413 mk_sms (dc @ (Decpair dc1 dc2 _)) i j 414 = (Pair sms1 sms2 (typ_of_dec dc) [] [] , j2) 415 where 416 (sms1, j1) = mk_sms dc1 i (j+1) 417 (sms2, j2) = mk_sms dc2 i j1 418 419 --mk_sms _ _ _ = 420 -- error "VTS_ERROR" -- ** exn 421 422 423 424 425 426 427 mk_smsl [] i tm1 = tm1 428 429 mk_smsl (dc:dcL) i tml 430 = mk_smsl dcL (i+1) (sms : tml) 431 where 432 (sms, _) = mk_sms dc i 0 433