author  ballarin 
Fri, 14 Nov 2008 16:49:52 +0100  
changeset 28795  6891e273c33b 
parent 28701  ca5840b1f7b3 
child 28832  cf7237498e7a 
permissions  rwrr 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

1 
(* Title: Pure/Isar/expression.ML 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

2 
ID: $Id$ 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

3 
Author: Clemens Ballarin, TU Muenchen 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

4 

28795  5 
New locale development  experimental. 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

6 
*) 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

7 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

8 
signature EXPRESSION = 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

9 
sig 
28795  10 
type map 
11 
type 'morph expr 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

12 

28795  13 
val empty_expr: 'morph expr 
14 

15 
type expression = (string * map) expr * (Name.binding * string option * mixfix) list 

16 
type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

17 

28795  18 
(* Declaring locales *) 
19 
val add_locale: string > bstring > expression > Element.context list > theory > 

20 
string * Proof.context 

21 
(* 

22 
val add_locale_i: string > bstring > expression_i > Element.context_i list > theory > 

23 
string * Proof.context 

24 
*) 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

25 

28795  26 
(* Debugging and development *) 
27 
val parse_expression: OuterParse.token list > expression * OuterParse.token list 

28 
val debug_parameters: expression > Proof.context > Proof.context 

29 
val debug_context: expression > Proof.context > Proof.context 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

30 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

31 
end; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

32 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

33 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

34 
structure Expression: EXPRESSION = 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

35 
struct 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

36 

28795  37 
datatype ctxt = datatype Element.ctxt; 
38 

39 

40 
(*** Expressions ***) 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

41 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

42 
datatype map = 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

43 
Positional of string option list  
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

44 
Named of (string * string) list; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

45 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

46 
datatype 'morph expr = Expr of (string * 'morph) list; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

47 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

48 
type expression = (string * map) expr * (Name.binding * string option * mixfix) list; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

49 
type expression_i = Morphism.morphism expr * (Name.binding * typ option * mixfix) list; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

50 

28795  51 
val empty_expr = Expr []; 
52 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

53 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

54 
(** Parsing and printing **) 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

55 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

56 
local 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

57 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

58 
structure P = OuterParse; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

59 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

60 
val loc_keyword = P.$$$ "fixes"  P.$$$ "constrains"  P.$$$ "assumes"  
28795  61 
P.$$$ "defines"  P.$$$ "notes"; 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

62 
fun plus1_unless test scan = 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

63 
scan ::: Scan.repeat (P.$$$ "+"  Scan.unless test (P.!!! scan)); 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

64 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

65 
val prefix = P.name  P.$$$ ":"; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

66 
val named = P.name  (P.$$$ "="  P.term); 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

67 
val position = P.maybe P.term; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

68 
val instance = P.$$$ "where"  P.and_list1 named >> Named  
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

69 
Scan.repeat1 position >> Positional; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

70 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

71 
in 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

72 

28795  73 
val parse_expression = 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

74 
let 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

75 
fun expr2 x = P.xname x; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

76 
fun expr1 x = (Scan.optional prefix ""  expr2  
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

77 
Scan.optional instance (Named []) >> (fn ((p, l), i) => (l, (p, i)))) x; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

78 
fun expr0 x = (plus1_unless loc_keyword expr1 >> Expr) x; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

79 
in expr0  P.for_fixes end; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

80 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

81 
end; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

82 

28795  83 
fun pretty_expr thy (Expr expr) = 
84 
let 

85 
fun pretty_pos NONE = Pretty.str "_" 

86 
 pretty_pos (SOME x) = Pretty.str x; 

87 
fun pretty_named (x, y) = [Pretty.str x, Pretty.brk 1, Pretty.str "=", 

88 
Pretty.brk 1, Pretty.str y] > Pretty.block; 

89 
fun pretty_ren (Positional ps) = take_suffix is_none ps > snd > 

90 
map pretty_pos > Pretty.breaks 

91 
 pretty_ren (Named []) = [] 

92 
 pretty_ren (Named ps) = Pretty.str "where" :: Pretty.brk 1 :: 

93 
(ps > map pretty_named > Pretty.separate "and"); 

94 
fun pretty_rename (loc, ("", ren)) = 

95 
Pretty.block (Pretty.str (NewLocale.extern thy loc) :: Pretty.brk 1 :: pretty_ren ren) 

96 
 pretty_rename (loc, (prfx, ren)) = 

97 
Pretty.block (Pretty.str prfx :: Pretty.brk 1 :: Pretty.str (NewLocale.extern thy loc) :: 

98 
Pretty.brk 1 :: pretty_ren ren); 

99 
in Pretty.separate "+" (map pretty_rename expr) > Pretty.block end; 

100 

101 
fun err_in_expr thy msg (Expr expr) = 

102 
let 

103 
val err_msg = 

104 
if null expr then msg 

105 
else msg ^ "\n" ^ Pretty.string_of (Pretty.block 

106 
[Pretty.str "The above error(s) occurred in expression:", Pretty.brk 1, 

107 
pretty_expr thy (Expr expr)]) 

108 
in error err_msg end; 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

109 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

110 

28795  111 
(** Internalise locale names **) 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

112 

28795  113 
fun intern_expr thy (Expr instances) = Expr (map (apfst (NewLocale.intern thy)) instances); 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

114 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

115 

28795  116 
(** Parameters of expression (not expression_i). 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

117 
Sanity check of instantiations. 
28795  118 
Positional instantiations are extended to match full length of parameter list. **) 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

119 

28701  120 
fun parameters thy (expr, fixed : (Name.binding * string option * mixfix) list) = 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

121 
let 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

122 
fun reject_dups message xs = 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

123 
let val dups = duplicates (op =) xs 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

124 
in 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

125 
if null dups then () else error (message ^ commas dups) 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

126 
end; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

127 

28795  128 
fun match_bind (n, b) = (n = Name.name_of b); 
129 
fun bind_eq (b1, b2) = (Name.name_of b1 = Name.name_of b2); 

130 
(* FIXME: cannot compare bindings for equality. *) 

131 

132 
fun params_loc loc = 

133 
(NewLocale.params_of thy loc > map (fn (p, _, mx) => (p, mx)), loc) 

134 
handle ERROR msg => err_in_expr thy msg (Expr [(loc, ("", Named []))]); 

135 
fun params_inst (expr as (loc, (prfx, Positional insts))) = 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

136 
let 
28795  137 
val (ps, loc') = params_loc loc; 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

138 
val d = length ps  length insts; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

139 
val insts' = 
28795  140 
if d < 0 then err_in_expr thy "More arguments than parameters in instantiation." 
141 
(Expr [expr]) 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

142 
else insts @ replicate d NONE; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

143 
val ps' = (ps ~~ insts') > 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

144 
map_filter (fn (p, NONE) => SOME p  (_, SOME _) => NONE); 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

145 
in 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

146 
(ps', (loc', (prfx, Positional insts'))) 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

147 
end 
28795  148 
 params_inst (expr as (loc, (prfx, Named insts))) = 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

149 
let 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

150 
val _ = reject_dups "Duplicate instantiation of the following parameter(s): " 
28795  151 
(map fst insts) 
152 
handle ERROR msg => err_in_expr thy msg (Expr [expr]); 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

153 

28795  154 
val (ps, loc') = params_loc loc; 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

155 
val ps' = fold (fn (p, _) => fn ps => 
28795  156 
if AList.defined match_bind ps p then AList.delete match_bind p ps 
157 
else err_in_expr thy (quote p ^" not a parameter of instantiated expression.") 

158 
(Expr [expr])) insts ps; 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

159 
in 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

160 
(ps', (loc', (prfx, Named insts))) 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

161 
end; 
28795  162 
fun params_expr (Expr is) = 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

163 
let 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

164 
val (is', ps') = fold_map (fn i => fn ps => 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

165 
let 
28795  166 
val (ps', i') = params_inst i; 
167 
val ps'' = AList.join bind_eq (fn p => fn (mx1, mx2) => 

168 
(* FIXME: should check for bindings being the same. 

169 
Instead we check for equal name and syntax. *) 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

170 
if mx1 = mx2 then mx1 
28795  171 
else err_in_expr thy ("Conflicting syntax for parameter" ^ quote (Name.name_of p) ^ " in expression.") 
172 
(Expr is)) (ps, ps') 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

173 
in (i', ps'') end) is [] 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

174 
in 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

175 
(ps', Expr is') 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

176 
end; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

177 

28795  178 
val (parms, expr') = params_expr expr; 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

179 

28795  180 
val parms' = map (fst #> Name.name_of) parms; 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

181 
val fixed' = map (#1 #> Name.name_of) fixed; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

182 
val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

183 
val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (parms' @ fixed'); 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

184 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

185 
in (expr', (parms, fixed)) end; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

186 

28795  187 

188 
(** Read instantiation **) 

189 

190 
fun read_inst parse_term parms (prfx, insts) ctxt = 

191 
let 

192 
(* parameters *) 

193 
val (parm_names, parm_types) = split_list parms; 

194 
val type_parm_names = fold Term.add_tfreesT parm_types [] > map fst; 

195 

196 
(* parameter instantiations *) 

197 
val insts' = case insts of 

198 
Positional insts => (insts ~~ parm_names) > map (fn 

199 
(NONE, p) => parse_term ctxt p  

200 
(SOME t, _) => parse_term ctxt t)  

201 
Named insts => parm_names > map (fn 

202 
p => case AList.lookup (op =) insts p of 

203 
SOME t => parse_term ctxt t  

204 
NONE => parse_term ctxt p); 

205 

206 
(* type inference and contexts *) 

207 
val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types; 

208 
val type_parms = fold Term.add_tvarsT parm_types' [] > map (Logic.mk_type o TVar); 

209 
val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts'; 

210 
val res = Syntax.check_terms ctxt arg; 

211 
val ctxt' = ctxt > fold Variable.auto_fixes res; 

212 

213 
(* instantiation *) 

214 
val (type_parms'', res') = chop (length type_parms) res; 

215 
val insts'' = (parm_names ~~ res') > map_filter 

216 
(fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst  

217 
inst => SOME inst); 

218 
val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms''); 

219 
val inst = Symtab.make insts''; 

220 
in 

221 
(Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $> 

222 
Morphism.name_morphism (Name.qualified prfx), ctxt') 

223 
end; 

224 

225 

226 
(** Debugging **) 

227 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

228 
fun debug_parameters raw_expr ctxt = 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

229 
let 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

230 
val thy = ProofContext.theory_of ctxt; 
28795  231 
val expr = apfst (intern_expr thy) raw_expr; 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

232 
val (expr', (parms, fixed)) = parameters thy expr; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

233 
in ctxt end; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

234 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

235 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

236 
fun debug_context (raw_expr, fixed) ctxt = 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

237 
let 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

238 
val thy = ProofContext.theory_of ctxt; 
28795  239 
val expr = intern_expr thy raw_expr; 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

240 
val (expr', (parms, fixed)) = parameters thy (expr, fixed); 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

241 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

242 
fun declare_parameters (parms, fixed) ctxt = 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

243 
let 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

244 
val (parms', ctxt') = 
28795  245 
ProofContext.add_fixes (map (fn (p, mx) => (p, NONE, mx)) parms) ctxt; 
28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

246 
val (fixed', ctxt'') = 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

247 
ProofContext.add_fixes fixed ctxt'; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

248 
in 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

249 
(parms' @ fixed', ctxt'') 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

250 
end; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

251 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

252 
fun rough_inst loc prfx insts ctxt = 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

253 
let 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

254 
(* locale data *) 
28795  255 
val (parm_names, parm_types) = loc > NewLocale.params_of thy > 
256 
map (fn (b, SOME T, _) => (Name.name_of b, T)) > split_list; 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

257 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

258 
(* type parameters *) 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

259 
val type_parm_names = fold Term.add_tfreesT parm_types [] > map fst; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

260 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

261 
(* parameter instantiations *) 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

262 
val insts' = case insts of 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

263 
Positional insts => (insts ~~ parm_names) > map (fn 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

264 
(NONE, p) => Syntax.parse_term ctxt p  
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

265 
(SOME t, _) => Syntax.parse_term ctxt t)  
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

266 
Named insts => parm_names > map (fn 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

267 
p => case AList.lookup (op =) insts p of 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

268 
SOME t => Syntax.parse_term ctxt t  
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

269 
NONE => Syntax.parse_term ctxt p); 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

270 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

271 
(* type inference and contexts *) 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

272 
val parm_types' = map (TypeInfer.paramify_vars o Logic.varifyT) parm_types; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

273 
val type_parms = fold Term.add_tvarsT parm_types' [] > map (Logic.mk_type o TVar); 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

274 
val arg = type_parms @ map2 TypeInfer.constrain parm_types' insts'; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

275 
val res = Syntax.check_terms ctxt arg; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

276 
val ctxt' = ctxt > fold Variable.auto_fixes res; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

277 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

278 
(* instantiation *) 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

279 
val (type_parms'', res') = chop (length type_parms) res; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

280 
val insts'' = (parm_names ~~ res') > map_filter 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

281 
(fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst  
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

282 
inst => SOME inst); 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

283 
val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms''); 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

284 
val inst = Symtab.make insts''; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

285 
in 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

286 
(Element.inst_morphism thy (instT, inst) $> 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

287 
Morphism.name_morphism (Name.qualified prfx), ctxt') 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

288 
end; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

289 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

290 
fun add_declarations loc morph ctxt = 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

291 
let 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

292 
(* locale data *) 
28795  293 
val parms = loc > NewLocale.params_of thy > 
294 
map (fn (b, SOME T, mx) => ((Name.name_of b, T), mx)); 

295 
val (typ_decls, term_decls) = NewLocale.declarations_of thy loc; 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

296 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

297 
(* declarations from locale *) 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

298 
val ctxt'' = ctxt > 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

299 
fold_rev (fn decl => Context.proof_map (decl morph)) typ_decls > 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

300 
fold_rev (fn decl => Context.proof_map (decl morph)) term_decls; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

301 
in 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

302 
ctxt'' 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

303 
end; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

304 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

305 
val Expr [(loc1, (prfx1, insts1))] = expr'; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

306 
val ctxt0 = ProofContext.init thy; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

307 
val (parms, ctxt') = declare_parameters (parms, fixed) ctxt0; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

308 
val (morph1, ctxt'') = rough_inst loc1 prfx1 insts1 ctxt'; 
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

309 
val ctxt'' = add_declarations loc1 morph1 ctxt'; 
28795  310 
in ctxt0 end; 
311 

312 

313 
(*** Locale processing ***) 

314 

315 
(** Prepare locale elements **) 

316 

317 
local 

318 

319 
fun declare_elem prep_vars (Fixes fixes) ctxt = 

320 
let val (vars, _) = prep_vars fixes ctxt 

321 
in ([], ctxt > ProofContext.add_fixes_i vars > snd) end 

322 
 declare_elem prep_vars (Constrains csts) ctxt = 

323 
let val (_, ctxt') = prep_vars (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) csts) ctxt 

324 
in ([], ctxt') end 

325 
 declare_elem _ (Assumes asms) ctxt = (map #2 asms, ctxt) 

326 
 declare_elem _ (Defines defs) ctxt = (map (fn (_, (t, ps)) => [(t, ps)]) defs, ctxt) 

327 
 declare_elem _ (Notes _) ctxt = ([], ctxt); 

328 

329 
in 

330 

331 
fun declare_elems prep_vars raw_elems ctxt = 

332 
fold_map (declare_elem prep_vars) raw_elems ctxt; 

333 

334 
end; 

335 

336 
local 

337 

338 
val norm_term = Envir.beta_norm oo Term.subst_atomic; 

339 

340 
fun abstract_thm thy eq = 

341 
Thm.assume (Thm.cterm_of thy eq) > Drule.gen_all > Drule.abs_def; 

342 

343 
fun bind_def ctxt eq (xs, env, ths) = 

344 
let 

345 
val ((y, T), b) = LocalDefs.abs_def eq; 

346 
val b' = norm_term env b; 

347 
val th = abstract_thm (ProofContext.theory_of ctxt) eq; 

348 
fun err msg = error (msg ^ ": " ^ quote y); 

349 
in 

350 
exists (fn (x, _) => x = y) xs andalso 

351 
err "Attempt to define previously specified variable"; 

352 
exists (fn (Free (y', _), _) => y = y'  _ => false) env andalso 

353 
err "Attempt to redefine variable"; 

354 
(Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths) 

355 
end; 

356 

357 
fun eval_text _ (Fixes _) text = text 

358 
 eval_text _ (Constrains _) text = text 

359 
 eval_text _ (Assumes asms) 

360 
(((exts, exts'), (ints, ints')), (xs, env, defs)) = 

361 
let 

362 
val ts = maps (map #1 o #2) asms; 

363 
val ts' = map (norm_term env) ts; 

364 
val spec' = ((exts @ ts, exts' @ ts'), (ints, ints')); 

365 
in (spec', (fold Term.add_frees ts' xs, env, defs)) end 

366 
 eval_text ctxt (Defines defs) (spec, binds) = 

367 
(spec, fold (bind_def ctxt o #1 o #2) defs binds) 

368 
 eval_text _ (Notes _) text = text; 

369 

370 
fun closeup _ false elem = elem 

371 
 closeup ctxt true elem = 

372 
let 

373 
fun close_frees t = 

374 
let 

375 
val rev_frees = 

376 
Term.fold_aterms (fn Free (x, T) => 

377 
if Variable.is_fixed ctxt x then I else insert (op =) (x, T)  _ => I) t []; 

378 
in Term.list_all_free (rev rev_frees, t) end; 

379 

380 
fun no_binds [] = [] 

381 
 no_binds _ = error "Illegal term bindings in locale element"; 

382 
in 

383 
(case elem of 

384 
Assumes asms => Assumes (asms > map (fn (a, propps) => 

385 
(a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) 

386 
 Defines defs => Defines (defs > map (fn (a, (t, ps)) => 

387 
(a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps)))) 

388 
 e => e) 

389 
end; 

390 

391 
fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (binding, _, mx) => 

392 
let val x = Name.name_of binding 

393 
in (binding, AList.lookup (op =) parms x, mx) end) fixes) 

394 
 finish_ext_elem _ _ (Constrains _, _) = Constrains [] 

395 
 finish_ext_elem _ close (Assumes asms, propp) = 

396 
close (Assumes (map #1 asms ~~ propp)) 

397 
 finish_ext_elem _ close (Defines defs, propp) = 

398 
close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp)) 

399 
 finish_ext_elem _ _ (Notes facts, _) = Notes facts; 

400 

401 
fun finish_elem ctxt parms do_close (elem, propp) text = 

402 
let 

403 
val elem' = finish_ext_elem parms (closeup ctxt do_close) (elem, propp); 

404 
val text' = eval_text ctxt elem' text; 

405 
in (elem', text') end 

406 

407 
in 

408 

409 
fun finish_elems ctxt parms do_close elems text = 

410 
fold_map (finish_elem ctxt parms do_close) elems text; 

411 

412 
end; 

413 

414 

415 
local 

416 

417 
fun param_types ps = map_filter (fn (_, NONE) => NONE  (x, SOME T) => SOME (x, T)) ps; 

418 

419 
fun frozen_tvars ctxt Ts = 

420 
#1 (Variable.importT_inst (map Logic.mk_type Ts) ctxt) 

421 
> map (fn ((xi, S), T) => (xi, (S, T))); 

422 

423 
fun unify_frozen ctxt maxidx Ts Us = 

424 
let 

425 
fun paramify NONE i = (NONE, i) 

426 
 paramify (SOME T) i = apfst SOME (TypeInfer.paramify_dummies T i); 

427 

428 
val (Ts', maxidx') = fold_map paramify Ts maxidx; 

429 
val (Us', maxidx'') = fold_map paramify Us maxidx'; 

430 
val thy = ProofContext.theory_of ctxt; 

431 

432 
fun unify (SOME T, SOME U) env = (Sign.typ_unify thy (U, T) env 

433 
handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], [])) 

434 
 unify _ env = env; 

435 
val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx''); 

436 
val Vs = map (Option.map (Envir.norm_type unifier)) Us'; 

437 
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs)); 

438 
in map (Option.map (Envir.norm_type unifier')) Vs end; 

439 

440 
fun prep_elems prep_vars prepp do_close context raw_elems raw_concl = 

441 
let 

442 
val (raw_propps, raw_ctxt) = declare_elems prep_vars raw_elems context; 

443 
(* raw_ctxt is context enriched by syntax from raw_elems *) 

444 

445 
fun prep_prop raw_propp (raw_ctxt, raw_concl) = 

446 
let 

447 
(* process patterns (conclusion and external elements) *) 

448 
val (ctxt, all_propp) = prepp (raw_ctxt, raw_concl @ raw_propp); 

449 
(* add type information from conclusion and external elements to context *) 

450 
val ctxt = fold Variable.declare_term (maps (map fst) all_propp) ctxt; 

451 
(* resolve schematic variables (patterns) in conclusion and external elements. *) 

452 
val all_propp' = map2 (curry (op ~~)) 

453 
(#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp); 

454 
val (concl, propp) = chop (length raw_concl) all_propp'; 

455 
in (propp, (ctxt, concl)) end 

456 

457 
val (propps, (ctxt, concl)) = fold_burrow prep_prop raw_propps (raw_ctxt, raw_concl); 

458 

459 
(* Infer parameter types *) 

460 
val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes)  

461 
_ => fn ps => ps) raw_elems []; 

462 
val typing = unify_frozen ctxt 0 

463 
(map (Variable.default_type raw_ctxt) xs) 

464 
(map (Variable.default_type ctxt) xs); 

465 
val parms = param_types (xs ~~ typing); 

466 

467 
(* CB: extract information from assumes and defines elements 

468 
(fixes, constrains and notes in raw_elemss don't have an effect on 

469 
text and elemss), compute final form of context elements. *) 

470 
val (elems, text) = finish_elems ctxt parms do_close 

471 
(raw_elems ~~ propps) ((([], []), ([], [])), ([], [], [])); 

472 
(* CB: text has the following structure: 

473 
(((exts, exts'), (ints, ints')), (xs, env, defs)) 

474 
where 

475 
exts: external assumptions (terms in external assumes elements) 

476 
exts': dito, normalised wrt. env 

477 
ints: internal assumptions (terms in internal assumes elements) 

478 
ints': dito, normalised wrt. env 

479 
xs: the free variables in exts' and ints' and rhss of definitions, 

480 
this includes parameters except defined parameters 

481 
env: list of term pairs encoding substitutions, where the first term 

482 
is a free variable; substitutions represent defines elements and 

483 
the rhs is normalised wrt. the previous env 

484 
defs: theorems representing the substitutions from defines elements 

485 
(thms are normalised wrt. env). 

486 
elems is an updated version of raw_elems: 

487 
 type info added to Fixes and modified in Constrains 

488 
 axiom and definition statement replaced by corresponding one 

489 
from proppss in Assumes and Defines 

490 
 Facts unchanged 

491 
*) 

492 
in ((parms, elems, concl), text) end 

493 

494 
in 

495 

496 
fun read_elems x = prep_elems ProofContext.read_vars ProofContext.read_propp_schematic x; 

497 
fun cert_elems x = prep_elems ProofContext.cert_vars ProofContext.cert_propp_schematic x; 

498 

499 
end; 

500 

501 

502 
(* facts and attributes *) 

503 

504 
local 

505 

506 
fun check_name name = 

507 
if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name) 

508 
else name; 

509 

510 
fun prep_facts prep_name get intern ctxt elem = elem > Element.map_ctxt 

511 
{var = I, typ = I, term = I, 

512 
name = Name.map_name prep_name, 

513 
fact = get ctxt, 

514 
attrib = Args.assignable o intern (ProofContext.theory_of ctxt)}; 

515 

516 
in 

517 

518 
fun read_facts x = prep_facts check_name ProofContext.get_fact Attrib.intern_src x; 

519 
fun cert_facts x = prep_facts I (K I) (K I) x; 

520 

521 
end; 

522 

523 

524 
(* activate elements in context, return elements and facts *) 

525 

526 
local 

527 

528 
fun axioms_export axs _ As = 

529 
(Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t); 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

530 

140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

531 

28795  532 
(* NB: derived ids contain only facts at this stage *) 
533 

534 
fun activate_elem (Fixes fixes) ctxt = 

535 
([], ctxt > ProofContext.add_fixes_i fixes > snd) 

536 
 activate_elem (Constrains _) ctxt = 

537 
([], ctxt) 

538 
 activate_elem (Assumes asms) ctxt = 

539 
let 

540 
val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms; 

541 
val ts = maps (map #1 o #2) asms'; 

542 
val (_, ctxt') = 

543 
ctxt > fold Variable.auto_fixes ts 

544 
> ProofContext.add_assms_i (axioms_export []) asms'; 

545 
in ([], ctxt') end 

546 
 activate_elem (Defines defs) ctxt = 

547 
let 

548 
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs; 

549 
val asms = defs' > map (fn ((name, atts), (t, ps)) => 

550 
let val ((c, _), t') = LocalDefs.cert_def ctxt t 

551 
in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end); 

552 
val (_, ctxt') = 

553 
ctxt > fold (Variable.auto_fixes o #1) asms 

554 
> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms); 

555 
in ([], ctxt') end 

556 
 activate_elem (Notes (kind, facts)) ctxt = 

557 
let 

558 
val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts; 

559 
val (res, ctxt') = ctxt > ProofContext.note_thmss_i kind facts'; 

560 
in ((map (#1 o #1) facts' ~~ map #2 res), ctxt') end; 

561 

562 
in 

563 

564 
fun activate_elems prep_facts raw_elems ctxt = 

565 
let 

566 
val elems = map (prep_facts ctxt) raw_elems; 

567 
val (res, ctxt') = fold_map activate_elem elems (ProofContext.qualified_names ctxt); 

568 
val elems' = elems > map (Element.map_ctxt_attrib Args.closure); 

569 
in ((elems', flat res), ProofContext.restore_naming ctxt ctxt') end; 

570 

28697
140bfb63f893
Newstyle locale expressions with instantiation (new file expression.ML).
ballarin
parents:
diff
changeset

571 
end; 
28795  572 

573 

574 
(* full context statements: import + elements + conclusion *) 

575 

576 
local 

577 

578 
fun prep_context_statement prep_expr prep_elems prep_facts 

579 
do_close imprt elements raw_concl context = 

580 
let 

581 
val thy = ProofContext.theory_of context; 

582 

583 
val (expr, (params, fors)) = parameters thy (apfst (prep_expr thy) imprt); 

584 
val ctxt = context > 

585 
ProofContext.add_fixes (map (fn (b, mx) => (b, NONE, mx)) params) > snd > 

586 
ProofContext.add_fixes fors > snd; 

587 
in 

588 
case expr of 

589 
Expr [] => let 

590 
val ((parms, elems, concl), (spec, (_, _, defs))) = prep_elems do_close 

591 
context elements raw_concl; 

592 
val ((elems', _), ctxt') = 

593 
activate_elems prep_facts elems (ProofContext.set_stmt true ctxt); 

594 
in 

595 
(((ctxt', elems'), (parms, spec, defs)), concl) 

596 
end 

597 
(* 

598 
 Expr [(name, insts)] => let 

599 
val parms = parameters_of thy name > map (fn (b, SOME T, _) => (Name.name_of b, T)); 

600 
val (morph, ctxt') = read_inst parms insts context; 

601 
in 

602 

603 
end 

604 
*) 

605 
end 

606 

607 
in 

608 

609 
fun read_context imprt body ctxt = 

610 
#1 (prep_context_statement intern_expr read_elems read_facts true imprt body [] ctxt); 

611 
(* 

612 
fun cert_context imprt body ctxt = 

613 
#1 (prep_context_statement (K I) cert_elems cert_facts true imprt body [] ctxt); 

614 
*) 

615 
end; 

616 

617 

618 
(** Dependencies **) 

619 

620 

621 

622 
(*** Locale declarations ***) 

623 

624 
local 

625 

626 
(* introN: name of theorems for introduction rules of locale and 

627 
delta predicates; 

628 
axiomsN: name of theorem set with destruct rules for locale predicates, 

629 
also name suffix of delta predicates. *) 

630 

631 
val introN = "intro"; 

632 
val axiomsN = "axioms"; 

633 

634 
fun atomize_spec thy ts = 

635 
let 

636 
val t = Logic.mk_conjunction_balanced ts; 

637 
val body = ObjectLogic.atomize_term thy t; 

638 
val bodyT = Term.fastype_of body; 

639 
in 

640 
if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t)) 

641 
else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t)) 

642 
end; 

643 

644 
(* achieve plain syntax for locale predicates (without "PROP") *) 

645 

646 
fun aprop_tr' n c = (Syntax.constN ^ c, fn ctxt => fn args => 

647 
if length args = n then 

648 
Syntax.const "_aprop" $ 

649 
Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args) 

650 
else raise Match); 

651 

652 
(* CB: define one predicate including its intro rule and axioms 

653 
 bname: predicate name 

654 
 parms: locale parameters 

655 
 defs: thms representing substitutions from defines elements 

656 
 ts: terms representing locale assumptions (not normalised wrt. defs) 

657 
 norm_ts: terms representing locale assumptions (normalised wrt. defs) 

658 
 thy: the theory 

659 
*) 

660 

661 
fun def_pred bname parms defs ts norm_ts thy = 

662 
let 

663 
val name = Sign.full_name thy bname; 

664 

665 
val (body, bodyT, body_eq) = atomize_spec thy norm_ts; 

666 
val env = Term.add_term_free_names (body, []); 

667 
val xs = filter (member (op =) env o #1) parms; 

668 
val Ts = map #2 xs; 

669 
val extraTs = (Term.term_tfrees body \\ fold Term.add_tfreesT Ts []) 

670 
> Library.sort_wrt #1 > map TFree; 

671 
val predT = map Term.itselfT extraTs > Ts > bodyT; 

672 

673 
val args = map Logic.mk_type extraTs @ map Free xs; 

674 
val head = Term.list_comb (Const (name, predT), args); 

675 
val statement = ObjectLogic.ensure_propT thy head; 

676 

677 
val ([pred_def], defs_thy) = 

678 
thy 

679 
> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], []) 

680 
> Sign.declare_const [] ((Name.binding bname, predT), NoSyn) > snd 

681 
> PureThy.add_defs false 

682 
[((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])]; 

683 
val defs_ctxt = ProofContext.init defs_thy > Variable.declare_term head; 

684 

685 
val cert = Thm.cterm_of defs_thy; 

686 

687 
val intro = Goal.prove_global defs_thy [] norm_ts statement (fn _ => 

688 
MetaSimplifier.rewrite_goals_tac [pred_def] THEN 

689 
Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN 

690 
Tactic.compose_tac (false, 

691 
Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1); 

692 

693 
val conjuncts = 

694 
(Drule.equal_elim_rule2 OF [body_eq, 

695 
MetaSimplifier.rewrite_rule [pred_def] (Thm.assume (cert statement))]) 

696 
> Conjunction.elim_balanced (length ts); 

697 
val axioms = ts ~~ conjuncts > map (fn (t, ax) => 

698 
Element.prove_witness defs_ctxt t 

699 
(MetaSimplifier.rewrite_goals_tac defs THEN 

700 
Tactic.compose_tac (false, ax, 0) 1)); 

701 
in ((statement, intro, axioms), defs_thy) end; 

702 

703 
in 

704 

705 
(* CB: main predicate definition function *) 

706 

707 
fun define_preds pname (parms, ((exts, exts'), (ints, ints')), defs) thy = 

708 
let 

709 
val (a_pred, a_intro, a_axioms, thy'') = 

710 
if null exts then (NONE, NONE, [], thy) 

711 
else 

712 
let 

713 
val aname = if null ints then pname else pname ^ "_" ^ axiomsN; 

714 
val ((statement, intro, axioms), thy') = 

715 
thy 

716 
> def_pred aname parms defs exts exts'; 

717 
val (_, thy'') = 

718 
thy' 

719 
> Sign.add_path aname 

720 
> Sign.no_base_names 

721 
> PureThy.note_thmss Thm.internalK [((Name.binding introN, []), [([intro], [])])] 

722 
> Sign.restore_naming thy'; 

723 
in (SOME statement, SOME intro, axioms, thy'') end; 

724 
val (b_pred, b_intro, b_axioms, thy'''') = 

725 
if null ints then (NONE, NONE, [], thy'') 

726 
else 

727 
let 

728 
val ((statement, intro, axioms), thy''') = 

729 
thy'' 

730 
> def_pred pname parms defs (ints @ the_list a_pred) (ints' @ the_list a_pred); 

731 
val (_, thy'''') = 

732 
thy''' 

733 
> Sign.add_path pname 

734 
> Sign.no_base_names 

735 
> PureThy.note_thmss Thm.internalK 

736 
[((Name.binding introN, []), [([intro], [])]), 

737 
((Name.binding axiomsN, []), 

738 
[(map (Drule.standard o Element.conclude_witness) axioms, [])])] 

739 
> Sign.restore_naming thy'''; 

740 
in (SOME statement, SOME intro, axioms, thy'''') end; 

741 
in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end; 

742 

743 
end; 

744 

745 

746 
local 

747 

748 
fun assumes_to_notes (Assumes asms) axms = 

749 
fold_map (fn (a, spec) => fn axs => 

750 
let val (ps, qs) = chop (length spec) axs 

751 
in ((a, [(ps, [])]), qs) end) asms axms 

752 
> apfst (curry Notes Thm.assumptionK) 

753 
 assumes_to_notes e axms = (e, axms); 

754 

755 
fun defines_to_notes thy (Defines defs) defns = 

756 
let 

757 
val defs' = map (fn (_, (def, _)) => def) defs 

758 
val notes = map (fn (a, (def, _)) => 

759 
(a, [([assume (cterm_of thy def)], [])])) defs 

760 
in 

761 
(Notes (Thm.definitionK, notes), defns @ defs') 

762 
end 

763 
 defines_to_notes _ e defns = (e, defns); 

764 

765 
fun gen_add_locale prep_ctxt 

766 
bname predicate_name raw_imprt raw_body thy = 

767 
let 

768 
val thy_ctxt = ProofContext.init thy; 

769 
val name = Sign.full_name thy bname; 

770 
val _ = NewLocale.test_locale thy name andalso 

771 
error ("Duplicate definition of locale " ^ quote name); 

772 

773 
val ((body_ctxt, body_elems), text as (parms, ((_, exts'), _), defs)) = 

774 
prep_ctxt raw_imprt raw_body thy_ctxt; 

775 
val ((statement, intro, axioms), _, thy') = 

776 
define_preds predicate_name text thy; 

777 

778 
val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) []; 

779 
val _ = if null extraTs then () 

780 
else warning ("Additional type variable(s) in locale specification " ^ quote bname); 

781 

782 
val params = body_elems > 

783 
map_filter (fn Fixes fixes => SOME fixes  _ => NONE) > flat; 

784 

785 
val (body_elems', defns) = fold_map (defines_to_notes thy) body_elems []; 

786 

787 
val notes = body_elems' > 

788 
(fn elems => fold_map assumes_to_notes elems (map Element.conclude_witness axioms)) > 

789 
fst > 

790 
map_filter (fn Notes notes => SOME notes  _ => NONE); 

791 

792 
val loc_ctxt = thy' > 

793 
NewLocale.register_locale name (extraTs, params) (statement, defns) ([], []) 

794 
(map (fn n => (n, stamp ())) notes > rev) [] > 

795 
NewLocale.init name 

796 
in (name, loc_ctxt) end; 

797 

798 
in 

799 

800 
val add_locale = gen_add_locale read_context; 

801 
(* val add_locale_i = gen_add_locale cert_context; *) 

802 

803 
end; 

804 

805 
end; 