author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 3399  0c4efa9eac29 
permissions  rwrr 
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

1 
(* Title: ZF/thy_syntax.ML 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

2 
ID: $Id$ 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

3 
Author: Lawrence C Paulson 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

4 
Copyright 1994 University of Cambridge 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

5 

713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

6 
Additional theory file sections for ZF 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

7 
*) 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

8 

713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

9 
structure ThySynData: THY_SYN_DATA = 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

10 
struct 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

11 

713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

12 
(*Inductive definitions theory section. co is either "" or "Co"*) 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

13 
fun inductive_decl co = 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

14 
let open ThyParse 
1428  15 
fun mk_intr_name (s,_) = (*the "op" cancels any infix status*) 
1461  16 
if Syntax.is_identifier s then "op " ^ s else "_" 
1428  17 
fun mk_params ((((((rec_tms, sdom_sum), ipairs), 
1461  18 
monos), con_defs), type_intrs), type_elims) = 
1428  19 
let val big_rec_name = space_implode "_" 
1461  20 
(map (scan_to_id o trim) rec_tms) 
21 
and srec_tms = mk_list rec_tms 

22 
and sintrs = mk_big_list (map snd ipairs) 

23 
val stri_name = big_rec_name ^ "_Intrnl" 

1428  24 
in 
1461  25 
(";\n\n\ 
26 
\structure " ^ stri_name ^ " =\n\ 

27 
\ struct\n\ 

28 
\ val _ = writeln \"" ^ co ^ 

29 
"Inductive definition " ^ big_rec_name ^ "\"\n\ 

30 
\ val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) " 

31 
^ srec_tms ^ "\n\ 

32 
\ and dom_sum\t= readtm (sign_of thy) Ind_Syntax.iT " ^ sdom_sum ^ "\n\ 

33 
\ and intr_tms\t= map (readtm (sign_of thy) propT)\n" 

34 
^ sintrs ^ "\n\ 

35 
\ end;\n\n\ 

36 
\val thy = thy > " ^ co ^ "Ind.add_fp_def_i \n (" ^ 

37 
stri_name ^ ".rec_tms, " ^ 

38 
stri_name ^ ".dom_sum, " ^ 

39 
stri_name ^ ".intr_tms)" 

40 
, 

41 
"structure " ^ big_rec_name ^ " =\n\ 

42 
\ let\n\ 

43 
\ val _ = writeln \"Proofs for " ^ co ^ 

44 
"Inductive definition " ^ big_rec_name ^ "\"\n\ 

45 
\ structure Result = " ^ co ^ "Ind_section_Fun\n\ 

46 
\\t (open " ^ stri_name ^ "\n\ 

47 
\\t val thy\t\t= thy\n\ 

48 
\\t val monos\t\t= " ^ monos ^ "\n\ 

49 
\\t val con_defs\t\t= " ^ con_defs ^ "\n\ 

50 
\\t val type_intrs\t= " ^ type_intrs ^ "\n\ 

51 
\\t val type_elims\t= " ^ type_elims ^ ")\n\ 

52 
\ in\n\ 

53 
\ struct\n\ 

54 
\ val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\ 

55 
\ open Result\n\ 

56 
\ end\n\ 

57 
\ end;\n\n\ 

58 
\structure " ^ stri_name ^ " = struct end;\n\n" 

59 
) 

1428  60 
end 
61 
val domains = "domains" $$ enum1 "+" string $$ "<="  !! string 

62 
val ipairs = "intrs" $$ repeat1 (ident  !! string) 

63 
fun optstring s = optional (s $$ string) "\"[]\"" >> trim 

797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

64 
in domains  ipairs  optstring "monos"  optstring "con_defs" 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

65 
 optstring "type_intrs"  optstring "type_elims" 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

66 
>> mk_params 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

67 
end; 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

68 

713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

69 

713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

70 
(*Datatype definitions theory section. co is either "" or "Co"*) 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

71 
fun datatype_decl co = 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

72 
let open ThyParse 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

73 
(*generate strings*) 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

74 
fun mk_const ((x, y), z) = mk_triple (x, mk_list y, z); 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

75 
val mk_data = mk_list o map mk_const o snd 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

76 
val mk_scons = mk_big_list o map mk_data 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

77 
fun mk_intr_name s = (*the "op" cancels any infix status*) 
1461  78 
if Syntax.is_identifier s then "op " ^ s ^ "_I" else "_" 
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

79 
fun mk_params ((((dom, rec_pairs), monos), type_intrs), type_elims) = 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

80 
let val rec_names = map (scan_to_id o trim o fst) rec_pairs 
1461  81 
val big_rec_name = space_implode "_" rec_names 
82 
and srec_tms = mk_list (map fst rec_pairs) 

797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

83 
and scons = mk_scons rec_pairs 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

84 
and sdom_sum = 
1461  85 
if dom = "" then (*default domain: univ or quniv*) 
86 
"Ind_Syntax." ^ co ^ "data_domain rec_tms" 

87 
else "readtm (sign_of thy) Ind_Syntax.iT " ^ dom 

797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

88 
val stri_name = big_rec_name ^ "_Intrnl" 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

89 
val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs) 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

90 
in 
1461  91 
(";\n\n\ 
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

92 
\structure " ^ stri_name ^ " =\n\ 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

93 
\ struct\n\ 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

94 
\ val _ = writeln \"" ^ co ^ 
1461  95 
"Datatype definition " ^ big_rec_name ^ "\"\n\ 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

96 
\ val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.iT) " ^ srec_tms ^ "\n\ 
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

97 
\ val dom_sum\t= " ^ sdom_sum ^ "\n\ 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

98 
\ and con_ty_lists\t= Ind_Syntax.read_constructs (sign_of thy)\n" 
1461  99 
^ scons ^ "\n\ 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

100 
\ val intr_tms\t= Ind_Syntax.mk_all_intr_tms (rec_tms, con_ty_lists)\n\ 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

101 
\ end;\n\n\ 
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

102 
\val thy = thy > " ^ co ^ "Ind.add_constructs_def(" ^ 
1461  103 
mk_list (map quote rec_names) ^ ", " ^ 
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

104 
stri_name ^ ".con_ty_lists) \n\ 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

105 
\ > " ^ co ^ "Ind.add_fp_def_i \n (" ^ 
1461  106 
stri_name ^ ".rec_tms, " ^ 
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

107 
stri_name ^ ".dom_sum, " ^ 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

108 
stri_name ^ ".intr_tms)" 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

109 
, 
1461  110 
"structure " ^ big_rec_name ^ " =\n\ 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

111 
\ let\n\ 
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

112 
\ val _ = writeln \"Proofs for " ^ co ^ 
1461  113 
"Datatype definition " ^ big_rec_name ^ "\"\n\ 
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

114 
\ structure Result = " ^ co ^ "Data_section_Fun\n\ 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

115 
\\t (open " ^ stri_name ^ "\n\ 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

116 
\\t val thy\t\t= thy\n\ 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

117 
\\t val big_rec_name\t= \"" ^ big_rec_name ^ "\"\n\ 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

118 
\\t val monos\t\t= " ^ monos ^ "\n\ 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

119 
\\t val type_intrs\t= " ^ type_intrs ^ "\n\ 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

120 
\\t val type_elims\t= " ^ type_elims ^ ");\n\ 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

121 
\ in\n\ 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

122 
\ struct\n\ 
797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

123 
\ val " ^ mk_list (map mk_intr_name con_names) ^ " = Result.intrs;\n\ 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

124 
\ open Result\n\ 
1418
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

125 
\ end\n\ 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

126 
\ end;\n\n\ 
f5f97ee67cbb
Improving space efficiency of inductive/datatype definitions.
paulson
parents:
797
diff
changeset

127 
\structure " ^ stri_name ^ " = struct end;\n\n" 
1461  128 
) 
129 
end 

797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

130 
fun optstring s = optional (s $$ string) "\"[]\"" >> trim 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

131 
val string_list = "(" $$ list1 string $$ ")"  ThyParse.empty; 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

132 
val construct = name  string_list  opt_mixfix; 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

133 
in optional ("<=" $$ string) ""  
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

134 
enum1 "and" (string $$ "="  enum1 "" construct)  
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

135 
optstring "monos"  optstring "type_intrs"  optstring "type_elims" 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

136 
>> mk_params 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

137 
end; 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

138 

713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

139 

713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

140 
(** Section specifications **) 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

141 

713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

142 
val user_keywords = ["inductive", "coinductive", "datatype", "codatatype", 
1461  143 
"and", "", "<=", "domains", "intrs", "monos", 
144 
"con_defs", "type_intrs", "type_elims"]; 

797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

145 

713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

146 
val user_sections = [("inductive", inductive_decl ""), 
1461  147 
("coinductive", inductive_decl "Co"), 
148 
("datatype", datatype_decl ""), 

149 
("codatatype", datatype_decl "Co")]; 

797
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

150 
end; 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

151 

713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

152 

713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

153 
structure ThySyn = ThySynFun(ThySynData); 
713efca1f0aa
Defines ZF theory sections (inductive, datatype) at the start/
lcp
parents:
diff
changeset

154 
init_thy_reader (); 