6 *) |
6 *) |
7 |
7 |
8 signature CODE_PACKAGE = |
8 signature CODE_PACKAGE = |
9 sig |
9 sig |
10 val evaluate_conv: theory |
10 val evaluate_conv: theory |
11 -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm |
11 -> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm |
12 -> string list -> cterm -> thm) |
12 -> string list -> thm)) |
13 -> cterm -> thm; |
13 -> cterm -> thm; |
14 val evaluate_term: theory |
14 val evaluate_term: theory |
15 -> (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm |
15 -> (term -> term * (CodeThingol.code -> CodeThingol.typscheme * CodeThingol.iterm |
16 -> string list -> term -> 'a) |
16 -> string list -> 'a)) |
17 -> term -> 'a; |
17 -> term -> 'a; |
18 val eval_conv: string * (unit -> thm) option ref |
18 val eval_conv: string * (unit -> thm) option ref |
19 -> theory -> cterm -> string list -> thm; |
19 -> theory -> cterm -> string list -> thm; |
20 val eval_term: string * (unit -> 'a) option ref |
20 val eval_term: string * (unit -> 'a) option ref |
21 -> theory -> term -> string list -> 'a; |
21 -> theory -> term -> string list -> 'a; |
101 CodeTarget.get_serializer thy target permissive module file args cs) seris; |
101 CodeTarget.get_serializer thy target permissive module file args cs) seris; |
102 in (map (fn f => f code) seris' : unit list; ()) end; |
102 in (map (fn f => f code) seris' : unit list; ()) end; |
103 |
103 |
104 (* evaluation machinery *) |
104 (* evaluation machinery *) |
105 |
105 |
106 fun evaluate eval_kind term_of thy eval = eval_kind thy (fn funcgr => fn ct => |
106 fun evaluate eval_kind thy evaluator = |
107 let |
107 let |
108 val ((code, (vs_ty_t, deps)), _) = generate thy funcgr |
108 fun evaluator'' evaluator''' funcgr t = |
109 CodeThingol.ensure_value (term_of ct) |
109 let |
110 in eval code vs_ty_t deps ct end); |
110 val ((code, (vs_ty_t, deps)), _) = |
111 |
111 generate thy funcgr CodeThingol.ensure_value t; |
112 fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv Thm.term_of thy; |
112 in evaluator''' code vs_ty_t deps end; |
113 fun evaluate_term thy = evaluate CodeFuncgr.eval_term I thy; |
113 fun evaluator' t = |
114 |
114 let |
115 fun eval_ml reff args thy code ((vs, ty), t) deps _ = |
115 val (t', evaluator''') = evaluator t; |
|
116 in (t', evaluator'' evaluator''') end; |
|
117 in eval_kind thy evaluator' end |
|
118 |
|
119 fun evaluate_conv thy = evaluate CodeFuncgr.eval_conv thy; |
|
120 fun evaluate_term thy = evaluate CodeFuncgr.eval_term thy; |
|
121 |
|
122 fun eval_ml reff args thy code ((vs, ty), t) deps = |
116 CodeTarget.eval thy reff code (t, ty) args; |
123 CodeTarget.eval thy reff code (t, ty) args; |
117 |
124 |
118 fun eval evaluate term_of reff thy ct args = |
125 fun eval evaluate term_of reff thy ct args = |
119 let |
126 let |
120 val _ = if null (term_frees (term_of ct)) then () else error ("Term " |
127 val _ = if null (term_frees (term_of ct)) then () else error ("Term " |
121 ^ quote (Sign.string_of_term thy (term_of ct)) |
128 ^ quote (Sign.string_of_term thy (term_of ct)) |
122 ^ " to be evaluated containts free variables"); |
129 ^ " to be evaluated contains free variables"); |
123 in evaluate thy (eval_ml reff args thy) ct end; |
130 in evaluate thy (fn t => (t, eval_ml reff args thy)) ct end; |
124 |
131 |
125 fun eval_conv reff = eval evaluate_conv Thm.term_of reff; |
132 fun eval_conv reff = eval evaluate_conv Thm.term_of reff; |
126 fun eval_term reff = eval evaluate_term I reff; |
133 fun eval_term reff = eval evaluate_term I reff; |
127 |
134 |
128 val satisfies_ref : (unit -> bool) option ref = ref NONE; |
135 val satisfies_ref : (unit -> bool) option ref = ref NONE; |