separation of static and dynamic thy context
authorhaftmann
Thu Sep 16 16:51:34 2010 +0200 (2010-09-16)
changeset 394759cc1ba3c5706
parent 39474 1986f18c4940
child 39476 8bc560df99ea
separation of static and dynamic thy context
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	Thu Sep 16 16:51:34 2010 +0200
     1.2 +++ b/src/Tools/Code/code_preproc.ML	Thu Sep 16 16:51:34 2010 +0200
     1.3 @@ -29,7 +29,9 @@
     1.4    val dynamic_eval_value: theory -> ((term -> term) -> 'a -> 'a)
     1.5      -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
     1.6    val static_eval_conv: theory -> string list
     1.7 -    -> (code_algebra -> code_graph -> (string * sort) list -> term -> conv) -> conv
     1.8 +    -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> conv) -> conv
     1.9 +  val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
    1.10 +    -> (code_algebra -> code_graph -> theory -> (string * sort) list -> term -> 'a) -> term -> 'a
    1.11  
    1.12    val setup: theory -> theory
    1.13  end
    1.14 @@ -138,6 +140,8 @@
    1.15  
    1.16  fun preprocess_conv thy ct =
    1.17    let
    1.18 +    val ctxt = ProofContext.init_global thy;
    1.19 +    val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
    1.20      val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
    1.21    in
    1.22      ct
    1.23 @@ -145,6 +149,8 @@
    1.24      |> trans_conv_rule (AxClass.unoverload_conv thy)
    1.25    end;
    1.26  
    1.27 +fun preprocess_term thy = term_of_conv thy (preprocess_conv thy);
    1.28 +
    1.29  fun postprocess_conv thy ct =
    1.30    let
    1.31      val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
    1.32 @@ -427,43 +433,56 @@
    1.33  
    1.34  fun dest_cterm ct = let val t = Thm.term_of ct in (Term.add_tfrees t [], t) end;
    1.35  
    1.36 -fun dynamic_eval thy cterm_of conclude_evaluation evaluator proto_ct =
    1.37 +fun dynamic_eval_conv thy conv ct =
    1.38    let
    1.39 -    val ctxt = Syntax.init_pretty_global thy;
    1.40 -    val ct = cterm_of proto_ct;
    1.41 -    val _ = (Sign.no_frees ctxt o map_types (K dummyT) o Sign.no_vars ctxt) (Thm.term_of ct);
    1.42 -    val thm = preprocess_conv thy ct;
    1.43 -    val ct' = Thm.rhs_of thm;
    1.44 +    val thm1 = preprocess_conv thy ct;
    1.45 +    val ct' = Thm.rhs_of thm1;
    1.46      val (vs', t') = dest_cterm ct';
    1.47      val consts = fold_aterms
    1.48        (fn Const (c, _) => insert (op =) c | _ => I) t' [];
    1.49      val (algebra', eqngr') = obtain false thy consts [t'];
    1.50 -  in conclude_evaluation (evaluator algebra' eqngr' vs' t' ct') thm end;
    1.51 +    val thm2 = conv algebra' eqngr' vs' t' ct';
    1.52 +    val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
    1.53 +  in
    1.54 +    Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
    1.55 +      error ("could not construct evaluation proof:\n"
    1.56 +      ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
    1.57 +  end;
    1.58  
    1.59 -fun dynamic_eval_conv thy =
    1.60 +fun dynamic_eval_value thy postproc evaluator t =
    1.61    let
    1.62 -    fun conclude_evaluation thm2 thm1 =
    1.63 -      let
    1.64 -        val thm3 = postprocess_conv thy (Thm.rhs_of thm2);
    1.65 -      in
    1.66 -        Thm.transitive thm1 (Thm.transitive thm2 thm3) handle THM _ =>
    1.67 -          error ("could not construct evaluation proof:\n"
    1.68 -          ^ (cat_lines o map (Display.string_of_thm_global thy)) [thm1, thm2, thm3])
    1.69 -      end;
    1.70 -  in dynamic_eval thy I conclude_evaluation end;
    1.71 -
    1.72 -fun dynamic_eval_value thy postproc evaluator = dynamic_eval thy (Thm.cterm_of thy)
    1.73 -  (K o postproc (postprocess_term thy)) (K oooo evaluator);
    1.74 +    val t' = preprocess_term thy t;
    1.75 +    val vs' = Term.add_tfrees t' [];
    1.76 +    val consts = fold_aterms
    1.77 +      (fn Const (c, _) => insert (op =) c | _ => I) t' [];
    1.78 +    val (algebra', eqngr') = obtain false thy consts [t'];
    1.79 +    val result = evaluator algebra' eqngr' vs' t';
    1.80 +  in
    1.81 +    evaluator algebra' eqngr' vs' t'
    1.82 +    |> postproc (postprocess_term thy)
    1.83 +  end;
    1.84  
    1.85  fun static_eval_conv thy consts conv =
    1.86    let
    1.87      val (algebra, eqngr) = obtain true thy consts [];
    1.88 +    val conv' = conv algebra eqngr;
    1.89    in
    1.90      Conv.tap_thy (fn thy => (preprocess_conv thy)
    1.91 -      then_conv (fn ct => uncurry (conv algebra eqngr) (dest_cterm ct) ct)
    1.92 +      then_conv (fn ct => uncurry (conv' thy) (dest_cterm ct) ct)
    1.93        then_conv (postprocess_conv thy))
    1.94    end;
    1.95  
    1.96 +fun static_eval_value thy postproc consts evaluator =
    1.97 +  let
    1.98 +    val (algebra, eqngr) = obtain true thy consts [];
    1.99 +    val evaluator' = evaluator algebra eqngr;
   1.100 +  in fn t =>
   1.101 +    t
   1.102 +    |> preprocess_term thy
   1.103 +    |> (fn t => evaluator' thy (Term.add_tfrees t [])  t)
   1.104 +    |> postproc (postprocess_term thy)
   1.105 +  end;
   1.106 +
   1.107  
   1.108  (** setup **)
   1.109  
     2.1 --- a/src/Tools/Code/code_simp.ML	Thu Sep 16 16:51:34 2010 +0200
     2.2 +++ b/src/Tools/Code/code_simp.ML	Thu Sep 16 16:51:34 2010 +0200
     2.3 @@ -84,7 +84,8 @@
     2.4  (* evaluation with freezed code context *)
     2.5  
     2.6  fun static_eval_conv thy some_ss consts = no_frees_conv
     2.7 -  (Code_Thingol.static_eval_conv_simple thy consts (rewrite_modulo thy some_ss));
     2.8 +  (Code_Thingol.static_eval_conv_simple thy consts
     2.9 +    (fn program => fn thy => rewrite_modulo thy some_ss program));
    2.10  
    2.11  fun static_eval_tac thy some_ss consts = CONVERSION (static_eval_conv thy some_ss consts)
    2.12    THEN' conclude_tac thy some_ss;
     3.1 --- a/src/Tools/Code/code_thingol.ML	Thu Sep 16 16:51:34 2010 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Sep 16 16:51:34 2010 +0200
     3.3 @@ -99,10 +99,13 @@
     3.4      -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
     3.5      -> term -> 'a
     3.6    val static_eval_conv: theory -> string list
     3.7 -    -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
     3.8 +    -> (naming -> program -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> conv)
     3.9      -> conv
    3.10    val static_eval_conv_simple: theory -> string list
    3.11 -    -> (program -> conv) -> conv
    3.12 +    -> (program -> theory -> conv) -> conv
    3.13 +  val static_eval_value: theory -> ((term -> term) -> 'a -> 'a) -> string list
    3.14 +    -> (naming -> program -> theory -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
    3.15 +    -> term -> 'a
    3.16  end;
    3.17  
    3.18  structure Code_Thingol: CODE_THINGOL =
    3.19 @@ -884,25 +887,34 @@
    3.20      #> term_value
    3.21    end;
    3.22  
    3.23 -fun base_evaluator thy evaluator algebra eqngr vs t =
    3.24 +fun base_evaluator evaluator algebra eqngr thy vs t =
    3.25    let
    3.26      val (((naming, program), (((vs', ty'), t'), deps)), _) =
    3.27        invoke_generation false thy (algebra, eqngr) ensure_value t;
    3.28      val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
    3.29 -  in evaluator naming program ((vs'', (vs', ty')), t') deps end;
    3.30 +  in evaluator naming program thy ((vs'', (vs', ty')), t') deps end;
    3.31 +
    3.32 +fun dynamic_evaluator thy evaluator algebra eqngr vs t =
    3.33 +  base_evaluator (fn naming => fn program => fn _ => evaluator naming program) algebra eqngr thy vs t;
    3.34  
    3.35 -fun dynamic_eval_conv thy = Code_Preproc.dynamic_eval_conv thy o base_evaluator thy;
    3.36 -fun dynamic_eval_value thy postproc = Code_Preproc.dynamic_eval_value thy postproc o base_evaluator thy;
    3.37 +fun dynamic_eval_conv thy evaluator =
    3.38 +  Code_Preproc.dynamic_eval_conv thy (dynamic_evaluator thy evaluator);
    3.39 +
    3.40 +fun dynamic_eval_value thy postproc evaluator =
    3.41 +  Code_Preproc.dynamic_eval_value thy postproc (dynamic_evaluator thy evaluator);
    3.42  
    3.43  fun static_eval_conv thy consts conv =
    3.44 -  Code_Preproc.static_eval_conv thy consts (base_evaluator thy conv); (*FIXME avoid re-generation*)
    3.45 +  Code_Preproc.static_eval_conv thy consts (base_evaluator conv); (*FIXME avoid re-generation*)
    3.46  
    3.47  fun static_eval_conv_simple thy consts conv =
    3.48 -  Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn _ => fn _ => fn ct =>
    3.49 +  Code_Preproc.static_eval_conv thy consts (fn algebra => fn eqngr => fn thy => fn _ => fn _ => fn ct =>
    3.50      conv ((NONE, (empty_naming, Graph.empty)) (*FIXME provide abstraction for this kind of invocation*)
    3.51        |> fold_map (ensure_const thy algebra eqngr false) consts
    3.52 -      |> (snd o snd o snd)) ct);
    3.53 +      |> (snd o snd o snd)) thy ct);
    3.54  
    3.55 +fun static_eval_value thy postproc consts conv =
    3.56 +  Code_Preproc.static_eval_value thy postproc consts (base_evaluator conv); (*FIXME avoid re-generation*)
    3.57 +  
    3.58  
    3.59  (** diagnostic commands **)
    3.60  
     4.1 --- a/src/Tools/nbe.ML	Thu Sep 16 16:51:34 2010 +0200
     4.2 +++ b/src/Tools/nbe.ML	Thu Sep 16 16:51:34 2010 +0200
     4.3 @@ -609,7 +609,8 @@
     4.4  
     4.5  fun static_eval_conv thy consts = Code_Simp.no_frees_conv
     4.6    (lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
     4.7 -    (K (fn program => oracle thy program (compile true thy program)))));
     4.8 +    (K (fn program => let val nbe_program = compile true thy program
     4.9 +      in fn thy => oracle thy program nbe_program end))));
    4.10  
    4.11  
    4.12  (** setup **)