dictionary constants must permit explicit weakening of classes;
authorhaftmann
Thu Dec 09 17:25:43 2010 +0100 (2010-12-09)
changeset 411006c0940392fb4
parent 41099 5cf62cefbbb4
child 41101 c1d1ec5b90f1
dictionary constants must permit explicit weakening of classes;
tuned names
src/Tools/Code/code_ml.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Dec 09 09:58:33 2010 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Dec 09 17:25:43 2010 +0100
     1.3 @@ -76,23 +76,20 @@
     1.4          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
     1.5      fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
     1.6      fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
     1.7 -    fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
     1.8 -          brackify fxy ((str o deresolve) inst ::
     1.9 +    fun print_classrels fxy [] ps = brackify fxy ps
    1.10 +      | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]
    1.11 +      | print_classrels fxy classrels ps =
    1.12 +          brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]
    1.13 +    fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
    1.14 +          print_classrels fxy classrels ((str o deresolve) inst ::
    1.15              (if is_pseudo_fun inst then [str "()"]
    1.16              else map_filter (print_dicts is_pseudo_fun BR) dss))
    1.17 -      | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
    1.18 -          let
    1.19 -            val v_p = str (if k = 1 then first_upper v ^ "_"
    1.20 -              else first_upper v ^ string_of_int (i+1) ^ "_");
    1.21 -          in case classrels
    1.22 -           of [] => v_p
    1.23 -            | [classrel] => brackets [(str o deresolve) classrel, v_p]
    1.24 -            | classrels => brackets
    1.25 -                [enum " o" "(" ")" (map (str o deresolve) classrels), v_p]
    1.26 -          end
    1.27 +      | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
    1.28 +          print_classrels fxy classrels [str (if k = 1 then first_upper v ^ "_"
    1.29 +            else first_upper v ^ string_of_int (i+1) ^ "_")]
    1.30      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    1.31      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    1.32 -      (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    1.33 +      (map_index (fn (i, _) => Dict_Var ([], (v, (i, length sort)))) sort));
    1.34      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    1.35            print_app is_pseudo_fun some_thm vars fxy (c, [])
    1.36        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    1.37 @@ -218,11 +215,11 @@
    1.38        | print_def is_pseudo_fun _ definer
    1.39            (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
    1.40            let
    1.41 -            fun print_super_instance (_, (classrel, dss)) =
    1.42 +            fun print_super_instance (_, (classrel, x)) =
    1.43                concat [
    1.44                  (str o Long_Name.base_name o deresolve) classrel,
    1.45                  str "=",
    1.46 -                print_dict is_pseudo_fun NOBR (DictConst dss)
    1.47 +                print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
    1.48                ];
    1.49              fun print_classparam_instance ((classparam, const), (thm, _)) =
    1.50                concat [
    1.51 @@ -381,18 +378,20 @@
    1.52          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    1.53      fun print_typscheme (vs, ty) = print_typscheme_prefix (vs, print_typ NOBR ty);
    1.54      fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
    1.55 -    fun print_dict is_pseudo_fun fxy (DictConst (inst, dss)) =
    1.56 -          brackify fxy ((str o deresolve) inst ::
    1.57 +    val print_classrels =
    1.58 +      fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])
    1.59 +    fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
    1.60 +          brackify BR ((str o deresolve) inst ::
    1.61              (if is_pseudo_fun inst then [str "()"]
    1.62              else map_filter (print_dicts is_pseudo_fun BR) dss))
    1.63 -      | print_dict is_pseudo_fun fxy (DictVar (classrels, (v, (i, k)))) =
    1.64 +          |> print_classrels classrels
    1.65 +      | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
    1.66            str (if k = 1 then "_" ^ first_upper v
    1.67              else "_" ^ first_upper v ^ string_of_int (i+1))
    1.68 -          |> fold_rev (fn classrel => fn p =>
    1.69 -               Pretty.block [p, str ".", (str o deresolve) classrel]) classrels
    1.70 +          |> print_classrels classrels
    1.71      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    1.72      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    1.73 -      (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
    1.74 +      (map_index (fn (i, _) => Dict_Var ([], (v, (i, length sort)))) sort));
    1.75      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    1.76            print_app is_pseudo_fun some_thm vars fxy (c, [])
    1.77        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    1.78 @@ -553,11 +552,11 @@
    1.79        | print_def is_pseudo_fun _ definer
    1.80              (ML_Instance (inst, ((class, (tyco, vs)), (super_instances, (classparam_instances, _))))) =
    1.81            let
    1.82 -            fun print_super_instance (_, (classrel, dss)) =
    1.83 +            fun print_super_instance (_, (classrel, x)) =
    1.84                concat [
    1.85                  (str o deresolve) classrel,
    1.86                  str "=",
    1.87 -                print_dict is_pseudo_fun NOBR (DictConst dss)
    1.88 +                print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
    1.89                ];
    1.90              fun print_classparam_instance ((classparam, const), (thm, _)) =
    1.91                concat [
     2.1 --- a/src/Tools/Code/code_thingol.ML	Thu Dec 09 09:58:33 2010 +0100
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Dec 09 17:25:43 2010 +0100
     2.3 @@ -15,8 +15,8 @@
     2.4  sig
     2.5    type vname = string;
     2.6    datatype dict =
     2.7 -      DictConst of string * dict list list
     2.8 -    | DictVar of string list * (vname * (int * int));
     2.9 +      Dict_Const of string list * (string * dict list list)
    2.10 +    | Dict_Var of string list * (vname * (int * int));
    2.11    datatype itype =
    2.12        `%% of string * itype list
    2.13      | ITyVar of vname;
    2.14 @@ -50,7 +50,7 @@
    2.15    val unfold_const_app: iterm -> (const * iterm list) option
    2.16    val is_IVar: iterm -> bool
    2.17    val eta_expand: int -> const * iterm list -> iterm
    2.18 -  val contains_dictvar: iterm -> bool
    2.19 +  val contains_dict_var: iterm -> bool
    2.20    val locally_monomorphic: iterm -> bool
    2.21    val add_constnames: iterm -> string list -> string list
    2.22    val add_tyconames: iterm -> string list -> string list
    2.23 @@ -132,8 +132,8 @@
    2.24  type vname = string;
    2.25  
    2.26  datatype dict =
    2.27 -    DictConst of string * dict list list
    2.28 -  | DictVar of string list * (vname * (int * int));
    2.29 +    Dict_Const of string list * (string * dict list list)
    2.30 +  | Dict_Var of string list * (vname * (int * int));
    2.31  
    2.32  datatype itype =
    2.33      `%% of string * itype list
    2.34 @@ -242,10 +242,10 @@
    2.35        (Name.names ctxt "a" ((take l o drop j) tys));
    2.36    in vs_tys `|==> IConst c `$$ ts @ map (IVar o fst) vs_tys end;
    2.37  
    2.38 -fun contains_dictvar t =
    2.39 +fun contains_dict_var t =
    2.40    let
    2.41 -    fun cont_dict (DictConst (_, dss)) = (exists o exists) cont_dict dss
    2.42 -      | cont_dict (DictVar _) = true;
    2.43 +    fun cont_dict (Dict_Const (_, (_, dss))) = (exists o exists) cont_dict dss
    2.44 +      | cont_dict (Dict_Var _) = true;
    2.45      fun cont_term (IConst (_, ((_, dss), _))) = (exists o exists) cont_dict dss
    2.46        | cont_term (IVar _) = false
    2.47        | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
    2.48 @@ -641,7 +641,7 @@
    2.49        ensure_class thy algbr eqngr permissive super_class
    2.50        ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
    2.51        ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
    2.52 -      #>> (fn ((super_class, classrel), [DictConst (inst, dss)]) =>
    2.53 +      #>> (fn ((super_class, classrel), [Dict_Const ([], (inst, dss))]) =>
    2.54              (super_class, (classrel, (inst, dss))));
    2.55      fun translate_classparam_instance (c, ty) =
    2.56        let
    2.57 @@ -801,32 +801,35 @@
    2.58    #>> (fn sort => (unprefix "'" v, sort))
    2.59  and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) =
    2.60    let
    2.61 -    datatype typarg =
    2.62 -        Global of (class * string) * typarg list list
    2.63 +    datatype typarg_witness =
    2.64 +        Global of (class * class) list * ((class * string) * typarg_witness list list)
    2.65        | Local of (class * class) list * (string * (int * sort));
    2.66 -    fun class_relation (Global ((_, tyco), yss), _) class =
    2.67 -          Global ((class, tyco), yss)
    2.68 -      | class_relation (Local (classrels, v), sub_class) super_class =
    2.69 -          Local ((sub_class, super_class) :: classrels, v);
    2.70 -    fun type_constructor (tyco, _) yss class =
    2.71 -      Global ((class, tyco), (map o map) fst yss);
    2.72 +    fun add_classrel classrel (Global (classrels, x)) =
    2.73 +          Global (classrel :: classrels, x)
    2.74 +      | add_classrel classrel (Local (classrels, x)) =
    2.75 +          Local (classrel :: classrels, x)
    2.76 +    fun class_relation (d, sub_class) super_class =
    2.77 +      add_classrel (sub_class, super_class) d;
    2.78 +    fun type_constructor (tyco, _) dss class =
    2.79 +      Global ([], ((class, tyco), (map o map) fst dss));
    2.80      fun type_variable (TFree (v, sort)) =
    2.81        let
    2.82          val sort' = proj_sort sort;
    2.83        in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
    2.84 -    val typargs = Sorts.of_sort_derivation algebra
    2.85 +    val typarg_witnesses = Sorts.of_sort_derivation algebra
    2.86        {class_relation = K (Sorts.classrel_derivation algebra class_relation),
    2.87         type_constructor = type_constructor,
    2.88         type_variable = type_variable} (ty, proj_sort sort)
    2.89        handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e;
    2.90 -    fun mk_dict (Global (inst, yss)) =
    2.91 -          ensure_inst thy algbr eqngr permissive inst
    2.92 -          ##>> (fold_map o fold_map) mk_dict yss
    2.93 -          #>> (fn (inst, dss) => DictConst (inst, dss))
    2.94 +    fun mk_dict (Global (classrels, (inst, dss))) =
    2.95 +          fold_map (ensure_classrel thy algbr eqngr permissive) classrels
    2.96 +          ##>> ensure_inst thy algbr eqngr permissive inst
    2.97 +          ##>> (fold_map o fold_map) mk_dict dss
    2.98 +          #>> (fn ((classrels, inst), dss) => Dict_Const (classrels, (inst, dss)))
    2.99        | mk_dict (Local (classrels, (v, (n, sort)))) =
   2.100            fold_map (ensure_classrel thy algbr eqngr permissive) classrels
   2.101 -          #>> (fn classrels => DictVar (classrels, (unprefix "'" v, (n, length sort))))
   2.102 -  in fold_map mk_dict typargs end;
   2.103 +          #>> (fn classrels => Dict_Var (classrels, (unprefix "'" v, (n, length sort))))
   2.104 +  in fold_map mk_dict typarg_witnesses end;
   2.105  
   2.106  
   2.107  (* store *)
     3.1 --- a/src/Tools/nbe.ML	Thu Dec 09 09:58:33 2010 +0100
     3.2 +++ b/src/Tools/nbe.ML	Thu Dec 09 17:25:43 2010 +0100
     3.3 @@ -297,10 +297,12 @@
     3.4              then nbe_apps (nbe_fun 0 c) ts'
     3.5              else nbe_apps_constr idx_of c ts'
     3.6        end
     3.7 -    and assemble_idict (DictConst (inst, dss)) =
     3.8 -          assemble_constapp inst dss []
     3.9 -      | assemble_idict (DictVar (supers, (v, (n, _)))) =
    3.10 -          fold_rev (fn super => assemble_constapp super [] o single) supers (nbe_dict v n);
    3.11 +    and assemble_classrels classrels =
    3.12 +      fold_rev (fn classrel => assemble_constapp classrel [] o single) classrels
    3.13 +    and assemble_idict (Dict_Const (classrels, (inst, dss))) =
    3.14 +          assemble_classrels classrels (assemble_constapp inst dss [])
    3.15 +      | assemble_idict (Dict_Var (classrels, (v, (n, _)))) =
    3.16 +          assemble_classrels classrels (nbe_dict v n);
    3.17  
    3.18      fun assemble_iterm constapp =
    3.19        let