src/Tools/Code/code_thingol.ML
changeset 56973 62da80041afd
parent 56969 7491932da574
child 58397 1c036d6216d3
     1.1 --- a/src/Tools/Code/code_thingol.ML	Thu May 15 16:38:31 2014 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Thu May 15 16:38:31 2014 +0200
     1.3 @@ -91,14 +91,15 @@
     1.4    val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
     1.5      -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
     1.6      -> term -> 'a
     1.7 -  val static_conv: Proof.context -> string list -> (program -> string list
     1.8 -    -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv)
     1.9 +  val static_conv: { ctxt: Proof.context, consts: string list }
    1.10 +    -> ({ program: program, deps: string list }
    1.11 +      -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv)
    1.12      -> Proof.context -> conv
    1.13 -  val static_conv_simple: Proof.context -> string list
    1.14 +  val static_conv_simple: { ctxt: Proof.context, consts: string list }
    1.15      -> (program -> Proof.context -> term -> conv)
    1.16      -> Proof.context -> conv
    1.17 -  val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list ->
    1.18 -    (program -> string list
    1.19 +  val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'a), consts: string list }
    1.20 +    -> ({ program: program, deps: string list }
    1.21        -> Proof.context -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
    1.22      -> Proof.context -> term -> 'a
    1.23  end;
    1.24 @@ -841,32 +842,31 @@
    1.25        ensure_value ctxt algebra eqngr t ([], program);
    1.26    in subevaluator ctxt t (vs_ty', t') deps end;
    1.27  
    1.28 -fun static_evaluator ctxt evaluator consts algebra eqngr =
    1.29 +fun static_evaluator ctxt evaluator consts { algebra, eqngr } =
    1.30    let
    1.31      fun generate_consts ctxt algebra eqngr =
    1.32        fold_map (ensure_const ctxt algebra eqngr false);
    1.33 -    val (consts', program) =
    1.34 +    val (deps, program) =
    1.35        invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
    1.36 -    val subevaluator = evaluator program consts';
    1.37 +    val subevaluator = evaluator { program = program, deps = deps };
    1.38    in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end;
    1.39  
    1.40 -fun static_evaluator_simple ctxt evaluator consts algebra eqngr =
    1.41 +fun static_evaluator_simple ctxt evaluator consts { algebra, eqngr } =
    1.42    let
    1.43      fun generate_consts ctxt algebra eqngr =
    1.44        fold_map (ensure_const ctxt algebra eqngr false);
    1.45      val (_, program) =
    1.46        invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
    1.47 -  in evaluator program end;
    1.48 +  in evaluator (program: program) end;
    1.49  
    1.50 -fun static_conv ctxt consts conv =
    1.51 -  Code_Preproc.static_conv ctxt consts (static_evaluator ctxt (fn program => fn deps =>
    1.52 -    let val conv' = conv program deps in fn ctxt => fn _ => conv' ctxt end) consts);
    1.53 +fun static_conv (ctxt_consts as { ctxt, consts }) conv =
    1.54 +  Code_Preproc.static_conv ctxt_consts (static_evaluator ctxt (K oo conv) consts);
    1.55  
    1.56 -fun static_conv_simple ctxt consts conv =
    1.57 -  Code_Preproc.static_conv ctxt consts (static_evaluator_simple ctxt conv consts);
    1.58 +fun static_conv_simple (ctxt_consts as { ctxt, consts }) conv =
    1.59 +  Code_Preproc.static_conv ctxt_consts (static_evaluator_simple ctxt conv consts);
    1.60  
    1.61 -fun static_value ctxt postproc consts evaluator =
    1.62 -  Code_Preproc.static_value ctxt postproc consts (static_evaluator ctxt evaluator consts);
    1.63 +fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) evaluator =
    1.64 +  Code_Preproc.static_value ctxt_postproc_consts (static_evaluator ctxt evaluator consts);
    1.65  
    1.66  
    1.67  (** constant expressions **)