|
1 (* Title: HOL/thy_syntax.ML |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel and Lawrence C Paulson |
|
4 |
|
5 Additional theory file sections for HOL. |
|
6 |
|
7 TODO: |
|
8 datatype, primrec |
|
9 *) |
|
10 |
|
11 structure ThySynData: THY_SYN_DATA = |
|
12 struct |
|
13 |
|
14 open ThyParse; |
|
15 |
|
16 |
|
17 (* subtype *) |
|
18 |
|
19 fun mk_subtype_decl (((((opt_name, vs), t), mx), rhs), wt) = |
|
20 let |
|
21 val name' = if_none opt_name t; |
|
22 val name = strip_quotes name'; |
|
23 in |
|
24 (cat_lines [name', mk_triple (t, mk_list vs, mx), rhs, wt], |
|
25 ["Rep_" ^ name, "Rep_" ^ name ^ "_inverse", "Abs_" ^ name ^ "_inverse"]) |
|
26 end; |
|
27 |
|
28 val subtype_decl = |
|
29 optional ("(" $$-- name --$$ ")" >> Some) None -- |
|
30 type_args -- name -- opt_infix --$$ "=" -- string -- opt_witness |
|
31 >> mk_subtype_decl; |
|
32 |
|
33 |
|
34 (* (co)inductive *) |
|
35 |
|
36 (*co is either "" or "Co"*) |
|
37 fun inductive_decl co = |
|
38 let |
|
39 fun mk_intr_name (s,_) = (*the "op" cancels any infix status*) |
|
40 if Syntax.is_identifier s then "op " ^ s else "_" |
|
41 fun mk_params (((recs, ipairs), monos), con_defs) = |
|
42 let val big_rec_name = space_implode "_" (map (scan_to_id o trim) recs) |
|
43 and srec_tms = mk_list recs |
|
44 and sintrs = mk_big_list (map snd ipairs) |
|
45 val stri_name = big_rec_name ^ "_Intrnl" |
|
46 in |
|
47 (";\n\n\ |
|
48 \structure " ^ stri_name ^ " =\n\ |
|
49 \ let open Ind_Syntax in\n\ |
|
50 \ struct\n\ |
|
51 \ val _ = writeln \"" ^ co ^ |
|
52 "Inductive definition " ^ big_rec_name ^ "\"\n\ |
|
53 \ val rec_tms\t= map (readtm (sign_of thy) termTVar) " |
|
54 ^ srec_tms ^ "\n\ |
|
55 \ and intr_tms\t= map (readtm (sign_of thy) propT)\n" |
|
56 ^ sintrs ^ "\n\ |
|
57 \ end\n\ |
|
58 \ end;\n\n\ |
|
59 \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n (" ^ |
|
60 stri_name ^ ".rec_tms, " ^ |
|
61 stri_name ^ ".intr_tms)" |
|
62 , |
|
63 "structure " ^ big_rec_name ^ " =\n\ |
|
64 \ struct\n\ |
|
65 \ structure Result = " ^ co ^ "Ind_section_Fun\n\ |
|
66 \ (open " ^ stri_name ^ "\n\ |
|
67 \ val thy\t\t= thy\n\ |
|
68 \ val monos\t\t= " ^ monos ^ "\n\ |
|
69 \ val con_defs\t\t= " ^ con_defs ^ ");\n\n\ |
|
70 \ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\ |
|
71 \ open Result\n\ |
|
72 \ end\n" |
|
73 ) |
|
74 end |
|
75 val ipairs = "intrs" $$-- repeat1 (ident -- !! string) |
|
76 fun optstring s = optional (s $$-- string) "\"[]\"" >> trim |
|
77 in repeat1 string -- ipairs -- optstring "monos" -- optstring "con_defs" |
|
78 >> mk_params |
|
79 end; |
|
80 |
|
81 |
|
82 (* sections *) |
|
83 |
|
84 val user_keywords = ["|", "intrs", "monos", "con_defs"]; |
|
85 |
|
86 val user_sections = |
|
87 [axm_section "subtype" "|> Subtype.add_subtype" subtype_decl, |
|
88 ("inductive", inductive_decl ""), |
|
89 ("coinductive", inductive_decl "Co")]; |
|
90 |
|
91 |
|
92 end; |
|
93 |
|
94 |
|
95 structure ThySyn = ThySynFun(ThySynData); |
|
96 init_thy_reader (); |