1.1 --- a/src/Pure/Isar/code.ML	Thu Jun 17 11:33:04 2010 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Thu Jun 17 15:59:46 2010 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4    val del_eqns: string -> theory -> theory
     1.5    val add_case: thm -> theory -> theory
     1.6    val add_undefined: string -> theory -> theory
     1.7 -  val get_type: theory -> string -> ((string * sort) list * (string * typ list) list)
     1.8 +  val get_type: theory -> string -> ((string * sort) list * ((string * string list) * typ list) list)
     1.9    val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
    1.10    val is_constr: theory -> string -> bool
    1.11    val is_abstr: theory -> string -> bool
    1.12 @@ -429,7 +429,13 @@
    1.13   of SOME (vs, Abstractor spec) => (vs, spec)
    1.14    | _ => error ("Not an abstract type: " ^ tyco);
    1.15   
    1.16 -fun get_type thy = fst o get_type_spec thy;
    1.17 +fun get_type thy tyco =
    1.18 +  let
    1.19 +    val ((vs, cos), _) = get_type_spec thy tyco;
    1.20 +    fun args_of c tys = map (fst o dest_TFree)
    1.21 +      (Sign.const_typargs thy (c, tys ---> Type (tyco, map TFree vs)));
    1.22 +    fun add_typargs (c, tys) = ((c, args_of c tys), tys);
    1.23 +  in (vs, map add_typargs cos) end;
    1.24  
    1.25  fun get_type_of_constr_or_abstr thy c =
    1.26    case (snd o strip_type o const_typ thy) c
    1.27 @@ -1115,7 +1121,7 @@
    1.28      val ([x, y], ctxt) = Name.variants ["A", "A'"] Name.context;
    1.29      val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
    1.30      val (ws, vs) = chop pos zs;
    1.31 -    val T = Logic.unvarifyT_global (const_typ thy case_const);
    1.32 +    val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
    1.33      val Ts = (fst o strip_type) T;
    1.34      val T_cong = nth Ts pos;
    1.35      fun mk_prem z = Free (z, T_cong);
    1.36 @@ -1177,7 +1183,7 @@
    1.37    Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
    1.38  
    1.39  fun datatype_interpretation f = Datatype_Interpretation.interpretation
    1.40 -  (fn (tyco, _) => fn thy => f (tyco, get_type thy tyco) thy);
    1.41 +  (fn (tyco, _) => fn thy => f (tyco, fst (get_type_spec thy tyco)) thy);
    1.42  
    1.43  fun add_datatype proto_constrs thy =
    1.44    let

     2.1 --- a/src/Tools/Code/code_eval.ML	Thu Jun 17 11:33:04 2010 +0200
     2.2 +++ b/src/Tools/Code/code_eval.ML	Thu Jun 17 15:59:46 2010 +0200
     2.3 @@ -122,7 +122,7 @@
     2.4  
     2.5  fun check_datatype thy tyco consts =
     2.6    let
     2.7 -    val constrs = (map fst o snd o Code.get_type thy) tyco;
     2.8 +    val constrs = (map (fst o fst) o snd o Code.get_type thy) tyco;
     2.9      val missing_constrs = subtract (op =) consts constrs;
    2.10      val _ = if null missing_constrs then []
    2.11        else error ("Missing constructor(s) " ^ commas (map quote missing_constrs)

     3.1 --- a/src/Tools/Code/code_thingol.ML	Thu Jun 17 11:33:04 2010 +0200
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jun 17 15:59:46 2010 +0200
     3.3 @@ -67,14 +67,16 @@
     3.4    datatype stmt =
     3.5        NoStmt
     3.6      | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
     3.7 -    | Datatype of string * ((vname * sort) list * (string * itype list) list)
     3.8 +    | Datatype of string * ((vname * sort) list *
     3.9 +        ((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
    3.10      | Datatypecons of string * string
    3.11      | Class of class * (vname * ((class * string) list * (string * itype) list))
    3.12      | Classrel of class * class
    3.13      | Classparam of string * class
    3.14 -    | Classinst of (class * (string * (vname * sort) list) (*class and arity*) )
    3.15 +    | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
    3.16            * ((class * (string * (string * dict list list))) list (*super instances*)
    3.17 -        * ((string * const) * (thm * bool)) list (*class parameter instances*))
    3.18 +        * (((string * const) * (thm * bool)) list (*class parameter instances*)
    3.19 +          * ((string * const) * (thm * bool)) list (*super class parameter instances*)))
    3.20    type program = stmt Graph.T
    3.21    val empty_funs: program -> string list
    3.22    val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
    3.23 @@ -403,14 +405,16 @@
    3.24  datatype stmt =
    3.25      NoStmt
    3.26    | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
    3.27 -  | Datatype of string * ((vname * sort) list * (string * itype list) list)
    3.28 +  | Datatype of string * ((vname * sort) list * ((string * vname list) * itype list) list)
    3.29    | Datatypecons of string * string
    3.30    | Class of class * (vname * ((class * string) list * (string * itype) list))
    3.31    | Classrel of class * class
    3.32    | Classparam of string * class
    3.33    | Classinst of (class * (string * (vname * sort) list))
    3.34          * ((class * (string * (string * dict list list))) list
    3.35 -      * ((string * const) * (thm * bool)) list) (*see also signature*);
    3.36 +      * (((string * const) * (thm * bool)) list
    3.37 +        * ((string * const) * (thm * bool)) list))
    3.38 +      (*see also signature*);
    3.39  
    3.40  type program = stmt Graph.T;
    3.41  
    3.42 @@ -428,6 +432,9 @@
    3.43        (ICase (((map_terms_bottom_up f t, ty), (map o pairself)
    3.44          (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
    3.45  
    3.46 +fun map_classparam_instances_as_term f =
    3.47 +  (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
    3.48 +
    3.49  fun map_terms_stmt f NoStmt = NoStmt
    3.50    | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
    3.51        (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
    3.52 @@ -436,9 +443,8 @@
    3.53    | map_terms_stmt f (stmt as Class _) = stmt
    3.54    | map_terms_stmt f (stmt as Classrel _) = stmt
    3.55    | map_terms_stmt f (stmt as Classparam _) = stmt
    3.56 -  | map_terms_stmt f (Classinst (arity, (super_instances, classparams))) =
    3.57 -      Classinst (arity, (super_instances, (map o apfst o apsnd) (fn const =>
    3.58 -        case f (IConst const) of IConst const' => const') classparams));
    3.59 +  | map_terms_stmt f (Classinst (arity, (super_instances, classparam_instances))) =
    3.60 +      Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances));
    3.61  
    3.62  fun is_cons program name = case Graph.get_node program name
    3.63   of Datatypecons _ => true
    3.64 @@ -557,8 +563,9 @@
    3.65      val (vs, cos) = Code.get_type thy tyco;
    3.66      val stmt_datatype =
    3.67        fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
    3.68 -      ##>> fold_map (fn (c, tys) =>
    3.69 +      ##>> fold_map (fn ((c, vs), tys) =>
    3.70          ensure_const thy algbr eqngr permissive c
    3.71 +        ##>> pair (map (unprefix "'") vs)
    3.72          ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
    3.73        #>> (fn info => Datatype (tyco, info));
    3.74    in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
    3.75 @@ -607,7 +614,10 @@
    3.76  and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
    3.77    let
    3.78      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
    3.79 -    val classparams = these (try (#params o AxClass.get_info thy) class);
    3.80 +    val these_classparams = these o try (#params o AxClass.get_info thy);
    3.81 +    val classparams = these_classparams class;
    3.82 +    val further_classparams = maps these_classparams
    3.83 +      ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
    3.84      val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
    3.85      val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
    3.86      val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
    3.87 @@ -637,8 +647,11 @@
    3.88        ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
    3.89        ##>> fold_map translate_super_instance super_classes
    3.90        ##>> fold_map translate_classparam_instance classparams
    3.91 -      #>> (fn ((((class, tyco), arity_args), super_instances), classparam_instances) =>
    3.92 -             Classinst ((class, (tyco, arity_args)), (super_instances, classparam_instances)));
    3.93 +      ##>> fold_map translate_classparam_instance further_classparams
    3.94 +      #>> (fn (((((class, tyco), arity_args), super_instances),
    3.95 +        classparam_instances), further_classparam_instances) =>
    3.96 +          Classinst ((class, (tyco, arity_args)), (super_instances,
    3.97 +            (classparam_instances, further_classparam_instances))));
    3.98    in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
    3.99  and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
   3.100        pair (ITyVar (unprefix "'" v))
   3.101 @@ -682,15 +695,15 @@
   3.102          then translation_error thy permissive some_thm
   3.103            "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
   3.104        else ()
   3.105 -    val tys = Sign.const_typargs thy (c, ty);
   3.106 +    val arg_typs = Sign.const_typargs thy (c, ty);
   3.107      val sorts = Code_Preproc.sortargs eqngr c;
   3.108 -    val tys_args = (fst o Term.strip_type) ty;
   3.109 +    val function_typs = (fst o Term.strip_type) ty;
   3.110    in
   3.111      ensure_const thy algbr eqngr permissive c
   3.112 -    ##>> fold_map (translate_typ thy algbr eqngr permissive) tys
   3.113 -    ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (tys ~~ sorts)
   3.114 -    ##>> fold_map (translate_typ thy algbr eqngr permissive) tys_args
   3.115 -    #>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args)))
   3.116 +    ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
   3.117 +    ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
   3.118 +    ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs
   3.119 +    #>> (fn (((c, arg_typs), dss), function_typs) => IConst (c, ((arg_typs, dss), function_typs)))
   3.120    end
   3.121  and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
   3.122    translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)