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_Core1 where 16 17 import Vtslib 18 19 import Core_datatype 20 21 22 {- 23 * Equality on trms, decs and sgns is just on the important parts, ie ignore 24 * extra types and information 25 * 26 -} 27 28 29 {- 30 * Pairwise compare values of two lists 31 * ie, eq_pair_wise cmp [a1,...,an] [b1,...,bn] = cmp a1 b1 andalso ... cmp an bn 32 -} 33 34 eq_pair_wise cmp [] [] = True 35 36 eq_pair_wise cmp ( x1 : l1 ) ( x2 : l2 ) 37 = cmp x1 x2 && eq_pair_wise cmp l1 l2 38 39 eq_pair_wise cmp _ _ = False 40 41 42 43 44 45 eq_trm (Sym i1 j1 _ _) (Sym i2 j2 _ _) 46 = i1 == i2 && j1 == j2 47 48 eq_trm (App tm1 tm2 _ _) (App tm3 tm4 _ _) 49 = eq_trm tm1 tm3 && eq_trm tm2 tm4 50 51 eq_trm (Pair tm1 tm2 tm3 _ _) (Pair tm4 tm5 tm6 _ _) 52 = eq_trm tm1 tm4 && eq_trm tm2 tm5 && eq_trm tm3 tm6 53 54 eq_trm (Binder b1 dc1 tm1 _ _) (Binder b2 dc2 tm2 _ _) 55 = b1 == b2 && eq_dec dc1 dc2 && eq_trm tm1 tm2 56 57 eq_trm (Constant c1 _ _) (Constant c2 _ _) 58 = c1 == c2 59 60 eq_trm (Unary c1 tm1 _ _) (Unary c2 tm2 _ _) 61 = c1 == c2 && eq_trm tm1 tm2 62 63 eq_trm (Binary' c1 tm1 tm2 _ _) (Binary' c2 tm3 tm4 _ _) 64 = c1 == c2 && eq_trm tm1 tm3 && eq_trm tm2 tm4 65 66 eq_trm (Cond dc1 tm1 tm2 _ _) (Cond dc2 tm3 tm4 _ _) 67 = eq_dec dc1 dc2 && eq_trm tm1 tm3 && eq_trm tm2 tm4 68 69 eq_trm (Const i1 j1 k1 _ _) (Const i2 j2 k2 _ _) 70 = i1 == i2 && j1 == j2 && k1 == k2 71 72 eq_trm (Recurse tmL1 tm1 _ _) (Recurse tmL2 tm2 _ _) 73 = eq_pair_wise eq_trm tmL1 tmL2 && eq_trm tm1 tm2 74 75 eq_trm _ _ = False 76 77 78 79 80 81 82 eq_dec (Symbol_dec tm1 _) (Symbol_dec tm2 _) 83 = eq_trm tm1 tm2 84 85 eq_dec (Axiom_dec tm1 _) (Axiom_dec tm2 _) 86 = eq_trm tm1 tm2 87 88 eq_dec (Def tm1 tm2 _) (Def tm3 tm4 _) 89 = eq_trm tm1 tm3 && eq_trm tm2 tm4 90 91 eq_dec (Data dcL1 tmLL1 _) (Data dcL2 tmLL2 _) 92 = eq_pair_wise eq_dec dcL1 dcL2 && 93 eq_pair_wise (eq_pair_wise eq_trm) tmLL1 tmLL2 94 95 eq_dec (Decpair dc1 dc2 _) (Decpair dc3 dc4 _) 96 = eq_dec dc1 dc3 && eq_dec dc2 dc4 97 98 eq_dec _ _ = False 99 100 101 102 103 eq_sgn (Empty _) (Empty _) = True 104 105 eq_sgn (Extend dc1 sg1 _) (Extend dc2 sg2 _) 106 = eq_dec dc1 dc2 && eq_sgn sg1 sg2 107 108 eq_sgn (Combine sg1 sg2 i1 _ _) (Combine sg3 sg4 i2 _ _) 109 = i1 == i2 && eq_sgn sg1 sg3 && eq_sgn sg2 sg4 110 111 eq_sgn (Share sg1 i1 j1 k1 _ _) (Share sg2 i2 j2 k2 _ _) 112 = i1 == i2 && j1 == j2 && j1 == j2 && eq_sgn sg1 sg2 113 114 eq_sgn _ _ = False 115 116 117 118 119 120 {- 121 * Extract a subterm from a term along with a list of all the 122 * declarations encounted on the spine down to the subterm. 123 * generate an exception if the index does not point at a valid subterm 124 * 125 -} 126 127 -- select_trm :: ITrm -> [ Int ] -> ( ITrm , [ IDec ] ) 128 129 130 select_trm tm iL 131 = sel_trm iL tm [] 132 where 133 sel_trm :: [ Int] -> ITrm -> [ IDec ] -> ( ITrm , [ IDec ] ) 134 135 sel_trm (i:iL) (App tm1 tm2 _ _) dcL 136 = sel_trm iL ([tm1,tm2]!!i) dcL 137 138 sel_trm (i:iL) (Pair tm1 tm2 _ _ _) dcL 139 = sel_trm iL ([tm1,tm2]!!i) dcL 140 141 sel_trm (i:iL) (Binder _ dc tm _ _) dcL 142 | i==0 = sel_dec iL dc dcL 143 | i==1 = sel_trm iL tm (dc:dcL) 144 145 sel_trm (0:iL) (Unary _ tm _ _) dcL 146 = sel_trm iL tm dcL 147 148 sel_trm (i:iL) (Binary' _ tm1 tm2 _ _) dcL 149 = sel_trm iL ([tm1,tm2]!!i) dcL 150 151 sel_trm (i:iL) (Cond (dc @ (Axiom_dec tm inf)) tm1 tm2 _ _) dcL 152 | i==0 = sel_dec iL dc dcL 153 | i/=0 = sel_trm iL ([tm1,tm2]!!(i-1)) (dc1:dcL) 154 where 155 dc1 = if i==1 156 then dc 157 else if i==2 158 then Axiom_dec (Unary Not tm [] inf) [] 159 else error "sel_trm" 160 161 sel_trm (i:iL) (Recurse tmL _ _ _) dcL 162 = sel_trm iL (tmL!!i) dcL 163 164 sel_trm [] tm dcL = (tm,dcL) 165 166 -- sel_trm _ _ _ = error "Subterm" -- ** exn 167 168 169 sel_dec :: [ Int ] -> IDec -> [ IDec ] -> ( ITrm , [ IDec ] ) 170 171 sel_dec (0:iL) (Symbol_dec tm _) dcL 172 = sel_trm iL tm dcL 173 174 sel_dec (0:iL) (Axiom_dec tm _) dcL 175 = sel_trm iL tm dcL 176 177 sel_dec (i:iL) (Decpair dc1 dc2 _) dcL 178 | i==0 = sel_dec iL dc1 dcL 179 | i==1 = sel_dec iL dc2 (dc1:dcL) 180 181 -- sel_dec _ _ _ = error "Subterm" -- ** exn 182 183 184 185 186 187 188 189 {- 190 * replace a subterm of a term. this function assumes that the replacement 191 * subterm is of an appropriate type and defined on the right signature. 192 * 193 -} 194 195 -- replace_trm :: ITrm -> ITrm -> [ Int ] -> ITrm 196 197 replace_trm tm1 tm2 iL 198 = rep_trm iL tm1 199 where 200 swap 0 (_:xL) y 201 = y : xL 202 203 swap i (x:xL) y 204 = x : swap (i-1) xL y 205 206 -- swap _ _ _ = error "Subterm" -- ** exn 207 208 rep_trm :: [Int] -> ITrm -> ITrm 209 210 rep_trm (i:iL) (App tm1 tm2 tyL inf) 211 | i==0 = App (rep_trm iL tm1) tm2 tyL inf 212 | i==1 = App tm1 (rep_trm iL tm2) tyL inf 213 214 rep_trm (i:iL) (Pair tm1 tm2 tm3 tyL inf) 215 | i==0 = Pair (rep_trm iL tm1) tm2 tm3 tyL inf 216 | i==1 = Pair tm1 (rep_trm iL tm2) tm3 tyL inf 217 218 rep_trm (i:iL) (Binder q dc tm tyL inf) 219 | i==0 = Binder q (rep_dec iL dc) tm tyL inf 220 | i==1 = Binder q dc (rep_trm iL tm) tyL inf 221 222 rep_trm (i:iL) (Unary c tm tyL inf) 223 | i==0 = Unary c (rep_trm iL tm) tyL inf 224 225 rep_trm (i:iL) (Binary' c tm1 tm2 tyL inf) 226 | i==0 = Binary' c (rep_trm iL tm1) tm2 tyL inf 227 | i==1 = Binary' c tm1 (rep_trm iL tm2) tyL inf 228 229 rep_trm (i:iL) (Cond dc tm1 tm2 tyL inf) 230 | i==0 = Cond (rep_dec iL dc) tm1 tm2 tyL inf 231 | i==1 = Cond dc (rep_trm iL tm1) tm2 tyL inf 232 | i==2 = Cond dc tm1 (rep_trm iL tm2) tyL inf 233 234 rep_trm (i:iL) (Recurse tmL tm tyL inf) 235 = Recurse tmL1 tm tyL inf 236 where 237 tmL1 = swap i tmL (rep_trm iL (tmL!!i)) 238 239 rep_trm [] _ = tm2 240 241 rep_trm iL _ = error ( "iL(len):" ++ show ( length iL) ++ "\niL:" ++ concat ( map show iL ) ++ "|" ) --"Subterm" -- ** exn 242 243 244 245 rep_dec (0:iL) (Symbol_dec tm inf) 246 = Symbol_dec (rep_trm iL tm) inf 247 248 rep_dec (0:iL) (Axiom_dec tm inf) 249 = Axiom_dec (rep_trm iL tm) inf 250 251 rep_dec (i:iL) (Decpair dc1 dc2 inf) 252 | i==0 = Decpair (rep_dec iL dc1) dc2 inf 253 | i==1 = Decpair dc1 (rep_dec iL dc2) inf 254 255 -- rep_dec _ _ = error "Subterm" -- ** exn 256 257 258 259 260 261 262 {- 263 * map two functions (one for symbol and one for constructors) over 264 * a term, applying then to all the non localally bound symbols and 265 * constructors in the term. Return two functions: the first applies to 266 * terms; the second to declarations 267 * 268 -} 269 270 type Sym_map = Int -> Int -> Int -> [ ITrm ] -> [ Attribute ] -> ITrm 271 272 type Const_map = Int -> Int -> Int -> Int -> [ ITrm ] -> [ Attribute ] -> ITrm 273 274 275 -- map_fn :: Sym_map -> Const_map -> (( ITrm -> ITrm ) , ( IDec -> IDec )) 276 277 map_fn map_symbol map_const 278 = (map_trm 0, map_dec 0) 279 where 280 map_trm n (Sym i j tyL inf) 281 = if i < n then Sym i j tyL1 inf 282 else map_symbol n i j tyL1 inf 283 where 284 tyL1 = map (map_trm n) tyL 285 286 map_trm n (Const i j k tyL inf) 287 = if i < n then Const i j k tyL1 inf 288 else map_const n i j k tyL1 inf 289 where 290 tyL1 = map (map_trm n) tyL 291 292 map_trm n (Constant c tyL inf) 293 = Constant c (map (map_trm n) tyL) inf 294 295 map_trm n (App tm1 tm2 tyL inf) 296 = App (map_trm n tm1) (map_trm n tm2) (map (map_trm n) tyL) inf 297 298 map_trm n (Pair tm1 tm2 tm3 tyL inf) 299 = Pair (map_trm n tm1) (map_trm n tm2) (map_trm n tm3) 300 (map (map_trm n) tyL) inf 301 302 map_trm n (Binder q dc tm tyL inf) 303 = Binder q (map_dec n dc) (map_trm (n+1) tm) 304 (map (map_trm n) tyL) inf 305 306 map_trm n (Unary c tm tyL inf) 307 = Unary c (map_trm n tm) (map (map_trm n) tyL) inf 308 309 map_trm n (Binary' c tm1 tm2 tyL inf) 310 = Binary' c (map_trm n tm1) (map_trm n tm2) 311 (map (map_trm n) tyL) inf 312 313 map_trm n (Cond dc tm1 tm2 tyL inf) 314 = Cond dc1 tm3 tm4 tyL1 inf 315 where 316 dc1 = map_dec n dc 317 tm3 = map_trm (n+1) tm1 318 tm4 = map_trm (n+1) tm2 319 tyL1 = map (map_trm n) tyL 320 321 map_trm n (Recurse tmL tm tyL inf) 322 = Recurse tmL1 tm1 tyL1 inf 323 where 324 tmL1 = map (map_trm n) tmL 325 tm1 = map_trm n tm 326 tyL1 = map (map_trm n) tyL 327 328 map_trm n (Tagid tg tg_argL) 329 = Tagid tg tg_argL -- need to shift tg_argL 330 331 map_trm n (ITrm_Err mesg ) 332 = ITrm_Err mesg 333 334 335 336 map_dec n (Symbol_dec tm inf) 337 = Symbol_dec (map_trm n tm) inf 338 339 map_dec n (Axiom_dec tm inf) 340 = Axiom_dec (map_trm n tm) inf 341 342 map_dec n (Decpair dc1 dc2 inf) 343 = Decpair (map_dec n dc1) (map_dec (n+1) dc2) inf 344 345 map_dec n (Def tm1 tm2 inf) 346 = Def (map_trm n tm1) (map_trm n tm2) inf 347 348 map_dec n (Data dcL tmLL inf) 349 = Data dcl' tmLL' inf' 350 where 351 (dcl', tmLL', inf') = (map_data n dcL tmLL inf) 352 353 354 map_data n [] tmLL inf 355 = ([], map (map (map_trm (n+1))) tmLL,inf) 356 357 map_data n (dc:dcL) tmLL inf 358 = (map_dec n dc:dcL,tmLL1,inf1) 359 where 360 (dcL1,tmLL1,inf1) = map_data (n+1) dcL tmLL inf 361 362 363 364 365 366 {- return the nth sub-signature of a signature. -} 367 368 nth_sgn 0 sg = sg 369 370 nth_sgn i (Extend _ sg _) 371 = nth_sgn (i-1) sg 372 373 nth_sgn i (Combine sg1 sg2 k _ _) 374 = if i<k then nth_sgn (i-1) sg2 375 else nth_sgn (i-k-1) sg1 376 377 nth_sgn i (Share sg _ _ _ _ _) 378 = nth_sgn (i-1) sg 379 380 --nth_sgn i (Empty _) 381 -- = error "Nth_Sgn" -- ** exn 382 383 384 385 386 387 388 389 {- return the ith declaration of a signature -} 390 391 nth_dec i sg 392 = case nth_sgn i sg of 393 Extend dc _ _ -> dc 394 -- _ -> error "NthDec" -- ** exn 395 396 397 398 399 400 {- Compute the length of a signature -} 401 402 -- len_sgn :: ISgn -> Int 403 404 len_sgn (Empty _) = 0 405 406 len_sgn (Extend _ sg _) = 1 + len_sgn sg 407 408 len_sgn (Combine sg _ k _ _) = 1+ k + len_sgn sg 409 410 len_sgn (Share sg _ _ _ _ _) = 1 + len_sgn sg 411