src/Tools/Code/code_thingol.ML
changeset 37448 3bd4b3809bee
parent 37447 ad3e04f289b6
child 37640 fc27be4c6b1c
     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)