author  haftmann 
Fri, 05 Dec 2014 19:35:36 +0100  
changeset 59104  a14475f044b2 
parent 58645  94bef115c08f 
child 59127  723b11f8ffbf 
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 
55757  14 
val dynamic_value: 'a cookie > Proof.context > string option 
39473
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 
55757  16 
val dynamic_value_strict: 'a cookie > Proof.context > string option 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

17 
> ((term > term) > 'a > 'a) > term > string list > 'a 
55757  18 
val dynamic_value_exn: 'a cookie > Proof.context > string option 
39473
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 
56973
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

20 
val static_value: 'a cookie > { ctxt: Proof.context, target: string option, 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

21 
lift_postproc: (term > term) > 'a > 'a, consts: string list } 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

22 
> Proof.context > term > 'a option 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

23 
val static_value_strict: 'a cookie > { ctxt: Proof.context, target: string option, 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

24 
lift_postproc: (term > term) > 'a > 'a, consts: string list } 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

25 
> Proof.context > term > 'a 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

26 
val static_value_exn: 'a cookie > { ctxt: Proof.context, target: string option, 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

27 
lift_postproc: (term > term) > 'a > 'a, consts: string list } 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

28 
> Proof.context > term > 'a Exn.result 
55757  29 
val dynamic_holds_conv: Proof.context > conv 
56973
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

30 
val static_holds_conv: { ctxt: Proof.context, consts: string list } > Proof.context > conv 
58643
133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

31 
val static_value': (Proof.context > term > 'a) cookie 
133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

32 
> { ctxt: Proof.context, lift_postproc: (term > term) > 'a > 'a, 
133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

33 
consts: (string * typ) list, T: typ } 
133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

34 
> Proof.context > term > 'a option (*EXPERIMENTAL!*) 
133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

35 
val static_value_strict': (Proof.context > term > 'a) cookie 
133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

36 
> { ctxt: Proof.context, lift_postproc: (term > term) > 'a > 'a, 
133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

37 
consts: (string * typ) list, T: typ } 
133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

38 
> Proof.context > term > 'a (*EXPERIMENTAL!*) 
58558
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

39 
val static_value_exn': (Proof.context > term > 'a) cookie 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

40 
> { ctxt: Proof.context, lift_postproc: (term > term) > 'a > 'a, 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

41 
consts: (string * typ) list, T: typ } 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

42 
> Proof.context > term > 'a Exn.result (*EXPERIMENTAL!*) 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

43 
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

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

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

46 
val put_truth: (unit > truth) > Proof.context > Proof.context 
57435  47 
val trace: bool Config.T 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

48 
val polyml_as_definition: (binding * typ) list > Path.T list > theory > theory 
28054  49 
end; 
50 

39401  51 
structure Code_Runtime : CODE_RUNTIME = 
28054  52 
struct 
53 

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

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

56 

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

57 
(** evaluation **) 
33992  58 

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

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

60 

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

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

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

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

64 

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

65 
val target = "Eval"; 
44663  66 
val structure_generated = "Generated_Code"; 
28054  67 

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

68 
datatype truth = Holds; 
39422  69 

53171  70 
val _ = Theory.setup 
59104  71 
(Code_Target.add_derived_target (target, [(Code_ML.target_SML, I)]) 
55150  72 
#> Code_Target.set_printings (Type_Constructor (@{type_name prop}, 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

73 
[(target, SOME (0, (K o K o K) (Code_Printer.str s_truth)))])) 
55150  74 
#> Code_Target.set_printings (Constant (@{const_name Code_Generator.holds}, 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

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

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

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

79 

57435  80 
val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false); 
40150  81 

57435  82 
fun exec ctxt verbose code = 
83 
(if Config.get ctxt trace then tracing code else (); 

40257  84 
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

85 

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

86 
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

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

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

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

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

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

92 
> put (fn () => error ("Bad evaluation for " ^ quote put_ml)) 
57435  93 
> Context.proof_map (exec ctxt false code); 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

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

95 

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

96 

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

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

98 

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

99 
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

100 

55757  101 
fun reject_vars ctxt t = 
102 
((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t); 

39605  103 

55757  104 
fun obtain_evaluator ctxt some_target program consts = 
105 
let 

106 
val evaluator' = Code_Target.evaluator ctxt (the_default target some_target) program consts false; 

107 
in 

108 
evaluator' 

109 
#> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules)) 

110 
end; 

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

111 

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

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

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

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

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

117 
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

118 

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

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

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

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

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

123 

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

125 
let 
55757  126 
val _ = reject_vars ctxt t; 
57435  127 
val _ = if Config.get ctxt trace 
55757  128 
then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t)) 
41099  129 
else () 
56920
d651b944c67e
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
haftmann
parents:
56618
diff
changeset

130 
fun evaluator program _ vs_ty_t deps = 
d651b944c67e
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
haftmann
parents:
56618
diff
changeset

131 
evaluation cookie ctxt (obtain_evaluator ctxt some_target program deps) vs_ty_t args; 
55757  132 
in Code_Thingol.dynamic_value ctxt (Exn.map_result o postproc) evaluator t end; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

133 

55757  134 
fun dynamic_value_strict cookie ctxt some_target postproc t args = 
135 
Exn.release (dynamic_value_exn cookie ctxt some_target postproc t args); 

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

136 

55757  137 
fun dynamic_value cookie ctxt some_target postproc t args = 
138 
partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args); 

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

139 

56973
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

140 
fun static_evaluator cookie ctxt some_target { program, deps } = 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

141 
let 
56973
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

142 
val evaluator = obtain_evaluator ctxt some_target program (map Constant deps); 
55757  143 
val evaluation' = evaluation cookie ctxt evaluator; 
56920
d651b944c67e
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
haftmann
parents:
56618
diff
changeset

144 
in fn _ => fn _ => fn vs_ty_t => fn _ => evaluation' vs_ty_t [] end; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

145 

56973
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

146 
fun static_value_exn cookie { ctxt, target, lift_postproc, consts } = 
55757  147 
let 
56973
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

148 
val evaluator = Code_Thingol.static_value { ctxt = ctxt, 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

149 
lift_postproc = Exn.map_result o lift_postproc, consts = consts } 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

150 
(static_evaluator cookie ctxt target); 
55757  151 
in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

152 

56973
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

153 
fun static_value_strict cookie = Exn.release ooo static_value_exn cookie; 
41347
064133cb4ef6
evaluator separating static and dynamic operations
haftmann
parents:
41343
diff
changeset

154 

56973
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

155 
fun static_value cookie = partiality_as_none ooo static_value_exn cookie; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

156 

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

157 

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

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

159 

39820  160 
structure Truth_Result = Proof_Data 
161 
( 

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

162 
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

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

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

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

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

167 
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

168 

58558
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

169 
local 
39605  170 

58558
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

171 
val reject_vars = fn ctxt => tap (reject_vars ctxt o Thm.term_of); 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

172 

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

174 
let 
55757  175 
val thy = Proof_Context.theory_of ctxt; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

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

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

178 
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

179 
else (); 
56245  180 
val iff = Thm.cterm_of thy (Term.Const (@{const_name Pure.eq}, propT > propT > propT)); 
55757  181 
val result = case partiality_as_none (evaluation truth_cookie ctxt evaluator vs_t []) 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

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

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

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

185 
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

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

187 

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

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

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

191 

56920
d651b944c67e
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
haftmann
parents:
56618
diff
changeset

192 
fun check_holds_oracle ctxt evaluator vs_ty_t ct = 
d651b944c67e
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
haftmann
parents:
56618
diff
changeset

193 
raw_check_holds_oracle (ctxt, evaluator, vs_ty_t, ct); 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

194 

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

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

196 

55757  197 
fun dynamic_holds_conv ctxt = Code_Thingol.dynamic_conv ctxt 
56969
7491932da574
dropped obsolete handwaving adjustion of type variables: safely done in preprocessor
haftmann
parents:
56920
diff
changeset

198 
(fn program => fn vs_t => fn deps => 
56920
d651b944c67e
normalizing of type variables before evaluation with explicit resubstitution function: make nbe work with funny type variables like \<AA>;
haftmann
parents:
56618
diff
changeset

199 
check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t) 
55757  200 
o reject_vars ctxt; 
39473
33638f4883ac
dynamic and static value computation; builtin evaluation of propositions
haftmann
parents:
39422
diff
changeset

201 

56973
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

202 
fun static_holds_conv (ctxt_consts as { ctxt, ... }) = 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

203 
Code_Thingol.static_conv ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t => 
62da80041afd
syntactic means to prevent accidental mixup of static and dynamic context
haftmann
parents:
56969
diff
changeset

204 
K (check_holds_oracle ctxt' (obtain_evaluator ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt')); 
41349
0e2a3f22f018
evaluator separating static and dynamic operations
haftmann
parents:
41348
diff
changeset

205 

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

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

207 

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

208 

58558
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

209 
(** full static evaluation  still with limited coverage! **) 
39404
a8c337299bc1
Code_Runtime.value, corresponding to ML_Context.value; tuned
haftmann
parents:
39401
diff
changeset

210 

58557  211 
fun evaluation_code ctxt module_name program tycos consts = 
33992  212 
let 
55757  213 
val thy = Proof_Context.theory_of ctxt; 
48568  214 
val (ml_modules, target_names) = 
55757  215 
Code_Target.produce_code_for ctxt 
55683  216 
target NONE module_name [] program false (map Constant consts @ map Type_Constructor tycos); 
48568  217 
val ml_code = space_implode "\n\n" (map snd ml_modules); 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

218 
val (consts', tycos') = chop (length consts) target_names; 
42359  219 
val consts_map = map2 (fn const => 
220 
fn NONE => 

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

222 
"\nhas a userdefined serialization") 

55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

223 
 SOME const' => (const, const')) consts consts' 
42359  224 
val tycos_map = map2 (fn tyco => 
225 
fn NONE => 

55304  226 
error ("Type " ^ quote (Proof_Context.markup_type ctxt tyco) ^ 
42359  227 
"\nhas a userdefined serialization") 
55147
bce3dbc11f95
prefer explicit code symbol type over adhoc name mangling
haftmann
parents:
53171
diff
changeset

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

229 
in (ml_code, (tycos_map, consts_map)) end; 
28054  230 

58558
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

231 
fun typ_signatures_for T = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

232 
let 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

233 
val (Ts, T') = strip_type T; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

234 
in map_range (fn n => (drop n Ts > T', take n Ts)) (length Ts + 1) end; 
28054  235 

58558
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

236 
fun typ_signatures cTs = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

237 
let 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

238 
fun add (c, T) = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

239 
fold (fn (T, Ts) => Typtab.map_default (T, []) (cons (c, Ts))) 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

240 
(typ_signatures_for T); 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

241 
in 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

242 
Typtab.empty 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

243 
> fold add cTs 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

244 
> Typtab.lookup_list 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

245 
end; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

246 

30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

247 
fun print_of_term_funs { typ_sign_for, ml_name_for_const, ml_name_for_typ } Ts = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

248 
let 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

249 
val var_names = map_range (fn n => "t" ^ string_of_int (n + 1)); 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

250 
fun print_lhs c xs = "Const (" ^ quote c ^ ", _)" 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

251 
> fold (fn x => fn s => s ^ " $ " ^ x) xs 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

252 
> enclose "(" ")" 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

253 
> prefix "ctxt "; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

254 
fun print_rhs c Ts xs = ml_name_for_const c 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

255 
> fold2 (fn T => fn x => fn s => 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

256 
s ^ (" (" ^ ml_name_for_typ T ^ " ctxt " ^ x ^ ")")) Ts xs 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

257 
fun print_eq (c, Ts) = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

258 
let 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

259 
val xs = var_names (length Ts); 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

260 
in print_lhs c xs ^ " = " ^ print_rhs c Ts xs end; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

261 
val err_eq = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

262 
"ctxt t = error (" ^ quote "Bad term: " ^ " ^ Syntax.string_of_term ctxt t)"; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

263 
fun print_eqs T = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

264 
let 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

265 
val typ_signs = typ_sign_for T; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

266 
val name = ml_name_for_typ T; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

267 
in 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

268 
(map print_eq typ_signs @ [err_eq]) 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

269 
> map (prefix (name ^ " ")) 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

270 
> space_implode "\n  " 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

271 
end; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

272 
in 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

273 
map print_eqs Ts 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

274 
> space_implode "\nand " 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

275 
> prefix "fun " 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

276 
> pair (map ml_name_for_typ Ts) 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

277 
end; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

278 

30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

279 
fun print_of_term ctxt ml_name_for_const T cTs = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

280 
let 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

281 
val typ_sign_for = typ_signatures cTs; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

282 
fun add_typ T Ts = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

283 
if member (op =) Ts T 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

284 
then Ts 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

285 
else Ts 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

286 
> cons T 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

287 
> fold (fold add_typ o snd) (typ_sign_for T); 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

288 
val Ts = add_typ T []; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

289 
fun tycos_of (Type (tyco, Ts)) = maps tycos_of Ts @ [tyco] 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

290 
 tycos_of _ = []; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

291 
val ml_name_of = Name.desymbolize NONE o Long_Name.base_name; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

292 
val ml_names = map (suffix "_of_term" o space_implode "_" o map ml_name_of o tycos_of) Ts 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

293 
> Name.variant_list []; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

294 
val ml_name_for_typ = the o AList.lookup (op =) (Ts ~~ ml_names); 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

295 
in 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

296 
print_of_term_funs { typ_sign_for = typ_sign_for, 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

297 
ml_name_for_const = ml_name_for_const, 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

298 
ml_name_for_typ = ml_name_for_typ } Ts 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

299 
end; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

300 

30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

301 
fun compile_evaluator cookie ctxt cs_code cTs T { program, deps } = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

302 
let 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

303 
val (context_code, (_, const_map)) = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

304 
evaluation_code ctxt structure_generated program [] cs_code; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

305 
val ml_name_for_const = the o AList.lookup (op =) const_map; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

306 
val (ml_names, of_term_code) = print_of_term ctxt ml_name_for_const T cTs 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

307 
val of_term = value ctxt cookie (context_code ^ "\n" ^ of_term_code, List.last ml_names); 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

308 
in fn ctxt' => fn t => fn _ => fn _ => Exn.interruptible_capture (of_term ctxt') t end; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

309 

30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

310 
fun static_value_exn' cookie { ctxt, lift_postproc, consts, T } = 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

311 
let 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

312 
val thy = Proof_Context.theory_of ctxt; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

313 
val cs_code = map (Axclass.unoverload_const thy) consts; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

314 
val cTs = map2 (fn (_, T) => fn c => (c, T)) consts cs_code; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

315 
val evaluator = Code_Thingol.static_value { ctxt = ctxt, 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

316 
lift_postproc = Exn.map_result o lift_postproc, consts = cs_code } 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

317 
(compile_evaluator cookie ctxt cs_code cTs T); 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

318 
in fn ctxt' => 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

319 
evaluator ctxt' o reject_vars ctxt' o Syntax.check_term ctxt' o Type.constraint T 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

320 
end; 
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

321 

58643
133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

322 
fun static_value_strict' cookie = Exn.release ooo static_value_exn' cookie; 
133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

323 

133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

324 
fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie; 
133203bd474b
formally completeted set of experimental static evaluation functions
haftmann
parents:
58558
diff
changeset

325 

58645  326 
fun static_value_strict' cookie = Exn.release ooo static_value_exn' cookie; 
327 

328 
fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie; 

329 

58558
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

330 

30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

331 
(** code antiquotation **) 
28054  332 

333 
local 

334 

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

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

337 
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

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

339 
fun init _ = (([], []), (true, (Lazy.value ("", [])))); 
28054  340 
); 
341 

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

342 
val is_first_occ = fst o snd o Code_Antiq_Data.get; 
28054  343 

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

346 
val ((tycos, consts), _) = Code_Antiq_Data.get ctxt; 
30962  347 
val tycos' = fold (insert (op =)) new_tycos tycos; 
348 
val consts' = fold (insert (op =)) new_consts consts; 

58557  349 
val program = Code_Thingol.consts_program (Proof_Context.theory_of ctxt) consts'; 
38930
072363be3fd9
modernized; avoid pointless tinkering with structure names
haftmann
parents:
38929
diff
changeset

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

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

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

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

28054  356 

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

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

359 
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

360 
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

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

362 
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

363 
in (ml_code, body) end; 
28054  364 

365 
in 

366 

56069
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55757
diff
changeset

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

369 
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

370 
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

371 
val is_first = is_first_occ ctxt; 
56069
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55757
diff
changeset

372 
in (print_code is_first const, register_const const ctxt) end; 
30962  373 

28054  374 
end; (*local*) 
375 

376 

58558
30cc7ee5ac10
basic support for fully static evaluator generation without dynamic compiler invocation
haftmann
parents:
58557
diff
changeset

377 
(** reflection support **) 
36470  378 

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

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

381 
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

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

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

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

385 
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

386 
val _ = if null missing_constrs then [] 
45430  387 
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

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

389 
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

390 
val _ = if null false_constrs then [] 
45430  391 
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

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

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

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

395 
in (tyco, constrs) end; 
36470  396 

397 
fun add_eval_tyco (tyco, tyco') thy = 

398 
let 

399 
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

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

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

403 
 pr pr' _ tys = 
36470  404 
Code_Printer.concat [Code_Printer.enum "," "(" ")" (map (pr' Code_Printer.BR) tys), tyco'] 
405 
in 

406 
thy 

55150  407 
> Code_Target.set_printings (Type_Constructor (tyco, [(target, SOME (k, pr))])) 
36470  408 
end; 
409 

36514  410 
fun add_eval_constr (const, const') thy = 
411 
let 

412 
val k = Code.args_number thy const; 

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

38922  414 
(const' :: the_list (Code_Printer.tuplify pr' Code_Printer.BR (map fst ts))); 
36514  415 
in 
416 
thy 

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

418 
[(target, SOME (Code_Printer.simple_const_syntax (k, pr)))])) 
36514  419 
end; 
420 

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

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

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

424 
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

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

426 
> Code_Target.add_reserved target module_name 
57435  427 
> Context.theory_map (exec (Proof_Context.init_global thy (*FIXME*)) true code) 
38935
2cf3d8305b47
corrected misbehaved additional qualification of generated names
haftmann
parents:
38933
diff
changeset

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

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

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

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

433 
val preamble = 
46737  434 
"(* Generated from " ^ 
56208  435 
Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^ 
46737  436 
"; DO NOT EDIT! *)"; 
39912
2ffe7060ca75
avoid antiquotation processing for code_reflect; moved ML_Context.value to Code_Runtime
haftmann
parents:
39816
diff
changeset

437 
val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code); 
36470  438 
in 
439 
thy 

440 
end; 

441 

442 
fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy = 

443 
let 

55757  444 
val ctxt = Proof_Context.init_global thy; 
36470  445 
val datatypes = map (fn (raw_tyco, raw_cos) => 
55757  446 
(prep_type ctxt raw_tyco, (Option.map o map) (prep_const thy) raw_cos)) raw_datatypes; 
40421
b41aabb629ce
constructors to datatypes in code_reflect can be globbed; dropped unused code
haftmann
parents:
40320
diff
changeset

447 
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

448 
> apsnd flat; 
36470  449 
val functions = map (prep_const thy) raw_functions; 
58557  450 
val consts = constrs @ functions; 
451 
val program = Code_Thingol.consts_program (Proof_Context.theory_of ctxt) consts; 

452 
val result = evaluation_code ctxt module_name program tycos consts 

36514  453 
> (apsnd o apsnd) (chop (length constrs)); 
36470  454 
in 
455 
thy 

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

456 
> process_reflection result module_name some_file 
36470  457 
end; 
458 

39422  459 
val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I); 
36470  460 
val code_reflect_cmd = gen_code_reflect Code_Target.read_tyco Code.read_const; 
461 

462 

28054  463 
(** Isar setup **) 
464 

56069
451d5b73f8cf
simplified programming interface to define ML antiquotations  NB: the transformed context ignores updates of the context parser;
wenzelm
parents:
55757
diff
changeset

465 
val _ = 
56205  466 
Theory.setup (ML_Antiquotation.declaration @{binding code} Args.term (fn _ => ml_code_antiq)); 
28054  467 

36470  468 
local 
469 

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

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

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

475 
in 

476 

477 
val _ = 

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

478 
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

479 
"enrich runtime environment with generated code" 
52434  480 
(Parse.name  Scan.optional (@{keyword "datatypes"}  Parse.!!! (parse_datatype 
46949  481 
::: Scan.repeat (@{keyword "and"}  parse_datatype))) [] 
52434  482 
 Scan.optional (@{keyword "functions"}  Parse.!!! (Scan.repeat1 Parse.name)) [] 
483 
 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

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

485 
(code_reflect_cmd raw_datatypes raw_functions module_name some_file))); 
36470  486 

487 
end; (*local*) 

488 

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

489 

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

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

491 

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

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

493 

39820  494 
structure Loaded_Values = Theory_Data 
495 
( 

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

496 
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

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

498 
val extend = I 
39820  499 
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

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

501 

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

502 
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

503 
let 
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

504 
val _ = #enterVal ML_Env.local_name_space (string, value); 
53171  505 
val _ = Theory.setup (Loaded_Values.map (insert (op =) string)); 
39816
c7cec137c48a
added polyml_as_definition  using external SML files as substitute for proper definitions  only for polyml!
haftmann
parents:
39605
diff
changeset

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

507 

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

508 
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

509 

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

510 
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

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

512 
name_space = 
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

513 
{lookupVal = #lookupVal ML_Env.local_name_space, 
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

514 
lookupType = #lookupType ML_Env.local_name_space, 
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

515 
lookupFix = #lookupFix ML_Env.local_name_space, 
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

516 
lookupStruct = #lookupStruct ML_Env.local_name_space, 
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

517 
lookupSig = #lookupSig ML_Env.local_name_space, 
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

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

519 
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

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

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

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

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

524 
enterFunct = abort, 
56618
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

525 
allVal = #allVal ML_Env.local_name_space, 
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

526 
allType = #allType ML_Env.local_name_space, 
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

527 
allFix = #allFix ML_Env.local_name_space, 
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

528 
allStruct = #allStruct ML_Env.local_name_space, 
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

529 
allSig = #allSig ML_Env.local_name_space, 
874bdedb2313
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
wenzelm
parents:
56245
diff
changeset

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

531 
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

532 
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

533 
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

534 

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

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

536 

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

537 
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

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

539 
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

540 
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

541 
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

542 
(0, Path.implode filepath) false (File.read filepath); 
45268  543 
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

544 
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

545 
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

546 

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

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

548 

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

549 
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

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

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

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

553 
> (fn ([Const (const, _)], _) => 
55150  554 
Code_Target.set_printings (Constant (const, 
52435
6646bb548c6b
migration from code_(consttypeclassinstance) to code_printing and from code_module to code_identifier
haftmann
parents:
52434
diff
changeset

555 
[(target, SOME (Code_Printer.simple_const_syntax (0, (K o K o K o Code_Printer.str) ml_name)))])) 
55757  556 
#> tap (fn thy => Code_Target.produce_code (Proof_Context.init_global thy) false [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

557 

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

558 
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

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

560 
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

561 
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

562 
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

563 
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

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

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

566 
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

567 
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

568 
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

569 
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

570 

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

571 
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

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

573 
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

574 
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

575 
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

576 
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

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

578 
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

579 

28054  580 
end; (*struct*) 