# HG changeset patch # User bulwahn # Date 1315396295 -7200 # Node ID 26b19918e670c1b1ac1c462571912ca23b553b16 # Parent 7ecb4124a3a3935b6925401c7d9faa89fe8a4cce adding minimalistic implementation for printing the type annotations diff -r 7ecb4124a3a3 -r 26b19918e670 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Wed Sep 07 13:51:34 2011 +0200 +++ b/src/Tools/Code/code_haskell.ML Wed Sep 07 13:51:35 2011 +0200 @@ -75,20 +75,14 @@ then print_case tyvars some_thm vars fxy cases else print_app tyvars some_thm vars fxy c_ts | NONE => print_case tyvars some_thm vars fxy cases) - and print_app_expr tyvars some_thm vars ((c, ((_, (function_typs, _)), _)), ts) = case contr_classparam_typs c - of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts - | fingerprint => let - val ts_fingerprint = ts ~~ take (length ts) fingerprint; - val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) => - (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint; - fun print_term_anno (t, NONE) _ = print_term tyvars some_thm vars BR t - | print_term_anno (t, SOME _) ty = - brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty]; - in - if needs_annotation then - (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs) - else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts - end + and print_app_expr tyvars some_thm vars ((c, ((_, (function_typs, body_typ)), annotate)), ts) = + let + val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (function_typs, body_typ) + fun put_annotation c = brackets [c, str "::", print_typ tyvars NOBR ty] + in + ((if annotate then put_annotation else I) + ((str o deresolve) c)) :: map (print_term tyvars some_thm vars BR) ts + end and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = diff -r 7ecb4124a3a3 -r 26b19918e670 src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Sep 07 13:51:34 2011 +0200 +++ b/src/Tools/Code/code_thingol.ML Wed Sep 07 13:51:35 2011 +0200 @@ -786,16 +786,17 @@ then translation_error thy permissive some_thm "Abstraction violation" ("constant " ^ Code.string_of_const thy c) else () - val arg_typs = Sign.const_typargs thy (c, ty); + val (annotate, ty') = (case ty of Type("", [ty']) => (true, ty') | ty' => (false, ty')) + val arg_typs = Sign.const_typargs thy (c, ty'); val sorts = Code_Preproc.sortargs eqngr c; - val (function_typs, body_typ) = Term.strip_type ty; + val (function_typs, body_typ) = Term.strip_type ty'; in ensure_const thy algbr eqngr permissive c ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts) ##>> fold_map (translate_typ thy algbr eqngr permissive) (body_typ :: function_typs) #>> (fn (((c, arg_typs), dss), body_typ :: function_typs) => - IConst (c, (((arg_typs, dss), (function_typs, body_typ)), false))) (* FIXME *) + IConst (c, (((arg_typs, dss), (function_typs, body_typ)), annotate))) end and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) = translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)