separated dictionary weakning into separate type
authorhaftmann
Mon Dec 13 22:54:47 2010 +0100 (2010-12-13)
changeset 41118b290841cd3b0
parent 41117 d6379876ec4c
child 41119 573f557ed716
separated dictionary weakning into separate type
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	Mon Dec 13 10:15:27 2010 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Mon Dec 13 22:54:47 2010 +0100
     1.3 @@ -80,16 +80,18 @@
     1.4        | print_classrels fxy [classrel] ps = brackify fxy [(str o deresolve) classrel, brackify BR ps]
     1.5        | print_classrels fxy classrels ps =
     1.6            brackify fxy [enum " o" "(" ")" (map (str o deresolve) classrels), brackify BR ps]
     1.7 -    fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
     1.8 -          print_classrels fxy classrels ((str o deresolve) inst ::
     1.9 +    fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
    1.10 +      print_classrels fxy classrels (print_plain_dict is_pseudo_fun fxy x)
    1.11 +    and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
    1.12 +          ((str o deresolve) inst ::
    1.13              (if is_pseudo_fun inst then [str "()"]
    1.14              else map_filter (print_dicts is_pseudo_fun BR) dss))
    1.15 -      | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
    1.16 -          print_classrels fxy classrels [str (if k = 1 then first_upper v ^ "_"
    1.17 +      | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
    1.18 +          [str (if k = 1 then first_upper v ^ "_"
    1.19              else first_upper v ^ string_of_int (i+1) ^ "_")]
    1.20      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    1.21      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    1.22 -      (map_index (fn (i, _) => Dict_Var ([], (v, (i, length sort)))) sort));
    1.23 +      (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
    1.24      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    1.25            print_app is_pseudo_fun some_thm vars fxy (c, [])
    1.26        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    1.27 @@ -219,7 +221,7 @@
    1.28                concat [
    1.29                  (str o Long_Name.base_name o deresolve) classrel,
    1.30                  str "=",
    1.31 -                print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
    1.32 +                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
    1.33                ];
    1.34              fun print_classparam_instance ((classparam, const), (thm, _)) =
    1.35                concat [
    1.36 @@ -380,18 +382,19 @@
    1.37      fun print_dicttypscheme (vs, class_ty) = print_typscheme_prefix (vs, print_dicttyp class_ty);
    1.38      val print_classrels =
    1.39        fold_rev (fn classrel => fn p => Pretty.block [p, str ".", (str o deresolve) classrel])
    1.40 -    fun print_dict is_pseudo_fun fxy (Dict_Const (classrels, (inst, dss))) =
    1.41 +    fun print_dict is_pseudo_fun fxy (Dict (classrels, x)) =
    1.42 +      print_plain_dict is_pseudo_fun fxy x
    1.43 +      |> print_classrels classrels
    1.44 +    and print_plain_dict is_pseudo_fun fxy (Dict_Const (inst, dss)) =
    1.45            brackify BR ((str o deresolve) inst ::
    1.46              (if is_pseudo_fun inst then [str "()"]
    1.47              else map_filter (print_dicts is_pseudo_fun BR) dss))
    1.48 -          |> print_classrels classrels
    1.49 -      | print_dict is_pseudo_fun fxy (Dict_Var (classrels, (v, (i, k)))) =
    1.50 +      | print_plain_dict is_pseudo_fun fxy (Dict_Var (v, (i, k))) =
    1.51            str (if k = 1 then "_" ^ first_upper v
    1.52              else "_" ^ first_upper v ^ string_of_int (i+1))
    1.53 -          |> print_classrels classrels
    1.54      and print_dicts is_pseudo_fun = tuplify (print_dict is_pseudo_fun);
    1.55      val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
    1.56 -      (map_index (fn (i, _) => Dict_Var ([], (v, (i, length sort)))) sort));
    1.57 +      (map_index (fn (i, _) => Dict ([], Dict_Var (v, (i, length sort)))) sort));
    1.58      fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
    1.59            print_app is_pseudo_fun some_thm vars fxy (c, [])
    1.60        | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
    1.61 @@ -556,7 +559,7 @@
    1.62                concat [
    1.63                  (str o deresolve) classrel,
    1.64                  str "=",
    1.65 -                print_dict is_pseudo_fun NOBR (Dict_Const ([], x))
    1.66 +                print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
    1.67                ];
    1.68              fun print_classparam_instance ((classparam, const), (thm, _)) =
    1.69                concat [
     2.1 --- a/src/Tools/Code/code_thingol.ML	Mon Dec 13 10:15:27 2010 +0100
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Dec 13 22:54:47 2010 +0100
     2.3 @@ -15,8 +15,10 @@
     2.4  sig
     2.5    type vname = string;
     2.6    datatype dict =
     2.7 -      Dict_Const of string list * (string * dict list list)
     2.8 -    | Dict_Var of string list * (vname * (int * int));
     2.9 +      Dict of (string list * plain_dict)
    2.10 +  and plain_dict = 
    2.11 +      Dict_Const of string * dict list list
    2.12 +    | Dict_Var of vname * (int * int)
    2.13    datatype itype =
    2.14        `%% of string * itype list
    2.15      | ITyVar of vname;
    2.16 @@ -132,8 +134,10 @@
    2.17  type vname = string;
    2.18  
    2.19  datatype dict =
    2.20 -    Dict_Const of string list * (string * dict list list)
    2.21 -  | Dict_Var of string list * (vname * (int * int));
    2.22 +    Dict of (string list * plain_dict)
    2.23 +and plain_dict = 
    2.24 +    Dict_Const of string * dict list list
    2.25 +  | Dict_Var of vname * (int * int)
    2.26  
    2.27  datatype itype =
    2.28      `%% of string * itype list
    2.29 @@ -244,8 +248,9 @@
    2.30  
    2.31  fun contains_dict_var t =
    2.32    let
    2.33 -    fun cont_dict (Dict_Const (_, (_, dss))) = (exists o exists) cont_dict dss
    2.34 -      | cont_dict (Dict_Var _) = true;
    2.35 +    fun cont_dict (Dict (_, d)) = cont_plain_dict d
    2.36 +    and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
    2.37 +      | cont_plain_dict (Dict_Var _) = true;
    2.38      fun cont_term (IConst (_, ((_, dss), _))) = (exists o exists) cont_dict dss
    2.39        | cont_term (IVar _) = false
    2.40        | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
    2.41 @@ -641,7 +646,7 @@
    2.42        ensure_class thy algbr eqngr permissive super_class
    2.43        ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)
    2.44        ##>> translate_dicts thy algbr eqngr permissive NONE (arity_typ, [super_class])
    2.45 -      #>> (fn ((super_class, classrel), [Dict_Const ([], (inst, dss))]) =>
    2.46 +      #>> (fn ((super_class, classrel), [Dict ([], Dict_Const (inst, dss))]) =>
    2.47              (super_class, (classrel, (inst, dss))));
    2.48      fun translate_classparam_instance (c, ty) =
    2.49        let
    2.50 @@ -802,33 +807,33 @@
    2.51  and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr permissive some_thm (ty, sort) =
    2.52    let
    2.53      datatype typarg_witness =
    2.54 -        Global of (class * class) list * ((class * string) * typarg_witness list list)
    2.55 -      | Local of (class * class) list * (string * (int * sort));
    2.56 -    fun add_classrel classrel (Global (classrels, x)) =
    2.57 -          Global (classrel :: classrels, x)
    2.58 -      | add_classrel classrel (Local (classrels, x)) =
    2.59 -          Local (classrel :: classrels, x)
    2.60 -    fun class_relation (d, sub_class) super_class =
    2.61 -      add_classrel (sub_class, super_class) d;
    2.62 +        Weakening of (class * class) list * plain_typarg_witness
    2.63 +    and plain_typarg_witness =
    2.64 +        Global of (class * string) * typarg_witness list list
    2.65 +      | Local of string * (int * sort);
    2.66 +    fun class_relation ((Weakening (classrels, x)), sub_class) super_class =
    2.67 +      Weakening ((sub_class, super_class) :: classrels, x);
    2.68      fun type_constructor (tyco, _) dss class =
    2.69 -      Global ([], ((class, tyco), (map o map) fst dss));
    2.70 +      Weakening ([], Global ((class, tyco), (map o map) fst dss));
    2.71      fun type_variable (TFree (v, sort)) =
    2.72        let
    2.73          val sort' = proj_sort sort;
    2.74 -      in map_index (fn (n, class) => (Local ([], (v, (n, sort'))), class)) sort' end;
    2.75 +      in map_index (fn (n, class) => (Weakening ([], Local (v, (n, sort'))), class)) sort' end;
    2.76      val typarg_witnesses = Sorts.of_sort_derivation algebra
    2.77        {class_relation = K (Sorts.classrel_derivation algebra class_relation),
    2.78         type_constructor = type_constructor,
    2.79         type_variable = type_variable} (ty, proj_sort sort)
    2.80        handle Sorts.CLASS_ERROR e => not_wellsorted thy permissive some_thm ty sort e;
    2.81 -    fun mk_dict (Global (classrels, (inst, dss))) =
    2.82 +    fun mk_dict (Weakening (classrels, x)) =
    2.83            fold_map (ensure_classrel thy algbr eqngr permissive) classrels
    2.84 -          ##>> ensure_inst thy algbr eqngr permissive inst
    2.85 +          ##>> mk_plain_dict x
    2.86 +          #>> Dict 
    2.87 +    and mk_plain_dict (Global (inst, dss)) =
    2.88 +          ensure_inst thy algbr eqngr permissive inst
    2.89            ##>> (fold_map o fold_map) mk_dict dss
    2.90 -          #>> (fn ((classrels, inst), dss) => Dict_Const (classrels, (inst, dss)))
    2.91 -      | mk_dict (Local (classrels, (v, (n, sort)))) =
    2.92 -          fold_map (ensure_classrel thy algbr eqngr permissive) classrels
    2.93 -          #>> (fn classrels => Dict_Var (classrels, (unprefix "'" v, (n, length sort))))
    2.94 +          #>> (fn (inst, dss) => Dict_Const (inst, dss))
    2.95 +      | mk_plain_dict (Local (v, (n, sort))) =
    2.96 +          pair (Dict_Var (unprefix "'" v, (n, length sort)))
    2.97    in fold_map mk_dict typarg_witnesses end;
    2.98  
    2.99  
     3.1 --- a/src/Tools/nbe.ML	Mon Dec 13 10:15:27 2010 +0100
     3.2 +++ b/src/Tools/nbe.ML	Mon Dec 13 22:54:47 2010 +0100
     3.3 @@ -287,7 +287,7 @@
     3.4  
     3.5      fun assemble_constapp c dss ts = 
     3.6        let
     3.7 -        val ts' = (maps o map) assemble_idict dss @ ts;
     3.8 +        val ts' = (maps o map) assemble_dict dss @ ts;
     3.9        in case AList.lookup (op =) eqnss' c
    3.10         of SOME (num_args, _) => if num_args <= length ts'
    3.11              then let val (ts1, ts2) = chop num_args ts'
    3.12 @@ -299,10 +299,12 @@
    3.13        end
    3.14      and assemble_classrels classrels =
    3.15        fold_rev (fn classrel => assemble_constapp classrel [] o single) classrels
    3.16 -    and assemble_idict (Dict_Const (classrels, (inst, dss))) =
    3.17 -          assemble_classrels classrels (assemble_constapp inst dss [])
    3.18 -      | assemble_idict (Dict_Var (classrels, (v, (n, _)))) =
    3.19 -          assemble_classrels classrels (nbe_dict v n);
    3.20 +    and assemble_dict (Dict (classrels, x)) =
    3.21 +          assemble_classrels classrels (assemble_plain_dict x)
    3.22 +    and assemble_plain_dict (Dict_Const (inst, dss)) =
    3.23 +          assemble_constapp inst dss []
    3.24 +      | assemble_plain_dict (Dict_Var (v, (n, _))) =
    3.25 +          nbe_dict v n
    3.26  
    3.27      fun assemble_iterm constapp =
    3.28        let