1.1 --- a/src/Tools/Code/code_thingol.ML Thu Jun 17 11:33:04 2010 +0200
1.2 +++ b/src/Tools/Code/code_thingol.ML Thu Jun 17 15:59:46 2010 +0200
1.3 @@ -67,14 +67,16 @@
1.4 datatype stmt =
1.5 NoStmt
1.6 | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
1.7 - | Datatype of string * ((vname * sort) list * (string * itype list) list)
1.8 + | Datatype of string * ((vname * sort) list *
1.9 + ((string * vname list (*type argument wrt. canonical order*)) * itype list) list)
1.10 | Datatypecons of string * string
1.11 | Class of class * (vname * ((class * string) list * (string * itype) list))
1.12 | Classrel of class * class
1.13 | Classparam of string * class
1.14 - | Classinst of (class * (string * (vname * sort) list) (*class and arity*) )
1.15 + | Classinst of (class * (string * (vname * sort) list) (*class and arity*))
1.16 * ((class * (string * (string * dict list list))) list (*super instances*)
1.17 - * ((string * const) * (thm * bool)) list (*class parameter instances*))
1.18 + * (((string * const) * (thm * bool)) list (*class parameter instances*)
1.19 + * ((string * const) * (thm * bool)) list (*super class parameter instances*)))
1.20 type program = stmt Graph.T
1.21 val empty_funs: program -> string list
1.22 val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
1.23 @@ -403,14 +405,16 @@
1.24 datatype stmt =
1.25 NoStmt
1.26 | Fun of string * ((typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option)
1.27 - | Datatype of string * ((vname * sort) list * (string * itype list) list)
1.28 + | Datatype of string * ((vname * sort) list * ((string * vname list) * itype list) list)
1.29 | Datatypecons of string * string
1.30 | Class of class * (vname * ((class * string) list * (string * itype) list))
1.31 | Classrel of class * class
1.32 | Classparam of string * class
1.33 | Classinst of (class * (string * (vname * sort) list))
1.34 * ((class * (string * (string * dict list list))) list
1.35 - * ((string * const) * (thm * bool)) list) (*see also signature*);
1.36 + * (((string * const) * (thm * bool)) list
1.37 + * ((string * const) * (thm * bool)) list))
1.38 + (*see also signature*);
1.39
1.40 type program = stmt Graph.T;
1.41
1.42 @@ -428,6 +432,9 @@
1.43 (ICase (((map_terms_bottom_up f t, ty), (map o pairself)
1.44 (map_terms_bottom_up f) ps), map_terms_bottom_up f t0));
1.45
1.46 +fun map_classparam_instances_as_term f =
1.47 + (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
1.48 +
1.49 fun map_terms_stmt f NoStmt = NoStmt
1.50 | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
1.51 (fn (ts, t) => (map f ts, f t)) eqs), case_cong))
1.52 @@ -436,9 +443,8 @@
1.53 | map_terms_stmt f (stmt as Class _) = stmt
1.54 | map_terms_stmt f (stmt as Classrel _) = stmt
1.55 | map_terms_stmt f (stmt as Classparam _) = stmt
1.56 - | map_terms_stmt f (Classinst (arity, (super_instances, classparams))) =
1.57 - Classinst (arity, (super_instances, (map o apfst o apsnd) (fn const =>
1.58 - case f (IConst const) of IConst const' => const') classparams));
1.59 + | map_terms_stmt f (Classinst (arity, (super_instances, classparam_instances))) =
1.60 + Classinst (arity, (super_instances, (pairself o map_classparam_instances_as_term) f classparam_instances));
1.61
1.62 fun is_cons program name = case Graph.get_node program name
1.63 of Datatypecons _ => true
1.64 @@ -557,8 +563,9 @@
1.65 val (vs, cos) = Code.get_type thy tyco;
1.66 val stmt_datatype =
1.67 fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
1.68 - ##>> fold_map (fn (c, tys) =>
1.69 + ##>> fold_map (fn ((c, vs), tys) =>
1.70 ensure_const thy algbr eqngr permissive c
1.71 + ##>> pair (map (unprefix "'") vs)
1.72 ##>> fold_map (translate_typ thy algbr eqngr permissive) tys) cos
1.73 #>> (fn info => Datatype (tyco, info));
1.74 in ensure_stmt lookup_tyco (declare_tyco thy) stmt_datatype tyco end
1.75 @@ -607,7 +614,10 @@
1.76 and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
1.77 let
1.78 val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
1.79 - val classparams = these (try (#params o AxClass.get_info thy) class);
1.80 + val these_classparams = these o try (#params o AxClass.get_info thy);
1.81 + val classparams = these_classparams class;
1.82 + val further_classparams = maps these_classparams
1.83 + ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
1.84 val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
1.85 val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
1.86 val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
1.87 @@ -637,8 +647,11 @@
1.88 ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
1.89 ##>> fold_map translate_super_instance super_classes
1.90 ##>> fold_map translate_classparam_instance classparams
1.91 - #>> (fn ((((class, tyco), arity_args), super_instances), classparam_instances) =>
1.92 - Classinst ((class, (tyco, arity_args)), (super_instances, classparam_instances)));
1.93 + ##>> fold_map translate_classparam_instance further_classparams
1.94 + #>> (fn (((((class, tyco), arity_args), super_instances),
1.95 + classparam_instances), further_classparam_instances) =>
1.96 + Classinst ((class, (tyco, arity_args)), (super_instances,
1.97 + (classparam_instances, further_classparam_instances))));
1.98 in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
1.99 and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
1.100 pair (ITyVar (unprefix "'" v))
1.101 @@ -682,15 +695,15 @@
1.102 then translation_error thy permissive some_thm
1.103 "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
1.104 else ()
1.105 - val tys = Sign.const_typargs thy (c, ty);
1.106 + val arg_typs = Sign.const_typargs thy (c, ty);
1.107 val sorts = Code_Preproc.sortargs eqngr c;
1.108 - val tys_args = (fst o Term.strip_type) ty;
1.109 + val function_typs = (fst o Term.strip_type) ty;
1.110 in
1.111 ensure_const thy algbr eqngr permissive c
1.112 - ##>> fold_map (translate_typ thy algbr eqngr permissive) tys
1.113 - ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (tys ~~ sorts)
1.114 - ##>> fold_map (translate_typ thy algbr eqngr permissive) tys_args
1.115 - #>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args)))
1.116 + ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
1.117 + ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
1.118 + ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs
1.119 + #>> (fn (((c, arg_typs), dss), function_typs) => IConst (c, ((arg_typs, dss), function_typs)))
1.120 end
1.121 and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
1.122 translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)