only annotating constants with sort constraints
authorbulwahn
Mon Sep 19 16:18:19 2011 +0200 (2011-09-19)
changeset 44997e534939f880d
parent 44996 410eea28b0f7
child 44998 f12ef61ea76e
only annotating constants with sort constraints
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:18 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:19 2011 +0200
     1.3 @@ -581,26 +581,35 @@
     1.4  
     1.5  (* inference of type annotations for disambiguation with type classes *)
     1.6  
     1.7 -fun annotate_term (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 -      (Const (c, if eq_set (op =) (tvar_names, tvar_names') then T else Type("", [T])), tvar_names')
    1.12 -    end
    1.13 -  | annotate_term (t1 $ u1, t $ u) tvar_names =
    1.14 -    let
    1.15 -      val (u', tvar_names') = annotate_term (u1, u) tvar_names
    1.16 -      val (t', tvar_names'') = annotate_term (t1, t) tvar_names'    
    1.17 -    in
    1.18 -      (t' $ u', tvar_names'')
    1.19 -    end
    1.20 -  | annotate_term (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
    1.21 -    apfst (fn t => Abs (x, T, t)) (annotate_term (t1, t) tvar_names)
    1.22 -  | annotate_term (Free _, t as Free _) tvar_names = (t, tvar_names)
    1.23 -  | annotate_term (Var _, t as Var _) tvar_names = (t, tvar_names)
    1.24 -  | annotate_term (Bound   _, t as Bound _) tvar_names = (t, tvar_names)
    1.25 +fun annotate_term (proj_sort, _) eqngr =
    1.26 +  let
    1.27 +    val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr
    1.28 +    fun annotate (Const (c', T'), Const (c, T)) tvar_names =
    1.29 +      let
    1.30 +        val tvar_names' = Term.add_tvar_namesT T' tvar_names
    1.31 +      in
    1.32 +        if not (eq_set (op =) (tvar_names, tvar_names')) andalso has_sort_constraints c then
    1.33 +          (Const (c, Type ("", [T])), tvar_names')
    1.34 +        else
    1.35 +          (Const (c, T), tvar_names)
    1.36 +      end
    1.37 +      | annotate (t1 $ u1, t $ u) tvar_names =
    1.38 +      let
    1.39 +        val (u', tvar_names') = annotate (u1, u) tvar_names
    1.40 +        val (t', tvar_names'') = annotate (t1, t) tvar_names'    
    1.41 +      in
    1.42 +        (t' $ u', tvar_names'')
    1.43 +      end
    1.44 +      | annotate (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
    1.45 +        apfst (fn t => Abs (x, T, t)) (annotate (t1, t) tvar_names)
    1.46 +      | annotate (Free _, t as Free _) tvar_names = (t, tvar_names)
    1.47 +      | annotate (Var _, t as Var _) tvar_names = (t, tvar_names)
    1.48 +      | annotate (Bound   _, t as Bound _) tvar_names = (t, tvar_names)
    1.49 +  in
    1.50 +    annotate
    1.51 +  end
    1.52  
    1.53 -fun annotate thy (c, ty) args rhs =
    1.54 +fun annotate thy algbr eqngr (c, ty) args rhs =
    1.55    let
    1.56      val ctxt = ProofContext.init_global thy |> Config.put Type_Infer_Context.const_sorts false
    1.57      val erase = map_types (fn _ => Type_Infer.anyT [])
    1.58 @@ -608,11 +617,12 @@
    1.59      val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
    1.60      val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
    1.61    in
    1.62 -    fst (annotate_term (reinferred_rhs, rhs) [])
    1.63 +    fst (annotate_term algbr eqngr (reinferred_rhs, rhs) [])
    1.64    end
    1.65  
    1.66 -fun annotate_eqns thy (c, ty) eqns = 
    1.67 -  map (apfst (fn (args, (rhs, some_abs)) => (args, (annotate thy (c, ty) args rhs, some_abs)))) eqns
    1.68 +fun annotate_eqns thy algbr eqngr (c, ty) eqns = 
    1.69 +  map (apfst (fn (args, (rhs, some_abs)) => (args,
    1.70 +    (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns
    1.71  
    1.72  (* translation *)
    1.73  
    1.74 @@ -638,7 +648,7 @@
    1.75      fun stmt_fun cert =
    1.76        let
    1.77          val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
    1.78 -        val eqns' = annotate_eqns thy (c, ty) eqns
    1.79 +        val eqns' = annotate_eqns thy algbr eqngr (c, ty) eqns
    1.80          val some_case_cong = Code.get_case_cong thy c;
    1.81        in
    1.82          fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
    1.83 @@ -919,7 +929,7 @@
    1.84      val ty = fastype_of t;
    1.85      val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
    1.86        o dest_TFree))) t [];
    1.87 -    val t' = annotate thy (Term.dummy_patternN, ty) [] (Code.subst_signatures thy t) 
    1.88 +    val t' = annotate thy algbr eqngr (Term.dummy_patternN, ty) [] (Code.subst_signatures thy t) 
    1.89      val stmt_value =
    1.90        fold_map (translate_tyvar_sort thy algbr eqngr false) vs
    1.91        ##>> translate_typ thy algbr eqngr false ty