author | clasohm |
Fri, 08 Sep 1995 13:23:04 +0200 | |
changeset 1251 | 81fc4d8e3eda |
parent 977 | 5d57287e5e1e |
child 1264 | 3eb91524b938 |
permissions | -rw-r--r-- |
923 | 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"); |
|
1251
81fc4d8e3eda
added nested types on right hand side of datatype definitions
clasohm
parents:
977
diff
changeset
|
141 |
fun complex_typ toks = |
81fc4d8e3eda
added nested types on right hand side of datatype definitions
clasohm
parents:
977
diff
changeset
|
142 |
(("(" $$-- complex_typ --$$ ")" >> (fn x => [x]) || tvars) |
81fc4d8e3eda
added nested types on right hand side of datatype definitions
clasohm
parents:
977
diff
changeset
|
143 |
-- (ident>>quote) >> (cat "dtTyp" o mk_pair o apfst mk_list) |
81fc4d8e3eda
added nested types on right hand side of datatype definitions
clasohm
parents:
977
diff
changeset
|
144 |
|| type_var >> cat "dtVar") toks; |
977
5d57287e5e1e
changed syntax of datatype declarations (curried types for constructor
clasohm
parents:
923
diff
changeset
|
145 |
val simple_typ = ident>>(cat "dtTyp" o curry mk_pair "[]" o quote) || |
5d57287e5e1e
changed syntax of datatype declarations (curried types for constructor
clasohm
parents:
923
diff
changeset
|
146 |
type_var >> cat "dtVar"; |
5d57287e5e1e
changed syntax of datatype declarations (curried types for constructor
clasohm
parents:
923
diff
changeset
|
147 |
val opt_typs = repeat (simple_typ || ("(" $$-- complex_typ --$$ ")")); |
923 | 148 |
val constructor = name -- opt_typs -- opt_mixfix; |
149 |
in |
|
150 |
val datatype_decl = |
|
151 |
(* FIXME tvars -> type_args *) |
|
152 |
tvars -- ident --$$ "=" -- enum1 "|" constructor >> mk_params; |
|
153 |
end; |
|
154 |
||
155 |
||
156 |
||
157 |
(** primrec **) |
|
158 |
||
159 |
fun mk_primrec_decl ((fname, tname), axms) = |
|
160 |
let |
|
161 |
fun mk_prove (name, eqn) = |
|
162 |
"val " ^ name ^ " = store_thm (" ^ quote name ^ ", prove_goalw thy [get_def thy " |
|
163 |
^ fname ^ "] " ^ eqn ^ "\n\ |
|
164 |
\ (fn _ => [simp_tac (HOL_ss addsimps " ^ tname ^ ".recs) 1]));"; |
|
165 |
val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms); |
|
166 |
in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)) end; |
|
167 |
||
168 |
val primrec_decl = |
|
169 |
name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl; |
|
170 |
||
171 |
||
172 |
||
173 |
(** sections **) |
|
174 |
||
175 |
val user_keywords = ["intrs", "monos", "con_defs", "|"]; |
|
176 |
||
177 |
val user_sections = |
|
178 |
[axm_section "subtype" "|> Subtype.add_subtype" subtype_decl, |
|
179 |
("inductive", inductive_decl ""), |
|
180 |
("coinductive", inductive_decl "Co"), |
|
181 |
("datatype", datatype_decl), |
|
182 |
("primrec", primrec_decl)]; |
|
183 |
||
184 |
||
185 |
end; |
|
186 |
||
187 |
||
188 |
structure ThySyn = ThySynFun(ThySynData); |
|
189 |
init_thy_reader (); |
|
190 |