1 (* Title: HOL/thy_syntax.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel and Lawrence C Paulson and Carsten Clasohm |
|
4 |
|
5 Additional theory file sections for HOL. |
|
6 |
|
7 TODO: |
|
8 move datatype / primrec stuff to pre_datatype.ML (?) |
|
9 *) |
|
10 |
|
11 (*the kind of distinctiveness axioms depends on number of constructors*) |
|
12 val dtK = 5; (* FIXME rename?, move? *) |
|
13 |
|
14 structure ThySynData: THY_SYN_DATA = |
|
15 struct |
|
16 |
|
17 open ThyParse; |
|
18 |
|
19 |
|
20 (** subtype **) |
|
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], |
|
28 [name ^ "_def", "Rep_" ^ name, "Rep_" ^ name ^ "_inverse", |
|
29 "Abs_" ^ name ^ "_inverse"]) |
|
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 |
|
38 |
|
39 (** (co)inductive **) |
|
40 |
|
41 (*co is either "" or "Co"*) |
|
42 fun inductive_decl co = |
|
43 let |
|
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 |
|
85 end; |
|
86 |
|
87 |
|
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); |
|
114 |
|
115 (*generate string for calling add_datatype*) |
|
116 fun mk_params ((ts, tname), cons) = |
|
117 ("val (thy, " ^ tname ^ "_add_primrec) = Datatype.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 -- (ident>>quote) >> (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 fun mk_primrec_decl ((fname, tname), axms) = |
|
157 let |
|
158 fun mk_prove (name, eqn) = |
|
159 "val " ^ name ^ " = store_thm (" ^ quote name ^ ", prove_goalw thy [get_def thy " |
|
160 ^ fname ^ "] " ^ eqn ^ "\n\ |
|
161 \ (fn _ => [simp_tac (HOL_ss addsimps " ^ tname ^ ".recs) 1]));"; |
|
162 val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms); |
|
163 in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)) end; |
|
164 |
|
165 val primrec_decl = |
|
166 name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl; |
|
167 |
|
168 |
|
169 |
|
170 (** sections **) |
|
171 |
|
172 val user_keywords = ["intrs", "monos", "con_defs", "|"]; |
|
173 |
|
174 val user_sections = |
|
175 [axm_section "subtype" "|> Subtype.add_subtype" subtype_decl, |
|
176 ("inductive", inductive_decl ""), |
|
177 ("coinductive", inductive_decl "Co"), |
|
178 ("datatype", datatype_decl), |
|
179 ("primrec", primrec_decl)]; |
|
180 |
|
181 |
|
182 end; |
|
183 |
|
184 |
|
185 structure ThySyn = ThySynFun(ThySynData); |
|
186 init_thy_reader (); |
|
187 |
|