adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used
authorbulwahn
Mon Sep 19 16:18:21 2011 +0200 (2011-09-19)
changeset 4499904b794da039e
parent 44998 f12ef61ea76e
child 45000 0febe2089425
adding type annotations more aggressively and redundantly to make code generation more reliable even when special printers for some constants are used
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:19 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:21 2011 +0200
     1.3 @@ -589,27 +589,16 @@
     1.4  fun annotate_term (proj_sort, _) eqngr =
     1.5    let
     1.6      val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr
     1.7 -    fun annotate (Const (c', T'), Const (c, T)) tvar_names =
     1.8 -      let
     1.9 -        val tvar_names' = Term.add_tvar_namesT T' tvar_names
    1.10 -      in
    1.11 -        if not (eq_set (op =) (tvar_names, tvar_names')) andalso has_sort_constraints c then
    1.12 -          (Const (c, Type ("", [T])), tvar_names')
    1.13 +    fun annotate (Const (c', T'), Const (c, T)) =
    1.14 +        if not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c then
    1.15 +          Const (c, Type ("", [T]))
    1.16          else
    1.17 -          (Const (c, T), tvar_names)
    1.18 -      end
    1.19 -      | annotate (t1 $ u1, t $ u) tvar_names =
    1.20 -      let
    1.21 -        val (u', tvar_names') = annotate (u1, u) tvar_names
    1.22 -        val (t', tvar_names'') = annotate (t1, t) tvar_names'    
    1.23 -      in
    1.24 -        (t' $ u', tvar_names'')
    1.25 -      end
    1.26 -      | annotate (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
    1.27 -        apfst (fn t => Abs (x, T, t)) (annotate (t1, t) tvar_names)
    1.28 -      | annotate (Free _, t as Free _) tvar_names = (t, tvar_names)
    1.29 -      | annotate (Var _, t as Var _) tvar_names = (t, tvar_names)
    1.30 -      | annotate (Bound   _, t as Bound _) tvar_names = (t, tvar_names)
    1.31 +          Const (c, T)
    1.32 +      | annotate (t1 $ u1, t $ u) = annotate (t1, t) $ annotate (u1, u)
    1.33 +      | annotate (Abs (_, _, t1) , Abs (x, T, t)) = Abs (x, T, annotate (t1, t))
    1.34 +      | annotate (Free _, t as Free _) = t
    1.35 +      | annotate (Var _, t as Var _) = t
    1.36 +      | annotate (Bound   _, t as Bound _) = t
    1.37    in
    1.38      annotate
    1.39    end
    1.40 @@ -622,7 +611,7 @@
    1.41      val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
    1.42      val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
    1.43    in
    1.44 -    fst (annotate_term algbr eqngr (reinferred_rhs, rhs) [])
    1.45 +    annotate_term algbr eqngr (reinferred_rhs, rhs)
    1.46    end
    1.47  
    1.48  fun annotate_eqns thy algbr eqngr (c, ty) eqns =