# HG changeset patch # User haftmann # Date 1372920764 -7200 # Node ID 598addf652090230ffb38d455bffc7902a00b060 # Parent c9a9359e028590efe9ba0e4565ad4623b82c8552 explicit hint for domain of class parameters in instance statements diff -r c9a9359e0285 -r 598addf65209 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Wed Jul 03 23:42:07 2013 +0200 +++ b/src/Tools/Code/code_haskell.ML Thu Jul 04 08:52:44 2013 +0200 @@ -228,7 +228,7 @@ of NONE => NONE | SOME (Code_Printer.Plain_const_syntax _) => SOME 0 | SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k; - fun print_classparam_instance ((classparam, const), (thm, _)) = + fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = case requires_args classparam of NONE => semicolon [ (str o Long_Name.base_name o deresolve) classparam, diff -r c9a9359e0285 -r 598addf65209 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Wed Jul 03 23:42:07 2013 +0200 +++ b/src/Tools/Code/code_ml.ML Thu Jul 04 08:52:44 2013 +0200 @@ -30,8 +30,8 @@ ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list) | ML_Instance of string * { class: string, tyco: string, vs: (vname * sort) list, superinsts: (class * (string * (string * dict list list))) list, - inst_params: ((string * const) * (thm * bool)) list, - superinst_params: ((string * const) * (thm * bool)) list }; + inst_params: ((string * (const * int)) * (thm * bool)) list, + superinst_params: ((string * (const * int)) * (thm * bool)) list }; datatype ml_stmt = ML_Exc of string * (typscheme * int) @@ -215,7 +215,7 @@ str "=", print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x)) ]; - fun print_classparam_instance ((classparam, const), (thm, _)) = + fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = concat [ (str o Long_Name.base_name o deresolve) classparam, str "=", @@ -552,7 +552,7 @@ str "=", print_dict is_pseudo_fun NOBR (Dict ([], Dict_Const x)) ]; - fun print_classparam_instance ((classparam, const), (thm, _)) = + fun print_classparam_instance ((classparam, (const, _)), (thm, _)) = concat [ (str o deresolve) classparam, str "=", diff -r c9a9359e0285 -r 598addf65209 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Wed Jul 03 23:42:07 2013 +0200 +++ b/src/Tools/Code/code_scala.ML Thu Jul 04 08:52:44 2013 +0200 @@ -260,7 +260,7 @@ let val tyvars = intro_tyvars vs reserved; val classtyp = (class, tyco `%% map (ITyVar o fst) vs); - fun print_classparam_instance ((classparam, const as { dom, ... }), (thm, _)) = + fun print_classparam_instance ((classparam, (const as { dom, ... }, _)), (thm, _)) = let val aux_dom = Name.invent_names (snd reserved) "a" dom; val auxs = map fst aux_dom; diff -r c9a9359e0285 -r 598addf65209 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Jul 03 23:42:07 2013 +0200 +++ b/src/Tools/Code/code_thingol.ML Thu Jul 04 08:52:44 2013 +0200 @@ -78,8 +78,8 @@ | Classparam of string * class | Classinst of { class: string, tyco: string, vs: (vname * sort) list, superinsts: (class * (string * (string * dict list list))) list, - inst_params: ((string * const) * (thm * bool)) list, - superinst_params: ((string * const) * (thm * bool)) list }; + inst_params: ((string * (const * int)) * (thm * bool)) list, + superinst_params: ((string * (const * int)) * (thm * bool)) list }; type program = stmt Graph.T val empty_funs: program -> string list val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm @@ -428,8 +428,8 @@ | Classparam of string * class | Classinst of { class: string, tyco: string, vs: (vname * sort) list, superinsts: (class * (string * (string * dict list list))) list, - inst_params: ((string * const) * (thm * bool)) list, - superinst_params: ((string * const) * (thm * bool)) list }; + inst_params: ((string * (const * int)) * (thm * bool)) list, + superinst_params: ((string * (const * int)) * (thm * bool)) list }; type program = stmt Graph.T; @@ -448,7 +448,7 @@ primitive = map_terms_bottom_up f t0 }); fun map_classparam_instances_as_term f = - (map o apfst o apsnd) (fn const => case f (IConst const) of IConst const' => const') + (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const') fun map_terms_stmt f NoStmt = NoStmt | map_terms_stmt f (Fun (c, ((tysm, eqs), case_cong))) = Fun (c, ((tysm, (map o apfst) @@ -708,13 +708,14 @@ fun translate_classparam_instance (c, ty) = let val raw_const = Const (c, map_type_tfree (K arity_typ') ty); + val dom_length = length (fst (strip_type ty)) val thm = Axclass.unoverload_conv thy (Thm.cterm_of thy raw_const); val const = (apsnd Logic.unvarifyT_global o dest_Const o snd o Logic.dest_equals o Thm.prop_of) thm; in ensure_const thy algbr eqngr permissive c ##>> translate_const thy algbr eqngr permissive (SOME thm) (const, NONE) - #>> (fn (c, IConst const') => ((c, const'), (thm, true))) + #>> (fn (c, IConst const') => ((c, (const', dom_length)), (thm, true))) end; val stmt_inst = ensure_class thy algbr eqngr permissive class diff -r c9a9359e0285 -r 598addf65209 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Jul 03 23:42:07 2013 +0200 +++ b/src/Tools/nbe.ML Thu Jul 04 08:52:44 2013 +0200 @@ -439,7 +439,7 @@ | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) = [(inst, (vs, [([], dummy_const class [] `$$ map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts - @ map (IConst o snd o fst) inst_params)]))]; + @ map (IConst o fst o snd o fst) inst_params)]))]; (* compile whole programs *)