made sml/nj happy
authorhaftmann
Fri Sep 17 08:41:07 2010 +0200 (2010-09-17)
changeset 394821c37d19e3d58
parent 39481 f15514acc942
child 39483 9f0e5684f04b
child 39484 505f95975a5a
child 39489 8bb7f32a3a08
made sml/nj happy
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu Sep 16 17:52:00 2010 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Sep 17 08:41:07 2010 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  
     1.5  type 'a cookie = (Proof.context -> unit -> 'a) * ((unit -> 'a) -> Proof.context -> Proof.context) * string;
     1.6  
     1.7 -fun base_evaluator cookie thy some_target naming program ((_, (vs, ty)), t) deps args =
     1.8 +fun base_evaluator cookie thy some_target naming program ((vs, ty), t) deps args =
     1.9    let
    1.10      val ctxt = ProofContext.init_global thy;
    1.11      val _ = if Code_Thingol.contains_dictvar t then
    1.12 @@ -83,8 +83,8 @@
    1.13  
    1.14  fun dynamic_value_exn cookie thy some_target postproc t args =
    1.15    let
    1.16 -    fun evaluator naming program expr deps =
    1.17 -      base_evaluator cookie thy some_target naming program expr deps args;
    1.18 +    fun evaluator naming program ((_, vs_ty), t) deps =
    1.19 +      base_evaluator cookie thy some_target naming program (vs_ty, t) deps args;
    1.20    in Code_Thingol.dynamic_eval_value thy (Exn.map_result o postproc) evaluator t end;
    1.21  
    1.22  fun dynamic_value_strict cookie thy some_target postproc t args =
    1.23 @@ -95,8 +95,8 @@
    1.24  
    1.25  fun static_value_exn cookie thy some_target postproc consts =
    1.26    let
    1.27 -    fun evaluator naming program thy expr deps =
    1.28 -      base_evaluator cookie thy some_target naming program expr deps [];
    1.29 +    fun evaluator naming program thy ((_, vs_ty), t) deps =
    1.30 +      base_evaluator cookie thy some_target naming program (vs_ty, t) deps [];
    1.31    in Code_Thingol.static_eval_value thy (Exn.map_result o postproc) consts evaluator end;
    1.32  
    1.33  fun static_value_strict cookie thy some_target postproc consts t =
    1.34 @@ -115,14 +115,14 @@
    1.35  val put_truth = Truth_Result.put;
    1.36  val truth_cookie = (Truth_Result.get, put_truth, Long_Name.append this "put_truth");
    1.37  
    1.38 -fun check_holds thy naming program expr deps ct =
    1.39 +fun check_holds thy naming program vs_t deps ct =
    1.40    let
    1.41      val t = Thm.term_of ct;
    1.42      val _ = if fastype_of t <> propT
    1.43        then error ("Not a proposition: " ^ Syntax.string_of_term_global thy t)
    1.44        else ();
    1.45      val iff = Thm.cterm_of thy (Term.Const ("==", propT --> propT --> propT));
    1.46 -    val result = case partiality_as_none (base_evaluator truth_cookie thy NONE naming program expr deps [])
    1.47 +    val result = case partiality_as_none (base_evaluator truth_cookie thy NONE naming program vs_t deps [])
    1.48       of SOME Holds => true
    1.49        | _ => false;
    1.50    in
    1.51 @@ -131,10 +131,10 @@
    1.52  
    1.53  val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
    1.54    (Thm.add_oracle (Binding.name "holds_by_evaluation",
    1.55 -  fn (thy, naming, program, expr, deps, ct) => check_holds thy naming program expr deps ct)));
    1.56 +  fn (thy, naming, program, vs_t, deps, ct) => check_holds thy naming program vs_t deps ct)));
    1.57  
    1.58 -fun check_holds_oracle thy naming program expr deps ct =
    1.59 -  raw_check_holds_oracle (thy, naming, program, expr, deps, ct);
    1.60 +fun check_holds_oracle thy naming program ((_, vs_ty), t) deps ct =
    1.61 +  raw_check_holds_oracle (thy, naming, program, (vs_ty, t), deps, ct);
    1.62  
    1.63  val dynamic_holds_conv = Conv.tap_thy (fn thy => Code_Thingol.dynamic_eval_conv thy (check_holds_oracle thy));
    1.64