160
|
1 |
(* Title: HOL/thy_syntax.ML
|
|
2 |
ID: $Id$
|
172
|
3 |
Author: Markus Wenzel and Lawrence C Paulson and Carsten Clasohm
|
160
|
4 |
|
|
5 |
Additional theory file sections for HOL.
|
|
6 |
|
|
7 |
TODO:
|
172
|
8 |
move datatype / primrec stuff to pre_datatype.ML (?)
|
160
|
9 |
*)
|
|
10 |
|
172
|
11 |
(*the kind of distinctiveness axioms depends on number of constructors*)
|
|
12 |
val dtK = 5; (* FIXME remove from datatype.ML, rename *)
|
|
13 |
|
160
|
14 |
structure ThySynData: THY_SYN_DATA =
|
|
15 |
struct
|
|
16 |
|
|
17 |
open ThyParse;
|
|
18 |
|
|
19 |
|
172
|
20 |
(** subtype **)
|
160
|
21 |
|
|
22 |
fun mk_subtype_decl (((((opt_name, vs), t), mx), rhs), wt) =
|
|
23 |
let
|
|
24 |
val name' = if_none opt_name t;
|
|
25 |
val name = strip_quotes name';
|
|
26 |
in
|
|
27 |
(cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt],
|
172
|
28 |
[name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse",
|
|
29 |
"Abs_" ^ name ^ "_inverse"])
|
160
|
30 |
end;
|
|
31 |
|
|
32 |
val subtype_decl =
|
|
33 |
optional ("(" $$-- name --$$ ")" >> Some) None --
|
|
34 |
type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness
|
|
35 |
>> mk_subtype_decl;
|
|
36 |
|
|
37 |
|
172
|
38 |
|
|
39 |
(** (co)inductive **)
|
160
|
40 |
|
|
41 |
(*co is either "" or "Co"*)
|
|
42 |
fun inductive_decl co =
|
|
43 |
let
|
172
|
44 |
fun mk_intr_name (s, _) = (*the "op" cancels any infix status*)
|
|
45 |
if Syntax.is_identifier s then "op " ^ s else "_";
|
|
46 |
fun mk_params (((recs, ipairs), monos), con_defs) =
|
|
47 |
let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs)
|
|
48 |
and srec_tms = mk_list recs
|
|
49 |
and sintrs = mk_big_list (map snd ipairs)
|
|
50 |
val stri_name = big_rec_name ^ "_Intrnl"
|
|
51 |
in
|
|
52 |
(";\n\n\
|
|
53 |
\structure " ^ stri_name ^ " =\n\
|
|
54 |
\ let open Ind_Syntax in\n\
|
|
55 |
\ struct\n\
|
|
56 |
\ val _ = writeln \"" ^ co ^
|
|
57 |
"Inductive definition " ^ big_rec_name ^ "\"\n\
|
|
58 |
\ val rec_tms\t= map (readtm (sign_of thy) termTVar) "
|
|
59 |
^ srec_tms ^ "\n\
|
|
60 |
\ and intr_tms\t= map (readtm (sign_of thy) propT)\n"
|
|
61 |
^ sintrs ^ "\n\
|
|
62 |
\ end\n\
|
|
63 |
\ end;\n\n\
|
|
64 |
\val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n (" ^
|
|
65 |
stri_name ^ ".rec_tms, " ^
|
|
66 |
stri_name ^ ".intr_tms)"
|
|
67 |
,
|
|
68 |
"structure " ^ big_rec_name ^ " =\n\
|
|
69 |
\ struct\n\
|
|
70 |
\ structure Result = " ^ co ^ "Ind_section_Fun\n\
|
|
71 |
\ (open " ^ stri_name ^ "\n\
|
|
72 |
\ val thy\t\t= thy\n\
|
|
73 |
\ val monos\t\t= " ^ monos ^ "\n\
|
|
74 |
\ val con_defs\t\t= " ^ con_defs ^ ");\n\n\
|
|
75 |
\ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
|
|
76 |
\ open Result\n\
|
|
77 |
\ end\n"
|
|
78 |
)
|
|
79 |
end
|
|
80 |
val ipairs = "intrs" $$-- repeat1 (ident -- !! string)
|
|
81 |
fun optstring s = optional (s $$-- string) "\"[]\"" >> trim
|
|
82 |
in
|
|
83 |
repeat1 string -- ipairs -- optstring "monos" -- optstring "con_defs"
|
|
84 |
>> mk_params
|
160
|
85 |
end;
|
|
86 |
|
|
87 |
|
172
|
88 |
|
|
89 |
(** datatype **)
|
|
90 |
|
|
91 |
local
|
|
92 |
(* FIXME err -> add_datatype *)
|
|
93 |
fun mk_cons cs =
|
|
94 |
(case duplicates (map (fst o fst) cs) of
|
|
95 |
[] => map (fn ((s, ts), syn) => mk_triple (s, mk_list ts, syn)) cs
|
|
96 |
| dups => error ("Duplicate constructors: " ^ commas_quote dups));
|
|
97 |
|
|
98 |
(*generate names of distinctiveness axioms*)
|
|
99 |
fun mk_distinct_rules cs tname =
|
|
100 |
let
|
|
101 |
val uqcs = map (fn ((s, _), _) => strip_quotes s) cs;
|
|
102 |
(*combine all constructor names with all others w/o duplicates*)
|
|
103 |
fun neg_one c = map (fn c2 => quote (c ^ "_not_" ^ c2));
|
|
104 |
fun neg1 [] = []
|
|
105 |
| neg1 (c1 :: cs) = neg_one c1 cs @ neg1 cs;
|
|
106 |
in
|
|
107 |
if length uqcs < dtK then neg1 uqcs
|
|
108 |
else quote (tname ^ "_ord_distinct") ::
|
|
109 |
map (fn c => quote (tname ^ "_ord_" ^ c)) uqcs
|
|
110 |
end;
|
|
111 |
|
|
112 |
fun mk_rules tname cons pre = " map (get_axiom thy) " ^
|
|
113 |
mk_list (map (fn ((s, _), _) => quote (tname ^ pre ^ strip_quotes s)) cons);
|
160
|
114 |
|
172
|
115 |
(*generate string for calling add_datatype*)
|
|
116 |
fun mk_params ((ts, tname), cons) =
|
|
117 |
("val (thy, " ^ tname ^ "_add_primrec) = add_datatype\n"
|
|
118 |
^ mk_triple (mk_list ts, quote tname, mk_list (mk_cons cons)) ^ " thy\n\
|
|
119 |
\val thy = thy",
|
|
120 |
"structure " ^ tname ^ " =\n\
|
|
121 |
\struct\n\
|
|
122 |
\ val inject = map (get_axiom thy) " ^
|
|
123 |
mk_list (map (fn ((s, _), _) => quote ("inject_" ^ strip_quotes s))
|
|
124 |
(filter_out (null o snd o fst) cons)) ^ ";\n\
|
|
125 |
\ val distinct = " ^
|
|
126 |
(if length cons < dtK then "let val distinct' = " else "") ^
|
|
127 |
"map (get_axiom thy) " ^ mk_list (mk_distinct_rules cons tname) ^
|
|
128 |
(if length cons < dtK then
|
|
129 |
" in distinct' @ (map (fn t => sym COMP (t RS contrapos))\
|
|
130 |
\ distinct') end"
|
|
131 |
else "") ^ ";\n\
|
|
132 |
\ val induct = get_axiom thy \"" ^ tname ^ "_induct\";\n\
|
|
133 |
\ val cases =" ^ mk_rules tname cons "_case_" ^ ";\n\
|
|
134 |
\ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
|
|
135 |
\ val simps = inject @ distinct @ cases @ recs;\n\
|
|
136 |
\ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
|
|
137 |
\end;\n");
|
|
138 |
|
|
139 |
(*parsers*)
|
|
140 |
val tvars = type_args >> map (cat "dtVar");
|
|
141 |
val typ =
|
|
142 |
tvars -- name >> (cat "dtTyp" o mk_pair o apfst mk_list) ||
|
|
143 |
type_var >> cat "dtVar";
|
|
144 |
val opt_typs = optional ("(" $$-- list1 typ --$$ ")") [];
|
|
145 |
val constructor = name -- opt_typs -- opt_mixfix;
|
|
146 |
in
|
|
147 |
val datatype_decl =
|
|
148 |
(* FIXME tvars -> type_args *)
|
|
149 |
tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params;
|
|
150 |
end;
|
|
151 |
|
|
152 |
|
|
153 |
|
|
154 |
(** primrec **)
|
|
155 |
|
|
156 |
(* FIXME add_thms_as_axms (?) *)
|
|
157 |
|
|
158 |
fun mk_primrec_decl ((fname, tname), axms) =
|
|
159 |
let
|
|
160 |
fun mk_prove (name, eqn) =
|
|
161 |
"val " ^ name ^ " = prove_goalw thy [get_def thy " ^ fname ^ "] " ^ eqn ^ "\n\
|
|
162 |
\ (fn _ => [simp_tac (HOL_ss addsimps " ^ tname ^ ".recs) 1])";
|
|
163 |
val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
|
|
164 |
in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)) end;
|
|
165 |
|
|
166 |
val primrec_decl =
|
|
167 |
name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl;
|
|
168 |
|
|
169 |
|
|
170 |
|
|
171 |
(** sections **)
|
|
172 |
|
|
173 |
val user_keywords = ["intrs", "monos", "con_defs", "|"];
|
160
|
174 |
|
|
175 |
val user_sections =
|
|
176 |
[axm_section "subtype" "|> Subtype.add_subtype" subtype_decl,
|
|
177 |
("inductive", inductive_decl ""),
|
172
|
178 |
("coinductive", inductive_decl "Co"),
|
|
179 |
("datatype", datatype_decl),
|
|
180 |
("primrec", primrec_decl)];
|
160
|
181 |
|
|
182 |
|
|
183 |
end;
|
|
184 |
|
|
185 |
|
|
186 |
structure ThySyn = ThySynFun(ThySynData);
|
|
187 |
init_thy_reader ();
|
172
|
188 |
|