1.1 --- a/src/Tools/Code/code_preproc.ML Tue Dec 21 08:40:39 2010 +0100
1.2 +++ b/src/Tools/Code/code_preproc.ML Tue Dec 21 09:18:29 2010 +0100
1.3 @@ -29,9 +29,9 @@
1.4 val dynamic_value: theory -> ((term -> term) -> 'a -> 'a)
1.5 -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
1.6 val static_conv: theory -> string list
1.7 - -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> conv) -> conv
1.8 + -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
1.9 val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
1.10 - -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> 'a) -> term -> 'a
1.11 + -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
1.12
1.13 val setup: theory -> theory
1.14 end
1.15 @@ -490,7 +490,7 @@
1.16 fun static_conv thy consts conv =
1.17 let
1.18 val (algebra, eqngr) = obtain true thy consts [];
1.19 - val conv' = conv algebra eqngr thy;
1.20 + val conv' = conv algebra eqngr;
1.21 in
1.22 no_variables_conv ((preprocess_conv thy)
1.23 then_conv (fn ct => uncurry conv' (dest_cterm ct) ct)
1.24 @@ -504,7 +504,7 @@
1.25 in
1.26 preprocess_term thy
1.27 #-> (fn resubst => fn t => t
1.28 - |> evaluator' thy (Term.add_tfrees t [])
1.29 + |> evaluator' (Term.add_tfrees t [])
1.30 |> postproc (postprocess_term thy o resubst))
1.31 end;
1.32
2.1 --- a/src/Tools/Code/code_simp.ML Tue Dec 21 08:40:39 2010 +0100
2.2 +++ b/src/Tools/Code/code_simp.ML Tue Dec 21 09:18:29 2010 +0100
2.3 @@ -68,7 +68,7 @@
2.4
2.5 fun static_conv thy some_ss consts =
2.6 Code_Thingol.static_conv_simple thy consts
2.7 - (fn program => fn thy => fn _ => fn _ => rewrite_modulo thy some_ss program);
2.8 + (fn program => fn _ => fn _ => rewrite_modulo thy some_ss program);
2.9
2.10 fun static_tac thy some_ss consts = CONVERSION (static_conv thy some_ss consts)
2.11 THEN' conclude_tac thy some_ss;
3.1 --- a/src/Tools/Code/code_thingol.ML Tue Dec 21 08:40:39 2010 +0100
3.2 +++ b/src/Tools/Code/code_thingol.ML Tue Dec 21 09:18:29 2010 +0100
3.3 @@ -100,14 +100,14 @@
3.4 val dynamic_value: theory -> ((term -> term) -> 'a -> 'a) -> (naming -> program
3.5 -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
3.6 -> term -> 'a
3.7 - val static_conv: theory -> string list -> (naming -> program
3.8 - -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
3.9 + val static_conv: theory -> string list -> (naming -> program -> string list
3.10 + -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
3.11 -> conv
3.12 val static_conv_simple: theory -> string list
3.13 - -> (program -> theory -> (string * sort) list -> term -> conv) -> conv
3.14 + -> (program -> (string * sort) list -> term -> conv) -> conv
3.15 val static_value: theory -> ((term -> term) -> 'a -> 'a) -> string list ->
3.16 - (naming -> program
3.17 - -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
3.18 + (naming -> program -> string list
3.19 + -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
3.20 -> term -> 'a
3.21 end;
3.22
3.23 @@ -916,27 +916,27 @@
3.24 let
3.25 fun generate_consts thy algebra eqngr =
3.26 fold_map (ensure_const thy algebra eqngr false);
3.27 - val (_, (naming, program)) = invoke_generation true thy (algebra, eqngr)
3.28 + val (consts', (naming, program)) = invoke_generation true thy (algebra, eqngr)
3.29 generate_consts consts;
3.30 - in f algebra eqngr naming program end;
3.31 + in f algebra eqngr naming program consts' end;
3.32
3.33 -fun static_evaluator evaluator algebra eqngr naming program thy vs t =
3.34 +fun static_evaluation thy evaluator algebra eqngr naming program consts' vs t =
3.35 let
3.36 val (((_, program'), (((vs', ty'), t'), deps)), _) =
3.37 ensure_value thy algebra eqngr t (NONE, (naming, program));
3.38 - in evaluator naming program' thy ((original_sorts vs vs', (vs', ty')), t') deps end;
3.39 + in evaluator naming program' consts' ((original_sorts vs vs', (vs', ty')), t') deps end;
3.40
3.41 fun static_conv thy consts conv =
3.42 Code_Preproc.static_conv thy consts
3.43 - (provide_program thy consts (static_evaluator conv));
3.44 + (provide_program thy consts (static_evaluation thy conv));
3.45
3.46 fun static_conv_simple thy consts conv =
3.47 Code_Preproc.static_conv thy consts
3.48 - (provide_program thy consts ((K o K o K) conv));
3.49 + (provide_program thy consts (fn _ => fn _ => fn _ => fn program => fn _ => conv program));
3.50
3.51 fun static_value thy postproc consts evaluator =
3.52 Code_Preproc.static_value thy postproc consts
3.53 - (provide_program thy consts (static_evaluator evaluator));
3.54 + (provide_program thy consts (static_evaluation thy evaluator));
3.55
3.56
3.57 (** diagnostic commands **)
4.1 --- a/src/Tools/nbe.ML Tue Dec 21 08:40:39 2010 +0100
4.2 +++ b/src/Tools/nbe.ML Tue Dec 21 09:18:29 2010 +0100
4.3 @@ -602,13 +602,13 @@
4.4
4.5 fun static_conv thy consts =
4.6 lift_triv_classes_conv thy (Code_Thingol.static_conv thy consts
4.7 - (K (fn program => let val nbe_program = compile true thy program
4.8 - in fn thy => oracle thy program nbe_program end)));
4.9 + (K (fn program => fn _ => let val nbe_program = compile true thy program
4.10 + in oracle thy program nbe_program end)));
4.11
4.12 fun static_value thy consts = lift_triv_classes_rew thy
4.13 (Code_Thingol.static_value thy I consts
4.14 - (K (fn program => let val nbe_program = compile true thy program
4.15 - in fn thy => eval_term thy program (compile false thy program) end)));
4.16 + (K (fn program => fn _ => let val nbe_program = compile true thy program
4.17 + in eval_term thy program (compile false thy program) end)));
4.18
4.19
4.20 (** setup **)