also adding type annotations for the dynamic invocation
authorbulwahn
Mon Sep 19 16:18:18 2011 +0200 (2011-09-19)
changeset 44996410eea28b0f7
parent 44995 eff5bccc9b76
child 44997 e534939f880d
also adding type annotations for the dynamic invocation
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Sep 19 14:35:51 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:18 2011 +0200
     1.3 @@ -600,22 +600,19 @@
     1.4    | annotate_term (Var _, t as Var _) tvar_names = (t, tvar_names)
     1.5    | annotate_term (Bound   _, t as Bound _) tvar_names = (t, tvar_names)
     1.6  
     1.7 -fun annotate_eqns thy (c, ty) eqns = 
     1.8 +fun annotate thy (c, ty) args rhs =
     1.9    let
    1.10      val ctxt = ProofContext.init_global thy |> Config.put Type_Infer_Context.const_sorts false
    1.11      val erase = map_types (fn _ => Type_Infer.anyT [])
    1.12      val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
    1.13 -    fun add_annotations (args, (rhs, some_abs)) =
    1.14 -      let
    1.15 -        val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
    1.16 -        val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
    1.17 -        val (rhs', _) = annotate_term (reinferred_rhs, rhs) []
    1.18 -     in
    1.19 -        (args, (rhs', some_abs))
    1.20 -     end
    1.21 +    val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
    1.22 +    val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
    1.23    in
    1.24 -    map (apfst add_annotations) eqns
    1.25 -  end;
    1.26 +    fst (annotate_term (reinferred_rhs, rhs) [])
    1.27 +  end
    1.28 +
    1.29 +fun annotate_eqns thy (c, ty) eqns = 
    1.30 +  map (apfst (fn (args, (rhs, some_abs)) => (args, (annotate thy (c, ty) args rhs, some_abs)))) eqns
    1.31  
    1.32  (* translation *)
    1.33  
    1.34 @@ -922,10 +919,11 @@
    1.35      val ty = fastype_of t;
    1.36      val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
    1.37        o dest_TFree))) t [];
    1.38 +    val t' = annotate thy (Term.dummy_patternN, ty) [] (Code.subst_signatures thy t) 
    1.39      val stmt_value =
    1.40        fold_map (translate_tyvar_sort thy algbr eqngr false) vs
    1.41        ##>> translate_typ thy algbr eqngr false ty
    1.42 -      ##>> translate_term thy algbr eqngr false NONE (Code.subst_signatures thy t, NONE)
    1.43 +      ##>> translate_term thy algbr eqngr false NONE (t', NONE)
    1.44        #>> (fn ((vs, ty), t) => Fun
    1.45          (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
    1.46      fun term_value (dep, (naming, program1)) =