syntactic means to prevent accidental mixup of static and dynamic context
authorhaftmann
Thu May 15 16:38:31 2014 +0200 (2014-05-15)
changeset 5697362da80041afd
parent 56972 f64730f667b9
child 56974 4ab498f41eee
syntactic means to prevent accidental mixup of static and dynamic context
src/HOL/Tools/code_evaluation.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_simp.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/HOL/Tools/code_evaluation.ML	Thu May 15 16:38:31 2014 +0200
     1.2 +++ b/src/HOL/Tools/code_evaluation.ML	Thu May 15 16:38:31 2014 +0200
     1.3 @@ -9,11 +9,15 @@
     1.4    val dynamic_value: Proof.context -> term -> term option
     1.5    val dynamic_value_strict: Proof.context -> term -> term
     1.6    val dynamic_value_exn: Proof.context -> term -> term Exn.result
     1.7 -  val static_value: Proof.context -> string list -> typ list -> Proof.context -> term -> term option
     1.8 -  val static_value_strict: Proof.context -> string list -> typ list -> Proof.context -> term -> term
     1.9 -  val static_value_exn: Proof.context -> string list -> typ list -> Proof.context -> term -> term Exn.result
    1.10 +  val static_value: { ctxt: Proof.context, consts: string list, Ts: typ list }
    1.11 +    -> Proof.context -> term -> term option
    1.12 +  val static_value_strict: { ctxt: Proof.context, consts: string list, Ts: typ list }
    1.13 +    -> Proof.context -> term -> term
    1.14 +  val static_value_exn: { ctxt: Proof.context, consts: string list, Ts: typ list }
    1.15 +    -> Proof.context -> term -> term Exn.result
    1.16    val dynamic_conv: Proof.context -> conv
    1.17 -  val static_conv: Proof.context -> string list -> typ list -> Proof.context -> conv
    1.18 +  val static_conv: { ctxt: Proof.context, consts: string list, Ts: typ list }
    1.19 +    -> Proof.context -> conv
    1.20    val put_term: (unit -> term) -> Proof.context -> Proof.context
    1.21    val tracing: string -> 'a -> 'a
    1.22  end;
    1.23 @@ -160,8 +164,7 @@
    1.24        | NONE => NONE)
    1.25    | subst_termify t = subst_termify_app (strip_comb t) 
    1.26  
    1.27 -fun check_termify ctxt ts =
    1.28 -  the_default ts (map_default subst_termify ts);
    1.29 +fun check_termify _ ts = the_default ts (map_default subst_termify ts);
    1.30  
    1.31  val _ = Context.>> (Syntax_Phases.term_check 0 "termify" check_termify);
    1.32  
    1.33 @@ -188,10 +191,11 @@
    1.34  val dynamic_value_strict = gen_dynamic_value Code_Runtime.dynamic_value_strict;
    1.35  val dynamic_value_exn = gen_dynamic_value Code_Runtime.dynamic_value_exn;
    1.36  
    1.37 -fun gen_static_value static_value ctxt consts Ts =
    1.38 +fun gen_static_value static_value { ctxt, consts, Ts } =
    1.39    let
    1.40 -    val static_value' = static_value cookie ctxt NONE I
    1.41 -      (union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts)
    1.42 +    val static_value' = static_value cookie
    1.43 +      { ctxt = ctxt, target = NONE, lift_postproc = I, consts =
    1.44 +        union (op =) (map (term_of_const_for (Proof_Context.theory_of ctxt)) Ts) consts }
    1.45    in fn ctxt' => fn t => static_value' ctxt' (mk_term_of t) end;
    1.46  
    1.47  val static_value = gen_static_value Code_Runtime.static_value;
    1.48 @@ -214,13 +218,13 @@
    1.49  fun dynamic_conv ctxt = certify_eval ctxt dynamic_value
    1.50    Code_Runtime.dynamic_holds_conv;
    1.51  
    1.52 -fun static_conv ctxt consts Ts =
    1.53 +fun static_conv { ctxt, consts, Ts }  =
    1.54    let
    1.55      val eqs = @{const_name Pure.eq} :: @{const_name HOL.eq} ::
    1.56        map (fn T => Axclass.unoverload_const (Proof_Context.theory_of ctxt)
    1.57          (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for Pure.eq etc.*)
    1.58 -    val value = static_value ctxt consts Ts;
    1.59 -    val holds = Code_Runtime.static_holds_conv ctxt (union (op =) eqs consts);
    1.60 +    val value = static_value { ctxt = ctxt, consts = consts, Ts = Ts };
    1.61 +    val holds = Code_Runtime.static_holds_conv { ctxt = ctxt, consts = union (op =) eqs consts };
    1.62    in
    1.63      fn ctxt' => certify_eval ctxt' value holds
    1.64    end;
     2.1 --- a/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:31 2014 +0200
     2.2 +++ b/src/Tools/Code/code_preproc.ML	Thu May 15 16:38:31 2014 +0200
     2.3 @@ -26,11 +26,11 @@
     2.4      -> (code_algebra -> code_graph -> term -> conv) -> conv
     2.5    val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'b)
     2.6      -> (code_algebra -> code_graph -> term -> 'a) -> term -> 'b
     2.7 -  val static_conv: Proof.context -> string list
     2.8 -    -> (code_algebra -> code_graph -> Proof.context -> term -> conv)
     2.9 +  val static_conv: { ctxt: Proof.context, consts: string list }
    2.10 +    -> ({ algebra: code_algebra, eqngr: code_graph } -> Proof.context -> term -> conv)
    2.11      -> Proof.context -> conv
    2.12 -  val static_value: Proof.context -> ((term -> term) -> 'a -> 'b) -> string list
    2.13 -    -> (code_algebra -> code_graph -> Proof.context -> term -> 'a)
    2.14 +  val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'b), consts: string list }
    2.15 +    -> ({ algebra: code_algebra, eqngr: code_graph } -> Proof.context -> term -> 'a)
    2.16      -> Proof.context -> term -> 'b
    2.17  end
    2.18  
    2.19 @@ -498,15 +498,15 @@
    2.20  fun dynamic_value ctxt lift_postproc evaluator =
    2.21    evaluation (value_sandwich ctxt) lift_postproc (dynamic_evaluator evaluator) ctxt;
    2.22  
    2.23 -fun static_conv ctxt consts conv =
    2.24 +fun static_conv { ctxt, consts } conv =
    2.25    let
    2.26      val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
    2.27 -  in finalize (value_sandwich ctxt) (conv algebra eqngr) end;
    2.28 +  in finalize (value_sandwich ctxt) (conv { algebra = algebra, eqngr = eqngr }) end;
    2.29  
    2.30 -fun static_value ctxt lift_postproc consts evaluator =
    2.31 +fun static_value { ctxt, lift_postproc, consts } evaluator =
    2.32    let
    2.33      val (algebra, eqngr) = obtain true (Proof_Context.theory_of ctxt) consts [];
    2.34 -  in evaluation (value_sandwich ctxt) lift_postproc (evaluator algebra eqngr) end;
    2.35 +  in evaluation (value_sandwich ctxt) lift_postproc (evaluator { algebra = algebra, eqngr = eqngr }) end;
    2.36  
    2.37  
    2.38  (** setup **)
     3.1 --- a/src/Tools/Code/code_runtime.ML	Thu May 15 16:38:31 2014 +0200
     3.2 +++ b/src/Tools/Code/code_runtime.ML	Thu May 15 16:38:31 2014 +0200
     3.3 @@ -17,14 +17,17 @@
     3.4      -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a
     3.5    val dynamic_value_exn: 'a cookie -> Proof.context -> string option
     3.6      -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
     3.7 -  val static_value: 'a cookie -> Proof.context -> string option
     3.8 -    -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a option
     3.9 -  val static_value_strict: 'a cookie -> Proof.context -> string option
    3.10 -    -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a
    3.11 -  val static_value_exn: 'a cookie -> Proof.context -> string option
    3.12 -    -> ((term -> term) -> 'a -> 'a) -> string list -> Proof.context -> term -> 'a Exn.result
    3.13 +  val static_value: 'a cookie -> { ctxt: Proof.context, target: string option,
    3.14 +    lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
    3.15 +    -> Proof.context -> term -> 'a option
    3.16 +  val static_value_strict: 'a cookie -> { ctxt: Proof.context, target: string option,
    3.17 +    lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
    3.18 +    -> Proof.context -> term -> 'a
    3.19 +  val static_value_exn: 'a cookie -> { ctxt: Proof.context, target: string option,
    3.20 +    lift_postproc: (term -> term) -> 'a -> 'a, consts: string list }
    3.21 +    -> Proof.context -> term -> 'a Exn.result
    3.22    val dynamic_holds_conv: Proof.context -> conv
    3.23 -  val static_holds_conv: Proof.context -> string list -> Proof.context -> conv
    3.24 +  val static_holds_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
    3.25    val code_reflect: (string * string list option) list -> string list -> string
    3.26      -> string option -> theory -> theory
    3.27    datatype truth = Holds
    3.28 @@ -122,23 +125,22 @@
    3.29  fun dynamic_value cookie ctxt some_target postproc t args =
    3.30    partiality_as_none (dynamic_value_exn cookie ctxt some_target postproc t args);
    3.31  
    3.32 -fun static_evaluator cookie ctxt some_target program consts' =
    3.33 +fun static_evaluator cookie ctxt some_target { program, deps } =
    3.34    let
    3.35 -    val evaluator = obtain_evaluator ctxt some_target program (map Constant consts');
    3.36 +    val evaluator = obtain_evaluator ctxt some_target program (map Constant deps);
    3.37      val evaluation' = evaluation cookie ctxt evaluator;
    3.38    in fn _ => fn _ => fn vs_ty_t => fn _ => evaluation' vs_ty_t [] end;
    3.39  
    3.40 -fun static_value_exn cookie ctxt some_target postproc consts =
    3.41 +fun static_value_exn cookie { ctxt, target, lift_postproc, consts } =
    3.42    let
    3.43 -    val evaluator = Code_Thingol.static_value ctxt (Exn.map_result o postproc) consts
    3.44 -      (static_evaluator cookie ctxt some_target);
    3.45 +    val evaluator = Code_Thingol.static_value { ctxt = ctxt,
    3.46 +      lift_postproc = Exn.map_result o lift_postproc, consts = consts }
    3.47 +      (static_evaluator cookie ctxt target);
    3.48    in fn ctxt' => evaluator ctxt' o reject_vars ctxt' end;
    3.49  
    3.50 -fun static_value_strict cookie ctxt some_target postproc consts =
    3.51 -  Exn.release oo static_value_exn cookie ctxt some_target postproc consts;
    3.52 +fun static_value_strict cookie = Exn.release ooo static_value_exn cookie;
    3.53  
    3.54 -fun static_value cookie thy some_target postproc consts =
    3.55 -  partiality_as_none oo static_value_exn cookie thy some_target postproc consts;
    3.56 +fun static_value cookie = partiality_as_none ooo static_value_exn cookie;
    3.57  
    3.58  
    3.59  (* evaluation for truth or nothing *)
    3.60 @@ -185,15 +187,9 @@
    3.61      check_holds_oracle ctxt (obtain_evaluator ctxt NONE program deps) vs_t)
    3.62        o reject_vars ctxt;
    3.63  
    3.64 -fun static_holds_conv ctxt consts =
    3.65 -  Code_Thingol.static_conv ctxt consts (fn program => fn consts' =>
    3.66 -    let
    3.67 -      val evaluator' = obtain_evaluator ctxt NONE program (map Constant consts')
    3.68 -    in
    3.69 -      fn ctxt' => fn vs_t => fn _ => check_holds_oracle ctxt' evaluator' vs_t o reject_vars ctxt'
    3.70 -    end);
    3.71 -
    3.72 -(* o reject_vars ctxt'*)
    3.73 +fun static_holds_conv (ctxt_consts as { ctxt, ... }) =
    3.74 +  Code_Thingol.static_conv ctxt_consts (fn { program, deps } => fn ctxt' => fn vs_t =>
    3.75 +    K (check_holds_oracle ctxt' (obtain_evaluator ctxt NONE program (map Constant deps)) vs_t o reject_vars ctxt'));
    3.76  
    3.77  end; (*local*)
    3.78  
     4.1 --- a/src/Tools/Code/code_simp.ML	Thu May 15 16:38:31 2014 +0200
     4.2 +++ b/src/Tools/Code/code_simp.ML	Thu May 15 16:38:31 2014 +0200
     4.3 @@ -10,8 +10,10 @@
     4.4    val dynamic_conv: Proof.context -> conv
     4.5    val dynamic_tac: Proof.context -> int -> tactic
     4.6    val dynamic_value: Proof.context -> term -> term
     4.7 -  val static_conv: Proof.context -> simpset option -> string list -> Proof.context -> conv
     4.8 -  val static_tac: Proof.context -> simpset option -> string list -> Proof.context -> int -> tactic
     4.9 +  val static_conv: { ctxt: Proof.context, simpset: simpset option, consts: string list }
    4.10 +    -> Proof.context -> conv
    4.11 +  val static_tac: { ctxt: Proof.context, simpset: simpset option, consts: string list }
    4.12 +    -> Proof.context -> int -> tactic
    4.13    val setup: theory -> theory
    4.14    val trace: bool Config.T
    4.15  end;
    4.16 @@ -92,15 +94,14 @@
    4.17  
    4.18  (* evaluation with static code context *)
    4.19  
    4.20 -fun static_conv ctxt some_ss consts =
    4.21 -  Code_Thingol.static_conv_simple ctxt consts
    4.22 -    (fn program => let val conv' = rewrite_modulo ctxt some_ss program
    4.23 -     in fn ctxt' => fn _ => conv' ctxt' end);
    4.24 +fun static_conv { ctxt, simpset, consts } =
    4.25 +  Code_Thingol.static_conv_simple { ctxt = ctxt, consts = consts }
    4.26 +    (K oo rewrite_modulo ctxt simpset);
    4.27  
    4.28 -fun static_tac ctxt some_ss consts =
    4.29 +fun static_tac { ctxt, simpset, consts } =
    4.30    let
    4.31 -    val conv = static_conv ctxt some_ss consts;
    4.32 -    val tac = conclude_tac ctxt some_ss;
    4.33 +    val conv = static_conv { ctxt = ctxt, simpset = simpset, consts = consts };
    4.34 +    val tac = conclude_tac ctxt simpset;
    4.35    in fn ctxt' => CONVERSION (conv ctxt') THEN' (tac ctxt') end;
    4.36  
    4.37  end;
     5.1 --- a/src/Tools/Code/code_thingol.ML	Thu May 15 16:38:31 2014 +0200
     5.2 +++ b/src/Tools/Code/code_thingol.ML	Thu May 15 16:38:31 2014 +0200
     5.3 @@ -91,14 +91,15 @@
     5.4    val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
     5.5      -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
     5.6      -> term -> 'a
     5.7 -  val static_conv: Proof.context -> string list -> (program -> string list
     5.8 -    -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv)
     5.9 +  val static_conv: { ctxt: Proof.context, consts: string list }
    5.10 +    -> ({ program: program, deps: string list }
    5.11 +      -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv)
    5.12      -> Proof.context -> conv
    5.13 -  val static_conv_simple: Proof.context -> string list
    5.14 +  val static_conv_simple: { ctxt: Proof.context, consts: string list }
    5.15      -> (program -> Proof.context -> term -> conv)
    5.16      -> Proof.context -> conv
    5.17 -  val static_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> string list ->
    5.18 -    (program -> string list
    5.19 +  val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'a), consts: string list }
    5.20 +    -> ({ program: program, deps: string list }
    5.21        -> Proof.context -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
    5.22      -> Proof.context -> term -> 'a
    5.23  end;
    5.24 @@ -841,32 +842,31 @@
    5.25        ensure_value ctxt algebra eqngr t ([], program);
    5.26    in subevaluator ctxt t (vs_ty', t') deps end;
    5.27  
    5.28 -fun static_evaluator ctxt evaluator consts algebra eqngr =
    5.29 +fun static_evaluator ctxt evaluator consts { algebra, eqngr } =
    5.30    let
    5.31      fun generate_consts ctxt algebra eqngr =
    5.32        fold_map (ensure_const ctxt algebra eqngr false);
    5.33 -    val (consts', program) =
    5.34 +    val (deps, program) =
    5.35        invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
    5.36 -    val subevaluator = evaluator program consts';
    5.37 +    val subevaluator = evaluator { program = program, deps = deps };
    5.38    in fn ctxt' => static_subevaluator ctxt' subevaluator algebra eqngr program end;
    5.39  
    5.40 -fun static_evaluator_simple ctxt evaluator consts algebra eqngr =
    5.41 +fun static_evaluator_simple ctxt evaluator consts { algebra, eqngr } =
    5.42    let
    5.43      fun generate_consts ctxt algebra eqngr =
    5.44        fold_map (ensure_const ctxt algebra eqngr false);
    5.45      val (_, program) =
    5.46        invoke_generation true (Proof_Context.theory_of ctxt) (algebra, eqngr) generate_consts consts;
    5.47 -  in evaluator program end;
    5.48 +  in evaluator (program: program) end;
    5.49  
    5.50 -fun static_conv ctxt consts conv =
    5.51 -  Code_Preproc.static_conv ctxt consts (static_evaluator ctxt (fn program => fn deps =>
    5.52 -    let val conv' = conv program deps in fn ctxt => fn _ => conv' ctxt end) consts);
    5.53 +fun static_conv (ctxt_consts as { ctxt, consts }) conv =
    5.54 +  Code_Preproc.static_conv ctxt_consts (static_evaluator ctxt (K oo conv) consts);
    5.55  
    5.56 -fun static_conv_simple ctxt consts conv =
    5.57 -  Code_Preproc.static_conv ctxt consts (static_evaluator_simple ctxt conv consts);
    5.58 +fun static_conv_simple (ctxt_consts as { ctxt, consts }) conv =
    5.59 +  Code_Preproc.static_conv ctxt_consts (static_evaluator_simple ctxt conv consts);
    5.60  
    5.61 -fun static_value ctxt postproc consts evaluator =
    5.62 -  Code_Preproc.static_value ctxt postproc consts (static_evaluator ctxt evaluator consts);
    5.63 +fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) evaluator =
    5.64 +  Code_Preproc.static_value ctxt_postproc_consts (static_evaluator ctxt evaluator consts);
    5.65  
    5.66  
    5.67  (** constant expressions **)
     6.1 --- a/src/Tools/nbe.ML	Thu May 15 16:38:31 2014 +0200
     6.2 +++ b/src/Tools/nbe.ML	Thu May 15 16:38:31 2014 +0200
     6.3 @@ -8,8 +8,8 @@
     6.4  sig
     6.5    val dynamic_conv: Proof.context -> conv
     6.6    val dynamic_value: Proof.context -> term -> term
     6.7 -  val static_conv: Proof.context -> string list -> Proof.context -> conv
     6.8 -  val static_value: Proof.context -> string list -> Proof.context -> term -> term
     6.9 +  val static_conv: { ctxt: Proof.context, consts: string list } -> Proof.context -> conv
    6.10 +  val static_value: { ctxt: Proof.context, consts: string list } -> Proof.context -> term -> term
    6.11  
    6.12    datatype Univ =
    6.13        Const of int * Univ list               (*named (uninterpreted) constants*)
    6.14 @@ -597,16 +597,16 @@
    6.15  fun dynamic_value ctxt = lift_triv_classes_rew ctxt
    6.16    (Code_Thingol.dynamic_value ctxt I (eval_term ctxt o compile false ctxt));
    6.17  
    6.18 -fun static_conv ctxt consts =
    6.19 +fun static_conv (ctxt_consts as { ctxt, ... }) =
    6.20    let
    6.21 -    val evaluator = Code_Thingol.static_conv ctxt consts
    6.22 -      (fn program => fn _ => fn ctxt' => oracle ctxt' (compile true ctxt program));
    6.23 +    val evaluator = Code_Thingol.static_conv ctxt_consts
    6.24 +      (fn { program, ... } => fn ctxt' => oracle ctxt' (compile true ctxt program));
    6.25    in fn ctxt' => lift_triv_classes_conv ctxt' (evaluator ctxt') end;
    6.26  
    6.27 -fun static_value ctxt consts =
    6.28 +fun static_value { ctxt, consts } =
    6.29    let
    6.30 -    val evaluator = Code_Thingol.static_value ctxt I consts
    6.31 -      (fn program => fn _ => fn ctxt' => eval_term ctxt' (compile false ctxt program));
    6.32 +    val evaluator = Code_Thingol.static_value { ctxt = ctxt, lift_postproc = I, consts = consts }
    6.33 +      (fn { program, ... } => fn ctxt' => eval_term ctxt' (compile false ctxt program));
    6.34    in fn ctxt' => lift_triv_classes_rew ctxt' (evaluator ctxt') end;
    6.35  
    6.36  end;