author  haftmann 
Fri, 26 Nov 2010 22:33:21 +0100  
changeset 40726  16dcfedc4eb7 
parent 40711  81bc73585eec 
child 41099  5cf62cefbbb4 
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 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

26 
val dynamic_holds_conv: conv 
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"; 
28054  50 

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

51 
datatype truth = Holds; 
39422  52 

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

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

54 
(Code_Target.extend_target (target, (Code_ML.target_SML, K I)) 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

55 
#> Code_Target.add_tyco_syntax target @{type_name prop} 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

56 
(SOME (0, (K o K o K) (Code_Printer.str s_truth))) 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

57 
#> Code_Target.add_const_syntax target @{const_name Code_Generator.holds} 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

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

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

60 
#> 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

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

62 

40150  63 
val trace = Unsynchronized.ref false; 
64 

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

65 
fun exec verbose code = 
40150  66 
(if ! trace then tracing code else (); 
40257  67 
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

68 

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

69 
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

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

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

72 
^ "\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

73 
^ " (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

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

75 
> 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

76 
> 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

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

78 

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

79 

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

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

81 

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

82 
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

83 

39605  84 
fun reject_vars thy t = 
85 
let 

86 
val ctxt = ProofContext.init_global thy; 

87 
in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end; 

88 

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

89 
fun obtain_serializer thy some_target = Code_Target.produce_code_for thy 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

90 
(the_default target some_target) NONE "Code" []; 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

91 

39537  92 
fun base_evaluator cookie serializer (naming : Code_Thingol.naming) thy program ((vs, ty), t) deps args = 
39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

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

94 
val ctxt = ProofContext.init_global thy; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

95 
val _ = if Code_Thingol.contains_dictvar t then 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

96 
error "Term to be evaluated contains free dictionaries" else (); 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

97 
val v' = Name.variant (map fst vs) "a"; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

98 
val vs' = (v', []) :: vs 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

99 
val ty' = Code_Thingol.fun_tyco `%% [ITyVar v', ty]; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

100 
val value_name = "Value.value.value" 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

101 
val program' = program 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

102 
> Graph.new_node (value_name, 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

103 
Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE))) 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

104 
> fold (curry Graph.add_edge value_name) deps; 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

105 
val (program_code, [SOME value_name']) = serializer naming program' [value_name]; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

106 
val value_code = space_implode " " 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

107 
(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

108 
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

109 

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

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

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

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

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

114 

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

115 
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

116 
let 
39605  117 
val _ = reject_vars thy t; 
39482  118 
fun evaluator naming program ((_, vs_ty), t) deps = 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

119 
base_evaluator cookie (obtain_serializer thy some_target) naming thy program (vs_ty, t) deps args; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

120 
in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end; 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

121 

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

122 
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

123 
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

124 

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

125 
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

126 
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

127 

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

128 
fun static_value_exn cookie thy some_target postproc consts = 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

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

130 
val serializer = obtain_serializer thy some_target; 
39482  131 
fun evaluator naming program thy ((_, vs_ty), t) deps = 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

132 
base_evaluator cookie serializer naming thy program (vs_ty, t) deps []; 
39605  133 
in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator o reject_vars thy end; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

134 

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

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

136 
Exn.release (static_value_exn cookie thy some_target postproc consts t); 
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 
fun static_value cookie thy some_target postproc consts t = 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

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

140 

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

141 

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

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

143 

39820  144 
structure Truth_Result = Proof_Data 
145 
( 

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

146 
type T = unit > truth 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

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

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

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

150 
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

151 

39605  152 
val reject_vars = fn thy => tap (reject_vars thy o Thm.term_of); 
153 

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

154 
fun check_holds serializer naming thy program vs_t deps 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)); 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

161 
val result = case partiality_as_none (base_evaluator truth_cookie serializer naming thy program vs_t deps []) 
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 
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

169 
(Thm.add_oracle (Binding.name "holds_by_evaluation", 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

170 
fn (serializer, naming, thy, program, vs_t, deps, ct) => check_holds serializer naming thy program vs_t deps ct))); 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

171 

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

172 
fun check_holds_oracle serializer naming thy program ((_, vs_ty), t) deps ct = 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

173 
raw_check_holds_oracle (serializer, naming, thy, program, (vs_ty, t), deps, ct); 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

174 

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

175 
val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy 
39605  176 
(fn naming => check_holds_oracle (obtain_serializer thy NONE) naming thy) 
177 
o reject_vars thy); 

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

178 

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

179 
fun static_holds_conv thy consts = 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

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

181 
val serializer = obtain_serializer thy NONE; 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

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

183 
Code_Thingol.static_eval_conv thy consts 
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

184 
(fn naming => fn program => fn thy => check_holds_oracle serializer naming thy program) 
39605  185 
o reject_vars thy 
39485
f7270a5e2550
closures preserve static serializer context for static evaluation; tuned
haftmann
parents:
39482
diff
changeset

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

187 

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 
(** instrumentalization **) 
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

190 

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

191 
fun evaluation_code thy module_name tycos consts = 
33992  192 
let 
36271
2ef9dbddfcb8
optionally ignore errors during translation of equations
haftmann
parents:
35360
diff
changeset

193 
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

194 
val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; 
38921  195 
val (ml_code, target_names) = Code_Target.produce_code_for thy 
38933
bd77e092f67c
avoid strange special treatment of empty module names
haftmann
parents:
38931
diff
changeset

196 
target NONE module_name [] naming program (consts' @ tycos'); 
34028
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

197 
val (consts'', tycos'') = chop (length consts') target_names; 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

198 
val consts_map = map2 (fn const => fn NONE => 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

199 
error ("Constant " ^ (quote o Code.string_of_const thy) const 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

200 
^ "\nhas a userdefined serialization") 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

201 
 SOME const'' => (const, const'')) consts consts'' 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

202 
val tycos_map = map2 (fn tyco => fn NONE => 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

203 
error ("Type " ^ (quote o Sign.extern_type thy) tyco 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

204 
^ "\nhas a userdefined serialization") 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

205 
 SOME tyco'' => (tyco, tyco'')) tycos tycos''; 
1e6206763036
split off evaluation mechanisms in separte module Code_Eval
haftmann
parents:
33992
diff
changeset

206 
in (ml_code, (tycos_map, consts_map)) end; 
28054  207 

208 

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

209 
(* by antiquotation *) 
28054  210 

211 
local 

212 

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

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

215 
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

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

217 
fun init _ = (([], []), (true, (Lazy.value ("", [])))); 
28054  218 
); 
219 

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

220 
val is_first_occ = fst o snd o Code_Antiq_Data.get; 
28054  221 

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

224 
val ((tycos, consts), _) = Code_Antiq_Data.get ctxt; 
30962  225 
val tycos' = fold (insert (op =)) new_tycos tycos; 
226 
val consts' = fold (insert (op =)) new_consts consts; 

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

227 
val acc_code = Lazy.lazy (fn () => 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

228 
evaluation_code (ProofContext.theory_of ctxt) "Code" tycos' consts' 
40422
d425d1ed82af
corrected slip: must keep constant map, not type map; tuned code
haftmann
parents:
40421
diff
changeset

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

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

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

28054  233 

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

234 
fun print_const const all_struct_name consts_map = 
30962  235 
(Long_Name.append all_struct_name o the o AList.lookup (op =) consts_map) const; 
236 

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

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

239 
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

240 
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

241 
val ml_code = if is_first then ml_code else ""; 
38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

242 
val all_struct_name = "Isabelle"; 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

243 
in (ml_code, print_const const all_struct_name consts_map) end; 
28054  244 

245 
in 

246 

35019
1ec0a3ff229e
simplified interface for ML antiquotations, struct_name is always "Isabelle";
wenzelm
parents:
34032
diff
changeset

247 
fun ml_code_antiq raw_const background = 
28054  248 
let 
31156  249 
val const = Code.check_const (ProofContext.theory_of background) raw_const; 
28054  250 
val is_first = is_first_occ background; 
251 
val background' = register_const const background; 

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

252 
in (print_code is_first const, background') end; 
30962  253 

28054  254 
end; (*local*) 
255 

256 

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

257 
(* reflection support *) 
36470  258 

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

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

261 
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

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

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

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

265 
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

266 
val _ = if null missing_constrs then [] 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

267 
else error ("Missing constructor(s) " ^ commas (map quote missing_constrs) 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

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

269 
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

270 
val _ = if null false_constrs then [] 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

271 
else error ("Nonconstructor(s) " ^ commas (map quote false_constrs) 
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

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

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

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

275 
in (tyco, constrs) end; 
36470  276 

277 
fun add_eval_tyco (tyco, tyco') thy = 

278 
let 

279 
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

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

281 
 pr pr' _ [ty] = 
36470  282 
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

283 
 pr pr' _ tys = 
36470  284 
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] 
285 
in 

286 
thy 

38923  287 
> Code_Target.add_tyco_syntax target tyco (SOME (k, pr)) 
36470  288 
end; 
289 

36514  290 
fun add_eval_constr (const, const') thy = 
291 
let 

292 
val k = Code.args_number thy const; 

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

38922  294 
(const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts))); 
36514  295 
in 
296 
thy 

38923  297 
> Code_Target.add_const_syntax target const (SOME (Code_Printer.simple_const_syntax (k, pr))) 
36514  298 
end; 
299 

38923  300 
fun add_eval_const (const, const') = Code_Target.add_const_syntax target 
36470  301 
const (SOME (Code_Printer.simple_const_syntax (0, (K o K o K) const'))); 
302 

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

303 
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

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

305 
> 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

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

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

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

309 
> 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

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

312 
val preamble = 
bc285d91041e
moved basic thy file name operations from Thy_Load to Thy_Header;
wenzelm
parents:
37744
diff
changeset

313 
"(* Generated from " ^ Path.implode (Thy_Header.thy_path (Context.theory_name thy)) 
36470  314 
^ "; DO NOT EDIT! *)"; 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

315 
val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code); 
36470  316 
in 
317 
thy 

318 
end; 

319 

320 
fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy = 

321 
let 

322 
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

323 
(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

324 
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

325 
> apsnd flat; 
36470  326 
val functions = map (prep_const thy) raw_functions; 
36514  327 
val result = evaluation_code thy module_name tycos (constrs @ functions) 
328 
> (apsnd o apsnd) (chop (length constrs)); 

36470  329 
in 
330 
thy 

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

331 
> process_reflection result module_name some_file 
36470  332 
end; 
333 

39422  334 
val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I); 
36470  335 
val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const; 
336 

337 

28054  338 
(** Isar setup **) 
339 

340 
val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq); 

341 

36470  342 
local 
343 

344 
val datatypesK = "datatypes"; 

345 
val functionsK = "functions"; 

346 
val fileK = "file"; 

347 
val andK = "and" 

348 

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

349 
val _ = List.app Keyword.keyword [datatypesK, functionsK]; 
36470  350 

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

351 
val parse_datatype = 
40711
81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents:
40422
diff
changeset

352 
Parse.name  Parse.$$$ "="  
81bc73585eec
globbing constant expressions use more idiomatic underscore rather than star
haftmann
parents:
40422
diff
changeset

353 
(((Parse.sym_ident  Parse.string) >> (fn "_" => NONE  _ => Scan.fail ())) 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

354 
 ((Parse.term ::: (Scan.repeat (Parse.$$$ ""  Parse.term))) >> SOME)); 
36470  355 

356 
in 

357 

358 
val _ = 

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

359 
Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code" 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

360 
Keyword.thy_decl (Parse.name  Scan.optional (Parse.$$$ datatypesK  (parse_datatype 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

361 
::: Scan.repeat (Parse.$$$ andK  parse_datatype))) [] 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

362 
 Scan.optional (Parse.$$$ functionsK  Scan.repeat1 Parse.name) [] 
01594f816e3a
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents:
36610
diff
changeset

363 
 Scan.option (Parse.$$$ fileK  Parse.name) 
36534  364 
>> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory 
36470  365 
(code_reflect_cmd raw_datatypes raw_functions module_name some_file))); 
366 

367 
end; (*local*) 

368 

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

369 

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

370 
(** 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

371 

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

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

373 

39820  374 
structure Loaded_Values = Theory_Data 
375 
( 

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

376 
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

377 
val empty = [] 
39820  378 
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

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

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

381 

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

382 
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

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

384 
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

385 
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

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

387 

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

388 
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

389 

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

390 
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

391 
{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

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

393 
{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

394 
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

395 
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

396 
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

397 
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

398 
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

399 
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

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

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

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

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

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

405 
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

406 
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

407 
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

408 
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

409 
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

410 
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

411 
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

412 
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

413 
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

414 

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

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

416 

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

417 
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

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

419 
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

420 
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

421 
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

422 
(0, Path.implode filepath) false (File.read filepath); 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

423 
val thy'' = (Context.the_theory o the) (Context.thread_data ()); 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

424 
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

425 
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

426 

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

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

428 

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

429 
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

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

431 
> 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

432 
> 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

433 
> (fn ([Const (const, _)], _) => 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

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

435 
(SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name))) 
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

436 
#> tap (fn thy => Code_Target.produce_code thy [const] target NONE "Code" [])); 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

437 

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

438 
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

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

440 
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

441 
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

442 
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

443 
else error ("Value binding(s) " ^ commas_quote superfluous 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

444 
^ " found in external file " ^ quote (Path.implode filepath) 
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

445 
^ " 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

446 
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

447 
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

448 
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

449 
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

450 

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

451 
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

452 
let 
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 = 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

454 
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

455 
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

456 
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

457 
^ " 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

458 
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

459 

28054  460 
end; (*struct*) 