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_Core3 where 16 17 import Vtslib 18 19 import Core_datatype 20 21 import Sub_Core2 22 23 import Sub_Core1 24 25 26 27 28 select_sm_ty f sg i j 29 = case extract_dc j dc of 30 Symbol_dec tm _ | f -> uncurry_trm dc j tm 31 Axiom_dec tm _ | not f -> uncurry_trm dc j tm 32 Def _ tm _ | f -> uncurry_trm dc j tm 33 Def tm _ _ | not f -> Binary' Eq' (Sym 0 j [] []) 34 (uncurry_trm dc j tm) [] [] 35 _ -> error ("select: " ++ show f ++ show i ++ show j ++ "|\n") 36 where 37 dc = nth_dec i sg 38 39 40 41 42 select_cn_ty :: ISgn -> Int -> Int -> Int -> ITrm 43 44 select_cn_ty sg i j k 45 = Sym 0 0 [] [] 46 {- 47 = case extract_dc j dc of 48 Data dcL tmL _ 49 -> if k == 0 then uncurry_trm dc j ty 50 else remake_ty ty4 dcL 51 (foldr make_app sms_base (reverse sms)) 52 where 53 ty = foldr mk_pi (Constant (Univ 0) [] []) 54 ( reverse dcL ) 55 sms = mk_smsl dcL 0 [] 56 ty1 = foldr make_app (Sym 0 0 [] []) ( reverse sms ) 57 ty2 = foldr mk_fnspace (Sym 0 0 [] []) (tmL!!k-1) 58 d1 = Symbol_dec (Constant (Univ 0) [] [] ) [] 59 ty3 = foldr mk_pi (Binder Pi d1 ty2 [] []) 60 ( reverse dcL ) 61 ty4 = uncurry_trm dc j ty3 62 sms_base = Const (length dcL) j 0 [] [] 63 -- _ -> error "BadIndex" -- ** exn 64 where 65 dc = nth_dec i sg 66 -} 67 68 69 make_app tm1 tm2 = App tm1 tm2 [] [] 70 71 72 {- return the type of a symbol -} 73 74 typ_of_sm sg i j 75 = shift_trm (get_share_map sg) i ty1 76 where 77 ty1 = select_sm_ty True sg i j -- partain: was true 78 79 80 81 82 83 {- return the type of a constructor -} 84 85 typ_of_cn sg i j k 86 = shift_trm (get_share_map sg) i ty1 87 where 88 ty1 = select_cn_ty sg i j k 89 90 91 92 93 94 95 {- return the type of an axiom -} 96 97 typ_of_axm sg i j 98 = shift_trm (get_share_map sg) i ty1 99 where 100 ty1 = select_sm_ty False sg i j -- partain: was false 101 102 103 104 105 106 {- extract the alternative types for a term -} 107 108 other_typ (Sym _ _ tmL _) = tmL 109 110 other_typ (App _ _ tmL _) = tmL 111 112 other_typ (Pair _ _ _ tmL _) = tmL 113 114 other_typ (Const _ _ _ tmL _) = tmL 115 116 other_typ (Binder _ _ _ tmL _) = tmL 117 118 other_typ (Unary _ _ tmL _) = tmL 119 120 other_typ (Binary' _ _ _ tmL _) = tmL 121 122 other_typ (Cond _ _ _ tmL _) = tmL 123 124 other_typ (Constant _ tmL _) = tmL 125 126 other_typ (Recurse _ _ tmL _) = tmL 127 128 129 130 131 132 {- 133 * return the type of a term. If a term has alternative type other 134 * than its natural type return that that. 135 * 136 -} 137 138 -- typ_of_trm :: ISgn -> ITrm -> ITrm 139 140 typ_of_trm sg tm 141 = case other_typ tm of 142 [] -> typ_of_trm' sg tm 143 (tm:_) -> tm 144 145 146 147 typ_of_trm' sg (Sym i j _ _) 148 = typ_of_sm sg i j 149 150 typ_of_trm' sg (Const i j k _ _) 151 = typ_of_cn sg i j k 152 153 typ_of_trm' sg (App tm1 tm2 _ _) 154 = case typ_of_trm sg tm1 of 155 Binder Pi dc tm3 _ _ 156 -> subst_trm dc tm3 tm2 157 _ -> case typ_of_trm' sg tm1 of 158 Binder Pi dc tm3 _ _ 159 -> subst_trm dc tm3 tm2 160 -- _ -> error "TypeOfTerm" -- ** exn 161 162 typ_of_trm' sg (Pair tm1 tm2 tm3 _ _) 163 = tm3 164 165 typ_of_trm' sg (Binder q dc tm _ _) 166 = typ_of_bnd sg q dc tm 167 168 typ_of_trm' sg (Constant c _ _) 169 = typ_of_cnt c 170 171 typ_of_trm' sg (Recurse _ tm _ _) 172 = tm 173 174 typ_of_trm' _ _ 175 = Constant Bool' [] [] 176 177 178 179 180 181 typ_of_bnd sg Forall dc tm 182 = Constant Bool' [] [] 183 184 typ_of_bnd sg Exists dc tm 185 = Constant Bool' [] [] 186 187 typ_of_bnd sg Imp dc tm 188 = Constant Bool' [] [] 189 190 typ_of_bnd sg Pi dc tm 191 = Constant (Univ (max i j)) [] [] 192 where 193 sg1 = Extend dc sg [] 194 (Constant (Univ i) _ _) = typ_of_trm sg1 tm 195 (Constant (Univ j) _ _) = typ_of_trm sg (typ_of_dec dc) 196 197 typ_of_bnd sg Sigma dc tm 198 = Constant (Univ (max i j)) [] [] 199 where 200 sg1 = Extend dc sg [] 201 (Constant (Univ i) _ _) = typ_of_trm sg1 tm 202 (Constant (Univ j) _ _) = typ_of_trm sg (typ_of_dec dc) 203 204 typ_of_bnd sg Subtype dc tm 205 = Constant (Univ 0) [] [] 206 207 typ_of_bnd sg Lambda dc tm 208 = Binder Pi dc (typ_of_trm (Extend dc sg []) tm) [] [] 209 210 typ_of_bnd sg Choose dc tm 211 = Binder Subtype dc tm [] [] 212 213 --typ_of_bnd _ _ _ _ = error "System_Error" -- ** exn 214 215 216 217 218 219 220 221 typ_of_cnt T = Constant Bool' [] [] 222 223 typ_of_cnt F = Constant Bool' [] [] 224 225 typ_of_cnt Bool' = Constant (Univ 0) [] [] 226 227 typ_of_cnt (Univ i) = Constant (Univ (i+1)) [] [] 228 229 230 231 232 233 234 {- 235 * evaluate a propositional term. 236 * A propositional term consists of: 237 * T, F, #fo d.t, #ex d.t, t1 #an t1, t1 #or t2, t1 #im t2, t1 = t2, #no t 238 * and locally bound symbols of type bool. 239 * 240 -} 241 242 -- eval :: ITrm -> Bool 243 244 eval (Constant T _ _) = True 245 246 eval (Constant F _ _) = False 247 248 --eval (Constant _ _ _) = error "EvalError" -- ** exn 249 250 eval (Binder Forall dc tm _ _) 251 = eval_quant forall dc tm 252 253 eval (Binder Exists dc tm _ _) 254 = eval_quant exists dc tm 255 256 eval (Binder Imp dc tm _ _) 257 = not (eval ( typ_of_dec dc)) || eval tm 258 259 --eval (Binder _ _ _ _ _) 260 -- = error "EvalError" 261 262 eval (Binary' And tm1 tm2 _ _) 263 = eval tm1 && eval tm2 264 265 eval (Binary' Or tm1 tm2 _ _) 266 = eval tm1 || eval tm2 267 268 eval (Binary' Eq' tm1 tm2 _ _) 269 = eval tm1 == eval tm2 270 271 eval (Unary Not tm _ _) 272 = not (eval tm) 273 274 eval (Cond dc tm1 tm2 _ _) 275 = eval (subst_trm dc tm1 (Constant T [] [])) && 276 eval (subst_trm dc tm1 (Constant F [] [])) 277 278 --eval _ = error "EvalError" -- ** exn 279 280 281 282 283 284 eval_quant f dc tm 285 = f (eval . subst_trm dc tm) (truth_table dc) 286 287 288 289 290 291 truth_table (Symbol_dec (Constant Bool' _ _ ) _) 292 = [ Constant T [] [] , Constant F [] [] ] 293 294 truth_table (Decpair dc1 dc2 _) 295 = make_pair (truth_table dc1) (truth_table dc2) 296 297 --truth_table _ = error "EvalError" -- ** exn 298 299 300 301 302 303 make_pair [] _ = [] 304 305 make_pair (tm:tmL) l 306 = map (\ x -> Pair tm x (Constant Bool' [] []) [] []) l 307 ++ make_pair tmL l 308 309 310 311 312 313 {- 314 * check to see if any symbols are defined at particular level 315 -} 316 317 occurs n (Sym i _ _ _) 318 = n == i 319 320 occurs n (App tm1 tm2 _ _) 321 = occurs n tm1 || occurs n tm2 322 323 occurs n (Pair tm1 tm2 tm3 _ _) 324 = occurs n tm1 || occurs n tm2 || occurs n tm3 325 326 occurs n (Binder _ dc tm _ _) 327 = occurs' n dc || occurs (n+1) tm 328 329 occurs n (Unary _ tm _ _) 330 = occurs n tm 331 332 occurs n (Binary' _ tm1 tm2 _ _) 333 = occurs n tm1 || occurs n tm2 334 335 occurs n (Cond dc tm1 tm2 _ _) 336 = occurs' n dc || occurs (n+1) tm1 || occurs (n+1) tm2 337 338 occurs n (Recurse tmL tm _ _) 339 = exists (occurs n) tmL || occurs n tm 340 341 occurs _ _ = False 342 343 344 345 346 347 occurs' n (Symbol_dec tm _) 348 = occurs n tm 349 350 occurs' n (Axiom_dec tm _) 351 = occurs n tm 352 353 occurs' n (Decpair dc1 dc2 _) 354 = occurs' n dc1 || occurs' (n+1) dc2 355 356 --occurs' _ _ = error "VTS_ERROR" -- ** exn 357 358 359 360 361 362 {- 363 * functions for retrieving and setting the information fields of 364 * term, decs and sigs. 365 -} 366 367 get_trm_att tm iL 368 = case subtm of 369 (Sym _ _ _ att) -> att 370 (App _ _ _ att) -> att 371 (Pair _ _ _ _ att) -> att 372 (Constant _ _ att) -> att 373 (Binder _ _ _ _ att) -> att 374 (Unary _ _ _ att) -> att 375 (Binary' _ _ _ _ att) -> att 376 (Cond _ _ _ _ att) -> att 377 (Const _ _ _ _ att) -> att 378 (Recurse _ _ _ att) -> att 379 where 380 (subtm,_) = select_trm tm iL 381 382 383 384 385 set_trm_att tm iL att 386 = replace_trm tm (set subtm) iL 387 where 388 set (Sym i j tmL _) = Sym i j tmL att 389 set (App tm1 tm2 tmL _) = App tm1 tm2 tmL att 390 set (Pair tm1 tm2 tm3 tmL _) = Pair tm1 tm2 tm3 tmL att 391 set (Constant c tmL _) = Constant c tmL att 392 set (Binder c tm1 tm2 tmL _) = Binder c tm1 tm2 tmL att 393 set (Unary c tm tmL _) = Unary c tm tmL att 394 set (Binary' c dc tm tmL _) = Binary' c dc tm tmL att 395 set (Cond dc tm1 tm2 tmL _) = Cond dc tm1 tm2 tmL att 396 set (Const i j k tmL _) = Const i j k tmL att 397 set (Recurse tmL tm tyL _) = Recurse tmL tm tyL att 398 399 (subtm,_) = select_trm tm iL 400 401 402 403