1.1 --- a/src/Tools/nbe.ML Tue May 18 19:00:55 2010 -0700
1.2 +++ b/src/Tools/nbe.ML Wed May 19 10:14:37 2010 +0200
1.3 @@ -76,7 +76,7 @@
1.4 val get_triv_classes = map fst o Triv_Class_Data.get;
1.5
1.6 val (_, triv_of_class) = Context.>>> (Context.map_theory_result
1.7 - (Thm.add_oracle (Binding.name "triv_of_class", fn (thy, (v, T), class) =>
1.8 + (Thm.add_oracle (Binding.name "triv_of_class", fn (thy, T, class) =>
1.9 Thm.cterm_of thy (Logic.mk_of_class (T, class)))));
1.10
1.11 in
1.12 @@ -84,37 +84,46 @@
1.13 fun lift_triv_classes_conv thy conv ct =
1.14 let
1.15 val algebra = Sign.classes_of thy;
1.16 + val certT = Thm.ctyp_of thy;
1.17 val triv_classes = get_triv_classes thy;
1.18 - val certT = Thm.ctyp_of thy;
1.19 - fun critical_classes sort = filter_out (fn class => Sign.subsort thy (sort, [class])) triv_classes;
1.20 - val vs = Term.add_tfrees (Thm.term_of ct) []
1.21 - |> map_filter (fn (v, sort) => case critical_classes sort
1.22 - of [] => NONE
1.23 - | classes => SOME (v, ((sort, classes), Sorts.inter_sort algebra (triv_classes, sort))));
1.24 - val of_classes = maps (fn (v, ((sort, classes), _)) => map (fn class =>
1.25 - ((v, class), triv_of_class (thy, (v, TVar ((v, 0), sort)), class))) classes
1.26 - @ map (fn class => ((v, class), Thm.of_class (certT (TVar ((v, 0), sort)), class)))
1.27 - sort) vs;
1.28 + fun additional_classes sort = filter_out (fn class => Sorts.sort_le algebra (sort, [class])) triv_classes;
1.29 + fun mk_entry (v, sort) =
1.30 + let
1.31 + val T = TFree (v, sort);
1.32 + val cT = certT T;
1.33 + val triv_sort = additional_classes sort;
1.34 + in
1.35 + (v, (Sorts.inter_sort algebra (sort, triv_sort),
1.36 + (cT, AList.make (fn class => Thm.of_class (cT, class)) sort
1.37 + @ AList.make (fn class => triv_of_class (thy, T, class)) triv_sort)))
1.38 + end;
1.39 + val vs_tab = map mk_entry (Term.add_tfrees (Thm.term_of ct) []);
1.40 + fun instantiate thm =
1.41 + let
1.42 + val cert_tvars = map (certT o TVar) (Term.add_tvars
1.43 + ((fst o Logic.dest_equals o Logic.strip_imp_concl o Thm.prop_of) thm) []);
1.44 + val instantiation =
1.45 + map2 (fn cert_tvar => fn (_, (_, (cT, _))) => (cert_tvar, cT)) cert_tvars vs_tab;
1.46 + in Thm.instantiate (instantiation, []) thm end;
1.47 + fun of_class (TFree (v, _), class) =
1.48 + the (AList.lookup (op =) ((snd o snd o the o AList.lookup (op =) vs_tab) v) class)
1.49 + | of_class (T, _) = error ("Bad type " ^ Syntax.string_of_typ_global thy T);
1.50 fun strip_of_class thm =
1.51 let
1.52 - val prem_props = (Logic.strip_imp_prems o Thm.prop_of) thm;
1.53 - val prem_thms = map (the o AList.lookup (op =) of_classes
1.54 - o apfst (fst o fst o dest_TVar) o Logic.dest_of_class) prem_props;
1.55 - in Drule.implies_elim_list thm prem_thms end;
1.56 + val prems_of_class = Thm.prop_of thm
1.57 + |> Logic.strip_imp_prems
1.58 + |> map (Logic.dest_of_class #> of_class);
1.59 + in fold Thm.elim_implies prems_of_class thm end;
1.60 in
1.61 - (* FIXME avoid legacy operations *)
1.62 ct
1.63 - |> Drule.cterm_rule Thm.varifyT_global
1.64 - |> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) =>
1.65 - (((v, 0), sort), TFree (v, sort'))) vs, []))
1.66 - |> Drule.cterm_rule Thm.legacy_freezeT
1.67 + |> (Drule.cterm_fun o map_types o map_type_tfree)
1.68 + (fn (v, sort) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v))
1.69 |> conv
1.70 + |> Thm.strip_shyps
1.71 |> Thm.varifyT_global
1.72 - |> fold (fn (v, (_, sort')) => Thm.legacy_unconstrainT (certT (TVar ((v, 0), sort')))) vs
1.73 - |> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) =>
1.74 - (((v, 0), []), TVar ((v, 0), sort))) vs, [])
1.75 + |> Thm.unconstrainT
1.76 + |> instantiate
1.77 |> strip_of_class
1.78 - |> Thm.legacy_freezeT
1.79 end;
1.80
1.81 fun lift_triv_classes_rew thy rew t =
1.82 @@ -365,7 +374,7 @@
1.83
1.84 (* code compilation *)
1.85
1.86 -fun compile_eqnss _ gr raw_deps [] = []
1.87 +fun compile_eqnss ctxt gr raw_deps [] = []
1.88 | compile_eqnss ctxt gr raw_deps eqnss =
1.89 let
1.90 val (deps, deps_vals) = split_list (map_filter
1.91 @@ -552,7 +561,7 @@
1.92 |> type_infer
1.93 |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
1.94 |> check_tvars
1.95 - |> traced (fn t => "---\n")
1.96 + |> traced (fn _ => "---\n")
1.97 end;
1.98
1.99