src/Tools/Code/code_thingol.ML
changeset 37384 5aba26803073
parent 37216 3165bc303f66
child 37431 e9004a3e0d94
     1.1 --- a/src/Tools/Code/code_thingol.ML	Sun Jun 06 18:47:29 2010 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Jun 07 13:42:38 2010 +0200
     1.3 @@ -72,9 +72,10 @@
     1.4      | Class of class * (vname * ((class * string) list * (string * itype) list))
     1.5      | Classrel of class * class
     1.6      | Classparam of string * class
     1.7 -    | Classinst of (class * (string * (vname * sort) list))
     1.8 -          * ((class * (string * (string * dict list list))) list
     1.9 -        * ((string * const) * (thm * bool)) list)
    1.10 +    | Classinst of (class * (string * (vname * sort) list) (*class and arity*) )
    1.11 +          * (((class * (string * (string * dict list list))) list (*super instances*)
    1.12 +            * (class * class) list list (*type argument weakening mapping*))
    1.13 +        * ((string * const) * (thm * bool)) list (*class parameter instances*))
    1.14    type program = stmt Graph.T
    1.15    val empty_funs: program -> string list
    1.16    val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
    1.17 @@ -276,8 +277,8 @@
    1.18  in
    1.19  
    1.20  fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
    1.21 -fun namify_classrel thy = namify thy (fn (class1, class2) => 
    1.22 -    Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1)
    1.23 +fun namify_classrel thy = namify thy (fn (sub_class, super_class) => 
    1.24 +    Long_Name.base_name sub_class ^ "_" ^ Long_Name.base_name super_class)
    1.25    (fn thy => thyname_of_class thy o fst);
    1.26    (*order fits nicely with composed projections*)
    1.27  fun namify_tyco thy "fun" = "Pure.fun"
    1.28 @@ -386,11 +387,12 @@
    1.29     of SOME const' => (const', naming)
    1.30      | NONE => declare_const thy const naming;
    1.31  
    1.32 -val fun_tyco = "Pure.fun.tyco" (*depends on suffix_tyco and namify_tyco!*);
    1.33 +val fun_tyco = Long_Name.append (namify_tyco Pure.thy "fun") suffix_tyco
    1.34 +  (*depends on add_suffix*);
    1.35  
    1.36  val unfold_fun = unfoldr
    1.37    (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
    1.38 -    | _ => NONE); (*depends on suffix_tyco and namify_tyco!*)
    1.39 +    | _ => NONE);
    1.40  
    1.41  end; (* local *)
    1.42  
    1.43 @@ -407,8 +409,9 @@
    1.44    | Classrel of class * class
    1.45    | Classparam of string * class
    1.46    | Classinst of (class * (string * (vname * sort) list))
    1.47 -        * ((class * (string * (string * dict list list))) list
    1.48 -      * ((string * const) * (thm * bool)) list);
    1.49 +        * (((class * (string * (string * dict list list))) list
    1.50 +          * (class * class) list list)
    1.51 +      * ((string * const) * (thm * bool)) list) (*see also signature*);
    1.52  
    1.53  type program = stmt Graph.T;
    1.54  
    1.55 @@ -434,8 +437,8 @@
    1.56    | map_terms_stmt f (stmt as Class _) = stmt
    1.57    | map_terms_stmt f (stmt as Classrel _) = stmt
    1.58    | map_terms_stmt f (stmt as Classparam _) = stmt
    1.59 -  | map_terms_stmt f (Classinst (arity, (superinsts, classparams))) =
    1.60 -      Classinst (arity, (superinsts, (map o apfst o apsnd) (fn const =>
    1.61 +  | map_terms_stmt f (Classinst (arity, ((super_instances, weakening), classparams))) =
    1.62 +      Classinst (arity, ((super_instances, weakening), (map o apfst o apsnd) (fn const =>
    1.63          case f (IConst const) of IConst const' => const') classparams));
    1.64  
    1.65  fun is_cons program name = case Graph.get_node program name
    1.66 @@ -580,25 +583,25 @@
    1.67    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
    1.68  and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
    1.69    let
    1.70 -    val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
    1.71 +    val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
    1.72      val cs = #params (AxClass.get_info thy class);
    1.73      val stmt_class =
    1.74 -      fold_map (fn superclass => ensure_class thy algbr eqngr permissive superclass
    1.75 -        ##>> ensure_classrel thy algbr eqngr permissive (class, superclass)) superclasses
    1.76 +      fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
    1.77 +        ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
    1.78        ##>> fold_map (fn (c, ty) => ensure_const thy algbr eqngr permissive c
    1.79          ##>> translate_typ thy algbr eqngr permissive ty) cs
    1.80        #>> (fn info => Class (class, (unprefix "'" Name.aT, info)))
    1.81    in ensure_stmt lookup_class (declare_class thy) stmt_class class end
    1.82 -and ensure_classrel thy algbr eqngr permissive (subclass, superclass) =
    1.83 +and ensure_classrel thy algbr eqngr permissive (sub_class, super_class) =
    1.84    let
    1.85      val stmt_classrel =
    1.86 -      ensure_class thy algbr eqngr permissive subclass
    1.87 -      ##>> ensure_class thy algbr eqngr permissive superclass
    1.88 +      ensure_class thy algbr eqngr permissive sub_class
    1.89 +      ##>> ensure_class thy algbr eqngr permissive super_class
    1.90        #>> Classrel;
    1.91 -  in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (subclass, superclass) end
    1.92 +  in ensure_stmt lookup_classrel (declare_classrel thy) stmt_classrel (sub_class, super_class) end
    1.93  and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
    1.94    let
    1.95 -    val superclasses = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
    1.96 +    val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
    1.97      val classparams = these (try (#params o AxClass.get_info thy) class);
    1.98      val vs = Name.names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
    1.99      val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
   1.100 @@ -606,31 +609,31 @@
   1.101        Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
   1.102      val arity_typ = Type (tyco, map TFree vs);
   1.103      val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
   1.104 -    fun translate_superarity superclass =
   1.105 -      ensure_class thy algbr eqngr permissive superclass
   1.106 -      ##>> ensure_classrel thy algbr eqngr permissive (class, superclass)
   1.107 -      ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [superclass])
   1.108 -      #>> (fn ((superclass, classrel), [DictConst (inst, dss)]) =>
   1.109 -            (superclass, (classrel, (inst, dss))));
   1.110 -    fun translate_classparam_inst (c, ty) =
   1.111 +    fun translate_super_instance super_class =
   1.112 +      ensure_class thy algbr eqngr permissive super_class
   1.113 +      ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
   1.114 +      ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
   1.115 +      #>> (fn ((super_class, classrel), [DictConst (inst, dss)]) =>
   1.116 +            (super_class, (classrel, (inst, dss))));
   1.117 +    fun translate_classparam_instance (c, ty) =
   1.118        let
   1.119 -        val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
   1.120 -        val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
   1.121 -        val c_ty = (apsnd Logic.unvarifyT_global o dest_Const o snd
   1.122 +        val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
   1.123 +        val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy raw_const);
   1.124 +        val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
   1.125            o Logic.dest_equals o Thm.prop_of) thm;
   1.126        in
   1.127          ensure_const thy algbr eqngr permissive c
   1.128 -        ##>> translate_const thy algbr eqngr permissive (SOME thm) (c_ty, NONE)
   1.129 -        #>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true)))
   1.130 +        ##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE)
   1.131 +        #>> (fn (c, IConst const') => ((c, const'), (thm, true)))
   1.132        end;
   1.133      val stmt_inst =
   1.134        ensure_class thy algbr eqngr permissive class
   1.135        ##>> ensure_tyco thy algbr eqngr permissive tyco
   1.136        ##>> fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
   1.137 -      ##>> fold_map translate_superarity superclasses
   1.138 -      ##>> fold_map translate_classparam_inst classparams
   1.139 -      #>> (fn ((((class, tyco), arity), superinsts), classparams) =>
   1.140 -             Classinst ((class, (tyco, arity)), (superinsts, classparams)));
   1.141 +      ##>> fold_map translate_super_instance super_classes
   1.142 +      ##>> fold_map translate_classparam_instance classparams
   1.143 +      #>> (fn ((((class, tyco), arity_args), super_instances), classparam_instances) =>
   1.144 +             Classinst ((class, (tyco, arity_args)), ((super_instances, []), classparam_instances)));
   1.145    in ensure_stmt lookup_instance (declare_instance thy) stmt_inst (class, tyco) end
   1.146  and translate_typ thy algbr eqngr permissive (TFree (v, _)) =
   1.147        pair (ITyVar (unprefix "'" v))
   1.148 @@ -772,8 +775,8 @@
   1.149        | Local of (class * class) list * (string * (int * sort));
   1.150      fun class_relation (Global ((_, tyco), yss), _) class =
   1.151            Global ((class, tyco), yss)
   1.152 -      | class_relation (Local (classrels, v), subclass) superclass =
   1.153 -          Local ((subclass, superclass) :: classrels, v);
   1.154 +      | class_relation (Local (classrels, v), sub_class) super_class =
   1.155 +          Local ((sub_class, super_class) :: classrels, v);
   1.156      fun type_constructor (tyco, _) yss class =
   1.157        Global ((class, tyco), (map o map) fst yss);
   1.158      fun type_variable (TFree (v, sort)) =