canonical handling of theory context argument
authorhaftmann
Tue Dec 21 09:18:29 2010 +0100 (2010-12-21)
changeset 413466673f6fa94ca
parent 41344 d990badc97a3
child 41347 064133cb4ef6
canonical handling of theory context argument
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_simp.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     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 **)