Skip to content

Commit 8fa3716

Browse files
ordinarymathordinarymath
committed
Get TypeBasePure working
1 parent e1bbdb7 commit 8fa3716

File tree

2 files changed

+119
-96
lines changed

2 files changed

+119
-96
lines changed

‎src/1/TypeBasePure.sig‎

Lines changed: 19 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -16,23 +16,24 @@ sig
1616
datatype shared_thm = ORIG of thm
1717
| COPY of (string * string) * thm
1818
type mk_datatype_record =
19-
{ax : shared_thm,
20-
induction : shared_thm,
21-
case_def : thm,
22-
case_cong : thm,
23-
case_eq : thm,
24-
case_elim : thm,
25-
nchotomy : thm,
26-
size : (term * shared_thm) option,
27-
encode : (term * shared_thm) option,
28-
lift : term option,
29-
one_one : thm option,
30-
distinct : thm option,
31-
fields : (string * rcd_fieldinfo) list,
32-
accessors : thm list,
33-
updates : thm list,
34-
destructors : thm list,
35-
recognizers : thm list}
19+
{ax : shared_thm,
20+
induction : shared_thm,
21+
case_def : thm,
22+
case_cong : thm,
23+
case_eq : thm,
24+
case_elim : thm,
25+
constant_case : thm,
26+
nchotomy : thm,
27+
size : (term * shared_thm) option,
28+
encode : (term * shared_thm) option,
29+
lift : term option,
30+
one_one : thm option,
31+
distinct : thm option,
32+
fields : (string * rcd_fieldinfo) list,
33+
accessors : thm list,
34+
updates : thm list,
35+
destructors : thm list,
36+
recognizers : thm list}
3637

3738
val mk_datatype_info_no_simpls : mk_datatype_record -> tyinfo
3839
val gen_std_rewrs : tyinfo -> thm list
@@ -63,6 +64,7 @@ sig
6364
val case_def_of : tyinfo -> thm
6465
val case_eq_of : tyinfo -> thm
6566
val case_elim_of : tyinfo -> thm
67+
val constant_case_of : tyinfo -> thm
6668
val nchotomy_of : tyinfo -> thm
6769
val distinct_of : tyinfo -> thm option
6870
val one_one_of : tyinfo -> thm option

‎src/1/TypeBasePure.sml‎

Lines changed: 100 additions & 79 deletions
Original file line numberDiff line numberDiff line change
@@ -27,23 +27,24 @@ datatype shared_thm
2727
| COPY of (string * string) * thm;
2828

2929
type mk_datatype_record =
30-
{ax : shared_thm,
31-
induction : shared_thm,
32-
case_def : thm,
33-
case_cong : thm,
34-
case_eq : thm,
35-
case_elim : thm,
36-
nchotomy : thm,
37-
size : (term * shared_thm) option,
38-
encode : (term * shared_thm) option,
39-
lift : term option,
40-
one_one : thm option,
41-
distinct : thm option,
42-
fields : (string * rcd_fieldinfo) list,
43-
accessors : thm list,
44-
updates : thm list,
45-
destructors : thm list,
46-
recognizers : thm list}
30+
{ax : shared_thm,
31+
induction : shared_thm,
32+
case_def : thm,
33+
case_cong : thm,
34+
case_eq : thm,
35+
case_elim : thm,
36+
constant_case : thm,
37+
nchotomy : thm,
38+
size : (term * shared_thm) option,
39+
encode : (term * shared_thm) option,
40+
lift : term option,
41+
one_one : thm option,
42+
distinct : thm option,
43+
fields : (string * rcd_fieldinfo) list,
44+
accessors : thm list,
45+
updates : thm list,
46+
destructors : thm list,
47+
recognizers : thm list}
4748

4849
fun thm_of (ORIG x) = x
4950
| thm_of (COPY (s,x)) = x;
@@ -53,59 +54,61 @@ fun thm_of (ORIG x) = x
5354
(*---------------------------------------------------------------------------*)
5455

5556
type dtyinfo =
56-
{ty : hol_type,
57-
axiom : shared_thm,
58-
induction : shared_thm,
59-
case_def : thm,
60-
case_eq : thm,
61-
case_elim : thm,
62-
case_cong : thm,
63-
nchotomy : thm,
64-
case_const : term,
65-
constructors : term list,
66-
destructors : thm list,
67-
recognizers : thm list,
68-
size : (term * shared_thm) option,
69-
encode : (term * shared_thm) option,
70-
lift : term option,
71-
distinct : thm option,
72-
one_one : thm option,
73-
fields : (string * rcd_fieldinfo) list,
74-
accessors : thm list,
75-
updates : thm list,
76-
simpls : simpfrag,
77-
extra : ThyDataSexp.t list} ;
57+
{ty : hol_type,
58+
axiom : shared_thm,
59+
induction : shared_thm,
60+
case_def : thm,
61+
case_eq : thm,
62+
case_elim : thm,
63+
constant_case : thm,
64+
case_cong : thm,
65+
nchotomy : thm,
66+
case_const : term,
67+
constructors : term list,
68+
destructors : thm list,
69+
recognizers : thm list,
70+
size : (term * shared_thm) option,
71+
encode : (term * shared_thm) option,
72+
lift : term option,
73+
distinct : thm option,
74+
one_one : thm option,
75+
fields : (string * rcd_fieldinfo) list,
76+
accessors : thm list,
77+
updates : thm list,
78+
simpls : simpfrag,
79+
extra : ThyDataSexp.t list} ;
7880

7981
open FunctionalRecordUpdate
80-
fun gcons_mkUp z = makeUpdate22 z
82+
fun gcons_mkUp z = makeUpdate23 z
8183
fun update_DTY z = let
8284
fun from accessors axiom case_cong case_const case_def case_eq case_elim
83-
constructors destructors distinct encode extra fields induction lift
84-
nchotomy one_one recognizers simpls size ty updates =
85+
constant_case constructors destructors distinct encode extra fields
86+
induction lift nchotomy one_one recognizers simpls size ty updates =
8587
{accessors = accessors, axiom = axiom, case_cong = case_cong,
8688
case_const = case_const, case_def = case_def, case_eq = case_eq,
87-
case_elim = case_elim, constructors = constructors,
89+
case_elim = case_elim, constant_case = constant_case, constructors = constructors,
8890
destructors = destructors, distinct = distinct, encode = encode,
8991
extra = extra, fields = fields, induction = induction, lift = lift,
9092
nchotomy = nchotomy, one_one = one_one, recognizers = recognizers,
9193
simpls = simpls, size = size, ty = ty, updates = updates}
9294
(* fields in reverse order to above *)
9395
fun from' updates ty size simpls recognizers one_one nchotomy lift induction
94-
fields extra encode distinct destructors constructors case_elim
95-
case_eq case_def case_const case_cong axiom accessors =
96+
fields extra encode distinct destructors constructors constant_case
97+
case_elim case_eq case_def case_const case_cong axiom accessors =
9698
{accessors = accessors, axiom = axiom, case_cong = case_cong,
9799
case_const = case_const, case_def = case_def, case_eq = case_eq,
98-
case_elim = case_elim, constructors = constructors, destructors = destructors,
100+
case_elim = case_elim, constant_case = constant_case,
101+
constructors = constructors, destructors = destructors,
99102
distinct = distinct, encode = encode, extra = extra, fields = fields,
100103
induction = induction, lift = lift, nchotomy = nchotomy,
101104
one_one = one_one, recognizers = recognizers, simpls = simpls,
102105
size = size, ty = ty, updates = updates}
103106
(* first order *)
104107
fun to f {accessors, axiom, case_cong, case_const, case_def, case_eq,
105-
case_elim, constructors, destructors, distinct, encode, extra, fields,
106-
induction, lift, nchotomy, one_one, recognizers, simpls, size, ty,
107-
updates} =
108-
f accessors axiom case_cong case_const case_def case_eq case_elim
108+
case_elim, constant_case, constructors, destructors, distinct,
109+
encode, extra, fields, induction, lift, nchotomy, one_one,
110+
recognizers, simpls, size, ty, updates} =
111+
f accessors axiom case_cong case_const case_def case_eq case_elim constant_case
109112
constructors destructors distinct encode extra fields induction lift
110113
nchotomy one_one recognizers simpls size ty updates
111114
in
@@ -186,6 +189,10 @@ fun case_elim_of (DFACTS {case_elim, ...}) = case_elim
186189
| case_elim_of (NFACTS (ty,_)) =
187190
raise ERR "case_elim_of" (dollarty ty^" is not a datatype");
188191

192+
fun constant_case_of (DFACTS {constant_case, ...}) = constant_case
193+
| constant_case_of (NFACTS (ty,_)) =
194+
raise ERR "constant_case_of" (dollarty ty^" is not a datatype");
195+
189196
fun extra_of (DFACTS{extra,...}) = extra
190197
| extra_of (NFACTS(_, {extra,...})) = extra
191198

@@ -363,42 +370,44 @@ val defn_const =
363370

364371
fun mk_datatype_info_no_simpls rcd =
365372
let
366-
val {ax,case_def,case_eq,case_elim,case_cong,induction,
367-
nchotomy,size,encode,lift,one_one,
368-
fields, accessors, updates, distinct,
373+
val {ax,case_def,case_eq,case_elim,constant_case,
374+
case_cong,induction,nchotomy,size,encode,lift,
375+
one_one, fields, accessors, updates, distinct,
369376
destructors,recognizers} = rcd
370377
val (ty,ty_names,constructors) = basic_info case_def
371378
in
372379
DFACTS
373-
{ty = ty,
374-
constructors = constructors,
375-
destructors = destructors,
376-
recognizers = recognizers,
377-
case_const = defn_const case_def,
378-
case_def = case_def,
379-
case_eq = case_eq,
380-
case_elim = case_elim,
381-
case_cong = case_cong,
382-
induction = induction,
383-
nchotomy = nchotomy,
384-
one_one = one_one,
385-
distinct = distinct,
386-
fields = fields,
387-
accessors = accessors,
388-
updates = updates,
389-
simpls = {rewrs = [], convs = []},
390-
size = size,
391-
encode = encode,
392-
lift = lift,
393-
axiom = ax,
394-
extra = []}
380+
{ty = ty,
381+
constructors = constructors,
382+
destructors = destructors,
383+
recognizers = recognizers,
384+
case_const = defn_const case_def,
385+
case_def = case_def,
386+
case_eq = case_eq,
387+
case_elim = case_elim,
388+
constant_case = constant_case,
389+
case_cong = case_cong,
390+
induction = induction,
391+
nchotomy = nchotomy,
392+
one_one = one_one,
393+
distinct = distinct,
394+
fields = fields,
395+
accessors = accessors,
396+
updates = updates,
397+
simpls = {rewrs = [], convs = []},
398+
size = size,
399+
encode = encode,
400+
lift = lift,
401+
axiom = ax,
402+
extra = []}
395403
end
396404

397405
fun gen_std_rewrs tyi =
398406
let
399407
val D = case distinct_of tyi of NONE => [] | SOME x => CONJUNCTS x
400408
val inj = case one_one_of tyi of NONE => [] | SOME th => [th]
401-
val c = D @ map GSYM D @ inj
409+
val const_case = [constant_case_of tyi] handle HOL_ERR _ => []
410+
val c = D @ map GSYM D @ inj @ const_case
402411
in
403412
case_def_of tyi :: c handle HOL_ERR _ => c
404413
end
@@ -415,6 +424,8 @@ local fun mk_ti (n,ax,ind)
415424
prove_case_eq_thm {case_def = cdef, nchotomy = nch},
416425
case_elim =
417426
prove_case_ho_elim_thm {case_def = cdef, nchotomy = nch},
427+
constant_case =
428+
prove_case_const_thm {case_def = cdef, nchotomy = nch},
418429
one_one=oo, distinct=d,size=NONE, encode=NONE,
419430
lift=NONE, fields=[], accessors=[],updates=[],
420431
recognizers=[],destructors=[]}
@@ -443,6 +454,8 @@ fun gen_datatype_info {ax, ind, case_defs} =
443454
prove_case_eq_thm {case_def = cased1, nchotomy = nch1},
444455
case_elim =
445456
prove_case_ho_elim_thm {case_def = cased1, nchotomy = nch1},
457+
constant_case =
458+
prove_case_const_thm {case_def = cased1, nchotomy = nch1},
446459
size=NONE, encode=NONE, lift=NONE,
447460
fields=[], accessors=[],updates=[],
448461
one_one=hd one_ones, distinct=hd distincts,
@@ -477,7 +490,8 @@ fun pp_tyinfo tyi =
477490
let
478491
val {ty,constructors, case_const, case_def, case_cong, induction,
479492
nchotomy,one_one,distinct,simpls,size,encode,lift,axiom, case_eq,
480-
case_elim, fields, accessors, updates,recognizers,destructors,extra}
493+
case_elim,constant_case,fields, accessors, updates,recognizers,
494+
destructors,extra}
481495
= recd
482496
val ty_namestring = name_pair (ty_name_of d)
483497
in
@@ -546,6 +560,11 @@ fun pp_tyinfo tyi =
546560
pp_thm case_elim
547561
) >> add_break(1,0) >>
548562

563+
block CONSISTENT 1 (
564+
add_string "Case-const constant case:" >> add_break (1,0) >>
565+
pp_thm constant_case
566+
) >> add_break(1,0) >>
567+
549568
block CONSISTENT 1 (
550569
add_string "Extras: [" >> add_break(1,0) >>
551570
pr_list pp_sexp (add_string "," >> add_break(1,0)) extra >>
@@ -1089,6 +1108,7 @@ fun dtyiToSEXPs (dtyi : dtyinfo) =
10891108
field "case_def" (Thm (#case_def dtyi)) @
10901109
field "case_eq" (Thm (#case_eq dtyi)) @
10911110
field "case_elim" (Thm (#case_elim dtyi)) @
1111+
field "constant_case" (Thm (#constant_case dtyi)) @
10921112
field "case_cong" (Thm (#case_cong dtyi)) @
10931113
field "case_const" (Term (#case_const dtyi)) @
10941114
field "constructors" (List (map Term (#constructors dtyi))) @
@@ -1155,6 +1175,7 @@ fun fromSEXP0 s =
11551175
Sym "case_def", Thm case_def,
11561176
Sym "case_eq", Thm case_eq,
11571177
Sym "case_elim", Thm case_elim,
1178+
Sym "constant_case", Thm constant_case,
11581179
Sym "case_cong", Thm case_cong,
11591180
Sym "case_const", Term case_const,
11601181
Sym "constructors", List clist,
@@ -1174,8 +1195,8 @@ fun fromSEXP0 s =
11741195
(SOME (
11751196
DFACTS {ty = typ, axiom = ORIG axiom, induction = ORIG induction,
11761197
case_def = case_def, case_eq = case_eq,
1177-
case_elim = case_elim, case_cong = case_cong,
1178-
case_const = case_const,
1198+
case_elim = case_elim, constant_case = constant_case,
1199+
case_cong = case_cong, case_const = case_const,
11791200
constructors = H "constructors" (map tm) clist,
11801201
destructors = H "destructors" (map thm) dlist,
11811202
recognizers = H "recognizers" (map thm) rlist,

0 commit comments

Comments
 (0)