dropped obscure type argument weakening mapping -- was only a misunderstanding
authorhaftmann
Thu Jun 17 10:51:38 2010 +0200 (2010-06-17)
changeset 37445e372fa3c7239
parent 37444 2e7e7ff21e25
child 37446 fc55011cfdfd
dropped obscure type argument weakening mapping -- was only a misunderstanding
src/Tools/Code/code_ml.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Jun 17 10:45:10 2010 +0200
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jun 17 10:51:38 2010 +0200
     1.3 @@ -32,7 +32,7 @@
     1.4  datatype ml_binding =
     1.5      ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     1.6    | ML_Instance of string * ((class * (string * (vname * sort) list))
     1.7 -        * (((class * (string * (string * dict list list))) list * (class * class) list list)
     1.8 +        * ((class * (string * (string * dict list list))) list
     1.9        * ((string * const) * (thm * bool)) list));
    1.10  
    1.11  datatype ml_stmt =
    1.12 @@ -219,7 +219,7 @@
    1.13              ))
    1.14            end
    1.15        | print_def is_pseudo_fun _ definer
    1.16 -          (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
    1.17 +          (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
    1.18            let
    1.19              fun print_super_instance (_, (classrel, dss)) =
    1.20                concat [
    1.21 @@ -554,7 +554,7 @@
    1.22              ))
    1.23            end
    1.24        | print_def is_pseudo_fun _ definer
    1.25 -            (ML_Instance (inst, ((class, (tyco, vs)), ((super_instances, _), classparam_instances)))) =
    1.26 +            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, classparam_instances)))) =
    1.27            let
    1.28              fun print_super_instance (_, (classrel, dss)) =
    1.29                concat [
     2.1 --- a/src/Tools/Code/code_scala.ML	Thu Jun 17 10:45:10 2010 +0200
     2.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jun 17 10:51:38 2010 +0200
     2.3 @@ -252,7 +252,7 @@
     2.4              )
     2.5            end
     2.6        | print_stmt (name, Code_Thingol.Classinst ((class, (tyco, vs)),
     2.7 -            ((super_instances, _), classparam_instances))) =
     2.8 +            (super_instances, classparam_instances))) =
     2.9            let
    2.10              val tyvars = intro_vars (map fst vs) reserved;
    2.11              val insttyp = tyco `%% map (ITyVar o fst) vs;
     3.1 --- a/src/Tools/Code/code_thingol.ML	Thu Jun 17 10:45:10 2010 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jun 17 10:51:38 2010 +0200
     3.3 @@ -73,8 +73,7 @@
     3.4      | Classrel of class * class
     3.5      | Classparam of string * class
     3.6      | Classinst of (class * (string * (vname * sort) list) (*class and arity*) )
     3.7 -          * (((class * (string * (string * dict list list))) list (*super instances*)
     3.8 -            * (class * class) list list (*type argument weakening mapping*))
     3.9 +          * ((class * (string * (string * dict list list))) list (*super instances*)
    3.10          * ((string * const) * (thm * bool)) list (*class parameter instances*))
    3.11    type program = stmt Graph.T
    3.12    val empty_funs: program -> string list
    3.13 @@ -410,8 +409,7 @@
    3.14    | Classrel of class * class
    3.15    | Classparam of string * class
    3.16    | Classinst of (class * (string * (vname * sort) list))
    3.17 -        * (((class * (string * (string * dict list list))) list
    3.18 -          * (class * class) list list)
    3.19 +        * ((class * (string * (string * dict list list))) list
    3.20        * ((string * const) * (thm * bool)) list) (*see also signature*);
    3.21  
    3.22  type program = stmt Graph.T;
    3.23 @@ -438,8 +436,8 @@
    3.24    | map_terms_stmt f (stmt as Class _) = stmt
    3.25    | map_terms_stmt f (stmt as Classrel _) = stmt
    3.26    | map_terms_stmt f (stmt as Classparam _) = stmt
    3.27 -  | map_terms_stmt f (Classinst (arity, ((super_instances, weakening), classparams))) =
    3.28 -      Classinst (arity, ((super_instances, weakening), (map o apfst o apsnd) (fn const =>
    3.29 +  | map_terms_stmt f (Classinst (arity, (super_instances, classparams))) =
    3.30 +      Classinst (arity, (super_instances, (map o apfst o apsnd) (fn const =>
    3.31          case f (IConst const) of IConst const' => const') classparams));
    3.32  
    3.33  fun is_cons program name = case Graph.get_node program name
    3.34 @@ -640,7 +638,7 @@
    3.35        ##>> fold_map translate_super_instance super_classes
    3.36        ##>> fold_map translate_classparam_instance classparams
    3.37        #>> (fn ((((class, tyco), arity_args), super_instances), classparam_instances) =>
    3.38 -             Classinst ((class, (tyco, arity_args)), ((super_instances, []), classparam_instances)));
    3.39 +             Classinst ((class, (tyco, arity_args)), (super_instances, classparam_instances)));
    3.40    in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
    3.41  and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
    3.42        pair (ITyVar (unprefix "'" v))
     4.1 --- a/src/Tools/nbe.ML	Thu Jun 17 10:45:10 2010 +0200
     4.2 +++ b/src/Tools/nbe.ML	Thu Jun 17 10:51:38 2010 +0200
     4.3 @@ -417,7 +417,7 @@
     4.4        []
     4.5    | eqns_of_stmt (_, Code_Thingol.Classparam _) =
     4.6        []
     4.7 -  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), ((super_instances, _), classparam_instances))) =
     4.8 +  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, classparam_instances))) =
     4.9        [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
    4.10          map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
    4.11          @ map (IConst o snd o fst) classparam_instances)]))];