author  wenzelm 
Fri, 23 Aug 2013 19:53:27 +0200  
changeset 53169  e2d31807cbf6 
parent 52435  6646bb548c6b 
child 53171  a5e54d4d9081 
permissions  rwrr 
39401  1 
(* Title: Tools/Code/code_runtime.ML 
28054  2 
Author: Florian Haftmann, TU Muenchen 
3 

34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

4 
Runtime services building on code generation into implementation language SML. 
28054  5 
*) 
6 

39401  7 
signature CODE_RUNTIME = 
28054  8 
sig 
34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

9 
val target: string 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

10 
val value: Proof.context > 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

11 
(Proof.context > unit > 'a) * ((unit > 'a) > Proof.context > Proof.context) * string > 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

12 
string * string > 'a 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

13 
type 'a cookie = (Proof.context > unit > 'a) * ((unit > 'a) > Proof.context > Proof.context) * string 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

14 
val dynamic_value: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

15 
> ((term > term) > 'a > 'a) > term > string list > 'a option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

16 
val dynamic_value_strict: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

17 
> ((term > term) > 'a > 'a) > term > string list > 'a 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

18 
val dynamic_value_exn: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

19 
> ((term > term) > 'a > 'a) > term > string list > 'a Exn.result 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

20 
val static_value: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

21 
> ((term > term) > 'a > 'a) > string list > term > 'a option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

22 
val static_value_strict: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

23 
> ((term > term) > 'a > 'a) > string list > term > 'a 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

24 
val static_value_exn: 'a cookie > theory > string option 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

25 
> ((term > term) > 'a > 'a) > string list > term > 'a Exn.result 
41247  26 
val dynamic_holds_conv: theory > conv 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

27 
val static_holds_conv: theory > string list > conv 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

28 
val code_reflect: (string * string list option) list > string list > string 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

29 
> string option > theory > theory 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

30 
datatype truth = Holds 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

31 
val put_truth: (unit > truth) > Proof.context > Proof.context 
40150  32 
val trace: bool Unsynchronized.ref 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

33 
val polyml_as_definition: (binding * typ) list > Path.T list > theory > theory 
28054  34 
end; 
35 

39401  36 
structure Code_Runtime : CODE_RUNTIME = 
28054  37 
struct 
38 

39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

39 
open Basic_Code_Thingol; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

40 

39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

41 
(** evaluation **) 
33992  42 

39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

43 
(* technical prerequisites *) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

44 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

45 
val this = "Code_Runtime"; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

46 
val s_truth = Long_Name.append this "truth"; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

47 
val s_Holds = Long_Name.append this "Holds"; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

48 

34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

49 
val target = "Eval"; 
44663  50 
val structure_generated = "Generated_Code"; 
28054  51 

39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

52 
datatype truth = Holds; 
39422  53 

39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

54 
val _ = Context.>> (Context.map_theory 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

55 
(Code_Target.extend_target (target, (Code_ML.target_SML, K I)) 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

56 
#> Code_Target.set_printings (Code_Symbol.Type_Constructor (@{type_name prop}, 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

57 
[(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))])) 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

58 
#> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Code_Generator.holds}, 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

59 
[(target, SOME (Code_Printer.plain_const_syntax s_Holds))])) 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

60 
#> Code_Target.add_reserved target this 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

61 
#> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"])); 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

62 
(*avoid further pervasive infix names*) 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

63 

40150  64 
val trace = Unsynchronized.ref false; 
65 

39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

66 
fun exec verbose code = 
40150  67 
(if ! trace then tracing code else (); 
40257  68 
ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)); 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

69 

2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

70 
fun value ctxt (get, put, put_ml) (prelude, value) = 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

71 
let 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

72 
val code = (prelude 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

73 
^ "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

74 
^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))"); 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

75 
val ctxt' = ctxt 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

76 
> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

77 
> Context.proof_map (exec false code); 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

78 
in get ctxt' () end; 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

79 

39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

80 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

81 
(* evaluation into target language values *) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

82 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

83 
type 'a cookie = (Proof.context > unit > 'a) * ((unit > 'a) > Proof.context > Proof.context) * string; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

84 

39605  85 
fun reject_vars thy t = 
86 
let 

42361  87 
val ctxt = Proof_Context.init_global thy; 
39605  88 
in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end; 
89 

48568  90 
fun obtain_evaluator thy some_target naming program consts expr = 
91 
Code_Target.evaluator thy (the_default target some_target) naming program consts expr 

92 
> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules)); 

39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

93 

41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

94 
fun evaluation cookie thy evaluator vs_t args = 
39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

95 
let 
42361  96 
val ctxt = Proof_Context.init_global thy; 
41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

97 
val (program_code, value_name) = evaluator vs_t; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

98 
val value_code = space_implode " " 
41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

99 
(value_name :: "()" :: map (enclose "(" ")") args); 
40235
87998864284e
use Exn.interruptible_capture to keep usercode interruptible (Exn.capture not immediately followed by Exn.release here);
wenzelm
parents:
40150
diff
changeset

100 
in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

101 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

102 
fun partiality_as_none e = SOME (Exn.release e) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

103 
handle General.Match => NONE 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

104 
 General.Bind => NONE 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

105 
 General.Fail _ => NONE; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

106 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

107 
fun dynamic_value_exn cookie thy some_target postproc t args = 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

108 
let 
39605  109 
val _ = reject_vars thy t; 
41099  110 
val _ = if ! trace 
111 
then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term_global thy t)) 

112 
else () 

39482  113 
fun evaluator naming program ((_, vs_ty), t) deps = 
41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

114 
evaluation cookie thy (obtain_evaluator thy some_target naming program deps) (vs_ty, t) args; 
41184  115 
in Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t end; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

116 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

117 
fun dynamic_value_strict cookie thy some_target postproc t args = 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

118 
Exn.release (dynamic_value_exn cookie thy some_target postproc t args); 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

119 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

120 
fun dynamic_value cookie thy some_target postproc t args = 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

121 
partiality_as_none (dynamic_value_exn cookie thy some_target postproc t args); 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

122 

41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

123 
fun static_evaluator cookie thy some_target naming program consts' = 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

124 
let 
41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

125 
val evaluator = obtain_evaluator thy some_target naming program consts' 
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

126 
in fn ((_, vs_ty), t) => fn _ => evaluation cookie thy evaluator (vs_ty, t) [] end; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

127 

41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

128 
fun static_value_exn cookie thy some_target postproc consts = 
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

129 
Code_Thingol.static_value thy (Exn.map_result o postproc) consts 
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

130 
(static_evaluator cookie thy some_target) o reject_vars thy; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

131 

41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

132 
fun static_value_strict cookie thy some_target postproc consts = 
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

133 
Exn.release o static_value_exn cookie thy some_target postproc consts; 
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

134 

064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

135 
fun static_value cookie thy some_target postproc consts = 
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

136 
partiality_as_none o static_value_exn cookie thy some_target postproc consts; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

137 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

138 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

139 
(* evaluation for truth or nothing *) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

140 

39820  141 
structure Truth_Result = Proof_Data 
142 
( 

39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

143 
type T = unit > truth 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41376
diff
changeset

144 
(* FIXME avoid user error with nonuser text *) 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

145 
fun init _ () = error "Truth_Result" 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

146 
); 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

147 
val put_truth = Truth_Result.put; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

148 
val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth"); 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

149 

39605  150 
val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of); 
151 

41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

152 
local 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

153 

47609  154 
fun check_holds thy evaluator vs_t ct = 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

155 
let 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

156 
val t = Thm.term_of ct; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

157 
val _ = if fastype_of t <> propT 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

158 
then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

159 
else (); 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

160 
val iff = Thm.cterm_of thy (Term.Const ("==", propT > propT > propT)); 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

161 
val result = case partiality_as_none (evaluation truth_cookie thy evaluator vs_t []) 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

162 
of SOME Holds => true 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

163 
 _ => false; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

164 
in 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

165 
Thm.mk_binop iff ct (if result then @{cprop "PROP Code_Generator.holds"} else ct) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

166 
end; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

167 

33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

168 
val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result 
43619
3803869014aa
proper @{binding} antiquotations (relevant for formal references);
wenzelm
parents:
43560
diff
changeset

169 
(Thm.add_oracle (@{binding holds_by_evaluation}, 
47609  170 
fn (thy, evaluator, vs_t, ct) => check_holds thy evaluator vs_t ct))); 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

171 

41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

172 
fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct = 
47609  173 
raw_check_holds_oracle (thy, evaluator, (vs_ty, t), ct); 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

174 

0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

175 
in 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

176 

41247  177 
fun dynamic_holds_conv thy = Code_Thingol.dynamic_conv thy 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

178 
(fn naming => fn program => fn vs_t => fn deps => 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

179 
check_holds_oracle thy (obtain_evaluator thy NONE naming program deps) vs_t deps) 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

180 
o reject_vars thy; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

181 

41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

182 
fun static_holds_conv thy consts = Code_Thingol.static_conv thy consts 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

183 
(fn naming => fn program => fn consts' => 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

184 
check_holds_oracle thy (obtain_evaluator thy NONE naming program consts')) 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

185 
o reject_vars thy; 
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

186 

0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

187 
end; (*local*) 
39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

188 

a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

189 

a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

190 
(** instrumentalization **) 
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

191 

38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

192 
fun evaluation_code thy module_name tycos consts = 
33992  193 
let 
42361  194 
val ctxt = Proof_Context.init_global thy; 
36271
2ef9dbddfcb8
optionally ignore errors during translation of equations
haftmann
parents:
35360
diff
changeset

195 
val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts; 
34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

196 
val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; 
48568  197 
val (ml_modules, target_names) = 
42359  198 
Code_Target.produce_code_for thy 
199 
target NONE module_name [] naming program (consts' @ tycos'); 

48568  200 
val ml_code = space_implode "\n\n" (map snd ml_modules); 
34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

201 
val (consts'', tycos'') = chop (length consts') target_names; 
42359  202 
val consts_map = map2 (fn const => 
203 
fn NONE => 

204 
error ("Constant " ^ (quote o Code.string_of_const thy) const ^ 

205 
"\nhas a userdefined serialization") 

206 
 SOME const'' => (const, const'')) consts consts'' 

207 
val tycos_map = map2 (fn tyco => 

208 
fn NONE => 

42361  209 
error ("Type " ^ quote (Proof_Context.extern_type ctxt tyco) ^ 
42359  210 
"\nhas a userdefined serialization") 
211 
 SOME tyco'' => (tyco, tyco'')) tycos tycos''; 

34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

212 
in (ml_code, (tycos_map, consts_map)) end; 
28054  213 

214 

39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

215 
(* by antiquotation *) 
28054  216 

217 
local 

218 

38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

219 
structure Code_Antiq_Data = Proof_Data 
28054  220 
( 
38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

221 
type T = (string list * string list) * (bool 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

222 
* (string * (string * string) list) lazy); 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

223 
fun init _ = (([], []), (true, (Lazy.value ("", [])))); 
28054  224 
); 
225 

38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

226 
val is_first_occ = fst o snd o Code_Antiq_Data.get; 
28054  227 

30962  228 
fun register_code new_tycos new_consts ctxt = 
28054  229 
let 
38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

230 
val ((tycos, consts), _) = Code_Antiq_Data.get ctxt; 
30962  231 
val tycos' = fold (insert (op =)) new_tycos tycos; 
232 
val consts' = fold (insert (op =)) new_consts consts; 

38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

233 
val acc_code = Lazy.lazy (fn () => 
44663  234 
evaluation_code (Proof_Context.theory_of ctxt) structure_generated tycos' consts' 
40422
d425d1ed82af
corrected slip: must keep constant map, not type map; tuned code
haftmann
parents:
40421
diff
changeset

235 
> apsnd snd); 
38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

236 
in Code_Antiq_Data.put ((tycos', consts'), (false, acc_code)) ctxt end; 
30962  237 

238 
fun register_const const = register_code [] [const]; 

28054  239 

40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

240 
fun print_code is_first const ctxt = 
30962  241 
let 
38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

242 
val (_, (_, acc_code)) = Code_Antiq_Data.get ctxt; 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

243 
val (ml_code, consts_map) = Lazy.force acc_code; 
40422
d425d1ed82af
corrected slip: must keep constant map, not type map; tuned code
haftmann
parents:
40421
diff
changeset

244 
val ml_code = if is_first then ml_code else ""; 
41486
82c1e348bc18
reverted 08240feb69c7  breaks positions of reports;
wenzelm
parents:
41472
diff
changeset

245 
val body = "Isabelle." ^ the (AList.lookup (op =) consts_map const); 
41376
08240feb69c7
more robust ML antiquotations  allow original tokens without adjacent whitespace;
wenzelm
parents:
41349
diff
changeset

246 
in (ml_code, body) end; 
28054  247 

248 
in 

249 

53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

250 
fun ml_code_antiq context raw_const = 
28054  251 
let 
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

252 
val ctxt = Context.the_proof context; 
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

253 
val thy = Proof_Context.theory_of ctxt; 
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

254 

e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

255 
val const = Code.check_const thy raw_const; 
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

256 
val is_first = is_first_occ ctxt; 
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

257 
val ctxt' = register_const const ctxt; 
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

258 
in (Context.Proof ctxt', print_code is_first const) end; 
30962  259 

28054  260 
end; (*local*) 
261 

262 

39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

263 
(* reflection support *) 
36470  264 

40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

265 
fun check_datatype thy tyco some_consts = 
36470  266 
let 
40726
16dcfedc4eb7
keep type variable arguments of datatype constructors in bookkeeping
haftmann
parents:
40711
diff
changeset

267 
val constrs = (map fst o snd o fst o Code.get_type thy) tyco; 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

268 
val _ = case some_consts 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

269 
of SOME consts => 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

270 
let 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

271 
val missing_constrs = subtract (op =) consts constrs; 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

272 
val _ = if null missing_constrs then [] 
45430  273 
else error ("Missing constructor(s) " ^ commas_quote missing_constrs 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

274 
^ " for datatype " ^ quote tyco); 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

275 
val false_constrs = subtract (op =) constrs consts; 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

276 
val _ = if null false_constrs then [] 
45430  277 
else error ("Nonconstructor(s) " ^ commas_quote false_constrs 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

278 
^ " for datatype " ^ quote tyco) 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

279 
in () end 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

280 
 NONE => (); 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

281 
in (tyco, constrs) end; 
36470  282 

283 
fun add_eval_tyco (tyco, tyco') thy = 

284 
let 

285 
val k = Sign.arity_number thy tyco; 

40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

286 
fun pr pr' _ [] = tyco' 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

287 
 pr pr' _ [ty] = 
36470  288 
Code_Printer.concat [pr' Code_Printer.BR ty, tyco'] 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

289 
 pr pr' _ tys = 
36470  290 
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] 
291 
in 

292 
thy 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

293 
> Code_Target.set_printings (Code_Symbol.Type_Constructor (tyco, [(target, SOME (k, pr))])) 
36470  294 
end; 
295 

36514  296 
fun add_eval_constr (const, const') thy = 
297 
let 

298 
val k = Code.args_number thy const; 

299 
fun pr pr' fxy ts = Code_Printer.brackify fxy 

38922  300 
(const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts))); 
36514  301 
in 
302 
thy 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

303 
> Code_Target.set_printings (Code_Symbol.Constant (const, 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

304 
[(target, SOME (Code_Printer.simple_const_syntax (k, pr)))])) 
36514  305 
end; 
306 

52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

307 
fun add_eval_const (const, const') = Code_Target.set_printings (Code_Symbol.Constant 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

308 
(const, [(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const')))])); 
36470  309 

39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

310 
fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy = 
38935
2cf3d8305b47
corrected misbehaved additional qualification of generated names
haftmann
parents:
38933
diff
changeset

311 
thy 
2cf3d8305b47
corrected misbehaved additional qualification of generated names
haftmann
parents:
38933
diff
changeset

312 
> Code_Target.add_reserved target module_name 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

313 
> Context.theory_map (exec true code) 
38935
2cf3d8305b47
corrected misbehaved additional qualification of generated names
haftmann
parents:
38933
diff
changeset

314 
> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map 
2cf3d8305b47
corrected misbehaved additional qualification of generated names
haftmann
parents:
38933
diff
changeset

315 
> fold (add_eval_constr o apsnd Code_Printer.str) constr_map 
2cf3d8305b47
corrected misbehaved additional qualification of generated names
haftmann
parents:
38933
diff
changeset

316 
> fold (add_eval_const o apsnd Code_Printer.str) const_map 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

317 
 process_reflection (code, _) _ (SOME file_name) thy = 
36470  318 
let 
37950
bc285d91041e
moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents:
37744
diff
changeset

319 
val preamble = 
46737  320 
"(* Generated from " ^ 
321 
Path.implode (Thy_Load.thy_path (Path.basic (Context.theory_name thy))) ^ 

322 
"; DO NOT EDIT! *)"; 

39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

323 
val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code); 
36470  324 
in 
325 
thy 

326 
end; 

327 

328 
fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy = 

329 
let 

330 
val datatypes = map (fn (raw_tyco, raw_cos) => 

40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

331 
(prep_type thy raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes; 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

332 
val (tycos, constrs) = map_split (uncurry (check_datatype thy)) datatypes 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

333 
> apsnd flat; 
36470  334 
val functions = map (prep_const thy) raw_functions; 
36514  335 
val result = evaluation_code thy module_name tycos (constrs @ functions) 
336 
> (apsnd o apsnd) (chop (length constrs)); 

36470  337 
in 
338 
thy 

39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

339 
> process_reflection result module_name some_file 
36470  340 
end; 
341 

39422  342 
val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I); 
36470  343 
val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const; 
344 

345 

28054  346 
(** Isar setup **) 
347 

43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

348 
val _ = 
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
42361
diff
changeset

349 
Context.>> (Context.map_theory 
53169
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

350 
(ML_Context.add_antiq @{binding code} 
e2d31807cbf6
clarified type ML_Context.antiq: context parser maintains compilation context, declaration is applied to final context;
wenzelm
parents:
52435
diff
changeset

351 
(Scan.depend (fn context => Scan.pass context Args.term >> ml_code_antiq context)))); 
28054  352 

36470  353 
local 
354 

36960
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

355 
val parse_datatype = 
46949  356 
Parse.name  @{keyword "="}  
40711
81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents:
40422
diff
changeset

357 
(((Parse.sym_ident  Parse.string) >> (fn "_" => NONE  _ => Scan.fail ())) 
46949  358 
 ((Parse.term ::: (Scan.repeat (@{keyword ""}  Parse.term))) >> SOME)); 
36470  359 

360 
in 

361 

362 
val _ = 

46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

363 
Outer_Syntax.command @{command_spec "code_reflect"} 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

364 
"enrich runtime environment with generated code" 
52434  365 
(Parse.name  Scan.optional (@{keyword "datatypes"}  Parse.!!! (parse_datatype 
46949  366 
::: Scan.repeat (@{keyword "and"}  parse_datatype))) [] 
52434  367 
 Scan.optional (@{keyword "functions"}  Parse.!!! (Scan.repeat1 Parse.name)) [] 
368 
 Scan.option (@{keyword "file"}  Parse.!!! Parse.name) 

46961
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

369 
>> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory 
5c6955f487e5
outer syntax command definitions based on formal command_spec derived from theory header declarations;
wenzelm
parents:
46949
diff
changeset

370 
(code_reflect_cmd raw_datatypes raw_functions module_name some_file))); 
36470  371 

372 
end; (*local*) 

373 

39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

374 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

375 
(** using external SML files as substitute for proper definitions  only for polyml! **) 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

376 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

377 
local 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

378 

39820  379 
structure Loaded_Values = Theory_Data 
380 
( 

39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

381 
type T = string list 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

382 
val empty = [] 
41472
f6ab14e61604
misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
wenzelm
parents:
41376
diff
changeset

383 
val extend = I 
39820  384 
fun merge data : T = Library.merge (op =) data 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

385 
); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

386 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

387 
fun notify_val (string, value) = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

388 
let 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

389 
val _ = #enterVal ML_Env.name_space (string, value); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

390 
val _ = Context.>> ((Context.map_theory o Loaded_Values.map) (insert (op =) string)); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

391 
in () end; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

392 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

393 
fun abort _ = error "Only value bindings allowed."; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

394 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

395 
val notifying_context : use_context = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

396 
{tune_source = #tune_source ML_Env.local_context, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

397 
name_space = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

398 
{lookupVal = #lookupVal ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

399 
lookupType = #lookupType ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

400 
lookupFix = #lookupFix ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

401 
lookupStruct = #lookupStruct ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

402 
lookupSig = #lookupSig ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

403 
lookupFunct = #lookupFunct ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

404 
enterVal = notify_val, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

405 
enterType = abort, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

406 
enterFix = abort, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

407 
enterStruct = abort, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

408 
enterSig = abort, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

409 
enterFunct = abort, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

410 
allVal = #allVal ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

411 
allType = #allType ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

412 
allFix = #allFix ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

413 
allStruct = #allStruct ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

414 
allSig = #allSig ML_Env.name_space, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

415 
allFunct = #allFunct ML_Env.name_space}, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

416 
str_of_pos = #str_of_pos ML_Env.local_context, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

417 
print = #print ML_Env.local_context, 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

418 
error = #error ML_Env.local_context}; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

419 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

420 
in 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

421 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

422 
fun use_file filepath thy = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

423 
let 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

424 
val thy' = Loaded_Values.put [] thy; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

425 
val _ = Context.set_thread_data ((SOME o Context.Theory) thy'); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

426 
val _ = Secure.use_text notifying_context 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

427 
(0, Path.implode filepath) false (File.read filepath); 
45268  428 
val thy'' = Context.the_theory (Context.the_thread_data ()); 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

429 
val names = Loaded_Values.get thy''; 
40320
abc52faa7761
polyml_as_definition does not require explicit dependencies on external ML files
haftmann
parents:
40257
diff
changeset

430 
in (names, thy'') end; 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

431 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

432 
end; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

433 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

434 
fun add_definiendum (ml_name, (b, T)) thy = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

435 
thy 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

436 
> Code_Target.add_reserved target ml_name 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

437 
> Specification.axiomatization [(b, SOME T, NoSyn)] [] 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

438 
> (fn ([Const (const, _)], _) => 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

439 
Code_Target.set_printings (Code_Symbol.Constant (const, 
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

440 
[(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))])) 
44663  441 
#> tap (fn thy => Code_Target.produce_code thy [const] target NONE structure_generated [])); 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

442 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

443 
fun process_file filepath (definienda, thy) = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

444 
let 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

445 
val (ml_names, thy') = use_file filepath thy; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

446 
val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

447 
val _ = if null superfluous then () 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

448 
else error ("Value binding(s) " ^ commas_quote superfluous 
41944
b97091ae583a
Path.print is the official way to show filesystem paths to users  note that Path.implode often indicates violation of the abstract datatype;
wenzelm
parents:
41486
diff
changeset

449 
^ " found in external file " ^ Path.print filepath 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

450 
^ " not present among the given contants binding(s)."); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

451 
val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

452 
val thy'' = fold add_definiendum these_definienda thy'; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

453 
val definienda' = fold (AList.delete (op =)) ml_names definienda; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

454 
in (definienda', thy'') end; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

455 

c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

456 
fun polyml_as_definition bTs filepaths thy = 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

457 
let 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

458 
val definienda = map (fn bT => ((Binding.name_of o fst) bT, bT)) bTs; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

459 
val (remaining, thy') = fold process_file filepaths (definienda, thy); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

460 
val _ = if null remaining then () 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

461 
else error ("Constant binding(s) " ^ commas_quote (map fst remaining) 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

462 
^ " not present in external file(s)."); 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

463 
in thy' end; 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

464 

28054  465 
end; (*struct*) 