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_Core4 where 16 17 import Vtslib 18 19 import Core_datatype 20 21 import Sub_Core1 22 23 import Sub_Core2 24 25 import Sub_Core3 26 27 28 29 30 get_dec_att (Symbol_dec _ att) = att 31 32 get_dec_att (Axiom_dec _ att) = att 33 34 get_dec_att (Def _ _ att) = att 35 36 get_dec_att (Data _ _ att) = att 37 38 get_dec_att (Decpair _ _ att) = att 39 40 41 42 43 44 set_dec_att (Symbol_dec tm _) att 45 = Symbol_dec tm att 46 47 set_dec_att (Axiom_dec tm _) att 48 = Axiom_dec tm att 49 50 set_dec_att (Def tm1 tm2 _) att 51 = Def tm1 tm2 att 52 53 set_dec_att (Data dcL tl _) att 54 = Data dcL tl att 55 56 set_dec_att (Decpair dc1 dc2 _) att 57 = Decpair dc1 dc2 att 58 59 60 61 62 63 get_sgn_att (Empty att) = att 64 65 get_sgn_att (Extend _ _ att) = att 66 67 get_sgn_att (Combine _ _ _ _ att) = att 68 69 get_sgn_att (Share _ _ _ _ _ att) = att 70 71 72 73 74 75 set_sgn_att (Empty _) att = Empty att 76 77 set_sgn_att (Extend dc sg _) att = Extend dc sg att 78 79 set_sgn_att (Combine sg1 sg2 l sm _) att = Combine sg1 sg2 l sm att 80 81 set_sgn_att (Share sg i j k sm _) att = Share sg i j k sm att 82 83 84 85 86 {- 87 (* given a signature and a datasum return the type of of each *) 88 (* clause in each prong of a corrsponding recurse expression of *) 89 (* which the datasum would be the type *) 90 -} 91 92 add_type (Sym i j tmL att) ty 93 = Sym i j (ty:tmL) att 94 95 add_type (App tm1 tm2 tmL att) ty 96 = App tm1 tm2 (ty:tmL) att 97 98 add_type (Pair tm1 tm2 tm3 tmL att) ty 99 = Pair tm1 tm2 tm3 (ty:tmL) att 100 101 add_type (Constant c tmL att) ty 102 = Constant c (ty:tmL) att 103 104 add_type (Binder c tm1 tm2 tmL att) ty 105 = Binder c tm1 tm2 (ty:tmL) att 106 107 add_type (Unary c tm tmL att) ty 108 = Unary c tm (ty:tmL) att 109 110 add_type (Binary' c dc tm tmL att) ty 111 = Binary' c dc tm (ty:tmL) att 112 113 add_type (Cond dc tm1 tm2 tmL att) ty 114 = Cond dc tm1 tm2 (ty:tmL) att 115 116 add_type (Const i j k tmL att) ty 117 = Const i j k (ty:tmL) att 118 119 add_type (Recurse tmL tm tyL att) ty 120 = Recurse tmL tm (ty:tyL) att 121 122 123 124 125 126 is_sub_sgn sg1 sg2 127 = sub_sgn 0 sg2 128 where 129 sub_sgn i sg2 130 = if eq_sgn sg1 sg2 131 then SOME i 132 else 133 case sg2 of 134 Empty _ 135 -> NONE 136 Extend _ sg3 _ 137 -> sub_sgn (i+1) sg3 138 Combine sg3 sg4 k _ _ 139 -> case sub_sgn i sg4 of 140 SOME i -> SOME i 141 NONE -> sub_sgn (i+k) sg3 142 Share sg3 _ _ _ _ _ 143 -> sub_sgn i sg3 144 145 146 eta_match dc tm i = error "VTS_ERROR" -- ** exn 147 148 149 150 151 152 make_rec fntype clause_ty [] 153 = clause_ty 154 155 make_rec (fntype @ ( Binder Pi dc tm _ _)) clause_ty (ty:tyL) 156 = Binder Pi (Symbol_dec ty2 []) ty1 [] [] 157 where 158 ty1 = make_rec (shift_trm [] 1 fntype) (shift_trm [] 1 clause_ty) tyL 159 ty2 = subst_trm dc tm ty 160 161 162 163 164 165 166 gen_type i (fntype @(Binder Pi dc tm _ _)) rectypeL const [] 167 = make_rec fntype (subst_trm dc tm const) rectypeL 168 169 gen_type i (fntype @(Binder Pi dc tm _ _)) rectypeL const (ty : tyL) 170 = Binder Pi (Symbol_dec (shift_trm [] i ty) []) ty1 [] [] 171 where 172 const1 = App (shift_trm [] 1 const) (Sym 0 0 [] []) [] [] 173 fntype1 = shift_trm [] 1 fntype 174 rectypeL1 = map (shift_trm [] 1) rectypeL ++ 175 if eq_trm ty (Sym 0 0 [] []) 176 then [Sym i 1 [] []] 177 else [] 178 ty1 = gen_type (i+1) fntype1 rectypeL1 const1 tyL 179 180 --gen_type _ _ _ _ _ = error "VTS_ERROR" -- ** exn 181 182 183 184 185 186 187 gen_typeL _ _ _ [] _ _ _ = [] 188 189 gen_typeL tyL tm fntype (tmL : tmLL) i j k 190 = substL (length tyL - 1) (subst_trm dc ty tm) tyL : 191 gen_typeL tyL tm fntype tmLL i j (k+1) 192 where 193 const = foldr make_app (Const i j k [] []) ( reverse tyL ) 194 ty = gen_type 0 fntype [] const tmL 195 dc = Symbol_dec tm [] 196 197 substL i tm [] = tm 198 substL i tm (tm1:tmL1) 199 = substL (i-1) (subst_trm dc tm (shift_trm [] i tm1)) tmL1 200 201 202 203 204 205 get_datatype_info sg (App tm1 tm2 _ _) 206 = (i,j,tm2:tmL,dcL,tmLLL) 207 where 208 (i,j,tmL,dcL,tmLLL) = get_datatype_info sg tm1 209 210 get_datatype_info sg (Const i j k _ _) 211 = case shift_dec (get_share_map sg) i dc of 212 Data dcL tmLLL _ -> (i,j,[],dcL,tmLLL) 213 -- _ -> error "VTS_ERROR" -- ** exn 214 where 215 dc = extract_dc j (nth_dec i sg) 216 217 --get_datatype_info _ _ = error "VTS_ERROR" -- ** exn 218 219 220 221 222 223 224 no_params :: [ITrm] -> Int 225 226 no_params ((Sym _ _ _ _) : tmL) = 2 + no_params tmL 227 228 no_params (_ : tmL) = no_params tmL 229 230 no_params [] = 0 231 232 233 234 235 236 237 shift :: Int -> Int -> ITrm -> ITrm 238 239 shift i j tm 240 = tm3 241 where 242 bind tm = Binder Pi (Symbol_dec (Sym 0 0 [] []) []) tm [] [] 243 body (Binder _ _ tm _ _) = tm 244 -- body _ = error "System_Error" -- ** exn 245 tm1 = for i bind tm 246 tm2 = shift_trm [] j tm1 247 tm3 = for i body tm2 248 249 250 251 252 253 clause_types :: ISgn -> ITrm -> ITrm -> ([ITrm], [Int]) 254 255 clause_types sg dtype fntype 256 = (clauses,params) 257 where 258 (i,j,spec,dcL,tmLL) = get_datatype_info sg dtype 259 fntype1 = shift_trm [] (length dcL + 1) fntype 260 dtype1 = shift_trm [] (length dcL) dtype 261 tmLL1 = map (map (shift (length dcL + 1) j)) tmLL 262 clauses = gen_typeL spec dtype1 fntype1 tmLL1 i j 0 263 params = map no_params tmLL 264 265 266 267 268 269 make_ind tm rectype [] = rectype 270 271 make_ind tm rectype (ty : tyL) 272 = Binder Imp ty2 ty1 [] [] 273 where 274 ty1 = make_ind tm rectype tyL 275 ty2 = Symbol_dec ( make_app tm ty ) [] 276 277 278 279 280 281 ind_type i tm rectypeL const [] 282 = make_ind tm (make_app tm const) rectypeL 283 284 ind_type i tm rectypeL const (ty : tyL) 285 = Binder Forall (Symbol_dec (shift_trm [] i ty) []) ty1 [] [] 286 where 287 const1 = make_app (shift_trm [] 1 const) (Sym 0 0 [] []) 288 tm1 = shift_trm [] 1 tm 289 rectypeL1 = map (shift_trm [] 1) rectypeL ++ 290 if eq_trm ty (Sym 0 0 [] []) 291 then [ty] 292 else [] 293 ty1 = ind_type (i+1) tm1 rectypeL1 const1 tyL 294 295 296 297 298 ind_typeL _ _ _ [] _ _ _ = [] 299 300 ind_typeL rectype sms tm (tyL:tyLL) i j k 301 = (ty2 : ind_typeL rectype sms tm tyLL i j (k+1)) 302 where 303 const = foldr make_app (Const i j k [] []) ( reverse sms ) 304 ty1 = ind_type 0 tm [] const tyL 305 ty2 = subst_trm (Symbol_dec (Const i j 0 [] []) []) ty1 rectype 306 307 308 309 310 311 induction_trm sg tm 312 = foldr make_forall tm2 ( reverse (dc : dcL)) 313 where 314 make_imp tm1 tm2 = Binder Imp dc_imp tm2 [] [] 315 make_forall dc tm = Binder Forall dc tm [] [] 316 (i,j,_,dcL,tmLL) = get_datatype_info sg tm 317 tmLL1 = map (map (shift 1 1)) tmLL 318 sms = mk_smsl dcL 0 [] 319 dtype = foldr make_app (shift_trm [] (length dcL) tm) ( reverse sms ) 320 ty = Binder Pi (Symbol_dec dtype []) (Constant Bool' [] []) [] [] 321 dc = Symbol_dec ty [] 322 dtype1 = shift_trm [] 1 dtype 323 sms1 = map (shift_trm [] 2) sms 324 tmL = ind_typeL dtype1 sms1 (Sym 1 0 [] []) 325 tmLL1 (2+i+length dcL) j 1 326 dc_imp = Symbol_dec tm1 [] 327 tm1 = Binder Forall (Symbol_dec dtype1 []) tm1 [] [] 328 where 329 tm1 = make_app (Sym 1 0 [] []) (Sym 0 0 [] []) 330 tm2 = foldr1 make_imp (tmL ++ [tm1]) 331 332 333 334 335 336 equiv :: (Eq b) => b -> [b] -> [Int] 337 338 equiv i m 339 = equivf 0 m 340 where 341 equivf j [] = [] 342 343 equivf j (k:m) 344 = (if k==i then [j] else []) ++ equivf (j+1) m 345 346 347 348 349 350 union (i:l) m 351 = (if i `elem` m then [] else [i]) ++ union l m 352 353 union [] m = m 354 355 356 357 358 update :: b -> [Int] -> [b] -> [b] 359 360 update i eq m 361 = updatef 0 m 362 where 363 updatef j [] = [] 364 updatef j (k:m) 365 = (if j `elem` eq then [i] else [k]) ++ updatef (j+1) m 366 367 368 369 370 canonical :: Int -> [b] -> b 371 372 canonical i m = m !! i 373 374 375 376 377 addequiv :: (Ord a) => (Int, Int) -> [a] -> [a] 378 379 addequiv (i,j) m 380 = update (min i' j') eqij m 381 where 382 i' = canonical i m 383 j' = canonical j m 384 eqi = equiv i' m 385 eqj = equiv j' m 386 eqij = union eqi eqj 387 388 389 390 391 392 addequivL i j k m 393 = foldr addequiv m (list i j k) 394 where 395 list i' j' 0 = [] 396 list i' j' k' = (i',j') : list (i'+1) (j'+1) (k'-1) 397 398 399 400 401 402 403 split_def (Def tm1 tm2 _) 404 = (Symbol_dec tm2 [],tm1,tm2) 405 406 split_def (Decpair dc1 dc2 _) 407 = (Decpair dc3 dc4 [] , Pair tm1 tm6 tm5 [] [] , tm5) 408 where 409 (dc3,tm1,tm2) = split_def dc1 410 (dc4,tm3,tm4) = split_def dc2 411 tm5 = shift_trm [] 1 (subst_trm dc1 tm4 tm1) 412 tm6 = subst_trm dc1 tm3 tm1 413 tm7 = Binder Sigma dc3 tm5 [] [] 414 415 --split_def _ = error "VTS_ERROR" -- ** exn 416