clarified code
authorhaftmann
Thu Dec 21 13:55:15 2006 +0100 (2006-12-21)
changeset 218956cbc0f69a21c
parent 21894 1a0e32ccb8bb
child 21896 9a7949815a84
clarified code
src/Pure/Tools/codegen_consts.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
     1.1 --- a/src/Pure/Tools/codegen_consts.ML	Thu Dec 21 13:55:14 2006 +0100
     1.2 +++ b/src/Pure/Tools/codegen_consts.ML	Thu Dec 21 13:55:15 2006 +0100
     1.3 @@ -106,29 +106,16 @@
     1.4      val inst_signs = (map o apsnd o map_type_tfree) (K ty_inst) cs;
     1.5    in (sort_args, inst_signs) end;
     1.6  
     1.7 -fun disc_typ_of_classop thy (c, [TVar _]) = 
     1.8 -      let
     1.9 -        val class = (the o AxClass.class_of_param thy) c;
    1.10 -        val (v, cs) = AxClass.params_of_class thy class;
    1.11 -      in
    1.12 -        (Logic.varifyT o map_type_tfree (K (TFree (v, [class]))))
    1.13 -          ((the o AList.lookup (op =) cs) c)
    1.14 -      end
    1.15 -  | disc_typ_of_classop thy (c, [TFree _]) = 
    1.16 -      let
    1.17 -        val class = (the o AxClass.class_of_param thy) c;
    1.18 -        val (v, cs) = AxClass.params_of_class thy class;
    1.19 -      in
    1.20 -        (Logic.varifyT o map_type_tfree (K (TFree (v, [class]))))
    1.21 -          ((the o AList.lookup (op =) cs) c)
    1.22 -      end
    1.23 -  | disc_typ_of_classop thy (c, [Type (tyco, _)]) =
    1.24 -      let
    1.25 -        val class = (the o AxClass.class_of_param thy) c;
    1.26 -        val (_, cs) = instance_dict thy (class, tyco);
    1.27 -      in
    1.28 -        Logic.varifyT ((the o AList.lookup (op =) cs) c)
    1.29 -      end;
    1.30 +fun disc_typ_of_classop thy (c, [ty]) = 
    1.31 +  let
    1.32 +    val class = (the o AxClass.class_of_param thy) c;
    1.33 +    val cs = case ty
    1.34 +     of TVar _ => snd (AxClass.params_of_class thy class)
    1.35 +      | TFree _ => snd (AxClass.params_of_class thy class)
    1.36 +      | Type (tyco, _) => snd (instance_dict thy (class, tyco));
    1.37 +  in
    1.38 +    (Logic.varifyT o the o AList.lookup (op =) cs) c
    1.39 +  end;
    1.40  
    1.41  fun disc_typ_of_const thy f (const as (c, [ty])) =
    1.42        if (is_some o AxClass.class_of_param thy) c
     2.1 --- a/src/Pure/Tools/codegen_package.ML	Thu Dec 21 13:55:14 2006 +0100
     2.2 +++ b/src/Pure/Tools/codegen_package.ML	Thu Dec 21 13:55:15 2006 +0100
     2.3 @@ -101,7 +101,7 @@
     2.4  
     2.5  fun ensure_def_class thy (algbr as ((proj_sort, _), _)) funcgr strct class trns =
     2.6    let
     2.7 -    val (v, cs) = (AxClass.params_of_class thy) class;
     2.8 +    val (v, cs) = AxClass.params_of_class thy class;
     2.9      val superclasses = (proj_sort o Sign.super_classes thy) class;
    2.10      val classops' = map (CodegenNames.const thy o CodegenConsts.norm_of_typ thy) cs;
    2.11      val class' = CodegenNames.class thy class;
     3.1 --- a/src/Pure/Tools/codegen_serializer.ML	Thu Dec 21 13:55:14 2006 +0100
     3.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Thu Dec 21 13:55:15 2006 +0100
     3.3 @@ -150,9 +150,9 @@
     3.4    end;
     3.5  
     3.6  fun parse_args f args =
     3.7 -  case f args
     3.8 -   of (x, []) => x
     3.9 -    | (_, _) => error "bad serializer arguments";
    3.10 +  case Scan.read Args.stopper f args
    3.11 +   of SOME x => x
    3.12 +    | NONE => error "bad serializer arguments";
    3.13  
    3.14  
    3.15  (* list and string serializer *)