# HG changeset patch # User haftmann # Date 1241618466 -7200 # Node ID 396d4d6a1594f468b9db30dbed42a19f3d2fbd95 # Parent ac146fc38b5114af9544216e1760b140d96f400c explicit type arguments in constants diff -r ac146fc38b51 -r 396d4d6a1594 src/Tools/code/code_haskell.ML --- a/src/Tools/code/code_haskell.ML Wed May 06 16:01:06 2009 +0200 +++ b/src/Tools/code/code_haskell.ML Wed May 06 16:01:06 2009 +0200 @@ -261,7 +261,7 @@ val vars = init_syms |> Code_Printer.intro_vars (the_list const) |> Code_Printer.intro_vars vs; - val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs; + val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs; (*dictionaries are not relevant at this late stage*) in semicolon [ diff -r ac146fc38b51 -r 396d4d6a1594 src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Wed May 06 16:01:06 2009 +0200 +++ b/src/Tools/code/code_ml.ML Wed May 06 16:01:06 2009 +0200 @@ -109,7 +109,7 @@ then pr_case is_closure thm vars fxy cases else pr_app is_closure thm vars fxy c_ts | NONE => pr_case is_closure thm vars fxy cases) - and pr_app' is_closure thm vars (app as ((c, (iss, tys)), ts)) = + and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) = if is_cons c then let val k = length tys @@ -414,7 +414,7 @@ then pr_case is_closure thm vars fxy cases else pr_app is_closure thm vars fxy c_ts | NONE => pr_case is_closure thm vars fxy cases) - and pr_app' is_closure thm vars (app as ((c, (iss, tys)), ts)) = + and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) = if is_cons c then if length tys = length ts then case ts diff -r ac146fc38b51 -r 396d4d6a1594 src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Wed May 06 16:01:06 2009 +0200 +++ b/src/Tools/code/code_thingol.ML Wed May 06 16:01:06 2009 +0200 @@ -20,7 +20,7 @@ datatype itype = `%% of string * itype list | ITyVar of vname; - type const = string * (dict list list * itype list (*types of arguments*)) + type const = string * ((itype list * dict list list) * itype list (*types of arguments*)) datatype iterm = IConst of const | IVar of vname @@ -44,11 +44,10 @@ val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm - val unfold_const_app: iterm -> - ((string * (dict list list * itype list)) * iterm list) option + val unfold_const_app: iterm -> (const * iterm list) option val collapse_let: ((vname * itype) * iterm) * iterm -> (iterm * itype) * (iterm * iterm) list - val eta_expand: int -> (string * (dict list list * itype list)) * iterm list -> iterm + val eta_expand: int -> const * iterm list -> iterm val contains_dictvar: iterm -> bool val locally_monomorphic: iterm -> bool val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a @@ -122,7 +121,7 @@ `%% of string * itype list | ITyVar of vname; -type const = string * (dict list list * itype list (*types of arguments*)) +type const = string * ((itype list * dict list list) * itype list (*types of arguments*)) datatype iterm = IConst of const @@ -212,7 +211,7 @@ | contains (DictVar _) = K true; in fold_aiterms - (fn IConst (_, (dss, _)) => (fold o fold) contains dss | _ => I) t false + (fn IConst (_, ((_, dss), _)) => (fold o fold) contains dss | _ => I) t false end; fun locally_monomorphic (IConst _) = false @@ -602,9 +601,10 @@ val tys_args = (fst o Term.strip_type) ty; in ensure_const thy algbr funcgr c + ##>> fold_map (translate_typ thy algbr funcgr) tys ##>> fold_map (translate_dicts thy algbr funcgr thm) (tys ~~ sorts) ##>> fold_map (translate_typ thy algbr funcgr) tys_args - #>> (fn ((c, iss), tys) => IConst (c, (iss, tys))) + #>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args))) end and translate_app_const thy algbr funcgr thm (c_ty, ts) = translate_const thy algbr funcgr thm c_ty diff -r ac146fc38b51 -r 396d4d6a1594 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed May 06 16:01:06 2009 +0200 +++ b/src/Tools/nbe.ML Wed May 06 16:01:06 2009 +0200 @@ -194,7 +194,7 @@ let val (t', ts) = Code_Thingol.unfold_app t in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end - and of_iapp match_cont (IConst (c, (dss, _))) ts = constapp c dss ts + and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts | of_iapp match_cont ((v, _) `|-> t) ts = nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts @@ -299,15 +299,15 @@ val params = Name.invent_list [] "d" (length names); fun mk (k, name) = (name, ([(v, [])], - [([IConst (class, ([], [])) `$$ map IVar params], IVar (nth params k))])); + [([IConst (class, (([], []), [])) `$$ map IVar params], IVar (nth params k))])); in map_index mk names end | eqns_of_stmt (_, Code_Thingol.Classrel _) = [] | eqns_of_stmt (_, Code_Thingol.Classparam _) = [] | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) = - [(inst, (arities, [([], IConst (class, ([], [])) `$$ - map (fn (_, (_, (inst, dicts))) => IConst (inst, (dicts, []))) superinsts + [(inst, (arities, [([], IConst (class, (([], []), [])) `$$ + map (fn (_, (_, (inst, dicts))) => IConst (inst, (([], dicts), []))) superinsts @ map (IConst o snd o fst) instops)]))]; fun compile_stmts ctxt stmts_deps =