# HG changeset patch # User Andreas Lochbihler # Date 1372922029 -7200 # Node ID 9a2cd366a322013747d91bbffdb9224a08bcf3f2 # Parent a1c4f586e3726d12d94a60d0d901cfd5b3a8fa5f# Parent 4a884366b0d86c9c910fd55600819251dd849a6b merged diff -r a1c4f586e372 -r 9a2cd366a322 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Wed Jul 03 00:08:29 2013 +0200 +++ b/src/Tools/Code/code_haskell.ML Thu Jul 04 09:13:49 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 a1c4f586e372 -r 9a2cd366a322 src/Tools/Code/code_ml.ML --- a/src/Tools/Code/code_ml.ML Wed Jul 03 00:08:29 2013 +0200 +++ b/src/Tools/Code/code_ml.ML Thu Jul 04 09:13:49 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 a1c4f586e372 -r 9a2cd366a322 src/Tools/Code/code_scala.ML --- a/src/Tools/Code/code_scala.ML Wed Jul 03 00:08:29 2013 +0200 +++ b/src/Tools/Code/code_scala.ML Thu Jul 04 09:13:49 2013 +0200 @@ -260,17 +260,21 @@ 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, ... }, dom_length)), (thm, _)) = let val aux_dom = Name.invent_names (snd reserved) "a" dom; val auxs = map fst aux_dom; val vars = intro_vars auxs reserved; - val aux_abstr = if null auxs then [] else [enum "," "(" ")" - (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux) - (print_typ tyvars NOBR ty)) aux_dom), str "=>"]; + val (aux_dom1, aux_dom2) = chop dom_length aux_dom; + fun abstract_using [] = [] + | abstract_using aux_dom = [enum "," "(" ")" + (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux) + (print_typ tyvars NOBR ty)) aux_dom), str "=>"]; + val aux_abstr1 = abstract_using aux_dom1; + val aux_abstr2 = abstract_using aux_dom2; in concat ([str "val", print_method classparam, str "="] - @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR + @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)) end; in diff -r a1c4f586e372 -r 9a2cd366a322 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Jul 03 00:08:29 2013 +0200 +++ b/src/Tools/Code/code_thingol.ML Thu Jul 04 09:13:49 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 a1c4f586e372 -r 9a2cd366a322 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Jul 03 00:08:29 2013 +0200 +++ b/src/Tools/nbe.ML Thu Jul 04 09:13:49 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 *)