integrated add_triv_classes into evaluation stack
authorhaftmann
Tue Jul 21 15:44:31 2009 +0200 (2009-07-21)
changeset 321238bac9ee4b28d
parent 32122 4ee1c1aebbcc
child 32124 954321008785
integrated add_triv_classes into evaluation stack
src/Tools/Code/code_ml.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_ml.ML	Tue Jul 21 15:44:31 2009 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Tue Jul 21 15:44:31 2009 +0200
     1.3 @@ -966,7 +966,7 @@
     1.4          val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
     1.5            ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
     1.6        in ML_Context.evaluate ctxt false reff sml_code end;
     1.7 -  in Code_Thingol.eval thy I postproc evaluator t end;
     1.8 +  in Code_Thingol.eval thy postproc evaluator t end;
     1.9  
    1.10  
    1.11  (* instrumentalization by antiquotation *)
     2.1 --- a/src/Tools/Code/code_preproc.ML	Tue Jul 21 15:44:31 2009 +0200
     2.2 +++ b/src/Tools/Code/code_preproc.ML	Tue Jul 21 15:44:31 2009 +0200
     2.3 @@ -23,9 +23,10 @@
     2.4    val all: code_graph -> string list
     2.5    val pretty: theory -> code_graph -> Pretty.T
     2.6    val obtain: theory -> string list -> term list -> code_algebra * code_graph
     2.7 -  val eval_conv: theory -> (sort -> sort)
     2.8 +  val resubst_triv_consts: theory -> term -> term
     2.9 +  val eval_conv: theory
    2.10      -> (code_algebra -> code_graph -> (string * sort) list -> term -> cterm -> thm) -> cterm -> thm
    2.11 -  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
    2.12 +  val eval: theory -> ((term -> term) -> 'a -> 'a)
    2.13      -> (code_algebra -> code_graph -> (string * sort) list -> term -> 'a) -> term -> 'a
    2.14  
    2.15    val setup: theory -> theory
    2.16 @@ -161,7 +162,10 @@
    2.17      |> rhs_conv (Simplifier.rewrite post)
    2.18    end;
    2.19  
    2.20 -fun postprocess_term thy = term_of_conv thy (postprocess_conv thy);
    2.21 +fun resubst_triv_consts thy = map_aterms (fn t as Const (c, ty) => Const (Code.resubst_alias thy c, ty)
    2.22 +  | t => t);
    2.23 +
    2.24 +fun postprocess_term thy = term_of_conv thy (postprocess_conv thy) #> resubst_triv_consts thy;
    2.25  
    2.26  fun print_codeproc thy =
    2.27    let
    2.28 @@ -495,7 +499,7 @@
    2.29        Abs (v, prepare_sorts_typ prep_sort ty, prepare_sorts prep_sort t)
    2.30    | prepare_sorts _ (t as Bound _) = t;
    2.31  
    2.32 -fun gen_eval thy cterm_of conclude_evaluation prep_sort evaluator proto_ct =
    2.33 +fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
    2.34    let
    2.35      val pp = Syntax.pp_global thy;
    2.36      val ct = cterm_of proto_ct;
    2.37 @@ -507,8 +511,10 @@
    2.38      val vs = Term.add_tfrees t' [];
    2.39      val consts = fold_aterms
    2.40        (fn Const (c, _) => insert (op =) c | _ => I) t' [];
    2.41 - 
    2.42 -    val t'' = prepare_sorts prep_sort t';
    2.43 +
    2.44 +    val add_triv_classes = curry (Sorts.inter_sort (Sign.classes_of thy))
    2.45 +      (Code.triv_classes thy);
    2.46 +    val t'' = prepare_sorts add_triv_classes t';
    2.47      val (algebra', eqngr') = obtain thy consts [t''];
    2.48    in conclude_evaluation (evaluator algebra' eqngr' vs t'' ct') thm end;
    2.49  
    2.50 @@ -527,8 +533,8 @@
    2.51        end;
    2.52    in gen_eval thy I conclude_evaluation end;
    2.53  
    2.54 -fun eval thy prep_sort postproc evaluator = gen_eval thy (Thm.cterm_of thy)
    2.55 -  (K o postproc (postprocess_term thy)) prep_sort (simple_evaluator evaluator);
    2.56 +fun eval thy postproc evaluator = gen_eval thy (Thm.cterm_of thy)
    2.57 +  (K o postproc (postprocess_term thy)) (simple_evaluator evaluator);
    2.58  
    2.59  
    2.60  (** setup **)
     3.1 --- a/src/Tools/Code/code_thingol.ML	Tue Jul 21 15:44:31 2009 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Jul 21 15:44:31 2009 +0200
     3.3 @@ -82,10 +82,10 @@
     3.4    val read_const_exprs: theory -> string list -> string list * string list
     3.5    val consts_program: theory -> string list -> string list * (naming * program)
     3.6    val cached_program: theory -> naming * program
     3.7 -  val eval_conv: theory -> (sort -> sort)
     3.8 +  val eval_conv: theory
     3.9      -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> cterm -> thm)
    3.10      -> cterm -> thm
    3.11 -  val eval: theory -> (sort -> sort) -> ((term -> term) -> 'a -> 'a)
    3.12 +  val eval: theory -> ((term -> term) -> 'a -> 'a)
    3.13      -> (naming -> program -> ((string * sort) list * typscheme) * iterm -> string list -> 'a)
    3.14      -> term -> 'a
    3.15  end;
    3.16 @@ -803,8 +803,8 @@
    3.17      val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
    3.18    in evaluator naming program ((vs'', (vs', ty')), t') deps end;
    3.19  
    3.20 -fun eval_conv thy prep_sort = Code_Preproc.eval_conv thy prep_sort o base_evaluator thy;
    3.21 -fun eval thy prep_sort postproc = Code_Preproc.eval thy prep_sort postproc o base_evaluator thy;
    3.22 +fun eval_conv thy = Code_Preproc.eval_conv thy o base_evaluator thy;
    3.23 +fun eval thy postproc = Code_Preproc.eval thy postproc o base_evaluator thy;
    3.24  
    3.25  
    3.26  (** diagnostic commands **)
     4.1 --- a/src/Tools/nbe.ML	Tue Jul 21 15:44:31 2009 +0200
     4.2 +++ b/src/Tools/nbe.ML	Tue Jul 21 15:44:31 2009 +0200
     4.3 @@ -439,9 +439,6 @@
     4.4  
     4.5  fun normalize thy naming program ((vs0, (vs, ty)), t) deps =
     4.6    let
     4.7 -    fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
     4.8 -      | t => t);
     4.9 -    val resubst_triv_consts = subst_const (Code.resubst_alias thy);
    4.10      val ty' = typ_of_itype program vs0 ty;
    4.11      fun type_infer t =
    4.12        singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
    4.13 @@ -453,8 +450,8 @@
    4.14      val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);
    4.15    in
    4.16      compile_eval thy naming program (vs, t) deps
    4.17 +    |> Code_Preproc.resubst_triv_consts thy
    4.18      |> tracing (fn t => "Normalized:\n" ^ string_of_term t)
    4.19 -    |> resubst_triv_consts
    4.20      |> type_infer
    4.21      |> tracing (fn t => "Types inferred:\n" ^ string_of_term t)
    4.22      |> check_tvars
    4.23 @@ -463,9 +460,6 @@
    4.24  
    4.25  (* evaluation oracle *)
    4.26  
    4.27 -fun add_triv_classes thy = curry (Sorts.inter_sort (Sign.classes_of thy))
    4.28 -  (Code.triv_classes thy);
    4.29 -
    4.30  fun mk_equals thy lhs raw_rhs =
    4.31    let
    4.32      val ty = Thm.typ_of (Thm.ctyp_of_term lhs);
    4.33 @@ -506,9 +500,9 @@
    4.34  val norm_conv = no_frees_conv (fn ct =>
    4.35    let
    4.36      val thy = Thm.theory_of_cterm ct;
    4.37 -  in Code_Thingol.eval_conv thy (add_triv_classes thy) (norm_oracle thy) ct end);
    4.38 +  in Code_Thingol.eval_conv thy (norm_oracle thy) ct end);
    4.39  
    4.40 -fun norm thy = no_frees_rew (Code_Thingol.eval thy (add_triv_classes thy) I (normalize thy));
    4.41 +fun norm thy = no_frees_rew (Code_Thingol.eval thy I (normalize thy));
    4.42  
    4.43  (* evaluation command *)
    4.44