explicit hint for domain of class parameters in instance statements
authorhaftmann
Thu Jul 04 08:52:44 2013 +0200 (2013-07-04)
changeset 52519598addf65209
parent 52518 c9a9359e0285
child 52520 4a884366b0d8
explicit hint for domain of class parameters in instance statements
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Wed Jul 03 23:42:07 2013 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Jul 04 08:52:44 2013 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4               of NONE => NONE
     1.5                | SOME (Code_Printer.Plain_const_syntax _) => SOME 0
     1.6                | SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
     1.7 -            fun print_classparam_instance ((classparam, const), (thm, _)) =
     1.8 +            fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
     1.9                case requires_args classparam
    1.10                 of NONE => semicolon [
    1.11                        (str o Long_Name.base_name o deresolve) classparam,
     2.1 --- a/src/Tools/Code/code_ml.ML	Wed Jul 03 23:42:07 2013 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Thu Jul 04 08:52:44 2013 +0200
     2.3 @@ -30,8 +30,8 @@
     2.4      ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
     2.5    | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list,
     2.6          superinsts: (class * (string * (string * dict list list))) list,
     2.7 -        inst_params: ((string * const) * (thm * bool)) list,
     2.8 -        superinst_params: ((string * const) * (thm * bool)) list };
     2.9 +        inst_params: ((string * (const * int)) * (thm * bool)) list,
    2.10 +        superinst_params: ((string * (const * int)) * (thm * bool)) list };
    2.11  
    2.12  datatype ml_stmt =
    2.13      ML_Exc of string * (typscheme * int)
    2.14 @@ -215,7 +215,7 @@
    2.15                  str "=",
    2.16                  print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
    2.17                ];
    2.18 -            fun print_classparam_instance ((classparam, const), (thm, _)) =
    2.19 +            fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
    2.20                concat [
    2.21                  (str o Long_Name.base_name o deresolve) classparam,
    2.22                  str "=",
    2.23 @@ -552,7 +552,7 @@
    2.24                  str "=",
    2.25                  print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x))
    2.26                ];
    2.27 -            fun print_classparam_instance ((classparam, const), (thm, _)) =
    2.28 +            fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
    2.29                concat [
    2.30                  (str o deresolve) classparam,
    2.31                  str "=",
     3.1 --- a/src/Tools/Code/code_scala.ML	Wed Jul 03 23:42:07 2013 +0200
     3.2 +++ b/src/Tools/Code/code_scala.ML	Thu Jul 04 08:52:44 2013 +0200
     3.3 @@ -260,7 +260,7 @@
     3.4            let
     3.5              val tyvars = intro_tyvars vs reserved;
     3.6              val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
     3.7 -            fun print_classparam_instance ((classparam, const as { dom, ... }), (thm, _)) =
     3.8 +            fun print_classparam_instance ((classparam, (const as { dom, ... }, _)), (thm, _)) =
     3.9                let
    3.10                  val aux_dom = Name.invent_names (snd reserved) "a" dom;
    3.11                  val auxs = map fst aux_dom;
     4.1 --- a/src/Tools/Code/code_thingol.ML	Wed Jul 03 23:42:07 2013 +0200
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Jul 04 08:52:44 2013 +0200
     4.3 @@ -78,8 +78,8 @@
     4.4      | Classparam of string * class
     4.5      | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
     4.6          superinsts: (class * (string * (string * dict list list))) list,
     4.7 -        inst_params: ((string * const) * (thm * bool)) list,
     4.8 -        superinst_params: ((string * const) * (thm * bool)) list };
     4.9 +        inst_params: ((string * (const * int)) * (thm * bool)) list,
    4.10 +        superinst_params: ((string * (const * int)) * (thm * bool)) list };
    4.11    type program = stmt Graph.T
    4.12    val empty_funs: program -> string list
    4.13    val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
    4.14 @@ -428,8 +428,8 @@
    4.15    | Classparam of string * class
    4.16    | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
    4.17        superinsts: (class * (string * (string * dict list list))) list,
    4.18 -      inst_params: ((string * const) * (thm * bool)) list,
    4.19 -      superinst_params: ((string * const) * (thm * bool)) list };
    4.20 +      inst_params: ((string * (const * int)) * (thm * bool)) list,
    4.21 +      superinst_params: ((string * (const * int)) * (thm * bool)) list };
    4.22  
    4.23  type program = stmt Graph.T;
    4.24  
    4.25 @@ -448,7 +448,7 @@
    4.26          primitive = map_terms_bottom_up f t0 });
    4.27  
    4.28  fun map_classparam_instances_as_term f =
    4.29 -  (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const')
    4.30 +  (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const')
    4.31  
    4.32  fun map_terms_stmt f NoStmt = NoStmt
    4.33    | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst)
    4.34 @@ -708,13 +708,14 @@
    4.35      fun translate_classparam_instance (c, ty) =
    4.36        let
    4.37          val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
    4.38 +        val dom_length = length (fst (strip_type ty))
    4.39          val thm = Axclass.unoverload_conv thy (Thm.cterm_of thy raw_const);
    4.40          val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
    4.41            o Logic.dest_equals o Thm.prop_of) thm;
    4.42        in
    4.43          ensure_const thy algbr eqngr permissive c
    4.44          ##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE)
    4.45 -        #>> (fn (c, IConst const') => ((c, const'), (thm, true)))
    4.46 +        #>> (fn (c, IConst const') => ((c, (const', dom_length)), (thm, true)))
    4.47        end;
    4.48      val stmt_inst =
    4.49        ensure_class thy algbr eqngr permissive class
     5.1 --- a/src/Tools/nbe.ML	Wed Jul 03 23:42:07 2013 +0200
     5.2 +++ b/src/Tools/nbe.ML	Thu Jul 04 08:52:44 2013 +0200
     5.3 @@ -439,7 +439,7 @@
     5.4    | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) =
     5.5        [(inst, (vs, [([], dummy_const class [] `$$
     5.6          map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts
     5.7 -        @ map (IConst o snd o fst) inst_params)]))];
     5.8 +        @ map (IConst o fst o snd o fst) inst_params)]))];
     5.9  
    5.10  
    5.11  (* compile whole programs *)