syntactic improvements and tuning names in the code generator due to Florian's code review
authorbulwahn
Tue Sep 20 09:30:19 2011 +0200 (2011-09-20)
changeset 4500999e1965f9c21
parent 45008 8b74cfea913a
child 45010 8a4db903039f
syntactic improvements and tuning names in the code generator due to Florian's code review
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Tue Sep 20 01:32:04 2011 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Sep 20 09:30:19 2011 +0200
     1.3 @@ -85,13 +85,16 @@
     1.4                  then print_case tyvars some_thm vars fxy cases
     1.5                  else print_app tyvars some_thm vars fxy c_ts
     1.6              | NONE => print_case tyvars some_thm vars fxy cases)
     1.7 -    and print_app_expr tyvars some_thm vars ((c, ((_, (function_typs, body_typ)), annotate)), ts) =
     1.8 +    and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
     1.9        let
    1.10 -        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (function_typs, body_typ)
    1.11 -        fun put_annotation c = brackets [c, str "::", print_typ tyvars NOBR ty]
    1.12 +        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
    1.13 +        val printed_const =
    1.14 +          if annotate then
    1.15 +            brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
    1.16 +          else
    1.17 +            (str o deresolve) c
    1.18        in 
    1.19 -        ((if annotate then put_annotation else I)
    1.20 -          ((str o deresolve) c)) :: map (print_term tyvars some_thm vars BR) ts
    1.21 +        printed_const :: map (print_term tyvars some_thm vars BR) ts
    1.22        end
    1.23      and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
    1.24      and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
    1.25 @@ -234,15 +237,16 @@
    1.26                      ]
    1.27                  | SOME k =>
    1.28                      let
    1.29 -                      val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *)
    1.30 +                      val (c, ((_, tys), _)) = const;
    1.31                        val (vs, rhs) = (apfst o map) fst
    1.32                          (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
    1.33                        val s = if (is_some o const_syntax) c
    1.34                          then NONE else (SOME o Long_Name.base_name o deresolve) c;
    1.35                        val vars = reserved
    1.36                          |> intro_vars (map_filter I (s :: vs));
    1.37 -                      val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs;
    1.38 -                        (*dictionaries are not relevant at this late stage*)
    1.39 +                      val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
    1.40 +                        (*dictionaries are not relevant at this late stage,
    1.41 +                          and these consts never need type annotations for disambiguation *)
    1.42                      in
    1.43                        semicolon [
    1.44                          print_term tyvars (SOME thm) vars NOBR lhs,
    1.45 @@ -323,8 +327,7 @@
    1.46        in deriv [] tyco end;
    1.47      fun print_stmt deresolve = print_haskell_stmt labelled_name
    1.48        class_syntax tyco_syntax const_syntax (make_vars reserved)
    1.49 -      deresolve
    1.50 -      (if string_classes then deriving_show else K false);
    1.51 +      deresolve (if string_classes then deriving_show else K false);
    1.52  
    1.53      (* print modules *)
    1.54      val import_includes_ps =
     2.1 --- a/src/Tools/Code/code_ml.ML	Tue Sep 20 01:32:04 2011 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Tue Sep 20 09:30:19 2011 +0200
     2.3 @@ -117,9 +117,9 @@
     2.4                  then print_case is_pseudo_fun some_thm vars fxy cases
     2.5                  else print_app is_pseudo_fun some_thm vars fxy c_ts
     2.6              | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
     2.7 -    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (function_typs, _)), _)), ts)) =
     2.8 +    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (arg_tys, _)), _)), ts)) =
     2.9        if is_cons c then
    2.10 -        let val k = length function_typs in
    2.11 +        let val k = length arg_tys in
    2.12            if k < 2 orelse length ts = k
    2.13            then (str o deresolve) c
    2.14              :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
     3.1 --- a/src/Tools/Code/code_printer.ML	Tue Sep 20 01:32:04 2011 +0200
     3.2 +++ b/src/Tools/Code/code_printer.ML	Tue Sep 20 09:30:19 2011 +0200
     3.3 @@ -315,7 +315,7 @@
     3.4        |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
     3.5  
     3.6  fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
     3.7 -    (app as ((c, ((_, (function_typs, _)), _)), ts)) =
     3.8 +    (app as ((c, ((_, (arg_tys, _)), _)), ts)) =
     3.9    case const_syntax c of
    3.10      NONE => brackify fxy (print_app_expr some_thm vars app)
    3.11    | SOME (Plain_const_syntax (_, s)) =>
    3.12 @@ -323,7 +323,7 @@
    3.13    | SOME (Complex_const_syntax (k, print)) =>
    3.14        let
    3.15          fun print' fxy ts =
    3.16 -          print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
    3.17 +          print (print_term some_thm) some_thm vars fxy (ts ~~ take k arg_tys);
    3.18        in
    3.19          if k = length ts
    3.20          then print' fxy ts
     4.1 --- a/src/Tools/Code/code_scala.ML	Tue Sep 20 01:32:04 2011 +0200
     4.2 +++ b/src/Tools/Code/code_scala.ML	Tue Sep 20 09:30:19 2011 +0200
     4.3 @@ -72,23 +72,23 @@
     4.4                  else print_app tyvars is_pat some_thm vars fxy c_ts
     4.5              | NONE => print_case tyvars some_thm vars fxy cases)
     4.6      and print_app tyvars is_pat some_thm vars fxy
     4.7 -        (app as ((c, (((arg_typs, _), (function_typs, _)), _)), ts)) =
     4.8 +        (app as ((c, (((tys, _), (arg_tys, _)), _)), ts)) =
     4.9        let
    4.10          val k = length ts;
    4.11 -        val arg_typs' = if is_pat orelse
    4.12 -          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else arg_typs;
    4.13 +        val tys' = if is_pat orelse
    4.14 +          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else tys;
    4.15          val (l, print') = case const_syntax c
    4.16           of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
    4.17                (print_term tyvars is_pat some_thm vars NOBR) fxy
    4.18                  (applify "[" "]" (print_typ tyvars NOBR)
    4.19 -                  NOBR ((str o deresolve) c) arg_typs') ts)
    4.20 +                  NOBR ((str o deresolve) c) tys') ts)
    4.21            | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
    4.22                (print_term tyvars is_pat some_thm vars NOBR) fxy
    4.23                  (applify "[" "]" (print_typ tyvars NOBR)
    4.24 -                  NOBR (str s) arg_typs') ts)
    4.25 +                  NOBR (str s) tys') ts)
    4.26            | SOME (Complex_const_syntax (k, print)) =>
    4.27                (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
    4.28 -                (ts ~~ take k function_typs))
    4.29 +                (ts ~~ take k arg_tys))
    4.30        in if k = l then print' fxy ts
    4.31        else if k < l then
    4.32          print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
     5.1 --- a/src/Tools/Code/code_thingol.ML	Tue Sep 20 01:32:04 2011 +0200
     5.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Sep 20 09:30:19 2011 +0200
     5.3 @@ -23,7 +23,7 @@
     5.4        `%% of string * itype list
     5.5      | ITyVar of vname;
     5.6    type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
     5.7 -    (* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
     5.8 +    (* (f [T1..Tn] {dicts} (_::S1) .. (_::Sm)) :: S =^= (f, ((([T1..Tn], dicts), ([S1..Sm], S)), ambiguous)) *)
     5.9    datatype iterm =
    5.10        IConst of const
    5.11      | IVar of vname option
    5.12 @@ -144,7 +144,7 @@
    5.13    | ITyVar of vname;
    5.14  
    5.15  type const = string * (((itype list * dict list list) *
    5.16 -  (itype list (*types of arguments*) * itype (*body type*))) * bool (*requires type annotation*))
    5.17 +  (itype list (*types of arguments*) * itype (*result type*))) * bool (*requires type annotation*))
    5.18  
    5.19  datatype iterm =
    5.20      IConst of const