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