transitive superclasses were also only a misunderstanding
authorhaftmann
Thu Jun 17 11:33:04 2010 +0200 (2010-06-17)
changeset 37447ad3e04f289b6
parent 37446 fc55011cfdfd
child 37448 3bd4b3809bee
transitive superclasses were also only a misunderstanding
src/Tools/Code/code_haskell.ML
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_haskell.ML	Thu Jun 17 10:57:00 2010 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Jun 17 11:33:04 2010 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4                @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
     1.5              )
     1.6            end
     1.7 -      | print_stmt (name, Code_Thingol.Class (_, (v, ((super_classes, _), classparams)))) =
     1.8 +      | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
     1.9            let
    1.10              val tyvars = intro_vars [v] reserved;
    1.11              fun print_classparam (classparam, ty) =
     2.1 --- a/src/Tools/Code/code_ml.ML	Thu Jun 17 10:57:00 2010 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jun 17 11:33:04 2010 +0200
     2.3 @@ -40,7 +40,7 @@
     2.4    | ML_Val of ml_binding
     2.5    | ML_Funs of ml_binding list * string list
     2.6    | ML_Datas of (string * ((vname * sort) list * (string * itype list) list)) list
     2.7 -  | ML_Class of string * (vname * (((class * string) list * (class * string) list) * (string * itype) list));
     2.8 +  | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
     2.9  
    2.10  fun stmt_name_of_binding (ML_Function (name, _)) = name
    2.11    | stmt_name_of_binding (ML_Instance (name, _)) = name;
    2.12 @@ -301,7 +301,7 @@
    2.13              sig_ps
    2.14              (Pretty.chunks (ps @| semicolon [p]))
    2.15            end
    2.16 -     | print_stmt (ML_Class (class, (v, ((super_classes, _), classparams)))) =
    2.17 +     | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
    2.18            let
    2.19              fun print_field s p = concat [str s, str ":", p];
    2.20              fun print_proj s p = semicolon
    2.21 @@ -635,7 +635,7 @@
    2.22              sig_ps
    2.23              (Pretty.chunks (ps @| doublesemicolon [p]))
    2.24            end
    2.25 -     | print_stmt (ML_Class (class, (v, ((super_classes, _), classparams)))) =
    2.26 +     | print_stmt (ML_Class (class, (v, (super_classes, classparams)))) =
    2.27            let
    2.28              fun print_field s p = concat [str s, str ":", p];
    2.29              fun print_super_class_field (super_class, classrel) =
     3.1 --- a/src/Tools/Code/code_scala.ML	Thu Jun 17 10:57:00 2010 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jun 17 11:33:04 2010 +0200
     3.3 @@ -212,7 +212,7 @@
     3.4                :: map print_co cos
     3.5              )
     3.6            end
     3.7 -      | print_stmt (name, Code_Thingol.Class (_, (v, ((super_classes, all_super_classes), classparams)))) =
     3.8 +      | print_stmt (name, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
     3.9            let
    3.10              val tyvars = intro_vars [v] reserved;
    3.11              val vs = [(v, [name])];
     4.1 --- a/src/Tools/Code/code_thingol.ML	Thu Jun 17 10:57:00 2010 +0200
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jun 17 11:33:04 2010 +0200
     4.3 @@ -69,13 +69,10 @@
     4.4      | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
     4.5      | Datatype of string * ((vname * sort) list * (string * itype list) list)
     4.6      | Datatypecons of string * string
     4.7 -    | Class of class * (vname
     4.8 -        * (((class * string) list (*direct superclasses*)
     4.9 -          * (class * string) list) (*indirect superclasses*)
    4.10 -            * (string * itype) list (*class operations*)))
    4.11 +    | Class of class * (vname * ((class * string) list * (string * itype) list))
    4.12      | Classrel of class * class
    4.13      | Classparam of string * class
    4.14 -    | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
    4.15 +    | Classinst of (class * (string * (vname * sort) list) (*class and arity*) )
    4.16            * ((class * (string * (string * dict list list))) list (*super instances*)
    4.17          * ((string * const) * (thm * bool)) list (*class parameter instances*))
    4.18    type program = stmt Graph.T
    4.19 @@ -403,17 +400,17 @@
    4.20  (** statements, abstract programs **)
    4.21  
    4.22  type typscheme = (vname * sort) list * itype;
    4.23 -datatype stmt = (*see also signature*)
    4.24 +datatype stmt =
    4.25      NoStmt
    4.26    | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
    4.27    | Datatype of string * ((vname * sort) list * (string * itype list) list)
    4.28    | Datatypecons of string * string
    4.29 -  | Class of class * (vname * (((class * string) list * (class * string) list) * (string * itype) list))
    4.30 +  | Class of class * (vname * ((class * string) list * (string * itype) list))
    4.31    | Classrel of class * class
    4.32    | Classparam of string * class
    4.33    | Classinst of (class * (string * (vname * sort) list))
    4.34          * ((class * (string * (string * dict list list))) list
    4.35 -      * ((string * const) * (thm * bool)) list);
    4.36 +      * ((string * const) * (thm * bool)) list) (*see also signature*);
    4.37  
    4.38  type program = stmt Graph.T;
    4.39  
    4.40 @@ -596,7 +593,6 @@
    4.41      val stmt_class =
    4.42        fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
    4.43          ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
    4.44 -      ##>> pair [] (*FIXME*)
    4.45        ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
    4.46          ##>> translate_typ thy algbr eqngr permissive ty) cs
    4.47        #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
     5.1 --- a/src/Tools/nbe.ML	Thu Jun 17 10:57:00 2010 +0200
     5.2 +++ b/src/Tools/nbe.ML	Thu Jun 17 11:33:04 2010 +0200
     5.3 @@ -404,7 +404,7 @@
     5.4        []
     5.5    | eqns_of_stmt (_, Code_Thingol.Datatype _) =
     5.6        []
     5.7 -  | eqns_of_stmt (class, Code_Thingol.Class (_, (v, ((super_classes, _), classparams)))) =
     5.8 +  | eqns_of_stmt (class, Code_Thingol.Class (_, (v, (super_classes, classparams)))) =
     5.9        let
    5.10          val names = map snd super_classes @ map fst classparams;
    5.11          val params = Name.invent_list [] "d" (length names);