src/Tools/Code/code_haskell.ML
changeset 48072 ace701efe203
parent 48003 1d11af40b106
child 48431 6efff142bb54
     1.1 --- a/src/Tools/Code/code_haskell.ML	Mon Jun 04 12:55:54 2012 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Tue Jun 05 07:05:56 2012 +0200
     1.3 @@ -60,8 +60,8 @@
     1.4        print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
     1.5      fun print_typscheme tyvars (vs, ty) =
     1.6        Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
     1.7 -    fun print_term tyvars some_thm vars fxy (IConst c) =
     1.8 -          print_app tyvars some_thm vars fxy (c, [])
     1.9 +    fun print_term tyvars some_thm vars fxy (IConst const) =
    1.10 +          print_app tyvars some_thm vars fxy (const, [])
    1.11        | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
    1.12            (case Code_Thingol.unfold_const_app t
    1.13             of SOME app => print_app tyvars some_thm vars fxy app
    1.14 @@ -79,15 +79,15 @@
    1.15              val (binds, t') = Code_Thingol.unfold_pat_abs t;
    1.16              val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
    1.17            in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
    1.18 -      | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
    1.19 -          (case Code_Thingol.unfold_const_app t0
    1.20 -           of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
    1.21 -                then print_case tyvars some_thm vars fxy cases
    1.22 -                else print_app tyvars some_thm vars fxy c_ts
    1.23 -            | NONE => print_case tyvars some_thm vars fxy cases)
    1.24 -    and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
    1.25 +      | print_term tyvars some_thm vars fxy (ICase case_expr) =
    1.26 +          (case Code_Thingol.unfold_const_app (#primitive case_expr)
    1.27 +           of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
    1.28 +                then print_case tyvars some_thm vars fxy case_expr
    1.29 +                else print_app tyvars some_thm vars fxy app
    1.30 +            | NONE => print_case tyvars some_thm vars fxy case_expr)
    1.31 +    and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
    1.32        let
    1.33 -        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
    1.34 +        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
    1.35          val printed_const =
    1.36            if annotate then
    1.37              brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
    1.38 @@ -98,9 +98,11 @@
    1.39        end
    1.40      and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
    1.41      and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
    1.42 -    and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
    1.43 +    and print_case tyvars some_thm vars fxy { clauses = [], ... } =
    1.44 +          (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
    1.45 +      | print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
    1.46            let
    1.47 -            val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    1.48 +            val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
    1.49              fun print_match ((pat, _), t) vars =
    1.50                vars
    1.51                |> print_bind tyvars some_thm BR pat
    1.52 @@ -110,7 +112,7 @@
    1.53              ps
    1.54              (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
    1.55            end
    1.56 -      | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
    1.57 +      | print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
    1.58            let
    1.59              fun print_select (pat, body) =
    1.60                let
    1.61 @@ -119,9 +121,7 @@
    1.62            in Pretty.block_enclose
    1.63              (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
    1.64              (map print_select clauses)
    1.65 -          end
    1.66 -      | print_case tyvars some_thm vars fxy ((_, []), _) =
    1.67 -          (brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
    1.68 +          end;
    1.69      fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
    1.70            let
    1.71              val tyvars = intro_vars (map fst vs) reserved;
    1.72 @@ -221,7 +221,7 @@
    1.73                str "};"
    1.74              ) (map print_classparam classparams)
    1.75            end
    1.76 -      | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
    1.77 +      | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
    1.78            let
    1.79              val tyvars = intro_vars (map fst vs) reserved;
    1.80              fun requires_args classparam = case const_syntax classparam
    1.81 @@ -237,14 +237,15 @@
    1.82                      ]
    1.83                  | SOME k =>
    1.84                      let
    1.85 -                      val (c, ((_, tys), _)) = const;
    1.86 +                      val { name = c, dom, range, ... } = const;
    1.87                        val (vs, rhs) = (apfst o map) fst
    1.88                          (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
    1.89                        val s = if (is_some o const_syntax) c
    1.90                          then NONE else (SOME o Long_Name.base_name o deresolve) c;
    1.91                        val vars = reserved
    1.92                          |> intro_vars (map_filter I (s :: vs));
    1.93 -                      val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
    1.94 +                      val lhs = IConst { name = classparam, typargs = [],
    1.95 +                        dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
    1.96                          (*dictionaries are not relevant at this late stage,
    1.97                            and these consts never need type annotations for disambiguation *)
    1.98                      in
    1.99 @@ -264,7 +265,7 @@
   1.100                  str " where {"
   1.101                ],
   1.102                str "};"
   1.103 -            ) (map print_classparam_instance classparam_instances)
   1.104 +            ) (map print_classparam_instance inst_params)
   1.105            end;
   1.106    in print_stmt end;
   1.107  
   1.108 @@ -407,7 +408,7 @@
   1.109       of SOME ((pat, ty), t') =>
   1.110            SOME ((SOME ((pat, ty), true), t1), t')
   1.111        | NONE => NONE;
   1.112 -    fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
   1.113 +    fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
   1.114            if c = c_bind_name then dest_bind t1 t2
   1.115            else NONE
   1.116        | dest_monad _ t = case Code_Thingol.split_let t