1(*---------------------------------------------------------------------------* 2 * Building records of facts about datatypes. * 3 *---------------------------------------------------------------------------*) 4 5structure TypeBasePure :> TypeBasePure = 6struct 7 8open HolKernel boolSyntax Drule Conv Prim_rec; 9type simpfrag = simpfrag.simpfrag 10type rcd_fieldinfo = {ty: hol_type, accessor: term, fupd : term} 11 12val ERR = mk_HOL_ERR "TypeBasePure"; 13val WARN = HOL_WARNING "TypeBasePure"; 14 15fun type_names ty = 16 let val {Thy,Tyop,Args} = Type.dest_thy_type ty 17 in (Thy,Tyop) 18 end; 19 20datatype shared_thm 21 = ORIG of thm 22 | COPY of (string * string) * thm; 23 24 type mk_datatype_record = 25 {ax : shared_thm, 26 induction : shared_thm, 27 case_def : thm, 28 case_cong : thm, 29 case_eq : thm, 30 nchotomy : thm, 31 size : (term * shared_thm) option, 32 encode : (term * shared_thm) option, 33 lift : term option, 34 one_one : thm option, 35 distinct : thm option, 36 fields : (string * rcd_fieldinfo) list, 37 accessors : thm list, 38 updates : thm list, 39 destructors : thm list, 40 recognizers : thm list} 41 42fun thm_of (ORIG x) = x 43 | thm_of (COPY (s,x)) = x; 44 45(*---------------------------------------------------------------------------*) 46(* Support both constructor-style datatypes and other types as well. *) 47(*---------------------------------------------------------------------------*) 48 49type dtyinfo = 50 {ty : hol_type, 51 axiom : shared_thm, 52 induction : shared_thm, 53 case_def : thm, 54 case_eq : thm, 55 case_cong : thm, 56 nchotomy : thm, 57 case_const : term, 58 constructors : term list, 59 destructors : thm list, 60 recognizers : thm list, 61 size : (term * shared_thm) option, 62 encode : (term * shared_thm) option, 63 lift : term option, 64 distinct : thm option, 65 one_one : thm option, 66 fields : (string * rcd_fieldinfo) list, 67 accessors : thm list, 68 updates : thm list, 69 simpls : simpfrag, 70 extra : ThyDataSexp.t list} ; 71 72open FunctionalRecordUpdate 73fun gcons_mkUp z = makeUpdate21 z 74fun update_DTY z = let 75 fun from accessors axiom case_cong case_const case_def case_eq 76 constructors destructors distinct encode extra fields induction lift 77 nchotomy one_one recognizers simpls size ty updates = 78 {accessors = accessors, axiom = axiom, case_cong = case_cong, 79 case_const = case_const, case_def = case_def, case_eq = case_eq, 80 constructors = constructors, destructors = destructors, 81 distinct = distinct, encode = encode, extra = extra, fields = fields, 82 induction = induction, lift = lift, nchotomy = nchotomy, 83 one_one = one_one, recognizers = recognizers, simpls = simpls, 84 size = size, ty = ty, updates = updates} 85 (* fields in reverse order to above *) 86 fun from' updates ty size simpls recognizers one_one nchotomy lift induction 87 fields extra encode distinct destructors constructors case_eq 88 case_def case_const case_cong axiom accessors = 89 {accessors = accessors, axiom = axiom, case_cong = case_cong, 90 case_const = case_const, case_def = case_def, case_eq = case_eq, 91 constructors = constructors, destructors = destructors, 92 distinct = distinct, encode = encode, extra = extra, fields = fields, 93 induction = induction, lift = lift, nchotomy = nchotomy, 94 one_one = one_one, recognizers = recognizers, simpls = simpls, 95 size = size, ty = ty, updates = updates} 96 (* first order *) 97 fun to f {accessors, axiom, case_cong, case_const, case_def, case_eq, 98 constructors, destructors, distinct, encode, extra, fields, 99 induction, lift, nchotomy, one_one, recognizers, simpls, size, ty, 100 updates} = 101 f accessors axiom case_cong case_const case_def case_eq 102 constructors destructors distinct encode extra fields induction lift 103 nchotomy one_one recognizers simpls size ty updates 104in 105 gcons_mkUp (from, from', to) 106end z 107 108type ntyrec = {encode : (term * thm) option, 109 extra : ThyDataSexp.t list, 110 induction : thm option, 111 nchotomy : thm option, 112 simpls : simpfrag.simpfrag, 113 size : (term * thm) option 114 }; 115 116fun gcons_mkUp z = makeUpdate6 z 117fun update_NTY z = let 118 fun from encode extra induction nchotomy simpls size = 119 {encode = encode, extra = extra, induction = induction, 120 nchotomy = nchotomy, simpls = simpls, size = size} 121 (* fields in reverse order to above *) 122 fun from' size simpls nchotomy induction extra encode = 123 {encode = encode, extra = extra, induction = induction, 124 nchotomy = nchotomy, simpls = simpls, size = size} 125 (* first order *) 126 fun to f {encode, extra, induction, nchotomy, simpls, size} = 127 f encode extra induction nchotomy simpls size 128in 129 gcons_mkUp (from, from', to) 130end z 131 132 133type ntyinfo = hol_type * ntyrec 134 135datatype tyinfo = DFACTS of dtyinfo 136 | NFACTS of ntyinfo; 137 138 139(*--------------------------------------------------------------------------- 140 Projections 141 ---------------------------------------------------------------------------*) 142 143fun ty_of (DFACTS {ty,...}) = ty 144 | ty_of (NFACTS(ty,_)) = ty; 145 146fun dollarty ty = 147 let val {Thy,Tyop,Args} = dest_thy_type ty 148 in Lib.quote (Thy ^ "$" ^ Tyop) 149 end; 150 151val ty_name_of = type_names o ty_of 152 153fun constructors_of (DFACTS {constructors,...}) = constructors 154 | constructors_of (NFACTS _) = []; 155 156fun destructors_of (DFACTS {destructors,...}) = destructors 157 | destructors_of (NFACTS _) = []; 158 159fun recognizers_of (DFACTS {recognizers,...}) = recognizers 160 | recognizers_of (NFACTS _) = []; 161 162fun case_const_of (DFACTS {case_const,...}) = case_const 163 | case_const_of (NFACTS (ty,_)) = 164 raise ERR "case_const_of" (dollarty ty^" is not a datatype"); 165 166fun case_cong_of (DFACTS {case_cong,...}) = case_cong 167 | case_cong_of (NFACTS (ty,_)) = 168 raise ERR "case_cong_of" (dollarty ty^" is not a datatype"); 169 170fun case_def_of (DFACTS {case_def,...}) = case_def 171 | case_def_of (NFACTS (ty,_)) = 172 raise ERR "case_def_of" (dollarty ty^" is not a datatype"); 173 174fun case_eq_of (DFACTS {case_eq, ...}) = case_eq 175 | case_eq_of (NFACTS (ty,_)) = 176 raise ERR "case_eq_of" (dollarty ty^" is not a datatype"); 177 178fun extra_of (DFACTS{extra,...}) = extra 179 | extra_of (NFACTS(_, {extra,...})) = extra 180 181fun induction_of0 (DFACTS {induction,...}) = induction 182 | induction_of0 (NFACTS (ty,{induction,...})) 183 = raise ERR "induction_of0" "not a mutrec. datatype"; 184 185fun induction_of (DFACTS {induction,...}) = thm_of induction 186 | induction_of (NFACTS(_,{induction=SOME th,...})) = th 187 | induction_of (NFACTS(ty,{induction=NONE,...})) = 188 raise ERR "induction_of" (dollarty ty^" no induction theorem available"); 189 190fun nchotomy_of (DFACTS {nchotomy,...}) = nchotomy 191 | nchotomy_of (NFACTS(_,{nchotomy=SOME th,...})) = th 192 | nchotomy_of (NFACTS(ty,{nchotomy=NONE,...})) = 193 raise ERR "nchotomy_of" (dollarty ty^" no cases theorem available"); 194 195fun distinct_of (DFACTS {distinct,...}) = distinct 196 | distinct_of (NFACTS (ty,_)) = NONE 197 198fun one_one_of (DFACTS {one_one,...}) = one_one 199 | one_one_of (NFACTS (ty,_)) = NONE 200 201fun fields_of (DFACTS {fields,...}) = fields 202 | fields_of (NFACTS _) = []; 203 204fun accessors_of (DFACTS {accessors,...}) = accessors 205 | accessors_of (NFACTS _) = []; 206 207fun updates_of (DFACTS {updates,...}) = updates 208 | updates_of (NFACTS _) = []; 209 210fun simpls_of (DFACTS {simpls,...}) = simpls 211 | simpls_of (NFACTS _) = simpfrag.empty_simpfrag; 212 213fun axiom_of0 (DFACTS {axiom,...}) = axiom 214 | axiom_of0 (NFACTS (ty,_)) = 215 raise ERR "axiom_of0" (dollarty ty^" is not a datatype"); 216 217fun axiom_of (DFACTS {axiom,...}) = thm_of axiom 218 | axiom_of (NFACTS (ty,_)) = 219 raise ERR "axiom_of" (dollarty ty^" is not a datatype"); 220 221fun size_of0 (DFACTS {size,...}) = size 222 | size_of0 (NFACTS (ty,{size,...})) = Option.map (I ## ORIG) size 223 224fun size_of (DFACTS {size=NONE,...}) = NONE 225 | size_of (DFACTS {size=SOME(tm,def),...}) = SOME(tm,thm_of def) 226 | size_of (NFACTS(_,{size,...})) = size; 227 228fun encode_of0(DFACTS {encode,...}) = encode 229 | encode_of0(NFACTS (ty,{encode,...})) = Option.map (I ## ORIG) encode 230 231fun encode_of(DFACTS {encode=NONE,...}) = NONE 232 | encode_of(DFACTS {encode=SOME(tm,def),...}) = SOME(tm,thm_of def) 233 | encode_of(NFACTS(_,{encode,...})) = encode; 234 235fun lift_of(DFACTS {lift,...}) = lift 236 | lift_of(NFACTS (ty,_)) = 237 raise ERR "lift_of" (dollarty ty^" is not a datatype") 238; 239 240fun extras_of (DFACTS{extra,...}) = extra 241 | extras_of (NFACTS(_, {extra,...})) = extra 242 243(*--------------------------------------------------------------------------- 244 Making alterations 245 ---------------------------------------------------------------------------*) 246 247fun put_nchotomy th (DFACTS dty) = DFACTS (update_DTY dty (U #nchotomy th) $$) 248 | put_nchotomy th (NFACTS(ty,ntyr)) = 249 NFACTS(ty,update_NTY ntyr (U #nchotomy (SOME th)) $$) 250 251fun put_simpls thl (DFACTS dty) = DFACTS (update_DTY dty (U #simpls thl) $$) 252 | put_simpls ssf (NFACTS (ty,nty)) = 253 NFACTS(ty, update_NTY nty (U #simpls ssf) $$) 254 255fun add_rewrs thl tyi = 256 let 257 val {convs,rewrs} = simpls_of tyi 258 in 259 put_simpls {convs = convs, rewrs = rewrs @ thl} tyi 260 end 261 262val add_convs = simpfrag.add_convs 263fun add_ssfrag_convs cds (DFACTS dty) = 264 DFACTS (update_DTY dty(U #simpls (add_convs cds (#simpls dty))) $$) 265 | add_ssfrag_convs cds (NFACTS(ty,nty)) = 266 NFACTS(ty, update_NTY nty (U #simpls (add_convs cds (#simpls nty))) $$) 267 268fun put_induction th (DFACTS dty) = DFACTS (update_DTY dty (U #induction th) $$) 269 | put_induction (ORIG th) (NFACTS(ty,ntyr)) = 270 NFACTS(ty,update_NTY ntyr (U #induction (SOME th)) $$) 271 | put_induction (COPY th) (NFACTS _) = 272 raise ERR "put_induction" "non-datatype but mutrec" 273 274fun put_axiom th (DFACTS dty) = DFACTS (update_DTY dty (U #axiom th) $$) 275 | put_axiom _ (NFACTS(ty,ntyr)) = 276 raise ERR "put_axiom" "updating non-datatype" 277 278fun put_size szinfo (DFACTS dty) = 279 DFACTS (update_DTY dty (U #size (SOME szinfo)) $$) 280 | put_size (size_tm,ORIG size_rw) (NFACTS(ty,ntyr)) = 281 NFACTS(ty,update_NTY ntyr (U #size (SOME(size_tm,size_rw))) $$) 282 | put_size (size_tm,COPY size_rw) (NFACTS _) = 283 raise ERR "put_size" "non-datatype but mutrec" 284 285fun put_encode encinfo (DFACTS dty) = 286 DFACTS (update_DTY dty (U #encode (SOME encinfo)) $$) 287 | put_encode (encode_tm,ORIG encode_rw) 288 (NFACTS(ty, ntyr)) = 289 NFACTS(ty, update_NTY ntyr (U #encode (SOME(encode_tm,encode_rw))) $$) 290 | put_encode (encode_tm,COPY encode_rw) (NFACTS _) = 291 raise ERR "put_encode" "non-datatype but mutrec" 292 293fun put_extra e tyi = 294 case tyi of 295 DFACTS dty => DFACTS (update_DTY dty (U #extra e) $$) 296 | NFACTS(ty,ntyr) => NFACTS (ty, update_NTY ntyr (U #extra e) $$) 297 298fun add_extra e tyi = 299 case tyi of 300 DFACTS dty => DFACTS (update_DTY dty (U #extra (#extra dty @ e)) $$) 301 | NFACTS (ty, ntyr) => 302 NFACTS (ty, update_NTY ntyr (U #extra (#extra ntyr @ e)) $$) 303 304fun put_lift lift_tm (DFACTS dty) = 305 DFACTS (update_DTY dty (U #lift (SOME lift_tm)) $$) 306 | put_lift _ _ = raise ERR "put_lift" "not a datatype"; 307 308fun put_fields flds (DFACTS dty) = DFACTS (update_DTY dty (U #fields flds) $$) 309 | put_fields _ _ = raise ERR "put_fields" "not a datatype"; 310 311fun put_accessors thl (DFACTS dty) = 312 DFACTS (update_DTY dty (U #accessors thl) $$) 313 | put_accessors _ _ = raise ERR "put_accessors" "not a datatype"; 314 315fun put_updates thl (DFACTS dty) = 316 DFACTS (update_DTY dty (U #updates thl) $$) 317 | put_updates _ _ = raise ERR "put_updates" "not a datatype"; 318 319fun put_recognizers thl (DFACTS dty) = 320 DFACTS (update_DTY dty (U #recognizers thl) $$) 321 | put_recognizers _ _ = raise ERR "put_recognizers" "not a datatype"; 322 323fun put_destructors thl (DFACTS dty) = 324 DFACTS (update_DTY dty (U #destructors thl) $$) 325 | put_destructors _ _ = raise ERR "put_destructors" "not a datatype"; 326 327(*---------------------------------------------------------------------------* 328 * Returns the datatype name and the constructors. The code is a copy of * 329 * the beginning of "Datatype.define_case". * 330 *---------------------------------------------------------------------------*) 331 332fun basic_info case_def = 333 let val clauses = (strip_conj o concl) case_def 334 val lefts = map (fst o dest_eq o #2 o strip_forall) clauses 335 val constrs = map (#1 o strip_comb o hd o #2 o strip_comb) lefts 336 val ty = type_of (hd (#2 (strip_comb (Lib.trye hd lefts)))) 337 in 338 (ty, type_names ty, constrs) 339 end 340 handle HOL_ERR _ => raise ERR "basic_info" ""; 341 342 343val defn_const = 344 #1 o strip_comb o lhs o #2 o strip_forall o hd o strip_conj o concl; 345 346 347(*---------------------------------------------------------------------------* 348 * The size field is not filled by mk_tyinfo, since that operation * 349 * requires access to the current fact database, and also assumes that * 350 * numbers are in the context, which is not necessarily true. * 351 *---------------------------------------------------------------------------*) 352 353fun mk_datatype_info_no_simpls rcd = 354 let 355 val {ax,case_def,case_eq,case_cong,induction, 356 nchotomy,size,encode,lift,one_one, 357 fields, accessors, updates, distinct, 358 destructors,recognizers} = rcd 359 val (ty,ty_names,constructors) = basic_info case_def 360 in 361 DFACTS 362 {ty = ty, 363 constructors = constructors, 364 destructors = destructors, 365 recognizers = recognizers, 366 case_const = defn_const case_def, 367 case_def = case_def, 368 case_eq = case_eq, 369 case_cong = case_cong, 370 induction = induction, 371 nchotomy = nchotomy, 372 one_one = one_one, 373 distinct = distinct, 374 fields = fields, 375 accessors = accessors, 376 updates = updates, 377 simpls = {rewrs = [], convs = []}, 378 size = size, 379 encode = encode, 380 lift = lift, 381 axiom = ax, 382 extra = []} 383 end 384 385fun gen_std_rewrs tyi = 386 let 387 val D = case distinct_of tyi of NONE => [] | SOME x => CONJUNCTS x 388 val inj = case one_one_of tyi of NONE => [] | SOME th => [th] 389 val c = D @ map GSYM D @ inj 390 in 391 case_def_of tyi :: c handle HOL_ERR _ => c 392 end 393fun add_std_simpls tyi = add_rewrs (gen_std_rewrs tyi) tyi 394 395fun mk_datatype_info rcd = 396 rcd |> mk_datatype_info_no_simpls |> add_std_simpls 397 398local fun mk_ti (n,ax,ind) 399 (cdef::cds) (ccong::cgs) (oo::oos) (d::ds) (nch::nchs) = 400 mk_datatype_info{ax=COPY(n,ax), induction=COPY(n,ind), 401 case_def=cdef,case_cong=ccong, nchotomy=nch, 402 case_eq = 403 prove_case_eq_thm {case_def = cdef, nchotomy = nch}, 404 one_one=oo, distinct=d,size=NONE, encode=NONE, 405 lift=NONE, fields=[], accessors=[],updates=[], 406 recognizers=[],destructors=[]} 407 :: mk_ti (n,ax,ind) cds cgs oos ds nchs 408 | mk_ti _ [] [] [] [] [] = [] 409 | mk_ti _ [] _ _ _ _ = raise ERR "gen_tyinfo" "Too few case defns" 410 | mk_ti _ _ _ _ _ _ = raise ERR "gen_tyinfo" "Too many case defns" 411in 412fun gen_datatype_info {ax, ind, case_defs} = 413 let val nchotomyl = prove_cases_thm ind 414 val case_congs = map2 case_cong_thm nchotomyl case_defs 415 val one_ones = prove_constructors_one_one ax 416 val distincts = prove_constructors_distinct ax 417 val _ = (length nchotomyl = length case_congs andalso 418 length case_congs = length one_ones andalso 419 length one_ones = length distincts) 420 orelse raise ERR "gen_tyinfo" 421 "Number of theorems automatically proved doesn't match up" 422 val cased1 = hd case_defs 423 val casec1 = hd case_congs 424 val nch1 = hd nchotomyl 425 val tyinfo_1 = mk_datatype_info_no_simpls 426 {ax=ORIG ax, induction=ORIG ind, 427 case_def = cased1, case_cong = casec1, nchotomy = nch1, 428 case_eq = 429 prove_case_eq_thm {case_def = cased1, nchotomy = nch1}, 430 size=NONE, encode=NONE, lift=NONE, 431 fields=[], accessors=[],updates=[], 432 one_one=hd one_ones, distinct=hd distincts, 433 recognizers=[],destructors=[]} 434 in 435 if length nchotomyl = 1 then [tyinfo_1] 436 else let val tyname = ty_name_of tyinfo_1 437 in tyinfo_1 :: mk_ti (tyname,ax,ind) 438 (tl case_defs) (tl case_congs) 439 (tl one_ones) (tl distincts) (tl nchotomyl) 440 end 441 end 442end; 443 444fun mk_nondatatype_info (ty,{encode,induction,nchotomy,size}) = 445 NFACTS(ty,{encode=encode,induction=induction,size=size,extra=[], 446 nchotomy=nchotomy,simpls=simpfrag.empty_simpfrag}); 447 448fun name_pair(s1,s2) = s1^"$"^s2; 449 450fun pp_tyinfo tyi = 451 let 452 open Portable smpp 453 val pp_type = lift Parse.pp_type 454 val pp_term = lift Parse.pp_term 455 val pp_thm = lift Parse.pp_thm 456 val pp_sexp = 457 lift (ThyDataSexp.pp_sexp Parse.pp_type Parse.pp_term Parse.pp_thm) 458 in 459 case tyi of 460 d as DFACTS recd => 461 let 462 val {ty,constructors, case_const, case_def, case_cong, induction, 463 nchotomy,one_one,distinct,simpls,size,encode,lift,axiom, case_eq, 464 fields, accessors, updates,recognizers,destructors,extra} = recd 465 val ty_namestring = name_pair (ty_name_of d) 466 in 467 block CONSISTENT 0 ( 468 block INCONSISTENT 0 ( 469 add_string "-----------------------" >> add_newline >> 470 add_string "-----------------------" >> add_newline >> 471 add_string "HOL datatype:" >> add_break(1,0) >> 472 add_string (Lib.quote ty_namestring) 473 ) >> add_break(1,0) >> 474 475 block CONSISTENT 1 ( 476 add_string "Primitive recursion:" >> add_break (1,0) >> 477 (case axiom of 478 ORIG thm => pp_thm thm 479 | COPY(sp,_) => add_string ("see "^Lib.quote (name_pair sp))) 480 ) >> add_break(1,0) >> 481 482 block CONSISTENT 1 ( 483 add_string "Case analysis:" >> add_break (1,0) >> pp_thm case_def 484 ) >> add_break(1,0) >> 485 486 (case size of 487 NONE => nothing 488 | SOME (tm,size_def) => 489 block CONSISTENT 1 ( 490 add_string "Size:" >> add_break (1,0) >> 491 (case size_def of 492 COPY(sp,th) => 493 add_string ("see "^Lib.quote (name_pair sp)) 494 | ORIG th => if is_const tm then pp_thm th 495 else pp_term tm) 496 ) >> add_break(1,0)) >> 497 498 (case encode of 499 NONE => nothing 500 | SOME (tm,encode_def) => 501 (block CONSISTENT 1 ( 502 add_string "Encoder:" >> add_break (1,0) >> 503 (case encode_def of 504 COPY(sp,th) => 505 add_string ("see "^Lib.quote (name_pair sp)) 506 | ORIG th => if is_const tm then pp_thm th 507 else pp_term tm) 508 ) >> add_break(1,0))) >> 509 510 block CONSISTENT 1 ( 511 add_string "Induction:" >> add_break (1,0) >> 512 (case induction of 513 ORIG thm => pp_thm thm 514 | COPY(sp,_) => add_string ("see "^Lib.quote (name_pair sp))) 515 ) >> add_break(1,0) >> 516 517 block CONSISTENT 1 ( 518 add_string "Case completeness:" >> add_break (1,0) >> 519 pp_thm nchotomy 520 ) >> add_break(1,0) >> 521 522 block CONSISTENT 1 ( 523 add_string "Case-const equality split:" >> add_break (1,0) >> 524 pp_thm case_eq 525 ) >> add_break(1,0) >> 526 527 block CONSISTENT 1 ( 528 add_string "Extras: [" >> add_break(1,0) >> 529 pr_list pp_sexp (add_string "," >> add_break(1,0)) extra >> 530 add_string "]" 531 ) >> 532 533 let fun do11 thm = 534 block CONSISTENT 1 (add_string "One-to-one:" >> 535 add_break (1,0) >> pp_thm thm) 536 fun do_distinct thm = 537 block CONSISTENT 1 (add_string "Distinctness:" >> 538 add_break (1,0) >> pp_thm thm) 539 in 540 case (one_one,distinct) 541 of (NONE,NONE) => nothing 542 | (NONE,SOME thm) => add_break(1,0) >> do_distinct thm 543 | (SOME thm,NONE) => add_break(1,0) >> do11 thm 544 | (SOME thm1,SOME thm2) => add_break(1,0) >> do11 thm1 >> 545 add_break(1,0) >> do_distinct thm2 546 end 547 ) 548 end 549 | NFACTS(ty,{nchotomy,induction,size,encode,extra,...}) => 550 block CONSISTENT 0 ( 551 block INCONSISTENT 0 ( 552 add_string "-----------------------" >> add_newline >> 553 add_string "-----------------------" >> add_newline >> 554 add_string "HOL type:" >> add_break(1,0) >> pp_type ty 555 ) >> add_break(1,0) >> 556 557 block CONSISTENT 1 ( 558 add_string "Case completeness:" >> add_break (1,0) >> 559 (case nchotomy of 560 NONE => add_string "none" 561 | SOME thm => pp_thm thm) 562 ) >> add_break(1,0) >> 563 564 block CONSISTENT 1 ( 565 add_string "Induction:" >> add_break (1,0) >> 566 (case induction of 567 NONE => add_string "none" 568 | SOME thm => pp_thm thm) 569 ) >> add_break(1,0) >> 570 571 block CONSISTENT 1 ( 572 add_string "Size:" >> add_break (1,0) >> 573 (case size of 574 NONE => add_string "none" 575 | SOME (tm,size_def) => 576 block CONSISTENT 1 ( 577 if is_const tm then pp_thm size_def else pp_term tm 578 ) 579 ) 580 ) >> add_break(1,0) >> 581 582 block CONSISTENT 1 ( 583 add_string "Extras:" >> add_break(1,0) >> 584 pr_list pp_sexp (add_string "," >> add_break(1,0)) extra 585 ) 586 ) 587 end 588 589val pp_tyinfo = Parse.mlower o pp_tyinfo 590 591(*---------------------------------------------------------------------------*) 592(* Database of facts. *) 593(*---------------------------------------------------------------------------*) 594 595type typeBase = tyinfo TypeNet.typenet 596 597val empty : typeBase = TypeNet.empty 598 599val fold = TypeNet.fold 600 601fun next_ty ty = mk_vartype(Lexis.tyvar_vary (dest_vartype ty)) 602 603(*---------------------------------------------------------------------------*) 604(* Rename type variables in a type so that they occur in alphabetical order, *) 605(* from left-to-right, and start from 'a. Example: *) 606(* *) 607(* normalise_ty ``:('k#'a) list`` = ``:('a#'b) list *) 608(* *) 609(*---------------------------------------------------------------------------*) 610 611fun normalise_ty ty = let 612 fun recurse (acc as (dict,usethis)) tylist = 613 case tylist of 614 [] => acc 615 | ty :: rest => let 616 in 617 if is_vartype ty then 618 case Binarymap.peek(dict,ty) of 619 NONE => recurse (Binarymap.insert(dict,ty,usethis), 620 next_ty usethis) 621 rest 622 | SOME _ => recurse acc rest 623 else let 624 val {Args,...} = dest_thy_type ty 625 in 626 recurse acc (Args @ rest) 627 end 628 end 629 val (inst0, _) = recurse (Binarymap.mkDict Type.compare, Type.alpha) [ty] 630 val inst = Binarymap.foldl (fn (tyk,tyv,acc) => (tyk |-> tyv)::acc) 631 [] 632 inst0 633in 634 Type.type_subst inst ty 635end 636 637fun prim_get (db:typeBase) (thy,tyop) = 638 case Type.op_arity {Thy = thy, Tyop = tyop} of 639 NONE => NONE 640 | SOME i => let 641 fun genargs (acc,nextty) n = if n = 0 then List.rev acc 642 else genargs (nextty :: acc, next_ty nextty) 643 (n - 1) 644 val ty = mk_thy_type {Thy = thy, Tyop = tyop, 645 Args = genargs ([], alpha) i} 646 in 647 TypeNet.peek (db, ty) 648 end 649 650fun insert db x = TypeNet.insert(db,normalise_ty (ty_of x), x); 651 652fun get db s = let 653 fun foldthis (ty,tyi as DFACTS _,acc) = 654 if #2 (type_names ty) = s then tyi::acc else acc 655 | foldthis (ty, _, acc) = acc 656in 657 TypeNet.fold foldthis [] db 658end 659 660fun listItems db = map #2 (TypeNet.listItems db) 661 662fun toPmatchThry tbase {Thy,Tyop} = 663 case prim_get tbase (Thy,Tyop) of 664 NONE => NONE 665 | SOME tyi => SOME {case_const = case_const_of tyi, 666 constructors = constructors_of tyi} 667 668 669 670(*---------------------------------------------------------------------------*) 671(* If ty1 is an instance of ty2, then return the record *) 672(*---------------------------------------------------------------------------*) 673 674fun tysize ty = 675 if Type.is_vartype ty then 1 676 else let 677 val {Args,...} = Type.dest_thy_type ty 678 in 679 1 + List.foldl (fn (ty,acc) => tysize ty + acc) 0 Args 680 end 681 682fun mymatch pat ty = let 683 val (i, sames) = Type.raw_match_type pat ty ([], []) 684in 685 i @ (map (fn ty => ty |-> ty) sames) 686end 687 688fun instsize i = 689 List.foldl (fn ({redex,residue},acc) => tysize residue + acc) 0 i 690 691fun check_match ty (pat, data) = 692 SOME(instsize (mymatch pat ty), data) handle HOL_ERR _ => NONE 693 694fun fetch tbase ty = 695 case TypeNet.match (tbase, ty) of 696 [] => NONE 697 | matches0 => let 698 val matches = List.mapPartial (check_match ty) matches0 699 val sorted = Listsort.sort (measure_cmp fst) matches 700 in 701 case sorted of 702 [] => NONE 703 | (_, tyi) :: _ => SOME tyi 704 end 705 706 707(*--------------------------------------------------------------------------- 708 General facility for interpreting types as terms. It takes a 709 couple of environments (theta,gamma); theta maps type variables 710 to (term) functions on those type variables, and gamma maps 711 type operators to (term) functions on elements of the given type. 712 The interpretation is partial: for types that are not mapped, 713 the supplied function undef is applied. 714 ---------------------------------------------------------------------------*) 715 716(* 717local fun drop [] ty = fst(dom_rng ty) 718 | drop (_::t) ty = drop t (snd(dom_rng ty)) 719in 720fun typeValue (theta,gamma,undef) = 721 let fun tyValue ty = 722 case theta ty 723 of SOME fvar => fvar 724 | NONE => 725 let val {Thy,Tyop,Args} = dest_thy_type ty 726 in case gamma (Thy,Tyop) 727 of SOME f => 728 let val vty = drop Args (type_of f) 729 val sigma = match_type vty ty 730 in list_mk_comb(inst sigma f, map tyValue Args) 731 end 732 | NONE => undef ty 733 end 734 in tyValue 735 end 736end 737*) 738 739fun tystring ty = 740 let val (thy,name) = type_names ty 741 in String.concat [thy,"$",name] 742 end; 743 744(*---------------------------------------------------------------------------*) 745(* gamma models polymorphic functions of the form *) 746(* *) 747(* ty |-> ty_size size1 ... sizen arg = ... *) 748(* *) 749(* where arg is a term with a type having n type variables. In order to *) 750(* synthesize the correct instance of ty_size, we have to match the types *) 751(* of size1...sizen against the concrete types found in the instance of type *) 752(* ty. Hence the complex lead-up to matching. *) 753(*---------------------------------------------------------------------------*) 754 755fun typeValue (theta,gamma,undef) = 756 let fun tyValue ty = 757 case theta ty 758 of SOME fvar => fvar 759 | NONE => 760 case gamma ty 761 of SOME f => 762 (let val args = snd(dest_type ty) 763 val csizefns = map tyValue args 764 val (tys,rng) = strip_fun (type_of f) 765 val (gen_sizefn_tys,vty) = front_last tys 766 val tyinst = match_type (list_mk_fun(gen_sizefn_tys,bool)) 767 (list_mk_fun(map type_of csizefns,bool)) 768 in list_mk_comb(inst tyinst f, csizefns) 769 end handle HOL_ERR _ 770 => (WARN "typeValue" 771 ("Badly typed terms at type constructor " 772 ^Lib.quote (tystring ty)^". Continuing anyway."); 773 undef ty)) 774 | NONE => undef ty 775 in tyValue 776 end 777 778(*---------------------------------------------------------------------------*) 779(* Map a HOL type (ty) into a term having type :ty -> num. *) 780(*---------------------------------------------------------------------------*) 781 782fun num() = mk_thy_type{Tyop="num",Thy="num",Args=[]} 783fun Zero() = mk_thy_const{Name="0",Thy="num", Ty=num()} 784 handle HOL_ERR _ => 785 raise ERR "type_size.Zero()" "Numbers not declared" 786 787fun type_size db ty = 788 let fun K0 ty = mk_abs(mk_var("v",ty),Zero()) 789 fun theta ty = if is_vartype ty then SOME (K0 ty) else NONE 790 val gamma = Option.map fst o 791 Option.composePartial (size_of,fetch db) 792 in 793 typeValue (theta,gamma,K0) ty 794 end 795 796(*--------------------------------------------------------------------------- 797 Encoding: map a HOL type (ty) into a term having type :ty -> bool list 798 ---------------------------------------------------------------------------*) 799 800local 801 fun tyencode_env db = 802 Option.map fst o Option.composePartial (encode_of, fetch db) 803 fun undef _ = raise ERR "type_encode" "unknown type" 804 fun theta ty = 805 if is_vartype ty then raise ERR "type_encode" "type variable" else NONE 806in 807fun type_encode db = typeValue (theta, tyencode_env db, undef) 808end; 809 810(*---------------------------------------------------------------------------*) 811(* Lifters are a bit different, since they are ML-level definitions. *) 812(* *) 813(* Build a HOL term that represents an ML expression that will construct a *) 814(* compound HOL type. *) 815(*---------------------------------------------------------------------------*) 816 817local 818 val string_tyv = mk_vartype "'string" 819 val type_tyv = mk_vartype "'type" 820 val typelist_tyv = mk_vartype "'typelist" 821 val stringXtypelist_tyv = mk_vartype "'string_X_typelist" 822 val mk_type_var = mk_var("mk_type", stringXtypelist_tyv --> type_tyv) 823 val cons_var = mk_var ("cons",type_tyv --> typelist_tyv --> typelist_tyv) 824 val nil_var = mk_var ("nil",typelist_tyv) 825 val comma_var = mk_var (",",string_tyv --> typelist_tyv 826 --> stringXtypelist_tyv) 827 val mk_vartype_var = mk_var("mk_vartype",string_tyv --> type_tyv) 828 fun Cons x y = list_mk_comb(cons_var,[x,y]) 829 fun to_list alist = itlist Cons alist nil_var 830 fun tyop_var tyop = mk_var(Lib.quote tyop,string_tyv) 831 fun Pair x y = list_mk_comb(comma_var,[x,y]) 832 val bool_var = mk_var("bool",type_tyv) 833in 834fun enc_type ty = 835 if is_vartype ty 836 then mk_comb(mk_vartype_var, 837 mk_var(Lib.quote (dest_vartype ty),string_tyv)) 838 else 839 if ty = Type.bool then bool_var 840 else 841 let val (tyop,args) = dest_type ty 842 val enc_args = to_list(map enc_type args) 843 val enc_tyop = tyop_var tyop 844 val pair = Pair enc_tyop enc_args 845 in 846 mk_comb(mk_type_var,pair) 847 end 848end; 849 850(*---------------------------------------------------------------------------*) 851(* Implements the interpretation of a type, which yields a function to be *) 852(* applied to a term. (Except that in this case, it is applied to an ML *) 853(* value.) *) 854(* *) 855(* [| v |] = Theta(v), where v is a type variable *) 856(* [| ty |] = Gamma(c) ty [| t1 |] ... [| tn |], where ty is (t1,...,tn)c *) 857(* *) 858(*---------------------------------------------------------------------------*) 859 860local fun drop [] ty = fst(dom_rng ty) 861 | drop (_::t) ty = drop t (snd(dom_rng ty)) 862in 863fun tyValue (theta,gamma,undef) = 864 let fun tyVal ty = 865 case theta ty (* map type variable *) 866 of SOME x => x 867 | NONE => (* map compound type *) 868 let val {Thy,Tyop,Args} = dest_thy_type ty 869 in case gamma ty 870 of SOME f => 871 let val vty = drop (alpha::Args) (type_of f) 872 val sigma = match_type vty ty 873 in list_mk_comb(inst sigma f, 874 enc_type ty::map tyVal Args) 875 end 876 | NONE => undef ty 877 end 878 in tyVal 879 end 880end 881 882fun Undef ty = 883 raise ERR "Undef" 884 (Lib.quote (Parse.type_to_string ty)^" is an unknown type"); 885 886(*---------------------------------------------------------------------------*) 887(* Used to synthesize lifters *) 888(*---------------------------------------------------------------------------*) 889 890local fun mk_K_1(tm,ty) = 891 let val ty1 = type_of tm 892 val K = mk_thy_const{Name="K",Thy="combin", 893 Ty = ty1 --> ty --> ty1} 894 in mk_comb(K,tm) 895 end 896in 897fun type_lift db ty = 898 let val TYV = type_vars ty 899 val tyv_fns = map (fn tyv => mk_K_1(boolSyntax.mk_arb tyv, tyv)) TYV 900 val Theta = C assoc (zip TYV tyv_fns) 901 val Gamma = Option.composePartial (lift_of, fetch db) 902 in 903 tyValue (total Theta, Gamma, Undef) ty 904 end 905end; 906 907(*---------------------------------------------------------------------------*) 908(* Instantiate a constructor to a type. Used in lifting (see *) 909(* datatype/Lift.sml *) 910(*---------------------------------------------------------------------------*) 911 912fun cinst ty c = 913 let val cty = snd(strip_fun(type_of c)) 914 val theta = match_type cty ty 915 in inst theta c 916 end 917 918(*---------------------------------------------------------------------------*) 919(* Is a constant a constructor for some datatype. *) 920(*---------------------------------------------------------------------------*) 921 922fun is_constructor tybase c = 923 let val (_,ty) = strip_fun (type_of c) 924 in case prim_get tybase (type_names ty) 925 of NONE => false 926 | SOME tyinfo => op_mem same_const c (constructors_of tyinfo) 927 end handle HOL_ERR _ => false; 928 929fun is_constructor_pat tybase tm = 930 is_constructor tybase (fst (strip_comb tm)) 931 932fun is_constructor_var_pat tybase tm = 933 is_var tm orelse is_constructor_pat tybase tm 934 935(* ---------------------------------------------------------------------- 936 Syntax operations on the (extensible) set of case expressions. 937 938 All implemented in Pmatch 939 ---------------------------------------------------------------------- *) 940 941fun dest_case tbase = Pmatch.dest_case (toPmatchThry tbase) 942fun is_case tbase = Pmatch.is_case (toPmatchThry tbase) 943fun strip_case tbase = Pmatch.strip_case (toPmatchThry tbase) 944fun mk_case tbase = Pmatch.mk_case (toPmatchThry tbase) 945 946(*---------------------------------------------------------------------------*) 947(* Syntax operations for record types. *) 948(*---------------------------------------------------------------------------*) 949 950fun dest_record_type tybase ty = 951 case Lib.total (fields_of o valOf o prim_get tybase o type_names) ty 952 of SOME (fields as (_::_)) => fields 953 | otherwise => raise ERR "dest_record_type" "not a record type"; 954 955fun is_record_type tybase ty = Lib.can (dest_record_type tybase) ty; 956 957fun has_record_type tybase M = is_record_type tybase (type_of M); 958 959(*---------------------------------------------------------------------------*) 960(* The function *) 961(* *) 962(* dest_record : tyBase -> term -> (string * hol_type) list *) 963(* *) 964(* needs to know about the TypeBase in order to tell if the term is an *) 965(* element of a record type. *) 966(*---------------------------------------------------------------------------*) 967 968fun mk_K_1 (tm,ty) = 969 let val K_tm = prim_mk_const{Name="K",Thy="combin"} 970 in mk_comb(inst [alpha |-> type_of tm, beta |-> ty] K_tm,tm) 971 end; 972fun dest_K_1 tm = 973 let val K_tm = prim_mk_const{Name="K",Thy="combin"} 974 in dest_monop K_tm (ERR "dest_K_1" "not a K-term") tm 975 end; 976 977fun get_field_name s1 s2 = 978 let val prefix = String.extract(s2,0,SOME(String.size s1)) 979 val rest = String.extract(s2,String.size s1 + 1, NONE) 980 val middle = String.extract(rest,0,SOME(String.size rest - 5)) 981 val suffix = String.extract(rest,String.size middle, NONE) 982 in 983 if prefix = s1 andalso suffix = "_fupd" 984 then middle 985 else raise ERR "get_field" ("unable to parse "^Lib.quote s2) 986 end; 987 988(*---------------------------------------------------------------------------*) 989(* A record looks like `fupd arg_1 (fupd arg_2 ... (fupd arg_n ARB) ...)` *) 990(* where each arg_i is a (name,type) pair showing how the ith field should *) 991(* be declared. *) 992(*---------------------------------------------------------------------------*) 993 994fun dest_field tm = 995 let val (ty,_) = dom_rng (type_of tm) 996 val tyname = fst(dest_type ty) 997 val (updf,arg) = dest_comb tm 998 val (name0,ty) = dest_const updf 999 val name = get_field_name tyname name0 1000 in 1001 (name,dest_K_1 arg) 1002 end 1003 handle HOL_ERR _ => raise ERR "dest_field" "unexpected term structure"; 1004 1005 1006fun dest_record tybase tm = 1007 let fun dest tm = 1008 if is_arb tm then [] 1009 else let val (f,a) = dest_comb tm 1010 in dest_field f::dest a 1011 end 1012 handle HOL_ERR _ => raise ERR "dest_record" "unexpected term structure" 1013 in 1014 if has_record_type tybase tm 1015 then (type_of tm, dest tm) 1016 else raise ERR "dest_record" "not a record" 1017 end; 1018 1019fun is_record tybase = can (dest_record tybase); 1020 1021fun mk_record tybase (ty,fields) = 1022 if is_record_type tybase ty 1023 then let val (Thy,Tyop) = type_names ty 1024 val fupds = map (fn p => String.concat[Tyop,"_",fst p,"_fupd"]) fields 1025 val updfns = map (fn n => prim_mk_const{Name=n,Thy=Thy}) fupds 1026 fun ifn c = let val (_,ty') = dom_rng (type_of c) 1027 val theta = match_type ty' (ty --> ty) 1028 in inst theta c 1029 end 1030 val updfns' = map ifn updfns 1031 fun mk_field (updfn,v) tm = 1032 mk_comb(mk_comb(updfn, mk_K_1(v,type_of v)),tm) 1033 in 1034 itlist mk_field (zip updfns' (map snd fields)) (mk_arb ty) 1035 end 1036 else raise ERR "mk_record" "first arg. not a record type"; 1037 1038exception OptionExn = Option 1039open ThyDataSexp 1040fun ty_to_key ty = 1041 let 1042 val {Thy,Tyop,...} = dest_thy_type ty 1043 in 1044 List [String Thy, String Tyop] 1045 end 1046 1047fun field s v = [Sym s, v] 1048fun option f v = 1049 case v of 1050 NONE => Sym "NONE" 1051 | SOME v0 => List [Sym "SOME", f v0] 1052fun rcdfinfo_to_sexp {ty,accessor,fupd} = 1053 List [Type ty, Term accessor, Term fupd] 1054 1055fun dtyiToSEXPs (dtyi : dtyinfo) = 1056 field "ty" (Type (#ty dtyi)) @ 1057 field "axiom" (Thm (thm_of (#axiom dtyi))) @ 1058 field "induction" (Thm (thm_of (#induction dtyi))) @ 1059 field "case_def" (Thm (#case_def dtyi)) @ 1060 field "case_eq" (Thm (#case_eq dtyi)) @ 1061 field "case_cong" (Thm (#case_cong dtyi)) @ 1062 field "case_const" (Term (#case_const dtyi)) @ 1063 field "constructors" (List (map Term (#constructors dtyi))) @ 1064 field "destructors" (List (map Thm (#destructors dtyi))) @ 1065 field "recognizers" (List (map Thm (#recognizers dtyi))) @ 1066 field "size" (option (fn (t,th) => List [Term t, Thm (thm_of th)]) 1067 (#size dtyi)) @ 1068 field "encode" (option (fn (t,th) => List [Term t, Thm (thm_of th)]) 1069 (#encode dtyi)) @ 1070 field "lift" (option Term (#lift dtyi)) @ 1071 field "distinct" (option Thm (#distinct dtyi)) @ 1072 field "nchotomy" (Thm (#nchotomy dtyi)) @ 1073 field "one_one" (option Thm (#one_one dtyi)) @ 1074 field "fields" 1075 (List (map (fn (s,rfi) => List[String s, rcdfinfo_to_sexp rfi]) 1076 (#fields dtyi))) @ 1077 field "accessors" (List (map Thm (#accessors dtyi))) @ 1078 field "updates" (List (map Thm (#updates dtyi))) @ 1079 field "simpls" (List (map Thm (#rewrs (#simpls dtyi)))) @ 1080 field "extra" (List (#extra dtyi)) 1081 1082fun toSEXP0 tyi = 1083 case tyi of 1084 DFACTS dtyi => List (Sym "DFACTS" :: dtyiToSEXPs dtyi) 1085 | NFACTS (ty,{nchotomy, induction, size, encode, extra, simpls}) => 1086 List ( 1087 Sym "NFACTS" :: 1088 field "ty" (Type ty) @ 1089 field "nchotomy" (option Thm nchotomy) @ 1090 field "induction" (option Thm induction) @ 1091 field "extra" (List extra) @ 1092 field "size" (option (fn (t,th) => List [Term t, Thm th]) size) @ 1093 field "encode" (option (fn (t,th) => List [Term t, Thm th]) encode) @ 1094 field "simpls" (List (map Thm (#rewrs simpls))) 1095 ) 1096 1097fun toSEXP tyi = 1098 List [ty_to_key (ty_of tyi), toSEXP0 tyi] 1099 1100fun fromSEXP0 s = 1101 let 1102 fun string (String s) = s | string _ = raise OptionExn 1103 fun ty (Type t) = t | ty _ = raise OptionExn 1104 fun tm (Term t) = t | tm _ = raise OptionExn 1105 fun thm (Thm th) = th | thm _ = raise OptionExn 1106 fun sthm (Thm th) = ORIG th | sthm _ = raise OptionExn 1107 fun dest_option df (Sym "NONE") = NONE 1108 | dest_option df (List [Sym "SOME", v]) = SOME (df v) 1109 | dest_option _ _ = raise OptionExn 1110 fun dest_pair df1 df2 (List [s1, s2]) = (df1 s1, df2 s2) 1111 | dest_pair _ _ _ = raise OptionExn 1112 fun dest_rfi (List [typ, acc, fupd]) = {ty = ty typ, accessor = tm acc, 1113 fupd = tm fupd} 1114 | dest_rfi _ = raise OptionExn 1115 1116 fun H nm f x = f x 1117 handle OptionExn => raise ERR "fromSEXP" ("Bad encoding for field "^nm) 1118 in 1119 case s of 1120 List [Sym "DFACTS", 1121 Sym "ty", Type typ, 1122 Sym "axiom", Thm axiom, 1123 Sym "induction", Thm induction, 1124 Sym "case_def", Thm case_def, 1125 Sym "case_eq", Thm case_eq, 1126 Sym "case_cong", Thm case_cong, 1127 Sym "case_const", Term case_const, 1128 Sym "constructors", List clist, 1129 Sym "destructors", List dlist, 1130 Sym "recognizers", List rlist, 1131 Sym "size", size_option, 1132 Sym "encode", encode_option, 1133 Sym "lift", lift_option, 1134 Sym "distinct", distinct_option, 1135 Sym "nchotomy", Thm nchotomy, 1136 Sym "one_one", one_one_option, 1137 Sym "fields", List field_list, 1138 Sym "accessors", List accessor_list, 1139 Sym "updates", List update_list, 1140 Sym "simpls", List fragrewr_list, 1141 Sym "extra", List extra] => 1142 (SOME ( 1143 DFACTS {ty = typ, axiom = ORIG axiom, induction = ORIG induction, 1144 case_def = case_def, case_eq = case_eq, 1145 case_cong = case_cong, 1146 case_const = case_const, 1147 constructors = H "constructors" (map tm) clist, 1148 destructors = H "destructors" (map thm) dlist, 1149 recognizers = H "recognizers" (map thm) rlist, 1150 size = 1151 H "size" (dest_option (dest_pair tm sthm)) size_option, 1152 encode = H "encode" 1153 (dest_option (dest_pair tm sthm)) encode_option, 1154 lift = H "lift" (dest_option tm) lift_option, 1155 distinct = H "distinct" (dest_option thm) distinct_option, 1156 nchotomy = nchotomy, 1157 one_one = H "one_one" (dest_option thm) one_one_option, 1158 fields = H "fields" 1159 (map (dest_pair string dest_rfi)) field_list, 1160 accessors = H "accessors" (map thm) accessor_list, 1161 updates = H "updates" (map thm) update_list, 1162 simpls = simpfrag.add_rwts simpfrag.empty_simpfrag 1163 (H "simpls" (map thm) fragrewr_list), 1164 extra = extra} 1165 ) handle OptionExn => NONE) 1166 | List [Sym "NFACTS", Sym "ty", Type typ, 1167 Sym "nchotomy", nch_option, 1168 Sym "induction", ind_option, 1169 Sym "extra", List extra, 1170 Sym "size", size_option, 1171 Sym "encode", encode_option, 1172 Sym "simpls", List rewrs] => 1173 (SOME ( 1174 NFACTS (typ, { 1175 nchotomy = H "nchotomy" (dest_option thm) nch_option, 1176 induction = H "induction" (dest_option thm) ind_option, 1177 extra = extra, 1178 size = H "size" (dest_option (dest_pair tm thm)) 1179 size_option, 1180 encode = H "encode" (dest_option (dest_pair tm thm)) 1181 encode_option, 1182 simpls = simpfrag.add_rwts simpfrag.empty_simpfrag 1183 (H "simpls" (map thm) rewrs)})) 1184 handle OptionExn => NONE) 1185 | _ => NONE 1186 end 1187 1188fun fromSEXP s = 1189 case s of 1190 List[_, s0] => fromSEXP0 s0 1191 | _ => NONE 1192 1193end (* struct *) 1194